%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : PUZ008-3 : TPTP v8.2.0. Released v1.2.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:02 EDT 2024 % Result : Unsatisfiable 58.41s 58.53s % Output : CNFRefutation 58.50s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.07 % Problem : PUZ008-3 : TPTP v8.2.0. Released v1.2.0. % 0.00/0.07 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.07/0.26 % Computer : n032.cluster.edu % 0.07/0.26 % Model : x86_64 x86_64 % 0.07/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.26 % Memory : 8042.1875MB % 0.07/0.26 % OS : Linux 3.10.0-693.el7.x86_64 % 0.07/0.26 % CPULimit : 300 % 0.07/0.26 % WCLimit : 300 % 0.07/0.26 % DateTime : Tue Jun 18 10:38:38 EDT 2024 % 0.07/0.26 % CPUTime : % 0.11/0.43 start to proof:theBenchmark % 58.33/58.51 %------------------------------------------- % 58.33/58.51 % File :CSE---1.7 % 58.33/58.51 % Problem :theBenchmark % 58.33/58.51 % Transform :cnf % 58.33/58.51 % Format :tptp:raw % 58.33/58.51 % Command :java -jar mcs_scs.jar %d %s % 58.33/58.51 % 58.33/58.51 % Result :Theorem 58.020000s % 58.33/58.51 % Output :CNFRefutation 58.020000s % 58.33/58.51 %------------------------------------------- % 58.41/58.53 %-------------------------------------------------------------------------- % 58.41/58.53 % File : PUZ008-3 : TPTP v8.2.0. Released v1.2.0. % 58.41/58.53 % Domain : Puzzles % 58.41/58.53 % Problem : Missionaries and Cannibals % 58.41/58.53 % Version : Especial. % 58.41/58.53 % Theorem formulation : Declarative, without subsumers. % 58.41/58.53 % English : There are 3 missionaries, 3 cannibals, and a boat on the west % 58.41/58.53 % bank of a river. All wish to cross, but the boat holds % 58.41/58.53 % at most 2 people. If the cannibals ever outnumber the % 58.41/58.53 % missionaries on either bank of the river the outnumbered % 58.41/58.53 % missionaries will be eaten. Can they all safely cross the % 58.41/58.53 % river? If so, how? (The boat cannot cross empty.) % 58.41/58.53 % 58.41/58.53 % Refs : [Rap95] Raptis (1995), Email to G. Sutcliffe % 58.41/58.53 % Source : [Rap95] % 58.41/58.53 % Names : % 58.41/58.53 % 58.41/58.53 % Status : Unsatisfiable % 58.41/58.53 % Rating : 0.00 v5.4.0, 0.06 v5.3.0, 0.15 v5.2.0, 0.08 v5.1.0, 0.06 v5.0.0, 0.07 v4.0.1, 0.00 v3.7.0, 0.14 v3.4.0, 0.20 v3.3.0, 0.00 v2.0.0 % 58.41/58.53 % Syntax : Number of clauses : 16 ( 4 unt; 0 nHn; 14 RR) % 58.41/58.53 % Number of literals : 48 ( 0 equ; 33 neg) % 58.41/58.53 % Maximal clause size : 4 ( 3 avg) % 58.41/58.53 % Maximal term depth : 6 ( 2 avg) % 58.41/58.53 % Number of predicates : 3 ( 3 usr; 0 prp; 2-3 aty) % 58.41/58.53 % Number of functors : 8 ( 8 usr; 3 con; 0-2 aty) % 58.41/58.53 % Number of variables : 47 ( 3 sgn) % 58.41/58.53 % SPC : CNF_UNS_RFO_NEQ_HRN % 58.41/58.53 % 58.41/58.53 % Comments : This is a repaired version of PUZ008-1. % 58.41/58.53 %-------------------------------------------------------------------------- % 58.41/58.53 %----Definition of safe % 58.41/58.53 cnf(no_missionaries_is_safe,axiom, % 58.41/58.53 safe(n0,X) ). % 58.41/58.53 % 58.41/58.53 cnf(same_or_more_missionaries_is_safe,axiom, % 58.41/58.53 ( ~ greater_or_equal(X,Y) % 58.41/58.53 | safe(X,Y) ) ). % 58.41/58.53 % 58.41/58.53 %----Definition of less than or equal % 58.41/58.53 cnf(great_eq_base,axiom, % 58.41/58.53 greater_or_equal(X,n0) ). % 58.41/58.53 % 58.41/58.53 cnf(great_eq_recursive,axiom, % 58.41/58.53 ( greater_or_equal(s(X),s(Y)) % 58.41/58.53 | ~ greater_or_equal(X,Y) ) ). % 58.41/58.53 % 58.41/58.53 %----Moving cannibals only % 58.41/58.53 cnf(cannibal_west_to_east,axiom, % 58.41/58.53 ( ~ achievable(west(m(X),c(s(Y))),boatonwest,east(m(Z),c(W))) % 58.41/58.53 | ~ safe(X,Y) % 58.41/58.53 | ~ safe(Z,s(W)) % 58.41/58.53 | achievable(west(m(X),c(Y)),boatoneast,east(m(Z),c(s(W)))) ) ). % 58.41/58.53 % 58.41/58.53 cnf(cannibal_east_to_west,axiom, % 58.41/58.53 ( ~ achievable(west(m(X),c(Y)),boatoneast,east(m(Z),c(s(W)))) % 58.41/58.53 | ~ safe(X,s(Y)) % 58.41/58.53 | ~ safe(Z,W) % 58.41/58.53 | achievable(west(m(X),c(s(Y))),boatonwest,east(m(Z),c(W))) ) ). % 58.41/58.53 % 58.41/58.53 cnf(two_cannibals_west_to_east,axiom, % 58.41/58.53 ( ~ achievable(west(m(X),c(s(s(Y)))),boatonwest,east(m(Z),c(W))) % 58.41/58.53 | ~ safe(X,Y) % 58.41/58.53 | ~ safe(Z,s(s(W))) % 58.41/58.53 | achievable(west(m(X),c(Y)),boatoneast,east(m(Z),c(s(s(W))))) ) ). % 58.41/58.53 % 58.41/58.53 cnf(two_cannibals_east_to_west,axiom, % 58.41/58.53 ( ~ achievable(west(m(X),c(Y)),boatoneast,east(m(Z),c(s(s(W))))) % 58.41/58.53 | ~ safe(X,s(s(Y))) % 58.41/58.53 | ~ safe(Z,W) % 58.41/58.53 | achievable(west(m(X),c(s(s(Y)))),boatonwest,east(m(Z),c(W))) ) ). % 58.41/58.53 % 58.41/58.53 %----Moving missionaries only % 58.41/58.53 cnf(missionary_west_to_east,axiom, % 58.41/58.53 ( ~ achievable(west(m(s(X)),c(Y)),boatonwest,east(m(Z),c(W))) % 58.41/58.53 | ~ safe(X,Y) % 58.41/58.53 | ~ safe(s(Z),W) % 58.41/58.53 | achievable(west(m(X),c(Y)),boatoneast,east(m(s(Z)),c(W))) ) ). % 58.41/58.53 % 58.41/58.53 cnf(missionary_east_to_west,axiom, % 58.41/58.53 ( ~ achievable(west(m(X),c(Y)),boatoneast,east(m(s(Z)),c(W))) % 58.41/58.53 | ~ safe(s(X),Y) % 58.41/58.53 | ~ safe(Z,W) % 58.41/58.53 | achievable(west(m(s(X)),c(Y)),boatonwest,east(m(Z),c(W))) ) ). % 58.41/58.53 % 58.41/58.53 cnf(two_missionaries_west_to_east,axiom, % 58.41/58.53 ( ~ achievable(west(m(s(s(X))),c(Y)),boatonwest,east(m(Z),c(W))) % 58.41/58.53 | ~ safe(X,Y) % 58.41/58.53 | ~ safe(s(s(Z)),W) % 58.41/58.53 | achievable(west(m(X),c(Y)),boatoneast,east(m(s(s(Z))),c(W))) ) ). % 58.41/58.53 % 58.41/58.53 cnf(two_missionaries_east_to_west,axiom, % 58.41/58.53 ( ~ achievable(west(m(X),c(Y)),boatoneast,east(m(s(s(Z))),c(W))) % 58.41/58.53 | ~ safe(s(s(X)),Y) % 58.41/58.53 | ~ safe(Z,W) % 58.41/58.53 | achievable(west(m(s(s(X))),c(Y)),boatonwest,east(m(Z),c(W))) ) ). % 58.41/58.53 % 58.41/58.53 %----Moving a missionary and a cannibal % 58.41/58.53 cnf(missionary_and_cannibal_west_to_east,axiom, % 58.41/58.53 ( ~ achievable(west(m(s(X)),c(s(Y))),boatonwest,east(m(Z),c(W))) % 58.41/58.53 | ~ safe(X,Y) % 58.41/58.53 | ~ safe(s(Z),s(W)) % 58.41/58.53 | achievable(west(m(X),c(Y)),boatoneast,east(m(s(Z)),c(s(W)))) ) ). % 58.41/58.53 % 58.41/58.53 cnf(missionary_and_cannibal_east_to_west,axiom, % 58.41/58.53 ( ~ achievable(west(m(X),c(Y)),boatoneast,east(m(s(Z)),c(s(W)))) % 58.41/58.53 | ~ safe(s(X),s(Y)) % 58.41/58.53 | ~ safe(Z,W) % 58.41/58.53 | achievable(west(m(s(X)),c(s(Y))),boatonwest,east(m(Z),c(W))) ) ). % 58.41/58.53 % 58.41/58.53 %----The passive clauses are removed % 58.41/58.53 %----input_clause(extra_cannibal_meal_on_west_bank,axiom, % 58.41/58.53 %---- [++achievable(west(m(s(X)),c(s(s(X)))),Y,east(Z,W))]). % 58.41/58.53 %---- % 58.41/58.53 %----input_clause(two_extra_cannibals_meal_on_west_bank,axiom, % 58.41/58.53 %---- [++achievable(west(m(s(X)),c(s(s(s(X))))),Y,east(Z,W))]). % 58.41/58.53 %---- % 58.41/58.53 %----input_clause(extra_cannibal_meal_on_east_bank,axiom, % 58.41/58.53 %---- [++achievable(west(X,Y),Z,east(m(s(W)),c(s(s(W)))))]). % 58.41/58.53 %---- % 58.41/58.53 %----input_clause(two_extra_cannibals_meal_on_east_bank,axiom, % 58.41/58.53 %---- [++achievable(west(X,Y),Z,east(m(s(W)),c(s(s(s(W))))))]). % 58.41/58.53 % 58.41/58.53 %----Initial state % 58.41/58.53 cnf(start_on_west_bank,hypothesis, % 58.41/58.53 achievable(west(m(s(s(s(n0)))),c(s(s(s(n0))))),boatonwest,east(m(n0),c(n0))) ). % 58.41/58.53 % 58.41/58.53 %----Final state % 58.41/58.53 cnf(prove_can_get_to_east_bank,negated_conjecture, % 58.41/58.53 ~ achievable(west(m(n0),c(n0)),X,east(m(s(s(s(n0)))),c(s(s(s(n0)))))) ). % 58.41/58.53 % 58.41/58.53 %-------------------------------------------------------------------------- % 58.41/58.53 %------------------------------------------- % 58.41/58.53 % Proof found % 58.41/58.53 % SZS status Theorem for theBenchmark % 58.41/58.53 % SZS output start Proof % 58.41/58.54 %ClaNum:16(EqnAxiom:0) % 58.41/58.54 %VarNum:131(SingletonVarNum:47) % 58.41/58.54 %MaxLitNum:4 % 58.41/58.54 %MaxfuncDepth:5 % 58.41/58.54 %SharedTerms:15 % 58.41/58.54 %goalClause: 4 % 58.41/58.54 %singleGoalClaCount:1 % 58.41/58.54 [3]P2(f8(f2(f7(f7(f7(a1)))),f3(f7(f7(f7(a1))))),a4,f6(f2(a1),f3(a1))) % 58.41/58.54 [1]P1(x11,a1) % 58.41/58.54 [2]P3(a1,x21) % 58.41/58.54 [4]~P2(f8(f2(a1),f3(a1)),x41,f6(f2(f7(f7(f7(a1)))),f3(f7(f7(f7(a1)))))) % 58.41/58.54 [5]~P1(x51,x52)+P3(x51,x52) % 58.41/58.54 [6]~P1(x61,x62)+P1(f7(x61),f7(x62)) % 58.41/58.54 [8]~P3(x81,x82)+~P3(f7(x83),x84)+P2(f8(f2(x81),f3(x82)),a5,f6(f2(f7(x83)),f3(x84)))+~P2(f8(f2(f7(x81)),f3(x82)),a4,f6(f2(x83),f3(x84))) % 58.41/58.54 [10]~P3(x103,x104)+~P3(f7(x101),x102)+P2(f8(f2(f7(x101)),f3(x102)),a4,f6(f2(x103),f3(x104)))+~P2(f8(f2(x101),f3(x102)),a5,f6(f2(f7(x103)),f3(x104))) % 58.41/58.54 [14]~P3(x141,x142)+P2(f8(f2(x141),f3(x142)),a5,f6(f2(f7(f7(x143))),f3(x144)))+~P2(f8(f2(f7(f7(x141))),f3(x142)),a4,f6(f2(x143),f3(x144)))+~P3(f7(f7(x143)),x144) % 58.41/58.54 [16]~P3(x163,x164)+~P3(f7(f7(x161)),x162)+P2(f8(f2(f7(f7(x161))),f3(x162)),a4,f6(f2(x163),f3(x164)))+~P2(f8(f2(x161),f3(x162)),a5,f6(f2(f7(f7(x163))),f3(x164))) % 58.41/58.54 [7]~P3(x71,x72)+~P3(x73,f7(x74))+~P2(f8(f2(x71),f3(f7(x72))),a4,f6(f2(x73),f3(x74)))+P2(f8(f2(x71),f3(x72)),a5,f6(f2(x73),f3(f7(x74)))) % 58.41/58.54 [9]~P3(x93,x94)+~P3(x91,f7(x92))+~P2(f8(f2(x91),f3(x92)),a5,f6(f2(x93),f3(f7(x94))))+P2(f8(f2(x91),f3(f7(x92))),a4,f6(f2(x93),f3(x94))) % 58.41/58.54 [11]~P3(x111,x112)+~P3(f7(x113),f7(x114))+~P2(f8(f2(f7(x111)),f3(f7(x112))),a4,f6(f2(x113),f3(x114)))+P2(f8(f2(x111),f3(x112)),a5,f6(f2(f7(x113)),f3(f7(x114)))) % 58.41/58.54 [12]~P3(x123,x124)+~P3(f7(x121),f7(x122))+~P2(f8(f2(x121),f3(x122)),a5,f6(f2(f7(x123)),f3(f7(x124))))+P2(f8(f2(f7(x121)),f3(f7(x122))),a4,f6(f2(x123),f3(x124))) % 58.41/58.54 [13]~P3(x131,x132)+~P3(x133,f7(f7(x134)))+~P2(f8(f2(x131),f3(f7(f7(x132)))),a4,f6(f2(x133),f3(x134)))+P2(f8(f2(x131),f3(x132)),a5,f6(f2(x133),f3(f7(f7(x134))))) % 58.41/58.54 [15]~P3(x153,x154)+~P3(x151,f7(f7(x152)))+~P2(f8(f2(x151),f3(x152)),a5,f6(f2(x153),f3(f7(f7(x154)))))+P2(f8(f2(x151),f3(f7(f7(x152)))),a4,f6(f2(x153),f3(x154))) % 58.41/58.54 %EqnAxiom % 58.41/58.54 % 58.41/58.54 %------------------------------------------- % 58.50/58.58 cnf(18,plain, % 58.50/58.58 (P3(a1,x181)), % 58.50/58.58 inference(rename_variables,[],[2])). % 58.50/58.58 cnf(20,plain, % 58.50/58.58 (~P3(f7(f7(f7(a1))),f7(a1))+P2(f8(f2(f7(f7(f7(a1)))),f3(f7(a1))),a5,f6(f2(a1),f3(f7(f7(a1)))))), % 58.50/58.58 inference(scs_inference,[],[2,18,3,7,8,11,13])). % 58.50/58.58 cnf(58,plain, % 58.50/58.59 (P3(f7(x581),f7(a1))), % 58.50/58.59 inference(scs_inference,[],[1,6,5])). % 58.50/58.59 cnf(59,plain, % 58.50/58.59 (P2(f8(f2(f7(f7(f7(a1)))),f3(f7(a1))),a5,f6(f2(a1),f3(f7(f7(a1)))))), % 58.50/58.59 inference(scs_inference,[],[58,20])). % 58.50/58.59 cnf(62,plain, % 58.50/58.59 (~P3(f7(f7(f7(a1))),f7(f7(a1)))+P2(f8(f2(f7(f7(f7(a1)))),f3(f7(f7(a1)))),a4,f6(f2(a1),f3(f7(a1))))), % 58.50/58.59 inference(scs_inference,[],[59,2,9])). % 58.50/58.59 cnf(349,plain, % 58.50/58.59 (~P1(f7(f7(f7(a1))),f7(f7(a1)))+P2(f8(f2(f7(f7(f7(a1)))),f3(f7(f7(a1)))),a4,f6(f2(a1),f3(f7(a1))))), % 58.50/58.59 inference(scs_inference,[],[5,62])). % 58.50/58.59 cnf(365,plain, % 58.50/58.59 (~P3(f7(f7(f7(a1))),a1)+~P1(f7(f7(f7(a1))),f7(f7(a1)))+P2(f8(f2(f7(f7(f7(a1)))),f3(a1)),a5,f6(f2(a1),f3(f7(f7(f7(a1))))))), % 58.50/58.59 inference(scs_inference,[],[2,349,13])). % 58.50/58.59 cnf(381,plain, % 58.50/58.59 (~P1(f7(f7(a1)),f7(a1))+P2(f8(f2(f7(f7(f7(a1)))),f3(a1)),a5,f6(f2(a1),f3(f7(f7(f7(a1))))))+~P3(f7(f7(f7(a1))),a1)), % 58.50/58.59 inference(scs_inference,[],[365,6])). % 58.50/58.59 cnf(397,plain, % 58.50/58.59 (~P1(f7(f7(a1)),f7(a1))+~P3(f7(f7(f7(a1))),a1)+P2(f8(f2(f7(f7(f7(a1)))),f3(f7(a1))),a4,f6(f2(a1),f3(f7(f7(a1)))))), % 58.50/58.59 inference(scs_inference,[],[58,2,381,9])). % 58.50/58.59 cnf(413,plain, % 58.50/58.59 (P2(f8(f2(f7(f7(f7(a1)))),f3(f7(a1))),a4,f6(f2(a1),f3(f7(f7(a1)))))+~P3(f7(f7(f7(a1))),a1)), % 58.50/58.59 inference(scs_inference,[],[1,397,6])). % 58.50/58.59 cnf(429,plain, % 58.50/58.59 (~P3(f7(f7(f7(a1))),a1)+P2(f8(f2(f7(f7(f7(a1)))),f3(a1)),a5,f6(f2(a1),f3(f7(f7(f7(a1))))))), % 58.50/58.59 inference(scs_inference,[],[2,413,7])). % 58.50/58.59 cnf(445,plain, % 58.50/58.59 (P2(f8(f2(f7(f7(f7(a1)))),f3(a1)),a5,f6(f2(a1),f3(f7(f7(f7(a1))))))), % 58.50/58.59 inference(scs_inference,[],[1,429,5])). % 58.50/58.59 cnf(446,plain, % 58.50/58.59 (P2(f8(f2(f7(f7(f7(a1)))),f3(f7(a1))),a4,f6(f2(a1),f3(f7(f7(a1)))))), % 58.50/58.59 inference(scs_inference,[],[445,2,58,9])). % 58.50/58.59 cnf(684,plain, % 58.50/58.59 (~P3(f7(f7(f7(a1))),f7(f7(f7(a1))))+~P2(f8(f2(a1),f3(f7(f7(a1)))),a4,f6(f2(f7(f7(f7(a1)))),f3(f7(a1))))), % 58.50/58.59 inference(scs_inference,[],[1,4,5,13])). % 58.50/58.59 cnf(700,plain, % 58.50/58.59 (~P1(f7(f7(f7(a1))),f7(f7(f7(a1))))+~P2(f8(f2(a1),f3(f7(f7(a1)))),a4,f6(f2(f7(f7(f7(a1)))),f3(f7(a1))))), % 58.50/58.59 inference(scs_inference,[],[684,5])). % 58.50/58.59 cnf(716,plain, % 58.50/58.59 (~P1(f7(f7(a1)),f7(f7(a1)))+~P2(f8(f2(a1),f3(f7(f7(a1)))),a4,f6(f2(f7(f7(f7(a1)))),f3(f7(a1))))), % 58.50/58.59 inference(scs_inference,[],[700,6])). % 58.50/58.59 cnf(732,plain, % 58.50/58.59 (~P1(f7(f7(a1)),f7(f7(a1)))+~P2(f8(f2(a1),f3(f7(a1))),a5,f6(f2(f7(f7(f7(a1)))),f3(f7(f7(a1)))))), % 58.50/58.59 inference(scs_inference,[],[2,58,716,9])). % 58.50/58.59 cnf(748,plain, % 58.50/58.59 (~P1(f7(a1),f7(a1))+~P2(f8(f2(a1),f3(f7(a1))),a5,f6(f2(f7(f7(f7(a1)))),f3(f7(f7(a1)))))), % 58.50/58.59 inference(scs_inference,[],[732,6])). % 58.50/58.59 cnf(1564,plain, % 58.50/58.59 (~P3(f7(f7(f7(a1))),f7(f7(f7(a1))))+~P2(f8(f2(f7(a1)),f3(a1)),a4,f6(f2(f7(f7(a1))),f3(f7(f7(f7(a1))))))), % 58.50/58.59 inference(scs_inference,[],[1,4,5,8])). % 58.50/58.59 cnf(1717,plain, % 58.50/58.59 (~P1(f7(f7(f7(a1))),f7(f7(f7(a1))))+~P2(f8(f2(f7(a1)),f3(a1)),a4,f6(f2(f7(f7(a1))),f3(f7(f7(f7(a1))))))), % 58.50/58.59 inference(scs_inference,[],[1564,5])). % 58.50/58.59 cnf(1873,plain, % 58.50/58.59 (~P1(f7(f7(a1)),f7(f7(a1)))+~P2(f8(f2(f7(a1)),f3(a1)),a4,f6(f2(f7(f7(a1))),f3(f7(f7(f7(a1))))))), % 58.50/58.59 inference(scs_inference,[],[1717,6])). % 58.50/58.59 cnf(5602,plain, % 58.50/58.59 (~P1(f7(a1),f7(a1))+P2(f8(f2(f7(a1)),f3(f7(a1))),a5,f6(f2(f7(f7(a1))),f3(f7(f7(a1)))))), % 58.50/58.59 inference(scs_inference,[],[58,446,14,5,6])). % 58.50/58.59 cnf(5960,plain, % 58.50/58.59 (P3(x59601,a1)), % 58.50/58.59 inference(scs_inference,[],[1,5])). % 58.50/58.59 cnf(51197,plain, % 58.50/58.59 (P1(f7(x511971),f7(a1))), % 58.50/58.59 inference(scs_inference,[],[1,6])). % 58.50/58.59 cnf(51199,plain, % 58.50/58.59 (~P2(f8(f2(a1),f3(f7(a1))),a5,f6(f2(f7(f7(f7(a1)))),f3(f7(f7(a1)))))), % 58.50/58.59 inference(scs_inference,[],[1,6,748])). % 58.50/58.59 cnf(51200,plain, % 58.50/58.59 (P2(f8(f2(f7(a1)),f3(f7(a1))),a5,f6(f2(f7(f7(a1))),f3(f7(f7(a1)))))), % 58.50/58.59 inference(scs_inference,[],[1,6,748,5602])). % 58.50/58.59 cnf(51222,plain, % 58.50/58.59 (P1(f7(f7(x512221)),f7(f7(a1)))), % 58.50/58.59 inference(scs_inference,[],[51197,6])). % 58.50/58.59 cnf(51226,plain, % 58.50/58.59 (P3(f7(f7(a1)),f7(f7(a1)))), % 58.50/58.59 inference(scs_inference,[],[51197,6,716,1873,5])). % 58.50/58.59 cnf(51246,plain, % 58.50/58.59 (P3(f7(f7(x512461)),f7(f7(a1)))), % 58.50/58.59 inference(scs_inference,[],[51222,5])). % 58.50/58.59 cnf(51248,plain, % 58.50/58.59 (P1(f7(f7(f7(x512481))),f7(f7(f7(a1))))), % 58.50/58.59 inference(scs_inference,[],[51222,5,6])). % 58.50/58.59 cnf(51252,plain, % 58.50/58.59 (~P2(f8(f2(a1),f3(f7(f7(f7(a1))))),a4,f6(f2(f7(f7(f7(a1)))),f3(a1)))), % 58.50/58.59 inference(scs_inference,[],[51222,51226,51199,5960,2,5,6,10,13])). % 58.50/58.59 cnf(51269,plain, % 58.50/58.59 (P1(f7(f7(f7(f7(x512691)))),f7(f7(f7(f7(a1)))))), % 58.50/58.59 inference(scs_inference,[],[51248,5,6])). % 58.50/58.59 cnf(51271,plain, % 58.50/58.59 (~P2(f8(f2(a1),f3(f7(f7(a1)))),a5,f6(f2(f7(f7(f7(a1)))),f3(f7(a1))))), % 58.50/58.59 inference(scs_inference,[],[51248,51252,5960,2,5,6,9])). % 58.50/58.59 cnf(51272,plain, % 58.50/58.59 (P3(x512721,a1)), % 58.50/58.59 inference(rename_variables,[],[5960])). % 58.50/58.59 cnf(51273,plain, % 58.50/58.59 (P3(a1,x512731)), % 58.50/58.59 inference(rename_variables,[],[2])). % 58.50/58.59 cnf(51280,plain, % 58.50/58.59 (P3(a1,x512801)), % 58.50/58.59 inference(rename_variables,[],[2])). % 58.50/58.59 cnf(51281,plain, % 58.50/58.59 (P3(f7(f7(x512811)),f7(f7(a1)))), % 58.50/58.59 inference(rename_variables,[],[51246])). % 58.50/58.59 cnf(51285,plain, % 58.50/58.59 (~P2(f8(f2(f7(a1)),f3(f7(f7(f7(a1))))),a4,f6(f2(f7(f7(a1))),f3(a1)))), % 58.50/58.59 inference(scs_inference,[],[4,51246,51281,51248,51252,51199,5960,51272,2,51273,51280,58,5,6,9,7,14,10,11])). % 58.50/58.59 cnf(51306,plain, % 58.50/58.59 (P3(f7(x513061),f7(a1))), % 58.50/58.59 inference(rename_variables,[],[58])). % 58.50/58.59 cnf(51309,plain, % 58.50/58.59 ($false), % 58.50/58.59 inference(scs_inference,[],[51269,51200,51285,51271,51246,5960,2,58,51306,5,6,15,14,12]), % 58.50/58.59 ['proof']). % 58.50/58.66 % SZS output end Proof % 58.50/58.66 % Total time :58.020000s %------------------------------------------------------------------------------