%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : GRP704-11 : TPTP v8.2.0. Released v8.1.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n020.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:40:31 EDT 2024 % Result : Unsatisfiable 189.69s 189.69s % Output : CNFRefutation 189.69s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : GRP704-11 : TPTP v8.2.0. Released v8.1.0. % 0.06/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n020.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 11:51:24 EDT 2024 % 0.12/0.33 % CPUTime : % 0.47/0.58 start to proof:theBenchmark % 189.64/189.68 %------------------------------------------- % 189.64/189.68 % File :CSE---1.7 % 189.64/189.68 % Problem :theBenchmark % 189.64/189.68 % Transform :cnf % 189.64/189.68 % Format :tptp:raw % 189.64/189.68 % Command :java -jar mcs_scs.jar %d %s % 189.64/189.68 % 189.64/189.68 % Result :Theorem 189.050000s % 189.64/189.68 % Output :CNFRefutation 189.050000s % 189.64/189.68 %------------------------------------------- % 189.69/189.68 %------------------------------------------------------------------------------ % 189.69/189.68 % File : GRP704-11 : TPTP v8.2.0. Released v8.1.0. % 189.69/189.68 % Domain : Group Theory (Quasigroups) % 189.69/189.69 % Problem : In C-loops the nucleus is normal - c % 189.69/189.69 % Version : Especial. % 189.69/189.69 % English : % 189.69/189.69 % 189.69/189.69 % Refs : [PV06] Phillips & Vojtechovsky (2006), C-loops: an Introducti % 189.69/189.69 % : [PS08] Phillips & Stanovsky (2008), Automated Theorem Proving % 189.69/189.69 % : [Sma21] Smallbone (2021), Email to Geoff Sutcliffe % 189.69/189.69 % Source : [Sma21] % 189.69/189.69 % Names : % 189.69/189.69 % 189.69/189.69 % Status : Unsatisfiable % 189.69/189.69 % Rating : 0.00 v8.2.0, 0.04 v8.1.0 % 189.69/189.69 % Syntax : Number of clauses : 14 ( 14 unt; 0 nHn; 1 RR) % 189.69/189.69 % Number of literals : 14 ( 14 equ; 1 neg) % 189.69/189.69 % Maximal clause size : 1 ( 1 avg) % 189.69/189.69 % Maximal term depth : 5 ( 2 avg) % 189.69/189.69 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty) % 189.69/189.69 % Number of functors : 10 ( 10 usr; 7 con; 0-2 aty) % 189.69/189.69 % Number of variables : 24 ( 0 sgn) % 189.69/189.69 % SPC : CNF_UNS_RFO_PEQ_UEQ % 189.69/189.69 % 189.69/189.69 % Comments : UEQ version, converted from GRP704+1.p % 189.69/189.69 %------------------------------------------------------------------------------ % 189.69/189.69 cnf(f01,axiom, % 189.69/189.69 mult(A,ld(A,B)) = B ). % 189.69/189.69 % 189.69/189.69 cnf(f02,axiom, % 189.69/189.69 ld(A,mult(A,B)) = B ). % 189.69/189.69 % 189.69/189.69 cnf(f03,axiom, % 189.69/189.69 mult(rd(A,B),B) = A ). % 189.69/189.69 % 189.69/189.69 cnf(f04,axiom, % 189.69/189.69 rd(mult(A,B),B) = A ). % 189.69/189.69 % 189.69/189.69 cnf(f05,axiom, % 189.69/189.69 mult(A,unit) = A ). % 189.69/189.69 % 189.69/189.69 cnf(f06,axiom, % 189.69/189.69 mult(unit,A) = A ). % 189.69/189.69 % 189.69/189.69 cnf(f07,axiom, % 189.69/189.69 mult(A,mult(B,mult(B,C))) = mult(mult(mult(A,B),B),C) ). % 189.69/189.69 % 189.69/189.69 cnf(f08,axiom, % 189.69/189.69 mult(op_c,mult(A,B)) = mult(mult(op_c,A),B) ). % 189.69/189.69 % 189.69/189.69 cnf(f09,axiom, % 189.69/189.69 mult(A,mult(B,op_c)) = mult(mult(A,B),op_c) ). % 189.69/189.69 % 189.69/189.69 cnf(f10,axiom, % 189.69/189.69 mult(A,mult(op_c,B)) = mult(mult(A,op_c),B) ). % 189.69/189.69 % 189.69/189.69 cnf(f11,axiom, % 189.69/189.69 op_d = ld(A,mult(op_c,A)) ). % 189.69/189.69 % 189.69/189.69 cnf(f12,axiom, % 189.69/189.69 op_e = mult(mult(rd(op_c,mult(A,B)),B),A) ). % 189.69/189.69 % 189.69/189.69 cnf(f13,axiom, % 189.69/189.69 op_f = mult(A,mult(B,ld(mult(A,B),op_c))) ). % 189.69/189.69 % 189.69/189.69 cnf(goal,negated_conjecture, % 189.69/189.69 mult(x4,mult(x5,op_f)) != mult(mult(x4,x5),op_f) ). % 189.69/189.69 % 189.69/189.69 %------------------------------------------------------------------------------ % 189.69/189.69 %------------------------------------------- % 189.69/189.69 % Proof found % 189.69/189.69 % SZS status Theorem for theBenchmark % 189.69/189.69 % SZS output start Proof % 189.69/189.69 %ClaNum:23(EqnAxiom:9) % 189.69/189.69 %VarNum:50(SingletonVarNum:24) % 189.69/189.69 %MaxLitNum:1 % 189.69/189.69 %MaxfuncDepth:4 % 189.69/189.69 %SharedTerms:12 % 189.69/189.69 %goalClause: 23 % 189.69/189.69 %singleGoalClaCount:1 % 189.69/189.69 [23]~E(f2(f2(a9,a10),a7),f2(a9,f2(a10,a7))) % 189.69/189.69 [10]E(f2(x101,a1),x101) % 189.69/189.69 [11]E(f2(a1,x111),x111) % 189.69/189.69 [12]E(f3(x121,f2(a4,x121)),a5) % 189.69/189.69 [13]E(f3(x131,f2(x131,x132)),x132) % 189.69/189.69 [14]E(f2(x141,f3(x141,x142)),x142) % 189.69/189.69 [15]E(f2(f6(x151,x152),x152),x151) % 189.69/189.69 [16]E(f6(f2(x161,x162),x162),x161) % 189.69/189.69 [17]E(f2(f2(x171,a4),x172),f2(x171,f2(a4,x172))) % 189.69/189.69 [18]E(f2(f2(x181,x182),a4),f2(x181,f2(x182,a4))) % 189.69/189.69 [19]E(f2(f2(a4,x191),x192),f2(a4,f2(x191,x192))) % 189.69/189.69 [21]E(f2(x211,f2(x212,f3(f2(x211,x212),a4))),a7) % 189.69/189.69 [22]E(f2(f2(f6(a4,f2(x221,x222)),x222),x221),a8) % 189.69/189.69 [20]E(f2(f2(f2(x201,x202),x202),x203),f2(x201,f2(x202,f2(x202,x203)))) % 189.69/189.69 %EqnAxiom % 189.69/189.69 [1]E(x11,x11) % 189.69/189.69 [2]E(x22,x21)+~E(x21,x22) % 189.69/189.69 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 189.69/189.69 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43)) % 189.69/189.69 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52)) % 189.69/189.69 [6]~E(x61,x62)+E(f6(x61,x63),f6(x62,x63)) % 189.69/189.69 [7]~E(x71,x72)+E(f6(x73,x71),f6(x73,x72)) % 189.69/189.69 [8]~E(x81,x82)+E(f3(x81,x83),f3(x82,x83)) % 189.69/189.69 [9]~E(x91,x92)+E(f3(x93,x91),f3(x93,x92)) % 189.69/189.69 % 189.69/189.69 %------------------------------------------- % 189.69/189.71 cnf(24,plain, % 189.69/189.71 (E(x241,f2(x241,a1))), % 189.69/189.71 inference(scs_inference,[],[10,2])). % 189.69/189.71 cnf(27,plain, % 189.69/189.71 (E(x271,f2(a1,x271))), % 189.69/189.71 inference(scs_inference,[],[11,2])). % 189.69/189.71 cnf(28,plain, % 189.69/189.71 (~E(f2(f2(a9,a10),a7),f2(a1,f2(a9,f2(a10,a7))))), % 189.69/189.71 inference(scs_inference,[],[23,11,2,3])). % 189.69/189.71 cnf(30,plain, % 189.69/189.71 (E(x301,f3(x302,f2(x302,x301)))), % 189.69/189.71 inference(scs_inference,[],[13,2])). % 189.69/189.71 cnf(31,plain, % 189.69/189.71 (~E(f2(f2(a9,a10),a7),f3(x311,f2(x311,f2(a9,f2(a10,a7)))))), % 189.69/189.71 inference(scs_inference,[],[23,13,2,3])). % 189.69/189.71 cnf(33,plain, % 189.69/189.71 (E(x331,f2(x332,f3(x332,x331)))), % 189.69/189.71 inference(scs_inference,[],[14,2])). % 189.69/189.71 cnf(34,plain, % 189.69/189.71 (~E(f2(f2(a9,a10),a7),f2(x341,f3(x341,f2(a9,f2(a10,a7)))))), % 189.69/189.71 inference(scs_inference,[],[23,14,2,3])). % 189.69/189.71 cnf(36,plain, % 189.69/189.71 (~E(a7,f3(f2(a9,a10),f2(a9,f2(a10,a7))))), % 189.69/189.71 inference(scs_inference,[],[23,14,2,3,5])). % 189.69/189.71 cnf(37,plain, % 189.69/189.71 (E(x371,f2(f6(x371,x372),x372))), % 189.69/189.71 inference(scs_inference,[],[15,2])). % 189.69/189.71 cnf(40,plain, % 189.69/189.71 (~E(f2(a9,a10),f6(f2(a9,f2(a10,a7)),a7))), % 189.69/189.71 inference(scs_inference,[],[23,15,2,3,4])). % 189.69/189.71 cnf(41,plain, % 189.69/189.71 (E(x411,f6(f2(x411,x412),x412))), % 189.69/189.71 inference(scs_inference,[],[16,2])). % 189.69/189.71 cnf(42,plain, % 189.69/189.71 (~E(f2(f2(a9,a10),a7),f6(f2(f2(a9,f2(a10,a7)),x421),x421))), % 189.69/189.71 inference(scs_inference,[],[23,16,2,3])). % 189.69/189.71 cnf(44,plain, % 189.69/189.71 (E(f2(x441,f2(a4,x442)),f2(f2(x441,a4),x442))), % 189.69/189.71 inference(scs_inference,[],[17,2])). % 189.69/189.71 cnf(45,plain, % 189.69/189.71 (E(x451,f2(a4,f2(x452,f3(f2(a4,x452),x451))))), % 189.69/189.71 inference(scs_inference,[],[33,17,19,2,3])). % 189.69/189.71 cnf(48,plain, % 189.69/189.71 (E(f2(a4,f2(x481,f3(f2(a4,x481),x482))),x482)), % 189.69/189.71 inference(scs_inference,[],[45,2])). % 189.69/189.71 cnf(49,plain, % 189.69/189.71 (E(a4,a5)), % 189.69/189.71 inference(scs_inference,[],[30,45,12,2,3])). % 189.69/189.71 cnf(52,plain, % 189.69/189.71 (E(a5,a4)), % 189.69/189.71 inference(scs_inference,[],[49,2])). % 189.69/189.71 cnf(53,plain, % 189.69/189.71 (E(f2(a4,f2(x531,f3(f2(a4,x531),a4))),a5)), % 189.69/189.71 inference(scs_inference,[],[48,49,2,3])). % 189.69/189.71 cnf(55,plain, % 189.69/189.71 (E(a5,f2(a4,f2(x551,f3(f2(a4,x551),a4))))), % 189.69/189.71 inference(scs_inference,[],[53,2])). % 189.69/189.71 cnf(56,plain, % 189.69/189.71 (E(f2(a4,f2(x561,f3(f2(a4,x561),a5))),a4)), % 189.69/189.71 inference(scs_inference,[],[52,48,53,2,3])). % 189.69/189.71 cnf(58,plain, % 189.69/189.71 (E(a4,f2(a4,f2(x581,f3(f2(a4,x581),a5))))), % 189.69/189.71 inference(scs_inference,[],[56,2])). % 189.69/189.71 cnf(59,plain, % 189.69/189.71 (E(f2(f6(a4,f2(x591,a4)),f2(a4,x591)),a8)), % 189.69/189.71 inference(scs_inference,[],[44,56,22,2,3])). % 189.69/189.71 cnf(62,plain, % 189.69/189.71 (E(a8,f2(f6(a4,f2(x621,a4)),f2(a4,x621)))), % 189.69/189.71 inference(scs_inference,[],[59,2])). % 189.69/189.71 cnf(63,plain, % 189.69/189.71 (E(a4,a8)), % 189.69/189.71 inference(scs_inference,[],[37,59,2,3])). % 189.69/189.71 cnf(66,plain, % 189.69/189.71 (E(a8,a4)), % 189.69/189.71 inference(scs_inference,[],[63,2])). % 189.69/189.71 cnf(67,plain, % 189.69/189.71 (E(a5,a8)), % 189.69/189.71 inference(scs_inference,[],[52,63,2,3])). % 189.69/189.71 cnf(68,plain, % 189.69/189.71 (E(a8,a5)), % 189.69/189.71 inference(scs_inference,[],[67,2])). % 189.69/189.71 cnf(69,plain, % 189.69/189.71 (E(a8,f2(a4,f2(x691,f3(f2(a4,x691),a5))))), % 189.69/189.71 inference(scs_inference,[],[58,66,67,2,3])). % 189.69/189.71 cnf(71,plain, % 189.69/189.71 (E(a8,f2(a4,f2(x711,f3(f2(a4,x711),a4))))), % 189.69/189.71 inference(scs_inference,[],[55,68,69,2,3])). % 189.69/189.71 cnf(72,plain, % 189.69/189.71 (E(f2(a4,f2(x721,f3(f2(a4,x721),a4))),a8)), % 189.69/189.71 inference(scs_inference,[],[71,2])). % 189.69/189.71 cnf(73,plain, % 189.69/189.71 (E(f2(x731,f3(f2(a1,x731),a4)),a7)), % 189.69/189.71 inference(scs_inference,[],[27,71,21,2,3])). % 189.69/189.71 cnf(76,plain, % 189.69/189.71 (E(a7,f2(x761,f3(f2(a1,x761),a4)))), % 189.69/189.71 inference(scs_inference,[],[73,2])). % 189.69/189.71 cnf(77,plain, % 189.69/189.71 (E(f2(a4,x771),f2(a4,f2(x771,a1)))), % 189.69/189.71 inference(scs_inference,[],[24,73,19,2,3])). % 189.69/189.71 cnf(80,plain, % 189.69/189.71 (E(f2(a4,f2(x801,a1)),f2(a4,x801))), % 189.69/189.71 inference(scs_inference,[],[77,2])). % 189.69/189.71 cnf(81,plain, % 189.69/189.71 (E(a7,f2(a4,f2(f3(f2(a1,a4),a4),a1)))), % 189.69/189.71 inference(scs_inference,[],[76,77,2,3])). % 189.69/189.71 cnf(84,plain, % 189.69/189.71 (E(f2(a4,f2(f3(f2(a1,a4),a4),a1)),a7)), % 189.69/189.71 inference(scs_inference,[],[81,2])). % 189.69/189.71 cnf(85,plain, % 189.69/189.71 (E(f2(x851,f2(x852,a4)),f2(f2(x851,x852),a4))), % 189.69/189.71 inference(scs_inference,[],[18,2])). % 189.69/189.71 cnf(86,plain, % 189.69/189.71 (E(f2(a4,f2(f2(x861,a4),a1)),f2(f2(a4,x861),a4))), % 189.69/189.71 inference(scs_inference,[],[80,18,2,3])). % 189.69/189.71 cnf(88,plain, % 189.69/189.71 (E(f2(f2(a4,x881),a4),f2(a4,f2(f2(x881,a4),a1)))), % 189.69/189.71 inference(scs_inference,[],[86,2])). % 189.69/189.71 cnf(92,plain, % 189.69/189.71 (E(f2(x921,f2(x922,f2(x922,x923))),f2(f2(f2(x921,x922),x922),x923))), % 189.69/189.71 inference(scs_inference,[],[20,2])). % 189.69/189.71 cnf(93,plain, % 189.69/189.71 (E(x931,f2(f2(f6(x931,f2(x932,a4)),x932),a4))), % 189.69/189.71 inference(scs_inference,[],[37,85,20,2,3])). % 189.69/189.71 cnf(96,plain, % 189.69/189.71 (E(f2(f2(f6(x961,f2(x962,a4)),x962),a4),x961)), % 189.69/189.71 inference(scs_inference,[],[93,2])). % 189.69/189.71 cnf(97,plain, % 189.69/189.71 (E(x971,f2(f2(f6(f6(f2(x971,x972),x972),f2(x973,a4)),x973),a4))), % 189.69/189.71 inference(scs_inference,[],[41,93,2,3])). % 189.69/189.71 cnf(99,plain, % 189.69/189.71 (E(f2(f2(f6(f6(f2(x991,x992),x992),f2(x993,a4)),x993),a4),x991)), % 189.69/189.71 inference(scs_inference,[],[97,2])). % 189.69/189.71 cnf(100,plain, % 189.69/189.71 (E(f2(f2(f6(a8,f2(x1001,a4)),x1001),a4),a4)), % 189.69/189.71 inference(scs_inference,[],[96,66,97,2,3])). % 189.69/189.71 cnf(102,plain, % 189.69/189.71 (E(a4,f2(f2(f6(a8,f2(x1021,a4)),x1021),a4))), % 189.69/189.71 inference(scs_inference,[],[100,2])). % 189.69/189.71 cnf(103,plain, % 189.69/189.71 (E(f2(f2(f6(f6(f2(a8,x1031),x1031),f2(x1032,a4)),x1032),a4),a5)), % 189.69/189.71 inference(scs_inference,[],[99,68,100,2,3])). % 189.69/189.71 cnf(105,plain, % 189.69/189.71 (E(a5,f2(f2(f6(f6(f2(a8,x1051),x1051),f2(x1052,a4)),x1052),a4))), % 189.69/189.71 inference(scs_inference,[],[103,2])). % 189.69/189.71 cnf(106,plain, % 189.69/189.71 (E(f2(f2(f6(a5,f2(x1061,a4)),x1061),a4),a4)), % 189.69/189.71 inference(scs_inference,[],[96,52,103,2,3])). % 189.69/189.71 cnf(108,plain, % 189.69/189.71 (E(a4,f2(f2(f6(a5,f2(x1081,a4)),x1081),a4))), % 189.69/189.71 inference(scs_inference,[],[106,2])). % 189.69/189.71 cnf(109,plain, % 189.69/189.71 (E(f2(f2(f6(f6(f2(a5,x1091),x1091),f2(x1092,a4)),x1092),a4),a4)), % 189.69/189.71 inference(scs_inference,[],[99,52,106,2,3])). % 189.69/189.71 cnf(111,plain, % 189.69/189.71 (E(a4,f2(f2(f6(f6(f2(a5,x1111),x1111),f2(x1112,a4)),x1112),a4))), % 189.69/189.71 inference(scs_inference,[],[109,2])). % 189.69/189.71 cnf(112,plain, % 189.69/189.71 (E(a8,f2(f2(f6(a5,f2(x1121,a4)),x1121),a4))), % 189.69/189.71 inference(scs_inference,[],[108,66,109,2,3])). % 189.69/189.71 cnf(114,plain, % 189.69/189.71 (E(f2(f6(a5,f2(a4,a4)),f2(a4,a4)),a4)), % 189.69/189.71 inference(scs_inference,[],[44,112,106,2,3])). % 189.69/189.71 cnf(117,plain, % 189.69/189.71 (E(a4,f2(f6(a5,f2(a4,a4)),f2(a4,a4)))), % 189.69/189.71 inference(scs_inference,[],[114,2])). % 189.69/189.71 cnf(118,plain, % 189.69/189.71 (E(f2(f2(a4,x1181),a4),f2(a4,f2(f2(f2(x1181,a4),a1),a1)))), % 189.69/189.71 inference(scs_inference,[],[88,114,77,2,3])). % 189.69/189.71 cnf(121,plain, % 189.69/189.71 (E(f2(a4,f2(a4,a4)),f2(a4,f2(f2(f2(a4,a4),a1),a1)))), % 189.69/189.71 inference(scs_inference,[],[44,118,2,3])). % 189.69/189.71 cnf(125,plain, % 189.69/189.71 (E(x1251,f2(a4,f2(f3(a4,x1251),a1)))), % 189.69/189.71 inference(scs_inference,[],[33,121,77,2,3])). % 189.69/189.71 cnf(128,plain, % 189.69/189.71 (E(f2(a4,f2(f3(a4,x1281),a1)),x1281)), % 189.69/189.71 inference(scs_inference,[],[125,2])). % 189.69/189.71 cnf(129,plain, % 189.69/189.71 (E(f2(f6(a4,f2(a1,x1291)),x1291),a8)), % 189.69/189.71 inference(scs_inference,[],[24,125,22,2,3])). % 189.69/189.71 cnf(132,plain, % 189.69/189.71 (E(a8,f2(f6(a4,f2(a1,x1321)),x1321))), % 189.69/189.71 inference(scs_inference,[],[129,2])). % 189.69/189.71 cnf(133,plain, % 189.69/189.71 (E(f2(a4,f2(f3(a4,a4),a1)),f2(f6(a5,f2(a4,a4)),f2(a4,a4)))), % 189.69/189.71 inference(scs_inference,[],[128,117,129,2,3])). % 189.69/189.71 cnf(135,plain, % 189.69/189.71 (E(f2(f6(a5,f2(a4,a4)),f2(a4,a4)),f2(a4,f2(f3(a4,a4),a1)))), % 189.69/189.71 inference(scs_inference,[],[133,2])). % 189.69/189.71 cnf(136,plain, % 189.69/189.71 (E(f2(a4,f2(f3(a4,a5),a1)),a4)), % 189.69/189.71 inference(scs_inference,[],[128,52,133,2,3])). % 189.69/189.71 cnf(138,plain, % 189.69/189.71 (E(a4,f2(a4,f2(f3(a4,a5),a1)))), % 189.69/189.71 inference(scs_inference,[],[136,2])). % 189.69/189.71 cnf(139,plain, % 189.69/189.71 (E(f2(a4,f2(f2(f3(a4,a5),a1),a1)),a4)), % 189.69/189.71 inference(scs_inference,[],[80,136,2,3])). % 189.69/189.71 cnf(141,plain, % 189.69/189.71 (E(a4,f2(a4,f2(f2(f3(a4,a5),a1),a1)))), % 189.69/189.71 inference(scs_inference,[],[139,2])). % 189.69/189.71 cnf(145,plain, % 189.69/189.71 (E(a5,f3(x1451,f2(a4,x1451)))), % 189.69/189.71 inference(scs_inference,[],[12,2])). % 189.69/189.71 cnf(146,plain, % 189.69/189.71 (E(a8,f3(x1461,f2(a4,x1461)))), % 189.69/189.71 inference(scs_inference,[],[68,12,2,3])). % 189.69/189.71 cnf(147,plain, % 189.69/189.71 (E(f3(x1471,f2(a4,x1471)),a8)), % 189.69/189.71 inference(scs_inference,[],[146,2])). % 189.69/189.71 cnf(148,plain, % 189.69/189.71 (E(f2(a4,f2(x1481,f3(f2(a4,x1481),a5))),f3(x1482,f2(a4,x1482)))), % 189.69/189.71 inference(scs_inference,[],[145,48,146,2,3])). % 189.69/189.71 cnf(150,plain, % 189.69/189.71 (E(f3(x1501,f2(a4,x1501)),f2(a4,f2(x1502,f3(f2(a4,x1502),a5))))), % 189.69/189.71 inference(scs_inference,[],[148,2])). % 189.69/189.71 cnf(151,plain, % 189.69/189.71 (E(f3(x1511,f2(a4,x1511)),f2(f6(a4,f2(a1,x1512)),x1512))), % 189.69/189.71 inference(scs_inference,[],[147,132,148,2,3])). % 189.69/189.71 cnf(152,plain, % 189.69/189.71 (E(f2(f6(a4,f2(a1,x1521)),x1521),f3(x1522,f2(a4,x1522)))), % 189.69/189.71 inference(scs_inference,[],[151,2])). % 189.69/189.71 cnf(153,plain, % 189.69/189.71 (E(f2(f2(f6(a5,f2(x1531,a4)),x1531),a4),f3(x1532,f2(a4,x1532)))), % 189.69/189.71 inference(scs_inference,[],[145,96,151,2,3])). % 189.69/189.71 cnf(155,plain, % 189.69/189.71 (E(f3(x1551,f2(a4,x1551)),f2(f2(f6(a5,f2(x1552,a4)),x1552),a4))), % 189.69/189.71 inference(scs_inference,[],[153,2])). % 189.69/189.71 cnf(156,plain, % 189.69/189.71 (E(a4,f3(x1561,f2(a4,x1561)))), % 189.69/189.71 inference(scs_inference,[],[108,153,2,3])). % 189.69/189.71 cnf(158,plain, % 189.69/189.71 (E(f3(x1581,f2(a4,x1581)),a4)), % 189.69/189.71 inference(scs_inference,[],[156,2])). % 189.69/189.71 cnf(159,plain, % 189.69/189.71 (E(f2(f2(f6(f6(f2(a5,x1591),x1591),f2(x1592,a4)),x1592),a4),a8)), % 189.69/189.71 inference(scs_inference,[],[99,156,67,2,3])). % 189.69/189.71 cnf(161,plain, % 189.69/189.71 (E(a8,f2(f2(f6(f6(f2(a5,x1611),x1611),f2(x1612,a4)),x1612),a4))), % 189.69/189.71 inference(scs_inference,[],[159,2])). % 189.69/189.71 cnf(162,plain, % 189.69/189.71 (E(f3(x1621,f2(a4,x1621)),f2(a4,f2(f3(a4,a5),a1)))), % 189.69/189.71 inference(scs_inference,[],[138,158,159,2,3])). % 189.69/189.71 cnf(163,plain, % 189.69/189.71 (E(f2(a4,f2(f3(a4,a5),a1)),f3(x1631,f2(a4,x1631)))), % 189.69/189.71 inference(scs_inference,[],[162,2])). % 189.69/189.71 cnf(164,plain, % 189.69/189.71 (E(f3(x1641,f2(a4,x1641)),f2(a4,f2(f2(f3(a4,a5),a1),a1)))), % 189.69/189.71 inference(scs_inference,[],[141,158,162,2,3])). % 189.69/189.71 cnf(165,plain, % 189.69/189.71 (E(f2(a4,f2(f2(f3(a4,a5),a1),a1)),f3(x1651,f2(a4,x1651)))), % 189.69/189.71 inference(scs_inference,[],[164,2])). % 189.69/189.71 cnf(166,plain, % 189.69/189.71 (E(f2(a4,f2(f3(a4,a4),a1)),f2(a4,f2(f3(a4,a5),a1)))), % 189.69/189.71 inference(scs_inference,[],[138,128,164,2,3])). % 189.69/189.71 cnf(168,plain, % 189.69/189.71 (E(f2(a4,f2(f3(a4,a5),a1)),f2(a4,f2(f3(a4,a4),a1)))), % 189.69/189.71 inference(scs_inference,[],[166,2])). % 189.69/189.71 cnf(169,plain, % 189.69/189.71 (E(f3(x1691,f2(a4,x1691)),f2(f2(f6(a8,f2(x1692,a4)),x1692),a4))), % 189.69/189.71 inference(scs_inference,[],[102,158,166,2,3])). % 189.69/189.71 cnf(170,plain, % 189.69/189.71 (E(f2(f2(f6(a8,f2(x1701,a4)),x1701),a4),f3(x1702,f2(a4,x1702)))), % 189.69/189.71 inference(scs_inference,[],[169,2])). % 189.69/189.71 cnf(171,plain, % 189.69/189.71 (E(a8,f2(f6(a5,f2(a4,a4)),f2(a4,a4)))), % 189.69/189.71 inference(scs_inference,[],[117,66,169,2,3])). % 189.69/189.71 cnf(172,plain, % 189.69/189.71 (E(f2(f6(a5,f2(a4,a4)),f2(a4,a4)),a8)), % 189.69/189.71 inference(scs_inference,[],[171,2])). % 189.69/189.71 cnf(173,plain, % 189.69/189.71 (E(a5,f2(a4,f2(f3(a4,a4),a1)))), % 189.69/189.71 inference(scs_inference,[],[135,37,171,2,3])). % 189.69/189.71 cnf(175,plain, % 189.69/189.71 (E(f2(a4,f2(f3(a4,a4),a1)),a5)), % 189.69/189.71 inference(scs_inference,[],[173,2])). % 189.69/189.71 cnf(176,plain, % 189.69/189.71 (E(f2(a4,f2(f3(a4,a5),a1)),a8)), % 189.69/189.71 inference(scs_inference,[],[163,147,173,2,3])). % 189.69/189.72 cnf(178,plain, % 189.69/189.72 (E(a8,f2(a4,f2(f3(a4,a5),a1)))), % 189.69/189.72 inference(scs_inference,[],[176,2])). % 189.69/189.72 cnf(179,plain, % 189.69/189.72 (E(f2(f6(a5,f2(a4,a4)),f2(a4,a4)),f2(f6(a4,f2(a1,x1791)),x1791))), % 189.69/189.72 inference(scs_inference,[],[172,132,176,2,3])). % 189.69/189.72 cnf(180,plain, % 189.69/189.72 (E(f2(f6(a4,f2(a1,x1801)),x1801),f2(f6(a5,f2(a4,a4)),f2(a4,a4)))), % 189.69/189.72 inference(scs_inference,[],[179,2])). % 189.69/189.72 cnf(181,plain, % 189.69/189.72 (E(a8,f2(a4,f2(f3(a4,a4),a1)))), % 189.69/189.72 inference(scs_inference,[],[168,178,179,2,3])). % 189.69/189.72 cnf(182,plain, % 189.69/189.72 (E(f2(a4,f2(f3(a4,a4),a1)),a8)), % 189.69/189.72 inference(scs_inference,[],[181,2])). % 189.69/189.72 cnf(183,plain, % 189.69/189.72 (E(f6(a4,f2(a1,a1)),f2(f6(a5,f2(a4,a4)),f2(a4,a4)))), % 189.69/189.72 inference(scs_inference,[],[180,24,181,2,3])). % 189.69/189.72 cnf(186,plain, % 189.69/189.72 (E(f2(f6(a5,f2(a4,a4)),f2(a4,a4)),f6(a4,f2(a1,a1)))), % 189.69/189.72 inference(scs_inference,[],[183,2])). % 189.69/189.72 cnf(187,plain, % 189.69/189.72 (E(f2(f6(a4,f2(a1,x1871)),x1871),f2(a4,f2(f3(a4,a4),a1)))), % 189.69/189.72 inference(scs_inference,[],[135,180,183,2,3])). % 189.69/189.72 cnf(188,plain, % 189.69/189.72 (E(f2(a4,f2(f3(a4,a4),a1)),f2(f6(a4,f2(a1,x1881)),x1881))), % 189.69/189.72 inference(scs_inference,[],[187,2])). % 189.69/189.72 cnf(189,plain, % 189.69/189.72 (E(f2(f6(a4,f2(a1,x1891)),x1891),f6(a4,f2(a1,a1)))), % 189.69/189.72 inference(scs_inference,[],[186,180,187,2,3])). % 189.69/189.72 cnf(190,plain, % 189.69/189.72 (E(f6(a4,f2(a1,a1)),f2(f6(a4,f2(a1,x1901)),x1901))), % 189.69/189.72 inference(scs_inference,[],[189,2])). % 189.69/189.72 cnf(191,plain, % 189.69/189.72 (E(f2(a4,f2(f3(a4,a5),a1)),f2(f6(a4,f2(a1,x1911)),x1911))), % 189.69/189.72 inference(scs_inference,[],[188,168,189,2,3])). % 189.69/189.72 cnf(192,plain, % 189.69/189.72 (E(f2(f6(a4,f2(a1,x1921)),x1921),f2(a4,f2(f3(a4,a5),a1)))), % 189.69/189.72 inference(scs_inference,[],[191,2])). % 189.69/189.72 cnf(193,plain, % 189.69/189.72 (E(f6(a4,f2(a1,a1)),f3(x1931,f2(a4,x1931)))), % 189.69/189.72 inference(scs_inference,[],[152,190,191,2,3])). % 189.69/189.72 cnf(195,plain, % 189.69/189.72 (E(f3(x1951,f2(a4,x1951)),f6(a4,f2(a1,a1)))), % 189.69/189.72 inference(scs_inference,[],[193,2])). % 189.69/189.72 cnf(196,plain, % 189.69/189.72 (E(f2(a4,f2(f3(a4,a4),a1)),f3(x1961,f2(a4,x1961)))), % 189.69/189.72 inference(scs_inference,[],[188,152,193,2,3])). % 189.69/189.72 cnf(198,plain, % 189.69/189.72 (E(f3(x1981,f2(a4,x1981)),f2(a4,f2(f3(a4,a4),a1)))), % 189.69/189.72 inference(scs_inference,[],[196,2])). % 189.69/189.72 cnf(199,plain, % 189.69/189.72 (E(f6(a4,f2(a1,a1)),f2(a4,f2(f3(a4,a5),a1)))), % 189.69/189.72 inference(scs_inference,[],[192,190,196,2,3])). % 189.69/189.72 cnf(201,plain, % 189.69/189.72 (E(f2(a4,f2(f3(a4,a5),a1)),f6(a4,f2(a1,a1)))), % 189.69/189.72 inference(scs_inference,[],[199,2])). % 189.69/189.72 cnf(202,plain, % 189.69/189.72 (E(f2(a4,f2(f2(f3(a4,a5),a1),a1)),f6(a4,f2(a1,a1)))), % 189.69/189.72 inference(scs_inference,[],[165,195,199,2,3])). % 189.69/189.72 cnf(204,plain, % 189.69/189.72 (E(f6(a4,f2(a1,a1)),f2(a4,f2(f2(f3(a4,a5),a1),a1)))), % 189.69/189.72 inference(scs_inference,[],[202,2])). % 189.69/189.72 cnf(205,plain, % 189.69/189.72 (E(a4,f6(a4,f2(a1,a1)))), % 189.69/189.72 inference(scs_inference,[],[186,117,202,2,3])). % 189.69/189.72 cnf(206,plain, % 189.69/189.72 (E(f6(a4,f2(a1,a1)),a4)), % 189.69/189.72 inference(scs_inference,[],[205,2])). % 189.69/189.72 cnf(207,plain, % 189.69/189.72 (E(f2(f2(f6(a8,f2(x2071,a4)),x2071),a4),f6(a4,f2(a1,a1)))), % 189.69/189.72 inference(scs_inference,[],[170,195,205,2,3])). % 189.69/189.72 cnf(210,plain, % 189.69/189.72 (E(f2(a4,f2(f3(a4,a4),a1)),f2(f6(a4,f2(x2101,a4)),f2(a4,x2101)))), % 189.69/189.72 inference(scs_inference,[],[182,62,207,2,3])). % 189.69/189.72 cnf(211,plain, % 189.69/189.72 (E(f2(f6(a4,f2(x2111,a4)),f2(a4,x2111)),f2(a4,f2(f3(a4,a4),a1)))), % 189.69/189.72 inference(scs_inference,[],[210,2])). % 189.69/189.72 cnf(212,plain, % 189.69/189.72 (E(f6(a4,f2(a1,a1)),f2(a4,f2(x2121,f3(f2(a4,x2121),a5))))), % 189.69/189.72 inference(scs_inference,[],[206,58,210,2,3])). % 189.69/189.72 cnf(213,plain, % 189.69/189.72 (E(f2(a4,f2(x2131,f3(f2(a4,x2131),a5))),f6(a4,f2(a1,a1)))), % 189.69/189.72 inference(scs_inference,[],[212,2])). % 189.69/189.72 cnf(214,plain, % 189.69/189.72 (E(a5,f6(a4,f2(a1,a1)))), % 189.69/189.72 inference(scs_inference,[],[186,37,212,2,3])). % 189.69/189.72 cnf(216,plain, % 189.69/189.72 (E(f6(a4,f2(a1,a1)),a5)), % 189.69/189.72 inference(scs_inference,[],[214,2])). % 189.69/189.72 cnf(217,plain, % 189.69/189.72 (E(f6(a4,f2(a1,a1)),f2(f2(f6(a5,f2(x2171,a4)),x2171),a4))), % 189.69/189.72 inference(scs_inference,[],[206,108,214,2,3])). % 189.69/189.72 cnf(218,plain, % 189.69/189.72 (E(f2(f2(f6(a5,f2(x2181,a4)),x2181),a4),f6(a4,f2(a1,a1)))), % 189.69/189.72 inference(scs_inference,[],[217,2])). % 189.69/189.72 cnf(219,plain, % 189.69/189.72 (E(f2(f6(a4,f2(a1,x2191)),x2191),a4)), % 189.69/189.72 inference(scs_inference,[],[180,217,114,2,3])). % 189.69/189.72 cnf(220,plain, % 189.69/189.72 (E(a4,f2(f6(a4,f2(a1,x2201)),x2201))), % 189.69/189.72 inference(scs_inference,[],[219,2])). % 189.69/189.72 cnf(221,plain, % 189.69/189.72 (E(f3(x2211,f2(a4,x2211)),f2(f6(a5,f2(a4,a4)),f2(a4,a4)))), % 189.69/189.72 inference(scs_inference,[],[198,219,133,2,3])). % 189.69/189.72 cnf(222,plain, % 189.69/189.72 (E(f2(f6(a5,f2(a4,a4)),f2(a4,a4)),f3(x2221,f2(a4,x2221)))), % 189.69/189.72 inference(scs_inference,[],[221,2])). % 189.69/189.72 cnf(223,plain, % 189.69/189.72 (E(f2(f6(a4,f2(x2231,a4)),f2(a4,x2231)),a5)), % 189.69/189.72 inference(scs_inference,[],[211,175,221,2,3])). % 189.69/189.72 cnf(224,plain, % 189.69/189.72 (E(a5,f2(f6(a4,f2(x2241,a4)),f2(a4,x2241)))), % 189.69/189.72 inference(scs_inference,[],[223,2])). % 189.69/189.72 cnf(225,plain, % 189.69/189.72 (E(f6(a4,f2(a1,a1)),f2(a4,f2(x2251,f3(f2(a4,x2251),a4))))), % 189.69/189.72 inference(scs_inference,[],[216,55,223,2,3])). % 189.69/189.72 cnf(226,plain, % 189.69/189.72 (E(f2(a4,f2(x2261,f3(f2(a4,x2261),a4))),f6(a4,f2(a1,a1)))), % 189.69/189.72 inference(scs_inference,[],[225,2])). % 189.69/189.72 cnf(227,plain, % 189.69/189.72 (E(f2(a4,f2(f3(a4,a5),a1)),f2(f6(a5,f2(a4,a4)),f2(a4,a4)))), % 189.69/189.72 inference(scs_inference,[],[201,225,183,2,3])). % 189.69/189.72 cnf(228,plain, % 189.69/189.72 (E(f2(f6(a5,f2(a4,a4)),f2(a4,a4)),f2(a4,f2(f3(a4,a5),a1)))), % 189.69/189.72 inference(scs_inference,[],[227,2])). % 189.69/189.72 cnf(229,plain, % 189.69/189.72 (E(f2(a4,f2(f3(a4,a4),a1)),f6(a4,f2(a1,a1)))), % 189.69/189.72 inference(scs_inference,[],[175,227,214,2,3])). % 189.69/189.72 cnf(230,plain, % 189.69/189.72 (E(f6(a4,f2(a1,a1)),f2(a4,f2(f3(a4,a4),a1)))), % 189.69/189.72 inference(scs_inference,[],[229,2])). % 189.69/189.72 cnf(231,plain, % 189.69/189.72 (E(f6(a4,f2(a1,a1)),f2(f6(a4,f2(x2311,a4)),f2(a4,x2311)))), % 189.69/189.72 inference(scs_inference,[],[224,216,229,2,3])). % 189.69/189.72 cnf(232,plain, % 189.69/189.72 (E(f2(f6(a4,f2(x2321,a4)),f2(a4,x2321)),f6(a4,f2(a1,a1)))), % 189.69/189.72 inference(scs_inference,[],[231,2])). % 189.69/189.72 cnf(233,plain, % 189.69/189.72 (E(f6(a4,f2(a1,a1)),a8)), % 189.69/189.72 inference(scs_inference,[],[230,182,231,2,3])). % 189.69/189.72 cnf(234,plain, % 189.69/189.72 (E(a8,f6(a4,f2(a1,a1)))), % 189.69/189.72 inference(scs_inference,[],[233,2])). % 189.69/189.72 cnf(235,plain, % 189.69/189.72 (E(f2(f6(a4,f2(x2351,a4)),f2(a4,x2351)),f2(f6(a4,f2(a1,x2352)),x2352))), % 189.69/189.72 inference(scs_inference,[],[232,190,233,2,3])). % 189.69/189.72 cnf(236,plain, % 189.69/189.72 (E(f2(f6(a4,f2(a1,x2361)),x2361),f2(f6(a4,f2(x2362,a4)),f2(a4,x2362)))), % 189.69/189.72 inference(scs_inference,[],[235,2])). % 189.69/189.72 cnf(237,plain, % 189.69/189.72 (E(a5,f2(f6(a4,f2(a1,x2371)),x2371))), % 189.69/189.72 inference(scs_inference,[],[224,235,2,3])). % 189.69/189.72 cnf(239,plain, % 189.69/189.72 (E(f2(f6(a4,f2(a1,x2391)),x2391),a5)), % 189.69/189.72 inference(scs_inference,[],[237,2])). % 189.69/189.72 cnf(240,plain, % 189.69/189.72 (E(a4,f2(f6(a4,f2(x2401,a4)),f2(a4,x2401)))), % 189.69/189.72 inference(scs_inference,[],[236,220,237,2,3])). % 189.69/189.72 cnf(242,plain, % 189.69/189.72 (E(f2(f6(a4,f2(x2421,a4)),f2(a4,x2421)),a4)), % 189.69/189.72 inference(scs_inference,[],[240,2])). % 189.69/189.72 cnf(244,plain, % 189.69/189.72 (E(a7,f2(x2441,f2(x2442,f3(f2(x2441,x2442),a4))))), % 189.69/189.72 inference(scs_inference,[],[21,2])). % 189.69/189.72 cnf(245,plain, % 189.69/189.72 (E(f2(f6(a4,f2(x2451,a4)),f2(a4,x2451)),f2(a4,f2(f3(a4,a5),a1)))), % 189.69/189.72 inference(scs_inference,[],[242,138,21,2,3])). % 189.69/189.72 cnf(246,plain, % 189.69/189.72 (E(f2(a4,f2(f3(a4,a5),a1)),f2(f6(a4,f2(x2461,a4)),f2(a4,x2461)))), % 189.69/189.72 inference(scs_inference,[],[245,2])). % 189.69/189.72 cnf(247,plain, % 189.69/189.72 (E(a7,f6(a4,f2(a1,a1)))), % 189.69/189.72 inference(scs_inference,[],[226,244,245,2,3])). % 189.69/189.72 cnf(250,plain, % 189.69/189.72 (E(f6(a4,f2(a1,a1)),a7)), % 189.69/189.72 inference(scs_inference,[],[247,2])). % 189.69/189.72 cnf(251,plain, % 189.69/189.72 (E(f2(f6(a5,f2(a4,a4)),f2(a4,a4)),f2(f6(a4,f2(x2511,a4)),f2(a4,x2511)))), % 189.69/189.72 inference(scs_inference,[],[228,246,247,2,3])). % 189.69/189.72 cnf(252,plain, % 189.69/189.72 (E(f2(f6(a4,f2(x2521,a4)),f2(a4,x2521)),f2(f6(a5,f2(a4,a4)),f2(a4,a4)))), % 189.69/189.72 inference(scs_inference,[],[251,2])). % 189.69/189.72 cnf(253,plain, % 189.69/189.72 (E(f2(a4,f2(x2531,f3(f2(a4,x2531),a5))),a7)), % 189.69/189.72 inference(scs_inference,[],[213,250,251,2,3])). % 189.69/189.72 cnf(255,plain, % 189.69/189.72 (E(f2(f6(a4,f2(x2551,a4)),f2(a4,x2551)),f3(x2552,f2(a4,x2552)))), % 189.69/189.72 inference(scs_inference,[],[222,252,253,2,3])). % 189.69/189.72 cnf(256,plain, % 189.69/189.72 (E(f3(x2561,f2(a4,x2561)),f2(f6(a4,f2(x2562,a4)),f2(a4,x2562)))), % 189.69/189.72 inference(scs_inference,[],[255,2])). % 189.69/189.72 cnf(257,plain, % 189.69/189.72 (E(a7,a8)), % 189.69/189.72 inference(scs_inference,[],[72,244,255,2,3])). % 189.69/189.72 cnf(260,plain, % 189.69/189.72 (E(a8,a7)), % 189.69/189.72 inference(scs_inference,[],[257,2])). % 189.69/189.72 cnf(261,plain, % 189.69/189.72 (E(f2(f2(f6(a5,f2(x2611,a4)),x2611),a4),a7)), % 189.69/189.72 inference(scs_inference,[],[218,250,257,2,3])). % 189.69/189.72 cnf(263,plain, % 189.69/189.72 (E(a8,f2(a4,f2(f2(f3(a4,a5),a1),a1)))), % 189.69/189.72 inference(scs_inference,[],[204,234,261,2,3])). % 189.69/189.72 cnf(264,plain, % 189.69/189.72 (E(f2(a4,f2(f2(f3(a4,a5),a1),a1)),a8)), % 189.69/189.72 inference(scs_inference,[],[263,2])). % 189.69/189.72 cnf(265,plain, % 189.69/189.72 (E(f2(a4,f2(f3(a4,a5),a1)),a7)), % 189.69/189.72 inference(scs_inference,[],[201,250,263,2,3])). % 189.69/189.72 cnf(266,plain, % 189.69/189.72 (E(a7,f2(a4,f2(f3(a4,a5),a1)))), % 189.69/189.72 inference(scs_inference,[],[265,2])). % 189.69/189.72 cnf(267,plain, % 189.69/189.72 (E(f2(a4,f2(f2(f3(a4,a5),a1),a1)),a7)), % 189.69/189.72 inference(scs_inference,[],[264,260,265,2,3])). % 189.69/189.72 cnf(268,plain, % 189.69/189.72 (E(a7,f2(a4,f2(f2(f3(a4,a5),a1),a1)))), % 189.69/189.72 inference(scs_inference,[],[267,2])). % 189.69/189.72 cnf(269,plain, % 189.69/189.72 (E(a7,f3(x2691,f2(a4,x2691)))), % 189.69/189.72 inference(scs_inference,[],[266,163,267,2,3])). % 189.69/189.72 cnf(270,plain, % 189.69/189.72 (E(f3(x2701,f2(a4,x2701)),a7)), % 189.69/189.72 inference(scs_inference,[],[269,2])). % 189.69/189.72 cnf(271,plain, % 189.69/189.72 (E(f2(f6(a4,f2(x2711,a4)),f2(a4,x2711)),a7)), % 189.69/189.72 inference(scs_inference,[],[232,250,269,2,3])). % 189.69/189.72 cnf(272,plain, % 189.69/189.72 (E(a7,f2(f6(a4,f2(x2721,a4)),f2(a4,x2721)))), % 189.69/189.72 inference(scs_inference,[],[271,2])). % 189.69/189.72 cnf(273,plain, % 189.69/189.72 (E(a4,a7)), % 189.69/189.72 inference(scs_inference,[],[270,30,271,2,3])). % 189.69/189.72 cnf(276,plain, % 189.69/189.72 (E(a7,a4)), % 189.69/189.72 inference(scs_inference,[],[273,2])). % 189.69/189.72 cnf(277,plain, % 189.69/189.72 (E(f2(f6(a5,f2(a4,a4)),f2(a4,a4)),a7)), % 189.69/189.72 inference(scs_inference,[],[222,270,273,2,3])). % 189.69/189.72 cnf(279,plain, % 189.69/189.72 (E(a7,f2(f6(a5,f2(a4,a4)),f2(a4,a4)))), % 189.69/189.72 inference(scs_inference,[],[277,2])). % 189.69/189.72 cnf(280,plain, % 189.69/189.72 (E(a7,f2(f2(f6(f6(f2(a5,x2801),x2801),f2(x2802,a4)),x2802),a4))), % 189.69/189.72 inference(scs_inference,[],[111,276,277,2,3])). % 189.69/189.72 cnf(282,plain, % 189.69/189.72 (E(f2(a4,f2(f3(f2(a1,a4),a4),a1)),a4)), % 189.69/189.72 inference(scs_inference,[],[84,276,280,2,3])). % 189.69/189.72 cnf(283,plain, % 189.69/189.72 (E(a4,f2(a4,f2(f3(f2(a1,a4),a4),a1)))), % 189.69/189.72 inference(scs_inference,[],[282,2])). % 189.69/189.72 cnf(284,plain, % 189.69/189.72 (E(a7,f2(a4,f2(f3(a4,a4),a1)))), % 189.69/189.72 inference(scs_inference,[],[279,135,282,2,3])). % 189.69/189.72 cnf(285,plain, % 189.69/189.72 (E(f2(a4,f2(f3(a4,a4),a1)),a7)), % 189.69/189.72 inference(scs_inference,[],[284,2])). % 189.69/189.72 cnf(287,plain, % 189.69/189.72 (E(a8,f2(f2(f6(a4,f2(x2871,x2872)),x2872),x2871))), % 189.69/189.72 inference(scs_inference,[],[22,2])). % 189.69/189.72 cnf(288,plain, % 189.69/189.72 (E(f2(a4,f2(f3(a4,a4),a1)),f2(x2881,f3(f2(a1,x2881),a4)))), % 189.69/189.72 inference(scs_inference,[],[285,76,22,2,3])). % 189.69/189.72 cnf(289,plain, % 189.69/189.72 (E(f2(x2891,f3(f2(a1,x2891),a4)),f2(a4,f2(f3(a4,a4),a1)))), % 189.69/189.72 inference(scs_inference,[],[288,2])). % 189.69/189.72 cnf(290,plain, % 189.69/189.72 (E(f6(a4,f2(a1,a1)),f2(x2901,f3(f2(a1,x2901),a4)))), % 189.69/189.72 inference(scs_inference,[],[230,288,2,3])). % 189.69/189.72 cnf(291,plain, % 189.69/189.72 (E(f2(x2911,f3(f2(a1,x2911),a4)),f6(a4,f2(a1,a1)))), % 189.69/189.72 inference(scs_inference,[],[290,2])). % 189.69/189.72 cnf(292,plain, % 189.69/189.72 (E(f2(x2921,f3(f2(a1,x2921),a4)),f2(f6(a4,f2(a1,x2922)),x2922))), % 189.69/189.72 inference(scs_inference,[],[289,188,290,2,3])). % 189.69/189.72 cnf(293,plain, % 189.69/189.72 (E(f2(f6(a4,f2(a1,x2931)),x2931),f2(x2932,f3(f2(a1,x2932),a4)))), % 189.69/189.72 inference(scs_inference,[],[292,2])). % 189.69/189.72 cnf(294,plain, % 189.69/189.72 (E(f2(x2941,f3(f2(a1,x2941),a4)),a5)), % 189.69/189.72 inference(scs_inference,[],[291,216,292,2,3])). % 189.69/189.72 cnf(295,plain, % 189.69/189.72 (E(a5,f2(x2951,f3(f2(a1,x2951),a4)))), % 189.69/189.72 inference(scs_inference,[],[294,2])). % 189.69/189.72 cnf(296,plain, % 189.69/189.72 (E(a4,f2(x2961,f3(f2(a1,x2961),a4)))), % 189.69/189.72 inference(scs_inference,[],[293,220,294,2,3])). % 189.69/189.72 cnf(298,plain, % 189.69/189.72 (E(f2(x2981,f3(f2(a1,x2981),a4)),a4)), % 189.69/189.72 inference(scs_inference,[],[296,2])). % 189.69/189.72 cnf(299,plain, % 189.69/189.72 (E(a8,f2(x2991,f3(f2(a1,x2991),a4)))), % 189.69/189.72 inference(scs_inference,[],[293,132,296,2,3])). % 189.69/189.72 cnf(301,plain, % 189.69/189.72 (E(f2(x3011,f3(f2(a1,x3011),a4)),a8)), % 189.69/189.72 inference(scs_inference,[],[299,2])). % 189.69/189.72 cnf(302,plain, % 189.69/189.72 (E(f2(x3021,f3(f2(a1,x3021),a4)),f2(a4,f2(f3(a4,a5),a1)))), % 189.69/189.72 inference(scs_inference,[],[298,138,299,2,3])). % 189.69/189.72 cnf(303,plain, % 189.69/189.72 (E(f2(a4,f2(f3(a4,a5),a1)),f2(x3031,f3(f2(a1,x3031),a4)))), % 189.69/189.72 inference(scs_inference,[],[302,2])). % 189.69/189.72 cnf(304,plain, % 189.69/189.72 (E(f2(x3041,f3(f2(a1,x3041),a4)),f2(f6(a4,f2(x3042,a4)),f2(a4,x3042)))), % 189.69/189.72 inference(scs_inference,[],[301,62,302,2,3])). % 189.69/189.72 cnf(305,plain, % 189.69/189.72 (E(f2(f6(a4,f2(x3051,a4)),f2(a4,x3051)),f2(x3052,f3(f2(a1,x3052),a4)))), % 189.69/189.72 inference(scs_inference,[],[304,2])). % 189.69/189.72 cnf(306,plain, % 189.69/189.72 (E(f2(x3061,f3(f2(a1,x3061),a4)),f2(f6(a5,f2(a4,a4)),f2(a4,a4)))), % 189.69/189.72 inference(scs_inference,[],[298,117,304,2,3])). % 189.69/189.72 cnf(307,plain, % 189.69/189.72 (E(f2(f6(a5,f2(a4,a4)),f2(a4,a4)),f2(x3071,f3(f2(a1,x3071),a4)))), % 189.69/189.72 inference(scs_inference,[],[306,2])). % 189.69/189.72 cnf(308,plain, % 189.69/189.72 (E(f3(x3081,f2(a4,x3081)),f2(x3082,f3(f2(a1,x3082),a4)))), % 189.69/189.72 inference(scs_inference,[],[256,305,306,2,3])). % 189.69/189.72 cnf(310,plain, % 189.69/189.72 (E(f2(x3101,f3(f2(a1,x3101),a4)),f3(x3102,f2(a4,x3102)))), % 189.69/189.72 inference(scs_inference,[],[308,2])). % 189.69/189.72 cnf(311,plain, % 189.69/189.72 (E(a7,f2(f6(a4,f2(a1,x3111)),x3111))), % 189.69/189.72 inference(scs_inference,[],[266,308,191,2,3])). % 189.69/189.72 cnf(312,plain, % 189.69/189.72 (E(f2(f6(a4,f2(a1,x3121)),x3121),a7)), % 189.69/189.72 inference(scs_inference,[],[311,2])). % 189.69/189.72 cnf(315,plain, % 189.69/189.72 (E(f2(a4,f2(x3151,x3152)),f2(f2(a4,x3151),x3152))), % 189.69/189.72 inference(scs_inference,[],[19,2])). % 189.69/189.72 cnf(317,plain, % 189.69/189.72 (E(a7,a5)), % 189.69/189.72 inference(scs_inference,[],[272,223,3])). % 189.69/189.72 cnf(319,plain, % 189.69/189.72 (E(a5,a7)), % 189.69/189.72 inference(scs_inference,[],[272,223,3,2])). % 189.69/189.72 cnf(324,plain, % 189.69/189.72 (E(f2(a4,f2(f3(f2(a1,a4),a4),a1)),f2(a4,a1))), % 189.69/189.72 inference(scs_inference,[],[10,283,3,2])). % 189.69/189.72 cnf(327,plain, % 189.69/189.72 (E(f2(x3271,f3(f2(a1,x3271),a4)),f2(f2(f6(a5,f2(a4,a4)),f2(a4,a4)),a1))), % 189.69/189.72 inference(scs_inference,[],[10,307,3,2])). % 189.69/189.72 cnf(330,plain, % 189.69/189.72 (E(f2(f2(f6(a4,f2(x3301,x3302)),x3302),x3301),f2(a8,a1))), % 189.69/189.72 inference(scs_inference,[],[10,287,3,2])). % 189.69/189.72 cnf(331,plain, % 189.69/189.72 (E(f2(a5,a1),f2(x3311,f3(f2(a1,x3311),a4)))), % 189.69/189.72 inference(scs_inference,[],[10,295,3])). % 189.69/189.72 cnf(333,plain, % 189.69/189.72 (E(f2(x3331,f3(f2(a1,x3331),a4)),f2(a5,a1))), % 189.69/189.72 inference(scs_inference,[],[10,295,3,2])). % 189.69/189.72 cnf(336,plain, % 189.69/189.72 (E(f2(a5,a1),f2(f2(x3361,f3(f2(a1,x3361),a4)),a1))), % 189.69/189.72 inference(scs_inference,[],[10,333,3,2])). % 189.69/189.72 cnf(339,plain, % 189.69/189.72 (E(f2(f2(x3391,f3(f2(a1,x3391),a4)),a1),f2(f2(a5,a1),a1))), % 189.69/189.72 inference(scs_inference,[],[10,336,3,2])). % 189.69/189.72 cnf(342,plain, % 189.69/189.72 (E(a7,f2(f2(f6(a4,f2(a1,x3421)),x3421),a1))), % 189.69/189.72 inference(scs_inference,[],[10,312,3,2])). % 189.69/189.72 cnf(348,plain, % 189.69/189.72 (E(f2(f2(f6(f6(f2(a5,x3481),x3481),f2(x3482,a4)),x3482),a4),f2(a8,a1))), % 189.69/189.72 inference(scs_inference,[],[10,161,3,2])). % 189.69/189.72 cnf(357,plain, % 189.69/189.72 (E(f2(f2(f6(a4,f2(a1,x3571)),x3571),a1),f2(a7,a1))), % 189.69/189.72 inference(scs_inference,[],[10,342,3,2])). % 189.69/189.72 cnf(358,plain, % 189.69/189.72 (E(f2(a8,a1),a7)), % 189.69/189.72 inference(scs_inference,[],[10,260,3])). % 189.69/189.72 cnf(360,plain, % 189.69/189.72 (E(a7,f2(a8,a1))), % 189.69/189.72 inference(scs_inference,[],[10,260,3,2])). % 189.69/189.72 cnf(361,plain, % 189.69/189.72 (E(f2(a7,a1),f2(a8,a1))), % 189.69/189.72 inference(scs_inference,[],[10,360,3])). % 189.69/189.72 cnf(363,plain, % 189.69/189.72 (E(f2(a8,a1),f2(a7,a1))), % 189.69/189.72 inference(scs_inference,[],[10,360,3,2])). % 189.69/189.72 cnf(366,plain, % 189.69/189.72 (E(f2(a7,a1),f2(f2(a8,a1),a1))), % 189.69/189.72 inference(scs_inference,[],[10,363,3,2])). % 189.69/189.72 cnf(369,plain, % 189.69/189.72 (E(f2(f2(a8,a1),a1),f2(f2(a7,a1),a1))), % 189.69/189.72 inference(scs_inference,[],[10,366,3,2])). % 189.69/189.72 cnf(372,plain, % 189.69/189.72 (E(f2(f2(a7,a1),a1),f2(f2(f2(a8,a1),a1),a1))), % 189.69/189.72 inference(scs_inference,[],[10,369,3,2])). % 189.69/189.72 cnf(373,plain, % 189.69/189.72 (E(f2(f2(f2(a7,a1),a1),a1),f2(f2(f2(a8,a1),a1),a1))), % 189.69/189.72 inference(scs_inference,[],[10,372,3])). % 189.69/189.72 cnf(375,plain, % 189.69/189.72 (E(f2(f2(f2(a8,a1),a1),a1),f2(f2(f2(a7,a1),a1),a1))), % 189.69/189.72 inference(scs_inference,[],[10,372,3,2])). % 189.69/189.72 cnf(378,plain, % 189.69/189.72 (E(a8,f2(f2(f6(a5,f2(a4,a4)),f2(a4,a4)),a1))), % 189.69/189.72 inference(scs_inference,[],[10,172,3,2])). % 189.69/189.72 cnf(381,plain, % 189.69/189.72 (E(f2(f2(f6(a5,f2(a4,a4)),f2(a4,a4)),a1),f2(a8,a1))), % 189.69/189.72 inference(scs_inference,[],[10,378,3,2])). % 189.69/189.72 cnf(382,plain, % 189.69/189.72 (E(f2(f2(f2(f6(a5,f2(a4,a4)),f2(a4,a4)),a1),a1),f2(a8,a1))), % 189.69/189.72 inference(scs_inference,[],[10,381,3])). % 189.69/189.72 cnf(385,plain, % 189.69/189.72 (E(f2(f2(f6(a5,f2(a4,a4)),f2(a4,a4)),a1),f2(a4,f2(f3(a4,a5),a1)))), % 189.69/189.72 inference(scs_inference,[],[10,228,382,2,3])). % 189.69/189.72 cnf(387,plain, % 189.69/189.72 (E(f2(a4,f2(f3(a4,a5),a1)),f2(f2(f6(a5,f2(a4,a4)),f2(a4,a4)),a1))), % 189.69/189.72 inference(scs_inference,[],[385,2])). % 189.69/189.72 cnf(388,plain, % 189.69/189.72 (E(f2(a7,a1),f2(f6(a5,f2(a4,a4)),f2(a4,a4)))), % 189.69/189.72 inference(scs_inference,[],[10,279,385,2,3])). % 189.69/189.72 cnf(390,plain, % 189.69/189.72 (E(f2(f6(a5,f2(a4,a4)),f2(a4,a4)),f2(a7,a1))), % 189.69/189.72 inference(scs_inference,[],[388,2])). % 189.69/189.72 cnf(391,plain, % 189.69/189.72 (E(f2(a8,a1),f2(a4,f2(f3(a4,a5),a1)))), % 189.69/189.72 inference(scs_inference,[],[10,178,388,2,3])). % 189.69/189.72 cnf(393,plain, % 189.69/189.72 (E(f2(a4,f2(f3(a4,a5),a1)),f2(a8,a1))), % 189.69/189.72 inference(scs_inference,[],[391,2])). % 189.69/189.72 cnf(394,plain, % 189.69/189.72 (E(f2(f2(f6(a5,f2(a4,a4)),f2(a4,a4)),a1),f2(a7,a1))), % 189.69/189.72 inference(scs_inference,[],[10,390,391,2,3])). % 189.69/189.72 cnf(396,plain, % 189.69/189.72 (E(f2(a7,a1),f2(f2(f6(a5,f2(a4,a4)),f2(a4,a4)),a1))), % 189.69/189.72 inference(scs_inference,[],[394,2])). % 189.69/189.72 cnf(397,plain, % 189.69/189.72 (E(f2(f2(a4,f2(f3(a4,a5),a1)),a1),f2(a8,a1))), % 189.69/189.72 inference(scs_inference,[],[10,393,394,2,3])). % 189.69/189.72 cnf(399,plain, % 189.69/189.72 (E(f2(a8,a1),f2(f2(a4,f2(f3(a4,a5),a1)),a1))), % 189.69/189.72 inference(scs_inference,[],[397,2])). % 189.69/189.72 cnf(400,plain, % 189.69/189.72 (E(f2(f2(a7,a1),a1),f2(f2(f6(a5,f2(a4,a4)),f2(a4,a4)),a1))), % 189.69/189.72 inference(scs_inference,[],[10,396,397,2,3])). % 189.69/189.72 cnf(402,plain, % 189.69/189.72 (E(f2(f2(f6(a5,f2(a4,a4)),f2(a4,a4)),a1),f2(f2(a7,a1),a1))), % 189.69/189.72 inference(scs_inference,[],[400,2])). % 189.69/189.72 cnf(403,plain, % 189.69/189.72 (E(f2(f2(a8,a1),a1),f2(f2(a4,f2(f3(a4,a5),a1)),a1))), % 189.69/189.72 inference(scs_inference,[],[10,399,400,2,3])). % 189.69/189.72 cnf(405,plain, % 189.69/189.72 (E(f2(f2(a4,f2(f3(a4,a5),a1)),a1),f2(f2(a8,a1),a1))), % 189.69/189.72 inference(scs_inference,[],[403,2])). % 189.69/189.72 cnf(406,plain, % 189.69/189.72 (E(f2(a5,a1),a7)), % 189.69/189.72 inference(scs_inference,[],[10,319,403,2,3])). % 189.69/189.72 cnf(408,plain, % 189.69/189.72 (E(a7,f2(a5,a1))), % 189.69/189.72 inference(scs_inference,[],[406,2])). % 189.69/189.72 cnf(409,plain, % 189.69/189.72 (E(f2(a4,a1),f2(a4,f2(f2(f3(a4,a5),a1),a1)))), % 189.69/189.72 inference(scs_inference,[],[10,141,406,2,3])). % 189.69/189.72 cnf(411,plain, % 189.69/189.72 (E(f2(a4,f2(f2(f3(a4,a5),a1),a1)),f2(a4,a1))), % 189.69/189.72 inference(scs_inference,[],[409,2])). % 189.69/189.72 cnf(412,plain, % 189.69/189.72 (E(f2(a7,a1),f2(a5,a1))), % 189.69/189.72 inference(scs_inference,[],[10,408,409,2,3])). % 189.69/189.72 cnf(414,plain, % 189.69/189.72 (E(f2(a5,a1),f2(a7,a1))), % 189.69/189.72 inference(scs_inference,[],[412,2])). % 189.69/189.72 cnf(415,plain, % 189.69/189.72 (E(f2(a8,a1),f6(a4,f2(a1,a1)))), % 189.69/189.72 inference(scs_inference,[],[10,234,412,2,3])). % 189.69/189.72 cnf(417,plain, % 189.69/189.72 (E(f6(a4,f2(a1,a1)),f2(a8,a1))), % 189.69/189.72 inference(scs_inference,[],[415,2])). % 189.69/189.72 cnf(418,plain, % 189.69/189.72 (E(f2(f2(a5,a1),a1),f2(a7,a1))), % 189.69/189.72 inference(scs_inference,[],[10,414,415,2,3])). % 189.69/189.72 cnf(420,plain, % 189.69/189.72 (E(f2(a7,a1),f2(f2(a5,a1),a1))), % 189.69/189.73 inference(scs_inference,[],[418,2])). % 189.69/189.73 cnf(421,plain, % 189.69/189.73 (E(f2(f6(a4,f2(a1,a1)),a1),f2(a8,a1))), % 189.69/189.73 inference(scs_inference,[],[10,417,418,2,3])). % 189.69/189.73 cnf(423,plain, % 189.69/189.73 (E(f2(a8,a1),f2(f6(a4,f2(a1,a1)),a1))), % 189.69/189.73 inference(scs_inference,[],[421,2])). % 189.69/189.73 cnf(424,plain, % 189.69/189.73 (E(f2(f2(a7,a1),a1),f2(f2(a5,a1),a1))), % 189.69/189.73 inference(scs_inference,[],[10,420,421,2,3])). % 189.69/189.73 cnf(426,plain, % 189.69/189.73 (E(f2(f2(a5,a1),a1),f2(f2(a7,a1),a1))), % 189.69/189.73 inference(scs_inference,[],[424,2])). % 189.69/189.73 cnf(427,plain, % 189.69/189.73 (E(f2(f2(a8,a1),a1),f2(f6(a4,f2(a1,a1)),a1))), % 189.69/189.73 inference(scs_inference,[],[10,423,424,2,3])). % 189.69/189.73 cnf(429,plain, % 189.69/189.73 (E(f2(f6(a4,f2(a1,a1)),a1),f2(f2(a8,a1),a1))), % 189.69/189.73 inference(scs_inference,[],[427,2])). % 189.69/189.73 cnf(430,plain, % 189.69/189.73 (E(f2(f2(f2(a5,a1),a1),a1),f2(f2(a7,a1),a1))), % 189.69/189.73 inference(scs_inference,[],[10,426,427,2,3])). % 189.69/189.73 cnf(432,plain, % 189.69/189.73 (E(f2(f2(a7,a1),a1),f2(f2(f2(a5,a1),a1),a1))), % 189.69/189.73 inference(scs_inference,[],[430,2])). % 189.69/189.73 cnf(433,plain, % 189.69/189.73 (E(f2(f2(f6(a4,f2(a1,a1)),a1),a1),f2(f2(a8,a1),a1))), % 189.69/189.73 inference(scs_inference,[],[10,429,430,2,3])). % 189.69/189.73 cnf(435,plain, % 189.69/189.73 (E(f2(f2(a8,a1),a1),f2(f2(f6(a4,f2(a1,a1)),a1),a1))), % 189.69/189.73 inference(scs_inference,[],[433,2])). % 189.69/189.73 cnf(436,plain, % 189.69/189.73 (E(f2(f2(f2(a7,a1),a1),a1),f2(f2(f2(a5,a1),a1),a1))), % 189.69/189.73 inference(scs_inference,[],[10,432,433,2,3])). % 189.69/189.73 cnf(439,plain, % 189.69/189.73 (E(f2(f2(a4,f2(f3(a4,a4),a1)),a1),a7)), % 189.69/189.73 inference(scs_inference,[],[10,285,436,2,3])). % 189.69/189.73 cnf(441,plain, % 189.69/189.73 (E(a7,f2(f2(a4,f2(f3(a4,a4),a1)),a1))), % 189.69/189.73 inference(scs_inference,[],[439,2])). % 189.69/189.73 cnf(442,plain, % 189.69/189.73 (E(f2(a7,a1),f2(a4,f2(f2(f3(a4,a5),a1),a1)))), % 189.69/189.73 inference(scs_inference,[],[10,268,439,2,3])). % 189.69/189.73 cnf(444,plain, % 189.69/189.73 (E(f2(a4,f2(f2(f3(a4,a5),a1),a1)),f2(a7,a1))), % 189.69/189.73 inference(scs_inference,[],[442,2])). % 189.69/189.73 cnf(445,plain, % 189.69/189.73 (E(f2(a7,a1),f2(f2(a4,f2(f3(a4,a4),a1)),a1))), % 189.69/189.73 inference(scs_inference,[],[10,441,442,2,3])). % 189.69/189.73 cnf(448,plain, % 189.69/189.73 (E(f2(f2(x4481,f3(f2(a1,x4481),a4)),a1),f3(x4482,f2(a4,x4482)))), % 189.69/189.73 inference(scs_inference,[],[10,310,445,2,3])). % 189.69/189.73 cnf(450,plain, % 189.69/189.73 (E(f3(x4501,f2(a4,x4501)),f2(f2(x4502,f3(f2(a1,x4502),a4)),a1))), % 189.69/189.73 inference(scs_inference,[],[448,2])). % 189.69/189.73 cnf(451,plain, % 189.69/189.73 (E(f2(f2(f6(a4,f2(x4511,a4)),f2(a4,x4511)),a1),f2(a4,f2(f3(a4,a4),a1)))), % 189.69/189.73 inference(scs_inference,[],[10,211,448,2,3])). % 189.69/189.73 cnf(453,plain, % 189.69/189.73 (E(f2(a4,f2(f3(a4,a4),a1)),f2(f2(f6(a4,f2(x4531,a4)),f2(a4,x4531)),a1))), % 189.69/189.73 inference(scs_inference,[],[451,2])). % 189.69/189.73 cnf(454,plain, % 189.69/189.73 (E(f2(f3(x4541,f2(a4,x4541)),a1),f2(f6(a4,f2(x4542,a4)),f2(a4,x4542)))), % 189.69/189.73 inference(scs_inference,[],[10,256,451,2,3])). % 189.69/189.73 cnf(456,plain, % 189.69/189.73 (E(f2(f6(a4,f2(x4561,a4)),f2(a4,x4561)),f2(f3(x4562,f2(a4,x4562)),a1))), % 189.69/189.73 inference(scs_inference,[],[454,2])). % 189.69/189.73 cnf(457,plain, % 189.69/189.73 (E(f2(f2(f6(a4,f2(x4571,a4)),f2(a4,x4571)),a1),f2(x4572,f3(f2(a1,x4572),a4)))), % 189.69/189.73 inference(scs_inference,[],[10,305,454,2,3])). % 189.69/189.73 cnf(460,plain, % 189.69/189.73 (E(f2(f2(f6(a4,f2(x4601,a4)),f2(a4,x4601)),a1),f2(f3(x4602,f2(a4,x4602)),a1))), % 189.69/189.73 inference(scs_inference,[],[10,456,457,2,3])). % 189.69/189.73 cnf(463,plain, % 189.69/189.73 (E(f2(f2(x4631,f3(f2(a1,x4631),a4)),a1),f6(a4,f2(a1,a1)))), % 189.69/189.73 inference(scs_inference,[],[10,291,460,2,3])). % 189.69/189.73 cnf(465,plain, % 189.69/189.73 (E(f6(a4,f2(a1,a1)),f2(f2(x4651,f3(f2(a1,x4651),a4)),a1))), % 189.69/189.73 inference(scs_inference,[],[463,2])). % 189.69/189.73 cnf(466,plain, % 189.69/189.73 (E(f2(f2(f2(a4,x4661),a4),a1),f2(a4,f2(f2(x4661,a4),a1)))), % 189.69/189.73 inference(scs_inference,[],[10,88,463,2,3])). % 189.69/189.73 cnf(469,plain, % 189.69/189.73 (E(f2(f2(f6(a4,f2(a1,x4691)),x4691),a1),a5)), % 189.69/189.73 inference(scs_inference,[],[10,239,466,2,3])). % 189.69/189.73 cnf(471,plain, % 189.69/189.73 (E(a5,f2(f2(f6(a4,f2(a1,x4711)),x4711),a1))), % 189.69/189.73 inference(scs_inference,[],[469,2])). % 189.69/189.73 cnf(472,plain, % 189.69/189.73 (E(f2(f2(x4721,f3(f2(a1,x4721),a4)),a1),a8)), % 189.69/189.73 inference(scs_inference,[],[10,301,469,2,3])). % 189.69/189.73 cnf(474,plain, % 189.69/189.73 (E(a8,f2(f2(x4741,f3(f2(a1,x4741),a4)),a1))), % 189.69/189.73 inference(scs_inference,[],[472,2])). % 189.69/189.73 cnf(475,plain, % 189.69/189.73 (E(f2(a5,a1),f2(f2(f6(a4,f2(a1,x4751)),x4751),a1))), % 189.69/189.73 inference(scs_inference,[],[10,471,472,2,3])). % 189.69/189.73 cnf(477,plain, % 189.69/189.73 (E(f2(f2(f6(a4,f2(a1,x4771)),x4771),a1),f2(a5,a1))), % 189.69/189.73 inference(scs_inference,[],[475,2])). % 189.69/189.73 cnf(478,plain, % 189.69/189.73 (E(f2(a8,a1),f2(f2(x4781,f3(f2(a1,x4781),a4)),a1))), % 189.69/189.73 inference(scs_inference,[],[10,474,475,2,3])). % 189.69/189.73 cnf(480,plain, % 189.69/189.73 (E(f2(f2(x4801,f3(f2(a1,x4801),a4)),a1),f2(a8,a1))), % 189.69/189.73 inference(scs_inference,[],[478,2])). % 189.69/189.73 cnf(481,plain, % 189.69/189.73 (E(f2(f2(f6(a4,f2(x4811,a4)),f2(a4,x4811)),a1),a4)), % 189.69/189.73 inference(scs_inference,[],[10,242,478,2,3])). % 189.69/189.73 cnf(483,plain, % 189.69/189.73 (E(a4,f2(f2(f6(a4,f2(x4831,a4)),f2(a4,x4831)),a1))), % 189.69/189.73 inference(scs_inference,[],[481,2])). % 189.69/189.73 cnf(484,plain, % 189.69/189.73 (E(f2(a7,a1),f2(f6(a4,f2(x4841,a4)),f2(a4,x4841)))), % 189.69/189.73 inference(scs_inference,[],[10,272,481,2,3])). % 189.69/189.73 cnf(486,plain, % 189.69/189.73 (E(f2(f6(a4,f2(x4861,a4)),f2(a4,x4861)),f2(a7,a1))), % 189.69/189.73 inference(scs_inference,[],[484,2])). % 189.69/189.73 cnf(487,plain, % 189.69/189.73 (E(f2(a4,a1),f2(f2(f6(a4,f2(x4871,a4)),f2(a4,x4871)),a1))), % 189.69/189.73 inference(scs_inference,[],[10,483,484,2,3])). % 189.69/189.73 cnf(489,plain, % 189.69/189.73 (E(f2(f2(f6(a4,f2(x4891,a4)),f2(a4,x4891)),a1),f2(a4,a1))), % 189.69/189.73 inference(scs_inference,[],[487,2])). % 189.69/189.73 cnf(490,plain, % 189.69/189.73 (E(f2(f2(f6(a4,f2(x4901,a4)),f2(a4,x4901)),a1),f2(a7,a1))), % 189.69/189.73 inference(scs_inference,[],[10,486,487,2,3])). % 189.69/189.73 cnf(492,plain, % 189.69/189.73 (E(f2(a7,a1),f2(f2(f6(a4,f2(x4921,a4)),f2(a4,x4921)),a1))), % 189.69/189.73 inference(scs_inference,[],[490,2])). % 189.69/189.73 cnf(493,plain, % 189.69/189.73 (E(f2(f2(f2(f6(a4,f2(x4931,a4)),f2(a4,x4931)),a1),a1),f2(a4,a1))), % 189.69/189.73 inference(scs_inference,[],[10,489,490,2,3])). % 189.69/189.73 cnf(496,plain, % 189.69/189.73 (E(f2(f2(a7,a1),a1),f2(f2(f6(a4,f2(x4961,a4)),f2(a4,x4961)),a1))), % 189.69/189.73 inference(scs_inference,[],[10,492,493,2,3])). % 189.69/189.73 cnf(498,plain, % 189.69/189.73 (E(f2(f2(f6(a4,f2(x4981,a4)),f2(a4,x4981)),a1),f2(f2(a7,a1),a1))), % 189.69/189.73 inference(scs_inference,[],[496,2])). % 189.69/189.73 cnf(499,plain, % 189.69/189.73 (E(f2(a4,a1),f2(f2(f6(f6(f2(a5,x4991),x4991),f2(x4992,a4)),x4992),a4))), % 189.69/189.73 inference(scs_inference,[],[10,111,496,2,3])). % 189.69/189.73 cnf(501,plain, % 189.69/189.73 (E(f2(f2(f6(f6(f2(a5,x5011),x5011),f2(x5012,a4)),x5012),a4),f2(a4,a1))), % 189.69/189.73 inference(scs_inference,[],[499,2])). % 189.69/189.73 cnf(502,plain, % 189.69/189.73 (E(f2(a4,a1),f2(f2(f6(a8,f2(x5021,a4)),x5021),a4))), % 189.69/189.73 inference(scs_inference,[],[10,102,499,2,3])). % 189.69/189.73 cnf(505,plain, % 189.69/189.73 (E(f2(a7,a1),f2(a4,f2(f3(a4,a5),a1)))), % 189.69/189.73 inference(scs_inference,[],[10,266,502,2,3])). % 189.69/189.73 cnf(507,plain, % 189.69/189.73 (E(f2(a4,f2(f3(a4,a5),a1)),f2(a7,a1))), % 189.69/189.73 inference(scs_inference,[],[505,2])). % 189.69/189.73 cnf(508,plain, % 189.69/189.73 (E(f2(a7,a1),a4)), % 189.69/189.73 inference(scs_inference,[],[10,276,505,2,3])). % 189.69/189.73 cnf(510,plain, % 189.69/189.73 (E(a4,f2(a7,a1))), % 189.69/189.73 inference(scs_inference,[],[508,2])). % 189.69/189.73 cnf(511,plain, % 189.69/189.73 (E(f2(f2(a4,f2(f3(a4,a5),a1)),a1),f2(a7,a1))), % 189.69/189.73 inference(scs_inference,[],[10,507,508,2,3])). % 189.69/189.73 cnf(513,plain, % 189.69/189.73 (E(f2(a7,a1),f2(f2(a4,f2(f3(a4,a5),a1)),a1))), % 189.69/189.73 inference(scs_inference,[],[511,2])). % 189.69/189.73 cnf(514,plain, % 189.69/189.73 (E(f2(a4,a1),f2(a7,a1))), % 189.69/189.73 inference(scs_inference,[],[10,510,511,2,3])). % 189.69/189.73 cnf(516,plain, % 189.69/189.73 (E(f2(a7,a1),f2(a4,a1))), % 189.69/189.73 inference(scs_inference,[],[514,2])). % 189.69/189.73 cnf(517,plain, % 189.69/189.73 (E(f2(f2(a7,a1),a1),f2(f2(a4,f2(f3(a4,a5),a1)),a1))), % 189.69/189.73 inference(scs_inference,[],[10,513,514,2,3])). % 189.69/189.73 cnf(519,plain, % 189.69/189.73 (E(f2(f2(a4,f2(f3(a4,a5),a1)),a1),f2(f2(a7,a1),a1))), % 189.69/189.73 inference(scs_inference,[],[517,2])). % 189.69/189.73 cnf(520,plain, % 189.69/189.73 (E(f2(f2(a7,a1),a1),f2(a4,a1))), % 189.69/189.73 inference(scs_inference,[],[10,516,517,2,3])). % 189.69/189.73 cnf(522,plain, % 189.69/189.73 (E(f2(a4,a1),f2(f2(a7,a1),a1))), % 189.69/189.73 inference(scs_inference,[],[520,2])). % 189.69/189.73 cnf(523,plain, % 189.69/189.73 (E(f2(f2(a4,f2(f3(a4,a5),a1)),a1),f6(a4,f2(a1,a1)))), % 189.69/189.73 inference(scs_inference,[],[10,201,520,2,3])). % 189.69/189.73 cnf(525,plain, % 189.69/189.73 (E(f6(a4,f2(a1,a1)),f2(f2(a4,f2(f3(a4,a5),a1)),a1))), % 189.69/189.73 inference(scs_inference,[],[523,2])). % 189.69/189.73 cnf(526,plain, % 189.69/189.73 (E(f2(f2(a4,a1),a1),f2(f2(a7,a1),a1))), % 189.69/189.73 inference(scs_inference,[],[10,522,523,2,3])). % 189.69/189.73 cnf(528,plain, % 189.69/189.73 (E(f2(f2(a7,a1),a1),f2(f2(a4,a1),a1))), % 189.69/189.73 inference(scs_inference,[],[526,2])). % 189.69/189.73 cnf(529,plain, % 189.69/189.73 (E(f2(f2(a4,f2(f3(a4,a4),a1)),a1),a5)), % 189.69/189.73 inference(scs_inference,[],[10,175,526,2,3])). % 189.69/189.73 cnf(531,plain, % 189.69/189.73 (E(a5,f2(f2(a4,f2(f3(a4,a4),a1)),a1))), % 189.69/189.73 inference(scs_inference,[],[529,2])). % 189.69/189.73 cnf(532,plain, % 189.69/189.73 (E(f2(f2(f2(a7,a1),a1),a1),f2(f2(a4,a1),a1))), % 189.69/189.73 inference(scs_inference,[],[10,528,529,2,3])). % 189.69/189.73 cnf(534,plain, % 189.69/189.73 (E(f2(f2(a4,a1),a1),f2(f2(f2(a7,a1),a1),a1))), % 189.69/189.73 inference(scs_inference,[],[532,2])). % 189.69/189.73 cnf(535,plain, % 189.69/189.73 (E(f2(a5,a1),f2(f2(a4,f2(f3(a4,a4),a1)),a1))), % 189.69/189.73 inference(scs_inference,[],[10,531,532,2,3])). % 189.69/189.73 cnf(537,plain, % 189.69/189.73 (E(f2(f2(a4,f2(f3(a4,a4),a1)),a1),f2(a5,a1))), % 189.69/189.73 inference(scs_inference,[],[535,2])). % 189.69/189.73 cnf(538,plain, % 189.69/189.73 (E(f2(f2(f2(a4,a1),a1),a1),f2(f2(f2(a7,a1),a1),a1))), % 189.69/189.73 inference(scs_inference,[],[10,534,535,2,3])). % 189.69/189.73 cnf(540,plain, % 189.69/189.73 (E(f2(f2(f2(a7,a1),a1),a1),f2(f2(f2(a4,a1),a1),a1))), % 189.69/189.73 inference(scs_inference,[],[538,2])). % 189.69/189.73 cnf(541,plain, % 189.69/189.73 (E(f2(f2(a4,f2(f3(a4,a4),a1)),a1),a8)), % 189.69/189.73 inference(scs_inference,[],[10,182,538,2,3])). % 189.69/189.73 cnf(543,plain, % 189.69/189.73 (E(a8,f2(f2(a4,f2(f3(a4,a4),a1)),a1))), % 189.69/189.73 inference(scs_inference,[],[541,2])). % 189.69/189.73 cnf(544,plain, % 189.69/189.73 (E(f2(f3(x5441,f2(a4,x5441)),a1),f2(a4,f2(f3(a4,a4),a1)))), % 189.69/189.73 inference(scs_inference,[],[10,198,541,2,3])). % 189.69/189.73 cnf(546,plain, % 189.69/189.73 (E(f2(a4,f2(f3(a4,a4),a1)),f2(f3(x5461,f2(a4,x5461)),a1))), % 189.69/189.73 inference(scs_inference,[],[544,2])). % 189.69/189.73 cnf(547,plain, % 189.69/189.73 (E(f2(a8,a1),f2(f2(a4,f2(f3(a4,a4),a1)),a1))), % 189.69/189.73 inference(scs_inference,[],[10,543,544,2,3])). % 189.69/189.73 cnf(549,plain, % 189.69/189.73 (E(f2(f2(a4,f2(f3(a4,a4),a1)),a1),f2(a8,a1))), % 189.69/189.73 inference(scs_inference,[],[547,2])). % 189.69/189.73 cnf(550,plain, % 189.69/189.73 (E(f2(f2(f6(a5,f2(a4,a4)),f2(a4,a4)),a1),f3(x5501,f2(a4,x5501)))), % 189.69/189.73 inference(scs_inference,[],[10,222,547,2,3])). % 189.69/189.73 cnf(552,plain, % 189.69/189.73 (E(f3(x5521,f2(a4,x5521)),f2(f2(f6(a5,f2(a4,a4)),f2(a4,a4)),a1))), % 189.69/189.73 inference(scs_inference,[],[550,2])). % 189.69/189.73 cnf(553,plain, % 189.69/189.73 (E(f2(f2(a4,f2(f3(a4,a5),a1)),a1),f3(x5531,f2(a4,x5531)))), % 189.69/189.73 inference(scs_inference,[],[10,163,550,2,3])). % 189.69/189.73 cnf(555,plain, % 189.69/189.73 (E(f3(x5551,f2(a4,x5551)),f2(f2(a4,f2(f3(a4,a5),a1)),a1))), % 189.69/189.73 inference(scs_inference,[],[553,2])). % 189.69/189.73 cnf(556,plain, % 189.69/189.73 (E(f2(f3(x5561,f2(a4,x5561)),a1),f2(f2(f6(a5,f2(a4,a4)),f2(a4,a4)),a1))), % 189.69/189.73 inference(scs_inference,[],[10,552,553,2,3])). % 189.69/189.73 cnf(558,plain, % 189.69/189.73 (E(f2(f2(f6(a5,f2(a4,a4)),f2(a4,a4)),a1),f2(f3(x5581,f2(a4,x5581)),a1))), % 189.69/189.73 inference(scs_inference,[],[556,2])). % 189.69/189.73 cnf(559,plain, % 189.69/189.73 (E(f2(f2(f6(a4,f2(a1,x5591)),x5591),a1),f3(x5592,f2(a4,x5592)))), % 189.69/189.73 inference(scs_inference,[],[10,152,556,2,3])). % 189.69/189.73 cnf(561,plain, % 189.69/189.73 (E(f3(x5611,f2(a4,x5611)),f2(f2(f6(a4,f2(a1,x5612)),x5612),a1))), % 189.69/189.73 inference(scs_inference,[],[559,2])). % 189.69/189.73 cnf(562,plain, % 189.69/189.73 (E(f2(f2(f6(a4,f2(x5621,a4)),f2(a4,x5621)),a1),f2(f6(a5,f2(a4,a4)),f2(a4,a4)))), % 189.69/189.73 inference(scs_inference,[],[10,252,559,2,3])). % 189.69/189.73 cnf(564,plain, % 189.69/189.73 (E(f2(f6(a5,f2(a4,a4)),f2(a4,a4)),f2(f2(f6(a4,f2(x5641,a4)),f2(a4,x5641)),a1))), % 189.69/189.73 inference(scs_inference,[],[562,2])). % 189.69/189.73 cnf(565,plain, % 189.69/189.73 (E(f2(f3(x5651,f2(a4,x5651)),a1),f6(a4,f2(a1,a1)))), % 189.69/189.73 inference(scs_inference,[],[10,195,562,2,3])). % 189.69/189.73 cnf(567,plain, % 189.69/189.73 (E(f6(a4,f2(a1,a1)),f2(f3(x5671,f2(a4,x5671)),a1))), % 189.69/189.73 inference(scs_inference,[],[565,2])). % 189.69/189.73 cnf(568,plain, % 189.69/189.73 (E(f2(f2(x5681,f2(x5682,a4)),a1),f2(f2(x5681,x5682),a4))), % 189.69/189.73 inference(scs_inference,[],[10,85,565,2,3])). % 189.69/189.73 cnf(570,plain, % 189.69/189.73 (E(f2(f2(x5701,x5702),a4),f2(f2(x5701,f2(x5702,a4)),a1))), % 189.69/189.73 inference(scs_inference,[],[568,2])). % 189.69/189.73 cnf(571,plain, % 189.69/189.73 (E(f2(f6(a4,f2(a1,a1)),a1),f2(f3(x5711,f2(a4,x5711)),a1))), % 189.69/189.73 inference(scs_inference,[],[10,567,568,2,3])). % 189.69/189.73 cnf(573,plain, % 189.69/189.73 (E(f2(f3(x5731,f2(a4,x5731)),a1),f2(f6(a4,f2(a1,a1)),a1))), % 189.69/189.73 inference(scs_inference,[],[571,2])). % 189.69/189.73 cnf(574,plain, % 189.69/189.73 (E(f2(f2(f2(x5741,x5742),a4),a1),f2(f2(x5741,f2(x5742,a4)),a1))), % 189.69/189.73 inference(scs_inference,[],[10,570,571,2,3])). % 189.69/189.73 cnf(577,plain, % 189.69/189.73 (E(f2(f2(f6(a4,f2(x5771,a4)),f2(a4,x5771)),a1),f6(a4,f2(a1,a1)))), % 189.69/189.73 inference(scs_inference,[],[10,232,574,2,3])). % 189.69/189.73 cnf(579,plain, % 189.69/189.73 (E(f6(a4,f2(a1,a1)),f2(f2(f6(a4,f2(x5791,a4)),f2(a4,x5791)),a1))), % 189.69/189.73 inference(scs_inference,[],[577,2])). % 189.69/189.73 cnf(580,plain, % 189.69/189.73 (E(f2(a7,a1),f2(x5801,f2(x5802,f3(f2(x5801,x5802),a4))))), % 189.69/189.73 inference(scs_inference,[],[10,244,577,2,3])). % 189.69/189.73 cnf(582,plain, % 189.69/189.73 (E(f2(x5821,f2(x5822,f3(f2(x5821,x5822),a4))),f2(a7,a1))), % 189.69/189.73 inference(scs_inference,[],[580,2])). % 189.69/189.73 cnf(583,plain, % 189.69/189.73 (E(f2(f6(a4,f2(a1,a1)),a1),f2(f2(f6(a4,f2(x5831,a4)),f2(a4,x5831)),a1))), % 189.69/189.73 inference(scs_inference,[],[10,579,580,2,3])). % 189.69/189.73 cnf(585,plain, % 189.69/189.73 (E(f2(f2(f6(a4,f2(x5851,a4)),f2(a4,x5851)),a1),f2(f6(a4,f2(a1,a1)),a1))), % 189.69/189.73 inference(scs_inference,[],[583,2])). % 189.69/189.73 cnf(586,plain, % 189.69/189.73 (E(f2(a5,a1),f3(x5861,f2(a4,x5861)))), % 189.69/189.73 inference(scs_inference,[],[10,145,583,2,3])). % 189.69/189.73 cnf(588,plain, % 189.69/189.73 (E(f3(x5881,f2(a4,x5881)),f2(a5,a1))), % 189.69/189.73 inference(scs_inference,[],[586,2])). % 189.69/189.73 cnf(589,plain, % 189.69/189.73 (E(f2(f3(x5891,f2(a4,x5891)),a1),a8)), % 189.69/189.73 inference(scs_inference,[],[10,147,586,2,3])). % 189.69/189.73 cnf(591,plain, % 189.69/189.73 (E(a8,f2(f3(x5911,f2(a4,x5911)),a1))), % 189.69/189.73 inference(scs_inference,[],[589,2])). % 189.69/189.73 cnf(592,plain, % 189.69/189.73 (E(f2(f3(x5921,f2(a4,x5921)),a1),f2(a5,a1))), % 189.69/189.73 inference(scs_inference,[],[10,588,589,2,3])). % 189.69/189.73 cnf(594,plain, % 189.69/189.73 (E(f2(a5,a1),f2(f3(x5941,f2(a4,x5941)),a1))), % 189.69/189.73 inference(scs_inference,[],[592,2])). % 189.69/189.73 cnf(595,plain, % 189.69/189.73 (E(f2(a8,a1),f2(f3(x5951,f2(a4,x5951)),a1))), % 189.69/189.73 inference(scs_inference,[],[10,591,592,2,3])). % 189.69/189.73 cnf(597,plain, % 189.69/189.73 (E(f2(f3(x5971,f2(a4,x5971)),a1),f2(a8,a1))), % 189.69/189.73 inference(scs_inference,[],[595,2])). % 189.69/189.73 cnf(598,plain, % 189.69/189.73 (E(f2(f2(a5,a1),a1),f2(f3(x5981,f2(a4,x5981)),a1))), % 189.69/189.73 inference(scs_inference,[],[10,594,595,2,3])). % 189.69/189.73 cnf(600,plain, % 189.69/189.73 (E(f2(f3(x6001,f2(a4,x6001)),a1),f2(f2(a5,a1),a1))), % 189.69/189.73 inference(scs_inference,[],[598,2])). % 189.69/189.73 cnf(601,plain, % 189.69/189.73 (E(f2(f2(f3(x6011,f2(a4,x6011)),a1),a1),f2(a8,a1))), % 189.69/189.73 inference(scs_inference,[],[10,597,598,2,3])). % 189.69/189.73 cnf(603,plain, % 189.69/189.73 (E(f2(a8,a1),f2(f2(f3(x6031,f2(a4,x6031)),a1),a1))), % 189.69/189.73 inference(scs_inference,[],[601,2])). % 189.69/189.73 cnf(604,plain, % 189.69/189.73 (E(f2(f2(f3(x6041,f2(a4,x6041)),a1),a1),f2(f2(a5,a1),a1))), % 189.69/189.73 inference(scs_inference,[],[10,600,601,2,3])). % 189.69/189.73 cnf(606,plain, % 189.69/189.73 (E(f2(f2(a5,a1),a1),f2(f2(f3(x6061,f2(a4,x6061)),a1),a1))), % 189.69/189.73 inference(scs_inference,[],[604,2])). % 189.69/189.73 cnf(607,plain, % 189.69/189.73 (E(f2(f2(a8,a1),a1),f2(f2(f3(x6071,f2(a4,x6071)),a1),a1))), % 189.69/189.73 inference(scs_inference,[],[10,603,604,2,3])). % 189.69/189.73 cnf(609,plain, % 189.69/189.73 (E(f2(f2(f3(x6091,f2(a4,x6091)),a1),a1),f2(f2(a8,a1),a1))), % 189.69/189.73 inference(scs_inference,[],[607,2])). % 189.69/189.73 cnf(610,plain, % 189.69/189.73 (E(f2(f3(x6101,f2(a4,x6101)),a1),a7)), % 189.69/189.73 inference(scs_inference,[],[10,270,607,2,3])). % 189.69/189.73 cnf(612,plain, % 189.69/189.73 (E(a7,f2(f3(x6121,f2(a4,x6121)),a1))), % 189.69/189.73 inference(scs_inference,[],[610,2])). % 189.69/189.73 cnf(613,plain, % 189.69/189.73 (E(f2(a7,a1),f2(x6131,f3(f2(a1,x6131),a4)))), % 189.69/189.73 inference(scs_inference,[],[10,76,610,2,3])). % 189.69/189.73 cnf(615,plain, % 189.69/189.73 (E(f2(x6151,f3(f2(a1,x6151),a4)),f2(a7,a1))), % 189.69/189.73 inference(scs_inference,[],[613,2])). % 189.69/189.73 cnf(616,plain, % 189.69/189.73 (E(f2(a7,a1),f2(f3(x6161,f2(a4,x6161)),a1))), % 189.69/189.73 inference(scs_inference,[],[10,612,613,2,3])). % 189.69/189.73 cnf(618,plain, % 189.69/189.73 (E(f2(f3(x6181,f2(a4,x6181)),a1),f2(a7,a1))), % 189.69/189.73 inference(scs_inference,[],[616,2])). % 189.69/189.73 cnf(619,plain, % 189.69/189.73 (E(f2(f2(x6191,f3(f2(a1,x6191),a4)),a1),f2(a7,a1))), % 189.69/189.73 inference(scs_inference,[],[10,615,616,2,3])). % 189.69/189.73 cnf(621,plain, % 189.69/189.73 (E(f2(a7,a1),f2(f2(x6211,f3(f2(a1,x6211),a4)),a1))), % 189.69/189.73 inference(scs_inference,[],[619,2])). % 189.69/189.73 cnf(622,plain, % 189.69/189.73 (E(f2(f2(f3(x6221,f2(a4,x6221)),a1),a1),f2(a7,a1))), % 189.69/189.73 inference(scs_inference,[],[10,618,619,2,3])). % 189.69/189.73 cnf(624,plain, % 189.69/189.73 (E(f2(a7,a1),f2(f2(f3(x6241,f2(a4,x6241)),a1),a1))), % 189.69/189.73 inference(scs_inference,[],[622,2])). % 189.69/189.73 cnf(625,plain, % 189.69/189.73 (E(f2(f2(a7,a1),a1),f2(f2(x6251,f3(f2(a1,x6251),a4)),a1))), % 189.69/189.73 inference(scs_inference,[],[10,621,622,2,3])). % 189.69/189.73 cnf(627,plain, % 189.69/189.73 (E(f2(f2(x6271,f3(f2(a1,x6271),a4)),a1),f2(f2(a7,a1),a1))), % 189.69/189.73 inference(scs_inference,[],[625,2])). % 189.69/189.73 cnf(628,plain, % 189.69/189.73 (E(f2(f2(a7,a1),a1),f2(f2(f3(x6281,f2(a4,x6281)),a1),a1))), % 189.69/189.73 inference(scs_inference,[],[10,624,625,2,3])). % 189.69/189.73 cnf(630,plain, % 189.69/189.73 (E(f2(f2(f3(x6301,f2(a4,x6301)),a1),a1),f2(f2(a7,a1),a1))), % 189.69/189.73 inference(scs_inference,[],[628,2])). % 189.69/189.73 cnf(631,plain, % 189.69/189.73 (E(f2(a4,a1),f2(f6(a4,f2(a1,x6311)),x6311))), % 189.69/189.73 inference(scs_inference,[],[10,220,628,2,3])). % 189.69/189.73 cnf(633,plain, % 189.69/189.73 (E(f2(f6(a4,f2(a1,x6331)),x6331),f2(a4,a1))), % 189.69/189.73 inference(scs_inference,[],[631,2])). % 189.69/189.73 cnf(634,plain, % 189.69/189.73 (E(f2(f2(x6341,f3(f2(a1,x6341),a4)),a1),a4)), % 189.69/189.73 inference(scs_inference,[],[10,298,631,2,3])). % 189.69/189.73 cnf(636,plain, % 189.69/189.73 (E(a4,f2(f2(x6361,f3(f2(a1,x6361),a4)),a1))), % 189.69/189.73 inference(scs_inference,[],[634,2])). % 189.69/189.73 cnf(637,plain, % 189.69/189.73 (E(f2(f2(f6(a4,f2(a1,x6371)),x6371),a1),f2(a4,a1))), % 189.69/189.73 inference(scs_inference,[],[10,633,634,2,3])). % 189.69/189.73 cnf(639,plain, % 189.69/189.73 (E(f2(a4,a1),f2(f2(f6(a4,f2(a1,x6391)),x6391),a1))), % 189.69/189.73 inference(scs_inference,[],[637,2])). % 189.69/189.73 cnf(640,plain, % 189.69/189.73 (E(f2(a4,a1),f2(f2(x6401,f3(f2(a1,x6401),a4)),a1))), % 189.69/189.73 inference(scs_inference,[],[10,636,637,2,3])). % 189.69/189.73 cnf(642,plain, % 189.69/189.73 (E(f2(f2(x6421,f3(f2(a1,x6421),a4)),a1),f2(a4,a1))), % 189.69/189.73 inference(scs_inference,[],[640,2])). % 189.69/189.73 cnf(643,plain, % 189.69/189.73 (E(f2(f2(a4,a1),a1),f2(f2(f6(a4,f2(a1,x6431)),x6431),a1))), % 189.69/189.73 inference(scs_inference,[],[10,639,640,2,3])). % 189.69/189.73 cnf(645,plain, % 189.69/189.73 (E(f2(f2(f6(a4,f2(a1,x6451)),x6451),a1),f2(f2(a4,a1),a1))), % 189.69/189.73 inference(scs_inference,[],[643,2])). % 189.69/189.73 cnf(646,plain, % 189.69/189.73 (E(f2(a5,a1),f2(f6(a4,f2(x6461,a4)),f2(a4,x6461)))), % 189.69/189.73 inference(scs_inference,[],[10,224,643,2,3])). % 189.69/189.73 cnf(648,plain, % 189.69/189.73 (E(f2(f6(a4,f2(x6481,a4)),f2(a4,x6481)),f2(a5,a1))), % 189.69/189.73 inference(scs_inference,[],[646,2])). % 189.69/189.73 cnf(649,plain, % 189.69/189.73 (E(f2(a5,a1),f2(a4,f2(x6491,f3(f2(a4,x6491),a4))))), % 189.69/189.73 inference(scs_inference,[],[10,55,646,2,3])). % 189.69/189.73 cnf(651,plain, % 189.69/189.73 (E(f2(a4,f2(x6511,f3(f2(a4,x6511),a4))),f2(a5,a1))), % 189.69/189.73 inference(scs_inference,[],[649,2])). % 189.69/189.73 cnf(652,plain, % 189.69/189.73 (E(f2(f2(f6(a4,f2(x6521,a4)),f2(a4,x6521)),a1),f2(a5,a1))), % 189.69/189.73 inference(scs_inference,[],[10,648,649,2,3])). % 189.69/189.73 cnf(654,plain, % 189.69/189.73 (E(f2(a5,a1),f2(f2(f6(a4,f2(x6541,a4)),f2(a4,x6541)),a1))), % 189.69/189.73 inference(scs_inference,[],[652,2])). % 189.69/189.73 cnf(655,plain, % 189.69/189.73 (E(f2(a4,a1),f2(a4,f2(x6551,f3(f2(a4,x6551),a5))))), % 189.69/189.73 inference(scs_inference,[],[10,58,652,2,3])). % 189.69/189.73 cnf(658,plain, % 189.69/189.73 (E(f2(a1,f2(a5,a1)),f2(f2(f6(a4,f2(x6581,a4)),f2(a4,x6581)),a1))), % 189.69/189.73 inference(scs_inference,[],[11,654,655,2,3])). % 189.69/189.73 cnf(660,plain, % 189.69/189.73 (E(f2(f2(f6(a4,f2(x6601,a4)),f2(a4,x6601)),a1),f2(a1,f2(a5,a1)))), % 189.69/189.73 inference(scs_inference,[],[658,2])). % 189.69/189.73 cnf(661,plain, % 189.69/189.73 (E(f2(a1,f2(a8,a1)),f2(a7,a1))), % 189.69/189.73 inference(scs_inference,[],[11,363,658,2,3])). % 189.69/189.73 cnf(663,plain, % 189.69/189.73 (E(f2(a7,a1),f2(a1,f2(a8,a1)))), % 189.69/189.73 inference(scs_inference,[],[661,2])). % 189.69/189.73 cnf(664,plain, % 189.69/189.73 (E(f2(a1,a7),f2(a8,a1))), % 189.69/189.73 inference(scs_inference,[],[11,360,661,2,3])). % 189.69/189.73 cnf(666,plain, % 189.69/189.73 (E(f2(a8,a1),f2(a1,a7))), % 189.69/189.73 inference(scs_inference,[],[664,2])). % 189.69/189.73 cnf(667,plain, % 189.69/189.73 (E(f2(a1,f2(a7,a1)),f2(a1,f2(a8,a1)))), % 189.69/189.73 inference(scs_inference,[],[11,663,664,2,3])). % 189.69/189.73 cnf(669,plain, % 189.69/189.73 (E(f2(a1,f2(a8,a1)),f2(a1,f2(a7,a1)))), % 189.69/189.73 inference(scs_inference,[],[667,2])). % 189.69/189.73 cnf(670,plain, % 189.69/189.73 (E(f2(a1,f2(a8,a1)),f2(a1,a7))), % 189.69/189.73 inference(scs_inference,[],[11,666,667,2,3])). % 189.69/189.73 cnf(672,plain, % 189.69/189.73 (E(f2(a1,a7),f2(a1,f2(a8,a1)))), % 189.69/189.73 inference(scs_inference,[],[670,2])). % 189.69/189.73 cnf(673,plain, % 189.69/189.73 (E(f2(a1,f2(a1,f2(a8,a1))),f2(a1,f2(a7,a1)))), % 189.69/189.73 inference(scs_inference,[],[11,669,670,2,3])). % 189.69/189.73 cnf(675,plain, % 189.69/189.73 (E(f2(a1,f2(a7,a1)),f2(a1,f2(a1,f2(a8,a1))))), % 189.69/189.73 inference(scs_inference,[],[673,2])). % 189.69/189.73 cnf(676,plain, % 189.69/189.73 (E(f2(a1,f2(a1,a7)),f2(a1,f2(a8,a1)))), % 189.69/189.73 inference(scs_inference,[],[11,672,673,2,3])). % 189.69/189.73 cnf(678,plain, % 189.69/189.73 (E(f2(a1,f2(a8,a1)),f2(a1,f2(a1,a7)))), % 189.69/189.73 inference(scs_inference,[],[676,2])). % 189.69/189.73 cnf(679,plain, % 189.69/189.73 (E(f2(a1,f2(a1,f2(a7,a1))),f2(a1,f2(a1,f2(a8,a1))))), % 189.69/189.73 inference(scs_inference,[],[11,675,676,2,3])). % 189.69/189.73 cnf(681,plain, % 189.69/189.73 (E(f2(a1,f2(a1,f2(a8,a1))),f2(a1,f2(a1,f2(a7,a1))))), % 189.69/189.73 inference(scs_inference,[],[679,2])). % 189.69/189.73 cnf(682,plain, % 189.69/189.73 (E(f2(a1,f2(a1,f2(a8,a1))),f2(a1,f2(a1,a7)))), % 189.69/189.73 inference(scs_inference,[],[11,678,679,2,3])). % 189.69/189.73 cnf(684,plain, % 189.69/189.73 (E(f2(a1,f2(a1,a7)),f2(a1,f2(a1,f2(a8,a1))))), % 189.69/189.73 inference(scs_inference,[],[682,2])). % 189.69/189.73 cnf(685,plain, % 189.69/189.73 (E(f2(a1,f2(a7,a1)),f2(f2(a8,a1),a1))), % 189.69/189.73 inference(scs_inference,[],[11,366,682,2,3])). % 189.69/189.73 cnf(687,plain, % 189.69/189.73 (E(f2(f2(a8,a1),a1),f2(a1,f2(a7,a1)))), % 189.69/189.73 inference(scs_inference,[],[685,2])). % 189.69/189.73 cnf(688,plain, % 189.69/189.73 (E(f2(a1,f2(a1,f2(a1,a7))),f2(a1,f2(a1,f2(a8,a1))))), % 189.69/189.73 inference(scs_inference,[],[11,684,685,2,3])). % 189.69/189.73 cnf(690,plain, % 189.69/189.73 (E(f2(a1,f2(a1,f2(a8,a1))),f2(a1,f2(a1,f2(a1,a7))))), % 189.69/189.73 inference(scs_inference,[],[688,2])). % 189.69/189.73 cnf(691,plain, % 189.69/189.73 (E(f2(a1,f2(f2(a8,a1),a1)),f2(a1,f2(a7,a1)))), % 189.69/189.73 inference(scs_inference,[],[11,687,688,2,3])). % 189.69/189.73 cnf(693,plain, % 189.69/189.73 (E(f2(a1,f2(a7,a1)),f2(a1,f2(f2(a8,a1),a1)))), % 189.69/189.73 inference(scs_inference,[],[691,2])). % 189.69/189.73 cnf(694,plain, % 189.69/189.73 (E(f2(a1,f2(f2(a8,a1),a1)),f2(f2(a7,a1),a1))), % 189.69/189.73 inference(scs_inference,[],[11,369,691,2,3])). % 189.69/189.73 cnf(696,plain, % 189.69/189.73 (E(f2(f2(a7,a1),a1),f2(a1,f2(f2(a8,a1),a1)))), % 189.69/189.73 inference(scs_inference,[],[694,2])). % 189.69/189.73 cnf(697,plain, % 189.69/189.73 (E(f2(a1,f2(a1,f2(a7,a1))),f2(a1,f2(f2(a8,a1),a1)))), % 189.69/189.73 inference(scs_inference,[],[11,693,694,2,3])). % 189.69/189.73 cnf(699,plain, % 189.69/189.73 (E(f2(a1,f2(f2(a8,a1),a1)),f2(a1,f2(a1,f2(a7,a1))))), % 189.69/189.73 inference(scs_inference,[],[697,2])). % 189.69/189.73 cnf(700,plain, % 189.69/189.73 (E(f2(a1,f2(f2(a7,a1),a1)),f2(a1,f2(f2(a8,a1),a1)))), % 189.69/189.73 inference(scs_inference,[],[11,696,697,2,3])). % 189.69/189.73 cnf(702,plain, % 189.69/189.73 (E(f2(a1,f2(f2(a8,a1),a1)),f2(a1,f2(f2(a7,a1),a1)))), % 189.69/189.73 inference(scs_inference,[],[700,2])). % 189.69/189.73 cnf(703,plain, % 189.69/189.73 (E(f2(a1,f2(f2(a7,a1),a1)),f2(f2(f2(a8,a1),a1),a1))), % 189.69/189.73 inference(scs_inference,[],[11,372,700,2,3])). % 189.69/189.73 cnf(705,plain, % 189.69/189.73 (E(f2(f2(f2(a8,a1),a1),a1),f2(a1,f2(f2(a7,a1),a1)))), % 189.69/189.73 inference(scs_inference,[],[703,2])). % 189.69/189.73 cnf(706,plain, % 189.69/189.73 (E(f2(a1,f2(f2(f6(a5,f2(a4,a4)),f2(a4,a4)),a1)),f2(a8,a1))), % 189.69/189.73 inference(scs_inference,[],[11,381,703,2,3])). % 189.69/189.73 cnf(708,plain, % 189.69/189.73 (E(f2(a8,a1),f2(a1,f2(f2(f6(a5,f2(a4,a4)),f2(a4,a4)),a1)))), % 189.69/189.73 inference(scs_inference,[],[706,2])). % 189.69/189.73 cnf(709,plain, % 189.69/189.73 (E(f2(a1,a8),f2(f2(f6(a5,f2(a4,a4)),f2(a4,a4)),a1))), % 189.69/189.73 inference(scs_inference,[],[11,378,706,2,3])). % 189.69/189.73 cnf(711,plain, % 189.69/189.73 (E(f2(f2(f6(a5,f2(a4,a4)),f2(a4,a4)),a1),f2(a1,a8))), % 189.69/189.73 inference(scs_inference,[],[709,2])). % 189.69/189.73 cnf(712,plain, % 189.69/189.73 (E(f2(a1,f2(a7,a1)),f2(f2(a4,f2(f3(a4,a5),a1)),a1))), % 189.69/189.73 inference(scs_inference,[],[11,513,709,2,3])). % 189.69/189.73 cnf(714,plain, % 189.69/189.73 (E(f2(f2(a4,f2(f3(a4,a5),a1)),a1),f2(a1,f2(a7,a1)))), % 189.69/189.73 inference(scs_inference,[],[712,2])). % 189.69/189.73 cnf(715,plain, % 189.69/189.73 (E(f2(a1,f2(f2(f6(a5,f2(a4,a4)),f2(a4,a4)),a1)),f2(a1,a8))), % 189.69/189.73 inference(scs_inference,[],[11,711,712,2,3])). % 189.69/189.73 cnf(718,plain, % 189.69/189.73 (E(f2(a1,a4),f2(a4,f2(f3(f2(a1,a4),a4),a1)))), % 189.69/189.73 inference(scs_inference,[],[11,283,715,2,3])). % 189.69/189.73 cnf(720,plain, % 189.69/189.73 (E(f2(a4,f2(f3(f2(a1,a4),a4),a1)),f2(a1,a4))), % 189.69/189.73 inference(scs_inference,[],[718,2])). % 189.69/189.73 cnf(721,plain, % 189.69/189.73 (E(f2(a1,f2(a7,a1)),f2(a4,a1))), % 189.69/189.73 inference(scs_inference,[],[11,516,718,2,3])). % 189.69/189.73 cnf(723,plain, % 189.69/189.73 (E(f2(a4,a1),f2(a1,f2(a7,a1)))), % 189.69/189.73 inference(scs_inference,[],[721,2])). % 189.69/189.73 cnf(724,plain, % 189.69/189.73 (E(f2(a1,f2(a4,a1)),f2(f2(a7,a1),a1))), % 189.69/189.73 inference(scs_inference,[],[11,522,721,2,3])). % 189.69/189.73 cnf(726,plain, % 189.69/189.73 (E(f2(f2(a7,a1),a1),f2(a1,f2(a4,a1)))), % 189.69/189.73 inference(scs_inference,[],[724,2])). % 189.69/189.73 cnf(727,plain, % 189.69/189.73 (E(f2(a1,f2(a4,a1)),f2(a1,f2(a7,a1)))), % 189.69/189.73 inference(scs_inference,[],[11,723,724,2,3])). % 189.69/189.73 cnf(729,plain, % 189.69/189.73 (E(f2(a1,f2(a7,a1)),f2(a1,f2(a4,a1)))), % 189.69/189.73 inference(scs_inference,[],[727,2])). % 189.69/189.73 cnf(730,plain, % 189.69/189.73 (E(f2(a1,f2(f2(a7,a1),a1)),f2(a1,f2(a4,a1)))), % 189.69/189.73 inference(scs_inference,[],[11,726,727,2,3])). % 189.69/189.73 cnf(732,plain, % 189.69/189.73 (E(f2(a1,f2(a4,a1)),f2(a1,f2(f2(a7,a1),a1)))), % 189.69/189.73 inference(scs_inference,[],[730,2])). % 189.69/189.73 cnf(733,plain, % 189.69/189.73 (E(f2(a1,f2(a1,f2(a7,a1))),f2(a1,f2(a4,a1)))), % 189.69/189.73 inference(scs_inference,[],[11,729,730,2,3])). % 189.69/189.73 cnf(735,plain, % 189.69/189.73 (E(f2(a1,f2(a4,a1)),f2(a1,f2(a1,f2(a7,a1))))), % 189.69/189.73 inference(scs_inference,[],[733,2])). % 189.69/189.73 cnf(736,plain, % 189.69/189.73 (E(f2(a1,f2(a1,f2(a4,a1))),f2(a1,f2(f2(a7,a1),a1)))), % 189.69/189.73 inference(scs_inference,[],[11,732,733,2,3])). % 189.69/189.73 cnf(738,plain, % 189.69/189.73 (E(f2(a1,f2(f2(a7,a1),a1)),f2(a1,f2(a1,f2(a4,a1))))), % 189.69/189.73 inference(scs_inference,[],[736,2])). % 189.69/189.73 cnf(739,plain, % 189.69/189.73 (E(f2(a1,f2(a1,f2(a4,a1))),f2(a1,f2(a1,f2(a7,a1))))), % 189.69/189.73 inference(scs_inference,[],[11,735,736,2,3])). % 189.69/189.73 cnf(741,plain, % 189.69/189.73 (E(f2(a1,f2(a1,f2(a7,a1))),f2(a1,f2(a1,f2(a4,a1))))), % 189.69/189.73 inference(scs_inference,[],[739,2])). % 189.69/189.73 cnf(742,plain, % 189.69/189.73 (E(f2(a1,f2(a8,a1)),f2(f6(a4,f2(a1,a1)),a1))), % 189.69/189.73 inference(scs_inference,[],[11,423,739,2,3])). % 189.69/189.73 cnf(744,plain, % 189.69/189.73 (E(f2(f6(a4,f2(a1,a1)),a1),f2(a1,f2(a8,a1)))), % 189.69/189.73 inference(scs_inference,[],[742,2])). % 189.69/189.73 cnf(745,plain, % 189.69/189.73 (E(f2(a1,f2(f6(a4,f2(a1,a1)),a1)),f2(f2(a8,a1),a1))), % 189.69/189.73 inference(scs_inference,[],[11,429,742,2,3])). % 189.69/189.73 cnf(747,plain, % 189.69/189.73 (E(f2(f2(a8,a1),a1),f2(a1,f2(f6(a4,f2(a1,a1)),a1)))), % 189.69/189.73 inference(scs_inference,[],[745,2])). % 189.69/189.73 cnf(748,plain, % 189.69/189.73 (E(f2(a1,f2(f6(a4,f2(a1,a1)),a1)),f2(a1,f2(a8,a1)))), % 189.69/189.73 inference(scs_inference,[],[11,744,745,2,3])). % 189.69/189.73 cnf(750,plain, % 189.69/189.73 (E(f2(a1,f2(a8,a1)),f2(a1,f2(f6(a4,f2(a1,a1)),a1)))), % 189.69/189.73 inference(scs_inference,[],[748,2])). % 189.69/189.73 cnf(751,plain, % 189.69/189.73 (E(f2(a1,f2(a8,a1)),f2(f2(a4,f2(f3(a4,a5),a1)),a1))), % 189.69/189.73 inference(scs_inference,[],[11,399,748,2,3])). % 189.69/189.73 cnf(753,plain, % 189.69/189.73 (E(f2(f2(a4,f2(f3(a4,a5),a1)),a1),f2(a1,f2(a8,a1)))), % 189.69/189.73 inference(scs_inference,[],[751,2])). % 189.69/189.73 cnf(754,plain, % 189.69/189.73 (E(f2(a1,f2(f2(a4,a1),a1)),f2(f2(f2(a7,a1),a1),a1))), % 189.69/189.73 inference(scs_inference,[],[11,534,751,2,3])). % 189.69/189.73 cnf(756,plain, % 189.69/189.73 (E(f2(f2(f2(a7,a1),a1),a1),f2(a1,f2(f2(a4,a1),a1)))), % 189.69/189.73 inference(scs_inference,[],[754,2])). % 189.69/189.73 cnf(757,plain, % 189.69/189.73 (E(f2(a1,f2(a7,a1)),f2(f2(f6(a5,f2(a4,a4)),f2(a4,a4)),a1))), % 189.69/189.73 inference(scs_inference,[],[11,396,754,2,3])). % 189.69/189.73 cnf(759,plain, % 189.69/189.73 (E(f2(f2(f6(a5,f2(a4,a4)),f2(a4,a4)),a1),f2(a1,f2(a7,a1)))), % 189.69/189.73 inference(scs_inference,[],[757,2])). % 189.69/189.73 cnf(760,plain, % 189.69/189.73 (E(f2(a1,f2(f2(a7,a1),a1)),f2(f2(a4,a1),a1))), % 189.69/189.73 inference(scs_inference,[],[11,528,757,2,3])). % 189.69/189.73 cnf(762,plain, % 189.69/189.73 (E(f2(f2(a4,a1),a1),f2(a1,f2(f2(a7,a1),a1)))), % 189.69/189.73 inference(scs_inference,[],[760,2])). % 189.69/189.73 cnf(763,plain, % 189.69/189.73 (E(f2(a1,f2(a5,a1)),f2(a7,a1))), % 189.69/189.73 inference(scs_inference,[],[11,414,760,2,3])). % 189.69/189.73 cnf(765,plain, % 189.69/189.73 (E(f2(a7,a1),f2(a1,f2(a5,a1)))), % 189.69/189.73 inference(scs_inference,[],[763,2])). % 189.69/189.73 cnf(766,plain, % 189.69/189.73 (E(f2(a1,f2(f2(a4,a1),a1)),f2(a1,f2(f2(a7,a1),a1)))), % 189.69/189.73 inference(scs_inference,[],[11,762,763,2,3])). % 189.69/189.73 cnf(768,plain, % 189.69/189.73 (E(f2(a1,f2(f2(a7,a1),a1)),f2(a1,f2(f2(a4,a1),a1)))), % 189.69/189.73 inference(scs_inference,[],[766,2])). % 189.69/189.73 cnf(769,plain, % 189.69/189.73 (E(f2(a1,f2(a7,a1)),f2(a1,f2(a5,a1)))), % 189.69/189.73 inference(scs_inference,[],[11,765,766,2,3])). % 189.69/189.73 cnf(771,plain, % 189.69/189.73 (E(f2(a1,f2(a5,a1)),f2(a1,f2(a7,a1)))), % 189.69/189.73 inference(scs_inference,[],[769,2])). % 189.69/189.73 cnf(772,plain, % 189.69/189.73 (E(f2(a1,f2(a7,a1)),f2(f2(a5,a1),a1))), % 189.69/189.73 inference(scs_inference,[],[11,420,769,2,3])). % 189.69/189.73 cnf(774,plain, % 189.69/189.73 (E(f2(f2(a5,a1),a1),f2(a1,f2(a7,a1)))), % 189.69/189.73 inference(scs_inference,[],[772,2])). % 189.69/189.73 cnf(775,plain, % 189.69/189.73 (E(f2(a1,f2(a1,f2(a5,a1))),f2(a1,f2(a7,a1)))), % 189.69/189.73 inference(scs_inference,[],[11,771,772,2,3])). % 189.69/189.73 cnf(777,plain, % 189.69/189.73 (E(f2(a1,f2(a7,a1)),f2(a1,f2(a1,f2(a5,a1))))), % 189.69/189.73 inference(scs_inference,[],[775,2])). % 189.69/189.73 cnf(778,plain, % 189.69/189.73 (E(f2(a1,f2(f2(a5,a1),a1)),f2(a1,f2(a7,a1)))), % 189.69/189.73 inference(scs_inference,[],[11,774,775,2,3])). % 189.69/189.73 cnf(780,plain, % 189.69/189.73 (E(f2(a1,f2(a7,a1)),f2(a1,f2(f2(a5,a1),a1)))), % 189.69/189.73 inference(scs_inference,[],[778,2])). % 189.69/189.73 cnf(781,plain, % 189.69/189.73 (E(f2(a1,f2(a1,f2(a7,a1))),f2(a1,f2(a1,f2(a5,a1))))), % 189.69/189.73 inference(scs_inference,[],[11,777,778,2,3])). % 189.69/189.73 cnf(783,plain, % 189.69/189.73 (E(f2(a1,f2(a1,f2(a5,a1))),f2(a1,f2(a1,f2(a7,a1))))), % 189.69/189.73 inference(scs_inference,[],[781,2])). % 189.69/189.73 cnf(784,plain, % 189.69/189.73 (E(f2(a1,f2(a1,f2(a7,a1))),f2(a1,f2(f2(a5,a1),a1)))), % 189.69/189.73 inference(scs_inference,[],[11,780,781,2,3])). % 189.69/189.73 cnf(786,plain, % 189.69/189.73 (E(f2(a1,f2(f2(a5,a1),a1)),f2(a1,f2(a1,f2(a7,a1))))), % 189.69/189.73 inference(scs_inference,[],[784,2])). % 189.69/189.73 cnf(787,plain, % 189.69/189.73 (E(f2(a1,f2(a4,f2(f3(a4,a5),a1))),f2(a7,a1))), % 189.69/189.73 inference(scs_inference,[],[11,507,784,2,3])). % 189.69/189.73 cnf(789,plain, % 189.69/189.73 (E(f2(a7,a1),f2(a1,f2(a4,f2(f3(a4,a5),a1))))), % 189.69/189.73 inference(scs_inference,[],[787,2])). % 189.69/189.73 cnf(790,plain, % 189.69/189.73 (E(f2(a1,f2(f2(a5,a1),a1)),f2(f2(a7,a1),a1))), % 189.69/189.73 inference(scs_inference,[],[11,426,787,2,3])). % 189.69/189.73 cnf(792,plain, % 189.69/189.73 (E(f2(f2(a7,a1),a1),f2(a1,f2(f2(a5,a1),a1)))), % 189.69/189.73 inference(scs_inference,[],[790,2])). % 189.69/189.73 cnf(793,plain, % 189.69/189.73 (E(f2(a1,f2(a7,a1)),f2(a1,f2(a4,f2(f3(a4,a5),a1))))), % 189.69/189.73 inference(scs_inference,[],[11,789,790,2,3])). % 189.69/189.73 cnf(795,plain, % 189.69/189.73 (E(f2(a1,f2(a4,f2(f3(a4,a5),a1))),f2(a1,f2(a7,a1)))), % 189.69/189.73 inference(scs_inference,[],[793,2])). % 189.69/189.73 cnf(796,plain, % 189.69/189.73 (E(f2(a1,f2(f2(a7,a1),a1)),f2(a1,f2(f2(a5,a1),a1)))), % 189.69/189.73 inference(scs_inference,[],[11,792,793,2,3])). % 189.69/189.73 cnf(798,plain, % 189.69/189.73 (E(f2(a1,f2(f2(a5,a1),a1)),f2(a1,f2(f2(a7,a1),a1)))), % 189.69/189.73 inference(scs_inference,[],[796,2])). % 189.69/189.73 cnf(799,plain, % 189.69/189.73 (E(f2(a1,f2(a4,f2(f3(a4,a5),a1))),f2(a8,a1))), % 189.69/189.73 inference(scs_inference,[],[11,393,796,2,3])). % 189.69/189.73 cnf(801,plain, % 189.69/189.73 (E(f2(a8,a1),f2(a1,f2(a4,f2(f3(a4,a5),a1))))), % 189.69/189.73 inference(scs_inference,[],[799,2])). % 189.69/189.73 cnf(802,plain, % 189.69/189.73 (E(f2(a1,f2(f6(a5,f2(a4,a4)),f2(a4,a4))),f2(a7,a1))), % 189.69/189.73 inference(scs_inference,[],[11,390,799,2,3])). % 189.69/189.73 cnf(804,plain, % 189.69/189.73 (E(f2(a7,a1),f2(a1,f2(f6(a5,f2(a4,a4)),f2(a4,a4))))), % 189.69/189.73 inference(scs_inference,[],[802,2])). % 189.69/189.73 cnf(805,plain, % 189.69/189.73 (E(f2(a1,f2(a8,a1)),f2(a1,f2(a4,f2(f3(a4,a5),a1))))), % 189.69/189.73 inference(scs_inference,[],[11,801,802,2,3])). % 189.69/189.73 cnf(807,plain, % 189.69/189.73 (E(f2(a1,f2(a4,f2(f3(a4,a5),a1))),f2(a1,f2(a8,a1)))), % 189.69/189.73 inference(scs_inference,[],[805,2])). % 189.69/189.73 cnf(808,plain, % 189.69/189.73 (E(f2(a1,f2(a7,a1)),f2(a1,f2(f6(a5,f2(a4,a4)),f2(a4,a4))))), % 189.69/189.73 inference(scs_inference,[],[11,804,805,2,3])). % 189.69/189.73 cnf(810,plain, % 189.69/189.73 (E(f2(a1,f2(f6(a5,f2(a4,a4)),f2(a4,a4))),f2(a1,f2(a7,a1)))), % 189.69/189.73 inference(scs_inference,[],[808,2])). % 189.69/189.73 cnf(811,plain, % 189.69/189.73 (E(f2(a1,f3(x8111,f2(a4,x8111))),f2(a5,a1))), % 189.69/189.73 inference(scs_inference,[],[11,588,808,2,3])). % 189.69/189.73 cnf(813,plain, % 189.69/189.73 (E(f2(a5,a1),f2(a1,f3(x8131,f2(a4,x8131))))), % 189.69/189.73 inference(scs_inference,[],[811,2])). % 189.69/189.73 cnf(814,plain, % 189.69/189.73 (E(f2(a1,f3(x8141,f2(a4,x8141))),f2(f2(f6(a5,f2(a4,a4)),f2(a4,a4)),a1))), % 189.69/189.73 inference(scs_inference,[],[11,552,811,2,3])). % 189.69/189.73 cnf(816,plain, % 189.69/189.73 (E(f2(f2(f6(a5,f2(a4,a4)),f2(a4,a4)),a1),f2(a1,f3(x8161,f2(a4,x8161))))), % 189.69/189.73 inference(scs_inference,[],[814,2])). % 189.69/189.73 cnf(817,plain, % 189.69/189.73 (E(f2(a1,f2(a5,a1)),f2(a1,f3(x8171,f2(a4,x8171))))), % 189.69/189.73 inference(scs_inference,[],[11,813,814,2,3])). % 189.69/189.73 cnf(819,plain, % 189.69/189.73 (E(f2(a1,f3(x8191,f2(a4,x8191))),f2(a1,f2(a5,a1)))), % 189.69/189.73 inference(scs_inference,[],[817,2])). % 189.69/189.73 cnf(820,plain, % 189.69/189.73 (E(f2(a1,f2(f6(a4,f2(a1,x8201)),x8201)),f2(a4,a1))), % 189.69/189.73 inference(scs_inference,[],[11,633,817,2,3])). % 189.69/189.73 cnf(822,plain, % 189.69/189.73 (E(f2(a4,a1),f2(a1,f2(f6(a4,f2(a1,x8221)),x8221)))), % 189.69/189.73 inference(scs_inference,[],[820,2])). % 189.69/189.73 cnf(823,plain, % 189.69/189.73 (E(f2(a1,f2(a1,f3(x8231,f2(a4,x8231)))),f2(a1,f2(a5,a1)))), % 189.69/189.73 inference(scs_inference,[],[11,819,820,2,3])). % 189.69/189.73 cnf(826,plain, % 189.69/189.73 (E(f2(a1,f2(a4,a1)),f2(a1,f2(f6(a4,f2(a1,x8261)),x8261)))), % 189.69/189.73 inference(scs_inference,[],[11,822,823,2,3])). % 189.69/189.73 cnf(828,plain, % 189.69/189.73 (E(f2(a1,f2(f6(a4,f2(a1,x8281)),x8281)),f2(a1,f2(a4,a1)))), % 189.69/189.73 inference(scs_inference,[],[826,2])). % 189.69/189.73 cnf(829,plain, % 189.69/189.73 (E(f2(a1,f2(f6(a5,f2(a4,a4)),f2(a4,a4))),f2(x8291,f3(f2(a1,x8291),a4)))), % 189.69/189.73 inference(scs_inference,[],[11,307,826,2,3])). % 189.69/189.73 cnf(831,plain, % 189.69/189.73 (E(f2(x8311,f3(f2(a1,x8311),a4)),f2(a1,f2(f6(a5,f2(a4,a4)),f2(a4,a4))))), % 189.69/189.73 inference(scs_inference,[],[829,2])). % 189.69/189.73 cnf(832,plain, % 189.69/189.73 (E(f2(a1,f2(f2(a7,a1),a1)),f2(f2(f2(a5,a1),a1),a1))), % 189.69/189.73 inference(scs_inference,[],[11,432,829,2,3])). % 189.69/189.73 cnf(834,plain, % 189.69/189.73 (E(f2(f2(f2(a5,a1),a1),a1),f2(a1,f2(f2(a7,a1),a1)))), % 189.69/189.73 inference(scs_inference,[],[832,2])). % 189.69/189.73 cnf(835,plain, % 189.69/189.73 (E(f2(a1,f2(f6(a4,f2(x8351,a4)),f2(a4,x8351))),f2(a7,a1))), % 189.69/189.73 inference(scs_inference,[],[11,486,832,2,3])). % 189.69/189.73 cnf(837,plain, % 189.69/189.73 (E(f2(a7,a1),f2(a1,f2(f6(a4,f2(x8371,a4)),f2(a4,x8371))))), % 189.69/189.73 inference(scs_inference,[],[835,2])). % 189.69/189.73 cnf(838,plain, % 189.69/189.73 (E(f2(a1,f2(f6(a4,f2(x8381,a4)),f2(a4,x8381))),f2(a5,a1))), % 189.69/189.73 inference(scs_inference,[],[11,648,835,2,3])). % 189.69/189.73 cnf(840,plain, % 189.69/189.73 (E(f2(a5,a1),f2(a1,f2(f6(a4,f2(x8401,a4)),f2(a4,x8401))))), % 189.69/189.73 inference(scs_inference,[],[838,2])). % 189.69/189.73 cnf(841,plain, % 189.69/189.73 (E(f2(a1,f2(a7,a1)),f2(a1,f2(f6(a4,f2(x8411,a4)),f2(a4,x8411))))), % 189.69/189.73 inference(scs_inference,[],[11,837,838,2,3])). % 189.69/189.73 cnf(843,plain, % 189.69/189.73 (E(f2(a1,f2(f6(a4,f2(x8431,a4)),f2(a4,x8431))),f2(a1,f2(a7,a1)))), % 189.69/189.73 inference(scs_inference,[],[841,2])). % 189.69/189.73 cnf(844,plain, % 189.69/189.73 (E(f2(a1,f2(a5,a1)),f2(a1,f2(f6(a4,f2(x8441,a4)),f2(a4,x8441))))), % 189.69/189.73 inference(scs_inference,[],[11,840,841,2,3])). % 189.69/189.73 cnf(846,plain, % 189.69/189.73 (E(f2(a1,f2(f6(a4,f2(x8461,a4)),f2(a4,x8461))),f2(a1,f2(a5,a1)))), % 189.69/189.73 inference(scs_inference,[],[844,2])). % 189.69/189.73 cnf(847,plain, % 189.69/189.73 (E(f2(a1,f6(a4,f2(a1,a1))),f2(a8,a1))), % 189.69/189.73 inference(scs_inference,[],[11,417,844,2,3])). % 189.69/189.73 cnf(849,plain, % 189.69/189.73 (E(f2(a8,a1),f2(a1,f6(a4,f2(a1,a1))))), % 189.69/189.73 inference(scs_inference,[],[847,2])). % 189.69/189.73 cnf(850,plain, % 189.69/189.73 (E(f2(a1,f2(f3(x8501,f2(a4,x8501)),a1)),f2(a8,a1))), % 189.69/189.73 inference(scs_inference,[],[11,597,847,2,3])). % 189.69/189.73 cnf(852,plain, % 189.69/189.73 (E(f2(a8,a1),f2(a1,f2(f3(x8521,f2(a4,x8521)),a1)))), % 189.69/189.73 inference(scs_inference,[],[850,2])). % 189.69/189.73 cnf(853,plain, % 189.69/189.73 (E(f2(a1,f2(a8,a1)),f2(a1,f6(a4,f2(a1,a1))))), % 189.69/189.73 inference(scs_inference,[],[11,849,850,2,3])). % 189.69/189.73 cnf(855,plain, % 189.69/189.73 (E(f2(a1,f6(a4,f2(a1,a1))),f2(a1,f2(a8,a1)))), % 189.69/189.73 inference(scs_inference,[],[853,2])). % 189.69/189.73 cnf(856,plain, % 189.69/189.73 (E(f2(a1,f2(a8,a1)),f2(a1,f2(f3(x8561,f2(a4,x8561)),a1)))), % 189.69/189.73 inference(scs_inference,[],[11,852,853,2,3])). % 189.69/189.73 cnf(858,plain, % 189.69/189.73 (E(f2(a1,f2(f3(x8581,f2(a4,x8581)),a1)),f2(a1,f2(a8,a1)))), % 189.69/189.73 inference(scs_inference,[],[856,2])). % 189.69/189.73 cnf(859,plain, % 189.69/189.73 (E(f2(a1,f2(a1,f6(a4,f2(a1,a1)))),f2(a1,f2(a8,a1)))), % 189.69/189.73 inference(scs_inference,[],[11,855,856,2,3])). % 189.69/189.73 cnf(861,plain, % 189.69/189.73 (E(f2(a1,f2(a8,a1)),f2(a1,f2(a1,f6(a4,f2(a1,a1)))))), % 189.69/189.73 inference(scs_inference,[],[859,2])). % 189.69/189.73 cnf(862,plain, % 189.69/189.73 (E(f2(a1,f2(f3(x8621,f2(a4,x8621)),a1)),f2(a7,a1))), % 189.69/189.73 inference(scs_inference,[],[11,618,859,2,3])). % 189.69/189.73 cnf(864,plain, % 189.69/189.73 (E(f2(a7,a1),f2(a1,f2(f3(x8641,f2(a4,x8641)),a1)))), % 189.69/189.73 inference(scs_inference,[],[862,2])). % 189.69/189.73 cnf(865,plain, % 189.69/189.73 (E(f2(a1,f2(f3(x8651,f2(a4,x8651)),a1)),f2(f2(a5,a1),a1))), % 189.69/189.73 inference(scs_inference,[],[11,600,862,2,3])). % 189.69/189.73 cnf(867,plain, % 189.69/189.73 (E(f2(f2(a5,a1),a1),f2(a1,f2(f3(x8671,f2(a4,x8671)),a1)))), % 189.69/189.73 inference(scs_inference,[],[865,2])). % 189.69/189.73 cnf(868,plain, % 189.69/189.73 (E(f2(a1,f2(a7,a1)),f2(a1,f2(f3(x8681,f2(a4,x8681)),a1)))), % 189.69/189.73 inference(scs_inference,[],[11,864,865,2,3])). % 189.69/189.73 cnf(871,plain, % 189.69/189.73 (E(f2(a1,f2(a5,a1)),f2(f3(x8711,f2(a4,x8711)),a1))), % 189.69/189.73 inference(scs_inference,[],[11,594,868,2,3])). % 189.69/189.73 cnf(873,plain, % 189.69/189.73 (E(f2(f3(x8731,f2(a4,x8731)),a1),f2(a1,f2(a5,a1)))), % 189.69/189.73 inference(scs_inference,[],[871,2])). % 189.69/189.73 cnf(874,plain, % 189.69/189.73 (E(f2(a1,f2(a7,a1)),f2(f2(x8741,f3(f2(a1,x8741),a4)),a1))), % 189.69/189.73 inference(scs_inference,[],[11,621,871,2,3])). % 189.69/189.73 cnf(876,plain, % 189.69/189.73 (E(f2(f2(x8761,f3(f2(a1,x8761),a4)),a1),f2(a1,f2(a7,a1)))), % 189.69/189.73 inference(scs_inference,[],[874,2])). % 189.69/189.73 cnf(877,plain, % 189.69/189.73 (E(f2(a1,f2(f3(x8771,f2(a4,x8771)),a1)),f2(a1,f2(a5,a1)))), % 189.69/189.73 inference(scs_inference,[],[11,873,874,2,3])). % 189.69/189.73 cnf(879,plain, % 189.69/189.73 (E(f2(a1,f2(a5,a1)),f2(a1,f2(f3(x8791,f2(a4,x8791)),a1)))), % 189.69/189.73 inference(scs_inference,[],[877,2])). % 189.69/189.73 cnf(880,plain, % 189.69/189.73 (E(f2(a1,f2(a4,a1)),f2(f2(f6(a4,f2(a1,x8801)),x8801),a1))), % 189.69/189.73 inference(scs_inference,[],[11,639,877,2,3])). % 189.69/189.73 cnf(882,plain, % 189.69/189.73 (E(f2(f2(f6(a4,f2(a1,x8821)),x8821),a1),f2(a1,f2(a4,a1)))), % 189.69/189.73 inference(scs_inference,[],[880,2])). % 189.69/189.73 cnf(883,plain, % 189.69/189.73 (E(f2(a1,f2(a7,a1)),f2(f2(f6(a4,f2(x8831,a4)),f2(a4,x8831)),a1))), % 189.69/189.73 inference(scs_inference,[],[11,492,880,2,3])). % 189.69/189.73 cnf(885,plain, % 189.69/189.73 (E(f2(f2(f6(a4,f2(x8851,a4)),f2(a4,x8851)),a1),f2(a1,f2(a7,a1)))), % 189.69/189.73 inference(scs_inference,[],[883,2])). % 189.69/189.73 cnf(886,plain, % 189.69/189.73 (E(f2(a1,f2(f2(f6(a4,f2(x8861,a4)),f2(a4,x8861)),a1)),f2(a4,a1))), % 189.69/189.73 inference(scs_inference,[],[11,489,883,2,3])). % 189.69/189.73 cnf(889,plain, % 189.69/189.73 (E(f2(a1,f2(a8,a1)),f2(f2(f3(x8891,f2(a4,x8891)),a1),a1))), % 189.69/189.73 inference(scs_inference,[],[11,603,886,2,3])). % 189.69/189.73 cnf(892,plain, % 189.69/189.73 (E(f2(a1,f2(a7,a1)),f2(f2(f3(x8921,f2(a4,x8921)),a1),a1))), % 189.69/189.73 inference(scs_inference,[],[11,624,889,2,3])). % 189.69/189.73 cnf(895,plain, % 189.69/189.73 (E(f2(a1,f2(x8951,f3(f2(a1,x8951),a4))),f2(a5,a1))), % 189.69/189.73 inference(scs_inference,[],[11,333,892,2,3])). % 189.69/189.73 cnf(897,plain, % 189.69/189.73 (E(f2(a5,a1),f2(a1,f2(x8971,f3(f2(a1,x8971),a4))))), % 189.69/189.73 inference(scs_inference,[],[895,2])). % 189.69/189.73 cnf(898,plain, % 189.69/189.73 (E(f2(a1,f2(a5,a1)),f2(f2(x8981,f3(f2(a1,x8981),a4)),a1))), % 189.69/189.73 inference(scs_inference,[],[11,336,895,2,3])). % 189.69/189.73 cnf(900,plain, % 189.69/189.73 (E(f2(f2(x9001,f3(f2(a1,x9001),a4)),a1),f2(a1,f2(a5,a1)))), % 189.69/189.73 inference(scs_inference,[],[898,2])). % 189.69/189.73 cnf(901,plain, % 189.69/189.73 (E(f2(a1,f2(a5,a1)),f2(a1,f2(x9011,f3(f2(a1,x9011),a4))))), % 189.69/189.73 inference(scs_inference,[],[11,897,898,2,3])). % 189.69/189.73 cnf(903,plain, % 189.69/189.73 (E(f2(a1,f2(x9031,f3(f2(a1,x9031),a4))),f2(a1,f2(a5,a1)))), % 189.69/189.73 inference(scs_inference,[],[901,2])). % 189.69/189.73 cnf(904,plain, % 189.69/189.73 (E(f2(a1,f2(f6(a4,f2(x9041,a4)),f2(a4,x9041))),f2(f3(x9042,f2(a4,x9042)),a1))), % 189.69/189.73 inference(scs_inference,[],[11,456,901,2,3])). % 189.69/189.73 cnf(907,plain, % 189.69/189.73 (E(f2(a1,f6(a4,f2(a1,a1))),f2(f3(x9071,f2(a4,x9071)),a1))), % 189.69/189.73 inference(scs_inference,[],[11,567,904,2,3])). % 189.69/189.73 cnf(909,plain, % 189.69/189.73 (E(f2(f3(x9091,f2(a4,x9091)),a1),f2(a1,f6(a4,f2(a1,a1))))), % 189.69/189.73 inference(scs_inference,[],[907,2])). % 189.69/189.73 cnf(910,plain, % 189.69/189.73 (E(f2(a1,f6(a4,f2(a1,a1))),f2(f2(f6(a4,f2(x9101,a4)),f2(a4,x9101)),a1))), % 189.69/189.73 inference(scs_inference,[],[11,579,907,2,3])). % 189.69/189.73 cnf(912,plain, % 189.69/189.73 (E(f2(f2(f6(a4,f2(x9121,a4)),f2(a4,x9121)),a1),f2(a1,f6(a4,f2(a1,a1))))), % 189.69/189.73 inference(scs_inference,[],[910,2])). % 189.69/189.73 cnf(913,plain, % 189.69/189.73 (E(f2(a1,f2(f2(x9131,x9132),a4)),f2(f2(x9131,f2(x9132,a4)),a1))), % 189.69/189.73 inference(scs_inference,[],[11,570,910,2,3])). % 189.69/189.73 cnf(916,plain, % 189.69/189.73 (E(f2(a1,a4),f2(a7,a1))), % 189.69/189.73 inference(scs_inference,[],[11,510,913,2,3])). % 189.69/189.73 cnf(918,plain, % 189.69/189.73 (E(f2(a7,a1),f2(a1,a4))), % 189.69/189.73 inference(scs_inference,[],[916,2])). % 189.69/189.73 cnf(919,plain, % 189.69/189.73 (E(f2(a1,a8),f2(f2(a4,f2(f3(a4,a4),a1)),a1))), % 189.69/189.73 inference(scs_inference,[],[11,543,916,2,3])). % 189.69/189.73 cnf(921,plain, % 189.69/189.73 (E(f2(f2(a4,f2(f3(a4,a4),a1)),a1),f2(a1,a8))), % 189.69/189.73 inference(scs_inference,[],[919,2])). % 189.69/189.73 cnf(922,plain, % 189.69/189.73 (E(f2(a1,f2(a7,a1)),f2(a1,a4))), % 189.69/189.73 inference(scs_inference,[],[11,918,919,2,3])). % 189.69/189.73 cnf(924,plain, % 189.69/189.73 (E(f2(a1,a4),f2(a1,f2(a7,a1)))), % 189.69/189.73 inference(scs_inference,[],[922,2])). % 189.69/189.73 cnf(925,plain, % 189.69/189.73 (E(f2(a1,a5),f2(f2(a4,f2(f3(a4,a4),a1)),a1))), % 189.69/189.73 inference(scs_inference,[],[11,531,922,2,3])). % 189.69/189.73 cnf(927,plain, % 189.69/189.73 (E(f2(f2(a4,f2(f3(a4,a4),a1)),a1),f2(a1,a5))), % 189.69/189.73 inference(scs_inference,[],[925,2])). % 189.69/189.73 cnf(928,plain, % 189.69/189.73 (E(f2(a1,f2(a1,a4)),f2(a1,f2(a7,a1)))), % 189.69/189.73 inference(scs_inference,[],[11,924,925,2,3])). % 189.69/189.73 cnf(930,plain, % 189.69/189.73 (E(f2(a1,f2(a7,a1)),f2(a1,f2(a1,a4)))), % 189.69/189.73 inference(scs_inference,[],[928,2])). % 189.69/189.73 cnf(931,plain, % 189.69/189.73 (E(f2(a1,a7),f2(a5,a1))), % 189.69/189.73 inference(scs_inference,[],[11,408,928,2,3])). % 189.69/189.73 cnf(933,plain, % 189.69/189.73 (E(f2(a5,a1),f2(a1,a7))), % 189.69/189.73 inference(scs_inference,[],[931,2])). % 189.69/189.73 cnf(934,plain, % 189.69/189.73 (E(f2(a1,f2(a1,f2(a7,a1))),f2(a1,f2(a1,a4)))), % 189.69/189.73 inference(scs_inference,[],[11,930,931,2,3])). % 189.69/189.73 cnf(936,plain, % 189.69/189.73 (E(f2(a1,f2(a1,a4)),f2(a1,f2(a1,f2(a7,a1))))), % 189.69/189.73 inference(scs_inference,[],[934,2])). % 189.69/189.73 cnf(937,plain, % 189.69/189.73 (E(f2(a1,f2(a5,a1)),f2(a1,a7))), % 189.69/189.73 inference(scs_inference,[],[11,933,934,2,3])). % 189.69/189.73 cnf(939,plain, % 189.69/189.73 (E(f2(a1,a7),f2(a1,f2(a5,a1)))), % 189.69/189.73 inference(scs_inference,[],[937,2])). % 189.69/189.73 cnf(940,plain, % 189.69/189.73 (E(f2(a1,f2(a1,f2(a1,a4))),f2(a1,f2(a1,f2(a7,a1))))), % 189.69/189.73 inference(scs_inference,[],[11,936,937,2,3])). % 189.69/189.73 cnf(942,plain, % 189.69/189.73 (E(f2(a1,f2(a1,f2(a7,a1))),f2(a1,f2(a1,f2(a1,a4))))), % 189.69/189.73 inference(scs_inference,[],[940,2])). % 189.69/189.73 cnf(943,plain, % 189.69/189.73 (E(f2(a1,f2(a1,a7)),f2(a1,f2(a5,a1)))), % 189.69/189.73 inference(scs_inference,[],[11,939,940,2,3])). % 189.69/189.73 cnf(945,plain, % 189.69/189.73 (E(f2(a1,f2(a5,a1)),f2(a1,f2(a1,a7)))), % 189.69/189.73 inference(scs_inference,[],[943,2])). % 189.69/189.73 cnf(946,plain, % 189.69/189.73 (E(f2(a1,a8),f2(f2(f6(a4,f2(x9461,x9462)),x9462),x9461))), % 189.69/189.73 inference(scs_inference,[],[11,287,943,2,3])). % 189.69/189.73 cnf(948,plain, % 189.69/189.73 (E(f2(f2(f6(a4,f2(x9481,x9482)),x9482),x9481),f2(a1,a8))), % 189.69/189.73 inference(scs_inference,[],[946,2])). % 189.69/189.73 cnf(949,plain, % 189.69/189.73 (E(f2(a1,f2(a1,f2(a5,a1))),f2(a1,f2(a1,a7)))), % 189.69/189.73 inference(scs_inference,[],[11,945,946,2,3])). % 189.69/189.73 cnf(951,plain, % 189.69/189.73 (E(f2(a1,f2(a1,a7)),f2(a1,f2(a1,f2(a5,a1))))), % 189.69/189.73 inference(scs_inference,[],[949,2])). % 189.69/189.73 cnf(952,plain, % 189.69/189.73 (E(f2(a1,a5),f2(x9521,f3(f2(a1,x9521),a4)))), % 189.69/189.73 inference(scs_inference,[],[11,295,949,2,3])). % 189.69/189.73 cnf(954,plain, % 189.69/189.73 (E(f2(x9541,f3(f2(a1,x9541),a4)),f2(a1,a5))), % 189.69/189.73 inference(scs_inference,[],[952,2])). % 189.69/189.73 cnf(955,plain, % 189.69/189.73 (E(f2(a1,f2(a1,f2(a1,a7))),f2(a1,f2(a1,f2(a5,a1))))), % 189.69/189.73 inference(scs_inference,[],[11,951,952,2,3])). % 189.69/189.73 cnf(957,plain, % 189.69/189.73 (E(f2(a1,f2(a1,f2(a5,a1))),f2(a1,f2(a1,f2(a1,a7))))), % 189.69/189.73 inference(scs_inference,[],[955,2])). % 189.69/189.73 cnf(958,plain, % 189.69/189.73 (E(f2(a1,f2(x9581,f3(f2(a1,x9581),a4))),f2(a1,a5))), % 189.69/189.73 inference(scs_inference,[],[11,954,955,2,3])). % 189.69/189.73 cnf(960,plain, % 189.69/189.73 (E(f2(a1,a5),f2(a1,f2(x9601,f3(f2(a1,x9601),a4))))), % 189.69/189.73 inference(scs_inference,[],[958,2])). % 189.69/189.73 cnf(961,plain, % 189.69/189.73 (E(f2(a1,f2(f6(a4,f2(a1,x9611)),x9611)),a7)), % 189.69/189.73 inference(scs_inference,[],[11,312,958,2,3])). % 189.69/189.73 cnf(963,plain, % 189.69/189.73 (E(a7,f2(a1,f2(f6(a4,f2(a1,x9631)),x9631)))), % 189.69/189.73 inference(scs_inference,[],[961,2])). % 189.69/189.73 cnf(964,plain, % 189.69/189.73 (E(f2(a1,f2(a1,a5)),f2(a1,f2(x9641,f3(f2(a1,x9641),a4))))), % 189.69/189.73 inference(scs_inference,[],[11,960,961,2,3])). % 189.69/189.73 cnf(967,plain, % 189.69/189.73 (E(f2(a1,a7),f2(a1,f2(f6(a4,f2(a1,x9671)),x9671)))), % 189.69/189.73 inference(scs_inference,[],[11,963,964,2,3])). % 189.69/189.73 cnf(969,plain, % 189.69/189.73 (E(f2(a1,f2(f6(a4,f2(a1,x9691)),x9691)),f2(a1,a7))), % 189.69/189.73 inference(scs_inference,[],[967,2])). % 189.69/189.73 cnf(970,plain, % 189.69/189.73 (E(f2(a1,a7),f2(f2(a4,f2(f3(a4,a4),a1)),a1))), % 189.69/189.73 inference(scs_inference,[],[11,441,967,2,3])). % 189.69/189.73 cnf(972,plain, % 189.69/189.73 (E(f2(f2(a4,f2(f3(a4,a4),a1)),a1),f2(a1,a7))), % 189.69/189.73 inference(scs_inference,[],[970,2])). % 189.69/189.73 cnf(973,plain, % 189.69/189.73 (E(f2(a1,a5),f2(f2(f6(f6(f2(a8,x9731),x9731),f2(x9732,a4)),x9732),a4))), % 189.69/189.73 inference(scs_inference,[],[11,105,970,2,3])). % 189.69/189.73 cnf(976,plain, % 189.69/189.73 (E(f2(a1,a8),f2(f2(f6(f6(f2(a5,x9761),x9761),f2(x9762,a4)),x9762),a4))), % 189.69/189.73 inference(scs_inference,[],[11,161,973,2,3])). % 189.69/189.73 cnf(978,plain, % 189.69/189.73 (E(f2(f2(f6(f6(f2(a5,x9781),x9781),f2(x9782,a4)),x9782),a4),f2(a1,a8))), % 189.69/189.73 inference(scs_inference,[],[976,2])). % 189.69/189.73 cnf(979,plain, % 189.69/189.73 (E(f2(a1,a8),f2(f3(x9791,f2(a4,x9791)),a1))), % 189.69/189.73 inference(scs_inference,[],[11,591,976,2,3])). % 189.69/189.73 cnf(981,plain, % 189.69/189.73 (E(f2(f3(x9811,f2(a4,x9811)),a1),f2(a1,a8))), % 189.69/189.73 inference(scs_inference,[],[979,2])). % 189.69/189.73 cnf(982,plain, % 189.69/189.73 (E(f2(a1,a7),f2(f3(x9821,f2(a4,x9821)),a1))), % 189.69/189.73 inference(scs_inference,[],[11,612,979,2,3])). % 189.69/189.73 cnf(984,plain, % 189.69/189.73 (E(f2(f3(x9841,f2(a4,x9841)),a1),f2(a1,a7))), % 189.69/189.73 inference(scs_inference,[],[982,2])). % 189.69/189.73 cnf(985,plain, % 189.69/189.73 (E(f2(a1,f2(f3(x9851,f2(a4,x9851)),a1)),f2(a1,a8))), % 189.69/189.73 inference(scs_inference,[],[11,981,982,2,3])). % 189.69/189.73 cnf(987,plain, % 189.69/189.73 (E(f2(a1,a8),f2(a1,f2(f3(x9871,f2(a4,x9871)),a1)))), % 189.69/189.73 inference(scs_inference,[],[985,2])). % 189.69/189.73 cnf(988,plain, % 189.69/189.73 (E(f2(a1,f2(f3(x9881,f2(a4,x9881)),a1)),f2(a1,a7))), % 189.69/189.73 inference(scs_inference,[],[11,984,985,2,3])). % 189.69/189.73 cnf(990,plain, % 189.69/189.73 (E(f2(a1,a7),f2(a1,f2(f3(x9901,f2(a4,x9901)),a1)))), % 189.69/189.73 inference(scs_inference,[],[988,2])). % 189.69/189.73 cnf(991,plain, % 189.69/189.73 (E(f2(a1,f2(a1,a8)),f2(a1,f2(f3(x9911,f2(a4,x9911)),a1)))), % 189.69/189.73 inference(scs_inference,[],[11,987,988,2,3])). % 189.69/189.73 cnf(993,plain, % 189.69/189.73 (E(f2(a1,f2(f3(x9931,f2(a4,x9931)),a1)),f2(a1,f2(a1,a8)))), % 189.69/189.73 inference(scs_inference,[],[991,2])). % 189.69/189.73 cnf(994,plain, % 189.69/189.73 (E(f2(a8,f2(a1,f2(a1,a1))),f2(f2(f2(a7,a1),a1),a1))), % 189.69/189.73 inference(scs_inference,[],[92,375,991,2,3])). % 189.69/189.73 cnf(996,plain, % 189.69/189.73 (E(f2(f2(f2(a7,a1),a1),a1),f2(a8,f2(a1,f2(a1,a1))))), % 189.69/189.73 inference(scs_inference,[],[994,2])). % 189.69/189.73 cnf(997,plain, % 189.69/189.73 (E(f3(x9971,f2(a4,x9971)),f2(f2(a7,a1),a1))), % 189.69/189.73 inference(scs_inference,[],[519,555,994,2,3])). % 189.69/189.73 cnf(998,plain, % 189.69/189.73 (E(f2(f2(a7,a1),a1),f3(x9981,f2(a4,x9981)))), % 189.69/189.73 inference(scs_inference,[],[997,2])). % 189.69/189.73 cnf(999,plain, % 189.69/189.73 (E(f2(a5,f2(a1,f2(a1,a1))),f2(a1,f2(f2(a7,a1),a1)))), % 189.69/189.73 inference(scs_inference,[],[834,92,997,2,3])). % 189.69/189.73 cnf(1002,plain, % 189.69/189.73 (E(f2(f2(a7,a1),a1),a5)), % 189.69/189.73 inference(scs_inference,[],[12,998,999,2,3])). % 189.69/189.73 cnf(1004,plain, % 189.69/189.73 (E(a5,f2(f2(a7,a1),a1))), % 189.69/189.73 inference(scs_inference,[],[1002,2])). % 189.69/189.73 cnf(1005,plain, % 189.69/189.73 (E(f6(a4,f2(a1,a1)),f2(a1,f2(a8,a1)))), % 189.69/189.73 inference(scs_inference,[],[753,525,1002,2,3])). % 189.69/189.73 cnf(1006,plain, % 189.69/189.73 (E(f2(a1,f2(a8,a1)),f6(a4,f2(a1,a1)))), % 189.69/189.73 inference(scs_inference,[],[1005,2])). % 189.69/189.73 cnf(1007,plain, % 189.69/189.73 (E(f2(a4,f2(f2(f3(a4,a4),a1),a1)),f2(a8,a1))), % 189.69/189.73 inference(scs_inference,[],[549,315,1005,2,3])). % 189.69/189.73 cnf(1009,plain, % 189.69/189.73 (E(f2(a8,a1),f2(a4,f2(f2(f3(a4,a4),a1),a1)))), % 189.69/189.73 inference(scs_inference,[],[1007,2])). % 189.69/189.73 cnf(1010,plain, % 189.69/189.73 (E(f2(a4,f2(f2(f3(a4,a4),a1),a1)),f2(a5,a1))), % 189.69/189.73 inference(scs_inference,[],[537,315,1007,2,3])). % 189.69/189.73 cnf(1012,plain, % 189.69/189.73 (E(f2(a5,a1),f2(a4,f2(f2(f3(a4,a4),a1),a1)))), % 189.69/189.73 inference(scs_inference,[],[1010,2])). % 189.69/189.73 cnf(1013,plain, % 189.69/189.73 (E(f2(x10131,f3(f2(a1,x10131),a4)),f2(a1,f2(a7,a1)))), % 189.69/189.73 inference(scs_inference,[],[810,831,1010,2,3])). % 189.69/189.73 cnf(1014,plain, % 189.69/189.73 (E(f2(a1,f2(a7,a1)),f2(x10141,f3(f2(a1,x10141),a4)))), % 189.69/189.73 inference(scs_inference,[],[1013,2])). % 189.69/189.73 cnf(1015,plain, % 189.69/189.73 (E(f2(a8,a1),f2(a1,f2(a7,a1)))), % 189.69/189.73 inference(scs_inference,[],[795,801,1013,2,3])). % 189.69/189.73 cnf(1016,plain, % 189.69/189.73 (E(f2(a1,f2(a7,a1)),f2(a8,a1))), % 189.69/189.73 inference(scs_inference,[],[1015,2])). % 189.69/189.73 cnf(1017,plain, % 189.69/189.73 (E(f2(f2(a7,a1),a1),f2(a1,f2(a1,f2(a7,a1))))), % 189.69/189.73 inference(scs_inference,[],[786,792,1015,2,3])). % 189.69/189.73 cnf(1018,plain, % 189.69/189.73 (E(f2(a1,f2(a1,f2(a7,a1))),f2(f2(a7,a1),a1))), % 189.69/189.73 inference(scs_inference,[],[1017,2])). % 189.69/189.73 cnf(1019,plain, % 189.69/189.73 (E(f2(a1,f2(a7,a1)),f2(a1,f2(f2(a7,a1),a1)))), % 189.69/189.73 inference(scs_inference,[],[798,780,1017,2,3])). % 189.69/189.73 cnf(1020,plain, % 189.69/189.73 (E(f2(a1,f2(f2(a7,a1),a1)),f2(a1,f2(a7,a1)))), % 189.69/189.73 inference(scs_inference,[],[1019,2])). % 189.69/189.73 cnf(1021,plain, % 189.69/189.74 (E(f2(a4,f2(f3(a4,a5),a1)),f2(a1,f2(a7,a1)))), % 189.69/189.74 inference(scs_inference,[],[759,387,1019,2,3])). % 189.69/189.74 cnf(1022,plain, % 189.69/189.74 (E(f2(a1,f2(a7,a1)),f2(a4,f2(f3(a4,a5),a1)))), % 189.69/189.74 inference(scs_inference,[],[1021,2])). % 189.69/189.74 cnf(1023,plain, % 189.69/189.74 (E(f2(a1,f2(f2(a7,a1),a1)),f2(a8,a1))), % 189.69/189.74 inference(scs_inference,[],[1016,1020,1021,2,3])). % 189.69/189.74 cnf(1024,plain, % 189.69/189.74 (E(f2(a8,a1),f2(a1,f2(f2(a7,a1),a1)))), % 189.69/189.74 inference(scs_inference,[],[1023,2])). % 189.69/189.74 cnf(1025,plain, % 189.69/189.74 (E(f2(a4,f2(f2(f3(a4,a4),a1),a1)),f2(a1,a7))), % 189.69/189.74 inference(scs_inference,[],[972,315,1023,2,3])). % 189.69/189.74 cnf(1027,plain, % 189.69/189.74 (E(f2(a1,a7),f2(a4,f2(f2(f3(a4,a4),a1),a1)))), % 189.69/189.74 inference(scs_inference,[],[1025,2])). % 189.69/189.74 cnf(1028,plain, % 189.69/189.74 (E(f3(x10281,f2(a4,x10281)),f2(f2(a8,a1),a1))), % 189.69/189.74 inference(scs_inference,[],[405,555,1025,2,3])). % 189.69/189.74 cnf(1029,plain, % 189.69/189.74 (E(f2(f2(a8,a1),a1),f3(x10291,f2(a4,x10291)))), % 189.69/189.74 inference(scs_inference,[],[1028,2])). % 189.69/189.74 cnf(1030,plain, % 189.69/189.74 (E(f6(a4,f2(a1,a1)),f2(a1,f2(a7,a1)))), % 189.69/189.74 inference(scs_inference,[],[714,525,1028,2,3])). % 189.69/189.74 cnf(1031,plain, % 189.69/189.74 (E(f2(a1,f2(a7,a1)),f6(a4,f2(a1,a1)))), % 189.69/189.74 inference(scs_inference,[],[1030,2])). % 189.69/189.74 cnf(1032,plain, % 189.69/189.74 (E(f2(f2(a8,a1),a1),a5)), % 189.69/189.74 inference(scs_inference,[],[12,1029,1030,2,3])). % 189.69/189.74 cnf(1034,plain, % 189.69/189.74 (E(a5,f2(f2(a8,a1),a1))), % 189.69/189.74 inference(scs_inference,[],[1032,2])). % 189.69/189.74 cnf(1035,plain, % 189.69/189.74 (E(f2(x10351,f3(f2(a1,x10351),a4)),f2(f2(a7,a1),a1))), % 189.69/189.74 inference(scs_inference,[],[402,327,1032,2,3])). % 189.69/189.74 cnf(1036,plain, % 189.69/189.74 (E(f2(f2(a7,a1),a1),f2(x10361,f3(f2(a1,x10361),a4)))), % 189.69/189.74 inference(scs_inference,[],[1035,2])). % 189.69/189.74 cnf(1037,plain, % 189.69/189.74 (E(f2(f2(a8,a1),a1),f2(a1,a8))), % 189.69/189.74 inference(scs_inference,[],[948,435,1035,2,3])). % 189.69/189.74 cnf(1039,plain, % 189.69/189.74 (E(f2(a1,a8),f2(f2(a8,a1),a1))), % 189.69/189.74 inference(scs_inference,[],[1037,2])). % 189.69/189.74 cnf(1040,plain, % 189.69/189.74 (E(f2(a8,f2(a1,f2(a1,a1))),f2(a1,f2(f2(a7,a1),a1)))), % 189.69/189.74 inference(scs_inference,[],[705,92,1037,2,3])). % 189.69/189.74 cnf(1042,plain, % 189.69/189.74 (E(f2(a1,f2(f2(a7,a1),a1)),f2(a8,f2(a1,f2(a1,a1))))), % 189.69/189.74 inference(scs_inference,[],[1040,2])). % 189.69/189.74 cnf(1043,plain, % 189.69/189.74 (E(f2(f2(a4,f2(f3(a4,a4),a1)),a1),f2(f2(a8,a1),a1))), % 189.69/189.74 inference(scs_inference,[],[1039,921,1040,2,3])). % 189.69/189.74 cnf(1044,plain, % 189.69/189.74 (E(f2(f2(a8,a1),a1),f2(f2(a4,f2(f3(a4,a4),a1)),a1))), % 189.69/189.74 inference(scs_inference,[],[1043,2])). % 189.69/189.74 cnf(1045,plain, % 189.69/189.74 (E(f2(a8,a1),f2(a1,f2(f2(a4,a1),a1)))), % 189.69/189.74 inference(scs_inference,[],[1024,768,1043,2,3])). % 189.69/189.74 cnf(1046,plain, % 189.69/189.74 (E(f2(a1,f2(f2(a4,a1),a1)),f2(a8,a1))), % 189.69/189.74 inference(scs_inference,[],[1045,2])). % 189.69/189.74 cnf(1047,plain, % 189.69/189.74 (E(f2(a1,f2(f2(a8,a1),a1)),f2(a8,f2(a1,f2(a1,a1))))), % 189.69/189.74 inference(scs_inference,[],[1042,702,1045,2,3])). % 189.69/189.74 cnf(1048,plain, % 189.69/189.74 (E(f2(a8,f2(a1,f2(a1,a1))),f2(a1,f2(f2(a8,a1),a1)))), % 189.69/189.74 inference(scs_inference,[],[1047,2])). % 189.69/189.74 cnf(1049,plain, % 189.69/189.74 (E(f2(f2(f2(a7,a1),a1),a1),f2(a8,a1))), % 189.69/189.74 inference(scs_inference,[],[1046,756,1047,2,3])). % 189.69/189.74 cnf(1050,plain, % 189.69/189.74 (E(f2(a8,a1),f2(f2(f2(a7,a1),a1),a1))), % 189.69/189.74 inference(scs_inference,[],[1049,2])). % 189.69/189.74 cnf(1051,plain, % 189.69/189.74 (E(f2(a8,f2(a1,f2(a1,a1))),f2(a1,f2(a1,f2(a7,a1))))), % 189.69/189.74 inference(scs_inference,[],[699,1048,1049,2,3])). % 189.69/189.74 cnf(1052,plain, % 189.69/189.74 (E(f2(a1,f2(a1,f2(a7,a1))),f2(a8,f2(a1,f2(a1,a1))))), % 189.69/189.74 inference(scs_inference,[],[1051,2])). % 189.69/189.74 cnf(1053,plain, % 189.69/189.74 (E(f2(a1,f2(a1,f2(a5,a1))),f2(f2(a7,a1),a1))), % 189.69/189.74 inference(scs_inference,[],[1018,783,1051,2,3])). % 189.69/189.74 cnf(1054,plain, % 189.69/189.74 (E(f2(f2(a7,a1),a1),f2(a1,f2(a1,f2(a5,a1))))), % 189.69/189.74 inference(scs_inference,[],[1053,2])). % 189.69/189.74 cnf(1055,plain, % 189.69/189.74 (E(f2(a1,f2(a1,f2(a8,a1))),f2(a8,f2(a1,f2(a1,a1))))), % 189.69/189.74 inference(scs_inference,[],[1052,681,1053,2,3])). % 189.69/189.74 cnf(1056,plain, % 189.69/189.74 (E(f2(a8,f2(a1,f2(a1,a1))),f2(a1,f2(a1,f2(a8,a1))))), % 189.69/189.74 inference(scs_inference,[],[1055,2])). % 189.69/189.74 cnf(1057,plain, % 189.69/189.74 (E(f2(f2(a7,a1),a1),f2(a1,f2(a1,f2(a1,a7))))), % 189.69/189.74 inference(scs_inference,[],[1054,957,1055,2,3])). % 189.69/189.74 cnf(1058,plain, % 189.69/189.74 (E(f2(a1,f2(a1,f2(a1,a7))),f2(f2(a7,a1),a1))), % 189.69/189.74 inference(scs_inference,[],[1057,2])). % 189.69/189.74 cnf(1059,plain, % 189.69/189.74 (E(f2(f2(f2(a7,a1),a1),a1),f2(a1,f2(a1,f2(a8,a1))))), % 189.69/189.74 inference(scs_inference,[],[1056,996,1057,2,3])). % 189.69/189.74 cnf(1060,plain, % 189.69/189.74 (E(f2(a1,f2(a1,f2(a8,a1))),f2(f2(f2(a7,a1),a1),a1))), % 189.69/189.74 inference(scs_inference,[],[1059,2])). % 189.69/189.74 cnf(1061,plain, % 189.69/189.74 (E(f2(a1,f2(a1,f2(a8,a1))),f2(f2(a7,a1),a1))), % 189.69/189.74 inference(scs_inference,[],[1058,690,1059,2,3])). % 189.69/189.74 cnf(1062,plain, % 189.69/189.74 (E(f2(f2(a7,a1),a1),f2(a1,f2(a1,f2(a8,a1))))), % 189.69/189.74 inference(scs_inference,[],[1061,2])). % 189.69/189.74 cnf(1063,plain, % 189.69/189.74 (E(f2(a1,f2(f2(a5,a1),a1)),f2(a1,f2(a1,f2(a4,a1))))), % 189.69/189.74 inference(scs_inference,[],[741,786,1061,2,3])). % 189.69/189.74 cnf(1065,plain, % 189.69/189.74 (E(f2(a8,a1),f2(f2(f2(a4,a1),a1),a1))), % 189.69/189.74 inference(scs_inference,[],[1050,540,1063,2,3])). % 189.69/189.74 cnf(1066,plain, % 189.69/189.74 (E(f2(f2(f2(a4,a1),a1),a1),f2(a8,a1))), % 189.69/189.74 inference(scs_inference,[],[1065,2])). % 189.69/189.74 cnf(1067,plain, % 189.69/189.74 (E(f2(a8,a1),f2(a1,f2(a1,f2(a4,a1))))), % 189.69/189.74 inference(scs_inference,[],[738,1024,1065,2,3])). % 189.69/189.74 cnf(1068,plain, % 189.69/189.74 (E(f2(a1,f2(a1,f2(a4,a1))),f2(a8,a1))), % 189.69/189.74 inference(scs_inference,[],[1067,2])). % 189.69/189.74 cnf(1069,plain, % 189.69/189.74 (E(f2(a1,f2(a4,a1)),f2(a1,f2(a1,f2(a1,a4))))), % 189.69/189.74 inference(scs_inference,[],[942,735,1067,2,3])). % 189.69/189.74 cnf(1070,plain, % 189.69/189.74 (E(f2(a1,f2(a1,f2(a1,a4))),f2(a1,f2(a4,a1)))), % 189.69/189.74 inference(scs_inference,[],[1069,2])). % 189.69/189.74 cnf(1071,plain, % 189.69/189.74 (E(f2(a1,f2(a1,f2(a7,a1))),f2(a8,a1))), % 189.69/189.74 inference(scs_inference,[],[1068,741,1069,2,3])). % 189.69/189.74 cnf(1072,plain, % 189.69/189.74 (E(f2(a8,a1),f2(a1,f2(a1,f2(a7,a1))))), % 189.69/189.74 inference(scs_inference,[],[1071,2])). % 189.69/189.74 cnf(1073,plain, % 189.69/189.74 (E(f6(a4,f2(a1,a1)),f2(a7,a1))), % 189.69/189.74 inference(scs_inference,[],[444,204,1071,2,3])). % 189.69/189.74 cnf(1074,plain, % 189.69/189.74 (E(f2(a7,a1),f6(a4,f2(a1,a1)))), % 189.69/189.74 inference(scs_inference,[],[1073,2])). % 189.69/189.74 cnf(1075,plain, % 189.69/189.74 (E(f2(f2(f2(a4,a1),a1),a1),f2(a1,f2(a1,f2(a7,a1))))), % 189.69/189.74 inference(scs_inference,[],[1072,1066,1073,2,3])). % 189.69/189.74 cnf(1077,plain, % 189.69/189.74 (E(f2(a1,f2(a4,f2(f3(a4,a5),a1))),f6(a4,f2(a1,a1)))), % 189.69/189.74 inference(scs_inference,[],[807,1006,1075,2,3])). % 189.69/189.74 cnf(1078,plain, % 189.69/189.74 (E(f6(a4,f2(a1,a1)),f2(a1,f2(a4,f2(f3(a4,a5),a1))))), % 189.69/189.74 inference(scs_inference,[],[1077,2])). % 189.69/189.74 cnf(1079,plain, % 189.69/189.74 (E(f2(x10791,f2(x10792,f3(f2(x10791,x10792),a4))),f6(a4,f2(a1,a1)))), % 189.69/189.74 inference(scs_inference,[],[582,1074,1077,2,3])). % 189.69/189.74 cnf(1080,plain, % 189.69/189.74 (E(f6(a4,f2(a1,a1)),f2(x10801,f2(x10802,f3(f2(x10801,x10802),a4))))), % 189.69/189.74 inference(scs_inference,[],[1079,2])). % 189.69/189.74 cnf(1081,plain, % 189.69/189.74 (E(f6(a4,f2(a1,a1)),f2(a4,a1))), % 189.69/189.74 inference(scs_inference,[],[411,204,1079,2,3])). % 189.69/189.74 cnf(1082,plain, % 189.69/189.74 (E(f2(a4,a1),f6(a4,f2(a1,a1)))), % 189.69/189.74 inference(scs_inference,[],[1081,2])). % 189.69/189.74 cnf(1083,plain, % 189.69/189.74 (E(f2(a1,f2(a7,a1)),f2(x10831,f2(x10832,f3(f2(x10831,x10832),a4))))), % 189.69/189.74 inference(scs_inference,[],[1031,1080,1081,2,3])). % 189.69/189.74 cnf(1084,plain, % 189.69/189.74 (E(f2(x10841,f2(x10842,f3(f2(x10841,x10842),a4))),f2(a1,f2(a7,a1)))), % 189.69/189.74 inference(scs_inference,[],[1083,2])). % 189.69/189.74 cnf(1085,plain, % 189.69/189.74 (E(f2(a4,f2(f3(f2(a1,a4),a4),a1)),f6(a4,f2(a1,a1)))), % 189.69/189.74 inference(scs_inference,[],[324,1082,1083,2,3])). % 189.69/189.74 cnf(1086,plain, % 189.69/189.74 (E(f6(a4,f2(a1,a1)),f2(a4,f2(f3(f2(a1,a4),a4),a1)))), % 189.69/189.74 inference(scs_inference,[],[1085,2])). % 189.69/189.74 cnf(1087,plain, % 189.69/189.74 (E(f2(f2(a8,a1),a1),f2(a1,a5))), % 189.69/189.74 inference(scs_inference,[],[1044,927,1085,2,3])). % 189.69/189.74 cnf(1088,plain, % 189.69/189.74 (E(f2(a1,a5),f2(f2(a8,a1),a1))), % 189.69/189.74 inference(scs_inference,[],[1087,2])). % 189.69/189.74 cnf(1089,plain, % 189.69/189.74 (E(f6(a4,f2(a1,a1)),f2(a1,a4))), % 189.69/189.74 inference(scs_inference,[],[720,1086,1087,2,3])). % 189.69/189.74 cnf(1090,plain, % 189.69/189.74 (E(f2(a1,a4),f6(a4,f2(a1,a1)))), % 189.69/189.74 inference(scs_inference,[],[1089,2])). % 189.69/189.74 cnf(1091,plain, % 189.69/189.74 (E(f2(a1,a5),f2(a1,f2(f6(a4,f2(a1,a1)),a1)))), % 189.69/189.74 inference(scs_inference,[],[1088,747,1089,2,3])). % 189.69/189.74 cnf(1092,plain, % 189.69/189.74 (E(f2(a1,f2(f6(a4,f2(a1,a1)),a1)),f2(a1,a5))), % 189.69/189.74 inference(scs_inference,[],[1091,2])). % 189.69/189.74 cnf(1093,plain, % 189.69/189.74 (E(f2(a1,a4),f2(a1,f2(a4,f2(f3(a4,a5),a1))))), % 189.69/189.74 inference(scs_inference,[],[1078,1090,1091,2,3])). % 189.69/189.74 cnf(1095,plain, % 189.69/189.74 (E(f2(a1,f2(a8,a1)),f2(a1,a5))), % 189.69/189.74 inference(scs_inference,[],[1092,750,1093,2,3])). % 189.69/189.74 cnf(1096,plain, % 189.69/189.74 (E(f2(a1,a5),f2(a1,f2(a8,a1)))), % 189.69/189.74 inference(scs_inference,[],[1095,2])). % 189.69/189.74 cnf(1097,plain, % 189.69/189.74 (E(a4,f2(a1,a8))), % 189.69/189.74 inference(scs_inference,[],[978,111,1095,2,3])). % 189.69/189.74 cnf(1099,plain, % 189.69/189.74 (E(f2(a1,a8),a4)), % 189.69/189.74 inference(scs_inference,[],[1097,2])). % 189.69/189.74 cnf(1100,plain, % 189.69/189.74 (E(f2(a1,a5),f2(a1,f2(a1,f6(a4,f2(a1,a1)))))), % 189.69/189.74 inference(scs_inference,[],[1096,861,1097,2,3])). % 189.69/189.74 cnf(1102,plain, % 189.69/189.74 (E(a8,f2(a4,a1))), % 189.69/189.74 inference(scs_inference,[],[501,161,1100,2,3])). % 189.69/189.74 cnf(1104,plain, % 189.69/189.74 (E(f2(a4,a1),a8)), % 189.69/189.74 inference(scs_inference,[],[1102,2])). % 189.69/189.74 cnf(1105,plain, % 189.69/189.74 (E(f3(x11051,f2(a4,x11051)),f2(a8,a1))), % 189.69/189.74 inference(scs_inference,[],[330,561,1102,2,3])). % 189.69/189.74 cnf(1107,plain, % 189.69/189.74 (E(f2(a8,a1),f3(x11071,f2(a4,x11071)))), % 189.69/189.74 inference(scs_inference,[],[1105,2])). % 189.69/189.74 cnf(1108,plain, % 189.69/189.74 (E(f2(a4,f2(f3(a4,a5),a1)),f2(f3(x11081,f2(a4,x11081)),a1))), % 189.69/189.74 inference(scs_inference,[],[558,387,1105,2,3])). % 189.69/189.74 cnf(1109,plain, % 189.69/189.74 (E(f2(f3(x11091,f2(a4,x11091)),a1),f2(a4,f2(f3(a4,a5),a1)))), % 189.69/189.74 inference(scs_inference,[],[1108,2])). % 189.69/189.74 cnf(1110,plain, % 189.69/189.74 (E(f2(a8,a1),a5)), % 189.69/189.74 inference(scs_inference,[],[12,1107,1108,2,3])). % 189.69/189.74 cnf(1112,plain, % 189.69/189.74 (E(a5,f2(a8,a1))), % 189.69/189.74 inference(scs_inference,[],[1110,2])). % 189.69/189.74 cnf(1113,plain, % 189.69/189.74 (E(f2(x11131,f3(f2(a1,x11131),a4)),f2(a1,f3(x11132,f2(a4,x11132))))), % 189.69/189.74 inference(scs_inference,[],[816,327,1110,2,3])). % 189.69/189.74 cnf(1114,plain, % 189.69/189.74 (E(f2(a1,f3(x11141,f2(a4,x11141))),f2(x11142,f3(f2(a1,x11142),a4)))), % 189.69/189.74 inference(scs_inference,[],[1113,2])). % 189.69/189.74 cnf(1115,plain, % 189.69/189.74 (E(f2(a4,f2(f3(a4,a4),a1)),f2(a1,f6(a4,f2(a1,a1))))), % 189.69/189.74 inference(scs_inference,[],[909,546,1113,2,3])). % 189.69/189.74 cnf(1117,plain, % 189.69/189.74 (E(f2(a1,f6(a4,f2(a1,a1))),f2(a4,f2(f3(a4,a4),a1)))), % 189.69/189.74 inference(scs_inference,[],[1115,2])). % 189.69/189.74 cnf(1118,plain, % 189.69/189.74 (E(f2(f2(f6(a5,f2(a4,a4)),f2(a4,a4)),a1),f2(f6(a4,f2(a1,a1)),a1))), % 189.69/189.74 inference(scs_inference,[],[573,558,1115,2,3])). % 189.69/189.74 cnf(1120,plain, % 189.69/189.74 (E(f2(f6(a4,f2(a1,a1)),a1),f2(f2(f6(a5,f2(a4,a4)),f2(a4,a4)),a1))), % 189.69/189.74 inference(scs_inference,[],[1118,2])). % 189.69/189.74 cnf(1121,plain, % 189.69/189.74 (E(f3(x11211,f2(a4,x11211)),f2(a4,a1))), % 189.69/189.74 inference(scs_inference,[],[642,450,1118,2,3])). % 189.69/189.74 cnf(1123,plain, % 189.69/189.74 (E(f2(a4,a1),f3(x11231,f2(a4,x11231)))), % 189.69/189.74 inference(scs_inference,[],[1121,2])). % 189.69/189.74 cnf(1124,plain, % 189.69/189.74 (E(f6(a4,f2(a1,a1)),f2(a5,a1))), % 189.69/189.74 inference(scs_inference,[],[651,1080,1121,2,3])). % 189.69/189.74 cnf(1127,plain, % 189.69/189.74 (E(f2(a5,a1),f6(a4,f2(a1,a1)))), % 189.69/189.74 inference(scs_inference,[],[1124,2])). % 189.69/189.74 cnf(1128,plain, % 189.69/189.74 (E(f2(a4,a1),a5)), % 189.69/189.74 inference(scs_inference,[],[12,1123,1124,2,3])). % 189.69/189.74 cnf(1130,plain, % 189.69/189.74 (E(a5,f2(a4,a1))), % 189.69/189.74 inference(scs_inference,[],[1128,2])). % 189.69/189.74 cnf(1131,plain, % 189.69/189.74 (E(f2(f2(f6(a4,f2(a1,x11311)),x11311),a1),f6(a4,f2(a1,a1)))), % 189.69/189.74 inference(scs_inference,[],[1127,477,1128,2,3])). % 189.69/189.74 cnf(1132,plain, % 189.69/189.74 (E(f6(a4,f2(a1,a1)),f2(f2(f6(a4,f2(a1,x11321)),x11321),a1))), % 189.69/189.74 inference(scs_inference,[],[1131,2])). % 189.69/189.74 cnf(1133,plain, % 189.69/189.74 (E(f6(a4,f2(a1,a1)),f2(f2(a7,a1),a1))), % 189.69/189.74 inference(scs_inference,[],[627,465,1131,2,3])). % 189.69/189.74 cnf(1135,plain, % 189.69/189.74 (E(f2(f2(a7,a1),a1),f6(a4,f2(a1,a1)))), % 189.69/189.74 inference(scs_inference,[],[1133,2])). % 189.69/189.74 cnf(1136,plain, % 189.69/189.74 (E(f2(f2(f6(a4,f2(x11361,a4)),f2(a4,x11361)),a1),f2(a1,f2(a1,f2(a8,a1))))), % 189.69/189.74 inference(scs_inference,[],[1062,498,1133,2,3])). % 189.69/189.74 cnf(1137,plain, % 189.69/189.74 (E(f2(a1,f2(a1,f2(a8,a1))),f2(f2(f6(a4,f2(x11371,a4)),f2(a4,x11371)),a1))), % 189.69/189.74 inference(scs_inference,[],[1136,2])). % 189.69/189.74 cnf(1138,plain, % 189.69/189.74 (E(f2(f2(f3(x11381,f2(a4,x11381)),a1),a1),f6(a4,f2(a1,a1)))), % 189.69/189.74 inference(scs_inference,[],[1135,630,1136,2,3])). % 189.69/189.74 cnf(1140,plain, % 189.69/189.74 (E(f6(a4,f2(a1,a1)),f2(f2(a4,a1),a1))), % 189.69/189.74 inference(scs_inference,[],[645,1132,1138,2,3])). % 189.69/189.74 cnf(1142,plain, % 189.69/189.74 (E(f2(f2(a4,a1),a1),f6(a4,f2(a1,a1)))), % 189.69/189.74 inference(scs_inference,[],[1140,2])). % 189.69/189.74 cnf(1143,plain, % 189.69/189.74 (E(f2(a1,f2(a8,a1)),f2(a1,f2(a4,a1)))), % 189.69/189.74 inference(scs_inference,[],[828,750,1140,2,3])). % 189.69/189.74 cnf(1145,plain, % 189.69/189.74 (E(f2(a1,f2(a4,a1)),f2(a1,f2(a8,a1)))), % 189.69/189.74 inference(scs_inference,[],[1143,2])). % 189.69/189.74 cnf(1146,plain, % 189.69/189.74 (E(f3(x11461,f2(a4,x11461)),f2(a1,f2(a7,a1)))), % 189.69/189.74 inference(scs_inference,[],[876,450,1143,2,3])). % 189.69/189.74 cnf(1148,plain, % 189.69/189.74 (E(f2(a1,f2(a7,a1)),f3(x11481,f2(a4,x11481)))), % 189.69/189.74 inference(scs_inference,[],[1146,2])). % 189.69/189.74 cnf(1149,plain, % 189.69/189.74 (E(f2(a1,f2(a1,f2(a1,a4))),f2(a1,f2(a8,a1)))), % 189.69/189.74 inference(scs_inference,[],[1145,1070,1146,2,3])). % 189.69/189.74 cnf(1151,plain, % 189.69/189.74 (E(f2(a1,f2(a7,a1)),a5)), % 189.69/189.74 inference(scs_inference,[],[12,1148,1149,2,3])). % 189.69/189.74 cnf(1153,plain, % 189.69/189.74 (E(a5,f2(a1,f2(a7,a1)))), % 189.69/189.74 inference(scs_inference,[],[1151,2])). % 189.69/189.74 cnf(1154,plain, % 189.69/189.74 (E(f2(f2(a8,a1),a1),f2(a1,f2(a4,a1)))), % 189.69/189.74 inference(scs_inference,[],[882,435,1151,2,3])). % 189.69/189.74 cnf(1156,plain, % 189.69/189.74 (E(f2(a1,f2(a4,a1)),f2(f2(a8,a1),a1))), % 189.69/189.74 inference(scs_inference,[],[1154,2])). % 189.69/189.74 cnf(1157,plain, % 189.69/189.74 (E(f6(a4,f2(a1,a1)),f2(a1,f2(a5,a1)))), % 189.69/189.74 inference(scs_inference,[],[900,465,1154,2,3])). % 189.69/189.74 cnf(1159,plain, % 189.69/189.74 (E(f2(a1,f2(a5,a1)),f6(a4,f2(a1,a1)))), % 189.69/189.74 inference(scs_inference,[],[1157,2])). % 189.69/189.74 cnf(1160,plain, % 189.69/189.74 (E(f2(x11601,f3(f2(a1,x11601),a4)),f2(a1,f2(a5,a1)))), % 189.69/189.74 inference(scs_inference,[],[903,27,1157,2,3])). % 189.69/189.74 cnf(1162,plain, % 189.69/189.74 (E(f2(a1,f2(a5,a1)),f2(x11621,f3(f2(a1,x11621),a4)))), % 189.69/189.74 inference(scs_inference,[],[1160,2])). % 189.69/189.74 cnf(1163,plain, % 189.69/189.74 (E(f2(a5,a1),f2(a1,f2(a7,a1)))), % 189.69/189.74 inference(scs_inference,[],[1084,897,1160,2,3])). % 189.69/189.74 cnf(1165,plain, % 189.69/189.74 (E(f2(a1,f2(a7,a1)),f2(a5,a1))), % 189.69/189.74 inference(scs_inference,[],[1163,2])). % 189.69/189.74 cnf(1166,plain, % 189.69/189.74 (E(f2(a1,f2(f6(a4,f2(x11661,a4)),f2(a4,x11661))),f2(a4,f2(f3(a4,a5),a1)))), % 189.69/189.74 inference(scs_inference,[],[1022,843,1163,2,3])). % 189.69/189.74 cnf(1168,plain, % 189.69/189.74 (E(f2(a1,f2(a7,a1)),f2(a4,f2(f2(f3(a4,a4),a1),a1)))), % 189.69/189.74 inference(scs_inference,[],[1165,1012,1166,2,3])). % 189.69/189.74 cnf(1169,plain, % 189.69/189.74 (E(f2(a4,f2(f2(f3(a4,a4),a1),a1)),f2(a1,f2(a7,a1)))), % 189.69/189.74 inference(scs_inference,[],[1168,2])). % 189.69/189.74 cnf(1170,plain, % 189.69/189.74 (E(f2(a1,f2(f6(a4,f2(x11701,a4)),f2(a4,x11701))),f2(x11702,f3(f2(a1,x11702),a4)))), % 189.69/189.74 inference(scs_inference,[],[1162,846,1168,2,3])). % 189.69/189.74 cnf(1172,plain, % 189.69/189.74 (E(f2(a1,a7),f2(a1,f2(a7,a1)))), % 189.69/189.74 inference(scs_inference,[],[1169,1027,1170,2,3])). % 189.69/189.74 cnf(1173,plain, % 189.69/189.74 (E(f2(a1,f2(a7,a1)),f2(a1,a7))), % 189.69/189.74 inference(scs_inference,[],[1172,2])). % 189.69/189.74 cnf(1174,plain, % 189.69/189.74 (E(f2(f3(x11741,f2(a4,x11741)),a1),f2(x11742,f3(f2(a1,x11742),a4)))), % 189.69/189.74 inference(scs_inference,[],[303,1109,1172,2,3])). % 189.69/189.74 cnf(1175,plain, % 189.69/189.74 (E(f2(x11751,f3(f2(a1,x11751),a4)),f2(f3(x11752,f2(a4,x11752)),a1))), % 189.69/189.74 inference(scs_inference,[],[1174,2])). % 189.69/189.74 cnf(1176,plain, % 189.69/189.74 (E(f2(f2(f6(a4,f2(x11761,a4)),f2(a4,x11761)),a1),f2(a1,a7))), % 189.69/189.74 inference(scs_inference,[],[1173,885,1174,2,3])). % 189.69/189.74 cnf(1177,plain, % 189.69/189.74 (E(f2(a1,a7),f2(f2(f6(a4,f2(x11771,a4)),f2(a4,x11771)),a1))), % 189.69/189.74 inference(scs_inference,[],[1176,2])). % 189.69/189.74 cnf(1178,plain, % 189.69/189.74 (E(f3(x11781,f2(a4,x11781)),f2(a7,a1))), % 189.69/189.74 inference(scs_inference,[],[357,561,1176,2,3])). % 189.69/189.74 cnf(1180,plain, % 189.69/189.74 (E(f2(a7,a1),f3(x11801,f2(a4,x11801)))), % 189.69/189.74 inference(scs_inference,[],[1178,2])). % 189.69/189.74 cnf(1181,plain, % 189.69/189.74 (E(f2(f2(a8,a1),a1),f2(a1,a7))), % 189.69/189.74 inference(scs_inference,[],[969,747,1178,2,3])). % 189.69/189.74 cnf(1183,plain, % 189.69/189.74 (E(f2(a1,a7),f2(f2(a8,a1),a1))), % 189.69/189.74 inference(scs_inference,[],[1181,2])). % 189.69/189.74 cnf(1184,plain, % 189.69/189.74 (E(f2(a7,a1),a5)), % 189.69/189.74 inference(scs_inference,[],[12,1180,1181,2,3])). % 189.69/189.74 cnf(1186,plain, % 189.69/189.74 (E(a5,f2(a7,a1))), % 189.69/189.74 inference(scs_inference,[],[1184,2])). % 189.69/189.74 cnf(1187,plain, % 189.69/189.74 (E(f2(a1,f2(a1,f2(a8,a1))),f2(f6(a4,f2(a1,a1)),a1))), % 189.69/189.74 inference(scs_inference,[],[585,1137,1184,2,3])). % 189.69/189.74 cnf(1189,plain, % 189.69/189.74 (E(f2(f6(a4,f2(a1,a1)),a1),f2(a1,f2(a1,f2(a8,a1))))), % 189.69/189.74 inference(scs_inference,[],[1187,2])). % 189.69/189.74 cnf(1190,plain, % 189.69/189.74 (E(f2(f6(f6(f2(a5,x11901),x11901),f2(a4,a4)),f2(a4,a4)),f2(a8,a1))), % 189.69/189.74 inference(scs_inference,[],[348,44,1187,2,3])). % 189.69/189.74 cnf(1193,plain, % 189.69/189.74 (E(f2(a8,a1),f2(f6(f6(f2(a5,x11931),x11931),f2(a4,a4)),f2(a4,a4)))), % 189.69/189.74 inference(scs_inference,[],[1190,2])). % 189.69/189.74 cnf(1194,plain, % 189.69/189.74 (E(f2(f3(x11941,f2(a4,x11941)),a1),f2(a1,f2(a1,f2(a8,a1))))), % 189.69/189.74 inference(scs_inference,[],[1189,573,1190,2,3])). % 189.69/189.74 cnf(1195,plain, % 189.69/189.74 (E(f2(a1,f2(a1,f2(a8,a1))),f2(f3(x11951,f2(a4,x11951)),a1))), % 189.69/189.74 inference(scs_inference,[],[1194,2])). % 189.69/189.74 cnf(1196,plain, % 189.69/189.74 (E(f2(f2(a5,a1),a1),f2(f2(a8,a1),a1))), % 189.69/189.74 inference(scs_inference,[],[609,606,1194,2,3])). % 189.69/189.74 cnf(1198,plain, % 189.69/189.74 (E(f2(f2(a8,a1),a1),f2(f2(a5,a1),a1))), % 189.69/189.74 inference(scs_inference,[],[1196,2])). % 189.69/189.74 cnf(1199,plain, % 189.69/189.74 (E(f2(f2(a7,a1),a1),f2(f3(x11991,f2(a4,x11991)),a1))), % 189.69/189.74 inference(scs_inference,[],[1195,1062,1196,2,3])). % 189.69/189.74 cnf(1201,plain, % 189.69/189.74 (E(f2(f6(a4,f2(a1,a1)),a1),f2(f2(f2(a7,a1),a1),a1))), % 189.69/189.74 inference(scs_inference,[],[1060,1189,1199,2,3])). % 189.69/189.74 cnf(1202,plain, % 189.69/189.74 (E(f2(f2(f2(a7,a1),a1),a1),f2(f6(a4,f2(a1,a1)),a1))), % 189.69/189.74 inference(scs_inference,[],[1201,2])). % 189.69/189.74 cnf(1203,plain, % 189.69/189.74 (E(f2(a1,f2(a4,a1)),f2(f2(a5,a1),a1))), % 189.69/189.74 inference(scs_inference,[],[1156,1198,1201,2,3])). % 189.69/189.74 cnf(1204,plain, % 189.69/189.74 (E(f2(f2(a5,a1),a1),f2(a1,f2(a4,a1)))), % 189.69/189.74 inference(scs_inference,[],[1203,2])). % 189.69/189.74 cnf(1205,plain, % 189.69/189.74 (E(f2(f2(f2(a7,a1),a1),a1),f2(f2(f6(a5,f2(a4,a4)),f2(a4,a4)),a1))), % 189.69/189.74 inference(scs_inference,[],[1120,1202,1203,2,3])). % 189.69/189.74 cnf(1207,plain, % 189.69/189.74 (E(f2(f2(x12071,f3(f2(a1,x12071),a4)),a1),f2(a1,f2(a4,a1)))), % 189.69/189.74 inference(scs_inference,[],[1204,339,1205,2,3])). % 189.69/189.74 cnf(1208,plain, % 189.69/189.74 (E(f2(a1,f2(a4,a1)),f2(f2(x12081,f3(f2(a1,x12081),a4)),a1))), % 189.69/189.74 inference(scs_inference,[],[1207,2])). % 189.69/189.74 cnf(1209,plain, % 189.69/189.74 (E(f2(f2(a5,a1),a1),f2(a1,f2(a8,a1)))), % 189.69/189.74 inference(scs_inference,[],[858,867,1207,2,3])). % 189.69/189.74 cnf(1211,plain, % 189.69/189.74 (E(f2(a1,f2(a8,a1)),f2(f2(a5,a1),a1))), % 189.69/189.74 inference(scs_inference,[],[1209,2])). % 189.69/189.74 cnf(1212,plain, % 189.69/189.74 (E(f2(a1,f2(a4,a1)),f2(a8,a1))), % 189.69/189.74 inference(scs_inference,[],[480,1208,1209,2,3])). % 189.69/189.74 cnf(1214,plain, % 189.69/189.74 (E(f2(a8,a1),f2(a1,f2(a4,a1)))), % 189.69/189.74 inference(scs_inference,[],[1212,2])). % 189.69/189.74 cnf(1215,plain, % 189.69/189.74 (E(a5,f2(a1,f2(f2(f6(a5,f2(a4,a4)),f2(a4,a4)),a1)))), % 189.69/189.74 inference(scs_inference,[],[708,1112,1212,2,3])). % 189.69/189.74 cnf(1217,plain, % 189.69/189.74 (E(f2(a1,f2(a7,a1)),f2(f6(f6(f2(a5,x12171),x12171),f2(a4,a4)),f2(a4,a4)))), % 189.69/189.74 inference(scs_inference,[],[1193,1016,1215,2,3])). % 189.69/189.74 cnf(1218,plain, % 189.69/189.74 (E(f2(f6(f6(f2(a5,x12181),x12181),f2(a4,a4)),f2(a4,a4)),f2(a1,f2(a7,a1)))), % 189.69/189.74 inference(scs_inference,[],[1217,2])). % 189.69/189.74 cnf(1219,plain, % 189.69/189.74 (E(f2(a1,f2(a5,a1)),f2(a1,f2(a1,a8)))), % 189.69/189.74 inference(scs_inference,[],[993,879,1217,2,3])). % 189.69/189.74 cnf(1221,plain, % 189.69/189.74 (E(f2(a1,f2(a1,a8)),f2(a1,f2(a5,a1)))), % 189.69/189.74 inference(scs_inference,[],[1219,2])). % 189.69/189.74 cnf(1222,plain, % 189.69/189.74 (E(f2(f6(f6(f2(a5,x12221),x12221),f2(a4,a4)),f2(a4,a4)),f2(x12222,f3(f2(a1,x12222),a4)))), % 189.69/189.74 inference(scs_inference,[],[1218,1014,1219,2,3])). % 189.69/189.74 cnf(1223,plain, % 189.69/189.74 (E(f2(x12231,f3(f2(a1,x12231),a4)),f2(f6(f6(f2(a5,x12232),x12232),f2(a4,a4)),f2(a4,a4)))), % 189.69/189.74 inference(scs_inference,[],[1222,2])). % 189.69/189.74 cnf(1224,plain, % 189.69/189.74 (E(f2(a1,f2(a1,a8)),f6(a4,f2(a1,a1)))), % 189.69/189.74 inference(scs_inference,[],[1221,1159,1222,2,3])). % 189.69/189.74 cnf(1225,plain, % 189.69/189.74 (E(f6(a4,f2(a1,a1)),f2(a1,f2(a1,a8)))), % 189.69/189.74 inference(scs_inference,[],[1224,2])). % 189.69/189.74 cnf(1226,plain, % 189.69/189.74 (E(f2(f2(a7,a1),a1),f2(f6(f6(f2(a5,x12261),x12261),f2(a4,a4)),f2(a4,a4)))), % 189.69/189.74 inference(scs_inference,[],[1036,1223,1224,2,3])). % 189.69/189.74 cnf(1228,plain, % 189.69/189.74 (E(f2(f6(f6(f2(a5,x12281),x12281),f2(a4,a4)),f2(a4,a4)),f2(f2(a7,a1),a1))), % 189.69/189.74 inference(scs_inference,[],[1226,2])). % 189.69/189.74 cnf(1229,plain, % 189.69/189.74 (E(f2(f2(a4,a1),a1),f2(a1,f2(a1,a8)))), % 189.69/189.74 inference(scs_inference,[],[1142,1225,1226,2,3])). % 189.69/189.74 cnf(1230,plain, % 189.69/189.74 (E(f2(a1,f2(a1,a8)),f2(f2(a4,a1),a1))), % 189.69/189.74 inference(scs_inference,[],[1229,2])). % 189.69/189.74 cnf(1231,plain, % 189.69/189.74 (E(f2(a8,a1),f2(f2(a7,a1),a1))), % 189.69/189.74 inference(scs_inference,[],[1228,1193,1229,2,3])). % 189.69/189.74 cnf(1233,plain, % 189.69/189.74 (E(f2(f2(a7,a1),a1),f2(a8,a1))), % 189.69/189.74 inference(scs_inference,[],[1231,2])). % 189.69/189.74 cnf(1234,plain, % 189.69/189.74 (E(a7,f2(f2(f6(a4,f2(x12341,a4)),f2(a4,x12341)),a1))), % 189.69/189.74 inference(scs_inference,[],[564,279,1231,2,3])). % 189.69/189.74 cnf(1236,plain, % 189.69/189.74 (E(f2(f2(a7,a1),a1),f2(a4,f2(f2(f3(a4,a4),a1),a1)))), % 189.69/189.74 inference(scs_inference,[],[1233,1009,1234,2,3])). % 189.69/189.74 cnf(1237,plain, % 189.69/189.74 (E(f2(a4,f2(f2(f3(a4,a4),a1),a1)),f2(f2(a7,a1),a1))), % 189.69/189.74 inference(scs_inference,[],[1236,2])). % 189.69/189.74 cnf(1238,plain, % 189.69/189.74 (E(f2(f2(a7,a1),a1),f2(a4,f2(x12381,f3(f2(a4,x12381),a5))))), % 189.69/189.74 inference(scs_inference,[],[150,998,1236,2,3])). % 189.69/189.74 cnf(1241,plain, % 189.69/189.74 (E(f2(a1,a7),f2(f2(a7,a1),a1))), % 189.69/189.74 inference(scs_inference,[],[1237,1027,1238,2,3])). % 189.69/189.74 cnf(1242,plain, % 189.69/189.74 (E(f2(f2(a7,a1),a1),f2(a1,a7))), % 189.69/189.74 inference(scs_inference,[],[1241,2])). % 189.69/189.74 cnf(1243,plain, % 189.69/189.74 (E(f2(f2(a8,a1),a1),f2(f2(f6(a5,f2(x12431,a4)),x12431),a4))), % 189.69/189.74 inference(scs_inference,[],[155,1029,1241,2,3])). % 189.69/189.74 cnf(1246,plain, % 189.69/189.74 (E(f2(f2(a7,a1),a1),f2(a1,f2(f3(x12461,f2(a4,x12461)),a1)))), % 189.69/189.74 inference(scs_inference,[],[1242,990,1243,2,3])). % 189.69/189.74 cnf(1248,plain, % 189.69/189.74 (E(f2(a1,f3(x12481,f2(a4,x12481))),f2(f3(x12482,f2(a4,x12482)),a1))), % 189.69/189.74 inference(scs_inference,[],[1114,1175,1246,2,3])). % 189.69/189.74 cnf(1251,plain, % 189.69/189.74 (E(f2(a4,f2(f3(a4,a4),a1)),f2(a1,f2(a5,a1)))), % 189.69/189.74 inference(scs_inference,[],[453,660,1248,2,3])). % 189.69/189.74 cnf(1253,plain, % 189.69/189.74 (E(f2(a1,f2(a5,a1)),f2(a4,f2(f3(a4,a4),a1)))), % 189.69/189.74 inference(scs_inference,[],[1251,2])). % 189.69/189.74 cnf(1254,plain, % 189.69/189.74 (E(f2(a1,a7),f2(a1,f6(a4,f2(a1,a1))))), % 189.69/189.74 inference(scs_inference,[],[912,1177,1251,2,3])). % 189.69/189.74 cnf(1256,plain, % 189.69/189.74 (E(f2(a1,f6(a4,f2(a1,a1))),f2(a1,a7))), % 189.69/189.74 inference(scs_inference,[],[1254,2])). % 189.69/189.74 cnf(1257,plain, % 189.69/189.74 (E(f2(a8,a1),f2(a4,f2(f3(a4,a4),a1)))), % 189.69/189.74 inference(scs_inference,[],[1117,849,1254,2,3])). % 189.69/189.74 cnf(1258,plain, % 189.69/189.74 (E(f2(a4,f2(f3(a4,a4),a1)),f2(a8,a1))), % 189.69/189.74 inference(scs_inference,[],[1257,2])). % 189.69/189.74 cnf(1259,plain, % 189.69/189.74 (E(f2(a1,f2(a1,a8)),f2(a4,f2(f3(a4,a4),a1)))), % 189.69/189.74 inference(scs_inference,[],[1253,1221,1257,2,3])). % 189.69/189.74 cnf(1261,plain, % 189.69/189.74 (E(f2(a4,f2(f3(a4,a4),a1)),f2(a1,f2(a4,a1)))), % 189.69/189.74 inference(scs_inference,[],[1214,1258,1259,2,3])). % 189.69/189.74 cnf(1263,plain, % 189.69/189.74 (E(f3(x12631,f2(x12631,f2(a1,f2(a8,a1)))),f2(f2(a5,a1),a1))), % 189.69/189.74 inference(scs_inference,[],[13,1211,1261,2,3])). % 189.69/189.74 cnf(1266,plain, % 189.69/189.74 (E(f3(x12661,f2(x12661,f2(a1,f2(a1,a8)))),f2(f2(a4,a1),a1))), % 189.69/189.74 inference(scs_inference,[],[13,1230,1263,2,3])). % 189.69/189.74 cnf(1269,plain, % 189.69/189.74 (E(f3(x12691,f2(x12691,f2(a1,a7))),f2(f2(a8,a1),a1))), % 189.69/189.74 inference(scs_inference,[],[13,1183,1266,2,3])). % 189.69/189.74 cnf(1272,plain, % 189.69/189.74 (E(f3(x12721,f2(x12721,f2(a4,a1))),a8)), % 189.69/189.74 inference(scs_inference,[],[13,1104,1269,2,3])). % 189.69/189.74 cnf(1274,plain, % 189.69/189.74 (E(a8,f3(x12741,f2(x12741,f2(a4,a1))))), % 189.69/189.74 inference(scs_inference,[],[1272,2])). % 189.69/189.74 cnf(1275,plain, % 189.69/189.74 (E(f3(x12751,f2(x12751,a5)),f2(a4,a1))), % 189.69/189.74 inference(scs_inference,[],[13,1130,1272,2,3])). % 189.69/189.74 cnf(1277,plain, % 189.69/189.74 (E(f2(a4,a1),f3(x12771,f2(x12771,a5)))), % 189.69/189.74 inference(scs_inference,[],[1275,2])). % 189.69/189.74 cnf(1278,plain, % 189.69/189.74 (E(f3(x12781,f2(x12781,a5)),f2(a7,a1))), % 189.69/189.74 inference(scs_inference,[],[13,1186,1275,2,3])). % 189.69/189.74 cnf(1280,plain, % 189.69/189.74 (E(f2(a7,a1),f3(x12801,f2(x12801,a5)))), % 189.69/189.74 inference(scs_inference,[],[1278,2])). % 189.69/189.74 cnf(1281,plain, % 189.69/189.74 (E(f3(x12811,f2(x12811,f2(a4,a1))),f3(x12812,f2(x12812,a5)))), % 189.69/189.74 inference(scs_inference,[],[13,1277,1278,2,3])). % 189.69/189.74 cnf(1284,plain, % 189.69/189.74 (E(f3(x12841,f2(x12841,f2(a7,a1))),f3(x12842,f2(x12842,a5)))), % 189.69/189.74 inference(scs_inference,[],[13,1280,1281,2,3])). % 189.69/189.74 cnf(1287,plain, % 189.69/189.74 (E(f3(x12871,f2(x12871,a5)),f2(f2(a7,a1),a1))), % 189.69/189.74 inference(scs_inference,[],[13,1004,1284,2,3])). % 189.69/189.74 cnf(1289,plain, % 189.69/189.74 (E(f2(f2(a7,a1),a1),f3(x12891,f2(x12891,a5)))), % 189.69/189.74 inference(scs_inference,[],[1287,2])). % 189.69/189.74 cnf(1290,plain, % 189.69/189.74 (E(f3(x12901,f2(x12901,a5)),f2(f2(a8,a1),a1))), % 189.69/189.74 inference(scs_inference,[],[13,1034,1287,2,3])). % 189.69/189.74 cnf(1292,plain, % 189.69/189.74 (E(f2(f2(a8,a1),a1),f3(x12921,f2(x12921,a5)))), % 189.69/189.74 inference(scs_inference,[],[1290,2])). % 189.69/189.74 cnf(1293,plain, % 189.69/189.74 (E(f3(x12931,f2(x12931,f2(f2(a7,a1),a1))),f3(x12932,f2(x12932,a5)))), % 189.69/189.74 inference(scs_inference,[],[13,1289,1290,2,3])). % 189.69/189.74 cnf(1296,plain, % 189.69/189.74 (E(f3(x12961,f2(x12961,f2(f2(a8,a1),a1))),f3(x12962,f2(x12962,a5)))), % 189.69/189.74 inference(scs_inference,[],[13,1292,1293,2,3])). % 189.69/189.74 cnf(1299,plain, % 189.69/189.74 (E(f3(x12991,f2(x12991,a5)),f2(a1,f2(a7,a1)))), % 189.69/189.74 inference(scs_inference,[],[13,1153,1296,2,3])). % 189.69/189.74 cnf(1301,plain, % 189.69/189.74 (E(f2(a1,f2(a7,a1)),f3(x13011,f2(x13011,a5)))), % 189.69/189.74 inference(scs_inference,[],[1299,2])). % 189.69/189.74 cnf(1302,plain, % 189.69/189.74 (E(f3(x13021,f2(x13021,a8)),f3(x13022,f2(x13022,f2(a4,a1))))), % 189.69/189.74 inference(scs_inference,[],[13,1274,1299,2,3])). % 189.69/189.74 cnf(1305,plain, % 189.69/189.74 (E(f3(x13051,f2(x13051,f2(a1,f2(a7,a1)))),f3(x13052,f2(x13052,a5)))), % 189.69/189.74 inference(scs_inference,[],[13,1301,1302,2,3])). % 189.69/189.74 cnf(1308,plain, % 189.69/189.74 (E(f3(x13081,f2(x13081,f2(a1,a8))),a4)), % 189.69/189.74 inference(scs_inference,[],[13,1099,1305,2,3])). % 189.69/189.74 cnf(1310,plain, % 189.69/189.74 (E(a4,f3(x13101,f2(x13101,f2(a1,a8))))), % 189.69/189.74 inference(scs_inference,[],[1308,2])). % 189.69/189.74 cnf(1311,plain, % 189.69/189.74 (E(f3(x13111,f2(x13111,f2(f2(a7,a1),a1))),f2(a8,a1))), % 189.69/189.74 inference(scs_inference,[],[13,1233,1308,2,3])). % 189.69/189.74 cnf(1314,plain, % 189.69/189.74 (E(f3(x13141,f2(x13141,a4)),f3(x13142,f2(x13142,f2(a1,a8))))), % 189.69/189.74 inference(scs_inference,[],[13,1310,1311,2,3])). % 189.69/189.74 cnf(1317,plain, % 189.69/189.74 (E(f3(x13171,f2(x13171,f2(a1,f2(a4,a1)))),f2(a1,f2(a8,a1)))), % 189.69/189.74 inference(scs_inference,[],[13,1145,1314,2,3])). % 189.69/189.74 cnf(1320,plain, % 189.69/189.74 (E(f3(x13201,f2(x13201,f2(a1,f2(a4,a1)))),f2(f2(a8,a1),a1))), % 189.69/189.74 inference(scs_inference,[],[13,1156,1317,2,3])). % 189.69/189.74 cnf(1323,plain, % 189.69/189.74 (E(f3(x13231,f2(x13231,f2(a8,a1))),f2(a1,f2(a4,a1)))), % 189.69/189.74 inference(scs_inference,[],[13,1214,1320,2,3])). % 189.69/189.74 cnf(1325,plain, % 189.69/189.74 (E(f2(a1,f2(a4,a1)),f3(x13251,f2(x13251,f2(a8,a1))))), % 189.69/189.74 inference(scs_inference,[],[1323,2])). % 189.69/189.74 cnf(1326,plain, % 189.69/189.74 (E(f3(x13261,f2(x13261,f2(a8,a1))),f2(a1,f2(a1,f2(a7,a1))))), % 189.69/189.74 inference(scs_inference,[],[13,1072,1323,2,3])). % 189.69/189.74 cnf(1329,plain, % 189.69/189.74 (E(f3(x13291,f2(x13291,f2(a1,f2(a7,a1)))),f2(a5,a1))), % 189.69/189.74 inference(scs_inference,[],[13,1165,1326,2,3])). % 189.69/189.74 cnf(1332,plain, % 189.69/189.74 (E(f3(x13321,f2(x13321,f2(a8,a1))),f2(f2(f2(a7,a1),a1),a1))), % 189.69/189.74 inference(scs_inference,[],[13,1050,1329,2,3])). % 189.69/189.74 cnf(1335,plain, % 189.69/189.74 (E(f3(x13351,f2(x13351,f2(f2(a8,a1),a1))),f2(f2(a5,a1),a1))), % 189.69/189.74 inference(scs_inference,[],[13,1198,1332,2,3])). % 189.69/189.74 cnf(1338,plain, % 189.69/189.74 (E(f3(x13381,f2(x13381,f2(f2(a5,a1),a1))),f2(a1,f2(a4,a1)))), % 189.69/189.74 inference(scs_inference,[],[13,1204,1335,2,3])). % 189.69/189.74 cnf(1341,plain, % 189.69/189.74 (E(f3(x13411,f2(x13411,f2(a7,a1))),f2(a1,a4))), % 189.69/189.74 inference(scs_inference,[],[13,918,1338,2,3])). % 189.69/189.74 cnf(1343,plain, % 189.69/189.74 (E(f2(a1,a4),f3(x13431,f2(x13431,f2(a7,a1))))), % 189.69/189.74 inference(scs_inference,[],[1341,2])). % 189.69/189.74 cnf(1344,plain, % 189.69/189.74 (E(f3(x13441,f2(x13441,f2(a7,a1))),f2(a1,f2(a8,a1)))), % 189.69/189.74 inference(scs_inference,[],[13,663,1341,2,3])). % 189.69/189.74 cnf(1347,plain, % 189.69/189.74 (E(f3(x13471,f2(x13471,f2(a1,a4))),f3(x13472,f2(x13472,f2(a7,a1))))), % 189.69/189.74 inference(scs_inference,[],[13,1343,1344,2,3])). % 189.69/189.74 cnf(1350,plain, % 189.69/189.74 (E(f3(x13501,f2(x13501,f2(a7,a1))),f2(a1,f2(f6(a5,f2(a4,a4)),f2(a4,a4))))), % 189.69/189.74 inference(scs_inference,[],[13,804,1347,2,3])). % 189.69/189.74 cnf(1353,plain, % 189.69/189.74 (E(f3(x13531,f2(x13531,f2(a1,f2(a5,a1)))),f2(a1,f2(a1,a7)))), % 189.69/189.74 inference(scs_inference,[],[13,945,1350,2,3])). % 189.69/189.74 cnf(1356,plain, % 189.69/189.74 (E(f3(x13561,f2(x13561,f2(f2(a7,a1),a1))),f2(a1,f2(a4,a1)))), % 189.69/189.74 inference(scs_inference,[],[13,726,1353,2,3])). % 189.69/189.74 cnf(1359,plain, % 189.69/189.74 (E(f3(x13591,f2(x13591,f2(f2(a5,a1),a1))),f2(a1,f2(a7,a1)))), % 189.69/189.74 inference(scs_inference,[],[13,774,1356,2,3])). % 189.69/189.74 cnf(1362,plain, % 189.69/189.74 (E(f3(x13621,f2(x13621,f2(a1,f2(a7,a1)))),f2(a1,a7))), % 189.69/189.74 inference(scs_inference,[],[13,1173,1359,2,3])). % 189.69/189.74 cnf(1365,plain, % 189.69/189.74 (E(f3(x13651,f2(x13651,f2(f2(a7,a1),a1))),f2(a1,a7))), % 189.69/189.74 inference(scs_inference,[],[13,1242,1362,2,3])). % 189.69/189.74 cnf(1368,plain, % 189.69/189.74 (E(f3(x13681,f2(x13681,f2(a1,a4))),f2(a1,f2(a7,a1)))), % 189.69/189.74 inference(scs_inference,[],[13,924,1365,2,3])). % 189.69/189.74 cnf(1371,plain, % 189.69/189.74 (E(f3(x13711,f2(x13711,f2(a1,a8))),f2(f2(a8,a1),a1))), % 189.69/189.74 inference(scs_inference,[],[13,1039,1368,2,3])). % 189.69/189.74 cnf(1374,plain, % 189.69/189.74 (E(f3(x13741,f2(x13741,f2(a1,f2(a7,a1)))),f2(a1,f2(a4,a1)))), % 189.69/189.74 inference(scs_inference,[],[13,729,1371,2,3])). % 189.69/189.74 cnf(1377,plain, % 189.69/189.74 (E(f3(x13771,f2(x13771,f2(a4,a1))),f2(a1,f2(a7,a1)))), % 189.69/189.74 inference(scs_inference,[],[13,723,1374,2,3])). % 189.69/189.74 cnf(1380,plain, % 189.69/189.74 (E(f3(x13801,f2(x13801,f2(a1,a5))),f2(f2(a8,a1),a1))), % 189.69/189.74 inference(scs_inference,[],[13,1088,1377,2,3])). % 189.69/189.74 cnf(1383,plain, % 189.69/189.74 (E(f3(x13831,f2(x13831,f2(a1,a5))),f2(a1,f2(a8,a1)))), % 189.69/189.74 inference(scs_inference,[],[13,1096,1380,2,3])). % 189.69/189.74 cnf(1386,plain, % 189.69/189.74 (E(f3(x13861,f2(x13861,f2(a1,f2(a5,a1)))),f2(a1,f2(a7,a1)))), % 189.69/189.74 inference(scs_inference,[],[13,771,1383,2,3])). % 189.69/189.74 cnf(1389,plain, % 189.69/189.74 (E(f3(x13891,f2(x13891,f2(f2(a8,a1),a1))),f2(a1,f2(a7,a1)))), % 189.69/189.74 inference(scs_inference,[],[13,687,1386,2,3])). % 189.69/189.74 cnf(1392,plain, % 189.69/189.74 (E(f3(x13921,f2(x13921,f2(a7,a1))),f2(a1,f2(a5,a1)))), % 189.69/189.74 inference(scs_inference,[],[13,765,1389,2,3])). % 189.69/189.74 cnf(1395,plain, % 189.69/189.74 (E(f3(x13951,f2(x13951,f2(a5,a1))),f2(a1,a7))), % 189.69/189.74 inference(scs_inference,[],[13,933,1392,2,3])). % 189.69/189.74 cnf(1397,plain, % 189.69/189.74 (E(f2(a1,a7),f3(x13971,f2(x13971,f2(a5,a1))))), % 189.69/189.74 inference(scs_inference,[],[1395,2])). % 189.69/189.74 cnf(1398,plain, % 189.69/189.74 (E(f3(x13981,f2(x13981,f2(a1,a7))),f2(a1,f2(a5,a1)))), % 189.69/189.74 inference(scs_inference,[],[13,939,1395,2,3])). % 189.69/189.74 cnf(1401,plain, % 189.69/189.74 (E(f3(x14011,f2(x14011,f2(a1,a7))),f3(x14012,f2(x14012,f2(a5,a1))))), % 189.69/189.74 inference(scs_inference,[],[13,1397,1398,2,3])). % 189.69/189.74 cnf(1404,plain, % 189.69/189.74 (E(f3(x14041,f2(x14041,f2(a8,a1))),f3(x14042,f2(a4,x14042)))), % 189.69/189.74 inference(scs_inference,[],[13,1107,1401,2,3])). % 189.69/189.74 cnf(1407,plain, % 189.69/189.74 (E(f3(x14071,f2(x14071,f2(a4,a1))),f3(x14072,f2(a4,x14072)))), % 189.69/189.74 inference(scs_inference,[],[13,1123,1404,2,3])). % 189.69/189.74 cnf(1410,plain, % 189.69/189.74 (E(f3(x14101,f2(x14101,f2(a1,f2(a7,a1)))),f3(x14102,f2(a4,x14102)))), % 189.69/189.74 inference(scs_inference,[],[13,1148,1407,2,3])). % 189.69/189.74 cnf(1413,plain, % 189.69/189.74 (E(f3(x14131,f2(x14131,f2(a7,a1))),f3(x14132,f2(a4,x14132)))), % 189.69/189.74 inference(scs_inference,[],[13,1180,1410,2,3])). % 189.69/189.74 cnf(1416,plain, % 189.69/189.74 (E(f3(x14161,f2(x14161,f2(a1,f2(a7,a1)))),f2(a1,f2(a1,a4)))), % 189.69/189.74 inference(scs_inference,[],[13,930,1413,2,3])). % 189.69/189.74 cnf(1419,plain, % 189.69/189.74 (E(f3(x14191,f2(x14191,f2(a1,f2(a8,a1)))),f2(a1,f2(a7,a1)))), % 189.69/189.74 inference(scs_inference,[],[13,669,1416,2,3])). % 189.69/189.74 cnf(1422,plain, % 189.69/189.74 (E(f3(x14221,f2(x14221,f2(a1,f2(a8,a1)))),f2(a1,f2(a1,a7)))), % 189.69/189.74 inference(scs_inference,[],[13,678,1419,2,3])). % 189.69/189.74 cnf(1425,plain, % 189.69/189.74 (E(f3(x14251,f2(x14251,f2(a1,f2(a8,a1)))),f6(a4,f2(a1,a1)))), % 189.69/189.74 inference(scs_inference,[],[13,1006,1422,2,3])). % 189.69/189.74 cnf(1428,plain, % 189.69/189.74 (E(f3(x14281,f2(x14281,f2(a1,f2(a7,a1)))),f6(a4,f2(a1,a1)))), % 189.69/189.74 inference(scs_inference,[],[13,1031,1425,2,3])). % 189.69/189.74 cnf(1431,plain, % 189.69/189.74 (E(f3(x14311,f2(x14311,f2(a7,a1))),f6(a4,f2(a1,a1)))), % 189.69/189.74 inference(scs_inference,[],[13,1074,1428,2,3])). % 189.69/189.74 cnf(1433,plain, % 189.69/189.74 (E(f6(a4,f2(a1,a1)),f3(x14331,f2(x14331,f2(a7,a1))))), % 189.69/189.74 inference(scs_inference,[],[1431,2])). % 189.69/189.74 cnf(1434,plain, % 189.69/189.74 (E(f3(x14341,f2(x14341,f2(a4,a1))),f6(a4,f2(a1,a1)))), % 189.69/189.74 inference(scs_inference,[],[13,1082,1431,2,3])). % 189.69/189.74 cnf(1436,plain, % 189.69/189.74 (E(f6(a4,f2(a1,a1)),f3(x14361,f2(x14361,f2(a4,a1))))), % 189.69/189.74 inference(scs_inference,[],[1434,2])). % 189.69/189.74 cnf(1780,plain, % 189.69/189.74 (E(f3(a7,x17801),f3(a5,x17801))), % 189.69/189.74 inference(scs_inference,[],[317,6,7,8])). % 189.69/189.74 cnf(1781,plain, % 189.69/189.74 (E(f3(x17811,a7),f3(x17811,a5))), % 189.69/189.74 inference(scs_inference,[],[317,6,7,8,9])). % 189.69/189.74 cnf(1783,plain, % 189.69/189.74 (E(f2(x17831,a7),f2(x17831,a5))), % 189.69/189.74 inference(scs_inference,[],[317,6,7,8,9,4,5])). % 189.69/189.74 cnf(1785,plain, % 189.69/189.74 (~E(f6(f2(f2(f2(a9,a10),a7),x17851),x17851),f2(a9,f2(a10,a7)))), % 189.69/189.74 inference(scs_inference,[],[23,317,41,6,7,8,9,4,5,2,3])). % 189.69/189.74 cnf(1787,plain, % 189.69/189.74 (E(f6(x17871,f2(a8,a1)),f6(x17871,a7))), % 189.69/189.74 inference(scs_inference,[],[358,7])). % 189.69/189.74 cnf(1788,plain, % 189.69/189.74 (E(f6(f2(a8,a1),x17881),f6(a7,x17881))), % 189.69/189.74 inference(scs_inference,[],[358,7,6])). % 189.69/189.74 cnf(1789,plain, % 189.69/189.74 (E(f3(f2(a8,a1),x17891),f3(a7,x17891))), % 189.69/189.74 inference(scs_inference,[],[358,7,6,8])). % 189.69/189.74 cnf(1790,plain, % 189.69/189.74 (E(f3(x17901,f2(a8,a1)),f3(x17901,a7))), % 189.69/189.74 inference(scs_inference,[],[358,7,6,8,9])). % 189.69/189.74 cnf(1791,plain, % 189.69/189.74 (E(f2(x17911,f2(a8,a1)),f2(x17911,a7))), % 189.69/189.74 inference(scs_inference,[],[358,7,6,8,9,5])). % 189.69/189.74 cnf(1792,plain, % 189.69/189.74 (E(f2(f2(a8,a1),x17921),f2(a7,x17921))), % 189.69/189.74 inference(scs_inference,[],[358,7,6,8,9,5,4])). % 189.69/189.74 cnf(1804,plain, % 189.69/189.74 (~E(f2(f2(a9,a10),a5),f2(a9,f2(a10,a7)))), % 189.69/189.74 inference(scs_inference,[],[23,361,1783,40,6,7,8,9,4,5,2,3])). % 189.69/189.74 cnf(1808,plain, % 189.69/189.74 (E(f3(f3(a7,x18081),x18082),f3(f3(a5,x18081),x18082))), % 189.69/189.74 inference(scs_inference,[],[1780,7,6,8])). % 189.69/189.74 cnf(1813,plain, % 189.69/189.74 (E(f3(a7,a7),f3(a5,a5))), % 189.69/189.74 inference(scs_inference,[],[1780,1781,1804,7,6,8,9,5,4,2,3])). % 189.69/189.74 cnf(1841,plain, % 189.69/189.74 (~E(f2(f2(a9,a10),a5),f2(a1,f2(a9,f2(a10,a7))))), % 189.69/189.74 inference(scs_inference,[],[1813,28,1783,6,7,8,9,4,5,2,3])). % 189.69/189.74 cnf(1850,plain, % 189.69/189.74 (~E(f6(f2(f2(f2(a9,a10),a7),f2(a8,a1)),a7),f2(a9,f2(a10,a7)))), % 189.69/189.74 inference(scs_inference,[],[1787,1841,1785,7,6,8,9,5,4,2,3])). % 189.69/189.74 cnf(1860,plain, % 189.69/189.74 (~E(a8,f3(f2(a9,a10),f2(a9,f2(a10,a7))))), % 189.69/189.74 inference(scs_inference,[],[1788,1850,257,36,6,7,8,9,4,5,2,3])). % 189.69/189.74 cnf(1868,plain, % 189.69/189.74 (E(f3(f2(a8,a1),f2(a8,a1)),f3(a7,a7))), % 189.69/189.74 inference(scs_inference,[],[1789,1790,1860,7,6,8,9,5,4,2,3])). % 189.69/189.74 cnf(1875,plain, % 189.69/189.74 (E(f2(f3(f2(a8,a1),f2(a8,a1)),x18751),f2(f3(a7,a7),x18751))), % 189.69/189.74 inference(scs_inference,[],[1868,6,7,8,9,4])). % 189.69/189.74 cnf(1878,plain, % 189.69/189.74 (~E(f2(a4,a1),f3(f2(a9,a10),f2(a9,f2(a10,a7))))), % 189.69/189.74 inference(scs_inference,[],[1868,31,1102,1860,6,7,8,9,4,5,2,3])). % 189.69/189.74 cnf(1886,plain, % 189.69/189.74 (E(f2(f2(a8,a1),f2(a8,a1)),f2(a7,a7))), % 189.69/189.74 inference(scs_inference,[],[1791,1792,1878,7,6,8,9,5,4,2,3])). % 189.69/189.74 cnf(1895,plain, % 189.69/189.74 (~E(f2(x18951,f3(x18951,f2(a9,f2(a10,a7)))),f2(f2(a9,a10),a7))), % 189.69/189.74 inference(scs_inference,[],[1886,34,6,7,8,9,4,5,2])). % 189.69/189.74 cnf(1964,plain, % 189.69/189.74 (~E(f6(f2(f2(a9,f2(a10,a7)),x19641),x19641),f2(f2(a9,a10),a7))), % 189.69/189.74 inference(scs_inference,[],[1808,42,6,7,8,9,5,4,2])). % 189.69/189.74 cnf(2168,plain, % 189.69/189.74 (~E(f6(a4,f2(a1,a1)),f3(f2(a9,a10),f2(a9,f2(a10,a7))))), % 189.69/189.74 inference(scs_inference,[],[1256,247,36,6,7,8,9,4,5,3])). % 189.69/189.74 cnf(2183,plain, % 189.69/189.74 (~E(f3(x21831,f2(x21831,f2(a7,a1))),f3(f2(a9,a10),f2(a9,f2(a10,a7))))), % 189.69/189.74 inference(scs_inference,[],[331,2168,1433,6,7,8,9,4,5,3])). % 189.69/189.74 cnf(2222,plain, % 189.69/189.74 (E(f6(a4,x22221),f6(a7,x22221))), % 189.69/189.74 inference(scs_inference,[],[273,6])). % 189.69/189.74 cnf(2223,plain, % 189.69/189.74 (E(f6(x22231,a4),f6(x22231,a7))), % 189.69/189.74 inference(scs_inference,[],[273,6,7])). % 189.69/189.74 cnf(2224,plain, % 189.69/189.74 (E(f3(x22241,a4),f3(x22241,a7))), % 189.69/189.74 inference(scs_inference,[],[273,6,7,9])). % 189.69/189.74 cnf(2225,plain, % 189.69/189.74 (E(f3(a4,x22251),f3(a7,x22251))), % 189.69/189.74 inference(scs_inference,[],[273,6,7,9,8])). % 189.69/189.74 cnf(2226,plain, % 189.69/189.74 (E(f2(a4,x22261),f2(a7,x22261))), % 189.69/189.74 inference(scs_inference,[],[273,6,7,9,8,4])). % 189.69/189.74 cnf(2227,plain, % 189.69/189.74 (E(f2(x22271,a4),f2(x22271,a7))), % 189.69/189.74 inference(scs_inference,[],[273,6,7,9,8,4,5])). % 189.69/189.74 cnf(2228,plain, % 189.69/189.74 (~E(f2(f3(a7,a7),f3(f3(f2(a8,a1),f2(a8,a1)),f2(a9,f2(a10,a7)))),f2(f2(a9,a10),a7))), % 189.69/189.74 inference(scs_inference,[],[1875,273,1895,6,7,9,8,4,5,3])). % 189.69/189.74 cnf(2234,plain, % 189.69/189.74 (E(f3(f6(a4,x22341),x22342),f3(f6(a7,x22341),x22342))), % 189.69/189.74 inference(scs_inference,[],[2222,6,7,9,8])). % 189.69/189.74 cnf(2238,plain, % 189.69/189.74 (~E(f2(a7,a1),f3(f2(a9,a10),f2(a9,f2(a10,a7))))), % 189.69/189.74 inference(scs_inference,[],[2222,2226,2228,1878,6,7,9,8,5,4,2,3])). % 189.69/189.74 cnf(2247,plain, % 189.69/189.74 (~E(f6(f2(f2(a9,f2(a10,a7)),a4),a7),f2(f2(a9,a10),a7))), % 189.69/189.74 inference(scs_inference,[],[2223,2238,1964,6,7,9,8,4,5,2,3])). % 189.69/189.74 cnf(2257,plain, % 189.69/189.74 (~E(f3(x22571,f2(x22571,f2(a4,a1))),f3(f2(a9,a10),f2(a9,f2(a10,a7))))), % 189.69/189.74 inference(scs_inference,[],[2224,1436,2247,2168,6,7,8,9,5,4,2,3])). % 189.69/189.74 cnf(2265,plain, % 189.69/189.74 (~E(f3(a7,f2(a4,f2(a4,a1))),f3(f2(a9,a10),f2(a9,f2(a10,a7))))), % 189.69/189.74 inference(scs_inference,[],[2225,2257,4,9,5,2,8,7,6,3])). % 189.69/189.74 cnf(2275,plain, % 189.69/189.74 (~E(f3(f6(a7,x22751),f2(f6(a4,x22751),f2(a7,a1))),f3(f2(a9,a10),f2(a9,f2(a10,a7))))), % 189.69/189.74 inference(scs_inference,[],[10,2234,2265,2183,9,4,2,5,8,6,7,3])). % 189.69/189.74 cnf(2281,plain, % 189.69/189.74 (E(f2(x22811,f2(x22812,a4)),f2(x22811,f2(x22812,a7)))), % 189.69/189.74 inference(scs_inference,[],[2227,2275,9,4,2,5])). % 189.69/189.74 cnf(3833,plain, % 189.69/189.74 (E(f2(x38331,a7),f2(x38331,a4))), % 189.69/189.74 inference(scs_inference,[],[2227,369,7,2])). % 189.69/189.74 cnf(4291,plain, % 189.69/189.74 (~E(f2(f2(a9,a10),a4),f2(a9,f2(a10,a7)))), % 189.69/189.74 inference(scs_inference,[],[23,373,3833,9,5,8,6,4,7,3])). % 189.69/189.74 cnf(4300,plain, % 189.69/189.74 ($false), % 189.69/189.74 inference(scs_inference,[],[18,1325,4291,2281,9,5,8,6,4,7,3]), % 189.69/189.74 ['proof']). % 189.69/189.74 % SZS output end Proof % 189.69/189.74 % Total time :189.050000s %------------------------------------------------------------------------------