%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : GRP529-1 : TPTP v8.2.0. Released v2.6.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/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 06:39:52 EDT 2024 % Result : Unsatisfiable 143.00s 142.98s % Output : CNFRefutation 143.05s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.14 % Problem : GRP529-1 : TPTP v8.2.0. Released v2.6.0. % 0.08/0.14 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.14/0.36 % Computer : n026.cluster.edu % 0.14/0.36 % Model : x86_64 x86_64 % 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.36 % Memory : 8042.1875MB % 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.36 % CPULimit : 300 % 0.14/0.36 % WCLimit : 300 % 0.14/0.36 % DateTime : Thu Jun 20 08:33:39 EDT 2024 % 0.14/0.36 % CPUTime : % 0.22/0.59 start to proof:theBenchmark % 142.90/142.95 %------------------------------------------- % 142.90/142.95 % File :CSE---1.7 % 142.90/142.95 % Problem :theBenchmark % 142.90/142.95 % Transform :cnf % 142.90/142.95 % Format :tptp:raw % 142.90/142.95 % Command :java -jar mcs_scs.jar %d %s % 142.90/142.95 % 142.90/142.95 % Result :Theorem 142.320000s % 142.90/142.95 % Output :CNFRefutation 142.320000s % 142.90/142.95 %------------------------------------------- % 143.00/142.98 %-------------------------------------------------------------------------- % 143.00/142.98 % File : GRP529-1 : TPTP v8.2.0. Released v2.6.0. % 143.00/142.98 % Domain : Group Theory (Abelian) % 143.00/142.98 % Problem : Axiom for Abelian group theory, in division, part 1 % 143.00/142.98 % Version : [McC93] (equality) axioms. % 143.00/142.98 % English : % 143.00/142.98 % 143.00/142.98 % Refs : [McC93] McCune (1993), Single Axioms for Groups and Abelian Gr % 143.00/142.98 % Source : [TPTP] % 143.00/142.98 % Names : % 143.00/142.98 % 143.00/142.98 % Status : Unsatisfiable % 143.00/142.98 % Rating : 0.05 v8.2.0, 0.00 v7.4.0, 0.09 v7.3.0, 0.05 v7.1.0, 0.00 v7.0.0, 0.05 v6.3.0, 0.12 v6.2.0, 0.14 v6.1.0, 0.06 v6.0.0, 0.14 v5.5.0, 0.11 v5.4.0, 0.00 v5.1.0, 0.07 v5.0.0, 0.00 v2.7.0, 0.09 v2.6.0 % 143.00/142.98 % Syntax : Number of clauses : 4 ( 4 unt; 0 nHn; 1 RR) % 143.00/142.98 % Number of literals : 4 ( 4 equ; 1 neg) % 143.00/142.98 % Maximal clause size : 1 ( 1 avg) % 143.00/142.98 % Maximal term depth : 4 ( 2 avg) % 143.00/142.98 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty) % 143.00/142.98 % Number of functors : 5 ( 5 usr; 2 con; 0-2 aty) % 143.00/142.98 % Number of variables : 8 ( 0 sgn) % 143.00/142.98 % SPC : CNF_UNS_RFO_PEQ_UEQ % 143.00/142.98 % 143.00/142.98 % Comments : A UEQ part of GRP090-1 % 143.00/142.98 %-------------------------------------------------------------------------- % 143.00/142.98 cnf(single_axiom,axiom, % 143.00/142.98 divide(divide(A,divide(B,C)),divide(A,B)) = C ). % 143.00/142.98 % 143.00/142.98 cnf(multiply,axiom, % 143.00/142.98 multiply(A,B) = divide(A,divide(divide(C,C),B)) ). % 143.00/142.98 % 143.00/142.98 cnf(inverse,axiom, % 143.00/142.98 inverse(A) = divide(divide(B,B),A) ). % 143.00/142.98 % 143.00/142.98 cnf(prove_these_axioms_1,negated_conjecture, % 143.00/142.98 multiply(inverse(a1),a1) != multiply(inverse(b1),b1) ). % 143.00/142.98 % 143.00/142.98 %-------------------------------------------------------------------------- % 143.00/142.98 %------------------------------------------- % 143.00/142.98 % Proof found % 143.00/142.98 % SZS status Theorem for theBenchmark % 143.00/142.98 % SZS output start Proof % 143.02/143.00 %ClaNum:12(EqnAxiom:8) % 143.02/143.00 %VarNum:16(SingletonVarNum:8) % 143.02/143.00 %MaxLitNum:1 % 143.02/143.00 %MaxfuncDepth:3 % 143.02/143.00 %SharedTerms:7 % 143.02/143.00 %goalClause: 12 % 143.02/143.00 %singleGoalClaCount:1 % 143.02/143.00 [12]~E(f5(f4(a2),a2),f5(f4(a3),a3)) % 143.02/143.01 [9]E(f1(f1(x91,x91),x92),f4(x92)) % 143.02/143.01 [11]E(f1(f1(x111,f1(x112,x113)),f1(x111,x112)),x113) % 143.02/143.01 [10]E(f1(x101,f1(f1(x102,x102),x103)),f5(x101,x103)) % 143.02/143.01 %EqnAxiom % 143.02/143.01 [1]E(x11,x11) % 143.02/143.01 [2]E(x22,x21)+~E(x21,x22) % 143.02/143.01 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 143.02/143.01 [4]~E(x41,x42)+E(f1(x41,x43),f1(x42,x43)) % 143.02/143.01 [5]~E(x51,x52)+E(f1(x53,x51),f1(x53,x52)) % 143.02/143.01 [6]~E(x61,x62)+E(f5(x61,x63),f5(x62,x63)) % 143.02/143.01 [7]~E(x71,x72)+E(f5(x73,x71),f5(x73,x72)) % 143.02/143.01 [8]~E(x81,x82)+E(f4(x81),f4(x82)) % 143.02/143.01 % 143.02/143.01 %------------------------------------------- % 143.05/143.04 cnf(13,plain, % 143.05/143.04 (E(f4(x131),f1(f1(x132,x132),x131))), % 143.05/143.04 inference(scs_inference,[],[9,2])). % 143.05/143.04 cnf(14,plain, % 143.05/143.04 (~E(f5(f4(a2),a2),f1(f4(a3),f1(f1(x141,x141),a3)))), % 143.05/143.04 inference(scs_inference,[],[12,9,10,2,3])). % 143.05/143.04 cnf(16,plain, % 143.05/143.04 (E(x161,f1(f1(x162,f1(x163,x161)),f1(x162,x163)))), % 143.05/143.04 inference(scs_inference,[],[11,2])). % 143.05/143.04 cnf(17,plain, % 143.05/143.04 (E(f5(x171,x172),f1(x171,f1(f1(x173,x173),x172)))), % 143.05/143.04 inference(scs_inference,[],[10,2])). % 143.05/143.04 cnf(20,plain, % 143.05/143.04 (E(x201,f4(f1(f1(x202,x201),x202)))), % 143.05/143.04 inference(scs_inference,[],[16,9,3])). % 143.05/143.04 cnf(27,plain, % 143.05/143.04 (E(f4(f1(f1(x271,x271),x272)),f5(f1(x273,x273),x272))), % 143.05/143.04 inference(scs_inference,[],[17,9,3,2])). % 143.05/143.04 cnf(28,plain, % 143.05/143.04 (E(f1(f1(x281,x281),f1(f1(x282,x282),x283)),f5(f1(x284,x284),x283))), % 143.05/143.04 inference(scs_inference,[],[9,27,3])). % 143.05/143.04 cnf(31,plain, % 143.05/143.04 (E(f1(f1(x311,f1(x312,x313)),f1(x311,x312)),f1(f1(x314,f1(x315,x313)),f1(x314,x315)))), % 143.05/143.04 inference(scs_inference,[],[11,16,3])). % 143.05/143.04 cnf(33,plain, % 143.05/143.04 (E(x331,f5(f1(x332,x332),x331))), % 143.05/143.04 inference(scs_inference,[],[16,28,3])). % 143.05/143.04 cnf(36,plain, % 143.05/143.04 (E(f5(f1(x361,x361),x362),x362)), % 143.05/143.04 inference(scs_inference,[],[16,28,3,2])). % 143.05/143.04 cnf(40,plain, % 143.05/143.04 (~E(f5(f4(a2),a2),f5(f1(x401,x401),f5(f4(a3),a3)))), % 143.05/143.04 inference(scs_inference,[],[36,12,3])). % 143.05/143.04 cnf(42,plain, % 143.05/143.04 (E(x421,f1(f1(x422,x422),f1(f1(x423,x421),x423)))), % 143.05/143.04 inference(scs_inference,[],[20,13,3])). % 143.05/143.04 cnf(60,plain, % 143.05/143.04 (E(f5(f1(x601,x601),x602),f1(f1(x603,x603),f1(f1(x604,x602),x604)))), % 143.05/143.04 inference(scs_inference,[],[36,42,3])). % 143.05/143.04 cnf(104,plain, % 143.05/143.04 (E(f1(f1(f1(x1041,x1041),x1042),x1043),f1(f4(x1042),x1043))), % 143.05/143.04 inference(scs_inference,[],[9,8,4])). % 143.05/143.04 cnf(105,plain, % 143.05/143.04 (E(f1(x1051,f1(f1(x1052,x1052),x1053)),f1(x1051,f4(x1053)))), % 143.05/143.04 inference(scs_inference,[],[9,8,4,5])). % 143.05/143.04 cnf(106,plain, % 143.05/143.04 (E(f5(f1(f1(x1061,x1061),x1062),x1063),f5(f4(x1062),x1063))), % 143.05/143.04 inference(scs_inference,[],[9,8,4,5,6])). % 143.05/143.04 cnf(108,plain, % 143.05/143.04 (~E(f5(f1(x1081,x1081),f5(f4(a3),a3)),f5(f4(a2),a2))), % 143.05/143.04 inference(scs_inference,[],[9,40,8,4,5,6,7,2])). % 143.05/143.04 cnf(111,plain, % 143.05/143.04 (E(f5(x1111,x1112),f5(f5(f1(x1113,x1113),x1111),x1112))), % 143.05/143.04 inference(scs_inference,[],[33,6])). % 143.05/143.04 cnf(113,plain, % 143.05/143.04 (E(f1(x1131,x1132),f1(f5(f1(x1133,x1133),x1131),x1132))), % 143.05/143.04 inference(scs_inference,[],[33,6,8,4])). % 143.05/143.04 cnf(114,plain, % 143.05/143.04 (E(f1(x1141,x1142),f1(x1141,f5(f1(x1143,x1143),x1142)))), % 143.05/143.04 inference(scs_inference,[],[33,6,8,4,5])). % 143.05/143.04 cnf(115,plain, % 143.05/143.04 (E(f5(x1151,x1152),f5(x1151,f5(f1(x1153,x1153),x1152)))), % 143.05/143.04 inference(scs_inference,[],[33,6,8,4,5,7])). % 143.05/143.04 cnf(116,plain, % 143.05/143.04 (~E(f1(f4(a3),f1(f1(x1161,x1161),a3)),f5(f4(a2),a2))), % 143.05/143.04 inference(scs_inference,[],[14,33,6,8,4,5,7,2])). % 143.05/143.04 cnf(121,plain, % 143.05/143.04 (E(f5(x1211,f1(f1(x1212,f1(x1213,x1214)),f1(x1212,x1213))),f5(x1211,x1214))), % 143.05/143.04 inference(scs_inference,[],[11,6,8,5,4,7])). % 143.05/143.04 cnf(122,plain, % 143.05/143.04 (~E(f5(f4(a3),a3),f5(f4(a2),a2))), % 143.05/143.04 inference(scs_inference,[],[12,11,6,8,5,4,7,2])). % 143.05/143.04 cnf(123,plain, % 143.05/143.04 (E(f5(x1231,x1232),f5(f1(f1(x1233,f1(x1234,x1231)),f1(x1233,x1234)),x1232))), % 143.05/143.04 inference(scs_inference,[],[16,6])). % 143.05/143.04 cnf(127,plain, % 143.05/143.04 (E(f5(x1271,x1272),f5(x1271,f1(f1(x1273,f1(x1274,x1272)),f1(x1273,x1274))))), % 143.05/143.04 inference(scs_inference,[],[16,6,8,4,5,7])). % 143.05/143.04 cnf(128,plain, % 143.05/143.04 (E(f5(f4(x1281),x1282),f5(f1(f1(x1283,x1283),x1281),x1282))), % 143.05/143.04 inference(scs_inference,[],[13,6])). % 143.05/143.04 cnf(130,plain, % 143.05/143.04 (E(f1(x1301,f4(x1302)),f1(x1301,f1(f1(x1303,x1303),x1302)))), % 143.05/143.04 inference(scs_inference,[],[13,6,8,5])). % 143.05/143.04 cnf(131,plain, % 143.05/143.04 (E(f1(f4(x1311),x1312),f1(f1(f1(x1313,x1313),x1311),x1312))), % 143.05/143.04 inference(scs_inference,[],[13,6,8,5,4])). % 143.05/143.04 cnf(132,plain, % 143.05/143.04 (E(f5(x1321,f4(x1322)),f5(x1321,f1(f1(x1323,x1323),x1322)))), % 143.05/143.04 inference(scs_inference,[],[13,6,8,5,4,7])). % 143.05/143.04 cnf(138,plain, % 143.05/143.04 (E(f1(f5(f1(x1381,x1381),x1382),x1383),f1(x1382,x1383))), % 143.05/143.04 inference(scs_inference,[],[36,6,8,4])). % 143.05/143.04 cnf(139,plain, % 143.05/143.04 (E(f1(x1391,f5(f1(x1392,x1392),x1393)),f1(x1391,x1393))), % 143.05/143.04 inference(scs_inference,[],[36,6,8,4,5])). % 143.05/143.04 cnf(140,plain, % 143.05/143.04 (E(f5(x1401,f5(f1(x1402,x1402),x1403)),f5(x1401,x1403))), % 143.05/143.04 inference(scs_inference,[],[36,6,8,4,5,7])). % 143.05/143.04 cnf(141,plain, % 143.05/143.04 (E(f1(f5(f1(x1411,x1411),f1(x1412,f1(x1413,x1414))),f1(x1412,x1413)),x1414)), % 143.05/143.04 inference(scs_inference,[],[11,138,3])). % 143.05/143.04 cnf(143,plain, % 143.05/143.04 (~E(f1(f5(f1(x1431,x1431),f4(a3)),f1(f1(x1432,x1432),a3)),f5(f4(a2),a2))), % 143.05/143.04 inference(scs_inference,[],[113,116,3])). % 143.05/143.04 cnf(146,plain, % 143.05/143.04 (~E(f1(f4(a2),f1(f1(x1461,x1461),a2)),f5(f4(a3),a3))), % 143.05/143.04 inference(scs_inference,[],[17,12,3])). % 143.05/143.04 cnf(151,plain, % 143.05/143.04 (~E(f1(f4(a2),f4(a2)),f5(f4(a3),a3))), % 143.05/143.04 inference(scs_inference,[],[105,146,3])). % 143.05/143.04 cnf(153,plain, % 143.05/143.04 (~E(f5(f4(a3),a3),f1(f4(a2),f4(a2)))), % 143.05/143.04 inference(scs_inference,[],[105,146,3,2])). % 143.05/143.04 cnf(154,plain, % 143.05/143.04 (~E(f1(f4(a2),f5(f1(x1541,x1541),f4(a2))),f5(f4(a3),a3))), % 143.05/143.04 inference(scs_inference,[],[151,114,3])). % 143.05/143.04 cnf(157,plain, % 143.05/143.04 (~E(f5(f4(a3),f5(f1(x1571,x1571),a3)),f1(f4(a2),f4(a2)))), % 143.05/143.04 inference(scs_inference,[],[153,115,3])). % 143.05/143.04 cnf(160,plain, % 143.05/143.04 (~E(f5(f1(x1601,x1601),f5(f4(a3),a3)),f1(f4(a2),f4(a2)))), % 143.05/143.04 inference(scs_inference,[],[33,153,3])). % 143.05/143.04 cnf(165,plain, % 143.05/143.04 (~E(f5(f1(x1651,x1651),f1(f4(a2),f4(a2))),f5(f4(a3),a3))), % 143.05/143.04 inference(scs_inference,[],[33,151,3])). % 143.05/143.04 cnf(170,plain, % 143.05/143.04 (~E(f5(f1(x1701,x1701),f5(f4(a2),a2)),f5(f4(a3),a3))), % 143.05/143.04 inference(scs_inference,[],[33,12,3])). % 143.05/143.04 cnf(175,plain, % 143.05/143.04 (~E(f5(f4(f1(x1751,x1751)),f1(f4(a2),f4(a2))),f5(f4(a3),a3))), % 143.05/143.04 inference(scs_inference,[],[106,165,3])). % 143.05/143.04 cnf(182,plain, % 143.05/143.04 (~E(f5(f1(f1(x1821,x1821),a3),f5(f1(x1822,x1822),a3)),f1(f4(a2),f4(a2)))), % 143.05/143.04 inference(scs_inference,[],[157,128,3])). % 143.05/143.04 cnf(185,plain, % 143.05/143.04 (~E(f5(f1(f1(x1851,x1851),a3),a3),f1(f4(a2),f4(a2)))), % 143.05/143.04 inference(scs_inference,[],[140,182,2,3])). % 143.05/143.04 cnf(188,plain, % 143.05/143.04 (~E(f1(f4(a2),f4(a2)),f5(f1(f1(x1881,x1881),a3),a3))), % 143.05/143.04 inference(scs_inference,[],[185,2])). % 143.05/143.04 cnf(200,plain, % 143.05/143.04 (~E(f1(f5(f1(x2001,x2001),f4(a3)),f4(a3)),f5(f4(a2),a2))), % 143.05/143.04 inference(scs_inference,[],[143,105,3])). % 143.05/143.04 cnf(205,plain, % 143.05/143.04 (~E(f5(f4(a2),a2),f1(f4(a3),f4(a3)))), % 143.05/143.04 inference(scs_inference,[],[138,200,3,2])). % 143.05/143.04 cnf(219,plain, % 143.05/143.04 (~E(f5(f4(f1(x2191,x2191)),f5(f4(a2),a2)),f5(f4(a3),a3))), % 143.05/143.04 inference(scs_inference,[],[170,106,3])). % 143.05/143.04 cnf(235,plain, % 143.05/143.04 (~E(f5(f4(f1(x2351,x2351)),f5(f4(a3),a3)),f5(f4(a2),a2))), % 143.05/143.04 inference(scs_inference,[],[106,108,3])). % 143.05/143.04 cnf(242,plain, % 143.05/143.04 (~E(f5(f4(f1(x2421,x2421)),f5(f4(a3),a3)),f1(f4(a2),f4(a2)))), % 143.05/143.04 inference(scs_inference,[],[106,160,3])). % 143.05/143.04 cnf(257,plain, % 143.05/143.04 (~E(f5(f5(f1(x2571,x2571),f4(a2)),a2),f1(f4(a3),f4(a3)))), % 143.05/143.04 inference(scs_inference,[],[111,205,3])). % 143.05/143.04 cnf(259,plain, % 143.05/143.04 (~E(f1(f4(a3),f4(a3)),f5(f5(f1(x2591,x2591),f4(a2)),a2))), % 143.05/143.04 inference(scs_inference,[],[111,205,3,2])). % 143.05/143.04 cnf(296,plain, % 143.05/143.04 (~E(f1(f5(f1(x2961,x2961),f4(a2)),f4(a2)),f5(f1(f1(x2962,x2962),a3),a3))), % 143.05/143.04 inference(scs_inference,[],[113,188,3])). % 143.05/143.04 cnf(299,plain, % 143.05/143.04 (~E(f1(f5(f1(x2991,x2991),f4(a2)),f1(f1(x2992,x2992),a2)),f1(f4(a3),f4(a3)))), % 143.05/143.04 inference(scs_inference,[],[257,296,17,2,3])). % 143.05/143.04 cnf(302,plain, % 143.05/143.04 (~E(f1(f5(f1(x3021,x3021),f4(a2)),f5(f1(x3022,x3022),f4(a2))),f5(f4(a3),a3))), % 143.05/143.04 inference(scs_inference,[],[113,299,154,2,3])). % 143.05/143.04 cnf(305,plain, % 143.05/143.04 (~E(f1(f5(f1(x3051,x3051),f4(a2)),f4(a2)),f5(f4(a3),a3))), % 143.05/143.04 inference(scs_inference,[],[302,139,2,3])). % 143.05/143.04 cnf(307,plain, % 143.05/143.04 (~E(f5(f4(a3),a3),f1(f5(f1(x3071,x3071),f4(a2)),f4(a2)))), % 143.05/143.04 inference(scs_inference,[],[305,2])). % 143.05/143.04 cnf(308,plain, % 143.05/143.04 (~E(f1(f5(f1(x3081,x3081),f5(f1(x3082,x3082),f4(a2))),f4(a2)),f5(f4(a3),a3))), % 143.05/143.04 inference(scs_inference,[],[113,305,2,3])). % 143.05/143.04 cnf(311,plain, % 143.05/143.04 (~E(f1(f1(f1(x3111,x3111),a3),f4(a3)),f5(f5(f1(x3112,x3112),f4(a2)),a2))), % 143.05/143.04 inference(scs_inference,[],[259,308,131,2,3])). % 143.05/143.04 cnf(314,plain, % 143.05/143.04 (~E(f1(f5(f1(x3141,x3141),f4(a2)),f1(f1(x3142,x3142),a2)),f5(f4(a3),a3))), % 143.05/143.04 inference(scs_inference,[],[113,311,146,2,3])). % 143.05/143.04 cnf(317,plain, % 143.05/143.04 (~E(f1(f4(a3),f1(f1(x3171,x3171),a3)),f1(f5(f1(x3172,x3172),f4(a2)),f4(a2)))), % 143.05/143.04 inference(scs_inference,[],[307,314,17,2,3])). % 143.05/143.04 cnf(319,plain, % 143.05/143.04 (~E(f1(f5(f1(x3191,x3191),f4(a2)),f4(a2)),f1(f4(a3),f1(f1(x3192,x3192),a3)))), % 143.05/143.04 inference(scs_inference,[],[317,2])). % 143.05/143.04 cnf(326,plain, % 143.05/143.04 (~E(f1(f4(a2),f4(a2)),f1(f4(a3),f1(f1(x3261,x3261),a3)))), % 143.05/143.04 inference(scs_inference,[],[319,138,3])). % 143.05/143.04 cnf(328,plain, % 143.05/143.04 (~E(f1(f4(a3),f1(f1(x3281,x3281),a3)),f1(f4(a2),f4(a2)))), % 143.05/143.04 inference(scs_inference,[],[326,2])). % 143.05/143.04 cnf(335,plain, % 143.05/143.04 (~E(f5(f4(a2),f5(f1(x3351,x3351),a2)),f5(f4(a3),a3))), % 143.05/143.04 inference(scs_inference,[],[115,12,3])). % 143.05/143.04 cnf(340,plain, % 143.05/143.04 (~E(f1(f4(a2),f4(a2)),f1(f4(a3),f4(a3)))), % 143.05/143.04 inference(scs_inference,[],[328,105,3,2])). % 143.05/143.04 cnf(341,plain, % 143.05/143.04 (~E(f1(f4(a2),f1(f1(x3411,x3411),a2)),f1(f4(a3),f4(a3)))), % 143.05/143.04 inference(scs_inference,[],[340,130,3])). % 143.05/143.04 cnf(343,plain, % 143.05/143.04 (~E(f1(f4(a3),f4(a3)),f1(f4(a2),f1(f1(x3431,x3431),a2)))), % 143.05/143.04 inference(scs_inference,[],[340,130,3,2])). % 143.05/143.04 cnf(356,plain, % 143.05/143.04 (~E(f5(f1(f1(x3561,x3561),a2),f5(f1(x3562,x3562),a2)),f5(f4(a3),a3))), % 143.05/143.04 inference(scs_inference,[],[335,128,3])). % 143.05/143.04 cnf(359,plain, % 143.05/143.04 (~E(f5(f4(a3),f1(f1(x3591,f1(x3592,a3)),f1(x3591,x3592))),f5(f4(a2),a2))), % 143.05/143.04 inference(scs_inference,[],[127,356,122,2,3])). % 143.05/143.04 cnf(362,plain, % 143.05/143.04 (~E(f1(f1(f1(x3621,x3621),a2),f1(f1(x3622,x3622),a2)),f1(f4(a3),f4(a3)))), % 143.05/143.04 inference(scs_inference,[],[341,359,131,2,3])). % 143.05/143.04 cnf(365,plain, % 143.05/143.04 (~E(f5(f4(a2),f1(f1(x3651,f1(x3652,a2)),f1(x3651,x3652))),f5(f4(a3),a3))), % 143.05/143.04 inference(scs_inference,[],[127,362,12,2,3])). % 143.05/143.04 cnf(368,plain, % 143.05/143.04 (~E(f1(f1(f1(x3681,x3681),a3),f4(a3)),f1(f4(a2),f1(f1(x3682,x3682),a2)))), % 143.05/143.04 inference(scs_inference,[],[343,365,131,2,3])). % 143.05/143.04 cnf(370,plain, % 143.05/143.04 (~E(f1(f4(a2),f1(f1(x3701,x3701),a2)),f1(f1(f1(x3702,x3702),a3),f4(a3)))), % 143.05/143.04 inference(scs_inference,[],[368,2])). % 143.05/143.04 cnf(371,plain, % 143.05/143.04 (~E(f5(f4(a2),a2),f1(f1(f1(x3711,x3711),a3),f4(a3)))), % 143.05/143.04 inference(scs_inference,[],[370,10,3])). % 143.05/143.04 cnf(373,plain, % 143.05/143.04 (~E(f1(f1(f1(x3731,x3731),a3),f4(a3)),f5(f4(a2),a2))), % 143.05/143.04 inference(scs_inference,[],[370,10,3,2])). % 143.05/143.04 cnf(376,plain, % 143.05/143.04 (~E(f1(f1(f1(x3761,x3761),a3),f4(a3)),f5(f1(f1(x3762,x3762),a2),a2))), % 143.05/143.04 inference(scs_inference,[],[128,371,3,2])). % 143.05/143.04 cnf(379,plain, % 143.05/143.04 (~E(f5(f1(f1(x3791,x3791),f1(x3792,x3792)),f5(f4(a3),a3)),f5(f4(a2),a2))), % 143.05/143.04 inference(scs_inference,[],[128,235,3])). % 143.05/143.04 cnf(382,plain, % 143.05/143.04 (~E(f1(f1(f1(x3821,x3821),a3),f1(f1(x3822,x3822),a3)),f5(f4(a2),a2))), % 143.05/143.04 inference(scs_inference,[],[373,379,130,2,3])). % 143.05/143.04 cnf(385,plain, % 143.05/143.04 (~E(f5(f1(f1(x3851,x3851),f1(x3852,x3852)),f5(f4(a3),a3)),f1(f4(a2),f4(a2)))), % 143.05/143.04 inference(scs_inference,[],[128,242,382,2,3])). % 143.05/143.04 cnf(388,plain, % 143.05/143.04 (~E(f1(f4(a3),f4(a3)),f5(f1(f1(x3881,x3881),a2),a2))), % 143.05/143.04 inference(scs_inference,[],[385,376,104,2,3])). % 143.05/143.04 cnf(391,plain, % 143.05/143.04 (~E(f5(f1(f1(x3911,x3911),f1(x3912,x3912)),f5(f4(a2),a2)),f5(f4(a3),a3))), % 143.05/143.04 inference(scs_inference,[],[128,388,219,2,3])). % 143.05/143.04 cnf(394,plain, % 143.05/143.04 (E(f5(f4(x3941),f4(x3942)),f5(f1(f1(x3943,x3943),x3941),f1(f1(x3944,x3944),x3942)))), % 143.05/143.04 inference(scs_inference,[],[128,391,132,2,3])). % 143.05/143.04 cnf(397,plain, % 143.05/143.04 (~E(f5(f1(f1(x3971,x3971),f1(x3972,x3972)),f1(f4(a2),f4(a2))),f5(f4(a3),a3))), % 143.05/143.04 inference(scs_inference,[],[128,175,3])). % 143.05/143.04 cnf(583,plain, % 143.05/143.04 (~E(f1(f1(x5831,x5831),f1(f1(x5832,f1(f4(a2),f4(a2))),x5832)),f5(f4(a3),a3))), % 143.05/143.04 inference(scs_inference,[],[397,121,60,6,4,5,8,7,3])). % 143.05/143.04 cnf(611,plain, % 143.05/143.04 (~E(f5(f4(a3),a3),f1(f1(x6111,f1(x6112,f1(f4(a2),f4(a2)))),f1(x6111,x6112)))), % 143.05/143.04 inference(scs_inference,[],[31,583,6,4,8,5,7,3,2])). % 143.05/143.04 cnf(744,plain, % 143.05/143.04 (~E(f5(f4(a3),a3),f5(f1(f1(x7441,x7441),f1(x7442,f1(f4(a2),f4(a2)))),x7442))), % 143.05/143.04 inference(scs_inference,[],[17,611,141,2,3])). % 143.05/143.04 cnf(1274,plain, % 143.05/143.04 (~E(f5(f4(a3),a3),f5(x12741,f1(f1(f4(a2),f4(a2)),x12741)))), % 143.05/143.04 inference(scs_inference,[],[744,123,3])). % 143.05/143.04 cnf(1291,plain, % 143.05/143.04 ($false), % 143.05/143.04 inference(scs_inference,[],[394,1274,20,3,7]), % 143.05/143.04 ['proof']). % 143.05/143.04 % SZS output end Proof % 143.05/143.04 % Total time :142.320000s %------------------------------------------------------------------------------