%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : COL064-4 : TPTP v8.2.0. Bugfixed v1.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n026.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 04:45:01 EDT 2024 % Result : Unsatisfiable 64.41s 64.53s % Output : CNFRefutation 64.45s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : COL064-4 : TPTP v8.2.0. Bugfixed v1.2.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.33 % Computer : n026.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Tue Jun 18 16:11:54 EDT 2024 % 0.13/0.34 % CPUTime : % 0.60/0.64 start to proof:theBenchmark % 64.41/64.52 %------------------------------------------- % 64.41/64.52 % File :CSE---1.7 % 64.41/64.52 % Problem :theBenchmark % 64.41/64.52 % Transform :cnf % 64.41/64.52 % Format :tptp:raw % 64.41/64.52 % Command :java -jar mcs_scs.jar %d %s % 64.41/64.52 % 64.41/64.52 % Result :Theorem 63.760000s % 64.41/64.52 % Output :CNFRefutation 63.760000s % 64.41/64.52 %------------------------------------------- % 64.41/64.53 %-------------------------------------------------------------------------- % 64.41/64.53 % File : COL064-4 : TPTP v8.2.0. Bugfixed v1.2.0. % 64.41/64.53 % Domain : Combinatory Logic % 64.41/64.53 % Problem : Find combinator equivalent to V from B and T % 64.41/64.53 % Version : [WM88] (equality) axioms. % 64.41/64.53 % Theorem formulation : The combinator is provided and checked. % 64.41/64.53 % English : Construct from B and T alone a combinator that behaves as the % 64.41/64.53 % combinator V does, where ((Bx)y)z = x(yz), (Tx)y = yx, % 64.41/64.53 % ((Vx)y)z = (zx)y. % 64.41/64.53 % 64.41/64.53 % Refs : [WM88] Wos & McCune (1988), Challenge Problems Focusing on Eq % 64.41/64.53 % : [WW+90] Wos et al. (1990), Automated Reasoning Contributes to % 64.41/64.53 % Source : [TPTP] % 64.41/64.53 % Names : % 64.41/64.53 % 64.41/64.53 % Status : Unsatisfiable % 64.41/64.53 % Rating : 0.05 v8.2.0, 0.08 v8.1.0, 0.15 v7.5.0, 0.12 v7.4.0, 0.17 v7.3.0, 0.11 v7.1.0, 0.00 v7.0.0, 0.11 v6.4.0, 0.16 v6.3.0, 0.12 v6.2.0, 0.14 v6.1.0, 0.12 v6.0.0, 0.24 v5.5.0, 0.26 v5.4.0, 0.07 v5.3.0, 0.08 v5.2.0, 0.14 v5.1.0, 0.13 v5.0.0, 0.14 v4.1.0, 0.09 v4.0.1, 0.07 v4.0.0, 0.08 v3.7.0, 0.11 v3.4.0, 0.12 v3.3.0, 0.07 v3.1.0, 0.11 v2.7.0, 0.00 v2.2.1, 0.22 v2.2.0, 0.29 v2.1.0, 0.57 v2.0.0 % 64.41/64.53 % Syntax : Number of clauses : 3 ( 3 unt; 0 nHn; 1 RR) % 64.41/64.53 % Number of literals : 3 ( 3 equ; 1 neg) % 64.41/64.53 % Maximal clause size : 1 ( 1 avg) % 64.41/64.53 % Maximal term depth : 9 ( 2 avg) % 64.41/64.53 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty) % 64.41/64.53 % Number of functors : 6 ( 6 usr; 5 con; 0-2 aty) % 64.41/64.53 % Number of variables : 5 ( 0 sgn) % 64.41/64.53 % SPC : CNF_UNS_RFO_PEQ_UEQ % 64.41/64.53 % 64.41/64.53 % Comments : % 64.41/64.53 % Bugfixes : v1.2.0 : Redundant [fgh]_substitution axioms removed. % 64.41/64.53 %-------------------------------------------------------------------------- % 64.41/64.53 cnf(b_definition,axiom, % 64.41/64.53 apply(apply(apply(b,X),Y),Z) = apply(X,apply(Y,Z)) ). % 64.41/64.53 % 64.41/64.53 cnf(t_definition,axiom, % 64.41/64.53 apply(apply(t,X),Y) = apply(Y,X) ). % 64.41/64.53 % 64.41/64.53 %----This is the V equivalent % 64.41/64.53 cnf(prove_v_combinator,negated_conjecture, % 64.41/64.53 apply(apply(apply(apply(apply(b,apply(t,apply(apply(b,b),t))),apply(apply(b,apply(apply(b,b),b)),t)),x),y),z) != apply(apply(z,x),y) ). % 64.41/64.53 % 64.41/64.53 %-------------------------------------------------------------------------- % 64.41/64.53 %------------------------------------------- % 64.41/64.53 % Proof found % 64.41/64.53 % SZS status Theorem for theBenchmark % 64.41/64.53 % SZS output start Proof % 64.41/64.54 %ClaNum:8(EqnAxiom:5) % 64.41/64.54 %VarNum:10(SingletonVarNum:5) % 64.41/64.54 %MaxLitNum:1 % 64.41/64.54 %MaxfuncDepth:8 % 64.41/64.54 %SharedTerms:19 % 64.41/64.54 %goalClause: 8 % 64.41/64.54 %singleGoalClaCount:1 % 64.41/64.54 [8]~E(f2(f2(f2(f2(f2(a3,f2(a1,f2(f2(a3,a3),a1))),f2(f2(a3,f2(f2(a3,a3),a3)),a1)),a4),a5),a6),f2(f2(a6,a4),a5)) % 64.41/64.54 [6]E(f2(f2(a1,x61),x62),f2(x62,x61)) % 64.41/64.54 [7]E(f2(f2(f2(a3,x71),x72),x73),f2(x71,f2(x72,x73))) % 64.41/64.54 %EqnAxiom % 64.41/64.54 [1]E(x11,x11) % 64.41/64.54 [2]E(x22,x21)+~E(x21,x22) % 64.41/64.54 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 64.41/64.54 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43)) % 64.41/64.54 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52)) % 64.41/64.54 % 64.41/64.54 %------------------------------------------- % 64.45/64.56 cnf(9,plain, % 64.45/64.56 (E(f2(x91,x92),f2(f2(a1,x92),x91))), % 64.45/64.56 inference(scs_inference,[],[6,2])). % 64.45/64.56 cnf(10,plain, % 64.45/64.56 (~E(f2(f2(f2(f2(f2(a3,f2(a1,f2(f2(a3,a3),a1))),f2(f2(a3,f2(f2(a3,a3),a3)),a1)),a4),a5),a6),f2(f2(a1,a5),f2(a6,a4)))), % 64.45/64.56 inference(scs_inference,[],[8,6,2,3])). % 64.45/64.56 cnf(12,plain, % 64.45/64.56 (E(f2(x121,f2(x122,x123)),f2(f2(f2(a3,x121),x122),x123))), % 64.45/64.56 inference(scs_inference,[],[7,2])). % 64.45/64.56 cnf(13,plain, % 64.45/64.56 (E(f2(f2(x131,x132),x133),f2(f2(f2(a3,f2(a1,x133)),x131),x132))), % 64.45/64.56 inference(scs_inference,[],[9,7,2,3])). % 64.45/64.56 cnf(15,plain, % 64.45/64.56 (E(f2(f2(f2(a3,f2(a1,x151)),x152),x153),f2(f2(x152,x153),x151))), % 64.45/64.56 inference(scs_inference,[],[13,2])). % 64.45/64.56 cnf(16,plain, % 64.45/64.56 (E(f2(x161,f2(x162,x163)),f2(f2(f2(a3,f2(a1,x163)),f2(a3,x161)),x162))), % 64.45/64.56 inference(scs_inference,[],[12,13,2,3])). % 64.45/64.56 cnf(18,plain, % 64.45/64.56 (E(f2(f2(f2(a3,f2(a1,x181)),f2(a3,x182)),x183),f2(x182,f2(x183,x181)))), % 64.45/64.56 inference(scs_inference,[],[16,2])). % 64.45/64.56 cnf(19,plain, % 64.45/64.56 (E(f2(f2(f2(a3,f2(a1,f2(x191,x192))),x193),x194),f2(f2(f2(a3,f2(x193,x194)),x191),x192))), % 64.45/64.56 inference(scs_inference,[],[15,12,16,2,3])). % 64.45/64.56 cnf(22,plain, % 64.45/64.56 (E(f2(f2(f2(a3,f2(x221,x222)),x223),x224),f2(f2(f2(a3,f2(a1,f2(x223,x224))),x221),x222))), % 64.45/64.56 inference(scs_inference,[],[19,2])). % 64.45/64.56 cnf(23,plain, % 64.45/64.56 (E(f2(f2(f2(a3,f2(a1,x231)),f2(a3,f2(f2(a3,f2(a1,f2(x232,x233))),x234))),x235),f2(f2(f2(a3,f2(x234,f2(x235,x231))),x232),x233))), % 64.45/64.56 inference(scs_inference,[],[18,19,2,3])). % 64.45/64.56 cnf(26,plain, % 64.45/64.56 (E(f2(f2(f2(a3,f2(a1,x261)),f2(a3,f2(x262,x263))),x264),f2(f2(f2(a3,f2(a1,f2(x264,x261))),x262),x263))), % 64.45/64.56 inference(scs_inference,[],[22,15,3])). % 64.45/64.56 cnf(29,plain, % 64.45/64.56 (E(f2(f2(f2(a3,f2(a1,f2(x291,x292))),x293),x294),f2(f2(f2(a3,f2(a1,x292)),f2(a3,f2(x293,x294))),x291))), % 64.45/64.56 inference(scs_inference,[],[22,15,3,2])). % 64.45/64.56 cnf(35,plain, % 64.45/64.56 (E(f2(f2(f2(a3,f2(a1,f2(f2(a3,f2(x351,x352)),x353))),a1),x354),f2(f2(f2(a3,f2(a1,f2(x353,x354))),x351),x352))), % 64.45/64.56 inference(scs_inference,[],[22,29,3,2])). % 64.45/64.56 cnf(39,plain, % 64.45/64.56 (E(f2(f2(f2(a3,f2(a1,f2(x391,x392))),x393),x394),f2(f2(a1,f2(f2(a3,f2(x393,x394)),x391)),f2(a1,x392)))), % 64.45/64.56 inference(scs_inference,[],[35,12,3,2])). % 64.45/64.56 cnf(48,plain, % 64.45/64.56 (E(f2(f2(a1,f2(f2(a3,f2(x481,x482)),x483)),f2(a1,x484)),f2(f2(f2(a3,f2(x481,x482)),x483),x484))), % 64.45/64.56 inference(scs_inference,[],[39,22,3,2])). % 64.45/64.56 cnf(52,plain, % 64.45/64.56 (E(f2(f2(f2(a3,f2(a1,x521)),f2(a3,f2(x522,x523))),x524),f2(f2(a1,f2(f2(a3,f2(a1,f2(x524,x521))),x522)),f2(a1,x523)))), % 64.45/64.56 inference(scs_inference,[],[48,29,3,2])). % 64.45/64.56 cnf(56,plain, % 64.45/64.56 (E(f2(f2(a1,f2(f2(a3,f2(a1,f2(x561,x562))),x563)),f2(a1,x564)),f2(f2(a1,f2(f2(a3,f2(a1,x562)),f2(a3,f2(x563,x564)))),f2(a1,x561)))), % 64.45/64.56 inference(scs_inference,[],[52,48,3,2])). % 64.45/64.56 cnf(59,plain, % 64.45/64.56 (E(f2(f2(a1,f2(f2(a3,f2(a1,x591)),f2(a3,f2(x592,x593)))),f2(a1,x594)),f2(f2(a1,x593),f2(f2(a3,f2(a1,f2(x594,x591))),x592)))), % 64.45/64.56 inference(scs_inference,[],[56,9,3,2])). % 64.45/64.56 cnf(63,plain, % 64.45/64.56 (E(f2(f2(a1,x631),f2(f2(a3,f2(a1,f2(x632,f2(x633,x634)))),x635)),f2(f2(f2(a3,f2(a1,x634)),f2(a3,f2(f2(a3,f2(x635,x631)),x632))),x633))), % 64.45/64.56 inference(scs_inference,[],[59,52,3,2])). % 64.45/64.56 cnf(67,plain, % 64.45/64.56 (E(f2(f2(a1,f2(x671,x672)),f2(f2(a3,f2(a1,f2(x673,f2(x674,x675)))),a1)),f2(f2(f2(a3,f2(x673,f2(x674,x675))),x671),x672))), % 64.45/64.56 inference(scs_inference,[],[63,23,3])). % 64.45/64.56 cnf(70,plain, % 64.45/64.56 (E(f2(f2(f2(a3,f2(x701,f2(x702,x703))),x704),x705),f2(f2(a1,f2(x704,x705)),f2(f2(a3,f2(a1,f2(x701,f2(x702,x703)))),a1)))), % 64.45/64.56 inference(scs_inference,[],[67,2])). % 64.45/64.56 cnf(71,plain, % 64.45/64.56 (E(f2(f2(a1,x711),f2(f2(a3,f2(a1,f2(x712,f2(x713,x714)))),x715)),f2(f2(f2(a3,f2(a1,f2(x713,x714))),f2(a3,f2(x715,x711))),x712))), % 64.45/64.56 inference(scs_inference,[],[63,26,67,2,3])). % 64.45/64.56 cnf(73,plain, % 64.45/64.56 (E(f2(f2(f2(a3,f2(a1,f2(x731,x732))),f2(a3,f2(x733,x734))),x735),f2(f2(a1,x734),f2(f2(a3,f2(a1,f2(x735,f2(x731,x732)))),x733)))), % 64.45/64.56 inference(scs_inference,[],[71,2])). % 64.45/64.56 cnf(79,plain, % 64.45/64.56 (E(f2(f2(a1,x791),f2(f2(a3,f2(a1,f2(x792,f2(x793,x794)))),x795)),f2(f2(a1,f2(x793,x794)),f2(f2(a3,f2(x795,x791)),x792)))), % 64.45/64.56 inference(scs_inference,[],[73,12,3,2])). % 64.45/64.56 cnf(84,plain, % 64.45/64.56 (E(f2(f2(f2(a3,f2(x841,f2(x842,x843))),x844),x845),f2(f2(a1,f2(x842,x843)),f2(f2(a3,f2(a1,f2(x844,x845))),x841)))), % 64.45/64.56 inference(scs_inference,[],[79,70,3])). % 64.45/64.56 cnf(582,plain, % 64.45/64.56 (E(f2(f2(f2(a3,x5821),x5822),x5823),f2(f2(a1,f2(x5822,x5823)),x5821))), % 64.45/64.56 inference(scs_inference,[],[6,12,3,2])). % 64.45/64.56 cnf(739,plain, % 64.45/64.56 (E(f2(f2(f2(a3,f2(f2(a3,x7391),x7392)),x7393),x7394),f2(f2(a1,f2(x7392,f2(x7393,x7394))),x7391))), % 64.45/64.56 inference(scs_inference,[],[7,582,3])). % 64.45/64.56 cnf(1209,plain, % 64.45/64.56 (E(f2(x12091,f2(f2(f2(a3,f2(f2(a3,x12092),x12093)),x12094),x12095)),f2(x12091,f2(f2(a1,f2(x12093,f2(x12094,x12095))),x12092)))), % 64.45/64.56 inference(scs_inference,[],[739,4,5])). % 64.45/64.56 cnf(1303,plain, % 64.45/64.56 (E(f2(f2(x13031,f2(f2(f2(a3,f2(f2(a3,x13032),x13033)),x13034),x13035)),x13036),f2(f2(x13031,f2(f2(a1,f2(x13033,f2(x13034,x13035))),x13032)),x13036))), % 64.45/64.56 inference(scs_inference,[],[1209,4])). % 64.45/64.56 cnf(1424,plain, % 64.45/64.56 (E(f2(f2(f2(f2(a3,x14241),x14242),x14243),x14244),f2(f2(x14241,f2(x14242,x14243)),x14244))), % 64.45/64.56 inference(scs_inference,[],[7,4])). % 64.45/64.56 cnf(1429,plain, % 64.45/64.56 (E(f2(f2(f2(f2(f2(a3,x14291),x14292),x14293),x14294),x14295),f2(f2(f2(x14291,f2(x14292,x14293)),x14294),x14295))), % 64.45/64.56 inference(scs_inference,[],[1424,4])). % 64.45/64.56 cnf(1452,plain, % 64.45/64.56 (~E(f2(f2(f2(f2(a1,f2(f2(a3,a3),a1)),f2(f2(f2(a3,f2(f2(a3,a3),a3)),a1),a4)),a5),a6),f2(f2(a1,a5),f2(a6,a4)))), % 64.45/64.56 inference(scs_inference,[],[10,1429,2,3])). % 64.45/64.56 cnf(1454,plain, % 64.45/64.56 (~E(f2(f2(a1,a5),f2(a6,a4)),f2(f2(f2(f2(a1,f2(f2(a3,a3),a1)),f2(f2(f2(a3,f2(f2(a3,a3),a3)),a1),a4)),a5),a6))), % 64.45/64.56 inference(scs_inference,[],[1452,2])). % 64.45/64.56 cnf(1484,plain, % 64.45/64.56 (~E(f2(f2(a3,f2(a1,a4)),f2(a3,f2(a1,a5))),f2(f2(f2(a1,f2(f2(a3,a3),a1)),f2(f2(f2(a3,f2(f2(a3,a3),a3)),a1),a4)),a5))), % 64.45/64.56 inference(scs_inference,[],[1454,16,3,2,4])). % 64.45/64.56 cnf(1485,plain, % 64.45/64.56 (~E(f2(f2(f2(a1,f2(f2(a3,a3),a1)),f2(f2(f2(a3,f2(f2(a3,a3),a3)),a1),a4)),a5),f2(f2(a3,f2(a1,a4)),f2(a3,f2(a1,a5))))), % 64.45/64.56 inference(scs_inference,[],[1484,2])). % 64.45/64.56 cnf(1491,plain, % 64.45/64.56 (~E(f2(f2(f2(a1,f2(f2(a3,a3),a1)),f2(f2(a1,f2(a3,f2(a1,a4))),a3)),a5),f2(f2(a3,f2(a1,a4)),f2(a3,f2(a1,a5))))), % 64.45/64.56 inference(scs_inference,[],[1485,1303,3])). % 64.45/64.56 cnf(1493,plain, % 64.45/64.56 (~E(f2(f2(a3,f2(a1,a4)),f2(a3,f2(a1,a5))),f2(f2(f2(a1,f2(f2(a3,a3),a1)),f2(f2(a1,f2(a3,f2(a1,a4))),a3)),a5))), % 64.45/64.56 inference(scs_inference,[],[1491,2])). % 64.45/64.56 cnf(1494,plain, % 64.45/64.56 (E(f2(f2(x14941,f2(x14942,x14943)),x14944),f2(f2(f2(f2(a3,x14941),x14942),x14943),x14944))), % 64.45/64.56 inference(scs_inference,[],[12,1491,2,4])). % 64.45/64.56 cnf(1497,plain, % 64.45/64.56 (~E(f2(f2(f2(a3,f2(a3,f2(a1,a4))),a3),f2(a1,a5)),f2(f2(f2(a1,f2(f2(a3,a3),a1)),f2(f2(a1,f2(a3,f2(a1,a4))),a3)),a5))), % 64.45/64.56 inference(scs_inference,[],[12,1493,3])). % 64.45/64.56 cnf(1499,plain, % 64.45/64.56 (~E(f2(f2(f2(a1,f2(f2(a3,a3),a1)),f2(f2(a1,f2(a3,f2(a1,a4))),a3)),a5),f2(f2(f2(a3,f2(a3,f2(a1,a4))),a3),f2(a1,a5)))), % 64.45/64.56 inference(scs_inference,[],[12,1493,3,2])). % 64.45/64.56 cnf(1501,plain, % 64.45/64.56 (E(f2(x15011,f2(x15012,x15013)),f2(f2(f2(a3,x15011),x15012),x15013))), % 64.45/64.56 inference(rename_variables,[],[12])). % 64.45/64.56 cnf(1502,plain, % 64.45/64.56 (E(f2(x15021,f2(x15022,f2(x15023,x15024))),f2(x15021,f2(f2(f2(a3,x15022),x15023),x15024)))), % 64.45/64.56 inference(scs_inference,[],[12,1501,1497,3,5])). % 64.45/64.56 cnf(1504,plain, % 64.45/64.56 (~E(f2(f2(a3,f2(f2(a3,f2(a3,f2(a1,a4))),a3)),a1),f2(f2(a1,f2(f2(a3,a3),a1)),f2(f2(a1,f2(a3,f2(a1,a4))),a3)))), % 64.45/64.56 inference(scs_inference,[],[12,1501,1497,3,5,2,4])). % 64.45/64.56 cnf(1505,plain, % 64.45/64.56 (~E(f2(f2(a1,f2(f2(a3,a3),a1)),f2(f2(a1,f2(a3,f2(a1,a4))),a3)),f2(f2(a3,f2(f2(a3,f2(a3,f2(a1,a4))),a3)),a1))), % 64.45/64.56 inference(scs_inference,[],[1504,2])). % 64.45/64.56 cnf(1506,plain, % 64.45/64.56 (E(f2(f2(f2(x15061,f2(x15062,x15063)),x15064),x15065),f2(f2(f2(f2(f2(a3,x15061),x15062),x15063),x15064),x15065))), % 64.45/64.56 inference(scs_inference,[],[1494,1504,2,4])). % 64.45/64.56 cnf(1507,plain, % 64.45/64.56 (~E(f2(f2(f2(f2(a3,f2(a1,f2(f2(a3,a3),a1))),f2(a1,f2(a3,f2(a1,a4)))),a3),a5),f2(f2(f2(a3,f2(a3,f2(a1,a4))),a3),f2(a1,a5)))), % 64.45/64.56 inference(scs_inference,[],[1494,1499,1504,2,4,3])). % 64.45/64.56 cnf(1509,plain, % 64.45/64.56 (~E(f2(f2(f2(a3,f2(a3,f2(a1,a4))),a3),f2(a1,a5)),f2(f2(f2(f2(a3,f2(a1,f2(f2(a3,a3),a1))),f2(a1,f2(a3,f2(a1,a4)))),a3),a5))), % 64.45/64.56 inference(scs_inference,[],[1507,2])). % 64.45/64.56 cnf(1510,plain, % 64.45/64.56 (~E(f2(f2(f2(a3,f2(a1,f2(f2(a3,a3),a1))),f2(a1,f2(a3,f2(a1,a4)))),a3),f2(f2(a3,f2(f2(a3,f2(a3,f2(a1,a4))),a3)),a1))), % 64.45/64.56 inference(scs_inference,[],[12,1507,1505,2,3])). % 64.45/64.56 cnf(1513,plain, % 64.45/64.56 (~E(f2(f2(f2(f2(f2(a3,a3),a1),f2(f2(a3,a3),a1)),f2(a1,f2(a3,f2(a1,a4)))),a3),f2(f2(a3,f2(f2(a3,f2(a3,f2(a1,a4))),a3)),a1))), % 64.45/64.56 inference(scs_inference,[],[1506,1510,2,3])). % 64.45/64.56 cnf(1516,plain, % 64.45/64.56 (E(f2(f2(x15161,f2(x15162,f2(x15163,x15164))),x15165),f2(f2(x15161,f2(f2(f2(a3,x15162),x15163),x15164)),x15165))), % 64.45/64.56 inference(scs_inference,[],[1502,1513,2,4])). % 64.45/64.56 cnf(1517,plain, % 64.45/64.56 (~E(f2(f2(a3,f2(a1,a4)),f2(f2(f2(a3,a3),a1),a5)),f2(f2(f2(a1,f2(f2(a3,a3),a1)),f2(f2(a1,f2(a3,f2(a1,a4))),a3)),a5))), % 64.45/64.56 inference(scs_inference,[],[1502,1513,1493,2,4,3])). % 64.45/64.56 cnf(1520,plain, % 64.45/64.56 (~E(f2(f2(f2(a1,f2(f2(a3,a3),a1)),f2(f2(a1,f2(a3,f2(a1,a4))),a3)),a5),f2(f2(a3,f2(a1,a4)),f2(f2(f2(a3,a3),a1),a5)))), % 64.45/64.56 inference(scs_inference,[],[1517,2])). % 64.45/64.56 cnf(1521,plain, % 64.45/64.56 (~E(f2(f2(f2(a3,f2(a3,f2(a1,a4))),f2(f2(a3,a3),a1)),a5),f2(f2(f2(a1,f2(f2(a3,a3),a1)),f2(f2(a1,f2(a3,f2(a1,a4))),a3)),a5))), % 64.45/64.56 inference(scs_inference,[],[12,1517,2,3])). % 64.45/64.56 cnf(1523,plain, % 64.45/64.56 (~E(f2(f2(a3,f2(a3,f2(a1,a4))),f2(f2(a3,a3),a1)),f2(f2(a1,f2(f2(a3,a3),a1)),f2(f2(a1,f2(a3,f2(a1,a4))),a3)))), % 64.45/64.56 inference(scs_inference,[],[12,1517,2,3,4])). % 64.45/64.56 cnf(1524,plain, % 64.45/64.56 (~E(f2(f2(a1,f2(f2(a3,a3),a1)),f2(f2(a1,f2(a3,f2(a1,a4))),a3)),f2(f2(a3,f2(a3,f2(a1,a4))),f2(f2(a3,a3),a1)))), % 64.45/64.56 inference(scs_inference,[],[1523,2])). % 64.45/64.56 cnf(1525,plain, % 64.45/64.56 (E(f2(f2(f2(x15251,f2(x15252,f2(x15253,x15254))),x15255),x15256),f2(f2(f2(x15251,f2(f2(f2(a3,x15252),x15253),x15254)),x15255),x15256))), % 64.45/64.56 inference(scs_inference,[],[1516,1523,2,4])). % 64.45/64.56 cnf(1526,plain, % 64.45/64.56 (~E(f2(f2(f2(a3,f2(a3,f2(a3,f2(a1,a4)))),f2(a3,a3)),a1),f2(f2(a1,f2(f2(a3,a3),a1)),f2(f2(a1,f2(a3,f2(a1,a4))),a3)))), % 64.45/64.56 inference(scs_inference,[],[12,1516,1523,2,4,3])). % 64.45/64.56 cnf(1528,plain, % 64.45/64.56 (~E(f2(f2(a1,f2(f2(a3,a3),a1)),f2(f2(a1,f2(a3,f2(a1,a4))),a3)),f2(f2(f2(a3,f2(a3,f2(a3,f2(a1,a4)))),f2(a3,a3)),a1))), % 64.45/64.56 inference(scs_inference,[],[1526,2])). % 64.45/64.56 cnf(1529,plain, % 64.45/64.57 (~E(f2(f2(f2(a3,f2(a1,f2(f2(a3,a3),a1))),f2(a1,f2(a3,f2(a1,a4)))),a3),f2(f2(a3,f2(a3,f2(a1,a4))),f2(f2(a3,a3),a1)))), % 64.45/64.57 inference(scs_inference,[],[12,1524,1526,2,3])). % 64.45/64.57 cnf(1531,plain, % 64.45/64.57 (~E(f2(f2(a3,f2(a3,f2(a1,a4))),f2(f2(a3,a3),a1)),f2(f2(f2(a3,f2(a1,f2(f2(a3,a3),a1))),f2(a1,f2(a3,f2(a1,a4)))),a3))), % 64.45/64.57 inference(scs_inference,[],[1529,2])). % 64.45/64.57 cnf(1532,plain, % 64.45/64.57 (~E(f2(f2(f2(a3,f2(a1,f2(f2(a3,a3),a1))),f2(a1,f2(a3,f2(a1,a4)))),a3),f2(f2(f2(a3,f2(a3,f2(a3,f2(a1,a4)))),f2(a3,a3)),a1))), % 64.45/64.57 inference(scs_inference,[],[12,1529,1528,2,3])). % 64.45/64.57 cnf(1535,plain, % 64.45/64.57 (~E(f2(f2(f2(a3,f2(a3,f2(a3,f2(a1,a4)))),f2(a3,a3)),a1),f2(f2(f2(a3,f2(a1,f2(f2(a3,a3),a1))),f2(a1,f2(a3,f2(a1,a4)))),a3))), % 64.45/64.57 inference(scs_inference,[],[1532,2])). % 64.45/64.57 cnf(1536,plain, % 64.45/64.57 (~E(f2(f2(f2(a3,f2(a1,f2(f2(a3,a3),a1))),a3),f2(a3,f2(a1,a4))),f2(f2(f2(a3,f2(a1,f2(f2(a3,a3),a1))),f2(a1,f2(a3,f2(a1,a4)))),a3))), % 64.45/64.57 inference(scs_inference,[],[13,1531,1532,2,3])). % 64.45/64.57 cnf(1539,plain, % 64.45/64.57 (~E(f2(f2(f2(a1,f2(f2(a3,a3),a1)),f2(f2(a1,f2(a3,f2(a1,a4))),a3)),a5),f2(f2(f2(a3,f2(a3,f2(a1,a4))),f2(f2(a3,a3),a1)),a5))), % 64.45/64.57 inference(scs_inference,[],[13,1521,4,2])). % 64.45/64.57 cnf(1540,plain, % 64.45/64.57 (~E(f2(f2(f2(a3,f2(a1,a5)),f2(a1,f2(f2(a3,a3),a1))),f2(f2(a1,f2(a3,f2(a1,a4))),a3)),f2(f2(a3,f2(a1,a4)),f2(f2(f2(a3,a3),a1),a5)))), % 64.45/64.57 inference(scs_inference,[],[13,1520,1521,4,2,3])). % 64.45/64.57 cnf(1543,plain, % 64.45/64.57 (~E(f2(f2(f2(a3,f2(a1,f2(f2(a1,f2(a3,f2(a1,a4))),a3))),f2(a3,f2(a1,a5))),f2(a1,f2(f2(a3,a3),a1))),f2(f2(a3,f2(a1,a4)),f2(f2(f2(a3,a3),a1),a5)))), % 64.45/64.57 inference(scs_inference,[],[13,1540,2,3])). % 64.45/64.57 cnf(1545,plain, % 64.45/64.57 (~E(f2(f2(f2(a3,f2(a1,f2(f2(a3,a3),a1))),f2(a1,f2(a3,f2(a1,a4)))),a3),f2(f2(f2(a3,f2(a1,f2(f2(a3,a3),a1))),a3),f2(a3,f2(a1,a4))))), % 64.45/64.57 inference(scs_inference,[],[1536,2])). % 64.45/64.57 cnf(1550,plain, % 64.45/64.57 (~E(f2(f2(f2(a3,f2(a1,a1)),f2(a3,f2(a3,f2(a3,f2(a1,a4))))),f2(a3,a3)),f2(f2(f2(a3,f2(a1,f2(f2(a3,a3),a1))),f2(a1,f2(a3,f2(a1,a4)))),a3))), % 64.45/64.57 inference(scs_inference,[],[13,1535,1543,2,3])). % 64.45/64.57 cnf(1553,plain, % 64.45/64.57 (~E(f2(f2(f2(a3,f2(a1,a5)),f2(a1,f2(f2(a3,a3),a1))),f2(f2(a1,f2(a3,f2(a1,a4))),a3)),f2(f2(f2(a3,f2(a3,f2(a1,a4))),f2(f2(a3,a3),a1)),a5))), % 64.45/64.57 inference(scs_inference,[],[13,1539,1550,2,3])). % 64.45/64.57 cnf(1556,plain, % 64.45/64.57 (~E(f2(f2(f2(a3,f2(a3,f2(a1,a4))),f2(f2(a3,a3),a1)),a5),f2(f2(f2(a3,f2(a1,a5)),f2(a1,f2(f2(a3,a3),a1))),f2(f2(a1,f2(a3,f2(a1,a4))),a3)))), % 64.45/64.57 inference(scs_inference,[],[1553,2])). % 64.45/64.57 cnf(1557,plain, % 64.45/64.57 (~E(f2(f2(f2(a3,f2(a1,f2(f2(a1,f2(a3,f2(a1,a4))),a3))),f2(a3,f2(a1,a5))),f2(a1,f2(f2(a3,a3),a1))),f2(f2(f2(a3,f2(a3,f2(a1,a4))),f2(f2(a3,a3),a1)),a5))), % 64.45/64.57 inference(scs_inference,[],[13,1553,2,3])). % 64.45/64.57 cnf(1560,plain, % 64.45/64.57 (~E(f2(f2(f2(a3,f2(a1,a5)),f2(a3,f2(a3,f2(a1,a4)))),f2(f2(a3,a3),a1)),f2(f2(f2(a3,f2(a1,a5)),f2(a1,f2(f2(a3,a3),a1))),f2(f2(a1,f2(a3,f2(a1,a4))),a3)))), % 64.45/64.57 inference(scs_inference,[],[13,1556,1557,2,3])). % 64.45/64.57 cnf(1563,plain, % 64.45/64.57 (~E(f2(f2(f2(a3,f2(a1,a5)),f2(a1,f2(f2(a3,a3),a1))),f2(f2(a1,f2(a3,f2(a1,a4))),a3)),f2(f2(f2(a3,f2(a1,a5)),f2(a3,f2(a3,f2(a1,a4)))),f2(f2(a3,a3),a1)))), % 64.45/64.57 inference(scs_inference,[],[1560,2])). % 64.45/64.57 cnf(1564,plain, % 64.45/64.57 (~E(f2(f2(f2(a3,f2(a1,f2(f2(a3,a3),a1))),f2(a3,f2(a1,a5))),f2(a3,f2(a3,f2(a1,a4)))),f2(f2(f2(a3,f2(a1,a5)),f2(a1,f2(f2(a3,a3),a1))),f2(f2(a1,f2(a3,f2(a1,a4))),a3)))), % 64.45/64.57 inference(scs_inference,[],[13,1560,2,3])). % 64.45/64.57 cnf(1567,plain, % 64.45/64.57 (~E(f2(f2(f2(a3,f2(a1,f2(f2(a1,f2(a3,f2(a1,a4))),a3))),f2(a3,f2(a1,a5))),f2(a1,f2(f2(a3,a3),a1))),f2(f2(f2(a3,f2(a1,a5)),f2(a3,f2(a3,f2(a1,a4)))),f2(f2(a3,a3),a1)))), % 64.45/64.57 inference(scs_inference,[],[13,1563,1564,2,3])). % 64.45/64.57 cnf(1578,plain, % 64.45/64.57 (~E(f2(f2(a1,f2(a1,a4)),f2(f2(a3,f2(a1,f2(a3,f2(a1,a5)))),a3)),f2(f2(f2(f2(a3,f2(a1,f2(f2(a3,a3),a1))),f2(a1,f2(a3,f2(a1,a4)))),a3),a5))), % 64.45/64.57 inference(scs_inference,[],[84,1509,1567,2,3])). % 64.45/64.57 cnf(1581,plain, % 64.45/64.57 (~E(f2(f2(f2(a1,f2(a3,f2(a1,a4))),a3),f2(f2(a3,a3),a1)),f2(f2(f2(a3,f2(a1,f2(f2(a3,a3),a1))),a3),f2(a3,f2(a1,a4))))), % 64.45/64.57 inference(scs_inference,[],[15,1545,1578,2,3])). % 64.45/64.57 cnf(1584,plain, % 64.45/64.57 (~E(f2(f2(f2(a3,f2(a1,f2(f2(a3,a3),a1))),a3),f2(a3,f2(a1,a4))),f2(f2(f2(a1,f2(a3,f2(a1,a4))),a3),f2(f2(a3,a3),a1)))), % 64.45/64.57 inference(scs_inference,[],[1581,2])). % 64.45/64.57 cnf(1585,plain, % 64.45/64.57 (~E(f2(f2(f2(a1,f2(f2(f2(a3,a3),a1),a4)),a3),f2(f2(a3,a3),a1)),f2(f2(f2(a3,f2(a1,f2(f2(a3,a3),a1))),a3),f2(a3,f2(a1,a4))))), % 64.45/64.57 inference(scs_inference,[],[1581,1525,2,3])). % 64.45/64.57 cnf(1590,plain, % 64.45/64.57 ($false), % 64.45/64.57 inference(scs_inference,[],[15,1584,1585,9,2,3,4]), % 64.45/64.57 ['proof']). % 64.45/64.57 % SZS output end Proof % 64.45/64.57 % Total time :63.760000s %------------------------------------------------------------------------------