%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : COL044-1 : TPTP v8.2.0. Released v1.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n013.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 04:44:54 EDT 2024 % Result : Unsatisfiable 261.26s 261.32s % Output : CNFRefutation 261.37s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.14 % Problem : COL044-1 : TPTP v8.2.0. Released v1.0.0. % 0.12/0.14 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.36 % Computer : n013.cluster.edu % 0.13/0.36 % Model : x86_64 x86_64 % 0.13/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.36 % Memory : 8042.1875MB % 0.13/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.36 % CPULimit : 300 % 0.13/0.36 % WCLimit : 300 % 0.13/0.36 % DateTime : Tue Jun 18 16:01:24 EDT 2024 % 0.13/0.36 % CPUTime : % 0.48/0.63 start to proof:theBenchmark % 261.17/261.29 %------------------------------------------- % 261.17/261.29 % File :CSE---1.7 % 261.17/261.29 % Problem :theBenchmark % 261.17/261.29 % Transform :cnf % 261.17/261.29 % Format :tptp:raw % 261.17/261.29 % Command :java -jar mcs_scs.jar %d %s % 261.17/261.29 % 261.17/261.29 % Result :Theorem 260.550000s % 261.17/261.29 % Output :CNFRefutation 260.550000s % 261.17/261.29 %------------------------------------------- % 261.26/261.32 %-------------------------------------------------------------------------- % 261.26/261.32 % File : COL044-1 : TPTP v8.2.0. Released v1.0.0. % 261.26/261.32 % Domain : Combinatory Logic % 261.26/261.32 % Problem : Strong fixed point for B and N % 261.26/261.32 % Version : [WM88] (equality) axioms. % 261.26/261.32 % English : The strong fixed point property holds for the set % 261.26/261.32 % P consisting of the combinators B and N, where ((Bx)y)z % 261.26/261.32 % = x(yz), ((Nx)y)z = ((xz)y)z. % 261.26/261.32 % 261.26/261.32 % Refs : [Smu85] Smullyan (1978), To Mock a Mocking Bird and Other Logi % 261.26/261.32 % : [MW87] McCune & Wos (1987), A Case Study in Automated Theorem % 261.26/261.32 % : [WM88] Wos & McCune (1988), Challenge Problems Focusing on Eq % 261.26/261.32 % : [MW88] McCune & Wos (1988), Some Fixed Point Problems in Comb % 261.26/261.32 % : [LW92] Lusk & Wos (1992), Benchmark Problems in Which Equalit % 261.26/261.32 % : [Wos93] Wos (1993), The Kernel Strategy and Its Use for the St % 261.26/261.32 % Source : [MW88] % 261.26/261.32 % Names : - [MW88] % 261.26/261.32 % : CL3 [LW92] % 261.26/261.32 % : Question 5 [Wos93] % 261.26/261.32 % 261.26/261.32 % Status : Unsatisfiable % 261.26/261.32 % Rating : 0.27 v8.2.0, 0.29 v8.1.0, 0.35 v7.5.0, 0.33 v7.4.0, 0.39 v7.3.0, 0.37 v7.1.0, 0.28 v7.0.0, 0.26 v6.4.0, 0.32 v6.3.0, 0.29 v6.1.0, 0.31 v6.0.0, 0.38 v5.5.0, 0.32 v5.4.0, 0.33 v5.3.0, 0.42 v5.2.0, 0.36 v5.1.0, 0.47 v5.0.0, 0.43 v4.1.0, 0.36 v4.0.1, 0.43 v4.0.0, 0.46 v3.7.0, 0.22 v3.4.0, 0.25 v3.3.0, 0.29 v3.2.0, 0.21 v3.1.0, 0.22 v2.7.0, 0.18 v2.6.0, 0.33 v2.5.0, 0.00 v2.2.1, 0.11 v2.2.0, 0.00 v2.1.0, 0.25 v2.0.0 % 261.26/261.32 % Syntax : Number of clauses : 3 ( 3 unt; 0 nHn; 1 RR) % 261.26/261.32 % Number of literals : 3 ( 3 equ; 1 neg) % 261.26/261.32 % Maximal clause size : 1 ( 1 avg) % 261.26/261.32 % Maximal term depth : 4 ( 2 avg) % 261.26/261.32 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty) % 261.26/261.32 % Number of functors : 4 ( 4 usr; 2 con; 0-2 aty) % 261.26/261.32 % Number of variables : 7 ( 0 sgn) % 261.26/261.32 % SPC : CNF_UNS_RFO_PEQ_UEQ % 261.26/261.32 % 261.26/261.32 % Comments : % 261.26/261.32 %-------------------------------------------------------------------------- % 261.26/261.32 cnf(b_definition,axiom, % 261.26/261.32 apply(apply(apply(b,X),Y),Z) = apply(X,apply(Y,Z)) ). % 261.26/261.32 % 261.26/261.32 cnf(n_definition,axiom, % 261.26/261.32 apply(apply(apply(n,X),Y),Z) = apply(apply(apply(X,Z),Y),Z) ). % 261.26/261.32 % 261.26/261.32 cnf(prove_fixed_point,negated_conjecture, % 261.26/261.32 apply(Y,f(Y)) != apply(f(Y),apply(Y,f(Y))) ). % 261.26/261.32 % 261.26/261.32 %-------------------------------------------------------------------------- % 261.26/261.32 %------------------------------------------- % 261.26/261.32 % Proof found % 261.26/261.32 % SZS status Theorem for theBenchmark % 261.26/261.32 % SZS output start Proof % 261.26/261.35 %ClaNum:9(EqnAxiom:6) % 261.26/261.35 %VarNum:18(SingletonVarNum:7) % 261.26/261.35 %MaxLitNum:1 % 261.26/261.35 %MaxfuncDepth:3 % 261.26/261.35 %SharedTerms:2 % 261.26/261.35 %goalClause: 9 % 261.26/261.35 %singleGoalClaCount:1 % 261.26/261.35 [9]~E(f2(f4(x91),f2(x91,f4(x91))),f2(x91,f4(x91))) % 261.26/261.35 [7]E(f2(f2(f2(a1,x71),x72),x73),f2(x71,f2(x72,x73))) % 261.26/261.35 [8]E(f2(f2(f2(a3,x81),x82),x83),f2(f2(f2(x81,x83),x82),x83)) % 261.26/261.35 %EqnAxiom % 261.26/261.35 [1]E(x11,x11) % 261.26/261.35 [2]E(x22,x21)+~E(x21,x22) % 261.26/261.35 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 261.26/261.35 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43)) % 261.26/261.35 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52)) % 261.26/261.35 [6]~E(x61,x62)+E(f4(x61),f4(x62)) % 261.26/261.35 % 261.26/261.35 %------------------------------------------- % 261.26/261.38 cnf(10,plain, % 261.26/261.38 (E(f2(f2(f2(x101,x102),x103),x102),f2(f2(f2(a3,x101),x103),x102))), % 261.26/261.38 inference(scs_inference,[],[8,2])). % 261.26/261.38 cnf(11,plain, % 261.26/261.38 (E(f2(f2(f2(a3,a1),x111),x112),f2(x112,f2(x111,x112)))), % 261.26/261.38 inference(scs_inference,[],[8,7,2,3])). % 261.26/261.38 cnf(14,plain, % 261.26/261.38 (E(f2(x141,f2(x142,x141)),f2(f2(f2(a3,a1),x142),x141))), % 261.26/261.38 inference(scs_inference,[],[11,2])). % 261.26/261.38 cnf(15,plain, % 261.26/261.38 (E(f2(x151,f2(x152,x153)),f2(f2(f2(a1,x151),x152),x153))), % 261.26/261.38 inference(scs_inference,[],[7,2])). % 261.26/261.38 cnf(16,plain, % 261.26/261.38 (E(f2(f2(f2(a3,a3),x161),a1),f2(a1,f2(x161,a1)))), % 261.26/261.38 inference(scs_inference,[],[8,11,3])). % 261.26/261.38 cnf(19,plain, % 261.26/261.38 (E(f2(a1,f2(x191,a1)),f2(f2(f2(a3,a3),x191),a1))), % 261.26/261.38 inference(scs_inference,[],[8,11,3,2])). % 261.26/261.38 cnf(20,plain, % 261.26/261.38 (E(f2(f2(f2(a1,a1),x201),a1),f2(f2(f2(a3,a3),x201),a1))), % 261.26/261.38 inference(scs_inference,[],[7,19,3])). % 261.26/261.38 cnf(23,plain, % 261.26/261.38 (E(f2(f2(f2(a3,a3),x231),a1),f2(f2(f2(a1,a1),x231),a1))), % 261.26/261.38 inference(scs_inference,[],[7,19,3,2])). % 261.26/261.38 cnf(25,plain, % 261.26/261.38 (E(f2(f2(f2(f2(a1,x251),x252),x253),x254),f2(f2(x251,f2(x252,x253)),x254))), % 261.26/261.38 inference(scs_inference,[],[7,6,4])). % 261.26/261.38 cnf(26,plain, % 261.26/261.38 (E(f2(x261,f2(f2(f2(a1,x262),x263),x264)),f2(x261,f2(x262,f2(x263,x264))))), % 261.26/261.38 inference(scs_inference,[],[7,6,4,5])). % 261.26/261.38 cnf(28,plain, % 261.26/261.38 (~E(f2(f2(f2(a3,a1),x281),f4(x281)),f2(x281,f4(x281)))), % 261.26/261.38 inference(scs_inference,[],[7,14,9,6,4,5,2,3])). % 261.26/261.38 cnf(32,plain, % 261.26/261.38 (E(f2(x321,f2(f2(f2(a3,a3),x322),a1)),f2(x321,f2(a1,f2(x322,a1))))), % 261.26/261.38 inference(scs_inference,[],[16,6,5])). % 261.26/261.38 cnf(34,plain, % 261.26/261.38 (~E(f2(x341,f4(x341)),f2(f2(f2(a3,a1),x341),f4(x341)))), % 261.26/261.38 inference(scs_inference,[],[28,16,6,5,4,2])). % 261.26/261.38 cnf(35,plain, % 261.26/261.38 (~E(f2(f2(f2(a1,f4(x351)),x351),f4(x351)),f2(x351,f4(x351)))), % 261.26/261.38 inference(scs_inference,[],[28,16,15,9,6,5,4,2,3])). % 261.26/261.38 cnf(38,plain, % 261.26/261.38 (E(f2(f2(x381,f2(x382,x381)),x383),f2(f2(f2(f2(a3,a1),x382),x381),x383))), % 261.26/261.38 inference(scs_inference,[],[14,6,4])). % 261.26/261.38 cnf(39,plain, % 261.26/261.38 (E(f2(x391,f2(x392,f2(x393,x392))),f2(x391,f2(f2(f2(a3,a1),x393),x392)))), % 261.26/261.38 inference(scs_inference,[],[14,6,4,5])). % 261.26/261.38 cnf(40,plain, % 261.26/261.38 (~E(f2(x401,f4(x401)),f2(f2(f2(a1,f4(x401)),x401),f4(x401)))), % 261.26/261.38 inference(scs_inference,[],[35,14,6,4,5,2])). % 261.26/261.38 cnf(41,plain, % 261.26/261.38 (E(f2(f2(f2(a3,a3),f2(f2(a1,x411),x412)),a1),f2(a1,f2(x411,f2(x412,a1))))), % 261.26/261.38 inference(scs_inference,[],[35,26,14,16,6,4,5,2,3])). % 261.26/261.38 cnf(45,plain, % 261.26/261.38 (E(f2(x451,f2(x452,f2(x453,x454))),f2(x451,f2(f2(f2(a1,x452),x453),x454)))), % 261.26/261.38 inference(scs_inference,[],[15,6,5])). % 261.26/261.38 cnf(46,plain, % 261.26/261.38 (E(f2(f2(x461,f2(x462,x463)),x464),f2(f2(f2(f2(a1,x461),x462),x463),x464))), % 261.26/261.38 inference(scs_inference,[],[15,6,5,4])). % 261.26/261.38 cnf(49,plain, % 261.26/261.38 (E(f2(x491,f2(a1,f2(x492,a1))),f2(x491,f2(f2(f2(a3,a3),x492),a1)))), % 261.26/261.38 inference(scs_inference,[],[19,6,4,5])). % 261.26/261.38 cnf(51,plain, % 261.26/261.38 (E(f2(x511,f2(f2(f2(a3,a1),x512),x513)),f2(x511,f2(x513,f2(x512,x513))))), % 261.26/261.38 inference(scs_inference,[],[11,6,5])). % 261.26/261.38 cnf(52,plain, % 261.26/261.38 (E(f2(f2(f2(f2(a3,a1),x521),x522),x523),f2(f2(x522,f2(x521,x522)),x523))), % 261.26/261.38 inference(scs_inference,[],[11,6,5,4])). % 261.26/261.38 cnf(53,plain, % 261.26/261.38 (E(f2(f2(f2(a3,a3),f2(f2(a3,a1),x531)),a1),f2(a1,f2(a1,f2(x531,a1))))), % 261.26/261.38 inference(scs_inference,[],[51,16,3])). % 261.26/261.38 cnf(56,plain, % 261.26/261.38 (E(f2(f2(f2(a3,a3),f2(f2(a3,a3),x561)),a1),f2(a1,f2(a1,f2(x561,a1))))), % 261.26/261.38 inference(scs_inference,[],[32,16,3])). % 261.26/261.38 cnf(59,plain, % 261.26/261.38 (E(f2(a1,f2(a1,f2(x591,a1))),f2(f2(f2(a3,a3),f2(f2(a3,a1),x591)),a1))), % 261.26/261.38 inference(scs_inference,[],[19,39,3])). % 261.26/261.38 cnf(62,plain, % 261.26/261.38 (E(f2(a1,f2(a1,f2(x621,a1))),f2(f2(f2(a1,a1),f2(f2(a3,a1),x621)),a1))), % 261.26/261.38 inference(scs_inference,[],[23,59,3])). % 261.26/261.38 cnf(64,plain, % 261.26/261.38 (E(f2(f2(f2(a1,a1),f2(f2(a1,x641),x642)),a1),f2(a1,f2(x641,f2(x642,a1))))), % 261.26/261.38 inference(scs_inference,[],[20,41,3])). % 261.26/261.38 cnf(66,plain, % 261.26/261.38 (E(f2(a1,f2(a1,f2(x661,a1))),f2(f2(f2(a3,a1),f2(f2(a3,a1),x661)),a1))), % 261.26/261.38 inference(scs_inference,[],[10,62,3])). % 261.26/261.38 cnf(68,plain, % 261.26/261.38 (E(f2(a1,f2(a1,f2(f2(a3,a1),a1))),f2(f2(f2(f2(a3,a1),f2(a3,a1)),f2(a3,a1)),a1))), % 261.26/261.38 inference(scs_inference,[],[38,66,3])). % 261.26/261.38 cnf(71,plain, % 261.26/261.38 (E(f2(f2(f2(a1,a1),f2(f2(a3,a1),x711)),a1),f2(a1,f2(a1,f2(x711,a1))))), % 261.26/261.38 inference(scs_inference,[],[53,20,3])). % 261.26/261.38 cnf(73,plain, % 261.26/261.38 (E(f2(a1,f2(a1,f2(x731,a1))),f2(f2(f2(f2(a1,f2(a3,a3)),f2(a3,a1)),x731),a1))), % 261.26/261.38 inference(scs_inference,[],[46,59,3])). % 261.26/261.38 cnf(76,plain, % 261.26/261.38 (E(f2(f2(f2(a1,a1),f2(f2(a3,a3),x761)),a1),f2(a1,f2(a1,f2(x761,a1))))), % 261.26/261.38 inference(scs_inference,[],[56,20,3])). % 261.26/261.38 cnf(78,plain, % 261.26/261.38 (E(f2(f2(f2(a1,a1),f2(f2(a1,a1),f2(a3,a1))),a1),f2(f2(f2(f2(a3,a1),f2(a3,a1)),f2(a3,a1)),a1))), % 261.26/261.38 inference(scs_inference,[],[68,64,3])). % 261.26/261.38 cnf(80,plain, % 261.26/261.38 (E(f2(f2(f2(a3,a3),f2(f2(a1,a1),f2(a3,a1))),a1),f2(f2(f2(f2(a3,a1),f2(a3,a1)),f2(a3,a1)),a1))), % 261.26/261.38 inference(scs_inference,[],[78,23,3])). % 261.26/261.38 cnf(82,plain, % 261.26/261.38 (E(f2(a1,f2(f2(f2(a1,a1),f2(a3,a1)),a1)),f2(f2(f2(f2(a3,a1),f2(a3,a1)),f2(a3,a1)),a1))), % 261.26/261.38 inference(scs_inference,[],[80,19,3])). % 261.26/261.38 cnf(84,plain, % 261.26/261.38 (E(f2(x841,f2(x842,f2(x843,x841))),f2(f2(f2(a3,a1),f2(f2(a1,x842),x843)),x841))), % 261.26/261.38 inference(scs_inference,[],[14,45,3])). % 261.26/261.38 cnf(87,plain, % 261.26/261.38 (E(f2(a1,f2(a1,f2(x871,a1))),f2(f2(f2(a3,a3),f2(f2(a3,a3),x871)),a1))), % 261.26/261.38 inference(scs_inference,[],[19,49,3])). % 261.26/261.38 cnf(90,plain, % 261.26/261.38 (E(f2(a1,f2(x901,f2(x902,a1))),f2(f2(f2(a3,a3),f2(f2(a1,x901),x902)),a1))), % 261.26/261.38 inference(scs_inference,[],[84,10,3])). % 261.26/261.38 cnf(93,plain, % 261.26/261.38 (E(f2(a1,f2(x931,f2(f2(a3,a3),a1))),f2(f2(f2(f2(a3,a1),f2(a1,x931)),f2(a3,a3)),a1))), % 261.26/261.38 inference(scs_inference,[],[38,90,3])). % 261.26/261.38 cnf(99,plain, % 261.26/261.38 (E(f2(a1,f2(a1,f2(x991,a1))),f2(f2(f2(f2(a1,f2(a3,a3)),f2(a3,a3)),x991),a1))), % 261.26/261.38 inference(scs_inference,[],[46,87,3])). % 261.26/261.38 cnf(102,plain, % 261.26/261.38 (E(f2(f2(f2(a1,a1),f2(f2(a3,a1),f2(a3,a3))),a1),f2(f2(f2(f2(a3,a1),f2(a1,a1)),f2(a3,a3)),a1))), % 261.26/261.38 inference(scs_inference,[],[71,93,3])). % 261.26/261.38 cnf(105,plain, % 261.26/261.38 (E(f2(f2(f2(a1,a1),f2(f2(a3,a3),f2(a3,a1))),a1),f2(f2(f2(f2(a3,a1),f2(a3,a1)),f2(a3,a1)),a1))), % 261.26/261.38 inference(scs_inference,[],[68,76,3])). % 261.26/261.38 cnf(107,plain, % 261.26/261.38 (E(f2(f2(f2(a3,a3),f2(f2(a3,a3),f2(a3,a1))),a1),f2(f2(f2(f2(a3,a1),f2(a3,a1)),f2(a3,a1)),a1))), % 261.26/261.38 inference(scs_inference,[],[105,23,3])). % 261.26/261.38 cnf(109,plain, % 261.26/261.38 (E(f2(f2(f2(a3,a3),f2(f2(a3,a1),f2(a3,a3))),a1),f2(f2(f2(f2(a3,a1),f2(a1,a1)),f2(a3,a3)),a1))), % 261.26/261.38 inference(scs_inference,[],[102,23,3])). % 261.26/261.38 cnf(111,plain, % 261.26/261.38 (E(f2(a1,f2(f2(f2(a3,a3),f2(a3,a1)),a1)),f2(f2(f2(f2(a3,a1),f2(a3,a1)),f2(a3,a1)),a1))), % 261.26/261.38 inference(scs_inference,[],[107,19,3])). % 261.26/261.38 cnf(115,plain, % 261.26/261.38 (E(f2(x1151,f2(x1152,f2(x1153,x1151))),f2(f2(f2(a1,x1151),f2(f2(a1,x1152),x1153)),x1151))), % 261.26/261.38 inference(scs_inference,[],[8,84,3])). % 261.26/261.38 cnf(118,plain, % 261.26/261.38 (E(f2(f2(x1181,a1),f2(f2(f2(a3,a3),x1181),a1)),f2(f2(f2(a3,a1),a1),f2(x1181,a1)))), % 261.26/261.38 inference(scs_inference,[],[14,32,3])). % 261.26/261.38 cnf(121,plain, % 261.26/261.38 (E(f2(a1,f2(a1,f2(x1211,a1))),f2(f2(f2(a1,a1),f2(f2(a3,a3),x1211)),a1))), % 261.26/261.38 inference(scs_inference,[],[23,87,3])). % 261.26/261.38 cnf(123,plain, % 261.26/261.38 (E(f2(x1231,f2(x1232,f2(f2(a1,x1231),x1231))),f2(f2(f2(f2(a3,a1),f2(a1,x1232)),f2(a1,x1231)),x1231))), % 261.26/261.38 inference(scs_inference,[],[38,115,3])). % 261.26/261.38 cnf(129,plain, % 261.26/261.38 (E(f2(f2(f2(a3,a3),f2(f2(a1,x1291),f2(a1,a1))),a1),f2(f2(f2(f2(a3,a1),f2(a1,x1291)),f2(a1,a1)),a1))), % 261.26/261.38 inference(scs_inference,[],[123,41,3])). % 261.26/261.38 cnf(132,plain, % 261.26/261.38 (E(f2(a1,f2(f2(f2(a1,x1321),f2(a1,a1)),a1)),f2(f2(f2(f2(a3,a1),f2(a1,x1321)),f2(a1,a1)),a1))), % 261.26/261.38 inference(scs_inference,[],[129,19,3])). % 261.26/261.38 cnf(134,plain, % 261.37/261.38 (E(f2(f2(f2(a1,a1),f2(f2(a3,a1),f2(a3,a1))),a1),f2(f2(f2(f2(a3,a1),f2(a3,a1)),f2(a3,a1)),a1))), % 261.37/261.38 inference(scs_inference,[],[68,71,3])). % 261.37/261.38 cnf(136,plain, % 261.37/261.38 (E(f2(f2(f2(a3,a3),f2(f2(a3,a1),f2(a3,a1))),a1),f2(f2(f2(f2(a3,a1),f2(a3,a1)),f2(a3,a1)),a1))), % 261.37/261.38 inference(scs_inference,[],[134,23,3])). % 261.37/261.38 cnf(138,plain, % 261.37/261.38 (E(f2(a1,f2(f2(f2(a3,a1),f2(a3,a1)),a1)),f2(f2(f2(f2(a3,a1),f2(a3,a1)),f2(a3,a1)),a1))), % 261.37/261.38 inference(scs_inference,[],[136,19,3])). % 261.37/261.38 cnf(140,plain, % 261.37/261.38 (E(f2(f2(f2(a3,a3),f2(f2(a3,a1),f2(a1,a1))),a1),f2(f2(f2(f2(a3,a1),f2(a1,a1)),f2(a1,a1)),a1))), % 261.37/261.38 inference(scs_inference,[],[123,53,3])). % 261.37/261.38 cnf(143,plain, % 261.37/261.38 (E(f2(f2(f2(a1,a1),f2(f2(a3,a1),f2(a1,a1))),a1),f2(f2(f2(f2(a3,a1),f2(a1,a1)),f2(a1,a1)),a1))), % 261.37/261.38 inference(scs_inference,[],[140,20,3])). % 261.37/261.38 cnf(145,plain, % 261.37/261.38 (E(f2(a1,f2(f2(f2(a3,a1),f2(a1,a1)),a1)),f2(f2(f2(f2(a3,a1),f2(a1,a1)),f2(a1,a1)),a1))), % 261.37/261.38 inference(scs_inference,[],[140,19,3])). % 261.37/261.38 cnf(147,plain, % 261.37/261.38 (E(f2(f2(x1471,a1),f2(f2(f2(a3,a3),x1471),a1)),f2(f2(f2(a1,f2(x1471,a1)),a1),f2(x1471,a1)))), % 261.37/261.38 inference(scs_inference,[],[8,118,3])). % 261.37/261.38 cnf(149,plain, % 261.37/261.38 (E(f2(x1491,f2(x1491,f2(x1492,x1491))),f2(f2(f2(a3,a1),f2(f2(a3,a1),x1492)),x1491))), % 261.37/261.38 inference(scs_inference,[],[14,39,3])). % 261.37/261.38 cnf(152,plain, % 261.37/261.38 (E(f2(x1521,f2(x1521,f2(f2(a3,a1),x1521))),f2(f2(f2(f2(a3,a1),f2(a3,a1)),f2(a3,a1)),x1521))), % 261.37/261.38 inference(scs_inference,[],[38,149,3])). % 261.37/261.38 cnf(155,plain, % 261.37/261.38 (E(f2(x1551,f2(x1551,f2(x1552,x1551))),f2(f2(f2(f2(a1,f2(a3,a1)),f2(a3,a1)),x1552),x1551))), % 261.37/261.38 inference(scs_inference,[],[46,149,3])). % 261.37/261.38 cnf(158,plain, % 261.37/261.38 (E(f2(f2(f2(a1,a1),f2(f2(a1,x1581),f2(a3,a3))),a1),f2(f2(f2(f2(a3,a1),f2(a1,x1581)),f2(a3,a3)),a1))), % 261.37/261.38 inference(scs_inference,[],[93,64,3])). % 261.37/261.38 cnf(167,plain, % 261.37/261.38 (E(f2(x1671,f2(x1671,f2(x1672,x1671))),f2(f2(f2(a1,x1671),f2(f2(a3,a1),x1672)),x1671))), % 261.37/261.38 inference(scs_inference,[],[8,149,3])). % 261.37/261.38 cnf(170,plain, % 261.37/261.38 (E(f2(a1,f2(a1,f2(x1701,a1))),f2(f2(f2(a3,a1),f2(f2(a3,a3),x1701)),a1))), % 261.37/261.38 inference(scs_inference,[],[14,49,3])). % 261.37/261.38 cnf(173,plain, % 261.37/261.38 (E(f2(x1731,f2(x1731,f2(f2(a1,x1731),x1731))),f2(f2(f2(f2(a3,a1),f2(a3,a1)),f2(a1,x1731)),x1731))), % 261.37/261.38 inference(scs_inference,[],[38,167,3])). % 261.37/261.38 cnf(176,plain, % 261.37/261.38 (E(f2(a1,f2(a1,f2(x1761,a1))),f2(f2(f2(f2(a1,f2(a3,a1)),f2(a3,a3)),x1761),a1))), % 261.37/261.38 inference(scs_inference,[],[46,170,3])). % 261.37/261.38 cnf(182,plain, % 261.37/261.38 (E(f2(a1,f2(f2(f2(a3,a3),f2(a1,a1)),a1)),f2(f2(f2(f2(a3,a1),f2(a3,a1)),f2(a1,a1)),a1))), % 261.37/261.38 inference(scs_inference,[],[173,32,3])). % 261.37/261.38 cnf(185,plain, % 261.37/261.38 (E(f2(f2(f2(a3,a3),f2(f2(a3,a3),f2(a1,a1))),a1),f2(f2(f2(f2(a3,a1),f2(a3,a1)),f2(a1,a1)),a1))), % 261.37/261.38 inference(scs_inference,[],[182,16,3])). % 261.37/261.38 cnf(189,plain, % 261.37/261.38 (E(f2(x1891,f2(x1892,f2(x1893,x1894))),f2(f2(f2(a1,x1891),f2(f2(a1,x1892),x1893)),x1894))), % 261.37/261.38 inference(scs_inference,[],[15,45,3])). % 261.37/261.38 cnf(195,plain, % 261.37/261.38 (E(f2(x1951,f2(x1951,f2(x1952,x1951))),f2(f2(f2(f2(a1,f2(a1,x1951)),f2(a3,a1)),x1952),x1951))), % 261.37/261.38 inference(scs_inference,[],[46,167,3])). % 261.37/261.38 cnf(198,plain, % 261.37/261.38 (E(f2(f2(f2(a3,a3),f2(f2(a3,a3),f2(a3,a3))),a1),f2(f2(f2(f2(a3,a1),f2(a1,a1)),f2(a3,a3)),a1))), % 261.37/261.38 inference(scs_inference,[],[93,56,3])). % 261.37/261.38 cnf(201,plain, % 261.37/261.38 (E(f2(a1,f2(f2(f2(a3,a3),f2(a3,a3)),a1)),f2(f2(f2(f2(a3,a1),f2(a1,a1)),f2(a3,a3)),a1))), % 261.37/261.38 inference(scs_inference,[],[198,19,3])). % 261.37/261.38 cnf(203,plain, % 261.37/261.38 (E(f2(f2(f2(a3,a3),f2(f2(a1,a1),f2(a1,a1))),a1),f2(f2(f2(f2(a3,a1),f2(a3,a1)),f2(a1,a1)),a1))), % 261.37/261.38 inference(scs_inference,[],[173,41,3])). % 261.37/261.39 cnf(206,plain, % 261.37/261.39 (E(f2(f2(f2(a1,a1),f2(f2(a1,a1),f2(a1,a1))),a1),f2(f2(f2(f2(a3,a1),f2(a3,a1)),f2(a1,a1)),a1))), % 261.37/261.39 inference(scs_inference,[],[203,20,3])). % 261.37/261.39 cnf(211,plain, % 261.37/261.39 (E(f2(a1,f2(f2(f2(a1,a1),f2(a1,a1)),a1)),f2(f2(f2(f2(a3,a1),f2(a3,a1)),f2(a1,a1)),a1))), % 261.37/261.39 inference(scs_inference,[],[203,19,3])). % 261.37/261.39 cnf(213,plain, % 261.37/261.39 (E(f2(f2(a3,a1),f2(f2(a3,a1),f2(f2(a3,a1),f2(a3,a1)))),f2(f2(f2(a3,f2(a3,a1)),f2(a3,a1)),f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[10,152,3])). % 261.37/261.39 cnf(216,plain, % 261.37/261.39 (E(f2(f2(f2(a1,a1),f2(f2(a1,x2161),x2162)),a1),f2(f2(f2(a1,a1),x2161),f2(x2162,a1)))), % 261.37/261.39 inference(scs_inference,[],[15,64,3])). % 261.37/261.39 cnf(219,plain, % 261.37/261.39 (E(f2(f2(a3,a1),f2(f2(a3,a1),f2(f2(a3,a1),f2(a3,a1)))),f2(f2(f2(a3,a3),f2(a3,a1)),f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[213,10,3])). % 261.37/261.39 cnf(221,plain, % 261.37/261.39 (E(f2(f2(f2(a3,a3),f2(f2(a1,x2211),x2212)),a1),f2(f2(f2(a1,a1),x2211),f2(x2212,a1)))), % 261.37/261.39 inference(scs_inference,[],[216,23,3])). % 261.37/261.39 cnf(223,plain, % 261.37/261.39 (E(f2(a1,f2(f2(f2(a1,x2231),x2232),a1)),f2(f2(f2(a1,a1),x2231),f2(x2232,a1)))), % 261.37/261.39 inference(scs_inference,[],[221,19,3])). % 261.37/261.39 cnf(225,plain, % 261.37/261.39 (E(f2(a1,f2(a1,f2(f2(a1,a1),a1))),f2(f2(f2(f2(a3,a1),f2(a3,a3)),f2(a1,a1)),a1))), % 261.37/261.39 inference(scs_inference,[],[38,121,3])). % 261.37/261.39 cnf(228,plain, % 261.37/261.39 (E(f2(f2(f2(a3,a3),f2(f2(a1,a1),f2(a1,a1))),a1),f2(f2(f2(f2(a3,a1),f2(a3,a3)),f2(a1,a1)),a1))), % 261.37/261.39 inference(scs_inference,[],[41,225,3])). % 261.37/261.39 cnf(230,plain, % 261.37/261.39 (E(f2(x2301,f2(x2302,f2(x2303,x2304))),f2(f2(f2(f2(a1,f2(a1,x2301)),f2(a1,x2302)),x2303),x2304))), % 261.37/261.39 inference(scs_inference,[],[46,189,3])). % 261.37/261.39 cnf(235,plain, % 261.37/261.39 (~E(x2351,f2(f2(a3,a1),x2351))), % 261.37/261.39 inference(scs_inference,[],[34,4])). % 261.37/261.39 cnf(236,plain, % 261.37/261.39 (~E(f2(f2(a3,a1),x2361),x2361)), % 261.37/261.39 inference(scs_inference,[],[34,4,2])). % 261.37/261.39 cnf(237,plain, % 261.37/261.39 (~E(f2(a1,f2(x2371,a1)),f2(f2(a3,a1),f2(f2(f2(a3,a3),x2371),a1)))), % 261.37/261.39 inference(scs_inference,[],[34,16,4,2,3])). % 261.37/261.39 cnf(238,plain, % 261.37/261.39 (~E(f2(f2(a3,a1),f2(f2(f2(a3,a3),x2381),a1)),f2(a1,f2(x2381,a1)))), % 261.37/261.39 inference(scs_inference,[],[237,2])). % 261.37/261.39 cnf(239,plain, % 261.37/261.39 (~E(f2(f2(f2(a3,a3),f2(a3,a1)),f2(a3,a1)),f2(f2(a3,a1),f2(f2(a3,a1),f2(a3,a1))))), % 261.37/261.39 inference(scs_inference,[],[236,237,219,2,3])). % 261.37/261.39 cnf(242,plain, % 261.37/261.39 (~E(f2(f2(f2(a3,x2421),x2422),x2423),f2(f2(a3,a1),f2(f2(f2(x2421,x2423),x2422),x2423)))), % 261.37/261.39 inference(scs_inference,[],[235,239,10,2,3])). % 261.37/261.39 cnf(244,plain, % 261.37/261.39 (~E(f2(f2(a3,a1),f2(f2(f2(x2441,x2442),x2443),x2442)),f2(f2(f2(a3,x2441),x2443),x2442))), % 261.37/261.39 inference(scs_inference,[],[242,2])). % 261.37/261.39 cnf(245,plain, % 261.37/261.39 (~E(f2(f2(f2(a1,f2(a3,a1)),a1),f2(a3,a1)),f2(a1,f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[238,242,147,2,3])). % 261.37/261.39 cnf(248,plain, % 261.37/261.39 (~E(f2(a1,f2(a3,a1)),f2(f2(f2(a1,f2(a3,a1)),a1),f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[245,2])). % 261.37/261.39 cnf(249,plain, % 261.37/261.39 (~E(f2(f2(a3,a1),f2(a1,f2(x2491,a1))),f2(f2(f2(a3,a3),x2491),a1))), % 261.37/261.39 inference(scs_inference,[],[245,244,51,2,3])). % 261.37/261.39 cnf(252,plain, % 261.37/261.39 (~E(x2521,f2(f2(a1,f4(x2521)),x2521))), % 261.37/261.39 inference(scs_inference,[],[40,245,244,51,2,3,4])). % 261.37/261.39 cnf(253,plain, % 261.37/261.39 (~E(f2(f2(a1,f4(x2531)),x2531),x2531)), % 261.37/261.39 inference(scs_inference,[],[252,2])). % 261.37/261.39 cnf(254,plain, % 261.37/261.39 (~E(f2(f2(f2(a1,a1),a3),a1),f2(f2(f2(a1,f2(a3,a1)),a1),f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[252,248,15,2,3])). % 261.37/261.39 cnf(257,plain, % 261.37/261.39 (~E(f2(f2(f2(a3,a1),a3),a1),f2(f2(f2(a1,f2(a3,a1)),a1),f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[99,254,10,2,3])). % 261.37/261.39 cnf(259,plain, % 261.37/261.39 (~E(f2(f2(f2(a3,a3),x2591),a1),f2(f2(a3,a1),f2(a1,f2(x2591,a1))))), % 261.37/261.39 inference(scs_inference,[],[249,2])). % 261.37/261.39 cnf(260,plain, % 261.37/261.39 (~E(f2(f2(f2(a3,f2(a3,a1)),f2(a3,a1)),f2(a3,a1)),f2(f2(a3,a1),f2(f2(a3,a1),f2(a3,a1))))), % 261.37/261.39 inference(scs_inference,[],[249,239,8,2,3])). % 261.37/261.39 cnf(262,plain, % 261.37/261.39 (E(f2(f2(f2(a1,a1),x2621),f2(x2622,a1)),f2(a1,f2(f2(f2(a1,x2621),x2622),a1)))), % 261.37/261.39 inference(scs_inference,[],[223,2])). % 261.37/261.39 cnf(263,plain, % 261.37/261.39 (~E(f2(f2(f2(a1,a1),x2631),a1),f2(f2(a3,a1),f2(a1,f2(x2631,a1))))), % 261.37/261.39 inference(scs_inference,[],[259,223,23,2,3])). % 261.37/261.39 cnf(265,plain, % 261.37/261.39 (~E(a1,f2(f2(a1,f2(a3,a1)),a1))), % 261.37/261.39 inference(scs_inference,[],[259,223,248,23,2,3,4])). % 261.37/261.39 cnf(267,plain, % 261.37/261.39 (~E(a1,f2(f2(f2(f2(a3,a1),a3),a1),a1))), % 261.37/261.39 inference(scs_inference,[],[265,52,2,3])). % 261.37/261.39 cnf(269,plain, % 261.37/261.39 (E(f2(f2(f2(f2(a3,a1),f2(a3,a1)),f2(a3,a1)),a1),f2(a1,f2(f2(f2(a3,a3),f2(a3,a1)),a1)))), % 261.37/261.39 inference(scs_inference,[],[111,2])). % 261.37/261.39 cnf(272,plain, % 261.37/261.39 (~E(f2(f2(a3,a1),f2(f2(a3,a1),f2(a3,a1))),f2(f2(f2(a3,f2(a3,a1)),f2(a3,a1)),f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[260,2])). % 261.37/261.39 cnf(276,plain, % 261.37/261.39 (~E(f2(f2(f2(f2(a1,f2(a3,a1)),f2(a3,a1)),x2761),f2(a3,a1)),f2(f2(a3,a1),f2(x2761,f2(a3,a1))))), % 261.37/261.39 inference(scs_inference,[],[102,155,236,2,3])). % 261.37/261.39 cnf(280,plain, % 261.37/261.39 (~E(f2(f2(f2(a3,a1),f2(f2(a3,a1),x2801)),f2(a3,a1)),f2(f2(a3,a1),f2(x2801,f2(a3,a1))))), % 261.37/261.39 inference(scs_inference,[],[263,276,25,2,3])). % 261.37/261.39 cnf(284,plain, % 261.37/261.39 (~E(f2(f2(f2(a3,a3),a3),a1),f2(f2(f2(a1,f2(a3,a1)),a1),f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[257,82,10,2,3])). % 261.37/261.39 cnf(287,plain, % 261.37/261.39 (~E(f2(f2(a3,a1),f2(f2(f2(a3,a1),x2871),f2(a3,a1))),f2(f2(a3,a1),f2(x2871,f2(a3,a1))))), % 261.37/261.39 inference(scs_inference,[],[267,280,11,2,3])). % 261.37/261.39 cnf(289,plain, % 261.37/261.39 (~E(f2(f2(f2(a3,a1),x2891),f2(a3,a1)),f2(x2891,f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[267,280,11,2,3,5])). % 261.37/261.39 cnf(291,plain, % 261.37/261.39 (~E(f2(f2(f2(a1,f2(a3,a1)),x2911),f2(a3,a1)),f2(x2911,f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[289,206,8,2,3])). % 261.37/261.39 cnf(293,plain, % 261.37/261.39 (~E(f2(f2(a1,f2(a3,a1)),x2931),x2931)), % 261.37/261.39 inference(scs_inference,[],[289,206,8,2,3,4])). % 261.37/261.39 cnf(294,plain, % 261.37/261.39 (~E(x2941,f2(f2(a1,f2(a3,a1)),x2941))), % 261.37/261.39 inference(scs_inference,[],[293,2])). % 261.37/261.39 cnf(298,plain, % 261.37/261.39 (~E(f2(x2981,f2(x2982,x2981)),f2(f2(a1,f2(a3,a1)),f2(f2(f2(a3,a1),x2982),x2981)))), % 261.37/261.39 inference(scs_inference,[],[294,143,11,2,3])). % 261.37/261.39 cnf(300,plain, % 261.37/261.39 (~E(f2(x3001,f2(a3,a1)),f2(f2(f2(a1,f2(a3,a1)),x3001),f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[291,2])). % 261.37/261.39 cnf(302,plain, % 261.37/261.39 (~E(f2(f2(f2(a1,f2(a3,a1)),a1),f2(a3,a1)),f2(f2(f2(a3,a3),a3),a1))), % 261.37/261.39 inference(scs_inference,[],[284,2])). % 261.37/261.39 cnf(303,plain, % 261.37/261.39 (E(f2(f2(f2(f2(a3,a1),f2(a3,a1)),f2(a3,a1)),a1),f2(f2(f2(a1,a1),f2(f2(a3,a3),f2(a3,a1))),a1))), % 261.37/261.39 inference(scs_inference,[],[105,2])). % 261.37/261.39 cnf(304,plain, % 261.37/261.39 (~E(f2(f2(f2(a3,x3041),x3042),f2(a3,a1)),f2(f2(f2(a1,f2(a3,a1)),f2(f2(x3041,f2(a3,a1)),x3042)),f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[105,300,10,2,3])). % 261.37/261.39 cnf(309,plain, % 261.37/261.39 (~E(f2(x3091,f2(a3,a1)),f2(f2(f2(a3,a1),x3091),f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[287,304,4,2,5])). % 261.37/261.39 cnf(310,plain, % 261.37/261.39 (~E(f2(a1,f2(f2(f2(a1,x3101),a3),a1)),f2(f2(f2(a3,a1),f2(f2(a1,a1),x3101)),f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[287,304,262,4,2,5,3])). % 261.37/261.39 cnf(312,plain, % 261.37/261.39 (E(f2(f2(f2(f2(a3,a1),f2(a1,a1)),f2(a1,a1)),a1),f2(a1,f2(f2(f2(a3,a1),f2(a1,a1)),a1)))), % 261.37/261.39 inference(scs_inference,[],[145,2])). % 261.37/261.39 cnf(313,plain, % 261.37/261.39 (~E(f2(f2(x3131,f2(x3132,x3131)),f2(a3,a1)),f2(f2(f2(a3,a1),f2(f2(f2(a3,a1),x3132),x3131)),f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[309,145,52,2,3])). % 261.37/261.39 cnf(317,plain, % 261.37/261.39 (~E(f2(f2(x3171,f2(x3172,x3173)),f2(a3,a1)),f2(f2(f2(a3,a1),f2(f2(f2(a1,x3171),x3172),x3173)),f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[298,309,25,2,3])). % 261.37/261.39 cnf(336,plain, % 261.37/261.39 (~E(f2(f2(f2(a3,a1),a1),f2(a3,a1)),f2(f2(f2(a3,a3),a3),a1))), % 261.37/261.39 inference(scs_inference,[],[302,138,10,2,3])). % 261.37/261.39 cnf(338,plain, % 261.37/261.39 (~E(f2(f2(f2(a3,a3),a3),a1),f2(f2(f2(a3,a1),a1),f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[336,2])). % 261.37/261.39 cnf(339,plain, % 261.37/261.39 (~E(f2(f2(f2(a1,a1),a3),a1),f2(f2(f2(a3,a1),a1),f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[336,23,2,3])). % 261.37/261.39 cnf(346,plain, % 261.37/261.39 (~E(f2(f2(f2(a3,a1),a3),a1),f2(f2(f2(a3,a1),a1),f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[339,338,8,2,3])). % 261.37/261.39 cnf(349,plain, % 261.37/261.39 (~E(f2(f2(f2(a3,a1),f2(a3,a1)),f2(a3,a1)),f2(f2(f2(a3,f2(a3,a1)),f2(a3,a1)),f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[107,272,14,2,3])). % 261.37/261.39 cnf(351,plain, % 261.37/261.39 (~E(f2(f2(f2(a3,f2(a3,a1)),f2(a3,a1)),f2(a3,a1)),f2(f2(f2(a3,a1),f2(a3,a1)),f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[349,2])). % 261.37/261.39 cnf(352,plain, % 261.37/261.39 (~E(f2(f2(a3,a1),f2(a3,a1)),f2(f2(a3,f2(a3,a1)),f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[349,2,4])). % 261.37/261.39 cnf(356,plain, % 261.37/261.39 (~E(f2(f2(a3,f2(a3,a1)),f2(a3,a1)),f2(f2(a3,a1),f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[352,2])). % 261.37/261.39 cnf(360,plain, % 261.37/261.39 (~E(f2(f2(f2(f2(a1,a3),a3),a1),f2(a3,a1)),f2(f2(a3,a1),f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[356,201,46,2,3])). % 261.37/261.39 cnf(363,plain, % 261.37/261.39 (~E(f2(f2(a3,a1),f2(a1,f2(a3,a1))),f2(f2(f2(a3,a1),a3),a1))), % 261.37/261.39 inference(scs_inference,[],[346,11,2,3])). % 261.37/261.39 cnf(365,plain, % 261.37/261.39 (~E(f2(f2(f2(a1,a3),a3),a1),f2(a3,a1))), % 261.37/261.39 inference(scs_inference,[],[346,360,11,2,3,4])). % 261.37/261.39 cnf(367,plain, % 261.37/261.39 (~E(f2(a3,f2(a3,a1)),f2(a3,a1))), % 261.37/261.39 inference(scs_inference,[],[365,211,7,2,3])). % 261.37/261.39 cnf(369,plain, % 261.37/261.39 (~E(f2(a3,a1),a1)), % 261.37/261.39 inference(scs_inference,[],[365,211,7,2,3,5])). % 261.37/261.39 cnf(371,plain, % 261.37/261.39 (~E(f2(f2(f2(f2(a3,a1),x3711),f2(a3,a1)),f2(a3,a1)),f2(f2(x3711,f2(a3,a1)),f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[369,289,38,2,3])). % 261.37/261.39 cnf(375,plain, % 261.37/261.39 (~E(f2(a3,a1),f2(a3,f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[367,2])). % 261.37/261.39 cnf(376,plain, % 261.37/261.39 (~E(f2(x3761,f2(x3762,x3763)),f2(f2(a3,a1),f2(f2(f2(a1,x3761),x3762),x3763)))), % 261.37/261.39 inference(scs_inference,[],[367,317,2,4])). % 261.37/261.39 cnf(378,plain, % 261.37/261.39 (~E(f2(f2(f2(a3,a3),f2(a3,a1)),f2(a3,a1)),f2(f2(a3,a1),f2(f2(f2(a1,f2(a3,a1)),f2(a3,a1)),f2(f2(a3,a1),f2(a3,a1)))))), % 261.37/261.39 inference(scs_inference,[],[109,376,219,2,3])). % 261.37/261.39 cnf(379,plain, % 261.37/261.39 (~E(f2(x3791,f2(x3792,x3793)),f2(f2(a3,a1),f2(f2(f2(a1,x3791),x3792),x3793)))), % 261.37/261.39 inference(rename_variables,[],[376])). % 261.37/261.39 cnf(380,plain, % 261.37/261.39 (~E(f2(x3801,x3802),f2(f2(f2(a1,f2(a3,a1)),x3801),x3802))), % 261.37/261.39 inference(scs_inference,[],[109,376,379,219,2,3,5])). % 261.37/261.39 cnf(382,plain, % 261.37/261.39 (~E(f2(f2(x3821,f2(a3,a1)),f2(a3,a1)),f2(f2(f2(f2(a3,a1),x3821),f2(a3,a1)),f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[371,2])). % 261.37/261.39 cnf(383,plain, % 261.37/261.39 (~E(f2(a3,a1),f2(f2(f2(a1,a3),a3),a1))), % 261.37/261.39 inference(scs_inference,[],[375,371,7,2,3])). % 261.37/261.39 cnf(386,plain, % 261.37/261.39 (~E(f2(f2(f2(a3,a1),a1),f2(x3861,a1)),f2(f2(f2(a1,f2(a3,a1)),f2(x3861,a1)),f2(f2(f2(a3,a3),x3861),a1)))), % 261.37/261.39 inference(scs_inference,[],[380,158,118,2,3])). % 261.37/261.39 cnf(392,plain, % 261.37/261.39 (~E(a3,f2(f2(a1,a3),a3))), % 261.37/261.39 inference(scs_inference,[],[383,363,195,236,2,3,4])). % 261.37/261.39 cnf(393,plain, % 261.37/261.39 (E(f2(f2(f2(f2(a3,a1),f2(a1,x3931)),f2(a1,a1)),a1),f2(a1,f2(f2(f2(a1,x3931),f2(a1,a1)),a1)))), % 261.37/261.39 inference(scs_inference,[],[132,2])). % 261.37/261.39 cnf(394,plain, % 261.37/261.39 (~E(f2(f2(f2(a3,x3941),f2(a3,a1)),f2(a3,a1)),f2(f2(f2(f2(a3,a1),f2(x3941,f2(a3,a1))),f2(a3,a1)),f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[382,132,10,2,3])). % 261.37/261.39 cnf(398,plain, % 261.37/261.39 (~E(f2(f2(a3,a1),f2(f2(a3,a1),f2(a3,a1))),f2(f2(f2(f2(a3,a1),f2(a1,f2(a3,a1))),f2(a3,a1)),f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[392,394,11,2,3])). % 261.37/261.39 cnf(406,plain, % 261.37/261.39 (E(f2(f2(f2(f2(a1,f2(a3,a1)),f2(a3,a3)),x4061),a1),f2(a1,f2(a1,f2(x4061,a1))))), % 261.37/261.39 inference(scs_inference,[],[176,2])). % 261.37/261.39 cnf(416,plain, % 261.37/261.39 (E(f2(f2(f2(f2(a1,f2(a3,a3)),f2(a3,a1)),x4161),a1),f2(a1,f2(a1,f2(x4161,a1))))), % 261.37/261.39 inference(scs_inference,[],[73,2])). % 261.37/261.39 cnf(427,plain, % 261.37/261.39 (~E(f2(f2(a3,x4271),f2(a3,a1)),f2(f2(f2(a3,a1),f2(x4271,f2(a3,a1))),f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[398,394,2,4])). % 261.37/261.39 cnf(431,plain, % 261.37/261.39 (~E(f2(f2(f2(a3,a1),f2(x4311,f2(a3,a1))),f2(a3,a1)),f2(f2(a3,x4311),f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[427,2])). % 261.37/261.39 cnf(433,plain, % 261.37/261.39 (E(f2(f2(f2(a3,f2(a3,a1)),f2(a3,a1)),f2(a3,a1)),f2(f2(a3,a1),f2(f2(a3,a1),f2(f2(a3,a1),f2(a3,a1)))))), % 261.37/261.39 inference(scs_inference,[],[213,2])). % 261.37/261.39 cnf(434,plain, % 261.37/261.39 (~E(f2(f2(f2(f2(a3,a1),x4341),f2(a3,a1)),f2(a3,a1)),f2(f2(a3,x4341),f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[431,213,38,2,3])). % 261.37/261.39 cnf(438,plain, % 261.37/261.39 (E(f2(f2(f2(a3,a1),f2(f2(a3,a3),x4381)),a1),f2(a1,f2(a1,f2(x4381,a1))))), % 261.37/261.39 inference(scs_inference,[],[170,2])). % 261.37/261.39 cnf(439,plain, % 261.37/261.39 (~E(f2(f2(a3,a1),f2(f2(a3,a1),f2(f2(a3,a1),f2(a3,a1)))),f2(f2(f2(a3,a1),f2(a3,a1)),f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[433,351,170,2,3])). % 261.37/261.39 cnf(440,plain, % 261.37/261.39 (~E(f2(f2(f2(a3,a1),x4401),f2(a3,a1)),f2(a3,x4401))), % 261.37/261.39 inference(scs_inference,[],[434,433,351,170,2,3,4])). % 261.37/261.39 cnf(441,plain, % 261.37/261.39 (~E(f2(a3,x4411),f2(f2(f2(a3,a1),x4411),f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[440,2])). % 261.37/261.39 cnf(442,plain, % 261.37/261.39 (~E(f2(f2(f2(f2(a3,a1),x4421),f2(a3,a1)),f2(a3,a1)),f2(a3,f2(x4421,f2(a3,a1))))), % 261.37/261.39 inference(scs_inference,[],[440,38,2,3])). % 261.37/261.39 cnf(451,plain, % 261.37/261.39 (~E(f2(a3,f2(x4511,f2(a3,a1))),f2(f2(f2(f2(a3,a1),x4511),f2(a3,a1)),f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[442,2])). % 261.37/261.39 cnf(459,plain, % 261.37/261.39 (~E(a3,f2(f2(a3,a1),f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[451,441,136,230,2,3,4])). % 261.37/261.39 cnf(463,plain, % 261.37/261.39 (~E(f2(f2(f2(f2(a1,f2(a3,a1)),f2(a3,a1)),f2(a3,a1)),f2(a3,a1)),f2(f2(f2(a3,a1),f2(a3,a1)),f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[459,439,155,2,3])). % 261.37/261.39 cnf(466,plain, % 261.37/261.39 (E(f2(f2(f2(f2(a3,a1),f2(a3,a1)),f2(a3,a1)),x4661),f2(x4661,f2(x4661,f2(f2(a3,a1),x4661))))), % 261.37/261.39 inference(scs_inference,[],[152,2])). % 261.37/261.39 cnf(470,plain, % 261.37/261.39 (~E(f2(f2(f2(a3,a1),f2(a3,a1)),f2(a3,a1)),f2(f2(f2(f2(a1,f2(a3,a1)),f2(a3,a1)),f2(a3,a1)),f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[463,2])). % 261.37/261.39 cnf(471,plain, % 261.37/261.39 (~E(f2(f2(f2(a3,f2(a1,f2(a3,a1))),f2(a3,a1)),f2(a3,a1)),f2(f2(f2(a3,a1),f2(a3,a1)),f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[463,10,2,3])). % 261.37/261.39 cnf(474,plain, % 261.37/261.39 (E(f2(f2(f2(f2(a3,a1),f2(a3,a1)),f2(a3,a1)),a1),f2(f2(f2(a1,a1),f2(f2(a1,a1),f2(a3,a1))),a1))), % 261.37/261.39 inference(scs_inference,[],[78,2])). % 261.37/261.39 cnf(477,plain, % 261.37/261.39 (~E(f2(f2(a3,f2(a1,f2(a3,a1))),f2(a3,a1)),f2(f2(a3,a1),f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[470,471,78,11,2,3,4])). % 261.37/261.39 cnf(479,plain, % 261.37/261.39 (~E(f2(f2(a3,a1),f2(a3,a1)),f2(f2(a3,f2(a1,f2(a3,a1))),f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[477,2])). % 261.37/261.39 cnf(482,plain, % 261.37/261.39 (~E(f2(f2(f2(a1,f2(a3,a1)),a3),a1),f2(f2(a3,f2(a1,f2(a3,a1))),f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[479,80,15,2,3])). % 261.37/261.39 cnf(487,plain, % 261.37/261.39 (~E(f2(a3,f2(a1,f2(a3,a1))),f2(a3,a1))), % 261.37/261.39 inference(scs_inference,[],[477,185,2,4])). % 261.37/261.39 cnf(490,plain, % 261.37/261.39 (~E(f2(a3,a1),f2(a3,f2(a1,f2(a3,a1))))), % 261.37/261.39 inference(scs_inference,[],[487,5,2])). % 261.37/261.39 cnf(502,plain, % 261.37/261.39 (~E(f2(a3,x5021),f2(f2(a3,a1),f2(x5021,f2(a3,a1))))), % 261.37/261.39 inference(scs_inference,[],[427,4])). % 261.37/261.39 cnf(509,plain, % 261.37/261.39 (~E(f2(f2(f2(a3,a1),f2(f2(a1,x5091),x5092)),a3),f2(f2(a3,a1),f2(f2(x5091,f2(x5092,a3)),f2(a3,a1))))), % 261.37/261.39 inference(scs_inference,[],[502,490,84,5,2,3])). % 261.37/261.39 cnf(513,plain, % 261.37/261.39 (E(f2(f2(f2(f2(a3,a1),f2(a3,a3)),f2(a1,a1)),a1),f2(a1,f2(a1,f2(f2(a1,a1),a1))))), % 261.37/261.39 inference(scs_inference,[],[225,2])). % 261.37/261.39 cnf(522,plain, % 261.37/261.39 (E(f2(f2(f2(f2(a3,a1),f2(a3,a3)),f2(a1,a1)),a1),f2(f2(f2(a3,a3),f2(f2(a1,a1),f2(a1,a1))),a1))), % 261.37/261.39 inference(scs_inference,[],[228,2])). % 261.37/261.39 cnf(542,plain, % 261.37/261.39 (E(f2(f2(f2(f2(a3,a1),f2(a1,x5421)),f2(a1,a1)),a1),f2(f2(f2(a3,a3),f2(f2(a1,x5421),f2(a1,a1))),a1))), % 261.37/261.39 inference(scs_inference,[],[129,2])). % 261.37/261.39 cnf(566,plain, % 261.37/261.39 (~E(f2(f2(f2(a3,a3),f2(f2(a1,x5661),a3)),a1),f2(f2(f2(a3,a1),f2(f2(a1,a1),x5661)),f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[310,203,19,2,3])). % 261.37/261.39 cnf(577,plain, % 261.37/261.39 (~E(f2(a1,f2(x5771,f2(a3,a1))),f2(f2(f2(a3,a1),f2(f2(a1,a1),x5771)),f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[482,566,41,2,3])). % 261.37/261.39 cnf(584,plain, % 261.37/261.39 (~E(f2(f2(f2(a3,a1),f2(f2(a3,a3),a3)),a1),f2(f2(f2(a3,a1),f2(f2(a1,a1),a1)),f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[577,170,2,3])). % 261.37/261.39 cnf(596,plain, % 261.37/261.39 (E(f2(f2(f2(f2(a1,f2(a1,x5961)),f2(a3,a1)),x5962),x5961),f2(x5961,f2(x5961,f2(x5962,x5961))))), % 261.37/261.39 inference(scs_inference,[],[195,2])). % 261.37/261.39 cnf(603,plain, % 261.37/261.39 (E(f2(f2(f2(a3,a3),f2(a3,a1)),f2(a3,a1)),f2(f2(a3,a1),f2(f2(a3,a1),f2(f2(a3,a1),f2(a3,a1)))))), % 261.37/261.39 inference(scs_inference,[],[219,2])). % 261.37/261.39 cnf(608,plain, % 261.37/261.39 (~E(f2(a3,f2(f2(f2(a1,x6081),x6082),a3)),f2(f2(a3,a1),f2(f2(x6081,f2(x6082,a3)),f2(a3,a1))))), % 261.37/261.39 inference(scs_inference,[],[584,509,11,2,3])). % 261.37/261.39 cnf(615,plain, % 261.37/261.39 (E(f2(f2(f2(a3,a1),f2(f2(a1,x6151),x6152)),x6153),f2(x6153,f2(x6151,f2(x6152,x6153))))), % 261.37/261.39 inference(scs_inference,[],[84,2])). % 261.37/261.39 cnf(619,plain, % 261.37/261.39 (E(f2(f2(f2(f2(a3,a1),f2(a1,x6191)),f2(a3,a3)),a1),f2(a1,f2(x6191,f2(f2(a3,a3),a1))))), % 261.37/261.39 inference(scs_inference,[],[93,2])). % 261.37/261.39 cnf(691,plain, % 261.37/261.39 (~E(f2(f2(a3,a1),f2(f2(a3,a1),f2(f2(a3,a1),f2(a3,a1)))),f2(f2(a3,f2(a3,a1)),f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[466,434,3])). % 261.37/261.39 cnf(696,plain, % 261.37/261.39 (~E(f2(f2(f2(a3,f2(a3,a1)),f2(a3,a1)),f2(a3,a1)),f2(f2(a3,f2(a3,a1)),f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[691,213,3])). % 261.37/261.39 cnf(699,plain, % 261.37/261.39 (~E(f2(f2(f2(a3,a3),f2(a3,a1)),f2(a3,a1)),f2(f2(a3,f2(a3,a1)),f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[696,10,3])). % 261.37/261.39 cnf(701,plain, % 261.37/261.39 (~E(f2(f2(a3,a1),f2(f2(a3,a1),f2(f2(a3,a1),f2(a3,a1)))),f2(f2(f2(f2(a3,a1),f2(a3,a3)),f2(a3,a1)),f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[603,382,3])). % 261.37/261.39 cnf(704,plain, % 261.37/261.39 (~E(f2(f2(f2(a3,f2(a3,a1)),f2(a3,a1)),f2(a3,a1)),f2(f2(f2(f2(a3,a1),f2(a3,a3)),f2(a3,a1)),f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[701,213,3])). % 261.37/261.39 cnf(711,plain, % 261.37/261.39 (E(f2(f2(f2(f2(a3,a1),f2(a3,a3)),f2(a3,a1)),a1),f2(a1,f2(a1,f2(f2(a3,a1),a1))))), % 261.37/261.39 inference(scs_inference,[],[438,52,3])). % 261.37/261.39 cnf(715,plain, % 261.37/261.39 (E(f2(a1,f2(a1,f2(f2(a3,a1),a1))),f2(f2(f2(f2(a3,a1),f2(a3,a3)),f2(a3,a1)),a1))), % 261.37/261.39 inference(scs_inference,[],[711,2])). % 261.37/261.39 cnf(716,plain, % 261.37/261.39 (~E(f2(f2(f2(f2(a1,f2(a3,a3)),a3),a1),f2(a3,a1)),f2(f2(a3,f2(a3,a1)),f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[699,711,46,2,3])). % 261.37/261.39 cnf(723,plain, % 261.37/261.39 (E(f2(f2(f2(f2(a1,f2(a1,a1)),f2(a3,a1)),f2(a3,a1)),a1),f2(f2(f2(f2(a3,a1),f2(a3,a3)),f2(a3,a1)),a1))), % 261.37/261.39 inference(scs_inference,[],[715,596,3])). % 261.37/261.39 cnf(727,plain, % 261.37/261.39 (E(f2(f2(f2(f2(a3,a1),f2(a3,a3)),f2(a3,a1)),a1),f2(f2(f2(f2(a1,f2(a1,a1)),f2(a3,a1)),f2(a3,a1)),a1))), % 261.37/261.39 inference(scs_inference,[],[723,2])). % 261.37/261.39 cnf(735,plain, % 261.37/261.39 (E(f2(f2(f2(f2(a1,f2(a3,a1)),f2(a3,a3)),f2(a3,a1)),a1),f2(f2(f2(f2(a3,a1),f2(a3,a3)),f2(a3,a1)),a1))), % 261.37/261.39 inference(scs_inference,[],[406,715,3])). % 261.37/261.39 cnf(766,plain, % 261.37/261.39 (~E(f2(f2(f2(a1,f2(a3,a3)),a3),a1),f2(a3,f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[716,474,216,3,4])). % 261.37/261.39 cnf(767,plain, % 261.37/261.39 (E(f2(f2(f2(a1,a1),a1),f2(f2(a3,a1),a1)),f2(f2(f2(f2(a3,a1),f2(a3,a1)),f2(a3,a1)),a1))), % 261.37/261.39 inference(scs_inference,[],[716,474,216,3,4,2])). % 261.37/261.39 cnf(773,plain, % 261.37/261.39 (~E(f2(f2(a3,a3),f2(a3,a1)),f2(a3,f2(a3,a1)))), % 261.37/261.39 inference(scs_inference,[],[766,7,3])). % 261.37/261.39 cnf(776,plain, % 261.37/261.39 (E(f2(f2(f2(f2(a3,a1),f2(a3,a3)),f2(a1,a1)),a1),f2(f2(f2(f2(a1,f2(a3,a1)),f2(a3,a3)),f2(a1,a1)),a1))), % 261.37/261.39 inference(scs_inference,[],[513,176,3])). % 261.37/261.39 cnf(779,plain, % 261.37/261.39 (E(f2(f2(f2(f2(a1,f2(a3,a1)),f2(a3,a3)),f2(a1,a1)),a1),f2(f2(f2(f2(a3,a1),f2(a3,a3)),f2(a1,a1)),a1))), % 261.37/261.39 inference(scs_inference,[],[776,2])). % 261.37/261.39 cnf(780,plain, % 261.37/261.40 (~E(f2(f2(a3,a3),f2(a3,a1)),f2(f2(f2(a1,a3),a3),a1))), % 261.37/261.40 inference(scs_inference,[],[773,776,7,2,3])). % 261.37/261.40 cnf(782,plain, % 261.37/261.40 (~E(f2(a3,a3),a3)), % 261.37/261.40 inference(scs_inference,[],[773,776,7,2,3,4])). % 261.37/261.40 cnf(785,plain, % 261.37/261.40 (~E(f2(f2(f2(a1,f2(a3,a3)),a3),a1),f2(f2(f2(a1,a3),a3),a1))), % 261.37/261.40 inference(scs_inference,[],[782,780,15,2,3])). % 261.37/261.40 cnf(788,plain, % 261.37/261.40 (E(f2(f2(f2(f2(a3,a1),f2(a3,a3)),f2(a1,a1)),a1),f2(f2(f2(f2(a3,a1),f2(a3,a1)),f2(a1,a1)),a1))), % 261.37/261.40 inference(scs_inference,[],[203,522,3])). % 261.37/261.40 cnf(791,plain, % 261.37/261.40 (E(f2(f2(f2(f2(a3,a1),f2(a3,a1)),f2(a1,a1)),a1),f2(f2(f2(f2(a3,a1),f2(a3,a3)),f2(a1,a1)),a1))), % 261.37/261.40 inference(scs_inference,[],[788,2])). % 261.37/261.40 cnf(793,plain, % 261.37/261.40 (~E(f2(f2(a1,f2(a3,a3)),a3),f2(f2(a1,a3),a3))), % 261.37/261.40 inference(scs_inference,[],[785,4])). % 261.37/261.40 cnf(797,plain, % 261.37/261.40 (E(f2(f2(f2(f2(a3,a1),f2(a1,a1)),f2(a1,a1)),a1),f2(f2(f2(f2(a3,a1),f2(a3,a1)),f2(a1,a1)),a1))), % 261.37/261.40 inference(scs_inference,[],[203,542,3])). % 261.37/261.40 cnf(799,plain, % 261.37/261.40 (E(f2(f2(f2(f2(a3,a1),f2(a3,a1)),f2(a1,a1)),a1),f2(f2(f2(f2(a3,a1),f2(a1,a1)),f2(a1,a1)),a1))), % 261.37/261.40 inference(scs_inference,[],[203,542,3,2])). % 261.37/261.40 cnf(801,plain, % 261.37/261.40 (~E(f2(f2(a1,a3),a3),f2(f2(a1,f2(a3,a3)),a3))), % 261.37/261.40 inference(scs_inference,[],[793,2])). % 261.37/261.40 cnf(802,plain, % 261.37/261.40 (~E(f2(f2(f2(f2(a1,a1),a3),a3),a3),f2(f2(a1,a3),a3))), % 261.37/261.40 inference(scs_inference,[],[793,46,2,3])). % 261.37/261.40 cnf(810,plain, % 261.37/261.40 (~E(f2(a1,a3),f2(a1,f2(a3,a3)))), % 261.37/261.40 inference(scs_inference,[],[801,767,269,3,2,4])). % 261.37/261.40 cnf(812,plain, % 261.37/261.40 (~E(f2(a1,f2(a3,a3)),f2(a1,a3))), % 261.37/261.40 inference(scs_inference,[],[810,2])). % 261.37/261.40 cnf(813,plain, % 261.37/261.40 (E(f2(f2(f2(f2(a3,a1),f2(a1,a1)),f2(a3,a3)),a1),f2(f2(f2(f2(a1,f2(a3,a3)),f2(a3,a3)),f2(a3,a3)),a1))), % 261.37/261.40 inference(scs_inference,[],[810,619,99,2,3])). % 261.37/261.40 cnf(818,plain, % 261.37/261.40 (~E(f2(f2(f2(a1,a1),a3),a3),f2(a1,a3))), % 261.37/261.40 inference(scs_inference,[],[812,813,15,2,3])). % 261.37/261.40 cnf(822,plain, % 261.37/261.40 (E(f2(f2(f2(a1,a1),a1),f2(f2(a3,a1),a1)),f2(f2(f2(a1,a1),f2(f2(a3,a3),f2(a3,a1))),a1))), % 261.37/261.40 inference(scs_inference,[],[818,303,767,2,3])). % 261.37/261.40 cnf(825,plain, % 261.37/261.40 (E(f2(f2(f2(f2(a3,a1),f2(a1,x8251)),f2(a1,a1)),a1),f2(f2(f2(a1,a1),x8251),f2(f2(a1,a1),a1)))), % 261.37/261.40 inference(scs_inference,[],[822,393,223,2,3])). % 261.37/261.40 cnf(833,plain, % 261.37/261.40 (E(f2(f2(f2(a1,a1),x8331),f2(f2(a1,a1),a1)),f2(f2(f2(f2(a3,a1),f2(a1,x8331)),f2(a1,a1)),a1))), % 261.37/261.40 inference(scs_inference,[],[825,2])). % 261.37/261.40 cnf(838,plain, % 261.37/261.40 (~E(f2(f2(a1,a3),a3),f2(f2(f2(f2(a1,a1),a3),a3),a3))), % 261.37/261.40 inference(scs_inference,[],[802,2])). % 261.37/261.40 cnf(849,plain, % 261.37/261.40 (E(f2(f2(f2(a1,a1),a1),f2(f2(a1,a1),a1)),f2(f2(f2(f2(a3,a1),f2(a3,a1)),f2(a1,a1)),a1))), % 261.37/261.40 inference(scs_inference,[],[797,833,3])). % 261.37/261.40 cnf(851,plain, % 261.37/261.40 (E(f2(f2(f2(f2(a3,a1),f2(a3,a1)),f2(a1,a1)),a1),f2(f2(f2(a1,a1),a1),f2(f2(a1,a1),a1)))), % 261.37/261.40 inference(scs_inference,[],[797,833,3,2])). % 261.37/261.40 cnf(857,plain, % 261.37/261.40 (E(f2(f2(f2(a1,a1),a1),f2(f2(a1,a1),a1)),f2(f2(f2(f2(a3,a1),f2(a3,a3)),f2(a1,a1)),a1))), % 261.37/261.40 inference(scs_inference,[],[791,849,3])). % 261.37/261.40 cnf(860,plain, % 261.37/261.40 (E(f2(f2(f2(f2(a3,a1),f2(a3,a3)),f2(a1,a1)),a1),f2(f2(f2(a1,a1),a1),f2(f2(a1,a1),a1)))), % 261.37/261.40 inference(scs_inference,[],[857,2])). % 261.37/261.40 cnf(862,plain, % 261.37/261.40 (E(f2(f2(f2(f2(a1,f2(a3,a1)),f2(a3,a3)),f2(a1,a1)),a1),f2(f2(f2(a1,a1),a1),f2(f2(a1,a1),a1)))), % 261.37/261.40 inference(scs_inference,[],[860,779,3])). % 261.37/261.40 cnf(865,plain, % 261.37/261.40 (E(f2(f2(f2(a1,a1),a1),f2(f2(a1,a1),a1)),f2(f2(f2(f2(a1,f2(a3,a1)),f2(a3,a3)),f2(a1,a1)),a1))), % 261.37/261.40 inference(scs_inference,[],[862,2])). % 261.37/261.40 cnf(866,plain, % 261.37/261.40 (~E(f2(f2(a1,a3),a3),f2(f2(f2(a3,f2(a1,a1)),a3),a3))), % 261.37/261.40 inference(scs_inference,[],[862,838,8,2,3])). % 261.37/261.40 cnf(869,plain, % 261.37/261.40 (E(f2(f2(f2(f2(a3,a1),f2(a3,a1)),f2(a1,a1)),a1),f2(f2(f2(f2(a1,f2(a3,a1)),f2(a3,a3)),f2(a1,a1)),a1))), % 261.37/261.40 inference(scs_inference,[],[851,865,3])). % 261.37/261.40 cnf(871,plain, % 261.37/261.40 (~E(f2(a1,a3),f2(f2(a3,f2(a1,a1)),a3))), % 261.37/261.40 inference(scs_inference,[],[866,851,865,3,2,4])). % 261.37/261.40 cnf(874,plain, % 261.37/261.40 (E(f2(f2(f2(f2(a3,a1),f2(a1,a1)),f2(a1,a1)),a1),f2(f2(f2(f2(a1,f2(a3,a1)),f2(a3,a3)),f2(a1,a1)),a1))), % 261.37/261.40 inference(scs_inference,[],[869,797,2,3])). % 261.37/261.40 cnf(877,plain, % 261.37/261.40 (~E(f2(a1,a3),f2(f2(f2(f2(a1,a3),a1),a1),a3))), % 261.37/261.40 inference(scs_inference,[],[871,874,25,2,3])). % 261.37/261.40 cnf(880,plain, % 261.37/261.40 (~E(f2(f2(f2(f2(a1,a3),a1),a1),a3),f2(a1,a3))), % 261.37/261.40 inference(scs_inference,[],[877,2])). % 261.37/261.40 cnf(881,plain, % 261.37/261.40 (E(f2(f2(f2(f2(a3,a1),f2(a3,a1)),f2(a1,a1)),a1),f2(a1,f2(f2(f2(a3,a1),f2(a1,a1)),a1)))), % 261.37/261.40 inference(scs_inference,[],[877,312,799,2,3])). % 261.37/261.40 cnf(883,plain, % 261.37/261.40 (E(f2(a1,f2(f2(f2(a3,a1),f2(a1,a1)),a1)),f2(f2(f2(f2(a3,a1),f2(a3,a1)),f2(a1,a1)),a1))), % 261.37/261.40 inference(scs_inference,[],[881,2])). % 261.37/261.40 cnf(884,plain, % 261.37/261.40 (E(f2(a1,f2(f2(f2(a1,a1),f2(a1,a1)),a1)),f2(f2(f2(f2(a3,a1),f2(a3,a3)),f2(a1,a1)),a1))), % 261.37/261.40 inference(scs_inference,[],[211,881,791,2,3])). % 261.37/261.40 cnf(885,plain, % 261.37/261.40 (~E(f2(f2(f2(a1,a3),a1),a1),a1)), % 261.37/261.40 inference(scs_inference,[],[211,880,881,791,2,3,4])). % 261.37/261.40 cnf(887,plain, % 261.37/261.40 (~E(a1,f2(f2(f2(a1,a3),a1),a1))), % 261.37/261.40 inference(scs_inference,[],[885,2])). % 261.37/261.40 cnf(891,plain, % 261.37/261.40 (~E(a1,f2(a3,f2(a1,a1)))), % 261.37/261.40 inference(scs_inference,[],[887,884,15,2,3])). % 261.37/261.40 cnf(894,plain, % 261.37/261.40 (E(f2(f2(f2(f2(a1,f2(a3,a3)),f2(a3,a1)),f2(a3,a1)),a1),f2(f2(f2(f2(a3,a1),f2(a3,a3)),f2(a3,a1)),a1))), % 261.37/261.40 inference(scs_inference,[],[891,416,715,2,3])). % 261.37/261.40 cnf(897,plain, % 261.37/261.40 (E(f2(f2(f2(f2(a3,a1),f2(a3,a3)),f2(a3,a1)),a1),f2(f2(f2(f2(a1,f2(a3,a3)),f2(a3,a1)),f2(a3,a1)),a1))), % 261.37/261.40 inference(scs_inference,[],[894,2])). % 261.37/261.40 cnf(907,plain, % 261.37/261.40 (E(f2(f2(f2(f2(a1,f2(a3,a1)),f2(a3,a3)),f2(a3,a1)),a1),f2(f2(f2(f2(a1,f2(a3,a3)),f2(a3,a1)),f2(a3,a1)),a1))), % 261.37/261.40 inference(scs_inference,[],[897,608,735,2,3])). % 261.37/261.40 cnf(910,plain, % 261.37/261.40 (~E(f2(f2(a3,a1),f2(f2(f2(a3,a1),f2(a3,a1)),f2(a3,a1))),f2(f2(a3,f2(a3,a1)),f2(a3,a1)))), % 261.37/261.40 inference(scs_inference,[],[907,691,39,2,3])). % 261.37/261.40 cnf(913,plain, % 261.37/261.40 (~E(f2(f2(a3,f2(a3,a1)),f2(a3,a1)),f2(f2(a3,a1),f2(f2(f2(a3,a1),f2(a3,a1)),f2(a3,a1))))), % 261.37/261.40 inference(scs_inference,[],[910,2])). % 261.37/261.40 cnf(918,plain, % 261.37/261.40 (~E(f2(f2(a3,a1),f2(f2(f2(a1,f2(a3,a1)),f2(a3,a1)),f2(f2(a3,a1),f2(a3,a1)))),f2(f2(f2(a3,a3),f2(a3,a1)),f2(a3,a1)))), % 261.37/261.40 inference(scs_inference,[],[378,2])). % 261.37/261.40 cnf(919,plain, % 261.37/261.40 (E(f2(f2(f2(f2(a1,f2(a3,a3)),f2(a3,a1)),f2(a3,a1)),a1),f2(f2(f2(f2(a1,f2(a1,a1)),f2(a3,a1)),f2(a3,a1)),a1))), % 261.37/261.40 inference(scs_inference,[],[727,378,894,2,3])). % 261.37/261.40 cnf(922,plain, % 261.37/261.40 (~E(f2(f2(f2(f2(a1,a3),a3),a1),f2(a3,a1)),f2(f2(a3,a1),f2(f2(f2(a3,a1),f2(a3,a1)),f2(a3,a1))))), % 261.37/261.40 inference(scs_inference,[],[913,919,46,2,3])). % 261.37/261.40 cnf(926,plain, % 261.37/261.40 (E(f2(a1,f2(f2(f2(a3,a1),f2(a1,a1)),a1)),f2(f2(f2(a1,a1),a1),f2(f2(a1,a1),a1)))), % 261.37/261.40 inference(scs_inference,[],[922,883,851,2,3])). % 261.37/261.40 cnf(929,plain, % 261.37/261.40 (E(f2(a1,f2(f2(f2(a3,a1),f2(a1,a1)),a1)),f2(f2(f2(f2(a3,a1),f2(a3,a3)),f2(a1,a1)),a1))), % 261.37/261.40 inference(scs_inference,[],[926,857,2,3])). % 261.37/261.40 cnf(936,plain, % 261.37/261.40 (E(f2(f2(f2(a3,a1),f2(f2(a1,f2(a3,a1)),f2(a3,a1))),f2(a3,a1)),f2(f2(f2(a3,f2(a3,a1)),f2(a3,a1)),f2(a3,a1)))), % 261.37/261.40 inference(scs_inference,[],[213,929,615,2,3])). % 261.37/261.40 cnf(940,plain, % 261.37/261.40 (E(f2(f2(f2(f2(a3,a1),f2(a1,f2(a3,a1))),f2(a3,a1)),f2(a3,a1)),f2(f2(f2(a3,f2(a3,a1)),f2(a3,a1)),f2(a3,a1)))), % 261.37/261.40 inference(scs_inference,[],[936,52,2,3])). % 261.37/261.40 cnf(947,plain, % 261.37/261.40 (E(f2(f2(f2(a3,f2(a3,a1)),f2(a3,a1)),f2(a3,a1)),f2(f2(f2(f2(a3,a1),f2(a1,f2(a3,a1))),f2(a3,a1)),f2(a3,a1)))), % 261.37/261.40 inference(scs_inference,[],[940,2])). % 261.37/261.40 cnf(1005,plain, % 261.37/261.40 (E(f4(f2(f2(a3,a1),f2(f2(a3,a1),f2(f2(a3,a1),f2(a3,a1))))),f4(f2(f2(f2(a3,a3),f2(a3,a1)),f2(a3,a1))))), % 261.37/261.40 inference(scs_inference,[],[219,918,386,2,3,4,6])). % 261.37/261.40 cnf(1060,plain, % 261.37/261.40 (~E(f2(f2(a3,a1),f2(x10601,f2(a3,a1))),f2(f2(f2(a3,a1),f2(f2(a3,a1),x10601)),f2(a3,a1)))), % 261.37/261.40 inference(scs_inference,[],[11,23,309,701,5,2,6,4,3])). % 261.37/261.40 cnf(1152,plain, % 261.37/261.40 (~E(f2(f2(f2(x11521,x11522),x11523),x11522),f2(f2(a3,a1),f2(f2(f2(a3,x11521),x11523),x11522)))), % 261.37/261.40 inference(scs_inference,[],[8,235,45,313,2,5,4,6,3])). % 261.37/261.40 cnf(1176,plain, % 261.37/261.40 (~E(f2(f2(f2(f2(a3,a1),f2(a3,a3)),f2(a3,a1)),f2(a3,a1)),f2(f2(f2(a3,f2(a3,a1)),f2(a3,a1)),f2(a3,a1)))), % 261.37/261.40 inference(scs_inference,[],[704,2])). % 261.37/261.40 cnf(1778,plain, % 261.37/261.40 (~E(f2(f2(a3,a1),f2(x17781,f2(a3,a1))),f2(f2(f2(a1,f2(a3,a1)),f2(f2(a3,a1),x17781)),f2(a3,a1)))), % 261.37/261.40 inference(scs_inference,[],[10,1060,3])). % 261.37/261.40 cnf(1820,plain, % 261.37/261.40 (~E(f2(f2(f2(f2(a3,a1),f2(a3,a3)),f2(a3,a1)),f2(a3,a1)),f2(f2(f2(f2(a3,a1),f2(a1,f2(a3,a1))),f2(a3,a1)),f2(a3,a1)))), % 261.37/261.40 inference(scs_inference,[],[1176,940,3])). % 261.37/261.40 cnf(1891,plain, % 261.37/261.40 (~E(f2(f2(f2(f2(a3,a1),f2(a1,f2(a3,a1))),f2(a3,a1)),f2(a3,a1)),f2(f2(f2(f2(a3,a1),f2(a3,f2(a3,a1))),f2(a3,a1)),f2(a3,a1)))), % 261.37/261.40 inference(scs_inference,[],[947,382,1778,2,3])). % 261.37/261.40 cnf(1898,plain, % 261.37/261.40 (~E(f2(f2(f2(f2(a3,a1),f2(a1,f2(a3,a1))),f2(a3,a1)),f2(a3,a1)),f2(f2(f2(f2(a3,a1),f2(a3,a3)),f2(a3,a1)),f2(a3,a1)))), % 261.37/261.40 inference(scs_inference,[],[1820,2])). % 261.37/261.40 cnf(2030,plain, % 261.37/261.40 (E(f4(f2(f2(f2(a3,a3),f2(f2(a1,a1),f2(a1,a1))),a1)),f4(f2(f2(f2(f2(a3,a1),f2(a3,a1)),f2(a1,a1)),a1)))), % 261.37/261.40 inference(scs_inference,[],[203,4,5,6])). % 261.37/261.40 cnf(2097,plain, % 261.37/261.40 (E(f4(f2(x20971,f2(x20971,f2(f2(a3,a1),x20971)))),f4(f2(f2(f2(f2(a3,a1),f2(a3,a1)),f2(a3,a1)),x20971)))), % 261.37/261.40 inference(scs_inference,[],[152,4,5,6])). % 261.37/261.40 cnf(2139,plain, % 261.37/261.40 (E(f4(f2(f2(f2(a1,a1),f2(f2(a3,a1),f2(a3,a1))),a1)),f4(f2(f2(f2(f2(a3,a1),f2(a3,a1)),f2(a3,a1)),a1)))), % 261.37/261.40 inference(scs_inference,[],[134,4,5,6])). % 261.37/261.40 cnf(2231,plain, % 261.37/261.40 (~E(f2(f2(f2(a3,a1),f2(a1,f2(a3,a1))),f2(a3,a1)),f2(f2(f2(a3,a1),f2(a3,a3)),f2(a3,a1)))), % 261.37/261.40 inference(scs_inference,[],[1898,2030,2,4])). % 261.37/261.40 cnf(2251,plain, % 261.37/261.40 (~E(f2(a1,f2(a3,a1)),f2(a3,a3))), % 261.37/261.40 inference(scs_inference,[],[2231,1005,2097,253,2,4,3,5])). % 261.37/261.40 cnf(2312,plain, % 261.37/261.40 (~E(f2(f2(f2(a3,a1),a3),a1),f2(a3,a3))), % 261.37/261.40 inference(scs_inference,[],[2251,2139,1891,14,2,4,3])). % 261.37/261.40 cnf(2454,plain, % 261.37/261.40 ($false), % 261.37/261.40 inference(scs_inference,[],[7,25,2312,1152,2,3]), % 261.37/261.40 ['proof']). % 261.37/261.40 % SZS output end Proof % 261.37/261.40 % Total time :260.550000s %------------------------------------------------------------------------------