%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : COL060-3 : 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 : n013.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Jun 24 04:44:58 EDT 2024 % Result : Unsatisfiable 77.48s 77.51s % Output : CNFRefutation 77.56s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : COL060-3 : TPTP v8.2.0. Bugfixed v1.2.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.33 % Computer : n013.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Tue Jun 18 16:31:09 EDT 2024 % 0.13/0.33 % CPUTime : % 0.51/0.57 start to proof:theBenchmark % 77.48/77.50 %------------------------------------------- % 77.48/77.50 % File :CSE---1.7 % 77.48/77.50 % Problem :theBenchmark % 77.48/77.50 % Transform :cnf % 77.48/77.50 % Format :tptp:raw % 77.48/77.50 % Command :java -jar mcs_scs.jar %d %s % 77.48/77.50 % 77.48/77.50 % Result :Theorem 76.900000s % 77.48/77.50 % Output :CNFRefutation 76.900000s % 77.48/77.50 %------------------------------------------- % 77.48/77.51 %-------------------------------------------------------------------------- % 77.48/77.51 % File : COL060-3 : TPTP v8.2.0. Bugfixed v1.2.0. % 77.48/77.51 % Domain : Combinatory Logic % 77.48/77.51 % Problem : Find combinator equivalent to Q from B and T % 77.48/77.51 % Version : [WM88] (equality) axioms. % 77.48/77.51 % Theorem formulation : The combinator is provided and checked. % 77.48/77.51 % English : Construct from B and T alone a combinator that behaves as the % 77.48/77.51 % combinator Q does, where ((Bx)y)z = x(yz), (Tx)y = yx, % 77.48/77.51 % ((Qx)y)z = y(xz). % 77.48/77.51 % 77.48/77.51 % Refs : [WM88] Wos & McCune (1988), Challenge Problems Focusing on Eq % 77.48/77.51 % : [WW+90] Wos et al. (1990), Automated Reasoning Contributes to % 77.48/77.51 % Source : [TPTP] % 77.48/77.51 % Names : % 77.48/77.51 % 77.48/77.51 % Status : Unsatisfiable % 77.48/77.51 % Rating : 0.05 v8.2.0, 0.12 v8.1.0, 0.15 v7.5.0, 0.12 v7.4.0, 0.17 v7.3.0, 0.11 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.10 v5.5.0, 0.11 v5.4.0, 0.00 v5.2.0, 0.07 v5.1.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 % 77.48/77.51 % Syntax : Number of clauses : 3 ( 3 unt; 0 nHn; 1 RR) % 77.48/77.51 % Number of literals : 3 ( 3 equ; 1 neg) % 77.48/77.51 % Maximal clause size : 1 ( 1 avg) % 77.48/77.51 % Maximal term depth : 9 ( 2 avg) % 77.48/77.51 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty) % 77.48/77.51 % Number of functors : 6 ( 6 usr; 5 con; 0-2 aty) % 77.48/77.51 % Number of variables : 5 ( 0 sgn) % 77.48/77.51 % SPC : CNF_UNS_RFO_PEQ_UEQ % 77.48/77.51 % 77.48/77.51 % Comments : % 77.48/77.51 % Bugfixes : v1.2.0 : Redundant [fgh]_substitution axioms removed. % 77.48/77.51 %-------------------------------------------------------------------------- % 77.48/77.51 cnf(b_definition,axiom, % 77.48/77.51 apply(apply(apply(b,X),Y),Z) = apply(X,apply(Y,Z)) ). % 77.48/77.51 % 77.48/77.51 cnf(t_definition,axiom, % 77.48/77.51 apply(apply(t,X),Y) = apply(Y,X) ). % 77.48/77.51 % 77.48/77.51 %----This is the q equivalent % 77.48/77.51 cnf(prove_q_combinator,negated_conjecture, % 77.48/77.51 apply(apply(apply(apply(apply(b,apply(apply(b,apply(t,b)),b)),t),x),y),z) != apply(y,apply(x,z)) ). % 77.48/77.51 % 77.48/77.51 %-------------------------------------------------------------------------- % 77.48/77.51 %------------------------------------------- % 77.48/77.51 % Proof found % 77.48/77.51 % SZS status Theorem for theBenchmark % 77.48/77.51 % SZS output start Proof % 77.48/77.51 %ClaNum:8(EqnAxiom:5) % 77.48/77.51 %VarNum:10(SingletonVarNum:5) % 77.48/77.51 %MaxLitNum:1 % 77.48/77.51 %MaxfuncDepth:8 % 77.48/77.51 %SharedTerms:16 % 77.48/77.51 %goalClause: 8 % 77.48/77.51 %singleGoalClaCount:1 % 77.48/77.51 [8]~E(f2(f2(f2(f2(f2(a3,f2(f2(a3,f2(a1,a3)),a3)),a1),a4),a5),a6),f2(a5,f2(a4,a6))) % 77.48/77.51 [6]E(f2(f2(a1,x61),x62),f2(x62,x61)) % 77.48/77.51 [7]E(f2(f2(f2(a3,x71),x72),x73),f2(x71,f2(x72,x73))) % 77.48/77.51 %EqnAxiom % 77.48/77.51 [1]E(x11,x11) % 77.48/77.51 [2]E(x22,x21)+~E(x21,x22) % 77.48/77.51 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 77.48/77.51 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43)) % 77.48/77.51 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52)) % 77.48/77.51 % 77.48/77.51 %------------------------------------------- % 77.48/77.53 cnf(9,plain, % 77.48/77.53 (E(f2(x91,x92),f2(f2(a1,x92),x91))), % 77.48/77.53 inference(scs_inference,[],[6,2])). % 77.48/77.53 cnf(10,plain, % 77.48/77.53 (E(f2(x101,f2(x102,x103)),f2(f2(f2(a3,x101),x102),x103))), % 77.48/77.53 inference(scs_inference,[],[7,2])). % 77.48/77.53 cnf(11,plain, % 77.48/77.53 (E(f2(f2(f2(a3,x111),x112),x113),f2(f2(a1,f2(x112,x113)),x111))), % 77.48/77.53 inference(scs_inference,[],[9,7,2,3])). % 77.48/77.53 cnf(13,plain, % 77.48/77.53 (E(f2(f2(a1,f2(x131,x132)),x133),f2(f2(f2(a3,x133),x131),x132))), % 77.48/77.53 inference(scs_inference,[],[11,2])). % 77.48/77.53 cnf(14,plain, % 77.48/77.53 (E(f2(f2(x141,x142),x143),f2(f2(f2(a3,f2(a1,x143)),x141),x142))), % 77.48/77.53 inference(scs_inference,[],[10,9,11,2,3])). % 77.48/77.53 cnf(17,plain, % 77.48/77.53 (E(f2(f2(f2(a3,f2(a1,x171)),x172),x173),f2(f2(x172,x173),x171))), % 77.48/77.53 inference(scs_inference,[],[14,2])). % 77.48/77.53 cnf(18,plain, % 77.48/77.53 (E(f2(f2(a1,f2(x181,f2(x182,x183))),x184),f2(f2(f2(a3,f2(f2(a3,x184),x181)),x182),x183))), % 77.48/77.53 inference(scs_inference,[],[13,10,14,2,3])). % 77.48/77.53 cnf(21,plain, % 77.48/77.53 (E(f2(f2(f2(a3,f2(f2(a3,x211),x212)),x213),x214),f2(f2(a1,f2(x212,f2(x213,x214))),x211))), % 77.48/77.53 inference(scs_inference,[],[18,2])). % 77.48/77.53 cnf(22,plain, % 77.48/77.53 (E(f2(f2(a1,f2(x221,x222)),f2(a1,x223)),f2(f2(x221,x222),x223))), % 77.48/77.53 inference(scs_inference,[],[17,13,18,2,3])). % 77.48/77.53 cnf(25,plain, % 77.48/77.53 (E(f2(f2(x251,x252),x253),f2(f2(a1,f2(x251,x252)),f2(a1,x253)))), % 77.48/77.53 inference(scs_inference,[],[22,2])). % 77.48/77.53 cnf(26,plain, % 77.48/77.53 (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))), % 77.48/77.53 inference(scs_inference,[],[21,17,22,2,3])). % 77.48/77.53 cnf(29,plain, % 77.48/77.53 (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))), % 77.48/77.53 inference(scs_inference,[],[26,2])). % 77.48/77.53 cnf(30,plain, % 77.48/77.53 (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)))), % 77.48/77.53 inference(scs_inference,[],[25,21,26,2,3])). % 77.48/77.53 cnf(32,plain, % 77.48/77.53 (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))), % 77.48/77.53 inference(scs_inference,[],[30,2])). % 77.48/77.53 cnf(33,plain, % 77.48/77.53 (E(f2(f2(x331,f2(x332,x333)),x334),f2(f2(f2(a3,f2(a1,x333)),f2(a3,f2(f2(a3,f2(a1,x334)),x331))),x332))), % 77.48/77.53 inference(scs_inference,[],[29,25,30,2,3])). % 77.48/77.53 cnf(36,plain, % 77.48/77.53 (E(f2(f2(f2(a3,f2(a1,x361)),f2(a3,f2(f2(a3,f2(a1,x362)),x363))),x364),f2(f2(x363,f2(x364,x361)),x362))), % 77.48/77.53 inference(scs_inference,[],[33,2])). % 77.48/77.53 cnf(37,plain, % 77.48/77.53 (E(f2(f2(f2(a3,f2(a1,f2(a1,x371))),a1),f2(a1,f2(x372,f2(x373,x374)))),f2(f2(f2(a3,f2(f2(a3,x371),x372)),x373),x374))), % 77.48/77.53 inference(scs_inference,[],[32,17,33,2,3])). % 77.48/77.53 cnf(39,plain, % 77.48/77.53 (E(f2(f2(f2(a3,f2(f2(a3,x391),x392)),x393),x394),f2(f2(f2(a3,f2(a1,f2(a1,x391))),a1),f2(a1,f2(x392,f2(x393,x394)))))), % 77.48/77.53 inference(scs_inference,[],[37,2])). % 77.48/77.53 cnf(40,plain, % 77.48/77.53 (E(f2(f2(f2(a3,f2(a1,f2(x401,x402))),f2(a3,f2(f2(a3,f2(a1,x403)),a1))),x404),f2(f2(f2(a3,f2(a1,x402)),f2(a3,f2(f2(a3,x403),x404))),x401))), % 77.48/77.53 inference(scs_inference,[],[36,29,37,2,3])). % 77.48/77.53 cnf(43,plain, % 77.48/77.53 (E(f2(f2(f2(a3,f2(a1,x431)),f2(a3,f2(f2(a3,x432),x433))),x434),f2(f2(f2(a3,f2(a1,f2(x434,x431))),f2(a3,f2(f2(a3,f2(a1,x432)),a1))),x433))), % 77.48/77.53 inference(scs_inference,[],[40,2])). % 77.48/77.53 cnf(44,plain, % 77.48/77.53 (E(f2(f2(a1,x441),f2(f2(a3,f2(f2(a3,f2(a1,x442)),x443)),x444)),f2(f2(x443,f2(x444,x441)),x442))), % 77.48/77.53 inference(scs_inference,[],[36,10,40,2,3])). % 77.48/77.53 cnf(47,plain, % 77.48/77.53 (E(f2(f2(x471,f2(x472,x473)),x474),f2(f2(a1,x473),f2(f2(a3,f2(f2(a3,f2(a1,x474)),x471)),x472)))), % 77.48/77.53 inference(scs_inference,[],[44,2])). % 77.48/77.53 cnf(48,plain, % 77.48/77.53 (E(f2(f2(f2(a3,f2(a1,x481)),f2(a3,f2(f2(a3,x482),x483))),x484),f2(f2(a1,x483),f2(f2(a3,f2(a1,f2(x484,x481))),f2(a3,f2(f2(a3,f2(a1,x482)),a1)))))), % 77.48/77.53 inference(scs_inference,[],[43,9,44,2,3])). % 77.48/77.53 cnf(51,plain, % 77.48/77.53 (E(f2(f2(x511,f2(x512,x513)),x514),f2(f2(a1,f2(a1,x513)),f2(a1,f2(f2(a3,f2(f2(a3,f2(a1,x514)),x511)),x512))))), % 77.48/77.53 inference(scs_inference,[],[47,25,48,2,3])). % 77.48/77.53 cnf(53,plain, % 77.48/77.53 (E(f2(f2(a1,f2(a1,x531)),f2(a1,f2(f2(a3,f2(f2(a3,f2(a1,x532)),x533)),x534))),f2(f2(x533,f2(x534,x531)),x532))), % 77.48/77.53 inference(scs_inference,[],[51,2])). % 77.48/77.53 cnf(62,plain, % 77.48/77.53 (E(f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x621))),a1)),a1),f2(x622,f2(x623,x624))),f2(f2(f2(a3,f2(f2(a3,x621),x622)),x623),x624))), % 77.48/77.53 inference(scs_inference,[],[39,10,3,2])). % 77.48/77.53 cnf(68,plain, % 77.48/77.53 (E(f2(f2(f2(a3,f2(f2(a3,f2(a1,x681)),a1)),x682),f2(x683,x684)),f2(f2(f2(a3,f2(a1,x684)),f2(a3,f2(f2(a3,x681),x682))),x683))), % 77.48/77.53 inference(scs_inference,[],[43,17,3,2])). % 77.48/77.53 cnf(75,plain, % 77.48/77.53 (E(f2(f2(x751,f2(x752,x753)),x754),f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x754))),a1)),x751),f2(x752,x753)))), % 77.48/77.53 inference(scs_inference,[],[68,36,3,2])). % 77.48/77.53 cnf(76,plain, % 77.48/77.53 (E(f2(f2(a1,f2(f2(a3,f2(f2(a3,f2(a1,x761)),x762)),x763)),f2(a1,x764)),f2(f2(x762,f2(x763,x764)),x761))), % 77.48/77.53 inference(scs_inference,[],[53,9,3])). % 77.48/77.53 cnf(78,plain, % 77.48/77.53 (E(f2(f2(x781,f2(x782,x783)),x784),f2(f2(a1,f2(f2(a3,f2(f2(a3,f2(a1,x784)),x781)),x782)),f2(a1,x783)))), % 77.48/77.53 inference(scs_inference,[],[76,2])). % 77.48/77.53 cnf(79,plain, % 77.48/77.53 (E(f2(f2(x791,f2(x792,x793)),x794),f2(f2(f2(a3,f2(a1,f2(a1,f2(a1,f2(a1,x794))))),a1),f2(a1,f2(a1,f2(x791,f2(x792,x793))))))), % 77.48/77.53 inference(scs_inference,[],[75,39,76,2,3])). % 77.48/77.53 cnf(81,plain, % 77.48/77.53 (E(f2(f2(f2(a3,f2(a1,f2(a1,f2(a1,f2(a1,x811))))),a1),f2(a1,f2(a1,f2(x812,f2(x813,x814))))),f2(f2(x812,f2(x813,x814)),x811))), % 77.48/77.53 inference(scs_inference,[],[79,2])). % 77.48/77.53 cnf(82,plain, % 77.48/77.53 (E(f2(f2(x821,f2(x822,x823)),x824),f2(f2(a1,x822),f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x823))),a1)),f2(a3,f2(f2(a3,f2(a1,x824)),x821)))))), % 77.48/77.53 inference(scs_inference,[],[78,47,79,2,3])). % 77.48/77.53 cnf(84,plain, % 77.48/77.53 (E(f2(f2(a1,x841),f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x842))),a1)),f2(a3,f2(f2(a3,f2(a1,x843)),x844)))),f2(f2(x844,f2(x841,x842)),x843))), % 77.48/77.53 inference(scs_inference,[],[82,2])). % 77.48/77.53 cnf(85,plain, % 77.48/77.53 (E(f2(f2(f2(a3,f2(a1,f2(a1,f2(a1,f2(a1,x851))))),a1),f2(a1,f2(a1,f2(a1,f2(x852,x853))))),f2(f2(f2(a3,x851),x852),x853))), % 77.48/77.53 inference(scs_inference,[],[81,13,82,2,3])). % 77.48/77.53 cnf(88,plain, % 77.48/77.53 (E(f2(f2(f2(a3,x881),x882),x883),f2(f2(f2(a3,f2(a1,f2(a1,f2(a1,f2(a1,x881))))),a1),f2(a1,f2(a1,f2(a1,f2(x882,x883))))))), % 77.48/77.53 inference(scs_inference,[],[85,2])). % 77.48/77.53 cnf(95,plain, % 77.48/77.53 (E(f2(f2(a1,f2(a1,f2(a1,f2(a1,f2(x951,x952))))),f2(a1,f2(a1,f2(a1,x953)))),f2(f2(f2(a3,x953),x951),x952))), % 77.48/77.53 inference(scs_inference,[],[88,17,3,2])). % 77.48/77.53 cnf(98,plain, % 77.48/77.53 (E(f2(f2(a1,x981),f2(f2(a3,x982),x983)),f2(f2(a1,f2(a1,f2(a1,f2(a1,f2(x983,x981))))),f2(a1,f2(a1,f2(a1,x982)))))), % 77.48/77.53 inference(scs_inference,[],[95,9,3,2])). % 77.48/77.53 cnf(99,plain, % 77.48/77.53 (E(f2(f2(a1,x991),f2(f2(a3,x992),x993)),f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x992))),a1)),a1),f2(x993,x991)))), % 77.48/77.53 inference(scs_inference,[],[98,32,3])). % 77.48/77.53 cnf(101,plain, % 77.48/77.53 (E(f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x1011))),a1)),a1),f2(x1012,x1013)),f2(f2(a1,x1013),f2(f2(a3,x1011),x1012)))), % 77.48/77.53 inference(scs_inference,[],[98,32,3,2])). % 77.48/77.53 cnf(105,plain, % 77.48/77.53 (E(f2(f2(a1,x1051),f2(f2(a3,x1052),x1053)),f2(f2(a1,f2(x1053,x1051)),x1052))), % 77.48/77.53 inference(scs_inference,[],[101,75,3,2])). % 77.48/77.53 cnf(106,plain, % 77.48/77.53 (E(f2(f2(a1,x1061),f2(f2(a3,x1062),x1063)),f2(f2(a1,f2(f2(a3,f2(f2(a3,f2(a1,x1062)),a1)),x1063)),f2(a1,x1061)))), % 77.48/77.53 inference(scs_inference,[],[105,78,3])). % 77.48/77.53 cnf(108,plain, % 77.48/77.53 (E(f2(f2(a1,f2(f2(a3,f2(f2(a3,f2(a1,x1081)),a1)),x1082)),f2(a1,x1083)),f2(f2(a1,x1083),f2(f2(a3,x1081),x1082)))), % 77.48/77.53 inference(scs_inference,[],[105,78,3,2])). % 77.48/77.53 cnf(111,plain, % 77.48/77.53 (E(f2(f2(f2(a3,f2(a1,x1111)),f2(a3,x1112)),x1113),f2(f2(a1,f2(f2(a3,f2(f2(a3,f2(a1,x1112)),a1)),x1113)),f2(a1,x1111)))), % 77.48/77.53 inference(scs_inference,[],[108,10,3,2])). % 77.48/77.53 cnf(112,plain, % 77.48/77.53 (E(f2(f2(f2(a3,f2(a1,x1121)),f2(a3,x1122)),x1123),f2(f2(a1,f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x1121))),a1)),f2(a3,f2(f2(a3,f2(a1,x1122)),a1)))),f2(a1,x1123)))), % 77.48/77.53 inference(scs_inference,[],[111,78,3])). % 77.48/77.53 cnf(114,plain, % 77.48/77.53 (E(f2(f2(a1,f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x1141))),a1)),f2(a3,f2(f2(a3,f2(a1,x1142)),a1)))),f2(a1,x1143)),f2(f2(f2(a3,f2(a1,x1141)),f2(a3,x1142)),x1143))), % 77.48/77.53 inference(scs_inference,[],[112,2])). % 77.48/77.53 cnf(118,plain, % 77.48/77.53 (E(f2(f2(f2(a3,f2(a1,x1181)),f2(a3,f2(a1,x1182))),f2(a3,f2(f2(a3,f2(a1,x1183)),a1))),f2(f2(f2(a3,f2(a1,x1182)),f2(a3,x1183)),x1181))), % 77.48/77.53 inference(scs_inference,[],[114,111,3])). % 77.48/77.53 cnf(121,plain, % 77.48/77.53 (E(f2(f2(f2(a3,f2(a1,x1211)),f2(a3,x1212)),x1213),f2(f2(f2(a3,f2(a1,x1213)),f2(a3,f2(a1,x1211))),f2(a3,f2(f2(a3,f2(a1,x1212)),a1))))), % 77.48/77.53 inference(scs_inference,[],[118,2])). % 77.48/77.53 cnf(127,plain, % 77.48/77.53 (E(f2(f2(a1,f2(f2(a3,f2(a1,x1271)),f2(a3,f2(a1,x1272)))),f2(a1,f2(a3,f2(f2(a3,f2(a1,x1273)),a1)))),f2(f2(f2(a3,f2(a1,x1272)),f2(a3,x1273)),x1271))), % 77.48/77.53 inference(scs_inference,[],[121,25,3,2])). % 77.48/77.53 cnf(130,plain, % 77.48/77.53 (E(f2(f2(f2(a3,x1301),x1302),x1303),f2(f2(a1,f2(f2(a3,f2(a1,x1302)),f2(a3,f2(a1,x1303)))),f2(a1,f2(a3,f2(f2(a3,f2(a1,x1301)),a1)))))), % 77.48/77.53 inference(scs_inference,[],[127,17,3,2])). % 77.48/77.53 cnf(138,plain, % 77.48/77.53 (E(f2(f2(a1,f2(f2(a3,f2(f2(a3,x1381),x1382)),x1383)),f2(a1,x1384)),f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x1381))),a1)),a1),f2(x1382,f2(x1383,x1384))))), % 77.48/77.53 inference(scs_inference,[],[62,25,3,2])). % 77.48/77.53 cnf(141,plain, % 77.48/77.53 (E(f2(f2(a1,f2(x1411,x1412)),f2(f2(a3,x1413),x1414)),f2(f2(a1,f2(f2(a3,f2(f2(a3,x1413),x1414)),x1411)),f2(a1,x1412)))), % 77.48/77.53 inference(scs_inference,[],[138,101,3,2])). % 77.48/77.53 cnf(142,plain, % 77.48/77.53 (E(f2(f2(a1,f2(f2(a3,f2(f2(a3,f2(a1,x1421)),a1)),x1422)),f2(f2(a3,f2(a1,f2(a1,x1423))),a1)),f2(f2(f2(a3,f2(a1,x1423)),f2(a3,x1421)),x1422))), % 77.48/77.53 inference(scs_inference,[],[141,114,3])). % 77.48/77.53 cnf(145,plain, % 77.48/77.53 (E(f2(f2(f2(a3,f2(a1,x1451)),f2(a3,x1452)),x1453),f2(f2(a1,f2(f2(a3,f2(f2(a3,f2(a1,x1452)),a1)),x1453)),f2(f2(a3,f2(a1,f2(a1,x1451))),a1)))), % 77.48/77.53 inference(scs_inference,[],[142,2])). % 77.48/77.53 cnf(156,plain, % 77.48/77.53 (E(f2(f2(a1,f2(a3,f2(f2(a3,f2(a1,x1561)),a1))),f2(f2(a3,f2(a1,x1562)),f2(a3,f2(a1,x1563)))),f2(f2(f2(a3,f2(a1,x1563)),f2(a3,x1561)),x1562))), % 77.48/77.53 inference(scs_inference,[],[121,9,3,2])). % 77.48/77.53 cnf(159,plain, % 77.48/77.53 (E(f2(f2(a1,f2(f2(a3,f2(a1,x1591)),f2(a3,x1592))),f2(a1,x1593)),f2(f2(a1,f2(a3,f2(f2(a3,f2(a1,x1592)),a1))),f2(f2(a3,f2(a1,x1593)),f2(a3,f2(a1,x1591)))))), % 77.48/77.53 inference(scs_inference,[],[156,25,3,2])). % 77.48/77.53 cnf(168,plain, % 77.48/77.53 (E(f2(f2(f2(a3,f2(f2(a3,f2(a1,x1681)),f2(a3,x1682))),x1683),x1684),f2(f2(a1,f2(a3,f2(f2(a3,f2(a1,x1682)),a1))),f2(f2(a3,f2(a1,f2(x1683,x1684))),f2(a3,f2(a1,x1681)))))), % 77.48/77.53 inference(scs_inference,[],[156,10,3,2])). % 77.48/77.53 cnf(176,plain, % 77.48/77.53 (E(f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(x1761,x1762))),f2(a3,f2(a1,x1763)))),a3),f2(f2(a3,f2(a1,x1764)),a1)),f2(f2(f2(a3,f2(f2(a3,f2(a1,x1763)),f2(a3,x1764))),x1761),x1762))), % 77.48/77.53 inference(scs_inference,[],[168,13,3,2])). % 77.48/77.53 cnf(182,plain, % 77.48/77.53 (E(f2(f2(f2(a3,f2(a1,f2(a1,f2(a1,f2(a1,x1821))))),a1),f2(a1,f2(a1,f2(f2(a3,f2(a1,x1822)),f2(x1823,x1824))))),f2(f2(f2(x1823,x1824),x1821),x1822))), % 77.48/77.53 inference(scs_inference,[],[81,17,3])). % 77.48/77.53 cnf(185,plain, % 77.48/77.53 (E(f2(f2(f2(x1851,x1852),x1853),x1854),f2(f2(f2(a3,f2(a1,f2(a1,f2(a1,f2(a1,x1853))))),a1),f2(a1,f2(a1,f2(f2(a3,f2(a1,x1854)),f2(x1851,x1852))))))), % 77.48/77.53 inference(scs_inference,[],[182,2])). % 77.48/77.53 cnf(186,plain, % 77.48/77.53 (E(f2(f2(a1,f2(x1861,x1862)),f2(f2(a3,f2(a1,x1863)),a1)),f2(f2(a1,x1862),f2(f2(a3,x1863),x1861)))), % 77.48/77.53 inference(scs_inference,[],[108,141,182,2,3])). % 77.48/77.53 cnf(189,plain, % 77.48/77.53 (E(f2(f2(a1,x1891),f2(f2(a3,x1892),x1893)),f2(f2(a1,f2(x1893,x1891)),f2(f2(a3,f2(a1,x1892)),a1)))), % 77.48/77.53 inference(scs_inference,[],[186,2])). % 77.48/77.53 cnf(190,plain, % 77.48/77.53 (E(f2(f2(f2(a3,x1901),x1902),x1903),f2(f2(f2(a3,f2(a1,f2(a3,f2(f2(a3,f2(a1,x1901)),a1)))),f2(a3,f2(a1,x1902))),f2(a3,f2(a1,x1903))))), % 77.48/77.53 inference(scs_inference,[],[130,13,186,2,3])). % 77.48/77.53 cnf(193,plain, % 77.48/77.53 (E(f2(f2(a1,x1931),f2(f2(a3,x1932),x1933)),f2(f2(a1,f2(a1,f2(a1,f2(a1,f2(a1,f2(x1933,x1931)))))),f2(a1,f2(a1,f2(a1,f2(a1,x1932))))))), % 77.48/77.53 inference(scs_inference,[],[189,98,190,2,3])). % 77.48/77.53 cnf(195,plain, % 77.48/77.53 (E(f2(f2(a1,f2(a1,f2(a1,f2(a1,f2(a1,f2(x1951,x1952)))))),f2(a1,f2(a1,f2(a1,f2(a1,x1953))))),f2(f2(a1,x1952),f2(f2(a3,x1953),x1951)))), % 77.48/77.53 inference(scs_inference,[],[193,2])). % 77.48/77.53 cnf(200,plain, % 77.48/77.53 (E(f2(f2(a1,f2(x2001,x2002)),x2003),f2(f2(a1,f2(a1,f2(a1,f2(a1,f2(a1,f2(x2001,x2002)))))),f2(a1,f2(a1,f2(a1,f2(a1,x2003))))))), % 77.48/77.53 inference(scs_inference,[],[195,105,3,2])). % 77.48/77.53 cnf(206,plain, % 77.48/77.53 (E(f2(f2(a1,f2(a1,f2(a1,f2(f2(a3,f2(a1,x2061)),f2(x2062,x2063))))),f2(a1,f2(a1,f2(a1,x2064)))),f2(f2(f2(x2062,x2063),x2064),x2061))), % 77.48/77.53 inference(scs_inference,[],[185,17,3,2])). % 77.48/77.53 cnf(209,plain, % 77.48/77.53 (E(f2(f2(a1,f2(f2(x2091,x2092),x2093)),f2(a1,x2094)),f2(f2(a1,f2(a1,f2(a1,f2(f2(a3,f2(a1,x2094)),f2(x2091,x2092))))),f2(a1,f2(a1,f2(a1,x2093)))))), % 77.48/77.53 inference(scs_inference,[],[206,25,3,2])). % 77.48/77.53 cnf(212,plain, % 77.48/77.53 (E(f2(f2(a1,f2(f2(x2121,x2122),x2123)),f2(a1,x2124)),f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x2123))),a1)),f2(a3,f2(a1,x2124))),f2(x2121,x2122)))), % 77.48/77.53 inference(scs_inference,[],[209,32,3])). % 77.48/77.53 cnf(214,plain, % 77.48/77.53 (E(f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x2141))),a1)),f2(a3,f2(a1,x2142))),f2(x2143,x2144)),f2(f2(a1,f2(f2(x2143,x2144),x2141)),f2(a1,x2142)))), % 77.48/77.53 inference(scs_inference,[],[209,32,3,2])). % 77.48/77.53 cnf(215,plain, % 77.48/77.53 (E(f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x2151))),a1)),f2(a3,f2(a1,x2152))),f2(a3,f2(f2(a3,f2(a1,x2153)),a1))),f2(f2(a1,x2152),f2(f2(a3,x2153),x2151)))), % 77.48/77.53 inference(scs_inference,[],[214,108,3])). % 77.48/77.53 cnf(218,plain, % 77.48/77.53 (E(f2(f2(a1,x2181),f2(f2(a3,x2182),x2183)),f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x2183))),a1)),f2(a3,f2(a1,x2181))),f2(a3,f2(f2(a3,f2(a1,x2182)),a1))))), % 77.48/77.53 inference(scs_inference,[],[215,2])). % 77.48/77.53 cnf(219,plain, % 77.48/77.53 (E(f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x2191))),a1)),f2(a3,f2(a1,x2192))),f2(x2193,x2194)),f2(f2(a1,x2191),f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x2192))),a1)),f2(x2193,x2194))))), % 77.48/77.53 inference(scs_inference,[],[214,47,215,2,3])). % 77.48/77.53 cnf(221,plain, % 77.48/77.53 (E(f2(f2(a1,x2211),f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x2212))),a1)),f2(x2213,x2214))),f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x2211))),a1)),f2(a3,f2(a1,x2212))),f2(x2213,x2214)))), % 77.48/77.53 inference(scs_inference,[],[219,2])). % 77.48/77.53 cnf(239,plain, % 77.48/77.53 (E(f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x2391))),a1)),f2(a3,f2(f2(a3,f2(a1,x2392)),a1))),x2393),f2(f2(f2(a3,f2(a1,x2391)),f2(a3,x2392)),x2393))), % 77.48/77.53 inference(scs_inference,[],[145,13,3,2])). % 77.48/77.53 cnf(242,plain, % 77.48/77.53 (E(f2(f2(a1,f2(a1,f2(x2421,x2422))),f2(a1,x2423)),f2(f2(a1,x2422),f2(f2(a3,x2423),x2421)))), % 77.48/77.53 inference(scs_inference,[],[189,105,3,2])). % 77.48/77.53 cnf(245,plain, % 77.48/77.53 (E(f2(f2(a1,f2(a1,f2(a1,f2(x2451,x2452)))),f2(f2(a3,f2(a1,f2(a1,f2(a1,x2453)))),a1)),f2(f2(a1,f2(x2451,x2452)),x2453))), % 77.48/77.53 inference(scs_inference,[],[242,200,3,2])). % 77.48/77.53 cnf(246,plain, % 77.48/77.53 (E(f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x2461))),a1)),f2(a3,f2(f2(a3,f2(a1,x2462)),a1))),x2463),f2(f2(f2(a3,x2462),x2463),x2461))), % 77.48/77.53 inference(scs_inference,[],[239,17,3])). % 77.48/77.53 cnf(248,plain, % 77.48/77.53 (E(f2(f2(f2(a3,x2481),x2482),x2483),f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x2483))),a1)),f2(a3,f2(f2(a3,f2(a1,x2481)),a1))),x2482))), % 77.48/77.53 inference(scs_inference,[],[246,2])). % 77.48/77.53 cnf(249,plain, % 77.48/77.53 (E(f2(f2(a1,f2(a1,f2(a1,f2(x2491,x2492)))),f2(f2(a3,f2(a1,f2(a1,f2(a1,x2493)))),a1)),f2(f2(a1,f2(a1,f2(x2491,x2492))),f2(a1,x2493)))), % 77.48/77.53 inference(scs_inference,[],[245,25,246,2,3])). % 77.48/77.53 cnf(251,plain, % 77.48/77.53 (E(f2(f2(a1,f2(a1,f2(x2511,x2512))),f2(a1,x2513)),f2(f2(a1,f2(a1,f2(a1,f2(x2511,x2512)))),f2(f2(a3,f2(a1,f2(a1,f2(a1,x2513)))),a1)))), % 77.48/77.53 inference(scs_inference,[],[249,2])). % 77.48/77.53 cnf(252,plain, % 77.48/77.53 (E(f2(f2(f2(a3,x2521),x2522),x2523),f2(f2(a1,f2(a1,f2(f2(a3,f2(f2(a3,f2(a1,x2521)),a1)),x2522))),f2(a1,f2(a1,x2523))))), % 77.48/77.53 inference(scs_inference,[],[248,21,249,2,3])). % 77.48/77.53 cnf(255,plain, % 77.48/77.53 (E(f2(f2(a1,f2(a1,f2(x2551,x2552))),f2(a1,x2553)),f2(f2(f2(a3,f2(a1,f2(a1,f2(a1,f2(x2551,x2552))))),f2(a3,f2(a1,f2(a1,f2(a1,x2553))))),a1))), % 77.48/77.53 inference(scs_inference,[],[251,10,252,2,3])). % 77.48/77.53 cnf(257,plain, % 77.48/77.53 (E(f2(f2(f2(a3,f2(a1,f2(a1,f2(a1,f2(x2571,x2572))))),f2(a3,f2(a1,f2(a1,f2(a1,x2573))))),a1),f2(f2(a1,f2(a1,f2(x2571,x2572))),f2(a1,x2573)))), % 77.48/77.53 inference(scs_inference,[],[255,2])). % 77.48/77.53 cnf(263,plain, % 77.48/77.53 (E(f2(f2(a1,x2631),f2(f2(a3,x2632),x2633)),f2(f2(f2(a3,f2(a1,f2(a1,f2(a1,f2(x2633,x2631))))),f2(a3,f2(a1,f2(a1,f2(a1,x2632))))),a1))), % 77.48/77.53 inference(scs_inference,[],[257,242,3,2])). % 77.48/77.53 cnf(264,plain, % 77.48/77.53 (E(f2(f2(a1,x2641),f2(f2(a3,x2642),x2643)),f2(f2(f2(a3,f2(a1,f2(a1,f2(a1,x2642)))),a1),f2(a1,f2(a1,f2(x2643,x2641)))))), % 77.48/77.53 inference(scs_inference,[],[263,17,3])). % 77.48/77.53 cnf(266,plain, % 77.48/77.53 (E(f2(f2(f2(a3,f2(a1,f2(a1,f2(a1,x2661)))),a1),f2(a1,f2(a1,f2(x2662,x2663)))),f2(f2(a1,x2663),f2(f2(a3,x2661),x2662)))), % 77.48/77.53 inference(scs_inference,[],[263,17,3,2])). % 77.48/77.53 cnf(269,plain, % 77.48/77.53 (E(f2(f2(a1,f2(x2691,x2692)),f2(f2(a3,f2(a1,x2693)),f2(a3,f2(a1,x2694)))),f2(f2(f2(x2691,x2692),x2693),x2694))), % 77.48/77.53 inference(scs_inference,[],[266,185,3,2])). % 77.48/77.53 cnf(273,plain, % 77.48/77.53 (E(f2(f2(a1,f2(f2(a3,f2(f2(a3,f2(a1,x2731)),a1)),x2732)),f2(a1,x2733)),f2(f2(a1,f2(a3,f2(a1,x2733))),f2(f2(a3,f2(a1,f2(a3,x2731))),f2(a3,f2(a1,x2732)))))), % 77.48/77.54 inference(scs_inference,[],[269,111,3,2])). % 77.48/77.54 cnf(276,plain, % 77.48/77.54 (E(f2(f2(a1,x2761),f2(f2(a3,x2762),x2763)),f2(f2(a1,f2(a3,f2(f2(a3,f2(a1,f2(a1,x2762))),a1))),f2(f2(a3,f2(a1,a1)),f2(a3,f2(a1,f2(x2763,x2761))))))), % 77.48/77.54 inference(scs_inference,[],[269,101,3,2])). % 77.48/77.54 cnf(279,plain, % 77.48/77.54 (E(f2(f2(f2(a3,f2(a1,f2(x2791,x2792))),f2(a3,f2(a1,x2793))),a1),f2(f2(a1,x2792),f2(f2(a3,x2793),x2791)))), % 77.48/77.54 inference(scs_inference,[],[276,156,3,2])). % 77.48/77.54 cnf(282,plain, % 77.48/77.54 (E(f2(f2(a1,f2(f2(a3,f2(a1,x2821)),f2(a3,f2(a1,x2822)))),f2(a1,f2(a3,x2823))),f2(f2(a1,f2(f2(a3,f2(f2(a3,f2(a1,x2823)),a1)),x2821)),f2(a1,x2822)))), % 77.48/77.54 inference(scs_inference,[],[273,105,3,2])). % 77.48/77.54 cnf(285,plain, % 77.48/77.54 (E(f2(f2(f2(x2851,x2852),x2853),x2854),f2(f2(f2(a3,f2(a1,f2(f2(a3,f2(a1,x2854)),f2(x2851,x2852)))),f2(a3,f2(a1,f2(a1,x2853)))),a1))), % 77.48/77.54 inference(scs_inference,[],[279,269,3,2])). % 77.48/77.54 cnf(288,plain, % 77.48/77.54 (E(f2(f2(a1,x2881),f2(f2(a3,x2882),x2883)),f2(f2(a1,f2(f2(a3,f2(a1,x2883)),f2(a3,f2(a1,x2881)))),f2(a1,f2(a3,x2882))))), % 77.48/77.54 inference(scs_inference,[],[282,108,3,2])). % 77.48/77.54 cnf(292,plain, % 77.48/77.54 (E(f2(f2(f2(a3,f2(a1,x2921)),f2(a3,x2922)),x2923),f2(f2(a1,x2921),f2(f2(a3,f2(f2(a3,f2(a1,x2922)),a1)),x2923)))), % 77.48/77.54 inference(scs_inference,[],[288,127,3,2])). % 77.48/77.54 cnf(293,plain, % 77.48/77.54 (E(f2(f2(f2(a3,f2(a1,x2931)),f2(a3,f2(a1,x2932))),f2(a3,f2(f2(a3,f2(a1,x2933)),x2934))),f2(f2(x2934,f2(x2931,x2932)),x2933))), % 77.48/77.54 inference(scs_inference,[],[292,84,3])). % 77.48/77.54 cnf(296,plain, % 77.48/77.54 (E(f2(f2(x2961,f2(x2962,x2963)),x2964),f2(f2(f2(a3,f2(a1,x2962)),f2(a3,f2(a1,x2963))),f2(a3,f2(f2(a3,f2(a1,x2964)),x2961))))), % 77.48/77.54 inference(scs_inference,[],[293,2])). % 77.48/77.54 cnf(297,plain, % 77.48/77.54 (E(f2(f2(f2(a3,f2(a1,x2971)),f2(a3,f2(a1,x2972))),f2(x2973,x2974)),f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x2971))),a1)),f2(a3,f2(a1,x2972))),f2(x2973,x2974)))), % 77.48/77.54 inference(scs_inference,[],[292,221,293,2,3])). % 77.48/77.54 cnf(300,plain, % 77.48/77.54 (E(f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x3001))),a1)),f2(a3,f2(a1,x3002))),f2(x3003,x3004)),f2(f2(f2(a3,f2(a1,x3001)),f2(a3,f2(a1,x3002))),f2(x3003,x3004)))), % 77.48/77.54 inference(scs_inference,[],[297,2])). % 77.48/77.54 cnf(301,plain, % 77.48/77.54 (E(f2(f2(x3011,f2(x3012,x3013)),x3014),f2(f2(a1,f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x3013))),a1)),f2(a3,f2(f2(a3,f2(a1,x3014)),x3011)))),f2(a1,x3012)))), % 77.48/77.54 inference(scs_inference,[],[296,111,297,2,3])). % 77.48/77.54 cnf(303,plain, % 77.48/77.54 (E(f2(f2(a1,f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x3031))),a1)),f2(a3,f2(f2(a3,f2(a1,x3032)),x3033)))),f2(a1,x3034)),f2(f2(x3033,f2(x3034,x3031)),x3032))), % 77.48/77.54 inference(scs_inference,[],[301,2])). % 77.48/77.54 cnf(325,plain, % 77.48/77.54 (E(f2(f2(f2(a3,f2(f2(a3,f2(a1,x3251)),f2(a3,f2(a1,x3252)))),x3253),x3254),f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x3251))),a1)),f2(a3,f2(a1,x3252))),f2(x3253,x3254)))), % 77.48/77.54 inference(scs_inference,[],[300,10,3,2])). % 77.48/77.54 cnf(330,plain, % 77.48/77.54 (E(f2(f2(a1,f2(f2(x3301,x3302),x3303)),f2(a1,x3304)),f2(f2(f2(a3,f2(f2(a3,f2(a1,x3303)),f2(a3,f2(a1,x3304)))),x3301),x3302))), % 77.48/77.54 inference(scs_inference,[],[325,214,3,2])). % 77.48/77.54 cnf(334,plain, % 77.48/77.54 (E(f2(f2(f2(a3,f2(f2(a3,f2(a1,x3341)),f2(a3,x3342))),x3343),x3344),f2(f2(a1,f2(f2(a3,f2(f2(a3,f2(a1,x3342)),a1)),f2(x3343,x3344))),f2(a1,x3341)))), % 77.48/77.54 inference(scs_inference,[],[330,176,3,2])). % 77.48/77.54 cnf(337,plain, % 77.48/77.54 (E(f2(f2(a1,f2(a3,f2(a1,x3371))),f2(f2(a3,f2(a1,f2(a3,x3372))),f2(a3,f2(a1,f2(x3373,x3374))))),f2(f2(f2(a3,f2(f2(a3,f2(a1,x3371)),f2(a3,x3372))),x3373),x3374))), % 77.48/77.54 inference(scs_inference,[],[334,273,3,2])). % 77.48/77.54 cnf(338,plain, % 77.48/77.54 (E(f2(f2(f2(a3,f2(f2(a3,f2(a1,x3381)),f2(a3,f2(a1,x3382)))),a3),f2(f2(a3,f2(a1,x3383)),x3384)),f2(f2(x3384,f2(x3381,x3382)),x3383))), % 77.48/77.54 inference(scs_inference,[],[334,303,3])). % 77.48/77.54 cnf(341,plain, % 77.48/77.54 (E(f2(f2(x3411,f2(x3412,x3413)),x3414),f2(f2(f2(a3,f2(f2(a3,f2(a1,x3412)),f2(a3,f2(a1,x3413)))),a3),f2(f2(a3,f2(a1,x3414)),x3411)))), % 77.48/77.54 inference(scs_inference,[],[338,2])). % 77.48/77.54 cnf(342,plain, % 77.48/77.54 (E(f2(f2(a1,f2(a3,f2(a1,x3421))),f2(f2(a3,f2(a1,f2(a3,x3422))),f2(a3,f2(a1,f2(x3423,x3424))))),f2(f2(a1,f2(f2(a3,x3422),f2(x3423,x3424))),f2(a1,x3421)))), % 77.48/77.54 inference(scs_inference,[],[337,21,338,2,3])). % 77.48/77.54 cnf(344,plain, % 77.48/77.54 (E(f2(f2(a1,f2(f2(a3,x3441),f2(x3442,x3443))),f2(a1,x3444)),f2(f2(a1,f2(a3,f2(a1,x3444))),f2(f2(a3,f2(a1,f2(a3,x3441))),f2(a3,f2(a1,f2(x3442,x3443))))))), % 77.48/77.54 inference(scs_inference,[],[342,2])). % 77.48/77.54 cnf(345,plain, % 77.48/77.54 (E(f2(f2(a1,x3451),f2(x3452,f2(x3453,x3454))),f2(f2(f2(a3,f2(f2(a3,f2(a1,x3453)),f2(a3,f2(a1,x3454)))),a3),f2(f2(a3,f2(a1,x3451)),x3452)))), % 77.48/77.54 inference(scs_inference,[],[6,341,342,2,3])). % 77.48/77.54 cnf(349,plain, % 77.48/77.54 (E(f2(f2(a1,f2(a1,x3491)),f2(a1,f2(f2(a3,x3492),f2(x3493,x3494)))),f2(f2(a1,f2(a3,f2(a1,x3491))),f2(f2(a3,f2(a1,f2(a3,x3492))),f2(a3,f2(a1,f2(x3493,x3494))))))), % 77.48/77.54 inference(scs_inference,[],[6,344,345,2,3])). % 77.48/77.54 cnf(351,plain, % 77.48/77.54 (E(f2(f2(a1,f2(a3,f2(a1,x3511))),f2(f2(a3,f2(a1,f2(a3,x3512))),f2(a3,f2(a1,f2(x3513,x3514))))),f2(f2(a1,f2(a1,x3511)),f2(a1,f2(f2(a3,x3512),f2(x3513,x3514)))))), % 77.48/77.54 inference(scs_inference,[],[349,2])). % 77.48/77.54 cnf(356,plain, % 77.48/77.54 (E(f2(f2(a1,f2(a1,x3561)),f2(a1,f2(f2(a3,x3562),f2(x3563,x3564)))),f2(f2(a1,f2(f2(a3,f2(a1,f2(a3,x3562))),f2(a3,f2(a1,f2(x3563,x3564))))),f2(a1,f2(a3,f2(a1,x3561)))))), % 77.48/77.54 inference(scs_inference,[],[6,351,3,2])). % 77.48/77.54 cnf(359,plain, % 77.48/77.54 (E(f2(f2(a1,f2(f2(a3,f2(a1,f2(a3,x3591))),f2(a3,f2(a1,f2(x3592,x3593))))),f2(a1,f2(a3,f2(a1,x3594)))),f2(f2(a1,f2(a1,f2(f2(a3,x3591),f2(x3592,x3593)))),f2(a1,f2(a1,x3594))))), % 77.48/77.54 inference(scs_inference,[],[6,356,3,2])). % 77.48/77.54 cnf(366,plain, % 77.48/77.54 (E(f2(f2(f2(a3,f2(a1,x3661)),f2(a3,f2(a1,x3662))),f2(a3,f2(f2(a3,f2(a1,x3663)),x3664))),f2(f2(a1,x3663),f2(x3664,f2(x3661,x3662))))), % 77.48/77.54 inference(scs_inference,[],[6,296,3,2])). % 77.48/77.54 cnf(367,plain, % 77.48/77.54 (E(f2(f2(a1,f2(a3,f2(f2(a3,f2(a1,x3671)),x3672))),f2(f2(a3,f2(a1,x3673)),f2(a3,f2(a1,x3674)))),f2(f2(a1,x3671),f2(x3672,f2(x3673,x3674))))), % 77.48/77.54 inference(scs_inference,[],[6,366,3])). % 77.48/77.54 cnf(369,plain, % 77.48/77.54 (E(f2(f2(a1,x3691),f2(x3692,f2(x3693,x3694))),f2(f2(a1,f2(a3,f2(f2(a3,f2(a1,x3691)),x3692))),f2(f2(a3,f2(a1,x3693)),f2(a3,f2(a1,x3694)))))), % 77.48/77.54 inference(scs_inference,[],[6,366,3,2])). % 77.48/77.54 cnf(372,plain, % 77.48/77.54 (E(f2(f2(a1,f2(a3,f2(f2(a3,f2(a1,x3721)),x3722))),f2(f2(a3,f2(a1,x3723)),f2(a3,f2(a1,x3724)))),f2(f2(a1,f2(x3722,f2(x3723,x3724))),f2(a1,x3721)))), % 77.48/77.54 inference(scs_inference,[],[6,369,3,2])). % 77.48/77.54 cnf(373,plain, % 77.48/77.54 (E(f2(f2(a1,f2(f2(a3,f2(a1,x3731)),f2(a3,f2(a1,x3732)))),f2(a1,f2(a3,f2(f2(a3,f2(a1,x3733)),x3734)))),f2(f2(a1,f2(x3734,f2(x3731,x3732))),f2(a1,x3733)))), % 77.48/77.54 inference(scs_inference,[],[6,372,3])). % 77.48/77.54 cnf(375,plain, % 77.48/77.54 (E(f2(f2(a1,f2(x3751,f2(x3752,x3753))),f2(a1,x3754)),f2(f2(a1,f2(f2(a3,f2(a1,x3752)),f2(a3,f2(a1,x3753)))),f2(a1,f2(a3,f2(f2(a3,f2(a1,x3754)),x3751)))))), % 77.48/77.54 inference(scs_inference,[],[373,2])). % 77.48/77.54 cnf(376,plain, % 77.48/77.54 (E(f2(f2(a1,f2(f2(a3,f2(a1,f2(a3,x3761))),f2(a3,f2(a1,f2(x3762,x3763))))),f2(a1,f2(a3,f2(a1,x3764)))),f2(f2(f2(a3,f2(f2(a3,f2(a1,x3764)),f2(a3,x3761))),x3762),x3763))), % 77.48/77.54 inference(scs_inference,[],[6,337,373,2,3])). % 77.48/77.54 cnf(378,plain, % 77.48/77.54 (E(f2(f2(f2(a3,f2(f2(a3,f2(a1,x3781)),f2(a3,x3782))),x3783),x3784),f2(f2(a1,f2(f2(a3,f2(a1,f2(a3,x3782))),f2(a3,f2(a1,f2(x3783,x3784))))),f2(a1,f2(a3,f2(a1,x3781)))))), % 77.48/77.54 inference(scs_inference,[],[376,2])). % 77.48/77.54 cnf(379,plain, % 77.48/77.54 (E(f2(f2(a1,f2(a1,x3791)),f2(a1,f2(x3792,f2(x3793,x3794)))),f2(f2(a1,f2(f2(a3,f2(a1,x3793)),f2(a3,f2(a1,x3794)))),f2(a1,f2(a3,f2(f2(a3,f2(a1,x3791)),x3792)))))), % 77.48/77.54 inference(scs_inference,[],[6,375,376,2,3])). % 77.48/77.54 cnf(381,plain, % 77.48/77.54 (E(f2(f2(a1,f2(f2(a3,f2(a1,x3811)),f2(a3,f2(a1,x3812)))),f2(a1,f2(a3,f2(f2(a3,f2(a1,x3813)),x3814)))),f2(f2(a1,f2(a1,x3813)),f2(a1,f2(x3814,f2(x3811,x3812)))))), % 77.48/77.54 inference(scs_inference,[],[379,2])). % 77.48/77.54 cnf(382,plain, % 77.48/77.54 (E(f2(f2(a1,x3821),f2(f2(a3,f2(f2(a3,f2(a1,x3822)),f2(a3,x3823))),x3824)),f2(f2(a1,f2(f2(a3,f2(a1,f2(a3,x3823))),f2(a3,f2(a1,f2(x3824,x3821))))),f2(a1,f2(a3,f2(a1,x3822)))))), % 77.48/77.54 inference(scs_inference,[],[6,378,379,2,3])). % 77.48/77.54 cnf(385,plain, % 77.48/77.54 (E(f2(f2(a1,f2(f2(a3,f2(a1,f2(a3,x3851))),f2(a3,f2(a1,f2(x3852,x3853))))),f2(a1,f2(a3,f2(a1,x3854)))),f2(f2(a1,x3853),f2(f2(a3,f2(f2(a3,f2(a1,x3854)),f2(a3,x3851))),x3852)))), % 77.48/77.54 inference(scs_inference,[],[382,2])). % 77.48/77.54 cnf(405,plain, % 77.48/77.54 (E(f2(f2(a1,f2(f2(a3,f2(a1,f2(a1,f2(a1,x4051)))),a1)),f2(a1,f2(a1,f2(a1,f2(x4052,x4053))))),f2(f2(a1,f2(x4052,x4053)),x4051))), % 77.48/77.54 inference(scs_inference,[],[6,245,3])). % 77.48/77.54 cnf(407,plain, % 77.48/77.54 (E(f2(f2(a1,f2(x4071,x4072)),x4073),f2(f2(a1,f2(f2(a3,f2(a1,f2(a1,f2(a1,x4073)))),a1)),f2(a1,f2(a1,f2(a1,f2(x4071,x4072))))))), % 77.48/77.54 inference(scs_inference,[],[405,2])). % 77.48/77.54 cnf(408,plain, % 77.48/77.54 (E(f2(f2(a1,f2(f2(a3,x4081),x4082)),f2(a1,x4083)),f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x4082))),a1)),f2(a3,f2(a1,x4083))),f2(a3,f2(f2(a3,f2(a1,x4081)),a1))))), % 77.48/77.54 inference(scs_inference,[],[6,218,405,2,3])). % 77.48/77.54 cnf(411,plain, % 77.48/77.54 (E(f2(f2(a1,x4111),f2(a1,f2(x4112,x4113))),f2(f2(a1,f2(f2(a3,f2(a1,f2(a1,f2(a1,x4111)))),a1)),f2(a1,f2(a1,f2(a1,f2(x4112,x4113))))))), % 77.48/77.54 inference(scs_inference,[],[6,407,408,2,3])). % 77.48/77.54 cnf(414,plain, % 77.48/77.54 (E(f2(f2(a1,f2(f2(a3,f2(a1,f2(a1,f2(a1,x4141)))),a1)),f2(a1,f2(a1,f2(a1,f2(x4142,x4143))))),f2(f2(a1,x4141),f2(a1,f2(x4142,x4143))))), % 77.48/77.54 inference(scs_inference,[],[411,2])). % 77.48/77.54 cnf(419,plain, % 77.48/77.54 (E(f2(f2(a1,f2(f2(a3,f2(a1,x4191)),f2(a3,f2(a1,x4192)))),f2(a1,f2(a3,x4193))),f2(f2(a1,f2(f2(a3,x4193),x4191)),f2(a1,x4192)))), % 77.48/77.54 inference(scs_inference,[],[6,288,3,2])). % 77.48/77.54 cnf(422,plain, % 77.48/77.54 (E(f2(f2(a1,f2(f2(a3,x4221),x4222)),f2(a1,x4223)),f2(f2(a1,f2(a1,f2(a3,x4221))),f2(a1,f2(f2(a3,f2(a1,x4222)),f2(a3,f2(a1,x4223))))))), % 77.48/77.54 inference(scs_inference,[],[6,419,3,2])). % 77.48/77.54 cnf(425,plain, % 77.48/77.54 (E(f2(f2(a1,f2(a1,f2(a3,x4251))),f2(a1,f2(f2(a3,f2(a1,x4252)),f2(a3,f2(a1,x4253))))),f2(f2(a1,f2(a1,x4253)),f2(a1,f2(f2(a3,x4251),x4252))))), % 77.48/77.54 inference(scs_inference,[],[6,422,3,2])). % 77.48/77.54 cnf(428,plain, % 77.48/77.54 (E(f2(f2(a1,f2(a1,x4281)),f2(a1,f2(f2(a3,x4282),x4283))),f2(f2(a1,f2(a1,f2(f2(a3,f2(a1,x4283)),f2(a3,f2(a1,x4281))))),f2(a1,f2(a1,f2(a3,x4282)))))), % 77.48/77.54 inference(scs_inference,[],[6,425,3,2])). % 77.48/77.54 cnf(431,plain, % 77.48/77.54 (E(f2(f2(a1,f2(a1,f2(f2(a3,f2(a1,x4311)),f2(a3,f2(a1,x4312))))),f2(a1,f2(a1,f2(a3,x4313)))),f2(f2(a1,f2(a1,f2(f2(a3,x4313),x4311))),f2(a1,f2(a1,x4312))))), % 77.48/77.54 inference(scs_inference,[],[6,428,3,2])). % 77.48/77.54 cnf(436,plain, % 77.48/77.54 (E(f2(f2(a1,x4361),f2(f2(a3,x4362),x4363)),f2(f2(a1,f2(a1,f2(a1,f2(x4363,x4361)))),f2(f2(a3,f2(a1,f2(a1,f2(a1,x4362)))),a1)))), % 77.48/77.54 inference(scs_inference,[],[6,266,3,2])). % 77.48/77.54 cnf(439,plain, % 77.48/77.54 (E(f2(f2(a1,f2(a1,f2(a1,f2(x4391,x4392)))),f2(f2(a3,f2(a1,f2(a1,f2(a1,x4393)))),a1)),f2(f2(a1,f2(f2(a3,x4393),x4391)),f2(a1,x4392)))), % 77.48/77.54 inference(scs_inference,[],[6,436,3,2])). % 77.48/77.54 cnf(440,plain, % 77.48/77.54 (E(f2(f2(a1,f2(f2(a3,f2(a1,f2(a1,f2(a1,x4401)))),a1)),f2(a1,f2(a1,f2(a1,f2(x4402,x4403))))),f2(f2(a1,f2(f2(a3,x4401),x4402)),f2(a1,x4403)))), % 77.48/77.54 inference(scs_inference,[],[6,439,3])). % 77.48/77.54 cnf(442,plain, % 77.48/77.54 (E(f2(f2(a1,f2(f2(a3,x4421),x4422)),f2(a1,x4423)),f2(f2(a1,f2(f2(a3,f2(a1,f2(a1,f2(a1,x4421)))),a1)),f2(a1,f2(a1,f2(a1,f2(x4422,x4423))))))), % 77.48/77.54 inference(scs_inference,[],[440,2])). % 77.48/77.54 cnf(443,plain, % 77.48/77.54 (E(f2(f2(a1,f2(a1,x4431)),f2(a1,f2(f2(a3,f2(a1,x4432)),f2(a3,x4433)))),f2(f2(a1,f2(a3,f2(f2(a3,f2(a1,x4433)),a1))),f2(f2(a3,f2(a1,x4431)),f2(a3,f2(a1,x4432)))))), % 77.48/77.54 inference(scs_inference,[],[6,159,440,2,3])). % 77.48/77.54 cnf(445,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a3,f2(f2(a3,f2(a1,x4451)),a1))),f2(f2(a3,f2(a1,x4452)),f2(a3,f2(a1,x4453)))),f2(f2(a1,f2(a1,x4452)),f2(a1,f2(f2(a3,f2(a1,x4453)),f2(a3,x4451)))))), % 77.56/77.54 inference(scs_inference,[],[443,2])). % 77.56/77.54 cnf(446,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,f2(a3,x4461))),f2(a1,f2(f2(a3,f2(a1,x4462)),f2(a3,f2(a1,x4463))))),f2(f2(a1,f2(f2(a3,f2(f2(a3,f2(a1,x4461)),a1)),x4462)),f2(a1,x4463)))), % 77.56/77.54 inference(scs_inference,[],[6,282,443,2,3])). % 77.56/77.54 cnf(448,plain, % 77.56/77.54 (E(f2(f2(a1,f2(f2(a3,f2(f2(a3,f2(a1,x4481)),a1)),x4482)),f2(a1,x4483)),f2(f2(a1,f2(a1,f2(a3,x4481))),f2(a1,f2(f2(a3,f2(a1,x4482)),f2(a3,f2(a1,x4483))))))), % 77.56/77.54 inference(scs_inference,[],[446,2])). % 77.56/77.54 cnf(449,plain, % 77.56/77.54 (E(f2(f2(a1,f2(f2(a3,f2(a1,x4491)),f2(a3,f2(a1,x4492)))),f2(a1,f2(a3,f2(f2(a3,f2(a1,x4493)),a1)))),f2(f2(a1,f2(a1,x4491)),f2(a1,f2(f2(a3,f2(a1,x4492)),f2(a3,x4493)))))), % 77.56/77.54 inference(scs_inference,[],[6,445,446,2,3])). % 77.56/77.54 cnf(451,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,x4511)),f2(a1,f2(f2(a3,f2(a1,x4512)),f2(a3,x4513)))),f2(f2(a1,f2(f2(a3,f2(a1,x4511)),f2(a3,f2(a1,x4512)))),f2(a1,f2(a3,f2(f2(a3,f2(a1,x4513)),a1)))))), % 77.56/77.54 inference(scs_inference,[],[449,2])). % 77.56/77.54 cnf(468,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,f2(a1,f2(x4681,x4682)))),f2(f2(a3,f2(a1,f2(a1,f2(a1,x4683)))),a1)),f2(f2(a1,f2(a1,x4683)),f2(a1,f2(a1,f2(x4681,x4682)))))), % 77.56/77.54 inference(scs_inference,[],[6,251,3,2])). % 77.56/77.54 cnf(475,plain, % 77.56/77.54 (E(f2(f2(a1,x4751),f2(f2(a3,x4752),x4753)),f2(f2(a1,a1),f2(f2(a3,f2(a1,f2(x4753,x4751))),f2(a3,f2(a1,x4752)))))), % 77.56/77.54 inference(scs_inference,[],[6,279,3,2])). % 77.56/77.54 cnf(478,plain, % 77.56/77.54 (E(f2(f2(a1,a1),f2(f2(a3,f2(a1,f2(x4781,x4782))),f2(a3,f2(a1,x4783)))),f2(f2(a1,f2(f2(a3,x4783),x4781)),f2(a1,x4782)))), % 77.56/77.54 inference(scs_inference,[],[6,475,3,2])). % 77.56/77.54 cnf(481,plain, % 77.56/77.54 (E(f2(f2(a1,f2(f2(a3,x4811),x4812)),f2(a1,x4813)),f2(f2(a1,f2(f2(a3,f2(a1,f2(x4812,x4813))),f2(a3,f2(a1,x4811)))),f2(a1,a1)))), % 77.56/77.54 inference(scs_inference,[],[6,478,3,2])). % 77.56/77.54 cnf(484,plain, % 77.56/77.54 (E(f2(f2(a1,f2(f2(a3,f2(a1,f2(x4841,x4842))),f2(a3,f2(a1,x4843)))),f2(a1,a1)),f2(f2(a1,f2(a1,x4842)),f2(a1,f2(f2(a3,x4843),x4841))))), % 77.56/77.54 inference(scs_inference,[],[6,481,3,2])). % 77.56/77.54 cnf(487,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,x4871)),f2(a1,f2(f2(a3,x4872),x4873))),f2(f2(a1,f2(a1,a1)),f2(a1,f2(f2(a3,f2(a1,f2(x4873,x4871))),f2(a3,f2(a1,x4872))))))), % 77.56/77.54 inference(scs_inference,[],[6,484,3,2])). % 77.56/77.54 cnf(490,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,a1)),f2(a1,f2(f2(a3,f2(a1,f2(x4901,x4902))),f2(a3,f2(a1,x4903))))),f2(f2(a1,f2(a1,f2(f2(a3,x4903),x4901))),f2(a1,f2(a1,x4902))))), % 77.56/77.54 inference(scs_inference,[],[6,487,3,2])). % 77.56/77.54 cnf(493,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,f2(f2(a3,x4931),x4932))),f2(a1,f2(a1,x4933))),f2(f2(a1,f2(a1,f2(f2(a3,f2(a1,f2(x4932,x4933))),f2(a3,f2(a1,x4931))))),f2(a1,f2(a1,a1))))), % 77.56/77.54 inference(scs_inference,[],[6,490,3,2])). % 77.56/77.54 cnf(496,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,f2(f2(a3,f2(a1,f2(x4961,x4962))),f2(a3,f2(a1,x4963))))),f2(a1,f2(a1,a1))),f2(f2(a1,f2(a1,f2(a1,x4962))),f2(a1,f2(a1,f2(f2(a3,x4963),x4961)))))), % 77.56/77.54 inference(scs_inference,[],[6,493,3,2])). % 77.56/77.54 cnf(524,plain, % 77.56/77.54 (E(f2(f2(a1,x5241),f2(f2(a3,f2(f2(a3,f2(a1,x5242)),a1)),x5243)),f2(f2(a1,x5243),f2(f2(a3,f2(a1,x5241)),f2(a3,x5242))))), % 77.56/77.54 inference(scs_inference,[],[6,292,3,2])). % 77.56/77.54 cnf(527,plain, % 77.56/77.54 (E(f2(f2(a1,x5271),f2(f2(a3,f2(a1,x5272)),f2(a3,x5273))),f2(f2(a1,f2(f2(a3,f2(f2(a3,f2(a1,x5273)),a1)),x5271)),f2(a1,x5272)))), % 77.56/77.54 inference(scs_inference,[],[6,524,3,2])). % 77.56/77.54 cnf(536,plain, % 77.56/77.54 (E(f2(f2(f2(a3,f2(a1,x5361)),f2(a3,f2(f2(a3,x5362),x5363))),x5364),f2(f2(a1,x5362),f2(a1,f2(x5363,f2(x5364,x5361)))))), % 77.56/77.54 inference(scs_inference,[],[6,29,3,2])). % 77.56/77.54 cnf(540,plain, % 77.56/77.54 (E(f2(f2(a1,x5401),f2(a1,f2(x5402,f2(x5403,x5404)))),f2(f2(a1,x5403),f2(f2(a3,f2(a1,x5404)),f2(a3,f2(f2(a3,x5401),x5402)))))), % 77.56/77.54 inference(scs_inference,[],[6,536,3,2])). % 77.56/77.54 cnf(543,plain, % 77.56/77.54 (E(f2(f2(a1,x5431),f2(f2(a3,f2(a1,x5432)),f2(a3,f2(f2(a3,x5433),x5434)))),f2(f2(a1,f2(a1,f2(x5434,f2(x5431,x5432)))),f2(a1,x5433)))), % 77.56/77.54 inference(scs_inference,[],[6,540,3,2])). % 77.56/77.54 cnf(555,plain, % 77.56/77.54 (E(f2(f2(a1,f2(f2(a3,f2(f2(a3,f2(a1,x5551)),a1)),f2(x5552,x5553))),f2(a1,x5554)),f2(f2(a1,x5553),f2(f2(a3,f2(f2(a3,f2(a1,x5554)),f2(a3,x5551))),x5552)))), % 77.56/77.54 inference(scs_inference,[],[6,334,3,2])). % 77.56/77.54 cnf(561,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a3,f2(f2(a3,f2(a1,x5611)),a1))),f2(f2(a3,f2(a1,f2(x5612,x5613))),f2(a3,f2(a1,x5614)))),f2(f2(a1,x5613),f2(f2(a3,f2(f2(a3,f2(a1,x5614)),f2(a3,x5611))),x5612)))), % 77.56/77.54 inference(scs_inference,[],[6,168,3,2])). % 77.56/77.54 cnf(571,plain, % 77.56/77.54 (E(f2(f2(f2(a3,f2(a1,x5711)),f2(a3,f2(a1,x5712))),f2(a3,f2(f2(a3,f2(a1,x5713)),a1))),f2(f2(a1,x5711),f2(f2(a3,f2(a1,x5712)),f2(a3,x5713))))), % 77.56/77.54 inference(scs_inference,[],[6,121,3,2])). % 77.56/77.54 cnf(572,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a3,f2(f2(a3,f2(a1,x5721)),a1))),f2(f2(a3,f2(a1,x5722)),f2(a3,f2(a1,x5723)))),f2(f2(a1,x5722),f2(f2(a3,f2(a1,x5723)),f2(a3,x5721))))), % 77.56/77.54 inference(scs_inference,[],[6,571,3])). % 77.56/77.54 cnf(574,plain, % 77.56/77.54 (E(f2(f2(a1,x5741),f2(f2(a3,f2(a1,x5742)),f2(a3,x5743))),f2(f2(a1,f2(a3,f2(f2(a3,f2(a1,x5743)),a1))),f2(f2(a3,f2(a1,x5741)),f2(a3,f2(a1,x5742)))))), % 77.56/77.54 inference(scs_inference,[],[6,571,3,2])). % 77.56/77.54 cnf(578,plain, % 77.56/77.54 (E(f2(f2(f2(a3,f2(a1,f2(a1,x5781))),a1),f2(a1,f2(x5782,f2(x5783,x5784)))),f2(f2(a1,x5784),f2(f2(a3,f2(f2(a3,x5781),x5782)),x5783)))), % 77.56/77.54 inference(scs_inference,[],[6,39,3,2])). % 77.56/77.54 cnf(581,plain, % 77.56/77.54 (E(f2(f2(a1,x5811),f2(f2(a3,f2(f2(a3,x5812),x5813)),x5814)),f2(f2(a1,f2(a1,f2(x5813,f2(x5814,x5811)))),f2(f2(a3,f2(a1,f2(a1,x5812))),a1)))), % 77.56/77.54 inference(scs_inference,[],[6,578,3,2])). % 77.56/77.54 cnf(584,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,f2(x5841,f2(x5842,x5843)))),f2(f2(a3,f2(a1,f2(a1,x5844))),a1)),f2(f2(a1,f2(f2(a3,f2(f2(a3,x5844),x5841)),x5842)),f2(a1,x5843)))), % 77.56/77.54 inference(scs_inference,[],[6,581,3,2])). % 77.56/77.54 cnf(592,plain, % 77.56/77.54 (E(f2(f2(a1,f2(f2(a3,f2(a1,x5921)),f2(a3,f2(a1,x5922)))),f2(a1,f2(a3,f2(f2(a3,f2(a1,x5923)),a1)))),f2(f2(a1,x5922),f2(f2(a3,x5923),x5921)))), % 77.56/77.54 inference(scs_inference,[],[6,130,3,2])). % 77.56/77.54 cnf(593,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,f2(a3,f2(f2(a3,f2(a1,x5931)),a1)))),f2(a1,f2(f2(a3,f2(a1,x5932)),f2(a3,f2(a1,x5933))))),f2(f2(a1,x5933),f2(f2(a3,x5931),x5932)))), % 77.56/77.54 inference(scs_inference,[],[6,592,3])). % 77.56/77.54 cnf(595,plain, % 77.56/77.54 (E(f2(f2(a1,x5951),f2(f2(a3,x5952),x5953)),f2(f2(a1,f2(a1,f2(a3,f2(f2(a3,f2(a1,x5952)),a1)))),f2(a1,f2(f2(a3,f2(a1,x5953)),f2(a3,f2(a1,x5951))))))), % 77.56/77.54 inference(scs_inference,[],[593,2])). % 77.56/77.54 cnf(596,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,f2(a3,f2(f2(a3,f2(a1,x5961)),a1)))),f2(a1,f2(f2(a3,f2(a1,x5962)),f2(a3,f2(a1,x5963))))),f2(f2(f2(a3,f2(a1,x5963)),f2(a3,x5961)),x5962))), % 77.56/77.54 inference(scs_inference,[],[6,127,593,2,3])). % 77.56/77.54 cnf(598,plain, % 77.56/77.54 (E(f2(f2(f2(a3,f2(a1,x5981)),f2(a3,x5982)),x5983),f2(f2(a1,f2(a1,f2(a3,f2(f2(a3,f2(a1,x5982)),a1)))),f2(a1,f2(f2(a3,f2(a1,x5983)),f2(a3,f2(a1,x5981))))))), % 77.56/77.54 inference(scs_inference,[],[596,2])). % 77.56/77.54 cnf(599,plain, % 77.56/77.54 (E(f2(f2(a1,f2(f2(a3,x5991),x5992)),f2(a1,x5993)),f2(f2(a1,f2(a1,f2(a3,f2(f2(a3,f2(a1,x5991)),a1)))),f2(a1,f2(f2(a3,f2(a1,x5992)),f2(a3,f2(a1,x5993))))))), % 77.56/77.54 inference(scs_inference,[],[6,595,596,2,3])). % 77.56/77.54 cnf(601,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,f2(a3,f2(f2(a3,f2(a1,x6011)),a1)))),f2(a1,f2(f2(a3,f2(a1,x6012)),f2(a3,f2(a1,x6013))))),f2(f2(a1,f2(f2(a3,x6011),x6012)),f2(a1,x6013)))), % 77.56/77.54 inference(scs_inference,[],[599,2])). % 77.56/77.54 cnf(602,plain, % 77.56/77.54 (E(f2(f2(a1,x6021),f2(f2(a3,f2(a1,x6022)),f2(a3,x6023))),f2(f2(a1,f2(a1,f2(a3,f2(f2(a3,f2(a1,x6023)),a1)))),f2(a1,f2(f2(a3,f2(a1,x6021)),f2(a3,f2(a1,x6022))))))), % 77.56/77.54 inference(scs_inference,[],[6,598,599,2,3])). % 77.56/77.54 cnf(605,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,f2(a3,f2(f2(a3,f2(a1,x6051)),a1)))),f2(a1,f2(f2(a3,f2(a1,x6052)),f2(a3,f2(a1,x6053))))),f2(f2(a1,x6052),f2(f2(a3,f2(a1,x6053)),f2(a3,x6051))))), % 77.56/77.54 inference(scs_inference,[],[602,2])). % 77.56/77.54 cnf(606,plain, % 77.56/77.54 (E(f2(f2(a1,f2(f2(a3,x6061),x6062)),f2(a1,x6063)),f2(f2(a1,f2(a3,f2(f2(a3,f2(a1,f2(a1,x6061))),a1))),f2(f2(a3,f2(a1,a1)),f2(a3,f2(a1,f2(x6062,x6063))))))), % 77.56/77.54 inference(scs_inference,[],[6,276,602,2,3])). % 77.56/77.54 cnf(608,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a3,f2(f2(a3,f2(a1,f2(a1,x6081))),a1))),f2(f2(a3,f2(a1,a1)),f2(a3,f2(a1,f2(x6082,x6083))))),f2(f2(a1,f2(f2(a3,x6081),x6082)),f2(a1,x6083)))), % 77.56/77.54 inference(scs_inference,[],[606,2])). % 77.56/77.54 cnf(609,plain, % 77.56/77.54 (E(f2(f2(a1,x6091),f2(f2(a3,f2(a1,x6092)),f2(a3,x6093))),f2(f2(a1,f2(f2(a3,f2(f2(a3,f2(a1,x6093)),a1)),x6091)),f2(f2(a3,f2(a1,f2(a1,x6092))),a1)))), % 77.56/77.54 inference(scs_inference,[],[6,145,606,2,3])). % 77.56/77.54 cnf(612,plain, % 77.56/77.54 (E(f2(f2(a1,f2(f2(a3,f2(f2(a3,f2(a1,x6121)),a1)),x6122)),f2(f2(a3,f2(a1,f2(a1,x6123))),a1)),f2(f2(a1,x6122),f2(f2(a3,f2(a1,x6123)),f2(a3,x6121))))), % 77.56/77.54 inference(scs_inference,[],[609,2])). % 77.56/77.54 cnf(613,plain, % 77.56/77.54 (E(f2(f2(a1,f2(f2(a3,x6131),x6132)),f2(a1,f2(x6133,x6134))),f2(f2(a1,f2(f2(a3,f2(f2(a3,x6131),x6132)),x6133)),f2(a1,x6134)))), % 77.56/77.54 inference(scs_inference,[],[6,141,609,2,3])). % 77.56/77.54 cnf(615,plain, % 77.56/77.54 (E(f2(f2(a1,f2(f2(a3,f2(f2(a3,x6151),x6152)),x6153)),f2(a1,x6154)),f2(f2(a1,f2(f2(a3,x6151),x6152)),f2(a1,f2(x6153,x6154))))), % 77.56/77.54 inference(scs_inference,[],[613,2])). % 77.56/77.54 cnf(616,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,x6161)),f2(a1,f2(a1,f2(x6162,x6163)))),f2(f2(a1,x6163),f2(f2(a3,x6161),x6162)))), % 77.56/77.54 inference(scs_inference,[],[6,242,613,2,3])). % 77.56/77.54 cnf(618,plain, % 77.56/77.54 (E(f2(f2(a1,x6181),f2(f2(a3,x6182),x6183)),f2(f2(a1,f2(a1,x6182)),f2(a1,f2(a1,f2(x6183,x6181)))))), % 77.56/77.54 inference(scs_inference,[],[616,2])). % 77.56/77.54 cnf(619,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,x6191)),f2(a1,f2(f2(a3,f2(f2(a3,x6192),x6193)),x6194))),f2(f2(a1,f2(f2(a3,x6192),x6193)),f2(a1,f2(x6194,x6191))))), % 77.56/77.54 inference(scs_inference,[],[6,615,616,2,3])). % 77.56/77.54 cnf(621,plain, % 77.56/77.54 (E(f2(f2(a1,f2(f2(a3,x6211),x6212)),f2(a1,f2(x6213,x6214))),f2(f2(a1,f2(a1,x6214)),f2(a1,f2(f2(a3,f2(f2(a3,x6211),x6212)),x6213))))), % 77.56/77.54 inference(scs_inference,[],[619,2])). % 77.56/77.54 cnf(622,plain, % 77.56/77.54 (E(f2(f2(a1,f2(f2(a3,x6221),x6222)),f2(a1,x6223)),f2(f2(a1,f2(a1,x6221)),f2(a1,f2(a1,f2(x6222,x6223)))))), % 77.56/77.54 inference(scs_inference,[],[6,618,619,2,3])). % 77.56/77.54 cnf(624,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,x6241)),f2(a1,f2(a1,f2(x6242,x6243)))),f2(f2(a1,f2(f2(a3,x6241),x6242)),f2(a1,x6243)))), % 77.56/77.54 inference(scs_inference,[],[622,2])). % 77.56/77.54 cnf(625,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,f2(x6251,x6252))),f2(a1,f2(f2(a3,x6253),x6254))),f2(f2(a1,f2(a1,x6252)),f2(a1,f2(f2(a3,f2(f2(a3,x6253),x6254)),x6251))))), % 77.56/77.54 inference(scs_inference,[],[6,621,622,2,3])). % 77.56/77.54 cnf(627,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,x6271)),f2(a1,f2(f2(a3,f2(f2(a3,x6272),x6273)),x6274))),f2(f2(a1,f2(a1,f2(x6274,x6271))),f2(a1,f2(f2(a3,x6272),x6273))))), % 77.56/77.54 inference(scs_inference,[],[625,2])). % 77.56/77.54 cnf(628,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,f2(a1,f2(x6281,x6282)))),f2(a1,f2(a1,x6283))),f2(f2(a1,f2(f2(a3,x6283),x6281)),f2(a1,x6282)))), % 77.56/77.54 inference(scs_inference,[],[6,624,625,2,3])). % 77.56/77.54 cnf(630,plain, % 77.56/77.54 (E(f2(f2(a1,f2(f2(a3,x6301),x6302)),f2(a1,x6303)),f2(f2(a1,f2(a1,f2(a1,f2(x6302,x6303)))),f2(a1,f2(a1,x6301))))), % 77.56/77.54 inference(scs_inference,[],[628,2])). % 77.56/77.54 cnf(631,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,f2(f2(a3,f2(f2(a3,x6311),x6312)),x6313))),f2(a1,f2(a1,x6314))),f2(f2(a1,f2(a1,f2(x6313,x6314))),f2(a1,f2(f2(a3,x6311),x6312))))), % 77.56/77.54 inference(scs_inference,[],[6,627,628,2,3])). % 77.56/77.54 cnf(633,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,f2(x6331,x6332))),f2(a1,f2(f2(a3,x6333),x6334))),f2(f2(a1,f2(a1,f2(f2(a3,f2(f2(a3,x6333),x6334)),x6331))),f2(a1,f2(a1,x6332))))), % 77.56/77.54 inference(scs_inference,[],[631,2])). % 77.56/77.54 cnf(634,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,x6341)),f2(a1,f2(f2(a3,x6342),x6343))),f2(f2(a1,f2(a1,f2(a1,f2(x6343,x6341)))),f2(a1,f2(a1,x6342))))), % 77.56/77.54 inference(scs_inference,[],[6,630,631,2,3])). % 77.56/77.54 cnf(636,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,f2(a1,f2(x6361,x6362)))),f2(a1,f2(a1,x6363))),f2(f2(a1,f2(a1,x6362)),f2(a1,f2(f2(a3,x6363),x6361))))), % 77.56/77.54 inference(scs_inference,[],[634,2])). % 77.56/77.54 cnf(637,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,f2(f2(a3,x6371),x6372))),f2(a1,f2(a1,f2(x6373,x6374)))),f2(f2(a1,f2(a1,f2(f2(a3,f2(f2(a3,x6371),x6372)),x6373))),f2(a1,f2(a1,x6374))))), % 77.56/77.54 inference(scs_inference,[],[6,633,634,2,3])). % 77.56/77.54 cnf(639,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,f2(f2(a3,f2(f2(a3,x6391),x6392)),x6393))),f2(a1,f2(a1,x6394))),f2(f2(a1,f2(a1,f2(f2(a3,x6391),x6392))),f2(a1,f2(a1,f2(x6393,x6394)))))), % 77.56/77.54 inference(scs_inference,[],[637,2])). % 77.56/77.54 cnf(640,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,f2(a1,x6401))),f2(a1,f2(a1,f2(a1,f2(x6402,x6403))))),f2(f2(a1,f2(a1,x6403)),f2(a1,f2(f2(a3,x6401),x6402))))), % 77.56/77.54 inference(scs_inference,[],[6,636,637,2,3])). % 77.56/77.54 cnf(642,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,x6421)),f2(a1,f2(f2(a3,x6422),x6423))),f2(f2(a1,f2(a1,f2(a1,x6422))),f2(a1,f2(a1,f2(a1,f2(x6423,x6421))))))), % 77.56/77.54 inference(scs_inference,[],[640,2])). % 77.56/77.54 cnf(643,plain, % 77.56/77.54 (E(f2(f2(a1,f2(f2(a3,x6431),x6432)),f2(a1,x6433)),f2(f2(a1,f2(x6432,x6433)),f2(f2(a3,f2(a1,x6431)),a1)))), % 77.56/77.54 inference(scs_inference,[],[6,189,640,2,3])). % 77.56/77.54 cnf(645,plain, % 77.56/77.54 (E(f2(f2(a1,f2(x6451,x6452)),f2(f2(a3,f2(a1,x6453)),a1)),f2(f2(a1,f2(f2(a3,x6453),x6451)),f2(a1,x6452)))), % 77.56/77.54 inference(scs_inference,[],[643,2])). % 77.56/77.54 cnf(646,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,f2(f2(a3,x6461),x6462))),f2(a1,f2(a1,x6463))),f2(f2(a1,f2(a1,f2(a1,x6461))),f2(a1,f2(a1,f2(a1,f2(x6462,x6463))))))), % 77.56/77.54 inference(scs_inference,[],[6,642,643,2,3])). % 77.56/77.54 cnf(648,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,f2(a1,x6481))),f2(a1,f2(a1,f2(a1,f2(x6482,x6483))))),f2(f2(a1,f2(a1,f2(f2(a3,x6481),x6482))),f2(a1,f2(a1,x6483))))), % 77.56/77.54 inference(scs_inference,[],[646,2])). % 77.56/77.54 cnf(649,plain, % 77.56/77.54 (E(f2(f2(a1,f2(f2(a3,f2(a1,x6491)),a1)),f2(a1,f2(x6492,x6493))),f2(f2(a1,f2(f2(a3,x6491),x6492)),f2(a1,x6493)))), % 77.56/77.54 inference(scs_inference,[],[6,645,646,2,3])). % 77.56/77.54 cnf(651,plain, % 77.56/77.54 (E(f2(f2(a1,f2(f2(a3,x6511),x6512)),f2(a1,x6513)),f2(f2(a1,f2(f2(a3,f2(a1,x6511)),a1)),f2(a1,f2(x6512,x6513))))), % 77.56/77.54 inference(scs_inference,[],[649,2])). % 77.56/77.54 cnf(652,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,f2(a1,f2(a1,f2(x6521,x6522))))),f2(a1,f2(a1,f2(a1,x6523)))),f2(f2(a1,f2(a1,f2(f2(a3,x6523),x6521))),f2(a1,f2(a1,x6522))))), % 77.56/77.54 inference(scs_inference,[],[6,648,649,2,3])). % 77.56/77.54 cnf(654,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,f2(f2(a3,x6541),x6542))),f2(a1,f2(a1,x6543))),f2(f2(a1,f2(a1,f2(a1,f2(a1,f2(x6542,x6543))))),f2(a1,f2(a1,f2(a1,x6541)))))), % 77.56/77.54 inference(scs_inference,[],[652,2])). % 77.56/77.54 cnf(655,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,x6551)),f2(a1,f2(f2(a3,x6552),x6553))),f2(f2(a1,f2(f2(a3,f2(a1,x6552)),a1)),f2(a1,f2(x6553,x6551))))), % 77.56/77.54 inference(scs_inference,[],[6,651,652,2,3])). % 77.56/77.54 cnf(657,plain, % 77.56/77.54 (E(f2(f2(a1,f2(f2(a3,f2(a1,x6571)),a1)),f2(a1,f2(x6572,x6573))),f2(f2(a1,f2(a1,x6573)),f2(a1,f2(f2(a3,x6571),x6572))))), % 77.56/77.54 inference(scs_inference,[],[655,2])). % 77.56/77.54 cnf(658,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,f2(a1,x6581))),f2(a1,f2(a1,f2(f2(a3,x6582),x6583)))),f2(f2(a1,f2(a1,f2(a1,f2(a1,f2(x6583,x6581))))),f2(a1,f2(a1,f2(a1,x6582)))))), % 77.56/77.54 inference(scs_inference,[],[6,654,655,2,3])). % 77.56/77.54 cnf(660,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,f2(a1,f2(a1,f2(x6601,x6602))))),f2(a1,f2(a1,f2(a1,x6603)))),f2(f2(a1,f2(a1,f2(a1,x6602))),f2(a1,f2(a1,f2(f2(a3,x6603),x6601)))))), % 77.56/77.54 inference(scs_inference,[],[658,2])). % 77.56/77.54 cnf(661,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,f2(x6611,x6612))),f2(a1,f2(f2(a3,f2(a1,x6613)),a1))),f2(f2(a1,f2(a1,x6612)),f2(a1,f2(f2(a3,x6613),x6611))))), % 77.56/77.54 inference(scs_inference,[],[6,657,658,2,3])). % 77.56/77.54 cnf(663,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,x6631)),f2(a1,f2(f2(a3,x6632),x6633))),f2(f2(a1,f2(a1,f2(x6633,x6631))),f2(a1,f2(f2(a3,f2(a1,x6632)),a1))))), % 77.56/77.54 inference(scs_inference,[],[661,2])). % 77.56/77.54 cnf(664,plain, % 77.56/77.54 (E(f2(f2(a1,x6641),f2(a1,f2(x6642,x6643))),f2(f2(a1,f2(a1,f2(a1,f2(a1,f2(a1,f2(x6642,x6643)))))),f2(a1,f2(a1,f2(a1,f2(a1,x6641))))))), % 77.56/77.54 inference(scs_inference,[],[6,200,661,2,3])). % 77.56/77.54 cnf(667,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,f2(a1,f2(a1,f2(a1,f2(x6671,x6672)))))),f2(a1,f2(a1,f2(a1,f2(a1,x6673))))),f2(f2(a1,x6673),f2(a1,f2(x6671,x6672))))), % 77.56/77.54 inference(scs_inference,[],[664,2])). % 77.56/77.54 cnf(668,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,f2(f2(a3,x6681),x6682))),f2(a1,f2(a1,x6683))),f2(f2(a1,f2(a1,f2(x6682,x6683))),f2(a1,f2(f2(a3,f2(a1,x6681)),a1))))), % 77.56/77.54 inference(scs_inference,[],[6,663,664,2,3])). % 77.56/77.54 cnf(670,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,f2(x6701,x6702))),f2(a1,f2(f2(a3,f2(a1,x6703)),a1))),f2(f2(a1,f2(a1,f2(f2(a3,x6703),x6701))),f2(a1,f2(a1,x6702))))), % 77.56/77.54 inference(scs_inference,[],[668,2])). % 77.56/77.54 cnf(671,plain, % 77.56/77.54 (E(f2(f2(a1,f2(f2(a3,x6711),x6712)),f2(a1,x6713)),f2(f2(a1,f2(a1,f2(a1,f2(a1,f2(x6712,x6713))))),f2(a1,f2(a1,f2(a1,x6711)))))), % 77.56/77.54 inference(scs_inference,[],[6,98,668,2,3])). % 77.56/77.54 cnf(673,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,f2(a1,f2(a1,f2(x6731,x6732))))),f2(a1,f2(a1,f2(a1,x6733)))),f2(f2(a1,f2(f2(a3,x6733),x6731)),f2(a1,x6732)))), % 77.56/77.54 inference(scs_inference,[],[671,2])). % 77.56/77.54 cnf(674,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,f2(f2(a3,f2(a1,x6741)),a1))),f2(a1,f2(a1,f2(x6742,x6743)))),f2(f2(a1,f2(a1,f2(f2(a3,x6741),x6742))),f2(a1,f2(a1,x6743))))), % 77.56/77.54 inference(scs_inference,[],[6,670,671,2,3])). % 77.56/77.54 cnf(676,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,f2(f2(a3,x6761),x6762))),f2(a1,f2(a1,x6763))),f2(f2(a1,f2(a1,f2(f2(a3,f2(a1,x6761)),a1))),f2(a1,f2(a1,f2(x6762,x6763)))))), % 77.56/77.54 inference(scs_inference,[],[674,2])). % 77.56/77.54 cnf(677,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,f2(a1,f2(a1,x6771)))),f2(a1,f2(a1,f2(a1,f2(a1,f2(x6772,x6773)))))),f2(f2(a1,f2(f2(a3,x6771),x6772)),f2(a1,x6773)))), % 77.56/77.54 inference(scs_inference,[],[6,673,674,2,3])). % 77.56/77.54 cnf(679,plain, % 77.56/77.54 (E(f2(f2(a1,f2(f2(a3,x6791),x6792)),f2(a1,x6793)),f2(f2(a1,f2(a1,f2(a1,f2(a1,x6791)))),f2(a1,f2(a1,f2(a1,f2(a1,f2(x6792,x6793)))))))), % 77.56/77.54 inference(scs_inference,[],[677,2])). % 77.56/77.54 cnf(680,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,f2(a1,x6801))),f2(a1,f2(a1,f2(f2(a3,x6802),x6803)))),f2(f2(a1,f2(a1,f2(f2(a3,f2(a1,x6802)),a1))),f2(a1,f2(a1,f2(x6803,x6801)))))), % 77.56/77.54 inference(scs_inference,[],[6,676,677,2,3])). % 77.56/77.54 cnf(682,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,f2(f2(a3,f2(a1,x6821)),a1))),f2(a1,f2(a1,f2(x6822,x6823)))),f2(f2(a1,f2(a1,f2(a1,x6823))),f2(a1,f2(a1,f2(f2(a3,x6821),x6822)))))), % 77.56/77.54 inference(scs_inference,[],[680,2])). % 77.56/77.54 cnf(683,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,x6831)),f2(a1,f2(f2(a3,x6832),x6833))),f2(f2(a1,f2(a1,f2(a1,f2(a1,x6832)))),f2(a1,f2(a1,f2(a1,f2(a1,f2(x6833,x6831)))))))), % 77.56/77.54 inference(scs_inference,[],[6,679,680,2,3])). % 77.56/77.54 cnf(685,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,f2(a1,f2(a1,x6851)))),f2(a1,f2(a1,f2(a1,f2(a1,f2(x6852,x6853)))))),f2(f2(a1,f2(a1,x6853)),f2(a1,f2(f2(a3,x6851),x6852))))), % 77.56/77.54 inference(scs_inference,[],[683,2])). % 77.56/77.54 cnf(686,plain, % 77.56/77.54 (E(f2(f2(f2(a3,f2(a1,x6861)),f2(a3,f2(a1,x6862))),f2(a3,x6863)),f2(f2(a1,f2(a3,f2(f2(a3,f2(a1,x6863)),a1))),f2(f2(a3,f2(a1,x6861)),f2(a3,f2(a1,x6862)))))), % 77.56/77.54 inference(scs_inference,[],[7,574,683,2,3])). % 77.56/77.54 cnf(688,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a3,f2(f2(a3,f2(a1,x6881)),a1))),f2(f2(a3,f2(a1,x6882)),f2(a3,f2(a1,x6883)))),f2(f2(f2(a3,f2(a1,x6882)),f2(a3,f2(a1,x6883))),f2(a3,x6881)))), % 77.56/77.54 inference(scs_inference,[],[686,2])). % 77.56/77.54 cnf(735,plain, % 77.56/77.54 (E(f2(f2(a1,f2(f2(a3,f2(f2(a3,f2(a1,x7351)),a1)),x7352)),f2(a1,x7353)),f2(f2(f2(a3,f2(a1,x7352)),f2(a3,f2(a1,x7353))),f2(a3,x7351)))), % 77.56/77.54 inference(scs_inference,[],[7,527,3,2])). % 77.56/77.54 cnf(739,plain, % 77.56/77.54 (E(f2(f2(a1,f2(f2(a3,f2(a1,f2(x7391,x7392))),f2(a3,f2(a1,x7393)))),f2(a1,a1)),f2(f2(f2(a3,f2(a1,f2(f2(a3,x7393),x7391))),a1),x7392))), % 77.56/77.54 inference(scs_inference,[],[7,481,3,2])). % 77.56/77.54 cnf(776,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,f2(f2(a3,x7761),x7762))),f2(a1,f2(a1,x7763))),f2(f2(f2(a3,f2(a1,f2(a1,a1))),a1),f2(f2(a3,f2(a1,f2(x7762,x7763))),f2(a3,f2(a1,x7761)))))), % 77.56/77.54 inference(scs_inference,[],[7,490,3,2])). % 77.56/77.54 cnf(793,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,f2(x7931,f2(x7932,x7933)))),f2(a1,x7934)),f2(f2(f2(a3,f2(a1,x7932)),f2(a3,f2(a1,x7933))),f2(a3,f2(f2(a3,x7934),x7931))))), % 77.56/77.54 inference(scs_inference,[],[7,543,3,2])). % 77.56/77.54 cnf(797,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,f2(x7971,f2(x7972,x7973)))),f2(f2(a3,f2(a1,f2(a1,x7974))),a1)),f2(f2(f2(a3,f2(a1,x7973)),f2(a3,f2(f2(a3,x7974),x7971))),x7972))), % 77.56/77.54 inference(scs_inference,[],[7,581,3,2])). % 77.56/77.54 cnf(801,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,f2(a1,f2(x8011,x8012)))),f2(f2(a3,f2(a1,f2(a1,f2(a1,x8013)))),a1)),f2(f2(f2(a3,f2(a1,x8012)),f2(a3,x8013)),x8011))), % 77.56/77.54 inference(scs_inference,[],[7,436,3,2])). % 77.56/77.54 cnf(834,plain, % 77.56/77.54 (E(f2(f2(a1,f2(f2(a3,f2(a1,x8341)),a1)),f2(a1,f2(x8342,x8343))),f2(f2(f2(a3,f2(a1,f2(f2(a3,x8341),x8342))),a1),x8343))), % 77.56/77.54 inference(scs_inference,[],[7,651,3,2])). % 77.56/77.54 cnf(838,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,f2(a3,x8381))),f2(a1,f2(f2(a3,f2(a1,x8382)),f2(a3,f2(a1,x8383))))),f2(f2(f2(a3,f2(a1,f2(f2(a3,x8381),x8382))),a1),x8383))), % 77.56/77.54 inference(scs_inference,[],[7,422,3,2])). % 77.56/77.54 cnf(855,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,f2(a1,f2(x8551,x8552)))),f2(a1,f2(a1,x8553))),f2(f2(f2(a3,f2(a1,f2(f2(a3,x8553),x8551))),a1),x8552))), % 77.56/77.54 inference(scs_inference,[],[7,630,3,2])). % 77.56/77.54 cnf(874,plain, % 77.56/77.54 (E(f2(f2(a1,f2(f2(a3,f2(a1,f2(a3,x8741))),f2(a3,f2(a1,f2(x8742,x8743))))),f2(a1,f2(a3,f2(a1,x8744)))),f2(f2(f2(a3,f2(a1,f2(a1,x8744))),a1),f2(f2(a3,x8741),f2(x8742,x8743))))), % 77.56/77.54 inference(scs_inference,[],[7,356,3,2])). % 77.56/77.54 cnf(883,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,f2(f2(a3,f2(a1,x8831)),f2(a3,f2(a1,x8832))))),f2(a1,f2(a1,f2(a3,x8833)))),f2(f2(f2(a3,f2(a1,f2(a1,x8832))),a1),f2(f2(a3,x8833),x8831)))), % 77.56/77.54 inference(scs_inference,[],[7,428,3,2])). % 77.56/77.54 cnf(906,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,f2(f2(a3,x9061),x9062))),f2(a1,f2(a1,x9063))),f2(f2(f2(a3,f2(a1,f2(a1,f2(x9062,x9063)))),a1),f2(f2(a3,f2(a1,x9061)),a1)))), % 77.56/77.54 inference(scs_inference,[],[7,670,3,2])). % 77.56/77.54 cnf(909,plain, % 77.56/77.54 (E(f2(f2(a1,f2(a1,f2(f2(a3,x9091),x9092))),f2(a1,f2(a1,x9093))),f2(f2(f2(a3,f2(a1,f2(a1,f2(a1,x9091)))),a1),f2(a1,f2(a1,f2(x9092,x9093)))))), % 77.56/77.54 inference(scs_inference,[],[7,648,3,2])). % 77.56/77.54 cnf(921,plain, % 77.56/77.54 (E(f2(f2(f2(a3,f2(a1,f2(a1,f2(a1,f2(x9211,x9212))))),f2(a3,f2(a1,f2(a1,f2(a1,x9213))))),a1),f2(f2(a1,f2(x9211,x9212)),x9213))), % 77.56/77.54 inference(scs_inference,[],[7,245,3])). % 77.56/77.54 cnf(923,plain, % 77.56/77.54 (E(f2(f2(a1,f2(x9231,x9232)),x9233),f2(f2(f2(a3,f2(a1,f2(a1,f2(a1,f2(x9231,x9232))))),f2(a3,f2(a1,f2(a1,f2(a1,x9233))))),a1))), % 77.56/77.54 inference(scs_inference,[],[921,2])). % 77.56/77.54 cnf(941,plain, % 77.56/77.54 (E(f2(f2(f2(a3,f2(a1,f2(f2(a3,f2(a1,f2(x9411,x9412))),f2(x9413,x9414)))),f2(a3,f2(a1,f2(a1,x9415)))),a1),f2(f2(f2(a3,f2(f2(x9413,x9414),x9415)),x9411),x9412))), % 77.56/77.54 inference(scs_inference,[],[7,285,3,2])). % 77.56/77.54 cnf(956,plain, % 77.56/77.54 (E(f2(f2(f2(x9561,x9562),x9563),x9564),f2(f2(f2(a3,f2(a1,f2(x9561,x9562))),f2(a3,f2(a1,x9563))),f2(a3,f2(a1,x9564))))), % 77.56/77.54 inference(scs_inference,[],[7,269,3,2])). % 77.56/77.54 cnf(957,plain, % 77.56/77.54 (E(f2(f2(f2(a3,f2(f2(x9571,x9572),x9573)),x9574),x9575),f2(f2(f2(a3,f2(a1,f2(x9571,x9572))),f2(a3,f2(a1,x9573))),f2(a3,f2(a1,f2(x9574,x9575)))))), % 77.56/77.54 inference(scs_inference,[],[7,956,3])). % 77.56/77.54 cnf(986,plain, % 77.56/77.55 (E(f2(f2(a1,f2(a3,f2(f2(a3,f2(a1,f2(a1,x9861))),a1))),f2(f2(a3,f2(a1,a1)),f2(a3,f2(a1,f2(x9862,x9863))))),f2(f2(f2(a3,f2(a1,x9863)),f2(a3,x9861)),x9862))), % 77.56/77.55 inference(scs_inference,[],[7,276,3,2])). % 77.56/77.55 cnf(990,plain, % 77.56/77.55 (E(f2(f2(a1,f2(f2(a3,f2(f2(a3,f2(a1,x9901)),a1)),f2(x9902,x9903))),f2(f2(a3,f2(a1,f2(a1,x9904))),a1)),f2(f2(f2(a3,f2(f2(a3,f2(a1,x9904)),f2(a3,x9901))),x9902),x9903))), % 77.56/77.55 inference(scs_inference,[],[7,145,3,2])). % 77.56/77.55 cnf(994,plain, % 77.56/77.55 (E(f2(f2(a1,f2(f2(a3,f2(f2(a3,x9941),x9942)),x9943)),f2(a1,x9944)),f2(f2(f2(a3,f2(a1,f2(x9943,x9944))),f2(a3,x9941)),x9942))), % 77.56/77.55 inference(scs_inference,[],[7,141,3,2])). % 77.56/77.55 cnf(1008,plain, % 77.56/77.55 (E(f2(f2(a1,f2(x10081,x10082)),f2(f2(a3,f2(a1,x10083)),a1)),f2(f2(f2(a3,f2(a1,x10082)),f2(a3,x10083)),x10081))), % 77.56/77.55 inference(scs_inference,[],[7,189,3,2])). % 77.56/77.55 cnf(1009,plain, % 77.56/77.55 (E(f2(f2(f2(a3,f2(a1,f2(x10091,x10092))),f2(a3,f2(a1,x10093))),a1),f2(f2(f2(a3,f2(a1,x10092)),f2(a3,x10093)),x10091))), % 77.56/77.55 inference(scs_inference,[],[7,1008,3])). % 77.56/77.55 cnf(1019,plain, % 77.56/77.55 (E(f2(f2(a1,f2(a1,f2(a1,f2(a1,f2(x10191,x10192))))),f2(a1,f2(a1,f2(a1,x10193)))),f2(f2(f2(a3,f2(a1,x10192)),f2(a3,x10193)),x10191))), % 77.56/77.55 inference(scs_inference,[],[7,98,3,2])). % 77.56/77.55 cnf(1022,plain, % 77.56/77.55 (E(f2(f2(f2(a3,f2(a1,x10221)),f2(a3,x10222)),x10223),f2(f2(a1,f2(x10223,x10221)),x10222))), % 77.56/77.55 inference(scs_inference,[],[7,105,3])). % 77.56/77.55 cnf(1025,plain, % 77.56/77.55 (E(f2(f2(a1,f2(x10251,x10252)),x10253),f2(f2(f2(a3,f2(a1,x10252)),f2(a3,x10253)),x10251))), % 77.56/77.55 inference(scs_inference,[],[7,105,3,2])). % 77.56/77.55 cnf(1039,plain, % 77.56/77.55 (E(f2(f2(f2(a3,f2(x10391,x10392)),x10393),x10394),f2(f2(f2(a3,f2(a1,f2(x10393,x10394))),x10391),x10392))), % 77.56/77.55 inference(scs_inference,[],[7,13,3,2])). % 77.56/77.55 cnf(1048,plain, % 77.56/77.55 (E(f2(f2(f2(a3,f2(a1,a1)),f2(a3,f2(a1,f2(x10481,x10482)))),f2(a3,f2(f2(a3,f2(a1,f2(a1,x10483))),a1))),f2(f2(f2(a3,f2(a1,x10482)),f2(a3,x10483)),x10481))), % 77.56/77.55 inference(scs_inference,[],[9,986,3])). % 77.56/77.55 cnf(1051,plain, % 77.56/77.55 (E(f2(f2(a1,a1),f2(f2(a3,f2(a1,f2(x10511,x10512))),f2(a3,f2(a1,x10513)))),f2(f2(f2(a3,f2(a1,f2(f2(a3,x10513),x10511))),a1),x10512))), % 77.56/77.55 inference(scs_inference,[],[9,739,1048,2,3])). % 77.56/77.55 cnf(1054,plain, % 77.56/77.55 (E(f2(f2(a1,x10541),f2(f2(a3,f2(f2(a3,x10542),x10543)),x10544)),f2(f2(f2(a3,f2(a1,f2(x10544,x10541))),f2(a3,x10542)),x10543))), % 77.56/77.55 inference(scs_inference,[],[9,994,1051,2,3])). % 77.56/77.55 cnf(1057,plain, % 77.56/77.55 (E(f2(f2(f2(a3,f2(a1,f2(a1,x10571))),a1),f2(f2(a3,f2(f2(a3,f2(a1,x10572)),a1)),f2(x10573,x10574))),f2(f2(f2(a3,f2(f2(a3,f2(a1,x10571)),f2(a3,x10572))),x10573),x10574))), % 77.56/77.55 inference(scs_inference,[],[9,990,1054,2,3])). % 77.56/77.55 cnf(1060,plain, % 77.56/77.55 (E(f2(f2(a1,f2(a1,x10601)),f2(a1,f2(f2(a3,x10602),x10603))),f2(f2(f2(a3,f2(a1,f2(a1,a1))),a1),f2(f2(a3,f2(a1,f2(x10603,x10601))),f2(a3,f2(a1,x10602)))))), % 77.56/77.55 inference(scs_inference,[],[9,776,1057,2,3])). % 77.56/77.55 cnf(1063,plain, % 77.56/77.55 (E(f2(f2(f2(a3,f2(a1,f2(a1,x10631))),a1),f2(a1,f2(x10632,f2(x10633,x10634)))),f2(f2(f2(a3,f2(a1,x10634)),f2(a3,f2(f2(a3,x10631),x10632))),x10633))), % 77.56/77.55 inference(scs_inference,[],[9,797,1060,2,3])). % 77.56/77.55 cnf(1066,plain, % 77.56/77.55 (E(f2(f2(f2(a3,f2(a1,f2(x10661,x10662))),f2(a3,f2(a1,x10663))),f2(a3,f2(f2(a3,f2(a1,x10664)),a1))),f2(f2(a1,x10662),f2(f2(a3,f2(f2(a3,f2(a1,x10663)),f2(a3,x10664))),x10661)))), % 77.56/77.55 inference(scs_inference,[],[9,561,1063,2,3])). % 77.56/77.55 cnf(1069,plain, % 77.56/77.55 (E(f2(f2(a1,f2(f2(a3,f2(a1,x10691)),f2(a3,f2(a1,x10692)))),f2(a1,f2(a3,f2(f2(a3,f2(a1,x10693)),a1)))),f2(f2(a1,x10691),f2(f2(a3,f2(a1,x10692)),f2(a3,x10693))))), % 77.56/77.55 inference(scs_inference,[],[9,605,1066,2,3])). % 77.56/77.55 cnf(1072,plain, % 77.56/77.55 (E(f2(f2(a1,f2(x10721,x10722)),f2(f2(a3,f2(a1,x10723)),a1)),f2(f2(f2(a3,f2(a1,f2(f2(a3,x10723),x10721))),a1),x10722))), % 77.56/77.55 inference(scs_inference,[],[9,834,1069,2,3])). % 77.56/77.55 cnf(1075,plain, % 77.56/77.55 (E(f2(f2(a1,f2(a1,f2(a1,f2(x10751,x10752)))),f2(f2(a3,f2(a1,f2(a1,f2(a1,x10753)))),a1)),f2(f2(a1,x10753),f2(a1,f2(x10751,x10752))))), % 77.56/77.55 inference(scs_inference,[],[9,414,1072,2,3])). % 77.56/77.55 cnf(1078,plain, % 77.56/77.55 (E(f2(f2(a1,f2(a1,f2(a1,f2(a1,x10781)))),f2(a1,f2(a1,f2(a1,f2(a1,f2(x10782,x10783)))))),f2(f2(a1,x10781),f2(a1,f2(x10782,x10783))))), % 77.56/77.55 inference(scs_inference,[],[9,667,1075,2,3])). % 77.56/77.55 cnf(1080,plain, % 77.56/77.55 (E(f2(f2(a1,x10801),f2(a1,f2(x10802,x10803))),f2(f2(a1,f2(a1,f2(a1,f2(a1,x10801)))),f2(a1,f2(a1,f2(a1,f2(a1,f2(x10802,x10803)))))))), % 77.56/77.55 inference(scs_inference,[],[1078,2])). % 77.56/77.55 cnf(1081,plain, % 77.56/77.55 (E(f2(f2(a1,x10811),f2(f2(a3,f2(f2(a3,f2(a1,x10812)),a1)),x10813)),f2(f2(f2(a3,f2(a1,x10813)),f2(a3,f2(a1,x10811))),f2(a3,x10812)))), % 77.56/77.55 inference(scs_inference,[],[9,735,1078,2,3])). % 77.56/77.55 cnf(1083,plain, % 77.56/77.55 (E(f2(f2(f2(a3,f2(a1,x10831)),f2(a3,f2(a1,x10832))),f2(a3,x10833)),f2(f2(a1,x10832),f2(f2(a3,f2(f2(a3,f2(a1,x10833)),a1)),x10831)))), % 77.56/77.55 inference(scs_inference,[],[1081,2])). % 77.56/77.55 cnf(1084,plain, % 77.56/77.55 (E(f2(f2(f2(a3,f2(a1,a1)),f2(a3,f2(a1,f2(x10841,x10842)))),f2(a3,f2(f2(a3,f2(a1,f2(a1,x10843))),a1))),f2(f2(a1,f2(f2(a3,x10843),x10841)),f2(a1,x10842)))), % 77.56/77.55 inference(scs_inference,[],[9,608,1081,2,3])). % 77.56/77.55 cnf(1086,plain, % 77.56/77.55 (E(f2(f2(a1,f2(f2(a3,x10861),x10862)),f2(a1,x10863)),f2(f2(f2(a3,f2(a1,a1)),f2(a3,f2(a1,f2(x10862,x10863)))),f2(a3,f2(f2(a3,f2(a1,f2(a1,x10861))),a1))))), % 77.56/77.55 inference(scs_inference,[],[1084,2])). % 77.56/77.55 cnf(1087,plain, % 77.56/77.55 (E(f2(f2(a1,f2(a3,f2(a1,x10871))),f2(f2(a3,f2(a1,f2(a3,x10872))),f2(a3,f2(a1,f2(x10873,x10874))))),f2(f2(a1,x10874),f2(f2(a3,f2(f2(a3,f2(a1,x10871)),f2(a3,x10872))),x10873)))), % 77.56/77.55 inference(scs_inference,[],[9,385,1084,2,3])). % 77.56/77.55 cnf(1090,plain, % 77.56/77.55 (E(f2(f2(a1,x10901),f2(f2(a3,x10902),x10903)),f2(f2(f2(a3,f2(a1,a1)),f2(a3,f2(a1,f2(x10903,x10901)))),f2(a3,f2(f2(a3,f2(a1,f2(a1,x10902))),a1))))), % 77.56/77.55 inference(scs_inference,[],[9,1086,1087,2,3])). % 77.56/77.55 cnf(1093,plain, % 77.56/77.55 (E(f2(f2(a1,f2(f2(a3,f2(a1,x10931)),f2(a3,f2(a1,x10932)))),f2(a1,f2(a3,x10933))),f2(f2(f2(a3,f2(a1,f2(f2(a3,x10933),x10931))),a1),x10932))), % 77.56/77.55 inference(scs_inference,[],[9,838,1090,2,3])). % 77.56/77.55 cnf(1096,plain, % 77.56/77.55 (E(f2(f2(a1,f2(a1,a1)),f2(a1,f2(f2(a3,f2(a1,f2(x10961,x10962))),f2(a3,f2(a1,x10963))))),f2(f2(a1,f2(a1,f2(a1,x10962))),f2(a1,f2(a1,f2(f2(a3,x10963),x10961)))))), % 77.56/77.55 inference(scs_inference,[],[9,496,1093,2,3])). % 77.56/77.55 cnf(1099,plain, % 77.56/77.55 (E(f2(f2(a1,f2(a1,x10991)),f2(a1,f2(a1,f2(x10992,x10993)))),f2(f2(f2(a3,f2(a1,f2(f2(a3,x10991),x10992))),a1),x10993))), % 77.56/77.55 inference(scs_inference,[],[9,855,1096,2,3])). % 77.56/77.55 cnf(1102,plain, % 77.56/77.55 (E(f2(f2(f2(a3,f2(a1,f2(a1,f2(a1,x11021)))),a1),f2(a1,f2(a1,f2(x11022,x11023)))),f2(f2(a1,f2(a1,x11021)),f2(a1,f2(a1,f2(x11022,x11023)))))), % 77.56/77.55 inference(scs_inference,[],[9,468,1099,2,3])). % 77.56/77.55 cnf(1104,plain, % 77.56/77.55 (E(f2(f2(a1,f2(a1,x11041)),f2(a1,f2(a1,f2(x11042,x11043)))),f2(f2(f2(a3,f2(a1,f2(a1,f2(a1,x11041)))),a1),f2(a1,f2(a1,f2(x11042,x11043)))))), % 77.56/77.55 inference(scs_inference,[],[1102,2])). % 77.56/77.55 cnf(1105,plain, % 77.56/77.55 (E(f2(f2(a1,f2(a3,f2(a1,x11051))),f2(f2(a3,f2(a1,f2(a3,x11052))),f2(a3,f2(a1,f2(x11053,x11054))))),f2(f2(f2(a3,f2(a1,f2(a1,x11051))),a1),f2(f2(a3,x11052),f2(x11053,x11054))))), % 77.56/77.55 inference(scs_inference,[],[9,874,1102,2,3])). % 77.56/77.55 cnf(1108,plain, % 77.56/77.55 (E(f2(f2(a1,x11081),f2(a1,f2(x11082,f2(x11083,x11084)))),f2(f2(f2(a3,f2(a1,x11083)),f2(a3,f2(a1,x11084))),f2(a3,f2(f2(a3,x11081),x11082))))), % 77.56/77.55 inference(scs_inference,[],[9,793,1105,2,3])). % 77.56/77.55 cnf(1111,plain, % 77.56/77.55 (E(f2(f2(f2(a3,f2(a1,f2(a1,x11111))),a1),f2(f2(a3,f2(f2(a3,f2(a1,x11112)),a1)),x11113)),f2(f2(a1,x11113),f2(f2(a3,f2(a1,x11111)),f2(a3,x11112))))), % 77.56/77.55 inference(scs_inference,[],[9,612,1108,2,3])). % 77.56/77.55 cnf(1113,plain, % 77.56/77.55 (E(f2(f2(a1,x11131),f2(f2(a3,f2(a1,x11132)),f2(a3,x11133))),f2(f2(f2(a3,f2(a1,f2(a1,x11132))),a1),f2(f2(a3,f2(f2(a3,f2(a1,x11133)),a1)),x11131)))), % 77.56/77.55 inference(scs_inference,[],[1111,2])). % 77.56/77.55 cnf(1114,plain, % 77.56/77.55 (E(f2(f2(a1,f2(a1,f2(a3,x11141))),f2(a1,f2(f2(a3,f2(a1,x11142)),f2(a3,f2(a1,x11143))))),f2(f2(f2(a3,f2(a1,f2(a1,x11143))),a1),f2(f2(a3,x11141),x11142)))), % 77.56/77.55 inference(scs_inference,[],[9,883,1111,2,3])). % 77.56/77.55 cnf(1117,plain, % 77.56/77.55 (E(f2(f2(f2(a3,f2(a1,x11171)),f2(a3,x11172)),x11173),f2(f2(f2(a3,f2(a1,f2(a1,x11171))),a1),f2(f2(a3,f2(f2(a3,f2(a1,x11172)),a1)),x11173)))), % 77.56/77.55 inference(scs_inference,[],[9,1113,1114,2,3])). % 77.56/77.55 cnf(1121,plain, % 77.56/77.55 (E(f2(f2(a1,f2(f2(a3,f2(a1,x11211)),f2(a3,f2(a1,x11212)))),f2(a1,f2(a3,f2(f2(a3,f2(a1,x11213)),a1)))),f2(f2(a1,f2(f2(a3,x11213),x11211)),f2(a1,x11212)))), % 77.56/77.55 inference(scs_inference,[],[9,601,1117,2,3])). % 77.56/77.55 cnf(1124,plain, % 77.56/77.55 (E(f2(f2(a1,f2(a1,f2(x11241,x11242))),f2(a1,x11243)),f2(f2(f2(a3,f2(a1,f2(a1,f2(a1,x11243)))),a1),f2(a1,f2(a1,f2(x11241,x11242)))))), % 77.56/77.55 inference(scs_inference,[],[9,1104,1121,2,3])). % 77.56/77.55 cnf(1126,plain, % 77.56/77.55 (E(f2(f2(f2(a3,f2(a1,f2(a1,f2(a1,x11261)))),a1),f2(a1,f2(a1,f2(x11262,x11263)))),f2(f2(a1,f2(a1,f2(x11262,x11263))),f2(a1,x11261)))), % 77.56/77.55 inference(scs_inference,[],[1124,2])). % 77.56/77.55 cnf(1127,plain, % 77.56/77.55 (E(f2(f2(a1,x11271),f2(f2(a3,f2(f2(a3,f2(a1,x11272)),a1)),x11273)),f2(f2(a1,f2(a1,f2(a3,x11272))),f2(a1,f2(f2(a3,f2(a1,x11273)),f2(a3,f2(a1,x11271))))))), % 77.56/77.55 inference(scs_inference,[],[9,448,1124,2,3])). % 77.56/77.55 cnf(1129,plain, % 77.56/77.55 (E(f2(f2(a1,f2(a1,f2(a3,x11291))),f2(a1,f2(f2(a3,f2(a1,x11292)),f2(a3,f2(a1,x11293))))),f2(f2(a1,x11293),f2(f2(a3,f2(f2(a3,f2(a1,x11291)),a1)),x11292)))), % 77.56/77.55 inference(scs_inference,[],[1127,2])). % 77.56/77.55 cnf(1130,plain, % 77.56/77.55 (E(f2(f2(a1,f2(a3,f2(f2(a3,f2(a1,x11301)),x11302))),f2(f2(a3,f2(a1,x11303)),f2(a3,f2(a1,x11304)))),f2(f2(a1,f2(a1,x11301)),f2(a1,f2(x11302,f2(x11303,x11304)))))), % 77.56/77.55 inference(scs_inference,[],[9,381,1127,2,3])). % 77.56/77.55 cnf(1133,plain, % 77.56/77.55 (E(f2(f2(a1,f2(f2(a3,f2(a1,x11331)),f2(a3,f2(a1,x11332)))),f2(a1,f2(a3,x11333))),f2(f2(a1,x11332),f2(f2(a3,f2(f2(a3,f2(a1,x11333)),a1)),x11331)))), % 77.56/77.55 inference(scs_inference,[],[9,1129,1130,2,3])). % 77.56/77.55 cnf(1135,plain, % 77.56/77.55 (E(f2(f2(a1,x11351),f2(f2(a3,f2(f2(a3,f2(a1,x11352)),a1)),x11353)),f2(f2(a1,f2(f2(a3,f2(a1,x11353)),f2(a3,f2(a1,x11351)))),f2(a1,f2(a3,x11352))))), % 77.56/77.55 inference(scs_inference,[],[1133,2])). % 77.56/77.55 cnf(1136,plain, % 77.56/77.55 (E(f2(f2(a1,f2(x11361,x11362)),x11363),f2(f2(a1,f2(a1,f2(a1,f2(a1,x11363)))),f2(a1,f2(a1,f2(a1,f2(a1,f2(x11361,x11362)))))))), % 77.56/77.55 inference(scs_inference,[],[9,1080,1133,2,3])). % 77.56/77.55 cnf(1139,plain, % 77.56/77.55 (E(f2(f2(a1,f2(a1,f2(a1,f2(a1,x11391)))),f2(a1,f2(a1,f2(a1,f2(a1,f2(x11392,x11393)))))),f2(f2(a1,f2(x11392,x11393)),x11391))), % 77.56/77.55 inference(scs_inference,[],[1136,2])). % 77.56/77.55 cnf(1140,plain, % 77.56/77.55 (E(f2(f2(f2(a3,f2(f2(a3,f2(a1,x11401)),a1)),x11402),x11403),f2(f2(a1,f2(f2(a3,f2(a1,x11402)),f2(a3,f2(a1,x11403)))),f2(a1,f2(a3,x11401))))), % 77.56/77.55 inference(scs_inference,[],[9,1135,1136,2,3])). % 77.56/77.55 cnf(1143,plain, % 77.56/77.55 (E(f2(f2(a1,f2(f2(a3,f2(a1,x11431)),f2(a3,f2(a1,x11432)))),f2(a1,f2(a3,x11433))),f2(f2(f2(a3,f2(f2(a3,f2(a1,x11433)),a1)),x11431),x11432))), % 77.56/77.55 inference(scs_inference,[],[1140,2])). % 77.56/77.55 cnf(1144,plain, % 77.56/77.55 (E(f2(f2(a1,f2(a1,f2(a1,f2(a1,f2(x11441,x11442))))),f2(a1,f2(a1,f2(a1,x11443)))),f2(f2(a1,f2(x11441,x11442)),x11443))), % 77.56/77.55 inference(scs_inference,[],[9,1139,1140,2,3])). % 77.56/77.55 cnf(1146,plain, % 77.56/77.55 (E(f2(f2(a1,f2(x11461,x11462)),x11463),f2(f2(a1,f2(a1,f2(a1,f2(a1,f2(x11461,x11462))))),f2(a1,f2(a1,f2(a1,x11463)))))), % 77.56/77.55 inference(scs_inference,[],[1144,2])). % 77.56/77.55 cnf(1147,plain, % 77.56/77.55 (E(f2(f2(a1,f2(a3,x11471)),f2(f2(a3,f2(a1,x11472)),f2(a3,f2(a1,x11473)))),f2(f2(f2(a3,f2(f2(a3,f2(a1,x11471)),a1)),x11472),x11473))), % 77.56/77.55 inference(scs_inference,[],[9,1143,1144,2,3])). % 77.56/77.55 cnf(1150,plain, % 77.56/77.55 (E(f2(x11501,f2(x11502,x11503)),f2(f2(a1,f2(a1,f2(a1,f2(a1,f2(x11502,x11503))))),f2(a1,f2(a1,f2(a1,x11501)))))), % 77.56/77.55 inference(scs_inference,[],[9,1146,1147,2,3])). % 77.56/77.55 cnf(1154,plain, % 77.56/77.55 (E(f2(f2(f2(a3,f2(a1,f2(a1,x11541))),a1),f2(a1,f2(x11542,f2(x11543,x11544)))),f2(f2(a1,f2(f2(a3,f2(f2(a3,x11541),x11542)),x11543)),f2(a1,x11544)))), % 77.56/77.55 inference(scs_inference,[],[9,584,1150,2,3])). % 77.56/77.55 cnf(1157,plain, % 77.56/77.55 (E(f2(f2(a1,x11571),f2(f2(a3,x11572),x11573)),f2(f2(a1,f2(f2(a3,f2(a1,f2(a1,f2(a1,x11572)))),a1)),f2(a1,f2(a1,f2(a1,f2(x11573,x11571))))))), % 77.56/77.55 inference(scs_inference,[],[9,442,1154,2,3])). % 77.56/77.55 cnf(1160,plain, % 77.56/77.55 (E(f2(f2(a1,f2(f2(a3,f2(a1,x11601)),f2(a3,x11602))),f2(a1,x11603)),f2(f2(a1,f2(f2(a3,f2(a1,x11603)),f2(a3,f2(a1,x11601)))),f2(a1,f2(a3,f2(f2(a3,f2(a1,x11602)),a1)))))), % 77.56/77.55 inference(scs_inference,[],[9,451,1157,2,3])). % 77.56/77.55 cnf(1163,plain, % 77.56/77.55 (E(f2(f2(a1,f2(a3,f2(a1,x11631))),f2(f2(a3,f2(a1,f2(a3,x11632))),f2(a3,f2(a1,f2(x11633,x11634))))),f2(f2(a1,f2(a1,f2(f2(a3,x11632),f2(x11633,x11634)))),f2(a1,f2(a1,x11631))))), % 77.56/77.55 inference(scs_inference,[],[9,359,1160,2,3])). % 77.56/77.55 cnf(1166,plain, % 77.56/77.55 (E(f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,x11661))),a1)),f2(a3,f2(a1,f2(x11662,x11663)))),f2(x11664,x11665)),f2(f2(f2(a3,f2(f2(x11664,x11665),x11661)),x11662),x11663))), % 77.56/77.55 inference(scs_inference,[],[1039,941,1163,2,3])). % 77.56/77.55 cnf(1169,plain, % 77.56/77.55 (E(f2(f2(a1,f2(a1,f2(a1,f2(a1,f2(x11691,x11692))))),f2(a1,f2(a1,f2(a1,x11693)))),f2(f2(a1,f2(a1,x11692)),f2(a1,f2(f2(a3,x11693),x11691))))), % 77.56/77.55 inference(scs_inference,[],[9,685,1166,2,3])). % 77.56/77.55 cnf(1172,plain, % 77.56/77.55 (E(f2(f2(a1,f2(a1,f2(a3,x11721))),f2(a1,f2(f2(a3,f2(a1,x11722)),f2(a3,f2(a1,x11723))))),f2(f2(a1,f2(a1,f2(f2(a3,x11721),x11722))),f2(a1,f2(a1,x11723))))), % 77.56/77.55 inference(scs_inference,[],[9,431,1169,2,3])). % 77.56/77.55 cnf(1175,plain, % 77.56/77.55 (E(f2(f2(a1,f2(a1,x11751)),f2(a1,f2(f2(a3,f2(f2(a3,x11752),x11753)),x11754))),f2(f2(a1,f2(a1,f2(f2(a3,x11752),x11753))),f2(a1,f2(a1,f2(x11754,x11751)))))), % 77.56/77.55 inference(scs_inference,[],[9,639,1172,2,3])). % 77.56/77.55 cnf(1178,plain, % 77.56/77.55 (E(f2(f2(a1,f2(a1,x11781)),f2(a1,f2(f2(a3,x11782),x11783))),f2(f2(f2(a3,f2(a1,f2(a1,f2(a1,x11782)))),a1),f2(a1,f2(a1,f2(x11783,x11781)))))), % 77.56/77.55 inference(scs_inference,[],[9,909,1175,2,3])). % 77.56/77.55 cnf(1181,plain, % 77.56/77.55 (E(f2(f2(a1,f2(a1,x11811)),f2(a1,f2(f2(a3,x11812),x11813))),f2(f2(f2(a3,f2(a1,f2(a1,f2(x11813,x11811)))),a1),f2(f2(a3,f2(a1,x11812)),a1)))), % 77.56/77.55 inference(scs_inference,[],[9,906,1178,2,3])). % 77.56/77.55 cnf(1184,plain, % 77.56/77.55 (E(f2(f2(a1,f2(a1,f2(x11841,x11842))),f2(a1,f2(f2(a3,f2(a1,x11843)),a1))),f2(f2(a1,f2(a1,f2(a1,x11842))),f2(a1,f2(a1,f2(f2(a3,x11843),x11841)))))), % 77.56/77.55 inference(scs_inference,[],[9,682,1181,2,3])). % 77.56/77.55 cnf(1187,plain, % 77.56/77.55 (E(f2(f2(a1,f2(a1,f2(a1,x11871))),f2(a1,f2(a1,f2(a1,f2(x11872,x11873))))),f2(f2(a1,f2(a1,f2(a1,x11873))),f2(a1,f2(a1,f2(f2(a3,x11871),x11872)))))), % 77.56/77.55 inference(scs_inference,[],[9,660,1184,2,3])). % 77.56/77.55 cnf(1190,plain, % 77.56/77.55 (E(f2(x11901,f2(x11902,x11903)),f2(f2(f2(a3,f2(a1,f2(a1,f2(a1,f2(x11902,x11903))))),f2(a3,f2(a1,f2(a1,f2(a1,x11901))))),a1))), % 77.56/77.55 inference(scs_inference,[],[9,923,1187,2,3])). % 77.56/77.55 cnf(1194,plain, % 77.56/77.55 (E(f2(x11941,f2(x11942,x11943)),f2(f2(f2(a3,f2(a1,x11943)),f2(a3,x11941)),x11942))), % 77.56/77.55 inference(scs_inference,[],[9,1025,1190,2,3])). % 77.56/77.55 cnf(1197,plain, % 77.56/77.55 (E(f2(f2(f2(a3,f2(a1,x11971)),f2(a3,x11972)),x11973),f2(x11972,f2(x11973,x11971)))), % 77.56/77.55 inference(scs_inference,[],[1194,2])). % 77.56/77.55 cnf(1237,plain, % 77.56/77.55 (E(f2(f2(f2(a3,f2(a1,x12371)),f2(a3,x12372)),x12373),f2(f2(a1,f2(a1,f2(a1,x12372))),f2(a1,f2(a1,f2(a1,f2(x12373,x12371))))))), % 77.56/77.55 inference(scs_inference,[],[9,1019,3,2])). % 77.56/77.55 cnf(1238,plain, % 77.56/77.55 (E(f2(f2(f2(a3,f2(a1,f2(a1,f2(a1,x12381)))),a1),f2(a1,f2(a1,f2(x12382,x12383)))),f2(f2(f2(a3,f2(a1,x12383)),f2(a3,x12381)),x12382))), % 77.56/77.55 inference(scs_inference,[],[9,801,3])). % 77.56/77.55 cnf(1241,plain, % 77.56/77.55 (E(f2(f2(a1,f2(a3,f2(f2(a3,f2(a1,x12411)),a1))),f2(f2(a3,f2(a1,x12412)),f2(a3,f2(a1,x12413)))),f2(f2(a1,x12413),f2(f2(a3,x12411),x12412)))), % 77.56/77.55 inference(scs_inference,[],[9,592,1238,2,3])). % 77.56/77.55 cnf(1243,plain, % 77.56/77.55 (E(f2(f2(a1,x12431),f2(f2(a3,x12432),x12433)),f2(f2(a1,f2(a3,f2(f2(a3,f2(a1,x12432)),a1))),f2(f2(a3,f2(a1,x12433)),f2(a3,f2(a1,x12431)))))), % 77.56/77.55 inference(scs_inference,[],[1241,2])). % 77.56/77.55 cnf(1244,plain, % 77.56/77.55 (E(f2(f2(f2(a3,f2(a1,x12441)),f2(a3,f2(a1,x12442))),f2(a3,f2(f2(a3,f2(a1,x12443)),a1))),f2(f2(f2(a3,f2(a1,x12441)),f2(a3,f2(a1,x12442))),f2(a3,x12443)))), % 77.56/77.55 inference(scs_inference,[],[9,688,1241,2,3])). % 77.56/77.55 cnf(1247,plain, % 77.56/77.55 (E(f2(f2(f2(a3,x12471),x12472),x12473),f2(f2(a1,f2(a3,f2(f2(a3,f2(a1,x12471)),a1))),f2(f2(a3,f2(a1,x12472)),f2(a3,f2(a1,x12473)))))), % 77.56/77.55 inference(scs_inference,[],[9,1243,1244,2,3])). % 77.56/77.55 cnf(1250,plain, % 77.56/77.55 (E(f2(f2(a1,f2(a3,f2(f2(a3,f2(a1,x12501)),a1))),f2(f2(a3,f2(a1,x12502)),f2(a3,f2(a1,x12503)))),f2(f2(f2(a3,x12501),x12502),x12503))), % 77.56/77.55 inference(scs_inference,[],[1247,2])). % 77.56/77.55 cnf(1251,plain, % 77.56/77.55 (E(f2(f2(a1,x12511),f2(f2(a3,f2(f2(a3,f2(a1,x12512)),a1)),f2(x12513,x12514))),f2(f2(a1,x12514),f2(f2(a3,f2(f2(a3,f2(a1,x12511)),f2(a3,x12512))),x12513)))), % 77.56/77.55 inference(scs_inference,[],[9,555,1247,2,3])). % 77.56/77.55 cnf(1254,plain, % 77.56/77.55 (~E(f2(f2(f2(f2(f2(a3,f2(f2(a3,f2(a1,a3)),a3)),a1),a4),a5),a6),f2(f2(f2(a3,f2(a1,a6)),f2(a3,a5)),a4))), % 77.56/77.55 inference(scs_inference,[],[1197,8,1251,2,3])). % 77.56/77.55 cnf(1262,plain, % 77.56/77.55 (E(f2(f2(f2(f2(a3,f2(a1,x12621)),f2(a3,x12622)),x12623),x12624),f2(f2(f2(a1,f2(x12623,x12621)),x12622),x12624))), % 77.56/77.55 inference(scs_inference,[],[1022,4])). % 77.56/77.55 cnf(1263,plain, % 77.56/77.55 (E(f2(x12631,f2(f2(f2(a3,f2(a1,x12632)),f2(a3,x12633)),x12634)),f2(x12631,f2(f2(a1,f2(x12634,x12632)),x12633)))), % 77.56/77.55 inference(scs_inference,[],[1022,4,5])). % 77.56/77.55 cnf(1301,plain, % 77.56/77.55 (E(f2(f2(f2(f2(a3,f2(a1,f2(x13011,x13012))),f2(a3,f2(a1,x13013))),a1),x13014),f2(f2(f2(f2(a3,f2(a1,x13012)),f2(a3,x13013)),x13011),x13014))), % 77.56/77.55 inference(scs_inference,[],[1009,4])). % 77.56/77.55 cnf(1302,plain, % 77.56/77.55 (E(f2(x13021,f2(f2(f2(a3,f2(a1,f2(x13022,x13023))),f2(a3,f2(a1,x13024))),a1)),f2(x13021,f2(f2(f2(a3,f2(a1,x13023)),f2(a3,x13024)),x13022)))), % 77.56/77.55 inference(scs_inference,[],[1009,4,5])). % 77.56/77.55 cnf(1303,plain, % 77.56/77.55 (E(f2(f2(f2(f2(f2(a3,f2(a1,x13031)),f2(a3,x13032)),x13033),x13034),x13035),f2(f2(f2(f2(a1,f2(x13033,x13031)),x13032),x13034),x13035))), % 77.56/77.55 inference(scs_inference,[],[1262,4])). % 77.56/77.55 cnf(1306,plain, % 77.56/77.55 (E(f2(x13061,f2(x13062,f2(f2(f2(a3,f2(a1,x13063)),f2(a3,x13064)),x13065))),f2(x13061,f2(x13062,f2(f2(a1,f2(x13065,x13063)),x13064))))), % 77.56/77.55 inference(scs_inference,[],[1263,4,5])). % 77.56/77.55 cnf(1371,plain, % 77.56/77.55 (E(f2(f2(f2(a1,x13711),x13712),x13713),f2(f2(x13712,x13711),x13713))), % 77.56/77.55 inference(scs_inference,[],[6,4])). % 77.56/77.55 cnf(1372,plain, % 77.56/77.55 (E(f2(x13721,f2(f2(a1,x13722),x13723)),f2(x13721,f2(x13723,x13722)))), % 77.56/77.55 inference(scs_inference,[],[6,4,5])). % 77.56/77.55 cnf(1375,plain, % 77.56/77.55 (E(f2(f2(f2(f2(a1,x13751),x13752),x13753),x13754),f2(f2(f2(x13752,x13751),x13753),x13754))), % 77.56/77.55 inference(scs_inference,[],[1371,4])). % 77.56/77.55 cnf(1376,plain, % 77.56/77.55 (E(f2(x13761,f2(f2(f2(a1,x13762),x13763),x13764)),f2(x13761,f2(f2(x13763,x13762),x13764)))), % 77.56/77.55 inference(scs_inference,[],[1371,4,5])). % 77.56/77.55 cnf(1377,plain, % 77.56/77.55 (E(f2(f2(x13771,f2(f2(a1,x13772),x13773)),x13774),f2(f2(x13771,f2(x13773,x13772)),x13774))), % 77.56/77.55 inference(scs_inference,[],[1372,4])). % 77.56/77.55 cnf(1378,plain, % 77.56/77.55 (E(f2(x13781,f2(x13782,f2(f2(a1,x13783),x13784))),f2(x13781,f2(x13782,f2(x13784,x13783))))), % 77.56/77.55 inference(scs_inference,[],[1372,4,5])). % 77.56/77.55 cnf(1379,plain, % 77.56/77.55 (E(f2(f2(f2(f2(f2(a1,x13791),x13792),x13793),x13794),x13795),f2(f2(f2(f2(x13792,x13791),x13793),x13794),x13795))), % 77.56/77.55 inference(scs_inference,[],[1375,4])). % 77.56/77.55 cnf(1382,plain, % 77.56/77.55 (E(f2(x13821,f2(x13822,f2(f2(f2(a1,x13823),x13824),x13825))),f2(x13821,f2(x13822,f2(f2(x13824,x13823),x13825))))), % 77.56/77.55 inference(scs_inference,[],[1376,4,5])). % 77.56/77.55 cnf(1385,plain, % 77.56/77.55 (E(f2(f2(f2(x13851,f2(f2(a1,x13852),x13853)),x13854),x13855),f2(f2(f2(x13851,f2(x13853,x13852)),x13854),x13855))), % 77.56/77.55 inference(scs_inference,[],[1377,4])). % 77.56/77.55 cnf(1387,plain, % 77.56/77.55 (E(f2(f2(x13871,f2(x13872,f2(f2(a1,x13873),x13874))),x13875),f2(f2(x13871,f2(x13872,f2(x13874,x13873))),x13875))), % 77.56/77.55 inference(scs_inference,[],[1378,4])). % 77.56/77.55 cnf(1393,plain, % 77.56/77.55 (E(f2(f2(a1,x13931),f2(f2(f2(f2(a1,x13932),x13933),x13934),x13935)),f2(f2(f2(f2(x13933,x13932),x13934),x13935),x13931))), % 77.56/77.55 inference(scs_inference,[],[6,1379,4,5,3])). % 77.56/77.55 cnf(1399,plain, % 77.56/77.55 (E(f2(f2(f2(f2(a3,x13991),x13992),x13993),x13994),f2(f2(x13991,f2(x13992,x13993)),x13994))), % 77.56/77.55 inference(scs_inference,[],[7,4])). % 77.56/77.55 cnf(1400,plain, % 77.56/77.55 (E(f2(x14001,f2(f2(f2(a3,x14002),x14003),x14004)),f2(x14001,f2(x14002,f2(x14003,x14004))))), % 77.56/77.55 inference(scs_inference,[],[7,4,5])). % 77.56/77.55 cnf(1401,plain, % 77.56/77.55 (E(f2(f2(f2(f2(f2(a3,x14011),x14012),x14013),x14014),x14015),f2(f2(f2(x14011,f2(x14012,x14013)),x14014),x14015))), % 77.56/77.55 inference(scs_inference,[],[1399,4])). % 77.56/77.55 cnf(1402,plain, % 77.56/77.55 (E(f2(x14021,f2(f2(f2(f2(a3,x14022),x14023),x14024),x14025)),f2(x14021,f2(f2(x14022,f2(x14023,x14024)),x14025)))), % 77.56/77.55 inference(scs_inference,[],[1399,4,5])). % 77.56/77.55 cnf(1403,plain, % 77.56/77.55 (E(f2(f2(f2(a3,f2(f2(f2(a3,x14031),x14032),x14033)),x14034),x14035),f2(f2(x14031,f2(x14032,x14033)),f2(x14034,x14035)))), % 77.56/77.55 inference(scs_inference,[],[7,1399,4,5,3])). % 77.56/77.55 cnf(1406,plain, % 77.56/77.55 (E(f2(f2(x14061,f2(f2(f2(a3,x14062),x14063),x14064)),x14065),f2(f2(x14061,f2(x14062,f2(x14063,x14064))),x14065))), % 77.56/77.55 inference(scs_inference,[],[1400,4])). % 77.56/77.55 cnf(1407,plain, % 77.56/77.55 (E(f2(x14071,f2(x14072,f2(f2(f2(a3,x14073),x14074),x14075))),f2(x14071,f2(x14072,f2(x14073,f2(x14074,x14075)))))), % 77.56/77.55 inference(scs_inference,[],[1400,4,5])). % 77.56/77.55 cnf(1408,plain, % 77.56/77.55 (~E(f2(f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5),a6),f2(f2(f2(a3,f2(a1,a6)),f2(a3,a5)),a4))), % 77.56/77.55 inference(scs_inference,[],[1400,1401,1254,4,5,3])). % 77.56/77.55 cnf(1412,plain, % 77.56/77.55 (~E(f2(f2(f2(a3,f2(a1,a6)),f2(a3,a5)),a4),f2(f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5),a6))), % 77.56/77.55 inference(scs_inference,[],[1408,1382,4,5,2])). % 77.56/77.55 cnf(1413,plain, % 77.56/77.55 (~E(f2(f2(a1,a6),f2(f2(a3,a5),a4)),f2(f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5),a6))), % 77.56/77.55 inference(scs_inference,[],[7,1408,1382,4,5,2,3])). % 77.56/77.55 cnf(1417,plain, % 77.56/77.55 (~E(f2(f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5),a6),f2(f2(a1,a6),f2(f2(a3,a5),a4)))), % 77.56/77.55 inference(scs_inference,[],[1413,1385,4,5,2])). % 77.56/77.55 cnf(1418,plain, % 77.56/77.55 (~E(f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,a5))),a1)),a1),f2(a4,a6)),f2(f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5),a6))), % 77.56/77.55 inference(scs_inference,[],[1413,1385,99,4,5,2,3])). % 77.56/77.55 cnf(1428,plain, % 77.56/77.55 (~E(f2(f2(f2(a3,f2(a1,f2(a1,a5))),a1),f2(a1,f2(a4,a6))),f2(f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5),a6))), % 77.56/77.55 inference(scs_inference,[],[7,1387,1418,4,5,3])). % 77.56/77.55 cnf(1430,plain, % 77.56/77.55 (~E(f2(f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5),a6),f2(f2(f2(a3,f2(a1,f2(a1,a5))),a1),f2(a1,f2(a4,a6))))), % 77.56/77.55 inference(scs_inference,[],[7,1387,1418,4,5,3,2])). % 77.56/77.55 cnf(1438,plain, % 77.56/77.55 (~E(f2(f2(a1,f2(a1,a5)),f2(a1,f2(a1,f2(a4,a6)))),f2(f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5),a6))), % 77.56/77.55 inference(scs_inference,[],[7,1402,1428,4,5,3])). % 77.56/77.55 cnf(1440,plain, % 77.56/77.55 (~E(f2(f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5),a6),f2(f2(a1,f2(a1,a5)),f2(a1,f2(a1,f2(a4,a6)))))), % 77.56/77.55 inference(scs_inference,[],[7,1402,1428,4,5,3,2])). % 77.56/77.55 cnf(1443,plain, % 77.56/77.55 (E(f2(f2(f2(a3,x14431),f2(f2(f2(a3,x14432),x14433),x14434)),x14435),f2(x14431,f2(f2(x14432,f2(x14433,x14434)),x14435)))), % 77.56/77.55 inference(scs_inference,[],[7,1406,4,5,3])). % 77.56/77.55 cnf(1448,plain, % 77.56/77.55 (~E(f2(f2(a1,f2(f2(a3,f2(f2(a3,f2(a1,a5)),a1)),a4)),f2(a1,a6)),f2(f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5),a6))), % 77.56/77.55 inference(scs_inference,[],[1407,106,1413,4,5,3])). % 77.56/77.55 cnf(1451,plain, % 77.56/77.55 (E(f2(f2(x14511,x14512),x14513),f2(f2(f2(a1,x14512),x14511),x14513))), % 77.56/77.55 inference(scs_inference,[],[9,1448,2,4])). % 77.56/77.55 cnf(1452,plain, % 77.56/77.55 (E(f2(x14521,f2(x14522,x14523)),f2(x14521,f2(f2(a1,x14523),x14522)))), % 77.56/77.55 inference(scs_inference,[],[9,1448,2,4,5])). % 77.56/77.55 cnf(1453,plain, % 77.56/77.55 (~E(f2(f2(a1,a6),f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5)),f2(f2(a1,a6),f2(f2(a3,a5),a4)))), % 77.56/77.55 inference(scs_inference,[],[9,1417,1448,2,4,5,3])). % 77.56/77.55 cnf(1455,plain, % 77.56/77.55 (~E(f2(f2(a1,a6),f2(f2(a3,a5),a4)),f2(f2(a1,a6),f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5)))), % 77.56/77.55 inference(scs_inference,[],[1453,2])). % 77.56/77.55 cnf(1456,plain, % 77.56/77.55 (E(f2(f2(f2(x14561,x14562),x14563),x14564),f2(f2(f2(f2(a1,x14562),x14561),x14563),x14564))), % 77.56/77.55 inference(scs_inference,[],[1451,1453,2,4])). % 77.56/77.55 cnf(1457,plain, % 77.56/77.55 (E(f2(x14571,f2(f2(x14572,x14573),x14574)),f2(x14571,f2(f2(f2(a1,x14573),x14572),x14574)))), % 77.56/77.55 inference(scs_inference,[],[1451,1453,2,4,5])). % 77.56/77.55 cnf(1458,plain, % 77.56/77.55 (~E(f2(f2(a1,f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5)),f2(a1,a6)),f2(f2(a1,a6),f2(f2(a3,a5),a4)))), % 77.56/77.55 inference(scs_inference,[],[9,1451,1453,2,4,5,3])). % 77.56/77.55 cnf(1460,plain, % 77.56/77.55 (~E(f2(f2(a1,a6),f2(f2(a3,a5),a4)),f2(f2(a1,f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5)),f2(a1,a6)))), % 77.56/77.55 inference(scs_inference,[],[1458,2])). % 77.56/77.55 cnf(1461,plain, % 77.56/77.55 (E(f2(f2(x14611,f2(x14612,x14613)),x14614),f2(f2(x14611,f2(f2(a1,x14613),x14612)),x14614))), % 77.56/77.55 inference(scs_inference,[],[1452,1458,2,4])). % 77.56/77.55 cnf(1462,plain, % 77.56/77.55 (E(f2(x14621,f2(x14622,f2(x14623,x14624))),f2(x14621,f2(x14622,f2(f2(a1,x14624),x14623))))), % 77.56/77.55 inference(scs_inference,[],[1452,1458,2,4,5])). % 77.56/77.55 cnf(1463,plain, % 77.56/77.55 (~E(f2(f2(a1,f2(f2(a3,a5),a4)),f2(a1,a6)),f2(f2(a1,a6),f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5)))), % 77.56/77.55 inference(scs_inference,[],[9,1452,1455,1458,2,4,5,3])). % 77.56/77.55 cnf(1465,plain, % 77.56/77.55 (~E(f2(f2(a1,a6),f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5)),f2(f2(a1,f2(f2(a3,a5),a4)),f2(a1,a6)))), % 77.56/77.55 inference(scs_inference,[],[1463,2])). % 77.56/77.55 cnf(1466,plain, % 77.56/77.55 (E(f2(f2(f2(f2(x14661,x14662),x14663),x14664),x14665),f2(f2(f2(f2(f2(a1,x14662),x14661),x14663),x14664),x14665))), % 77.56/77.55 inference(scs_inference,[],[1456,1463,2,4])). % 77.56/77.55 cnf(1467,plain, % 77.56/77.55 (E(f2(x14671,f2(f2(f2(x14672,x14673),x14674),x14675)),f2(x14671,f2(f2(f2(f2(a1,x14673),x14672),x14674),x14675)))), % 77.56/77.55 inference(scs_inference,[],[1456,1463,2,4,5])). % 77.56/77.55 cnf(1468,plain, % 77.56/77.55 (~E(f2(f2(a1,f2(f2(a3,a5),a4)),f2(a1,a6)),f2(f2(a1,f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5)),f2(a1,a6)))), % 77.56/77.55 inference(scs_inference,[],[9,1456,1460,1463,2,4,5,3])). % 77.56/77.55 cnf(1470,plain, % 77.56/77.55 (~E(f2(f2(a1,f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5)),f2(a1,a6)),f2(f2(a1,f2(f2(a3,a5),a4)),f2(a1,a6)))), % 77.56/77.55 inference(scs_inference,[],[1468,2])). % 77.56/77.55 cnf(1471,plain, % 77.56/77.55 (E(f2(f2(x14711,f2(f2(x14712,x14713),x14714)),x14715),f2(f2(x14711,f2(f2(f2(a1,x14713),x14712),x14714)),x14715))), % 77.56/77.55 inference(scs_inference,[],[1457,1468,2,4])). % 77.56/77.55 cnf(1472,plain, % 77.56/77.55 (E(f2(x14721,f2(x14722,f2(f2(x14723,x14724),x14725))),f2(x14721,f2(x14722,f2(f2(f2(a1,x14724),x14723),x14725))))), % 77.56/77.55 inference(scs_inference,[],[1457,1468,2,4,5])). % 77.56/77.55 cnf(1473,plain, % 77.56/77.55 (~E(f2(f2(f2(a3,f2(a1,a6)),f2(f2(a1,a5),a3)),a4),f2(f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5),a6))), % 77.56/77.55 inference(scs_inference,[],[1457,1461,1412,1468,2,4,5,3])). % 77.56/77.55 cnf(1475,plain, % 77.56/77.55 (~E(f2(f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5),a6),f2(f2(f2(a3,f2(a1,a6)),f2(f2(a1,a5),a3)),a4))), % 77.56/77.55 inference(scs_inference,[],[1473,2])). % 77.56/77.55 cnf(1476,plain, % 77.56/77.55 (E(f2(f2(x14761,f2(x14762,f2(x14763,x14764))),x14765),f2(f2(x14761,f2(x14762,f2(f2(a1,x14764),x14763))),x14765))), % 77.56/77.55 inference(scs_inference,[],[1462,1473,2,4])). % 77.56/77.55 cnf(1477,plain, % 77.56/77.55 (E(f2(x14771,f2(x14772,f2(x14773,f2(x14774,x14775)))),f2(x14771,f2(x14772,f2(x14773,f2(f2(a1,x14775),x14774)))))), % 77.56/77.55 inference(scs_inference,[],[1462,1473,2,4,5])). % 77.56/77.55 cnf(1478,plain, % 77.56/77.55 (~E(f2(f2(a1,f2(a1,a6)),f2(a1,f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5))),f2(f2(a1,f2(f2(a3,a5),a4)),f2(a1,a6)))), % 77.56/77.55 inference(scs_inference,[],[9,1462,1470,1473,2,4,5,3])). % 77.56/77.55 cnf(1480,plain, % 77.56/77.55 (~E(f2(f2(a1,f2(f2(a3,a5),a4)),f2(a1,a6)),f2(f2(a1,f2(a1,a6)),f2(a1,f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5))))), % 77.56/77.55 inference(scs_inference,[],[1478,2])). % 77.56/77.55 cnf(1483,plain, % 77.56/77.55 (E(f2(f2(f2(a3,x14831),f2(f2(f2(a3,x14832),x14833),x14834)),x14835),f2(f2(a1,f2(f2(x14832,f2(x14833,x14834)),x14835)),x14831))), % 77.56/77.55 inference(scs_inference,[],[9,1443,1478,2,4,5,3])). % 77.56/77.55 cnf(1488,plain, % 77.56/77.55 (~E(f2(f2(a1,f2(a1,f2(a1,f2(a4,a6)))),f2(a1,f2(a1,a5))),f2(f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5),a6))), % 77.56/77.55 inference(scs_inference,[],[9,1438,1393,4,5,3])). % 77.56/77.55 cnf(1493,plain, % 77.56/77.55 (~E(f2(f2(f2(f2(f2(a1,a3),f2(a3,f2(a1,a3))),f2(a1,a4)),a5),a6),f2(f2(a1,f2(a1,a5)),f2(a1,f2(a1,f2(a4,a6)))))), % 77.56/77.55 inference(scs_inference,[],[1440,1466,4,5,3])). % 77.56/77.55 cnf(1495,plain, % 77.56/77.55 (~E(f2(f2(a1,f2(a1,a5)),f2(a1,f2(a1,f2(a4,a6)))),f2(f2(f2(f2(f2(a1,a3),f2(a3,f2(a1,a3))),f2(a1,a4)),a5),a6))), % 77.56/77.55 inference(scs_inference,[],[1493,2])). % 77.56/77.55 cnf(1498,plain, % 77.56/77.55 (~E(f2(f2(a1,a6),f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5)),f2(f2(f2(a3,f2(a1,a6)),f2(f2(a1,a5),a3)),a4))), % 77.56/77.55 inference(scs_inference,[],[9,1475,1493,1467,2,4,5,3])). % 77.56/77.55 cnf(1500,plain, % 77.56/77.55 (~E(f2(f2(f2(a3,f2(a1,a6)),f2(f2(a1,a5),a3)),a4),f2(f2(a1,a6),f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5)))), % 77.56/77.55 inference(scs_inference,[],[1498,2])). % 77.56/77.55 cnf(1503,plain, % 77.56/77.55 (~E(f2(f2(a1,f2(f2(f2(a1,a5),a3),a4)),f2(a1,a6)),f2(f2(a1,f2(a1,a6)),f2(a1,f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5))))), % 77.56/77.55 inference(scs_inference,[],[1498,1471,1480,2,4,5,3])). % 77.56/77.55 cnf(1505,plain, % 77.56/77.55 (~E(f2(f2(a1,f2(a1,a6)),f2(a1,f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5))),f2(f2(a1,f2(f2(f2(a1,a5),a3),a4)),f2(a1,a6)))), % 77.56/77.55 inference(scs_inference,[],[1503,2])). % 77.56/77.55 cnf(1506,plain, % 77.56/77.55 (E(f2(f2(x15061,f2(x15062,x15063)),x15064),f2(f2(f2(f2(a3,x15061),x15062),x15063),x15064))), % 77.56/77.55 inference(scs_inference,[],[10,1503,2,4])). % 77.56/77.55 cnf(1507,plain, % 77.56/77.55 (E(f2(x15071,f2(x15072,f2(x15073,x15074))),f2(x15071,f2(f2(f2(a3,x15072),x15073),x15074)))), % 77.56/77.55 inference(scs_inference,[],[10,1503,2,4,5])). % 77.56/77.55 cnf(1508,plain, % 77.56/77.55 (~E(f2(f2(f2(a3,f2(a1,a6)),f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4))),a5),f2(f2(a1,f2(f2(a3,a5),a4)),f2(a1,a6)))), % 77.56/77.55 inference(scs_inference,[],[10,1465,1503,2,4,5,3])). % 77.56/77.55 cnf(1510,plain, % 77.56/77.55 (~E(f2(f2(a1,f2(f2(a3,a5),a4)),f2(a1,a6)),f2(f2(f2(a3,f2(a1,a6)),f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4))),a5))), % 77.56/77.55 inference(scs_inference,[],[1508,2])). % 77.56/77.55 cnf(1511,plain, % 77.56/77.55 (E(f2(f2(f2(x15111,f2(x15112,x15113)),x15114),x15115),f2(f2(f2(f2(f2(a3,x15111),x15112),x15113),x15114),x15115))), % 77.56/77.55 inference(scs_inference,[],[1506,1508,2,4])). % 77.56/77.55 cnf(1512,plain, % 77.56/77.55 (E(f2(x15121,f2(f2(x15122,f2(x15123,x15124)),x15125)),f2(x15121,f2(f2(f2(f2(a3,x15122),x15123),x15124),x15125)))), % 77.56/77.55 inference(scs_inference,[],[1506,1508,2,4,5])). % 77.56/77.55 cnf(1513,plain, % 77.56/77.55 (~E(f2(f2(f2(a3,f2(a1,f2(a1,a5))),a1),f2(a1,f2(a4,a6))),f2(f2(f2(f2(f2(a1,a3),f2(a3,f2(a1,a3))),f2(a1,a4)),a5),a6))), % 77.56/77.55 inference(scs_inference,[],[10,1506,1508,1495,2,4,5,3])). % 77.56/77.55 cnf(1516,plain, % 77.56/77.55 (E(f2(f2(x15161,f2(x15162,f2(x15163,x15164))),x15165),f2(f2(x15161,f2(f2(f2(a3,x15162),x15163),x15164)),x15165))), % 77.56/77.55 inference(scs_inference,[],[1507,1513,2,4])). % 77.56/77.55 cnf(1517,plain, % 77.56/77.55 (E(f2(x15171,f2(x15172,f2(x15173,f2(x15174,x15175)))),f2(x15171,f2(x15172,f2(f2(f2(a3,x15173),x15174),x15175))))), % 77.56/77.55 inference(scs_inference,[],[1507,1513,2,4,5])). % 77.56/77.55 cnf(1518,plain, % 77.56/77.55 (~E(f2(f2(f2(a3,f2(a1,f2(f2(a3,a5),a4))),a1),a6),f2(f2(f2(a3,f2(a1,a6)),f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4))),a5))), % 77.56/77.55 inference(scs_inference,[],[10,1507,1510,1513,2,4,5,3])). % 77.56/77.55 cnf(1520,plain, % 77.56/77.55 (~E(f2(f2(f2(a3,f2(a1,a6)),f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4))),a5),f2(f2(f2(a3,f2(a1,f2(f2(a3,a5),a4))),a1),a6))), % 77.56/77.55 inference(scs_inference,[],[1518,2])). % 77.56/77.55 cnf(1523,plain, % 77.56/77.55 (~E(f2(f2(f2(a3,f2(a1,f2(a1,f2(a1,f2(a4,a6))))),a1),f2(a1,a5)),f2(f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5),a6))), % 77.56/77.55 inference(scs_inference,[],[10,1472,1488,1518,2,4,5,3])). % 77.56/77.55 cnf(1526,plain, % 77.56/77.55 (E(f2(f2(f2(x15261,f2(x15262,f2(x15263,x15264))),x15265),x15266),f2(f2(f2(x15261,f2(x15262,f2(f2(a1,x15264),x15263))),x15265),x15266))), % 77.56/77.55 inference(scs_inference,[],[1476,1523,2,4])). % 77.56/77.55 cnf(1528,plain, % 77.56/77.55 (~E(f2(f2(f2(f2(f2(a3,a3),a1),a6),f2(f2(a1,a5),a3)),a4),f2(f2(a1,a6),f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5)))), % 77.56/77.55 inference(scs_inference,[],[1500,1476,1511,1523,2,4,5,3])). % 77.56/77.55 cnf(1530,plain, % 77.56/77.55 (~E(f2(f2(a1,a6),f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5)),f2(f2(f2(f2(f2(a3,a3),a1),a6),f2(f2(a1,a5),a3)),a4))), % 77.56/77.55 inference(scs_inference,[],[1528,2])). % 77.56/77.55 cnf(1533,plain, % 77.56/77.55 (~E(f2(f2(f2(a3,f2(a1,f2(a1,a6))),a1),f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5)),f2(f2(a1,f2(f2(f2(a1,a5),a3),a4)),f2(a1,a6)))), % 77.56/77.55 inference(scs_inference,[],[10,1477,1528,1505,2,4,5,3])). % 77.56/77.55 cnf(1535,plain, % 77.56/77.55 (~E(f2(f2(a1,f2(f2(f2(a1,a5),a3),a4)),f2(a1,a6)),f2(f2(f2(a3,f2(a1,f2(a1,a6))),a1),f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5)))), % 77.56/77.55 inference(scs_inference,[],[1533,2])). % 77.56/77.55 cnf(1538,plain, % 77.56/77.55 (~E(f2(f2(f2(a3,f2(a1,a6)),f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4))),a5),f2(f2(f2(f2(f2(a3,a3),a1),a6),f2(f2(a1,a5),a3)),a4))), % 77.56/77.55 inference(scs_inference,[],[10,1512,1530,1533,2,4,5,3])). % 77.56/77.55 cnf(1543,plain, % 77.56/77.55 (~E(f2(f2(a1,f2(a1,a5)),f2(a1,f2(f2(f2(a3,a1),a4),a6))),f2(f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5),a6))), % 77.56/77.55 inference(scs_inference,[],[1516,1517,1538,1438,2,4,5,3])). % 77.56/77.55 cnf(1548,plain, % 77.56/77.55 (~E(f2(f2(f2(a3,f2(a1,f2(a1,a5))),a1),f2(f2(f2(a3,a1),a4),a6)),f2(f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5),a6))), % 77.56/77.55 inference(scs_inference,[],[10,1403,1543,2,4,5,3])). % 77.56/77.55 cnf(1553,plain, % 77.56/77.55 (~E(f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,a5))),a1)),f2(f2(a3,a1),a4)),a6),f2(f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5),a6))), % 77.56/77.55 inference(scs_inference,[],[10,1126,1548,2,4,5,3])). % 77.56/77.55 cnf(1558,plain, % 77.56/77.55 (~E(f2(f2(f2(a3,f2(a1,a6)),f2(a3,a5)),a4),f2(f2(a1,a6),f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5)))), % 77.56/77.55 inference(scs_inference,[],[10,1250,1553,1455,2,4,5,3])). % 77.56/77.55 cnf(1560,plain, % 77.56/77.55 (~E(f2(f2(a1,a6),f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5)),f2(f2(f2(a3,f2(a1,a6)),f2(a3,a5)),a4))), % 77.56/77.55 inference(scs_inference,[],[1558,2])). % 77.56/77.55 cnf(1561,plain, % 77.56/77.55 (E(f2(f2(f2(f2(a3,x15611),x15612),x15613),x15614),f2(f2(f2(a1,f2(x15612,x15613)),x15611),x15614))), % 77.56/77.55 inference(scs_inference,[],[11,1558,2,4])). % 77.56/77.55 cnf(1562,plain, % 77.56/77.55 (E(f2(x15621,f2(f2(f2(a3,x15622),x15623),x15624)),f2(x15621,f2(f2(a1,f2(x15623,x15624)),x15622)))), % 77.56/77.55 inference(scs_inference,[],[11,1558,2,4,5])). % 77.56/77.55 cnf(1563,plain, % 77.56/77.55 (~E(f2(f2(a1,f2(a1,f2(a1,a5))),f2(a1,f2(a1,f2(a1,f2(a4,a6))))),f2(f2(a1,a6),f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5)))), % 77.56/77.55 inference(scs_inference,[],[11,1558,1237,2,4,5,3])). % 77.56/77.55 cnf(1566,plain, % 77.56/77.55 (E(f2(f2(f2(f2(f2(a3,x15661),x15662),x15663),x15664),x15665),f2(f2(f2(f2(a1,f2(x15662,x15663)),x15661),x15664),x15665))), % 77.56/77.55 inference(scs_inference,[],[1561,1563,2,4])). % 77.56/77.55 cnf(1567,plain, % 77.56/77.55 (E(f2(x15671,f2(f2(f2(f2(a3,x15672),x15673),x15674),x15675)),f2(x15671,f2(f2(f2(a1,f2(x15673,x15674)),x15672),x15675)))), % 77.56/77.55 inference(scs_inference,[],[1561,1563,2,4,5])). % 77.56/77.55 cnf(1568,plain, % 77.56/77.55 (~E(f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,a4))),a1)),f2(a3,f2(a1,a6))),f2(f2(a1,a5),a3)),f2(f2(f2(a3,f2(a1,f2(a1,a6))),a1),f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5)))), % 77.56/77.55 inference(scs_inference,[],[1561,212,1563,1535,2,4,5,3])). % 77.56/77.55 cnf(1570,plain, % 77.56/77.55 (~E(f2(f2(f2(a3,f2(a1,f2(a1,a6))),a1),f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5)),f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,a4))),a1)),f2(a3,f2(a1,a6))),f2(f2(a1,a5),a3)))), % 77.56/77.55 inference(scs_inference,[],[1568,2])). % 77.56/77.55 cnf(1571,plain, % 77.56/77.55 (E(f2(f2(x15711,f2(f2(f2(a3,x15712),x15713),x15714)),x15715),f2(f2(x15711,f2(f2(a1,f2(x15713,x15714)),x15712)),x15715))), % 77.56/77.55 inference(scs_inference,[],[1562,1568,2,4])). % 77.56/77.55 cnf(1572,plain, % 77.56/77.55 (E(f2(x15721,f2(x15722,f2(f2(f2(a3,x15723),x15724),x15725))),f2(x15721,f2(x15722,f2(f2(a1,f2(x15724,x15725)),x15723))))), % 77.56/77.55 inference(scs_inference,[],[1562,1568,2,4,5])). % 77.56/77.55 cnf(1573,plain, % 77.56/77.55 (~E(f2(f2(a1,f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5)),f2(a1,a6)),f2(f2(f2(a3,f2(a1,f2(f2(a3,a5),a4))),a1),a6))), % 77.56/77.55 inference(scs_inference,[],[11,1562,1520,1568,2,4,5,3])). % 77.56/77.55 cnf(1575,plain, % 77.56/77.55 (~E(f2(f2(f2(a3,f2(a1,f2(f2(a3,a5),a4))),a1),a6),f2(f2(a1,f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5)),f2(a1,a6)))), % 77.56/77.55 inference(scs_inference,[],[1573,2])). % 77.56/77.55 cnf(1578,plain, % 77.56/77.55 (~E(f2(f2(a1,a6),f2(f2(f2(a1,f2(a3,f2(a1,a4))),f2(a1,a3)),a5)),f2(f2(f2(a3,f2(a1,a6)),f2(a3,a5)),a4))), % 77.56/77.55 inference(scs_inference,[],[1560,367,1567,1573,2,4,5,3])). % 77.56/77.55 cnf(1580,plain, % 77.56/77.55 (~E(f2(f2(f2(a3,f2(a1,a6)),f2(a3,a5)),a4),f2(f2(a1,a6),f2(f2(f2(a1,f2(a3,f2(a1,a4))),f2(a1,a3)),a5)))), % 77.56/77.55 inference(scs_inference,[],[1578,2])). % 77.56/77.55 cnf(1583,plain, % 77.56/77.55 (~E(f2(f2(a1,f2(a1,a6)),f2(a1,f2(f2(a3,a5),a4))),f2(f2(a1,f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5)),f2(a1,a6)))), % 77.56/77.55 inference(scs_inference,[],[11,1578,1301,1575,2,4,5,3])). % 77.56/77.55 cnf(1585,plain, % 77.56/77.55 (~E(f2(f2(a1,f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5)),f2(a1,a6)),f2(f2(a1,f2(a1,a6)),f2(a1,f2(f2(a3,a5),a4))))), % 77.56/77.55 inference(scs_inference,[],[1583,2])). % 77.56/77.55 cnf(1588,plain, % 77.56/77.55 (~E(f2(f2(a1,f2(f2(a3,a5),a4)),f2(a1,a6)),f2(f2(a1,a6),f2(f2(f2(a1,f2(a3,f2(a1,a4))),f2(a1,a3)),a5)))), % 77.56/77.55 inference(scs_inference,[],[11,1580,1583,1302,2,4,5,3])). % 77.56/77.55 cnf(1593,plain, % 77.56/77.55 (~E(f2(f2(a1,f2(a1,f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5))),f2(a1,f2(a1,a6))),f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,a4))),a1)),f2(a3,f2(a1,a6))),f2(f2(a1,a5),a3)))), % 77.56/77.55 inference(scs_inference,[],[11,1588,1566,1570,2,4,5,3])). % 77.56/77.55 cnf(1595,plain, % 77.56/77.55 (~E(f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(a1,a4))),a1)),f2(a3,f2(a1,a6))),f2(f2(a1,a5),a3)),f2(f2(a1,f2(a1,f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5))),f2(a1,f2(a1,a6))))), % 77.56/77.55 inference(scs_inference,[],[1593,2])). % 77.56/77.55 cnf(1598,plain, % 77.56/77.55 (~E(f2(f2(f2(a3,f2(a1,f2(a1,f2(a1,a5)))),a1),f2(a1,f2(a1,f2(a4,a6)))),f2(f2(a1,f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5)),f2(a1,a6)))), % 77.56/77.55 inference(scs_inference,[],[264,1571,1593,1460,2,4,5,3])). % 77.56/77.55 cnf(1603,plain, % 77.56/77.55 (~E(f2(f2(a1,f2(a1,f2(a1,f2(a1,f2(a4,a6))))),f2(a1,f2(a1,f2(a1,a5)))),f2(f2(a1,f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5)),f2(a1,a6)))), % 77.56/77.55 inference(scs_inference,[],[11,1572,1598,2,4,5,3])). % 77.56/77.55 cnf(1605,plain, % 77.56/77.55 (~E(f2(f2(a1,f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5)),f2(a1,a6)),f2(f2(a1,f2(a1,f2(a1,f2(a1,f2(a4,a6))))),f2(a1,f2(a1,f2(a1,a5)))))), % 77.56/77.55 inference(scs_inference,[],[1603,2])). % 77.56/77.55 cnf(1608,plain, % 77.56/77.55 (~E(f2(f2(a1,f2(f2(a3,f2(a1,a6)),f2(f2(a1,a5),a3))),f2(f2(a3,f2(a1,f2(a1,a4))),a1)),f2(f2(a1,f2(a1,f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5))),f2(a1,f2(a1,a6))))), % 77.56/77.55 inference(scs_inference,[],[11,1483,1603,1595,2,4,5,3])). % 77.56/77.55 cnf(1613,plain, % 77.56/77.55 (~E(f2(f2(a1,f2(f2(a3,a5),a4)),f2(a1,a6)),f2(f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5),a6))), % 77.56/77.55 inference(scs_inference,[],[11,572,1608,1412,5,2,4,3])). % 77.56/77.55 cnf(1615,plain, % 77.56/77.55 (E(f2(x16151,f2(f2(a1,f2(x16152,x16153)),x16154)),f2(x16151,f2(f2(f2(a3,x16154),x16152),x16153)))), % 77.56/77.55 inference(scs_inference,[],[13,5])). % 77.56/77.55 cnf(1617,plain, % 77.56/77.55 (E(f2(f2(f2(a1,f2(x16171,x16172)),x16173),x16174),f2(f2(f2(f2(a3,x16173),x16171),x16172),x16174))), % 77.56/77.55 inference(scs_inference,[],[13,1613,5,2,4])). % 77.56/77.55 cnf(1618,plain, % 77.56/77.55 (~E(f2(f2(f2(a3,f2(a1,a6)),f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4))),a5),f2(f2(a1,f2(a1,a6)),f2(a1,f2(f2(a3,a5),a4))))), % 77.56/77.55 inference(scs_inference,[],[13,1613,1585,5,2,4,3])). % 77.56/77.55 cnf(1623,plain, % 77.56/77.55 (~E(f2(f2(f2(a3,f2(a1,a6)),f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4))),a5),f2(f2(a1,f2(a1,f2(a1,f2(a1,f2(a4,a6))))),f2(a1,f2(a1,f2(a1,a5)))))), % 77.56/77.55 inference(scs_inference,[],[13,1615,1618,1605,5,2,4,3])). % 77.56/77.55 cnf(1627,plain, % 77.56/77.55 (E(f2(f2(f2(f2(a1,f2(x16271,x16272)),x16273),x16274),x16275),f2(f2(f2(f2(f2(a3,x16273),x16271),x16272),x16274),x16275))), % 77.56/77.55 inference(scs_inference,[],[1617,1623,5,2,4])). % 77.56/77.55 cnf(1648,plain, % 77.56/77.55 (~E(f2(f2(f2(a3,f2(a1,a6)),f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4))),a5),f2(f2(a1,a6),f2(f2(a3,a5),a4)))), % 77.56/77.55 inference(scs_inference,[],[13,1627,1458,5,4,3])). % 77.56/77.55 cnf(1668,plain, % 77.56/77.55 (~E(f2(f2(f2(a3,f2(a1,a6)),f2(a3,a5)),a4),f2(f2(a1,f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5)),f2(a1,a6)))), % 77.56/77.55 inference(scs_inference,[],[13,1303,1468,4,5,3])). % 77.56/77.55 cnf(1671,plain, % 77.56/77.55 (E(f2(f2(f2(x16711,x16712),x16713),x16714),f2(f2(f2(f2(a3,f2(a1,x16713)),x16711),x16712),x16714))), % 77.56/77.55 inference(scs_inference,[],[14,4])). % 77.56/77.55 cnf(1672,plain, % 77.56/77.55 (E(f2(x16721,f2(f2(x16722,x16723),x16724)),f2(x16721,f2(f2(f2(a3,f2(a1,x16724)),x16722),x16723)))), % 77.56/77.55 inference(scs_inference,[],[14,4,5])). % 77.56/77.55 cnf(1676,plain, % 77.56/77.55 (E(f2(x16761,f2(f2(f2(x16762,x16763),x16764),x16765)),f2(x16761,f2(f2(f2(f2(a3,f2(a1,x16764)),x16762),x16763),x16765)))), % 77.56/77.55 inference(scs_inference,[],[1671,4,5])). % 77.56/77.55 cnf(1679,plain, % 77.56/77.55 (~E(f2(f2(a1,a6),f2(f2(a3,a5),a4)),f2(f2(f2(a3,f2(a1,a5)),f2(a3,f2(a1,a6))),f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4))))), % 77.56/77.55 inference(scs_inference,[],[14,1648,1671,4,5,3,2])). % 77.56/77.55 cnf(1682,plain, % 77.56/77.55 (~E(f2(f2(a1,a6),f2(f2(f2(a3,f2(a1,a4)),a3),a5)),f2(f2(f2(a3,f2(a1,a5)),f2(a3,f2(a1,a6))),f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4))))), % 77.56/77.55 inference(scs_inference,[],[1679,1672,4,5,3])). % 77.56/77.55 cnf(1699,plain, % 77.56/77.55 (~E(f2(f2(a1,f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5)),f2(a1,a6)),f2(f2(f2(a3,f2(a1,a4)),f2(a3,f2(a1,a6))),f2(a3,a5)))), % 77.56/77.55 inference(scs_inference,[],[14,1668,1306,4,5,3,2])). % 77.56/77.55 cnf(1718,plain, % 77.56/77.55 (~E(f2(f2(f2(a3,f2(a1,a4)),f2(a3,f2(a1,a6))),f2(a3,a5)),f2(f2(f2(a3,f2(a1,f2(a1,a6))),a1),f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5)))), % 77.56/77.55 inference(scs_inference,[],[14,1699,957,4,5,3,2])). % 77.56/77.55 cnf(1841,plain, % 77.56/77.55 (~E(f2(f2(f2(f2(a1,a3),f2(a3,f2(a1,a4))),a5),a6),f2(f2(f2(a3,f2(a1,f2(a1,a5))),a1),f2(a1,f2(a4,a6))))), % 77.56/77.55 inference(scs_inference,[],[1430,1401,3])). % 77.56/77.55 cnf(1962,plain, % 77.56/77.55 (~E(f2(f2(f2(f2(a1,a3),f2(a3,f2(f2(a1,a4),a1))),a5),a6),f2(f2(f2(a3,f2(a1,f2(a1,a5))),a1),f2(a1,f2(a4,a6))))), % 77.56/77.55 inference(scs_inference,[],[1841,1526,3])). % 77.56/77.55 cnf(1966,plain, % 77.56/77.55 (~E(f2(f2(a1,a6),f2(f2(a3,f2(f2(a3,f2(a1,a5)),a1)),a4)),f2(f2(f2(a3,f2(a1,f2(a1,a6))),a1),f2(f2(f2(f2(a3,f2(a1,a3)),a3),f2(a1,a4)),a5)))), % 77.56/77.55 inference(scs_inference,[],[1718,1083,1962,2,3])). % 77.56/77.55 cnf(1969,plain, % 77.56/77.55 ($false), % 77.56/77.55 inference(scs_inference,[],[1682,1676,1966,1194,2,3]), % 77.56/77.55 ['proof']). % 77.56/77.55 % SZS output end Proof % 77.56/77.55 % Total time :76.900000s %------------------------------------------------------------------------------