%---------------- 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: [person(other)]

Gamma_13: (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: [person(other)]
  6: [person(asked)]

Gamma_14: (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: [person(other)]
  6: [person(asked)]
  7: [truth(isa(asked,knave))], truth(isa(asked,knight)), ~(person(asked))

Gamma_15: (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: [person(other)]
  6: [person(asked)]
  7: [truth(isa(asked,knave))], truth(isa(asked,knight)), ~(person(asked))
  8: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), ~(truth(isa(other,knight))), [~(
truth(isa(asked,knave)))]

Gamma_16: (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: [person(other)]
  6: [person(asked)]
  7: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), ~(truth(isa(other,knight))), [~(
truth(isa(asked,knave)))]
  8: [truth(isa(asked,knave))], truth(isa(asked,knight)), ~(person(asked))

Gamma_17: (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: [person(other)]
  6: [person(asked)]
  7: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), ~(truth(isa(other,knight))), [~(
truth(isa(asked,knave)))]
  8: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), ~(truth(isa(other,knight))), [truth(
isa(asked,knight))], ~(person(asked))

Gamma_18: (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: [person(other)]
  6: [person(asked)]
  7: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), ~(truth(isa(other,knight))), [~(
truth(isa(asked,knave)))]
  8: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), ~(truth(isa(other,knight))), [truth(
isa(asked,knight))], ~(person(asked))

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(
not(or(isa(asked,knight),isa(other,knight)))), [truth(not(not(or(isa(asked,knight),isa(other,knight)))))]
  5: [person(other)]
  6: [person(asked)]
  7: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), ~(truth(isa(other,knight))), [~(
truth(isa(asked,knave)))]
  8: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), ~(truth(isa(other,knight))), [truth(
isa(asked,knight))], ~(person(asked))
  9: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), ~(truth(isa(other,knight))), [~(
truth(isa(asked,knight)))]

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: [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: [person(other)]
  6: [person(asked)]
  7: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), ~(truth(isa(other,knight))), [~(
truth(isa(asked,knave)))]
  8: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), ~(truth(isa(other,knight))), [~(
truth(isa(asked,knight)))]
  9: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), ~(truth(isa(other,knight))), [truth(
isa(asked,knight))], ~(person(asked))

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: [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: [person(other)]
  6: [person(asked)]
  7: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), ~(truth(isa(other,knight))), [~(
truth(isa(asked,knave)))]
  8: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), ~(truth(isa(other,knight))), [~(
truth(isa(asked,knight)))]
  9: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))], ~(
truth(isa(other,knight))), ~(person(asked))

Gamma_22: (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: [person(other)]
  6: [person(asked)]
  7: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), ~(truth(isa(other,knight))), [~(
truth(isa(asked,knave)))]
  8: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), ~(truth(isa(other,knight))), [~(
truth(isa(asked,knight)))]
  9: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), ~(truth(isa(other,knight))), [~(
person(asked))]

Gamma_23: (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: [person(other)]
  6: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), ~(truth(isa(other,knight))), [~(
person(asked))]
  7: [person(asked)]
  8: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), ~(truth(isa(other,knight))), [~(
truth(isa(asked,knave)))]
  9: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), ~(truth(isa(other,knight))), [~(
truth(isa(asked,knight)))]

Gamma_24: (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: [person(other)]
  6: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), ~(truth(isa(other,knight))), [~(
person(asked))]
  7: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))], ~(
truth(isa(other,knight)))
  8: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), ~(truth(isa(other,knight))), [~(
truth(isa(asked,knave)))]
  9: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), ~(truth(isa(other,knight))), [~(
truth(isa(asked,knight)))]

Gamma_25: (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: [person(other)]
  6: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), ~(truth(isa(other,knight))), [~(
person(asked))]
  7: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~(
truth(isa(other,knight)))]
  8: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), ~(truth(isa(other,knight))), [~(
truth(isa(asked,knave)))]
  9: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), ~(truth(isa(other,knight))), [~(
truth(isa(asked,knight)))]

Gamma_26: (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)))]
  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(
not(or(isa(asked,knight),isa(other,knight)))), [truth(not(not(or(isa(asked,knight),isa(other,knight)))))]
  6: [person(other)]
  7: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), ~(truth(isa(other,knight))), [~(
person(asked))]
  8: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), ~(truth(isa(other,knight))), [~(
truth(isa(asked,knave)))]
  9: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), ~(truth(isa(other,knight))), [~(
truth(isa(asked,knight)))]

