%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : COL062-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 : n022.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:44:59 EDT 2024 % Result : Unsatisfiable 200.28s 200.30s % Output : CNFRefutation 200.36s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.12 % Problem : COL062-1 : TPTP v8.2.0. Released v1.0.0. % 0.08/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n022.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Tue Jun 18 16:16:09 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.57 start to proof:theBenchmark % 200.25/200.26 %------------------------------------------- % 200.25/200.26 % File :CSE---1.7 % 200.25/200.26 % Problem :theBenchmark % 200.25/200.26 % Transform :cnf % 200.25/200.26 % Format :tptp:raw % 200.25/200.26 % Command :java -jar mcs_scs.jar %d %s % 200.25/200.26 % 200.25/200.26 % Result :Theorem 199.630000s % 200.25/200.26 % Output :CNFRefutation 199.630000s % 200.25/200.26 %------------------------------------------- % 200.28/200.30 %-------------------------------------------------------------------------- % 200.28/200.30 % File : COL062-1 : TPTP v8.2.0. Released v1.0.0. % 200.28/200.30 % Domain : Combinatory Logic % 200.28/200.30 % Problem : Find combinator equivalent to C from B and T % 200.28/200.30 % Version : [WM88] (equality) axioms. % 200.28/200.30 % English : Construct from B and T alone a combinator that behaves as the % 200.28/200.30 % combinator C does, where ((Bx)y)z = x(yz), (Tx)y = yx, % 200.28/200.30 % ((Cx)y)z = (xz)y % 200.28/200.30 % 200.28/200.30 % Refs : [WM88] Wos & McCune (1988), Challenge Problems Focusing on Eq % 200.28/200.30 % : [WW+90] Wos et al. (1990), Automated Reasoning Contributes to % 200.28/200.30 % Source : [WW+90] % 200.28/200.30 % Names : CL-3 [WW+90] % 200.28/200.30 % 200.28/200.30 % Status : Unsatisfiable % 200.28/200.30 % Rating : 0.27 v8.2.0, 0.33 v8.1.0, 0.30 v7.5.0, 0.33 v7.4.0, 0.48 v7.3.0, 0.37 v7.1.0, 0.28 v7.0.0, 0.32 v6.4.0, 0.37 v6.3.0, 0.41 v6.2.0, 0.43 v6.1.0, 0.38 v6.0.0, 0.48 v5.5.0, 0.42 v5.4.0, 0.33 v5.3.0, 0.42 v5.2.0, 0.36 v5.1.0, 0.33 v5.0.0, 0.29 v4.1.0, 0.27 v4.0.1, 0.36 v4.0.0, 0.38 v3.7.0, 0.33 v3.4.0, 0.50 v3.1.0, 0.44 v2.7.0, 0.36 v2.6.0, 0.17 v2.5.0, 0.00 v2.2.1, 0.44 v2.2.0, 0.57 v2.1.0, 1.00 v2.0.0 % 200.28/200.30 % Syntax : Number of clauses : 3 ( 3 unt; 0 nHn; 1 RR) % 200.28/200.30 % Number of literals : 3 ( 3 equ; 1 neg) % 200.28/200.30 % Maximal clause size : 1 ( 1 avg) % 200.28/200.30 % Maximal term depth : 5 ( 2 avg) % 200.28/200.30 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty) % 200.28/200.30 % Number of functors : 6 ( 6 usr; 2 con; 0-2 aty) % 200.28/200.30 % Number of variables : 6 ( 0 sgn) % 200.28/200.30 % SPC : CNF_UNS_RFO_PEQ_UEQ % 200.28/200.30 % 200.28/200.30 % Comments : % 200.28/200.30 %-------------------------------------------------------------------------- % 200.28/200.30 cnf(b_definition,axiom, % 200.28/200.30 apply(apply(apply(b,X),Y),Z) = apply(X,apply(Y,Z)) ). % 200.28/200.30 % 200.28/200.30 cnf(t_definition,axiom, % 200.28/200.30 apply(apply(t,X),Y) = apply(Y,X) ). % 200.28/200.30 % 200.28/200.30 cnf(prove_c_combinator,negated_conjecture, % 200.28/200.30 apply(apply(apply(X,f(X)),g(X)),h(X)) != apply(apply(f(X),h(X)),g(X)) ). % 200.28/200.30 % 200.28/200.30 %-------------------------------------------------------------------------- % 200.28/200.30 %------------------------------------------- % 200.28/200.30 % Proof found % 200.28/200.30 % SZS status Theorem for theBenchmark % 200.28/200.30 % SZS output start Proof % 200.28/200.34 %ClaNum:11(EqnAxiom:8) % 200.28/200.34 %VarNum:17(SingletonVarNum:6) % 200.28/200.34 %MaxLitNum:1 % 200.28/200.34 %MaxfuncDepth:3 % 200.28/200.34 %SharedTerms:2 % 200.28/200.34 %goalClause: 11 % 200.28/200.34 %singleGoalClaCount:1 % 200.28/200.34 [11]~E(f2(f2(f2(x111,f4(x111)),f5(x111)),f6(x111)),f2(f2(f4(x111),f6(x111)),f5(x111))) % 200.28/200.34 [9]E(f2(f2(a1,x91),x92),f2(x92,x91)) % 200.28/200.34 [10]E(f2(f2(f2(a3,x101),x102),x103),f2(x101,f2(x102,x103))) % 200.28/200.34 %EqnAxiom % 200.28/200.34 [1]E(x11,x11) % 200.28/200.34 [2]E(x22,x21)+~E(x21,x22) % 200.28/200.34 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 200.28/200.34 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43)) % 200.28/200.34 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52)) % 200.28/200.34 [6]~E(x61,x62)+E(f5(x61),f5(x62)) % 200.28/200.34 [7]~E(x71,x72)+E(f6(x71),f6(x72)) % 200.28/200.34 [8]~E(x81,x82)+E(f4(x81),f4(x82)) % 200.28/200.34 % 200.28/200.34 %------------------------------------------- % 200.36/200.37 cnf(12,plain, % 200.36/200.37 (E(f2(x121,x122),f2(f2(a1,x122),x121))), % 200.36/200.37 inference(scs_inference,[],[9,2])). % 200.36/200.37 cnf(13,plain, % 200.36/200.37 (E(f2(f2(a1,x131),f2(f2(a3,x132),x133)),f2(x132,f2(x133,x131)))), % 200.36/200.37 inference(scs_inference,[],[9,10,2,3])). % 200.36/200.37 cnf(16,plain, % 200.36/200.37 (E(f2(x161,f2(x162,x163)),f2(f2(a1,x163),f2(f2(a3,x161),x162)))), % 200.36/200.37 inference(scs_inference,[],[13,2])). % 200.36/200.37 cnf(17,plain, % 200.36/200.37 (E(f2(f2(a1,x171),f2(f2(a3,x172),x173)),f2(f2(a1,f2(x173,x171)),x172))), % 200.36/200.37 inference(scs_inference,[],[12,13,2,3])). % 200.36/200.37 cnf(19,plain, % 200.36/200.37 (E(f2(f2(a1,f2(x191,x192)),x193),f2(f2(a1,x192),f2(f2(a3,x193),x191)))), % 200.36/200.37 inference(scs_inference,[],[17,2])). % 200.36/200.37 cnf(20,plain, % 200.36/200.37 (E(f2(x201,f2(x202,x203)),f2(f2(a1,f2(f2(a3,x201),x202)),f2(a1,x203)))), % 200.36/200.37 inference(scs_inference,[],[16,12,17,2,3])). % 200.36/200.37 cnf(23,plain, % 200.36/200.37 (E(f2(x231,f2(x232,x233)),f2(f2(f2(a3,x231),x232),x233))), % 200.36/200.37 inference(scs_inference,[],[10,2])). % 200.36/200.38 cnf(31,plain, % 200.36/200.38 (E(f2(f2(f2(a3,x311),x312),x313),f2(f2(a1,f2(x312,x313)),x311))), % 200.36/200.38 inference(scs_inference,[],[9,23,3,2])). % 200.36/200.38 cnf(32,plain, % 200.36/200.38 (E(f2(f2(a1,x321),f2(a1,f2(x322,x323))),f2(f2(a1,x323),f2(f2(a3,x321),x322)))), % 200.36/200.38 inference(scs_inference,[],[9,19,3])). % 200.36/200.38 cnf(35,plain, % 200.36/200.38 (E(f2(f2(a1,x351),f2(f2(a3,x352),x353)),f2(f2(a1,x352),f2(a1,f2(x353,x351))))), % 200.36/200.38 inference(scs_inference,[],[9,19,3,2])). % 200.36/200.38 cnf(43,plain, % 200.36/200.38 (E(f2(x431,f2(x432,x433)),f2(f2(f2(a3,f2(a1,x433)),f2(a3,x431)),x432))), % 200.36/200.38 inference(scs_inference,[],[10,13,3,2])). % 200.36/200.38 cnf(44,plain, % 200.36/200.38 (E(f2(x441,f2(x442,x443)),f2(f2(a1,x442),f2(f2(a3,f2(a1,x443)),f2(a3,x441))))), % 200.36/200.38 inference(scs_inference,[],[12,43,3])). % 200.36/200.38 cnf(46,plain, % 200.36/200.38 (E(f2(f2(a1,x461),f2(f2(a3,f2(a1,x462)),f2(a3,x463))),f2(x463,f2(x461,x462)))), % 200.36/200.38 inference(scs_inference,[],[12,43,3,2])). % 200.36/200.38 cnf(47,plain, % 200.36/200.38 (E(f2(x471,f2(x472,x473)),f2(f2(a1,x471),f2(a1,f2(x472,x473))))), % 200.36/200.38 inference(scs_inference,[],[16,35,3])). % 200.36/200.38 cnf(49,plain, % 200.36/200.38 (E(f2(f2(a1,x491),f2(a1,f2(x492,x493))),f2(x491,f2(x492,x493)))), % 200.36/200.38 inference(scs_inference,[],[16,35,3,2])). % 200.36/200.38 cnf(52,plain, % 200.36/200.38 (E(f2(f2(f2(a3,f2(a1,x521)),f2(a3,f2(a1,x522))),f2(a3,x523)),f2(x523,f2(x521,x522)))), % 200.36/200.38 inference(scs_inference,[],[16,43,3,2])). % 200.36/200.38 cnf(59,plain, % 200.36/200.38 (E(f2(f2(x591,x592),x593),f2(f2(a1,f2(a1,x593)),f2(a1,f2(x591,x592))))), % 200.36/200.38 inference(scs_inference,[],[12,47,3])). % 200.36/200.38 cnf(63,plain, % 200.36/200.38 (E(f2(x631,x632),f2(f2(a1,f2(a1,x631)),f2(a1,f2(a1,x632))))), % 200.36/200.38 inference(scs_inference,[],[12,59,3])). % 200.36/200.38 cnf(65,plain, % 200.36/200.38 (E(f2(f2(a1,f2(a1,x651)),f2(a1,f2(a1,x652))),f2(x651,x652))), % 200.36/200.38 inference(scs_inference,[],[12,59,3,2])). % 200.36/200.38 cnf(69,plain, % 200.36/200.38 (E(f2(x691,x692),f2(f2(a1,x691),f2(a1,x692)))), % 200.36/200.38 inference(scs_inference,[],[63,49,3])). % 200.36/200.38 cnf(71,plain, % 200.36/200.38 (E(f2(f2(a1,x711),f2(a1,x712)),f2(x711,x712))), % 200.36/200.38 inference(scs_inference,[],[63,49,3,2])). % 200.36/200.38 cnf(72,plain, % 200.36/200.38 (E(f2(x721,x722),f2(f2(f2(a3,f2(a1,x721)),a1),x722))), % 200.36/200.38 inference(scs_inference,[],[69,23,3])). % 200.36/200.38 cnf(74,plain, % 200.36/200.38 (E(f2(f2(f2(a3,f2(a1,x741)),a1),x742),f2(x741,x742))), % 200.36/200.38 inference(scs_inference,[],[69,23,3,2])). % 200.36/200.38 cnf(75,plain, % 200.36/200.38 (E(f2(x751,x752),f2(f2(a1,f2(a1,x752)),f2(a1,x751)))), % 200.36/200.38 inference(scs_inference,[],[72,31,3])). % 200.36/200.38 cnf(77,plain, % 200.36/200.38 (E(f2(f2(a1,f2(a1,x771)),f2(a1,x772)),f2(x772,x771))), % 200.36/200.38 inference(scs_inference,[],[72,31,3,2])). % 200.36/200.38 cnf(80,plain, % 200.36/200.38 (E(f2(f2(a1,x801),f2(f2(a3,f2(a1,x802)),a1)),f2(x802,x801))), % 200.36/200.38 inference(scs_inference,[],[63,32,3,2])). % 200.36/200.38 cnf(81,plain, % 200.36/200.38 (~E(f2(f2(f2(x811,f4(x811)),f5(x811)),f6(x811)),f2(f2(a1,f2(f4(x811),f6(x811))),f2(a1,f5(x811))))), % 200.36/200.38 inference(scs_inference,[],[71,11,3])). % 200.36/200.38 cnf(83,plain, % 200.36/200.38 (~E(f2(f2(f2(x831,f4(x831)),f5(x831)),f6(x831)),f2(f2(f2(a3,f2(a1,f5(x831))),f4(x831)),f6(x831)))), % 200.36/200.38 inference(scs_inference,[],[31,81,3])). % 200.36/200.38 cnf(85,plain, % 200.36/200.38 (~E(f2(f2(x851,f4(x851)),f5(x851)),f2(f2(a3,f2(a1,f5(x851))),f4(x851)))), % 200.36/200.38 inference(scs_inference,[],[31,81,3,4])). % 200.36/200.38 cnf(86,plain, % 200.36/200.38 (~E(f2(f2(f2(x861,f4(x861)),f5(x861)),f6(x861)),f2(f2(a1,f5(x861)),f2(f4(x861),f6(x861))))), % 200.36/200.38 inference(scs_inference,[],[23,83,3])). % 200.36/200.38 cnf(107,plain, % 200.36/200.38 (E(f2(f2(f2(a3,f2(a1,x1071)),a1),f2(x1072,x1073)),f2(f2(a1,x1072),f2(f2(a3,f2(a1,x1073)),f2(a3,x1071))))), % 200.36/200.38 inference(scs_inference,[],[44,74,3])). % 200.36/200.38 cnf(110,plain, % 200.36/200.38 (E(f2(f2(a1,x1101),f2(f2(a3,f2(a1,x1102)),f2(a3,x1103))),f2(f2(f2(a3,f2(a1,x1103)),a1),f2(x1101,x1102)))), % 200.36/200.38 inference(scs_inference,[],[107,2])). % 200.36/200.38 cnf(116,plain, % 200.36/200.38 (E(f2(f2(a1,f2(a1,f2(x1161,x1162))),f2(a1,x1163)),f2(f2(a1,x1161),f2(f2(a3,f2(a1,x1162)),f2(a3,x1163))))), % 200.36/200.38 inference(scs_inference,[],[46,75,3,2])). % 200.36/200.38 cnf(120,plain, % 200.36/200.38 (E(f2(f2(f2(a3,f2(a1,x1201)),f2(a3,f2(a1,x1202))),f2(a3,x1203)),f2(f2(f2(a3,f2(a1,x1203)),a1),f2(x1201,x1202)))), % 200.36/200.38 inference(scs_inference,[],[52,72,3])). % 200.36/200.38 cnf(122,plain, % 200.36/200.38 (E(f5(f2(f2(a1,f2(a1,x1221)),f2(a1,x1222))),f5(f2(x1222,x1221)))), % 200.36/200.38 inference(scs_inference,[],[77,6])). % 200.36/200.38 cnf(125,plain, % 200.36/200.38 (E(f2(x1251,f2(f2(a1,f2(a1,x1252)),f2(a1,x1253))),f2(x1251,f2(x1253,x1252)))), % 200.36/200.38 inference(scs_inference,[],[77,6,7,8,5])). % 200.36/200.38 cnf(126,plain, % 200.36/200.38 (E(f2(f2(f2(a1,f2(a1,x1261)),f2(a1,x1262)),x1263),f2(f2(x1262,x1261),x1263))), % 200.36/200.38 inference(scs_inference,[],[77,6,7,8,5,4])). % 200.36/200.38 cnf(132,plain, % 200.36/200.38 (E(f2(x1321,f2(f2(a1,f2(a1,x1322)),f2(a1,f2(a1,x1323)))),f2(x1321,f2(x1322,x1323)))), % 200.36/200.38 inference(scs_inference,[],[65,6,5])). % 200.36/200.38 cnf(136,plain, % 200.36/200.38 (~E(f2(f2(a3,f2(a1,f5(x1361))),f4(x1361)),f2(f2(x1361,f4(x1361)),f5(x1361)))), % 200.36/200.38 inference(scs_inference,[],[65,85,6,5,8,7,4,2])). % 200.36/200.38 cnf(173,plain, % 200.36/200.38 (E(f5(f2(x1731,x1732)),f5(f2(f2(a1,x1731),f2(a1,x1732))))), % 200.36/200.38 inference(scs_inference,[],[69,6])). % 200.36/200.38 cnf(178,plain, % 200.36/200.38 (E(f2(f2(f2(a1,f2(a1,x1781)),f2(a1,a1)),f2(f2(a3,f2(a1,x1782)),a1)),f2(x1782,x1781))), % 200.36/200.38 inference(scs_inference,[],[126,80,69,6,7,8,5,4,3])). % 200.36/200.38 cnf(193,plain, % 200.36/200.38 (E(f5(f2(f2(a1,x1931),x1932)),f5(f2(x1932,x1931)))), % 200.36/200.38 inference(scs_inference,[],[173,122,6,5,7,8,4,3])). % 200.36/200.38 cnf(199,plain, % 200.36/200.38 (E(f2(f5(f2(f2(a1,x1991),x1992)),x1993),f2(f5(f2(x1992,x1991)),x1993))), % 200.36/200.38 inference(scs_inference,[],[193,6,7,8,5,4])). % 200.36/200.38 cnf(227,plain, % 200.36/200.38 (E(f5(f2(x2271,x2272)),f5(f2(f2(a1,f2(a1,x2272)),f2(a1,x2271))))), % 200.36/200.38 inference(scs_inference,[],[75,6])). % 200.36/200.38 cnf(243,plain, % 200.36/200.38 (E(f6(f2(f2(f2(a3,x2431),x2432),x2433)),f6(f2(x2431,f2(x2432,x2433))))), % 200.36/200.38 inference(scs_inference,[],[10,6,5,7])). % 200.36/200.38 cnf(245,plain, % 200.36/200.38 (E(f2(f2(f2(f2(a3,x2451),x2452),x2453),x2454),f2(f2(x2451,f2(x2452,x2453)),x2454))), % 200.36/200.38 inference(scs_inference,[],[10,6,5,7,8,4])). % 200.36/200.38 cnf(270,plain, % 200.36/200.38 (E(f2(x2701,f2(x2702,f2(x2703,x2704))),f2(x2701,f2(f2(f2(a3,x2702),x2703),x2704)))), % 200.36/200.38 inference(scs_inference,[],[23,6,7,8,5])). % 200.36/200.38 cnf(284,plain, % 200.36/200.38 (E(f5(f2(x2841,x2842)),f5(f2(f2(a1,x2842),x2841)))), % 200.36/200.38 inference(scs_inference,[],[12,6])). % 200.36/200.38 cnf(287,plain, % 200.36/200.38 (E(f2(x2871,f2(f2(a1,x2872),x2873)),f2(x2871,f2(x2873,x2872)))), % 200.36/200.38 inference(scs_inference,[],[9,12,6,7,8,5])). % 200.36/200.38 cnf(288,plain, % 200.36/200.38 (E(f2(f2(f2(a1,x2881),x2882),x2883),f2(f2(x2882,x2881),x2883))), % 200.36/200.38 inference(scs_inference,[],[9,12,6,7,8,5,4])). % 200.36/200.38 cnf(292,plain, % 200.36/200.38 (E(f6(f2(x2921,f2(f2(a1,x2922),x2923))),f6(f2(x2921,f2(x2923,x2922))))), % 200.36/200.38 inference(scs_inference,[],[287,6,8,5,7])). % 200.36/200.38 cnf(294,plain, % 200.36/200.38 (~E(f2(f2(f5(a1),f4(a1)),f6(a1)),f2(f2(f4(a1),f6(a1)),f5(a1)))), % 200.36/200.38 inference(scs_inference,[],[11,287,288,6,8,5,7,4,3])). % 200.36/200.38 cnf(297,plain, % 200.36/200.38 (~E(f2(f2(f4(a1),f6(a1)),f5(a1)),f2(f2(f5(a1),f4(a1)),f6(a1)))), % 200.36/200.38 inference(scs_inference,[],[11,287,288,6,8,5,7,4,3,2])). % 200.36/200.38 cnf(308,plain, % 200.36/200.38 (E(f6(f2(f2(f2(a1,x3081),x3082),x3083)),f6(f2(f2(x3082,x3081),x3083)))), % 200.36/200.38 inference(scs_inference,[],[284,288,6,8,7])). % 200.36/200.38 cnf(318,plain, % 200.36/200.38 (E(f2(f2(x3181,x3182),x3183),f2(f2(f2(a1,x3182),x3181),x3183))), % 200.36/200.38 inference(scs_inference,[],[12,5,4])). % 200.36/200.38 cnf(320,plain, % 200.36/200.38 (E(f6(f2(x3201,f2(x3202,x3203))),f6(f2(x3201,f2(f2(a1,x3203),x3202))))), % 200.36/200.38 inference(scs_inference,[],[12,5,4,6,7])). % 200.36/200.38 cnf(332,plain, % 200.36/200.38 (E(f6(f2(f2(f2(a3,x3321),f2(a1,x3322)),x3323)),f6(f2(x3321,f2(x3323,x3322))))), % 200.36/200.38 inference(scs_inference,[],[243,292,318,5,4,3])). % 200.36/200.38 cnf(340,plain, % 200.36/200.38 (E(f2(f2(a1,x3401),f2(f2(a1,f2(a1,x3402)),f2(a1,f2(a1,x3403)))),f2(f2(x3402,x3403),x3401))), % 200.36/200.38 inference(scs_inference,[],[9,178,132,2,3])). % 200.36/200.38 cnf(343,plain, % 200.36/200.38 (~E(f2(f4(a3),f2(f5(a3),f6(a3))),f2(f2(a1,f5(a3)),f2(f4(a3),f6(a3))))), % 200.36/200.38 inference(scs_inference,[],[10,86,3])). % 200.36/200.38 cnf(348,plain, % 200.36/200.38 (E(f2(f2(a1,x3481),f2(f2(a3,f2(a1,x3482)),f2(a3,x3483))),f2(f2(a1,x3483),f2(a1,f2(x3481,x3482))))), % 200.36/200.38 inference(scs_inference,[],[10,340,110,2,3])). % 200.36/200.38 cnf(354,plain, % 200.36/200.38 (E(f2(f2(a1,x3541),f2(a1,f2(x3542,x3543))),f2(f2(a1,x3542),f2(f2(a3,f2(a1,x3543)),f2(a3,x3541))))), % 200.36/200.38 inference(scs_inference,[],[348,2])). % 200.36/200.38 cnf(379,plain, % 200.36/200.38 (~E(f2(f2(a1,f5(a1)),f2(f4(a1),f6(a1))),f2(f2(f5(a1),f4(a1)),f6(a1)))), % 200.36/200.38 inference(scs_inference,[],[12,297,3])). % 200.36/200.38 cnf(381,plain, % 200.36/200.38 (~E(f2(f2(f5(a1),f4(a1)),f6(a1)),f2(f2(a1,f5(a1)),f2(f4(a1),f6(a1))))), % 200.36/200.38 inference(scs_inference,[],[12,297,3,2])). % 200.36/200.38 cnf(383,plain, % 200.36/200.38 (~E(f2(f2(a1,f6(a1)),f2(f5(a1),f4(a1))),f2(f2(f4(a1),f6(a1)),f5(a1)))), % 200.36/200.38 inference(scs_inference,[],[12,294,120,2,3])). % 200.36/200.38 cnf(386,plain, % 200.36/200.38 (~E(f2(f2(a1,f2(f5(a1),f4(a1))),f2(a1,f6(a1))),f2(f2(f4(a1),f6(a1)),f5(a1)))), % 200.36/200.38 inference(scs_inference,[],[12,383,2,3])). % 200.36/200.38 cnf(389,plain, % 200.36/200.38 (E(f2(f2(a1,x3891),f2(a1,f2(x3892,x3893))),f2(f2(a1,f2(f2(a3,f2(a1,x3893)),f2(a3,x3891))),f2(a1,x3892)))), % 200.36/200.38 inference(scs_inference,[],[12,354,332,2,3])). % 200.36/200.38 cnf(392,plain, % 200.36/200.38 (~E(f2(f2(a1,f2(f4(a1),f6(a1))),f2(a1,f5(a1))),f2(f2(f5(a1),f4(a1)),f6(a1)))), % 200.36/200.38 inference(scs_inference,[],[12,379,386,2,3])). % 200.36/200.38 cnf(395,plain, % 200.36/200.38 (E(f2(f2(a1,f2(a1,f2(x3951,x3952))),f2(a1,x3953)),f2(f2(a1,f2(f2(a3,f2(a1,x3952)),f2(a3,x3953))),f2(a1,x3951)))), % 200.36/200.38 inference(scs_inference,[],[12,389,116,2,3])). % 200.36/200.38 cnf(398,plain, % 200.36/200.38 (~E(f2(f2(a1,f4(x3981)),f2(a3,f2(a1,f5(x3981)))),f2(f2(x3981,f4(x3981)),f5(x3981)))), % 200.36/200.38 inference(scs_inference,[],[12,136,392,2,3])). % 200.36/200.38 cnf(401,plain, % 200.36/200.38 (E(f2(f5(f2(f2(a1,x4011),x4012)),x4013),f2(f2(a1,x4013),f5(f2(x4012,x4011))))), % 200.36/200.38 inference(scs_inference,[],[12,395,199,2,3])). % 200.36/200.38 cnf(405,plain, % 200.36/200.38 (~E(f2(f2(a1,f6(a1)),f2(f5(a1),f4(a1))),f2(f2(a1,f5(a1)),f2(f4(a1),f6(a1))))), % 200.36/200.38 inference(scs_inference,[],[12,381,398,2,3])). % 200.36/200.38 cnf(411,plain, % 200.36/200.38 (~E(f2(f2(a1,f5(a1)),f2(f4(a1),f6(a1))),f2(f2(a1,f6(a1)),f2(f5(a1),f4(a1))))), % 200.36/200.38 inference(scs_inference,[],[405,2])). % 200.36/200.38 cnf(421,plain, % 200.36/200.38 (~E(f2(f2(a1,f6(a3)),f2(f2(a3,f4(a3)),f5(a3))),f2(f2(a1,f5(a3)),f2(f4(a3),f6(a3))))), % 200.36/200.38 inference(scs_inference,[],[16,343,3])). % 200.36/200.38 cnf(432,plain, % 200.36/200.38 (~E(f2(f2(a1,f4(x4321)),f2(f2(f2(a3,a3),a1),f5(x4321))),f2(f2(x4321,f4(x4321)),f5(x4321)))), % 200.36/200.38 inference(scs_inference,[],[401,270,398,2,3])). % 200.36/200.38 cnf(435,plain, % 200.36/200.38 (~E(f2(f2(a1,f6(a1)),f2(f2(a3,f2(a1,f5(a1))),f4(a1))),f2(f2(f5(a1),f4(a1)),f6(a1)))), % 200.36/200.38 inference(scs_inference,[],[16,432,379,2,3])). % 200.36/200.38 cnf(441,plain, % 200.36/200.38 (~E(f2(f2(a1,f4(a1)),f2(f2(a3,f2(a1,f6(a1))),f5(a1))),f2(f2(f4(a1),f6(a1)),f5(a1)))), % 200.36/200.38 inference(scs_inference,[],[16,435,383,2,3])). % 200.36/200.38 cnf(449,plain, % 200.36/200.38 (E(f2(x4491,f2(f2(a1,f2(a1,x4492)),f2(a1,x4493))),f2(f2(a1,x4492),f2(f2(a3,x4491),x4493)))), % 200.36/200.38 inference(scs_inference,[],[16,441,125,2,3])). % 200.36/200.38 cnf(452,plain, % 200.36/200.38 (~E(f2(f2(a1,f2(f5(a3),f6(a3))),f4(a3)),f2(f2(a1,f5(a3)),f2(f4(a3),f6(a3))))), % 200.36/200.38 inference(scs_inference,[],[17,449,421,2,3])). % 200.36/200.38 cnf(454,plain, % 200.36/200.38 (~E(f2(f2(a1,f5(a3)),f2(f4(a3),f6(a3))),f2(f2(a1,f2(f5(a3),f6(a3))),f4(a3)))), % 200.36/200.38 inference(scs_inference,[],[452,2])). % 200.36/200.38 cnf(467,plain, % 200.36/200.38 (~E(f2(f2(f2(a3,f2(a1,f5(a3))),f4(a3)),f6(a3)),f2(f2(a1,f2(f5(a3),f6(a3))),f4(a3)))), % 200.36/200.38 inference(scs_inference,[],[23,454,3])). % 200.36/200.38 cnf(473,plain, % 200.36/200.38 (~E(f2(f2(f2(a3,f2(a1,f5(a1))),f4(a1)),f6(a1)),f2(f2(a1,f6(a1)),f2(f5(a1),f4(a1))))), % 200.36/200.38 inference(scs_inference,[],[23,411,467,2,3])). % 200.36/200.38 cnf(479,plain, % 200.36/200.38 (~E(f2(f2(f2(a3,f2(a1,f4(x4791))),f2(f2(a3,a3),a1)),f5(x4791)),f2(f2(x4791,f4(x4791)),f5(x4791)))), % 200.36/200.38 inference(scs_inference,[],[23,473,432,2,3])). % 200.36/200.38 cnf(624,plain, % 200.36/200.38 (~E(f2(x6241,f4(x6241)),f2(f2(a3,f2(a1,f4(x6241))),f2(f2(a3,a3),a1)))), % 200.36/200.38 inference(scs_inference,[],[9,20,479,432,4,5,3,2])). % 200.36/200.38 cnf(1802,plain, % 200.36/200.38 (E(f2(f2(a1,x18021),f2(f2(f2(a3,x18022),x18023),x18024)),f2(f2(x18022,f2(x18023,x18024)),x18021))), % 200.36/200.38 inference(scs_inference,[],[9,245,227,4,5,8,7,6,3])). % 200.36/200.38 cnf(1985,plain, % 200.36/200.38 (E(f6(f2(f2(f2(a1,x19851),x19852),f2(x19853,x19854))),f6(f2(f2(x19852,x19851),f2(f2(a1,x19854),x19853))))), % 200.36/200.38 inference(scs_inference,[],[308,320,1802,2,3])). % 200.36/200.38 cnf(1989,plain, % 200.36/200.38 ($false), % 200.36/200.38 inference(scs_inference,[],[10,1985,624,1802,2,3]), % 200.36/200.38 ['proof']). % 200.36/200.39 % SZS output end Proof % 200.36/200.39 % Total time :199.630000s %------------------------------------------------------------------------------