%---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------% ------ Parsing...successful ------ Proving... use I- Gamma_0: (extend-no-conflict) 0: says(asked,or(isa(asked,knight),isa(other,knight))), [says( asked,not(or(isa(asked,knight),isa(other,knight))))] Gamma_1: (extend-no-conflict) 0: says(asked,or(isa(asked,knight),isa(other,knight))), [says( asked,not(or(isa(asked,knight),isa(other,knight))))] 1: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), truth( or(isa(asked,knight),isa(other,knight))), [truth(not(or(isa(asked,knight),isa(other,knight))))] Gamma_2: (extend-no-conflict) 0: says(asked,or(isa(asked,knight),isa(other,knight))), [says( asked,not(or(isa(asked,knight),isa(other,knight))))] 1: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), truth( or(isa(asked,knight),isa(other,knight))), [truth(not(or(isa(asked,knight),isa(other,knight))))] 2: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [truth( isa(asked,knight))], ~(truth(not(or(isa(asked,knight),isa(other,knight))))) Gamma_3: (extend-conflict) 0: says(asked,or(isa(asked,knight),isa(other,knight))), [says( asked,not(or(isa(asked,knight),isa(other,knight))))] 1: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), truth( or(isa(asked,knight),isa(other,knight))), [truth(not(or(isa(asked,knight),isa(other,knight))))] 2: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [truth( isa(asked,knight))], ~(truth(not(or(isa(asked,knight),isa(other,knight))))) 3: [~(truth(isa(asked,knight)))], ~(truth(not(or(isa(asked,knight),isa(other,knight))))) Gamma_4: (move) 0: says(asked,or(isa(asked,knight),isa(other,knight))), [says( asked,not(or(isa(asked,knight),isa(other,knight))))] 1: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), truth( or(isa(asked,knight),isa(other,knight))), [truth(not(or(isa(asked,knight),isa(other,knight))))] 2: [~(truth(isa(asked,knight)))], ~(truth(not(or(isa(asked,knight),isa(other,knight))))) 3: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [truth( isa(asked,knight))], ~(truth(not(or(isa(asked,knight),isa(other,knight))))) Gamma_5: (resolve) 0: says(asked,or(isa(asked,knight),isa(other,knight))), [says( asked,not(or(isa(asked,knight),isa(other,knight))))] 1: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), truth( or(isa(asked,knight),isa(other,knight))), [truth(not(or(isa(asked,knight),isa(other,knight))))] 2: [~(truth(isa(asked,knight)))], ~(truth(not(or(isa(asked,knight),isa(other,knight))))) 3: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))], ~( truth(not(or(isa(asked,knight),isa(other,knight))))) Gamma_6: (extend-conflict) 0: says(asked,or(isa(asked,knight),isa(other,knight))), [says( asked,not(or(isa(asked,knight),isa(other,knight))))] 1: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), truth( or(isa(asked,knight),isa(other,knight))), [truth(not(or(isa(asked,knight),isa(other,knight))))] 2: [~(truth(isa(asked,knight)))], ~(truth(not(or(isa(asked,knight),isa(other,knight))))) 3: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(not(or(isa(asked,knight),isa(other,knight)))))] Gamma_7: (move) 0: says(asked,or(isa(asked,knight),isa(other,knight))), [says( asked,not(or(isa(asked,knight),isa(other,knight))))] 1: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(not(or(isa(asked,knight),isa(other,knight)))))] 2: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), truth( or(isa(asked,knight),isa(other,knight))), [truth(not(or(isa(asked,knight),isa(other,knight))))] 3: [~(truth(isa(asked,knight)))], ~(truth(not(or(isa(asked,knight),isa(other,knight))))) Gamma_8: (resolve) 0: says(asked,or(isa(asked,knight),isa(other,knight))), [says( asked,not(or(isa(asked,knight),isa(other,knight))))] 1: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(not(or(isa(asked,knight),isa(other,knight)))))] 2: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))], truth( or(isa(asked,knight),isa(other,knight))) Gamma_9: (extend-no-conflict) 0: says(asked,or(isa(asked,knight),isa(other,knight))), [says( asked,not(or(isa(asked,knight),isa(other,knight))))] 1: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(not(or(isa(asked,knight),isa(other,knight)))))] 2: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [truth( or(isa(asked,knight),isa(other,knight)))] Gamma_10: (extend-no-conflict) 0: says(asked,or(isa(asked,knight),isa(other,knight))), [says( asked,not(or(isa(asked,knight),isa(other,knight))))] 1: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(not(or(isa(asked,knight),isa(other,knight)))))] 2: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [truth( or(isa(asked,knight),isa(other,knight)))] 3: [truth(isa(other,knight))], truth(isa(asked,knight)), ~(truth(or(isa(asked,knight),isa(other,knight)))) Gamma_11: (extend-no-conflict) 0: says(asked,or(isa(asked,knight),isa(other,knight))), [says( asked,not(or(isa(asked,knight),isa(other,knight))))] 1: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(not(or(isa(asked,knight),isa(other,knight)))))] 2: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [truth( or(isa(asked,knight),isa(other,knight)))] 3: [truth(isa(other,knight))], truth(isa(asked,knight)), ~(truth(or(isa(asked,knight),isa(other,knight)))) 4: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), truth( not(or(isa(asked,knight),isa(other,knight)))), [truth(not(not(or(isa(asked,knight),isa(other,knight)))))] Gamma_12: (extend-no-conflict) 0: says(asked,or(isa(asked,knight),isa(other,knight))), [says( asked,not(or(isa(asked,knight),isa(other,knight))))] 1: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(not(or(isa(asked,knight),isa(other,knight)))))] 2: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [truth( or(isa(asked,knight),isa(other,knight)))] 3: [truth(isa(other,knight))], truth(isa(asked,knight)), ~(truth(or(isa(asked,knight),isa(other,knight)))) 4: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), truth( not(or(isa(asked,knight),isa(other,knight)))), [truth(not(not(or(isa(asked,knight),isa(other,knight)))))] 5: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [truth( isa(asked,knave))], ~(truth(not(not(or(isa(asked,knight),isa(other,knight)))))) Gamma_13: (extend-conflict) 0: says(asked,or(isa(asked,knight),isa(other,knight))), [says( asked,not(or(isa(asked,knight),isa(other,knight))))] 1: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(not(or(isa(asked,knight),isa(other,knight)))))] 2: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [truth( or(isa(asked,knight),isa(other,knight)))] 3: [truth(isa(other,knight))], truth(isa(asked,knight)), ~(truth(or(isa(asked,knight),isa(other,knight)))) 4: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), truth( not(or(isa(asked,knight),isa(other,knight)))), [truth(not(not(or(isa(asked,knight),isa(other,knight)))))] 5: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [truth( isa(asked,knave))], ~(truth(not(not(or(isa(asked,knight),isa(other,knight)))))) 6: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), ~(truth(isa(other,knight))), [~( truth(isa(asked,knave)))] Gamma_14: (move) 0: says(asked,or(isa(asked,knight),isa(other,knight))), [says( asked,not(or(isa(asked,knight),isa(other,knight))))] 1: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(not(or(isa(asked,knight),isa(other,knight)))))] 2: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [truth( or(isa(asked,knight),isa(other,knight)))] 3: [truth(isa(other,knight))], truth(isa(asked,knight)), ~(truth(or(isa(asked,knight),isa(other,knight)))) 4: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), truth( not(or(isa(asked,knight),isa(other,knight)))), [truth(not(not(or(isa(asked,knight),isa(other,knight)))))] 5: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), ~(truth(isa(other,knight))), [~( truth(isa(asked,knave)))] 6: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [truth( isa(asked,knave))], ~(truth(not(not(or(isa(asked,knight),isa(other,knight)))))) Gamma_15: (resolve) 0: says(asked,or(isa(asked,knight),isa(other,knight))), [says( asked,not(or(isa(asked,knight),isa(other,knight))))] 1: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(not(or(isa(asked,knight),isa(other,knight)))))] 2: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [truth( or(isa(asked,knight),isa(other,knight)))] 3: [truth(isa(other,knight))], truth(isa(asked,knight)), ~(truth(or(isa(asked,knight),isa(other,knight)))) 4: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), truth( not(or(isa(asked,knight),isa(other,knight)))), [truth(not(not(or(isa(asked,knight),isa(other,knight)))))] 5: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), ~(truth(isa(other,knight))), [~( truth(isa(asked,knave)))] 6: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))], ~( truth(isa(other,knight))), ~(truth(not(not(or(isa(asked,knight),isa(other,knight)))))) Gamma_16: (extend-conflict) 0: says(asked,or(isa(asked,knight),isa(other,knight))), [says( asked,not(or(isa(asked,knight),isa(other,knight))))] 1: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(not(or(isa(asked,knight),isa(other,knight)))))] 2: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [truth( or(isa(asked,knight),isa(other,knight)))] 3: [truth(isa(other,knight))], truth(isa(asked,knight)), ~(truth(or(isa(asked,knight),isa(other,knight)))) 4: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), truth( not(or(isa(asked,knight),isa(other,knight)))), [truth(not(not(or(isa(asked,knight),isa(other,knight)))))] 5: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), ~(truth(isa(other,knight))), [~( truth(isa(asked,knave)))] 6: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), ~(truth(isa(other,knight))), [~( truth(not(not(or(isa(asked,knight),isa(other,knight))))))] Gamma_17: (move) 0: says(asked,or(isa(asked,knight),isa(other,knight))), [says( asked,not(or(isa(asked,knight),isa(other,knight))))] 1: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(not(or(isa(asked,knight),isa(other,knight)))))] 2: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [truth( or(isa(asked,knight),isa(other,knight)))] 3: [truth(isa(other,knight))], truth(isa(asked,knight)), ~(truth(or(isa(asked,knight),isa(other,knight)))) 4: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), ~(truth(isa(other,knight))), [~( truth(not(not(or(isa(asked,knight),isa(other,knight))))))] 5: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), truth( not(or(isa(asked,knight),isa(other,knight)))), [truth(not(not(or(isa(asked,knight),isa(other,knight)))))] 6: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), ~(truth(isa(other,knight))), [~( truth(isa(asked,knave)))] Gamma_18: (resolve) 0: says(asked,or(isa(asked,knight),isa(other,knight))), [says( asked,not(or(isa(asked,knight),isa(other,knight))))] 1: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(not(or(isa(asked,knight),isa(other,knight)))))] 2: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [truth( or(isa(asked,knight),isa(other,knight)))] 3: [truth(isa(other,knight))], truth(isa(asked,knight)), ~(truth(or(isa(asked,knight),isa(other,knight)))) 4: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), ~(truth(isa(other,knight))), [~( truth(not(not(or(isa(asked,knight),isa(other,knight))))))] 5: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))], ~( truth(isa(other,knight))), truth(not(or(isa(asked,knight),isa(other,knight)))) 6: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), ~(truth(isa(other,knight))), [~( truth(isa(asked,knave)))] Gamma_19: (extend-conflict) 0: says(asked,or(isa(asked,knight),isa(other,knight))), [says( asked,not(or(isa(asked,knight),isa(other,knight))))] 1: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(not(or(isa(asked,knight),isa(other,knight)))))] 2: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [truth( or(isa(asked,knight),isa(other,knight)))] 3: [truth(isa(other,knight))], truth(isa(asked,knight)), ~(truth(or(isa(asked,knight),isa(other,knight)))) 4: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), ~(truth(isa(other,knight))), [~( truth(not(not(or(isa(asked,knight),isa(other,knight))))))] 5: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(isa(other,knight)))], truth(not(or(isa(asked,knight),isa(other,knight)))) 6: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), ~(truth(isa(other,knight))), [~( truth(isa(asked,knave)))] Gamma_20: (move) 0: says(asked,or(isa(asked,knight),isa(other,knight))), [says( asked,not(or(isa(asked,knight),isa(other,knight))))] 1: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(not(or(isa(asked,knight),isa(other,knight)))))] 2: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [truth( or(isa(asked,knight),isa(other,knight)))] 3: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(isa(other,knight)))], truth(not(or(isa(asked,knight),isa(other,knight)))) 4: [truth(isa(other,knight))], truth(isa(asked,knight)), ~(truth(or(isa(asked,knight),isa(other,knight)))) 5: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), ~(truth(isa(other,knight))), [~( truth(not(not(or(isa(asked,knight),isa(other,knight))))))] 6: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), ~(truth(isa(other,knight))), [~( truth(isa(asked,knave)))] Gamma_21: (resolve) 0: says(asked,or(isa(asked,knight),isa(other,knight))), [says( asked,not(or(isa(asked,knight),isa(other,knight))))] 1: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(not(or(isa(asked,knight),isa(other,knight)))))] 2: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [truth( or(isa(asked,knight),isa(other,knight)))] 3: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(isa(other,knight)))], truth(not(or(isa(asked,knight),isa(other,knight)))) 4: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [truth( isa(asked,knight))], ~(truth(or(isa(asked,knight),isa(other,knight)))), truth( not(or(isa(asked,knight),isa(other,knight)))) Gamma_22: (extend-no-conflict) 0: says(asked,or(isa(asked,knight),isa(other,knight))), [says( asked,not(or(isa(asked,knight),isa(other,knight))))] 1: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(not(or(isa(asked,knight),isa(other,knight)))))] 2: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [truth( or(isa(asked,knight),isa(other,knight)))] 3: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(isa(other,knight)))], truth(not(or(isa(asked,knight),isa(other,knight)))) 4: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [truth( isa(asked,knight))], ~(truth(or(isa(asked,knight),isa(other,knight)))), truth( not(or(isa(asked,knight),isa(other,knight)))) Gamma_23: (extend-conflict) 0: says(asked,or(isa(asked,knight),isa(other,knight))), [says( asked,not(or(isa(asked,knight),isa(other,knight))))] 1: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(not(or(isa(asked,knight),isa(other,knight)))))] 2: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [truth( or(isa(asked,knight),isa(other,knight)))] 3: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(isa(other,knight)))], truth(not(or(isa(asked,knight),isa(other,knight)))) 4: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [truth( isa(asked,knight))], ~(truth(or(isa(asked,knight),isa(other,knight)))), truth( not(or(isa(asked,knight),isa(other,knight)))) 5: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(isa(asked,knight)))], truth(not(or(isa(asked,knight),isa(other,knight)))) Gamma_24: (move) 0: says(asked,or(isa(asked,knight),isa(other,knight))), [says( asked,not(or(isa(asked,knight),isa(other,knight))))] 1: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(not(or(isa(asked,knight),isa(other,knight)))))] 2: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [truth( or(isa(asked,knight),isa(other,knight)))] 3: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(isa(other,knight)))], truth(not(or(isa(asked,knight),isa(other,knight)))) 4: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(isa(asked,knight)))], truth(not(or(isa(asked,knight),isa(other,knight)))) 5: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [truth( isa(asked,knight))], ~(truth(or(isa(asked,knight),isa(other,knight)))), truth( not(or(isa(asked,knight),isa(other,knight)))) Gamma_25: (resolve) 0: says(asked,or(isa(asked,knight),isa(other,knight))), [says( asked,not(or(isa(asked,knight),isa(other,knight))))] 1: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(not(or(isa(asked,knight),isa(other,knight)))))] 2: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [truth( or(isa(asked,knight),isa(other,knight)))] 3: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(isa(other,knight)))], truth(not(or(isa(asked,knight),isa(other,knight)))) 4: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(isa(asked,knight)))], truth(not(or(isa(asked,knight),isa(other,knight)))) 5: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))], ~( truth(or(isa(asked,knight),isa(other,knight)))), truth(not(or(isa(asked,knight),isa(other,knight)))) Gamma_26: (extend-conflict) 0: says(asked,or(isa(asked,knight),isa(other,knight))), [says( asked,not(or(isa(asked,knight),isa(other,knight))))] 1: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(not(or(isa(asked,knight),isa(other,knight)))))] 2: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [truth( or(isa(asked,knight),isa(other,knight)))] 3: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(isa(other,knight)))], truth(not(or(isa(asked,knight),isa(other,knight)))) 4: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(isa(asked,knight)))], truth(not(or(isa(asked,knight),isa(other,knight)))) 5: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(or(isa(asked,knight),isa(other,knight))))], truth(not(or(isa(asked,knight),isa(other,knight)))) Gamma_27: (move) 0: says(asked,or(isa(asked,knight),isa(other,knight))), [says( asked,not(or(isa(asked,knight),isa(other,knight))))] 1: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(not(or(isa(asked,knight),isa(other,knight)))))] 2: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(or(isa(asked,knight),isa(other,knight))))], truth(not(or(isa(asked,knight),isa(other,knight)))) 3: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [truth( or(isa(asked,knight),isa(other,knight)))] 4: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(isa(other,knight)))], truth(not(or(isa(asked,knight),isa(other,knight)))) 5: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(isa(asked,knight)))], truth(not(or(isa(asked,knight),isa(other,knight)))) Gamma_28: (resolve) 0: says(asked,or(isa(asked,knight),isa(other,knight))), [says( asked,not(or(isa(asked,knight),isa(other,knight))))] 1: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(not(or(isa(asked,knight),isa(other,knight)))))] 2: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(or(isa(asked,knight),isa(other,knight))))], truth(not(or(isa(asked,knight),isa(other,knight)))) 3: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))], truth( not(or(isa(asked,knight),isa(other,knight)))) 4: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(isa(other,knight)))], truth(not(or(isa(asked,knight),isa(other,knight)))) 5: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(isa(asked,knight)))], truth(not(or(isa(asked,knight),isa(other,knight)))) Gamma_29: (extend-conflict) 0: says(asked,or(isa(asked,knight),isa(other,knight))), [says( asked,not(or(isa(asked,knight),isa(other,knight))))] 1: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(not(or(isa(asked,knight),isa(other,knight)))))] 2: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(or(isa(asked,knight),isa(other,knight))))], truth(not(or(isa(asked,knight),isa(other,knight)))) 3: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [truth( not(or(isa(asked,knight),isa(other,knight))))] 4: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(isa(other,knight)))], truth(not(or(isa(asked,knight),isa(other,knight)))) 5: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(isa(asked,knight)))], truth(not(or(isa(asked,knight),isa(other,knight)))) Gamma_30: (resolve) 0: says(asked,or(isa(asked,knight),isa(other,knight))), [says( asked,not(or(isa(asked,knight),isa(other,knight))))] 1: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(not(or(isa(asked,knight),isa(other,knight)))))] 2: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(or(isa(asked,knight),isa(other,knight))))], truth(not(or(isa(asked,knight),isa(other,knight)))) 3: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 4: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(isa(other,knight)))], truth(not(or(isa(asked,knight),isa(other,knight)))) 5: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(isa(asked,knight)))], truth(not(or(isa(asked,knight),isa(other,knight)))) Gamma_31: (extend-conflict) 0: says(asked,or(isa(asked,knight),isa(other,knight))), [says( asked,not(or(isa(asked,knight),isa(other,knight))))] 1: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(not(or(isa(asked,knight),isa(other,knight)))))] 2: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(or(isa(asked,knight),isa(other,knight))))], truth(not(or(isa(asked,knight),isa(other,knight)))) 3: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 4: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(isa(other,knight)))], truth(not(or(isa(asked,knight),isa(other,knight)))) 5: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(isa(asked,knight)))], truth(not(or(isa(asked,knight),isa(other,knight)))) Gamma_32: (move) 0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 1: says(asked,or(isa(asked,knight),isa(other,knight))), [says(asked, not(or(isa(asked,knight),isa(other,knight))))] 2: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(not(or(isa(asked,knight),isa(other,knight)))))] 3: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(or(isa(asked,knight),isa(other,knight))))], truth(not(or(isa(asked,knight),isa(other,knight)))) 4: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(isa(other,knight)))], truth(not(or(isa(asked,knight),isa(other,knight)))) 5: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~( truth(isa(asked,knight)))], truth(not(or(isa(asked,knight),isa(other,knight)))) Gamma_33: (resolve) 0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 1: [says(asked,or(isa(asked,knight),isa(other,knight)))] Gamma_34: (extend-no-conflict) 0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 1: [says(asked,or(isa(asked,knight),isa(other,knight)))] Gamma_35: (extend-no-conflict) 0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 1: [says(asked,or(isa(asked,knight),isa(other,knight)))] 2: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), truth(or(isa(asked,knight),isa(other,knight))), [truth( not(or(isa(asked,knight),isa(other,knight))))] Gamma_36: (extend-no-conflict) 0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 1: [says(asked,or(isa(asked,knight),isa(other,knight)))] 2: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), truth(or(isa(asked,knight),isa(other,knight))), [truth( not(or(isa(asked,knight),isa(other,knight))))] 3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(asked,knave))], ~( truth(not(or(isa(asked,knight),isa(other,knight))))) Gamma_37: (extend-no-conflict) 0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 1: [says(asked,or(isa(asked,knight),isa(other,knight)))] 2: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), truth(or(isa(asked,knight),isa(other,knight))), [truth( not(or(isa(asked,knight),isa(other,knight))))] 3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(asked,knave))], ~( truth(not(or(isa(asked,knight),isa(other,knight))))) 4: [person(other)] Gamma_38: (extend-no-conflict) 0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 1: [says(asked,or(isa(asked,knight),isa(other,knight)))] 2: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), truth(or(isa(asked,knight),isa(other,knight))), [truth( not(or(isa(asked,knight),isa(other,knight))))] 3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(asked,knave))], ~( truth(not(or(isa(asked,knight),isa(other,knight))))) 4: [person(other)] 5: [truth(isa(other,knave))], truth(isa(other,knight)), ~(person(other)) Gamma_39: (extend-conflict) 0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 1: [says(asked,or(isa(asked,knight),isa(other,knight)))] 2: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), truth(or(isa(asked,knight),isa(other,knight))), [truth( not(or(isa(asked,knight),isa(other,knight))))] 3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(asked,knave))], ~( truth(not(or(isa(asked,knight),isa(other,knight))))) 4: [person(other)] 5: [truth(isa(other,knave))], truth(isa(other,knight)), ~(person(other)) 6: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knave)))], ~( truth(isa(asked,knave))) Gamma_40: (move) 0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 1: [says(asked,or(isa(asked,knight),isa(other,knight)))] 2: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), truth(or(isa(asked,knight),isa(other,knight))), [truth( not(or(isa(asked,knight),isa(other,knight))))] 3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(asked,knave))], ~( truth(not(or(isa(asked,knight),isa(other,knight))))) 4: [person(other)] 5: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knave)))], ~( truth(isa(asked,knave))) 6: [truth(isa(other,knave))], truth(isa(other,knight)), ~(person(other)) Gamma_41: (resolve) 0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 1: [says(asked,or(isa(asked,knight),isa(other,knight)))] 2: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), truth(or(isa(asked,knight),isa(other,knight))), [truth( not(or(isa(asked,knight),isa(other,knight))))] 3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(asked,knave))], ~( truth(not(or(isa(asked,knight),isa(other,knight))))) 4: [person(other)] 5: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knave)))], ~( truth(isa(asked,knave))) 6: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(other,knight))], ~( truth(isa(asked,knave))), ~(person(other)) Gamma_42: (extend-no-conflict) 0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 1: [says(asked,or(isa(asked,knight),isa(other,knight)))] 2: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), truth(or(isa(asked,knight),isa(other,knight))), [truth( not(or(isa(asked,knight),isa(other,knight))))] 3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(asked,knave))], ~( truth(not(or(isa(asked,knight),isa(other,knight))))) 4: [person(other)] 5: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knave)))], ~( truth(isa(asked,knave))) 6: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(other,knight))], ~( truth(isa(asked,knave))), ~(person(other)) Gamma_43: (extend-conflict) 0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 1: [says(asked,or(isa(asked,knight),isa(other,knight)))] 2: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), truth(or(isa(asked,knight),isa(other,knight))), [truth( not(or(isa(asked,knight),isa(other,knight))))] 3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(asked,knave))], ~( truth(not(or(isa(asked,knight),isa(other,knight))))) 4: [person(other)] 5: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knave)))], ~( truth(isa(asked,knave))) 6: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(other,knight))], ~( truth(isa(asked,knave))), ~(person(other)) 7: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knight)))], ~( truth(isa(asked,knave))) Gamma_44: (move) 0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 1: [says(asked,or(isa(asked,knight),isa(other,knight)))] 2: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), truth(or(isa(asked,knight),isa(other,knight))), [truth( not(or(isa(asked,knight),isa(other,knight))))] 3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(asked,knave))], ~( truth(not(or(isa(asked,knight),isa(other,knight))))) 4: [person(other)] 5: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knave)))], ~( truth(isa(asked,knave))) 6: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knight)))], ~( truth(isa(asked,knave))) 7: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(other,knight))], ~( truth(isa(asked,knave))), ~(person(other)) Gamma_45: (resolve) 0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 1: [says(asked,or(isa(asked,knight),isa(other,knight)))] 2: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), truth(or(isa(asked,knight),isa(other,knight))), [truth( not(or(isa(asked,knight),isa(other,knight))))] 3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(asked,knave))], ~( truth(not(or(isa(asked,knight),isa(other,knight))))) 4: [person(other)] 5: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knave)))], ~( truth(isa(asked,knave))) 6: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knight)))], ~( truth(isa(asked,knave))) 7: [~(says(asked,or(isa(asked,knight),isa(other,knight))))], ~(truth(isa(asked,knave))), ~( person(other)) Gamma_46: (extend-conflict) 0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 1: [says(asked,or(isa(asked,knight),isa(other,knight)))] 2: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), truth(or(isa(asked,knight),isa(other,knight))), [truth( not(or(isa(asked,knight),isa(other,knight))))] 3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(asked,knave))], ~( truth(not(or(isa(asked,knight),isa(other,knight))))) 4: [person(other)] 5: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knave)))], ~( truth(isa(asked,knave))) 6: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knight)))], ~( truth(isa(asked,knave))) 7: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), ~(truth(isa(asked,knave))), [~( person(other))] Gamma_47: (move) 0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 1: [says(asked,or(isa(asked,knight),isa(other,knight)))] 2: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), truth(or(isa(asked,knight),isa(other,knight))), [truth( not(or(isa(asked,knight),isa(other,knight))))] 3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(asked,knave))], ~( truth(not(or(isa(asked,knight),isa(other,knight))))) 4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), ~(truth(isa(asked,knave))), [~( person(other))] 5: [person(other)] 6: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knave)))], ~( truth(isa(asked,knave))) 7: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knight)))], ~( truth(isa(asked,knave))) Gamma_48: (resolve) 0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 1: [says(asked,or(isa(asked,knight),isa(other,knight)))] 2: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), truth(or(isa(asked,knight),isa(other,knight))), [truth( not(or(isa(asked,knight),isa(other,knight))))] 3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(asked,knave))], ~( truth(not(or(isa(asked,knight),isa(other,knight))))) 4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), ~(truth(isa(asked,knave))), [~( person(other))] 5: [~(says(asked,or(isa(asked,knight),isa(other,knight))))], ~(truth(isa(asked,knave))) 6: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knave)))], ~( truth(isa(asked,knave))) 7: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knight)))], ~( truth(isa(asked,knave))) Gamma_49: (extend-conflict) 0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 1: [says(asked,or(isa(asked,knight),isa(other,knight)))] 2: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), truth(or(isa(asked,knight),isa(other,knight))), [truth( not(or(isa(asked,knight),isa(other,knight))))] 3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(asked,knave))], ~( truth(not(or(isa(asked,knight),isa(other,knight))))) 4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), ~(truth(isa(asked,knave))), [~( person(other))] 5: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(asked,knave)))] 6: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knave)))], ~( truth(isa(asked,knave))) 7: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knight)))], ~( truth(isa(asked,knave))) Gamma_50: (move) 0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 1: [says(asked,or(isa(asked,knight),isa(other,knight)))] 2: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), truth(or(isa(asked,knight),isa(other,knight))), [truth( not(or(isa(asked,knight),isa(other,knight))))] 3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(asked,knave)))] 4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(asked,knave))], ~( truth(not(or(isa(asked,knight),isa(other,knight))))) 5: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), ~(truth(isa(asked,knave))), [~( person(other))] 6: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knave)))], ~( truth(isa(asked,knave))) 7: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knight)))], ~( truth(isa(asked,knave))) Gamma_51: (resolve) 0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 1: [says(asked,or(isa(asked,knight),isa(other,knight)))] 2: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), truth(or(isa(asked,knight),isa(other,knight))), [truth( not(or(isa(asked,knight),isa(other,knight))))] 3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(asked,knave)))] 4: [~(says(asked,or(isa(asked,knight),isa(other,knight))))], ~(truth(not(or(isa(asked,knight),isa(other,knight))))) Gamma_52: (extend-conflict) 0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 1: [says(asked,or(isa(asked,knight),isa(other,knight)))] 2: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), truth(or(isa(asked,knight),isa(other,knight))), [truth( not(or(isa(asked,knight),isa(other,knight))))] 3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(asked,knave)))] 4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(not(or(isa(asked,knight),isa(other,knight)))))] Gamma_53: (move) 0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 1: [says(asked,or(isa(asked,knight),isa(other,knight)))] 2: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(not(or(isa(asked,knight),isa(other,knight)))))] 3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), truth(or(isa(asked,knight),isa(other,knight))), [truth( not(or(isa(asked,knight),isa(other,knight))))] 4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(asked,knave)))] Gamma_54: (resolve) 0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 1: [says(asked,or(isa(asked,knight),isa(other,knight)))] 2: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(not(or(isa(asked,knight),isa(other,knight)))))] 3: [~(says(asked,or(isa(asked,knight),isa(other,knight))))], truth( or(isa(asked,knight),isa(other,knight))) 4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(asked,knave)))] Gamma_55: (extend-no-conflict) 0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 1: [says(asked,or(isa(asked,knight),isa(other,knight)))] 2: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(not(or(isa(asked,knight),isa(other,knight)))))] 3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(or(isa(asked,knight),isa(other,knight)))] 4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(asked,knave)))] Gamma_56: (extend-no-conflict) 0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 1: [says(asked,or(isa(asked,knight),isa(other,knight)))] 2: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(not(or(isa(asked,knight),isa(other,knight)))))] 3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(or(isa(asked,knight),isa(other,knight)))] 4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(asked,knave)))] 5: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(asked,knight))], ~( truth(or(isa(asked,knight),isa(other,knight)))) Gamma_57: (extend-no-conflict) 0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 1: [says(asked,or(isa(asked,knight),isa(other,knight)))] 2: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(not(or(isa(asked,knight),isa(other,knight)))))] 3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(or(isa(asked,knight),isa(other,knight)))] 4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(asked,knave)))] 5: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(asked,knight))], ~( truth(or(isa(asked,knight),isa(other,knight)))) 6: [person(other)] Gamma_58: (extend-no-conflict) 0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 1: [says(asked,or(isa(asked,knight),isa(other,knight)))] 2: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(not(or(isa(asked,knight),isa(other,knight)))))] 3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(or(isa(asked,knight),isa(other,knight)))] 4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(asked,knave)))] 5: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(asked,knight))], ~( truth(or(isa(asked,knight),isa(other,knight)))) 6: [person(other)] 7: [truth(isa(other,knave))], truth(isa(other,knight)), ~(person(other)) Gamma_59: (extend-conflict) 0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 1: [says(asked,or(isa(asked,knight),isa(other,knight)))] 2: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(not(or(isa(asked,knight),isa(other,knight)))))] 3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(or(isa(asked,knight),isa(other,knight)))] 4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(asked,knave)))] 5: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(asked,knight))], ~( truth(or(isa(asked,knight),isa(other,knight)))) 6: [person(other)] 7: [truth(isa(other,knave))], truth(isa(other,knight)), ~(person(other)) 8: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knave)))], ~( truth(isa(asked,knight))) Gamma_60: (move) 0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 1: [says(asked,or(isa(asked,knight),isa(other,knight)))] 2: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(not(or(isa(asked,knight),isa(other,knight)))))] 3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(or(isa(asked,knight),isa(other,knight)))] 4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(asked,knave)))] 5: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(asked,knight))], ~( truth(or(isa(asked,knight),isa(other,knight)))) 6: [person(other)] 7: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knave)))], ~( truth(isa(asked,knight))) 8: [truth(isa(other,knave))], truth(isa(other,knight)), ~(person(other)) Gamma_61: (resolve) 0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 1: [says(asked,or(isa(asked,knight),isa(other,knight)))] 2: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(not(or(isa(asked,knight),isa(other,knight)))))] 3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(or(isa(asked,knight),isa(other,knight)))] 4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(asked,knave)))] 5: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(asked,knight))], ~( truth(or(isa(asked,knight),isa(other,knight)))) 6: [person(other)] 7: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knave)))], ~( truth(isa(asked,knight))) 8: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(other,knight))], ~( truth(isa(asked,knight))), ~(person(other)) Gamma_62: (extend-no-conflict) 0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 1: [says(asked,or(isa(asked,knight),isa(other,knight)))] 2: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(not(or(isa(asked,knight),isa(other,knight)))))] 3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(or(isa(asked,knight),isa(other,knight)))] 4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(asked,knave)))] 5: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(asked,knight))], ~( truth(or(isa(asked,knight),isa(other,knight)))) 6: [person(other)] 7: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knave)))], ~( truth(isa(asked,knight))) 8: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(other,knight))], ~( truth(isa(asked,knight))), ~(person(other)) Gamma_63: (extend-conflict) 0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 1: [says(asked,or(isa(asked,knight),isa(other,knight)))] 2: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(not(or(isa(asked,knight),isa(other,knight)))))] 3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(or(isa(asked,knight),isa(other,knight)))] 4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(asked,knave)))] 5: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(asked,knight))], ~( truth(or(isa(asked,knight),isa(other,knight)))) 6: [person(other)] 7: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knave)))], ~( truth(isa(asked,knight))) 8: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(other,knight))], ~( truth(isa(asked,knight))), ~(person(other)) 9: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knight)))], ~( truth(isa(asked,knight))) Gamma_64: (move) 0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 1: [says(asked,or(isa(asked,knight),isa(other,knight)))] 2: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(not(or(isa(asked,knight),isa(other,knight)))))] 3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(or(isa(asked,knight),isa(other,knight)))] 4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(asked,knave)))] 5: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(asked,knight))], ~( truth(or(isa(asked,knight),isa(other,knight)))) 6: [person(other)] 7: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knave)))], ~( truth(isa(asked,knight))) 8: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knight)))], ~( truth(isa(asked,knight))) 9: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(other,knight))], ~( truth(isa(asked,knight))), ~(person(other)) Gamma_65: (resolve) 0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 1: [says(asked,or(isa(asked,knight),isa(other,knight)))] 2: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(not(or(isa(asked,knight),isa(other,knight)))))] 3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(or(isa(asked,knight),isa(other,knight)))] 4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(asked,knave)))] 5: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(asked,knight))], ~( truth(or(isa(asked,knight),isa(other,knight)))) 6: [person(other)] 7: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knave)))], ~( truth(isa(asked,knight))) 8: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knight)))], ~( truth(isa(asked,knight))) 9: [~(says(asked,or(isa(asked,knight),isa(other,knight))))], ~(truth(isa(asked,knight))), ~( person(other)) Gamma_66: (extend-conflict) 0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 1: [says(asked,or(isa(asked,knight),isa(other,knight)))] 2: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(not(or(isa(asked,knight),isa(other,knight)))))] 3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(or(isa(asked,knight),isa(other,knight)))] 4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(asked,knave)))] 5: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(asked,knight))], ~( truth(or(isa(asked,knight),isa(other,knight)))) 6: [person(other)] 7: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knave)))], ~( truth(isa(asked,knight))) 8: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knight)))], ~( truth(isa(asked,knight))) 9: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), ~(truth(isa(asked,knight))), [~( person(other))] Gamma_67: (move) 0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 1: [says(asked,or(isa(asked,knight),isa(other,knight)))] 2: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(not(or(isa(asked,knight),isa(other,knight)))))] 3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(or(isa(asked,knight),isa(other,knight)))] 4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(asked,knave)))] 5: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(asked,knight))], ~( truth(or(isa(asked,knight),isa(other,knight)))) 6: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), ~(truth(isa(asked,knight))), [~( person(other))] 7: [person(other)] 8: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knave)))], ~( truth(isa(asked,knight))) 9: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knight)))], ~( truth(isa(asked,knight))) Gamma_68: (resolve) 0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 1: [says(asked,or(isa(asked,knight),isa(other,knight)))] 2: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(not(or(isa(asked,knight),isa(other,knight)))))] 3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(or(isa(asked,knight),isa(other,knight)))] 4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(asked,knave)))] 5: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(asked,knight))], ~( truth(or(isa(asked,knight),isa(other,knight)))) 6: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), ~(truth(isa(asked,knight))), [~( person(other))] 7: [~(says(asked,or(isa(asked,knight),isa(other,knight))))], ~(truth(isa(asked,knight))) 8: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knave)))], ~( truth(isa(asked,knight))) 9: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knight)))], ~( truth(isa(asked,knight))) Gamma_69: (extend-conflict) 0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 1: [says(asked,or(isa(asked,knight),isa(other,knight)))] 2: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(not(or(isa(asked,knight),isa(other,knight)))))] 3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(or(isa(asked,knight),isa(other,knight)))] 4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(asked,knave)))] 5: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(asked,knight))], ~( truth(or(isa(asked,knight),isa(other,knight)))) 6: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), ~(truth(isa(asked,knight))), [~( person(other))] 7: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(asked,knight)))] 8: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knave)))], ~( truth(isa(asked,knight))) 9: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knight)))], ~( truth(isa(asked,knight))) Gamma_70: (move) 0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 1: [says(asked,or(isa(asked,knight),isa(other,knight)))] 2: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(not(or(isa(asked,knight),isa(other,knight)))))] 3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(or(isa(asked,knight),isa(other,knight)))] 4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(asked,knave)))] 5: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(asked,knight)))] 6: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(asked,knight))], ~( truth(or(isa(asked,knight),isa(other,knight)))) 7: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), ~(truth(isa(asked,knight))), [~( person(other))] 8: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knave)))], ~( truth(isa(asked,knight))) 9: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knight)))], ~( truth(isa(asked,knight))) Gamma_71: (resolve) 0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 1: [says(asked,or(isa(asked,knight),isa(other,knight)))] 2: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(not(or(isa(asked,knight),isa(other,knight)))))] 3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(or(isa(asked,knight),isa(other,knight)))] 4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(asked,knave)))] 5: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(asked,knight)))] 6: [~(says(asked,or(isa(asked,knight),isa(other,knight))))], ~(truth(or(isa(asked,knight),isa(other,knight)))) Gamma_72: (extend-conflict) 0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 1: [says(asked,or(isa(asked,knight),isa(other,knight)))] 2: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(not(or(isa(asked,knight),isa(other,knight)))))] 3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(or(isa(asked,knight),isa(other,knight)))] 4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(asked,knave)))] 5: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(asked,knight)))] 6: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(or(isa(asked,knight),isa(other,knight))))] Gamma_73: (move) 0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 1: [says(asked,or(isa(asked,knight),isa(other,knight)))] 2: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(not(or(isa(asked,knight),isa(other,knight)))))] 3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(or(isa(asked,knight),isa(other,knight))))] 4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(or(isa(asked,knight),isa(other,knight)))] 5: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(asked,knave)))] 6: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(asked,knight)))] Gamma_74: (resolve) 0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 1: [says(asked,or(isa(asked,knight),isa(other,knight)))] 2: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(not(or(isa(asked,knight),isa(other,knight)))))] 3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(or(isa(asked,knight),isa(other,knight))))] 4: [~(says(asked,or(isa(asked,knight),isa(other,knight))))] 5: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(asked,knave)))] 6: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(asked,knight)))] Gamma_75: (extend-conflict) 0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 1: [says(asked,or(isa(asked,knight),isa(other,knight)))] 2: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(not(or(isa(asked,knight),isa(other,knight)))))] 3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(or(isa(asked,knight),isa(other,knight))))] 4: [~(says(asked,or(isa(asked,knight),isa(other,knight))))] 5: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(asked,knave)))] 6: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(asked,knight)))] Gamma_76: (move) 0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 1: [~(says(asked,or(isa(asked,knight),isa(other,knight))))] 2: [says(asked,or(isa(asked,knight),isa(other,knight)))] 3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(not(or(isa(asked,knight),isa(other,knight)))))] 4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(or(isa(asked,knight),isa(other,knight))))] 5: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(asked,knave)))] 6: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(asked,knight)))] Gamma_77: (resolve) 0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))] 1: [~(says(asked,or(isa(asked,knight),isa(other,knight))))] 2: [] SZS status Unsatisfiable