%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : ALG235-1 : TPTP v8.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n012.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 03:41:10 EDT 2024 % Result : Unsatisfiable 230.44s 230.75s % Output : CNFRefutation 230.51s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.09 % Problem : ALG235-1 : TPTP v8.2.0. Released v4.0.0. % 0.00/0.09 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.08/0.29 % Computer : n012.cluster.edu % 0.08/0.29 % Model : x86_64 x86_64 % 0.08/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.29 % Memory : 8042.1875MB % 0.08/0.29 % OS : Linux 3.10.0-693.el7.x86_64 % 0.08/0.29 % CPULimit : 300 % 0.08/0.29 % WCLimit : 300 % 0.08/0.29 % DateTime : Wed Jun 19 16:24:09 EDT 2024 % 0.08/0.29 % CPUTime : % 0.14/0.52 start to proof:theBenchmark % 230.44/230.73 %------------------------------------------- % 230.44/230.73 % File :CSE---1.7 % 230.44/230.73 % Problem :theBenchmark % 230.44/230.73 % Transform :cnf % 230.44/230.73 % Format :tptp:raw % 230.44/230.73 % Command :java -jar mcs_scs.jar %d %s % 230.44/230.73 % 230.44/230.73 % Result :Theorem 229.900000s % 230.44/230.73 % Output :CNFRefutation 229.900000s % 230.44/230.73 %------------------------------------------- % 230.44/230.75 %------------------------------------------------------------------------------ % 230.44/230.75 % File : ALG235-1 : TPTP v8.2.0. Released v4.0.0. % 230.44/230.75 % Domain : Algebra (Non-associative) % 230.44/230.75 % Problem : Short equational base for two varieties of groupoids - part 1a % 230.44/230.75 % Version : Especial. % 230.44/230.75 % English : % 230.44/230.75 % 230.44/230.75 % Refs : [Phi06] Phillips (2006), Short Equational Bases for Two Variet % 230.44/230.75 % : [PS08] Phillips & Stanovsky (2008), Using Automated Theorem P % 230.44/230.75 % : [Sta08] Stanovsky (2008), Email to G. Sutcliffe % 230.44/230.75 % Source : [Sta08] % 230.44/230.75 % Names : P06_1a [Sta08] % 230.44/230.75 % 230.44/230.75 % Status : Unsatisfiable % 230.44/230.75 % Rating : 0.00 v8.2.0, 0.04 v8.1.0, 0.10 v7.5.0, 0.04 v7.4.0, 0.17 v7.3.0, 0.05 v7.1.0, 0.00 v7.0.0, 0.05 v6.4.0, 0.11 v6.3.0, 0.12 v6.2.0, 0.14 v6.1.0, 0.00 v6.0.0, 0.10 v5.5.0, 0.11 v5.4.0, 0.00 v5.2.0, 0.07 v5.0.0, 0.14 v4.1.0, 0.18 v4.0.1, 0.21 v4.0.0 % 230.44/230.75 % Syntax : Number of clauses : 4 ( 4 unt; 0 nHn; 1 RR) % 230.44/230.75 % Number of literals : 4 ( 4 equ; 1 neg) % 230.44/230.75 % Maximal clause size : 1 ( 1 avg) % 230.44/230.75 % Maximal term depth : 6 ( 2 avg) % 230.44/230.75 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty) % 230.44/230.75 % Number of functors : 5 ( 5 usr; 4 con; 0-2 aty) % 230.44/230.75 % Number of variables : 10 ( 0 sgn) % 230.44/230.75 % SPC : CNF_UNS_RFO_PEQ_UEQ % 230.44/230.75 % 230.44/230.75 % Comments : % 230.44/230.75 %------------------------------------------------------------------------------ % 230.44/230.75 cnf(c01,axiom, % 230.44/230.75 mult(A,mult(B,mult(A,B))) = mult(A,B) ). % 230.44/230.75 % 230.44/230.75 cnf(c02,axiom, % 230.44/230.75 mult(A,mult(B,mult(C,D))) = mult(C,mult(B,mult(A,D))) ). % 230.44/230.75 % 230.44/230.75 cnf(c03,axiom, % 230.44/230.75 mult(mult(A,mult(B,mult(C,B))),D) = mult(A,mult(D,mult(mult(C,B),D))) ). % 230.44/230.75 % 230.44/230.75 cnf(goals,negated_conjecture, % 230.44/230.75 mult(a,mult(b,mult(a,mult(c,mult(d,c))))) != mult(a,mult(b,mult(d,c))) ). % 230.44/230.75 % 230.44/230.75 %------------------------------------------------------------------------------ % 230.44/230.75 %------------------------------------------- % 230.44/230.75 % Proof found % 230.44/230.75 % SZS status Theorem for theBenchmark % 230.44/230.75 % SZS output start Proof % 230.51/230.77 %ClaNum:9(EqnAxiom:5) % 230.51/230.77 %VarNum:24(SingletonVarNum:10) % 230.51/230.77 %MaxLitNum:1 % 230.51/230.77 %MaxfuncDepth:5 % 230.51/230.77 %SharedTerms:12 % 230.51/230.77 %goalClause: 9 % 230.51/230.77 %singleGoalClaCount:1 % 230.51/230.77 [9]~E(f1(a2,f1(a3,f1(a2,f1(a4,f1(a5,a4))))),f1(a2,f1(a3,f1(a5,a4)))) % 230.51/230.77 [6]E(f1(x61,f1(x62,f1(x61,x62))),f1(x61,x62)) % 230.51/230.77 [7]E(f1(x71,f1(x72,f1(x73,x74))),f1(x73,f1(x72,f1(x71,x74)))) % 230.51/230.77 [8]E(f1(f1(x81,f1(x82,f1(x83,x82))),x84),f1(x81,f1(x84,f1(f1(x83,x82),x84)))) % 230.51/230.77 %EqnAxiom % 230.51/230.77 [1]E(x11,x11) % 230.51/230.77 [2]E(x22,x21)+~E(x21,x22) % 230.51/230.77 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 230.51/230.77 [4]~E(x41,x42)+E(f1(x41,x43),f1(x42,x43)) % 230.51/230.77 [5]~E(x51,x52)+E(f1(x53,x51),f1(x53,x52)) % 230.51/230.77 % 230.51/230.77 %------------------------------------------- % 230.51/230.80 cnf(10,plain, % 230.51/230.80 (E(f1(x101,x102),f1(x101,f1(x102,f1(x101,x102))))), % 230.51/230.80 inference(scs_inference,[],[6,2])). % 230.51/230.80 cnf(11,plain, % 230.51/230.80 (~E(f1(a3,f1(a2,f1(a4,f1(a5,a4)))),f1(a3,f1(a5,a4)))), % 230.51/230.80 inference(scs_inference,[],[9,6,2,5])). % 230.51/230.80 cnf(12,plain, % 230.51/230.80 (~E(f1(a2,f1(a3,f1(a2,f1(a4,f1(a5,a4))))),f1(a5,f1(a3,f1(a2,a4))))), % 230.51/230.80 inference(scs_inference,[],[9,6,7,2,5,3])). % 230.51/230.80 cnf(14,plain, % 230.51/230.80 (~E(f1(a2,f1(a4,f1(a5,a4))),f1(a5,a4))), % 230.51/230.80 inference(scs_inference,[],[11,5])). % 230.51/230.80 cnf(15,plain, % 230.51/230.80 (E(f1(x151,f1(x152,f1(f1(x153,x154),x152))),f1(f1(x151,f1(x154,f1(x153,x154))),x152))), % 230.51/230.80 inference(scs_inference,[],[11,8,5,2])). % 230.51/230.80 cnf(16,plain, % 230.51/230.80 (E(f1(f1(x161,x162),x163),f1(f1(f1(x161,x162),f1(x162,f1(x161,x162))),x163))), % 230.51/230.80 inference(scs_inference,[],[10,11,8,5,2,3])). % 230.51/230.80 cnf(18,plain, % 230.51/230.80 (E(f1(f1(f1(x181,x182),f1(x182,f1(x181,x182))),x183),f1(f1(x181,x182),x183))), % 230.51/230.80 inference(scs_inference,[],[16,2])). % 230.51/230.80 cnf(19,plain, % 230.51/230.80 (E(f1(f1(x191,x192),f1(x193,f1(x194,x193))),f1(f1(x194,f1(x192,f1(x191,x192))),x193))), % 230.51/230.80 inference(scs_inference,[],[7,15,3])). % 230.51/230.80 cnf(22,plain, % 230.51/230.80 (E(f1(f1(x221,f1(x222,f1(x223,x222))),x224),f1(f1(x223,x222),f1(x224,f1(x221,x224))))), % 230.51/230.80 inference(scs_inference,[],[7,15,3,2])). % 230.51/230.80 cnf(23,plain, % 230.51/230.80 (E(f1(x231,f1(x232,f1(x233,x234))),f1(x233,f1(f1(x232,f1(x231,x234)),f1(x233,f1(x232,f1(x231,x234))))))), % 230.51/230.80 inference(scs_inference,[],[7,10,3])). % 230.51/230.80 cnf(25,plain, % 230.51/230.80 (E(f1(x251,f1(f1(x252,f1(x253,x254)),f1(x251,f1(x252,f1(x253,x254))))),f1(x253,f1(x252,f1(x251,x254))))), % 230.51/230.80 inference(scs_inference,[],[7,10,3,2])). % 230.51/230.80 cnf(26,plain, % 230.51/230.80 (E(f1(x261,f1(x262,f1(f1(x263,x264),x265))),f1(f1(f1(x263,x264),f1(x264,f1(x263,x264))),f1(x262,f1(x261,x265))))), % 230.51/230.80 inference(scs_inference,[],[7,16,3])). % 230.51/230.80 cnf(29,plain, % 230.51/230.80 (E(f1(f1(f1(x291,x292),f1(x292,f1(x291,x292))),f1(x293,f1(x294,x295))),f1(x294,f1(x293,f1(f1(x291,x292),x295))))), % 230.51/230.80 inference(scs_inference,[],[7,16,3,2])). % 230.51/230.80 cnf(30,plain, % 230.51/230.80 (E(f1(f1(x301,f1(x302,f1(x303,x302))),x304),f1(f1(f1(x303,x302),f1(x302,f1(x303,x302))),f1(x304,f1(x301,x304))))), % 230.51/230.80 inference(scs_inference,[],[8,26,3])). % 230.51/230.80 cnf(32,plain, % 230.51/230.80 (E(f1(f1(f1(x321,x322),f1(x322,f1(x321,x322))),f1(x323,f1(x324,x323))),f1(f1(x324,f1(x322,f1(x321,x322))),x323))), % 230.51/230.80 inference(scs_inference,[],[8,26,3,2])). % 230.51/230.80 cnf(33,plain, % 230.51/230.80 (E(f1(f1(f1(x331,x332),f1(x333,f1(x334,x333))),x335),f1(f1(f1(x334,x333),f1(x332,f1(x331,x332))),x335))), % 230.51/230.80 inference(scs_inference,[],[8,19,3])). % 230.51/230.80 cnf(36,plain, % 230.51/230.80 (E(f1(x361,x362),f1(x361,f1(f1(x362,f1(x361,x362)),f1(x361,f1(x362,f1(x361,x362))))))), % 230.51/230.80 inference(scs_inference,[],[10,23,3])). % 230.51/230.80 cnf(38,plain, % 230.51/230.80 (E(f1(x381,f1(f1(x382,f1(x381,x382)),f1(x381,f1(x382,f1(x381,x382))))),f1(x381,x382))), % 230.51/230.80 inference(scs_inference,[],[10,23,3,2])). % 230.51/230.80 cnf(39,plain, % 230.51/230.80 (E(f1(f1(x391,x392),x393),f1(f1(f1(x391,x392),f1(x392,f1(x391,x392))),f1(x393,f1(f1(x391,x392),x393))))), % 230.51/230.80 inference(scs_inference,[],[10,26,3])). % 230.51/230.80 cnf(42,plain, % 230.51/230.80 (E(f1(f1(f1(x421,x422),f1(x422,f1(x421,x422))),f1(x423,f1(f1(x421,x422),x423))),f1(f1(x421,x422),x423))), % 230.51/230.80 inference(scs_inference,[],[10,26,3,2])). % 230.51/230.80 cnf(43,plain, % 230.51/230.80 (~E(f1(a3,f1(a2,f1(a4,f1(a5,a4)))),f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))))), % 230.51/230.80 inference(scs_inference,[],[11,6,3])). % 230.51/230.80 cnf(45,plain, % 230.51/230.80 (~E(f1(a2,f1(a4,f1(a5,a4))),f1(f1(a5,a4),f1(a3,f1(a5,a4))))), % 230.51/230.80 inference(scs_inference,[],[11,6,3,5])). % 230.51/230.80 cnf(46,plain, % 230.51/230.80 (~E(f1(a2,f1(a4,f1(a5,a4))),f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4))))), % 230.51/230.80 inference(scs_inference,[],[18,45,3])). % 230.51/230.80 cnf(48,plain, % 230.51/230.80 (~E(f1(a2,f1(a4,f1(a5,a4))),f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4))))))), % 230.51/230.80 inference(scs_inference,[],[15,46,3])). % 230.51/230.80 cnf(50,plain, % 230.51/230.80 (~E(f1(a2,f1(a4,f1(a5,a4))),f1(a5,f1(a3,f1(f1(a5,a4),a4))))), % 230.51/230.80 inference(scs_inference,[],[23,48,3])). % 230.51/230.81 cnf(52,plain, % 230.51/230.81 (~E(f1(a2,f1(a4,f1(a5,a4))),f1(a5,f1(f1(a4,f1(a5,a4)),f1(a5,f1(a4,f1(a5,a4))))))), % 230.51/230.81 inference(scs_inference,[],[14,38,3])). % 230.51/230.81 cnf(54,plain, % 230.51/230.81 (~E(f1(a2,f1(a4,f1(a5,a4))),f1(a5,f1(a4,f1(a5,a4))))), % 230.51/230.81 inference(scs_inference,[],[23,52,3])). % 230.51/230.81 cnf(56,plain, % 230.51/230.81 (~E(a2,a5)), % 230.51/230.81 inference(scs_inference,[],[23,52,3,4])). % 230.51/230.81 cnf(57,plain, % 230.51/230.81 (~E(f1(a2,f1(a4,f1(a5,a4))),f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4))))))), % 230.51/230.81 inference(scs_inference,[],[42,45,3])). % 230.51/230.81 cnf(59,plain, % 230.51/230.81 (~E(f1(a2,f1(a3,f1(a2,f1(a4,f1(a5,a4))))),f1(a5,f1(f1(a3,f1(a2,a4)),f1(a5,f1(a3,f1(a2,a4))))))), % 230.51/230.81 inference(scs_inference,[],[25,9,3])). % 230.51/230.81 cnf(61,plain, % 230.51/230.81 (~E(f1(a2,f1(a3,f1(a2,f1(a4,f1(a5,a4))))),f1(a2,f1(f1(a3,f1(a5,a4)),f1(a2,f1(a3,f1(a5,a4))))))), % 230.51/230.81 inference(scs_inference,[],[9,6,3])). % 230.51/230.81 cnf(63,plain, % 230.51/230.81 (~E(f1(a3,f1(a2,f1(a4,f1(a5,a4)))),f1(f1(a3,f1(a5,a4)),f1(a2,f1(a3,f1(a5,a4)))))), % 230.51/230.81 inference(scs_inference,[],[9,6,3,5])). % 230.51/230.81 cnf(64,plain, % 230.51/230.81 (~E(f1(a2,f1(a4,f1(a5,a4))),f1(f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4))))), % 230.51/230.81 inference(scs_inference,[],[57,8,3])). % 230.51/230.81 cnf(66,plain, % 230.51/230.81 (~E(f1(a2,f1(a4,f1(a5,a4))),f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(f1(a3,f1(a5,a4)),f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4))))))), % 230.51/230.81 inference(scs_inference,[],[32,64,3])). % 230.51/230.81 cnf(68,plain, % 230.51/230.81 (~E(f1(a2,f1(a4,f1(a5,a4))),f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4))))))), % 230.51/230.81 inference(scs_inference,[],[16,66,3])). % 230.51/230.81 cnf(70,plain, % 230.51/230.81 (~E(f1(a3,f1(a2,f1(a4,f1(a5,a4)))),f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a2,f1(a3,f1(a5,a4)))))), % 230.51/230.81 inference(scs_inference,[],[18,63,3])). % 230.51/230.81 cnf(72,plain, % 230.51/230.81 (~E(f1(a3,f1(a2,f1(a4,f1(a5,a4)))),f1(a3,f1(a2,f1(f1(a3,f1(a5,a4)),f1(a5,a4)))))), % 230.51/230.81 inference(scs_inference,[],[26,70,3])). % 230.51/230.81 cnf(74,plain, % 230.51/230.81 (~E(f1(a2,f1(a4,f1(a5,a4))),f1(a2,f1(f1(a3,f1(a5,a4)),f1(a5,a4))))), % 230.51/230.81 inference(scs_inference,[],[26,70,3,5])). % 230.51/230.81 cnf(75,plain, % 230.51/230.81 (~E(f1(a4,f1(a5,a4)),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))), % 230.51/230.81 inference(scs_inference,[],[74,5])). % 230.51/230.81 cnf(76,plain, % 230.51/230.81 (~E(a4,f1(a3,f1(a5,a4)))), % 230.51/230.81 inference(scs_inference,[],[74,5,4])). % 230.51/230.81 cnf(77,plain, % 230.51/230.81 (~E(f1(a4,f1(a5,a4)),f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))))), % 230.51/230.81 inference(scs_inference,[],[42,75,3])). % 230.51/230.81 cnf(79,plain, % 230.51/230.81 (~E(f1(a4,f1(a5,a4)),f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))))), % 230.51/230.81 inference(scs_inference,[],[16,77,3])). % 230.51/230.81 cnf(81,plain, % 230.51/230.81 (~E(f1(a4,f1(a5,a4)),f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)))), % 230.51/230.81 inference(scs_inference,[],[22,79,3])). % 230.51/230.81 cnf(83,plain, % 230.51/230.81 (~E(a4,f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))))), % 230.51/230.81 inference(scs_inference,[],[22,79,3,4])). % 230.51/230.81 cnf(84,plain, % 230.51/230.81 (~E(a4,f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)))), % 230.51/230.81 inference(scs_inference,[],[22,83,3])). % 230.51/230.81 cnf(86,plain, % 230.51/230.81 (~E(f1(a3,f1(a2,f1(a4,f1(a5,a4)))),f1(a3,f1(f1(f1(a5,a4),f1(a3,f1(a5,a4))),f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))))))), % 230.51/230.81 inference(scs_inference,[],[43,6,3])). % 230.51/230.81 cnf(88,plain, % 230.51/230.81 (~E(f1(a2,f1(a4,f1(a5,a4))),f1(f1(f1(a5,a4),f1(a3,f1(a5,a4))),f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4))))))), % 230.51/230.81 inference(scs_inference,[],[43,6,3,5])). % 230.51/230.81 cnf(89,plain, % 230.51/230.81 (~E(f1(a2,f1(a4,f1(a5,a4))),f1(a5,f1(f1(a3,f1(f1(a5,a4),a4)),f1(a5,f1(a3,f1(f1(a5,a4),a4))))))), % 230.51/230.81 inference(scs_inference,[],[45,25,3])). % 230.51/230.81 cnf(91,plain, % 230.51/230.81 (E(f1(f1(x911,f1(x912,f1(x911,x912))),x913),f1(f1(x911,x912),x913))), % 230.51/230.81 inference(scs_inference,[],[6,4])). % 230.51/230.81 cnf(92,plain, % 230.51/230.81 (E(f1(x921,f1(x922,f1(x923,f1(x922,x923)))),f1(x921,f1(x922,x923)))), % 230.51/230.81 inference(scs_inference,[],[6,4,5])). % 230.51/230.81 cnf(94,plain, % 230.51/230.81 (~E(a4,f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))))), % 230.51/230.81 inference(scs_inference,[],[6,56,76,4,5,2,3])). % 230.51/230.81 cnf(96,plain, % 230.51/230.81 (E(f1(f1(f1(x961,f1(x962,f1(x961,x962))),x963),x964),f1(f1(f1(x961,x962),x963),x964))), % 230.51/230.81 inference(scs_inference,[],[91,4])). % 230.51/230.81 cnf(97,plain, % 230.51/230.81 (E(f1(x971,f1(f1(x972,f1(x973,f1(x972,x973))),x974)),f1(x971,f1(f1(x972,x973),x974)))), % 230.51/230.81 inference(scs_inference,[],[91,4,5])). % 230.51/230.81 cnf(98,plain, % 230.51/230.81 (~E(f1(a5,f1(a4,f1(a5,a4))),f1(a2,f1(a4,f1(a5,a4))))), % 230.51/230.81 inference(scs_inference,[],[54,91,4,5,2])). % 230.51/230.81 cnf(99,plain, % 230.51/230.81 (~E(f1(a5,a4),f1(a2,f1(a4,f1(a5,a4))))), % 230.51/230.81 inference(scs_inference,[],[6,54,91,4,5,2,3])). % 230.51/230.81 cnf(101,plain, % 230.51/230.81 (E(f1(f1(x1011,f1(x1012,f1(x1013,f1(x1012,x1013)))),x1014),f1(f1(x1011,f1(x1012,x1013)),x1014))), % 230.51/230.81 inference(scs_inference,[],[92,4])). % 230.51/230.81 cnf(102,plain, % 230.51/230.81 (E(f1(x1021,f1(x1022,f1(x1023,f1(x1024,f1(x1023,x1024))))),f1(x1021,f1(x1022,f1(x1023,x1024))))), % 230.51/230.81 inference(scs_inference,[],[92,4,5])). % 230.51/230.81 cnf(103,plain, % 230.51/230.81 (~E(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),a4)), % 230.51/230.81 inference(scs_inference,[],[94,92,4,5,2])). % 230.51/230.81 cnf(104,plain, % 230.51/230.81 (~E(f1(a5,f1(f1(a4,f1(a5,a4)),f1(a5,f1(a4,f1(a5,a4))))),f1(a2,f1(a4,f1(a5,a4))))), % 230.51/230.81 inference(scs_inference,[],[99,94,92,36,4,5,2,3])). % 230.51/230.81 cnf(106,plain, % 230.51/230.81 (E(f1(f1(f1(x1061,x1062),x1063),x1064),f1(f1(f1(f1(x1061,x1062),f1(x1062,f1(x1061,x1062))),f1(x1063,f1(f1(x1061,x1062),x1063))),x1064))), % 230.51/230.81 inference(scs_inference,[],[39,4])). % 230.51/230.81 cnf(107,plain, % 230.51/230.81 (E(f1(x1071,f1(f1(x1072,x1073),x1074)),f1(x1071,f1(f1(f1(x1072,x1073),f1(x1073,f1(x1072,x1073))),f1(x1074,f1(f1(x1072,x1073),x1074)))))), % 230.51/230.81 inference(scs_inference,[],[39,4,5])). % 230.51/230.81 cnf(108,plain, % 230.51/230.81 (~E(f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)),a4)), % 230.51/230.81 inference(scs_inference,[],[84,39,4,5,2])). % 230.51/230.81 cnf(109,plain, % 230.51/230.81 (~E(f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),a4)), % 230.51/230.81 inference(scs_inference,[],[84,39,30,4,5,2,3])). % 230.51/230.81 cnf(111,plain, % 230.51/230.81 (E(f1(f1(f1(f1(x1111,x1112),f1(x1112,f1(x1111,x1112))),f1(x1113,f1(x1114,x1115))),x1116),f1(f1(x1114,f1(x1113,f1(f1(x1111,x1112),x1115))),x1116))), % 230.51/230.81 inference(scs_inference,[],[29,4])). % 230.51/230.81 cnf(112,plain, % 230.51/230.81 (E(f1(x1121,f1(f1(f1(x1122,x1123),f1(x1123,f1(x1122,x1123))),f1(x1124,f1(x1125,x1126)))),f1(x1121,f1(x1125,f1(x1124,f1(f1(x1122,x1123),x1126)))))), % 230.51/230.81 inference(scs_inference,[],[29,4,5])). % 230.51/230.81 cnf(113,plain, % 230.51/230.81 (~E(f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)),f1(a4,f1(a5,a4)))), % 230.51/230.81 inference(scs_inference,[],[81,29,4,5,2])). % 230.51/230.81 cnf(114,plain, % 230.51/230.81 (~E(f1(a3,f1(a5,a4)),a4)), % 230.51/230.81 inference(scs_inference,[],[6,103,81,29,4,5,2,3])). % 230.51/230.81 cnf(117,plain, % 230.51/230.81 (E(f1(x1171,f1(f1(f1(x1172,x1173),f1(x1174,f1(x1175,x1174))),x1176)),f1(x1171,f1(f1(f1(x1175,x1174),f1(x1173,f1(x1172,x1173))),x1176)))), % 230.51/230.81 inference(scs_inference,[],[33,4,5])). % 230.51/230.81 cnf(118,plain, % 230.51/230.81 (~E(f1(a5,f1(a3,f1(f1(a5,a4),a4))),f1(a2,f1(a4,f1(a5,a4))))), % 230.51/230.81 inference(scs_inference,[],[50,33,4,5,2])). % 230.51/230.81 cnf(119,plain, % 230.51/230.81 (E(f1(f1(f1(x1191,f1(x1192,f1(x1191,x1192))),x1193),f1(x1194,f1(f1(f1(x1191,x1192),x1193),x1194))),f1(f1(f1(x1191,x1192),x1193),x1194))), % 230.51/230.81 inference(scs_inference,[],[6,50,33,96,4,5,2,3])). % 230.51/230.81 cnf(122,plain, % 230.51/230.81 (E(f1(f1(x1221,f1(f1(x1222,f1(x1223,f1(x1222,x1223))),x1224)),x1225),f1(f1(x1221,f1(f1(x1222,x1223),x1224)),x1225))), % 230.51/230.81 inference(scs_inference,[],[97,4])). % 230.51/230.81 cnf(123,plain, % 230.51/230.81 (E(f1(x1231,f1(x1232,f1(f1(x1233,f1(x1234,f1(x1233,x1234))),x1235))),f1(x1231,f1(x1232,f1(f1(x1233,x1234),x1235))))), % 230.51/230.81 inference(scs_inference,[],[97,4,5])). % 230.51/230.81 cnf(125,plain, % 230.51/230.81 (~E(a4,f1(a3,f1(f1(f1(a5,a4),f1(a3,f1(a5,a4))),f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))))))), % 230.51/230.81 inference(scs_inference,[],[6,12,97,94,4,5,2,3])). % 230.51/230.81 cnf(127,plain, % 230.51/230.81 (E(f1(f1(f1(x1271,f1(x1272,f1(x1273,f1(x1272,x1273)))),x1274),x1275),f1(f1(f1(x1271,f1(x1272,x1273)),x1274),x1275))), % 230.51/230.81 inference(scs_inference,[],[101,4])). % 230.51/230.81 cnf(128,plain, % 230.51/230.81 (E(f1(x1281,f1(f1(x1282,f1(x1283,f1(x1284,f1(x1283,x1284)))),x1285)),f1(x1281,f1(f1(x1282,f1(x1283,x1284)),x1285)))), % 230.51/230.81 inference(scs_inference,[],[101,4,5])). % 230.51/230.81 cnf(129,plain, % 230.51/230.81 (~E(a4,f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(a3,f1(a5,a4)))))), % 230.51/230.81 inference(scs_inference,[],[101,109,4,5,2])). % 230.51/230.81 cnf(130,plain, % 230.51/230.81 (E(f1(f1(x1301,f1(x1302,f1(x1303,f1(x1302,x1303)))),f1(x1304,f1(f1(x1301,f1(x1302,x1303)),x1304))),f1(f1(x1301,f1(x1302,x1303)),x1304))), % 230.51/230.81 inference(scs_inference,[],[6,101,109,4,5,2,3])). % 230.51/230.81 cnf(133,plain, % 230.51/230.81 (E(f1(f1(x1331,f1(x1332,f1(x1333,f1(x1334,f1(x1333,x1334))))),x1335),f1(f1(x1331,f1(x1332,f1(x1333,x1334))),x1335))), % 230.51/230.81 inference(scs_inference,[],[102,4])). % 230.51/230.81 cnf(134,plain, % 230.51/230.81 (E(f1(x1341,f1(x1342,f1(x1343,f1(x1344,f1(x1345,f1(x1344,x1345)))))),f1(x1341,f1(x1342,f1(x1343,f1(x1344,x1345)))))), % 230.51/230.81 inference(scs_inference,[],[102,4,5])). % 230.51/230.81 cnf(135,plain, % 230.51/230.81 (~E(f1(a3,f1(a2,f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(a3,f1(a2,f1(a4,f1(a5,a4)))))), % 230.51/230.81 inference(scs_inference,[],[102,72,4,5,2])). % 230.51/230.81 cnf(136,plain, % 230.51/230.81 (~E(a4,f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)))))), % 230.51/230.81 inference(scs_inference,[],[6,102,72,84,4,5,2,3])). % 230.51/230.81 cnf(138,plain, % 230.51/230.81 (E(f1(f1(f1(x1381,x1382),f1(x1383,f1(x1384,x1383))),x1385),f1(f1(f1(x1384,f1(x1382,f1(x1381,x1382))),x1383),x1385))), % 230.51/230.81 inference(scs_inference,[],[19,4])). % 230.51/230.81 cnf(139,plain, % 230.51/230.81 (E(f1(x1391,f1(f1(x1392,x1393),f1(x1394,f1(x1395,x1394)))),f1(x1391,f1(f1(x1395,f1(x1393,f1(x1392,x1393))),x1394)))), % 230.51/230.81 inference(scs_inference,[],[19,4,5])). % 230.51/230.81 cnf(140,plain, % 230.51/230.81 (~E(f1(f1(f1(a5,a4),f1(a3,f1(a5,a4))),f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4))))),f1(a2,f1(a4,f1(a5,a4))))), % 230.51/230.81 inference(scs_inference,[],[88,19,4,5,2])). % 230.51/230.81 cnf(141,plain, % 230.51/230.81 (E(f1(x1411,f1(f1(f1(x1412,x1413),f1(x1413,f1(x1412,x1413))),f1(x1411,f1(f1(f1(x1412,x1413),x1414),x1414)))),f1(x1411,f1(f1(x1412,x1413),x1414)))), % 230.51/230.81 inference(scs_inference,[],[6,88,112,19,4,5,2,3])). % 230.51/230.81 cnf(144,plain, % 230.51/230.81 (E(f1(f1(f1(f1(x1441,x1442),f1(x1443,f1(x1444,x1443))),x1445),x1446),f1(f1(f1(f1(x1444,f1(x1442,f1(x1441,x1442))),x1443),x1445),x1446))), % 230.51/230.81 inference(scs_inference,[],[138,4])). % 230.51/230.81 cnf(145,plain, % 230.51/230.81 (E(f1(x1451,f1(f1(f1(x1452,x1453),f1(x1454,f1(x1455,x1454))),x1456)),f1(x1451,f1(f1(f1(x1455,f1(x1453,f1(x1452,x1453))),x1454),x1456)))), % 230.51/230.81 inference(scs_inference,[],[138,4,5])). % 230.51/230.81 cnf(146,plain, % 230.51/230.81 (~E(f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4))))),f1(a2,f1(a4,f1(a5,a4))))), % 230.51/230.81 inference(scs_inference,[],[138,68,4,5,2])). % 230.51/230.81 cnf(147,plain, % 230.51/230.81 (~E(a4,f1(f1(a3,f1(a5,a4)),f1(f1(f1(a5,a4),f1(a3,f1(a5,a4))),f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))))))), % 230.51/230.81 inference(scs_inference,[],[6,138,68,83,4,5,2,3])). % 230.51/230.81 cnf(149,plain, % 230.51/230.81 (E(f1(f1(x1491,f1(x1492,f1(x1493,x1494))),x1495),f1(f1(x1493,f1(x1492,f1(x1491,x1494))),x1495))), % 230.51/230.81 inference(scs_inference,[],[7,4])). % 230.51/230.81 cnf(150,plain, % 230.51/230.81 (E(f1(x1501,f1(x1502,f1(x1503,f1(x1504,x1505)))),f1(x1501,f1(x1504,f1(x1503,f1(x1502,x1505)))))), % 230.51/230.81 inference(scs_inference,[],[7,4,5])). % 230.51/230.81 cnf(151,plain, % 230.51/230.81 (~E(f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)))),a4)), % 230.51/230.81 inference(scs_inference,[],[7,136,4,5,2])). % 230.51/230.81 cnf(152,plain, % 230.51/230.81 (E(f1(x1521,f1(f1(x1522,x1523),f1(f1(x1524,x1525),f1(x1526,f1(x1524,x1525))))),f1(x1524,f1(f1(x1526,f1(x1523,f1(x1522,x1523))),f1(x1521,x1525))))), % 230.51/230.81 inference(scs_inference,[],[7,139,136,4,5,2,3])). % 230.51/230.81 cnf(155,plain, % 230.51/230.81 (E(f1(f1(f1(x1551,f1(x1552,f1(x1553,x1554))),x1555),x1556),f1(f1(f1(x1553,f1(x1552,f1(x1551,x1554))),x1555),x1556))), % 230.51/230.81 inference(scs_inference,[],[149,4])). % 230.51/230.81 cnf(156,plain, % 230.51/230.81 (E(f1(x1561,f1(f1(x1562,f1(x1563,f1(x1564,x1565))),x1566)),f1(x1561,f1(f1(x1564,f1(x1563,f1(x1562,x1565))),x1566)))), % 230.51/230.81 inference(scs_inference,[],[149,4,5])). % 230.51/230.81 cnf(157,plain, % 230.51/230.81 (~E(f1(a3,f1(f1(f1(a5,a4),f1(a3,f1(a5,a4))),f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))))),a4)), % 230.51/230.81 inference(scs_inference,[],[149,125,4,5,2])). % 230.51/230.81 cnf(158,plain, % 230.51/230.81 (~E(f1(f1(a3,f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(a5,a4)),f1(a4,f1(a5,a4)))), % 230.51/230.81 inference(scs_inference,[],[113,149,125,4,5,2,3])). % 230.51/230.81 cnf(160,plain, % 230.51/230.81 (E(f1(f1(x1601,f1(x1602,f1(x1603,f1(x1604,x1605)))),x1606),f1(f1(x1601,f1(x1604,f1(x1603,f1(x1602,x1605)))),x1606))), % 230.51/230.81 inference(scs_inference,[],[150,4])). % 230.51/230.81 cnf(161,plain, % 230.51/230.81 (E(f1(x1611,f1(x1612,f1(x1613,f1(x1614,f1(x1615,x1616))))),f1(x1611,f1(x1612,f1(x1615,f1(x1614,f1(x1613,x1616))))))), % 230.51/230.81 inference(scs_inference,[],[150,4,5])). % 230.51/230.81 cnf(162,plain, % 230.51/230.81 (~E(f1(a4,f1(a5,a4)),f1(f1(a3,f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(a5,a4)))), % 230.51/230.81 inference(scs_inference,[],[158,150,4,5,2])). % 230.51/230.81 cnf(163,plain, % 230.51/230.81 (~E(f1(a3,f1(a5,f1(f1(a3,f1(a5,a4)),f1(a2,a4)))),f1(a3,f1(a2,f1(a4,f1(a5,a4)))))), % 230.51/230.81 inference(scs_inference,[],[158,150,135,4,5,2,3])). % 230.51/230.81 cnf(165,plain, % 230.51/230.81 (E(f1(f1(x1651,f1(f1(x1652,f1(x1651,x1652)),f1(x1651,f1(x1652,f1(x1651,x1652))))),x1653),f1(f1(x1651,x1652),x1653))), % 230.51/230.81 inference(scs_inference,[],[38,4])). % 230.51/230.81 cnf(166,plain, % 230.51/230.81 (E(f1(x1661,f1(x1662,f1(f1(x1663,f1(x1662,x1663)),f1(x1662,f1(x1663,f1(x1662,x1663)))))),f1(x1661,f1(x1662,x1663)))), % 230.51/230.81 inference(scs_inference,[],[38,4,5])). % 230.51/230.81 cnf(167,plain, % 230.51/230.81 (~E(f1(a3,f1(a2,f1(a4,f1(a5,a4)))),f1(a3,f1(a5,f1(f1(a3,f1(a5,a4)),f1(a2,a4)))))), % 230.51/230.81 inference(scs_inference,[],[163,38,4,5,2])). % 230.51/230.81 cnf(168,plain, % 230.51/230.81 (~E(f1(f1(a3,f1(a5,f1(a3,f1(f1(a5,a4),a4)))),f1(a5,a4)),a4)), % 230.51/230.81 inference(scs_inference,[],[108,163,160,38,4,5,2,3])). % 230.51/230.81 cnf(170,plain, % 230.51/230.81 (E(f1(f1(f1(x1701,f1(x1702,f1(x1703,x1702))),x1704),x1705),f1(f1(f1(f1(x1703,x1702),f1(x1702,f1(x1703,x1702))),f1(x1704,f1(x1701,x1704))),x1705))), % 230.51/230.81 inference(scs_inference,[],[30,4])). % 230.51/230.81 cnf(171,plain, % 230.51/230.81 (E(f1(x1711,f1(f1(x1712,f1(x1713,f1(x1714,x1713))),x1715)),f1(x1711,f1(f1(f1(x1714,x1713),f1(x1713,f1(x1714,x1713))),f1(x1715,f1(x1712,x1715)))))), % 230.51/230.81 inference(scs_inference,[],[30,4,5])). % 230.51/230.81 cnf(172,plain, % 230.51/230.81 (~E(a4,f1(f1(a3,f1(a5,f1(a3,f1(f1(a5,a4),a4)))),f1(a5,a4)))), % 230.51/230.81 inference(scs_inference,[],[168,30,4,5,2])). % 230.51/230.81 cnf(173,plain, % 230.51/230.81 (E(f1(f1(x1731,f1(f1(x1732,f1(x1731,x1732)),f1(x1731,f1(x1732,f1(x1731,x1732))))),f1(x1733,f1(x1734,x1735))),f1(x1734,f1(x1733,f1(f1(x1731,x1732),x1735))))), % 230.51/230.81 inference(scs_inference,[],[7,168,165,30,4,5,2,3])). % 230.51/230.81 cnf(176,plain, % 230.51/230.81 (E(f1(f1(f1(f1(x1761,x1762),f1(x1762,f1(x1761,x1762))),f1(x1763,f1(x1764,x1763))),x1765),f1(f1(f1(x1764,f1(x1762,f1(x1761,x1762))),x1763),x1765))), % 230.51/230.81 inference(scs_inference,[],[32,4])). % 230.51/230.81 cnf(177,plain, % 230.51/230.81 (E(f1(x1771,f1(f1(f1(x1772,x1773),f1(x1773,f1(x1772,x1773))),f1(x1774,f1(x1775,x1774)))),f1(x1771,f1(f1(x1775,f1(x1773,f1(x1772,x1773))),x1774)))), % 230.51/230.81 inference(scs_inference,[],[32,4,5])). % 230.51/230.81 cnf(178,plain, % 230.51/230.81 (~E(f1(f1(a3,f1(a5,a4)),f1(f1(f1(a5,a4),f1(a3,f1(a5,a4))),f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))))),a4)), % 230.51/230.81 inference(scs_inference,[],[147,32,4,5,2])). % 230.51/230.81 cnf(181,plain, % 230.51/230.81 (E(f1(f1(f1(f1(x1811,f1(x1812,f1(x1811,x1812))),x1813),x1814),x1815),f1(f1(f1(f1(x1811,x1812),x1813),x1814),x1815))), % 230.51/230.81 inference(scs_inference,[],[96,4])). % 230.51/230.81 cnf(182,plain, % 230.51/230.81 (E(f1(x1821,f1(f1(f1(x1822,f1(x1823,f1(x1822,x1823))),x1824),x1825)),f1(x1821,f1(f1(f1(x1822,x1823),x1824),x1825)))), % 230.51/230.81 inference(scs_inference,[],[96,4,5])). % 230.51/230.81 cnf(184,plain, % 230.51/230.81 (E(f1(x1841,f1(f1(x1842,f1(x1843,f1(x1844,x1843))),x1845)),f1(x1845,f1(f1(f1(x1844,x1843),f1(x1843,f1(x1844,x1843))),f1(x1841,f1(x1842,x1845)))))), % 230.51/230.81 inference(scs_inference,[],[7,171,59,96,4,5,2,3])). % 230.51/230.81 cnf(187,plain, % 230.51/230.81 (E(f1(f1(x1871,f1(f1(x1872,x1873),f1(x1874,f1(x1875,x1874)))),x1876),f1(f1(x1871,f1(f1(x1875,f1(x1873,f1(x1872,x1873))),x1874)),x1876))), % 230.51/230.81 inference(scs_inference,[],[139,4])). % 230.51/230.81 cnf(188,plain, % 230.51/230.81 (E(f1(x1881,f1(x1882,f1(f1(x1883,x1884),f1(x1885,f1(x1886,x1885))))),f1(x1881,f1(x1882,f1(f1(x1886,f1(x1884,f1(x1883,x1884))),x1885))))), % 230.51/230.81 inference(scs_inference,[],[139,4,5])). % 230.51/230.81 cnf(190,plain, % 230.51/230.81 (~E(f1(a4,f1(a2,f1(a3,f1(a5,a4)))),f1(a3,f1(a5,f1(f1(a3,f1(a5,a4)),f1(a2,a4)))))), % 230.51/230.81 inference(scs_inference,[],[7,167,61,139,4,5,2,3])). % 230.51/230.81 cnf(192,plain, % 230.51/230.81 (E(f1(f1(f1(f1(x1921,x1922),f1(x1922,f1(x1921,x1922))),x1923),x1924),f1(f1(f1(x1921,x1922),x1923),x1924))), % 230.51/230.81 inference(scs_inference,[],[18,4])). % 230.51/230.81 cnf(193,plain, % 230.51/230.81 (E(f1(x1931,f1(f1(f1(x1932,x1933),f1(x1933,f1(x1932,x1933))),x1934)),f1(x1931,f1(f1(x1932,x1933),x1934)))), % 230.51/230.81 inference(scs_inference,[],[18,4,5])). % 230.51/230.81 cnf(194,plain, % 230.51/230.81 (~E(f1(a3,f1(a5,f1(f1(a3,f1(a5,a4)),f1(a2,a4)))),f1(a4,f1(a2,f1(a3,f1(a5,a4)))))), % 230.51/230.81 inference(scs_inference,[],[190,18,4,5,2])). % 230.51/230.81 cnf(195,plain, % 230.51/230.81 (E(f1(x1951,f1(f1(f1(x1952,x1953),f1(x1953,f1(x1952,x1953))),f1(f1(x1954,x1955),f1(x1956,f1(x1954,x1955))))),f1(x1954,f1(f1(x1956,f1(x1953,f1(x1952,x1953))),f1(x1951,x1955))))), % 230.51/230.81 inference(scs_inference,[],[7,190,177,18,4,5,2,3])). % 230.51/230.81 cnf(198,plain, % 230.51/230.81 (E(f1(f1(f1(f1(f1(x1981,x1982),f1(x1982,f1(x1981,x1982))),x1983),x1984),x1985),f1(f1(f1(f1(x1981,x1982),x1983),x1984),x1985))), % 230.51/230.81 inference(scs_inference,[],[192,4])). % 230.51/230.81 cnf(199,plain, % 230.51/230.81 (E(f1(x1991,f1(f1(f1(f1(x1992,x1993),f1(x1993,f1(x1992,x1993))),x1994),x1995)),f1(x1991,f1(f1(f1(x1992,x1993),x1994),x1995)))), % 230.51/230.81 inference(scs_inference,[],[192,4,5])). % 230.51/230.81 cnf(201,plain, % 230.51/230.81 (~E(f1(f1(a3,f1(a5,a4)),f1(a5,f1(a3,f1(a2,a4)))),f1(a4,f1(a2,f1(a3,f1(a5,a4)))))), % 230.51/230.81 inference(scs_inference,[],[7,192,194,89,4,5,2,3])). % 230.51/230.81 cnf(203,plain, % 230.51/230.81 (E(f1(f1(x2031,f1(f1(f1(x2032,x2033),f1(x2033,f1(x2032,x2033))),x2034)),x2035),f1(f1(x2031,f1(f1(x2032,x2033),x2034)),x2035))), % 230.51/230.81 inference(scs_inference,[],[193,4])). % 230.51/230.81 cnf(204,plain, % 230.51/230.81 (E(f1(x2041,f1(x2042,f1(f1(f1(x2043,x2044),f1(x2044,f1(x2043,x2044))),x2045))),f1(x2041,f1(x2042,f1(f1(x2043,x2044),x2045))))), % 230.51/230.81 inference(scs_inference,[],[193,4,5])). % 230.51/230.81 cnf(205,plain, % 230.51/230.81 (~E(f1(a4,f1(a2,f1(a3,f1(a5,a4)))),f1(f1(a3,f1(a5,a4)),f1(a5,f1(a3,f1(a2,a4)))))), % 230.51/230.81 inference(scs_inference,[],[193,201,4,5,2])). % 230.51/230.81 cnf(206,plain, % 230.51/230.81 (E(f1(x2061,f1(f1(f1(x2062,x2063),f1(x2063,f1(x2062,x2063))),f1(x2064,x2065))),f1(x2064,f1(f1(x2062,x2063),f1(x2061,x2065))))), % 230.51/230.81 inference(scs_inference,[],[7,193,201,4,5,2,3])). % 230.51/230.81 cnf(209,plain, % 230.51/230.81 (E(f1(f1(f1(x2091,f1(x2092,f1(x2093,x2092))),x2094),x2095),f1(f1(x2091,f1(x2094,f1(f1(x2093,x2092),x2094))),x2095))), % 230.51/230.81 inference(scs_inference,[],[8,4])). % 230.51/230.81 cnf(210,plain, % 230.51/230.81 (E(f1(x2101,f1(f1(x2102,f1(x2103,f1(x2104,x2103))),x2105)),f1(x2101,f1(x2102,f1(x2105,f1(f1(x2104,x2103),x2105)))))), % 230.51/230.81 inference(scs_inference,[],[8,4,5])). % 230.51/230.81 cnf(212,plain, % 230.51/230.81 (~E(a4,f1(a3,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)))))), % 230.51/230.81 inference(scs_inference,[],[8,206,129,86,4,5,2,3])). % 230.51/230.81 cnf(214,plain, % 230.51/230.81 (E(f1(f1(x2141,f1(f1(f1(x2142,x2143),f1(x2143,f1(x2142,x2143))),f1(x2144,x2145))),x2146),f1(f1(x2144,f1(f1(x2142,x2143),f1(x2141,x2145))),x2146))), % 230.51/230.81 inference(scs_inference,[],[206,4])). % 230.51/230.81 cnf(215,plain, % 230.51/230.81 (E(f1(x2151,f1(x2152,f1(f1(f1(x2153,x2154),f1(x2154,f1(x2153,x2154))),f1(x2155,x2156)))),f1(x2151,f1(x2155,f1(f1(x2153,x2154),f1(x2152,x2156)))))), % 230.51/230.81 inference(scs_inference,[],[206,4,5])). % 230.51/230.81 cnf(216,plain, % 230.51/230.81 (~E(f1(a3,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)))),a4)), % 230.51/230.81 inference(scs_inference,[],[212,206,4,5,2])). % 230.51/230.81 cnf(217,plain, % 230.51/230.81 (E(f1(f1(x2171,f1(x2172,f1(x2173,x2172))),f1(x2174,f1(f1(x2175,f1(x2174,x2175)),f1(x2174,f1(x2175,f1(x2174,x2175)))))),f1(x2171,f1(f1(x2174,x2175),f1(f1(x2173,x2172),f1(x2174,x2175)))))), % 230.51/230.81 inference(scs_inference,[],[8,212,166,206,4,5,2,3])). % 230.51/230.81 cnf(220,plain, % 230.51/230.81 (E(f1(f1(f1(x2201,f1(x2202,f1(x2203,x2202))),x2204),x2205),f1(f1(f1(x2203,x2202),f1(x2204,f1(x2201,x2204))),x2205))), % 230.51/230.81 inference(scs_inference,[],[22,4])). % 230.51/230.81 cnf(221,plain, % 230.51/230.81 (E(f1(x2211,f1(f1(x2212,f1(x2213,f1(x2214,x2213))),x2215)),f1(x2211,f1(f1(x2214,x2213),f1(x2215,f1(x2212,x2215)))))), % 230.51/230.82 inference(scs_inference,[],[22,4,5])). % 230.51/230.82 cnf(222,plain, % 230.51/230.82 (~E(f1(f1(a3,f1(a5,a4)),f1(a5,a4)),f1(a4,f1(a5,a4)))), % 230.51/230.82 inference(scs_inference,[],[75,22,4,5,2])). % 230.51/230.82 cnf(223,plain, % 230.51/230.82 (~E(a4,f1(a3,f1(a5,f1(f1(a4,f1(a5,a4)),f1(a5,f1(a4,f1(a5,a4)))))))), % 230.51/230.82 inference(scs_inference,[],[76,75,166,22,4,5,2,3])). % 230.51/230.82 cnf(225,plain, % 230.51/230.82 (E(f1(f1(f1(f1(x2251,f1(x2252,f1(x2253,x2252))),x2254),x2255),x2256),f1(f1(f1(f1(x2253,x2252),f1(x2254,f1(x2251,x2254))),x2255),x2256))), % 230.51/230.82 inference(scs_inference,[],[220,4])). % 230.51/230.82 cnf(226,plain, % 230.51/230.82 (E(f1(x2261,f1(f1(f1(x2262,f1(x2263,f1(x2264,x2263))),x2265),x2266)),f1(x2261,f1(f1(f1(x2264,x2263),f1(x2265,f1(x2262,x2265))),x2266)))), % 230.51/230.82 inference(scs_inference,[],[220,4,5])). % 230.51/230.82 cnf(227,plain, % 230.51/230.82 (~E(f1(a3,f1(a5,f1(f1(a4,f1(a5,a4)),f1(a5,f1(a4,f1(a5,a4)))))),a4)), % 230.51/230.82 inference(scs_inference,[],[220,223,4,5,2])). % 230.51/230.82 cnf(228,plain, % 230.51/230.82 (E(f1(f1(x2281,f1(f1(f1(x2282,x2283),f1(x2283,f1(x2282,x2283))),f1(x2284,f1(x2282,x2283)))),x2285),f1(x2284,f1(x2285,f1(f1(x2281,f1(x2282,x2283)),x2285))))), % 230.51/230.82 inference(scs_inference,[],[8,214,220,223,4,5,2,3])). % 230.51/230.82 cnf(232,plain, % 230.51/230.82 (E(f1(x2321,f1(x2322,f1(f1(x2323,f1(x2324,f1(x2325,x2324))),x2326))),f1(x2321,f1(x2322,f1(f1(x2325,x2324),f1(x2326,f1(x2323,x2326))))))), % 230.51/230.82 inference(scs_inference,[],[221,4,5])). % 230.51/230.82 cnf(233,plain, % 230.51/230.82 (~E(f1(a2,f1(f1(a3,f1(a5,a4)),f1(a5,a4))),f1(a2,f1(a4,f1(a5,a4))))), % 230.51/230.82 inference(scs_inference,[],[221,74,4,5,2])). % 230.51/230.82 cnf(234,plain, % 230.51/230.82 (~E(f1(a3,f1(a5,f1(a4,f1(a5,f1(f1(a4,f1(a5,a4)),f1(a5,a4)))))),a4)), % 230.51/230.82 inference(scs_inference,[],[221,227,161,74,4,5,2,3])). % 230.51/230.82 cnf(236,plain, % 230.51/230.82 (E(f1(f1(f1(f1(x2361,x2362),f1(x2362,f1(x2361,x2362))),f1(x2363,f1(f1(x2361,x2362),x2363))),x2364),f1(f1(f1(x2361,x2362),x2363),x2364))), % 230.51/230.82 inference(scs_inference,[],[42,4])). % 230.51/230.82 cnf(237,plain, % 230.51/230.82 (E(f1(x2371,f1(f1(f1(x2372,x2373),f1(x2373,f1(x2372,x2373))),f1(x2374,f1(f1(x2372,x2373),x2374)))),f1(x2371,f1(f1(x2372,x2373),x2374)))), % 230.51/230.82 inference(scs_inference,[],[42,4,5])). % 230.51/230.82 cnf(239,plain, % 230.51/230.82 (E(f1(f1(f1(x2391,f1(x2392,f1(x2393,x2392))),x2394),x2395),f1(f1(f1(x2393,x2392),f1(x2392,f1(x2393,x2392))),f1(x2395,f1(f1(x2391,x2394),x2395))))), % 230.51/230.82 inference(scs_inference,[],[8,234,170,42,4,5,2,3])). % 230.51/230.82 cnf(243,plain, % 230.51/230.82 (E(f1(x2431,f1(f1(f1(f1(x2432,x2433),f1(x2433,f1(x2432,x2433))),f1(x2434,f1(f1(x2432,x2433),x2434))),x2435)),f1(x2431,f1(f1(f1(x2432,x2433),x2434),x2435)))), % 230.51/230.82 inference(scs_inference,[],[236,4,5])). % 230.51/230.82 cnf(244,plain, % 230.51/230.82 (~E(f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4))),f1(a2,f1(a4,f1(a5,a4))))), % 230.51/230.82 inference(scs_inference,[],[236,46,4,5,2])). % 230.51/230.82 cnf(245,plain, % 230.51/230.82 (~E(f1(a3,f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),a4)), % 230.51/230.82 inference(scs_inference,[],[8,236,108,46,4,5,2,3])). % 230.51/230.82 cnf(248,plain, % 230.51/230.82 (E(f1(x2481,f1(x2482,f1(f1(f1(x2483,x2484),f1(x2484,f1(x2483,x2484))),f1(x2485,f1(f1(x2483,x2484),x2485))))),f1(x2481,f1(x2482,f1(f1(x2483,x2484),x2485))))), % 230.51/230.82 inference(scs_inference,[],[237,4,5])). % 230.51/230.82 cnf(249,plain, % 230.51/230.82 (~E(a4,f1(a3,f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))))), % 230.51/230.82 inference(scs_inference,[],[245,237,4,5,2])). % 230.51/230.82 cnf(250,plain, % 230.51/230.82 (E(f1(f1(f1(f1(x2501,x2502),f1(x2502,f1(x2501,x2502))),f1(x2503,f1(x2504,x2503))),x2505),f1(x2504,f1(x2505,f1(f1(f1(x2501,x2502),x2503),x2505))))), % 230.51/230.82 inference(scs_inference,[],[8,245,237,111,4,5,2,3])). % 230.51/230.82 cnf(253,plain, % 230.51/230.82 (E(f1(f1(x2531,f1(x2532,f1(f1(x2533,x2534),x2532))),x2535),f1(f1(f1(x2531,f1(x2534,f1(x2533,x2534))),x2532),x2535))), % 230.51/230.82 inference(scs_inference,[],[15,4])). % 230.51/230.82 cnf(254,plain, % 230.51/230.82 (E(f1(x2541,f1(x2542,f1(x2543,f1(f1(x2544,x2545),x2543)))),f1(x2541,f1(f1(x2542,f1(x2545,f1(x2544,x2545))),x2543)))), % 230.51/230.82 inference(scs_inference,[],[15,4,5])). % 230.51/230.82 cnf(255,plain, % 230.51/230.82 (~E(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(a4,f1(a5,a4)))), % 230.51/230.82 inference(scs_inference,[],[79,15,4,5,2])). % 230.51/230.82 cnf(256,plain, % 230.51/230.82 (~E(f1(a3,f1(f1(a5,a4),f1(f1(f1(a3,f1(a5,a4)),f1(a5,a4)),f1(a5,a4)))),f1(a4,f1(a5,a4)))), % 230.51/230.82 inference(scs_inference,[],[8,158,79,15,4,5,2,3])). % 230.51/230.82 cnf(258,plain, % 230.51/230.82 (E(f1(f1(x2581,f1(f1(x2582,f1(x2583,x2584)),f1(x2581,f1(x2582,f1(x2583,x2584))))),x2585),f1(f1(x2583,f1(x2582,f1(x2581,x2584))),x2585))), % 230.51/230.82 inference(scs_inference,[],[25,4])). % 230.51/230.82 cnf(259,plain, % 230.51/230.82 (E(f1(x2591,f1(x2592,f1(f1(x2593,f1(x2594,x2595)),f1(x2592,f1(x2593,f1(x2594,x2595)))))),f1(x2591,f1(x2594,f1(x2593,f1(x2592,x2595)))))), % 230.51/230.82 inference(scs_inference,[],[25,4,5])). % 230.51/230.82 cnf(260,plain, % 230.51/230.82 (~E(f1(a4,f1(a5,a4)),f1(a3,f1(f1(a5,a4),f1(f1(f1(a3,f1(a5,a4)),f1(a5,a4)),f1(a5,a4)))))), % 230.51/230.82 inference(scs_inference,[],[256,25,4,5,2])). % 230.51/230.82 cnf(261,plain, % 230.51/230.82 (E(f1(f1(f1(x2611,f1(x2612,f1(x2613,x2612))),x2614),x2615),f1(x2611,f1(x2615,f1(f1(f1(x2613,x2612),x2614),x2615))))), % 230.51/230.82 inference(scs_inference,[],[8,256,209,25,4,5,2,3])). % 230.51/230.82 cnf(264,plain, % 230.51/230.82 (~E(f1(f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4))),f1(a2,f1(a4,f1(a5,a4))))), % 230.51/230.82 inference(scs_inference,[],[64,2])). % 230.51/230.82 cnf(265,plain, % 230.51/230.82 (E(f1(f1(x2651,f1(x2652,f1(f1(x2653,x2654),x2655))),x2656),f1(f1(f1(f1(x2653,x2654),f1(x2654,f1(x2653,x2654))),f1(x2652,f1(x2651,x2655))),x2656))), % 230.51/230.82 inference(scs_inference,[],[64,26,2,4])). % 230.51/230.82 cnf(266,plain, % 230.51/230.82 (E(f1(x2661,f1(x2662,f1(x2663,f1(f1(x2664,x2665),x2666)))),f1(x2661,f1(f1(f1(x2664,x2665),f1(x2665,f1(x2664,x2665))),f1(x2663,f1(x2662,x2666)))))), % 230.51/230.82 inference(scs_inference,[],[64,26,2,4,5])). % 230.51/230.82 cnf(267,plain, % 230.51/230.82 (~E(a4,f1(a3,f1(a5,f1(f1(f1(a4,f1(a5,a4)),f1(f1(a5,a4),f1(a4,f1(a5,a4)))),f1(a5,f1(a4,f1(a5,a4)))))))), % 230.51/230.82 inference(scs_inference,[],[215,64,223,26,2,4,5,3])). % 230.51/230.82 cnf(270,plain, % 230.51/230.82 (E(f1(f1(x2701,x2702),x2703),f1(f1(x2701,f1(x2702,f1(x2701,x2702))),x2703))), % 230.51/230.82 inference(scs_inference,[],[10,267,2,4])). % 230.51/230.82 cnf(271,plain, % 230.51/230.82 (E(f1(x2711,f1(x2712,x2713)),f1(x2711,f1(x2712,f1(x2713,f1(x2712,x2713)))))), % 230.51/230.82 inference(scs_inference,[],[10,267,2,4,5])). % 230.51/230.82 cnf(272,plain, % 230.51/230.82 (~E(f1(f1(f1(a5,f1(a4,f1(a5,a4))),a4),f1(a3,f1(a5,a4))),f1(a2,f1(a4,f1(a5,a4))))), % 230.51/230.82 inference(scs_inference,[],[10,264,176,267,2,4,5,3])). % 230.51/230.82 cnf(274,plain, % 230.51/230.82 (~E(f1(a2,f1(a4,f1(a5,a4))),f1(f1(f1(a5,f1(a4,f1(a5,a4))),a4),f1(a3,f1(a5,a4))))), % 230.51/230.82 inference(scs_inference,[],[272,2])). % 230.51/230.82 cnf(275,plain, % 230.51/230.82 (E(f1(f1(f1(x2751,x2752),x2753),x2754),f1(f1(f1(x2751,f1(x2752,f1(x2751,x2752))),x2753),x2754))), % 230.51/230.82 inference(scs_inference,[],[270,272,2,4])). % 230.51/230.82 cnf(276,plain, % 230.51/230.82 (E(f1(x2761,f1(f1(x2762,x2763),x2764)),f1(x2761,f1(f1(x2762,f1(x2763,f1(x2762,x2763))),x2764)))), % 230.51/230.82 inference(scs_inference,[],[270,272,2,4,5])). % 230.51/230.82 cnf(277,plain, % 230.51/230.82 (~E(f1(a2,f1(f1(f1(a3,f1(a5,a4)),f1(a5,a4)),f1(a2,f1(f1(a3,f1(a5,a4)),f1(a5,a4))))),f1(a2,f1(a4,f1(a5,a4))))), % 230.51/230.82 inference(scs_inference,[],[10,233,270,272,2,4,5,3])). % 230.51/230.82 cnf(280,plain, % 230.51/230.82 (E(f1(f1(x2801,f1(x2802,x2803)),x2804),f1(f1(x2801,f1(x2802,f1(x2803,f1(x2802,x2803)))),x2804))), % 230.51/230.82 inference(scs_inference,[],[271,277,2,4])). % 230.51/230.82 cnf(281,plain, % 230.51/230.82 (E(f1(x2811,f1(x2812,f1(x2813,x2814))),f1(x2811,f1(x2812,f1(x2813,f1(x2814,f1(x2813,x2814))))))), % 230.51/230.82 inference(scs_inference,[],[271,277,2,4,5])). % 230.51/230.82 cnf(282,plain, % 230.51/230.82 (~E(f1(a3,f1(a5,f1(a4,f1(a5,a4)))),a4)), % 230.51/230.82 inference(scs_inference,[],[114,271,277,2,4,5,3])). % 230.51/230.82 cnf(284,plain, % 230.51/230.82 (~E(a4,f1(a3,f1(a5,f1(a4,f1(a5,a4)))))), % 230.51/230.82 inference(scs_inference,[],[282,2])). % 230.51/230.82 cnf(285,plain, % 230.51/230.82 (E(f1(f1(f1(f1(x2851,x2852),x2853),x2854),x2855),f1(f1(f1(f1(x2851,f1(x2852,f1(x2851,x2852))),x2853),x2854),x2855))), % 230.51/230.82 inference(scs_inference,[],[282,275,2,4])). % 230.51/230.82 cnf(286,plain, % 230.51/230.82 (E(f1(x2861,f1(f1(f1(x2862,x2863),x2864),x2865)),f1(x2861,f1(f1(f1(x2862,f1(x2863,f1(x2862,x2863))),x2864),x2865)))), % 230.51/230.82 inference(scs_inference,[],[282,275,2,4,5])). % 230.51/230.82 cnf(287,plain, % 230.51/230.82 (~E(f1(a3,f1(f1(a5,f1(a4,f1(a5,a4))),f1(a3,f1(a5,f1(a4,f1(a5,a4)))))),a4)), % 230.51/230.82 inference(scs_inference,[],[10,282,275,2,4,5,3])). % 230.51/230.82 cnf(289,plain, % 230.51/230.82 (~E(a4,f1(a3,f1(f1(a5,f1(a4,f1(a5,a4))),f1(a3,f1(a5,f1(a4,f1(a5,a4)))))))), % 230.51/230.82 inference(scs_inference,[],[287,2])). % 230.51/230.82 cnf(290,plain, % 230.51/230.82 (E(f1(f1(x2901,f1(f1(x2902,x2903),x2904)),x2905),f1(f1(x2901,f1(f1(x2902,f1(x2903,f1(x2902,x2903))),x2904)),x2905))), % 230.51/230.82 inference(scs_inference,[],[276,287,2,4])). % 230.51/230.82 cnf(291,plain, % 230.51/230.82 (E(f1(x2911,f1(x2912,f1(f1(x2913,x2914),x2915))),f1(x2911,f1(x2912,f1(f1(x2913,f1(x2914,f1(x2913,x2914))),x2915))))), % 230.51/230.82 inference(scs_inference,[],[276,287,2,4,5])). % 230.51/230.82 cnf(292,plain, % 230.51/230.82 (~E(f1(f1(a3,f1(a5,a4)),f1(f1(a5,f1(a4,f1(a5,a4))),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(a4,f1(a5,a4)))), % 230.51/230.82 inference(scs_inference,[],[255,276,287,2,4,5,3])). % 230.51/230.82 cnf(295,plain, % 230.51/230.82 (E(f1(f1(f1(x2951,f1(x2952,x2953)),x2954),x2955),f1(f1(f1(x2951,f1(x2952,f1(x2953,f1(x2952,x2953)))),x2954),x2955))), % 230.51/230.82 inference(scs_inference,[],[292,280,2,4])). % 230.51/230.82 cnf(296,plain, % 230.51/230.82 (E(f1(x2961,f1(f1(x2962,f1(x2963,x2964)),x2965)),f1(x2961,f1(f1(x2962,f1(x2963,f1(x2964,f1(x2963,x2964)))),x2965)))), % 230.51/230.82 inference(scs_inference,[],[292,280,2,4,5])). % 230.51/230.82 cnf(297,plain, % 230.51/230.82 (~E(a4,f1(a3,f1(a5,f1(a4,f1(a5,f1(a4,f1(a5,a4)))))))), % 230.51/230.82 inference(scs_inference,[],[284,292,280,134,2,4,5,3])). % 230.51/230.82 cnf(300,plain, % 230.51/230.82 (E(f1(f1(x3001,f1(x3002,f1(x3003,x3004))),x3005),f1(f1(x3001,f1(x3002,f1(x3003,f1(x3004,f1(x3003,x3004))))),x3005))), % 230.51/230.82 inference(scs_inference,[],[281,297,2,4])). % 230.51/230.82 cnf(301,plain, % 230.51/230.82 (E(f1(x3011,f1(x3012,f1(x3013,f1(x3014,x3015)))),f1(x3011,f1(x3012,f1(x3013,f1(x3014,f1(x3015,f1(x3014,x3015)))))))), % 230.51/230.82 inference(scs_inference,[],[281,297,2,4,5])). % 230.51/230.82 cnf(302,plain, % 230.51/230.82 (~E(f1(a5,f1(a4,f1(a5,f1(a4,f1(a5,a4))))),f1(a2,f1(a4,f1(a5,a4))))), % 230.51/230.82 inference(scs_inference,[],[98,281,297,2,4,5,3])). % 230.51/230.82 cnf(304,plain, % 230.51/230.82 (~E(f1(a2,f1(a4,f1(a5,a4))),f1(a5,f1(a4,f1(a5,f1(a4,f1(a5,a4))))))), % 230.51/230.82 inference(scs_inference,[],[302,2])). % 230.51/230.82 cnf(305,plain, % 230.51/230.82 (E(f1(f1(f1(x3051,x3052),x3053),x3054),f1(f1(f1(f1(x3051,x3052),f1(x3052,f1(x3051,x3052))),x3053),x3054))), % 230.51/230.82 inference(scs_inference,[],[302,16,2,4])). % 230.51/230.82 cnf(306,plain, % 230.51/230.82 (E(f1(x3061,f1(f1(x3062,x3063),x3064)),f1(x3061,f1(f1(f1(x3062,x3063),f1(x3063,f1(x3062,x3063))),x3064)))), % 230.51/230.82 inference(scs_inference,[],[302,16,2,4,5])). % 230.51/230.82 cnf(307,plain, % 230.51/230.82 (~E(a4,f1(f1(a3,f1(f1(f1(a5,a4),f1(a3,f1(a5,a4))),f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))))),f1(f1(a5,a4),f1(a3,f1(a5,a4)))))), % 230.51/230.82 inference(scs_inference,[],[249,302,173,16,2,4,5,3])). % 230.51/230.82 cnf(309,plain, % 230.51/230.82 (~E(f1(f1(a3,f1(f1(f1(a5,a4),f1(a3,f1(a5,a4))),f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))))),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),a4)), % 230.51/230.82 inference(scs_inference,[],[307,2])). % 230.51/230.82 cnf(310,plain, % 230.51/230.82 (~E(f1(a5,f1(f1(a3,f1(a5,a4)),f1(f1(f1(a5,a4),a4),f1(a3,f1(a5,a4))))),f1(a2,f1(a4,f1(a5,a4))))), % 230.51/230.82 inference(scs_inference,[],[250,307,264,2,3])). % 230.51/230.82 cnf(313,plain, % 230.51/230.82 (~E(f1(a4,f1(f1(a5,a4),f1(a4,f1(a5,a4)))),f1(f1(a3,f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(a5,a4)))), % 230.51/230.82 inference(scs_inference,[],[10,162,310,2,3])). % 230.51/230.82 cnf(315,plain, % 230.51/230.82 (~E(f1(f1(a3,f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(a5,a4)),f1(a4,f1(f1(a5,a4),f1(a4,f1(a5,a4)))))), % 230.51/230.82 inference(scs_inference,[],[313,2])). % 230.51/230.82 cnf(316,plain, % 230.51/230.82 (~E(f1(a4,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a4,f1(a5,a4)))),f1(f1(a3,f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(a5,a4)))), % 230.51/230.82 inference(scs_inference,[],[306,313,2,3])). % 230.51/230.82 cnf(318,plain, % 230.51/230.82 (~E(f1(a3,f1(a5,a4)),f1(a3,f1(a2,f1(a4,f1(a5,a4)))))), % 230.51/230.82 inference(scs_inference,[],[11,2])). % 230.51/230.82 cnf(325,plain, % 230.51/230.82 (~E(f1(f1(a3,f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(a5,a4)),f1(a4,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a4,f1(a5,a4)))))), % 230.51/230.82 inference(scs_inference,[],[316,2])). % 230.51/230.82 cnf(326,plain, % 230.51/230.82 (~E(a4,f1(f1(a3,f1(a5,f1(a3,f1(f1(f1(a5,a4),a4),f1(a3,f1(f1(a5,a4),a4)))))),f1(a5,a4)))), % 230.51/230.82 inference(scs_inference,[],[172,316,133,2,3])). % 230.51/230.82 cnf(329,plain, % 230.51/230.82 (~E(f1(f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)),f1(a5,a4)),f1(a4,f1(f1(a5,a4),f1(a4,f1(a5,a4)))))), % 230.51/230.82 inference(scs_inference,[],[315,253,326,2,3])). % 230.51/230.82 cnf(331,plain, % 230.51/230.82 (~E(f1(a4,f1(f1(a5,a4),f1(a4,f1(a5,a4)))),f1(f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)),f1(a5,a4)))), % 230.51/230.82 inference(scs_inference,[],[329,2])). % 230.51/230.82 cnf(332,plain, % 230.51/230.82 (~E(a4,f1(a3,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a3,f1(f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4))),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))))))), % 230.51/230.82 inference(scs_inference,[],[329,141,249,2,3])). % 230.51/230.82 cnf(335,plain, % 230.51/230.82 (~E(f1(f1(a3,f1(a5,a4)),f1(f1(f1(f1(a5,a4),f1(a3,f1(a5,a4))),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4)))),a4)), % 230.51/230.82 inference(scs_inference,[],[254,178,332,2,3])). % 230.51/230.82 cnf(337,plain, % 230.51/230.82 (~E(a4,f1(f1(a3,f1(a5,a4)),f1(f1(f1(f1(a5,a4),f1(a3,f1(a5,a4))),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4)))))), % 230.51/230.82 inference(scs_inference,[],[335,2])). % 230.51/230.82 cnf(338,plain, % 230.51/230.82 (~E(f1(a5,f1(a3,f1(f1(a5,f1(a4,f1(a5,a4))),a4))),f1(a2,f1(a4,f1(a5,a4))))), % 230.51/230.82 inference(scs_inference,[],[335,291,118,2,3])). % 230.51/230.82 cnf(341,plain, % 230.51/230.82 (~E(f1(a3,f1(f1(a5,f1(a4,f1(f1(a5,a4),a4))),f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)))),a4)), % 230.51/230.82 inference(scs_inference,[],[216,338,156,2,3])). % 230.51/230.82 cnf(344,plain, % 230.51/230.82 (~E(a4,f1(a3,f1(f1(a5,a4),f1(f1(f1(a3,f1(a5,a4)),f1(a5,a4)),f1(f1(f1(a5,a4),f1(a3,f1(a5,a4))),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))))))), % 230.51/230.82 inference(scs_inference,[],[337,152,341,2,3])). % 230.51/230.82 cnf(347,plain, % 230.51/230.82 (~E(f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),a4)), % 230.51/230.82 inference(scs_inference,[],[151,123,344,2,3])). % 230.51/230.82 cnf(349,plain, % 230.51/230.82 (~E(a4,f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))))), % 230.51/230.82 inference(scs_inference,[],[347,2])). % 230.51/230.82 cnf(350,plain, % 230.51/230.82 (~E(a4,f1(a3,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(f1(f1(a3,f1(a5,a4)),f1(a5,a4)),f1(f1(f1(a5,a4),f1(a3,f1(a5,a4))),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))))))), % 230.51/230.82 inference(scs_inference,[],[347,195,337,2,3])). % 230.51/230.82 cnf(353,plain, % 230.51/230.82 (~E(f1(f1(f1(f1(a5,f1(a4,f1(a5,a4))),f1(a4,f1(a5,a4))),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4))),f1(a2,f1(a4,f1(a5,a4))))), % 230.51/230.82 inference(scs_inference,[],[285,350,264,2,3])). % 230.51/230.82 cnf(355,plain, % 230.51/230.82 (~E(f1(a2,f1(a4,f1(a5,a4))),f1(f1(f1(f1(a5,f1(a4,f1(a5,a4))),f1(a4,f1(a5,a4))),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4))))), % 230.51/230.82 inference(scs_inference,[],[353,2])). % 230.51/230.82 cnf(356,plain, % 230.51/230.82 (~E(a4,f1(f1(a3,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))))), % 230.51/230.82 inference(scs_inference,[],[349,353,203,2,3])). % 230.51/230.82 cnf(358,plain, % 230.51/230.82 (~E(f1(f1(a3,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),a4)), % 230.51/230.82 inference(scs_inference,[],[356,2])). % 230.51/230.82 cnf(359,plain, % 230.51/230.82 (~E(f1(a3,f1(f1(f1(a5,f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4))),f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))))),a4)), % 230.51/230.82 inference(scs_inference,[],[356,157,286,2,3])). % 230.51/230.82 cnf(362,plain, % 230.51/230.82 (~E(a4,f1(a3,f1(f1(a5,f1(a4,f1(f1(a5,a4),f1(a4,f1(a5,a4))))),f1(a3,f1(a5,f1(a4,f1(a5,a4)))))))), % 230.51/230.82 inference(scs_inference,[],[289,128,359,2,3])). % 230.51/230.82 cnf(365,plain, % 230.51/230.82 (~E(f1(f1(f1(a3,f1(a5,f1(a4,f1(a5,a4)))),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)),f1(a4,f1(a5,a4)))), % 230.51/230.82 inference(scs_inference,[],[295,362,113,2,3])). % 230.51/230.82 cnf(367,plain, % 230.51/230.82 (~E(f1(a4,f1(a5,a4)),f1(f1(f1(a3,f1(a5,f1(a4,f1(a5,a4)))),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)))), % 230.51/230.82 inference(scs_inference,[],[365,2])). % 230.51/230.82 cnf(368,plain, % 230.51/230.82 (~E(a4,f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)))))), % 230.51/230.82 inference(scs_inference,[],[365,204,349,2,3])). % 230.51/230.82 cnf(370,plain, % 230.51/230.82 (~E(f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)))),a4)), % 230.51/230.82 inference(scs_inference,[],[368,2])). % 230.51/230.82 cnf(371,plain, % 230.51/230.82 (~E(f1(a5,f1(f1(a4,f1(a5,f1(a4,f1(a5,a4)))),f1(a5,f1(a4,f1(a5,a4))))),f1(a2,f1(a4,f1(a5,a4))))), % 230.51/230.82 inference(scs_inference,[],[104,368,296,2,3])). % 230.51/230.82 cnf(374,plain, % 230.51/230.82 (~E(a4,f1(a3,f1(a5,f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),a4)))))), % 230.51/230.82 inference(scs_inference,[],[371,266,212,2,3])). % 230.51/230.82 cnf(376,plain, % 230.51/230.82 (~E(f1(a3,f1(a5,f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),a4)))),a4)), % 230.51/230.82 inference(scs_inference,[],[374,2])). % 230.51/230.82 cnf(377,plain, % 230.51/230.82 (~E(f1(f1(f1(a5,a4),f1(a4,f1(a5,f1(a4,f1(a5,a4))))),f1(a3,f1(a5,a4))),f1(a2,f1(a4,f1(a5,a4))))), % 230.51/230.82 inference(scs_inference,[],[244,374,300,2,3])). % 230.51/230.82 cnf(379,plain, % 230.51/230.82 (~E(f1(a2,f1(a4,f1(a5,a4))),f1(f1(f1(a5,a4),f1(a4,f1(a5,f1(a4,f1(a5,a4))))),f1(a3,f1(a5,a4))))), % 230.51/230.82 inference(scs_inference,[],[377,2])). % 230.51/230.82 cnf(380,plain, % 230.51/230.82 (~E(a4,f1(f1(a3,f1(f1(f1(a5,a4),f1(f1(a4,f1(a5,a4)),f1(f1(a5,a4),f1(a4,f1(a5,a4))))),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))))), % 230.51/230.82 inference(scs_inference,[],[377,122,356,2,3])). % 230.51/230.82 cnf(382,plain, % 230.51/230.82 (~E(f1(f1(a3,f1(f1(f1(a5,a4),f1(f1(a4,f1(a5,a4)),f1(f1(a5,a4),f1(a4,f1(a5,a4))))),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),a4)), % 230.51/230.82 inference(scs_inference,[],[380,2])). % 230.51/230.82 cnf(383,plain, % 230.51/230.82 (~E(f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),a4)), % 230.51/230.82 inference(scs_inference,[],[258,380,309,2,3])). % 230.51/230.82 cnf(385,plain, % 230.51/230.82 (~E(a4,f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(a3,f1(a5,a4)))))), % 230.51/230.82 inference(scs_inference,[],[383,2])). % 230.51/230.82 cnf(386,plain, % 230.51/230.82 (~E(f1(a5,f1(a3,f1(f1(a5,a4),f1(a4,f1(a5,a4))))),f1(a2,f1(a4,f1(a5,a4))))), % 230.51/230.82 inference(scs_inference,[],[383,232,338,2,3])). % 230.51/230.82 cnf(389,plain, % 230.51/230.82 (~E(f1(f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4))),f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4))))),f1(a2,f1(a4,f1(a5,a4))))), % 230.51/230.82 inference(scs_inference,[],[386,140,305,2,3])). % 230.51/230.82 cnf(392,plain, % 230.51/230.82 (~E(a4,f1(a3,f1(f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4))),f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))))))), % 230.51/230.82 inference(scs_inference,[],[389,199,125,2,3])). % 230.51/230.82 cnf(395,plain, % 230.51/230.82 (~E(f1(a4,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a4,f1(a5,a4)))),f1(f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)),f1(a5,a4)))), % 230.51/230.82 inference(scs_inference,[],[331,392,306,2,3])). % 230.51/230.82 cnf(397,plain, % 230.51/230.82 (~E(f1(f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)),f1(a5,a4)),f1(a4,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a4,f1(a5,a4)))))), % 230.51/230.82 inference(scs_inference,[],[395,2])). % 230.51/230.82 cnf(398,plain, % 230.51/230.82 (~E(a4,f1(f1(f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)))), % 230.51/230.82 inference(scs_inference,[],[395,261,368,2,3])). % 230.51/230.82 cnf(400,plain, % 230.51/230.82 (~E(f1(f1(f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)),a4)), % 230.51/230.82 inference(scs_inference,[],[398,2])). % 230.51/230.82 cnf(401,plain, % 230.51/230.82 (~E(f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(a4,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a4,f1(a5,a4)))))), % 230.51/230.82 inference(scs_inference,[],[397,398,239,2,3])). % 230.51/230.82 cnf(404,plain, % 230.51/230.82 (~E(a4,f1(a3,f1(f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4))))),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))))), % 230.51/230.82 inference(scs_inference,[],[210,401,344,2,3])). % 230.51/230.82 cnf(406,plain, % 230.51/230.82 (~E(f1(a3,f1(f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4))))),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),a4)), % 230.51/230.82 inference(scs_inference,[],[404,2])). % 230.51/230.82 cnf(407,plain, % 230.51/230.82 (~E(f1(f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)),a4)), % 230.51/230.82 inference(scs_inference,[],[404,400,181,2,3])). % 230.51/230.82 cnf(409,plain, % 230.51/230.82 (~E(a4,f1(f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)))), % 230.51/230.82 inference(scs_inference,[],[407,2])). % 230.51/230.82 cnf(410,plain, % 230.51/230.82 (~E(a4,f1(a3,f1(f1(f1(f1(a5,a4),f1(a3,f1(a5,a4))),f1(a4,f1(a5,a4))),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))))), % 230.51/230.82 inference(scs_inference,[],[407,117,404,2,3])). % 230.51/230.82 cnf(412,plain, % 230.51/230.82 (~E(f1(a3,f1(f1(f1(f1(a5,a4),f1(a3,f1(a5,a4))),f1(a4,f1(a5,a4))),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),a4)), % 230.51/230.82 inference(scs_inference,[],[410,2])). % 230.51/230.82 cnf(413,plain, % 230.51/230.82 (~E(f1(a3,f1(f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4))),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),a4)), % 230.51/230.82 inference(scs_inference,[],[410,406,145,2,3])). % 230.51/230.82 cnf(415,plain, % 230.51/230.82 (~E(a4,f1(a3,f1(f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4))),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))))), % 230.51/230.82 inference(scs_inference,[],[413,2])). % 230.51/230.82 cnf(416,plain, % 230.51/230.82 (~E(a4,f1(a3,f1(f1(f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4))))),f1(a4,f1(a5,a4))),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))))), % 230.51/230.82 inference(scs_inference,[],[413,182,410,2,3])). % 230.51/230.82 cnf(419,plain, % 230.51/230.82 (~E(f1(f1(f1(a3,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)),a4)), % 230.51/230.82 inference(scs_inference,[],[15,358,416,2,3])). % 230.51/230.82 cnf(421,plain, % 230.51/230.82 (~E(a4,f1(f1(f1(a3,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)))), % 230.51/230.82 inference(scs_inference,[],[419,2])). % 230.51/230.82 cnf(422,plain, % 230.51/230.82 (~E(a4,f1(a3,f1(f1(f1(a5,a4),f1(a3,f1(a5,a4))),f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))))))), % 230.51/230.82 inference(scs_inference,[],[15,385,419,2,3])). % 230.51/230.82 cnf(424,plain, % 230.51/230.82 (~E(f1(a3,f1(f1(f1(a5,a4),f1(a3,f1(a5,a4))),f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))))),a4)), % 230.51/230.82 inference(scs_inference,[],[422,2])). % 230.51/230.82 cnf(429,plain, % 230.51/230.82 (~E(a4,f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))))), % 230.51/230.82 inference(scs_inference,[],[15,409,43,2,3])). % 230.51/230.82 cnf(431,plain, % 230.51/230.82 (~E(f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),a4)), % 230.51/230.82 inference(scs_inference,[],[429,2])). % 230.51/230.82 cnf(432,plain, % 230.51/230.82 (~E(f1(f1(a3,f1(f1(a5,f1(a4,f1(a5,a4))),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(a5,a4)),f1(a4,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a4,f1(a5,a4)))))), % 230.51/230.82 inference(scs_inference,[],[429,325,290,2,3])). % 230.51/230.82 cnf(434,plain, % 230.51/230.82 (~E(f1(a4,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a4,f1(a5,a4)))),f1(f1(a3,f1(f1(a5,f1(a4,f1(a5,a4))),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(a5,a4)))), % 230.51/230.82 inference(scs_inference,[],[432,2])). % 230.51/230.82 cnf(435,plain, % 230.51/230.82 (~E(f1(f1(f1(a3,f1(f1(f1(a5,a4),f1(f1(a4,f1(a5,a4)),f1(f1(a5,a4),f1(a4,f1(a5,a4))))),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)),a4)), % 230.51/230.82 inference(scs_inference,[],[15,432,382,2,3])). % 230.51/230.82 cnf(437,plain, % 230.51/230.82 (~E(a4,f1(f1(f1(a3,f1(f1(f1(a5,a4),f1(f1(a4,f1(a5,a4)),f1(f1(a5,a4),f1(a4,f1(a5,a4))))),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)))), % 230.51/230.82 inference(scs_inference,[],[435,2])). % 230.51/230.82 cnf(441,plain, % 230.51/230.82 (~E(f1(f1(a3,f1(a5,a4)),f1(a2,f1(a3,f1(a5,a4)))),f1(a3,f1(a2,f1(a4,f1(a5,a4)))))), % 230.51/230.82 inference(scs_inference,[],[63,2])). % 230.51/230.82 cnf(442,plain, % 230.51/230.82 (~E(f1(f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)),a4)), % 230.51/230.82 inference(scs_inference,[],[15,63,347,2,3])). % 230.51/230.82 cnf(444,plain, % 230.51/230.82 (~E(a4,f1(f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)))), % 230.51/230.82 inference(scs_inference,[],[442,2])). % 230.51/230.82 cnf(445,plain, % 230.51/230.82 (E(f1(x4451,f1(x4452,f1(f1(f1(x4453,x4454),f1(x4454,f1(x4453,x4454))),f1(x4452,f1(f1(x4453,x4454),x4452))))),f1(f1(x4451,f1(x4454,f1(x4453,x4454))),x4452))), % 230.51/230.82 inference(scs_inference,[],[15,442,248,2,3])). % 230.51/230.82 cnf(447,plain, % 230.51/230.82 (~E(f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4))))),f1(a2,f1(a4,f1(a5,a4))))), % 230.51/230.82 inference(scs_inference,[],[48,2])). % 230.51/230.82 cnf(448,plain, % 230.51/230.82 (~E(a4,f1(f1(a3,f1(a5,a4)),f1(f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4))),f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))))))), % 230.51/230.82 inference(scs_inference,[],[15,429,48,2,3])). % 230.51/230.82 cnf(451,plain, % 230.51/230.82 (~E(f1(a5,f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),a4))),f1(a2,f1(a4,f1(a5,a4))))), % 230.51/230.82 inference(scs_inference,[],[447,448,152,2,3])). % 230.51/230.82 cnf(454,plain, % 230.51/230.82 (~E(f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a2,f1(a3,f1(a5,a4)))),f1(a3,f1(a2,f1(a4,f1(a5,a4)))))), % 230.51/230.82 inference(scs_inference,[],[16,441,451,2,3])). % 230.51/230.82 cnf(456,plain, % 230.51/230.82 (~E(f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(a4,f1(a5,a4)))), % 230.51/230.82 inference(scs_inference,[],[77,2])). % 230.51/230.82 cnf(457,plain, % 230.51/230.82 (~E(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),a4)), % 230.51/230.82 inference(scs_inference,[],[77,165,309,2,3])). % 230.51/230.82 cnf(459,plain, % 230.51/230.82 (~E(f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4))))),f1(a2,f1(a4,f1(a5,a4))))), % 230.51/230.82 inference(scs_inference,[],[57,2])). % 230.51/230.82 cnf(460,plain, % 230.51/230.82 (~E(f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(f1(a3,f1(a5,a4)),f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4))))),f1(a2,f1(a4,f1(a5,a4))))), % 230.51/230.82 inference(scs_inference,[],[16,146,57,2,3])). % 230.51/230.82 cnf(463,plain, % 230.51/230.82 (~E(f1(f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)),f1(a5,a4)),a4)), % 230.51/230.82 inference(scs_inference,[],[407,176,9,2,3])). % 230.51/230.82 cnf(465,plain, % 230.51/230.82 (~E(a4,f1(f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)),f1(a5,a4)))), % 230.51/230.82 inference(scs_inference,[],[463,2])). % 230.51/230.82 cnf(466,plain, % 230.51/230.82 (~E(f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,f1(a4,f1(a5,a4))),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(a4,f1(a5,a4)))), % 230.51/230.82 inference(scs_inference,[],[16,463,292,2,3])). % 230.51/230.82 cnf(469,plain, % 230.51/230.82 (~E(f1(a4,f1(f1(a5,f1(a4,f1(a5,a4))),a4)),f1(f1(a3,f1(f1(a5,f1(a4,f1(a5,a4))),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(a5,a4)))), % 230.51/230.82 inference(scs_inference,[],[466,434,177,2,3])). % 230.51/230.82 cnf(471,plain, % 230.51/230.82 (~E(f1(f1(a3,f1(f1(a5,f1(a4,f1(a5,a4))),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(a5,a4)),f1(a4,f1(f1(a5,f1(a4,f1(a5,a4))),a4)))), % 230.51/230.82 inference(scs_inference,[],[469,2])). % 230.51/230.82 cnf(472,plain, % 230.51/230.82 (~E(f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,f1(a3,f1(a2,a4)))),f1(a4,f1(a2,f1(a3,f1(a5,a4)))))), % 230.51/230.82 inference(scs_inference,[],[16,469,201,2,3])). % 230.51/230.82 cnf(474,plain, % 230.51/230.82 (~E(f1(a4,f1(a2,f1(a3,f1(a5,a4)))),f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,f1(a3,f1(a2,a4)))))), % 230.51/230.82 inference(scs_inference,[],[472,2])). % 230.51/230.82 cnf(475,plain, % 230.51/230.82 (~E(f1(a3,f1(f1(a5,a4),f1(f1(f1(a3,f1(a5,a4)),f1(a5,a4)),f1(a5,a4)))),a4)), % 230.51/230.82 inference(scs_inference,[],[472,250,407,2,3])). % 230.51/230.82 cnf(477,plain, % 230.51/230.82 (~E(a4,f1(a3,f1(f1(a5,a4),f1(f1(f1(a3,f1(a5,a4)),f1(a5,a4)),f1(a5,a4)))))), % 230.51/230.82 inference(scs_inference,[],[475,2])). % 230.51/230.82 cnf(478,plain, % 230.51/230.82 (~E(f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(f1(f1(a5,a4),f1(a3,f1(a5,a4))),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4)))),a4)), % 230.51/230.82 inference(scs_inference,[],[16,475,335,2,3])). % 230.51/230.82 cnf(481,plain, % 230.51/230.82 (~E(f1(f1(a5,f1(a3,f1(f1(a5,a4),a4))),f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4))))),f1(a2,f1(a4,f1(a5,a4))))), % 230.51/230.82 inference(scs_inference,[],[478,389,111,2,3])). % 230.51/230.82 cnf(484,plain, % 230.51/230.82 (~E(a4,f1(a3,f1(a5,f1(f1(a3,f1(f1(a5,a4),a4)),f1(a5,f1(a3,f1(f1(a5,a4),a4)))))))), % 230.51/230.82 inference(scs_inference,[],[481,259,94,2,3])). % 230.51/230.82 cnf(486,plain, % 230.51/230.82 (~E(f1(a3,f1(a5,f1(f1(a3,f1(f1(a5,a4),a4)),f1(a5,f1(a3,f1(f1(a5,a4),a4)))))),a4)), % 230.51/230.82 inference(scs_inference,[],[484,2])). % 230.51/230.82 cnf(487,plain, % 230.51/230.82 (~E(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),a4)), % 230.51/230.82 inference(scs_inference,[],[18,431,484,2,3])). % 230.51/230.82 cnf(489,plain, % 230.51/230.82 (~E(a4,f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))))), % 230.51/230.82 inference(scs_inference,[],[487,2])). % 230.51/230.82 cnf(490,plain, % 230.51/230.82 (~E(a4,f1(f1(f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)),f1(f1(a5,a4),f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)))),f1(a5,a4)))), % 230.51/230.82 inference(scs_inference,[],[18,465,487,2,3])). % 230.51/230.82 cnf(492,plain, % 230.51/230.82 (~E(f1(f1(f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)),f1(f1(a5,a4),f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)))),f1(a5,a4)),a4)), % 230.51/230.82 inference(scs_inference,[],[490,2])). % 230.51/230.82 cnf(493,plain, % 230.51/230.82 (E(f1(f1(f1(x4931,f1(x4932,f1(x4931,x4932))),f1(x4932,f1(x4931,x4932))),f1(x4933,f1(f1(f1(x4931,x4932),f1(x4932,f1(x4931,x4932))),x4933))),f1(f1(x4931,x4932),x4933))), % 230.51/230.82 inference(scs_inference,[],[18,119,490,2,3])). % 230.51/230.82 cnf(495,plain, % 230.51/230.82 (~E(a4,f1(f1(f1(a3,f1(a5,a4)),f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4)))),f1(a5,a4)))), % 230.51/230.82 inference(scs_inference,[],[477,228,3])). % 230.51/230.82 cnf(497,plain, % 230.51/230.82 (~E(f1(f1(f1(a3,f1(a5,a4)),f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4)))),f1(a5,a4)),a4)), % 230.51/230.82 inference(scs_inference,[],[495,2])). % 230.51/230.82 cnf(498,plain, % 230.51/230.82 (E(f1(f1(x4981,x4982),f1(x4983,f1(f1(f1(x4981,x4982),f1(x4982,f1(x4981,x4982))),f1(x4983,f1(f1(x4981,x4982),x4983))))),f1(f1(x4981,x4982),x4983))), % 230.51/230.82 inference(scs_inference,[],[18,495,445,2,3])). % 230.51/230.82 cnf(512,plain, % 230.51/230.82 (~E(a4,f1(f1(a3,f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(a5,f1(f1(a4,f1(a5,a4)),f1(a5,f1(a4,f1(a5,a4)))))))), % 230.51/230.82 inference(scs_inference,[],[217,477,3])). % 230.51/230.82 cnf(514,plain, % 230.51/230.82 (~E(f1(f1(a3,f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(a5,f1(f1(a4,f1(a5,a4)),f1(a5,f1(a4,f1(a5,a4)))))),a4)), % 230.51/230.82 inference(scs_inference,[],[512,2])). % 230.51/230.82 cnf(515,plain, % 230.51/230.82 (~E(f1(f1(a3,f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(a5,a4)),a4)), % 230.51/230.82 inference(scs_inference,[],[497,512,214,2,3])). % 230.51/230.82 cnf(517,plain, % 230.51/230.82 (~E(a4,f1(f1(a3,f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(a5,a4)))), % 230.51/230.82 inference(scs_inference,[],[515,2])). % 230.51/230.82 cnf(518,plain, % 230.51/230.82 (~E(a4,f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)))))), % 230.51/230.82 inference(scs_inference,[],[19,515,444,2,3])). % 230.51/230.82 cnf(520,plain, % 230.51/230.82 (~E(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)))),a4)), % 230.51/230.82 inference(scs_inference,[],[518,2])). % 230.51/230.82 cnf(521,plain, % 230.51/230.82 (~E(f1(a3,f1(f1(f1(f1(a5,a4),f1(a3,f1(a5,a4))),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4)))),a4)), % 230.51/230.82 inference(scs_inference,[],[518,424,254,2,3])). % 230.51/230.82 cnf(523,plain, % 230.51/230.82 (~E(a4,f1(a3,f1(f1(f1(f1(a5,a4),f1(a3,f1(a5,a4))),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4)))))), % 230.51/230.82 inference(scs_inference,[],[521,2])). % 230.51/230.82 cnf(524,plain, % 230.51/230.82 (~E(a4,f1(f1(f1(a3,f1(a5,a4)),f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))))), % 230.51/230.82 inference(scs_inference,[],[19,517,521,2,3])). % 230.51/230.82 cnf(526,plain, % 230.51/230.82 (~E(f1(f1(f1(a3,f1(a5,a4)),f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),a4)), % 230.51/230.82 inference(scs_inference,[],[524,2])). % 230.51/230.82 cnf(527,plain, % 230.51/230.82 (~E(f1(f1(f1(a3,f1(a5,a4)),f1(a5,f1(a3,f1(f1(a5,a4),a4)))),f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(a4,f1(a5,a4)))), % 230.51/230.82 inference(scs_inference,[],[524,456,160,2,3])). % 230.51/230.82 cnf(530,plain, % 230.51/230.82 (~E(a4,f1(a3,f1(f1(f1(a5,f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4))))),a4),f1(a3,f1(a5,a4)))))), % 230.51/230.82 inference(scs_inference,[],[523,527,226,2,3])). % 230.51/230.82 cnf(533,plain, % 230.51/230.82 (~E(f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)),a4)), % 230.51/230.82 inference(scs_inference,[],[530,497,203,2,3])). % 230.51/230.82 cnf(535,plain, % 230.51/230.82 (~E(a4,f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)))), % 230.51/230.82 inference(scs_inference,[],[533,2])). % 230.51/230.82 cnf(536,plain, % 230.51/230.82 (~E(a4,f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(f1(a3,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4)))),f1(a5,a4)))))), % 230.51/230.82 inference(scs_inference,[],[19,533,421,2,3])). % 230.51/230.82 cnf(539,plain, % 230.51/230.82 (~E(f1(a3,f1(a5,f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),a4)))),a4)), % 230.51/230.82 inference(scs_inference,[],[536,376,204,2,3])). % 230.51/230.82 cnf(541,plain, % 230.51/230.82 (~E(a4,f1(a3,f1(a5,f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),a4)))))), % 230.51/230.82 inference(scs_inference,[],[539,2])). % 230.51/230.82 cnf(542,plain, % 230.51/230.82 (~E(a4,f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(f1(a3,f1(f1(f1(a5,a4),f1(f1(a4,f1(a5,a4)),f1(f1(a5,a4),f1(a4,f1(a5,a4))))),f1(a3,f1(a5,a4)))),f1(a5,a4)))))), % 230.51/230.82 inference(scs_inference,[],[19,539,437,2,3])). % 230.51/230.82 cnf(545,plain, % 230.51/230.82 (~E(f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),a4)))),a4)), % 230.51/230.82 inference(scs_inference,[],[370,542,215,2,3])). % 230.51/230.82 cnf(547,plain, % 230.51/230.82 (~E(a4,f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),a4)))))), % 230.51/230.82 inference(scs_inference,[],[545,2])). % 230.51/230.82 cnf(548,plain, % 230.51/230.82 (~E(a4,f1(f1(a3,f1(a5,a4)),f1(f1(f1(a5,a4),f1(a3,f1(a5,a4))),f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))))))), % 230.51/230.82 inference(scs_inference,[],[19,545,385,2,3])). % 230.51/230.82 cnf(550,plain, % 230.51/230.82 (~E(f1(f1(a3,f1(a5,a4)),f1(f1(f1(a5,a4),f1(a3,f1(a5,a4))),f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))))),a4)), % 230.51/230.82 inference(scs_inference,[],[548,2])). % 230.51/230.82 cnf(551,plain, % 230.51/230.82 (E(f1(f1(f1(f1(f1(x5511,x5512),f1(x5512,f1(x5511,x5512))),x5513),f1(x5514,f1(x5515,x5514))),x5516),f1(f1(x5515,x5514),f1(x5516,f1(f1(f1(x5511,x5512),x5513),x5516))))), % 230.51/230.82 inference(scs_inference,[],[22,548,198,2,3])). % 230.51/230.82 cnf(554,plain, % 230.51/230.82 (~E(f1(f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)),f1(f1(a5,a4),f1(f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)),f1(a5,a4)))),a4)), % 230.51/230.82 inference(scs_inference,[],[22,492,3])). % 230.51/230.82 cnf(557,plain, % 230.51/230.82 (~E(f1(f1(a3,f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(f1(a5,a4),f1(f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)),f1(a5,a4)))),a4)), % 230.51/230.82 inference(scs_inference,[],[554,209,2,3])). % 230.51/230.82 cnf(560,plain, % 230.51/230.82 (~E(a4,f1(a3,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(f1(a3,f1(a5,a4)),f1(f1(f1(a5,a4),f1(a3,f1(a5,a4))),f1(a3,f1(a5,a4)))))))), % 230.51/230.82 inference(scs_inference,[],[557,523,195,2,3])). % 230.51/230.82 cnf(563,plain, % 230.51/230.82 (~E(f1(f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)),f1(a5,f1(f1(a4,f1(a5,a4)),f1(a5,f1(a4,f1(a5,a4)))))),a4)), % 230.51/230.82 inference(scs_inference,[],[560,514,253,2,3])). % 230.51/230.82 cnf(566,plain, % 230.51/230.82 (~E(a4,f1(f1(a3,f1(f1(f1(a5,a4),f1(a3,f1(a5,a4))),f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))))),f1(a5,a4)))), % 230.51/230.82 inference(scs_inference,[],[22,563,129,2,3])). % 230.51/230.82 cnf(569,plain, % 230.51/230.82 (~E(f1(f1(a3,f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(a5,a4)),f1(a4,f1(f1(a5,f1(a4,f1(a5,a4))),a4)))), % 230.51/230.82 inference(scs_inference,[],[566,471,122,2,3])). % 230.51/230.82 cnf(571,plain, % 230.51/230.82 (~E(f1(a4,f1(f1(a5,f1(a4,f1(a5,a4))),a4)),f1(f1(a3,f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(a5,a4)))), % 230.51/230.82 inference(scs_inference,[],[569,2])). % 230.51/230.82 cnf(572,plain, % 230.51/230.82 (~E(f1(f1(f1(a3,f1(a5,a4)),f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a4,f1(f1(a5,f1(a4,f1(a5,a4))),a4)))), % 230.51/230.82 inference(scs_inference,[],[22,569,2,3])). % 230.51/230.82 cnf(574,plain, % 230.51/230.82 (~E(f1(a4,f1(f1(a5,f1(a4,f1(a5,a4))),a4)),f1(f1(f1(a3,f1(a5,a4)),f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))))), % 230.51/230.82 inference(scs_inference,[],[572,2])). % 230.51/230.82 cnf(575,plain, % 230.51/230.82 (~E(f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4)))),f1(a2,f1(a3,f1(a5,a4)))),f1(a3,f1(a2,f1(a4,f1(a5,a4)))))), % 230.51/230.82 inference(scs_inference,[],[572,454,290,2,3])). % 230.51/230.82 cnf(578,plain, % 230.51/230.82 (~E(f1(f1(f1(a3,f1(a5,a4)),f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a4,f1(f1(a5,a4),f1(a4,f1(a5,a4)))))), % 230.51/230.82 inference(scs_inference,[],[22,575,315,2,3])). % 230.51/230.82 cnf(581,plain, % 230.51/230.82 (~E(f1(f1(f1(a3,f1(a5,f1(a4,f1(a5,a4)))),f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),a4)), % 230.51/230.82 inference(scs_inference,[],[526,578,295,2,3])). % 230.51/230.82 cnf(584,plain, % 230.51/230.82 (~E(f1(a5,f1(f1(a4,f1(a2,a4)),f1(a5,f1(a4,f1(a2,a4))))),f1(f1(f1(a5,f1(a4,f1(a5,a4))),a4),f1(a3,f1(a5,a4))))), % 230.51/230.82 inference(scs_inference,[],[23,274,581,2,3])). % 230.51/230.82 cnf(586,plain, % 230.51/230.82 (~E(f1(f1(f1(a5,f1(a4,f1(a5,a4))),a4),f1(a3,f1(a5,a4))),f1(a5,f1(f1(a4,f1(a2,a4)),f1(a5,f1(a4,f1(a2,a4))))))), % 230.51/230.82 inference(scs_inference,[],[584,2])). % 230.51/230.82 cnf(587,plain, % 230.51/230.82 (~E(f1(f1(f1(a5,a4),f1(a4,f1(a5,f1(a4,f1(a5,a4))))),f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4))))),f1(a2,f1(a4,f1(a5,a4))))), % 230.51/230.82 inference(scs_inference,[],[459,584,300,2,3])). % 230.51/230.82 cnf(590,plain, % 230.51/230.82 (~E(f1(a3,f1(f1(a2,f1(a4,f1(a5,a4))),f1(a3,f1(a2,f1(a4,f1(a5,a4)))))),f1(f1(a3,f1(a5,a4)),f1(a5,f1(a3,f1(a2,a4)))))), % 230.51/230.82 inference(scs_inference,[],[23,205,587,2,3])). % 230.51/230.82 cnf(593,plain, % 230.51/230.82 (~E(f1(f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4))),f1(a5,f1(f1(a4,f1(a2,a4)),f1(a5,f1(a4,f1(a2,a4))))))), % 230.51/230.82 inference(scs_inference,[],[586,590,170,2,3])). % 230.51/230.82 cnf(596,plain, % 230.51/230.82 (~E(f1(a5,f1(f1(a4,f1(a2,a4)),f1(a5,f1(a4,f1(a2,a4))))),f1(a5,f1(a4,f1(a5,f1(a4,f1(a5,a4))))))), % 230.51/230.82 inference(scs_inference,[],[23,304,593,2,3])). % 230.51/230.82 cnf(598,plain, % 230.51/230.82 (~E(f1(a5,f1(a4,f1(a5,f1(a4,f1(a5,a4))))),f1(a5,f1(f1(a4,f1(a2,a4)),f1(a5,f1(a4,f1(a2,a4))))))), % 230.51/230.82 inference(scs_inference,[],[596,2])). % 230.51/230.82 cnf(599,plain, % 230.51/230.82 (E(f1(x5991,f1(f1(f1(f1(x5992,x5993),f1(x5993,f1(x5992,x5993))),f1(x5994,f1(f1(x5992,x5993),x5994))),f1(x5995,x5996))),f1(x5995,f1(f1(f1(f1(x5992,x5993),x5994),f1(x5991,x5996)),f1(x5995,f1(f1(f1(x5992,x5993),x5994),f1(x5991,x5996))))))), % 230.51/230.82 inference(scs_inference,[],[23,596,243,2,3])). % 230.51/230.82 cnf(605,plain, % 230.51/230.82 (~E(f1(a3,f1(a5,f1(a3,f1(f1(a5,a4),a4)))),a4)), % 230.51/230.82 inference(scs_inference,[],[486,92,3])). % 230.51/230.82 cnf(607,plain, % 230.51/230.82 (~E(a4,f1(a3,f1(a5,f1(a3,f1(f1(a5,a4),a4)))))), % 230.51/230.82 inference(scs_inference,[],[486,92,3,2])). % 230.51/230.82 cnf(608,plain, % 230.51/230.82 (~E(a4,f1(a3,f1(a5,f1(a3,f1(f1(a5,a4),f1(a4,f1(f1(a5,a4),a4)))))))), % 230.51/230.82 inference(scs_inference,[],[607,134,3])). % 230.51/230.82 cnf(610,plain, % 230.51/230.82 (~E(f1(a3,f1(a5,f1(a3,f1(f1(a5,a4),f1(a4,f1(f1(a5,a4),a4)))))),a4)), % 230.51/230.82 inference(scs_inference,[],[608,2])). % 230.51/230.82 cnf(611,plain, % 230.51/230.82 (~E(f1(a3,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4)))),a4)), % 230.51/230.82 inference(scs_inference,[],[605,608,266,2,3])). % 230.51/230.82 cnf(613,plain, % 230.51/230.82 (~E(a4,f1(a3,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4)))))), % 230.51/230.82 inference(scs_inference,[],[611,2])). % 230.51/230.82 cnf(614,plain, % 230.51/230.82 (~E(f1(a5,f1(f1(a4,f1(a2,a4)),f1(a5,f1(a4,f1(a2,a4))))),f1(f1(f1(f1(a5,f1(a4,f1(a5,a4))),f1(a4,f1(a5,a4))),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4))))), % 230.51/230.82 inference(scs_inference,[],[23,611,355,2,3])). % 230.51/230.82 cnf(617,plain, % 230.51/230.82 (~E(f1(a5,f1(a3,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),a4))),f1(a2,f1(a4,f1(a5,a4))))), % 230.51/230.82 inference(scs_inference,[],[25,460,614,2,3])). % 230.51/230.82 cnf(620,plain, % 230.51/230.82 (~E(a4,f1(a3,f1(f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4))),f1(a3,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4)))))))), % 230.51/230.82 inference(scs_inference,[],[25,613,617,2,3])). % 230.51/230.82 cnf(623,plain, % 230.51/230.82 (E(f1(f1(f1(f1(f1(x6231,x6232),f1(x6232,f1(x6231,x6232))),x6233),f1(x6233,f1(f1(x6231,x6232),x6233))),f1(x6234,f1(x6235,x6236))),f1(x6235,f1(x6234,f1(f1(f1(x6231,x6232),x6233),x6236))))), % 230.51/230.82 inference(scs_inference,[],[25,551,620,2,3])). % 230.51/230.82 cnf(626,plain, % 230.51/230.82 (~E(a4,f1(a4,f1(f1(a5,f1(a3,f1(a5,a4))),f1(a4,f1(a5,f1(a3,f1(a5,a4)))))))), % 230.51/230.82 inference(scs_inference,[],[25,284,3])). % 230.51/230.82 cnf(628,plain, % 230.51/230.82 (~E(f1(a4,f1(f1(a5,f1(a3,f1(a5,a4))),f1(a4,f1(a5,f1(a3,f1(a5,a4)))))),a4)), % 230.51/230.82 inference(scs_inference,[],[25,284,3,2])). % 230.51/230.82 cnf(629,plain, % 230.51/230.82 (~E(f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)),f1(a4,f1(a5,a4)))), % 230.51/230.82 inference(scs_inference,[],[222,270,3])). % 230.51/230.82 cnf(631,plain, % 230.51/230.82 (~E(f1(a4,f1(a5,a4)),f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)))), % 230.51/230.82 inference(scs_inference,[],[222,270,3,2])). % 230.51/230.82 cnf(632,plain, % 230.51/230.82 (~E(a4,f1(a3,f1(f1(f1(a5,a4),f1(f1(f1(a3,f1(a5,a4)),f1(a5,a4)),f1(a5,a4))),f1(a3,f1(f1(a5,a4),f1(f1(f1(a3,f1(a5,a4)),f1(a5,a4)),f1(a5,a4)))))))), % 230.51/230.82 inference(scs_inference,[],[25,524,3])). % 230.51/230.82 cnf(635,plain, % 230.51/230.82 (~E(f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4))),f1(a5,f1(f1(a4,f1(a2,a4)),f1(a5,f1(a4,f1(a2,a4))))))), % 230.51/230.82 inference(scs_inference,[],[632,593,192,2,3])). % 230.51/230.82 cnf(638,plain, % 230.51/230.82 (~E(f1(a5,f1(f1(a3,f1(a5,a4)),f1(a2,a4))),f1(a2,f1(a4,f1(a5,a4))))), % 230.51/230.82 inference(scs_inference,[],[25,635,277,2,3])). % 230.51/230.82 cnf(640,plain, % 230.51/230.82 (~E(f1(a2,f1(a4,f1(a5,a4))),f1(a5,f1(f1(a3,f1(a5,a4)),f1(a2,a4))))), % 230.51/230.82 inference(scs_inference,[],[638,2])). % 230.51/230.82 cnf(641,plain, % 230.51/230.82 (~E(f1(a5,f1(f1(a3,f1(a5,f1(a4,f1(a5,a4)))),f1(a2,a4))),f1(a2,f1(a4,f1(a5,a4))))), % 230.51/230.82 inference(scs_inference,[],[638,296,2,3])). % 230.51/230.82 cnf(643,plain, % 230.51/230.82 (~E(f1(a2,f1(a4,f1(a5,a4))),f1(a5,f1(f1(a3,f1(a5,f1(a4,f1(a5,a4)))),f1(a2,a4))))), % 230.51/230.82 inference(scs_inference,[],[641,2])). % 230.51/230.82 cnf(644,plain, % 230.51/230.82 (~E(f1(a4,f1(a5,f1(a3,f1(a5,a4)))),a4)), % 230.51/230.82 inference(scs_inference,[],[25,641,287,2,3])). % 230.51/230.82 cnf(646,plain, % 230.51/230.82 (~E(a4,f1(a4,f1(a5,f1(a3,f1(a5,a4)))))), % 230.51/230.82 inference(scs_inference,[],[644,2])). % 230.51/230.82 cnf(647,plain, % 230.51/230.82 (~E(f1(a4,f1(a5,f1(a3,f1(a5,f1(a4,f1(a5,a4)))))),a4)), % 230.51/230.82 inference(scs_inference,[],[644,301,2,3])). % 230.51/230.82 cnf(650,plain, % 230.51/230.82 (~E(a4,f1(a4,f1(a5,f1(f1(a3,f1(a5,a4)),f1(a5,f1(a3,f1(a5,a4)))))))), % 230.51/230.82 inference(scs_inference,[],[646,647,259,2,3])). % 230.51/230.82 cnf(653,plain, % 230.51/230.82 (E(f1(f1(f1(f1(f1(x6531,x6532),f1(x6532,f1(x6531,x6532))),x6533),f1(x6534,f1(x6535,x6534))),x6536),f1(f1(f1(f1(x6531,x6532),x6533),f1(x6533,f1(f1(x6531,x6532),x6533))),f1(x6536,f1(f1(x6535,x6534),x6536))))), % 230.51/230.82 inference(scs_inference,[],[26,650,551,2,3])). % 230.51/230.82 cnf(664,plain, % 230.51/230.82 (~E(f1(a4,f1(f1(a5,a4),a4)),f1(f1(a3,f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(a5,a4)))), % 230.51/230.82 inference(scs_inference,[],[571,97,3])). % 230.51/230.82 cnf(666,plain, % 230.51/230.82 (~E(f1(f1(a3,f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(a5,a4)),f1(a4,f1(f1(a5,a4),a4)))), % 230.51/230.82 inference(scs_inference,[],[571,97,3,2])). % 230.51/230.82 cnf(667,plain, % 230.51/230.82 (~E(f1(a4,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a4,f1(f1(a5,a4),a4)))),f1(f1(a3,f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(a5,a4)))), % 230.51/230.82 inference(scs_inference,[],[664,107,3])). % 230.51/230.82 cnf(669,plain, % 230.51/230.82 (~E(f1(f1(a3,f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(a5,a4)),f1(a4,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a4,f1(f1(a5,a4),a4)))))), % 230.51/230.82 inference(scs_inference,[],[664,107,3,2])). % 230.51/230.82 cnf(670,plain, % 230.51/230.82 (~E(f1(f1(a3,f1(a5,a4)),f1(f1(f1(a5,a4),f1(a3,f1(a5,a4))),f1(a3,f1(a5,a4)))),a4)), % 230.51/230.82 inference(scs_inference,[],[550,102,3])). % 230.51/230.82 cnf(673,plain, % 230.51/230.82 (~E(f1(a4,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a4,f1(a5,a4)))),f1(f1(f1(a3,f1(a5,a4)),f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))))), % 230.51/230.82 inference(scs_inference,[],[574,184,3])). % 230.51/230.82 cnf(675,plain, % 230.51/230.82 (~E(f1(f1(f1(a3,f1(a5,a4)),f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a4,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a4,f1(a5,a4)))))), % 230.51/230.82 inference(scs_inference,[],[574,184,3,2])). % 230.51/230.82 cnf(676,plain, % 230.51/230.82 (~E(f1(f1(a3,f1(a5,a4)),f1(f1(a5,f1(a3,f1(f1(a5,a4),a4))),f1(a3,f1(a5,a4)))),a4)), % 230.51/230.82 inference(scs_inference,[],[670,156,3])). % 230.51/230.82 cnf(687,plain, % 230.51/230.82 (~E(f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,f1(a3,f1(f1(a5,a4),a4)))),a4)), % 230.51/230.82 inference(scs_inference,[],[29,541,3,2])). % 230.51/230.82 cnf(688,plain, % 230.51/230.82 (~E(f1(f1(a3,f1(a5,a4)),f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4)))),a4)), % 230.51/230.82 inference(scs_inference,[],[457,306,3])). % 230.51/230.82 cnf(693,plain, % 230.51/230.82 (~E(f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4))),f1(a3,f1(a5,a4)))),a4)), % 230.51/230.82 inference(scs_inference,[],[29,415,3,2])). % 230.51/230.82 cnf(694,plain, % 230.51/230.82 (~E(f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(f1(a5,a4),f1(a3,f1(a5,a4))),f1(a3,f1(a5,a4)))),a4)), % 230.51/230.82 inference(scs_inference,[],[693,199,3])). % 230.51/230.82 cnf(697,plain, % 230.51/230.83 (~E(f1(a3,f1(f1(f1(a5,a4),f1(a3,f1(a5,a4))),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),a4)), % 230.51/230.83 inference(scs_inference,[],[29,694,2,3])). % 230.51/230.83 cnf(700,plain, % 230.51/230.83 (~E(f1(f1(a3,f1(a5,a4)),f1(f1(f1(a5,f1(a4,f1(a5,a4))),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4)))),a4)), % 230.51/230.83 inference(scs_inference,[],[688,697,286,2,3])). % 230.51/230.83 cnf(703,plain, % 230.51/230.83 (~E(a4,f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),a4)))))), % 230.51/230.83 inference(scs_inference,[],[29,700,547,2,3])). % 230.51/230.83 cnf(706,plain, % 230.51/230.83 (~E(f1(f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a4,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a4,f1(a5,a4)))))), % 230.51/230.83 inference(scs_inference,[],[675,703,275,2,3])). % 230.51/230.83 cnf(708,plain, % 230.51/230.83 (~E(f1(a4,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a4,f1(a5,a4)))),f1(f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))))), % 230.51/230.83 inference(scs_inference,[],[706,2])). % 230.51/230.83 cnf(709,plain, % 230.51/230.83 (~E(f1(a5,f1(a3,f1(f1(a5,a4),a4))),f1(a5,f1(f1(a4,f1(a2,a4)),f1(a5,f1(a4,f1(a2,a4))))))), % 230.51/230.83 inference(scs_inference,[],[29,706,635,2,3])). % 230.51/230.83 cnf(711,plain, % 230.51/230.83 (~E(f1(a5,f1(f1(a4,f1(a2,a4)),f1(a5,f1(a4,f1(a2,a4))))),f1(a5,f1(a3,f1(f1(a5,a4),a4))))), % 230.51/230.83 inference(scs_inference,[],[709,2])). % 230.51/230.83 cnf(712,plain, % 230.51/230.83 (E(f1(f1(f1(f1(x7121,x7122),f1(x7122,f1(x7121,x7122))),f1(f1(x7122,f1(x7121,x7122)),f1(f1(x7121,x7122),f1(x7122,f1(x7121,x7122))))),f1(x7123,f1(x7124,x7125))),f1(x7124,f1(x7123,f1(f1(x7121,x7122),x7125))))), % 230.51/230.83 inference(scs_inference,[],[29,709,236,2,3])). % 230.51/230.83 cnf(714,plain, % 230.51/230.83 (~E(f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a4,f1(a5,a4)))), % 230.51/230.83 inference(scs_inference,[],[30,629,3])). % 230.51/230.83 cnf(717,plain, % 230.51/230.83 (~E(f1(f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a4,f1(a5,a4)))), % 230.51/230.83 inference(scs_inference,[],[714,138,2,3])). % 230.51/230.83 cnf(720,plain, % 230.51/230.83 (~E(a4,f1(a3,f1(f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(f1(a4,f1(a5,a4)),f1(f1(a5,a4),f1(a4,f1(a5,a4))))),f1(a3,f1(a5,a4)))))), % 230.51/230.83 inference(scs_inference,[],[717,599,620,2,3])). % 230.51/230.83 cnf(723,plain, % 230.51/230.83 (~E(f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4)))),a4)), % 230.51/230.83 inference(scs_inference,[],[687,720,266,2,3])). % 230.51/230.83 cnf(726,plain, % 230.51/230.83 (~E(a4,f1(a3,f1(f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4))))),f1(a3,f1(a5,a4)))))), % 230.51/230.83 inference(scs_inference,[],[723,117,523,2,3])). % 230.51/230.83 cnf(728,plain, % 230.51/230.83 (~E(f1(a3,f1(f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4))))),f1(a3,f1(a5,a4)))),a4)), % 230.51/230.83 inference(scs_inference,[],[726,2])). % 230.51/230.83 cnf(729,plain, % 230.51/230.83 (~E(f1(a5,f1(f1(a3,f1(a5,a4)),f1(f1(f1(a5,a4),a4),f1(a3,f1(a5,a4))))),f1(a5,f1(f1(a4,f1(a2,a4)),f1(a5,f1(a4,f1(a2,a4))))))), % 230.51/230.83 inference(scs_inference,[],[726,250,593,2,3])). % 230.51/230.83 cnf(732,plain, % 230.51/230.83 (~E(a4,f1(a3,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a3,f1(f1(f1(a5,a4),f1(a3,f1(a5,a4))),f1(a3,f1(a5,a4)))))))), % 230.51/230.83 inference(scs_inference,[],[729,141,94,2,3])). % 230.51/230.83 cnf(734,plain, % 230.51/230.83 (~E(f1(a3,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a3,f1(f1(f1(a5,a4),f1(a3,f1(a5,a4))),f1(a3,f1(a5,a4)))))),a4)), % 230.51/230.83 inference(scs_inference,[],[732,2])). % 230.51/230.83 cnf(735,plain, % 230.51/230.83 (~E(f1(a4,f1(a5,f1(a4,f1(f1(a5,a4),a4)))),f1(f1(f1(a3,f1(a5,a4)),f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))))), % 230.51/230.83 inference(scs_inference,[],[673,732,112,2,3])). % 230.51/230.83 cnf(737,plain, % 230.51/230.83 (~E(f1(f1(f1(a3,f1(a5,a4)),f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a4,f1(a5,f1(a4,f1(f1(a5,a4),a4)))))), % 230.51/230.83 inference(scs_inference,[],[735,2])). % 230.51/230.83 cnf(738,plain, % 230.51/230.83 (~E(a4,f1(a4,f1(f1(a5,f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4))))),f1(a4,f1(a5,f1(a3,f1(a5,a4)))))))), % 230.51/230.83 inference(scs_inference,[],[735,626,128,2,3])). % 230.51/230.83 cnf(741,plain, % 230.51/230.83 (~E(f1(a4,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),a4)),f1(f1(a3,f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(a5,a4)))), % 230.51/230.83 inference(scs_inference,[],[667,738,177,2,3])). % 230.51/230.83 cnf(743,plain, % 230.51/230.83 (~E(f1(f1(a3,f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(a5,a4)),f1(a4,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),a4)))), % 230.51/230.83 inference(scs_inference,[],[741,2])). % 230.51/230.83 cnf(744,plain, % 230.51/230.83 (~E(a4,f1(a3,f1(f1(f1(a5,f1(a4,f1(a5,a4))),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4)))))), % 230.51/230.83 inference(scs_inference,[],[741,613,182,2,3])). % 230.51/230.83 cnf(746,plain, % 230.51/230.83 (~E(f1(a3,f1(f1(f1(a5,f1(a4,f1(a5,a4))),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4)))),a4)), % 230.51/230.83 inference(scs_inference,[],[744,2])). % 230.51/230.83 cnf(747,plain, % 230.51/230.83 (E(f1(f1(f1(f1(f1(x7471,x7472),f1(x7472,f1(x7471,x7472))),x7473),f1(x7474,f1(x7475,x7474))),x7476),f1(f1(f1(x7475,x7474),f1(x7473,f1(f1(x7471,x7472),x7473))),x7476))), % 230.51/230.83 inference(scs_inference,[],[32,744,653,2,3])). % 230.51/230.83 cnf(750,plain, % 230.51/230.83 (~E(a4,f1(f1(f1(f1(a3,f1(a5,a4)),f1(a5,a4)),f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(f1(a5,a4),f1(a3,f1(a5,a4)))))), % 230.51/230.83 inference(scs_inference,[],[32,517,3])). % 230.51/230.83 cnf(752,plain, % 230.51/230.83 (~E(f1(f1(f1(f1(a3,f1(a5,a4)),f1(a5,a4)),f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),a4)), % 230.51/230.83 inference(scs_inference,[],[750,2])). % 230.51/230.83 cnf(753,plain, % 230.51/230.83 (E(f1(f1(f1(f1(f1(x7531,x7532),f1(x7532,f1(x7531,x7532))),x7533),f1(x7533,f1(f1(x7531,x7532),x7533))),f1(x7534,f1(x7535,x7534))),f1(f1(x7535,f1(x7533,f1(f1(x7531,x7532),x7533))),x7534))), % 230.51/230.83 inference(scs_inference,[],[32,750,747,2,3])). % 230.51/230.83 cnf(756,plain, % 230.51/230.83 (~E(a4,f1(a3,f1(f1(f1(a5,f1(f1(a4,f1(a5,a4)),f1(a5,f1(a4,f1(a5,a4))))),a4),f1(a3,f1(a5,a4)))))), % 230.51/230.83 inference(scs_inference,[],[744,226,3])). % 230.51/230.83 cnf(759,plain, % 230.51/230.83 (~E(f1(f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)),f1(a5,a4)),f1(a4,f1(f1(a5,a4),a4)))), % 230.51/230.83 inference(scs_inference,[],[666,756,253,2,3])). % 230.51/230.83 cnf(761,plain, % 230.51/230.83 (~E(f1(a4,f1(f1(a5,a4),a4)),f1(f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)),f1(a5,a4)))), % 230.51/230.83 inference(scs_inference,[],[759,2])). % 230.51/230.83 cnf(762,plain, % 230.51/230.83 (~E(a4,f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)))))), % 230.51/230.83 inference(scs_inference,[],[32,759,444,2,3])). % 230.51/230.83 cnf(765,plain, % 230.51/230.83 (~E(f1(a4,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a4,f1(f1(a5,a4),a4)))),f1(f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)),f1(a5,a4)))), % 230.51/230.83 inference(scs_inference,[],[761,762,107,2,3])). % 230.51/230.83 cnf(767,plain, % 230.51/230.83 (~E(f1(f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)),f1(a5,a4)),f1(a4,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a4,f1(f1(a5,a4),a4)))))), % 230.51/230.83 inference(scs_inference,[],[765,2])). % 230.51/230.83 cnf(768,plain, % 230.51/230.83 (~E(a4,f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)))))), % 230.51/230.83 inference(scs_inference,[],[32,765,409,2,3])). % 230.51/230.83 cnf(770,plain, % 230.51/230.83 (~E(f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)))),a4)), % 230.51/230.83 inference(scs_inference,[],[768,2])). % 230.51/230.83 cnf(771,plain, % 230.51/230.83 (~E(f1(a3,f1(f1(a5,a4),f1(f1(f1(a3,f1(a5,a4)),f1(a5,a4)),f1(a5,a4)))),f1(a4,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a4,f1(f1(a5,a4),a4)))))), % 230.51/230.83 inference(scs_inference,[],[768,767,261,2,3])). % 230.51/230.83 cnf(773,plain, % 230.51/230.83 (~E(f1(a4,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a4,f1(f1(a5,a4),a4)))),f1(a3,f1(f1(a5,a4),f1(f1(f1(a3,f1(a5,a4)),f1(a5,a4)),f1(a5,a4)))))), % 230.51/230.83 inference(scs_inference,[],[771,2])). % 230.51/230.83 cnf(774,plain, % 230.51/230.83 (~E(a4,f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(f1(a3,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4)))),f1(a5,a4)))))), % 230.51/230.83 inference(scs_inference,[],[32,771,421,2,3])). % 230.51/230.83 cnf(777,plain, % 230.51/230.83 (~E(f1(f1(a3,f1(a5,f1(a4,f1(a5,a4)))),f1(f1(a5,a4),f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)))),a4)), % 230.51/230.83 inference(scs_inference,[],[520,774,280,2,3])). % 230.51/230.83 cnf(780,plain, % 230.51/230.83 (~E(a4,f1(a3,f1(f1(f1(a5,a4),f1(f1(a4,f1(a5,a4)),f1(a5,f1(a4,f1(a5,a4))))),f1(a3,f1(a5,a4)))))), % 230.51/230.83 inference(scs_inference,[],[777,145,744,2,3])). % 230.51/230.83 cnf(782,plain, % 230.51/230.83 (~E(f1(a3,f1(f1(f1(a5,a4),f1(f1(a4,f1(a5,a4)),f1(a5,f1(a4,f1(a5,a4))))),f1(a3,f1(a5,a4)))),a4)), % 230.51/230.83 inference(scs_inference,[],[780,2])). % 230.51/230.83 cnf(786,plain, % 230.51/230.83 (~E(a4,f1(f1(f1(a3,f1(a5,a4)),f1(f1(f1(a5,a4),f1(a3,f1(a5,a4))),f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))))),f1(a5,a4)))), % 230.51/230.83 inference(scs_inference,[],[33,444,3])). % 230.51/230.83 cnf(788,plain, % 230.51/230.83 (~E(f1(f1(f1(a3,f1(a5,a4)),f1(f1(f1(a5,a4),f1(a3,f1(a5,a4))),f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))))),f1(a5,a4)),a4)), % 230.51/230.83 inference(scs_inference,[],[786,2])). % 230.51/230.83 cnf(791,plain, % 230.51/230.83 (~E(a4,f1(f1(f1(a3,f1(a5,a4)),f1(f1(f1(a5,a4),f1(a3,f1(a5,a4))),f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))))),f1(a5,a4)))), % 230.51/230.83 inference(scs_inference,[],[33,409,3])). % 230.51/230.83 cnf(794,plain, % 230.51/230.83 (~E(f1(f1(f1(a3,f1(a5,a4)),f1(f1(f1(a5,a4),f1(a3,f1(a5,a4))),f1(a3,f1(a5,a4)))),f1(a5,a4)),a4)), % 230.51/230.83 inference(scs_inference,[],[788,791,133,2,3])). % 230.51/230.83 cnf(797,plain, % 230.51/230.83 (~E(a4,f1(a3,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))))))), % 230.51/230.83 inference(scs_inference,[],[794,237,94,2,3])). % 230.51/230.83 cnf(799,plain, % 230.51/230.83 (~E(f1(a3,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))))),a4)), % 230.51/230.83 inference(scs_inference,[],[797,2])). % 230.51/230.83 cnf(803,plain, % 230.51/230.83 (~E(a4,f1(a3,f1(f1(a5,f1(a4,f1(a5,a4))),f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))))))), % 230.51/230.83 inference(scs_inference,[],[780,152,3])). % 230.51/230.83 cnf(805,plain, % 230.51/230.83 (~E(f1(a3,f1(f1(a5,f1(a4,f1(a5,a4))),f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))))),a4)), % 230.51/230.83 inference(scs_inference,[],[803,2])). % 230.51/230.83 cnf(806,plain, % 230.51/230.83 (~E(f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),a4)))),a4)), % 230.51/230.83 inference(scs_inference,[],[803,770,215,2,3])). % 230.51/230.83 cnf(809,plain, % 230.51/230.83 (~E(f1(a3,f1(f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4)))),a4)), % 230.51/230.83 inference(scs_inference,[],[806,799,254,2,3])). % 230.51/230.83 cnf(812,plain, % 230.51/230.83 (~E(a4,f1(f1(a3,f1(a5,a4)),f1(a5,a4)))), % 230.51/230.83 inference(scs_inference,[],[36,809,448,2,3])). % 230.51/230.83 cnf(814,plain, % 230.51/230.83 (~E(f1(f1(a3,f1(a5,a4)),f1(a5,a4)),a4)), % 230.51/230.83 inference(scs_inference,[],[812,2])). % 230.51/230.83 cnf(815,plain, % 230.51/230.83 (~E(f1(f1(f1(f1(a3,f1(a5,a4)),f1(a5,a4)),f1(f1(a5,f1(a4,f1(a5,a4))),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),a4)), % 230.51/230.83 inference(scs_inference,[],[812,752,290,2,3])). % 230.51/230.83 cnf(818,plain, % 230.51/230.83 (~E(a4,f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))))))), % 230.51/230.83 inference(scs_inference,[],[815,498,812,2,3])). % 230.51/230.83 cnf(821,plain, % 230.51/230.83 (~E(f1(f1(a3,f1(a5,f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),a4)))),f1(a5,a4)),f1(a4,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),a4)))), % 230.51/230.83 inference(scs_inference,[],[743,818,160,2,3])). % 230.51/230.83 cnf(824,plain, % 230.51/230.83 (~E(a4,f1(f1(f1(a3,f1(a5,f1(a4,f1(a5,a4)))),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)))), % 230.51/230.83 inference(scs_inference,[],[535,127,821,2,3])). % 230.51/230.83 cnf(827,plain, % 230.51/230.83 (~E(f1(f1(f1(a3,f1(a5,f1(a4,f1(a5,a4)))),f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a4,f1(a5,f1(a4,f1(f1(a5,a4),a4)))))), % 230.51/230.83 inference(scs_inference,[],[824,737,295,2,3])). % 230.51/230.83 cnf(829,plain, % 230.51/230.83 (~E(f1(a4,f1(a5,f1(a4,f1(f1(a5,a4),a4)))),f1(f1(f1(a3,f1(a5,f1(a4,f1(a5,a4)))),f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))))), % 230.51/230.83 inference(scs_inference,[],[827,2])). % 230.51/230.83 cnf(851,plain, % 230.51/230.83 (~E(f1(f1(f1(a5,a4),f1(a3,f1(a5,a4))),f1(a3,f1(a5,a4))),f1(a2,f1(a4,f1(a5,a4))))), % 230.51/230.83 inference(scs_inference,[],[140,92,3])). % 230.51/230.83 cnf(854,plain, % 230.51/230.83 (~E(f1(a5,f1(a3,f1(f1(a5,f1(a4,f1(a5,a4))),f1(a4,f1(a5,a4))))),f1(a2,f1(a4,f1(a5,a4))))), % 230.51/230.83 inference(scs_inference,[],[386,291,3])). % 230.51/230.83 cnf(857,plain, % 230.51/230.83 (~E(f1(f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4))),f1(a3,f1(a5,a4))),f1(a2,f1(a4,f1(a5,a4))))), % 230.51/230.83 inference(scs_inference,[],[851,854,305,2,3])). % 230.51/230.83 cnf(860,plain, % 230.51/230.83 (~E(f1(f1(a3,f1(a5,a4)),f1(a5,f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),a4)))),a4)), % 230.51/230.83 inference(scs_inference,[],[857,545,91,2,3])). % 230.51/230.83 cnf(863,plain, % 230.51/230.83 (~E(f1(f1(a5,f1(a3,f1(f1(a5,a4),a4))),f1(a3,f1(a5,a4))),f1(a2,f1(a4,f1(a5,a4))))), % 230.51/230.83 inference(scs_inference,[],[860,857,111,2,3])). % 230.51/230.83 cnf(866,plain, % 230.51/230.83 (~E(f1(a5,f1(a3,f1(f1(a5,a4),f1(a4,f1(f1(a5,a4),a4))))),f1(a2,f1(a4,f1(a5,a4))))), % 230.51/230.83 inference(scs_inference,[],[863,617,232,2,3])). % 230.51/230.83 cnf(869,plain, % 230.51/230.83 (~E(f1(f1(a3,f1(a5,a4)),f1(a5,f1(a4,f1(a5,a4)))),a4)), % 230.51/230.83 inference(scs_inference,[],[814,866,271,2,3])). % 230.51/230.83 cnf(871,plain, % 230.51/230.83 (~E(a4,f1(f1(a3,f1(a5,a4)),f1(a5,f1(a4,f1(a5,a4)))))), % 230.51/230.83 inference(scs_inference,[],[869,2])). % 230.51/230.83 cnf(891,plain, % 230.51/230.83 (~E(f1(a4,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),a4)),f1(a3,f1(f1(a5,a4),f1(f1(f1(a3,f1(a5,a4)),f1(a5,a4)),f1(a5,a4)))))), % 230.51/230.83 inference(scs_inference,[],[773,177,3])). % 230.51/230.83 cnf(896,plain, % 230.51/230.83 (E(f1(x8961,f1(f1(f1(x8962,x8963),x8964),x8965)),f1(x8961,f1(f1(f1(f1(x8962,x8963),f1(x8963,f1(x8962,x8963))),f1(x8964,f1(f1(x8962,x8963),x8964))),x8965)))), % 230.51/230.83 inference(scs_inference,[],[106,5])). % 230.51/230.83 cnf(898,plain, % 230.51/230.83 (~E(f1(a4,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a4,f1(f1(a5,a4),f1(a4,f1(a5,a4)))))),f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)))), % 230.51/230.83 inference(scs_inference,[],[631,106,36,5,4,3])). % 230.51/230.83 cnf(904,plain, % 230.51/230.83 (~E(f1(a3,f1(f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4))),f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))))),a4)), % 230.51/230.83 inference(scs_inference,[],[898,358,228,214,5,2,4,3])). % 230.51/230.83 cnf(910,plain, % 230.51/230.83 (~E(f1(a3,f1(a5,f1(a4,f1(f1(a5,a4),f1(a3,f1(f1(a5,a4),a4)))))),a4)), % 230.51/230.83 inference(scs_inference,[],[904,610,107,161,5,2,4,3])). % 230.51/230.83 cnf(915,plain, % 230.51/230.83 (E(f1(f1(f1(x9151,f1(f1(x9152,f1(x9151,x9152)),f1(x9151,f1(x9152,f1(x9151,x9152))))),x9153),x9154),f1(f1(f1(x9151,x9152),x9153),x9154))), % 230.51/230.83 inference(scs_inference,[],[910,165,5,2,4])). % 230.51/230.83 cnf(916,plain, % 230.51/230.83 (E(f1(f1(f1(f1(f1(x9161,x9162),f1(x9162,f1(x9161,x9162))),x9163),f1(x9163,f1(f1(x9161,x9162),x9163))),x9164),f1(f1(f1(x9161,x9162),x9163),x9164))), % 230.51/230.83 inference(scs_inference,[],[42,910,653,165,5,2,4,3])). % 230.51/230.83 cnf(920,plain, % 230.51/230.83 (E(f1(f1(x9201,f1(x9202,f1(f1(x9203,f1(x9202,x9203)),f1(x9202,f1(x9203,f1(x9202,x9203)))))),x9204),f1(f1(x9201,f1(x9202,x9203)),x9204))), % 230.51/230.83 inference(scs_inference,[],[166,5,4])). % 230.51/230.83 cnf(923,plain, % 230.51/230.83 (E(f1(x9231,f1(x9232,x9233)),f1(x9231,f1(x9232,f1(f1(x9233,f1(x9232,x9233)),f1(x9232,f1(x9233,f1(x9232,x9233)))))))), % 230.51/230.83 inference(scs_inference,[],[36,5])). % 230.51/230.83 cnf(928,plain, % 230.51/230.83 (~E(f1(f1(a3,f1(a5,f1(a4,f1(a5,a4)))),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),a4)), % 230.51/230.83 inference(scs_inference,[],[367,2,4])). % 230.51/230.83 cnf(929,plain, % 230.51/230.83 (E(f1(x9291,f1(f1(f1(x9292,x9293),x9294),x9295)),f1(x9291,f1(f1(f1(f1(x9292,x9293),f1(x9293,f1(x9292,x9293))),x9294),x9295)))), % 230.51/230.83 inference(scs_inference,[],[305,5])). % 230.51/230.83 cnf(932,plain, % 230.51/230.83 (~E(f1(a3,f1(a5,f1(f1(a4,f1(a5,a4)),f1(a5,f1(a4,f1(a5,a4)))))),f1(a3,f1(a2,f1(a4,f1(a5,a4)))))), % 230.51/230.83 inference(scs_inference,[],[318,928,923,305,5,2,4,3])). % 230.51/230.83 cnf(936,plain, % 230.51/230.83 (E(f1(f1(x9361,f1(f1(x9362,x9363),x9364)),x9365),f1(f1(x9361,f1(f1(f1(x9362,x9363),f1(x9363,f1(x9362,x9363))),x9364)),x9365))), % 230.51/230.83 inference(scs_inference,[],[932,306,5,2,4])). % 230.51/230.83 cnf(942,plain, % 230.51/230.83 (~E(f1(a4,f1(a5,f1(f1(a4,f1(a5,a4)),f1(a5,f1(a4,f1(a5,a4)))))),f1(a3,f1(f1(a5,a4),f1(f1(f1(a3,f1(a5,a4)),f1(a5,a4)),f1(a5,a4)))))), % 230.51/230.83 inference(scs_inference,[],[260,923,215,5,4,3])). % 230.51/230.83 cnf(947,plain, % 230.51/230.83 (E(f1(f1(x9471,f1(f1(x9472,x9473),f1(f1(x9474,x9475),f1(x9476,f1(x9474,x9475))))),x9477),f1(f1(x9474,f1(f1(x9476,f1(x9473,f1(x9472,x9473))),f1(x9471,x9475))),x9477))), % 230.51/230.83 inference(scs_inference,[],[152,5,4])). % 230.51/230.83 cnf(948,plain, % 230.51/230.83 (E(f1(f1(f1(x9481,f1(f1(x9482,f1(x9481,x9482)),f1(x9481,f1(x9482,f1(x9481,x9482))))),f1(x9482,f1(x9481,x9482))),f1(x9483,f1(f1(x9481,x9482),x9483))),f1(f1(x9481,x9482),x9483))), % 230.51/230.83 inference(scs_inference,[],[42,915,152,5,4,3])). % 230.51/230.83 cnf(951,plain, % 230.51/230.83 (E(f1(f1(x9511,f1(x9512,f1(x9513,x9514))),x9515),f1(f1(x9513,f1(f1(x9512,f1(x9511,x9514)),f1(x9513,f1(x9512,f1(x9511,x9514))))),x9515))), % 230.51/230.83 inference(scs_inference,[],[23,4])). % 230.51/230.83 cnf(952,plain, % 230.51/230.83 (E(f1(x9521,f1(x9522,f1(x9523,f1(x9524,x9525)))),f1(x9521,f1(x9524,f1(f1(x9523,f1(x9522,x9525)),f1(x9524,f1(x9523,f1(x9522,x9525)))))))), % 230.51/230.83 inference(scs_inference,[],[23,4,5])). % 230.51/230.83 cnf(953,plain, % 230.51/230.83 (~E(f1(a3,f1(f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4))))),f1(a3,f1(a5,a4)))),a4)), % 230.51/230.83 inference(scs_inference,[],[728,929,23,4,5,3])). % 230.51/230.83 cnf(956,plain, % 230.51/230.83 (~E(a4,f1(a3,f1(f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4))))),f1(a3,f1(a5,a4)))))), % 230.51/230.83 inference(scs_inference,[],[953,2])). % 230.51/230.83 cnf(957,plain, % 230.51/230.83 (~E(f1(a3,f1(a5,f1(f1(a4,f1(a2,a4)),f1(a5,f1(a4,f1(a2,a4)))))),f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))))), % 230.51/230.83 inference(scs_inference,[],[43,953,952,2,3])). % 230.51/230.83 cnf(960,plain, % 230.51/230.83 (~E(f1(a3,f1(f1(a5,f1(a4,f1(f1(a5,f1(a4,f1(a5,a4))),a4))),f1(a3,f1(a5,a4)))),a4)), % 230.51/230.83 inference(scs_inference,[],[746,957,156,2,3])). % 230.51/230.83 cnf(964,plain, % 230.51/230.83 (~E(f1(f1(a3,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(a5,a4)),f1(a4,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a4,f1(f1(a5,a4),a4)))))), % 230.51/230.83 inference(scs_inference,[],[960,669,936,2,3])). % 230.51/230.83 cnf(967,plain, % 230.51/230.83 (~E(f1(a4,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a4,f1(f1(a5,a4),a4)))),f1(f1(a3,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(a5,a4)))), % 230.51/230.83 inference(scs_inference,[],[964,2])). % 230.51/230.83 cnf(1000,plain, % 230.51/230.83 (~E(a4,f1(a3,f1(f1(f1(a5,a4),f1(a3,f1(a5,a4))),f1(a3,f1(a5,a4)))))), % 230.51/230.83 inference(scs_inference,[],[956,896,3])). % 230.51/230.83 cnf(1002,plain, % 230.51/230.83 (~E(f1(a3,f1(f1(f1(a5,a4),f1(a3,f1(a5,a4))),f1(a3,f1(a5,a4)))),a4)), % 230.51/230.83 inference(scs_inference,[],[1000,2])). % 230.51/230.83 cnf(1003,plain, % 230.51/230.83 (~E(f1(a4,f1(a5,f1(a4,f1(a5,a4)))),f1(a3,f1(f1(a5,a4),f1(f1(f1(a3,f1(a5,a4)),f1(a5,a4)),f1(a5,a4)))))), % 230.51/230.83 inference(scs_inference,[],[1000,942,259,2,3])). % 230.51/230.83 cnf(1007,plain, % 230.51/230.83 (~E(f1(a3,f1(f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4))),f1(a3,f1(a5,a4)))),a4)), % 230.51/230.83 inference(scs_inference,[],[1002,1003,929,2,3])). % 230.51/230.83 cnf(1011,plain, % 230.51/230.83 (~E(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(a4,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a4,f1(f1(a5,a4),a4)))))), % 230.51/230.83 inference(scs_inference,[],[1007,964,228,2,3])). % 230.51/230.83 cnf(1014,plain, % 230.51/230.83 (~E(f1(a4,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a4,f1(f1(a5,a4),a4)))),f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))))), % 230.51/230.83 inference(scs_inference,[],[1011,2])). % 230.51/230.83 cnf(1015,plain, % 230.51/230.83 (~E(f1(f1(a3,f1(a5,a4)),f1(a5,f1(f1(a4,f1(a5,a4)),f1(a5,f1(a4,f1(a5,a4)))))),a4)), % 230.51/230.83 inference(scs_inference,[],[1011,814,923,2,3])). % 230.51/230.83 cnf(1019,plain, % 230.51/230.83 (E(f1(f1(f1(f1(f1(x10191,x10192),f1(x10192,f1(x10191,x10192))),f1(x10192,f1(x10191,x10192))),f1(x10193,f1(x10194,x10193))),x10195),f1(f1(x10194,x10193),f1(x10195,f1(f1(x10191,x10192),x10195))))), % 230.51/230.83 inference(scs_inference,[],[1015,712,653,2,3])). % 230.51/230.83 cnf(1030,plain, % 230.51/230.83 (~E(f1(a4,f1(a5,f1(f1(a4,f1(a5,a4)),f1(a5,f1(a4,f1(a5,a4)))))),f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)))), % 230.51/230.83 inference(scs_inference,[],[631,923,3])). % 230.51/230.83 cnf(1033,plain, % 230.51/230.83 (~E(f1(a4,f1(f1(a5,a4),f1(a4,f1(f1(a5,a4),a4)))),f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))))), % 230.51/230.83 inference(scs_inference,[],[1014,112,3])). % 230.51/230.83 cnf(1039,plain, % 230.51/230.83 (~E(f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4))),f1(a2,f1(a4,f1(a5,f1(a4,f1(a5,a4))))))), % 230.51/230.83 inference(scs_inference,[],[46,281,3,2])). % 230.51/230.83 cnf(1041,plain, % 230.51/230.83 (~E(f1(f1(f1(a5,a4),f1(a4,f1(a5,f1(a4,f1(a5,a4))))),f1(a3,f1(a5,a4))),f1(a2,f1(a4,f1(a5,f1(a4,f1(a5,a4))))))), % 230.51/230.83 inference(scs_inference,[],[1039,300,3])). % 230.51/230.83 cnf(1045,plain, % 230.51/230.83 (~E(f1(a4,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),a4)),f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))))), % 230.51/230.83 inference(scs_inference,[],[1033,1041,254,2,3])). % 230.51/230.83 cnf(1048,plain, % 230.51/230.83 (~E(f1(a2,f1(f1(a3,f1(a5,f1(a4,f1(a5,a4)))),f1(a5,a4))),f1(a2,f1(a4,f1(a5,a4))))), % 230.51/230.83 inference(scs_inference,[],[1045,233,296,2,3])). % 230.51/230.83 cnf(1052,plain, % 230.51/230.83 (~E(f1(a2,f1(f1(a4,f1(a5,f1(a3,f1(a5,a4)))),f1(a5,a4))),f1(a2,f1(a4,f1(a5,a4))))), % 230.51/230.83 inference(scs_inference,[],[1048,156,2,3])). % 230.51/230.83 cnf(1056,plain, % 230.51/230.83 (~E(f1(a4,f1(a5,f1(f1(a4,f1(a5,a4)),f1(a5,f1(a4,f1(a5,a4)))))),f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)))), % 230.51/230.83 inference(scs_inference,[],[1052,81,923,2,3])). % 230.51/230.83 cnf(1060,plain, % 230.51/230.83 (~E(f1(a3,f1(f1(f1(f1(a5,a4),f1(a3,f1(a5,a4))),f1(a4,f1(a5,a4))),f1(f1(a3,f1(a5,a4)),f1(a5,f1(a4,f1(a5,a4)))))),a4)), % 230.51/230.83 inference(scs_inference,[],[412,1056,301,2,3])). % 230.51/230.83 cnf(1063,plain, % 230.51/230.83 (~E(f1(a2,f1(a4,f1(f1(a5,a4),f1(a4,f1(a5,a4))))),f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4))))), % 230.51/230.83 inference(scs_inference,[],[46,1060,271,2,3])). % 230.51/230.83 cnf(1066,plain, % 230.51/230.83 (~E(f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4))),f1(a2,f1(a4,f1(f1(a5,a4),f1(a4,f1(a5,a4))))))), % 230.51/230.83 inference(scs_inference,[],[1063,2])). % 230.51/230.83 cnf(1067,plain, % 230.51/230.83 (~E(f1(a2,f1(a4,f1(f1(a5,f1(a4,f1(a5,a4))),a4))),f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4))))), % 230.51/230.83 inference(scs_inference,[],[1063,188,2,3])). % 230.51/230.83 cnf(1071,plain, % 230.51/230.83 (~E(f1(a2,f1(a4,f1(a5,f1(a4,f1(a5,a4))))),f1(a5,f1(f1(a3,f1(a5,a4)),f1(a2,a4))))), % 230.51/230.83 inference(scs_inference,[],[640,1067,281,2,3])). % 230.51/230.83 cnf(1074,plain, % 230.51/230.83 (~E(f1(a5,f1(f1(a3,f1(a5,a4)),f1(a2,a4))),f1(a2,f1(a4,f1(a5,f1(a4,f1(a5,a4))))))), % 230.51/230.83 inference(scs_inference,[],[1071,2])). % 230.51/230.83 cnf(1075,plain, % 230.51/230.83 (~E(f1(a3,f1(f1(f1(a5,f1(a4,f1(a5,a4))),f1(f1(a4,f1(a5,a4)),f1(a5,f1(a4,f1(a5,a4))))),f1(a3,f1(a5,a4)))),a4)), % 230.51/230.83 inference(scs_inference,[],[1071,782,286,2,3])). % 230.51/230.83 cnf(1079,plain, % 230.51/230.83 (~E(f1(a5,f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a2,a4))),f1(a2,f1(a4,f1(a5,f1(a4,f1(a5,a4))))))), % 230.51/230.83 inference(scs_inference,[],[1074,1075,276,2,3])). % 230.51/230.83 cnf(1082,plain, % 230.51/230.83 (~E(f1(a2,f1(a4,f1(a5,f1(a4,f1(a5,a4))))),f1(a5,f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a2,a4))))), % 230.51/230.83 inference(scs_inference,[],[1079,2])). % 230.51/230.83 cnf(1083,plain, % 230.51/230.83 (~E(f1(a4,f1(f1(a5,a4),f1(a4,f1(f1(a5,a4),a4)))),f1(a3,f1(f1(a5,a4),f1(f1(f1(a3,f1(a5,a4)),f1(a5,a4)),f1(a5,a4)))))), % 230.51/230.83 inference(scs_inference,[],[891,1079,210,2,3])). % 230.51/230.83 cnf(1086,plain, % 230.51/230.83 (~E(f1(f1(a5,f1(f1(a4,f1(f1(a5,a4),a4)),f1(a5,f1(a4,f1(f1(a5,a4),a4))))),f1(a3,f1(a5,a4))),f1(a2,f1(a4,f1(a5,a4))))), % 230.51/230.83 inference(scs_inference,[],[1083,244,951,2,3])). % 230.51/230.83 cnf(1090,plain, % 230.51/230.83 (~E(f1(f1(f1(a5,a4),f1(a4,f1(a5,f1(a4,f1(a5,a4))))),f1(a3,f1(a5,a4))),f1(a2,f1(a4,f1(f1(a5,a4),f1(a4,f1(a5,a4))))))), % 230.51/230.83 inference(scs_inference,[],[1066,1086,300,2,3])). % 230.51/230.83 cnf(1094,plain, % 230.51/230.83 (~E(f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(a4,f1(f1(a5,a4),a4)))), % 230.51/230.83 inference(scs_inference,[],[1090,759,239,2,3])). % 230.51/230.83 cnf(1098,plain, % 230.51/230.83 (~E(f1(f1(f1(a3,f1(a5,a4)),f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(a4,f1(f1(a5,a4),a4)))), % 230.51/230.83 inference(scs_inference,[],[1094,936,2,3])). % 230.51/230.83 cnf(1102,plain, % 230.51/230.83 (~E(f1(f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)),f1(a4,f1(f1(a5,a4),a4)))), % 230.51/230.83 inference(scs_inference,[],[1098,666,265,2,3])). % 230.51/230.83 cnf(1106,plain, % 230.51/230.83 (~E(f1(f1(f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)),f1(a4,f1(f1(a5,a4),a4)))), % 230.51/230.83 inference(scs_inference,[],[1102,144,2,3])). % 230.51/230.83 cnf(1110,plain, % 230.51/230.83 (~E(f1(a3,f1(a5,f1(f1(a4,f1(a2,a4)),f1(a5,f1(a4,f1(a2,a4)))))),f1(a3,f1(a2,f1(f1(a3,f1(a5,a4)),f1(a5,a4)))))), % 230.51/230.83 inference(scs_inference,[],[1106,72,952,2,3])). % 230.51/230.83 cnf(1114,plain, % 230.51/230.83 (~E(f1(a3,f1(f1(a5,a4),f1(f1(f1(a3,f1(a5,a4)),f1(a5,a4)),f1(a5,a4)))),f1(a4,f1(f1(a5,a4),a4)))), % 230.51/230.83 inference(scs_inference,[],[1110,1102,250,2,3])). % 230.51/230.83 cnf(1117,plain, % 230.51/230.83 (~E(f1(f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),a4)), % 230.51/230.83 inference(scs_inference,[],[1114,526,106,2,3])). % 230.51/230.83 cnf(1121,plain, % 230.51/230.83 (~E(f1(f1(f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),a4)), % 230.51/230.83 inference(scs_inference,[],[1117,285,2,3])). % 230.51/230.83 cnf(1125,plain, % 230.51/230.83 (~E(a4,f1(f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,f1(f1(a4,f1(a5,a4)),f1(a5,f1(a4,f1(a5,a4)))))),f1(a5,a4)))), % 230.51/230.83 inference(scs_inference,[],[920,1121,465,2,3])). % 230.51/230.83 cnf(1128,plain, % 230.51/230.83 (~E(f1(f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,f1(f1(a4,f1(a5,a4)),f1(a5,f1(a4,f1(a5,a4)))))),f1(a5,a4)),a4)), % 230.51/230.83 inference(scs_inference,[],[1125,2])). % 230.51/230.83 cnf(1129,plain, % 230.51/230.83 (~E(f1(f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),a4)), % 230.51/230.83 inference(scs_inference,[],[1125,176,1117,2,3])). % 230.51/230.83 cnf(1131,plain, % 230.51/230.83 (~E(a4,f1(f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))))), % 230.51/230.83 inference(scs_inference,[],[1129,2])). % 230.51/230.83 cnf(1132,plain, % 230.51/230.83 (~E(a4,f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))))),f1(a5,a4)))), % 230.51/230.83 inference(scs_inference,[],[1129,187,495,2,3])). % 230.51/230.83 cnf(1135,plain, % 230.51/230.83 (~E(f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))))),f1(a5,a4)),a4)), % 230.51/230.83 inference(scs_inference,[],[1132,2])). % 230.51/230.83 cnf(1136,plain, % 230.51/230.83 (~E(f1(a4,f1(a5,f1(a4,f1(a5,a4)))),f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)))), % 230.51/230.83 inference(scs_inference,[],[1132,1030,259,2,3])). % 230.51/230.83 cnf(1139,plain, % 230.51/230.83 (~E(f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)),f1(a4,f1(a5,f1(a4,f1(a5,a4)))))), % 230.51/230.83 inference(scs_inference,[],[1136,2])). % 230.51/230.83 cnf(1140,plain, % 230.51/230.83 (~E(f1(f1(a3,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(a5,a4)),a4)), % 230.51/230.83 inference(scs_inference,[],[1136,1135,947,2,3])). % 230.51/230.83 cnf(1144,plain, % 230.51/230.83 (~E(a4,f1(f1(f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)),f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))))), % 230.51/230.83 inference(scs_inference,[],[1140,1131,225,2,3])). % 230.51/230.83 cnf(1147,plain, % 230.51/230.83 (~E(f1(f1(f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)),f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),a4)), % 230.51/230.83 inference(scs_inference,[],[1144,2])). % 230.51/230.83 cnf(1148,plain, % 230.51/230.83 (~E(f1(f1(a3,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4)))),f1(a5,a4)),f1(a4,f1(a5,f1(a4,f1(a5,a4)))))), % 230.51/230.83 inference(scs_inference,[],[1139,1144,936,2,3])). % 230.51/230.83 cnf(1151,plain, % 230.51/230.83 (~E(f1(a4,f1(a5,f1(a4,f1(a5,a4)))),f1(f1(a3,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4)))),f1(a5,a4)))), % 230.51/230.83 inference(scs_inference,[],[1148,2])). % 230.51/230.83 cnf(1152,plain, % 230.51/230.83 (~E(a4,f1(f1(f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)))), % 230.51/230.83 inference(scs_inference,[],[489,1148,1019,2,3])). % 230.51/230.83 cnf(1155,plain, % 230.51/230.83 (~E(f1(f1(f1(f1(a3,f1(a5,a4)),f1(a5,a4)),f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),a4)), % 230.51/230.83 inference(scs_inference,[],[1147,1152,181,2,3])). % 230.51/230.83 cnf(1158,plain, % 230.51/230.83 (~E(a4,f1(f1(f1(f1(a3,f1(a5,a4)),f1(a5,a4)),f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))))), % 230.51/230.83 inference(scs_inference,[],[1155,2])). % 230.51/230.83 cnf(1159,plain, % 230.51/230.83 (~E(f1(a4,f1(a5,f1(f1(a3,f1(a2,a4)),f1(a5,f1(a3,f1(a2,a4)))))),f1(a3,f1(a5,f1(f1(a3,f1(a5,a4)),f1(a2,a4)))))), % 230.51/230.83 inference(scs_inference,[],[1155,190,952,2,3])). % 230.51/230.83 cnf(1163,plain, % 230.51/230.83 (~E(f1(a3,f1(f1(a5,a4),f1(a3,f1(f1(f1(a5,a4),f1(a3,f1(a5,a4))),f1(a3,f1(a5,a4)))))),a4)), % 230.51/230.83 inference(scs_inference,[],[734,1159,206,2,3])). % 230.51/230.83 cnf(1167,plain, % 230.51/230.83 (~E(f1(a5,f1(f1(a4,f1(a2,a4)),f1(a2,f1(a4,f1(a5,a4))))),f1(a5,f1(a3,f1(f1(a5,a4),a4))))), % 230.51/230.83 inference(scs_inference,[],[711,1163,161,2,3])). % 230.51/230.83 cnf(1170,plain, % 230.51/230.83 (~E(f1(a4,f1(f1(a5,a4),f1(a4,f1(a5,a4)))),f1(f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))))), % 230.51/230.83 inference(scs_inference,[],[1167,708,193,2,3])). % 230.51/230.83 cnf(1173,plain, % 230.51/230.83 (~E(f1(f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a4,f1(f1(a5,a4),f1(a4,f1(a5,a4)))))), % 230.51/230.83 inference(scs_inference,[],[1170,2])). % 230.51/230.83 cnf(1174,plain, % 230.51/230.83 (~E(f1(a4,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a4,f1(a5,a4)))),f1(f1(f1(a3,f1(a5,f1(a4,f1(a5,a4)))),f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))))), % 230.51/230.83 inference(scs_inference,[],[1170,829,266,2,3])). % 230.51/230.83 cnf(1178,plain, % 230.51/230.83 (~E(f1(f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a4,f1(f1(a5,a4),f1(a4,f1(a5,a4)))))), % 230.51/230.83 inference(scs_inference,[],[1173,1174,170,2,3])). % 230.51/230.83 cnf(1182,plain, % 230.51/230.83 (~E(f1(a4,f1(a5,f1(f1(a3,f1(a2,a4)),f1(a5,f1(a3,f1(a2,a4)))))),f1(f1(a3,f1(a5,a4)),f1(a5,f1(a3,f1(a2,a4)))))), % 230.51/230.83 inference(scs_inference,[],[1178,205,952,2,3])). % 230.51/230.83 cnf(1186,plain, % 230.51/230.83 (~E(f1(f1(a3,f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a4,f1(f1(a5,a4),f1(a4,f1(a5,a4)))))), % 230.51/230.83 inference(scs_inference,[],[1182,1178,111,2,3])). % 230.51/230.83 cnf(1189,plain, % 230.51/230.83 (~E(f1(a4,f1(f1(a5,a4),f1(a4,f1(a5,a4)))),f1(f1(a3,f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(f1(a5,a4),f1(a3,f1(a5,a4)))))), % 230.51/230.83 inference(scs_inference,[],[1186,2])). % 230.51/230.83 cnf(1190,plain, % 230.51/230.83 (~E(a4,f1(f1(a3,f1(a5,f1(a4,f1(a5,a4)))),f1(f1(a5,f1(a4,f1(a5,a4))),f1(f1(a3,f1(a5,a4)),f1(a5,f1(a4,f1(a5,a4)))))))), % 230.51/230.83 inference(scs_inference,[],[871,1186,130,2,3])). % 230.51/230.83 cnf(1192,plain, % 230.51/230.83 (~E(f1(f1(a3,f1(a5,f1(a4,f1(a5,a4)))),f1(f1(a5,f1(a4,f1(a5,a4))),f1(f1(a3,f1(a5,a4)),f1(a5,f1(a4,f1(a5,a4)))))),a4)), % 230.51/230.83 inference(scs_inference,[],[1190,2])). % 230.51/230.83 cnf(1193,plain, % 230.51/230.83 (~E(f1(f1(f1(a3,f1(a5,a4)),f1(a5,f1(f1(a4,f1(a5,a4)),f1(a5,f1(a4,f1(a5,a4)))))),f1(a5,a4)),a4)), % 230.51/230.83 inference(scs_inference,[],[1128,1190,96,2,3])). % 230.51/230.83 cnf(1197,plain, % 230.51/230.83 (~E(a4,f1(f1(f1(f1(f1(f1(a3,f1(a5,a4)),f1(a5,a4)),f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(a5,a4)),f1(f1(a5,a4),f1(f1(f1(a3,f1(a5,a4)),f1(a5,a4)),f1(a5,a4)))),f1(f1(a5,a4),f1(a3,f1(a5,a4)))))), % 230.51/230.83 inference(scs_inference,[],[1158,1193,916,2,3])). % 230.51/230.83 cnf(1200,plain, % 230.51/230.83 (~E(f1(f1(f1(f1(f1(f1(a3,f1(a5,a4)),f1(a5,a4)),f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(a5,a4)),f1(f1(a5,a4),f1(f1(f1(a3,f1(a5,a4)),f1(a5,a4)),f1(a5,a4)))),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),a4)), % 230.51/230.83 inference(scs_inference,[],[1197,2])). % 230.51/230.83 cnf(1201,plain, % 230.51/230.83 (~E(f1(f1(f1(a3,f1(a5,a4)),f1(a5,a4)),f1(a5,a4)),a4)), % 230.51/230.83 inference(scs_inference,[],[1197,1193,920,2,3])). % 230.51/230.83 cnf(1204,plain, % 230.51/230.83 (~E(a4,f1(f1(f1(a3,f1(a5,a4)),f1(a5,a4)),f1(a5,a4)))), % 230.51/230.83 inference(scs_inference,[],[1201,2])). % 230.51/230.83 cnf(1205,plain, % 230.51/230.83 (~E(f1(a4,f1(a5,f1(a4,f1(f1(a5,f1(a3,f1(a5,a4))),f1(a3,f1(a5,a4)))))),a4)), % 230.51/230.83 inference(scs_inference,[],[1201,628,150,2,3])). % 230.51/230.83 cnf(1209,plain, % 230.51/230.83 (~E(f1(f1(a3,f1(f1(a5,a4),f1(f1(f1(a3,f1(a5,a4)),f1(a5,a4)),f1(a5,a4)))),f1(a5,a4)),a4)), % 230.51/230.83 inference(scs_inference,[],[1205,1200,753,2,3])). % 230.51/230.83 cnf(1213,plain, % 230.51/230.83 (~E(f1(a4,f1(a5,f1(a4,f1(a5,f1(a4,f1(a5,a4)))))),f1(f1(a3,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4)))),f1(a5,a4)))), % 230.51/230.83 inference(scs_inference,[],[1209,1151,301,2,3])). % 230.51/230.83 cnf(1215,plain, % 230.51/230.83 (~E(f1(f1(a3,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4)))),f1(a5,a4)),f1(a4,f1(a5,f1(a4,f1(a5,f1(a4,f1(a5,a4)))))))), % 230.51/230.83 inference(scs_inference,[],[1213,2])). % 230.51/230.83 cnf(1216,plain, % 230.51/230.83 (~E(f1(a3,f1(f1(a5,a4),f1(f1(f1(f1(a3,f1(a5,a4)),f1(a5,a4)),f1(a5,a4)),f1(a5,a4)))),a4)), % 230.51/230.83 inference(scs_inference,[],[1213,1200,623,2,3])). % 230.51/230.83 cnf(1220,plain, % 230.51/230.83 (~E(f1(a2,f1(a4,f1(a5,a4))),f1(a5,f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a2,a4))))), % 230.51/230.83 inference(scs_inference,[],[1216,1082,102,2,3])). % 230.51/230.83 cnf(1223,plain, % 230.51/230.83 (~E(f1(a5,f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a2,a4))),f1(a2,f1(a4,f1(a5,a4))))), % 230.51/230.83 inference(scs_inference,[],[1220,2])). % 230.51/230.83 cnf(1228,plain, % 230.51/230.83 (~E(f1(a5,f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a2,a4),f1(a3,f1(a2,a4))))),f1(a2,f1(a4,f1(a5,a4))))), % 230.51/230.83 inference(scs_inference,[],[1223,171,3])). % 230.51/230.83 cnf(1232,plain, % 230.51/230.83 (~E(f1(a2,f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4))),f1(a2,f1(a4,f1(a5,a4))))), % 230.51/230.83 inference(scs_inference,[],[1228,195,2,3])). % 230.51/230.83 cnf(1236,plain, % 230.51/230.83 (~E(f1(a4,f1(f1(a5,f1(a4,f1(a5,a4))),a4)),f1(f1(a3,f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(f1(a5,a4),f1(a3,f1(a5,a4)))))), % 230.51/230.83 inference(scs_inference,[],[1232,1189,139,2,3])). % 230.51/230.83 cnf(1239,plain, % 230.51/230.83 (~E(f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)),f1(a4,f1(a5,f1(a4,f1(a5,f1(a4,f1(a5,a4)))))))), % 230.51/230.83 inference(scs_inference,[],[1236,1215,203,2,3])). % 230.51/230.83 cnf(1243,plain, % 230.51/230.83 (~E(f1(a3,f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))))),a4)), % 230.51/230.83 inference(scs_inference,[],[805,1239,97,2,3])). % 230.51/230.83 cnf(1247,plain, % 230.51/230.83 (~E(f1(a2,f1(a3,f1(a5,f1(a4,f1(a2,a4))))),f1(a5,f1(a3,f1(a2,a4))))), % 230.51/230.83 inference(scs_inference,[],[1243,12,161,2,3])). % 230.51/230.83 cnf(1251,plain, % 230.51/230.83 (~E(f1(f1(a3,f1(a5,a4)),f1(f1(a5,f1(a4,f1(a5,a4))),f1(f1(a3,f1(a5,a4)),f1(a5,f1(a4,f1(a5,a4)))))),a4)), % 230.51/230.83 inference(scs_inference,[],[1247,1192,101,2,3])). % 230.51/230.83 cnf(1255,plain, % 230.51/230.83 (~E(f1(a3,f1(a5,f1(f1(a4,f1(a2,a4)),f1(a5,f1(a4,f1(a2,a4)))))),f1(a3,f1(a5,f1(f1(a3,f1(a5,a4)),f1(a2,a4)))))), % 230.51/230.83 inference(scs_inference,[],[1251,167,952,2,3])). % 230.51/230.83 cnf(1259,plain, % 230.51/230.83 (~E(f1(f1(a3,f1(a5,f1(a4,f1(a5,a4)))),f1(f1(a5,f1(a3,f1(f1(a5,a4),a4))),f1(a3,f1(a5,a4)))),a4)), % 230.51/230.83 inference(scs_inference,[],[676,1255,280,2,3])). % 230.51/230.83 cnf(1262,plain, % 230.51/230.83 (~E(a4,f1(f1(f1(a3,f1(a5,f1(a4,f1(a5,a4)))),f1(a5,a4)),f1(a5,a4)))), % 230.51/230.83 inference(scs_inference,[],[1204,1259,127,2,3])). % 230.51/230.83 cnf(1265,plain, % 230.51/230.83 (~E(f1(f1(f1(a3,f1(a5,f1(a4,f1(a5,a4)))),f1(a5,a4)),f1(a5,a4)),a4)), % 230.51/230.83 inference(scs_inference,[],[1262,2])). % 230.51/230.83 cnf(1266,plain, % 230.51/230.83 (~E(f1(a4,f1(f1(a5,a4),a4)),f1(f1(a3,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(a5,a4)))), % 230.51/230.83 inference(scs_inference,[],[1262,967,237,2,3])). % 230.51/230.83 cnf(1269,plain, % 230.51/230.83 (~E(f1(f1(a3,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(a5,a4)),f1(a4,f1(f1(a5,a4),a4)))), % 230.51/230.83 inference(scs_inference,[],[1266,2])). % 230.51/230.83 cnf(1270,plain, % 230.51/230.83 (~E(f1(a4,f1(a5,f1(a3,f1(a2,a4)))),f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,f1(a3,f1(a2,a4)))))), % 230.51/230.83 inference(scs_inference,[],[1266,474,150,2,3])). % 230.51/230.83 cnf(1273,plain, % 230.51/230.83 (~E(f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,f1(a3,f1(a2,a4)))),f1(a4,f1(a5,f1(a3,f1(a2,a4)))))), % 230.51/230.83 inference(scs_inference,[],[1270,2])). % 230.51/230.83 cnf(1274,plain, % 230.51/230.83 (~E(f1(f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4)))),f1(a5,a4)),f1(a4,f1(f1(a5,a4),a4)))), % 230.51/230.83 inference(scs_inference,[],[1269,1270,265,2,3])). % 230.51/230.83 cnf(1278,plain, % 230.51/230.83 (~E(f1(a5,f1(a4,f1(a5,a4))),f1(a5,f1(f1(a4,f1(a2,a4)),f1(a5,f1(a4,f1(a2,a4))))))), % 230.51/230.83 inference(scs_inference,[],[1274,598,102,2,3])). % 230.51/230.83 cnf(1281,plain, % 230.51/230.83 (~E(f1(a5,f1(f1(a4,f1(a2,a4)),f1(a5,f1(a4,f1(a2,a4))))),f1(a5,f1(a4,f1(a5,a4))))), % 230.51/230.83 inference(scs_inference,[],[1278,2])). % 230.51/230.83 cnf(1282,plain, % 230.51/230.83 (~E(f1(f1(f1(a4,f1(a5,f1(a3,f1(a5,a4)))),f1(a5,a4)),f1(a5,a4)),a4)), % 230.51/230.83 inference(scs_inference,[],[1265,1278,155,2,3])). % 230.51/230.83 cnf(1286,plain, % 230.51/230.83 (~E(f1(a4,f1(a5,a4)),f1(f1(a3,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4)))),f1(a5,a4)))), % 230.51/230.83 inference(scs_inference,[],[1282,1151,92,2,3])). % 230.51/230.83 cnf(1290,plain, % 230.51/230.83 (~E(f1(f1(f1(a3,f1(a5,a4)),f1(a5,f1(a3,f1(f1(a5,a4),a4)))),f1(a5,f1(a3,f1(a2,a4)))),f1(a4,f1(a5,f1(a3,f1(a2,a4)))))), % 230.51/230.83 inference(scs_inference,[],[1286,1273,160,2,3])). % 230.51/230.83 cnf(1293,plain, % 230.51/230.83 (~E(f1(a4,f1(a5,f1(a3,f1(a2,a4)))),f1(f1(f1(a3,f1(a5,a4)),f1(a5,f1(a3,f1(f1(a5,a4),a4)))),f1(a5,f1(a3,f1(a2,a4)))))), % 230.51/230.83 inference(scs_inference,[],[1290,2])). % 230.51/230.83 cnf(1305,plain, % 230.51/230.83 (~E(f1(f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4))),f1(a5,f1(f1(a4,f1(a2,a4)),f1(a2,f1(a4,f1(a5,a4))))))), % 230.51/230.83 inference(scs_inference,[],[161,206,593,1048,1293,2,5,4,3])). % 230.51/230.83 cnf(1329,plain, % 230.51/230.83 (~E(f1(a2,f1(a4,f1(a5,a4))),f1(f1(f1(a5,f1(a4,f1(a5,a4))),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4))))), % 230.51/230.83 inference(scs_inference,[],[46,96,261,957,2,5,3])). % 230.51/230.83 cnf(1337,plain, % 230.51/230.83 (~E(f1(a2,f1(a4,f1(a5,a4))),f1(f1(a5,f1(a4,f1(f1(a5,a4),a4))),f1(a3,f1(a5,a4))))), % 230.51/230.83 inference(scs_inference,[],[46,149,1110,5,3])). % 230.51/230.83 cnf(1361,plain, % 230.51/230.83 (E(f1(x13611,f1(x13612,f1(f1(x13613,x13614),f1(x13612,f1(x13613,x13614))))),f1(x13613,f1(x13612,f1(x13611,x13614))))), % 230.51/230.83 inference(scs_inference,[],[6,7,5,3])). % 230.51/230.83 cnf(1363,plain, % 230.51/230.83 (E(f1(x13631,f1(x13632,f1(x13633,x13634))),f1(x13633,f1(x13632,f1(f1(x13631,x13634),f1(x13632,f1(x13631,x13634))))))), % 230.51/230.83 inference(scs_inference,[],[1361,1281,5,2])). % 230.51/230.83 cnf(1389,plain, % 230.51/230.83 (~E(f1(a4,f1(a5,a4)),f1(f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)))), % 230.51/230.83 inference(scs_inference,[],[8,152,77,2,3])). % 230.51/230.83 cnf(1395,plain, % 230.51/230.83 (E(f1(f1(x13951,f1(f1(x13952,x13953),f1(x13954,x13955))),x13956),f1(f1(x13954,f1(f1(f1(x13952,x13953),f1(x13953,f1(x13952,x13953))),f1(x13951,x13955))),x13956))), % 230.51/230.83 inference(scs_inference,[],[214,2])). % 230.51/230.83 cnf(1422,plain, % 230.51/230.83 (~E(f1(a2,f1(a4,f1(a5,a4))),f1(f1(f1(a5,a4),f1(a4,f1(f1(a5,a4),f1(a4,f1(a5,a4))))),f1(a3,f1(a5,a4))))), % 230.51/230.83 inference(scs_inference,[],[46,101,948,2,3])). % 230.51/230.83 cnf(1432,plain, % 230.51/230.83 (E(f1(f1(x14321,x14322),x14323),f1(f1(f1(x14321,f1(x14322,f1(x14321,x14322))),f1(x14322,f1(x14321,x14322))),f1(x14323,f1(f1(f1(x14321,x14322),f1(x14322,f1(x14321,x14322))),x14323))))), % 230.51/230.83 inference(scs_inference,[],[493,2])). % 230.51/230.83 cnf(1463,plain, % 230.51/230.83 (~E(f1(a4,f1(f1(a5,a4),f1(a4,f1(a5,a4)))),f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))))), % 230.51/230.83 inference(scs_inference,[],[10,77,3])). % 230.51/230.83 cnf(1466,plain, % 230.51/230.83 (~E(f1(a5,f1(a4,f1(a2,a4))),f1(f1(a5,a4),f1(a3,f1(a5,a4))))), % 230.51/230.83 inference(scs_inference,[],[7,45,3])). % 230.51/230.83 cnf(1469,plain, % 230.51/230.83 (~E(f1(a5,f1(a3,f1(f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a4,f1(a5,a4))),a4))),f1(a2,f1(a4,f1(a5,a4))))), % 230.51/230.83 inference(scs_inference,[],[7,264,3])). % 230.51/230.83 cnf(1560,plain, % 230.51/230.83 (~E(f1(f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)),f1(a4,f1(a5,a4)))), % 230.51/230.83 inference(scs_inference,[],[1389,2])). % 230.51/230.83 cnf(1674,plain, % 230.51/230.83 (~E(f1(f1(a5,a4),f1(a3,f1(a5,a4))),f1(a5,f1(a4,f1(a2,a4))))), % 230.51/230.83 inference(scs_inference,[],[1466,2])). % 230.51/230.83 cnf(1675,plain, % 230.51/230.83 (~E(f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)))),f1(a4,f1(a5,a4)))), % 230.51/230.83 inference(scs_inference,[],[10,113,1466,2,3])). % 230.51/230.83 cnf(1679,plain, % 230.51/230.83 (~E(f1(f1(a3,f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(f1(a5,a4),f1(f1(a3,f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(a5,a4)))),f1(a4,f1(a5,a4)))), % 230.51/230.83 inference(scs_inference,[],[10,158,1675,2,3])). % 230.51/230.83 cnf(1683,plain, % 230.51/230.83 (~E(f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(f1(a5,a4),f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)))),f1(a4,f1(a5,a4)))), % 230.51/230.83 inference(scs_inference,[],[10,629,1679,2,3])). % 230.51/230.83 cnf(1687,plain, % 230.51/230.83 (~E(f1(f1(a3,f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(f1(a5,a4),f1(f1(a3,f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(a5,a4)))),f1(a4,f1(f1(a5,a4),a4)))), % 230.51/230.83 inference(scs_inference,[],[10,666,1683,2,3])). % 230.51/230.83 cnf(1711,plain, % 230.51/230.83 (~E(f1(a5,f1(a4,f1(a2,a4))),f1(f1(f1(f1(a5,f1(a4,f1(a5,a4))),f1(a4,f1(a5,a4))),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4))))), % 230.51/230.83 inference(scs_inference,[],[7,355,1687,2,3])). % 230.51/230.83 cnf(1715,plain, % 230.51/230.83 (~E(f1(f1(a5,a4),f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4))),f1(a2,f1(a4,f1(a5,a4))))), % 230.51/230.83 inference(scs_inference,[],[7,451,1711,2,3])). % 230.51/230.83 cnf(1718,plain, % 230.51/230.83 (~E(f1(a2,f1(a4,f1(a5,a4))),f1(f1(a5,a4),f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4))))), % 230.51/230.83 inference(scs_inference,[],[1715,2])). % 230.51/230.83 cnf(1731,plain, % 230.51/230.83 (~E(f1(f1(f1(a3,f1(a5,a4)),f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a4,f1(f1(a5,a4),a4)))), % 230.51/230.83 inference(scs_inference,[],[7,1114,1469,2,3])). % 230.51/230.83 cnf(1734,plain, % 230.51/230.83 (~E(f1(a5,f1(a4,f1(a2,a4))),f1(f1(f1(a5,f1(a4,f1(a5,a4))),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4))))), % 230.51/230.83 inference(scs_inference,[],[7,1329,1731,2,3])). % 230.51/230.83 cnf(1737,plain, % 230.51/230.83 (~E(f1(a5,f1(a4,f1(a2,a4))),f1(f1(a5,f1(a4,f1(f1(a5,a4),a4))),f1(a3,f1(a5,a4))))), % 230.51/230.83 inference(scs_inference,[],[7,1337,1734,2,3])). % 230.51/230.83 cnf(1740,plain, % 230.51/230.83 (~E(f1(a5,f1(a4,f1(a2,a4))),f1(f1(f1(a5,a4),f1(a4,f1(f1(a5,a4),f1(a4,f1(a5,a4))))),f1(a3,f1(a5,a4))))), % 230.51/230.83 inference(scs_inference,[],[7,1422,1737,2,3])). % 230.51/230.83 cnf(1744,plain, % 230.51/230.83 (~E(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(f1(f1(a3,f1(a5,a4)),f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4)))),f1(a5,a4)))),f1(a4,f1(f1(a5,a4),a4)))), % 230.51/230.83 inference(scs_inference,[],[7,1098,1740,2,3])). % 230.51/230.83 cnf(1748,plain, % 230.51/230.83 (~E(f1(f1(a5,f1(a4,f1(a5,a4))),f1(a3,f1(a5,f1(a4,f1(a5,a4))))),f1(a2,f1(a4,f1(a5,a4))))), % 230.51/230.83 inference(scs_inference,[],[7,854,1744,2,3])). % 230.51/230.83 cnf(1753,plain, % 230.51/230.83 (~E(f1(f1(a3,f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(f1(a5,a4),f1(f1(a3,f1(f1(a5,a4),f1(f1(a3,f1(a5,a4)),f1(a5,a4)))),f1(a5,a4)))),f1(a4,f1(f1(a5,a4),f1(a4,f1(a5,a4)))))), % 230.51/230.83 inference(scs_inference,[],[10,923,315,1748,2,5,3])). % 230.51/230.83 cnf(2052,plain, % 230.51/230.83 (~E(f1(f1(a3,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)))),f1(a5,a4)),f1(a4,f1(a5,a4)))), % 230.51/230.83 inference(scs_inference,[],[1395,1560,1463,2,3])). % 230.51/230.83 cnf(2054,plain, % 230.51/230.83 (~E(f1(a4,f1(a5,a4)),f1(f1(a3,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)))),f1(a5,a4)))), % 230.51/230.83 inference(scs_inference,[],[2052,2])). % 230.51/230.83 cnf(2055,plain, % 230.51/230.83 (~E(f1(a5,f1(a4,f1(f1(a2,a4),f1(a4,f1(a2,a4))))),f1(f1(f1(a5,a4),f1(a4,f1(a5,f1(a4,f1(a5,a4))))),f1(a3,f1(a5,a4))))), % 230.51/230.83 inference(scs_inference,[],[1363,379,2052,2,3])). % 230.51/230.83 cnf(2059,plain, % 230.51/230.83 (~E(f1(a4,f1(f1(a5,a4),f1(a4,f1(a5,a4)))),f1(f1(a3,f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4)))),f1(a5,a4)))), % 230.51/230.83 inference(scs_inference,[],[10,2054,1753,2,3])). % 230.51/230.83 cnf(2063,plain, % 230.51/230.83 (~E(f1(a5,f1(a4,f1(f1(a2,a4),f1(a4,f1(a2,a4))))),f1(a5,f1(f1(a3,f1(a5,f1(a4,f1(a5,a4)))),f1(a2,a4))))), % 230.51/230.83 inference(scs_inference,[],[1363,643,2059,2,3])). % 230.51/230.83 cnf(2067,plain, % 230.51/230.83 (~E(f1(f1(f1(a5,f1(a4,f1(a5,a4))),f1(a4,f1(a5,a4))),f1(f1(a3,f1(a5,a4)),f1(f1(f1(a5,a4),f1(a4,f1(a5,a4))),f1(a3,f1(a5,a4))))),f1(a5,f1(a4,f1(a2,a4))))), % 230.51/230.83 inference(scs_inference,[],[1432,1674,1305,2,3])). % 230.51/230.83 cnf(2070,plain, % 230.51/230.83 (~E(f1(a5,f1(a4,f1(f1(a2,a4),f1(a4,f1(a2,a4))))),f1(f1(a5,a4),f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4))))), % 230.51/230.83 inference(scs_inference,[],[1363,1718,2067,2,3])). % 230.51/230.83 cnf(2130,plain, % 230.51/230.83 (~E(f1(f1(a3,f1(a5,a4)),f1(f1(a5,a4),f1(f1(f1(a3,f1(a5,a4)),f1(a5,f1(a3,f1(f1(a5,a4),a4)))),f1(a5,a4)))),f1(a4,f1(a5,a4)))), % 230.51/230.83 inference(scs_inference,[],[7,527,2070,2,3])). % 230.51/230.83 cnf(2133,plain, % 230.51/230.83 (~E(f1(f1(a2,a4),f1(a4,f1(a5,f1(a4,f1(a2,a4))))),f1(a5,f1(f1(a3,f1(a5,f1(a4,f1(a5,a4)))),f1(a2,a4))))), % 230.51/230.83 inference(scs_inference,[],[7,2063,2130,2,3])). % 230.51/230.83 cnf(2136,plain, % 230.51/230.83 (~E(f1(f1(a2,a4),f1(a4,f1(a5,f1(a4,f1(a2,a4))))),f1(f1(f1(a5,a4),f1(a4,f1(a5,f1(a4,f1(a5,a4))))),f1(a3,f1(a5,a4))))), % 230.51/230.83 inference(scs_inference,[],[7,2055,2133,2,3])). % 230.51/230.83 cnf(2139,plain, % 230.51/230.83 (~E(f1(f1(a2,a4),f1(a4,f1(a5,f1(a4,f1(a2,a4))))),f1(f1(a5,a4),f1(f1(a3,f1(f1(a5,a4),f1(a3,f1(a5,a4)))),f1(a5,a4))))), % 230.51/230.83 inference(scs_inference,[],[7,2070,2136,2,3])). % 230.51/230.83 cnf(2142,plain, % 230.51/230.83 ($false), % 230.51/230.83 inference(scs_inference,[],[7,102,1247,2139,2,3]), % 230.51/230.83 ['proof']). % 230.51/230.83 % SZS output end Proof % 230.51/230.83 % Total time :229.900000s %------------------------------------------------------------------------------