Gamma_27: (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)))]
  4: ~(says(asked,not(or(isa(asked,knight),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(
not(or(isa(asked,knight),isa(other,knight)))), [truth(not(not(or(isa(asked,knight),isa(other,knight)))))]
  6: [person(other)]

Gamma_28: (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)))]
  4: ~(says(asked,not(or(isa(asked,knight),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(
not(or(isa(asked,knight),isa(other,knight)))), [truth(not(not(or(isa(asked,knight),isa(other,knight)))))]
  6: [person(other)]

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)))]
  3: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~(
truth(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))))
  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: [person(other)]
  7: ~(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: (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)))]
  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))))
  6: ~(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)))))]
  7: [person(other)]

Gamma_31: (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)))]
  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))))
  6: ~(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)))))]
  7: [person(other)]

Gamma_32: (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)))]
  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))))
  6: ~(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)))))]
  7: [person(other)]

Gamma_33: (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)))]
  5: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~(
truth(isa(asked,knight)))], truth(not(or(isa(asked,knight),isa(other,knight))))
  6: ~(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)))))]
  7: [person(other)]

Gamma_34: (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)))]
  5: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~(
truth(isa(asked,knight)))], truth(not(or(isa(asked,knight),isa(other,knight))))
  6: ~(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)))))]
  7: [person(other)]

Gamma_35: (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)))]
  5: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~(
truth(isa(asked,knight)))], truth(not(or(isa(asked,knight),isa(other,knight))))
  6: ~(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)))))]
  7: [person(other)]

Gamma_36: (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)))]
  5: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~(
truth(isa(asked,knight)))], truth(not(or(isa(asked,knight),isa(other,knight))))
  6: ~(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)))))]
  7: [person(other)]

Gamma_37: (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)))]
  5: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~(
truth(isa(asked,knight)))], truth(not(or(isa(asked,knight),isa(other,knight))))
  6: ~(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)))))]
  7: [person(other)]

Gamma_38: (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)))]
  5: ~(says(asked,not(or(isa(asked,knight),isa(other,knight))))), [~(
truth(isa(asked,knight)))], truth(not(or(isa(asked,knight),isa(other,knight))))
  6: ~(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)))))]
  7: [person(other)]

Gamma_39: (resolve)
  0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))]
  1: [says(asked,or(isa(asked,knight),isa(other,knight)))]
  2: [person(other)]

Gamma_40: (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: [person(other)]

Gamma_41: (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: [person(other)]
  3: [truth(isa(other,knave))], truth(isa(other,knight)), ~(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: [person(other)]
  3: [truth(isa(other,knave))], truth(isa(other,knight)), ~(person(other))
  4: ~(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_43: (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: [person(other)]
  3: [truth(isa(other,knave))], truth(isa(other,knight)), ~(person(other))
  4: ~(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))))]
  5: [person(asked)]

Gamma_44: (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: [person(other)]
  3: [truth(isa(other,knave))], truth(isa(other,knight)), ~(person(other))
  4: ~(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))))]
  5: [person(asked)]
  6: [truth(isa(asked,knave))], truth(isa(asked,knight)), ~(person(asked))

Gamma_45: (extend-conflict)
  0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))]
  1: [says(asked,or(isa(asked,knight),isa(other,knight)))]
  2: [person(other)]
  3: [truth(isa(other,knave))], truth(isa(other,knight)), ~(person(other))
  4: ~(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))))]
  5: [person(asked)]
  6: [truth(isa(asked,knave))], truth(isa(asked,knight)), ~(person(asked))
  7: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), ~(truth(isa(other,knave))), [~(
truth(isa(asked,knave)))]

Gamma_46: (move)
  0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))]
  1: [says(asked,or(isa(asked,knight),isa(other,knight)))]
  2: [person(other)]
  3: [truth(isa(other,knave))], truth(isa(other,knight)), ~(person(other))
  4: ~(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))))]
  5: [person(asked)]
  6: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), ~(truth(isa(other,knave))), [~(
truth(isa(asked,knave)))]
  7: [truth(isa(asked,knave))], truth(isa(asked,knight)), ~(person(asked))

