%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : COL060-2 : TPTP v8.2.0. Bugfixed v1.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n022.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:58 EDT 2024 % Result : Unsatisfiable 67.66s 67.72s % Output : CNFRefutation 67.68s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : COL060-2 : TPTP v8.2.0. Bugfixed v1.2.0. % 0.12/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n022.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Tue Jun 18 16:08:54 EDT 2024 % 0.12/0.33 % CPUTime : % 0.55/0.58 start to proof:theBenchmark % 67.62/67.71 %------------------------------------------- % 67.62/67.71 % File :CSE---1.7 % 67.62/67.71 % Problem :theBenchmark % 67.62/67.71 % Transform :cnf % 67.62/67.71 % Format :tptp:raw % 67.62/67.71 % Command :java -jar mcs_scs.jar %d %s % 67.62/67.71 % 67.62/67.71 % Result :Theorem 67.070000s % 67.62/67.71 % Output :CNFRefutation 67.070000s % 67.62/67.71 %------------------------------------------- % 67.66/67.72 %-------------------------------------------------------------------------- % 67.66/67.72 % File : COL060-2 : TPTP v8.2.0. Bugfixed v1.2.0. % 67.66/67.72 % Domain : Combinatory Logic % 67.66/67.72 % Problem : Find combinator equivalent to Q from B and T % 67.66/67.72 % Version : [WM88] (equality) axioms. % 67.66/67.72 % Theorem formulation : The combinator is provided and checked. % 67.66/67.72 % English : Construct from B and T alone a combinator that behaves as the % 67.66/67.72 % combinator Q does, where ((Bx)y)z = x(yz), (Tx)y = yx, % 67.66/67.72 % ((Qx)y)z = y(xz). % 67.66/67.72 % 67.66/67.72 % Refs : [WM88] Wos & McCune (1988), Challenge Problems Focusing on Eq % 67.66/67.72 % : [WW+90] Wos et al. (1990), Automated Reasoning Contributes to % 67.66/67.72 % Source : [TPTP] % 67.66/67.72 % Names : % 67.66/67.72 % 67.66/67.72 % Status : Unsatisfiable % 67.66/67.72 % Rating : 0.00 v8.2.0, 0.08 v8.1.0, 0.10 v7.5.0, 0.08 v7.4.0, 0.13 v7.3.0, 0.05 v7.1.0, 0.00 v7.0.0, 0.05 v6.4.0, 0.11 v6.3.0, 0.06 v6.2.0, 0.07 v6.1.0, 0.00 v6.0.0, 0.05 v5.4.0, 0.00 v5.0.0, 0.07 v4.1.0, 0.09 v4.0.1, 0.07 v4.0.0, 0.08 v3.7.0, 0.11 v3.4.0, 0.12 v3.3.0, 0.00 v2.1.0, 0.29 v2.0.0 % 67.66/67.72 % Syntax : Number of clauses : 3 ( 3 unt; 0 nHn; 1 RR) % 67.66/67.72 % Number of literals : 3 ( 3 equ; 1 neg) % 67.66/67.72 % Maximal clause size : 1 ( 1 avg) % 67.66/67.72 % Maximal term depth : 7 ( 2 avg) % 67.66/67.72 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty) % 67.66/67.72 % Number of functors : 6 ( 6 usr; 5 con; 0-2 aty) % 67.66/67.72 % Number of variables : 5 ( 0 sgn) % 67.66/67.72 % SPC : CNF_UNS_RFO_PEQ_UEQ % 67.66/67.72 % 67.66/67.72 % Comments : % 67.66/67.72 % Bugfixes : v1.2.0 : Redundant [fgh]_substitution axioms removed. % 67.66/67.72 %-------------------------------------------------------------------------- % 67.66/67.72 cnf(b_definition,axiom, % 67.66/67.72 apply(apply(apply(b,X),Y),Z) = apply(X,apply(Y,Z)) ). % 67.66/67.72 % 67.66/67.72 cnf(t_definition,axiom, % 67.66/67.72 apply(apply(t,X),Y) = apply(Y,X) ). % 67.66/67.72 % 67.66/67.72 %----This is the q equivalent % 67.66/67.72 cnf(prove_q_combinator,negated_conjecture, % 67.66/67.72 apply(apply(apply(apply(apply(b,apply(t,b)),apply(apply(b,b),t)),x),y),z) != apply(y,apply(x,z)) ). % 67.66/67.72 % 67.66/67.72 %-------------------------------------------------------------------------- % 67.66/67.72 %------------------------------------------- % 67.66/67.72 % Proof found % 67.66/67.72 % SZS status Theorem for theBenchmark % 67.66/67.72 % SZS output start Proof % 67.66/67.73 %ClaNum:8(EqnAxiom:5) % 67.66/67.73 %VarNum:10(SingletonVarNum:5) % 67.66/67.73 %MaxLitNum:1 % 67.66/67.73 %MaxfuncDepth:6 % 67.66/67.73 %SharedTerms:16 % 67.66/67.73 %goalClause: 8 % 67.66/67.73 %singleGoalClaCount:1 % 67.66/67.73 [8]~E(f2(f2(f2(f2(f2(a3,f2(a1,a3)),f2(f2(a3,a3),a1)),a4),a5),a6),f2(a5,f2(a4,a6))) % 67.66/67.73 [6]E(f2(f2(a1,x61),x62),f2(x62,x61)) % 67.66/67.73 [7]E(f2(f2(f2(a3,x71),x72),x73),f2(x71,f2(x72,x73))) % 67.66/67.73 %EqnAxiom % 67.66/67.73 [1]E(x11,x11) % 67.66/67.73 [2]E(x22,x21)+~E(x21,x22) % 67.66/67.73 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 67.66/67.73 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43)) % 67.66/67.73 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52)) % 67.66/67.73 % 67.66/67.73 %------------------------------------------- % 67.68/67.74 cnf(9,plain, % 67.68/67.74 (E(f2(x91,x92),f2(f2(a1,x92),x91))), % 67.68/67.74 inference(scs_inference,[],[6,2])). % 67.68/67.74 cnf(10,plain, % 67.68/67.74 (E(f2(x101,f2(x102,x103)),f2(f2(f2(a3,x101),x102),x103))), % 67.68/67.74 inference(scs_inference,[],[7,2])). % 67.68/67.74 cnf(11,plain, % 67.68/67.74 (E(f2(f2(f2(a3,x111),x112),x113),f2(f2(a1,f2(x112,x113)),x111))), % 67.68/67.74 inference(scs_inference,[],[9,7,2,3])). % 67.68/67.74 cnf(13,plain, % 67.68/67.74 (E(f2(f2(a1,f2(x131,x132)),x133),f2(f2(f2(a3,x133),x131),x132))), % 67.68/67.74 inference(scs_inference,[],[11,2])). % 67.68/67.74 cnf(14,plain, % 67.68/67.74 (E(f2(f2(x141,x142),x143),f2(f2(f2(a3,f2(a1,x143)),x141),x142))), % 67.68/67.74 inference(scs_inference,[],[10,9,11,2,3])). % 67.68/67.74 cnf(17,plain, % 67.68/67.74 (E(f2(f2(f2(a3,f2(a1,x171)),x172),x173),f2(f2(x172,x173),x171))), % 67.68/67.74 inference(scs_inference,[],[14,2])). % 67.68/67.74 cnf(18,plain, % 67.68/67.74 (E(f2(f2(a1,f2(x181,f2(x182,x183))),x184),f2(f2(f2(a3,f2(f2(a3,x184),x181)),x182),x183))), % 67.68/67.74 inference(scs_inference,[],[13,10,14,2,3])). % 67.68/67.74 cnf(21,plain, % 67.68/67.74 (E(f2(f2(f2(a3,f2(f2(a3,x211),x212)),x213),x214),f2(f2(a1,f2(x212,f2(x213,x214))),x211))), % 67.68/67.74 inference(scs_inference,[],[18,2])). % 67.68/67.74 cnf(22,plain, % 67.68/67.74 (E(f2(f2(a1,f2(x221,x222)),f2(a1,x223)),f2(f2(x221,x222),x223))), % 67.68/67.74 inference(scs_inference,[],[17,13,18,2,3])). % 67.68/67.74 cnf(25,plain, % 67.68/67.74 (E(f2(f2(x251,x252),x253),f2(f2(a1,f2(x251,x252)),f2(a1,x253)))), % 67.68/67.74 inference(scs_inference,[],[22,2])). % 67.68/67.74 cnf(26,plain, % 67.68/67.74 (E(f2(f2(f2(a3,f2(a1,x261)),f2(a3,f2(f2(a3,x262),x263))),x264),f2(f2(a1,f2(x263,f2(x264,x261))),x262))), % 67.68/67.74 inference(scs_inference,[],[21,17,22,2,3])). % 67.68/67.74 cnf(29,plain, % 67.68/67.74 (E(f2(f2(a1,f2(x291,f2(x292,x293))),x294),f2(f2(f2(a3,f2(a1,x293)),f2(a3,f2(f2(a3,x294),x291))),x292))), % 67.68/67.74 inference(scs_inference,[],[26,2])). % 67.68/67.74 cnf(30,plain, % 67.68/67.74 (E(f2(f2(f2(a3,f2(f2(a3,x301),x302)),x303),x304),f2(f2(a1,f2(a1,f2(x302,f2(x303,x304)))),f2(a1,x301)))), % 67.68/67.74 inference(scs_inference,[],[25,21,26,2,3])). % 67.68/67.74 cnf(32,plain, % 67.68/67.74 (E(f2(f2(a1,f2(a1,f2(x321,f2(x322,x323)))),f2(a1,x324)),f2(f2(f2(a3,f2(f2(a3,x324),x321)),x322),x323))), % 67.68/67.74 inference(scs_inference,[],[30,2])). % 67.68/67.74 cnf(33,plain, % 67.68/67.74 (E(f2(f2(a1,f2(x331,f2(x332,x333))),x334),f2(f2(a1,f2(f2(a3,f2(a1,x333)),f2(a3,f2(f2(a3,x334),x331)))),f2(a1,x332)))), % 67.68/67.74 inference(scs_inference,[],[29,25,30,2,3])). % 67.68/67.74 cnf(35,plain, % 67.68/67.74 (E(f2(f2(a1,f2(f2(a3,f2(a1,x351)),f2(a3,f2(f2(a3,x352),x353)))),f2(a1,x354)),f2(f2(a1,f2(x353,f2(x354,x351))),x352))), % 67.68/67.74 inference(scs_inference,[],[33,2])). % 67.68/67.74 cnf(36,plain, % 67.68/67.74 (E(f2(f2(f2(a3,f2(a1,x361)),a1),f2(x362,f2(x363,x364))),f2(f2(f2(a3,f2(a1,x364)),f2(a3,f2(f2(a3,x361),x362))),x363))), % 67.68/67.74 inference(scs_inference,[],[29,17,33,2,3])). % 67.68/67.74 cnf(39,plain, % 67.68/67.74 (E(f2(f2(f2(a3,f2(a1,x391)),f2(a3,f2(f2(a3,x392),x393))),x394),f2(f2(f2(a3,f2(a1,x392)),a1),f2(x393,f2(x394,x391))))), % 67.68/67.74 inference(scs_inference,[],[36,2])). % 67.68/67.74 cnf(40,plain, % 67.68/67.74 (E(f2(f2(a1,x401),f2(f2(a3,f2(a1,x402)),f2(a3,f2(f2(a3,x403),x404)))),f2(f2(a1,f2(x404,f2(x401,x402))),x403))), % 67.68/67.74 inference(scs_inference,[],[35,9,36,2,3])). % 67.68/67.74 cnf(42,plain, % 67.68/67.74 (E(f2(f2(a1,f2(x421,f2(x422,x423))),x424),f2(f2(a1,x422),f2(f2(a3,f2(a1,x423)),f2(a3,f2(f2(a3,x424),x421)))))), % 67.68/67.74 inference(scs_inference,[],[40,2])). % 67.68/67.74 cnf(43,plain, % 67.68/67.74 (E(f2(f2(a1,x431),f2(f2(a3,f2(f2(a3,x432),x433)),x434)),f2(f2(f2(a3,f2(a1,x432)),a1),f2(x433,f2(x434,x431))))), % 67.68/67.74 inference(scs_inference,[],[39,10,40,2,3])). % 67.68/67.74 cnf(46,plain, % 67.68/67.74 (E(f2(f2(f2(a3,f2(a1,x461)),a1),f2(x462,f2(x463,x464))),f2(f2(a1,x464),f2(f2(a3,f2(f2(a3,x461),x462)),x463)))), % 67.68/67.74 inference(scs_inference,[],[43,2])). % 67.68/67.74 cnf(47,plain, % 67.68/67.74 (E(f2(f2(a1,f2(f2(a3,f2(f2(a3,x471),x472)),x473)),f2(a1,x474)),f2(f2(f2(a3,f2(a1,x471)),a1),f2(x472,f2(x473,x474))))), % 67.68/67.74 inference(scs_inference,[],[39,13,43,2,3])). % 67.68/67.74 cnf(50,plain, % 67.68/67.74 (E(f2(f2(f2(a3,f2(a1,x501)),a1),f2(x502,f2(x503,x504))),f2(f2(a1,f2(f2(a3,f2(f2(a3,x501),x502)),x503)),f2(a1,x504)))), % 67.68/67.74 inference(scs_inference,[],[47,2])). % 67.68/67.74 cnf(51,plain, % 67.68/67.74 (E(f2(f2(a1,f2(a1,f2(x511,f2(x512,x513)))),f2(a1,x514)),f2(f2(a1,f2(f2(a3,f2(f2(a3,x514),x511)),x512)),f2(a1,x513)))), % 67.68/67.74 inference(scs_inference,[],[32,25,47,2,3])). % 67.68/67.74 cnf(53,plain, % 67.68/67.74 (E(f2(f2(a1,f2(f2(a3,f2(f2(a3,x531),x532)),x533)),f2(a1,x534)),f2(f2(a1,f2(a1,f2(x532,f2(x533,x534)))),f2(a1,x531)))), % 67.68/67.74 inference(scs_inference,[],[51,2])). % 67.68/67.74 cnf(54,plain, % 67.68/67.74 (E(f2(f2(a1,f2(x541,f2(x542,x543))),x544),f2(f2(f2(a3,f2(a1,x542)),f2(a3,f2(a1,x543))),f2(a3,f2(f2(a3,x544),x541))))), % 67.68/67.74 inference(scs_inference,[],[42,10,51,2,3])). % 67.68/67.74 cnf(56,plain, % 67.68/67.74 (E(f2(f2(f2(a3,f2(a1,x561)),f2(a3,f2(a1,x562))),f2(a3,f2(f2(a3,x563),x564))),f2(f2(a1,f2(x564,f2(x561,x562))),x563))), % 67.68/67.74 inference(scs_inference,[],[54,2])). % 67.68/67.74 cnf(57,plain, % 67.68/67.74 (E(f2(f2(a1,f2(a1,f2(x571,f2(x572,x573)))),f2(a1,x574)),f2(f2(a1,f2(x572,x573)),f2(f2(a3,x574),x571)))), % 67.68/67.74 inference(scs_inference,[],[32,54,11,2,3])). % 67.68/67.74 cnf(59,plain, % 67.68/67.74 (E(f2(f2(a1,f2(x591,x592)),f2(f2(a3,x593),x594)),f2(f2(a1,f2(a1,f2(x594,f2(x591,x592)))),f2(a1,x593)))), % 67.68/67.74 inference(scs_inference,[],[57,2])). % 67.68/67.74 cnf(60,plain, % 67.68/67.74 (E(f2(f2(f2(a3,f2(a1,x601)),f2(a3,f2(a1,x602))),f2(a3,f2(f2(a3,f2(a1,x603)),x604))),f2(f2(x604,f2(x601,x602)),x603))), % 67.68/67.74 inference(scs_inference,[],[56,57,22,2,3])). % 67.68/67.74 cnf(63,plain, % 67.68/67.74 (E(f2(f2(x631,f2(x632,x633)),x634),f2(f2(f2(a3,f2(a1,x632)),f2(a3,f2(a1,x633))),f2(a3,f2(f2(a3,f2(a1,x634)),x631))))), % 67.68/67.74 inference(scs_inference,[],[60,2])). % 67.68/67.74 cnf(64,plain, % 67.68/67.74 (E(f2(f2(a1,f2(x641,x642)),f2(f2(a3,x643),x644)),f2(f2(a1,f2(f2(a3,f2(f2(a3,x643),x644)),x641)),f2(a1,x642)))), % 67.68/67.74 inference(scs_inference,[],[59,60,51,2,3])). % 67.68/67.74 cnf(66,plain, % 67.68/67.74 (E(f2(f2(a1,f2(f2(a3,f2(f2(a3,x661),x662)),x663)),f2(a1,x664)),f2(f2(a1,f2(x663,x664)),f2(f2(a3,x661),x662)))), % 67.68/67.74 inference(scs_inference,[],[64,2])). % 67.68/67.74 cnf(67,plain, % 67.68/67.74 (E(f2(f2(f2(a3,f2(a1,x671)),a1),f2(x672,f2(x673,x674))),f2(f2(f2(a3,f2(f2(a3,x671),x672)),x673),x674))), % 67.68/67.74 inference(scs_inference,[],[50,64,22,2,3])). % 67.68/67.74 cnf(69,plain, % 67.68/67.74 (E(f2(f2(f2(a3,f2(f2(a3,x691),x692)),x693),x694),f2(f2(f2(a3,f2(a1,x691)),a1),f2(x692,f2(x693,x694))))), % 67.68/67.74 inference(scs_inference,[],[67,2])). % 67.68/67.74 cnf(70,plain, % 67.68/67.74 (E(f2(f2(a1,f2(f2(a3,f2(f2(a3,x701),x702)),x703)),f2(a1,x704)),f2(f2(a1,f2(x702,f2(x703,x704))),x701))), % 67.68/67.74 inference(scs_inference,[],[53,67,22,2,3])). % 67.68/67.74 cnf(72,plain, % 67.68/67.74 (E(f2(f2(a1,f2(x721,f2(x722,x723))),x724),f2(f2(a1,f2(f2(a3,f2(f2(a3,x724),x721)),x722)),f2(a1,x723)))), % 67.68/67.74 inference(scs_inference,[],[70,2])). % 67.68/67.74 cnf(75,plain, % 67.68/67.74 (E(f2(f2(a1,f2(x751,x752)),f2(f2(a3,x753),x754)),f2(f2(a1,f2(x754,f2(x751,x752))),x753))), % 67.68/67.74 inference(scs_inference,[],[72,66,3,2])). % 67.68/67.74 cnf(76,plain, % 67.68/67.74 (E(f2(f2(f2(a3,f2(a1,x761)),a1),f2(x762,f2(x763,f2(x764,x765)))),f2(f2(a1,f2(x763,f2(x764,x765))),f2(f2(a3,x761),x762)))), % 67.68/67.74 inference(scs_inference,[],[75,46,3])). % 67.68/67.74 cnf(80,plain, % 67.68/67.74 (E(f2(f2(a1,f2(x801,x802)),f2(f2(a3,x803),x804)),f2(f2(a1,x801),f2(f2(a3,f2(a1,x802)),f2(a3,f2(f2(a3,x803),x804)))))), % 67.68/67.74 inference(scs_inference,[],[75,42,3])). % 67.68/67.74 cnf(82,plain, % 67.68/67.74 (E(f2(f2(a1,x821),f2(f2(a3,f2(a1,x822)),f2(a3,f2(f2(a3,x823),x824)))),f2(f2(a1,f2(x821,x822)),f2(f2(a3,x823),x824)))), % 67.68/67.74 inference(scs_inference,[],[75,42,3,2])). % 67.68/67.74 cnf(86,plain, % 67.68/67.74 (E(f2(f2(a1,x861),f2(x862,f2(x863,x864))),f2(f2(f2(a3,f2(a1,x863)),f2(a3,f2(a1,x864))),f2(a3,f2(f2(a3,f2(a1,x861)),x862))))), % 67.68/67.74 inference(scs_inference,[],[6,63,3])). % 67.68/67.74 cnf(93,plain, % 67.68/67.74 (E(f2(f2(a1,f2(f2(a3,f2(a1,x931)),f2(a3,f2(f2(a3,x932),x933)))),f2(a1,x934)),f2(f2(a1,f2(x934,x931)),f2(f2(a3,x932),x933)))), % 67.68/67.74 inference(scs_inference,[],[6,82,3])). % 67.68/67.74 cnf(95,plain, % 67.68/67.74 (E(f2(f2(a1,f2(x951,x952)),f2(f2(a3,x953),x954)),f2(f2(a1,f2(f2(a3,f2(a1,x952)),f2(a3,f2(f2(a3,x953),x954)))),f2(a1,x951)))), % 67.68/67.74 inference(scs_inference,[],[93,2])). % 67.68/67.74 cnf(96,plain, % 67.68/67.74 (E(f2(f2(a1,x961),f2(a1,f2(x962,f2(x963,x964)))),f2(f2(a1,f2(f2(a3,f2(f2(a3,x961),x962)),x963)),f2(a1,x964)))), % 67.68/67.74 inference(scs_inference,[],[6,72,93,2,3])). % 67.68/67.74 cnf(100,plain, % 67.68/67.74 (E(f2(f2(a1,f2(f2(a3,x1001),x1002)),f2(a1,f2(x1003,x1004))),f2(f2(a1,f2(f2(a3,f2(a1,x1004)),f2(a3,f2(f2(a3,x1001),x1002)))),f2(a1,x1003)))), % 67.68/67.74 inference(scs_inference,[],[6,95,96,2,3])). % 67.68/67.74 cnf(103,plain, % 67.68/67.74 (E(f2(f2(a1,x1031),f2(f2(a3,f2(f2(a3,x1032),x1033)),x1034)),f2(f2(a1,f2(x1033,f2(x1034,x1031))),x1032))), % 67.68/67.74 inference(scs_inference,[],[6,21,100,2,3])). % 67.68/67.74 cnf(106,plain, % 67.68/67.74 (E(f2(f2(a1,f2(x1061,f2(x1062,x1063))),x1064),f2(f2(a1,x1063),f2(f2(a3,f2(f2(a3,x1064),x1061)),x1062)))), % 67.68/67.74 inference(scs_inference,[],[103,2])). % 67.68/67.74 cnf(107,plain, % 67.68/67.74 (E(f2(f2(a1,x1071),f2(a1,f2(x1072,f2(x1073,x1074)))),f2(f2(f2(a3,f2(a1,x1074)),f2(a3,f2(f2(a3,x1071),x1072))),x1073))), % 67.68/67.74 inference(scs_inference,[],[6,29,103,2,3])). % 67.68/67.74 cnf(110,plain, % 67.68/67.74 (E(f2(f2(f2(a3,f2(a1,x1101)),f2(a3,f2(f2(a3,x1102),x1103))),x1104),f2(f2(a1,x1102),f2(a1,f2(x1103,f2(x1104,x1101)))))), % 67.68/67.74 inference(scs_inference,[],[107,2])). % 67.68/67.74 cnf(111,plain, % 67.68/67.74 (E(f2(f2(a1,x1111),f2(a1,f2(x1112,f2(x1113,x1114)))),f2(f2(a1,x1114),f2(f2(a3,f2(f2(a3,x1111),x1112)),x1113)))), % 67.68/67.74 inference(scs_inference,[],[6,106,107,2,3])). % 67.68/67.74 cnf(115,plain, % 67.68/67.74 (E(f2(f2(a1,x1151),f2(f2(a3,f2(a1,x1152)),f2(a3,f2(f2(a3,x1153),x1154)))),f2(f2(a1,x1153),f2(a1,f2(x1154,f2(x1151,x1152)))))), % 67.68/67.74 inference(scs_inference,[],[6,110,111,2,3])). % 67.68/67.74 cnf(119,plain, % 67.68/67.74 (E(f2(f2(a1,x1191),f2(f2(a3,f2(a1,x1192)),f2(a3,f2(f2(a3,x1193),x1194)))),f2(f2(f2(a3,f2(a1,x1193)),a1),f2(x1194,f2(x1191,x1192))))), % 67.68/67.74 inference(scs_inference,[],[6,39,115,2,3])). % 67.68/67.74 cnf(123,plain, % 67.68/67.74 (E(f2(f2(a1,f2(f2(a3,x1231),x1232)),f2(a1,f2(x1233,x1234))),f2(f2(a1,f2(x1232,f2(x1233,x1234))),x1231))), % 67.68/67.74 inference(scs_inference,[],[6,75,119,2,3])). % 67.68/67.74 cnf(125,plain, % 67.68/67.74 (E(f2(f2(a1,f2(x1251,f2(x1252,x1253))),x1254),f2(f2(a1,f2(f2(a3,x1254),x1251)),f2(a1,f2(x1252,x1253))))), % 67.68/67.74 inference(scs_inference,[],[123,2])). % 67.68/67.74 cnf(126,plain, % 67.68/67.74 (E(f2(f2(a1,f2(f2(a3,x1261),x1262)),f2(a1,f2(x1263,x1264))),f2(f2(a1,f2(a1,f2(x1262,f2(x1263,x1264)))),f2(a1,x1261)))), % 67.68/67.74 inference(scs_inference,[],[6,59,123,2,3])). % 67.68/67.74 cnf(128,plain, % 67.68/67.74 (E(f2(f2(a1,f2(a1,f2(x1281,f2(x1282,x1283)))),f2(a1,x1284)),f2(f2(a1,f2(f2(a3,x1284),x1281)),f2(a1,f2(x1282,x1283))))), % 67.68/67.74 inference(scs_inference,[],[126,2])). % 67.68/67.74 cnf(129,plain, % 67.68/67.74 (E(f2(f2(a1,x1291),f2(a1,f2(x1292,f2(x1293,x1294)))),f2(f2(a1,f2(f2(a3,x1291),x1292)),f2(a1,f2(x1293,x1294))))), % 67.68/67.74 inference(scs_inference,[],[6,125,126,2,3])). % 67.68/67.74 cnf(132,plain, % 67.68/67.74 (E(f2(f2(a1,f2(f2(a3,x1321),x1322)),f2(a1,f2(x1323,x1324))),f2(f2(a1,x1321),f2(a1,f2(x1322,f2(x1323,x1324)))))), % 67.68/67.74 inference(scs_inference,[],[129,2])). % 67.68/67.75 cnf(133,plain, % 67.68/67.75 (E(f2(f2(a1,f2(a1,x1331)),f2(a1,f2(a1,f2(x1332,f2(x1333,x1334))))),f2(f2(a1,f2(f2(a3,x1331),x1332)),f2(a1,f2(x1333,x1334))))), % 67.68/67.75 inference(scs_inference,[],[6,128,129,2,3])). % 67.68/67.75 cnf(136,plain, % 67.68/67.75 (E(f2(f2(a1,f2(a1,f2(x1361,x1362))),f2(a1,f2(f2(a3,x1363),x1364))),f2(f2(a1,x1363),f2(a1,f2(x1364,f2(x1361,x1362)))))), % 67.68/67.75 inference(scs_inference,[],[6,132,133,2,3])). % 67.68/67.75 cnf(138,plain, % 67.68/67.75 (E(f2(f2(a1,x1381),f2(a1,f2(x1382,f2(x1383,x1384)))),f2(f2(a1,f2(a1,f2(x1383,x1384))),f2(a1,f2(f2(a3,x1381),x1382))))), % 67.68/67.75 inference(scs_inference,[],[136,2])). % 67.68/67.75 cnf(139,plain, % 67.68/67.75 (E(f2(f2(a1,x1391),f2(f2(a3,f2(a1,x1392)),x1393)),f2(f2(x1393,x1391),x1392))), % 67.68/67.75 inference(scs_inference,[],[6,17,136,2,3])). % 67.68/67.75 cnf(142,plain, % 67.68/67.75 (E(f2(f2(x1421,x1422),x1423),f2(f2(a1,x1422),f2(f2(a3,f2(a1,x1423)),x1421)))), % 67.68/67.75 inference(scs_inference,[],[139,2])). % 67.68/67.75 cnf(143,plain, % 67.68/67.75 (E(f2(f2(a1,f2(a1,f2(x1431,f2(x1432,x1433)))),f2(a1,x1434)),f2(f2(a1,f2(a1,f2(x1432,x1433))),f2(a1,f2(f2(a3,x1434),x1431))))), % 67.68/67.75 inference(scs_inference,[],[6,138,139,2,3])). % 67.68/67.75 cnf(146,plain, % 67.68/67.75 (E(f2(f2(a1,x1461),f2(x1462,x1463)),f2(f2(a1,x1463),f2(f2(a3,f2(a1,x1461)),x1462)))), % 67.68/67.75 inference(scs_inference,[],[6,142,143,2,3])). % 67.68/67.75 cnf(149,plain, % 67.68/67.75 (E(f2(f2(a1,x1491),f2(f2(a3,f2(a1,x1492)),x1493)),f2(f2(a1,x1492),f2(x1493,x1491)))), % 67.68/67.75 inference(scs_inference,[],[146,2])). % 67.68/67.75 cnf(150,plain, % 67.68/67.75 (E(f2(f2(a1,x1501),f2(a1,f2(x1502,x1503))),f2(f2(f2(a3,x1501),x1502),x1503))), % 67.68/67.75 inference(scs_inference,[],[6,13,146,2,3])). % 67.68/67.75 cnf(153,plain, % 67.68/67.75 (E(f2(f2(f2(a3,x1531),x1532),x1533),f2(f2(a1,x1531),f2(a1,f2(x1532,x1533))))), % 67.68/67.75 inference(scs_inference,[],[150,2])). % 67.68/67.75 cnf(154,plain, % 67.68/67.75 (E(f2(f2(a1,f2(f2(a3,f2(a1,x1541)),x1542)),f2(a1,x1543)),f2(f2(a1,x1541),f2(x1542,x1543)))), % 67.68/67.75 inference(scs_inference,[],[6,149,150,2,3])). % 67.68/67.75 cnf(156,plain, % 67.68/67.75 (E(f2(f2(a1,x1561),f2(x1562,x1563)),f2(f2(a1,f2(f2(a3,f2(a1,x1561)),x1562)),f2(a1,x1563)))), % 67.68/67.75 inference(scs_inference,[],[154,2])). % 67.68/67.75 cnf(157,plain, % 67.68/67.75 (E(f2(f2(a1,x1571),f2(f2(a3,x1572),x1573)),f2(f2(a1,x1572),f2(a1,f2(x1573,x1571))))), % 67.68/67.75 inference(scs_inference,[],[6,153,154,2,3])). % 67.68/67.75 cnf(160,plain, % 67.68/67.75 (E(f2(f2(a1,x1601),f2(a1,f2(x1602,x1603))),f2(f2(a1,x1603),f2(f2(a3,x1601),x1602)))), % 67.68/67.75 inference(scs_inference,[],[157,2])). % 67.68/67.75 cnf(161,plain, % 67.68/67.75 (E(f2(f2(a1,f2(x1611,x1612)),f2(a1,x1613)),f2(f2(a1,f2(f2(a3,f2(a1,x1613)),x1611)),f2(a1,x1612)))), % 67.68/67.75 inference(scs_inference,[],[6,156,157,2,3])). % 67.68/67.75 cnf(163,plain, % 67.68/67.75 (E(f2(f2(a1,f2(f2(a3,f2(a1,x1631)),x1632)),f2(a1,x1633)),f2(f2(a1,f2(x1632,x1633)),f2(a1,x1631)))), % 67.68/67.75 inference(scs_inference,[],[161,2])). % 67.68/67.75 cnf(164,plain, % 67.68/67.75 (E(f2(f2(a1,f2(a1,f2(x1641,x1642))),f2(a1,x1643)),f2(f2(a1,x1642),f2(f2(a3,x1643),x1641)))), % 67.68/67.75 inference(scs_inference,[],[6,160,161,2,3])). % 67.68/67.75 cnf(166,plain, % 67.68/67.75 (E(f2(f2(a1,x1661),f2(f2(a3,x1662),x1663)),f2(f2(a1,f2(a1,f2(x1663,x1661))),f2(a1,x1662)))), % 67.68/67.75 inference(scs_inference,[],[164,2])). % 67.68/67.75 cnf(167,plain, % 67.68/67.75 (E(f2(f2(a1,f2(a1,x1671)),f2(a1,f2(f2(a3,f2(a1,x1672)),x1673))),f2(f2(a1,f2(x1673,x1671)),f2(a1,x1672)))), % 67.68/67.75 inference(scs_inference,[],[6,163,164,2,3])). % 67.68/67.76 cnf(169,plain, % 67.68/67.76 (E(f2(f2(a1,f2(x1691,x1692)),f2(a1,x1693)),f2(f2(a1,f2(a1,x1692)),f2(a1,f2(f2(a3,f2(a1,x1693)),x1691))))), % 67.68/67.76 inference(scs_inference,[],[167,2])). % 67.68/67.76 cnf(170,plain, % 67.68/67.76 (E(f2(f2(a1,f2(f2(a3,x1701),x1702)),f2(a1,x1703)),f2(f2(a1,f2(a1,f2(x1702,x1703))),f2(a1,x1701)))), % 67.68/67.76 inference(scs_inference,[],[6,166,167,2,3])). % 67.68/67.76 cnf(172,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,f2(x1721,x1722))),f2(a1,x1723)),f2(f2(a1,f2(f2(a3,x1723),x1721)),f2(a1,x1722)))), % 67.68/67.76 inference(scs_inference,[],[170,2])). % 67.68/67.76 cnf(173,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,x1731)),f2(a1,f2(x1732,x1733))),f2(f2(a1,f2(a1,x1733)),f2(a1,f2(f2(a3,f2(a1,x1731)),x1732))))), % 67.68/67.76 inference(scs_inference,[],[6,169,170,2,3])). % 67.68/67.76 cnf(175,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,x1751)),f2(a1,f2(f2(a3,f2(a1,x1752)),x1753))),f2(f2(a1,f2(a1,x1752)),f2(a1,f2(x1753,x1751))))), % 67.68/67.76 inference(scs_inference,[],[173,2])). % 67.68/67.76 cnf(176,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,x1761)),f2(a1,f2(a1,f2(x1762,x1763)))),f2(f2(a1,f2(f2(a3,x1761),x1762)),f2(a1,x1763)))), % 67.68/67.76 inference(scs_inference,[],[6,172,173,2,3])). % 67.68/67.76 cnf(178,plain, % 67.68/67.76 (E(f2(f2(a1,f2(f2(a3,x1781),x1782)),f2(a1,x1783)),f2(f2(a1,f2(a1,x1781)),f2(a1,f2(a1,f2(x1782,x1783)))))), % 67.68/67.76 inference(scs_inference,[],[176,2])). % 67.68/67.76 cnf(179,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,f2(f2(a3,f2(a1,x1791)),x1792))),f2(a1,f2(a1,x1793))),f2(f2(a1,f2(a1,x1791)),f2(a1,f2(x1792,x1793))))), % 67.68/67.76 inference(scs_inference,[],[6,175,176,2,3])). % 67.68/67.76 cnf(182,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,x1821)),f2(a1,f2(f2(a3,x1822),x1823))),f2(f2(a1,f2(a1,x1822)),f2(a1,f2(a1,f2(x1823,x1821)))))), % 67.68/67.76 inference(scs_inference,[],[6,178,179,2,3])). % 67.68/67.76 cnf(184,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,x1841)),f2(a1,f2(a1,f2(x1842,x1843)))),f2(f2(a1,f2(a1,x1843)),f2(a1,f2(f2(a3,x1841),x1842))))), % 67.68/67.76 inference(scs_inference,[],[182,2])). % 67.68/67.76 cnf(185,plain, % 67.68/67.76 (E(f2(f2(a1,f2(x1851,f2(x1852,f2(x1853,x1854)))),f2(f2(a3,f2(a1,x1855)),a1)),f2(f2(a1,f2(x1852,f2(x1853,x1854))),f2(f2(a3,x1855),x1851)))), % 67.68/67.76 inference(scs_inference,[],[6,76,182,2,3])). % 67.68/67.76 cnf(188,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,f2(a1,f2(x1881,x1882)))),f2(a1,f2(a1,x1883))),f2(f2(a1,f2(a1,x1882)),f2(a1,f2(f2(a3,x1883),x1881))))), % 67.68/67.76 inference(scs_inference,[],[6,184,185,2,3])). % 67.68/67.76 cnf(190,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,x1901)),f2(a1,f2(f2(a3,x1902),x1903))),f2(f2(a1,f2(a1,f2(a1,f2(x1903,x1901)))),f2(a1,f2(a1,x1902))))), % 67.68/67.76 inference(scs_inference,[],[188,2])). % 67.68/67.76 cnf(191,plain, % 67.68/67.76 (E(f2(f2(a1,f2(f2(a3,x1911),x1912)),f2(a1,f2(x1913,x1914))),f2(f2(a1,x1913),f2(f2(a3,f2(a1,x1914)),f2(a3,f2(f2(a3,x1911),x1912)))))), % 67.68/67.76 inference(scs_inference,[],[6,80,188,2,3])). % 67.68/67.76 cnf(194,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,f2(f2(a3,x1941),x1942))),f2(a1,f2(a1,x1943))),f2(f2(a1,f2(a1,f2(a1,f2(x1942,x1943)))),f2(a1,f2(a1,x1941))))), % 67.68/67.76 inference(scs_inference,[],[6,190,191,2,3])). % 67.68/67.76 cnf(197,plain, % 67.68/67.76 (E(f2(f2(a1,x1971),f2(a1,f2(x1972,f2(x1973,x1974)))),f2(f2(f2(a3,f2(f2(a3,x1971),x1972)),x1973),x1974))), % 67.68/67.76 inference(scs_inference,[],[6,194,18,2,3])). % 67.68/67.76 cnf(201,plain, % 67.68/67.76 (E(f2(f2(a1,f2(f2(a3,f2(a1,x2011)),x2012)),f2(a1,x2013)),f2(f2(x2012,x2013),x2011))), % 67.68/67.76 inference(scs_inference,[],[6,197,139,2,3])). % 67.68/67.76 cnf(203,plain, % 67.68/67.76 (E(f2(f2(x2031,x2032),x2033),f2(f2(a1,f2(f2(a3,f2(a1,x2033)),x2031)),f2(a1,x2032)))), % 67.68/67.76 inference(scs_inference,[],[201,2])). % 67.68/67.76 cnf(204,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,x2041)),f2(a1,f2(f2(a3,f2(a1,x2042)),x2043))),f2(f2(x2043,x2041),x2042))), % 67.68/67.76 inference(scs_inference,[],[6,201,2,3])). % 67.68/67.76 cnf(206,plain, % 67.68/67.76 (E(f2(f2(x2061,x2062),x2063),f2(f2(a1,f2(a1,x2062)),f2(a1,f2(f2(a3,f2(a1,x2063)),x2061))))), % 67.68/67.76 inference(scs_inference,[],[204,2])). % 67.68/67.76 cnf(207,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,f2(f2(a3,f2(a1,x2071)),x2072))),f2(a1,f2(a1,x2073))),f2(f2(x2072,x2073),x2071))), % 67.68/67.76 inference(scs_inference,[],[6,204,2,3])). % 67.68/67.76 cnf(209,plain, % 67.68/67.76 (E(f2(f2(x2091,x2092),x2093),f2(f2(a1,f2(a1,f2(f2(a3,f2(a1,x2093)),x2091))),f2(a1,f2(a1,x2092))))), % 67.68/67.76 inference(scs_inference,[],[207,2])). % 67.68/67.76 cnf(210,plain, % 67.68/67.76 (E(f2(f2(a1,x2101),f2(x2102,x2103)),f2(f2(a1,f2(a1,x2103)),f2(a1,f2(f2(a3,f2(a1,x2101)),x2102))))), % 67.68/67.76 inference(scs_inference,[],[6,206,207,2,3])). % 67.68/67.76 cnf(213,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,x2131)),f2(a1,f2(f2(a3,f2(a1,x2132)),x2133))),f2(f2(a1,x2132),f2(x2133,x2131)))), % 67.68/67.76 inference(scs_inference,[],[210,2])). % 67.68/67.76 cnf(214,plain, % 67.68/67.76 (E(f2(f2(a1,x2141),f2(x2142,x2143)),f2(f2(a1,f2(a1,f2(f2(a3,f2(a1,x2141)),x2142))),f2(a1,f2(a1,x2143))))), % 67.68/67.76 inference(scs_inference,[],[6,209,210,2,3])). % 67.68/67.76 cnf(218,plain, % 67.68/67.76 (E(f2(f2(a1,f2(x2181,x2182)),f2(a1,x2183)),f2(f2(a1,f2(a1,f2(f2(a3,f2(a1,x2183)),x2181))),f2(a1,f2(a1,x2182))))), % 67.68/67.76 inference(scs_inference,[],[6,214,2,3])). % 67.68/67.76 cnf(221,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,f2(x2211,x2212))),f2(a1,x2213)),f2(f2(f2(a3,x2213),x2211),x2212))), % 67.68/67.76 inference(scs_inference,[],[6,218,150,2,3])). % 67.68/67.76 cnf(224,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,x2241)),f2(a1,f2(a1,f2(x2242,x2243)))),f2(f2(f2(a3,x2241),x2242),x2243))), % 67.68/67.76 inference(scs_inference,[],[6,221,2,3])). % 67.68/67.76 cnf(226,plain, % 67.68/67.76 (E(f2(f2(f2(a3,x2261),x2262),x2263),f2(f2(a1,f2(a1,x2261)),f2(a1,f2(a1,f2(x2262,x2263)))))), % 67.68/67.76 inference(scs_inference,[],[224,2])). % 67.68/67.76 cnf(227,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,f2(a1,f2(x2271,x2272)))),f2(a1,f2(a1,x2273))),f2(f2(f2(a3,x2273),x2271),x2272))), % 67.68/67.76 inference(scs_inference,[],[6,224,2,3])). % 67.68/67.76 cnf(229,plain, % 67.68/67.76 (E(f2(f2(f2(a3,x2291),x2292),x2293),f2(f2(a1,f2(a1,f2(a1,f2(x2292,x2293)))),f2(a1,f2(a1,x2291))))), % 67.68/67.76 inference(scs_inference,[],[227,2])). % 67.68/67.76 cnf(230,plain, % 67.68/67.76 (E(f2(f2(a1,x2301),f2(f2(a3,x2302),x2303)),f2(f2(a1,f2(a1,x2302)),f2(a1,f2(a1,f2(x2303,x2301)))))), % 67.68/67.76 inference(scs_inference,[],[6,226,227,2,3])). % 67.68/67.76 cnf(233,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,x2331)),f2(a1,f2(a1,f2(x2332,x2333)))),f2(f2(a1,x2333),f2(f2(a3,x2331),x2332)))), % 67.68/67.76 inference(scs_inference,[],[230,2])). % 67.68/67.76 cnf(234,plain, % 67.68/67.76 (E(f2(f2(a1,x2341),f2(f2(a3,x2342),x2343)),f2(f2(a1,f2(a1,f2(a1,f2(x2343,x2341)))),f2(a1,f2(a1,x2342))))), % 67.68/67.76 inference(scs_inference,[],[6,229,230,2,3])). % 67.68/67.76 cnf(237,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,f2(a1,f2(x2371,x2372)))),f2(a1,f2(a1,x2373))),f2(f2(a1,x2372),f2(f2(a3,x2373),x2371)))), % 67.68/67.76 inference(scs_inference,[],[234,2])). % 67.68/67.76 cnf(238,plain, % 67.68/67.76 (E(f2(f2(a1,f2(f2(a3,x2381),x2382)),f2(a1,x2383)),f2(f2(a1,f2(a1,f2(a1,f2(x2382,x2383)))),f2(a1,f2(a1,x2381))))), % 67.68/67.76 inference(scs_inference,[],[6,234,2,3])). % 67.68/67.76 cnf(240,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,f2(a1,f2(x2401,x2402)))),f2(a1,f2(a1,x2403))),f2(f2(a1,f2(f2(a3,x2403),x2401)),f2(a1,x2402)))), % 67.68/67.76 inference(scs_inference,[],[238,2])). % 67.68/67.76 cnf(241,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,f2(a1,x2411))),f2(a1,f2(a1,f2(a1,f2(x2412,x2413))))),f2(f2(a1,x2413),f2(f2(a3,x2411),x2412)))), % 67.68/67.76 inference(scs_inference,[],[6,237,238,2,3])). % 67.68/67.76 cnf(243,plain, % 67.68/67.76 (E(f2(f2(a1,x2431),f2(f2(a3,x2432),x2433)),f2(f2(a1,f2(a1,f2(a1,x2432))),f2(a1,f2(a1,f2(a1,f2(x2433,x2431))))))), % 67.68/67.76 inference(scs_inference,[],[241,2])). % 67.68/67.76 cnf(244,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,f2(a1,x2441))),f2(a1,f2(a1,f2(a1,f2(x2442,x2443))))),f2(f2(a1,f2(f2(a3,x2441),x2442)),f2(a1,x2443)))), % 67.68/67.76 inference(scs_inference,[],[6,240,241,2,3])). % 67.68/67.76 cnf(247,plain, % 67.68/67.76 (E(f2(f2(a1,f2(x2471,x2472)),f2(a1,x2473)),f2(f2(a1,x2472),f2(f2(a3,f2(a1,x2473)),x2471)))), % 67.68/67.76 inference(scs_inference,[],[6,244,146,2,3])). % 67.68/67.76 cnf(250,plain, % 67.68/67.76 (E(f2(f2(a1,x2501),f2(f2(a3,f2(f2(a3,x2502),x2503)),x2504)),f2(f2(a1,f2(a1,f2(x2503,f2(x2504,x2501)))),f2(a1,x2502)))), % 67.68/67.76 inference(scs_inference,[],[6,247,30,2,3])). % 67.68/67.76 cnf(254,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,f2(x2541,f2(x2542,x2543)))),f2(a1,x2544)),f2(f2(f2(a3,f2(a1,x2543)),f2(a3,f2(f2(a3,x2544),x2541))),x2542))), % 67.68/67.76 inference(scs_inference,[],[6,250,107,2,3])). % 67.68/67.76 cnf(257,plain, % 67.68/67.76 (E(f2(f2(a1,x2571),f2(a1,f2(x2572,f2(x2573,x2574)))),f2(f2(f2(a3,f2(a1,x2573)),f2(a3,f2(a1,x2574))),f2(a3,f2(f2(a3,x2571),x2572))))), % 67.68/67.76 inference(scs_inference,[],[6,254,54,2,3])). % 67.68/67.76 cnf(261,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,f2(x2611,f2(x2612,x2613)))),f2(a1,x2614)),f2(f2(f2(a3,f2(a1,x2612)),f2(a3,f2(a1,x2613))),f2(a3,f2(f2(a3,x2614),x2611))))), % 67.68/67.76 inference(scs_inference,[],[6,257,2,3])). % 67.68/67.76 cnf(264,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,f2(a1,x2641))),f2(a1,f2(a1,f2(a1,f2(x2642,x2643))))),f2(f2(f2(a3,x2641),x2642),x2643))), % 67.68/67.76 inference(scs_inference,[],[6,261,227,2,3])). % 67.68/67.76 cnf(267,plain, % 67.68/67.76 (E(f2(f2(a1,f2(f2(a3,f2(a1,x2671)),f2(a3,f2(f2(a3,x2672),x2673)))),f2(a1,x2674)),f2(f2(f2(a3,f2(a1,x2672)),a1),f2(x2673,f2(x2674,x2671))))), % 67.68/67.76 inference(scs_inference,[],[6,264,119,2,3])). % 67.68/67.76 cnf(270,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,f2(x2701,x2702))),f2(a1,f2(f2(a3,x2703),x2704))),f2(f2(a1,f2(x2704,f2(x2701,x2702))),x2703))), % 67.68/67.76 inference(scs_inference,[],[6,267,123,2,3])). % 67.68/67.76 cnf(273,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,f2(f2(a3,x2731),x2732))),f2(a1,f2(a1,f2(x2733,x2734)))),f2(f2(a1,f2(x2732,f2(x2733,x2734))),x2731))), % 67.68/67.76 inference(scs_inference,[],[6,270,2,3])). % 67.68/67.76 cnf(275,plain, % 67.68/67.76 (E(f2(f2(a1,f2(x2751,f2(x2752,x2753))),x2754),f2(f2(a1,f2(a1,f2(f2(a3,x2754),x2751))),f2(a1,f2(a1,f2(x2752,x2753)))))), % 67.68/67.76 inference(scs_inference,[],[273,2])). % 67.68/67.76 cnf(276,plain, % 67.68/67.76 (E(f2(f2(a1,x2761),f2(a1,f2(x2762,f2(x2763,x2764)))),f2(f2(a1,f2(f2(a3,f2(a1,x2764)),f2(a3,f2(f2(a3,x2761),x2762)))),f2(a1,x2763)))), % 67.68/67.76 inference(scs_inference,[],[6,273,33,2,3])). % 67.68/67.76 cnf(280,plain, % 67.68/67.76 (E(f2(f2(a1,x2801),f2(a1,f2(x2802,f2(x2803,x2804)))),f2(f2(a1,f2(a1,f2(f2(a3,x2801),x2802))),f2(a1,f2(a1,f2(x2803,x2804)))))), % 67.68/67.76 inference(scs_inference,[],[6,275,276,2,3])). % 67.68/67.76 cnf(284,plain, % 67.68/67.76 (E(f2(f2(a1,f2(f2(a3,x2841),x2842)),f2(a1,x2843)),f2(f2(a1,x2841),f2(a1,f2(x2842,x2843))))), % 67.68/67.76 inference(scs_inference,[],[6,280,157,2,3])). % 67.68/67.76 cnf(286,plain, % 67.68/67.76 (E(f2(f2(a1,x2861),f2(a1,f2(x2862,x2863))),f2(f2(a1,f2(f2(a3,x2861),x2862)),f2(a1,x2863)))), % 67.68/67.76 inference(scs_inference,[],[284,2])). % 67.68/67.76 cnf(287,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,x2871)),f2(a1,f2(f2(a3,x2872),x2873))),f2(f2(a1,x2872),f2(a1,f2(x2873,x2871))))), % 67.68/67.76 inference(scs_inference,[],[6,284,2,3])). % 67.68/67.76 cnf(289,plain, % 67.68/67.76 (E(f2(f2(a1,x2891),f2(a1,f2(x2892,x2893))),f2(f2(a1,f2(a1,x2893)),f2(a1,f2(f2(a3,x2891),x2892))))), % 67.68/67.76 inference(scs_inference,[],[287,2])). % 67.68/67.76 cnf(290,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,f2(f2(a3,x2901),x2902))),f2(a1,f2(a1,x2903))),f2(f2(a1,x2901),f2(a1,f2(x2902,x2903))))), % 67.68/67.76 inference(scs_inference,[],[6,287,2,3])). % 67.68/67.76 cnf(292,plain, % 67.68/67.76 (E(f2(f2(a1,x2921),f2(a1,f2(x2922,x2923))),f2(f2(a1,f2(a1,f2(f2(a3,x2921),x2922))),f2(a1,f2(a1,x2923))))), % 67.68/67.76 inference(scs_inference,[],[290,2])). % 67.68/67.76 cnf(293,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,f2(x2931,x2932))),f2(a1,x2933)),f2(f2(a1,f2(a1,x2932)),f2(a1,f2(f2(a3,x2933),x2931))))), % 67.68/67.76 inference(scs_inference,[],[6,289,290,2,3])). % 67.68/67.76 cnf(295,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,x2951)),f2(a1,f2(f2(a3,x2952),x2953))),f2(f2(a1,f2(a1,f2(x2953,x2951))),f2(a1,x2952)))), % 67.68/67.76 inference(scs_inference,[],[293,2])). % 67.68/67.76 cnf(296,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,f2(x2961,x2962))),f2(a1,x2963)),f2(f2(a1,f2(a1,f2(f2(a3,x2963),x2961))),f2(a1,f2(a1,x2962))))), % 67.68/67.76 inference(scs_inference,[],[6,292,293,2,3])). % 67.68/67.76 cnf(298,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,f2(f2(a3,x2981),x2982))),f2(a1,f2(a1,x2983))),f2(f2(a1,f2(a1,f2(x2982,x2983))),f2(a1,x2981)))), % 67.68/67.76 inference(scs_inference,[],[296,2])). % 67.68/67.76 cnf(299,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,x2991)),f2(a1,f2(a1,f2(x2992,x2993)))),f2(f2(a1,f2(a1,f2(f2(a3,x2991),x2992))),f2(a1,f2(a1,x2993))))), % 67.68/67.76 inference(scs_inference,[],[6,296,2,3])). % 67.68/67.76 cnf(302,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,f2(a1,x3021))),f2(a1,f2(a1,f2(f2(a3,x3022),x3023)))),f2(f2(a1,f2(a1,f2(x3023,x3021))),f2(a1,x3022)))), % 67.68/67.76 inference(scs_inference,[],[6,298,299,2,3])). % 67.68/67.76 cnf(305,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,f2(a1,x3051))),f2(a1,f2(a1,f2(f2(a3,x3052),x3053)))),f2(f2(a1,x3052),f2(a1,f2(x3053,x3051))))), % 67.68/67.76 inference(scs_inference,[],[6,302,290,2,3])). % 67.68/67.76 cnf(308,plain, % 67.68/67.76 (E(f2(f2(a1,x3081),f2(f2(a3,x3082),x3083)),f2(f2(a1,f2(x3083,x3081)),x3082))), % 67.68/67.76 inference(scs_inference,[],[6,305,11,2,3])). % 67.68/67.76 cnf(311,plain, % 67.68/67.76 (E(f2(f2(a1,f2(x3111,x3112)),x3113),f2(f2(a1,x3112),f2(f2(a3,x3113),x3111)))), % 67.68/67.76 inference(scs_inference,[],[308,2])). % 67.68/67.76 cnf(312,plain, % 67.68/67.76 (E(f2(f2(a1,f2(f2(a3,x3121),x3122)),f2(a1,x3123)),f2(f2(a1,f2(x3122,x3123)),x3121))), % 67.68/67.76 inference(scs_inference,[],[6,308,2,3])). % 67.68/67.76 cnf(314,plain, % 67.68/67.76 (E(f2(f2(a1,f2(x3141,x3142)),x3143),f2(f2(a1,f2(f2(a3,x3143),x3141)),f2(a1,x3142)))), % 67.68/67.76 inference(scs_inference,[],[312,2])). % 67.68/67.76 cnf(315,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,x3151)),f2(a1,f2(f2(a3,x3152),x3153))),f2(f2(a1,f2(x3153,x3151)),x3152))), % 67.68/67.76 inference(scs_inference,[],[6,312,2,3])). % 67.68/67.76 cnf(317,plain, % 67.68/67.76 (E(f2(f2(a1,f2(x3171,x3172)),x3173),f2(f2(a1,f2(a1,x3172)),f2(a1,f2(f2(a3,x3173),x3171))))), % 67.68/67.76 inference(scs_inference,[],[315,2])). % 67.68/67.76 cnf(318,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,f2(f2(a3,x3181),x3182))),f2(a1,f2(a1,x3183))),f2(f2(a1,f2(x3182,x3183)),x3181))), % 67.68/67.76 inference(scs_inference,[],[6,315,2,3])). % 67.68/67.76 cnf(320,plain, % 67.68/67.76 (E(f2(f2(a1,f2(x3201,x3202)),x3203),f2(f2(a1,f2(a1,f2(f2(a3,x3203),x3201))),f2(a1,f2(a1,x3202))))), % 67.68/67.76 inference(scs_inference,[],[318,2])). % 67.68/67.76 cnf(321,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,f2(a1,x3211))),f2(a1,f2(a1,f2(f2(a3,x3212),x3213)))),f2(f2(a1,f2(x3213,x3211)),x3212))), % 67.68/67.76 inference(scs_inference,[],[6,318,2,3])). % 67.68/67.76 cnf(323,plain, % 67.68/67.76 (E(f2(f2(a1,f2(x3231,x3232)),x3233),f2(f2(a1,f2(a1,f2(a1,x3232))),f2(a1,f2(a1,f2(f2(a3,x3233),x3231)))))), % 67.68/67.76 inference(scs_inference,[],[321,2])). % 67.68/67.76 cnf(324,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,x3241)),f2(a1,f2(x3242,x3243))),f2(f2(x3242,x3243),x3241))), % 67.68/67.76 inference(scs_inference,[],[6,321,22,2,3])). % 67.68/67.76 cnf(326,plain, % 67.68/67.76 (E(f2(f2(x3261,x3262),x3263),f2(f2(a1,f2(a1,x3263)),f2(a1,f2(x3261,x3262))))), % 67.68/67.76 inference(scs_inference,[],[324,2])). % 67.68/67.76 cnf(327,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,f2(x3271,x3272))),f2(a1,f2(a1,x3273))),f2(f2(x3271,x3272),x3273))), % 67.68/67.76 inference(scs_inference,[],[6,324,2,3])). % 67.68/67.76 cnf(330,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,f2(a1,x3301))),f2(a1,f2(a1,f2(x3302,x3303)))),f2(f2(x3302,x3303),x3301))), % 67.68/67.76 inference(scs_inference,[],[6,327,2,3])). % 67.68/67.76 cnf(332,plain, % 67.68/67.76 (E(f2(f2(x3321,x3322),x3323),f2(f2(a1,f2(a1,f2(a1,x3323))),f2(a1,f2(a1,f2(x3321,x3322)))))), % 67.68/67.76 inference(scs_inference,[],[330,2])). % 67.68/67.76 cnf(333,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,f2(a1,f2(x3331,x3332)))),f2(a1,f2(a1,f2(a1,x3333)))),f2(f2(x3331,x3332),x3333))), % 67.68/67.76 inference(scs_inference,[],[6,330,2,3])). % 67.68/67.76 cnf(336,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,f2(a1,f2(a1,x3361)))),f2(a1,f2(a1,f2(a1,f2(x3362,x3363))))),f2(f2(x3362,x3363),x3361))), % 67.68/67.76 inference(scs_inference,[],[6,333,2,3])). % 67.68/67.76 cnf(338,plain, % 67.68/67.76 (E(f2(f2(x3381,x3382),x3383),f2(f2(a1,f2(a1,f2(a1,f2(a1,x3383)))),f2(a1,f2(a1,f2(a1,f2(x3381,x3382))))))), % 67.68/67.76 inference(scs_inference,[],[336,2])). % 67.68/67.76 cnf(339,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(x3391,x3392)),x3393),x3394),f2(f2(a1,f2(f2(a3,f2(a1,f2(x3393,x3394))),x3391)),f2(a1,x3392)))), % 67.68/67.76 inference(scs_inference,[],[7,203,3])). % 67.68/67.76 cnf(343,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,f2(x3431,x3432))),x3433),x3434),f2(f2(a1,x3432),f2(f2(a3,f2(x3433,x3434)),x3431)))), % 67.68/67.76 inference(scs_inference,[],[7,311,3])). % 67.68/67.76 cnf(346,plain, % 67.68/67.76 (E(f2(f2(a1,x3461),f2(f2(a3,f2(x3462,x3463)),x3464)),f2(f2(f2(a3,f2(a1,f2(x3464,x3461))),x3462),x3463))), % 67.68/67.76 inference(scs_inference,[],[7,311,3,2])). % 67.68/67.76 cnf(347,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,x3471)),f2(a3,f2(x3472,x3473))),x3474),f2(f2(f2(a3,f2(a1,f2(x3474,x3471))),x3472),x3473))), % 67.68/67.76 inference(scs_inference,[],[7,346,3])). % 67.68/67.76 cnf(350,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,f2(x3501,x3502))),x3503),x3504),f2(f2(f2(a3,f2(a1,x3502)),f2(a3,f2(x3503,x3504))),x3501))), % 67.68/67.76 inference(scs_inference,[],[7,346,3,2])). % 67.68/67.76 cnf(351,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,f2(a1,x3511))),a1),f2(f2(a3,f2(a1,x3512)),x3513)),f2(f2(a1,x3512),f2(x3513,x3511)))), % 67.68/67.76 inference(scs_inference,[],[7,213,3])). % 67.68/67.76 cnf(358,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,f2(x3581,x3582))),x3583),x3584),f2(f2(a1,f2(f2(a3,f2(x3583,x3584)),x3581)),f2(a1,x3582)))), % 67.68/67.76 inference(scs_inference,[],[7,314,3])). % 67.68/67.76 cnf(367,plain, % 67.68/67.76 (E(f2(f2(a1,x3671),f2(f2(a3,x3672),x3673)),f2(f2(f2(a3,f2(a1,f2(a1,x3672))),a1),f2(a1,f2(x3673,x3671))))), % 67.68/67.76 inference(scs_inference,[],[7,233,3,2])). % 67.68/67.76 cnf(368,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,x3681)),f2(a3,x3682)),x3683),f2(f2(f2(a3,f2(a1,f2(a1,x3682))),a1),f2(a1,f2(x3683,x3681))))), % 67.68/67.76 inference(scs_inference,[],[7,367,3])). % 67.68/67.76 cnf(372,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,x3721)),f2(a3,x3722)),x3723),f2(f2(a1,f2(a1,f2(a1,x3722))),f2(a1,f2(a1,f2(a1,f2(x3723,x3721))))))), % 67.68/67.76 inference(scs_inference,[],[7,243,3])). % 67.68/67.76 cnf(376,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,x3761)),a1),f2(x3762,x3763)),f2(f2(a1,f2(f2(a3,x3761),x3762)),f2(a1,x3763)))), % 67.68/67.76 inference(scs_inference,[],[7,286,3])). % 67.68/67.76 cnf(379,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,f2(a1,x3791))),a1),f2(f2(a3,x3792),x3793)),f2(f2(a1,f2(a1,f2(x3793,x3791))),f2(a1,x3792)))), % 67.68/67.76 inference(scs_inference,[],[7,295,3])). % 67.68/67.76 cnf(385,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(x3851,x3852)),x3853),x3854),f2(f2(a1,x3852),f2(f2(a3,f2(a1,f2(x3853,x3854))),x3851)))), % 67.68/67.76 inference(scs_inference,[],[7,142,3])). % 67.68/67.76 cnf(388,plain, % 67.68/67.76 (E(f2(f2(a1,x3881),f2(f2(a3,f2(a1,f2(x3882,x3883))),x3884)),f2(f2(f2(a3,f2(x3884,x3881)),x3882),x3883))), % 67.68/67.76 inference(scs_inference,[],[7,142,3,2])). % 67.68/67.76 cnf(392,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(x3921,x3922)),x3923),x3924),f2(f2(f2(a3,f2(a1,x3922)),f2(a3,f2(a1,f2(x3923,x3924)))),x3921))), % 67.68/67.76 inference(scs_inference,[],[7,388,3,2])). % 67.68/67.76 cnf(401,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,x4011)),a1),f2(x4012,x4013)),f2(f2(a1,x4013),f2(f2(a3,x4011),x4012)))), % 67.68/67.76 inference(scs_inference,[],[7,160,3])). % 67.68/67.76 cnf(403,plain, % 67.68/67.76 (E(f2(f2(a1,x4031),f2(f2(a3,x4032),x4033)),f2(f2(f2(a3,f2(a1,x4032)),a1),f2(x4033,x4031)))), % 67.68/67.76 inference(scs_inference,[],[7,160,3,2])). % 67.68/67.76 cnf(404,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,x4041)),f2(a3,x4042)),x4043),f2(f2(f2(a3,f2(a1,x4042)),a1),f2(x4043,x4041)))), % 67.68/67.76 inference(scs_inference,[],[7,403,3])). % 67.68/67.76 cnf(407,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,x4071)),a1),f2(x4072,x4073)),f2(f2(f2(a3,f2(a1,x4073)),f2(a3,x4071)),x4072))), % 67.68/67.76 inference(scs_inference,[],[7,403,3,2])). % 67.68/67.76 cnf(412,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,x4121)),f2(a3,x4122)),x4123),f2(f2(a1,f2(a1,f2(x4123,x4121))),f2(a1,x4122)))), % 67.68/67.76 inference(scs_inference,[],[7,166,3])). % 67.68/67.76 cnf(416,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,x4161)),a1),f2(x4162,x4163)),f2(f2(a1,f2(a1,x4163)),f2(a1,f2(f2(a3,x4161),x4162))))), % 67.68/67.76 inference(scs_inference,[],[7,289,3])). % 67.68/67.76 cnf(418,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,x4181)),f2(a1,f2(f2(a3,x4182),x4183))),f2(f2(f2(a3,f2(a1,x4182)),a1),f2(x4183,x4181)))), % 67.68/67.76 inference(scs_inference,[],[7,289,3,2])). % 67.68/67.76 cnf(419,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,f2(a1,x4191))),a1),f2(f2(a3,x4192),x4193)),f2(f2(f2(a3,f2(a1,x4192)),a1),f2(x4193,x4191)))), % 67.68/67.76 inference(scs_inference,[],[7,418,3])). % 67.68/67.76 cnf(421,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,x4211)),a1),f2(x4212,x4213)),f2(f2(f2(a3,f2(a1,f2(a1,x4213))),a1),f2(f2(a3,x4211),x4212)))), % 67.68/67.76 inference(scs_inference,[],[7,418,3,2])). % 67.68/67.76 cnf(422,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,x4221)),a1),f2(x4222,x4223)),f2(f2(a1,f2(a1,f2(f2(a3,x4221),x4222))),f2(a1,f2(a1,x4223))))), % 67.68/67.76 inference(scs_inference,[],[7,292,3])). % 67.68/67.76 cnf(434,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,x4341)),f2(a3,f2(a1,x4342))),f2(a3,f2(f2(a3,x4343),x4344))),f2(f2(a1,f2(x4341,x4342)),f2(f2(a3,x4343),x4344)))), % 67.68/67.76 inference(scs_inference,[],[7,82,3])). % 67.68/67.76 cnf(436,plain, % 67.68/67.76 (E(f2(f2(a1,f2(x4361,x4362)),f2(f2(a3,x4363),x4364)),f2(f2(f2(a3,f2(a1,x4361)),f2(a3,f2(a1,x4362))),f2(a3,f2(f2(a3,x4363),x4364))))), % 67.68/67.76 inference(scs_inference,[],[7,82,3,2])). % 67.68/67.76 cnf(444,plain, % 67.68/67.76 (E(f2(f2(x4441,f2(x4442,x4443)),x4444),f2(f2(f2(a3,f2(f2(a3,f2(a1,x4444)),x4441)),x4442),x4443))), % 67.68/67.76 inference(scs_inference,[],[7,17,3,2])). % 67.68/67.76 cnf(448,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(x4481,x4482)),x4483),x4484),f2(f2(f2(a3,f2(a1,f2(x4483,x4484))),x4481),x4482))), % 67.68/67.76 inference(scs_inference,[],[7,13,3,2])). % 67.68/67.76 cnf(449,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(f2(a3,f2(a1,x4491)),f2(a3,x4492))),x4493),x4494),f2(f2(f2(a3,f2(a1,x4492)),a1),f2(f2(x4493,x4494),x4491)))), % 67.68/67.76 inference(scs_inference,[],[7,404,3])). % 67.68/67.76 cnf(453,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x4531))),a1)),f2(a3,f2(a1,x4532))),x4533),f2(f2(a1,x4532),f2(x4533,x4531)))), % 67.68/67.76 inference(scs_inference,[],[7,351,3])). % 67.68/67.76 cnf(457,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(f2(a3,f2(a1,x4571)),a1)),x4572),x4573),f2(f2(a1,x4573),f2(f2(a3,x4571),x4572)))), % 67.68/67.76 inference(scs_inference,[],[7,453,401,2,3])). % 67.68/67.76 cnf(461,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,x4611)),x4612),f2(x4613,x4614)),f2(f2(f2(a3,f2(a1,x4613)),f2(a3,f2(a1,x4614))),f2(a3,f2(f2(a3,f2(a1,x4611)),x4612))))), % 67.68/67.76 inference(scs_inference,[],[7,457,86,2,3])). % 67.68/67.76 cnf(465,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(f2(a3,f2(a1,x4651)),f2(a3,x4652))),x4653),x4654),f2(f2(a1,f2(a1,f2(f2(x4653,x4654),x4651))),f2(a1,x4652)))), % 67.68/67.76 inference(scs_inference,[],[7,461,412,2,3])). % 67.68/67.76 cnf(469,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(f2(a3,f2(a1,x4691)),f2(a3,f2(a1,x4692)))),a3),f2(f2(a3,x4693),x4694)),f2(f2(a1,f2(x4691,x4692)),f2(f2(a3,x4693),x4694)))), % 67.68/67.76 inference(scs_inference,[],[7,465,434,2,3])). % 67.68/67.76 cnf(471,plain, % 67.68/67.76 (E(f2(f2(a1,f2(x4711,x4712)),f2(f2(a3,x4713),x4714)),f2(f2(f2(a3,f2(f2(a3,f2(a1,x4711)),f2(a3,f2(a1,x4712)))),a3),f2(f2(a3,x4713),x4714)))), % 67.68/67.76 inference(scs_inference,[],[469,2])). % 67.68/67.76 cnf(472,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x4721))),a1)),f2(a3,x4722)),x4723),f2(f2(f2(a3,f2(a1,x4722)),a1),f2(x4723,x4721)))), % 67.68/67.76 inference(scs_inference,[],[7,469,419,2,3])). % 67.68/67.76 cnf(476,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x4761))),a1)),f2(a3,x4762)),x4763),f2(f2(a1,f2(a1,f2(x4763,x4761))),f2(a1,x4762)))), % 67.68/67.76 inference(scs_inference,[],[7,472,379,2,3])). % 67.68/67.76 cnf(480,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,f2(x4801,x4802))),f2(a3,x4803)),x4804),f2(f2(a1,x4801),f2(f2(a3,f2(a1,x4802)),f2(a3,f2(f2(a3,x4803),x4804)))))), % 67.68/67.76 inference(scs_inference,[],[7,476,80,2,3])). % 67.68/67.76 cnf(484,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,f2(a1,f2(x4841,x4842)))),a1),x4843),f2(f2(a1,x4842),f2(f2(a3,x4843),x4841)))), % 67.68/67.76 inference(scs_inference,[],[7,480,164,2,3])). % 67.68/67.76 cnf(488,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,x4881)),f2(a3,x4882)),x4883),f2(f2(a1,f2(a1,x4882)),f2(a1,f2(a1,f2(x4883,x4881)))))), % 67.68/67.76 inference(scs_inference,[],[7,484,230,2,3])). % 67.68/67.76 cnf(492,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,f2(a1,x4921))),a1),f2(a1,f2(x4922,x4923))),f2(f2(a1,f2(f2(a3,x4921),x4922)),f2(a1,x4923)))), % 67.68/67.76 inference(scs_inference,[],[7,488,176,2,3])). % 67.68/67.76 cnf(495,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,f2(a1,x4951))),a1),f2(f2(a3,x4952),x4953)),f2(f2(a1,f2(a1,x4952)),f2(a1,f2(a1,f2(x4953,x4951)))))), % 67.68/67.76 inference(scs_inference,[],[7,492,182,2,3])). % 67.68/67.76 cnf(498,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,f2(a1,x4981))),a1),f2(a1,f2(x4982,x4983))),f2(f2(a1,f2(a1,f2(f2(a3,x4981),x4982))),f2(a1,f2(a1,x4983))))), % 67.68/67.76 inference(scs_inference,[],[7,495,299,2,3])). % 67.68/67.76 cnf(501,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,x5011)),f2(a3,f2(a1,x5012))),x5013),f2(f2(x5013,x5011),x5012))), % 67.68/67.76 inference(scs_inference,[],[7,498,139,2,3])). % 67.68/67.76 cnf(504,plain, % 67.68/67.76 (E(f2(f2(x5041,x5042),x5043),f2(f2(f2(a3,f2(a1,x5042)),f2(a3,f2(a1,x5043))),x5041))), % 67.68/67.76 inference(scs_inference,[],[501,2])). % 67.68/67.76 cnf(505,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,f2(a1,x5051))),a1),f2(x5052,x5053)),f2(f2(x5052,x5053),x5051))), % 67.68/67.76 inference(scs_inference,[],[7,501,324,2,3])). % 67.68/67.76 cnf(507,plain, % 67.68/67.76 (E(f2(f2(x5071,x5072),x5073),f2(f2(f2(a3,f2(a1,f2(a1,x5073))),a1),f2(x5071,x5072)))), % 67.68/67.76 inference(scs_inference,[],[505,2])). % 67.68/67.76 cnf(508,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,x5081)),a1),f2(x5082,x5083)),f2(f2(f2(a3,x5081),x5082),x5083))), % 67.68/67.76 inference(scs_inference,[],[7,505,150,2,3])). % 67.68/67.76 cnf(510,plain, % 67.68/67.76 (E(f2(f2(f2(a3,x5101),x5102),x5103),f2(f2(f2(a3,f2(a1,x5101)),a1),f2(x5102,x5103)))), % 67.68/67.76 inference(scs_inference,[],[508,2])). % 67.68/67.76 cnf(511,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(x5111,x5112)),x5113),x5114),f2(f2(f2(a3,f2(a1,f2(a1,f2(x5113,x5114)))),a1),f2(x5111,x5112)))), % 67.68/67.76 inference(scs_inference,[],[7,507,508,2,3])). % 67.68/67.76 cnf(515,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(f2(a3,f2(a1,x5151)),a1)),x5152),x5153),f2(f2(f2(a3,x5151),x5152),x5153))), % 67.68/67.76 inference(scs_inference,[],[7,511,508,2,3])). % 67.68/67.76 cnf(518,plain, % 67.68/67.76 (E(f2(f2(f2(a3,x5181),x5182),x5183),f2(f2(f2(a3,f2(f2(a3,f2(a1,x5181)),a1)),x5182),x5183))), % 67.68/67.76 inference(scs_inference,[],[515,2])). % 67.68/67.76 cnf(519,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,x5191)),f2(a3,x5192)),x5193),f2(f2(a1,f2(x5193,x5191)),x5192))), % 67.68/67.76 inference(scs_inference,[],[7,515,308,2,3])). % 67.68/67.76 cnf(522,plain, % 67.68/67.76 (E(f2(f2(a1,f2(x5221,x5222)),x5223),f2(f2(f2(a3,f2(a1,x5222)),f2(a3,x5223)),x5221))), % 67.68/67.76 inference(scs_inference,[],[519,2])). % 67.68/67.76 cnf(523,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(f2(a3,f2(a1,x5231)),f2(a3,x5232))),x5233),x5234),f2(f2(a1,f2(f2(x5233,x5234),x5231)),x5232))), % 67.68/67.76 inference(scs_inference,[],[7,519,2,3])). % 67.68/67.76 cnf(526,plain, % 67.68/67.76 (E(f2(f2(a1,f2(f2(x5261,x5262),x5263)),x5264),f2(f2(f2(a3,f2(f2(a3,f2(a1,x5263)),f2(a3,x5264))),x5261),x5262))), % 67.68/67.76 inference(scs_inference,[],[523,2])). % 67.68/67.76 cnf(527,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,f2(a1,x5271))),a1),f2(f2(a3,f2(a1,x5272)),x5273)),f2(f2(x5273,x5271),x5272))), % 67.68/67.76 inference(scs_inference,[],[7,523,204,2,3])). % 67.68/67.76 cnf(529,plain, % 67.68/67.76 (E(f2(f2(x5291,x5292),x5293),f2(f2(f2(a3,f2(a1,f2(a1,x5292))),a1),f2(f2(a3,f2(a1,x5293)),x5291)))), % 67.68/67.76 inference(scs_inference,[],[527,2])). % 67.68/67.76 cnf(530,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x5301))),a1)),f2(a3,f2(a1,x5302))),x5303),f2(f2(x5303,x5301),x5302))), % 67.68/67.76 inference(scs_inference,[],[7,527,2,3])). % 67.68/67.76 cnf(533,plain, % 67.68/67.76 (E(f2(f2(x5331,x5332),x5333),f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x5332))),a1)),f2(a3,f2(a1,x5333))),x5331))), % 67.68/67.76 inference(scs_inference,[],[530,2])). % 67.68/67.76 cnf(534,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,f2(a1,f2(x5341,x5342)))),a1),f2(a1,x5343)),f2(f2(x5341,x5342),x5343))), % 67.68/67.76 inference(scs_inference,[],[7,530,327,2,3])). % 67.68/67.76 cnf(536,plain, % 67.68/67.76 (E(f2(f2(x5361,x5362),x5363),f2(f2(f2(a3,f2(a1,f2(a1,f2(x5361,x5362)))),a1),f2(a1,x5363)))), % 67.68/67.76 inference(scs_inference,[],[534,2])). % 67.68/67.76 cnf(537,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,f2(a1,f2(x5371,x5372)))),a1),x5373),f2(f2(f2(a3,x5373),x5371),x5372))), % 67.68/67.76 inference(scs_inference,[],[7,534,221,2,3])). % 67.68/67.76 cnf(541,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,f2(a1,f2(a1,x5411)))),a1),f2(a1,f2(x5412,x5413))),f2(f2(x5412,x5413),x5411))), % 67.68/67.76 inference(scs_inference,[],[7,537,330,2,3])). % 67.68/67.76 cnf(544,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,f2(a1,x5441))),a1),f2(a1,f2(x5442,x5443))),f2(f2(f2(a3,x5441),x5442),x5443))), % 67.68/67.76 inference(scs_inference,[],[7,541,224,2,3])). % 67.68/67.76 cnf(547,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,x5471)),f2(a3,f2(a1,x5472))),f2(a3,f2(f2(a3,x5473),x5474))),f2(f2(f2(a3,f2(a1,x5473)),a1),f2(x5474,f2(x5471,x5472))))), % 67.68/67.76 inference(scs_inference,[],[7,544,119,2,3])). % 67.68/67.76 cnf(550,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,f2(f2(a3,x5501),x5502))),a1),x5503),f2(f2(a1,f2(x5502,x5503)),x5501))), % 67.68/67.76 inference(scs_inference,[],[7,547,312,2,3])). % 67.68/67.76 cnf(553,plain, % 67.68/67.76 (E(f2(f2(a1,f2(x5531,x5532)),x5533),f2(f2(f2(a3,f2(a1,f2(f2(a3,x5533),x5531))),a1),x5532))), % 67.68/67.76 inference(scs_inference,[],[550,2])). % 67.68/67.76 cnf(554,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,x5541)),f2(a3,x5542)),x5543),f2(f2(a1,x5542),f2(a1,f2(x5543,x5541))))), % 67.68/67.76 inference(scs_inference,[],[7,550,157,2,3])). % 67.68/67.76 cnf(558,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(f2(a3,f2(a1,x5581)),f2(a3,x5582))),x5583),x5584),f2(f2(a1,x5582),f2(a1,f2(f2(x5583,x5584),x5581))))), % 67.68/67.76 inference(scs_inference,[],[7,554,2,3])). % 67.68/67.76 cnf(562,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,f2(a1,x5621))),a1),f2(f2(a3,x5622),x5623)),f2(f2(a1,f2(x5623,x5621)),x5622))), % 67.68/67.76 inference(scs_inference,[],[7,558,315,2,3])). % 67.68/67.76 cnf(564,plain, % 67.68/67.76 (E(f2(f2(a1,f2(x5641,x5642)),x5643),f2(f2(f2(a3,f2(a1,f2(a1,x5642))),a1),f2(f2(a3,x5643),x5641)))), % 67.68/67.76 inference(scs_inference,[],[562,2])). % 67.68/67.76 cnf(565,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x5651))),a1)),f2(a3,x5652)),x5653),f2(f2(a1,f2(x5653,x5651)),x5652))), % 67.68/67.76 inference(scs_inference,[],[7,562,2,3])). % 67.68/67.76 cnf(568,plain, % 67.68/67.76 (E(f2(f2(a1,f2(x5681,x5682)),x5683),f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x5682))),a1)),f2(a3,x5683)),x5681))), % 67.68/67.76 inference(scs_inference,[],[565,2])). % 67.68/67.76 cnf(569,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,x5691)),f2(a3,x5692)),x5693),f2(f2(a1,f2(a1,f2(a1,f2(x5693,x5691)))),f2(a1,f2(a1,x5692))))), % 67.68/67.76 inference(scs_inference,[],[7,565,234,2,3])). % 67.68/67.76 cnf(573,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,f2(f2(a3,x5731),x5732))),a1),x5733),f2(f2(a1,x5731),f2(a1,f2(x5732,x5733))))), % 67.68/67.76 inference(scs_inference,[],[7,569,284,2,3])). % 67.68/67.76 cnf(577,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,f2(a1,x5771))),a1),f2(f2(a3,x5772),x5773)),f2(f2(a1,x5772),f2(a1,f2(x5773,x5771))))), % 67.68/67.76 inference(scs_inference,[],[7,573,287,2,3])). % 67.68/67.76 cnf(580,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x5801))),a1)),f2(a3,x5802)),x5803),f2(f2(a1,x5802),f2(a1,f2(x5803,x5801))))), % 67.68/67.76 inference(scs_inference,[],[7,577,2,3])). % 67.68/67.76 cnf(584,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,f2(x5841,x5842))),a1),x5843),f2(f2(x5841,x5842),x5843))), % 67.68/67.76 inference(scs_inference,[],[7,580,22,2,3])). % 67.68/67.76 cnf(587,plain, % 67.68/67.76 (E(f2(f2(x5871,x5872),x5873),f2(f2(f2(a3,f2(a1,f2(x5871,x5872))),a1),x5873))), % 67.68/67.76 inference(scs_inference,[],[584,2])). % 67.68/67.76 cnf(588,plain, % 67.68/67.76 (E(f2(f2(x5881,f2(x5882,x5883)),x5884),f2(f2(a1,x5883),f2(f2(a3,f2(f2(a3,f2(a1,x5884)),x5881)),x5882)))), % 67.68/67.76 inference(scs_inference,[],[9,444,3])). % 67.68/67.76 cnf(590,plain, % 67.68/67.76 (E(f2(f2(a1,x5901),f2(f2(a3,f2(f2(a3,f2(a1,x5902)),x5903)),x5904)),f2(f2(x5903,f2(x5904,x5901)),x5902))), % 67.68/67.76 inference(scs_inference,[],[588,2])). % 67.68/67.76 cnf(591,plain, % 67.68/67.76 (E(f2(f2(f2(a3,x5911),x5912),x5913),f2(f2(f2(a3,f2(a1,f2(x5912,x5913))),f2(a3,f2(a1,x5911))),a1))), % 67.68/67.76 inference(scs_inference,[],[448,518,588,2,3])). % 67.68/67.76 cnf(593,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,f2(x5931,x5932))),f2(a3,f2(a1,x5933))),a1),f2(f2(f2(a3,x5933),x5931),x5932))), % 67.68/67.76 inference(scs_inference,[],[591,2])). % 67.68/67.76 cnf(594,plain, % 67.68/67.76 (E(f2(f2(x5941,x5942),x5943),f2(f2(a1,x5941),f2(f2(a3,f2(a1,x5942)),f2(a3,f2(a1,x5943)))))), % 67.68/67.76 inference(scs_inference,[],[9,504,591,2,3])). % 67.68/67.76 cnf(596,plain, % 67.68/67.76 (E(f2(f2(a1,x5961),f2(f2(a3,f2(a1,x5962)),f2(a3,f2(a1,x5963)))),f2(f2(x5961,x5962),x5963))), % 67.68/67.76 inference(scs_inference,[],[594,2])). % 67.68/67.76 cnf(597,plain, % 67.68/67.76 (E(f2(f2(x5971,x5972),x5973),f2(f2(a1,x5971),f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x5972))),a1)),f2(a3,f2(a1,x5973)))))), % 67.68/67.76 inference(scs_inference,[],[9,533,594,2,3])). % 67.68/67.76 cnf(600,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,f2(x6001,x6002))),x6003),x6004),f2(f2(a1,x6001),f2(f2(a3,f2(a1,x6002)),f2(a3,f2(x6003,x6004)))))), % 67.68/67.76 inference(scs_inference,[],[9,350,597,2,3])). % 67.68/67.76 cnf(603,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(x6031,x6032)),x6033),x6034),f2(f2(a1,x6031),f2(f2(a3,f2(a1,x6032)),f2(a3,f2(a1,f2(x6033,x6034))))))), % 67.68/67.76 inference(scs_inference,[],[9,392,600,2,3])). % 67.68/67.76 cnf(606,plain, % 67.68/67.76 (E(f2(f2(a1,x6061),f2(f2(a3,f2(f2(a3,f2(a1,x6062)),x6063)),x6064)),f2(f2(a1,x6062),f2(x6063,f2(x6064,x6061))))), % 67.68/67.76 inference(scs_inference,[],[9,590,603,2,3])). % 67.68/67.76 cnf(609,plain, % 67.68/67.76 (E(f2(f2(a1,f2(f2(x6091,x6092),x6093)),x6094),f2(f2(a1,x6092),f2(f2(a3,f2(f2(a3,f2(a1,x6093)),f2(a3,x6094))),x6091)))), % 67.68/67.76 inference(scs_inference,[],[9,526,606,2,3])). % 67.68/67.76 cnf(611,plain, % 67.68/67.76 (E(f2(f2(a1,x6111),f2(f2(a3,f2(f2(a3,f2(a1,x6112)),f2(a3,x6113))),x6114)),f2(f2(a1,f2(f2(x6114,x6111),x6112)),x6113))), % 67.68/67.76 inference(scs_inference,[],[609,2])). % 67.68/67.76 cnf(612,plain, % 67.68/67.76 (E(f2(f2(x6121,x6122),x6123),f2(f2(a1,x6123),f2(f2(a3,f2(a1,f2(x6121,x6122))),a1)))), % 67.68/67.76 inference(scs_inference,[],[9,587,609,2,3])). % 67.68/67.76 cnf(615,plain, % 67.68/67.76 (E(f2(f2(f2(a3,x6151),x6152),x6153),f2(f2(a1,f2(x6152,x6153)),f2(f2(a3,f2(a1,x6151)),a1)))), % 67.68/67.76 inference(scs_inference,[],[9,510,612,2,3])). % 67.68/67.76 cnf(618,plain, % 67.68/67.76 (E(f2(f2(a1,f2(x6181,x6182)),x6183),f2(f2(a1,x6181),f2(f2(a3,f2(a1,x6182)),f2(a3,x6183))))), % 67.68/67.76 inference(scs_inference,[],[9,522,615,2,3])). % 67.68/67.76 cnf(621,plain, % 67.68/67.76 (E(f2(x6211,f2(x6212,x6213)),f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x6213))),a1)),f2(a3,x6211)),x6212))), % 67.68/67.76 inference(scs_inference,[],[9,568,618,2,3])). % 67.68/67.76 cnf(624,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x6241))),a1)),f2(a3,x6242)),x6243),f2(x6242,f2(x6243,x6241)))), % 67.68/67.76 inference(scs_inference,[],[621,2])). % 67.68/67.76 cnf(625,plain, % 67.68/67.76 (E(f2(x6251,x6252),f2(f2(f2(a3,f2(a1,f2(a1,x6252))),a1),f2(f2(a3,f2(a1,x6251)),a1)))), % 67.68/67.76 inference(scs_inference,[],[9,529,621,2,3])). % 67.68/67.76 cnf(628,plain, % 67.68/67.76 (E(f2(x6281,x6282),f2(f2(a1,f2(a1,x6281)),f2(a1,f2(a1,x6282))))), % 67.68/67.76 inference(scs_inference,[],[9,326,625,2,3])). % 67.68/67.76 cnf(631,plain, % 67.68/67.76 (E(f2(x6311,f2(x6312,x6313)),f2(f2(f2(a3,f2(a1,f2(f2(a3,x6311),x6312))),a1),x6313))), % 67.68/67.76 inference(scs_inference,[],[9,553,628,2,3])). % 67.68/67.76 cnf(635,plain, % 67.68/67.76 (E(f2(x6351,x6352),f2(f2(f2(a3,f2(a1,f2(a1,f2(a1,x6352)))),a1),f2(a1,x6351)))), % 67.68/67.76 inference(scs_inference,[],[9,536,631,2,3])). % 67.68/67.76 cnf(638,plain, % 67.68/67.76 (E(f2(x6381,x6382),f2(f2(a1,f2(a1,f2(a1,x6381))),f2(a1,f2(a1,f2(a1,x6382)))))), % 67.68/67.76 inference(scs_inference,[],[9,332,635,2,3])). % 67.68/67.76 cnf(641,plain, % 67.68/67.76 (E(f2(x6411,f2(x6412,x6413)),f2(f2(f2(a3,f2(a1,f2(a1,x6413))),a1),f2(f2(a3,x6411),x6412)))), % 67.68/67.76 inference(scs_inference,[],[9,564,638,2,3])). % 67.68/67.76 cnf(645,plain, % 67.68/67.76 (E(f2(x6451,x6452),f2(f2(a1,f2(a1,f2(a1,f2(a1,x6451)))),f2(a1,f2(a1,f2(a1,f2(a1,x6452))))))), % 67.68/67.76 inference(scs_inference,[],[9,338,641,2,3])). % 67.68/67.76 cnf(648,plain, % 67.68/67.76 (E(f2(f2(f2(a3,x6481),x6482),f2(x6483,x6484)),f2(f2(f2(a3,f2(f2(a3,f2(a1,x6483)),f2(a3,f2(a1,x6484)))),a3),f2(f2(a3,x6481),x6482)))), % 67.68/67.76 inference(scs_inference,[],[9,471,645,2,3])). % 67.68/67.76 cnf(651,plain, % 67.68/67.76 (E(f2(x6511,f2(x6512,x6513)),f2(f2(a1,f2(a1,x6513)),f2(a1,f2(f2(a3,x6511),x6512))))), % 67.68/67.76 inference(scs_inference,[],[9,317,648,2,3])). % 67.68/67.76 cnf(655,plain, % 67.68/67.76 (E(f2(x6551,f2(x6552,x6553)),f2(f2(a1,f2(a1,f2(f2(a3,x6551),x6552))),f2(a1,f2(a1,x6553))))), % 67.68/67.76 inference(scs_inference,[],[9,320,651,2,3])). % 67.68/67.76 cnf(659,plain, % 67.68/67.76 (E(f2(x6591,f2(x6592,x6593)),f2(f2(a1,f2(a1,f2(a1,x6593))),f2(a1,f2(a1,f2(f2(a3,x6591),x6592)))))), % 67.68/67.76 inference(scs_inference,[],[9,323,655,2,3])). % 67.68/67.76 cnf(663,plain, % 67.68/67.76 (E(f2(x6631,f2(x6632,x6633)),f2(f2(f2(a3,f2(f2(a3,f2(a1,x6631)),a1)),x6632),x6633))), % 67.68/67.76 inference(scs_inference,[],[9,444,659,2,3])). % 67.68/67.76 cnf(666,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(f2(a3,f2(a1,x6661)),a1)),x6662),x6663),f2(x6661,f2(x6662,x6663)))), % 67.68/67.76 inference(scs_inference,[],[663,2])). % 67.68/67.76 cnf(667,plain, % 67.68/67.76 (E(f2(x6671,x6672),f2(f2(f2(a3,f2(a1,x6672)),f2(a3,f2(a1,x6671))),a1))), % 67.68/67.76 inference(scs_inference,[],[9,504,663,2,3])). % 67.68/67.76 cnf(669,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,x6691)),f2(a3,f2(a1,x6692))),a1),f2(x6692,x6691))), % 67.68/67.76 inference(scs_inference,[],[667,2])). % 67.68/67.76 cnf(670,plain, % 67.68/67.76 (E(f2(x6701,x6702),f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x6702))),a1)),f2(a3,f2(a1,x6701))),a1))), % 67.68/67.76 inference(scs_inference,[],[9,533,667,2,3])). % 67.68/67.76 cnf(673,plain, % 67.68/67.76 (E(f2(x6731,f2(f2(x6732,x6733),x6734)),f2(f2(f2(a3,f2(f2(a3,f2(a1,x6734)),f2(a3,x6731))),x6732),x6733))), % 67.68/67.76 inference(scs_inference,[],[9,526,670,2,3])). % 67.68/67.76 cnf(676,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(f2(a3,f2(a1,x6761)),f2(a3,x6762))),x6763),x6764),f2(x6762,f2(f2(x6763,x6764),x6761)))), % 67.68/67.76 inference(scs_inference,[],[673,2])). % 67.68/67.76 cnf(677,plain, % 67.68/67.76 (E(f2(x6771,x6772),f2(f2(f2(a3,f2(a1,f2(a1,x6772))),a1),x6771))), % 67.68/67.76 inference(scs_inference,[],[9,587,673,2,3])). % 67.68/67.76 cnf(679,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,f2(a1,x6791))),a1),x6792),f2(x6792,x6791))), % 67.68/67.76 inference(scs_inference,[],[677,2])). % 67.68/67.76 cnf(680,plain, % 67.68/67.76 (E(f2(x6801,f2(x6802,x6803)),f2(f2(f2(a3,f2(a1,x6803)),f2(a3,x6801)),x6802))), % 67.68/67.76 inference(scs_inference,[],[9,522,677,2,3])). % 67.68/67.76 cnf(683,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,x6831)),f2(a3,x6832)),x6833),f2(x6832,f2(x6833,x6831)))), % 67.68/67.76 inference(scs_inference,[],[680,2])). % 67.68/67.76 cnf(684,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,f2(a1,a1))),a1),f2(f2(a3,f2(a1,f2(x6841,x6842))),f2(a3,f2(a1,x6843)))),f2(f2(f2(a3,x6843),x6841),x6842))), % 67.68/67.76 inference(scs_inference,[],[679,593,680,2,3])). % 67.68/67.76 cnf(686,plain, % 67.68/67.76 (E(f2(f2(f2(a3,x6861),x6862),x6863),f2(f2(f2(a3,f2(a1,f2(a1,a1))),a1),f2(f2(a3,f2(a1,f2(x6862,x6863))),f2(a3,f2(a1,x6861)))))), % 67.68/67.76 inference(scs_inference,[],[684,2])). % 67.68/67.76 cnf(687,plain, % 67.68/67.76 (E(f2(x6871,f2(x6872,x6873)),f2(f2(f2(a3,f2(a1,x6872)),f2(a3,f2(a1,x6873))),f2(a3,f2(f2(a3,f2(a1,x6871)),a1))))), % 67.68/67.76 inference(scs_inference,[],[9,63,684,2,3])). % 67.68/67.76 cnf(691,plain, % 67.68/67.76 (E(f2(x6911,x6912),f2(f2(a1,f2(f2(a3,f2(a1,x6911)),a1)),f2(a1,x6912)))), % 67.68/67.76 inference(scs_inference,[],[9,203,687,2,3])). % 67.68/67.76 cnf(694,plain, % 67.68/67.76 (E(f2(x6941,f2(x6942,x6943)),f2(f2(a1,x6943),f2(f2(a3,x6941),x6942)))), % 67.68/67.76 inference(scs_inference,[],[9,311,691,2,3])). % 67.68/67.76 cnf(698,plain, % 67.68/67.76 (E(f2(x6981,f2(x6982,f2(x6983,x6984))),f2(f2(a1,x6984),f2(f2(a3,f2(f2(a3,x6981),x6982)),x6983)))), % 67.68/67.76 inference(scs_inference,[],[9,106,694,2,3])). % 67.68/67.76 cnf(701,plain, % 67.68/67.76 (E(f2(f2(a1,x7011),f2(f2(a3,f2(f2(a3,x7012),x7013)),x7014)),f2(x7012,f2(x7013,f2(x7014,x7011))))), % 67.68/67.76 inference(scs_inference,[],[698,2])). % 67.68/67.76 cnf(702,plain, % 67.68/67.76 (E(f2(x7021,x7022),f2(f2(a1,f2(a1,x7022)),f2(a1,f2(f2(a3,f2(a1,x7021)),a1))))), % 67.68/67.76 inference(scs_inference,[],[9,206,698,2,3])). % 67.68/67.76 cnf(705,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(f2(a3,x7051),x7052)),x7053),x7054),f2(x7051,f2(x7052,f2(x7053,x7054))))), % 67.68/67.76 inference(scs_inference,[],[9,701,702,2,3])). % 67.68/67.76 cnf(708,plain, % 67.68/67.76 (E(f2(x7081,f2(x7082,f2(x7083,x7084))),f2(f2(f2(a3,f2(f2(a3,x7081),x7082)),x7083),x7084))), % 67.68/67.76 inference(scs_inference,[],[705,2])). % 67.68/67.76 cnf(709,plain, % 67.68/67.76 (E(f2(x7091,x7092),f2(f2(a1,f2(a1,f2(f2(a3,f2(a1,x7091)),a1))),f2(a1,f2(a1,x7092))))), % 67.68/67.76 inference(scs_inference,[],[9,209,705,2,3])). % 67.68/67.76 cnf(712,plain, % 67.68/67.76 (E(f2(x7121,f2(x7122,f2(x7123,x7124))),f2(f2(f2(a3,f2(a1,x7121)),a1),f2(x7122,f2(x7123,x7124))))), % 67.68/67.76 inference(scs_inference,[],[708,69,709,2,3])). % 67.68/67.76 cnf(715,plain, % 67.68/67.76 (E(f2(f2(f2(a3,x7151),x7152),f2(x7153,x7154)),f2(f2(f2(a3,f2(a1,x7153)),f2(a3,f2(a1,x7154))),f2(a3,f2(f2(a3,x7151),x7152))))), % 67.68/67.76 inference(scs_inference,[],[9,436,712,2,3])). % 67.68/67.76 cnf(718,plain, % 67.68/67.76 (E(f2(x7181,f2(x7182,x7183)),f2(f2(a1,f2(f2(a3,x7181),x7182)),f2(a1,x7183)))), % 67.68/67.76 inference(scs_inference,[],[9,314,715,2,3])). % 67.68/67.76 cnf(722,plain, % 67.68/67.76 (E(f2(x7221,x7222),f2(f2(a1,x7222),f2(f2(a3,f2(a1,x7221)),a1)))), % 67.68/67.76 inference(scs_inference,[],[9,142,718,2,3])). % 67.68/67.76 cnf(725,plain, % 67.68/67.76 (E(f2(x7251,f2(x7252,f2(x7253,x7254))),f2(f2(a1,x7253),f2(f2(a3,f2(a1,x7254)),f2(a3,f2(f2(a3,x7251),x7252)))))), % 67.68/67.76 inference(scs_inference,[],[9,42,722,2,3])). % 67.68/67.76 cnf(728,plain, % 67.68/67.76 (E(f2(f2(a1,x7281),f2(f2(a3,f2(a1,x7282)),f2(a3,f2(f2(a3,x7283),x7284)))),f2(x7283,f2(x7284,f2(x7281,x7282))))), % 67.68/67.76 inference(scs_inference,[],[725,2])). % 67.68/67.76 cnf(729,plain, % 67.68/67.76 (E(f2(x7291,f2(x7292,f2(x7293,x7294))),f2(f2(a1,f2(f2(a3,f2(f2(a3,x7291),x7292)),x7293)),f2(a1,x7294)))), % 67.68/67.76 inference(scs_inference,[],[9,72,725,2,3])). % 67.68/67.76 cnf(733,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,x7331)),f2(a3,f2(f2(a3,x7332),x7333))),x7334),f2(x7332,f2(x7333,f2(x7334,x7331))))), % 67.68/67.76 inference(scs_inference,[],[9,728,729,2,3])). % 67.68/67.76 cnf(737,plain, % 67.68/67.76 (E(f2(f2(f2(a3,x7371),x7372),f2(x7373,x7374)),f2(f2(a1,f2(f2(a3,f2(a1,x7374)),f2(a3,f2(f2(a3,x7371),x7372)))),f2(a1,x7373)))), % 67.68/67.76 inference(scs_inference,[],[9,95,733,2,3])). % 67.68/67.76 cnf(739,plain, % 67.68/67.76 (E(f2(f2(a1,f2(f2(a3,f2(a1,x7391)),f2(a3,f2(f2(a3,x7392),x7393)))),f2(a1,x7394)),f2(f2(f2(a3,x7392),x7393),f2(x7394,x7391)))), % 67.68/67.76 inference(scs_inference,[],[737,2])). % 67.68/67.76 cnf(740,plain, % 67.68/67.76 (E(f2(x7401,x7402),f2(f2(a1,f2(a1,x7402)),f2(a1,x7401)))), % 67.68/67.76 inference(scs_inference,[],[9,25,737,2,3])). % 67.68/67.76 cnf(742,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,x7421)),f2(a1,x7422)),f2(x7422,x7421))), % 67.68/67.76 inference(scs_inference,[],[740,2])). % 67.68/67.76 cnf(743,plain, % 67.68/67.76 (E(f2(f2(a1,x7431),f2(f2(a3,f2(a1,x7432)),f2(a3,f2(f2(a3,x7433),x7434)))),f2(f2(f2(a3,x7433),x7434),f2(x7431,x7432)))), % 67.68/67.76 inference(scs_inference,[],[9,739,740,2,3])). % 67.68/67.76 cnf(746,plain, % 67.68/67.76 (E(f2(x7461,x7462),f2(f2(f2(a3,f2(a1,x7461)),a1),x7462))), % 67.68/67.76 inference(scs_inference,[],[9,743,14,2,3])). % 67.68/67.76 cnf(749,plain, % 67.68/67.76 (E(f2(x7491,f2(x7492,x7493)),f2(f2(a1,x7493),f2(f2(a3,f2(f2(a3,f2(a1,x7491)),a1)),x7492)))), % 67.68/67.76 inference(scs_inference,[],[9,746,588,2,3])). % 67.68/67.76 cnf(753,plain, % 67.68/67.76 (E(f2(x7531,x7532),f2(f2(f2(a3,f2(a1,f2(a1,x7531))),a1),f2(a1,x7532)))), % 67.68/67.76 inference(scs_inference,[],[9,749,677,2,3])). % 67.68/67.76 cnf(756,plain, % 67.68/67.76 (E(f2(x7561,x7562),f2(f2(a1,a1),f2(f2(a3,f2(a1,x7562)),f2(a3,f2(a1,x7561)))))), % 67.68/67.76 inference(scs_inference,[],[9,753,594,2,3])). % 67.68/67.76 cnf(759,plain, % 67.68/67.76 (E(f2(x7591,x7592),f2(f2(a1,a1),f2(f2(a3,f2(a1,x7591)),f2(a3,f2(a1,f2(a1,x7592))))))), % 67.68/67.76 inference(scs_inference,[],[9,756,2,3])). % 67.68/67.76 cnf(762,plain, % 67.68/67.76 (E(f2(x7621,x7622),f2(f2(a1,a1),f2(f2(a3,f2(a1,f2(a1,x7622))),f2(a3,f2(a1,f2(a1,x7621))))))), % 67.68/67.76 inference(scs_inference,[],[9,759,2,3])). % 67.68/67.76 cnf(765,plain, % 67.68/67.76 (E(f2(x7651,x7652),f2(f2(a1,a1),f2(f2(a3,f2(a1,f2(a1,x7651))),f2(a3,f2(a1,f2(a1,f2(a1,x7652)))))))), % 67.68/67.76 inference(scs_inference,[],[9,762,2,3])). % 67.68/67.76 cnf(768,plain, % 67.68/67.76 (E(f2(x7681,x7682),f2(f2(a1,a1),f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x7682))),a1)),f2(a3,f2(a1,x7681)))))), % 67.68/67.76 inference(scs_inference,[],[9,765,597,2,3])). % 67.68/67.76 cnf(771,plain, % 67.68/67.76 (E(f2(x7711,f2(f2(x7712,x7713),x7714)),f2(f2(a1,x7713),f2(f2(a3,f2(f2(a3,f2(a1,x7714)),f2(a3,x7711))),x7712)))), % 67.68/67.76 inference(scs_inference,[],[9,768,609,2,3])). % 67.68/67.76 cnf(774,plain, % 67.68/67.76 (E(f2(f2(a1,x7741),f2(f2(a3,f2(f2(a3,f2(a1,x7742)),f2(a3,x7743))),x7744)),f2(x7743,f2(f2(x7744,x7741),x7742)))), % 67.68/67.76 inference(scs_inference,[],[771,2])). % 67.68/67.76 cnf(775,plain, % 67.68/67.76 (E(f2(x7751,x7752),f2(f2(a1,x7751),f2(f2(a3,f2(a1,f2(a1,x7752))),a1)))), % 67.68/67.76 inference(scs_inference,[],[9,771,722,2,3])). % 67.68/67.76 cnf(778,plain, % 67.68/67.76 (E(f2(x7781,x7782),f2(f2(a1,f2(a1,x7782)),f2(f2(a3,f2(a1,f2(a1,x7781))),a1)))), % 67.68/67.76 inference(scs_inference,[],[9,775,2,3])). % 67.68/67.76 cnf(781,plain, % 67.68/67.76 (E(f2(x7811,x7812),f2(f2(a1,f2(a1,x7811)),f2(f2(a3,f2(a1,f2(a1,f2(a1,x7812)))),a1)))), % 67.68/67.76 inference(scs_inference,[],[9,778,2,3])). % 67.68/67.76 cnf(784,plain, % 67.68/67.76 (E(f2(x7841,x7842),f2(f2(a1,f2(a1,f2(a1,x7842))),f2(f2(a3,f2(a1,f2(a1,f2(a1,x7841)))),a1)))), % 67.68/67.76 inference(scs_inference,[],[9,781,2,3])). % 67.68/67.76 cnf(787,plain, % 67.68/67.76 (E(f2(x7871,x7872),f2(f2(a1,f2(f2(a3,f2(a1,f2(a1,x7872))),a1)),f2(a1,x7871)))), % 67.68/67.76 inference(scs_inference,[],[9,784,691,2,3])). % 67.68/67.76 cnf(790,plain, % 67.68/67.76 (E(f2(x7901,x7902),f2(f2(a1,f2(f2(a3,f2(a1,f2(a1,x7901))),a1)),f2(a1,f2(a1,x7902))))), % 67.68/67.76 inference(scs_inference,[],[9,787,2,3])). % 67.68/67.76 cnf(793,plain, % 67.68/67.76 (E(f2(x7931,x7932),f2(f2(a1,f2(f2(a3,f2(a1,f2(a1,f2(a1,x7932)))),a1)),f2(a1,f2(a1,x7931))))), % 67.68/67.76 inference(scs_inference,[],[9,790,2,3])). % 67.68/67.76 cnf(796,plain, % 67.68/67.76 (E(f2(x7961,x7962),f2(f2(f2(a3,f2(a1,f2(a1,f2(a1,x7961)))),a1),f2(a1,f2(a1,x7962))))), % 67.68/67.76 inference(scs_inference,[],[9,793,635,2,3])). % 67.68/67.76 cnf(799,plain, % 67.68/67.76 (E(f2(x7991,x7992),f2(f2(f2(a3,f2(a1,f2(a1,f2(a1,f2(a1,x7992))))),a1),f2(a1,f2(a1,x7991))))), % 67.68/67.76 inference(scs_inference,[],[9,796,2,3])). % 67.68/67.76 cnf(802,plain, % 67.68/67.76 (E(f2(x8021,x8022),f2(f2(a1,f2(a1,f2(a1,x8022))),f2(a1,f2(a1,x8021))))), % 67.68/67.76 inference(scs_inference,[],[9,799,628,2,3])). % 67.68/67.76 cnf(805,plain, % 67.68/67.76 (E(f2(x8051,f2(x8052,x8053)),f2(f2(a1,x8052),f2(f2(a3,f2(a1,x8053)),f2(a3,x8051))))), % 67.68/67.76 inference(scs_inference,[],[9,802,618,2,3])). % 67.68/67.76 cnf(809,plain, % 67.68/67.76 (E(f2(x8091,x8092),f2(f2(a1,f2(a1,x8091)),f2(a1,f2(f2(a3,f2(a1,f2(a1,x8092))),a1))))), % 67.68/67.76 inference(scs_inference,[],[9,805,702,2,3])). % 67.68/67.76 cnf(812,plain, % 67.68/67.76 (E(f2(x8121,x8122),f2(f2(a1,f2(a1,f2(a1,x8122))),f2(a1,f2(f2(a3,f2(a1,f2(a1,x8121))),a1))))), % 67.68/67.76 inference(scs_inference,[],[9,809,2,3])). % 67.68/67.76 cnf(815,plain, % 67.68/67.76 (E(f2(x8151,x8152),f2(f2(a1,f2(a1,f2(f2(a3,f2(a1,f2(a1,x8152))),a1))),f2(a1,f2(a1,x8151))))), % 67.68/67.76 inference(scs_inference,[],[9,812,709,2,3])). % 67.68/67.76 cnf(818,plain, % 67.68/67.76 (E(f2(x8181,x8182),f2(f2(a1,f2(a1,f2(a1,f2(a1,x8182)))),f2(a1,f2(a1,f2(a1,x8181)))))), % 67.68/67.76 inference(scs_inference,[],[9,815,638,2,3])). % 67.68/67.76 cnf(821,plain, % 67.68/67.76 (E(f2(x8211,x8212),f2(f2(f2(a3,f2(a1,f2(a1,x8211))),a1),f2(f2(a3,f2(a1,f2(a1,x8212))),a1)))), % 67.68/67.76 inference(scs_inference,[],[9,818,625,2,3])). % 67.68/67.76 cnf(824,plain, % 67.68/67.76 (E(f2(x8241,x8242),f2(f2(f2(a3,f2(a1,x8241)),f2(a3,f2(a1,f2(a1,x8242)))),a1))), % 67.68/67.76 inference(scs_inference,[],[9,821,667,2,3])). % 67.68/67.76 cnf(827,plain, % 67.68/67.76 (E(f2(x8271,x8272),f2(f2(f2(a3,f2(a1,f2(a1,x8272))),f2(a3,f2(a1,f2(a1,x8271)))),a1))), % 67.68/67.76 inference(scs_inference,[],[9,824,2,3])). % 67.68/67.76 cnf(830,plain, % 67.68/67.76 (E(f2(x8301,x8302),f2(f2(f2(a3,f2(a1,f2(a1,x8301))),f2(a3,f2(a1,f2(a1,f2(a1,x8302))))),a1))), % 67.68/67.76 inference(scs_inference,[],[9,827,2,3])). % 67.68/67.76 cnf(833,plain, % 67.68/67.76 (E(f2(x8331,f2(x8332,f2(x8333,x8334))),f2(f2(f2(a3,f2(a1,x8333)),f2(a3,f2(a1,x8334))),f2(a3,f2(f2(a3,x8331),x8332))))), % 67.68/67.76 inference(scs_inference,[],[9,830,54,2,3])). % 67.68/67.76 cnf(836,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,x8361)),f2(a3,f2(a1,x8362))),f2(a3,f2(f2(a3,x8363),x8364))),f2(x8363,f2(x8364,f2(x8361,x8362))))), % 67.68/67.76 inference(scs_inference,[],[833,2])). % 67.68/67.76 cnf(841,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(f2(a3,f2(a1,x8411)),f2(a3,f2(a1,x8412)))),a3),f2(f2(a3,f2(a1,x8413)),f2(a3,x8414))),f2(x8414,f2(f2(x8411,x8412),x8413)))), % 67.68/67.76 inference(scs_inference,[],[676,774,3])). % 67.68/67.76 cnf(845,plain, % 67.68/67.76 (E(f2(x8451,f2(x8452,x8453)),f2(f2(f2(a3,f2(a1,f2(a1,a1))),a1),f2(f2(a3,f2(a1,f2(x8452,x8453))),f2(a3,f2(a1,x8451)))))), % 67.68/67.76 inference(scs_inference,[],[10,686,841,2,3])). % 67.68/67.76 cnf(848,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x8481))),a1)),f2(a3,f2(a1,x8482))),f2(a3,f2(a1,x8483))),f2(f2(x8481,x8482),x8483))), % 67.68/67.76 inference(scs_inference,[],[666,596,845,2,3])). % 67.68/67.76 cnf(851,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,x8511)),f2(a3,f2(a1,x8512))),f2(a3,f2(f2(a3,f2(a1,x8513)),f2(a3,x8514)))),f2(f2(a1,f2(f2(x8511,x8512),x8513)),x8514))), % 67.68/67.76 inference(scs_inference,[],[683,611,848,2,3])). % 67.68/67.76 cnf(855,plain, % 67.68/67.76 (E(f2(x8551,f2(x8552,x8553)),f2(f2(f2(a3,f2(a1,f2(a1,x8552))),a1),f2(f2(a3,f2(a1,x8553)),f2(a3,x8551))))), % 67.68/67.76 inference(scs_inference,[],[10,529,851,2,3])). % 67.68/67.76 cnf(858,plain, % 67.68/67.76 (E(f2(x8581,f2(x8582,x8583)),f2(f2(a1,x8581),f2(a1,f2(x8582,x8583))))), % 67.68/67.76 inference(scs_inference,[],[10,153,855,2,3])). % 67.68/67.76 cnf(861,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x8611))),a1)),f2(a3,f2(a1,x8612))),f2(a3,x8613)),f2(f2(f2(a3,f2(a1,x8613)),a1),f2(x8611,x8612)))), % 67.68/67.76 inference(scs_inference,[],[624,403,858,2,3])). % 67.68/67.76 cnf(864,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,x8641)),a1),f2(x8642,x8643)),f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x8642))),a1)),f2(a3,f2(a1,x8643))),f2(a3,x8641)))), % 67.68/67.76 inference(scs_inference,[],[861,2])). % 67.68/67.76 cnf(865,plain, % 67.68/67.76 (E(f2(x8651,f2(x8652,x8653)),f2(f2(f2(a3,f2(a1,x8652)),f2(a3,f2(a1,x8653))),f2(a3,x8651)))), % 67.68/67.76 inference(scs_inference,[],[10,504,861,2,3])). % 67.68/67.76 cnf(868,plain, % 67.68/67.76 (E(f2(f2(a1,x8681),f2(a1,f2(x8682,x8683))),f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x8682))),a1)),f2(a3,f2(a1,x8683))),f2(a3,x8681)))), % 67.68/67.76 inference(scs_inference,[],[10,864,865,2,3])). % 67.68/67.76 cnf(870,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x8701))),a1)),f2(a3,f2(a1,x8702))),f2(a3,x8703)),f2(f2(a1,x8703),f2(a1,f2(x8701,x8702))))), % 67.68/67.76 inference(scs_inference,[],[868,2])). % 67.68/67.76 cnf(871,plain, % 67.68/67.76 (E(f2(x8711,f2(x8712,x8713)),f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x8712))),a1)),f2(a3,f2(a1,x8713))),f2(a3,x8711)))), % 67.68/67.76 inference(scs_inference,[],[10,533,868,2,3])). % 67.68/67.76 cnf(874,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,f2(a1,x8741))),a1),f2(f2(a3,f2(a1,x8742)),f2(a3,x8743))),f2(f2(a1,x8743),f2(a1,f2(x8741,x8742))))), % 67.68/67.76 inference(scs_inference,[],[10,870,871,2,3])). % 67.68/67.76 cnf(877,plain, % 67.68/67.76 (E(f2(x8771,f2(f2(x8772,x8773),x8774)),f2(f2(f2(a3,f2(a1,x8772)),f2(a3,f2(a1,x8773))),f2(a3,f2(f2(a3,f2(a1,x8774)),f2(a3,x8771)))))), % 67.68/67.76 inference(scs_inference,[],[10,63,874,2,3])). % 67.68/67.76 cnf(880,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,x8801)),f2(a3,f2(a1,x8802))),f2(a3,f2(f2(a3,f2(a1,x8803)),f2(a3,x8804)))),f2(x8804,f2(f2(x8801,x8802),x8803)))), % 67.68/67.76 inference(scs_inference,[],[877,2])). % 67.68/67.76 cnf(881,plain, % 67.68/67.76 (E(f2(x8811,f2(x8812,x8813)),f2(f2(a1,f2(f2(a3,f2(a1,x8813)),f2(a3,x8811))),f2(a1,x8812)))), % 67.68/67.76 inference(scs_inference,[],[10,203,877,2,3])). % 67.68/67.76 cnf(896,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,f2(a1,x8961))),a1),f2(f2(a3,f2(a1,x8962)),f2(a3,f2(a1,x8963)))),f2(f2(x8961,x8962),x8963))), % 67.68/67.76 inference(scs_inference,[],[10,848,3])). % 67.68/67.76 cnf(898,plain, % 67.68/67.76 (E(f2(f2(x8981,x8982),x8983),f2(f2(f2(a3,f2(a1,f2(a1,x8981))),a1),f2(f2(a3,f2(a1,x8982)),f2(a3,f2(a1,x8983)))))), % 67.68/67.76 inference(scs_inference,[],[896,2])). % 67.68/67.76 cnf(899,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,x8991)),f2(a1,f2(f2(a3,f2(a1,x8992)),f2(a3,f2(a1,x8993))))),f2(f2(x8991,x8992),x8993))), % 67.68/67.76 inference(scs_inference,[],[10,896,2,3])). % 67.68/67.76 cnf(901,plain, % 67.68/67.76 (E(f2(f2(x9011,x9012),x9013),f2(f2(a1,f2(a1,x9011)),f2(a1,f2(f2(a3,f2(a1,x9012)),f2(a3,f2(a1,x9013))))))), % 67.68/67.76 inference(scs_inference,[],[899,2])). % 67.68/67.76 cnf(902,plain, % 67.68/67.76 (E(f2(x9021,f2(x9022,x9023)),f2(f2(f2(a3,f2(a1,f2(a1,f2(a3,x9021)))),a1),f2(f2(a3,f2(a1,x9022)),f2(a3,f2(a1,x9023)))))), % 67.68/67.76 inference(scs_inference,[],[10,898,899,2,3])). % 67.68/67.76 cnf(905,plain, % 67.68/67.76 (E(f2(x9051,f2(x9052,x9053)),f2(f2(a1,f2(a1,f2(a3,x9051))),f2(a1,f2(f2(a3,f2(a1,x9052)),f2(a3,f2(a1,x9053))))))), % 67.68/67.76 inference(scs_inference,[],[10,901,902,2,3])). % 67.68/67.76 cnf(908,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,a1)),f2(a1,f2(f2(a3,f2(a1,f2(x9081,x9082))),f2(a3,f2(a1,x9083))))),f2(f2(f2(a3,x9083),x9081),x9082))), % 67.68/67.76 inference(scs_inference,[],[10,905,684,2,3])). % 67.68/67.76 cnf(910,plain, % 67.68/67.76 (E(f2(f2(f2(a3,x9101),x9102),x9103),f2(f2(a1,f2(a1,a1)),f2(a1,f2(f2(a3,f2(a1,f2(x9102,x9103))),f2(a3,f2(a1,x9101))))))), % 67.68/67.76 inference(scs_inference,[],[908,2])). % 67.68/67.76 cnf(911,plain, % 67.68/67.76 (E(f2(x9111,f2(x9112,x9113)),f2(f2(f2(a3,f2(a1,f2(a1,f2(f2(a3,x9111),x9112)))),a1),f2(a1,x9113)))), % 67.68/67.76 inference(scs_inference,[],[10,908,753,2,3])). % 67.68/67.76 cnf(914,plain, % 67.68/67.76 (E(f2(x9141,f2(x9142,x9143)),f2(f2(a1,f2(a1,a1)),f2(a1,f2(f2(a3,f2(a1,f2(x9142,x9143))),f2(a3,f2(a1,x9141))))))), % 67.68/67.76 inference(scs_inference,[],[10,910,911,2,3])). % 67.68/67.76 cnf(917,plain, % 67.68/67.76 (E(f2(f2(a1,x9171),f2(f2(a3,f2(a1,x9172)),f2(a3,f2(f2(a3,f2(a1,x9173)),f2(a3,x9174))))),f2(f2(a1,f2(f2(x9171,x9172),x9173)),x9174))), % 67.68/67.76 inference(scs_inference,[],[10,914,851,2,3])). % 67.68/67.76 cnf(919,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,f2(a1,x9191))),a1),f2(f2(a3,f2(a1,x9192)),f2(a3,x9193))),f2(f2(f2(a3,f2(a1,x9193)),a1),f2(x9191,x9192)))), % 67.68/67.76 inference(scs_inference,[],[10,861,3])). % 67.68/67.76 cnf(921,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,x9211)),a1),f2(x9212,x9213)),f2(f2(f2(a3,f2(a1,f2(a1,x9212))),a1),f2(f2(a3,f2(a1,x9213)),f2(a3,x9211))))), % 67.68/67.76 inference(scs_inference,[],[919,2])). % 67.68/67.76 cnf(922,plain, % 67.68/67.76 (E(f2(f2(a1,f2(a1,x9221)),f2(a1,f2(f2(a3,f2(a1,x9222)),f2(a3,x9223)))),f2(f2(f2(a3,f2(a1,x9223)),a1),f2(x9221,x9222)))), % 67.68/67.76 inference(scs_inference,[],[10,919,2,3])). % 67.68/67.76 cnf(924,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(a1,x9241)),a1),f2(x9242,x9243)),f2(f2(a1,f2(a1,x9242)),f2(a1,f2(f2(a3,f2(a1,x9243)),f2(a3,x9241)))))), % 67.68/67.76 inference(scs_inference,[],[922,2])). % 67.68/67.76 cnf(980,plain, % 67.68/67.76 (E(f2(f2(a1,f2(f2(x9801,x9802),x9803)),x9804),f2(f2(a1,x9801),f2(f2(a3,f2(a1,x9802)),f2(a3,f2(f2(a3,f2(a1,x9803)),f2(a3,x9804))))))), % 67.68/67.76 inference(scs_inference,[],[917,2])). % 67.68/67.76 cnf(981,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(x9811,x9812)),x9813),x9814),f2(f2(f2(a3,f2(a1,x9811)),f2(a3,f2(a1,x9812))),f2(a3,f2(a1,f2(x9813,x9814)))))), % 67.68/67.76 inference(scs_inference,[],[11,917,865,2,3])). % 67.68/67.76 cnf(985,plain, % 67.68/67.76 (E(f2(f2(f2(a3,x9851),f2(x9852,x9853)),x9854),f2(f2(a1,x9852),f2(f2(a3,f2(a1,x9853)),f2(a3,f2(f2(a3,f2(a1,x9854)),f2(a3,x9851))))))), % 67.68/67.76 inference(scs_inference,[],[11,980,981,2,3])). % 67.68/67.76 cnf(989,plain, % 67.68/67.76 (E(f2(f2(f2(a3,f2(x9891,x9892)),x9893),x9894),f2(f2(a1,f2(f2(a3,f2(a1,x9892)),f2(a3,f2(a1,f2(x9893,x9894))))),f2(a1,x9891)))), % 67.68/67.76 inference(scs_inference,[],[11,985,881,2,3])). % 67.68/67.76 cnf(993,plain, % 67.68/67.76 (E(f2(f2(f2(a3,x9931),x9932),x9933),f2(f2(a1,x9933),f2(f2(a3,f2(f2(a3,f2(a1,x9931)),a1)),x9932)))), % 67.68/67.76 inference(scs_inference,[],[11,989,588,2,3])). % 67.68/67.77 cnf(996,plain, % 67.68/67.77 (E(f2(f2(f2(a3,x9961),x9962),x9963),f2(f2(a1,a1),f2(f2(a3,f2(a1,f2(x9962,x9963))),f2(a3,f2(a1,x9961)))))), % 67.68/67.77 inference(scs_inference,[],[11,993,594,2,3])). % 67.68/67.77 cnf(1008,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,f2(a1,x10081))),a1),f2(f2(a3,f2(a1,x10082)),f2(a3,x10083))),f2(f2(a1,f2(a1,f2(x10081,x10082))),f2(a1,x10083)))), % 67.68/67.77 inference(scs_inference,[],[13,921,3,2])). % 67.68/67.77 cnf(1009,plain, % 67.68/67.77 (E(f2(f2(a1,f2(a1,f2(x10091,x10092))),f2(a1,x10093)),f2(f2(a1,f2(a1,x10091)),f2(a1,f2(f2(a3,f2(a1,x10092)),f2(a3,x10093)))))), % 67.68/67.77 inference(scs_inference,[],[13,924,3])). % 67.68/67.77 cnf(1015,plain, % 67.68/67.77 (E(f2(f2(a1,f2(f2(a3,f2(a1,x10151)),f2(a3,f2(f2(a3,f2(a1,x10152)),f2(a3,x10153))))),f2(a1,x10154)),f2(x10153,f2(f2(x10154,x10151),x10152)))), % 67.68/67.77 inference(scs_inference,[],[13,880,3])). % 67.68/67.77 cnf(1018,plain, % 67.68/67.77 (E(f2(f2(a1,f2(x10181,x10182)),x10183),f2(f2(a1,f2(a1,f2(a3,x10183))),f2(a1,f2(f2(a3,f2(a1,x10181)),f2(a3,f2(a1,x10182))))))), % 67.68/67.77 inference(scs_inference,[],[13,901,1015,2,3])). % 67.68/67.77 cnf(1021,plain, % 67.68/67.77 (E(f2(f2(a1,f2(a1,f2(x10211,x10212))),f2(a1,x10213)),f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x10211))),a1)),f2(a3,f2(a1,x10212))),f2(a3,x10213)))), % 67.68/67.77 inference(scs_inference,[],[13,864,1018,2,3])). % 67.68/67.77 cnf(1023,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x10231))),a1)),f2(a3,f2(a1,x10232))),f2(a3,x10233)),f2(f2(a1,f2(a1,f2(x10231,x10232))),f2(a1,x10233)))), % 67.68/67.77 inference(scs_inference,[],[1021,2])). % 67.68/67.77 cnf(1024,plain, % 67.68/67.77 (E(f2(f2(a1,f2(f2(a3,f2(a1,x10241)),f2(a3,x10242))),f2(f2(a3,f2(a1,f2(a1,x10243))),a1)),f2(f2(a1,x10242),f2(a1,f2(x10243,x10241))))), % 67.68/67.77 inference(scs_inference,[],[13,870,1021,2,3])). % 67.68/67.77 cnf(1027,plain, % 67.68/67.77 (E(f2(f2(a1,f2(f2(a3,f2(a1,x10271)),f2(a3,x10272))),f2(f2(a3,f2(a1,f2(a1,x10273))),a1)),f2(f2(a1,f2(a1,f2(x10273,x10271))),f2(a1,x10272)))), % 67.68/67.77 inference(scs_inference,[],[13,1023,1024,2,3])). % 67.68/67.77 cnf(1030,plain, % 67.68/67.77 (E(f2(f2(a1,f2(x10301,x10302)),x10303),f2(f2(f2(a3,f2(a1,f2(a1,x10301))),a1),f2(f2(a3,f2(a1,x10302)),f2(a3,x10303))))), % 67.68/67.77 inference(scs_inference,[],[13,529,1027,2,3])). % 67.68/67.77 cnf(1032,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,f2(a1,x10321))),a1),f2(f2(a3,f2(a1,x10322)),f2(a3,x10323))),f2(f2(a1,f2(x10321,x10322)),x10323))), % 67.68/67.77 inference(scs_inference,[],[1030,2])). % 67.68/67.77 cnf(1033,plain, % 67.68/67.77 (E(f2(f2(a1,f2(x10331,x10332)),x10333),f2(f2(f2(a3,f2(a1,x10331)),f2(a3,f2(a1,x10332))),f2(a3,x10333)))), % 67.68/67.77 inference(scs_inference,[],[13,504,1030,2,3])). % 67.68/67.77 cnf(1035,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,x10351)),f2(a3,f2(a1,x10352))),f2(a3,x10353)),f2(f2(a1,f2(x10351,x10352)),x10353))), % 67.68/67.77 inference(scs_inference,[],[1033,2])). % 67.68/67.77 cnf(1036,plain, % 67.68/67.77 (E(f2(f2(a1,f2(a1,f2(f2(a3,f2(a1,x10361)),f2(a3,x10362)))),f2(a1,f2(a1,x10363))),f2(f2(a1,f2(x10363,x10361)),x10362))), % 67.68/67.77 inference(scs_inference,[],[13,1032,1033,2,3])). % 67.68/67.77 cnf(1039,plain, % 67.68/67.77 (E(f2(f2(a1,f2(f2(a3,f2(a1,x10391)),f2(a3,x10392))),f2(a1,x10393)),f2(f2(a1,f2(x10393,x10391)),x10392))), % 67.68/67.77 inference(scs_inference,[],[13,1035,1036,2,3])). % 67.68/67.77 cnf(1042,plain, % 67.68/67.77 (E(f2(f2(a1,f2(x10421,x10422)),x10423),f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x10421))),a1)),f2(a3,f2(a1,x10422))),f2(a3,x10423)))), % 67.68/67.77 inference(scs_inference,[],[13,533,1039,2,3])). % 67.68/67.77 cnf(1044,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x10441))),a1)),f2(a3,f2(a1,x10442))),f2(a3,x10443)),f2(f2(a1,f2(x10441,x10442)),x10443))), % 67.68/67.77 inference(scs_inference,[],[1042,2])). % 67.68/67.77 cnf(1045,plain, % 67.68/67.77 (E(f2(f2(a1,f2(x10451,x10452)),x10453),f2(f2(a1,f2(a1,x10451)),f2(a1,f2(f2(a3,f2(a1,x10452)),f2(a3,x10453)))))), % 67.68/67.77 inference(scs_inference,[],[13,206,1042,2,3])). % 67.68/67.77 cnf(1048,plain, % 67.68/67.77 (E(f2(f2(a1,f2(f2(a3,f2(a1,x10481)),f2(a3,x10482))),f2(f2(a3,f2(a1,f2(a1,x10483))),a1)),f2(f2(a1,f2(x10483,x10481)),x10482))), % 67.68/67.77 inference(scs_inference,[],[13,1044,1045,2,3])). % 67.68/67.77 cnf(1051,plain, % 67.68/67.77 (E(f2(f2(a1,f2(x10511,x10512)),f2(f2(a3,f2(a1,x10513)),f2(a3,x10514))),f2(f2(f2(a3,f2(a1,x10514)),a1),f2(f2(x10511,x10512),x10513)))), % 67.68/67.77 inference(scs_inference,[],[13,449,1048,2,3])). % 67.68/67.77 cnf(1054,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,x10541)),a1),f2(f2(x10542,x10543),x10544)),f2(f2(a1,f2(x10542,x10543)),f2(f2(a3,f2(a1,x10544)),f2(a3,x10541))))), % 67.68/67.77 inference(scs_inference,[],[1051,2])). % 67.68/67.77 cnf(1118,plain, % 67.68/67.77 (E(f2(f2(a1,f2(a1,f2(x11181,x11182))),f2(a1,x11183)),f2(f2(a1,f2(f2(a3,f2(a1,x11182)),f2(a3,x11183))),f2(a1,x11181)))), % 67.68/67.77 inference(scs_inference,[],[14,1008,3,2])). % 67.68/67.77 cnf(1126,plain, % 67.68/67.77 (E(f2(f2(x11261,x11262),x11263),f2(f2(f2(a3,f2(a1,x11261)),f2(a3,f2(a1,x11262))),f2(a3,f2(a1,x11263))))), % 67.68/67.77 inference(scs_inference,[],[14,504,3])). % 67.68/67.77 cnf(1129,plain, % 67.68/67.77 (E(f2(f2(f2(x11291,x11292),x11293),x11294),f2(f2(f2(a3,f2(a1,x11291)),f2(a3,f2(a1,x11292))),f2(a3,f2(f2(a3,f2(a1,x11293)),f2(a3,f2(a1,x11294))))))), % 67.68/67.77 inference(scs_inference,[],[14,63,3])). % 67.68/67.77 cnf(1133,plain, % 67.68/67.77 (E(f2(f2(x11331,x11332),x11333),f2(f2(a1,f2(f2(a3,f2(a1,x11332)),f2(a3,f2(a1,x11333)))),f2(a1,x11331)))), % 67.68/67.77 inference(scs_inference,[],[14,203,1129,2,3])). % 67.68/67.77 cnf(1136,plain, % 67.68/67.77 (E(f2(f2(x11361,x11362),x11363),f2(f2(f2(a3,f2(a1,f2(a3,f2(a1,x11363)))),f2(a3,f2(a1,x11361))),f2(a3,f2(a1,x11362))))), % 67.68/67.77 inference(scs_inference,[],[14,1126,1133,2,3])). % 67.68/67.77 cnf(1139,plain, % 67.68/67.77 (E(f2(f2(x11391,x11392),x11393),f2(f2(f2(a3,f2(a1,a1)),f2(a3,f2(a1,x11393))),f2(a3,f2(a1,f2(x11391,x11392)))))), % 67.68/67.77 inference(scs_inference,[],[14,1136,981,2,3])). % 67.68/67.77 cnf(1141,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,a1)),f2(a3,f2(a1,x11411))),f2(a3,f2(a1,f2(x11412,x11413)))),f2(f2(x11412,x11413),x11411))), % 67.68/67.77 inference(scs_inference,[],[1139,2])). % 67.68/67.77 cnf(1142,plain, % 67.68/67.77 (E(f2(f2(x11421,x11422),x11423),f2(f2(a1,f2(f2(a3,f2(a1,x11421)),f2(a3,f2(a1,x11422)))),f2(a1,f2(a3,f2(a1,x11423)))))), % 67.68/67.77 inference(scs_inference,[],[14,1139,1133,2,3])). % 67.68/67.77 cnf(1145,plain, % 67.68/67.77 (E(f2(f2(x11451,x11452),x11453),f2(f2(a1,f2(f2(a3,f2(a1,x11453)),f2(a3,f2(a1,f2(x11451,x11452))))),f2(a1,a1)))), % 67.68/67.77 inference(scs_inference,[],[14,1142,989,2,3])). % 67.68/67.77 cnf(1147,plain, % 67.68/67.77 (E(f2(f2(a1,f2(f2(a3,f2(a1,x11471)),f2(a3,f2(a1,f2(x11472,x11473))))),f2(a1,a1)),f2(f2(x11472,x11473),x11471))), % 67.68/67.77 inference(scs_inference,[],[1145,2])). % 67.68/67.77 cnf(1148,plain, % 67.68/67.77 (E(f2(f2(a1,f2(f2(a3,f2(a1,f2(x11481,x11482))),f2(a3,f2(a1,x11483)))),f2(a1,a1)),f2(f2(f2(a3,x11483),x11481),x11482))), % 67.68/67.77 inference(scs_inference,[],[14,1145,684,2,3])). % 67.68/67.77 cnf(1150,plain, % 67.68/67.77 (E(f2(f2(f2(a3,x11501),x11502),x11503),f2(f2(a1,f2(f2(a3,f2(a1,f2(x11502,x11503))),f2(a3,f2(a1,x11501)))),f2(a1,a1)))), % 67.68/67.77 inference(scs_inference,[],[1148,2])). % 67.68/67.77 cnf(1151,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,x11511)),f2(a3,f2(f2(a3,f2(a1,x11512)),f2(a3,x11513)))),x11514),f2(f2(a1,f2(f2(x11514,x11511),x11512)),x11513))), % 67.68/67.77 inference(scs_inference,[],[14,1148,851,2,3])). % 67.68/67.77 cnf(1154,plain, % 67.68/67.77 (E(f2(f2(a1,f2(f2(x11541,x11542),x11543)),x11544),f2(f2(f2(a3,f2(a1,x11542)),f2(a3,f2(f2(a3,f2(a1,x11543)),f2(a3,x11544)))),x11541))), % 67.68/67.77 inference(scs_inference,[],[1151,2])). % 67.68/67.77 cnf(1155,plain, % 67.68/67.77 (E(f2(f2(x11551,x11552),x11553),f2(f2(a1,f2(f2(a3,f2(a1,f2(x11551,x11552))),f2(a3,f2(a1,f2(a1,x11553))))),f2(a1,a1)))), % 67.68/67.77 inference(scs_inference,[],[14,1150,1151,2,3])). % 67.68/67.77 cnf(1158,plain, % 67.68/67.77 (E(f2(f2(a1,f2(f2(a3,f2(a1,x11581)),f2(a3,x11582))),f2(a1,x11583)),f2(f2(f2(a3,f2(a1,x11582)),a1),f2(x11583,x11581)))), % 67.68/67.77 inference(scs_inference,[],[14,1155,919,2,3])). % 67.68/67.77 cnf(1160,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,x11601)),a1),f2(x11602,x11603)),f2(f2(a1,f2(f2(a3,f2(a1,x11603)),f2(a3,x11601))),f2(a1,x11602)))), % 67.68/67.77 inference(scs_inference,[],[1158,2])). % 67.68/67.77 cnf(1170,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,f2(a1,a1))),a1),f2(f2(a3,f2(a1,x11701)),f2(a3,f2(a1,f2(x11702,x11703))))),f2(f2(x11702,x11703),x11701))), % 67.68/67.77 inference(scs_inference,[],[17,1147,3])). % 67.68/67.77 cnf(1173,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,f2(a3,f2(a1,f2(x11731,x11732))))),f2(a3,f2(a1,a1))),f2(a3,f2(a1,x11733))),f2(f2(x11731,x11732),x11733))), % 67.68/67.77 inference(scs_inference,[],[17,1141,1170,2,3])). % 67.68/67.77 cnf(1176,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,x11761)),a1),f2(f2(x11762,x11763),x11764)),f2(f2(f2(a3,f2(a1,x11763)),f2(a3,f2(f2(a3,f2(a1,x11764)),f2(a3,x11761)))),x11762))), % 67.68/67.77 inference(scs_inference,[],[17,1154,1173,2,3])). % 67.68/67.77 cnf(1179,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,x11791)),f2(a3,f2(f2(a3,f2(a1,x11792)),f2(a3,x11793)))),x11794),f2(f2(f2(a3,f2(a1,x11793)),a1),f2(f2(x11794,x11791),x11792)))), % 67.68/67.77 inference(scs_inference,[],[1176,2])). % 67.68/67.77 cnf(1180,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,f2(x11801,x11802))),f2(a3,f2(a1,x11803))),a1),f2(f2(f2(a3,f2(a1,x11802)),f2(a3,x11803)),x11801))), % 67.68/67.77 inference(scs_inference,[],[17,407,1176,2,3])). % 67.68/67.77 cnf(1182,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,x11821)),f2(a3,x11822)),x11823),f2(f2(f2(a3,f2(a1,f2(x11823,x11821))),f2(a3,f2(a1,x11822))),a1))), % 67.68/67.77 inference(scs_inference,[],[1180,2])). % 67.68/67.77 cnf(1183,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,x11831)),f2(a3,f2(a1,x11832))),f2(a3,f2(f2(a3,f2(a1,x11833)),f2(a3,x11834)))),f2(f2(f2(a3,f2(a1,x11834)),a1),f2(f2(x11831,x11832),x11833)))), % 67.68/67.77 inference(scs_inference,[],[17,1179,1180,2,3])). % 67.68/67.77 cnf(1187,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,f2(x11871,x11872))),f2(a3,f2(a1,x11873))),a1),f2(f2(f2(a3,f2(a1,f2(a1,x11872))),a1),f2(f2(a3,x11873),x11871)))), % 67.68/67.77 inference(scs_inference,[],[17,421,1183,2,3])). % 67.68/67.77 cnf(1190,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,f2(x11901,x11902))),f2(a3,f2(a1,x11903))),a1),f2(f2(a1,f2(f2(a3,f2(a1,x11902)),f2(a3,x11903))),f2(a1,x11901)))), % 67.68/67.77 inference(scs_inference,[],[17,1160,1187,2,3])). % 67.68/67.77 cnf(1193,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,f2(a1,x11931))),a1),f2(a1,f2(x11932,x11933))),f2(f2(a1,f2(f2(a3,f2(a1,x11933)),f2(a3,x11931))),f2(a1,x11932)))), % 67.68/67.77 inference(scs_inference,[],[17,1118,1190,2,3])). % 67.68/67.77 cnf(1196,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,x11961)),f2(a3,f2(a1,x11962))),f2(a3,x11963)),f2(f2(f2(a3,f2(a1,f2(x11961,x11962))),f2(a3,f2(a1,x11963))),a1))), % 67.68/67.77 inference(scs_inference,[],[17,1182,1193,2,3])). % 67.68/67.77 cnf(1199,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,f2(x11991,x11992))),f2(a3,f2(a1,x11993))),a1),f2(f2(f2(a3,f2(a1,x11991)),f2(a3,f2(a1,x11992))),f2(a3,x11993)))), % 67.68/67.77 inference(scs_inference,[],[1196,2])). % 67.68/67.77 cnf(1200,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,x12001)),f2(a3,f2(a1,f2(x12002,x12003)))),x12004),f2(f2(f2(a3,f2(a1,x12003)),f2(a3,f2(x12004,x12001))),x12002))), % 67.68/67.77 inference(scs_inference,[],[17,350,1196,2,3])). % 67.68/67.77 cnf(1203,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,x12031)),f2(a3,f2(x12032,x12033))),x12034),f2(f2(f2(a3,f2(a1,x12033)),f2(a3,f2(a1,f2(x12034,x12031)))),x12032))), % 67.68/67.77 inference(scs_inference,[],[1200,2])). % 67.68/67.77 cnf(1204,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,a1)),f2(a3,f2(a1,f2(x12041,x12042)))),f2(a3,f2(a1,x12043))),f2(f2(f2(a3,f2(a1,x12041)),f2(a3,f2(a1,x12042))),f2(a3,x12043)))), % 67.68/67.77 inference(scs_inference,[],[17,1199,1200,2,3])). % 67.68/67.77 cnf(1207,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,x12071)),f2(a3,f2(a1,x12072))),f2(a3,f2(x12073,x12074))),f2(f2(f2(a3,f2(a1,x12074)),f2(a3,f2(a1,f2(x12071,x12072)))),x12073))), % 67.68/67.77 inference(scs_inference,[],[17,1203,1204,2,3])). % 67.68/67.77 cnf(1210,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,x12101)),f2(a3,f2(a1,f2(x12102,x12103)))),x12104),f2(f2(f2(a3,f2(a1,x12102)),f2(a3,f2(a1,x12103))),f2(a3,f2(x12104,x12101))))), % 67.68/67.77 inference(scs_inference,[],[1207,2])). % 67.68/67.77 cnf(1211,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,x12111)),f2(a3,x12112)),x12113),f2(f2(a1,f2(f2(a3,f2(a1,f2(x12113,x12111))),f2(a3,f2(a1,x12112)))),f2(a1,a1)))), % 67.68/67.77 inference(scs_inference,[],[17,1150,1207,2,3])). % 67.68/67.77 cnf(1215,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,x12151)),f2(a3,f2(a1,x12152))),f2(a3,f2(a1,f2(x12153,x12154)))),f2(f2(f2(a3,f2(a1,x12153)),f2(a3,f2(a1,x12154))),f2(a3,f2(x12151,x12152))))), % 67.68/67.77 inference(scs_inference,[],[17,1210,1211,2,3])). % 67.68/67.77 cnf(1219,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,x12191)),f2(a3,x12192)),x12193),f2(f2(a1,f2(a1,a1)),f2(a1,f2(f2(a3,f2(a1,f2(x12193,x12191))),f2(a3,f2(a1,x12192))))))), % 67.68/67.77 inference(scs_inference,[],[17,910,1215,2,3])). % 67.68/67.77 cnf(1223,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,x12231)),a1),f2(f2(x12232,x12233),x12234)),f2(f2(a1,x12232),f2(f2(a3,f2(a1,x12233)),f2(a3,f2(f2(a3,f2(a1,x12234)),f2(a3,x12231))))))), % 67.68/67.77 inference(scs_inference,[],[17,980,1219,2,3])). % 67.68/67.77 cnf(1227,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,f2(a3,x12271))),f2(a3,f2(a1,x12272))),f2(a3,f2(a1,x12273))),f2(f2(a1,f2(x12272,x12273)),x12271))), % 67.68/67.77 inference(scs_inference,[],[17,1035,1223,2,3])). % 67.68/67.77 cnf(1229,plain, % 67.68/67.77 (E(f2(f2(a1,f2(x12291,x12292)),x12293),f2(f2(f2(a3,f2(a1,f2(a3,x12293))),f2(a3,f2(a1,x12291))),f2(a3,f2(a1,x12292))))), % 67.68/67.77 inference(scs_inference,[],[1227,2])). % 67.68/67.77 cnf(1230,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,f2(f2(x12301,x12302),x12303))),f2(a3,f2(a1,x12304))),a1),f2(f2(a1,f2(x12301,x12302)),f2(f2(a3,f2(a1,x12303)),f2(a3,x12304))))), % 67.68/67.77 inference(scs_inference,[],[17,1054,1227,2,3])). % 67.68/67.77 cnf(1233,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,x12331)),a1),f2(x12332,x12333)),f2(f2(f2(a3,f2(a1,f2(a3,x12331))),f2(a3,f2(a1,x12332))),f2(a3,f2(a1,x12333))))), % 67.68/67.77 inference(scs_inference,[],[17,1229,1230,2,3])). % 67.68/67.77 cnf(1237,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,f2(x12371,x12372))),f2(a3,f2(a1,x12373))),a1),f2(f2(a1,f2(a1,x12371)),f2(a1,f2(f2(a3,f2(a1,x12372)),f2(a3,x12373)))))), % 67.68/67.77 inference(scs_inference,[],[17,924,1233,2,3])). % 67.68/67.77 cnf(1240,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,a1)),f2(a3,f2(a1,f2(x12401,x12402)))),f2(a3,f2(a1,x12403))),f2(f2(f2(a3,x12403),x12401),x12402))), % 67.68/67.77 inference(scs_inference,[],[17,593,1237,2,3])). % 67.68/67.77 cnf(1242,plain, % 67.68/67.77 (E(f2(f2(f2(a3,x12421),x12422),x12423),f2(f2(f2(a3,f2(a1,a1)),f2(a3,f2(a1,f2(x12422,x12423)))),f2(a3,f2(a1,x12421))))), % 67.68/67.77 inference(scs_inference,[],[1240,2])). % 67.68/67.77 cnf(1243,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,x12431)),f2(a3,f2(a1,x12432))),f2(a3,f2(x12433,x12434))),f2(f2(f2(a3,f2(a1,f2(x12431,x12432))),x12433),x12434))), % 67.68/67.77 inference(scs_inference,[],[17,347,1240,2,3])). % 67.68/67.77 cnf(1247,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,x12471)),f2(a3,x12472)),x12473),f2(f2(f2(a3,f2(a1,a1)),f2(a3,f2(a1,f2(x12473,x12471)))),f2(a3,f2(a1,x12472))))), % 67.68/67.77 inference(scs_inference,[],[17,1242,1243,2,3])). % 67.68/67.77 cnf(1251,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,x12511)),f2(a3,f2(a1,f2(x12512,x12513)))),x12514),f2(f2(a1,x12513),f2(f2(a3,f2(x12514,x12511)),x12512)))), % 67.68/67.77 inference(scs_inference,[],[17,343,1247,2,3])). % 67.68/67.77 cnf(1255,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,x12551)),f2(a3,f2(x12552,x12553))),x12554),f2(f2(a1,x12553),f2(f2(a3,f2(a1,f2(x12554,x12551))),x12552)))), % 67.68/67.77 inference(scs_inference,[],[17,385,1251,2,3])). % 67.68/67.77 cnf(1259,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,x12591)),f2(a3,f2(a1,x12592))),f2(a3,f2(x12593,x12594))),f2(f2(a1,x12594),f2(f2(a3,f2(a1,f2(x12591,x12592))),x12593)))), % 67.68/67.77 inference(scs_inference,[],[17,1255,2,3])). % 67.68/67.77 cnf(1263,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,x12631)),f2(a3,f2(x12632,x12633))),x12634),f2(f2(a1,f2(f2(a3,f2(a1,f2(x12634,x12631))),x12632)),f2(a1,x12633)))), % 67.68/67.77 inference(scs_inference,[],[17,339,1259,2,3])). % 67.68/67.77 cnf(1267,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,x12671)),f2(a3,f2(a1,f2(x12672,x12673)))),x12674),f2(f2(a1,f2(f2(a3,f2(x12674,x12671)),x12672)),f2(a1,x12673)))), % 67.68/67.77 inference(scs_inference,[],[17,358,1263,2,3])). % 67.68/67.77 cnf(1271,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,x12711)),f2(a3,f2(a1,x12712))),f2(a3,f2(a1,f2(x12713,x12714)))),f2(f2(a1,f2(f2(a3,f2(x12711,x12712)),x12713)),f2(a1,x12714)))), % 67.68/67.77 inference(scs_inference,[],[17,1267,2,3])). % 67.68/67.77 cnf(1275,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,x12751)),f2(a3,f2(a1,x12752))),f2(a3,x12753)),f2(f2(f2(a3,f2(a1,f2(a1,x12753))),a1),f2(a1,f2(x12751,x12752))))), % 67.68/67.77 inference(scs_inference,[],[17,368,1271,2,3])). % 67.68/67.77 cnf(1279,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,x12791)),f2(a3,f2(a1,x12792))),f2(a3,x12793)),f2(f2(a1,f2(a1,f2(a1,x12793))),f2(a1,f2(a1,f2(a1,f2(x12791,x12792))))))), % 67.68/67.77 inference(scs_inference,[],[17,372,1275,2,3])). % 67.68/67.77 cnf(1283,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,f2(x12831,x12832))),f2(a3,f2(a1,x12833))),a1),f2(f2(a1,f2(f2(a3,x12833),x12831)),f2(a1,x12832)))), % 67.68/67.77 inference(scs_inference,[],[17,376,1279,2,3])). % 67.68/67.77 cnf(1286,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,f2(x12861,x12862))),f2(a3,f2(a1,x12863))),a1),f2(f2(a1,f2(a1,x12862)),f2(a1,f2(f2(a3,x12863),x12861))))), % 67.68/67.77 inference(scs_inference,[],[17,416,1283,2,3])). % 67.68/67.77 cnf(1289,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,f2(x12891,x12892))),f2(a3,f2(a1,x12893))),a1),f2(f2(a1,f2(a1,f2(f2(a3,x12893),x12891))),f2(a1,f2(a1,x12892))))), % 67.68/67.77 inference(scs_inference,[],[17,422,1286,2,3])). % 67.68/67.77 cnf(1292,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,f2(a1,x12921))),a1),f2(a1,f2(x12922,x12923))),f2(f2(a1,f2(a1,x12922)),f2(a1,f2(f2(a3,f2(a1,x12923)),f2(a3,x12921)))))), % 67.68/67.77 inference(scs_inference,[],[17,1009,1289,2,3])). % 67.68/67.77 cnf(1295,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,x12951)),f2(a3,x12952)),x12953),f2(f2(a1,a1),f2(f2(a3,f2(a1,f2(x12953,x12951))),f2(a3,f2(a1,x12952)))))), % 67.68/67.77 inference(scs_inference,[],[17,1292,996,2,3])). % 67.68/67.77 cnf(1298,plain, % 67.68/67.77 (E(f2(f2(a1,a1),f2(f2(a3,f2(a1,f2(x12981,x12982))),f2(a3,f2(a1,x12983)))),f2(f2(f2(a3,f2(a1,x12982)),f2(a3,x12983)),x12981))), % 67.68/67.77 inference(scs_inference,[],[1295,2])). % 67.68/67.77 cnf(1345,plain, % 67.68/67.77 (~E(f2(a5,f2(a4,a6)),f2(f2(f2(f2(f2(a3,f2(a1,a3)),f2(f2(a3,a3),a1)),a4),a5),a6))), % 67.68/67.77 inference(scs_inference,[],[8,742,4,5,2])). % 67.68/67.77 cnf(1380,plain, % 67.68/67.77 (E(f2(f2(f2(f2(a3,f2(a1,x13801)),f2(a3,f2(a1,x13802))),a1),x13803),f2(f2(x13802,x13801),x13803))), % 67.68/67.77 inference(scs_inference,[],[669,4])). % 67.68/67.77 cnf(1515,plain, % 67.68/67.77 (~E(f2(f2(f2(f2(f2(a3,f2(a1,a3)),f2(f2(a3,a3),a1)),a4),a5),a6),f2(f2(a1,a6),f2(f2(a3,a5),a4)))), % 67.68/67.77 inference(scs_inference,[],[1380,694,1345,4,5,3,2])). % 67.68/67.77 cnf(1603,plain, % 67.68/67.77 (E(f2(f2(x16031,x16032),x16033),f2(f2(f2(a1,x16032),x16031),x16033))), % 67.68/67.77 inference(scs_inference,[],[9,4])). % 67.68/67.77 cnf(1605,plain, % 67.68/67.77 (~E(f2(f2(a1,a6),f2(f2(f2(f2(a3,f2(a1,a3)),f2(f2(a3,a3),a1)),a4),a5)),f2(f2(a1,a6),f2(f2(a3,a5),a4)))), % 67.68/67.77 inference(scs_inference,[],[9,1515,4,5,3])). % 67.68/67.77 cnf(1608,plain, % 67.68/67.77 (~E(f2(f2(a1,a6),f2(f2(a3,a5),a4)),f2(f2(a1,a6),f2(f2(f2(f2(a3,f2(a1,a3)),f2(f2(a3,a3),a1)),a4),a5)))), % 67.68/67.77 inference(scs_inference,[],[1603,1605,4,2])). % 67.68/67.77 cnf(1658,plain, % 67.68/67.77 (E(f2(f2(x16581,f2(x16582,x16583)),x16584),f2(f2(f2(f2(a3,x16581),x16582),x16583),x16584))), % 67.68/67.77 inference(scs_inference,[],[10,5,4])). % 67.68/67.77 cnf(1793,plain, % 67.68/67.77 (~E(f2(f2(a3,a5),a4),f2(f2(f2(f2(a3,f2(a1,a3)),f2(f2(a3,a3),a1)),a4),a5))), % 67.68/67.77 inference(scs_inference,[],[1608,5])). % 67.68/67.77 cnf(1794,plain, % 67.68/67.77 (~E(f2(f2(f2(f2(a3,f2(a1,a3)),f2(f2(a3,a3),a1)),a4),a5),f2(f2(a3,a5),a4))), % 67.68/67.77 inference(scs_inference,[],[1608,5,2])). % 67.68/67.77 cnf(1813,plain, % 67.68/67.77 (E(f2(f2(f2(x18131,x18132),x18133),x18134),f2(f2(f2(f2(a3,f2(a1,x18133)),x18131),x18132),x18134))), % 67.68/67.77 inference(scs_inference,[],[14,4])). % 67.68/67.77 cnf(1815,plain, % 67.68/67.77 (~E(f2(f2(f2(a3,f2(a1,a5)),f2(f2(a3,f2(a1,a3)),f2(f2(a3,a3),a1))),a4),f2(f2(a3,a5),a4))), % 67.68/67.77 inference(scs_inference,[],[14,1794,4,5,3])). % 67.68/67.77 cnf(1818,plain, % 67.68/67.77 (~E(f2(f2(a3,f2(a1,a5)),f2(f2(a3,f2(a1,a3)),f2(f2(a3,a3),a1))),f2(a3,a5))), % 67.68/67.77 inference(scs_inference,[],[1815,4])). % 67.68/67.77 cnf(1819,plain, % 67.68/67.77 (~E(f2(f2(f2(a3,f2(a1,a4)),a3),a5),f2(f2(f2(f2(a3,f2(a1,a3)),f2(f2(a3,a3),a1)),a4),a5))), % 67.68/67.77 inference(scs_inference,[],[14,1793,1815,4,3])). % 67.68/67.77 cnf(1821,plain, % 67.68/67.77 (~E(f2(a3,a5),f2(f2(a3,f2(a1,a5)),f2(f2(a3,f2(a1,a3)),f2(f2(a3,a3),a1))))), % 67.68/67.77 inference(scs_inference,[],[14,1793,1815,4,3,2])). % 67.68/67.77 cnf(1822,plain, % 67.68/67.77 (~E(f2(f2(f2(f2(a3,f2(a1,a3)),f2(f2(a3,a3),a1)),a4),a5),f2(f2(f2(a3,f2(a1,a4)),a3),a5))), % 67.68/67.77 inference(scs_inference,[],[1819,2])). % 67.68/67.77 cnf(1824,plain, % 67.68/67.77 (~E(f2(f2(f2(a3,f2(a1,f2(f2(a3,f2(a1,a3)),f2(f2(a3,a3),a1)))),a3),f2(a1,a5)),f2(a3,a5))), % 67.68/67.77 inference(scs_inference,[],[14,1818,1298,1819,2,4,3])). % 67.68/67.77 cnf(1827,plain, % 67.68/67.77 (~E(f2(f2(f2(a3,f2(a1,a3)),f2(f2(a3,a3),a1)),a4),f2(f2(a3,f2(a1,a4)),a3))), % 67.68/67.77 inference(scs_inference,[],[1824,1822,2,4])). % 67.68/67.77 cnf(1830,plain, % 67.68/67.77 (~E(f2(f2(a3,f2(a1,a4)),a3),f2(f2(f2(a3,f2(a1,a3)),f2(f2(a3,a3),a1)),a4))), % 67.68/67.77 inference(scs_inference,[],[1827,2])). % 67.68/67.77 cnf(1832,plain, % 67.68/67.77 (~E(f2(f2(f2(a3,f2(a1,a3)),a1),a5),f2(f2(a3,f2(a1,a5)),f2(f2(a3,f2(a1,a3)),f2(f2(a3,a3),a1))))), % 67.68/67.77 inference(scs_inference,[],[1821,1827,836,746,2,4,3])). % 67.68/67.77 cnf(1836,plain, % 67.68/67.77 (~E(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),f2(f2(f2(a3,f2(a1,a3)),f2(f2(a3,a3),a1)),a4))), % 67.68/67.77 inference(scs_inference,[],[14,1830,1832,2,3])). % 67.68/67.77 cnf(1838,plain, % 67.68/67.77 (~E(f2(f2(f2(a3,f2(a1,a3)),f2(f2(a3,a3),a1)),a4),f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)))), % 67.68/67.77 inference(scs_inference,[],[1836,2])). % 67.68/67.77 cnf(1839,plain, % 67.68/67.77 (~E(f2(f2(f2(a3,f2(a1,f2(a1,a4))),f2(a3,f2(a1,a3))),a3),f2(f2(f2(a3,f2(a1,a3)),f2(f2(a3,a3),a1)),a4))), % 67.68/67.77 inference(scs_inference,[],[14,1836,2,3])). % 67.68/67.77 cnf(1841,plain, % 67.68/67.77 (~E(f2(f2(f2(a3,f2(a1,a3)),f2(f2(a3,a3),a1)),a4),f2(f2(f2(a3,f2(a1,f2(a1,a4))),f2(a3,f2(a1,a3))),a3))), % 67.68/67.77 inference(scs_inference,[],[1839,2])). % 67.68/67.77 cnf(1842,plain, % 67.68/67.77 (~E(f2(f2(f2(a3,f2(a1,a4)),f2(a3,f2(a1,a3))),f2(f2(a3,a3),a1)),f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)))), % 67.68/67.77 inference(scs_inference,[],[14,1838,1839,2,3])). % 67.68/67.77 cnf(1844,plain, % 67.68/67.77 (~E(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),f2(f2(f2(a3,f2(a1,a4)),f2(a3,f2(a1,a3))),f2(f2(a3,a3),a1)))), % 67.68/67.77 inference(scs_inference,[],[1842,2])). % 67.68/67.77 cnf(1845,plain, % 67.68/67.77 (~E(f2(f2(f2(a3,f2(a1,f2(f2(a3,a3),a1))),f2(a3,f2(a1,a4))),f2(a3,f2(a1,a3))),f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)))), % 67.68/67.77 inference(scs_inference,[],[14,1842,2,3])). % 67.68/67.77 cnf(1849,plain, % 67.68/67.77 (~E(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),f2(f2(f2(a3,f2(a1,f2(f2(a3,a3),a1))),f2(a3,f2(a1,a4))),f2(a3,f2(a1,a3))))), % 67.68/67.77 inference(scs_inference,[],[1845,2])). % 67.68/67.77 cnf(1850,plain, % 67.68/67.77 (~E(f2(f2(f2(a3,f2(a1,f2(a1,a4))),f2(a3,f2(a1,a3))),a3),f2(f2(f2(a3,f2(a1,a4)),f2(a3,f2(a1,a3))),f2(f2(a3,a3),a1)))), % 67.68/67.77 inference(scs_inference,[],[14,1844,1845,2,3])). % 67.68/67.77 cnf(1853,plain, % 67.68/67.77 (~E(f2(f2(f2(a3,f2(a1,f2(a1,a4))),f2(a3,f2(a1,a3))),a3),f2(f2(f2(a3,f2(a1,f2(f2(a3,a3),a1))),f2(a3,f2(a1,a4))),f2(a3,f2(a1,a3))))), % 67.68/67.77 inference(scs_inference,[],[14,1849,1850,2,3])). % 67.68/67.77 cnf(1860,plain, % 67.68/67.77 (~E(f2(f2(f2(f2(a3,a3),a1),a4),a3),f2(f2(f2(a3,f2(a1,f2(a1,a4))),f2(a3,f2(a1,a3))),a3))), % 67.68/67.77 inference(scs_inference,[],[17,1841,1853,2,3])). % 67.68/67.77 cnf(1861,plain, % 67.68/67.77 (E(f2(f2(f2(a3,f2(a1,x18611)),x18612),x18613),f2(f2(x18612,x18613),x18611))), % 67.68/67.77 inference(rename_variables,[],[17])). % 67.68/67.77 cnf(1863,plain, % 67.68/67.77 (E(f2(f2(f2(f2(a3,f2(a1,x18631)),x18632),x18633),x18634),f2(f2(f2(x18632,x18633),x18631),x18634))), % 67.68/67.77 inference(scs_inference,[],[17,1861,1841,1853,2,3,5,4])). % 67.68/67.77 cnf(1864,plain, % 67.68/67.77 (~E(f2(f2(f2(a3,a3),a1),a4),f2(f2(a3,f2(a1,f2(a1,a4))),f2(a3,f2(a1,a3))))), % 67.68/67.77 inference(scs_inference,[],[1860,4])). % 67.68/67.77 cnf(1865,plain, % 67.68/67.77 (~E(f2(f2(f2(a3,f2(a1,f2(a1,a4))),f2(a3,f2(a1,a3))),a3),f2(f2(f2(f2(a3,a3),a1),a4),a3))), % 67.68/67.77 inference(scs_inference,[],[1860,4,2])). % 67.68/67.77 cnf(1870,plain, % 67.68/67.77 (~E(f2(f2(f2(f2(a3,f2(a1,a1)),a3),a3),a4),f2(f2(a3,f2(a1,f2(a1,a4))),f2(a3,f2(a1,a3))))), % 67.68/67.77 inference(scs_inference,[],[1864,1863,1813,4,2,3])). % 67.68/67.77 cnf(1873,plain, % 67.68/67.77 (~E(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),f2(f2(f2(f2(a3,a3),a1),a4),a3))), % 67.68/67.77 inference(scs_inference,[],[17,1865,1870,2,3])). % 67.68/67.77 cnf(1876,plain, % 67.68/67.77 ($false), % 67.68/67.77 inference(scs_inference,[],[17,1873,1658,2,3]), % 67.68/67.77 ['proof']). % 67.68/67.77 % SZS output end Proof % 67.68/67.77 % Total time :67.070000s %------------------------------------------------------------------------------