%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : PUZ027-1 : TPTP v8.2.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n016.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 2.20s 2.38s
% Output : CNFRefutation 2.20s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.22 % Problem : PUZ027-1 : TPTP v8.2.0. Released v1.0.0.
% 0.07/0.22 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.43 % Computer : n016.cluster.edu
% 0.12/0.43 % Model : x86_64 x86_64
% 0.12/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.43 % Memory : 8042.1875MB
% 0.12/0.43 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.44 % CPULimit : 300
% 0.12/0.44 % WCLimit : 300
% 0.12/0.44 % DateTime : Tue Jun 18 09:49:39 EDT 2024
% 0.12/0.44 % CPUTime :
% 0.52/0.67 start to proof:theBenchmark
% 2.20/2.37 %-------------------------------------------
% 2.20/2.37 % File :CSE---1.7
% 2.20/2.37 % Problem :theBenchmark
% 2.20/2.37 % Transform :cnf
% 2.20/2.37 % Format :tptp:raw
% 2.20/2.37 % Command :java -jar mcs_scs.jar %d %s
% 2.20/2.37
% 2.20/2.37 % Result :Theorem 1.660000s
% 2.20/2.37 % Output :CNFRefutation 1.660000s
% 2.20/2.37 %-------------------------------------------
% 2.20/2.37 %--------------------------------------------------------------------------
% 2.20/2.37 % File : PUZ027-1 : TPTP v8.2.0. Released v1.0.0.
% 2.20/2.37 % Domain : Puzzles
% 2.20/2.37 % Problem : Knights and Knaves #42
% 2.20/2.37 % Version : Especial.
% 2.20/2.37 % English : There is an island with exactly three types of people -
% 2.20/2.37 % truthtellers who always tell the truth, and liars who always
% 2.20/2.37 % lie, and normals who sometimes tell the truth and sometimes
% 2.20/2.37 % lie. Liars are said to be of the lowest rank, normals are
% 2.20/2.37 % middle rank, and truthtellers of the highest rank. Two people
% 2.20/2.37 % A and B on the island make the following statements. A: I am
% 2.20/2.37 % of lower rank than B. B: That's not true! What are the ranks
% 2.20/2.37 % of A and B, and which of the two statements are true? Answer:
% 2.20/2.37 % A is a normal and B is a normal.
% 2.20/2.37
% 2.20/2.37 % Refs : [Smu78] Smullyan (1978), What is the Name of this Book?
% 2.20/2.37 % Source : [ANL]
% 2.20/2.37 % Names : Problem 42 [Smu78]
% 2.20/2.37 % : tandl42.ver1.in [ANL]
% 2.20/2.37
% 2.20/2.37 % Status : Unsatisfiable
% 2.20/2.37 % Rating : 0.00 v2.0.0
% 2.20/2.37 % Syntax : Number of clauses : 32 ( 4 unt; 9 nHn; 29 RR)
% 2.20/2.37 % Number of literals : 88 ( 0 equ; 53 neg)
% 2.20/2.37 % Maximal clause size : 4 ( 2 avg)
% 2.20/2.37 % Maximal term depth : 3 ( 1 avg)
% 2.20/2.37 % Number of predicates : 2 ( 2 usr; 0 prp; 1-1 aty)
% 2.20/2.37 % Number of functors : 17 ( 17 usr; 11 con; 0-2 aty)
% 2.20/2.37 % Number of variables : 36 ( 3 sgn)
% 2.20/2.37 % SPC : CNF_UNS_RFO_NEQ_NHN
% 2.20/2.37
% 2.20/2.37 % Comments :
% 2.20/2.37 %--------------------------------------------------------------------------
% 2.20/2.37 %----Include axioms on truthtellers, liars and normal people
% 2.20/2.37 include('Axioms/PUZ003-0.ax').
% 2.20/2.37 %--------------------------------------------------------------------------
% 2.20/2.37 %----The next 12 clause define lower thand and not lower than
% 2.20/2.37 cnf(not_lower_is_irreflexive,axiom,
% 2.20/2.37 a_truth(not_lower(X,X)) ).
% 2.20/2.37
% 2.20/2.37 cnf(not_not_lower_and_lower,axiom,
% 2.20/2.37 ( ~ a_truth(not_lower(X,Y))
% 2.20/2.37 | ~ a_truth(lower(X,Y)) ) ).
% 2.20/2.37
% 2.20/2.37 cnf(not_lower_or_lower,axiom,
% 2.20/2.37 ( a_truth(not_lower(X,Y))
% 2.20/2.37 | a_truth(lower(X,Y)) ) ).
% 2.20/2.37
% 2.20/2.37 cnf(liars_lowest,axiom,
% 2.20/2.37 ( ~ a_truth(lower(X,Y))
% 2.20/2.37 | ~ a_truth(liar(X))
% 2.20/2.37 | a_truth(normal(Y))
% 2.20/2.38 | a_truth(truthteller(Y)) ) ).
% 2.20/2.38
% 2.20/2.38 cnf(truthtellers_highest,axiom,
% 2.20/2.38 ( ~ a_truth(lower(X,Y))
% 2.20/2.38 | ~ a_truth(normal(X))
% 2.20/2.38 | a_truth(truthteller(Y)) ) ).
% 2.20/2.38
% 2.20/2.38 cnf(truthtellers_lower_than_no_one,axiom,
% 2.20/2.38 ( ~ a_truth(lower(X,Y))
% 2.20/2.38 | ~ a_truth(truthteller(X)) ) ).
% 2.20/2.38
% 2.20/2.38 cnf(normal_and_liars_lower_than_truthtellers,axiom,
% 2.20/2.38 ( ~ a_truth(lower(X,Y))
% 2.20/2.38 | ~ a_truth(truthteller(Y))
% 2.20/2.38 | a_truth(normal(X))
% 2.20/2.38 | a_truth(liar(X)) ) ).
% 2.20/2.38
% 2.20/2.38 cnf(liars_lower_than_normal,axiom,
% 2.20/2.38 ( ~ a_truth(lower(X,Y))
% 2.20/2.38 | ~ a_truth(normal(Y))
% 2.20/2.38 | a_truth(liar(X)) ) ).
% 2.20/2.38
% 2.20/2.38 cnf(no_one_lower_than_liars,axiom,
% 2.20/2.38 ( ~ a_truth(lower(X,Y))
% 2.20/2.38 | ~ a_truth(liar(Y)) ) ).
% 2.20/2.38
% 2.20/2.38 cnf(not_lower_than_truthteller,axiom,
% 2.20/2.38 ( ~ a_truth(not_lower(X,Y))
% 2.20/2.38 | ~ a_truth(truthteller(X))
% 2.20/2.38 | a_truth(truthteller(Y))
% 2.20/2.38 | a_truth(lower(Y,X)) ) ).
% 2.20/2.38
% 2.20/2.38 cnf(not_lower_than_liar,axiom,
% 2.20/2.38 ( ~ a_truth(not_lower(X,Y))
% 2.20/2.38 | ~ a_truth(liar(X))
% 2.20/2.38 | a_truth(liar(Y))
% 2.20/2.38 | a_truth(lower(Y,X)) ) ).
% 2.20/2.38
% 2.20/2.38 cnf(not_lower_than_normal,axiom,
% 2.20/2.38 ( ~ a_truth(not_lower(X,Y))
% 2.20/2.38 | ~ a_truth(normal(X))
% 2.20/2.38 | a_truth(normal(Y))
% 2.20/2.38 | a_truth(lower(Y,X)) ) ).
% 2.20/2.38
% 2.20/2.38 cnf(a_says_a_lower_than_b,hypothesis,
% 2.20/2.38 a_truth(says(a,lower(a,b))) ).
% 2.20/2.38
% 2.20/2.38 cnf(b_says_a_not_lower_than_b,hypothesis,
% 2.20/2.38 a_truth(says(b,not_lower(a,b))) ).
% 2.20/2.38
% 2.20/2.38 %----This is an honest way of doing this. A simpler version could simply
% 2.20/2.38 %----prove that A is a normal and B is a normal.
% 2.20/2.38 cnf(a_and_b_truthteller,hypothesis,
% 2.20/2.38 ( ~ a_truth(truthteller(a))
% 2.20/2.38 | ~ a_truth(truthteller(b))
% 2.20/2.38 | answer(a_and_b_truthteller) ) ).
% 2.20/2.38
% 2.20/2.38 cnf(a_truthteller_b_normal,hypothesis,
% 2.20/2.38 ( ~ a_truth(truthteller(a))
% 2.20/2.38 | ~ a_truth(normal(b))
% 2.20/2.38 | answer(a_truthteller_b_normal) ) ).
% 2.20/2.38
% 2.20/2.38 cnf(a_truthteller_b_liar,hypothesis,
% 2.20/2.38 ( ~ a_truth(truthteller(a))
% 2.20/2.38 | ~ a_truth(liar(b))
% 2.20/2.38 | answer(a_truthteller_b_liar) ) ).
% 2.20/2.38
% 2.20/2.38 cnf(a_normal_b_truthteller,hypothesis,
% 2.20/2.38 ( ~ a_truth(normal(a))
% 2.20/2.38 | ~ a_truth(truthteller(b))
% 2.20/2.38 | answer(a_normal_b_truthteller) ) ).
% 2.20/2.38
% 2.20/2.38 cnf(a_and_b_normal,hypothesis,
% 2.20/2.38 ( ~ a_truth(normal(a))
% 2.20/2.38 | ~ a_truth(normal(b))
% 2.20/2.38 | answer(a_and_b_normal) ) ).
% 2.20/2.38
% 2.20/2.38 cnf(a_normal_b_liar,hypothesis,
% 2.20/2.38 ( ~ a_truth(normal(a))
% 2.20/2.38 | ~ a_truth(liar(b))
% 2.20/2.38 | answer(a_normal_b_liar) ) ).
% 2.20/2.38
% 2.20/2.38 cnf(a_liar_b_truthteller,hypothesis,
% 2.20/2.38 ( ~ a_truth(liar(a))
% 2.20/2.38 | ~ a_truth(truthteller(b))
% 2.20/2.38 | answer(a_liar_b_truthteller) ) ).
% 2.20/2.38
% 2.20/2.38 cnf(a_liar_b_normal,hypothesis,
% 2.20/2.38 ( ~ a_truth(liar(a))
% 2.20/2.38 | ~ a_truth(normal(b))
% 2.20/2.38 | answer(a_liar_b_normal) ) ).
% 2.20/2.38
% 2.20/2.38 cnf(a_and_b_liar,hypothesis,
% 2.20/2.38 ( ~ a_truth(liar(a))
% 2.20/2.38 | ~ a_truth(liar(b))
% 2.20/2.38 | answer(a_and_b_liar) ) ).
% 2.20/2.38
% 2.20/2.38 cnf(prove_there_is_an_answer,negated_conjecture,
% 2.20/2.38 ~ answer(Answer) ).
% 2.20/2.38
% 2.20/2.38 %--------------------------------------------------------------------------
% 2.20/2.38 %-------------------------------------------
% 2.20/2.38 % Proof found
% 2.20/2.38 % SZS status Theorem for theBenchmark
% 2.20/2.38 % SZS output start Proof
% 2.20/2.38 %ClaNum:32(EqnAxiom:0)
% 2.20/2.38 %VarNum:80(SingletonVarNum:36)
% 2.20/2.38 %MaxLitNum:4
% 2.20/2.38 %MaxfuncDepth:2
% 2.20/2.38 %SharedTerms:38
% 2.20/2.38 %goalClause: 4
% 2.20/2.38 %singleGoalClaCount:1
% 2.20/2.38 [2]P1(f16(a2,f13(a2,a3)))
% 2.20/2.38 [3]P1(f16(a3,f1(a2,a3)))
% 2.20/2.38 [4]~P2(x41)
% 2.20/2.38 [1]P1(f1(x11,x11))
% 2.20/2.38 [15]~P1(f14(x151))+~P1(f17(x151))
% 2.20/2.38 [16]~P1(f15(x161))+~P1(f17(x161))
% 2.20/2.38 [17]~P1(f15(x171))+~P1(f14(x171))
% 2.20/2.38 [18]P1(f13(x181,x182))+P1(f1(x181,x182))
% 2.20/2.38 [19]~P1(f17(x191))+~P1(f13(x191,x192))
% 2.20/2.38 [20]~P1(f14(x201))+~P1(f13(x202,x201))
% 2.20/2.38 [29]~P1(f13(x291,x292))+~P1(f1(x291,x292))
% 2.20/2.38 [5]P2(a4)+~P1(f17(a2))+~P1(f17(a3))
% 2.20/2.38 [6]P2(a7)+~P1(f15(a3))+~P1(f17(a2))
% 2.20/2.38 [7]P2(a8)+~P1(f14(a3))+~P1(f17(a2))
% 2.20/2.38 [8]P2(a9)+~P1(f15(a2))+~P1(f17(a3))
% 2.20/2.38 [9]P2(a5)+~P1(f15(a2))+~P1(f15(a3))
% 2.20/2.38 [10]P2(a10)+~P1(f14(a3))+~P1(f15(a2))
% 2.20/2.38 [11]P2(a11)+~P1(f14(a2))+~P1(f17(a3))
% 2.20/2.38 [12]P2(a12)+~P1(f14(a2))+~P1(f15(a3))
% 2.20/2.38 [13]P2(a6)+~P1(f14(a2))+~P1(f14(a3))
% 2.20/2.38 [14]P1(f14(x141))+P1(f15(x141))+P1(f17(x141))
% 2.20/2.38 [21]P1(x211)+~P1(f16(x212,x211))+~P1(f17(x212))
% 2.20/2.38 [22]~P1(x221)+~P1(f16(x222,x221))+~P1(f14(x222))
% 2.20/2.38 [24]~P1(f13(x242,x241))+P1(f17(x241))+~P1(f15(x242))
% 2.20/2.38 [25]~P1(f13(x251,x252))+P1(f14(x251))+~P1(f15(x252))
% 2.20/2.38 [23]P1(x231)+P1(f15(x232))+~P1(f16(x232,x231))+P1(f14(x232))
% 2.20/2.38 [26]~P1(x262)+P1(f15(x261))+~P1(f16(x261,x262))+P1(f17(x261))
% 2.20/2.38 [27]P1(f15(x271))+~P1(f13(x272,x271))+P1(f17(x271))+~P1(f14(x272))
% 2.20/2.38 [28]P1(f15(x281))+~P1(f13(x281,x282))+P1(f14(x281))+~P1(f17(x282))
% 2.20/2.38 [30]~P1(f17(x302))+~P1(f1(x302,x301))+P1(f17(x301))+P1(f13(x301,x302))
% 2.20/2.38 [31]~P1(f14(x312))+~P1(f1(x312,x311))+P1(f14(x311))+P1(f13(x311,x312))
% 2.20/2.38 [32]~P1(f15(x322))+~P1(f1(x322,x321))+P1(f15(x321))+P1(f13(x321,x322))
% 2.20/2.38 %EqnAxiom
% 2.20/2.38
% 2.20/2.38 %-------------------------------------------
% 2.20/2.38 cnf(39,plain,
% 2.20/2.38 (~P1(f15(a2))+~P1(f17(a3))),
% 2.20/2.38 inference(scs_inference,[],[4,8])).
% 2.20/2.38 cnf(40,plain,
% 2.20/2.38 (~P1(f15(a2))+~P1(f15(a3))),
% 2.20/2.38 inference(scs_inference,[],[4,9])).
% 2.20/2.38 cnf(41,plain,
% 2.20/2.38 (~P1(f14(a3))+~P1(f15(a2))),
% 2.20/2.38 inference(scs_inference,[],[4,10])).
% 2.20/2.38 cnf(51,plain,
% 2.20/2.38 (~P1(f1(a2,a3))+~P1(f14(a3))+P1(f15(a3))),
% 2.20/2.38 inference(scs_inference,[],[3,15,26])).
% 2.20/2.38 cnf(243,plain,
% 2.20/2.38 (~P1(f13(a2,a3))+~P1(f13(a2,x2431))+P1(f15(a2))),
% 2.20/2.38 inference(scs_inference,[],[2,19,26])).
% 2.20/2.38 cnf(244,plain,
% 2.20/2.38 (~P1(f13(a2,a3))+P1(f15(a2))),
% 2.20/2.38 inference(factoring_inference,[],[243])).
% 2.20/2.38 cnf(308,plain,
% 2.20/2.38 (P1(f15(a2))+P1(f1(a2,a3))),
% 2.20/2.38 inference(scs_inference,[],[244,18])).
% 2.20/2.38 cnf(498,plain,
% 2.20/2.38 (P1(f15(a3))+P1(f15(a2))+~P1(f14(a3))),
% 2.20/2.38 inference(scs_inference,[],[51,308])).
% 2.20/2.38 cnf(514,plain,
% 2.20/2.38 (P1(f15(a3))+~P1(f14(a3))),
% 2.20/2.38 inference(scs_inference,[],[498,41])).
% 2.20/2.38 cnf(530,plain,
% 2.20/2.38 (~P1(f14(a3))),
% 2.20/2.38 inference(scs_inference,[],[514,17])).
% 2.20/2.38 cnf(1033,plain,
% 2.20/2.38 (P1(f13(a2,a3))+~P1(f17(a2))+P1(f15(a2))),
% 2.20/2.38 inference(scs_inference,[],[2,15,23])).
% 2.20/2.38 cnf(1049,plain,
% 2.20/2.38 (P1(f15(a2))+~P1(f17(a2))),
% 2.20/2.38 inference(scs_inference,[],[1033,19])).
% 2.20/2.38 cnf(1065,plain,
% 2.20/2.38 (~P1(f17(a2))),
% 2.20/2.38 inference(scs_inference,[],[1049,16])).
% 2.20/2.38 cnf(1689,plain,
% 2.20/2.38 (~P1(f13(a2,a3))+~P1(f14(a2))),
% 2.20/2.38 inference(scs_inference,[],[2,1065,17,26])).
% 2.20/2.38 cnf(1735,plain,
% 2.20/2.38 (P1(f1(a2,a3))+~P1(f14(a2))),
% 2.20/2.38 inference(scs_inference,[],[1689,18])).
% 2.20/2.38 cnf(1781,plain,
% 2.20/2.38 (P1(f13(a3,a2))+~P1(f14(a2))),
% 2.20/2.38 inference(scs_inference,[],[530,1735,31])).
% 2.20/2.38 cnf(1827,plain,
% 2.20/2.38 (~P1(f14(a2))),
% 2.20/2.38 inference(scs_inference,[],[1781,20])).
% 2.20/2.38 cnf(2371,plain,
% 2.20/2.38 (P1(f15(a3))+~P1(f15(a2))),
% 2.20/2.38 inference(scs_inference,[],[530,39,14])).
% 2.20/2.38 cnf(2387,plain,
% 2.20/2.38 (~P1(f15(a2))),
% 2.20/2.38 inference(scs_inference,[],[2371,40])).
% 2.20/2.38 cnf(2395,plain,
% 2.20/2.38 ($false),
% 2.20/2.38 inference(scs_inference,[],[1827,2387,1065,14]),
% 2.20/2.38 ['proof']).
% 2.20/2.38 % SZS output end Proof
% 2.20/2.38 % Total time :1.660000s
%------------------------------------------------------------------------------