Gamma_47: (resolve)
  0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))]
  1: [says(asked,or(isa(asked,knight),isa(other,knight)))]
  2: [person(other)]
  3: [truth(isa(other,knave))], truth(isa(other,knight)), ~(person(other))
  4: ~(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))))]
  5: [person(asked)]
  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,knave))), [truth(
isa(asked,knight))], ~(person(asked))

Gamma_48: (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: [person(other)]
  3: [truth(isa(other,knave))], truth(isa(other,knight)), ~(person(other))
  4: ~(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))))]
  5: [person(asked)]
  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,knave))), [truth(
isa(asked,knight))], ~(person(asked))

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: [person(other)]
  3: [truth(isa(other,knave))], truth(isa(other,knight)), ~(person(other))
  4: ~(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))))]
  5: [person(asked)]
  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,knave))), [truth(
isa(asked,knight))], ~(person(asked))
  8: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), ~(truth(isa(other,knave))), [~(
truth(isa(asked,knight)))]

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: [person(other)]
  3: [truth(isa(other,knave))], truth(isa(other,knight)), ~(person(other))
  4: ~(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))))]
  5: [person(asked)]
  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,knave))), [~(
truth(isa(asked,knight)))]
  8: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), ~(truth(isa(other,knave))), [truth(
isa(asked,knight))], ~(person(asked))

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: [person(other)]
  3: [truth(isa(other,knave))], truth(isa(other,knight)), ~(person(other))
  4: ~(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))))]
  5: [person(asked)]
  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,knave))), [~(
truth(isa(asked,knight)))]
  8: [~(says(asked,or(isa(asked,knight),isa(other,knight))))], ~(truth(isa(other,knave))), ~(
person(asked))

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: [person(other)]
  3: [truth(isa(other,knave))], truth(isa(other,knight)), ~(person(other))
  4: ~(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))))]
  5: [person(asked)]
  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,knave))), [~(
truth(isa(asked,knight)))]
  8: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), ~(truth(isa(other,knave))), [~(
person(asked))]

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: [person(other)]
  3: [truth(isa(other,knave))], truth(isa(other,knight)), ~(person(other))
  4: ~(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))))]
  5: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), ~(truth(isa(other,knave))), [~(
person(asked))]
  6: [person(asked)]
  7: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), ~(truth(isa(other,knave))), [~(
truth(isa(asked,knave)))]
  8: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), ~(truth(isa(other,knave))), [~(
truth(isa(asked,knight)))]

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: [person(other)]
  3: [truth(isa(other,knave))], truth(isa(other,knight)), ~(person(other))
  4: ~(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))))]
  5: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), ~(truth(isa(other,knave))), [~(
person(asked))]
  6: [~(says(asked,or(isa(asked,knight),isa(other,knight))))], ~(truth(isa(other,knave)))
  7: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), ~(truth(isa(other,knave))), [~(
truth(isa(asked,knave)))]
  8: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), ~(truth(isa(other,knave))), [~(
truth(isa(asked,knight)))]

Gamma_55: (extend-conflict)
  0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))]
  1: [says(asked,or(isa(asked,knight),isa(other,knight)))]
  2: [person(other)]
  3: [truth(isa(other,knave))], truth(isa(other,knight)), ~(person(other))
  4: ~(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))))]
  5: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), ~(truth(isa(other,knave))), [~(
person(asked))]
  6: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knave)))]
  7: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), ~(truth(isa(other,knave))), [~(
truth(isa(asked,knave)))]
  8: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), ~(truth(isa(other,knave))), [~(
truth(isa(asked,knight)))]

Gamma_56: (move)
  0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))]
  1: [says(asked,or(isa(asked,knight),isa(other,knight)))]
  2: [person(other)]
  3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knave)))]
  4: [truth(isa(other,knave))], truth(isa(other,knight)), ~(person(other))
  5: ~(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))))]
  6: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), ~(truth(isa(other,knave))), [~(
person(asked))]
  7: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), ~(truth(isa(other,knave))), [~(
truth(isa(asked,knave)))]
  8: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), ~(truth(isa(other,knave))), [~(
truth(isa(asked,knight)))]

