%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : GRP521-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 : n019.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:50 EDT 2024 % Result : Unsatisfiable 105.76s 105.78s % Output : CNFRefutation 105.80s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.13 % Problem : GRP521-1 : TPTP v8.2.0. Released v2.6.0. % 0.04/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n019.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Thu Jun 20 07:43:09 EDT 2024 % 0.12/0.34 % CPUTime : % 0.52/0.57 start to proof:theBenchmark % 105.75/105.74 %------------------------------------------- % 105.75/105.74 % File :CSE---1.7 % 105.75/105.74 % Problem :theBenchmark % 105.75/105.74 % Transform :cnf % 105.76/105.74 % Format :tptp:raw % 105.76/105.74 % Command :java -jar mcs_scs.jar %d %s % 105.76/105.74 % 105.76/105.74 % Result :Theorem 105.140000s % 105.76/105.74 % Output :CNFRefutation 105.140000s % 105.76/105.74 %------------------------------------------- % 105.76/105.78 %-------------------------------------------------------------------------- % 105.76/105.78 % File : GRP521-1 : TPTP v8.2.0. Released v2.6.0. % 105.76/105.78 % Domain : Group Theory (Abelian) % 105.76/105.78 % Problem : Axiom for Abelian group theory, in division, part 1 % 105.76/105.78 % Version : [McC93] (equality) axioms. % 105.76/105.78 % English : % 105.76/105.78 % 105.76/105.78 % Refs : [Tar38] Tarski (1938), Ein Beitrag zur Axiomatik der Abelschen % 105.76/105.78 % : [McC93] McCune (1993), Single Axioms for Groups and Abelian Gr % 105.76/105.78 % Source : [TPTP] % 105.76/105.78 % Names : % 105.76/105.78 % 105.76/105.78 % Status : Unsatisfiable % 105.76/105.78 % Rating : 0.05 v8.2.0, 0.00 v7.4.0, 0.09 v7.3.0, 0.00 v6.0.0, 0.10 v5.5.0, 0.05 v5.4.0, 0.00 v5.1.0, 0.07 v5.0.0, 0.00 v2.6.0 % 105.76/105.78 % Syntax : Number of clauses : 4 ( 4 unt; 0 nHn; 1 RR) % 105.76/105.78 % Number of literals : 4 ( 4 equ; 1 neg) % 105.76/105.78 % Maximal clause size : 1 ( 1 avg) % 105.76/105.78 % Maximal term depth : 5 ( 2 avg) % 105.76/105.78 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty) % 105.76/105.78 % Number of functors : 5 ( 5 usr; 2 con; 0-2 aty) % 105.76/105.78 % Number of variables : 8 ( 0 sgn) % 105.76/105.78 % SPC : CNF_UNS_RFO_PEQ_UEQ % 105.76/105.78 % 105.76/105.78 % Comments : A UEQ part of GRP088-1 % 105.76/105.78 %-------------------------------------------------------------------------- % 105.76/105.78 cnf(single_axiom,axiom, % 105.76/105.78 divide(A,divide(B,divide(C,divide(A,B)))) = C ). % 105.76/105.78 % 105.76/105.78 cnf(multiply,axiom, % 105.76/105.78 multiply(A,B) = divide(A,divide(divide(C,C),B)) ). % 105.76/105.78 % 105.76/105.78 cnf(inverse,axiom, % 105.76/105.78 inverse(A) = divide(divide(B,B),A) ). % 105.76/105.78 % 105.76/105.78 cnf(prove_these_axioms_1,negated_conjecture, % 105.76/105.78 multiply(inverse(a1),a1) != multiply(inverse(b1),b1) ). % 105.76/105.78 % 105.76/105.78 %-------------------------------------------------------------------------- % 105.76/105.78 %------------------------------------------- % 105.76/105.78 % Proof found % 105.76/105.78 % SZS status Theorem for theBenchmark % 105.76/105.78 % SZS output start Proof % 105.80/105.80 %ClaNum:12(EqnAxiom:8) % 105.80/105.80 %VarNum:16(SingletonVarNum:8) % 105.80/105.80 %MaxLitNum:1 % 105.80/105.80 %MaxfuncDepth:4 % 105.80/105.80 %SharedTerms:7 % 105.80/105.80 %goalClause: 12 % 105.80/105.80 %singleGoalClaCount:1 % 105.80/105.80 [12]~E(f5(f4(a2),a2),f5(f4(a3),a3)) % 105.80/105.80 [9]E(f1(f1(x91,x91),x92),f4(x92)) % 105.80/105.80 [10]E(f1(x101,f1(f1(x102,x102),x103)),f5(x101,x103)) % 105.80/105.80 [11]E(f1(x111,f1(x112,f1(x113,f1(x111,x112)))),x113) % 105.80/105.80 %EqnAxiom % 105.80/105.80 [1]E(x11,x11) % 105.80/105.80 [2]E(x22,x21)+~E(x21,x22) % 105.80/105.80 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 105.80/105.80 [4]~E(x41,x42)+E(f1(x41,x43),f1(x42,x43)) % 105.80/105.80 [5]~E(x51,x52)+E(f1(x53,x51),f1(x53,x52)) % 105.80/105.80 [6]~E(x61,x62)+E(f5(x61,x63),f5(x62,x63)) % 105.80/105.80 [7]~E(x71,x72)+E(f5(x73,x71),f5(x73,x72)) % 105.80/105.80 [8]~E(x81,x82)+E(f4(x81),f4(x82)) % 105.80/105.80 % 105.80/105.80 %------------------------------------------- % 105.80/105.83 cnf(13,plain, % 105.80/105.83 (E(f4(x131),f1(f1(x132,x132),x131))), % 105.80/105.83 inference(scs_inference,[],[9,2])). % 105.80/105.83 cnf(14,plain, % 105.80/105.83 (E(f1(x141,f1(x142,f1(f1(f1(x143,x143),x144),f1(x141,x142)))),f4(x144))), % 105.80/105.83 inference(scs_inference,[],[9,11,2,3])). % 105.80/105.83 cnf(16,plain, % 105.80/105.83 (E(f4(x161),f1(x162,f1(x163,f1(f1(f1(x164,x164),x161),f1(x162,x163)))))), % 105.80/105.83 inference(scs_inference,[],[14,2])). % 105.80/105.84 cnf(17,plain, % 105.80/105.84 (~E(f5(f4(a2),a2),f1(f4(a3),f1(f1(x171,x171),a3)))), % 105.80/105.84 inference(scs_inference,[],[12,14,10,2,3])). % 105.80/105.84 cnf(19,plain, % 105.80/105.84 (E(f5(x191,x192),f1(x191,f1(f1(x193,x193),x192)))), % 105.80/105.84 inference(scs_inference,[],[10,2])). % 105.80/105.84 cnf(20,plain, % 105.80/105.84 (E(x201,f1(x202,f1(x203,f1(x201,f1(x202,x203)))))), % 105.80/105.84 inference(scs_inference,[],[11,2])). % 105.80/105.84 cnf(21,plain, % 105.80/105.84 (E(f1(f1(x211,x211),x212),f1(f1(x213,x213),x212))), % 105.80/105.84 inference(scs_inference,[],[9,13,3])). % 105.80/105.84 cnf(23,plain, % 105.80/105.84 (E(f5(f1(x231,x231),x232),f4(f1(f1(x233,x233),x232)))), % 105.80/105.84 inference(scs_inference,[],[9,19,3])). % 105.80/105.84 cnf(26,plain, % 105.80/105.84 (E(f4(f1(f1(x261,x261),x262)),f5(f1(x263,x263),x262))), % 105.80/105.84 inference(scs_inference,[],[9,19,3,2])). % 105.80/105.84 cnf(27,plain, % 105.80/105.84 (E(f1(f1(x271,x271),f1(f1(x272,x272),x273)),f5(f1(x274,x274),x273))), % 105.80/105.84 inference(scs_inference,[],[9,26,3])). % 105.80/105.84 cnf(29,plain, % 105.80/105.84 (E(f5(f1(x291,x291),x292),f1(f1(x293,x293),f1(f1(x294,x294),x292)))), % 105.80/105.84 inference(scs_inference,[],[9,26,3,2])). % 105.80/105.84 cnf(30,plain, % 105.80/105.84 (E(f4(f1(f1(x301,x301),x302)),f1(f1(x303,x303),f1(f1(x304,x304),x302)))), % 105.80/105.84 inference(scs_inference,[],[29,26,3])). % 105.80/105.84 cnf(32,plain, % 105.80/105.84 (E(f1(f1(x321,x321),f1(f1(x322,x322),x323)),f4(f1(f1(x324,x324),x323)))), % 105.80/105.84 inference(scs_inference,[],[29,26,3,2])). % 105.80/105.84 cnf(33,plain, % 105.80/105.84 (E(f1(f1(x331,x331),x332),f1(x333,f1(x334,f1(f4(x332),f1(x333,x334)))))), % 105.80/105.84 inference(scs_inference,[],[9,20,3])). % 105.80/105.84 cnf(35,plain, % 105.80/105.84 (E(f1(x351,f1(x352,f1(f4(x353),f1(x351,x352)))),f1(f1(x354,x354),x353))), % 105.80/105.84 inference(scs_inference,[],[9,20,3,2])). % 105.80/105.84 cnf(36,plain, % 105.80/105.84 (E(f4(f1(f1(x361,x361),x362)),f4(f1(f1(x363,x363),x362)))), % 105.80/105.84 inference(scs_inference,[],[26,23,3])). % 105.80/105.84 cnf(40,plain, % 105.80/105.84 (E(f4(x401),f5(f1(x402,x402),f1(f1(f1(x403,x403),x401),f1(f1(x404,x404),f1(x405,x405)))))), % 105.80/105.84 inference(scs_inference,[],[16,27,3])). % 105.80/105.84 cnf(43,plain, % 105.80/105.84 (E(f5(f1(x431,x431),f1(f1(f1(x432,x432),x433),f1(f1(x434,x434),f1(x435,x435)))),f4(x433))), % 105.80/105.84 inference(scs_inference,[],[40,2])). % 105.80/105.84 cnf(44,plain, % 105.80/105.84 (E(f5(x441,f1(f4(x442),f1(x441,f1(x443,x443)))),f1(f1(x444,x444),x442))), % 105.80/105.84 inference(scs_inference,[],[19,35,3])). % 105.80/105.84 cnf(48,plain, % 105.80/105.84 (E(f5(x481,f1(f1(f1(x482,x482),x483),f1(x481,f1(x484,x484)))),f4(x483))), % 105.80/105.84 inference(scs_inference,[],[19,14,3])). % 105.80/105.84 cnf(51,plain, % 105.80/105.84 (E(f4(x511),f5(x512,f1(f1(f1(x513,x513),x511),f1(x512,f1(x514,x514)))))), % 105.80/105.84 inference(scs_inference,[],[48,2])). % 105.80/105.84 cnf(52,plain, % 105.80/105.84 (E(f5(f1(x521,x521),x522),f5(f1(x523,x523),x522))), % 105.80/105.84 inference(scs_inference,[],[19,48,27,2,3])). % 105.80/105.84 cnf(55,plain, % 105.80/105.84 (E(x551,f5(f1(x552,x552),f1(x551,f1(f1(x553,x553),f1(x554,x554)))))), % 105.80/105.84 inference(scs_inference,[],[20,27,3])). % 105.80/105.84 cnf(58,plain, % 105.80/105.84 (E(f5(f1(x581,x581),f1(x582,f1(f1(x583,x583),f1(x584,x584)))),x582)), % 105.80/105.84 inference(scs_inference,[],[20,27,3,2])). % 105.80/105.84 cnf(63,plain, % 105.80/105.84 (E(f5(x631,f1(f4(x632),f1(x631,f1(x633,x633)))),f4(x632))), % 105.80/105.84 inference(scs_inference,[],[44,9,3])). % 105.80/105.84 cnf(66,plain, % 105.80/105.84 (~E(f5(f4(a2),a2),f5(f1(x661,x661),f1(f5(f4(a3),a3),f1(f1(x662,x662),f1(x663,x663)))))), % 105.80/105.84 inference(scs_inference,[],[58,12,3])). % 105.80/105.84 cnf(68,plain, % 105.80/105.84 (~E(f5(f4(a2),a2),f1(x681,f1(x682,f1(f5(f4(a3),a3),f1(x681,x682)))))), % 105.80/105.84 inference(scs_inference,[],[12,11,3])). % 105.80/105.84 cnf(70,plain, % 105.80/105.84 (~E(f5(f4(a2),a2),f5(x701,f1(f5(f4(a3),a3),f1(x701,f1(x702,x702)))))), % 105.80/105.84 inference(scs_inference,[],[19,68,3])). % 105.80/105.84 cnf(73,plain, % 105.80/105.84 (~E(a2,f1(f5(f4(a3),a3),f1(f4(a2),f1(x731,x731))))), % 105.80/105.84 inference(scs_inference,[],[19,68,3,7])). % 105.80/105.84 cnf(74,plain, % 105.80/105.84 (~E(a2,f1(f5(f4(a3),a3),f4(a2)))), % 105.80/105.84 inference(scs_inference,[],[20,73,3])). % 105.80/105.84 cnf(77,plain, % 105.80/105.84 (~E(a2,f5(f1(x771,x771),f1(f1(f5(f4(a3),a3),f4(a2)),f1(f1(x772,x772),f1(x773,x773)))))), % 105.80/105.84 inference(scs_inference,[],[74,58,3])). % 105.80/105.84 cnf(79,plain, % 105.80/105.84 (~E(a2,f1(x791,f1(x792,f1(f1(f5(f4(a3),a3),f4(a2)),f1(x791,x792)))))), % 105.80/105.84 inference(scs_inference,[],[74,11,3])). % 105.80/105.84 cnf(86,plain, % 105.80/105.84 (E(f5(x861,f1(f1(f1(x862,x862),x863),f1(x861,f1(x864,x864)))),f1(f1(x865,x865),x863))), % 105.80/105.84 inference(scs_inference,[],[9,51,3,2])). % 105.80/105.84 cnf(92,plain, % 105.80/105.84 (E(f5(f1(x921,x921),f1(f1(f1(x922,x922),x923),f1(f1(x924,x924),f1(x925,x925)))),f1(f1(x926,x926),x923))), % 105.80/105.84 inference(scs_inference,[],[9,40,3,2])). % 105.80/105.84 cnf(93,plain, % 105.80/105.84 (E(f4(f1(f1(x931,x931),x932)),f4(f4(x932)))), % 105.80/105.84 inference(scs_inference,[],[9,8])). % 105.80/105.84 cnf(94,plain, % 105.80/105.84 (E(f1(f1(f1(x941,x941),x942),x943),f1(f4(x942),x943))), % 105.80/105.84 inference(scs_inference,[],[9,8,4])). % 105.80/105.84 cnf(95,plain, % 105.80/105.84 (E(f1(x951,f1(f1(x952,x952),x953)),f1(x951,f4(x953)))), % 105.80/105.84 inference(scs_inference,[],[9,8,4,5])). % 105.80/105.84 cnf(96,plain, % 105.80/105.84 (E(f5(f1(f1(x961,x961),x962),x963),f5(f4(x962),x963))), % 105.80/105.84 inference(scs_inference,[],[9,8,4,5,6])). % 105.80/105.84 cnf(97,plain, % 105.80/105.84 (E(f5(x971,f1(f1(x972,x972),x973)),f5(x971,f4(x973)))), % 105.80/105.84 inference(scs_inference,[],[9,8,4,5,6,7])). % 105.80/105.84 cnf(98,plain, % 105.80/105.84 (~E(f1(f4(a3),f1(f1(x981,x981),a3)),f5(f4(a2),a2))), % 105.80/105.84 inference(scs_inference,[],[9,17,8,4,5,6,7,2])). % 105.80/105.84 cnf(101,plain, % 105.80/105.84 (E(f1(x1011,f1(f1(x1012,x1012),x1013)),f1(x1011,f1(f1(x1014,x1014),x1013)))), % 105.80/105.84 inference(scs_inference,[],[21,5])). % 105.80/105.84 cnf(103,plain, % 105.80/105.84 (E(f4(f5(f1(x1031,x1031),x1032)),f4(f5(f1(x1033,x1033),x1032)))), % 105.80/105.84 inference(scs_inference,[],[21,52,5,4,8])). % 105.80/105.84 cnf(105,plain, % 105.80/105.84 (E(f5(x1051,f1(f1(x1052,x1052),x1053)),f5(x1051,f1(f1(x1054,x1054),x1053)))), % 105.80/105.84 inference(scs_inference,[],[21,52,5,4,8,6,7])). % 105.80/105.84 cnf(106,plain, % 105.80/105.84 (~E(f5(f1(x1061,x1061),f1(f5(f4(a3),a3),f1(f1(x1062,x1062),f1(x1063,x1063)))),f5(f4(a2),a2))), % 105.80/105.84 inference(scs_inference,[],[21,52,66,5,4,8,6,7,2])). % 105.80/105.84 cnf(107,plain, % 105.80/105.84 (E(f1(f1(x1071,x1071),f1(f1(x1072,x1072),x1073)),f4(f4(x1073)))), % 105.80/105.84 inference(scs_inference,[],[9,21,52,93,66,5,4,8,6,7,2,3])). % 105.80/105.84 cnf(110,plain, % 105.80/105.84 (E(f4(f1(f1(f1(x1101,x1101),x1102),x1103)),f4(f1(f4(x1102),x1103)))), % 105.80/105.84 inference(scs_inference,[],[94,5,8])). % 105.80/105.84 cnf(112,plain, % 105.80/105.84 (E(f5(f1(f1(f1(x1121,x1121),x1122),x1123),x1124),f5(f1(f4(x1122),x1123),x1124))), % 105.80/105.84 inference(scs_inference,[],[94,5,8,4,6])). % 105.80/105.84 cnf(115,plain, % 105.80/105.84 (~E(f1(f4(a3),f4(a3)),f5(f4(a2),a2))), % 105.80/105.84 inference(scs_inference,[],[94,95,98,70,5,8,4,6,7,2,3])). % 105.80/105.84 cnf(123,plain, % 105.80/105.84 (~E(f5(f4(a2),a2),f1(f4(a3),f4(a3)))), % 105.80/105.84 inference(scs_inference,[],[115,96,4,8,5,6,7,2])). % 105.80/105.84 cnf(124,plain, % 105.80/105.84 (~E(f5(f4(f1(x1241,x1241)),f1(f5(f4(a3),a3),f1(f1(x1242,x1242),f1(x1243,x1243)))),f5(f4(a2),a2))), % 105.80/105.84 inference(scs_inference,[],[115,96,106,4,8,5,6,7,2,3])). % 105.80/105.84 cnf(132,plain, % 105.80/105.84 (~E(f5(f1(x1321,x1321),f1(f1(f5(f4(a3),a3),f4(a2)),f1(f1(x1322,x1322),f1(x1323,x1323)))),a2)), % 105.80/105.84 inference(scs_inference,[],[97,77,5,4,8,6,7,2])). % 105.80/105.84 cnf(136,plain, % 105.80/105.84 (E(f1(f1(f1(x1361,x1361),f1(f1(x1362,x1362),x1363)),x1364),f1(f4(f4(x1363)),x1364))), % 105.80/105.84 inference(scs_inference,[],[107,8,4])). % 105.80/105.84 cnf(138,plain, % 105.80/105.84 (E(f5(f1(f1(x1381,x1381),f1(f1(x1382,x1382),x1383)),x1384),f5(f4(f4(x1383)),x1384))), % 105.80/105.84 inference(scs_inference,[],[107,8,4,5,6])). % 105.80/105.84 cnf(139,plain, % 105.80/105.84 (E(f5(x1391,f1(f1(x1392,x1392),f1(f1(x1393,x1393),x1394))),f5(x1391,f4(f4(x1394))))), % 105.80/105.84 inference(scs_inference,[],[107,8,4,5,6,7])). % 105.80/105.84 cnf(144,plain, % 105.80/105.84 (E(f1(x1441,f4(x1442)),f1(x1441,f1(f1(x1443,x1443),x1442)))), % 105.80/105.84 inference(scs_inference,[],[13,5])). % 105.80/105.84 cnf(145,plain, % 105.80/105.84 (E(f4(f4(x1451)),f4(f1(f1(x1452,x1452),x1451)))), % 105.80/105.84 inference(scs_inference,[],[13,5,8])). % 105.80/105.84 cnf(146,plain, % 105.80/105.84 (E(f1(f4(x1461),x1462),f1(f1(f1(x1463,x1463),x1461),x1462))), % 105.80/105.84 inference(scs_inference,[],[13,5,8,4])). % 105.80/105.84 cnf(147,plain, % 105.80/105.84 (E(f5(f4(x1471),x1472),f5(f1(f1(x1473,x1473),x1471),x1472))), % 105.80/105.84 inference(scs_inference,[],[13,5,8,4,6])). % 105.80/105.84 cnf(148,plain, % 105.80/105.84 (E(f5(x1481,f4(x1482)),f5(x1481,f1(f1(x1483,x1483),x1482)))), % 105.80/105.84 inference(scs_inference,[],[13,5,8,4,6,7])). % 105.80/105.84 cnf(149,plain, % 105.80/105.84 (~E(f1(f5(f4(a3),a3),f1(f4(a2),f1(x1491,x1491))),a2)), % 105.80/105.84 inference(scs_inference,[],[13,73,5,8,4,6,7,2])). % 105.80/105.84 cnf(150,plain, % 105.80/105.84 (~E(f5(f1(x1501,x1501),f1(f1(f4(a3),f4(a3)),f1(f1(x1502,x1502),f1(x1503,x1503)))),f5(f4(a2),a2))), % 105.80/105.84 inference(scs_inference,[],[13,115,73,55,5,8,4,6,7,2,3])). % 105.80/105.84 cnf(153,plain, % 105.80/105.84 (E(f4(f1(x1531,f4(x1532))),f4(f1(x1531,f1(f1(x1533,x1533),x1532))))), % 105.80/105.84 inference(scs_inference,[],[144,4,8])). % 105.80/105.84 cnf(155,plain, % 105.80/105.84 (E(f5(f1(x1551,f4(x1552)),x1553),f5(f1(x1551,f1(f1(x1554,x1554),x1552)),x1553))), % 105.80/105.84 inference(scs_inference,[],[144,4,8,5,6])). % 105.80/105.84 cnf(158,plain, % 105.80/105.84 (~E(f1(f1(f1(x1581,x1581),a3),f1(f1(x1582,x1582),a3)),f5(f4(a2),a2))), % 105.80/105.84 inference(scs_inference,[],[144,146,98,68,4,8,5,6,7,2,3])). % 105.80/105.84 cnf(161,plain, % 105.80/105.84 (E(f1(f4(f4(x1611)),x1612),f1(f4(f1(f1(x1613,x1613),x1611)),x1612))), % 105.80/105.84 inference(scs_inference,[],[145,5,4])). % 105.80/105.84 cnf(162,plain, % 105.80/105.84 (E(f4(f4(f4(x1621))),f4(f4(f1(f1(x1622,x1622),x1621))))), % 105.80/105.84 inference(scs_inference,[],[145,5,4,8])). % 105.80/105.84 cnf(163,plain, % 105.80/105.84 (E(f5(f4(f4(x1631)),x1632),f5(f4(f1(f1(x1633,x1633),x1631)),x1632))), % 105.80/105.84 inference(scs_inference,[],[145,5,4,8,6])). % 105.80/105.84 cnf(165,plain, % 105.80/105.84 (~E(f5(f4(a2),a2),f1(f1(f1(x1651,x1651),a3),f1(f1(x1652,x1652),a3)))), % 105.80/105.84 inference(scs_inference,[],[145,158,5,4,8,6,7,2])). % 105.80/105.84 cnf(175,plain, % 105.80/105.84 (~E(f5(f1(x1751,x1751),f1(f1(x1752,x1752),f1(f1(x1753,x1753),f1(x1754,x1754)))),f5(f4(a2),a2))), % 105.80/105.84 inference(scs_inference,[],[148,105,150,79,8,4,5,6,7,2,3])). % 105.80/105.84 cnf(182,plain, % 105.80/105.84 (~E(f1(f5(f4(a3),a3),f4(a2)),a2)), % 105.80/105.84 inference(scs_inference,[],[52,93,74,5,8,4,6,7,2])). % 105.80/105.84 cnf(183,plain, % 105.80/105.84 (~E(f5(f1(f1(x1831,x1831),a2),a2),f1(f1(f1(x1832,x1832),a3),f1(f1(x1833,x1833),a3)))), % 105.80/105.84 inference(scs_inference,[],[165,52,93,147,74,5,8,4,6,7,2,3])). % 105.80/105.84 cnf(185,plain, % 105.80/105.84 (E(f1(f1(x1851,f1(f1(x1852,x1852),x1853)),x1854),f1(f5(x1851,x1853),x1854))), % 105.80/105.84 inference(scs_inference,[],[10,4])). % 105.80/105.84 cnf(186,plain, % 105.80/105.84 (E(f1(x1861,f1(x1862,f1(f1(x1863,x1863),x1864))),f1(x1861,f5(x1862,x1864)))), % 105.80/105.84 inference(scs_inference,[],[10,4,5])). % 105.80/105.84 cnf(187,plain, % 105.80/105.84 (E(f4(f1(x1871,f1(f1(x1872,x1872),x1873))),f4(f5(x1871,x1873)))), % 105.80/105.84 inference(scs_inference,[],[10,4,5,8])). % 105.80/105.84 cnf(189,plain, % 105.80/105.84 (E(f5(x1891,f1(x1892,f1(f1(x1893,x1893),x1894))),f5(x1891,f5(x1892,x1894)))), % 105.80/105.84 inference(scs_inference,[],[10,4,5,8,6,7])). % 105.80/105.84 cnf(190,plain, % 105.80/105.84 (~E(f1(f1(f1(x1901,x1901),a3),f1(f1(x1902,x1902),a3)),f5(f1(f1(x1903,x1903),a2),a2))), % 105.80/105.84 inference(scs_inference,[],[10,183,4,5,8,6,7,2])). % 105.80/105.84 cnf(191,plain, % 105.80/105.84 (~E(f4(f1(x1911,x1911)),f5(f4(a2),a2))), % 105.80/105.84 inference(scs_inference,[],[10,43,175,183,4,5,8,6,7,2,3])). % 105.80/105.84 cnf(194,plain, % 105.80/105.84 (E(f4(f1(x1941,f1(f1(x1942,x1942),x1943))),f4(f1(x1941,f4(x1943))))), % 105.80/105.84 inference(scs_inference,[],[95,8])). % 105.80/105.84 cnf(195,plain, % 105.80/105.84 (E(f1(f1(x1951,f1(f1(x1952,x1952),x1953)),x1954),f1(f1(x1951,f4(x1953)),x1954))), % 105.80/105.84 inference(scs_inference,[],[95,8,4])). % 105.80/105.84 cnf(197,plain, % 105.80/105.84 (E(f5(f1(x1971,f1(f1(x1972,x1972),x1973)),x1974),f5(f1(x1971,f4(x1973)),x1974))), % 105.80/105.84 inference(scs_inference,[],[95,8,4,5,6])). % 105.80/105.84 cnf(198,plain, % 105.80/105.84 (E(f5(x1981,f1(x1982,f1(f1(x1983,x1983),x1984))),f5(x1981,f1(x1982,f4(x1984))))), % 105.80/105.84 inference(scs_inference,[],[95,8,4,5,6,7])). % 105.80/105.84 cnf(199,plain, % 105.80/105.84 (~E(f5(f4(a2),a2),f4(f1(x1991,x1991)))), % 105.80/105.84 inference(scs_inference,[],[191,95,8,4,5,6,7,2])). % 105.80/105.84 cnf(200,plain, % 105.80/105.84 (~E(f4(f1(f1(x2001,x2001),f1(x2002,x2002))),f5(f4(a2),a2))), % 105.80/105.84 inference(scs_inference,[],[191,36,95,8,4,5,6,7,2,3])). % 105.80/105.84 cnf(205,plain, % 105.80/105.84 (E(f1(f5(f1(x2051,x2051),x2052),x2053),f1(f4(f1(f1(x2054,x2054),x2052)),x2053))), % 105.80/105.84 inference(scs_inference,[],[23,5,8,4])). % 105.80/105.84 cnf(208,plain, % 105.80/105.84 (~E(f5(f4(a2),a2),f4(f1(f1(x2081,x2081),f1(x2082,x2082))))), % 105.80/105.84 inference(scs_inference,[],[200,23,5,8,4,6,7,2])). % 105.80/105.84 cnf(209,plain, % 105.80/105.84 (~E(f5(f1(f1(x2091,x2091),a3),a3),f5(f1(f1(x2092,x2092),a2),a2))), % 105.80/105.85 inference(scs_inference,[],[10,200,190,23,5,8,4,6,7,2,3])). % 105.80/105.85 cnf(212,plain, % 105.80/105.85 (E(f1(x2121,f1(f4(x2122),x2123)),f1(x2121,f1(f1(f1(x2124,x2124),x2122),x2123)))), % 105.80/105.85 inference(scs_inference,[],[146,4,5])). % 105.80/105.85 cnf(214,plain, % 105.80/105.85 (E(f5(f1(f4(x2141),x2142),x2143),f5(f1(f1(f1(x2144,x2144),x2141),x2142),x2143))), % 105.80/105.85 inference(scs_inference,[],[146,4,5,8,6])). % 105.80/105.85 cnf(216,plain, % 105.80/105.85 (~E(f5(f1(f1(x2161,x2161),a2),a2),f5(f1(f1(x2162,x2162),a3),a3))), % 105.80/105.85 inference(scs_inference,[],[209,146,4,5,8,6,7,2])). % 105.80/105.85 cnf(217,plain, % 105.80/105.85 (~E(f5(f1(f1(x2171,x2171),a2),a2),f4(f1(x2172,x2172)))), % 105.80/105.85 inference(scs_inference,[],[199,209,146,147,4,5,8,6,7,2,3])). % 105.80/105.85 cnf(219,plain, % 105.80/105.85 (E(f4(f5(f1(x2191,x2191),x2192)),f4(f1(f1(x2193,x2193),f1(f1(x2194,x2194),x2192))))), % 105.80/105.85 inference(scs_inference,[],[29,8])). % 105.80/105.85 cnf(220,plain, % 105.80/105.85 (E(f1(f4(f1(f1(x2201,x2201),x2202)),x2203),f1(f4(f4(x2202)),x2203))), % 105.80/105.85 inference(scs_inference,[],[93,29,8,4])). % 105.80/105.85 cnf(222,plain, % 105.80/105.85 (E(f5(f4(f1(f1(x2221,x2221),x2222)),x2223),f5(f4(f4(x2222)),x2223))), % 105.80/105.85 inference(scs_inference,[],[93,29,8,4,5,6])). % 105.80/105.85 cnf(224,plain, % 105.80/105.85 (~E(f4(f1(x2241,x2241)),f5(f1(f1(x2242,x2242),a2),a2))), % 105.80/105.85 inference(scs_inference,[],[217,93,29,8,4,5,6,7,2])). % 105.80/105.85 cnf(225,plain, % 105.80/105.85 (~E(f1(f5(f4(a3),a3),f5(f4(a2),f1(x2251,x2251))),a2)), % 105.80/105.85 inference(scs_inference,[],[217,149,186,93,29,8,4,5,6,7,2,3])). % 105.80/105.85 cnf(228,plain, % 105.80/105.85 (E(f1(x2281,f4(f1(f1(x2282,x2282),x2283))),f1(x2281,f5(f1(x2284,x2284),x2283)))), % 105.80/105.85 inference(scs_inference,[],[26,5])). % 105.80/105.85 cnf(229,plain, % 105.80/105.85 (E(f4(f4(f1(f1(x2291,x2291),x2292))),f4(f5(f1(x2293,x2293),x2292)))), % 105.80/105.85 inference(scs_inference,[],[26,5,8])). % 105.80/105.85 cnf(231,plain, % 105.80/105.85 (E(f5(f4(f1(f1(x2311,x2311),x2312)),x2313),f5(f5(f1(x2314,x2314),x2312),x2313))), % 105.80/105.85 inference(scs_inference,[],[26,5,8,4,6])). % 105.80/105.85 cnf(234,plain, % 105.80/105.85 (~E(f5(f1(f1(x2341,x2341),a2),a2),f4(f1(f1(x2342,x2342),f1(x2343,x2343))))), % 105.80/105.85 inference(scs_inference,[],[208,225,26,147,5,8,4,6,7,2,3])). % 105.80/105.85 cnf(236,plain, % 105.80/105.85 (E(f1(f1(f1(x2361,x2361),f1(f1(x2362,x2362),x2363)),x2364),f1(f5(f1(x2365,x2365),x2363),x2364))), % 105.80/105.85 inference(scs_inference,[],[27,4])). % 105.80/105.85 cnf(238,plain, % 105.80/105.85 (E(f4(f1(f1(x2381,x2381),f1(f1(x2382,x2382),x2383))),f4(f5(f1(x2384,x2384),x2383)))), % 105.80/105.85 inference(scs_inference,[],[27,4,5,8])). % 105.80/105.85 cnf(240,plain, % 105.80/105.85 (E(f5(x2401,f1(f1(x2402,x2402),f1(f1(x2403,x2403),x2404))),f5(x2401,f5(f1(x2405,x2405),x2404)))), % 105.80/105.85 inference(scs_inference,[],[27,4,5,8,6,7])). % 105.80/105.85 cnf(241,plain, % 105.80/105.85 (~E(f4(f1(f1(x2411,x2411),f1(x2412,x2412))),f5(f1(f1(x2413,x2413),a2),a2))), % 105.80/105.85 inference(scs_inference,[],[234,27,4,5,8,6,7,2])). % 105.80/105.85 cnf(242,plain, % 105.80/105.85 (~E(f4(f5(f1(f1(x2421,x2421),x2422),x2422)),f5(f1(f1(x2423,x2423),a2),a2))), % 105.80/105.85 inference(scs_inference,[],[224,234,187,27,4,5,8,6,7,2,3])). % 105.80/105.85 cnf(246,plain, % 105.80/105.85 (E(f1(f5(f1(x2461,x2461),x2462),x2463),f1(f1(f1(x2464,x2464),f1(f1(x2465,x2465),x2462)),x2463))), % 105.80/105.85 inference(scs_inference,[],[29,147,8,4])). % 105.80/105.85 cnf(248,plain, % 105.80/105.85 (E(f5(f5(f1(x2481,x2481),x2482),x2483),f5(f1(f1(x2484,x2484),f1(f1(x2485,x2485),x2482)),x2483))), % 105.80/105.85 inference(scs_inference,[],[29,147,8,4,5,6])). % 105.80/105.85 cnf(249,plain, % 105.80/105.85 (E(f5(x2491,f5(f1(x2492,x2492),x2493)),f5(x2491,f1(f1(x2494,x2494),f1(f1(x2495,x2495),x2493))))), % 105.80/105.85 inference(scs_inference,[],[29,147,8,4,5,6,7])). % 105.80/105.85 cnf(251,plain, % 105.80/105.85 (~E(f5(f1(f4(f1(x2511,x2511)),a2),a2),f5(f1(f1(x2512,x2512),a3),a3))), % 105.80/105.85 inference(scs_inference,[],[216,112,242,29,147,8,4,5,6,7,2,3])). % 105.80/105.85 cnf(255,plain, % 105.80/105.85 (E(f4(f5(x2551,x2552)),f4(f1(x2551,f1(f1(x2553,x2553),x2552))))), % 105.80/105.85 inference(scs_inference,[],[147,19,5,8])). % 105.80/105.85 cnf(256,plain, % 105.80/105.85 (E(f1(f5(f4(x2561),x2562),x2563),f1(f5(f1(f1(x2564,x2564),x2561),x2562),x2563))), % 105.80/105.85 inference(scs_inference,[],[147,19,5,8,4])). % 105.80/105.85 cnf(260,plain, % 105.80/105.85 (~E(f4(f5(f1(x2601,x2601),f1(x2602,x2602))),f5(f1(f1(x2603,x2603),a2),a2))), % 105.80/105.85 inference(scs_inference,[],[103,251,242,147,19,5,8,4,6,7,2,3])). % 105.80/105.85 cnf(263,plain, % 105.80/105.85 (E(f1(f5(x2631,x2632),x2633),f1(f1(x2631,f1(f1(x2634,x2634),x2632)),x2633))), % 105.80/105.85 inference(scs_inference,[],[19,4])). % 105.80/105.85 cnf(264,plain, % 105.80/105.85 (E(f1(x2641,f5(x2642,x2643)),f1(x2641,f1(x2642,f1(f1(x2644,x2644),x2643))))), % 105.80/105.85 inference(scs_inference,[],[19,4,5])). % 105.80/105.85 cnf(267,plain, % 105.80/105.85 (~E(f5(f1(f1(x2671,x2671),a2),a2),f4(f5(f1(x2672,x2672),f1(x2673,x2673))))), % 105.80/105.85 inference(scs_inference,[],[260,19,4,5,6,7,2])). % 105.80/105.85 cnf(268,plain, % 105.80/105.85 (~E(f1(f5(f1(f1(x2681,x2681),a3),a3),f4(a2)),a2)), % 105.80/105.85 inference(scs_inference,[],[182,260,256,19,4,5,6,7,2,3])). % 105.80/105.85 cnf(271,plain, % 105.80/105.85 (~E(f5(f1(x2711,x2711),f5(f1(f5(f4(a3),a3),f4(a2)),f1(x2712,x2712))),a2)), % 105.80/105.85 inference(scs_inference,[],[268,189,132,2,3])). % 105.80/105.85 cnf(273,plain, % 105.80/105.85 (~E(a2,f5(f1(x2731,x2731),f5(f1(f5(f4(a3),a3),f4(a2)),f1(x2732,x2732))))), % 105.80/105.85 inference(scs_inference,[],[271,2])). % 105.80/105.85 cnf(280,plain, % 105.80/105.85 (~E(f5(f4(f1(x2801,x2801)),f1(f5(f4(a3),a3),f4(f1(x2802,x2802)))),f5(f4(a2),a2))), % 105.80/105.85 inference(scs_inference,[],[124,198,3])). % 105.80/105.85 cnf(284,plain, % 105.80/105.85 (~E(f4(f1(f1(x2841,x2841),f1(f1(x2842,x2842),f1(x2843,x2843)))),f5(f1(f1(x2844,x2844),a2),a2))), % 105.80/105.85 inference(scs_inference,[],[255,280,260,2,3])). % 105.80/105.85 cnf(286,plain, % 105.80/105.85 (~E(f5(f1(f1(x2861,x2861),a2),a2),f4(f1(f1(x2862,x2862),f1(f1(x2863,x2863),f1(x2864,x2864)))))), % 105.80/105.85 inference(scs_inference,[],[284,2])). % 105.80/105.85 cnf(287,plain, % 105.80/105.85 (~E(f1(x2871,f1(x2872,f1(f5(f4(a2),a2),f1(x2871,x2872)))),f1(f4(a3),f4(a3)))), % 105.80/105.85 inference(scs_inference,[],[284,123,20,2,3])). % 105.80/105.85 cnf(289,plain, % 105.80/105.85 (~E(f1(f4(a3),f4(a3)),f1(x2891,f1(x2892,f1(f5(f4(a2),a2),f1(x2891,x2892)))))), % 105.80/105.85 inference(scs_inference,[],[287,2])). % 105.80/105.85 cnf(290,plain, % 105.80/105.85 (~E(f1(f5(f4(a3),a3),f1(f4(a2),f1(f1(x2901,x2901),f1(x2902,x2902)))),a2)), % 105.80/105.85 inference(scs_inference,[],[264,287,225,2,3])). % 105.80/105.85 cnf(293,plain, % 105.80/105.85 (~E(f1(f1(f4(a3),f1(f1(x2931,x2931),a3)),f1(f4(a2),f1(f1(x2932,x2932),f1(x2933,x2933)))),a2)), % 105.80/105.85 inference(scs_inference,[],[263,290,2,3])). % 105.80/105.85 cnf(296,plain, % 105.80/105.85 (~E(f1(f1(x2961,x2961),f1(x2962,x2962)),f5(f4(a2),a2))), % 105.80/105.85 inference(scs_inference,[],[86,293,175,2,3])). % 105.80/105.85 cnf(300,plain, % 105.80/105.85 (~E(f1(f1(f4(a3),f1(f1(x3001,x3001),a3)),f4(a2)),a2)), % 105.80/105.85 inference(scs_inference,[],[296,182,263,2,3])). % 105.80/105.85 cnf(303,plain, % 105.80/105.85 (~E(f4(f1(f4(f1(x3031,x3031)),f1(x3032,x3032))),f5(f1(f1(x3033,x3033),a2),a2))), % 105.80/105.85 inference(scs_inference,[],[300,241,110,2,3])). % 105.80/105.85 cnf(307,plain, % 105.80/105.85 (~E(f4(a3),f1(x3071,f1(f5(f4(a2),a2),f1(f4(a3),x3071))))), % 105.80/105.85 inference(scs_inference,[],[303,289,2,5])). % 105.80/105.85 cnf(312,plain, % 105.80/105.85 (~E(f1(f1(x3121,x3121),a3),f1(x3122,f1(f5(f4(a2),a2),f1(f4(a3),x3122))))), % 105.80/105.85 inference(scs_inference,[],[13,307,2,3])). % 105.80/105.85 cnf(314,plain, % 105.80/105.85 (~E(f1(x3141,f1(f5(f4(a2),a2),f1(f4(a3),x3141))),f1(f1(x3142,x3142),a3))), % 105.80/105.85 inference(scs_inference,[],[312,2])). % 105.80/105.85 cnf(315,plain, % 105.80/105.85 (~E(f1(x3151,f1(x3152,f1(f5(f4(a2),a2),f1(x3151,x3152)))),f4(f1(x3153,x3153)))), % 105.80/105.85 inference(scs_inference,[],[312,199,20,2,3])). % 105.80/105.85 cnf(317,plain, % 105.80/105.85 (~E(f4(f1(x3171,x3171)),f1(x3172,f1(x3173,f1(f5(f4(a2),a2),f1(x3172,x3173)))))), % 105.80/105.85 inference(scs_inference,[],[315,2])). % 105.80/105.85 cnf(318,plain, % 105.80/105.85 (~E(f1(f1(x3181,x3181),f1(f1(x3182,x3182),f1(x3183,x3183))),f5(f4(a2),a2))), % 105.80/105.85 inference(scs_inference,[],[13,315,200,2,3])). % 105.80/105.85 cnf(320,plain, % 105.80/105.85 (~E(f5(f4(a2),a2),f1(f1(x3201,x3201),f1(f1(x3202,x3202),f1(x3203,x3203))))), % 105.80/105.85 inference(scs_inference,[],[318,2])). % 105.80/105.85 cnf(321,plain, % 105.80/105.85 (~E(f1(f1(x3211,x3211),f1(x3212,x3212)),f1(x3213,f1(x3214,f1(f5(f4(a2),a2),f1(x3213,x3214)))))), % 105.80/105.85 inference(scs_inference,[],[13,318,317,2,3])). % 105.80/105.85 cnf(323,plain, % 105.80/105.85 (~E(f1(f5(f4(a2),a2),f1(f4(a3),f1(x3231,x3231))),a3)), % 105.80/105.85 inference(scs_inference,[],[13,318,314,317,2,3,5])). % 105.80/105.85 cnf(325,plain, % 105.80/105.85 (~E(a3,f1(f5(f4(a2),a2),f1(f4(a3),f1(x3251,x3251))))), % 105.80/105.85 inference(scs_inference,[],[323,2])). % 105.80/105.85 cnf(326,plain, % 105.80/105.85 (~E(f1(f1(x3261,x3261),f1(x3262,x3262)),f5(f1(f1(x3263,x3263),a2),a2))), % 105.80/105.85 inference(scs_inference,[],[13,323,224,2,3])). % 105.80/105.85 cnf(333,plain, % 105.80/105.85 (~E(f1(f1(x3331,x3331),f1(f1(x3332,x3332),f1(x3333,x3333))),f5(f1(f1(x3334,x3334),a2),a2))), % 105.80/105.85 inference(scs_inference,[],[13,326,241,2,3])). % 105.80/105.85 cnf(336,plain, % 105.80/105.85 (~E(f1(f5(f4(a2),a2),f1(f1(f1(x3361,x3361),a3),f1(x3362,x3362))),a3)), % 105.80/105.85 inference(scs_inference,[],[136,212,323,2,3])). % 105.80/105.85 cnf(338,plain, % 105.80/105.85 (~E(f1(x3381,x3381),f1(x3382,f1(f5(f4(a2),a2),f1(f1(x3383,x3383),x3382))))), % 105.80/105.85 inference(scs_inference,[],[321,136,212,323,2,3,5])). % 105.80/105.85 cnf(340,plain, % 105.80/105.85 (~E(f1(f5(f4(a2),a2),f1(f1(x3401,x3401),x3402)),x3402)), % 105.80/105.85 inference(scs_inference,[],[321,136,212,323,2,3,5,4])). % 105.80/105.85 cnf(342,plain, % 105.80/105.85 (~E(f1(f1(x3421,x3421),f1(f4(f1(x3422,x3422)),f1(x3423,x3423))),f5(f1(f1(x3424,x3424),a2),a2))), % 105.80/105.85 inference(scs_inference,[],[13,340,303,2,3])). % 105.80/105.85 cnf(352,plain, % 105.80/105.85 (~E(f4(f4(f1(x3521,x3521))),f5(f1(f1(x3522,x3522),a2),a2))), % 105.80/105.85 inference(scs_inference,[],[14,342,138,2,3])). % 105.80/105.85 cnf(358,plain, % 105.80/105.85 (~E(f1(f5(f1(f1(x3581,x3581),x3582),x3582),f1(f1(x3583,x3583),f1(x3584,x3584))),f5(f1(f1(x3585,x3585),a2),a2))), % 105.80/105.85 inference(scs_inference,[],[336,333,185,2,3])). % 105.80/105.85 cnf(361,plain, % 105.80/105.85 (E(f5(x3611,f4(f4(x3612))),f5(x3611,f1(f1(x3613,x3613),f1(f1(x3614,x3614),x3612))))), % 105.80/105.85 inference(scs_inference,[],[139,2])). % 105.80/105.85 cnf(365,plain, % 105.80/105.85 (~E(f5(f1(f1(x3651,x3651),a2),a2),f4(f4(f1(x3652,x3652))))), % 105.80/105.85 inference(scs_inference,[],[352,2])). % 105.80/105.85 cnf(382,plain, % 105.80/105.85 (~E(f5(f1(f4(f1(x3821,x3821)),a2),a2),f4(f5(f1(x3822,x3822),f1(x3823,x3823))))), % 105.80/105.85 inference(scs_inference,[],[267,112,3])). % 105.80/105.85 cnf(388,plain, % 105.80/105.85 (~E(f5(f1(f4(f1(x3881,x3881)),a2),a2),f4(f4(f1(x3882,x3882))))), % 105.80/105.85 inference(scs_inference,[],[365,112,3])). % 105.80/105.85 cnf(405,plain, % 105.80/105.85 (~E(f1(x4051,f1(f5(f4(a2),a2),f1(f1(x4052,x4052),x4051))),f1(x4053,x4053))), % 105.80/105.85 inference(scs_inference,[],[338,382,214,3,2])). % 105.80/105.85 cnf(406,plain, % 105.80/105.85 (~E(f1(x4061,f5(f5(f4(a2),a2),x4061)),f1(x4062,x4062))), % 105.80/105.85 inference(scs_inference,[],[405,186,3])). % 105.80/105.85 cnf(408,plain, % 105.80/105.85 (~E(x4081,f5(f5(f4(a2),a2),x4081))), % 105.80/105.85 inference(scs_inference,[],[405,186,3,4])). % 105.80/105.85 cnf(411,plain, % 105.80/105.85 (~E(f5(f5(f4(a2),a2),x4111),x4111)), % 105.80/105.85 inference(scs_inference,[],[16,408,406,3,5])). % 105.80/105.85 cnf(413,plain, % 105.80/105.85 (~E(f4(x4131),f1(f4(x4131),f1(f5(f4(a2),a2),f1(x4132,x4132))))), % 105.80/105.85 inference(scs_inference,[],[411,63,3])). % 105.80/105.85 cnf(418,plain, % 105.80/105.85 (~E(f1(f4(x4181),f1(f5(f4(a2),a2),f1(x4182,x4182))),f4(x4181))), % 105.80/105.85 inference(scs_inference,[],[413,388,214,3,2])). % 105.80/105.85 cnf(419,plain, % 105.80/105.85 (~E(f1(f4(f4(x4191)),f1(f5(f4(a2),a2),f1(x4192,x4192))),f4(f1(f1(x4193,x4193),x4191)))), % 105.80/105.85 inference(scs_inference,[],[418,220,3])). % 105.80/105.85 cnf(438,plain, % 105.80/105.85 (~E(f1(f1(f4(a3),f4(a3)),f4(a2)),a2)), % 105.80/105.85 inference(scs_inference,[],[195,300,3])). % 105.80/105.85 cnf(442,plain, % 105.80/105.85 (~E(f1(x4421,f1(x4422,f1(f4(f4(a2)),f1(x4421,x4422)))),a2)), % 105.80/105.85 inference(scs_inference,[],[438,33,3])). % 105.80/105.85 cnf(463,plain, % 105.80/105.85 (~E(a2,f1(x4631,f1(x4632,f1(f4(f4(a2)),f1(x4631,x4632)))))), % 105.80/105.85 inference(scs_inference,[],[19,320,442,3,2])). % 105.80/105.85 cnf(485,plain, % 105.80/105.85 (~E(f1(f1(f1(x4851,x4851),a2),f1(f1(x4852,x4852),a2)),f4(f1(x4853,x4853)))), % 105.80/105.85 inference(scs_inference,[],[19,217,3])). % 105.80/105.85 cnf(487,plain, % 105.80/105.85 (~E(f4(f1(x4871,x4871)),f1(f1(f1(x4872,x4872),a2),f1(f1(x4873,x4873),a2)))), % 105.80/105.85 inference(scs_inference,[],[485,2])). % 105.80/105.85 cnf(488,plain, % 105.80/105.85 (E(f1(x4881,f1(f1(x4882,x4882),x4883)),f1(x4884,f1(x4885,f1(f5(x4881,x4883),f1(x4884,x4885)))))), % 105.80/105.85 inference(scs_inference,[],[20,485,10,2,3])). % 105.80/105.85 cnf(491,plain, % 105.80/105.85 (~E(a3,f1(f5(f4(a2),a2),f4(a3)))), % 105.80/105.85 inference(scs_inference,[],[20,325,488,2,3])). % 105.80/105.85 cnf(495,plain, % 105.80/105.85 (~E(f1(x4951,f1(x4952,f1(a3,f1(x4951,x4952)))),f1(f5(f4(a2),a2),f4(a3)))), % 105.80/105.85 inference(scs_inference,[],[20,491,2,3])). % 105.80/105.85 cnf(497,plain, % 105.80/105.85 (E(f5(x4971,x4972),f1(x4973,f1(x4974,f1(f1(x4971,f1(f1(x4975,x4975),x4972)),f1(x4973,x4974)))))), % 105.80/105.85 inference(scs_inference,[],[20,19,3])). % 105.80/105.85 cnf(499,plain, % 105.80/105.85 (E(f1(x4991,f1(x4992,f1(f1(x4993,f1(f1(x4994,x4994),x4995)),f1(x4991,x4992)))),f5(x4993,x4995))), % 105.80/105.85 inference(scs_inference,[],[497,2])). % 105.80/105.85 cnf(517,plain, % 105.80/105.85 (E(f1(f1(x5171,x5171),f4(f1(f1(x5172,x5172),x5173))),f1(f1(x5174,x5174),f5(f1(x5175,x5175),x5173)))), % 105.80/105.85 inference(scs_inference,[],[21,495,228,2,3])). % 105.80/105.85 cnf(521,plain, % 105.80/105.85 (~E(a2,f5(f1(f4(x5211),f1(f1(x5212,x5212),x5211)),f5(f1(f5(f4(a3),a3),f4(a2)),f1(x5213,x5213))))), % 105.80/105.85 inference(scs_inference,[],[273,197,517,2,3])). % 105.80/105.85 cnf(524,plain, % 105.80/105.85 (~E(f4(f1(f1(x5241,x5241),x5242)),f1(f4(f4(x5242)),f1(f5(f4(a2),a2),f1(x5243,x5243))))), % 105.80/105.85 inference(scs_inference,[],[419,2])). % 105.80/105.85 cnf(561,plain, % 105.80/105.85 (E(f5(f1(f1(f1(x5611,x5611),x5612),f4(x5612)),x5613),f4(f1(f1(x5614,x5614),x5613)))), % 105.80/105.85 inference(scs_inference,[],[23,155,3])). % 105.80/105.85 cnf(564,plain, % 105.80/105.85 (E(f4(f1(f1(x5641,x5641),x5642)),f5(f1(f1(f1(x5643,x5643),x5644),f4(x5644)),x5642))), % 105.80/105.85 inference(scs_inference,[],[561,2])). % 105.80/105.85 cnf(565,plain, % 105.80/105.85 (~E(f5(f1(f1(x5651,x5651),a2),a2),f5(f1(x5652,x5652),f1(f1(x5653,x5653),f1(x5654,x5654))))), % 105.80/105.85 inference(scs_inference,[],[23,561,286,2,3])). % 105.80/105.85 cnf(571,plain, % 105.80/105.85 (E(f5(f5(f1(x5711,x5711),f1(x5712,x5712)),x5713),f4(f1(f1(x5714,x5714),x5713)))), % 105.80/105.85 inference(scs_inference,[],[23,248,3])). % 105.80/105.85 cnf(574,plain, % 105.80/105.85 (E(f4(f1(f1(x5741,x5741),x5742)),f5(f5(f1(x5743,x5743),f1(x5744,x5744)),x5742))), % 105.80/105.85 inference(scs_inference,[],[23,248,3,2])). % 105.80/105.85 cnf(576,plain, % 105.80/105.85 (~E(f5(f4(a2),a2),f5(f1(x5761,x5761),f1(x5762,x5762)))), % 105.80/105.85 inference(scs_inference,[],[23,565,208,2,3])). % 105.80/105.85 cnf(578,plain, % 105.80/105.85 (~E(f5(f5(f1(x5781,x5781),f1(x5782,x5782)),f1(x5783,x5783)),f1(f1(f1(x5784,x5784),a2),f1(f1(x5785,x5785),a2)))), % 105.80/105.85 inference(scs_inference,[],[487,574,3])). % 105.80/105.85 cnf(581,plain, % 105.80/105.85 (E(f5(f4(f1(f1(x5811,x5811),f1(x5812,x5812))),x5813),f4(f1(f1(x5814,x5814),x5813)))), % 105.80/105.85 inference(scs_inference,[],[571,231,3])). % 105.80/105.85 cnf(583,plain, % 105.80/105.85 (E(f4(f1(f1(x5831,x5831),x5832)),f5(f4(f1(f1(x5833,x5833),f1(x5834,x5834))),x5832))), % 105.80/105.85 inference(scs_inference,[],[571,231,3,2])). % 105.80/105.85 cnf(584,plain, % 105.80/105.85 (~E(f5(f1(x5841,x5841),f1(x5842,x5842)),f5(f4(a2),a2))), % 105.80/105.85 inference(scs_inference,[],[576,2])). % 105.80/105.85 cnf(588,plain, % 105.80/105.85 (~E(f5(f5(f1(x5881,x5881),f1(x5882,x5882)),f1(x5883,x5883)),f1(f1(f1(x5884,x5884),a2),f1(f1(x5885,x5885),a2)))), % 105.80/105.85 inference(rename_variables,[],[578])). % 105.80/105.85 cnf(590,plain, % 105.80/105.85 (~E(f1(f1(f1(x5901,x5901),a2),f1(f1(x5902,x5902),a2)),f5(f5(f1(x5903,x5903),f1(x5904,x5904)),f1(x5905,x5905)))), % 105.80/105.85 inference(scs_inference,[],[578,588,240,3,2])). % 105.80/105.85 cnf(599,plain, % 105.80/105.85 (~E(f5(f1(x5991,x5991),x5992),f1(f4(f4(x5992)),f1(f5(f4(a2),a2),f1(x5993,x5993))))), % 105.80/105.85 inference(scs_inference,[],[26,524,3])). % 105.80/105.85 cnf(601,plain, % 105.80/105.85 (E(f5(f4(f1(f1(x6011,x6011),f1(x6012,x6012))),x6013),f5(f1(x6014,x6014),x6013))), % 105.80/105.85 inference(scs_inference,[],[26,581,3])). % 105.80/105.85 cnf(604,plain, % 105.80/105.85 (~E(f1(f4(f4(x6041)),f1(f5(f4(a2),a2),f1(x6042,x6042))),f5(f1(x6043,x6043),x6041))), % 105.80/105.85 inference(scs_inference,[],[599,2])). % 105.80/105.85 cnf(608,plain, % 105.80/105.85 (~E(f1(f4(f1(f1(x6081,x6081),x6082)),f1(f5(f4(a2),a2),f1(x6083,x6083))),f5(f1(x6084,x6084),x6082))), % 105.80/105.85 inference(scs_inference,[],[604,161,3])). % 105.80/105.85 cnf(614,plain, % 105.80/105.85 (E(f5(f1(x6141,x6141),f1(f1(x6142,x6142),x6143)),f4(f1(f1(x6144,x6144),f4(x6143))))), % 105.80/105.85 inference(scs_inference,[],[26,153,3,2])). % 105.80/105.85 cnf(622,plain, % 105.80/105.85 (~E(f5(f1(x6221,x6221),x6222),f1(f4(f1(f1(x6223,x6223),x6222)),f1(f5(f4(a2),a2),f1(x6224,x6224))))), % 105.80/105.85 inference(scs_inference,[],[584,614,608,3,2])). % 105.80/105.85 cnf(632,plain, % 105.80/105.85 (E(f5(f4(f4(f1(x6321,x6321))),x6322),f5(f1(x6323,x6323),x6322))), % 105.80/105.85 inference(scs_inference,[],[601,163,3])). % 105.80/105.85 cnf(642,plain, % 105.80/105.85 (E(f1(f5(f1(x6421,x6421),f1(x6422,x6422)),f1(f1(x6423,x6423),x6424)),f5(f1(x6425,x6425),x6424))), % 105.80/105.85 inference(scs_inference,[],[27,246,3])). % 105.80/105.85 cnf(646,plain, % 105.80/105.85 (E(f5(f1(x6461,x6461),x6462),f1(f5(f1(x6463,x6463),f1(x6464,x6464)),f1(f1(x6465,x6465),x6462)))), % 105.80/105.85 inference(scs_inference,[],[642,2])). % 105.80/105.85 cnf(654,plain, % 105.80/105.85 (E(f1(f1(x6541,x6541),f1(f1(x6542,x6542),x6543)),f1(f5(f1(x6544,x6544),f1(x6545,x6545)),f1(f1(x6546,x6546),x6543)))), % 105.80/105.85 inference(scs_inference,[],[27,646,3])). % 105.80/105.85 cnf(656,plain, % 105.80/105.85 (E(f1(f5(f1(x6561,x6561),f1(x6562,x6562)),f1(f1(x6563,x6563),x6564)),f1(f1(x6565,x6565),f1(f1(x6566,x6566),x6564)))), % 105.80/105.85 inference(scs_inference,[],[27,646,3,2])). % 105.80/105.85 cnf(668,plain, % 105.80/105.85 (~E(a2,f5(f1(x6681,x6681),f1(f4(f4(a2)),f1(f1(x6682,x6682),f1(x6683,x6683)))))), % 105.80/105.85 inference(scs_inference,[],[29,463,521,2,3])). % 105.80/105.85 cnf(673,plain, % 105.80/105.85 (E(f5(f4(f4(f1(x6731,x6731))),x6732),f1(f1(x6733,x6733),f1(f1(x6734,x6734),x6732)))), % 105.80/105.85 inference(scs_inference,[],[29,632,3])). % 105.80/105.85 cnf(676,plain, % 105.80/105.85 (~E(f5(f1(x6761,x6761),f1(f4(f4(a2)),f1(f1(x6762,x6762),f1(x6763,x6763)))),a2)), % 105.80/105.85 inference(scs_inference,[],[668,2])). % 105.80/105.85 cnf(683,plain, % 105.80/105.85 (E(f1(f5(f1(x6831,x6831),f1(x6832,x6832)),f1(f1(x6833,x6833),x6834)),f1(f5(f1(x6835,x6835),f1(x6836,x6836)),f1(f1(x6837,x6837),x6834)))), % 105.80/105.85 inference(scs_inference,[],[654,656,3])). % 105.80/105.85 cnf(690,plain, % 105.80/105.85 (E(f4(f4(f4(x6901))),f4(f5(f1(x6902,x6902),x6901)))), % 105.80/105.85 inference(scs_inference,[],[229,162,3])). % 105.80/105.85 cnf(694,plain, % 105.80/105.85 (~E(f5(f1(x6941,x6941),x6942),f1(f5(f1(x6943,x6943),x6942),f1(f5(f4(a2),a2),f1(x6944,x6944))))), % 105.80/105.85 inference(scs_inference,[],[690,622,205,2,3])). % 105.80/105.85 cnf(696,plain, % 105.80/105.85 (~E(f1(f5(f1(x6961,x6961),x6962),f1(f5(f4(a2),a2),f1(x6963,x6963))),f5(f1(x6964,x6964),x6962))), % 105.80/105.85 inference(scs_inference,[],[694,2])). % 105.80/105.85 cnf(697,plain, % 105.80/105.85 (~E(f1(f5(f1(x6971,x6971),f1(x6972,x6972)),f1(f1(x6973,x6973),f1(x6974,x6974))),f5(f1(f1(x6975,x6975),a2),a2))), % 105.80/105.85 inference(scs_inference,[],[694,683,358,2,3])). % 105.80/105.85 cnf(700,plain, % 105.80/105.85 (E(f4(f5(f1(x7001,x7001),x7002)),f1(f1(x7003,x7003),f1(f1(x7004,x7004),f1(f1(x7005,x7005),x7002))))), % 105.80/105.85 inference(scs_inference,[],[30,219,3])). % 105.80/105.85 cnf(706,plain, % 105.80/105.85 (~E(f1(f5(f4(a2),a2),f1(x7061,x7061)),f1(f1(x7062,x7062),f1(x7063,x7063)))), % 105.80/105.85 inference(scs_inference,[],[696,700,642,2,3,5])). % 105.80/105.85 cnf(707,plain, % 105.80/105.85 (~E(f5(f4(a2),a2),f1(x7071,x7071))), % 105.80/105.85 inference(scs_inference,[],[706,4])). % 105.80/105.85 cnf(708,plain, % 105.80/105.85 (~E(f1(f5(f4(a2),a2),f1(x7081,x7081)),f1(f1(x7082,x7082),f1(x7083,x7083)))), % 105.80/105.85 inference(rename_variables,[],[706])). % 105.80/105.85 cnf(709,plain, % 105.80/105.85 (~E(f1(f1(x7091,x7091),f1(x7092,x7092)),f1(f5(f4(a2),a2),f1(x7093,x7093)))), % 105.80/105.85 inference(scs_inference,[],[706,708,4,2])). % 105.80/105.85 cnf(710,plain, % 105.80/105.85 (~E(f1(f5(f4(a2),a2),f1(f1(x7101,x7101),f1(x7102,x7102))),f1(f1(x7103,x7103),f1(x7104,x7104)))), % 105.80/105.85 inference(scs_inference,[],[706,708,101,4,2,3])). % 105.80/105.85 cnf(717,plain, % 105.80/105.85 (~E(f5(f4(a2),a2),f1(f1(f1(x7171,x7171),f1(f1(x7172,x7172),x7173)),f5(f1(x7174,x7174),x7173)))), % 105.80/105.85 inference(scs_inference,[],[707,236,2,3])). % 105.80/105.85 cnf(723,plain, % 105.80/105.85 (E(f5(f1(x7231,x7231),f5(f1(x7232,x7232),f1(x7233,x7233))),f1(f1(x7234,x7234),f1(x7235,x7235)))), % 105.80/105.85 inference(scs_inference,[],[92,249,3])). % 105.80/105.85 cnf(726,plain, % 105.80/105.85 (E(f5(f5(f1(x7261,x7261),f5(f1(x7262,x7262),f1(x7263,x7263))),x7264),f5(f1(f1(x7265,x7265),f1(x7266,x7266)),x7264))), % 105.80/105.85 inference(scs_inference,[],[92,249,3,6])). % 105.80/105.85 cnf(729,plain, % 105.80/105.85 (E(f1(f1(x7291,x7291),f1(x7292,x7292)),f5(f1(x7293,x7293),f5(f1(x7294,x7294),f1(x7295,x7295))))), % 105.80/105.85 inference(scs_inference,[],[92,249,3,6,7,5,2])). % 105.80/105.85 cnf(732,plain, % 105.80/105.85 (~E(f1(f1(x7321,x7321),f1(x7322,x7322)),f1(f5(f4(a2),a2),f1(f1(x7323,x7323),f1(x7324,x7324))))), % 105.80/105.85 inference(scs_inference,[],[710,2])). % 105.80/105.85 cnf(733,plain, % 105.80/105.85 (~E(f1(f5(f4(a2),a2),f1(f1(x7331,x7331),f1(x7332,x7332))),f4(f1(f1(x7333,x7333),f1(x7334,x7334))))), % 105.80/105.85 inference(scs_inference,[],[30,710,2,3])). % 105.80/105.85 cnf(737,plain, % 105.80/105.85 (~E(f5(f1(x7371,x7371),f5(f1(x7372,x7372),f1(x7373,x7373))),f1(f5(f4(a2),a2),f1(x7374,x7374)))), % 105.80/105.85 inference(scs_inference,[],[709,729,726,2,3])). % 105.80/105.85 cnf(739,plain, % 105.80/105.85 (~E(f1(f5(f4(a2),a2),f1(x7391,x7391)),f5(f1(x7392,x7392),f5(f1(x7393,x7393),f1(x7394,x7394))))), % 105.80/105.85 inference(scs_inference,[],[737,2])). % 105.80/105.85 cnf(740,plain, % 105.80/105.85 (E(f1(f1(x7401,x7401),f1(f1(x7402,x7402),x7403)),f5(f1(f1(f1(x7404,x7404),x7405),f4(x7405)),x7403))), % 105.80/105.85 inference(scs_inference,[],[32,737,564,2,3])). % 105.80/105.85 cnf(743,plain, % 105.80/105.85 (~E(f1(f5(f4(a2),a2),f1(f1(x7431,x7431),f1(x7432,x7432))),f1(f1(x7433,x7433),f1(f1(x7434,x7434),f1(x7435,x7435))))), % 105.80/105.85 inference(scs_inference,[],[32,740,733,2,3])). % 105.80/105.85 cnf(745,plain, % 105.80/105.85 (E(f4(f1(f1(x7451,x7451),f1(x7452,x7452))),f4(f5(f1(x7453,x7453),f5(f1(x7454,x7454),f1(x7455,x7455)))))), % 105.80/105.85 inference(scs_inference,[],[32,740,733,729,2,3,8])). % 105.80/105.85 cnf(750,plain, % 105.80/105.85 (~E(f4(f1(f1(x7501,x7501),f1(x7502,x7502))),f1(f5(f4(a2),a2),f1(f1(x7503,x7503),f1(x7504,x7504))))), % 105.80/105.85 inference(scs_inference,[],[32,732,743,2,3])). % 105.80/105.85 cnf(756,plain, % 105.80/105.85 (E(f4(f1(f1(x7561,x7561),f1(x7562,x7562))),f5(f1(x7563,x7563),f5(f1(x7564,x7564),f1(x7565,x7565))))), % 105.80/105.85 inference(scs_inference,[],[32,723,3,2])). % 105.80/105.85 cnf(758,plain, % 105.80/105.85 (~E(f1(f5(f4(a2),a2),f1(x7581,x7581)),f4(f1(f1(x7582,x7582),f1(x7583,x7583))))), % 105.80/105.85 inference(scs_inference,[],[739,756,717,2,3])). % 105.80/105.85 cnf(763,plain, % 105.80/105.85 (~E(f4(f1(f1(x7631,x7631),f1(x7632,x7632))),f1(f5(f4(a2),a2),f1(x7633,x7633)))), % 105.80/105.85 inference(scs_inference,[],[758,750,238,3,2])). % 105.80/105.85 cnf(770,plain, % 105.80/105.85 (~E(f5(f4(f1(f1(x7701,x7701),f1(x7702,x7702))),f1(x7703,x7703)),f1(f5(f4(a2),a2),f1(x7704,x7704)))), % 105.80/105.85 inference(scs_inference,[],[763,583,3])). % 105.80/105.85 cnf(773,plain, % 105.80/105.85 (E(f1(f1(x7731,x7731),f1(f1(x7732,x7732),f1(x7733,x7733))),f4(f5(f1(x7734,x7734),f5(f1(x7735,x7735),f1(x7736,x7736)))))), % 105.80/105.85 inference(scs_inference,[],[32,745,3])). % 105.80/105.85 cnf(775,plain, % 105.80/105.85 (E(f4(f5(f1(x7751,x7751),f5(f1(x7752,x7752),f1(x7753,x7753)))),f1(f1(x7754,x7754),f1(f1(x7755,x7755),f1(x7756,x7756))))), % 105.80/105.85 inference(scs_inference,[],[32,745,3,2])). % 105.80/105.85 cnf(779,plain, % 105.80/105.85 (~E(f5(f4(f4(f1(x7791,x7791))),f1(x7792,x7792)),f1(f5(f4(a2),a2),f1(x7793,x7793)))), % 105.80/105.85 inference(scs_inference,[],[770,222,3])). % 105.80/105.85 cnf(792,plain, % 105.80/105.85 (~E(f1(f5(f4(a2),a2),f1(x7921,x7921)),f5(f4(f4(f1(x7922,x7922))),f1(x7923,x7923)))), % 105.80/105.85 inference(scs_inference,[],[779,697,499,3,2])). % 105.80/105.85 cnf(858,plain, % 105.80/105.85 (E(f4(f1(f1(x8581,x8581),f4(x8582))),f4(f1(f1(x8583,x8583),f1(f1(x8584,x8584),x8582))))), % 105.80/105.85 inference(scs_inference,[],[36,194,3,2])). % 105.80/105.85 cnf(875,plain, % 105.80/105.85 (E(f1(f1(x8751,x8751),f1(f1(x8752,x8752),f1(x8753,x8753))),f1(f1(x8754,x8754),f1(f1(x8755,x8755),f1(x8756,x8756))))), % 105.80/105.85 inference(scs_inference,[],[775,773,3])). % 105.80/105.85 cnf(885,plain, % 105.80/105.85 (E(f1(f1(x8851,x8851),f1(f1(x8852,x8852),f1(x8853,x8853))),f5(f4(f4(f1(x8854,x8854))),f1(x8855,x8855)))), % 105.80/105.86 inference(scs_inference,[],[875,673,3,2])). % 105.80/105.86 cnf(964,plain, % 105.80/105.86 (E(f4(f1(x9641,x9641)),f5(f1(x9642,x9642),f4(f4(f1(x9643,x9643)))))), % 105.80/105.86 inference(scs_inference,[],[43,361,3,2])). % 105.80/105.86 cnf(992,plain, % 105.80/105.86 (E(f5(f1(x9921,x9921),f1(f1(x9922,x9922),x9923)),f4(f1(f1(x9924,x9924),f1(f1(x9925,x9925),x9923))))), % 105.80/105.86 inference(scs_inference,[],[858,614,3])). % 105.80/105.86 cnf(1001,plain, % 105.80/105.86 (E(f5(f1(x10011,x10011),f1(f1(x10012,x10012),f1(x10013,x10013))),f5(f1(x10014,x10014),f4(f4(f1(x10015,x10015)))))), % 105.80/105.86 inference(scs_inference,[],[964,992,3])). % 105.80/105.86 cnf(1005,plain, % 105.80/105.86 (~E(f1(f5(f4(a2),a2),f1(x10051,x10051)),f5(f1(f1(x10052,x10052),f1(f1(x10053,x10053),f1(x10054,x10054))),f1(x10055,x10055)))), % 105.80/105.86 inference(scs_inference,[],[1001,792,138,2,3])). % 105.80/105.86 cnf(1008,plain, % 105.80/105.86 (~E(f1(f1(x10081,x10081),f4(a2)),a2)), % 105.80/105.86 inference(scs_inference,[],[44,1005,676,2,3])). % 105.80/105.86 cnf(1111,plain, % 105.80/105.86 (E(f1(f1(x11111,x11111),f1(f1(x11112,x11112),f1(x11113,x11113))),f5(f1(x11114,x11114),f1(x11115,x11115)))), % 105.80/105.86 inference(scs_inference,[],[632,885,3])). % 105.80/105.86 cnf(1114,plain, % 105.80/105.86 (E(f5(f1(x11141,x11141),f1(x11142,x11142)),f1(f1(x11143,x11143),f1(f1(x11144,x11144),f1(x11145,x11145))))), % 105.80/105.86 inference(scs_inference,[],[632,885,3,2])). % 105.80/105.86 cnf(1115,plain, % 105.80/105.86 (E(f4(f1(f1(x11151,x11151),f1(f1(x11152,x11152),f1(x11153,x11153)))),f4(f5(f1(x11154,x11154),f1(x11155,x11155))))), % 105.80/105.86 inference(scs_inference,[],[632,885,3,2,8])). % 105.80/105.86 cnf(1116,plain, % 105.80/105.86 (E(f1(f1(f1(x11161,x11161),f1(f1(x11162,x11162),f1(x11163,x11163))),x11164),f1(f5(f1(x11165,x11165),f1(x11166,x11166)),x11164))), % 105.80/105.86 inference(scs_inference,[],[632,885,3,2,8,4])). % 105.80/105.86 cnf(1117,plain, % 105.80/105.86 (E(f5(f1(f1(x11171,x11171),f1(f1(x11172,x11172),f1(x11173,x11173))),x11174),f5(f5(f1(x11175,x11175),f1(x11176,x11176)),x11174))), % 105.80/105.86 inference(scs_inference,[],[632,885,3,2,8,4,6])). % 105.80/105.86 cnf(1125,plain, % 105.80/105.86 (~E(f1(f5(f1(x11251,x11251),f1(x11252,x11252)),f4(a2)),a2)), % 105.80/105.86 inference(scs_inference,[],[1008,1115,1116,2,3])). % 105.80/105.86 cnf(1129,plain, % 105.80/105.86 (E(f1(f1(x11291,x11291),f1(f1(x11292,x11292),f1(x11293,x11293))),f5(f5(f1(x11294,x11294),f1(x11295,x11295)),f1(x11296,x11296)))), % 105.80/105.86 inference(scs_inference,[],[1125,1111,1117,2,3])). % 105.80/105.86 cnf(1136,plain, % 105.80/105.86 (E(f5(f5(f1(x11361,x11361),f1(x11362,x11362)),x11363),f5(f1(f1(x11364,x11364),f1(f1(x11365,x11365),f1(x11366,x11366))),x11363))), % 105.80/105.86 inference(scs_inference,[],[1129,1114,590,2,3,4,6])). % 105.80/105.86 cnf(1182,plain, % 105.80/105.86 (E(f5(f5(f1(x11821,x11821),f1(x11822,x11822)),x11823),f5(f1(x11824,x11824),x11823))), % 105.80/105.86 inference(scs_inference,[],[52,1136,3])). % 105.80/105.86 cnf(1185,plain, % 105.80/105.86 (E(f4(f5(f5(f1(x11851,x11851),f1(x11852,x11852)),x11853)),f4(f5(f1(x11854,x11854),x11853)))), % 105.80/105.86 inference(scs_inference,[],[52,1136,3,8])). % 105.80/105.86 cnf(1191,plain, % 105.80/105.86 (E(f5(f1(x11911,x11911),x11912),f5(f5(f1(x11913,x11913),f1(x11914,x11914)),x11912))), % 105.80/105.86 inference(scs_inference,[],[1182,2])). % 105.80/105.86 cnf(1198,plain, % 105.80/105.86 (E(x11981,f5(f5(f1(x11982,x11982),f1(x11983,x11983)),f1(x11981,f1(f1(x11984,x11984),f1(x11985,x11985)))))), % 105.80/105.86 inference(scs_inference,[],[55,1191,1185,2,3])). % 105.80/105.86 cnf(1212,plain, % 105.80/105.86 (~E(f1(f5(f4(a2),a2),f1(f1(x12121,x12121),f1(x12122,x12122))),f1(x12123,x12123))), % 105.80/105.86 inference(scs_inference,[],[55,1198,576,2,3,7])). % 105.80/105.86 cnf(1214,plain, % 105.80/105.86 ($false), % 105.80/105.86 inference(scs_inference,[],[55,1212,565,19,2,3]), % 105.80/105.86 ['proof']). % 105.80/105.86 % SZS output end Proof % 105.80/105.86 % Total time :105.140000s %------------------------------------------------------------------------------