%--------------------------------------------------------------------------
% File     : PUZ032-1 : TPTP v2.1.0. Released v1.0.0.
% Domain   : Puzzles
% Problem  : Knights and Knaves #26
% Version  : Special.
% English  : On a certain island the inhabitants are partitioned into those
%            who always tell the truth and those who always lie. I landed on
%            the island and met three inhabitants A, B, and C. I asked A,
%            'Are you a truthteller or a liar?' He mumbled something which I
%            couldn't make out. I asked B what A had said. B replied, 'A
%            said he was a liar'. C then volunteered, 'Don't believe B, he's
%            lying!' What can you tell about A, B, and C?

% Refs     : [Smu78] Smullyan (1978), What is the Name of This Book? The Ri
%          : [LO85]  Lusk & Overbeek (1985), Non-Horn Problems
% Source   : [LO85]
% Names    : Problem 26 [Smu78]
%          : Truthtellers and the Liars [LO85]
%          : tandl.ver1.in [ANL]

% Status   : unsatisfiable
% Rating   : 0.22 v2.1.0, 0.00 v2.0.0
% Syntax   : Number of clauses    :   10 (   2 non-Horn;   4 unit;   9 RR)
%            Number of literals   :   20 (   0 equality)
%            Maximal clause size  :    3 (   2 average)
%            Number of predicates :    1 (   0 propositional; 1-1 arity)
%            Number of functors   :    7 (   4 constant; 0-2 arity)
%            Number of variables  :   10 (   0 singleton)
%            Maximal term depth   :    4 (   1 average)

% Comments : 
%          : tptp2X -f tptp -t rm_equality:rstfp PUZ032-1.p 
%--------------------------------------------------------------------------
input_clause(truthteller_or_liar,axiom,
    [++ a_truth(truthteller(X)),
     ++ a_truth(liar(X))]).

input_clause(not_both,axiom,
    [-- a_truth(truthteller(X)),
     -- a_truth(liar(X))]).

input_clause(truthtellers_tell_truth,axiom,
    [-- a_truth(truthteller(Truthteller)),
     -- a_truth(says(Truthteller, Statement)),
     ++ a_truth(Statement)]).

input_clause(liars_lie,axiom,
    [-- a_truth(liar(Liar)),
     -- a_truth(says(Liar, Statement)),
     -- a_truth(Statement)]).

input_clause(truths_are_told_by_truthtellers,axiom,
    [-- a_truth(Statement),
     -- a_truth(says(Truthteller, Statement)),
     ++ a_truth(truthteller(Truthteller))]).

input_clause(liars_are_told_by_liars,axiom,
    [++ a_truth(Statement),
     -- a_truth(says(Liar, Statement)),
     ++ a_truth(liar(Liar))]).

input_clause(a_mumbles,hypothesis,
    [++ a_truth(says(a, mumble))]).

input_clause(b_says_a_says_hes_a_liar,hypothesis,
    [++ a_truth(says(b, says(a, liar(a))))]).

input_clause(c_says_b_is_a_liar,hypothesis,
    [++ a_truth(says(c, liar(b)))]).

input_clause(prove_c_is_a_truthteller,conjecture,
    [-- a_truth(truthteller(c))]).
%--------------------------------------------------------------------------