knight(X),knave(X) -> []. knight(X),normal(X) -> []. knight(X), knave(X), normal(X). hrank2(Y,Z) <- hrank3(X,Y,Z), knight(X). hrank3(X,Y,Z),knave(X),hrank2(Y,Z) -> []. knight(X), normal(X) <- hrank2(X,Y). knight(X), knave(Y) <- hrank2(X,Y). normal(X) <- hrank2(X,Y), knight(Y). knave(Y) <- hrank2(X,Y), knight(Y). hrank2(X,Y), knight(Y) <- knight(X). hrank2(X,Y) <- normal(X), knave(Y). normal(a), normal(b), normal(c). knight(a), knight(b), knight(c). knave(a), knave(b), knave(c). hrank3(a,b,c). hrank3(b,c,a). hrank3(c,b,a), hrank3(c,a,b). goal hrank3(c,b,a) -> []. /* Proof: ====== 1 : knight(B),knave(B) -> [axiom] 4 : hrank3(B,C,D),knight(B) -> hrank2(C,D) [axiom] 5 : hrank3(B,C,D),knave(B),hrank2(C,D) -> [axiom] 7 : hrank2(B,C) -> knight(B),knave(C) [axiom] 9 : hrank2(B,C),knight(C) -> knave(C) [axiom] 10 : knight(B) -> hrank2(B,C),knight(C) [axiom] 13 : knight(a),knight(b),knight(c) [axiom] 15 : hrank3(a,b,c) [axiom] 16 : hrank3(b,c,a) [axiom] 17 : hrank3(c,b,a),hrank3(c,a,b) [axiom] 18 + hrank3(c,b,a) -> [axiom] 19 + hrank3(c,a,b) [reduction of 17 by [18]] 20 : true,knight(a) -> hrank2(b,c) [negative chaining of 15 from 4] 21 : true,knight(b) -> hrank2(c,a) [negative chaining of 16 from 4] 22 + true,knight(c) -> hrank2(a,b) [negative chaining of 19 from 4] 23 : true,knave(a),hrank2(b,c) -> [negative chaining of 15 from 5] 24 : true,knave(b),hrank2(c,a) -> [negative chaining of 16 from 5] 25 + true,knave(c),hrank2(a,b) -> [negative chaining of 19 from 5] 29 : true,knight(a) -> knight(b),knave(c) [negative chaining of 20 from 7] 31 : true,knight(b),knight(a) -> knave(a) [negative chaining of 21 from 9] 33 : true,knight(b) -> knight(c),knave(a) [negative chaining of 21 from 7] 35 : true,knight(b),knave(a) -> knight(c) [negative chaining of 10 from 23] 38 : true,knight(c),knave(b) -> knight(a) [negative chaining of 10 from 24] 42 + true -> knight(a),knight(b),hrank2(a,b) [negative chaining of 13 from 22] 48 + true,knave(a),knight(b) -> hrank2(a,b) [negative chaining of 35 from 22] 52 + true,knave(a),knight(b),knight(b) -> knave(b) [negative chaining of 48 from 9] 56 + knave(a),knight(b) -> knave(b) [condensement of 52] 60 : true,knave(b) -> knight(a),knight(b),knight(a) [negative chaining of 13 from 38] 62 : knave(b) -> knight(b),knight(a) [condensement of 60] 63 : knave(b) -> knight(a) [reduction of 62 by [1]] 67 + true -> knight(a),knight(b),knight(a),knave(b) [negative chaining of 42 from 7] 70 + knight(b),knight(a),knave(b) [condensement of 67] 71 + knight(b),knight(a) [reduction of 70 by [63]] 74 + true,knave(a) -> knight(a),knave(b) [negative chaining of 71 from 56] 76 + knave(a) -> knave(b) [reduction of 74 by [1]] 80 + true,knave(a) -> knight(a) [negative chaining of 76 from 63] 81 + knave(a) -> [reduction of 80 by [1]] 82 + knight(b) -> knight(c) [reduction of 33 by [81]] 86 + knight(b),knight(a) -> [reduction of 31 by [81]] 88 + knight(a) -> knave(c) [reduction of 29 by [86]] 90 + true,knight(b) -> hrank2(a,b) [negative chaining of 82 from 22] 93 + true,knight(a),hrank2(a,b) -> [negative chaining of 88 from 25] 96 + true,knight(b),knight(b) -> knave(b) [negative chaining of 90 from 9] 101 + knight(b) -> knave(b) [condensement of 96] 103 + true,knight(a),knight(a) -> knight(b) [negative chaining of 10 from 93] 105 + knight(a) -> knight(b) [condensement of 103] 106 + knight(a) -> [reduction of 105 by [86]] 107 + knave(b) -> [reduction of 63 by [106]] 108 + knight(b) [reduction of 71 by [106]] 110 + false [reduction of 101 by [108,107]] Length = 50, Depth = 19 Total time: 5770 milliseconds Number of search inferences: 62 Number of kept clauses: 74 */