%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : PUZ032-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 : n025.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:09 EDT 2024
% Result : Unsatisfiable 0.15s 0.57s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.09 % Problem : PUZ032-1 : TPTP v8.2.0. Released v1.0.0.
% 0.00/0.09 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.09/0.30 % Computer : n025.cluster.edu
% 0.09/0.30 % Model : x86_64 x86_64
% 0.09/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.30 % Memory : 8042.1875MB
% 0.09/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.30 % CPULimit : 300
% 0.09/0.30 % WCLimit : 300
% 0.09/0.30 % DateTime : Tue Jun 18 09:47:54 EDT 2024
% 0.15/0.30 % CPUTime :
% 0.15/0.54 start to proof:theBenchmark
% 0.15/0.57 %-------------------------------------------
% 0.15/0.57 % File :CSE---1.7
% 0.15/0.57 % Problem :theBenchmark
% 0.15/0.57 % Transform :cnf
% 0.15/0.57 % Format :tptp:raw
% 0.15/0.57 % Command :java -jar mcs_scs.jar %d %s
% 0.15/0.57
% 0.15/0.57 % Result :Theorem 0.000000s
% 0.15/0.57 % Output :CNFRefutation 0.000000s
% 0.15/0.57 %-------------------------------------------
% 0.15/0.57 %------------------------------------------------------------------------------
% 0.15/0.57 % File : PUZ032-1 : TPTP v8.2.0. Released v1.0.0.
% 0.15/0.57 % Domain : Puzzles
% 0.15/0.57 % Problem : Knights and Knaves #26
% 0.15/0.57 % Version : Especial.
% 0.15/0.57 % English : On a certain island the inhabitants are partitioned into those
% 0.15/0.57 % who always tell the truth and those who always lie. I landed on
% 0.15/0.57 % the island and met three inhabitants A, B, and C. I asked A,
% 0.15/0.57 % 'Are you a truthteller or a liar?' He mumbled something which I
% 0.15/0.57 % couldn't make out. I asked B what A had said. B replied, 'A
% 0.15/0.57 % said he was a liar'. C then volunteered, 'Don't believe B, he's
% 0.15/0.57 % lying!' Prove C is a truthteller.
% 0.15/0.57
% 0.15/0.57 % Refs : [Smu78] Smullyan (1978), What is the Name of this Book?
% 0.15/0.57 % : [LO85] Lusk & Overbeek (1985), Non-Horn Problems
% 0.15/0.57 % Source : [LO85]
% 0.15/0.57 % Names : Problem 26 [Smu78]
% 0.15/0.57 % : Truthtellers and the Liars [LO85]
% 0.15/0.57 % : tandl.ver1.in [ANL]
% 0.15/0.57
% 0.15/0.57 % Status : Unsatisfiable
% 0.15/0.57 % Rating : 0.00 v2.2.1, 0.25 v2.1.0, 0.00 v2.0.0
% 0.15/0.57 % Syntax : Number of clauses : 10 ( 4 unt; 2 nHn; 9 RR)
% 0.15/0.57 % Number of literals : 20 ( 0 equ; 11 neg)
% 0.15/0.57 % Maximal clause size : 3 ( 2 avg)
% 0.15/0.57 % Maximal term depth : 4 ( 1 avg)
% 0.15/0.57 % Number of predicates : 1 ( 1 usr; 0 prp; 1-1 aty)
% 0.15/0.57 % Number of functors : 7 ( 7 usr; 4 con; 0-2 aty)
% 0.15/0.57 % Number of variables : 10 ( 0 sgn)
% 0.15/0.57 % SPC : CNF_UNS_RFO_NEQ_NHN
% 0.15/0.57
% 0.15/0.57 % Comments :
% 0.15/0.57 %------------------------------------------------------------------------------
% 0.15/0.57 %----Include axioms for truthtellers and liars
% 0.15/0.57 include('Axioms/PUZ002-0.ax').
% 0.15/0.57 %------------------------------------------------------------------------------
% 0.15/0.57 cnf(a_mumbles,hypothesis,
% 0.15/0.57 a_truth(says(a,mumble)) ).
% 0.15/0.57
% 0.15/0.57 cnf(b_says_a_says_hes_a_liar,hypothesis,
% 0.15/0.57 a_truth(says(b,says(a,liar(a)))) ).
% 0.15/0.57
% 0.15/0.57 cnf(c_says_b_is_a_liar,hypothesis,
% 0.15/0.57 a_truth(says(c,liar(b))) ).
% 0.15/0.57
% 0.15/0.57 cnf(prove_c_is_a_truthteller,negated_conjecture,
% 0.15/0.57 ~ a_truth(truthteller(c)) ).
% 0.15/0.57
% 0.15/0.57 %------------------------------------------------------------------------------
% 0.15/0.57 %-------------------------------------------
% 0.15/0.57 % Proof found
% 0.15/0.57 % SZS status Theorem for theBenchmark
% 0.15/0.57 % SZS output start Proof
% 0.15/0.57 %ClaNum:10(EqnAxiom:0)
% 0.15/0.57 %VarNum:20(SingletonVarNum:10)
% 0.15/0.57 %MaxLitNum:3
% 0.15/0.57 %MaxfuncDepth:3
% 0.15/0.57 %SharedTerms:15
% 0.15/0.57 %goalClause: 4
% 0.15/0.57 %singleGoalClaCount:1
% 0.15/0.57 [1]P1(f6(a1,a2))
% 0.15/0.57 [4]~P1(f7(a3))
% 0.15/0.57 [2]P1(f6(a3,f5(a4)))
% 0.15/0.57 [3]P1(f6(a4,f6(a1,f5(a1))))
% 0.15/0.57 [5]P1(f5(x51))+P1(f7(x51))
% 0.15/0.57 [6]~P1(f5(x61))+~P1(f7(x61))
% 0.15/0.57 [7]P1(x71)+~P1(f6(x72,x71))+P1(f5(x72))
% 0.15/0.57 [8]~P1(x82)+~P1(f6(x81,x82))+P1(f7(x81))
% 0.15/0.57 [9]P1(x91)+~P1(f6(x92,x91))+~P1(f7(x92))
% 0.15/0.57 [10]~P1(x101)+~P1(f6(x102,x101))+~P1(f5(x102))
% 0.15/0.57 %EqnAxiom
% 0.15/0.57
% 0.15/0.57 %-------------------------------------------
% 0.15/0.57 cnf(13,plain,
% 0.15/0.57 (~P1(f5(a4))),
% 0.15/0.57 inference(scs_inference,[],[4,2,5,8])).
% 0.15/0.57 cnf(15,plain,
% 0.15/0.57 (P1(f6(a1,f5(a1)))),
% 0.15/0.57 inference(scs_inference,[],[4,2,3,5,8,7])).
% 0.15/0.57 cnf(18,plain,
% 0.15/0.57 (P1(f5(a1))+~P1(f7(a4))),
% 0.15/0.57 inference(scs_inference,[],[3,9,7])).
% 0.15/0.57 cnf(19,plain,
% 0.15/0.57 (~P1(f7(a4))),
% 0.15/0.57 inference(scs_inference,[],[15,18,10])).
% 0.15/0.57 cnf(20,plain,
% 0.15/0.57 ($false),
% 0.15/0.57 inference(scs_inference,[],[19,13,5]),
% 0.15/0.57 ['proof']).
% 0.15/0.57 % SZS output end Proof
% 0.15/0.57 % Total time :0.000000s
%------------------------------------------------------------------------------