%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : PUZ023-1 : TPTP v8.2.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 13:42:05 EDT 2024
% Result : Unsatisfiable 0.45s 0.63s
% Output : CNFRefutation 0.45s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : PUZ023-1 : TPTP v8.2.0. Released v1.0.0.
% 0.07/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.34 % Computer : n011.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Tue Jun 18 10:05:54 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.45/0.58 start to proof:theBenchmark
% 0.45/0.62 %-------------------------------------------
% 0.45/0.62 % File :CSE---1.7
% 0.45/0.62 % Problem :theBenchmark
% 0.45/0.62 % Transform :cnf
% 0.45/0.62 % Format :tptp:raw
% 0.45/0.62 % Command :java -jar mcs_scs.jar %d %s
% 0.45/0.62
% 0.45/0.62 % Result :Theorem 0.000000s
% 0.45/0.62 % Output :CNFRefutation 0.000000s
% 0.45/0.62 %-------------------------------------------
% 0.45/0.62 %--------------------------------------------------------------------------
% 0.45/0.62 % File : PUZ023-1 : TPTP v8.2.0. Released v1.0.0.
% 0.45/0.62 % Domain : Puzzles
% 0.45/0.62 % Problem : Knights and Knaves #27
% 0.45/0.62 % Version : Especial.
% 0.45/0.62 % English : There is an island with exactly two types of people :
% 0.45/0.62 % truthtellers who always tell the truth and liars who always
% 0.45/0.62 % lie. There are a group of three people, A, B, and C on the
% 0.45/0.62 % island. A stranger passes by and asks A, "How many
% 0.45/0.62 % truthtellers are among you ?" A answers indistinctly. So the
% 0.45/0.62 % stranger asks B, "what did A say?". B replies "A said that
% 0.45/0.62 % there is exactly one truthteller among us." Then C says,
% 0.45/0.62 % "Don't believe B; he is lying!" What are B and C. Answer:
% 0.45/0.62 % B is a liar and C is a truth-teller.
% 0.45/0.62
% 0.45/0.62 % Refs : [Smu78] Smullyan (1978), What is the Name of this Book?
% 0.45/0.62 % Source : [ANL]
% 0.45/0.62 % Names : Problem 27 [Smu78]
% 0.45/0.62 % : tandl27.ver1.in [ANL]
% 0.45/0.62
% 0.45/0.62 % Status : Unsatisfiable
% 0.45/0.62 % Rating : 0.00 v2.0.0
% 0.45/0.62 % Syntax : Number of clauses : 22 ( 5 unt; 6 nHn; 21 RR)
% 0.45/0.62 % Number of literals : 65 ( 0 equ; 39 neg)
% 0.45/0.62 % Maximal clause size : 5 ( 2 avg)
% 0.45/0.62 % Maximal term depth : 3 ( 1 avg)
% 0.45/0.62 % Number of predicates : 3 ( 3 usr; 0 prp; 1-3 aty)
% 0.45/0.62 % Number of functors : 12 ( 12 usr; 9 con; 0-2 aty)
% 0.45/0.62 % Number of variables : 32 ( 4 sgn)
% 0.45/0.62 % SPC : CNF_UNS_RFO_NEQ_NHN
% 0.45/0.62
% 0.45/0.62 % Comments :
% 0.45/0.62 %--------------------------------------------------------------------------
% 0.45/0.62 %----Include axioms for truthtellers and liars
% 0.45/0.62 include('Axioms/PUZ002-0.ax').
% 0.45/0.62 %--------------------------------------------------------------------------
% 0.45/0.62 cnf(one_is_the_truthteller,axiom,
% 0.45/0.62 ( ~ people(X,Y,Z)
% 0.45/0.62 | ~ a_truth(one_truthteller)
% 0.45/0.62 | a_truth(truthteller(X))
% 0.45/0.62 | a_truth(truthteller(Y))
% 0.45/0.62 | a_truth(truthteller(Z)) ) ).
% 0.45/0.62
% 0.45/0.62 cnf(two_truthtellers1,axiom,
% 0.45/0.62 ( ~ people(X,Y,Z)
% 0.45/0.62 | ~ a_truth(truthteller(X))
% 0.45/0.62 | ~ a_truth(truthteller(Y))
% 0.45/0.62 | ~ a_truth(one_truthteller) ) ).
% 0.45/0.62
% 0.45/0.62 cnf(two_truthtellers2,axiom,
% 0.45/0.62 ( ~ people(X,Y,Z)
% 0.45/0.62 | ~ a_truth(truthteller(X))
% 0.45/0.62 | ~ a_truth(truthteller(Z))
% 0.45/0.62 | ~ a_truth(one_truthteller) ) ).
% 0.45/0.62
% 0.45/0.62 cnf(two_truthtellers3,axiom,
% 0.45/0.62 ( ~ people(X,Y,Z)
% 0.45/0.62 | ~ a_truth(truthteller(Y))
% 0.45/0.62 | ~ a_truth(truthteller(Z))
% 0.45/0.62 | ~ a_truth(one_truthteller) ) ).
% 0.45/0.62
% 0.45/0.62 cnf(identify_one_truthteller1,axiom,
% 0.45/0.62 ( ~ people(X,Y,Z)
% 0.45/0.63 | a_truth(one_truthteller)
% 0.45/0.63 | ~ a_truth(truthteller(X))
% 0.45/0.63 | a_truth(truthteller(Y))
% 0.45/0.63 | a_truth(truthteller(Z)) ) ).
% 0.45/0.63
% 0.45/0.63 cnf(identify_one_truthteller2,axiom,
% 0.45/0.63 ( ~ people(X,Y,Z)
% 0.45/0.63 | a_truth(one_truthteller)
% 0.45/0.63 | ~ a_truth(truthteller(Y))
% 0.45/0.63 | a_truth(truthteller(X))
% 0.45/0.63 | a_truth(truthteller(Z)) ) ).
% 0.45/0.63
% 0.45/0.63 cnf(identify_one_truthteller3,axiom,
% 0.45/0.63 ( ~ people(X,Y,Z)
% 0.45/0.63 | a_truth(one_truthteller)
% 0.45/0.63 | ~ a_truth(truthteller(Z))
% 0.45/0.63 | a_truth(truthteller(Y))
% 0.45/0.63 | a_truth(truthteller(X)) ) ).
% 0.45/0.63
% 0.45/0.63 cnf(a_b_and_c_are_people,hypothesis,
% 0.45/0.63 people(a,b,c) ).
% 0.45/0.63
% 0.45/0.63 cnf(a_says_garbage,hypothesis,
% 0.45/0.63 a_truth(says(a,garbage)) ).
% 0.45/0.63
% 0.45/0.63 cnf(b_says_a_says_one_truthteller,hypothesis,
% 0.45/0.63 a_truth(says(b,says(a,one_truthteller))) ).
% 0.45/0.63
% 0.45/0.63 cnf(c_says_b_lies,hypothesis,
% 0.45/0.63 a_truth(says(c,liar(b))) ).
% 0.45/0.63
% 0.45/0.63 %----This is an honest way of doing this. A simpler version could simply
% 0.45/0.63 %----prove that B is a liar and C is a truth-teller.
% 0.45/0.63 cnf(b_and_c_liars,hypothesis,
% 0.45/0.63 ( ~ a_truth(liar(b))
% 0.45/0.63 | ~ a_truth(liar(c))
% 0.45/0.63 | an_answer(b_and_c_liars) ) ).
% 0.45/0.63
% 0.45/0.63 cnf(b_liar_and_c_truthteller,hypothesis,
% 0.45/0.63 ( ~ a_truth(liar(b))
% 0.45/0.63 | ~ a_truth(truthteller(c))
% 0.45/0.63 | an_answer(b_liar_and_c_truthteller) ) ).
% 0.45/0.63
% 0.45/0.63 cnf(b_truthteller_and_c_liar,hypothesis,
% 0.45/0.63 ( ~ a_truth(truthteller(b))
% 0.45/0.63 | ~ a_truth(liar(c))
% 0.45/0.63 | an_answer(b_truthteller_and_c_liar) ) ).
% 0.45/0.63
% 0.45/0.63 cnf(b_and_c_truthtellers,hypothesis,
% 0.45/0.63 ( ~ a_truth(truthteller(b))
% 0.45/0.63 | ~ a_truth(truthteller(c))
% 0.45/0.63 | an_answer(b_and_c_truthtellers) ) ).
% 0.45/0.63
% 0.45/0.63 cnf(prove_there_is_an_answer,negated_conjecture,
% 0.45/0.63 ~ an_answer(X) ).
% 0.45/0.63
% 0.45/0.63 %--------------------------------------------------------------------------
% 0.45/0.63 %-------------------------------------------
% 0.45/0.63 % Proof found
% 0.45/0.63 % SZS status Theorem for theBenchmark
% 0.45/0.63 % SZS output start Proof
% 0.45/0.63 %ClaNum:22(EqnAxiom:0)
% 0.45/0.63 %VarNum:60(SingletonVarNum:32)
% 0.45/0.63 %MaxLitNum:5
% 0.45/0.63 %MaxfuncDepth:2
% 0.45/0.63 %SharedTerms:31
% 0.45/0.63 %goalClause: 5
% 0.45/0.63 %singleGoalClaCount:1
% 0.45/0.63 [3]P2(a1,a4,a3)
% 0.45/0.63 [1]P1(f9(a1,a2))
% 0.45/0.63 [2]P1(f9(a3,f10(a4)))
% 0.45/0.63 [4]P1(f9(a4,f9(a1,a11)))
% 0.45/0.63 [5]~P3(x51)
% 0.45/0.63 [6]P1(f10(x61))+P1(f12(x61))
% 0.45/0.63 [11]~P1(f10(x111))+~P1(f12(x111))
% 0.45/0.63 [7]P3(a5)+~P1(f10(a4))+~P1(f10(a3))
% 0.45/0.63 [8]P3(a6)+~P1(f12(a3))+~P1(f10(a4))
% 0.45/0.63 [9]P3(a8)+~P1(f12(a4))+~P1(f10(a3))
% 0.45/0.63 [10]P3(a7)+~P1(f12(a4))+~P1(f12(a3))
% 0.45/0.63 [12]P1(x121)+~P1(f9(x122,x121))+P1(f10(x122))
% 0.45/0.63 [13]~P1(x132)+~P1(f9(x131,x132))+P1(f12(x131))
% 0.45/0.63 [14]P1(x141)+~P1(f9(x142,x141))+~P1(f12(x142))
% 0.45/0.63 [15]~P1(x151)+~P1(f9(x152,x151))+~P1(f10(x152))
% 0.45/0.63 [17]~P2(x173,x172,x171)+~P1(a11)+~P1(f12(x171))+~P1(f12(x172))
% 0.45/0.63 [18]~P2(x182,x183,x181)+~P1(a11)+~P1(f12(x181))+~P1(f12(x182))
% 0.45/0.63 [19]~P2(x192,x191,x193)+~P1(a11)+~P1(f12(x191))+~P1(f12(x192))
% 0.45/0.63 [16]~P2(x163,x162,x161)+P1(f12(x161))+P1(f12(x162))+P1(f12(x163))+~P1(a11)
% 0.45/0.63 [20]~P2(x203,x202,x201)+P1(a11)+P1(f12(x201))+P1(f12(x202))+~P1(f12(x203))
% 0.45/0.63 [21]~P2(x212,x213,x211)+P1(a11)+P1(f12(x211))+P1(f12(x212))+~P1(f12(x213))
% 0.45/0.63 [22]~P2(x222,x221,x223)+P1(a11)+P1(f12(x221))+P1(f12(x222))+~P1(f12(x223))
% 0.45/0.63 %EqnAxiom
% 0.45/0.63
% 0.45/0.63 %-------------------------------------------
% 0.45/0.63 cnf(23,plain,
% 0.45/0.63 (~P1(f10(a4))+~P1(f10(a3))),
% 0.45/0.63 inference(scs_inference,[],[5,7])).
% 0.45/0.63 cnf(24,plain,
% 0.45/0.63 (~P1(f12(a3))+~P1(f10(a4))),
% 0.45/0.63 inference(scs_inference,[],[5,8])).
% 0.45/0.63 cnf(25,plain,
% 0.45/0.63 (~P1(f12(a4))+~P1(f10(a3))),
% 0.45/0.63 inference(scs_inference,[],[5,9])).
% 0.45/0.63 cnf(28,plain,
% 0.45/0.63 (P1(f12(a4))+~P1(f10(a3))),
% 0.45/0.63 inference(scs_inference,[],[23,6])).
% 0.45/0.63 cnf(29,plain,
% 0.45/0.63 (P1(f10(a3))+~P1(f10(a4))),
% 0.45/0.63 inference(scs_inference,[],[24,6])).
% 0.45/0.63 cnf(30,plain,
% 0.45/0.63 (~P1(f10(a3))),
% 0.45/0.63 inference(scs_inference,[],[25,28])).
% 0.45/0.63 cnf(31,plain,
% 0.45/0.63 (~P1(f10(a4))),
% 0.45/0.63 inference(scs_inference,[],[30,29])).
% 0.45/0.63 cnf(32,plain,
% 0.45/0.63 (P1(f10(a4))),
% 0.45/0.63 inference(scs_inference,[],[30,2,12])).
% 0.45/0.63 cnf(36,plain,
% 0.45/0.63 ($false),
% 0.45/0.63 inference(scs_inference,[],[31,32]),
% 0.45/0.63 ['proof']).
% 0.45/0.63 % SZS output end Proof
% 0.45/0.63 % Total time :0.000000s
%------------------------------------------------------------------------------