tff(inhabitant_decl,type,inhabitant: $tType ). tff(mel_decl,type,mel: inhabitant ). tff(zoey_decl,type,zoey: inhabitant ). tff(is_knight_decl,type,is_knight: inhabitant > $o ). tff(is_knave_decl,type,is_knave: inhabitant > $o ). tff(says_decl,type,says: ( inhabitant * $o ) > $o ). tff(knights_xor_knaves,axiom, ! [I: inhabitant] : ( is_knight(I) <~> is_knave(I) ) ). tff(knights_tell_truth,axiom, ! [I: inhabitant,S: $o] : ( ( is_knight(I) & says(I,S) ) => S ) ). tff(knaves_lie,axiom, ! [I: inhabitant,S: $o] : ( ( is_knave(I) & says(I,S) ) => ~ S ) ). tff(zoey_speaks,axiom, says(zoey,is_knave(mel)) ). tff(mel_speaks,axiom, says(mel, ~ is_knave(zoey) & ~ is_knave(mel)) ). tff(knight_and_knave,conjecture, ? [Knight: inhabitant,Knave: inhabitant] : ( is_knight(Knight) & is_knave(Knave) ) ).