%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : GRP526-1 : TPTP v8.2.0. Released v2.6.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n024.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:51 EDT 2024 % Result : Unsatisfiable 200.96s 201.17s % Output : CNFRefutation 201.05s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.13 % Problem : GRP526-1 : TPTP v8.2.0. Released v2.6.0. % 0.08/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n024.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Thu Jun 20 12:38:39 EDT 2024 % 0.13/0.34 % CPUTime : % 0.48/0.56 start to proof:theBenchmark % 200.88/201.12 %------------------------------------------- % 200.88/201.12 % File :CSE---1.7 % 200.88/201.12 % Problem :theBenchmark % 200.88/201.12 % Transform :cnf % 200.88/201.12 % Format :tptp:raw % 200.88/201.12 % Command :java -jar mcs_scs.jar %d %s % 200.88/201.12 % 200.88/201.12 % Result :Theorem 200.280000s % 200.88/201.12 % Output :CNFRefutation 200.280000s % 200.88/201.12 %------------------------------------------- % 200.96/201.16 %-------------------------------------------------------------------------- % 200.96/201.16 % File : GRP526-1 : TPTP v8.2.0. Released v2.6.0. % 200.96/201.16 % Domain : Group Theory (Abelian) % 200.96/201.16 % Problem : Axiom for Abelian group theory, in division, part 2 % 200.96/201.16 % Version : [McC93] (equality) axioms. % 200.96/201.16 % English : % 200.96/201.16 % 200.96/201.16 % Refs : [McC93] McCune (1993), Single Axioms for Groups and Abelian Gr % 200.96/201.16 % Source : [TPTP] % 200.96/201.16 % Names : % 200.96/201.16 % 200.96/201.16 % Status : Unsatisfiable % 200.96/201.16 % Rating : 0.00 v7.4.0, 0.09 v7.3.0, 0.00 v6.4.0, 0.05 v6.3.0, 0.06 v6.2.0, 0.07 v6.1.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 % 200.96/201.16 % Syntax : Number of clauses : 4 ( 4 unt; 0 nHn; 1 RR) % 200.96/201.16 % Number of literals : 4 ( 4 equ; 1 neg) % 200.96/201.16 % Maximal clause size : 1 ( 1 avg) % 200.96/201.16 % Maximal term depth : 4 ( 2 avg) % 200.96/201.16 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty) % 200.96/201.16 % Number of functors : 5 ( 5 usr; 2 con; 0-2 aty) % 200.96/201.16 % Number of variables : 8 ( 0 sgn) % 200.96/201.16 % SPC : CNF_UNS_RFO_PEQ_UEQ % 200.96/201.16 % 200.96/201.16 % Comments : A UEQ part of GRP089-1 % 200.96/201.16 %-------------------------------------------------------------------------- % 200.96/201.16 cnf(single_axiom,axiom, % 200.96/201.16 divide(A,divide(divide(A,B),divide(C,B))) = C ). % 200.96/201.16 % 200.96/201.16 cnf(multiply,axiom, % 200.96/201.16 multiply(A,B) = divide(A,divide(divide(C,C),B)) ). % 200.96/201.16 % 200.96/201.16 cnf(inverse,axiom, % 200.96/201.16 inverse(A) = divide(divide(B,B),A) ). % 200.96/201.16 % 200.96/201.16 cnf(prove_these_axioms_2,negated_conjecture, % 200.96/201.16 multiply(multiply(inverse(b2),b2),a2) != a2 ). % 200.96/201.16 % 200.96/201.16 %-------------------------------------------------------------------------- % 200.96/201.17 %------------------------------------------- % 200.96/201.17 % Proof found % 200.96/201.17 % SZS status Theorem for theBenchmark % 200.96/201.17 % SZS output start Proof % 200.96/201.20 %ClaNum:12(EqnAxiom:8) % 200.96/201.20 %VarNum:16(SingletonVarNum:8) % 200.96/201.20 %MaxLitNum:1 % 200.96/201.20 %MaxfuncDepth:3 % 200.96/201.20 %SharedTerms:6 % 200.96/201.20 %goalClause: 12 % 200.96/201.20 %singleGoalClaCount:1 % 200.96/201.20 [12]~E(f5(f5(f4(a2),a2),a3),a3) % 200.96/201.20 [9]E(f1(f1(x91,x91),x92),f4(x92)) % 200.96/201.20 [10]E(f1(x101,f1(f1(x102,x102),x103)),f5(x101,x103)) % 200.96/201.20 [11]E(f1(x111,f1(f1(x111,x112),f1(x113,x112))),x113) % 200.96/201.20 %EqnAxiom % 200.96/201.20 [1]E(x11,x11) % 200.96/201.20 [2]E(x22,x21)+~E(x21,x22) % 200.96/201.20 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 200.96/201.20 [4]~E(x41,x42)+E(f1(x41,x43),f1(x42,x43)) % 200.96/201.20 [5]~E(x51,x52)+E(f1(x53,x51),f1(x53,x52)) % 200.96/201.20 [6]~E(x61,x62)+E(f5(x61,x63),f5(x62,x63)) % 200.96/201.20 [7]~E(x71,x72)+E(f5(x73,x71),f5(x73,x72)) % 200.96/201.20 [8]~E(x81,x82)+E(f4(x81),f4(x82)) % 200.96/201.20 % 200.96/201.20 %------------------------------------------- % 200.96/201.23 cnf(13,plain, % 200.96/201.23 (E(f4(x131),f1(f1(x132,x132),x131))), % 200.96/201.23 inference(scs_inference,[],[9,2])). % 200.96/201.23 cnf(14,plain, % 200.96/201.23 (E(f5(x141,x142),f1(x141,f1(f1(x143,x143),x142)))), % 200.96/201.23 inference(scs_inference,[],[10,2])). % 200.96/201.23 cnf(15,plain, % 200.96/201.23 (E(f4(f1(f1(x151,x151),x152)),f5(f1(x153,x153),x152))), % 200.96/201.23 inference(scs_inference,[],[13,10,2,3])). % 200.96/201.23 cnf(18,plain, % 200.96/201.23 (E(f5(f1(x181,x181),x182),f4(f1(f1(x183,x183),x182)))), % 200.96/201.23 inference(scs_inference,[],[15,2])). % 200.96/201.23 cnf(19,plain, % 200.96/201.23 (E(x191,f1(x192,f1(f1(x192,x193),f1(x191,x193))))), % 200.96/201.23 inference(scs_inference,[],[11,2])). % 200.96/201.23 cnf(20,plain, % 200.96/201.23 (E(f5(f1(x201,x201),x202),f1(f1(x203,x203),f1(f1(x204,x204),x202)))), % 200.96/201.23 inference(scs_inference,[],[18,13,11,2,3])). % 200.96/201.23 cnf(22,plain, % 200.96/201.23 (E(f1(f1(x221,x221),f1(f1(x222,x222),x223)),f5(f1(x224,x224),x223))), % 200.96/201.23 inference(scs_inference,[],[20,2])). % 200.96/201.23 cnf(23,plain, % 200.96/201.23 (E(f5(f1(x231,x231),x232),f5(f1(x233,x233),x232))), % 200.96/201.23 inference(scs_inference,[],[18,20,15,2,3])). % 200.96/201.23 cnf(27,plain, % 200.96/201.23 (E(x271,f5(f1(x272,x272),f1(x271,f1(x273,x273))))), % 200.96/201.23 inference(scs_inference,[],[19,22,3])). % 200.96/201.23 cnf(30,plain, % 200.96/201.23 (E(f5(f1(x301,x301),f1(x302,f1(x303,x303))),x302)), % 200.96/201.23 inference(scs_inference,[],[19,22,3,2])). % 200.96/201.23 cnf(31,plain, % 200.96/201.23 (E(f5(f1(x311,x311),f1(f4(x312),f1(x313,x313))),f1(f1(x314,x314),x312))), % 200.96/201.23 inference(scs_inference,[],[30,13,3])). % 200.96/201.23 cnf(33,plain, % 200.96/201.23 (E(f1(f1(x331,x331),x332),f5(f1(x333,x333),f1(f4(x332),f1(x334,x334))))), % 200.96/201.23 inference(scs_inference,[],[30,13,3,2])). % 200.96/201.23 cnf(34,plain, % 200.96/201.23 (E(x341,f4(f1(f1(f1(x342,x342),x343),f1(x341,x343))))), % 200.96/201.23 inference(scs_inference,[],[19,9,3])). % 200.96/201.23 cnf(38,plain, % 200.96/201.23 (E(x381,f5(x382,f1(x381,x382)))), % 200.96/201.23 inference(scs_inference,[],[19,10,3])). % 200.96/201.23 cnf(41,plain, % 200.96/201.23 (E(f5(x411,f1(x412,x411)),x412)), % 200.96/201.23 inference(scs_inference,[],[19,10,3,2])). % 200.96/201.23 cnf(42,plain, % 200.96/201.24 (E(f5(x421,f1(x422,x421)),f1(x423,f1(f1(x423,x424),f1(x422,x424))))), % 200.96/201.24 inference(scs_inference,[],[19,41,3])). % 200.96/201.24 cnf(44,plain, % 200.96/201.24 (E(f1(x441,f1(f1(x441,x442),f1(x443,x442))),f5(x444,f1(x443,x444)))), % 200.96/201.24 inference(scs_inference,[],[19,41,3,2])). % 200.96/201.24 cnf(45,plain, % 200.96/201.24 (~E(f5(f5(f4(a2),a2),a3),f5(x451,f1(a3,x451)))), % 200.96/201.24 inference(scs_inference,[],[12,41,3])). % 201.05/201.24 cnf(47,plain, % 201.05/201.24 (E(f5(f1(x471,x471),f1(f1(f1(x472,x472),x473),f1(x474,x474))),f4(x473))), % 201.05/201.24 inference(scs_inference,[],[30,9,3])). % 201.05/201.24 cnf(49,plain, % 201.05/201.24 (E(f4(x491),f5(f1(x492,x492),f1(f1(f1(x493,x493),x491),f1(x494,x494))))), % 201.05/201.24 inference(scs_inference,[],[47,2])). % 201.05/201.24 cnf(50,plain, % 201.05/201.24 (E(x501,f1(f1(x502,x502),f1(f1(f1(x503,x503),x504),f1(x501,x504))))), % 201.05/201.24 inference(scs_inference,[],[34,13,3])). % 201.05/201.24 cnf(53,plain, % 201.05/201.24 (E(x531,f1(x532,f1(f1(x533,x533),f1(x531,x532))))), % 201.05/201.24 inference(scs_inference,[],[38,14,3])). % 201.05/201.24 cnf(55,plain, % 201.05/201.24 (E(f1(x551,f1(f1(x552,x552),f1(x553,x551))),x553)), % 201.05/201.24 inference(scs_inference,[],[38,14,3,2])). % 201.05/201.24 cnf(56,plain, % 201.05/201.24 (E(f5(x561,f1(f4(x562),x561)),f1(f1(x563,x563),x562))), % 201.05/201.24 inference(scs_inference,[],[41,13,3])). % 201.05/201.24 cnf(58,plain, % 201.05/201.24 (E(f1(f1(x581,x581),x582),f5(x583,f1(f4(x582),x583)))), % 201.05/201.24 inference(scs_inference,[],[41,13,3,2])). % 201.05/201.24 cnf(59,plain, % 201.05/201.24 (E(f5(x591,f1(x592,x591)),f1(x593,f1(f1(x594,x594),f1(x592,x593))))), % 201.05/201.24 inference(scs_inference,[],[41,53,3])). % 201.05/201.24 cnf(61,plain, % 201.05/201.24 (E(f1(x611,f1(f1(x612,x612),f1(x613,x611))),f5(x614,f1(x613,x614)))), % 201.05/201.24 inference(scs_inference,[],[41,53,3,2])). % 201.05/201.24 cnf(62,plain, % 201.05/201.24 (E(f4(f1(f1(x621,x621),x622)),f4(f4(x622)))), % 201.05/201.24 inference(scs_inference,[],[9,8])). % 201.05/201.24 cnf(63,plain, % 201.05/201.24 (E(f1(f1(f1(x631,x631),x632),x633),f1(f4(x632),x633))), % 201.05/201.24 inference(scs_inference,[],[9,8,4])). % 201.05/201.24 cnf(64,plain, % 201.05/201.24 (E(f1(x641,f1(f1(x642,x642),x643)),f1(x641,f4(x643)))), % 201.05/201.24 inference(scs_inference,[],[9,8,4,5])). % 201.05/201.24 cnf(65,plain, % 201.05/201.24 (E(f5(f1(f1(x651,x651),x652),x653),f5(f4(x652),x653))), % 201.05/201.24 inference(scs_inference,[],[9,8,4,5,6])). % 201.05/201.24 cnf(66,plain, % 201.05/201.24 (E(f5(x661,f1(f1(x662,x662),x663)),f5(x661,f4(x663)))), % 201.05/201.24 inference(scs_inference,[],[9,8,4,5,6,7])). % 201.05/201.24 cnf(67,plain, % 201.05/201.24 (~E(f5(x671,f1(a3,x671)),f5(f5(f4(a2),a2),a3))), % 201.05/201.24 inference(scs_inference,[],[9,45,8,4,5,6,7,2])). % 201.05/201.24 cnf(68,plain, % 201.05/201.24 (~E(f5(f1(x681,x681),f1(f5(f5(f4(a2),a2),a3),f1(x682,x682))),a3)), % 201.05/201.24 inference(scs_inference,[],[9,27,45,12,8,4,5,6,7,2,3])). % 201.05/201.24 cnf(70,plain, % 201.05/201.24 (E(f1(x701,x702),f1(x701,f5(x703,f1(x702,x703))))), % 201.05/201.24 inference(scs_inference,[],[38,5])). % 201.05/201.24 cnf(71,plain, % 201.05/201.24 (E(f1(x711,x712),f1(f5(x713,f1(x711,x713)),x712))), % 201.05/201.24 inference(scs_inference,[],[38,5,4])). % 201.05/201.24 cnf(72,plain, % 201.05/201.24 (E(f5(x721,x722),f5(f5(x723,f1(x721,x723)),x722))), % 201.05/201.24 inference(scs_inference,[],[38,5,4,6])). % 201.05/201.24 cnf(73,plain, % 201.05/201.24 (E(f4(x731),f4(f5(x732,f1(x731,x732))))), % 201.05/201.24 inference(scs_inference,[],[38,5,4,6,8])). % 201.05/201.24 cnf(74,plain, % 201.05/201.24 (E(f5(x741,x742),f5(x741,f5(x743,f1(x742,x743))))), % 201.05/201.24 inference(scs_inference,[],[38,5,4,6,8,7])). % 201.05/201.24 cnf(75,plain, % 201.05/201.24 (~E(a3,f5(f5(f4(a2),a2),a3))), % 201.05/201.24 inference(scs_inference,[],[38,12,5,4,6,8,7,2])). % 201.05/201.24 cnf(76,plain, % 201.05/201.24 (E(f1(f1(x761,x761),f1(f1(x762,x762),x763)),f4(f4(x763)))), % 201.05/201.24 inference(scs_inference,[],[9,62,38,12,5,4,6,8,7,2,3])). % 201.05/201.24 cnf(78,plain, % 201.05/201.24 (E(f5(f5(x781,f1(x782,x781)),x783),f5(x782,x783))), % 201.05/201.24 inference(scs_inference,[],[41,6])). % 201.05/201.24 cnf(79,plain, % 201.05/201.24 (E(f1(f5(x791,f1(x792,x791)),x793),f1(x792,x793))), % 201.05/201.24 inference(scs_inference,[],[41,6,4])). % 201.05/201.24 cnf(80,plain, % 201.05/201.24 (E(f1(x801,f5(x802,f1(x803,x802))),f1(x801,x803))), % 201.05/201.24 inference(scs_inference,[],[41,6,4,5])). % 201.05/201.24 cnf(81,plain, % 201.05/201.24 (E(f4(f5(x811,f1(x812,x811))),f4(x812))), % 201.05/201.24 inference(scs_inference,[],[41,6,4,5,8])). % 201.05/201.24 cnf(83,plain, % 201.05/201.24 (E(f1(f1(x831,x831),x832),f4(f5(x833,f1(x832,x833))))), % 201.05/201.24 inference(scs_inference,[],[9,73,41,6,4,5,8,7,3])). % 201.05/201.24 cnf(85,plain, % 201.05/201.24 (E(f1(x851,f4(x852)),f1(x851,f1(f1(x853,x853),x852)))), % 201.05/201.24 inference(scs_inference,[],[13,5])). % 201.05/201.24 cnf(86,plain, % 201.05/201.24 (E(f1(f4(x861),x862),f1(f1(f1(x863,x863),x861),x862))), % 201.05/201.24 inference(scs_inference,[],[13,5,4])). % 201.05/201.24 cnf(87,plain, % 201.05/201.24 (E(f5(f4(x871),x872),f5(f1(f1(x873,x873),x871),x872))), % 201.05/201.24 inference(scs_inference,[],[13,5,4,6])). % 201.05/201.24 cnf(88,plain, % 201.05/201.24 (E(f4(f4(x881)),f4(f1(f1(x882,x882),x881)))), % 201.05/201.24 inference(scs_inference,[],[13,5,4,6,8])). % 201.05/201.24 cnf(89,plain, % 201.05/201.24 (E(f5(x891,f4(x892)),f5(x891,f1(f1(x893,x893),x892)))), % 201.05/201.24 inference(scs_inference,[],[13,5,4,6,8,7])). % 201.05/201.24 cnf(90,plain, % 201.05/201.24 (E(f1(f5(x901,f1(x902,x901)),f1(f1(x902,x903),f1(x904,x903))),x904)), % 201.05/201.24 inference(scs_inference,[],[11,79,3])). % 201.05/201.24 cnf(92,plain, % 201.05/201.24 (~E(f1(f5(f4(a2),a2),f1(f1(x921,x921),a3)),a3)), % 201.05/201.24 inference(scs_inference,[],[14,12,3])). % 201.05/201.24 cnf(94,plain, % 201.05/201.24 (~E(a3,f1(f5(f4(a2),a2),f1(f1(x941,x941),a3)))), % 201.05/201.24 inference(scs_inference,[],[92,2])). % 201.05/201.24 cnf(99,plain, % 201.05/201.24 (~E(f1(f5(f4(a2),a2),f4(a3)),a3)), % 201.05/201.24 inference(scs_inference,[],[64,92,3])). % 201.05/201.24 cnf(101,plain, % 201.05/201.24 (~E(a3,f1(f5(f4(a2),a2),f4(a3)))), % 201.05/201.24 inference(scs_inference,[],[99,2])). % 201.05/201.24 cnf(102,plain, % 201.05/201.24 (E(f5(f1(x1021,x1021),f1(f1(x1022,x1022),x1023)),f5(f1(x1024,x1024),f4(x1023)))), % 201.05/201.24 inference(scs_inference,[],[23,66,3])). % 201.05/201.24 cnf(105,plain, % 201.05/201.24 (E(f5(f1(x1051,x1051),f4(f1(x1052,x1052))),f1(x1053,x1053))), % 201.05/201.24 inference(scs_inference,[],[30,89,3])). % 201.05/201.24 cnf(108,plain, % 201.05/201.24 (~E(f5(x1081,f1(a3,x1081)),f1(f5(f4(a2),a2),f4(a3)))), % 201.05/201.24 inference(scs_inference,[],[101,38,3])). % 201.05/201.24 cnf(110,plain, % 201.05/201.24 (~E(f1(f5(f4(a2),a2),f4(a3)),f5(x1101,f1(a3,x1101)))), % 201.05/201.24 inference(scs_inference,[],[101,38,3,2])). % 201.05/201.24 cnf(111,plain, % 201.05/201.24 (~E(f5(f5(x1111,f1(x1112,x1111)),f1(a3,x1112)),f1(f5(f4(a2),a2),f4(a3)))), % 201.05/201.24 inference(scs_inference,[],[108,72,3])). % 201.05/201.24 cnf(113,plain, % 201.05/201.24 (~E(f1(f5(f4(a2),a2),f4(a3)),f5(f5(x1131,f1(x1132,x1131)),f1(a3,x1132)))), % 201.05/201.24 inference(scs_inference,[],[111,2])). % 201.05/201.24 cnf(114,plain, % 201.05/201.24 (~E(f5(f5(f4(a2),a2),f5(x1141,f1(a3,x1141))),a3)), % 201.05/201.24 inference(scs_inference,[],[74,111,12,2,3])). % 201.05/201.24 cnf(116,plain, % 201.05/201.24 (~E(a3,f5(f5(f4(a2),a2),f5(x1161,f1(a3,x1161))))), % 201.05/201.24 inference(scs_inference,[],[114,2])). % 201.05/201.24 cnf(117,plain, % 201.05/201.24 (E(f5(f1(x1171,x1171),f1(f1(x1172,x1172),f1(x1173,x1173))),f1(x1174,x1174))), % 201.05/201.24 inference(scs_inference,[],[105,102,114,2,3])). % 201.05/201.24 cnf(119,plain, % 201.05/201.24 (E(f4(f1(x1191,x1191)),f1(x1192,x1192))), % 201.05/201.24 inference(scs_inference,[],[117,49,3])). % 201.05/201.24 cnf(122,plain, % 201.05/201.24 (E(f5(f4(f1(x1221,x1221)),x1222),f5(f1(x1223,x1223),x1222))), % 201.05/201.24 inference(scs_inference,[],[117,49,3,6])). % 201.05/201.24 cnf(123,plain, % 201.05/201.24 (E(f1(f4(f1(x1231,x1231)),x1232),f1(f1(x1233,x1233),x1232))), % 201.05/201.24 inference(scs_inference,[],[117,49,3,6,4])). % 201.05/201.24 cnf(124,plain, % 201.05/201.24 (E(f1(x1241,f4(f1(x1242,x1242))),f1(x1241,f1(x1243,x1243)))), % 201.05/201.24 inference(scs_inference,[],[117,49,3,6,4,5])). % 201.05/201.24 cnf(125,plain, % 201.05/201.24 (E(f4(f4(f1(x1251,x1251))),f4(f1(x1252,x1252)))), % 201.05/201.24 inference(scs_inference,[],[117,49,3,6,4,5,8])). % 201.05/201.24 cnf(126,plain, % 201.05/201.24 (E(f5(x1261,f4(f1(x1262,x1262))),f5(x1261,f1(x1263,x1263)))), % 201.05/201.24 inference(scs_inference,[],[117,49,3,6,4,5,8,7])). % 201.05/201.24 cnf(127,plain, % 201.05/201.24 (E(f1(f1(x1271,x1271),f1(f1(x1272,x1272),f1(x1273,x1273))),f4(f1(x1274,x1274)))), % 201.05/201.24 inference(scs_inference,[],[76,125,3])). % 201.05/201.24 cnf(129,plain, % 201.05/201.24 (E(f4(f1(x1291,x1291)),f1(x1292,f5(x1293,f1(x1292,x1293))))), % 201.05/201.24 inference(scs_inference,[],[119,70,3])). % 201.05/201.24 cnf(132,plain, % 201.05/201.24 (E(f1(x1321,f4(f1(x1322,x1322))),f5(x1323,f1(x1321,x1323)))), % 201.05/201.24 inference(scs_inference,[],[61,124,3])). % 201.05/201.24 cnf(135,plain, % 201.05/201.24 (E(f4(f1(x1351,x1351)),f1(f1(f1(x1352,x1352),x1353),f4(x1353)))), % 201.05/201.24 inference(scs_inference,[],[64,119,3])). % 201.05/201.24 cnf(138,plain, % 201.05/201.24 (E(f5(f1(x1381,x1381),f1(f1(x1382,x1382),f1(x1383,x1383))),f5(f1(x1384,x1384),f1(x1385,x1385)))), % 201.05/201.24 inference(scs_inference,[],[126,102,3])). % 201.05/201.24 cnf(141,plain, % 201.05/201.24 (E(f1(f5(x1411,f1(x1412,x1411)),f1(f1(x1413,x1413),f1(x1414,x1412))),x1414)), % 201.05/201.24 inference(scs_inference,[],[55,79,3])). % 201.05/201.24 cnf(143,plain, % 201.05/201.24 (E(f4(f1(x1431,x1431)),f5(f1(x1432,x1432),f1(x1433,x1433)))), % 201.05/201.24 inference(scs_inference,[],[138,49,3])). % 201.05/201.24 cnf(146,plain, % 201.05/201.24 (E(f4(f1(x1461,x1461)),f5(f4(f1(x1462,x1462)),f1(x1463,x1463)))), % 201.05/201.24 inference(scs_inference,[],[143,65,3])). % 201.05/201.24 cnf(149,plain, % 201.05/201.24 (E(f4(f1(x1491,x1491)),f1(f5(x1492,f1(x1493,x1492)),x1493))), % 201.05/201.24 inference(scs_inference,[],[71,119,3])). % 201.05/201.24 cnf(154,plain, % 201.05/201.24 (E(f1(f1(f1(x1541,x1541),f1(x1542,x1542)),x1543),f1(f1(x1544,x1544),x1543))), % 201.05/201.24 inference(scs_inference,[],[123,63,3])). % 201.05/201.24 cnf(156,plain, % 201.05/201.24 (E(f5(f1(x1561,x1561),f4(f1(x1562,x1562))),f4(f1(x1563,x1563)))), % 201.05/201.24 inference(scs_inference,[],[127,105,3])). % 201.05/201.24 cnf(159,plain, % 201.05/201.24 (E(f5(f1(x1591,x1591),f1(f1(x1592,x1592),f1(x1593,x1593))),f4(f1(x1594,x1594)))), % 201.05/201.24 inference(scs_inference,[],[156,102,3])). % 201.05/201.24 cnf(161,plain, % 201.05/201.24 (E(f4(f1(x1611,x1611)),f4(f1(x1612,x1612)))), % 201.05/201.24 inference(scs_inference,[],[159,143,3])). % 201.05/201.24 cnf(164,plain, % 201.05/201.24 (E(f1(f1(x1641,x1641),f1(x1642,x1642)),f4(f1(x1643,x1643)))), % 201.05/201.24 inference(scs_inference,[],[161,9,3])). % 201.05/201.24 cnf(166,plain, % 201.05/201.24 (E(f1(f1(x1661,x1661),f1(x1662,x1662)),f1(f1(f1(x1663,x1663),x1664),f4(x1664)))), % 201.05/201.24 inference(scs_inference,[],[164,135,3])). % 201.05/201.24 cnf(168,plain, % 201.05/201.24 (E(f1(f4(f1(x1681,x1681)),f1(x1682,x1682)),f1(f1(f1(x1683,x1683),x1684),f4(x1684)))), % 201.05/201.24 inference(scs_inference,[],[166,86,3])). % 201.05/201.24 cnf(171,plain, % 201.05/201.24 (E(f4(f1(x1711,x1711)),f1(f1(x1712,x1712),f1(x1713,x1713)))), % 201.05/201.24 inference(scs_inference,[],[146,56,3])). % 201.05/201.24 cnf(176,plain, % 201.05/201.24 (E(f1(f1(x1761,x1761),f4(f1(x1762,x1762))),f5(f1(x1763,x1763),f1(x1764,x1764)))), % 201.05/201.24 inference(scs_inference,[],[138,132,3])). % 201.05/201.24 cnf(179,plain, % 201.05/201.24 (E(f1(f1(x1791,x1791),f1(x1792,x1792)),f1(f1(x1793,x1793),f4(f1(x1794,x1794))))), % 201.05/201.24 inference(scs_inference,[],[154,166,3])). % 201.05/201.24 cnf(182,plain, % 201.05/201.24 (E(f4(f4(f1(x1821,x1821))),f1(f1(x1822,x1822),f1(x1823,x1823)))), % 201.05/201.24 inference(scs_inference,[],[171,88,3])). % 201.05/201.24 cnf(185,plain, % 201.05/201.24 (E(f1(f4(f1(x1851,x1851)),f1(x1852,x1852)),f5(f1(x1853,x1853),f1(x1854,x1854)))), % 201.05/201.24 inference(scs_inference,[],[168,176,3])). % 201.05/201.24 cnf(188,plain, % 201.05/201.24 (E(f4(f1(x1881,x1881)),f5(x1882,f1(f1(x1883,x1883),x1882)))), % 201.05/201.24 inference(scs_inference,[],[44,171,3])). % 201.05/201.24 cnf(191,plain, % 201.05/201.24 (E(f1(f1(x1911,x1911),f1(x1912,x1912)),f5(f1(x1913,x1913),f1(x1914,x1914)))), % 201.05/201.24 inference(scs_inference,[],[176,179,3])). % 201.05/201.24 cnf(193,plain, % 201.05/201.24 (E(f4(f4(f1(x1931,x1931))),f5(f1(x1932,x1932),f1(x1933,x1933)))), % 201.05/201.24 inference(scs_inference,[],[191,182,3])). % 201.05/201.24 cnf(195,plain, % 201.05/201.24 (E(f4(f1(f1(x1951,x1951),f1(x1952,x1952))),f5(f1(x1953,x1953),f1(x1954,x1954)))), % 201.05/201.24 inference(scs_inference,[],[193,62,3])). % 201.05/201.24 cnf(199,plain, % 201.05/201.24 (E(f1(f1(x1991,x1991),x1992),f1(f1(x1993,x1993),f5(x1994,f1(x1992,x1994))))), % 201.05/201.24 inference(scs_inference,[],[13,83,3])). % 201.05/201.24 cnf(201,plain, % 201.05/201.24 (E(f1(f1(x2011,x2011),f1(x2012,x2012)),f4(f1(f1(x2013,x2013),f1(x2014,x2014))))), % 201.05/201.24 inference(scs_inference,[],[18,191,3])). % 201.05/201.24 cnf(204,plain, % 201.05/201.24 (E(f1(f1(f1(x2041,x2041),f1(x2042,x2042)),f1(x2043,x2043)),f5(f1(x2044,x2044),f1(x2045,x2045)))), % 201.05/201.24 inference(scs_inference,[],[185,63,3])). % 201.05/201.24 cnf(206,plain, % 201.05/201.24 (E(f4(f1(x2061,x2061)),f5(f1(x2062,x2062),f1(f1(x2063,x2063),f1(x2064,x2064))))), % 201.05/201.24 inference(scs_inference,[],[27,119,3])). % 201.05/201.24 cnf(208,plain, % 201.05/201.24 (E(f1(f1(x2081,x2081),f1(f1(x2082,x2082),f1(x2083,x2083))),f5(f1(x2084,x2084),f1(x2085,x2085)))), % 201.05/201.24 inference(scs_inference,[],[195,127,3])). % 201.05/201.24 cnf(211,plain, % 201.05/201.24 (E(f1(f1(f1(x2111,x2111),f1(x2112,x2112)),f1(x2113,x2113)),f1(x2114,x2114))), % 201.05/201.24 inference(scs_inference,[],[41,204,3])). % 201.05/201.24 cnf(214,plain, % 201.05/201.24 (E(f5(f1(x2141,x2141),f1(f4(f1(x2142,x2142)),f1(x2143,x2143))),f1(x2144,x2144))), % 201.05/201.24 inference(scs_inference,[],[211,31,3])). % 201.05/201.24 cnf(217,plain, % 201.05/201.24 (E(f1(f1(x2171,x2171),f1(x2172,x2172)),f1(f5(x2173,f1(x2174,x2173)),x2174))), % 201.05/201.24 inference(scs_inference,[],[149,201,3])). % 201.05/201.24 cnf(225,plain, % 201.05/201.24 (E(f1(f1(x2251,x2251),f1(x2252,x2252)),f1(x2253,x2253))), % 201.05/201.25 inference(scs_inference,[],[214,33,3])). % 201.05/201.25 cnf(227,plain, % 201.05/201.25 (E(f1(x2271,f1(f1(x2272,x2272),f1(x2273,x2273))),f1(x2271,f1(x2274,x2274)))), % 201.05/201.25 inference(scs_inference,[],[214,33,3,5])). % 201.05/201.25 cnf(230,plain, % 201.05/201.25 (E(f5(x2301,f1(f1(x2302,x2302),f1(x2303,x2303))),f5(x2301,f1(x2304,x2304)))), % 201.05/201.25 inference(scs_inference,[],[214,33,3,5,6,8,7])). % 201.05/201.25 cnf(231,plain, % 201.05/201.25 (E(f1(f1(x2311,x2311),f4(f1(x2312,x2312))),f1(x2313,x2313))), % 201.05/201.25 inference(scs_inference,[],[225,124,3])). % 201.05/201.25 cnf(233,plain, % 201.05/201.25 (E(f1(f4(f1(x2331,x2331)),f1(x2332,x2332)),f1(x2333,x2333))), % 201.05/201.25 inference(scs_inference,[],[231,168,3])). % 201.05/201.25 cnf(236,plain, % 201.05/201.25 (E(f1(f1(x2361,x2361),f1(x2362,x2362)),f1(f1(x2363,x2363),f1(f1(x2364,x2364),f1(x2365,x2365))))), % 201.05/201.25 inference(scs_inference,[],[85,179,3])). % 201.05/201.25 cnf(240,plain, % 201.05/201.25 (E(f1(f4(f1(x2401,x2401)),f4(f1(x2402,x2402))),f1(x2403,x2403))), % 201.05/201.25 inference(scs_inference,[],[233,124,3])). % 201.05/201.25 cnf(242,plain, % 201.05/201.25 (E(f4(f1(x2421,x2421)),f5(f1(f1(x2422,x2422),f1(x2423,x2423)),f1(x2424,x2424)))), % 201.05/201.25 inference(scs_inference,[],[87,146,3])). % 201.05/201.25 cnf(244,plain, % 201.05/201.25 (E(f1(f1(x2441,x2441),f1(x2442,x2442)),f5(f1(f1(x2443,x2443),f1(x2444,x2444)),f1(x2445,x2445)))), % 201.05/201.25 inference(scs_inference,[],[242,201,3])). % 201.05/201.25 cnf(247,plain, % 201.05/201.25 (E(f1(f4(f1(x2471,x2471)),f1(x2472,x2472)),f5(f1(f1(x2473,x2473),f1(x2474,x2474)),f1(x2475,x2475)))), % 201.05/201.25 inference(scs_inference,[],[244,233,3])). % 201.05/201.25 cnf(250,plain, % 201.05/201.25 (E(f1(f1(f1(x2501,x2501),f1(x2502,x2502)),f4(f1(x2503,x2503))),f1(x2504,x2504))), % 201.05/201.25 inference(scs_inference,[],[240,63,3])). % 201.05/201.25 cnf(252,plain, % 201.05/201.25 (E(f4(f4(f1(x2521,x2521))),f1(x2522,x2522))), % 201.05/201.25 inference(scs_inference,[],[250,13,3])). % 201.05/201.25 cnf(255,plain, % 201.05/201.25 (E(f1(f1(x2551,x2551),f1(f1(x2552,x2552),f1(x2553,x2553))),f1(x2554,x2554))), % 201.05/201.25 inference(scs_inference,[],[252,76,3])). % 201.05/201.25 cnf(257,plain, % 201.05/201.25 (E(f4(f1(f1(x2571,x2571),f1(x2572,x2572))),f1(x2573,x2573))), % 201.05/201.25 inference(scs_inference,[],[117,195,3])). % 201.05/201.25 cnf(260,plain, % 201.05/201.25 (E(f1(f4(f1(x2601,x2601)),f1(f1(x2602,x2602),f1(x2603,x2603))),f1(x2604,x2604))), % 201.05/201.25 inference(scs_inference,[],[123,255,3])). % 201.05/201.25 cnf(262,plain, % 201.05/201.25 (E(f1(f1(f1(x2621,x2621),f1(x2622,x2622)),f1(f1(x2623,x2623),f1(x2624,x2624))),f1(x2625,x2625))), % 201.05/201.25 inference(scs_inference,[],[260,63,3])). % 201.05/201.25 cnf(264,plain, % 201.05/201.25 (E(f1(f1(x2641,x2641),f1(x2642,x2642)),f5(x2643,f1(f1(x2644,x2644),x2643)))), % 201.05/201.25 inference(scs_inference,[],[132,179,3])). % 201.05/201.25 cnf(267,plain, % 201.05/201.25 (E(f1(f5(x2671,f1(x2672,x2671)),f4(f1(x2673,x2673))),x2672)), % 201.05/201.25 inference(scs_inference,[],[141,124,3])). % 201.05/201.25 cnf(273,plain, % 201.05/201.25 (E(f1(f1(x2731,x2731),f4(f1(x2732,x2732))),f4(f1(x2733,x2733)))), % 201.05/201.25 inference(scs_inference,[],[164,231,3])). % 201.05/201.25 cnf(276,plain, % 201.05/201.25 (E(f1(f1(x2761,x2761),f4(f1(x2762,x2762))),f1(f1(x2763,x2763),f1(x2764,x2764)))), % 201.05/201.25 inference(scs_inference,[],[171,273,3])). % 201.05/201.25 cnf(278,plain, % 201.05/201.25 (E(f1(f1(x2781,x2781),f1(x2782,x2782)),f1(f1(x2783,x2783),f1(x2784,x2784)))), % 201.05/201.25 inference(scs_inference,[],[179,276,3])). % 201.05/201.25 cnf(280,plain, % 201.05/201.25 (E(f4(f1(f1(x2801,x2801),f1(x2802,x2802))),f1(f1(x2803,x2803),f1(x2804,x2804)))), % 201.05/201.25 inference(scs_inference,[],[278,257,3])). % 201.05/201.25 cnf(283,plain, % 201.05/201.25 (E(f5(f1(x2831,x2831),f4(f1(x2832,x2832))),f5(f1(x2833,x2833),f1(x2834,x2834)))), % 201.05/201.25 inference(scs_inference,[],[195,156,3])). % 201.05/201.25 cnf(286,plain, % 201.05/201.25 (E(f4(f1(x2861,x2861)),f4(f1(f1(x2862,x2862),f1(x2863,x2863))))), % 201.05/201.25 inference(scs_inference,[],[201,171,3])). % 201.05/201.25 cnf(291,plain, % 201.05/201.25 (E(f1(f4(f1(x2911,x2911)),f1(x2912,x2912)),f1(f1(f1(x2913,x2913),f1(x2914,x2914)),f1(x2915,x2915)))), % 201.05/201.25 inference(scs_inference,[],[227,233,3])). % 201.05/201.25 cnf(294,plain, % 201.05/201.25 (E(f5(f1(x2941,x2941),f1(f1(x2942,x2942),f1(x2943,x2943))),f1(f1(x2944,x2944),f1(x2945,x2945)))), % 201.05/201.25 inference(scs_inference,[],[280,159,3])). % 201.05/201.25 cnf(297,plain, % 201.05/201.25 (E(f1(f4(f1(x2971,x2971)),f1(x2972,x2972)),f1(f1(x2973,x2973),f1(x2974,x2974)))), % 201.05/201.25 inference(scs_inference,[],[247,294,3])). % 201.05/201.25 cnf(300,plain, % 201.05/201.25 (E(f1(f1(f1(x3001,x3001),f1(x3002,x3002)),f1(x3003,x3003)),f1(f1(x3004,x3004),f1(x3005,x3005)))), % 201.05/201.25 inference(scs_inference,[],[297,63,3])). % 201.05/201.25 cnf(302,plain, % 201.05/201.25 (E(f5(f1(x3021,x3021),f4(f1(x3022,x3022))),f1(f1(x3023,x3023),f1(x3024,x3024)))), % 201.05/201.25 inference(scs_inference,[],[300,105,3])). % 201.05/201.25 cnf(305,plain, % 201.05/201.25 (E(f1(f1(f1(x3051,x3051),f1(x3052,x3052)),f1(x3053,x3053)),f1(f1(f1(x3054,x3054),f1(x3055,x3055)),f1(x3056,x3056)))), % 201.05/201.25 inference(scs_inference,[],[291,63,3])). % 201.05/201.25 cnf(307,plain, % 201.05/201.25 (E(f1(f4(f1(x3071,x3071)),f1(x3072,x3072)),f4(f1(x3073,x3073)))), % 201.05/201.25 inference(scs_inference,[],[273,168,3])). % 201.05/201.25 cnf(310,plain, % 201.05/201.25 (E(f1(f1(x3101,x3101),f1(f1(x3102,x3102),f1(x3103,x3103))),f1(f1(x3104,x3104),f1(x3105,x3105)))), % 201.05/201.25 inference(scs_inference,[],[280,127,3])). % 201.05/201.25 cnf(313,plain, % 201.05/201.25 (E(f1(f1(f1(x3131,x3131),f1(x3132,x3132)),f1(x3133,x3133)),f4(f1(x3134,x3134)))), % 201.05/201.25 inference(scs_inference,[],[307,63,3])). % 201.05/201.25 cnf(315,plain, % 201.05/201.25 (E(f4(f1(x3151,x3151)),f1(f1(f1(x3152,x3152),f1(x3153,x3153)),f1(x3154,x3154)))), % 201.05/201.25 inference(scs_inference,[],[305,119,3])). % 201.05/201.25 cnf(318,plain, % 201.05/201.25 (E(f1(f1(x3181,x3181),f1(x3182,x3182)),f1(f1(f1(x3183,x3183),f1(x3184,x3184)),f1(x3185,x3185)))), % 201.05/201.25 inference(scs_inference,[],[315,164,3])). % 201.05/201.25 cnf(320,plain, % 201.05/201.25 (E(f1(f4(f1(x3201,x3201)),x3202),f4(x3202))), % 201.05/201.25 inference(scs_inference,[],[9,86,3])). % 201.05/201.25 cnf(323,plain, % 201.05/201.25 (E(f4(x3231),f1(f1(x3232,x3232),f5(x3233,f1(x3231,x3233))))), % 201.05/201.25 inference(scs_inference,[],[13,73,3])). % 201.05/201.25 cnf(325,plain, % 201.05/201.25 (E(f1(f1(f1(x3251,x3251),f1(x3252,x3252)),x3253),f4(x3253))), % 201.05/201.25 inference(scs_inference,[],[320,63,3])). % 201.05/201.25 cnf(327,plain, % 201.05/201.25 (E(f1(f1(x3271,x3271),f1(x3272,x3272)),f5(f1(x3273,x3273),f1(f1(x3274,x3274),f1(x3275,x3275))))), % 201.05/201.25 inference(scs_inference,[],[23,264,3])). % 201.05/201.25 cnf(332,plain, % 201.05/201.25 (E(f5(x3321,f4(f1(x3322,x3322))),x3321)), % 201.05/201.25 inference(scs_inference,[],[41,126,3])). % 201.05/201.25 cnf(338,plain, % 201.05/201.25 (E(f1(x3381,f4(f1(x3382,x3382))),x3381)), % 201.05/201.25 inference(scs_inference,[],[55,124,3])). % 201.05/201.25 cnf(341,plain, % 201.05/201.25 (E(f4(x3411),f1(f4(f1(x3412,x3412)),f5(x3413,f1(x3411,x3413))))), % 201.05/201.25 inference(scs_inference,[],[63,323,3])). % 201.05/201.25 cnf(344,plain, % 201.05/201.25 (E(f4(f1(x3441,x3441)),f5(x3442,f4(x3442)))), % 201.05/201.25 inference(scs_inference,[],[66,188,3])). % 201.05/201.25 cnf(347,plain, % 201.05/201.25 (E(f1(f1(f1(x3471,x3471),f1(x3472,x3472)),f1(x3473,x3473)),f5(x3474,f4(x3474)))), % 201.05/201.25 inference(scs_inference,[],[344,313,3])). % 201.05/201.25 cnf(349,plain, % 201.05/201.25 (E(f4(x3491),f1(f4(f1(x3492,x3492)),x3491))), % 201.05/201.25 inference(scs_inference,[],[80,341,3])). % 201.05/201.25 cnf(352,plain, % 201.05/201.25 (E(f1(f4(f1(x3521,x3521)),f1(x3522,x3522)),f1(f4(f1(x3523,x3523)),f1(x3524,x3524)))), % 201.05/201.25 inference(scs_inference,[],[349,307,3])). % 201.05/201.25 cnf(354,plain, % 201.05/201.25 (E(f1(f1(x3541,x3541),f4(x3542)),f4(f1(f1(x3543,x3543),x3542)))), % 201.05/201.25 inference(scs_inference,[],[88,9,3])). % 201.05/201.25 cnf(356,plain, % 201.05/201.25 (E(f4(f1(x3561,x3561)),f5(f1(x3562,x3562),f4(f1(x3563,x3563))))), % 201.05/201.25 inference(scs_inference,[],[102,206,3])). % 201.05/201.25 cnf(361,plain, % 201.05/201.25 (E(f4(f1(x3611,x3611)),f1(f4(f1(x3612,x3612)),f1(x3613,x3613)))), % 201.05/201.25 inference(scs_inference,[],[124,119,3])). % 201.05/201.25 cnf(364,plain, % 201.05/201.25 (E(f1(f1(f1(x3641,x3641),f1(x3642,x3642)),f1(x3643,x3643)),f1(f4(f1(x3644,x3644)),f1(x3645,x3645)))), % 201.05/201.25 inference(scs_inference,[],[361,325,3])). % 201.05/201.25 cnf(366,plain, % 201.05/201.25 (E(f1(f1(f1(x3661,x3661),f1(x3662,x3662)),f1(x3663,x3663)),f1(f1(f1(x3664,x3664),x3665),f4(x3665)))), % 201.05/201.25 inference(scs_inference,[],[135,313,3])). % 201.05/201.25 cnf(368,plain, % 201.05/201.25 (E(f1(f4(f1(x3681,x3681)),f1(x3682,x3682)),f5(f4(f1(x3683,x3683)),f1(x3684,x3684)))), % 201.05/201.25 inference(scs_inference,[],[146,320,3])). % 201.05/201.25 cnf(373,plain, % 201.05/201.25 (E(f5(f1(f1(x3731,x3731),f1(x3732,x3732)),f4(f1(x3733,x3733))),f1(x3734,x3734))), % 201.05/201.25 inference(scs_inference,[],[225,332,3])). % 201.05/201.25 cnf(375,plain, % 201.05/201.25 (E(f1(f1(f1(x3751,x3751),f1(x3752,x3752)),f1(x3753,x3753)),f5(f1(f1(x3754,x3754),f1(x3755,x3755)),f1(x3756,x3756)))), % 201.05/201.25 inference(scs_inference,[],[242,325,3])). % 201.05/201.25 cnf(377,plain, % 201.05/201.25 (E(f5(f1(x3771,x3771),f4(f1(x3772,x3772))),f5(x3773,f4(x3773)))), % 201.05/201.25 inference(scs_inference,[],[347,302,3])). % 201.05/201.25 cnf(380,plain, % 201.05/201.25 (E(f5(x3801,f1(f1(x3802,x3802),f1(x3803,x3803))),x3801)), % 201.05/201.25 inference(scs_inference,[],[332,66,3])). % 201.05/201.25 cnf(382,plain, % 201.05/201.25 (E(f1(f1(x3821,x3821),f4(f1(x3822,x3822))),f5(x3823,f4(x3823)))), % 201.05/201.25 inference(scs_inference,[],[344,354,3])). % 201.05/201.25 cnf(385,plain, % 201.05/201.25 (E(f1(f1(f1(x3851,x3851),f1(x3852,x3852)),f1(x3853,x3853)),f5(f4(f1(x3854,x3854)),f1(x3855,x3855)))), % 201.05/201.25 inference(scs_inference,[],[364,368,3])). % 201.05/201.25 cnf(387,plain, % 201.05/201.25 (E(f1(f1(x3871,x3871),f1(x3872,x3872)),f1(f4(f1(x3873,x3873)),f1(x3874,x3874)))), % 201.05/201.25 inference(scs_inference,[],[361,201,3])). % 201.05/201.25 cnf(390,plain, % 201.05/201.25 (E(f1(f1(x3901,x3901),f1(x3902,x3902)),f5(f4(f1(x3903,x3903)),f1(x3904,x3904)))), % 201.05/201.25 inference(scs_inference,[],[368,387,3])). % 201.05/201.25 cnf(392,plain, % 201.05/201.25 (E(f5(f1(x3921,x3921),f1(f1(x3922,x3922),f1(x3923,x3923))),f5(x3924,f4(x3924)))), % 201.05/201.25 inference(scs_inference,[],[377,66,3])). % 201.05/201.25 cnf(394,plain, % 201.05/201.25 (E(f1(f1(x3941,x3941),f1(f1(x3942,x3942),f1(x3943,x3943))),f5(x3944,f4(x3944)))), % 201.05/201.25 inference(scs_inference,[],[392,208,3])). % 201.05/201.25 cnf(397,plain, % 201.05/201.25 (E(f5(f1(f1(x3971,x3971),x3972),f1(f1(x3973,x3973),f1(x3974,x3974))),f4(x3972))), % 201.05/201.25 inference(scs_inference,[],[9,380,3])). % 201.05/201.25 cnf(399,plain, % 201.05/201.25 (E(f1(f4(x3991),f4(f1(x3992,x3992))),f1(f1(x3993,x3993),x3991))), % 201.05/201.25 inference(scs_inference,[],[13,338,3])). % 201.05/201.25 cnf(404,plain, % 201.05/201.25 (E(f5(x4041,f1(f1(x4042,x4042),f1(x4043,x4043))),f5(x4044,f1(x4041,x4044)))), % 201.05/201.25 inference(scs_inference,[],[38,380,3])). % 201.05/201.25 cnf(406,plain, % 201.05/201.25 (E(f5(f4(x4061),f4(f1(x4062,x4062))),f1(f1(x4063,x4063),x4061))), % 201.05/201.25 inference(scs_inference,[],[56,126,3])). % 201.05/201.25 cnf(409,plain, % 201.05/201.25 (E(f4(f1(x4091,x4091)),f1(f4(x4092),f1(f1(x4093,x4093),x4092)))), % 201.05/201.25 inference(scs_inference,[],[63,119,3])). % 201.05/201.25 cnf(412,plain, % 201.05/201.25 (E(f1(f1(x4121,x4121),f1(x4122,x4122)),f5(f1(x4123,x4123),f4(f1(x4124,x4124))))), % 201.05/201.25 inference(scs_inference,[],[66,327,3])). % 201.05/201.25 cnf(415,plain, % 201.05/201.25 (E(f1(f1(f1(x4151,x4151),f1(x4152,x4152)),f1(x4153,x4153)),f5(f5(x4154,f1(x4155,x4154)),f4(x4155)))), % 201.05/201.25 inference(scs_inference,[],[72,347,3])). % 201.05/201.25 cnf(418,plain, % 201.05/201.25 (E(f4(f4(x4181)),f1(f1(x4182,x4182),f1(f1(x4183,x4183),x4181)))), % 201.05/201.25 inference(scs_inference,[],[85,13,3])). % 201.05/201.25 cnf(421,plain, % 201.05/201.25 (E(f5(f1(f1(x4211,x4211),f1(x4212,x4212)),f1(f1(x4213,x4213),f1(x4214,x4214))),f1(x4215,x4215))), % 201.05/201.25 inference(scs_inference,[],[119,397,3])). % 201.05/201.25 cnf(428,plain, % 201.05/201.25 (~E(f1(x4281,f1(f1(x4282,x4282),f1(f1(f5(f4(a2),a2),f4(a3)),x4281))),f5(x4283,f1(a3,x4283)))), % 201.05/201.25 inference(scs_inference,[],[123,110,68,53,6,5,7,8,2,3])). % 201.05/201.25 cnf(431,plain, % 201.05/201.25 (~E(f1(a3,f5(f4(a2),a2)),a3)), % 201.05/201.25 inference(scs_inference,[],[67,7])). % 201.05/201.25 cnf(434,plain, % 201.05/201.25 (~E(f1(f1(x4341,x4341),f1(f1(x4342,x4342),f1(f1(f5(f4(a2),a2),f4(a3)),f4(f1(x4343,x4343))))),f5(x4344,f1(a3,x4344)))), % 201.05/201.25 inference(scs_inference,[],[123,67,428,7,2,3])). % 201.05/201.25 cnf(438,plain, % 201.05/201.25 (~E(a3,f1(a3,f5(f4(a2),a2)))), % 201.05/201.25 inference(scs_inference,[],[78,431,7,2])). % 201.05/201.25 cnf(439,plain, % 201.05/201.25 (~E(f4(f1(f1(f1(x4391,x4391),x4392),f1(a3,x4392))),f5(f5(f4(a2),a2),a3))), % 201.05/201.25 inference(scs_inference,[],[78,75,431,34,7,2,3])). % 201.05/201.25 cnf(441,plain, % 201.05/201.25 (~E(f5(f5(f4(a2),a2),a3),f4(f1(f1(f1(x4411,x4411),x4412),f1(a3,x4412))))), % 201.05/201.25 inference(scs_inference,[],[439,2])). % 201.05/201.25 cnf(445,plain, % 201.05/201.25 (~E(f1(f1(x4451,x4451),f1(f1(f1(x4452,x4452),x4453),f1(a3,x4453))),f1(a3,f5(f4(a2),a2)))), % 201.05/201.25 inference(scs_inference,[],[438,434,50,2,3])). % 201.05/201.25 cnf(449,plain, % 201.05/201.25 (E(f1(x4491,f1(f1(x4492,x4492),f1(x4493,x4493))),f1(x4491,f1(f1(f1(x4494,x4494),f1(x4495,x4495)),f1(x4496,x4496))))), % 201.05/201.25 inference(scs_inference,[],[318,438,434,50,2,3,4,6,5])). % 201.05/201.25 cnf(451,plain, % 201.05/201.25 (~E(f1(a3,f5(f4(a2),a2)),f1(f1(x4511,x4511),f1(f1(f1(x4512,x4512),x4513),f1(a3,x4513))))), % 201.05/201.25 inference(scs_inference,[],[445,2])). % 201.05/201.25 cnf(455,plain, % 201.05/201.25 (~E(f1(f5(f4(a2),a2),f5(x4551,f1(f4(a3),x4551))),f5(f5(x4552,f1(x4553,x4552)),f1(a3,x4553)))), % 201.05/201.25 inference(scs_inference,[],[123,113,70,2,3])). % 201.05/201.25 cnf(458,plain, % 201.05/201.25 (~E(f5(f5(x4581,f1(x4582,x4581)),f1(a3,x4582)),f1(f5(f4(a2),a2),f5(x4583,f1(f4(a3),x4583))))), % 201.05/201.25 inference(scs_inference,[],[455,2])). % 201.05/201.25 cnf(461,plain, % 201.05/201.25 (E(f1(x4611,x4611),f1(f1(f1(x4612,x4612),f1(x4613,x4613)),f1(f1(x4614,x4614),f1(x4615,x4615))))), % 201.05/201.25 inference(scs_inference,[],[262,2])). % 201.05/201.25 cnf(462,plain, % 201.05/201.25 (~E(f5(f1(x4621,x4621),f1(a3,f1(x4622,x4622))),f5(f5(f4(a2),a2),f5(x4623,f1(a3,x4623))))), % 201.05/201.25 inference(scs_inference,[],[262,116,27,2,3])). % 201.05/201.25 cnf(472,plain, % 201.05/201.25 (E(f1(x4721,x4721),f5(f1(f1(x4722,x4722),f1(x4723,x4723)),f4(f1(x4724,x4724))))), % 201.05/201.25 inference(scs_inference,[],[373,2])). % 201.05/201.25 cnf(475,plain, % 201.05/201.25 (~E(f1(f1(x4751,x4751),f1(a3,f5(f4(a2),a2))),f1(f1(x4752,x4752),a3))), % 201.05/201.25 inference(scs_inference,[],[373,94,53,2,3,5])). % 201.05/201.25 cnf(477,plain, % 201.05/201.25 (~E(f1(f1(x4771,x4771),a3),f1(f1(x4772,x4772),f1(a3,f5(f4(a2),a2))))), % 201.05/201.25 inference(scs_inference,[],[475,2])). % 201.05/201.25 cnf(479,plain, % 201.05/201.25 (E(f5(f1(f1(x4791,x4791),f1(x4792,x4792)),f1(f1(x4793,x4793),f1(x4794,x4794))),f1(f4(f1(x4795,x4795)),f1(x4796,x4796)))), % 201.05/201.25 inference(scs_inference,[],[124,421,475,2,5,3])). % 201.05/201.25 cnf(492,plain, % 201.05/201.25 (E(f5(x4921,f1(x4922,x4922)),f5(x4921,f1(f1(x4923,x4923),f1(x4924,x4924))))), % 201.05/201.25 inference(scs_inference,[],[230,2])). % 201.05/201.25 cnf(494,plain, % 201.05/201.25 (~E(f1(f5(x4941,f1(a3,x4941)),f5(f4(a2),a2)),f1(f1(x4942,x4942),f1(f1(f1(x4943,x4943),x4944),f1(a3,x4944))))), % 201.05/201.25 inference(scs_inference,[],[230,451,71,2,5,3])). % 201.05/201.25 cnf(498,plain, % 201.05/201.25 (E(f5(f1(x4981,x4981),f4(f1(x4982,x4982))),f5(x4983,f1(f1(x4984,x4984),x4983)))), % 201.05/201.25 inference(scs_inference,[],[283,404,494,2,3])). % 201.05/201.25 cnf(502,plain, % 201.05/201.25 (~E(f5(f5(f4(a2),a2),f5(x5021,f1(a3,x5021))),f4(f1(f1(f1(x5022,x5022),x5023),f1(a3,x5023))))), % 201.05/201.25 inference(scs_inference,[],[366,441,74,2,3])). % 201.05/201.25 cnf(508,plain, % 201.05/201.25 (E(f1(f4(f1(x5081,x5081)),f4(f1(x5082,x5082))),f1(f4(f1(x5083,x5083)),f1(x5084,x5084)))), % 201.05/201.25 inference(scs_inference,[],[124,352,502,2,3])). % 201.05/201.25 cnf(511,plain, % 201.05/201.25 (~E(f1(f1(x5111,x5111),f5(x5112,f1(a3,x5112))),f1(f1(x5113,x5113),f1(a3,f5(f4(a2),a2))))), % 201.05/201.25 inference(scs_inference,[],[375,199,477,2,3])). % 201.05/201.25 cnf(516,plain, % 201.05/201.25 (~E(f5(x5161,f1(a3,x5161)),f1(a3,f5(f4(a2),a2)))), % 201.05/201.25 inference(scs_inference,[],[511,5])). % 201.05/201.25 cnf(517,plain, % 201.05/201.25 (~E(f1(f1(x5171,x5171),f5(x5172,f1(a3,x5172))),f1(f1(x5173,x5173),f1(a3,f5(f4(a2),a2))))), % 201.05/201.25 inference(rename_variables,[],[511])). % 201.05/201.25 cnf(518,plain, % 201.05/201.25 (~E(f1(f1(x5181,x5181),f1(a3,f5(f4(a2),a2))),f1(f1(x5182,x5182),f5(x5183,f1(a3,x5183))))), % 201.05/201.25 inference(scs_inference,[],[511,517,5,2])). % 201.05/201.25 cnf(519,plain, % 201.05/201.25 (E(f1(f1(f1(x5191,x5191),f1(x5192,x5192)),f4(f1(x5193,x5193))),f5(f4(f1(x5194,x5194)),f1(x5195,x5195)))), % 201.05/201.25 inference(scs_inference,[],[124,385,511,517,5,2,3])). % 201.05/201.25 cnf(522,plain, % 201.05/201.25 (E(f5(x5221,f4(x5221)),f1(f1(x5222,x5222),f1(f1(x5223,x5223),f1(x5224,x5224))))), % 201.05/201.25 inference(scs_inference,[],[394,5,2])). % 201.05/201.25 cnf(523,plain, % 201.05/201.25 (~E(f5(f1(x5231,x5231),f1(a3,f4(f1(x5232,x5232)))),f1(a3,f5(f4(a2),a2)))), % 201.05/201.25 inference(scs_inference,[],[394,122,516,5,2,3])). % 201.05/201.25 cnf(529,plain, % 201.05/201.25 (~E(f1(a3,f5(f4(a2),a2)),f5(x5291,f1(a3,x5291)))), % 201.05/201.25 inference(scs_inference,[],[518,5])). % 201.05/201.25 cnf(532,plain, % 201.05/201.25 (E(f1(f1(f1(x5321,x5321),f1(x5322,x5322)),f4(f1(x5323,x5323))),f5(f5(x5324,f1(x5325,x5324)),f4(x5325)))), % 201.05/201.25 inference(scs_inference,[],[124,415,518,523,5,2,3])). % 201.05/201.25 cnf(535,plain, % 201.05/201.25 (E(f1(f1(x5351,x5351),x5352),f1(f4(x5352),f4(f1(x5353,x5353))))), % 201.05/201.25 inference(scs_inference,[],[125,399,5,2])). % 201.05/201.25 cnf(536,plain, % 201.05/201.25 (~E(f1(a3,f5(x5361,f1(f5(f4(a2),a2),x5361))),f5(x5362,f1(a3,x5362)))), % 201.05/201.25 inference(scs_inference,[],[125,399,529,70,5,2,3])). % 201.05/201.25 cnf(542,plain, % 201.05/201.25 (E(f1(f1(x5421,x5421),x5422),f5(f4(x5422),f4(f1(x5423,x5423))))), % 201.05/201.25 inference(scs_inference,[],[406,2])). % 201.05/201.25 cnf(548,plain, % 201.05/201.25 (~E(f5(x5481,f1(a3,x5481)),f1(a3,f5(x5482,f1(f5(f4(a2),a2),x5482))))), % 201.05/201.25 inference(scs_inference,[],[536,2])). % 201.05/201.25 cnf(549,plain, % 201.05/201.25 (E(f4(f4(f1(x5491,x5491))),f4(f1(f1(x5492,x5492),f1(x5493,x5493))))), % 201.05/201.25 inference(scs_inference,[],[125,286,536,2,3])). % 201.05/201.25 cnf(560,plain, % 201.05/201.25 (E(f1(f5(x5601,f1(x5602,x5601)),x5602),f1(f1(x5603,x5603),f1(x5604,x5604)))), % 201.05/201.25 inference(scs_inference,[],[217,2])). % 201.05/201.25 cnf(561,plain, % 201.05/201.25 (~E(f5(f5(x5611,f1(a3,x5611)),f1(f1(x5612,x5612),f1(x5613,x5613))),f1(f5(f4(a2),a2),f5(x5614,f1(f4(a3),x5614))))), % 201.05/201.25 inference(scs_inference,[],[217,492,458,2,3])). % 201.05/201.25 cnf(568,plain, % 201.05/201.25 (E(f4(f4(f1(x5681,x5681))),f5(f1(x5682,x5682),f4(f1(x5683,x5683))))), % 201.05/201.25 inference(scs_inference,[],[125,356,561,2,3])). % 201.05/201.25 cnf(570,plain, % 201.05/201.25 (E(x5701,f1(f5(x5702,f1(x5701,x5702)),f4(f1(x5703,x5703))))), % 201.05/201.25 inference(scs_inference,[],[267,2])). % 201.05/201.25 cnf(579,plain, % 201.05/201.25 (E(f1(f4(x5791),f1(f1(x5792,x5792),x5791)),f4(f1(x5793,x5793)))), % 201.05/201.25 inference(scs_inference,[],[409,2])). % 201.05/201.25 cnf(598,plain, % 201.05/201.25 (E(x5981,f1(f5(x5982,f1(x5983,x5982)),f1(f1(x5983,x5984),f1(x5981,x5984))))), % 201.05/201.25 inference(scs_inference,[],[90,2])). % 201.05/201.25 cnf(605,plain, % 201.05/201.25 (~E(f1(f1(a3,x6051),f1(a3,x6051)),f5(x6052,f1(f5(f4(a2),a2),x6052)))), % 201.05/201.25 inference(scs_inference,[],[126,42,90,548,2,3,4,6,8,5])). % 201.05/201.25 cnf(607,plain, % 201.05/201.25 (~E(f5(x6071,f1(f5(f4(a2),a2),x6071)),f1(f1(a3,x6072),f1(a3,x6072)))), % 201.05/201.25 inference(scs_inference,[],[579,605,5,2])). % 201.05/201.25 cnf(608,plain, % 201.05/201.25 (~E(f1(f1(x6081,x6081),f1(f1(x6082,x6082),f1(x6083,x6083))),f5(x6084,f1(f5(f4(a2),a2),x6084)))), % 201.05/201.25 inference(scs_inference,[],[579,236,605,5,2,3])). % 201.05/201.25 cnf(611,plain, % 201.05/201.25 (E(f1(f4(f1(x6111,x6111)),f1(x6112,x6112)),f5(f1(f1(x6113,x6113),f1(x6114,x6114)),f1(f1(x6115,x6115),f1(x6116,x6116))))), % 201.05/201.25 inference(scs_inference,[],[479,2])). % 201.05/201.25 cnf(612,plain, % 201.05/201.25 (~E(f5(f1(x6121,x6121),f4(f1(x6122,x6122))),f5(x6123,f1(f5(f4(a2),a2),x6123)))), % 201.05/201.25 inference(scs_inference,[],[412,479,608,2,3])). % 201.05/201.25 cnf(616,plain, % 201.05/201.25 (~E(f4(f1(x6161,x6161)),f1(f5(f4(a2),a2),f1(x6162,x6162)))), % 201.05/201.25 inference(scs_inference,[],[612,7])). % 201.05/201.25 cnf(617,plain, % 201.05/201.25 (~E(f5(f1(x6171,x6171),f4(f1(x6172,x6172))),f5(x6173,f1(f5(f4(a2),a2),x6173)))), % 201.05/201.25 inference(rename_variables,[],[612])). % 201.05/201.25 cnf(619,plain, % 201.05/201.25 (~E(f5(f1(x6191,x6191),f1(x6192,x6192)),f5(x6193,f1(f5(f4(a2),a2),x6193)))), % 201.05/201.25 inference(scs_inference,[],[126,612,617,7,2,3])). % 201.05/201.25 cnf(621,plain, % 201.05/201.25 (~E(f1(x6211,x6211),f5(f4(a2),a2))), % 201.05/201.25 inference(scs_inference,[],[126,612,617,7,2,3,6])). % 201.05/201.25 cnf(625,plain, % 201.05/201.25 (E(f1(f4(f1(x6251,x6251)),f1(x6252,x6252)),f1(f4(f1(x6253,x6253)),f4(f1(x6254,x6254))))), % 201.05/201.25 inference(scs_inference,[],[418,508,6,7,5,2])). % 201.05/201.25 cnf(626,plain, % 201.05/201.25 (~E(f1(f1(f1(x6261,x6261),f1(x6262,x6262)),f1(f1(x6263,x6263),f1(x6264,x6264))),f5(f4(a2),a2))), % 201.05/201.25 inference(scs_inference,[],[621,418,461,508,6,7,5,2,3])). % 201.05/201.25 cnf(630,plain, % 201.05/201.25 (~E(f1(x6301,x6301),f1(f5(f4(a2),a2),f1(x6302,x6302)))), % 201.05/201.25 inference(scs_inference,[],[619,7])). % 201.05/201.25 cnf(632,plain, % 201.05/201.25 (~E(f5(f4(a2),a2),f1(x6321,x6321))), % 201.05/201.25 inference(scs_inference,[],[619,7,5])). % 201.05/201.25 cnf(633,plain, % 201.05/201.25 (~E(f1(f5(f4(a2),a2),f1(x6331,x6331)),f4(f1(x6332,x6332)))), % 201.05/201.25 inference(scs_inference,[],[616,619,7,5,2])). % 201.05/201.25 cnf(634,plain, % 201.05/201.25 (~E(f5(f1(f1(x6341,x6341),f1(x6342,x6342)),f4(f1(x6343,x6343))),f5(f4(a2),a2))), % 201.05/201.25 inference(scs_inference,[],[616,472,626,619,7,5,2,3])). % 201.05/201.25 cnf(641,plain, % 201.05/201.25 (~E(f1(f5(x6411,f1(x6412,x6411)),f1(f1(x6412,x6413),f1(f5(f4(a2),a2),x6413))),f1(x6414,x6414))), % 201.05/201.25 inference(scs_inference,[],[632,522,598,519,6,7,5,2,3])). % 201.05/201.25 cnf(647,plain, % 201.05/201.25 (~E(f1(f5(f4(a2),a2),f1(x6471,x6471)),f1(x6472,x6472))), % 201.05/201.25 inference(scs_inference,[],[630,535,641,4,5,2])). % 201.05/201.25 cnf(648,plain, % 201.05/201.25 (~E(f5(f1(f1(x6481,x6481),f1(x6482,x6482)),f1(x6483,x6483)),f5(f4(a2),a2))), % 201.05/201.25 inference(scs_inference,[],[126,630,535,634,641,4,5,2,3])). % 201.05/201.25 cnf(652,plain, % 201.05/201.25 (~E(f1(f5(f4(a2),a2),f1(f1(f1(x6521,x6521),f1(x6522,x6522)),f1(x6523,x6523))),f1(x6524,x6524))), % 201.05/201.25 inference(scs_inference,[],[127,647,532,449,5,2,3])). % 201.05/201.25 cnf(658,plain, % 201.05/201.25 (~E(f1(f1(f1(x6581,x6581),f1(x6582,x6582)),f1(x6583,x6583)),f5(f4(a2),a2))), % 201.05/201.25 inference(scs_inference,[],[127,652,4,5])). % 201.05/201.25 cnf(660,plain, % 201.05/201.25 (~E(f5(f4(a2),a2),f5(f1(f1(x6601,x6601),f1(x6602,x6602)),f1(x6603,x6603)))), % 201.05/201.25 inference(scs_inference,[],[127,648,652,4,5,2])). % 201.05/201.25 cnf(661,plain, % 201.05/201.25 (~E(f4(f1(x6611,x6611)),f5(f4(a2),a2))), % 201.05/201.25 inference(scs_inference,[],[127,648,652,621,4,5,2,3])). % 201.05/201.25 cnf(665,plain, % 201.05/201.25 (E(f5(x6651,f1(f1(x6652,x6652),x6651)),f5(f1(x6653,x6653),f4(f1(x6654,x6654))))), % 201.05/201.25 inference(scs_inference,[],[542,498,5,2])). % 201.05/201.25 cnf(670,plain, % 201.05/201.25 (~E(f5(f4(a2),a2),f4(f1(x6701,x6701)))), % 201.05/201.25 inference(scs_inference,[],[661,2])). % 201.05/201.25 cnf(674,plain, % 201.05/201.25 (~E(f1(f4(f1(x6741,x6741)),f4(a2)),a2)), % 201.05/201.25 inference(scs_inference,[],[661,658,58,2,3,7])). % 201.05/201.25 cnf(681,plain, % 201.05/201.25 (~E(a2,f1(f4(f1(x6811,x6811)),f4(a2)))), % 201.05/201.25 inference(scs_inference,[],[674,2])). % 201.05/201.25 cnf(684,plain, % 201.05/201.26 (~E(f1(f1(x6841,x6841),f1(f5(f4(a2),a2),f1(a3,x6842))),f1(a3,x6842))), % 201.05/201.26 inference(scs_inference,[],[674,59,607,2,3,5])). % 201.05/201.26 cnf(687,plain, % 201.05/201.26 (~E(f1(f5(x6871,f1(a2,x6871)),f4(f1(x6872,x6872))),f1(f4(f1(x6873,x6873)),f4(a2)))), % 201.05/201.26 inference(scs_inference,[],[681,549,570,5,2,3])). % 201.05/201.26 cnf(691,plain, % 201.05/201.26 (E(f1(f4(f1(x6911,x6911)),f1(x6912,x6912)),f5(f1(x6913,x6913),f4(f1(x6914,x6914))))), % 201.05/201.26 inference(scs_inference,[],[684,611,665,2,3])). % 201.05/201.26 cnf(697,plain, % 201.05/201.26 (E(f5(f1(x6971,x6971),f4(f1(x6972,x6972))),f1(f4(f1(x6973,x6973)),f1(x6974,x6974)))), % 201.05/201.26 inference(scs_inference,[],[691,7,5,2])). % 201.05/201.26 cnf(698,plain, % 201.05/201.26 (~E(f5(f1(f1(x6981,x6981),a2),a2),f5(f1(f1(x6982,x6982),f1(x6983,x6983)),f1(x6984,x6984)))), % 201.05/201.26 inference(scs_inference,[],[660,691,87,7,5,2,3])). % 201.05/201.26 cnf(701,plain, % 201.05/201.26 (~E(f5(f1(f1(x7011,x7011),f1(x7012,x7012)),f1(x7013,x7013)),f5(f1(f1(x7014,x7014),a2),a2))), % 201.05/201.26 inference(scs_inference,[],[698,2])). % 201.05/201.26 cnf(702,plain, % 201.05/201.26 (~E(f1(f4(f1(x7021,x7021)),f1(x7022,x7022)),f5(f4(a2),a2))), % 201.05/201.26 inference(scs_inference,[],[697,698,634,2,3])). % 201.05/201.26 cnf(706,plain, % 201.05/201.26 (~E(f1(f4(f1(x7061,x7061)),f4(f1(x7062,x7062))),f5(f4(a2),a2))), % 201.05/201.26 inference(scs_inference,[],[702,568,625,2,3])). % 201.05/201.26 cnf(710,plain, % 201.05/201.26 (~E(f1(x7101,f5(x7102,f1(x7101,x7102))),f5(f4(a2),a2))), % 201.05/201.26 inference(scs_inference,[],[129,706,661,2,3])). % 201.05/201.26 cnf(713,plain, % 201.05/201.26 (E(f1(x7131,f5(x7132,f1(x7131,x7132))),f4(f1(x7133,x7133)))), % 201.05/201.26 inference(scs_inference,[],[129,2])). % 201.05/201.26 cnf(722,plain, % 201.05/201.26 (~E(f5(x7221,f1(f5(f4(a2),a2),x7221)),f1(x7222,x7222))), % 201.05/201.26 inference(scs_inference,[],[129,710,616,2,3,5])). % 201.05/201.26 cnf(741,plain, % 201.05/201.26 (E(f1(x7411,x7411),f4(f1(x7412,x7412)))), % 201.05/201.26 inference(scs_inference,[],[119,2])). % 201.05/201.26 cnf(743,plain, % 201.05/201.26 (~E(f5(f4(a2),a2),f1(f1(x7431,x7431),f1(x7432,x7432)))), % 201.05/201.26 inference(scs_inference,[],[9,119,670,2,6,3])). % 201.05/201.26 cnf(751,plain, % 201.05/201.26 (~E(f4(f1(x7511,x7511)),f1(f5(f4(a2),a2),f4(f1(x7512,x7512))))), % 201.05/201.26 inference(scs_inference,[],[124,63,105,616,2,5,7,8,4,6,3])). % 201.05/201.26 cnf(762,plain, % 201.05/201.26 (E(f4(x7621),f1(f1(f1(x7622,x7622),f1(x7623,x7623)),x7621))), % 201.05/201.26 inference(scs_inference,[],[325,2])). % 201.05/201.26 cnf(793,plain, % 201.05/201.26 (~E(f5(f4(a2),a2),f1(f1(x7931,x7931),f1(f1(x7932,x7932),f1(x7933,x7933))))), % 201.05/201.26 inference(scs_inference,[],[127,233,325,670,146,4,7,5,6,2,8,3])). % 201.05/201.26 cnf(878,plain, % 201.05/201.26 (E(f1(f1(f1(x8781,x8781),x8782),f4(x8782)),f1(f1(x8783,x8783),f1(x8784,x8784)))), % 201.05/201.26 inference(scs_inference,[],[168,19,138,166,8,7,4,6,2])). % 201.05/201.26 cnf(904,plain, % 201.05/201.26 (E(f5(f1(f1(x9041,x9041),f1(x9042,x9042)),f1(x9043,x9043)),f4(f1(x9044,x9044)))), % 201.05/201.26 inference(scs_inference,[],[179,201,332,242,7,8,5,6,2])). % 201.05/201.26 cnf(913,plain, % 201.05/201.26 (E(f1(x9131,f5(x9132,f4(f1(x9133,x9133)))),f1(x9131,x9132))), % 201.05/201.26 inference(scs_inference,[],[201,332,79,344,8,7,2,4,6,5])). % 201.05/201.26 cnf(937,plain, % 201.05/201.26 (E(x9371,f5(x9371,f1(f1(x9372,x9372),f1(x9373,x9373))))), % 201.05/201.26 inference(scs_inference,[],[79,117,231,143,380,7,8,6,5,2])). % 201.05/201.26 cnf(947,plain, % 201.05/201.26 (E(f1(x9471,f4(f1(x9472,x9472))),f1(x9471,f5(f1(x9473,x9473),f1(x9474,x9474))))), % 201.05/201.26 inference(scs_inference,[],[117,231,143,176,211,8,7,2,4,6,5])). % 201.05/201.26 cnf(1033,plain, % 201.05/201.26 (E(f1(x10331,f5(f1(x10332,x10332),f1(x10333,f1(x10334,x10334)))),f1(x10331,x10333))), % 201.05/201.26 inference(scs_inference,[],[64,30,72,8,7,5])). % 201.05/201.26 cnf(1169,plain, % 201.05/201.26 (E(f5(f4(f1(x11691,x11691)),f1(x11692,x11692)),f1(f1(x11693,x11693),f1(x11694,x11694)))), % 201.05/201.26 inference(scs_inference,[],[397,15,156,390,8,6,7,4,2])). % 201.05/201.26 cnf(1258,plain, % 201.05/201.26 (E(f4(f1(f1(x12581,x12581),x12582)),f1(f1(x12583,x12583),f4(x12582)))), % 201.05/201.26 inference(scs_inference,[],[273,283,310,382,354,8,5,4,6,7,2])). % 201.05/201.26 cnf(1318,plain, % 201.05/201.26 (~E(f5(f1(x13181,x13181),f1(a3,f1(x13182,x13182))),f5(f5(f4(a2),a2),a3))), % 201.05/201.26 inference(scs_inference,[],[49,53,70,76,74,462,913,8,5,4,6,7,2,3])). % 201.05/201.26 cnf(1628,plain, % 201.05/201.26 (E(f5(f1(x16281,f1(f1(x16282,x16282),f1(x16283,x16281))),x16284),f5(x16283,x16284))), % 201.05/201.26 inference(scs_inference,[],[560,55,4,6])). % 201.05/201.26 cnf(1638,plain, % 201.05/201.26 (E(f5(x16381,f1(x16382,f1(f1(x16383,x16383),f1(x16384,x16382)))),f5(x16381,x16384))), % 201.05/201.26 inference(scs_inference,[],[713,55,85,86,4,8,6,7])). % 201.05/201.26 cnf(1718,plain, % 201.05/201.26 (E(f5(x17181,f1(x17182,f1(f1(x17182,x17183),f1(x17184,x17183)))),f5(x17181,x17184))), % 201.05/201.26 inference(scs_inference,[],[449,11,78,81,4,8,6,7])). % 201.05/201.26 cnf(2293,plain, % 201.05/201.26 (~E(f5(f5(f4(a2),a2),f1(x22931,x22931)),f4(f1(x22932,x22932)))), % 201.05/201.26 inference(scs_inference,[],[10,633,743,2,3])). % 201.05/201.26 cnf(2296,plain, % 201.05/201.26 (~E(f4(f1(x22961,x22961)),f5(f5(f4(a2),a2),f1(x22962,x22962)))), % 201.05/201.26 inference(scs_inference,[],[2293,2])). % 201.05/201.26 cnf(2304,plain, % 201.05/201.26 (~E(f5(f5(f4(a2),a2),f1(f1(x23041,x23041),f1(x23042,x23042))),f1(x23043,x23043))), % 201.05/201.26 inference(scs_inference,[],[937,793,632,2,3])). % 201.05/201.26 cnf(2307,plain, % 201.05/201.26 (E(f1(f1(f1(x23071,x23071),x23072),f4(x23072)),f1(x23073,x23073))), % 201.05/201.26 inference(scs_inference,[],[11,878,2304,2,3])). % 201.05/201.26 cnf(2316,plain, % 201.05/201.26 (~E(f5(f1(x23161,x23161),a3),f5(f5(f4(a2),a2),a3))), % 201.05/201.26 inference(scs_inference,[],[1638,2307,1318,5,8,2,7,6,4,3])). % 201.05/201.26 cnf(2319,plain, % 201.05/201.26 (~E(f1(f5(f4(a2),a2),f4(f1(x23191,x23191))),f4(f1(x23192,x23192)))), % 201.05/201.26 inference(scs_inference,[],[751,2])). % 201.05/201.26 cnf(2320,plain, % 201.05/201.26 (~E(f5(f1(f1(f5(f4(a2),a2),x23201),f1(x23202,x23201)),x23202),f1(x23203,x23203))), % 201.05/201.26 inference(scs_inference,[],[1718,722,751,2,3])). % 201.05/201.26 cnf(2324,plain, % 201.05/201.26 (~E(f1(f1(x23241,x23241),f4(f1(x23242,x23242))),f5(f5(f4(a2),a2),f1(x23243,x23243)))), % 201.05/201.26 inference(scs_inference,[],[1258,2320,2296,2,3])). % 201.05/201.26 cnf(2328,plain, % 201.05/201.26 (~E(f5(f1(x23281,x23281),f1(x23282,x23282)),f5(f1(f1(x23283,x23283),a2),a2))), % 201.05/201.26 inference(scs_inference,[],[1628,2324,701,2,3])). % 201.05/201.26 cnf(2332,plain, % 201.05/201.26 (~E(f1(f5(f4(a2),a2),f5(f1(x23321,x23321),f1(x23322,x23322))),f4(f1(x23323,x23323)))), % 201.05/201.26 inference(scs_inference,[],[947,2319,687,2,3])). % 201.05/201.26 cnf(2335,plain, % 201.05/201.26 (~E(f4(f1(x23351,x23351)),f1(f5(f4(a2),a2),f5(f1(x23352,x23352),f1(x23353,x23353))))), % 201.05/201.26 inference(scs_inference,[],[2332,2])). % 201.05/201.26 cnf(2340,plain, % 201.05/201.26 (~E(f1(f1(f1(x23401,x23401),f1(x23402,x23402)),f1(x23403,x23403)),f1(f5(f4(a2),a2),f5(f1(x23404,x23404),f1(x23405,x23405))))), % 201.05/201.26 inference(scs_inference,[],[762,2335,2316,2,3])). % 201.05/201.26 cnf(2342,plain, % 201.05/201.26 (~E(f1(f5(f4(a2),a2),f5(f1(x23421,x23421),f1(x23422,x23422))),f1(f1(f1(x23423,x23423),f1(x23424,x23424)),f1(x23425,x23425)))), % 201.05/201.26 inference(scs_inference,[],[2340,2])). % 201.05/201.26 cnf(2343,plain, % 201.05/201.26 (~E(f4(f1(x23431,x23431)),f5(f1(f1(x23432,x23432),a2),a2))), % 201.05/201.26 inference(scs_inference,[],[904,2340,2328,2,3])). % 201.05/201.26 cnf(2346,plain, % 201.05/201.26 (~E(f5(f1(f1(x23461,x23461),a2),a2),f4(f1(x23462,x23462)))), % 201.05/201.26 inference(scs_inference,[],[2343,2])). % 201.05/201.26 cnf(2347,plain, % 201.05/201.26 (~E(f1(f5(f4(a2),a2),f1(x23471,x23471)),f1(f1(f1(x23472,x23472),f1(x23473,x23473)),f1(x23474,x23474)))), % 201.05/201.26 inference(scs_inference,[],[1033,2342,2343,2,3])). % 201.05/201.26 cnf(2351,plain, % 201.05/201.26 (E(f5(f4(f1(x23511,x23511)),f1(x23512,x23512)),f1(x23513,x23513))), % 201.05/201.26 inference(scs_inference,[],[11,1169,2347,2,3])). % 201.05/201.26 cnf(2434,plain, % 201.05/201.26 ($false), % 201.05/201.26 inference(scs_inference,[],[741,14,2346,2351,2,3]), % 201.05/201.26 ['proof']). % 201.05/201.26 % SZS output end Proof % 201.05/201.26 % Total time :200.280000s %------------------------------------------------------------------------------