%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : PUZ026-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 : n032.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:06 EDT 2024
% Result : Unsatisfiable 58.52s 58.66s
% Output : CNFRefutation 58.76s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.08 % Problem : PUZ026-1 : TPTP v8.2.0. Released v1.0.0.
% 0.00/0.08 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.08/0.27 % Computer : n032.cluster.edu
% 0.08/0.27 % Model : x86_64 x86_64
% 0.08/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.27 % Memory : 8042.1875MB
% 0.08/0.27 % OS : Linux 3.10.0-693.el7.x86_64
% 0.08/0.27 % CPULimit : 300
% 0.08/0.27 % WCLimit : 300
% 0.08/0.27 % DateTime : Tue Jun 18 09:42:54 EDT 2024
% 0.08/0.27 % CPUTime :
% 0.12/0.53 start to proof:theBenchmark
% 58.52/58.65 %-------------------------------------------
% 58.52/58.65 % File :CSE---1.7
% 58.52/58.65 % Problem :theBenchmark
% 58.52/58.65 % Transform :cnf
% 58.52/58.65 % Format :tptp:raw
% 58.52/58.65 % Command :java -jar mcs_scs.jar %d %s
% 58.52/58.65
% 58.52/58.65 % Result :Theorem 58.000000s
% 58.52/58.65 % Output :CNFRefutation 58.000000s
% 58.52/58.65 %-------------------------------------------
% 58.52/58.66 %--------------------------------------------------------------------------
% 58.52/58.66 % File : PUZ026-1 : TPTP v8.2.0. Released v1.0.0.
% 58.52/58.66 % Domain : Puzzles
% 58.52/58.66 % Problem : Knights and Knaves #39
% 58.52/58.66 % Version : Especial.
% 58.52/58.66 % English : There is an island with exactly three types of people -
% 58.52/58.66 % truthtellers who always tell the truth, and liars who always
% 58.52/58.66 % lie, and normals who sometimes tell the truth and sometimes
% 58.52/58.66 % lie. We are given three people, A, B, C, one of whom is a
% 58.52/58.66 % truthteller, one a liar, and one a normal (but not neccesarily
% 58.52/58.66 % in that order). They make the following statements. A: I am
% 58.52/58.66 % normal; B: That is true. C: I am not normal. What are A,B,
% 58.52/58.66 % and C? Answer: A is a liar, B is a normal, and C is a truthteller.
% 58.52/58.66
% 58.52/58.66 % Refs : [Smu78] Smullyan (1978), What is the Name of this Book?
% 58.52/58.66 % Source : [ANL]
% 58.52/58.66 % Names : Problem 39 [Smu78]
% 58.52/58.66 % : tandl39.ver1.in [ANL]
% 58.52/58.66
% 58.52/58.66 % Status : Unsatisfiable
% 58.52/58.66 % Rating : 0.00 v2.5.0, 0.20 v2.4.0, 0.00 v2.1.0, 0.00 v2.0.0
% 58.52/58.66 % Syntax : Number of clauses : 23 ( 6 unt; 4 nHn; 21 RR)
% 58.52/58.66 % Number of literals : 54 ( 0 equ; 37 neg)
% 58.52/58.66 % Maximal clause size : 4 ( 2 avg)
% 58.52/58.66 % Maximal term depth : 3 ( 1 avg)
% 58.52/58.66 % Number of predicates : 2 ( 2 usr; 0 prp; 1-3 aty)
% 58.52/58.66 % Number of functors : 8 ( 8 usr; 3 con; 0-2 aty)
% 58.52/58.66 % Number of variables : 35 ( 9 sgn)
% 58.52/58.66 % SPC : CNF_UNS_RFO_NEQ_NHN
% 58.52/58.66
% 58.52/58.66 % Comments :
% 58.52/58.66 %--------------------------------------------------------------------------
% 58.52/58.66 %----Include axioms on truthtellers, liars and normal people
% 58.52/58.66 include('Axioms/PUZ003-0.ax').
% 58.52/58.66 %--------------------------------------------------------------------------
% 58.52/58.66 cnf(not_normal_and_not_normal,axiom,
% 58.52/58.66 ( ~ a_truth(not_normal(X))
% 58.52/58.66 | ~ a_truth(normal(X)) ) ).
% 58.52/58.66
% 58.52/58.66 cnf(normal_or_not_normal,axiom,
% 58.52/58.66 ( a_truth(not_normal(X))
% 58.52/58.66 | a_truth(normal(X)) ) ).
% 58.52/58.66
% 58.52/58.66 %----The next 6 clause says there is one each of normal, truthteller and
% 58.52/58.66 %----liar.
% 58.52/58.66 cnf(not_two_truthtellers1,axiom,
% 58.52/58.66 ( ~ people(X,Y,Z)
% 58.52/58.66 | ~ a_truth(truthteller(X))
% 58.52/58.66 | ~ a_truth(truthteller(Y)) ) ).
% 58.52/58.66
% 58.52/58.66 cnf(not_two_truthtellers2,axiom,
% 58.52/58.66 ( ~ people(X,Y,Z)
% 58.52/58.66 | ~ a_truth(truthteller(X))
% 58.52/58.66 | ~ a_truth(truthteller(Z)) ) ).
% 58.52/58.66
% 58.52/58.66 cnf(not_two_liars1,axiom,
% 58.52/58.66 ( ~ people(X,Y,Z)
% 58.52/58.66 | ~ a_truth(liar(X))
% 58.52/58.66 | ~ a_truth(liar(Y)) ) ).
% 58.52/58.66
% 58.52/58.66 cnf(not_two_liars2,axiom,
% 58.52/58.66 ( ~ people(X,Y,Z)
% 58.52/58.66 | ~ a_truth(liar(X))
% 58.52/58.66 | ~ a_truth(liar(Z)) ) ).
% 58.52/58.66
% 58.52/58.66 cnf(not_two_normal1,axiom,
% 58.52/58.66 ( ~ people(X,Y,Z)
% 58.52/58.66 | ~ a_truth(normal(X))
% 58.52/58.66 | ~ a_truth(normal(Y)) ) ).
% 58.52/58.66
% 58.52/58.66 cnf(not_two_normal2,axiom,
% 58.52/58.66 ( ~ people(X,Y,Z)
% 58.52/58.66 | ~ a_truth(normal(X))
% 58.52/58.66 | ~ a_truth(normal(Z)) ) ).
% 58.52/58.66
% 58.52/58.66 cnf(a_b_c_are_people,hypothesis,
% 58.52/58.66 people(a,b,c) ).
% 58.52/58.66
% 58.52/58.66 cnf(b_c_a_are_people,hypothesis,
% 58.52/58.66 people(b,c,a) ).
% 58.52/58.66
% 58.52/58.66 cnf(c_b_a_are_people,hypothesis,
% 58.52/58.66 people(c,b,a) ).
% 58.52/58.66
% 58.52/58.66 cnf(a_says_a_normal,hypothesis,
% 58.52/58.66 a_truth(says(a,normal(a))) ).
% 58.52/58.66
% 58.52/58.66 cnf(b_says_a_normal,hypothesis,
% 58.52/58.66 a_truth(says(b,normal(a))) ).
% 58.52/58.66
% 58.52/58.66 cnf(c_says_c_not_normal,hypothesis,
% 58.52/58.66 a_truth(says(c,not_normal(c))) ).
% 58.52/58.66
% 58.52/58.66 cnf(prove_one_of_each,negated_conjecture,
% 58.52/58.66 ( ~ a_truth(liar(Liar))
% 58.52/58.66 | ~ a_truth(normal(Normal))
% 58.52/58.66 | ~ a_truth(truthteller(Truthteller)) ) ).
% 58.52/58.66
% 58.52/58.66 %--------------------------------------------------------------------------
% 58.52/58.66 %-------------------------------------------
% 58.52/58.66 % Proof found
% 58.52/58.66 % SZS status Theorem for theBenchmark
% 58.52/58.66 % SZS output start Proof
% 58.52/58.67 %ClaNum:23(EqnAxiom:0)
% 58.52/58.67 %VarNum:64(SingletonVarNum:35)
% 58.52/58.67 %MaxLitNum:4
% 58.52/58.67 %MaxfuncDepth:2
% 58.52/58.67 %SharedTerms:14
% 58.52/58.67 %goalClause: 13
% 58.52/58.67 [4]P2(a1,a3,a4)
% 58.52/58.67 [5]P2(a3,a4,a1)
% 58.52/58.67 [6]P2(a4,a3,a1)
% 58.52/58.67 [1]P1(f6(a1,f2(a1)))
% 58.52/58.67 [2]P1(f6(a3,f2(a1)))
% 58.52/58.67 [3]P1(f6(a4,f7(a4)))
% 58.52/58.67 [7]P1(f7(x71))+P1(f2(x71))
% 58.52/58.67 [9]~P1(f5(x91))+~P1(f8(x91))
% 58.52/58.67 [10]~P1(f2(x101))+~P1(f8(x101))
% 58.52/58.67 [11]~P1(f2(x111))+~P1(f5(x111))
% 58.52/58.67 [12]~P1(f7(x121))+~P1(f2(x121))
% 58.52/58.67 [8]P1(f5(x81))+P1(f2(x81))+P1(f8(x81))
% 58.52/58.67 [14]P1(x141)+~P1(f6(x142,x141))+~P1(f8(x142))
% 58.52/58.67 [15]~P1(x151)+~P1(f6(x152,x151))+~P1(f5(x152))
% 58.52/58.67 [13]~P1(f8(x131))+~P1(f5(x132))+~P1(f2(x133))
% 58.52/58.67 [18]~P2(x182,x183,x181)+~P1(f8(x181))+~P1(f8(x182))
% 58.52/58.67 [19]~P2(x192,x191,x193)+~P1(f8(x191))+~P1(f8(x192))
% 58.52/58.67 [20]~P2(x202,x203,x201)+~P1(f5(x201))+~P1(f5(x202))
% 58.52/58.67 [21]~P2(x212,x211,x213)+~P1(f5(x211))+~P1(f5(x212))
% 58.52/58.67 [22]~P2(x222,x223,x221)+~P1(f2(x221))+~P1(f2(x222))
% 58.52/58.67 [23]~P2(x232,x231,x233)+~P1(f2(x231))+~P1(f2(x232))
% 58.52/58.67 [16]P1(x161)+P1(f2(x162))+~P1(f6(x162,x161))+P1(f5(x162))
% 58.52/58.67 [17]~P1(x172)+P1(f2(x171))+~P1(f6(x171,x172))+P1(f8(x171))
% 58.52/58.67 %EqnAxiom
% 58.52/58.67
% 58.52/58.67 %-------------------------------------------
% 58.61/58.75 cnf(24,plain,
% 58.61/58.75 (P1(f2(a1))+P1(f5(a1))),
% 58.61/58.75 inference(scs_inference,[],[1,16])).
% 58.61/58.75 cnf(44,plain,
% 58.61/58.75 (~P1(f8(x441))+P1(f7(x441))),
% 58.61/58.75 inference(scs_inference,[],[7,10])).
% 58.61/58.75 cnf(108,plain,
% 58.61/58.75 (~P1(f7(a4))+P1(f8(a4))+P1(f2(a4))),
% 58.61/58.75 inference(scs_inference,[],[3,17])).
% 58.61/58.75 cnf(109,plain,
% 58.61/58.75 (~P1(f2(a1))+P1(f8(a3))+P1(f2(a3))),
% 58.61/58.75 inference(scs_inference,[],[2,17])).
% 58.61/58.75 cnf(144,plain,
% 58.61/58.75 (P1(f2(a1))+P1(f5(a3))+P1(f2(a3))),
% 58.61/58.75 inference(scs_inference,[],[2,16])).
% 58.61/58.75 cnf(154,plain,
% 58.61/58.75 (P1(f8(a4))+P1(f2(a4))),
% 58.61/58.75 inference(scs_inference,[],[108,7])).
% 58.61/58.75 cnf(281,plain,
% 58.61/58.75 (P1(f2(a4))+~P1(f8(a3))),
% 58.61/58.75 inference(scs_inference,[],[5,19,154])).
% 58.61/58.75 cnf(361,plain,
% 58.61/58.75 (~P1(f2(a1))+P1(f7(a3))),
% 58.61/58.75 inference(scs_inference,[],[4,23,7])).
% 58.61/58.75 cnf(377,plain,
% 58.61/58.75 (P1(f7(a3))+P1(f5(a1))),
% 58.61/58.75 inference(scs_inference,[],[361,24])).
% 58.61/58.75 cnf(393,plain,
% 58.61/58.75 (P1(f5(a1))+~P1(f2(a3))),
% 58.61/58.75 inference(scs_inference,[],[377,12])).
% 58.61/58.75 cnf(409,plain,
% 58.61/58.75 (~P1(f2(a3))+~P1(f2(a1))),
% 58.61/58.75 inference(scs_inference,[],[393,11])).
% 58.61/58.75 cnf(676,plain,
% 58.61/58.75 (~P1(f2(a3))+P1(f7(a1))),
% 58.61/58.75 inference(scs_inference,[],[7,409])).
% 58.61/58.75 cnf(692,plain,
% 58.61/58.75 (P1(f7(a1))+P1(f8(a3))+P1(f5(a3))),
% 58.61/58.75 inference(scs_inference,[],[676,8])).
% 58.61/58.75 cnf(708,plain,
% 58.61/58.75 (P1(f8(a3))+P1(f5(a3))+~P1(f2(a1))),
% 58.61/58.75 inference(scs_inference,[],[692,12])).
% 58.61/58.75 cnf(740,plain,
% 58.61/58.75 (~P1(f2(a4))+P1(f7(a1))),
% 58.61/58.75 inference(scs_inference,[],[6,7,22])).
% 58.61/58.75 cnf(756,plain,
% 58.61/58.75 (P1(f7(a1))+P1(f8(a4))),
% 58.61/58.75 inference(scs_inference,[],[740,154])).
% 58.61/58.75 cnf(772,plain,
% 58.61/58.75 (P1(f8(a4))+~P1(f2(a1))),
% 58.61/58.75 inference(scs_inference,[],[756,12])).
% 58.61/58.75 cnf(788,plain,
% 58.61/58.75 (~P1(f2(a1))+~P1(f2(a4))),
% 58.61/58.75 inference(scs_inference,[],[772,10])).
% 58.61/58.75 cnf(804,plain,
% 58.61/58.75 (~P1(f2(a4))+P1(f5(a1))),
% 58.61/58.75 inference(scs_inference,[],[1,788,16])).
% 58.61/58.75 cnf(820,plain,
% 58.61/58.75 (P1(f5(a1))+~P1(f8(a3))),
% 58.61/58.75 inference(scs_inference,[],[804,281])).
% 58.61/58.75 cnf(915,plain,
% 58.61/58.75 (P1(f7(a1))+P1(f7(a4))),
% 58.61/58.75 inference(scs_inference,[],[7,740])).
% 58.61/58.75 cnf(931,plain,
% 58.61/58.75 (P1(f7(a4))+~P1(f2(a1))),
% 58.61/58.75 inference(scs_inference,[],[915,12])).
% 58.61/58.75 cnf(947,plain,
% 58.61/58.75 (P1(f7(a4))+P1(f5(a1))),
% 58.61/58.75 inference(scs_inference,[],[1,931,16])).
% 58.61/58.75 cnf(963,plain,
% 58.61/58.75 (P1(f7(a4))+~P1(f6(a1,f5(a1)))),
% 58.61/58.75 inference(scs_inference,[],[947,15])).
% 58.61/58.75 cnf(1245,plain,
% 58.61/58.75 (P1(f2(a1))+P1(f2(a3))+~P1(f8(a3))),
% 58.61/58.75 inference(scs_inference,[],[9,144])).
% 58.61/58.75 cnf(1261,plain,
% 58.61/58.75 (P1(f2(a3))+~P1(f8(a3))+~P1(f5(a1))),
% 58.61/58.75 inference(scs_inference,[],[1,1245,15])).
% 58.61/58.75 cnf(1277,plain,
% 58.61/58.75 (P1(f2(a3))+~P1(f8(a3))),
% 58.61/58.75 inference(scs_inference,[],[1261,820])).
% 58.61/58.75 cnf(1293,plain,
% 58.61/58.75 (~P1(f8(a3))),
% 58.61/58.75 inference(scs_inference,[],[1277,10])).
% 58.61/58.75 cnf(1294,plain,
% 58.61/58.75 (~P1(f2(a1))+P1(f2(a3))),
% 58.61/58.75 inference(scs_inference,[],[1293,109])).
% 58.61/58.75 cnf(1297,plain,
% 58.61/58.75 (P1(f5(a3))+~P1(f2(a1))),
% 58.61/58.75 inference(scs_inference,[],[1293,708])).
% 58.61/58.75 cnf(1309,plain,
% 58.61/58.75 (~P1(f2(a1))+~P1(f5(a3))),
% 58.61/58.75 inference(scs_inference,[],[1294,11])).
% 58.61/58.75 cnf(1357,plain,
% 58.61/58.75 (~P1(f2(a1))),
% 58.61/58.75 inference(scs_inference,[],[1297,1309])).
% 58.61/58.75 cnf(1358,plain,
% 58.61/58.76 (P1(f5(a1))),
% 58.61/58.76 inference(scs_inference,[],[1357,24])).
% 58.61/58.76 cnf(1360,plain,
% 58.61/58.76 (P1(f5(a3))+P1(f2(a3))),
% 58.61/58.76 inference(scs_inference,[],[1357,144])).
% 58.61/58.76 cnf(1364,plain,
% 58.61/58.76 (~P1(f8(x13641))+~P1(f2(x13642))),
% 58.61/58.76 inference(scs_inference,[],[1358,13])).
% 58.61/58.76 cnf(2775,plain,
% 58.61/58.76 (~P1(f6(a1,f5(a1)))+~P1(f2(a4))),
% 58.61/58.76 inference(scs_inference,[],[12,963])).
% 58.61/58.76 cnf(2851,plain,
% 58.61/58.76 (~P1(f6(a1,f5(a1)))+P1(f8(a4))),
% 58.61/58.76 inference(scs_inference,[],[2775,154])).
% 58.61/58.76 cnf(3531,plain,
% 58.61/58.76 (P1(f8(a4))+~P1(f7(a4))),
% 58.61/58.76 inference(scs_inference,[],[154,12])).
% 58.61/58.76 cnf(3607,plain,
% 58.61/58.76 (~P1(f2(x36071))+~P1(f7(a4))),
% 58.61/58.76 inference(scs_inference,[],[3531,1364])).
% 58.61/58.76 cnf(3683,plain,
% 58.61/58.76 (~P1(f7(a4))+P1(f7(x36831))),
% 58.61/58.76 inference(scs_inference,[],[3607,7])).
% 58.61/58.76 cnf(4213,plain,
% 58.61/58.76 (~P1(f8(x42131))+P1(f8(a4))),
% 58.61/58.76 inference(scs_inference,[],[154,1364])).
% 58.61/58.76 cnf(4289,plain,
% 58.61/58.76 (P1(f7(a4))+~P1(f8(x42891))),
% 58.61/58.76 inference(scs_inference,[],[4213,44])).
% 58.61/58.76 cnf(4365,plain,
% 58.61/58.76 (~P1(f8(x43651))+P1(f7(x43652))),
% 58.61/58.76 inference(scs_inference,[],[4289,3683])).
% 58.61/58.76 cnf(4441,plain,
% 58.61/58.76 (P1(f7(x44411))+~P1(f6(a1,f5(a1)))),
% 58.61/58.76 inference(scs_inference,[],[4365,2851])).
% 58.61/58.76 cnf(4517,plain,
% 58.61/58.76 (~P1(f6(a1,f5(a1)))+~P1(f2(x45171))),
% 58.61/58.76 inference(scs_inference,[],[4441,12])).
% 58.61/58.76 cnf(4896,plain,
% 58.61/58.76 (P1(f8(a4))+~P1(f6(a1,f2(a4)))),
% 58.61/58.76 inference(scs_inference,[],[1358,154,15])).
% 58.61/58.76 cnf(4972,plain,
% 58.61/58.76 (~P1(f6(a1,f2(a4)))+~P1(f2(a4))),
% 58.61/58.76 inference(scs_inference,[],[4896,10])).
% 58.61/58.76 cnf(5048,plain,
% 58.61/58.76 (~P1(f6(a1,f2(a4)))+P1(f7(a4))),
% 58.61/58.76 inference(scs_inference,[],[4972,7])).
% 58.61/58.76 cnf(5124,plain,
% 58.61/58.76 (~P1(f2(x51241))+~P1(f6(a1,f2(a4)))),
% 58.61/58.76 inference(scs_inference,[],[5048,3607])).
% 58.61/58.76 cnf(169278,plain,
% 58.61/58.76 (P1(f2(a3))),
% 58.61/58.76 inference(scs_inference,[],[4,1358,21,1360])).
% 58.61/58.76 cnf(169283,plain,
% 58.61/58.76 (~P1(f2(a4))),
% 58.61/58.76 inference(scs_inference,[],[4,5,1358,21,1360,4517,5124,23])).
% 58.61/58.76 cnf(169292,plain,
% 58.61/58.76 (P1(f8(a4))),
% 58.61/58.76 inference(scs_inference,[],[169283,154])).
% 58.61/58.76 cnf(169296,plain,
% 58.61/58.76 (~P1(f8(x1692961))),
% 58.61/58.76 inference(scs_inference,[],[169278,1364])).
% 58.61/58.76 cnf(169309,plain,
% 58.61/58.76 ($false),
% 58.61/58.76 inference(scs_inference,[],[169296,169292]),
% 58.61/58.76 ['proof']).
% 58.76/58.82 % SZS output end Proof
% 58.76/58.82 % Total time :58.000000s
%------------------------------------------------------------------------------