Gamma_57: (resolve)
  0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))]
  1: [says(asked,or(isa(asked,knight),isa(other,knight)))]
  2: [person(other)]
  3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knave)))]
  4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(other,knight))], ~(
person(other))
  5: ~(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_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: [person(other)]
  3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knave)))]
  4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(other,knight))], ~(
person(other))
  5: ~(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_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: [person(other)]
  3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knave)))]
  4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(other,knight))], ~(
person(other))
  5: ~(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))))]
  6: ~(truth(isa(other,knight))), [~(truth(not(or(isa(asked,knight),isa(other,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: [person(other)]
  3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knave)))]
  4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(other,knight))], ~(
person(other))
  5: ~(truth(isa(other,knight))), [~(truth(not(or(isa(asked,knight),isa(other,knight)))))]
  6: ~(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_61: (resolve)
  0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))]
  1: [says(asked,or(isa(asked,knight),isa(other,knight)))]
  2: [person(other)]
  3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knave)))]
  4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(other,knight))], ~(
person(other))
  5: ~(truth(isa(other,knight))), [~(truth(not(or(isa(asked,knight),isa(other,knight)))))]
  6: [~(says(asked,or(isa(asked,knight),isa(other,knight))))], ~(truth(isa(other,knight))), truth(
or(isa(asked,knight),isa(other,knight)))

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: [person(other)]
  3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knave)))]
  4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(other,knight))], ~(
person(other))
  5: ~(truth(isa(other,knight))), [~(truth(not(or(isa(asked,knight),isa(other,knight)))))]
  6: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), ~(truth(isa(other,knight))), [truth(
or(isa(asked,knight),isa(other,knight)))]

Gamma_63: (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: [person(other)]
  3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knave)))]
  4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(other,knight))], ~(
person(other))
  5: ~(truth(isa(other,knight))), [~(truth(not(or(isa(asked,knight),isa(other,knight)))))]
  6: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), ~(truth(isa(other,knight))), [truth(
or(isa(asked,knight),isa(other,knight)))]
  7: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(asked,knight))], ~(
truth(or(isa(asked,knight),isa(other,knight))))

Gamma_64: (extend-conflict)
  0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))]
  1: [says(asked,or(isa(asked,knight),isa(other,knight)))]
  2: [person(other)]
  3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knave)))]
  4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(other,knight))], ~(
person(other))
  5: ~(truth(isa(other,knight))), [~(truth(not(or(isa(asked,knight),isa(other,knight)))))]
  6: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), ~(truth(isa(other,knight))), [truth(
or(isa(asked,knight),isa(other,knight)))]
  7: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(asked,knight))], ~(
truth(or(isa(asked,knight),isa(other,knight))))
  8: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), ~(truth(isa(other,knight))), [~(
truth(isa(asked,knight)))]

Gamma_65: (move)
  0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))]
  1: [says(asked,or(isa(asked,knight),isa(other,knight)))]
  2: [person(other)]
  3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knave)))]
  4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(other,knight))], ~(
person(other))
  5: ~(truth(isa(other,knight))), [~(truth(not(or(isa(asked,knight),isa(other,knight)))))]
  6: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), ~(truth(isa(other,knight))), [truth(
or(isa(asked,knight),isa(other,knight)))]
  7: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), ~(truth(isa(other,knight))), [~(
truth(isa(asked,knight)))]
  8: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(asked,knight))], ~(
truth(or(isa(asked,knight),isa(other,knight))))

Gamma_66: (resolve)
  0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))]
  1: [says(asked,or(isa(asked,knight),isa(other,knight)))]
  2: [person(other)]
  3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knave)))]
  4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(other,knight))], ~(
person(other))
  5: ~(truth(isa(other,knight))), [~(truth(not(or(isa(asked,knight),isa(other,knight)))))]
  6: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), ~(truth(isa(other,knight))), [truth(
or(isa(asked,knight),isa(other,knight)))]
  7: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), ~(truth(isa(other,knight))), [~(
truth(isa(asked,knight)))]
  8: [~(says(asked,or(isa(asked,knight),isa(other,knight))))], ~(truth(isa(other,knight))), ~(
truth(or(isa(asked,knight),isa(other,knight))))

