%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : GRP522-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 : n001.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 186.64s 186.81s % Output : CNFRefutation 186.81s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : GRP522-1 : TPTP v8.2.0. Released v2.6.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n001.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 : Thu Jun 20 12:19:38 EDT 2024 % 0.12/0.33 % CPUTime : % 0.52/0.56 start to proof:theBenchmark % 186.64/186.77 %------------------------------------------- % 186.64/186.77 % File :CSE---1.7 % 186.64/186.77 % Problem :theBenchmark % 186.64/186.77 % Transform :cnf % 186.64/186.77 % Format :tptp:raw % 186.64/186.77 % Command :java -jar mcs_scs.jar %d %s % 186.64/186.77 % 186.64/186.77 % Result :Theorem 186.040000s % 186.64/186.77 % Output :CNFRefutation 186.040000s % 186.64/186.77 %------------------------------------------- % 186.64/186.81 %-------------------------------------------------------------------------- % 186.64/186.81 % File : GRP522-1 : TPTP v8.2.0. Released v2.6.0. % 186.64/186.81 % Domain : Group Theory (Abelian) % 186.64/186.81 % Problem : Axiom for Abelian group theory, in division, part 2 % 186.64/186.81 % Version : [McC93] (equality) axioms. % 186.64/186.81 % English : % 186.64/186.81 % 186.64/186.81 % Refs : [Tar38] Tarski (1938), Ein Beitrag zur Axiomatik der Abelschen % 186.64/186.81 % : [McC93] McCune (1993), Single Axioms for Groups and Abelian Gr % 186.64/186.81 % Source : [TPTP] % 186.64/186.81 % Names : % 186.64/186.81 % 186.64/186.81 % Status : Unsatisfiable % 186.64/186.81 % Rating : 0.00 v8.1.0, 0.05 v7.5.0, 0.04 v7.4.0, 0.13 v7.3.0, 0.05 v7.1.0, 0.00 v7.0.0, 0.05 v6.3.0, 0.06 v6.2.0, 0.07 v6.1.0, 0.06 v6.0.0, 0.14 v5.5.0, 0.11 v5.4.0, 0.00 v5.1.0, 0.13 v5.0.0, 0.07 v4.1.0, 0.09 v4.0.1, 0.07 v4.0.0, 0.08 v3.7.0, 0.00 v2.6.0 % 186.64/186.81 % Syntax : Number of clauses : 4 ( 4 unt; 0 nHn; 1 RR) % 186.64/186.81 % Number of literals : 4 ( 4 equ; 1 neg) % 186.64/186.81 % Maximal clause size : 1 ( 1 avg) % 186.64/186.81 % Maximal term depth : 5 ( 2 avg) % 186.64/186.81 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty) % 186.64/186.81 % Number of functors : 5 ( 5 usr; 2 con; 0-2 aty) % 186.64/186.81 % Number of variables : 8 ( 0 sgn) % 186.64/186.81 % SPC : CNF_UNS_RFO_PEQ_UEQ % 186.64/186.81 % 186.64/186.81 % Comments : A UEQ part of GRP088-1 % 186.64/186.81 %-------------------------------------------------------------------------- % 186.64/186.81 cnf(single_axiom,axiom, % 186.64/186.81 divide(A,divide(B,divide(C,divide(A,B)))) = C ). % 186.64/186.81 % 186.64/186.81 cnf(multiply,axiom, % 186.64/186.81 multiply(A,B) = divide(A,divide(divide(C,C),B)) ). % 186.64/186.81 % 186.64/186.81 cnf(inverse,axiom, % 186.64/186.81 inverse(A) = divide(divide(B,B),A) ). % 186.64/186.81 % 186.64/186.81 cnf(prove_these_axioms_2,negated_conjecture, % 186.64/186.81 multiply(multiply(inverse(b2),b2),a2) != a2 ). % 186.64/186.81 % 186.64/186.81 %-------------------------------------------------------------------------- % 186.64/186.81 %------------------------------------------- % 186.64/186.81 % Proof found % 186.64/186.81 % SZS status Theorem for theBenchmark % 186.64/186.81 % SZS output start Proof % 186.74/186.85 %ClaNum:12(EqnAxiom:8) % 186.74/186.85 %VarNum:16(SingletonVarNum:8) % 186.74/186.85 %MaxLitNum:1 % 186.74/186.85 %MaxfuncDepth:4 % 186.74/186.85 %SharedTerms:6 % 186.74/186.85 %goalClause: 12 % 186.74/186.85 %singleGoalClaCount:1 % 186.74/186.85 [12]~E(f5(f5(f4(a2),a2),a3),a3) % 186.74/186.85 [9]E(f1(f1(x91,x91),x92),f4(x92)) % 186.74/186.85 [10]E(f1(x101,f1(f1(x102,x102),x103)),f5(x101,x103)) % 186.74/186.85 [11]E(f1(x111,f1(x112,f1(x113,f1(x111,x112)))),x113) % 186.74/186.85 %EqnAxiom % 186.74/186.85 [1]E(x11,x11) % 186.74/186.85 [2]E(x22,x21)+~E(x21,x22) % 186.74/186.85 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 186.74/186.85 [4]~E(x41,x42)+E(f1(x41,x43),f1(x42,x43)) % 186.74/186.85 [5]~E(x51,x52)+E(f1(x53,x51),f1(x53,x52)) % 186.74/186.85 [6]~E(x61,x62)+E(f5(x61,x63),f5(x62,x63)) % 186.74/186.85 [7]~E(x71,x72)+E(f5(x73,x71),f5(x73,x72)) % 186.74/186.85 [8]~E(x81,x82)+E(f4(x81),f4(x82)) % 186.74/186.85 % 186.74/186.85 %------------------------------------------- % 186.74/186.89 cnf(13,plain, % 186.74/186.89 (E(f4(x131),f1(f1(x132,x132),x131))), % 186.74/186.89 inference(scs_inference,[],[9,2])). % 186.74/186.89 cnf(14,plain, % 186.74/186.89 (E(f1(x141,f1(x142,f1(f1(f1(x143,x143),x144),f1(x141,x142)))),f4(x144))), % 186.74/186.89 inference(scs_inference,[],[9,11,2,3])). % 186.74/186.89 cnf(16,plain, % 186.74/186.89 (E(f4(x161),f1(x162,f1(x163,f1(f1(f1(x164,x164),x161),f1(x162,x163)))))), % 186.74/186.89 inference(scs_inference,[],[14,2])). % 186.74/186.89 cnf(17,plain, % 186.74/186.89 (E(f4(f1(f1(x171,x171),x172)),f5(f1(x173,x173),x172))), % 186.74/186.89 inference(scs_inference,[],[13,14,10,2,3])). % 186.74/186.89 cnf(20,plain, % 186.74/186.89 (E(f5(f1(x201,x201),x202),f4(f1(f1(x203,x203),x202)))), % 186.74/186.89 inference(scs_inference,[],[17,2])). % 186.74/186.89 cnf(21,plain, % 186.74/186.89 (E(f4(x211),f5(x212,f1(f1(f1(x213,x213),x211),f1(x212,f1(x214,x214)))))), % 186.74/186.89 inference(scs_inference,[],[16,17,10,2,3])). % 186.74/186.89 cnf(24,plain, % 186.74/186.89 (E(f5(x241,f1(f1(f1(x242,x242),x243),f1(x241,f1(x244,x244)))),f4(x243))), % 186.74/186.89 inference(scs_inference,[],[21,2])). % 186.74/186.89 cnf(25,plain, % 186.74/186.89 (E(f5(f1(x251,x251),x252),f1(f1(x253,x253),f1(f1(x254,x254),x252)))), % 186.74/186.89 inference(scs_inference,[],[20,13,21,2,3])). % 186.74/186.89 cnf(27,plain, % 186.74/186.89 (E(f1(f1(x271,x271),f1(f1(x272,x272),x273)),f5(f1(x274,x274),x273))), % 186.74/186.89 inference(scs_inference,[],[25,2])). % 186.74/186.89 cnf(28,plain, % 186.74/186.89 (E(f4(f1(f1(x281,x281),x282)),f4(f1(f1(x283,x283),x282)))), % 186.74/186.89 inference(scs_inference,[],[20,25,17,2,3])). % 186.74/186.89 cnf(30,plain, % 186.74/186.89 (E(x301,f1(x302,f1(x303,f1(x301,f1(x302,x303)))))), % 186.74/186.89 inference(scs_inference,[],[11,2])). % 186.74/186.89 cnf(31,plain, % 186.74/186.89 (E(f4(x311),f5(f1(x312,x312),f1(f1(f1(x313,x313),x311),f1(f1(x314,x314),f1(x315,x315)))))), % 186.74/186.89 inference(scs_inference,[],[27,16,11,2,3])). % 186.74/186.89 cnf(35,plain, % 186.74/186.89 (E(x351,f5(f1(x352,x352),f1(x351,f1(f1(x353,x353),f1(x354,x354)))))), % 186.74/186.89 inference(scs_inference,[],[30,27,31,2,3])). % 186.74/186.89 cnf(38,plain, % 186.74/186.89 (E(f5(f1(x381,x381),f1(x382,f1(f1(x383,x383),f1(x384,x384)))),x382)), % 186.74/186.90 inference(scs_inference,[],[35,2])). % 186.74/186.90 cnf(39,plain, % 186.74/186.90 (E(f1(f1(x391,x391),f1(f1(x392,x392),x393)),f4(f1(f1(x394,x394),x393)))), % 186.74/186.90 inference(scs_inference,[],[27,20,35,2,3])). % 186.74/186.90 cnf(41,plain, % 186.74/186.90 (E(f4(f1(f1(x411,x411),x412)),f1(f1(x413,x413),f1(f1(x414,x414),x412)))), % 186.74/186.90 inference(scs_inference,[],[39,2])). % 186.74/186.90 cnf(42,plain, % 186.74/186.90 (E(f5(x421,x422),f1(x421,f1(f1(x423,x423),x422)))), % 186.74/186.90 inference(scs_inference,[],[10,2])). % 186.74/186.90 cnf(43,plain, % 186.74/186.90 (E(f1(f1(x431,x431),f1(f1(x432,x432),x433)),f1(f1(x434,x434),f1(f1(x435,x435),x433)))), % 186.74/186.90 inference(scs_inference,[],[9,41,3])). % 186.74/186.90 cnf(45,plain, % 186.74/186.90 (E(f1(f1(x451,x451),x452),f1(x453,f1(x454,f1(f4(x452),f1(x453,x454)))))), % 186.74/186.90 inference(scs_inference,[],[9,30,3])). % 186.74/186.90 cnf(47,plain, % 186.74/186.90 (E(f1(x471,f1(x472,f1(f4(x473),f1(x471,x472)))),f1(f1(x474,x474),x473))), % 186.74/186.90 inference(scs_inference,[],[9,30,3,2])). % 186.74/186.90 cnf(48,plain, % 186.74/186.90 (E(f5(x481,f1(f4(x482),f1(x481,f1(x483,x483)))),f1(f1(x484,x484),x482))), % 186.74/186.90 inference(scs_inference,[],[47,42,3])). % 186.74/186.90 cnf(52,plain, % 186.74/186.90 (E(f1(f1(x521,x521),x522),f1(f1(x523,x523),x522))), % 186.74/186.90 inference(scs_inference,[],[9,13,3])). % 186.74/186.90 cnf(62,plain, % 186.74/186.90 (E(f5(f1(x621,x621),x622),f5(f1(x623,x623),x622))), % 186.74/186.90 inference(scs_inference,[],[20,17,3])). % 186.74/186.90 cnf(64,plain, % 186.74/186.90 (E(x641,f5(x642,f1(x641,f1(x642,f1(x643,x643)))))), % 186.74/186.90 inference(scs_inference,[],[30,10,3])). % 186.74/186.90 cnf(67,plain, % 186.74/186.90 (E(f5(x671,f1(x672,f1(x671,f1(x673,x673)))),x672)), % 186.74/186.90 inference(scs_inference,[],[30,10,3,2])). % 186.74/186.90 cnf(68,plain, % 186.74/186.90 (~E(f5(f5(f4(a2),a2),a3),f5(f1(x681,x681),f1(a3,f1(f1(x682,x682),f1(x683,x683)))))), % 186.74/186.90 inference(scs_inference,[],[38,12,3])). % 186.74/186.90 cnf(70,plain, % 186.74/186.90 (~E(f5(f5(f4(a2),a2),a3),f5(x701,f1(a3,f1(x701,f1(x702,x702)))))), % 186.74/186.90 inference(scs_inference,[],[67,12,3])). % 186.74/186.90 cnf(72,plain, % 186.74/186.90 (E(f5(x721,f1(f1(f1(x722,x722),x723),f1(x721,f1(x724,x724)))),f1(f1(x725,x725),x723))), % 186.74/186.90 inference(scs_inference,[],[24,13,3])). % 186.74/186.90 cnf(83,plain, % 186.74/186.90 (E(f4(f1(f1(x831,x831),x832)),f4(f4(x832)))), % 186.74/186.90 inference(scs_inference,[],[9,8])). % 186.74/186.90 cnf(84,plain, % 186.74/186.90 (E(f1(f1(f1(x841,x841),x842),x843),f1(f4(x842),x843))), % 186.74/186.90 inference(scs_inference,[],[9,8,4])). % 186.74/186.90 cnf(85,plain, % 186.74/186.90 (E(f1(x851,f1(f1(x852,x852),x853)),f1(x851,f4(x853)))), % 186.74/186.90 inference(scs_inference,[],[9,8,4,5])). % 186.74/186.90 cnf(86,plain, % 186.74/186.90 (E(f5(f1(f1(x861,x861),x862),x863),f5(f4(x862),x863))), % 186.74/186.90 inference(scs_inference,[],[9,8,4,5,6])). % 186.74/186.90 cnf(87,plain, % 186.74/186.90 (E(f5(x871,f1(f1(x872,x872),x873)),f5(x871,f4(x873)))), % 186.74/186.90 inference(scs_inference,[],[9,8,4,5,6,7])). % 186.74/186.90 cnf(91,plain, % 186.74/186.90 (E(f1(x911,f5(f1(x912,x912),x913)),f1(x911,f5(f1(x914,x914),x913)))), % 186.74/186.90 inference(scs_inference,[],[62,5])). % 186.74/186.90 cnf(92,plain, % 186.74/186.90 (E(f4(f5(f1(x921,x921),x922)),f4(f5(f1(x923,x923),x922)))), % 186.74/186.90 inference(scs_inference,[],[62,5,8])). % 186.74/186.90 cnf(94,plain, % 186.74/186.90 (E(f1(f1(f1(x941,x941),x942),x943),f1(f1(f1(x944,x944),x942),x943))), % 186.74/186.90 inference(scs_inference,[],[52,62,5,8,7,4])). % 186.74/186.90 cnf(95,plain, % 186.74/186.90 (E(f5(f1(f1(x951,x951),x952),x953),f5(f1(f1(x954,x954),x952),x953))), % 186.74/186.90 inference(scs_inference,[],[52,62,5,8,7,4,6])). % 186.74/186.90 cnf(96,plain, % 186.74/186.90 (~E(f5(f1(x961,x961),f1(a3,f1(f1(x962,x962),f1(x963,x963)))),f5(f5(f4(a2),a2),a3))), % 186.74/186.90 inference(scs_inference,[],[52,62,68,5,8,7,4,6,2])). % 186.74/186.90 cnf(100,plain, % 186.74/186.90 (E(f5(x1001,f4(f1(f1(x1002,x1002),x1003))),f5(x1001,f4(f4(x1003))))), % 186.74/186.90 inference(scs_inference,[],[83,7])). % 186.74/186.90 cnf(103,plain, % 186.74/186.90 (E(f5(f4(f1(f1(x1031,x1031),x1032)),x1033),f5(f4(f4(x1032)),x1033))), % 186.74/186.90 inference(scs_inference,[],[83,7,5,8,6])). % 186.74/186.90 cnf(104,plain, % 186.74/186.90 (E(f1(f4(f1(f1(x1041,x1041),x1042)),x1043),f1(f4(f4(x1042)),x1043))), % 186.74/186.90 inference(scs_inference,[],[83,7,5,8,6,4])). % 186.74/186.90 cnf(106,plain, % 186.74/186.90 (E(f5(f1(f1(x1061,x1061),x1062),f1(f1(x1063,x1063),x1064)),f5(f4(x1062),f4(x1064)))), % 186.74/186.90 inference(scs_inference,[],[83,86,87,70,7,5,8,6,4,2,3])). % 186.74/186.90 cnf(109,plain, % 186.74/186.90 (E(f5(x1091,f1(f1(f1(x1092,x1092),x1093),x1094)),f5(x1091,f1(f4(x1093),x1094)))), % 186.74/186.90 inference(scs_inference,[],[84,7])). % 186.74/186.90 cnf(111,plain, % 186.74/186.90 (E(f1(x1111,f1(f1(f1(x1112,x1112),x1113),x1114)),f1(x1111,f1(f4(x1113),x1114)))), % 186.74/186.90 inference(scs_inference,[],[84,7,8,5])). % 186.74/186.90 cnf(113,plain, % 186.74/186.90 (E(f5(f1(f1(f1(x1131,x1131),x1132),x1133),x1134),f5(f1(f4(x1132),x1133),x1134))), % 186.74/186.90 inference(scs_inference,[],[84,7,8,5,4,6])). % 186.74/186.90 cnf(115,plain, % 186.74/186.90 (E(f5(x1151,f1(x1152,f1(f1(x1153,x1153),x1154))),f5(x1151,f1(x1152,f4(x1154))))), % 186.74/186.90 inference(scs_inference,[],[85,7])). % 186.74/186.90 cnf(116,plain, % 186.74/186.90 (E(f1(x1161,f1(x1162,f1(f1(x1163,x1163),x1164))),f1(x1161,f1(x1162,f4(x1164))))), % 186.74/186.90 inference(scs_inference,[],[85,7,5])). % 186.74/186.90 cnf(117,plain, % 186.74/186.90 (E(f4(f1(x1171,f1(f1(x1172,x1172),x1173))),f4(f1(x1171,f4(x1173))))), % 186.74/186.90 inference(scs_inference,[],[85,7,5,8])). % 186.74/186.90 cnf(118,plain, % 186.74/186.90 (E(f5(f1(x1181,f1(f1(x1182,x1182),x1183)),x1184),f5(f1(x1181,f4(x1183)),x1184))), % 186.74/186.90 inference(scs_inference,[],[85,7,5,8,6])). % 186.74/186.90 cnf(124,plain, % 186.74/186.90 (E(f1(f5(f1(f1(x1241,x1241),x1242),x1243),x1244),f1(f5(f4(x1242),x1243),x1244))), % 186.74/186.90 inference(scs_inference,[],[86,7,8,5,4])). % 186.74/186.90 cnf(125,plain, % 186.74/186.90 (E(f5(f5(f1(f1(x1251,x1251),x1252),x1253),x1254),f5(f5(f4(x1252),x1253),x1254))), % 186.74/186.90 inference(scs_inference,[],[86,7,8,5,4,6])). % 186.74/186.90 cnf(129,plain, % 186.74/186.90 (E(f4(f5(x1291,f1(f1(x1292,x1292),x1293))),f4(f5(x1291,f4(x1293))))), % 186.74/186.90 inference(scs_inference,[],[87,7,5,8])). % 186.74/186.90 cnf(130,plain, % 186.74/186.90 (E(f5(f5(x1301,f1(f1(x1302,x1302),x1303)),x1304),f5(f5(x1301,f4(x1303)),x1304))), % 186.74/186.90 inference(scs_inference,[],[87,7,5,8,6])). % 186.74/186.90 cnf(131,plain, % 186.74/186.90 (E(f1(f5(x1311,f1(f1(x1312,x1312),x1313)),x1314),f1(f5(x1311,f4(x1313)),x1314))), % 186.74/186.90 inference(scs_inference,[],[87,7,5,8,6,4])). % 186.74/186.90 cnf(135,plain, % 186.74/186.90 (E(f5(x1351,f5(f1(x1352,x1352),x1353)),f5(x1351,f1(f1(x1354,x1354),f1(f1(x1355,x1355),x1353))))), % 186.74/186.90 inference(scs_inference,[],[25,7])). % 186.74/186.90 cnf(137,plain, % 186.74/186.90 (E(f1(x1371,f5(f1(x1372,x1372),x1373)),f1(x1371,f1(f1(x1374,x1374),f1(f1(x1375,x1375),x1373))))), % 186.74/186.90 inference(scs_inference,[],[25,7,8,5])). % 186.74/186.90 cnf(139,plain, % 186.74/186.90 (E(f5(f5(f1(x1391,x1391),x1392),x1393),f5(f1(f1(x1394,x1394),f1(f1(x1395,x1395),x1392)),x1393))), % 186.74/186.90 inference(scs_inference,[],[25,7,8,5,4,6])). % 186.74/186.90 cnf(140,plain, % 186.74/186.90 (E(f5(x1401,f5(x1402,x1403)),f5(x1401,f1(x1402,f1(f1(x1404,x1404),x1403))))), % 186.74/186.90 inference(scs_inference,[],[42,7])). % 186.74/186.90 cnf(141,plain, % 186.74/186.90 (E(f1(x1411,f5(x1412,x1413)),f1(x1411,f1(x1412,f1(f1(x1414,x1414),x1413))))), % 186.74/186.90 inference(scs_inference,[],[42,7,5])). % 186.74/186.90 cnf(143,plain, % 186.81/186.90 (E(f5(f5(x1431,x1432),x1433),f5(f1(x1431,f1(f1(x1434,x1434),x1432)),x1433))), % 186.81/186.90 inference(scs_inference,[],[42,7,5,8,6])). % 186.81/186.90 cnf(144,plain, % 186.81/186.90 (E(f1(f5(x1441,x1442),x1443),f1(f1(x1441,f1(f1(x1444,x1444),x1442)),x1443))), % 186.81/186.90 inference(scs_inference,[],[42,7,5,8,6,4])). % 186.81/186.90 cnf(145,plain, % 186.81/186.90 (E(f5(x1451,f5(f1(x1452,x1452),x1453)),f5(x1451,f5(f1(x1454,x1454),x1453)))), % 186.81/186.90 inference(scs_inference,[],[62,7])). % 186.81/186.90 cnf(146,plain, % 186.81/186.90 (E(f4(f4(f1(f1(x1461,x1461),x1462))),f4(f5(f1(x1463,x1463),x1462)))), % 186.81/186.90 inference(scs_inference,[],[62,17,7,8])). % 186.81/186.90 cnf(148,plain, % 186.81/186.90 (E(f1(f5(f1(x1481,x1481),x1482),x1483),f1(f5(f1(x1484,x1484),x1482),x1483))), % 186.81/186.90 inference(scs_inference,[],[62,17,7,8,5,4])). % 186.81/186.90 cnf(149,plain, % 186.81/186.90 (E(f5(f5(f1(x1491,x1491),x1492),x1493),f5(f5(f1(x1494,x1494),x1492),x1493))), % 186.81/186.90 inference(scs_inference,[],[62,17,7,8,5,4,6])). % 186.81/186.90 cnf(150,plain, % 186.81/186.90 (~E(f5(f1(f4(a2),f1(f1(x1501,x1501),a2)),a3),a3)), % 186.81/186.90 inference(scs_inference,[],[143,62,17,12,7,8,5,4,6,3])). % 186.81/186.90 cnf(154,plain, % 186.81/186.90 (E(f1(x1541,f1(f1(x1542,x1542),f1(f1(x1543,x1543),x1544))),f1(x1541,f5(f1(x1545,x1545),x1544)))), % 186.81/186.90 inference(scs_inference,[],[27,7,5])). % 186.81/186.90 cnf(156,plain, % 186.81/186.90 (E(f5(f1(f1(x1561,x1561),f1(f1(x1562,x1562),x1563)),x1564),f5(f5(f1(x1565,x1565),x1563),x1564))), % 186.81/186.90 inference(scs_inference,[],[27,7,5,8,6])). % 186.81/186.90 cnf(158,plain, % 186.81/186.90 (E(f1(f1(x1581,x1581),f5(x1582,x1583)),f4(f1(x1582,f1(f1(x1584,x1584),x1583))))), % 186.81/186.90 inference(scs_inference,[],[9,141,27,7,5,8,6,4,3])). % 186.81/186.90 cnf(161,plain, % 186.81/186.90 (E(f5(x1611,f1(x1612,f1(f1(x1613,x1613),x1614))),f5(x1611,f5(x1612,x1614)))), % 186.81/186.90 inference(scs_inference,[],[10,7])). % 186.81/186.90 cnf(162,plain, % 186.81/186.90 (E(f4(f1(x1621,f1(f1(x1622,x1622),x1623))),f4(f5(x1621,x1623)))), % 186.81/186.90 inference(scs_inference,[],[10,7,8])). % 186.81/186.90 cnf(163,plain, % 186.81/186.90 (E(f1(x1631,f1(x1632,f1(f1(x1633,x1633),x1634))),f1(x1631,f5(x1632,x1634)))), % 186.81/186.90 inference(scs_inference,[],[10,7,8,5])). % 186.81/186.90 cnf(164,plain, % 186.81/186.90 (E(f1(f1(x1641,f1(f1(x1642,x1642),x1643)),x1644),f1(f5(x1641,x1643),x1644))), % 186.81/186.90 inference(scs_inference,[],[10,7,8,5,4])). % 186.81/186.90 cnf(165,plain, % 186.81/186.90 (E(f5(f1(x1651,f1(f1(x1652,x1652),x1653)),x1654),f5(f5(x1651,x1653),x1654))), % 186.81/186.90 inference(scs_inference,[],[10,7,8,5,4,6])). % 186.81/186.90 cnf(166,plain, % 186.81/186.90 (~E(f5(f1(f4(a2),f4(a2)),a3),a3)), % 186.81/186.90 inference(scs_inference,[],[10,150,118,7,8,5,4,6,3])). % 186.81/186.90 cnf(169,plain, % 186.81/186.90 (~E(a3,f5(f1(f4(a2),f4(a2)),a3))), % 186.81/186.90 inference(scs_inference,[],[10,150,118,7,8,5,4,6,3,2])). % 186.81/186.90 cnf(170,plain, % 186.81/186.90 (E(f5(x1701,f5(f1(x1702,x1702),x1703)),f5(x1701,f4(f1(f1(x1704,x1704),x1703))))), % 186.81/186.90 inference(scs_inference,[],[20,7])). % 186.81/186.90 cnf(174,plain, % 186.81/186.90 (E(f1(f5(f1(x1741,x1741),x1742),x1743),f1(f4(f1(f1(x1744,x1744),x1742)),x1743))), % 186.81/186.90 inference(scs_inference,[],[20,7,5,8,6,4])). % 186.81/186.90 cnf(175,plain, % 186.81/186.90 (~E(f5(f1(x1751,x1751),f5(a3,f1(x1752,x1752))),f5(f5(f4(a2),a2),a3))), % 186.81/186.90 inference(scs_inference,[],[161,96,20,7,5,8,6,4,3])). % 186.81/186.90 cnf(179,plain, % 186.81/186.90 (E(f4(f4(x1791)),f4(f1(f1(x1792,x1792),x1791)))), % 186.81/186.90 inference(scs_inference,[],[17,13,7,8])). % 186.81/186.90 cnf(180,plain, % 186.81/186.90 (E(f1(x1801,f4(x1802)),f1(x1801,f1(f1(x1803,x1803),x1802)))), % 186.81/186.90 inference(scs_inference,[],[17,13,7,8,5])). % 186.81/186.90 cnf(183,plain, % 186.81/186.90 (~E(f5(x1831,f1(a3,f1(x1831,f1(x1832,x1832)))),f5(f1(f4(a2),f4(a2)),a3))), % 186.81/186.90 inference(scs_inference,[],[169,64,17,13,7,8,5,4,6,3])). % 186.81/186.90 cnf(191,plain, % 186.81/186.90 (E(f1(x1911,f4(x1912)),f5(x1911,x1912))), % 186.81/186.90 inference(scs_inference,[],[10,179,180,7,5,8,6,4,3])). % 186.81/186.90 cnf(193,plain, % 186.81/186.90 (E(f5(x1931,f1(x1932,f4(x1933))),f5(x1931,f5(x1932,x1933)))), % 186.81/186.90 inference(scs_inference,[],[191,7])). % 186.81/186.90 cnf(194,plain, % 186.81/186.90 (E(f4(f1(x1941,f4(x1942))),f4(f5(x1941,x1942)))), % 186.81/186.90 inference(scs_inference,[],[191,7,8])). % 186.81/186.90 cnf(195,plain, % 186.81/186.90 (E(f1(x1951,f1(x1952,f4(x1953))),f1(x1951,f5(x1952,x1953)))), % 186.81/186.90 inference(scs_inference,[],[191,7,8,5])). % 186.81/186.90 cnf(196,plain, % 186.81/186.90 (E(f1(f1(x1961,f4(x1962)),x1963),f1(f5(x1961,x1962),x1963))), % 186.81/186.90 inference(scs_inference,[],[191,7,8,5,4])). % 186.81/186.91 cnf(197,plain, % 186.81/186.91 (E(f5(f1(x1971,f4(x1972)),x1973),f5(f5(x1971,x1972),x1973))), % 186.81/186.91 inference(scs_inference,[],[191,7,8,5,4,6])). % 186.81/186.91 cnf(198,plain, % 186.81/186.91 (~E(f5(f1(x1981,x1981),f1(f5(f1(f4(a2),f4(a2)),a3),f1(f1(x1982,x1982),f1(x1983,x1983)))),a3)), % 186.81/186.91 inference(scs_inference,[],[191,166,35,7,8,5,4,6,3])). % 186.81/186.91 cnf(200,plain, % 186.81/186.91 (E(f5(x2001,f5(x2002,f1(x2003,f4(x2004)))),f5(x2001,f5(x2002,f5(x2003,x2004))))), % 186.81/186.91 inference(scs_inference,[],[193,7])). % 186.81/186.91 cnf(203,plain, % 186.81/186.91 (E(f5(f5(x2031,f1(x2032,f4(x2033))),x2034),f5(f5(x2031,f5(x2032,x2033)),x2034))), % 186.81/186.91 inference(scs_inference,[],[193,7,5,8,6])). % 186.81/186.91 cnf(206,plain, % 186.81/186.91 (E(f5(f1(x2061,f4(x2062)),f1(x2063,f4(x2064))),f5(f5(x2061,x2062),f5(x2063,x2064)))), % 186.81/186.91 inference(scs_inference,[],[193,197,198,7,5,8,6,4,2,3])). % 186.81/186.91 cnf(213,plain, % 186.81/186.91 (E(f5(f4(f1(x2131,f4(x2132))),x2133),f5(f4(f5(x2131,x2132)),x2133))), % 186.81/186.91 inference(scs_inference,[],[194,7,8,5,4,6])). % 186.81/186.91 cnf(214,plain, % 186.81/186.91 (~E(f5(f1(f1(x2141,x2141),f1(x2142,x2142)),f5(a3,f1(x2143,x2143))),f5(f5(f4(a2),a2),a3))), % 186.81/186.91 inference(scs_inference,[],[194,95,175,7,8,5,4,6,3])). % 186.81/186.91 cnf(220,plain, % 186.81/186.91 (E(f4(f1(x2201,f1(x2202,f4(x2203)))),f4(f1(x2201,f5(x2202,x2203))))), % 186.81/186.91 inference(scs_inference,[],[195,7,5,8])). % 186.81/186.91 cnf(221,plain, % 186.81/186.91 (E(f5(f1(x2211,f1(x2212,f4(x2213))),x2214),f5(f1(x2211,f5(x2212,x2213)),x2214))), % 186.81/186.91 inference(scs_inference,[],[195,7,5,8,6])). % 186.81/186.91 cnf(223,plain, % 186.81/186.91 (E(f1(f1(x2231,f4(x2232)),f1(x2233,f4(x2234))),f1(f5(x2231,x2232),f5(x2233,x2234)))), % 186.81/186.91 inference(scs_inference,[],[195,196,7,5,8,6,4,3])). % 186.81/186.91 cnf(226,plain, % 186.81/186.91 (E(f5(x2261,f1(f1(x2262,f4(x2263)),x2264)),f5(x2261,f1(f5(x2262,x2263),x2264)))), % 186.81/186.91 inference(scs_inference,[],[196,7])). % 186.81/186.91 cnf(227,plain, % 186.81/186.91 (E(f4(f1(f1(x2271,f4(x2272)),x2273)),f4(f1(f5(x2271,x2272),x2273)))), % 186.81/186.91 inference(scs_inference,[],[196,7,8])). % 186.81/186.91 cnf(228,plain, % 186.81/186.91 (E(f1(x2281,f1(f1(x2282,f4(x2283)),x2284)),f1(x2281,f1(f5(x2282,x2283),x2284)))), % 186.81/186.91 inference(scs_inference,[],[196,7,8,5])). % 186.81/186.91 cnf(230,plain, % 186.81/186.91 (E(f5(f1(f1(x2301,f4(x2302)),x2303),x2304),f5(f1(f5(x2301,x2302),x2303),x2304))), % 186.81/186.91 inference(scs_inference,[],[196,7,8,5,4,6])). % 186.81/186.91 cnf(235,plain, % 186.81/186.91 (E(f1(x2351,f5(f1(x2352,f4(x2353)),x2354)),f1(x2351,f5(f5(x2352,x2353),x2354)))), % 186.81/186.91 inference(scs_inference,[],[197,7,5])). % 186.81/186.91 cnf(236,plain, % 186.81/186.91 (E(f4(f5(f1(x2361,f4(x2362)),x2363)),f4(f5(f5(x2361,x2362),x2363)))), % 186.81/186.91 inference(scs_inference,[],[197,7,5,8])). % 186.81/186.91 cnf(237,plain, % 186.81/186.91 (E(f5(f5(f1(x2371,f4(x2372)),x2373),x2374),f5(f5(f5(x2371,x2372),x2373),x2374))), % 186.81/186.91 inference(scs_inference,[],[197,7,5,8,6])). % 186.81/186.91 cnf(238,plain, % 186.81/186.91 (E(f1(f5(f1(x2381,f4(x2382)),x2383),x2384),f1(f5(f5(x2381,x2382),x2383),x2384))), % 186.81/186.91 inference(scs_inference,[],[197,7,5,8,6,4])). % 186.81/186.91 cnf(239,plain, % 186.81/186.91 (E(f5(f1(x2391,f4(x2392)),f1(f1(x2393,x2393),f4(x2394))),f5(f5(x2391,x2392),f5(f1(x2395,x2395),x2394)))), % 186.81/186.91 inference(scs_inference,[],[206,145,197,7,5,8,6,4,3])). % 186.81/186.91 cnf(243,plain, % 186.81/186.91 (E(f4(f1(x2431,f4(x2432))),f4(f1(x2431,f1(f1(x2433,x2433),x2432))))), % 186.81/186.91 inference(scs_inference,[],[180,7,8])). % 186.81/186.91 cnf(250,plain, % 186.81/186.91 (~E(f5(f5(f4(a2),a2),a3),f5(f5(f1(x2501,x2501),f1(x2502,x2502)),f5(a3,f1(x2503,x2503))))), % 186.81/186.91 inference(scs_inference,[],[165,214,180,7,8,5,4,6,3,2])). % 186.81/186.91 cnf(251,plain, % 186.81/186.91 (E(f5(x2511,f4(x2512)),f5(x2511,f1(f1(x2513,x2513),x2512)))), % 186.81/186.91 inference(scs_inference,[],[13,7])). % 186.81/186.91 cnf(254,plain, % 186.81/186.91 (E(f5(f4(x2541),x2542),f5(f1(f1(x2543,x2543),x2541),x2542))), % 186.81/186.91 inference(scs_inference,[],[13,7,5,8,6])). % 186.81/186.91 cnf(255,plain, % 186.81/186.91 (E(f1(f4(x2551),x2552),f1(f1(f1(x2553,x2553),x2551),x2552))), % 186.81/186.91 inference(scs_inference,[],[13,7,5,8,6,4])). % 186.81/186.91 cnf(256,plain, % 186.81/186.91 (E(f1(f1(x2561,f4(x2562)),f1(f1(x2563,x2563),f4(x2564))),f1(f5(x2561,x2562),f5(f1(x2565,x2565),x2564)))), % 186.81/186.91 inference(scs_inference,[],[223,91,13,7,5,8,6,4,3])). % 186.81/186.91 cnf(263,plain, % 186.81/186.91 (E(f5(f5(x2631,f4(x2632)),x2633),f5(f5(x2631,f1(f1(x2634,x2634),x2632)),x2633))), % 186.81/186.91 inference(scs_inference,[],[251,254,7,8,5,4,6])). % 186.81/186.91 cnf(267,plain, % 186.81/186.91 (E(f5(f1(f4(x2671),x2672),x2673),f5(f1(f1(f1(x2674,x2674),x2671),x2672),x2673))), % 186.81/186.91 inference(scs_inference,[],[255,7,5,8,6])). % 186.81/186.91 cnf(269,plain, % 186.81/186.91 (E(f1(f4(x2691),f1(x2692,f1(f1(x2693,x2693),x2694))),f1(f1(f1(x2695,x2695),x2691),f5(x2692,x2694)))), % 186.81/186.91 inference(scs_inference,[],[255,163,7,5,8,6,4,3])). % 186.81/186.91 cnf(274,plain, % 186.81/186.91 (E(f5(f5(f4(x2741),x2742),x2743),f5(f5(f1(f1(x2744,x2744),x2741),x2742),x2743))), % 186.81/186.91 inference(scs_inference,[],[254,7,4,6])). % 186.81/186.91 cnf(275,plain, % 186.81/186.91 (~E(f5(f1(f1(f1(x2751,x2751),a2),f1(f1(x2752,x2752),a2)),a3),a3)), % 186.81/186.91 inference(scs_inference,[],[267,150,254,7,4,6,3])). % 186.81/186.91 cnf(278,plain, % 186.81/186.91 (E(f5(f1(f1(x2781,x2781),f4(x2782)),f1(f1(x2783,x2783),f4(x2784))),f5(f5(f1(x2785,x2785),x2782),f5(f1(x2786,x2786),x2784)))), % 186.81/186.91 inference(scs_inference,[],[149,239,275,2,3])). % 186.81/186.91 cnf(284,plain, % 186.81/186.91 (E(f1(f1(f1(x2841,x2841),f4(x2842)),f1(f1(x2843,x2843),f4(x2844))),f1(f5(f1(x2845,x2845),x2842),f5(f1(x2846,x2846),x2844)))), % 186.81/186.91 inference(scs_inference,[],[148,256,3])). % 186.81/186.91 cnf(296,plain, % 186.81/186.91 (~E(f5(f1(f4(a2),f4(a2)),a3),f5(f1(x2961,x2961),f1(a3,f4(f1(x2962,x2962)))))), % 186.81/186.91 inference(scs_inference,[],[115,183,3,2])). % 186.81/186.91 cnf(300,plain, % 186.81/186.91 (E(f1(f1(x3001,x3001),f1(f1(x3002,x3002),f1(f1(x3003,x3003),x3004))),f1(f1(x3005,x3005),f1(f1(x3006,x3006),f4(x3004))))), % 186.81/186.91 inference(scs_inference,[],[43,116,3])). % 186.81/186.91 cnf(306,plain, % 186.81/186.91 (E(f4(f5(f1(x3061,x3061),f1(f1(x3062,x3062),x3063))),f4(f5(f1(x3064,x3064),f4(x3063))))), % 186.81/186.91 inference(scs_inference,[],[92,129,3])). % 186.81/186.91 cnf(309,plain, % 186.81/186.91 (~E(f4(f1(f1(x3091,x3091),a3)),a3)), % 186.81/186.91 inference(scs_inference,[],[20,166,3])). % 186.81/186.91 cnf(311,plain, % 186.81/186.91 (~E(a3,f4(f1(f1(x3111,x3111),a3)))), % 186.81/186.91 inference(scs_inference,[],[20,166,3,2])). % 186.81/186.91 cnf(330,plain, % 186.81/186.91 (~E(f4(f1(f1(x3301,x3301),f5(a3,f1(x3302,x3302)))),f5(f5(f4(a2),a2),a3))), % 186.81/186.91 inference(scs_inference,[],[20,175,3])). % 186.81/186.91 cnf(334,plain, % 186.81/186.91 (E(f5(x3341,f1(f4(x3342),f1(x3341,f1(x3343,x3343)))),f1(f1(f1(x3344,x3344),f1(x3345,x3345)),x3342))), % 186.81/186.91 inference(scs_inference,[],[94,48,3])). % 186.81/186.91 cnf(337,plain, % 186.81/186.91 (~E(f5(x3371,f1(f1(f1(x3372,x3372),f1(f1(x3373,x3373),a3)),f1(x3371,f1(x3374,x3374)))),a3)), % 186.81/186.91 inference(scs_inference,[],[21,309,3])). % 186.81/186.91 cnf(340,plain, % 186.81/186.91 (~E(f1(f1(x3401,x3401),f1(f1(x3402,x3402),a3)),a3)), % 186.81/186.91 inference(scs_inference,[],[72,337,2,3])). % 186.81/186.91 cnf(342,plain, % 186.81/186.91 (~E(a3,f1(f1(x3421,x3421),f1(f1(x3422,x3422),a3)))), % 186.81/186.91 inference(scs_inference,[],[340,2])). % 186.81/186.91 cnf(343,plain, % 186.81/186.91 (~E(f1(f5(f1(f1(x3431,x3431),x3432),x3432),f1(f1(x3433,x3433),a3)),a3)), % 186.81/186.91 inference(scs_inference,[],[340,164,2,3])). % 186.81/186.91 cnf(347,plain, % 186.81/186.91 (~E(f1(f1(f1(f1(x3471,x3471),x3472),f1(f1(x3473,x3473),x3472)),f1(f1(x3474,x3474),a3)),a3)), % 186.81/186.91 inference(scs_inference,[],[343,144,2,3])). % 186.81/186.91 cnf(350,plain, % 186.81/186.91 (~E(f5(x3501,f1(a3,f1(x3501,f1(x3502,x3502)))),f1(f1(x3503,x3503),f1(f1(x3504,x3504),a3)))), % 186.81/186.91 inference(scs_inference,[],[342,347,64,2,3])). % 186.81/186.91 cnf(352,plain, % 186.81/186.91 (~E(f1(f1(x3521,x3521),f1(f1(x3522,x3522),a3)),f5(x3523,f1(a3,f1(x3523,f1(x3524,x3524)))))), % 186.81/186.91 inference(scs_inference,[],[350,2])). % 186.81/186.91 cnf(353,plain, % 186.81/186.91 (~E(f5(x3531,f1(f4(f1(f1(x3532,x3532),a3)),f1(x3531,f1(x3533,x3533)))),a3)), % 186.81/186.91 inference(scs_inference,[],[109,350,337,2,3])). % 186.81/186.91 cnf(356,plain, % 186.81/186.91 (~E(f1(x3561,f1(x3562,f1(a3,f1(x3561,x3562)))),f4(f1(f1(x3563,x3563),a3)))), % 186.81/186.91 inference(scs_inference,[],[311,353,30,2,3])). % 186.81/186.91 cnf(359,plain, % 186.81/186.91 (~E(f1(f1(f1(x3591,x3591),f1(x3592,x3592)),f1(f1(x3593,x3593),a3)),a3)), % 186.81/186.91 inference(scs_inference,[],[334,356,353,2,3])). % 186.81/186.91 cnf(362,plain, % 186.81/186.91 (~E(f1(x3621,f1(x3622,f1(f4(f1(f1(x3623,x3623),a3)),f1(x3621,x3622)))),a3)), % 186.81/186.91 inference(scs_inference,[],[359,45,2,3])). % 186.81/186.91 cnf(366,plain, % 186.81/186.91 (E(f5(x3661,f5(f1(x3662,x3662),x3663)),f5(x3661,f4(f4(x3663))))), % 186.81/186.91 inference(scs_inference,[],[100,170,362,2,3])). % 186.81/186.91 cnf(370,plain, % 186.81/186.91 (~E(f5(f1(f4(a2),f4(a2)),a3),f5(f1(x3701,x3701),f1(a3,f1(f1(x3702,x3702),f1(x3703,x3703)))))), % 186.81/186.91 inference(scs_inference,[],[169,35,3,2])). % 186.81/186.91 cnf(371,plain, % 186.81/186.91 (E(f5(f1(f1(x3711,x3711),f1(f1(x3712,x3712),x3713)),f1(f1(x3714,x3714),x3715)),f5(f4(f4(x3713)),f4(x3715)))), % 186.81/186.91 inference(scs_inference,[],[106,103,3])). % 186.81/186.91 cnf(381,plain, % 186.81/186.91 (~E(f1(f5(f1(f1(x3811,x3811),x3812),x3812),f1(f4(f1(x3813,x3813)),a3)),a3)), % 186.81/186.91 inference(scs_inference,[],[111,343,3])). % 186.81/186.91 cnf(388,plain, % 186.81/186.91 (~E(f1(f5(f4(x3881),x3881),f1(f4(f1(x3882,x3882)),a3)),a3)), % 186.81/186.91 inference(scs_inference,[],[124,381,3])). % 186.81/186.91 cnf(392,plain, % 186.81/186.91 (E(f4(f1(f1(x3921,x3921),f1(x3922,f4(x3923)))),f4(f1(f1(x3924,x3924),f5(x3922,x3923))))), % 186.81/186.91 inference(scs_inference,[],[388,220,28,2,3])). % 186.81/186.91 cnf(395,plain, % 186.81/186.91 (~E(f1(f1(x3951,x3951),f1(f1(x3952,x3952),f5(a3,f1(x3953,x3953)))),f5(f5(f4(a2),a2),a3))), % 186.81/186.91 inference(scs_inference,[],[330,41,3])). % 186.81/186.91 cnf(399,plain, % 186.81/186.91 (E(f5(f1(x3991,x3991),f5(f1(x3992,x3992),f1(x3993,x3993))),f4(f1(x3994,x3994)))), % 186.81/186.91 inference(scs_inference,[],[24,395,135,2,3])). % 186.81/186.91 cnf(402,plain, % 186.81/186.91 (E(f5(x4021,f5(f1(x4022,x4022),f5(f1(x4023,x4023),f1(x4024,x4024)))),f5(x4021,f4(f1(x4025,x4025))))), % 186.81/186.91 inference(scs_inference,[],[24,395,135,2,3,7])). % 186.81/186.91 cnf(403,plain, % 186.81/186.91 (E(f4(f5(f1(x4031,x4031),f5(f1(x4032,x4032),f1(x4033,x4033)))),f4(f4(f1(x4034,x4034))))), % 186.81/186.91 inference(scs_inference,[],[24,395,135,2,3,7,8])). % 186.81/186.91 cnf(413,plain, % 186.81/186.91 (~E(f1(f1(x4131,x4131),f1(f1(x4132,x4132),a3)),f5(f1(x4133,x4133),f1(a3,f1(f1(x4134,x4134),f1(x4135,x4135)))))), % 186.81/186.91 inference(scs_inference,[],[25,370,3])). % 186.81/186.91 cnf(423,plain, % 186.81/186.91 (~E(f1(f1(x4231,x4231),f1(f1(x4232,x4232),a3)),f5(f1(x4233,x4233),f1(a3,f4(f1(x4234,x4234)))))), % 186.81/186.91 inference(scs_inference,[],[25,296,3])). % 186.81/186.91 cnf(429,plain, % 186.81/186.91 (~E(f1(f5(f1(f1(x4291,x4291),f1(f1(x4292,x4292),x4293)),f4(x4293)),f1(f1(x4294,x4294),a3)),a3)), % 186.81/186.91 inference(scs_inference,[],[131,343,3])). % 186.81/186.91 cnf(450,plain, % 186.81/186.91 (~E(f5(f1(x4501,x4501),a3),f5(x4502,f1(a3,f1(x4502,f1(x4503,x4503)))))), % 186.81/186.91 inference(scs_inference,[],[27,352,3])). % 186.81/186.91 cnf(453,plain, % 186.81/186.91 (~E(f5(x4531,f1(a3,f1(x4531,f1(x4532,x4532)))),f5(f1(x4533,x4533),a3))), % 186.81/186.91 inference(scs_inference,[],[27,352,3,2])). % 186.81/186.91 cnf(457,plain, % 186.81/186.91 (~E(f5(f1(x4571,x4571),a3),f5(f1(x4572,x4572),f1(a3,f1(f1(x4573,x4573),f1(x4574,x4574)))))), % 186.81/186.91 inference(scs_inference,[],[27,413,3])). % 186.81/186.91 cnf(460,plain, % 186.81/186.91 (~E(f5(f1(x4601,x4601),f1(a3,f1(f1(x4602,x4602),f1(x4603,x4603)))),f5(f1(x4604,x4604),a3))), % 186.81/186.91 inference(scs_inference,[],[27,413,3,2])). % 186.81/186.91 cnf(466,plain, % 186.81/186.91 (~E(f5(f1(x4661,x4661),f1(a3,f4(f1(x4662,x4662)))),f5(f1(x4663,x4663),a3))), % 186.81/186.91 inference(scs_inference,[],[27,423,3,2])). % 186.81/186.91 cnf(467,plain, % 186.81/186.91 (E(f1(f1(x4671,x4671),f1(f1(x4672,x4672),f1(f1(x4673,x4673),x4674))),f5(f1(x4675,x4675),f4(x4674)))), % 186.81/186.91 inference(scs_inference,[],[27,300,3])). % 186.81/186.91 cnf(477,plain, % 186.81/186.91 (~E(f5(f1(x4771,x4771),a3),a3)), % 186.81/186.91 inference(scs_inference,[],[27,340,3])). % 186.81/186.91 cnf(481,plain, % 186.81/186.91 (~E(f5(f1(f4(x4811),f1(f1(x4812,x4812),x4811)),a3),a3)), % 186.81/186.91 inference(scs_inference,[],[477,113,3])). % 186.81/186.91 cnf(485,plain, % 186.81/186.91 (~E(f5(f1(f4(f4(x4851)),f5(f1(x4852,x4852),x4851)),a3),a3)), % 186.81/186.91 inference(scs_inference,[],[481,221,2,3])). % 186.81/186.91 cnf(489,plain, % 186.81/186.91 (E(f1(f1(x4891,x4891),f1(f1(x4892,x4892),f1(f1(x4893,x4893),x4894))),f5(f5(f1(x4895,x4895),f1(x4896,x4896)),f4(x4894)))), % 186.81/186.91 inference(scs_inference,[],[467,485,156,2,3])). % 186.81/186.91 cnf(492,plain, % 186.81/186.91 (~E(f5(f1(f5(x4921,x4922),f1(x4921,f4(x4922))),a3),a3)), % 186.81/186.91 inference(scs_inference,[],[230,477,3])). % 186.81/186.91 cnf(496,plain, % 186.81/186.91 (E(f1(f1(x4961,x4961),f1(f1(x4962,x4962),f1(f1(x4963,x4963),x4964))),f5(f5(f4(f1(x4965,x4965)),f1(x4966,x4966)),f4(x4964)))), % 186.81/186.91 inference(scs_inference,[],[489,125,3])). % 186.81/186.91 cnf(499,plain, % 186.81/186.91 (~E(f5(f5(f5(f1(x4991,x4991),x4992),f4(x4992)),a3),a3)), % 186.81/186.91 inference(scs_inference,[],[492,165,3])). % 186.81/186.91 cnf(506,plain, % 186.81/186.91 (~E(f5(f5(f5(f1(x5061,x5061),x5062),f1(f1(x5063,x5063),x5062)),a3),a3)), % 186.81/186.91 inference(scs_inference,[],[499,263,3])). % 186.81/186.91 cnf(510,plain, % 186.81/186.91 (E(f4(f5(f1(x5101,x5101),f5(f1(x5102,x5102),f1(x5103,x5103)))),f4(f5(f1(x5104,x5104),f1(x5105,x5105))))), % 186.81/186.91 inference(scs_inference,[],[506,146,403,2,3])). % 186.81/186.91 cnf(521,plain, % 186.81/186.91 (~E(f5(f1(f1(f1(x5211,x5211),f4(x5212)),f5(f1(x5213,x5213),x5212)),a3),a3)), % 186.81/186.91 inference(scs_inference,[],[485,267,3])). % 186.81/186.91 cnf(524,plain, % 186.81/186.91 (E(f4(f1(f1(x5241,x5241),f4(x5242))),f4(f1(f1(x5243,x5243),f1(f1(x5244,x5244),x5242))))), % 186.81/186.91 inference(scs_inference,[],[28,521,243,2,3])). % 186.81/186.91 cnf(533,plain, % 186.81/186.92 (~E(f1(x5331,f1(x5332,f1(a3,f1(x5331,x5332)))),f1(f1(x5333,x5333),f1(f1(x5334,x5334),a3)))), % 186.81/186.92 inference(scs_inference,[],[30,342,3])). % 186.81/186.92 cnf(535,plain, % 186.81/186.92 (~E(f1(f1(x5351,x5351),f1(f1(x5352,x5352),a3)),f1(x5353,f1(x5354,f1(a3,f1(x5353,x5354)))))), % 186.81/186.92 inference(scs_inference,[],[30,342,3,2])). % 186.81/186.92 cnf(536,plain, % 186.81/186.92 (~E(f5(f5(f4(x5361),x5361),f5(a3,f1(x5362,x5362))),f5(f1(x5363,x5363),a3))), % 186.81/186.92 inference(scs_inference,[],[466,206,3])). % 186.81/186.92 cnf(539,plain, % 186.81/186.92 (~E(f5(f1(x5391,x5391),a3),f5(f5(f4(x5392),x5392),f5(a3,f1(x5393,x5393))))), % 186.81/186.92 inference(scs_inference,[],[466,206,3,2])). % 186.81/186.92 cnf(543,plain, % 186.81/186.92 (~E(f5(f5(f4(x5431),x5431),f1(a3,f1(f1(x5432,x5432),f1(x5433,x5433)))),f5(f1(x5434,x5434),a3))), % 186.81/186.92 inference(scs_inference,[],[536,140,3])). % 186.81/186.92 cnf(546,plain, % 186.81/186.92 (~E(f1(x5461,f1(x5462,f1(f1(f1(x5463,x5463),f1(f1(x5464,x5464),a3)),f1(x5461,x5462)))),a3)), % 186.81/186.92 inference(scs_inference,[],[30,340,3])). % 186.81/186.92 cnf(549,plain, % 186.81/186.92 (~E(f5(f1(f1(x5491,x5491),f1(x5492,x5492)),a3),f5(f5(f4(x5493),x5493),f5(a3,f1(x5494,x5494))))), % 186.81/186.92 inference(scs_inference,[],[539,546,95,2,3])). % 186.81/186.92 cnf(574,plain, % 186.81/186.92 (~E(f5(f1(f4(f1(x5741,x5741)),f1(x5742,x5742)),a3),f5(f5(f4(x5743),x5743),f5(a3,f1(x5744,x5744))))), % 186.81/186.92 inference(scs_inference,[],[549,113,3])). % 186.81/186.92 cnf(594,plain, % 186.81/186.92 (~E(f5(f5(f4(f1(x5941,x5941)),f1(x5942,x5942)),a3),f5(f5(f4(x5943),x5943),f5(a3,f1(x5944,x5944))))), % 186.81/186.92 inference(scs_inference,[],[574,165,3])). % 186.81/186.92 cnf(628,plain, % 186.81/186.92 (~E(f5(x6281,f1(a3,f1(x6281,f1(x6282,x6282)))),f5(f1(f1(x6283,x6283),f1(x6284,x6284)),a3))), % 186.81/186.92 inference(scs_inference,[],[450,95,3,2])). % 186.81/186.92 cnf(629,plain, % 186.81/186.92 (E(f4(f1(f1(x6291,x6291),f4(x6292))),f4(f5(f1(x6293,x6293),x6292)))), % 186.81/186.92 inference(scs_inference,[],[524,162,3])). % 186.81/186.92 cnf(635,plain, % 186.81/186.92 (~E(f5(f1(x6351,x6351),f5(a3,f1(x6352,x6352))),f5(f1(x6353,x6353),a3))), % 186.81/186.92 inference(scs_inference,[],[460,161,3])). % 186.81/186.92 cnf(637,plain, % 186.81/186.92 (~E(f5(f1(x6371,x6371),a3),f5(f1(x6372,x6372),f5(a3,f1(x6373,x6373))))), % 186.81/186.92 inference(scs_inference,[],[460,161,3,2])). % 186.81/186.92 cnf(641,plain, % 186.81/186.92 (~E(f5(f1(f4(x6411),f1(f1(x6412,x6412),x6411)),a3),f5(f1(x6413,x6413),f5(a3,f1(x6414,x6414))))), % 186.81/186.92 inference(scs_inference,[],[637,113,3])). % 186.81/186.92 cnf(651,plain, % 186.81/186.92 (~E(f5(f1(x6511,x6511),f1(a3,f1(f1(x6512,x6512),f1(x6513,x6513)))),f5(f5(f1(x6514,x6514),f1(x6515,x6515)),a3))), % 186.81/186.92 inference(scs_inference,[],[457,156,3,2])). % 186.81/186.92 cnf(652,plain, % 186.81/186.92 (E(f5(f1(x6521,x6521),f1(f1(x6522,f4(x6523)),f1(f1(x6524,x6524),f1(x6525,x6525)))),f5(x6522,x6523))), % 186.81/186.92 inference(scs_inference,[],[38,226,3])). % 186.81/186.92 cnf(658,plain, % 186.81/186.92 (~E(f5(f1(f1(x6581,x6581),f1(x6582,x6582)),a3),a3)), % 186.81/186.92 inference(scs_inference,[],[38,628,3,2])). % 186.81/186.92 cnf(662,plain, % 186.81/186.92 (~E(f5(f1(f1(x6621,x6621),f5(f4(x6622),x6622)),a3),a3)), % 186.81/186.92 inference(scs_inference,[],[658,221,3])). % 186.81/186.92 cnf(678,plain, % 186.81/186.92 (~E(f5(f5(f1(x6781,x6781),f1(x6782,x6782)),a3),a3)), % 186.81/186.92 inference(scs_inference,[],[38,651,3,2])). % 186.81/186.92 cnf(702,plain, % 186.81/186.92 (~E(f5(f1(f1(x7021,x7021),f1(f1(x7022,x7022),f1(x7023,x7023))),a3),a3)), % 186.81/186.92 inference(scs_inference,[],[139,678,3])). % 186.81/186.92 cnf(713,plain, % 186.81/186.92 (E(f1(f1(x7131,x7131),f5(x7132,x7133)),f4(f1(x7132,f4(x7133))))), % 186.81/186.92 inference(scs_inference,[],[158,117,3])). % 186.81/186.92 cnf(719,plain, % 186.81/186.92 (E(f5(f1(f1(x7191,x7191),f5(x7192,x7193)),x7194),f5(f4(f1(x7192,f4(x7193))),x7194))), % 186.81/186.92 inference(scs_inference,[],[158,117,3,7,5,8,4,6])). % 186.81/186.92 cnf(720,plain, % 186.81/186.92 (~E(f5(f4(f1(f4(x7201),f4(x7201))),a3),a3)), % 186.81/186.92 inference(scs_inference,[],[719,662,3])). % 186.81/186.92 cnf(724,plain, % 186.81/186.92 (E(f1(f1(x7241,x7241),f5(f1(x7242,x7242),x7243)),f1(f1(x7244,x7244),f1(f1(x7245,x7245),f4(x7243))))), % 186.81/186.92 inference(scs_inference,[],[41,713,720,2,3])). % 186.81/186.92 cnf(727,plain, % 186.81/186.92 (~E(f5(f4(f5(f4(x7271),x7271)),a3),a3)), % 186.81/186.92 inference(scs_inference,[],[213,720,3])). % 186.81/186.92 cnf(742,plain, % 186.81/186.92 (~E(f5(f1(x7421,x7421),f5(a3,f1(x7422,x7422))),f5(f5(f4(x7423),x7423),a3))), % 186.81/186.92 inference(scs_inference,[],[641,165,3,2])). % 186.81/186.92 cnf(746,plain, % 186.81/186.92 (~E(f5(f1(x7461,x7461),f1(a3,f1(f1(x7462,x7462),f1(x7463,x7463)))),f5(f5(f4(x7464),x7464),a3))), % 186.81/186.92 inference(scs_inference,[],[742,140,3])). % 186.81/186.92 cnf(759,plain, % 186.81/186.92 (~E(f1(f1(f1(x7591,x7591),f1(f1(x7592,x7592),f1(x7593,x7593))),f1(f1(x7594,x7594),a3)),a3)), % 186.81/186.92 inference(scs_inference,[],[42,702,3])). % 186.81/186.92 cnf(762,plain, % 186.81/186.92 (~E(f1(f4(f5(f4(x7621),x7621)),f1(f1(x7622,x7622),a3)),a3)), % 186.81/186.92 inference(scs_inference,[],[42,759,727,2,3])). % 186.81/186.92 cnf(765,plain, % 186.81/186.92 (~E(f1(f4(f5(f4(x7651),x7651)),f1(f5(f4(x7652),x7652),a3)),a3)), % 186.81/186.92 inference(scs_inference,[],[762,228,2,3])). % 186.81/186.92 cnf(769,plain, % 186.81/186.92 (E(f1(f1(x7691,x7691),f5(f1(x7692,x7692),x7693)),f4(f5(f1(x7694,x7694),x7693)))), % 186.81/186.92 inference(scs_inference,[],[765,713,629,2,3])). % 186.81/186.92 cnf(778,plain, % 186.81/186.92 (~E(f5(f5(f1(x7781,x7781),f1(x7782,x7782)),f5(a3,f1(x7783,x7783))),f1(f5(f4(a2),a2),f1(f1(x7784,x7784),a3)))), % 186.81/186.92 inference(scs_inference,[],[42,250,3,2])). % 186.81/186.92 cnf(797,plain, % 186.81/186.92 (~E(f5(f5(f4(x7971),x7971),a3),a3)), % 186.81/186.92 inference(scs_inference,[],[746,67,3,2])). % 186.81/186.92 cnf(804,plain, % 186.81/186.92 (~E(f5(f5(f5(f4(x8041),x8041),f1(x8042,x8042)),f5(a3,f1(x8043,x8043))),f1(f5(f4(a2),a2),f1(f1(x8044,x8044),a3)))), % 186.81/186.92 inference(scs_inference,[],[778,237,3])). % 186.81/186.92 cnf(808,plain, % 186.81/186.92 (~E(f5(f1(x8081,x8081),f5(a3,f5(f4(x8082),x8082))),f5(f1(x8083,x8083),a3))), % 186.81/186.92 inference(scs_inference,[],[804,635,200,2,3])). % 186.81/186.92 cnf(815,plain, % 186.81/186.92 (~E(f1(f4(f1(f1(x8151,x8151),f4(f1(x8152,x8152)))),f1(f1(x8153,x8153),a3)),a3)), % 186.81/186.92 inference(scs_inference,[],[174,429,3])). % 186.81/186.92 cnf(822,plain, % 186.81/186.92 (~E(f1(f4(f4(f4(f1(x8221,x8221)))),f1(f1(x8222,x8222),a3)),a3)), % 186.81/186.92 inference(scs_inference,[],[104,815,3])). % 186.81/186.92 cnf(826,plain, % 186.81/186.92 (E(f5(f1(x8261,x8261),f5(f1(x8262,x8262),f1(x8263,x8263))),f5(f4(x8264),x8264))), % 186.81/186.92 inference(scs_inference,[],[652,822,135,2,3])). % 186.81/186.92 cnf(851,plain, % 186.81/186.92 (E(f1(f4(x8511),f5(f1(x8512,x8512),x8513)),f1(f1(f1(x8514,x8514),x8511),f5(f1(x8515,x8515),x8513)))), % 186.81/186.92 inference(scs_inference,[],[269,137,3])). % 186.81/186.92 cnf(867,plain, % 186.81/186.92 (~E(f5(f5(f4(f1(f1(x8671,x8671),x8672)),f4(x8672)),a3),a3)), % 186.81/186.92 inference(scs_inference,[],[797,130,3])). % 186.81/186.92 cnf(880,plain, % 186.81/186.92 (~E(f5(f5(f4(f1(x8801,f4(x8802))),f5(x8801,x8802)),a3),a3)), % 186.81/186.92 inference(scs_inference,[],[797,203,3])). % 186.81/186.92 cnf(893,plain, % 186.81/186.92 (~E(f5(f1(f4(f1(f1(x8931,x8931),x8932)),f1(f1(x8933,x8933),f4(x8932))),a3),a3)), % 186.81/186.92 inference(scs_inference,[],[867,143,3])). % 186.81/186.92 cnf(918,plain, % 186.81/186.92 (~E(f5(f1(f4(f1(x9181,f4(x9182))),f1(f1(x9183,x9183),f5(x9181,x9182))),a3),a3)), % 186.81/186.92 inference(scs_inference,[],[880,143,3])). % 186.81/186.92 cnf(931,plain, % 186.81/186.92 (~E(f5(f1(f4(f1(f1(x9311,x9311),x9312)),f5(f1(x9313,x9313),x9312)),a3),a3)), % 186.81/186.92 inference(scs_inference,[],[893,221,3])). % 186.81/186.92 cnf(935,plain, % 186.81/186.92 (~E(f5(f5(f4(x9351),x9351),f1(a3,f4(f1(x9352,x9352)))),f5(f1(x9353,x9353),a3))), % 186.81/186.92 inference(scs_inference,[],[543,931,115,2,3])). % 186.81/186.92 cnf(938,plain, % 186.81/186.92 (~E(f5(f1(f1(f1(x9381,x9381),f1(x9382,f4(x9383))),f1(f1(x9384,x9384),f5(x9382,x9383))),a3),a3)), % 186.81/186.92 inference(scs_inference,[],[935,918,267,2,3])). % 186.81/186.92 cnf(941,plain, % 186.81/186.92 (E(f1(f1(x9411,x9411),f1(f1(x9412,x9412),f1(f1(x9413,x9413),x9414))),f1(f1(x9415,x9415),f5(f1(x9416,x9416),x9414)))), % 186.81/186.92 inference(scs_inference,[],[52,154,938,2,3])). % 186.81/186.92 cnf(989,plain, % 186.81/186.92 (~E(f1(x9891,f1(a3,f1(f1(x9892,x9892),x9891))),f1(f1(x9893,x9893),a3))), % 186.81/186.92 inference(scs_inference,[],[533,5])). % 186.81/186.92 cnf(994,plain, % 186.81/186.92 (E(f5(x9941,f4(x9942)),f1(x9941,f5(f1(x9943,x9943),x9942)))), % 186.81/186.92 inference(scs_inference,[],[42,195,453,533,5,2,7,3])). % 186.81/186.92 cnf(1002,plain, % 186.81/186.92 (E(f5(f1(x10021,f4(x10022)),x10023),f1(f5(x10021,x10022),f1(f1(x10024,x10024),x10023)))), % 186.81/186.92 inference(scs_inference,[],[42,196,466,535,5,2,7,3])). % 186.81/186.92 cnf(1021,plain, % 186.81/186.92 (E(f1(x10211,f1(f1(x10212,x10212),f1(x10213,f4(x10214)))),f5(x10211,f5(x10213,x10214)))), % 186.81/186.92 inference(scs_inference,[],[10,193,191,808,7,2,3])). % 186.81/186.92 cnf(1027,plain, % 186.81/186.92 (E(f1(f1(x10271,f4(x10272)),f1(f1(x10273,x10273),x10274)),f5(f5(x10271,x10272),x10274))), % 186.81/186.92 inference(scs_inference,[],[10,197,371,594,2,7,3])). % 186.81/186.92 cnf(1100,plain, % 186.81/186.92 (E(f1(f1(x11001,f1(x11002,f4(x11003))),f1(f1(x11004,x11004),x11005)),f5(f1(x11001,f5(x11002,x11003)),x11005))), % 186.81/186.92 inference(scs_inference,[],[10,221,227,2,3])). % 186.81/186.92 cnf(1116,plain, % 186.81/186.92 (E(f1(f1(x11161,f1(f1(x11162,x11162),x11163)),f1(f1(x11164,x11164),x11165)),f5(f5(x11161,x11163),x11165))), % 186.81/186.92 inference(scs_inference,[],[10,165,629,2,3])). % 186.81/186.92 cnf(1122,plain, % 186.81/186.92 (E(f4(f1(x11221,f4(x11222))),f1(f1(x11223,x11223),f5(x11221,x11222)))), % 186.81/186.92 inference(scs_inference,[],[713,2])). % 186.81/186.92 cnf(1123,plain, % 186.81/186.92 (E(f1(f1(x11231,x11231),f1(f1(x11232,x11232),f5(f1(x11233,x11233),f1(x11234,x11234)))),f4(f1(x11235,x11235)))), % 186.81/186.92 inference(scs_inference,[],[10,399,713,2,3])). % 186.81/186.92 cnf(1129,plain, % 186.81/186.92 (E(f4(f1(x11291,f1(f1(x11292,x11292),x11293))),f1(f1(x11294,x11294),f5(x11291,x11293)))), % 186.81/186.92 inference(scs_inference,[],[158,2])). % 186.81/186.92 cnf(1212,plain, % 186.81/186.92 (E(f4(f1(f1(x12121,x12121),x12122)),f1(f1(x12123,x12123),f4(x12122)))), % 186.81/186.92 inference(scs_inference,[],[13,85,278,2,3])). % 186.81/186.92 cnf(1216,plain, % 186.81/186.92 (E(f1(f4(x12161),f1(f1(x12162,x12162),f4(x12163))),f1(f1(f1(x12164,x12164),x12161),f5(f1(x12165,x12165),x12163)))), % 186.81/186.92 inference(scs_inference,[],[195,851,284,2,3])). % 186.81/186.92 cnf(1224,plain, % 186.81/186.92 (E(f4(f1(x12241,f1(x12242,f1(f1(x12243,x12243),x12241)))),x12242)), % 186.81/186.92 inference(scs_inference,[],[13,11,306,2,3])). % 186.81/186.92 cnf(1236,plain, % 186.81/186.92 (E(f4(f1(x12361,f4(x12362))),f1(f5(f4(x12363),x12363),f5(x12361,x12362)))), % 186.81/186.92 inference(scs_inference,[],[13,223,402,2,3])). % 186.81/186.92 cnf(1260,plain, % 186.81/186.92 (E(f1(f1(x12601,x12601),f1(f1(x12602,x12602),f5(f1(x12603,x12603),f1(x12604,x12604)))),f5(f4(x12605),x12605))), % 186.81/186.92 inference(scs_inference,[],[10,826,510,2,3])). % 186.81/186.92 cnf(1270,plain, % 186.81/186.92 (E(f1(f1(x12701,x12701),f1(f1(x12702,x12702),f4(x12703))),f1(f1(x12704,x12704),f5(f1(x12705,x12705),x12703)))), % 186.81/186.92 inference(scs_inference,[],[724,2])). % 186.81/186.92 cnf(1315,plain, % 186.81/186.92 (E(f4(f5(f1(x13151,f4(x13152)),x13153)),f1(f1(x13154,x13154),f5(f5(x13151,x13152),x13153)))), % 186.81/186.92 inference(scs_inference,[],[13,235,496,2,3])). % 186.81/186.92 cnf(1319,plain, % 186.81/186.92 (E(f1(f1(x13191,x13191),f5(f1(x13192,f4(x13193)),x13194)),f4(f5(f5(x13192,x13193),x13194)))), % 186.81/186.92 inference(scs_inference,[],[9,236,1021,2,3])). % 186.81/186.92 cnf(1322,plain, % 186.81/186.92 (E(f5(f5(f1(x13221,f4(x13222)),x13223),x13224),f1(f5(f5(x13221,x13222),x13223),f1(f1(x13225,x13225),x13224)))), % 186.81/186.92 inference(scs_inference,[],[42,238,1027,2,3])). % 186.81/186.92 cnf(1535,plain, % 186.81/186.92 (E(f1(x15351,f1(f1(x15352,x15352),f4(f1(f1(x15353,x15353),x15354)))),f5(x15351,f4(f4(x15354))))), % 186.81/186.92 inference(scs_inference,[],[10,100,941,2,3])). % 186.81/186.92 cnf(1584,plain, % 186.81/186.92 (E(f1(x15841,f5(f1(x15842,x15842),x15843)),f5(x15841,f4(x15843)))), % 186.81/186.92 inference(scs_inference,[],[994,2])). % 186.81/186.92 cnf(1714,plain, % 186.81/186.92 (E(f1(x17141,f1(f1(x17142,x17142),f4(x17143))),f1(x17141,f5(f1(x17144,x17144),x17143)))), % 186.81/186.92 inference(scs_inference,[],[10,994,1315,2,3])). % 186.81/186.92 cnf(1718,plain, % 186.81/186.92 (E(f1(f1(x17181,f4(x17182)),f1(f1(x17183,x17183),x17184)),f1(f5(x17181,x17182),f1(f1(x17185,x17185),x17184)))), % 186.81/186.92 inference(scs_inference,[],[10,1002,1319,2,3])). % 186.81/186.92 cnf(1722,plain, % 186.81/186.92 (E(f4(f1(f1(x17221,x17221),x17222)),f5(f1(f1(x17223,f4(x17224)),f5(x17223,x17224)),x17222))), % 186.81/186.92 inference(scs_inference,[],[13,1100,1322,2,3])). % 186.81/186.92 cnf(1764,plain, % 186.81/186.92 (E(f5(f4(x17641),f4(x17642)),f1(f1(f1(x17643,x17643),x17641),f5(f1(x17644,x17644),x17642)))), % 186.81/186.92 inference(scs_inference,[],[42,1216,1535,2,3])). % 186.81/186.92 cnf(1908,plain, % 186.81/186.92 (E(f4(f1(f1(x19081,x19081),f4(x19082))),f1(f1(x19083,x19083),f5(f1(x19084,x19084),x19082)))), % 186.81/186.92 inference(scs_inference,[],[13,274,1714,1718,2,7,3])). % 186.81/186.92 cnf(1912,plain, % 186.81/186.92 (E(f5(x19121,f5(f1(f1(x19122,x19122),x19123),f1(f1(x19124,x19124),x19125))),f5(x19121,f5(f4(x19123),f4(x19125))))), % 186.81/186.92 inference(scs_inference,[],[106,1722,2,7])). % 186.81/186.92 cnf(1951,plain, % 186.81/186.92 (E(f1(f1(x19511,x19511),f1(x19512,f4(x19513))),f1(f1(x19514,x19514),f5(x19512,x19513)))), % 186.81/186.92 inference(scs_inference,[],[9,200,1122,1764,2,7,3])). % 186.81/186.92 cnf(1955,plain, % 186.81/186.92 (E(f4(f1(f1(x19551,x19551),f5(f1(x19552,x19552),f1(x19553,x19553)))),f4(f1(x19554,x19554)))), % 186.81/186.92 inference(scs_inference,[],[13,220,1123,1951,2,7,3])). % 186.81/186.92 cnf(1960,plain, % 186.81/186.92 (E(f1(f1(x19601,x19601),f1(x19602,f1(f1(x19603,x19603),x19604))),f1(f1(x19605,x19605),f5(x19602,x19604)))), % 186.81/186.92 inference(scs_inference,[],[9,227,1129,1955,2,7,3])). % 186.81/186.92 cnf(1964,plain, % 186.81/186.92 (E(f1(f1(x19641,x19641),f1(f1(x19642,x19642),x19643)),f1(f1(x19644,x19644),f4(x19643)))), % 186.81/186.92 inference(scs_inference,[],[9,237,1212,1960,2,7,3])). % 186.81/186.92 cnf(1968,plain, % 186.81/186.92 (E(f4(f1(f1(x19681,x19681),f5(f1(x19682,x19682),f1(x19683,x19683)))),f5(f4(x19684),x19684))), % 186.81/186.92 inference(scs_inference,[],[13,366,1260,1964,2,7,3])). % 186.81/186.92 cnf(1973,plain, % 186.81/186.92 (E(f4(f5(f1(x19731,x19731),x19732)),f5(f1(x19733,x19733),f4(x19732)))), % 186.81/186.92 inference(scs_inference,[],[13,392,1584,1968,2,7,3])). % 186.81/186.92 cnf(2259,plain, % 186.81/186.92 (E(f1(x22591,f1(x22592,f1(x22593,f1(x22594,f1(x22592,x22593))))),f1(x22591,x22594))), % 186.81/186.92 inference(scs_inference,[],[11,724,1908,2,7,5])). % 186.81/186.92 cnf(2268,plain, % 186.81/186.92 (E(f1(x22681,f5(x22682,f1(f1(f1(x22683,x22683),x22684),f1(x22682,f1(x22685,x22685))))),f1(x22681,f4(x22684)))), % 186.81/186.92 inference(scs_inference,[],[24,16,1912,2,7,5])). % 186.81/186.92 cnf(2272,plain, % 186.81/186.92 (E(f4(f1(x22721,f1(x22722,f1(x22723,f1(x22721,x22722))))),f1(f1(x22724,x22724),x22723))), % 186.81/186.92 inference(scs_inference,[],[13,629,24,16,2259,1912,2,7,5,4,8,6,3])). % 186.81/186.92 cnf(2281,plain, % 186.81/186.92 (E(f4(f5(x22811,f1(f1(f1(x22812,x22812),x22813),f1(x22811,f1(x22814,x22814))))),f1(f1(x22815,x22815),f4(x22813)))), % 186.81/186.92 inference(scs_inference,[],[13,769,223,67,2268,2,7,5,4,8,6,3])). % 186.81/186.92 cnf(2290,plain, % 186.81/186.92 (E(f1(f1(x22901,x22901),f1(x22902,f1(x22903,f1(x22904,f1(x22902,x22903))))),f1(f1(x22905,x22905),x22904))), % 186.81/186.92 inference(scs_inference,[],[9,38,28,14,2272,2,7,5,4,8,6,3])). % 186.81/186.92 cnf(2296,plain, % 186.81/186.92 (E(f5(f1(x22961,f1(x22962,f1(x22963,f1(x22961,x22962)))),x22964),f5(x22963,x22964))), % 186.81/186.92 inference(scs_inference,[],[11,95,1027,2281,2,7,5,4,6])). % 186.81/186.92 cnf(2297,plain, % 186.81/186.92 (E(f4(f1(x22971,f1(x22972,f1(x22973,f1(x22971,x22972))))),f4(x22973))), % 186.81/186.92 inference(scs_inference,[],[11,95,1027,2281,2,7,5,4,6,8])). % 186.81/186.92 cnf(2304,plain, % 186.81/186.92 (E(f1(f5(x23041,f1(f1(f1(x23042,x23042),x23043),f1(x23041,f1(x23044,x23044)))),x23045),f1(f4(x23043),x23045))), % 186.81/186.92 inference(scs_inference,[],[24,724,1116,2290,2,7,5,4])). % 186.81/186.92 cnf(2315,plain, % 186.81/186.92 (E(f1(f1(x23151,f1(x23152,f1(x23153,f1(x23151,x23152)))),f1(f1(x23154,x23154),x23155)),f5(x23153,x23155))), % 186.81/186.92 inference(scs_inference,[],[10,223,16,1236,2296,2304,2,7,5,4,6,8,3])). % 186.81/186.92 cnf(2324,plain, % 186.81/186.92 (E(f1(f1(x23241,x23241),f1(x23242,f1(x23243,f1(x23244,f1(x23242,x23243))))),f4(x23244))), % 186.81/186.92 inference(scs_inference,[],[9,28,67,1973,2297,2315,2,7,5,4,6,8,3])). % 186.81/186.92 cnf(2469,plain, % 186.81/186.92 ($false), % 186.81/186.92 inference(scs_inference,[],[2324,1270,1224,989,8,6,4,5,7,3]), % 186.81/186.92 ['proof']). % 186.81/186.92 % SZS output end Proof % 186.81/186.92 % Total time :186.040000s %------------------------------------------------------------------------------