Gamma_67: (extend-conflict)
  0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))]
  1: [says(asked,or(isa(asked,knight),isa(other,knight)))]
  2: [person(other)]
  3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knave)))]
  4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(other,knight))], ~(
person(other))
  5: ~(truth(isa(other,knight))), [~(truth(not(or(isa(asked,knight),isa(other,knight)))))]
  6: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), ~(truth(isa(other,knight))), [truth(
or(isa(asked,knight),isa(other,knight)))]
  7: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), ~(truth(isa(other,knight))), [~(
truth(isa(asked,knight)))]
  8: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), ~(truth(isa(other,knight))), [~(
truth(or(isa(asked,knight),isa(other,knight))))]

Gamma_68: (move)
  0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))]
  1: [says(asked,or(isa(asked,knight),isa(other,knight)))]
  2: [person(other)]
  3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knave)))]
  4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(other,knight))], ~(
person(other))
  5: ~(truth(isa(other,knight))), [~(truth(not(or(isa(asked,knight),isa(other,knight)))))]
  6: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), ~(truth(isa(other,knight))), [~(
truth(or(isa(asked,knight),isa(other,knight))))]
  7: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), ~(truth(isa(other,knight))), [truth(
or(isa(asked,knight),isa(other,knight)))]
  8: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), ~(truth(isa(other,knight))), [~(
truth(isa(asked,knight)))]

Gamma_69: (resolve)
  0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))]
  1: [says(asked,or(isa(asked,knight),isa(other,knight)))]
  2: [person(other)]
  3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knave)))]
  4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(other,knight))], ~(
person(other))
  5: ~(truth(isa(other,knight))), [~(truth(not(or(isa(asked,knight),isa(other,knight)))))]
  6: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), ~(truth(isa(other,knight))), [~(
truth(or(isa(asked,knight),isa(other,knight))))]
  7: [~(says(asked,or(isa(asked,knight),isa(other,knight))))], ~(truth(isa(other,knight)))
  8: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), ~(truth(isa(other,knight))), [~(
truth(isa(asked,knight)))]

Gamma_70: (extend-conflict)
  0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))]
  1: [says(asked,or(isa(asked,knight),isa(other,knight)))]
  2: [person(other)]
  3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knave)))]
  4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(other,knight))], ~(
person(other))
  5: ~(truth(isa(other,knight))), [~(truth(not(or(isa(asked,knight),isa(other,knight)))))]
  6: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), ~(truth(isa(other,knight))), [~(
truth(or(isa(asked,knight),isa(other,knight))))]
  7: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knight)))]
  8: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), ~(truth(isa(other,knight))), [~(
truth(isa(asked,knight)))]

Gamma_71: (move)
  0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))]
  1: [says(asked,or(isa(asked,knight),isa(other,knight)))]
  2: [person(other)]
  3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knave)))]
  4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knight)))]
  5: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [truth(isa(other,knight))], ~(
person(other))
  6: ~(truth(isa(other,knight))), [~(truth(not(or(isa(asked,knight),isa(other,knight)))))]
  7: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), ~(truth(isa(other,knight))), [~(
truth(or(isa(asked,knight),isa(other,knight))))]
  8: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), ~(truth(isa(other,knight))), [~(
truth(isa(asked,knight)))]

Gamma_72: (resolve)
  0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))]
  1: [says(asked,or(isa(asked,knight),isa(other,knight)))]
  2: [person(other)]
  3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knave)))]
  4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knight)))]
  5: [~(says(asked,or(isa(asked,knight),isa(other,knight))))], ~(person(other))

Gamma_73: (extend-conflict)
  0: [~(says(asked,not(or(isa(asked,knight),isa(other,knight)))))]
  1: [says(asked,or(isa(asked,knight),isa(other,knight)))]
  2: [person(other)]
  3: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knave)))]
  4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knight)))]
  5: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(person(other))]

Gamma_74: (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)))), [~(person(other))]
  3: [person(other)]
  4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knave)))]
  5: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knight)))]

Gamma_75: (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)))), [~(person(other))]
  3: [~(says(asked,or(isa(asked,knight),isa(other,knight))))]
  4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knave)))]
  5: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knight)))]

Gamma_76: (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)))), [~(person(other))]
  3: [~(says(asked,or(isa(asked,knight),isa(other,knight))))]
  4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knave)))]
  5: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knight)))]

Gamma_77: (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)))), [~(person(other))]
  4: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knave)))]
  5: ~(says(asked,or(isa(asked,knight),isa(other,knight)))), [~(truth(isa(other,knight)))]

Gamma_78: (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