%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : COL064-10 : 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 : n029.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:45:00 EDT 2024 % Result : Unsatisfiable 98.89s 98.91s % Output : CNFRefutation 98.89s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : COL064-10 : TPTP v8.2.0. Bugfixed v1.2.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n029.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Tue Jun 18 15:46:54 EDT 2024 % 0.12/0.33 % CPUTime : % 0.53/0.56 start to proof:theBenchmark % 98.82/98.90 %------------------------------------------- % 98.82/98.90 % File :CSE---1.7 % 98.82/98.90 % Problem :theBenchmark % 98.82/98.90 % Transform :cnf % 98.82/98.90 % Format :tptp:raw % 98.82/98.90 % Command :java -jar mcs_scs.jar %d %s % 98.82/98.90 % 98.82/98.90 % Result :Theorem 98.280000s % 98.82/98.90 % Output :CNFRefutation 98.280000s % 98.82/98.90 %------------------------------------------- % 98.82/98.91 %-------------------------------------------------------------------------- % 98.82/98.91 % File : COL064-10 : TPTP v8.2.0. Bugfixed v1.2.0. % 98.82/98.91 % Domain : Combinatory Logic % 98.82/98.91 % Problem : Find combinator equivalent to V from B and T % 98.82/98.91 % Version : [WM88] (equality) axioms. % 98.82/98.91 % Theorem formulation : The combinator is provided and checked. % 98.82/98.91 % English : Construct from B and T alone a combinator that behaves as the % 98.82/98.91 % combinator V does, where ((Bx)y)z = x(yz), (Tx)y = yx, % 98.82/98.91 % ((Vx)y)z = (zx)y. % 98.82/98.91 % 98.82/98.91 % Refs : [WM88] Wos & McCune (1988), Challenge Problems Focusing on Eq % 98.82/98.91 % : [WW+90] Wos et al. (1990), Automated Reasoning Contributes to % 98.82/98.91 % Source : [TPTP] % 98.82/98.91 % Names : % 98.82/98.91 % 98.82/98.91 % Status : Unsatisfiable % 98.82/98.91 % Rating : 0.09 v8.2.0, 0.17 v8.1.0, 0.20 v7.5.0, 0.17 v7.4.0, 0.22 v7.3.0, 0.16 v7.1.0, 0.06 v7.0.0, 0.16 v6.4.0, 0.21 v6.3.0, 0.18 v6.2.0, 0.21 v6.1.0, 0.12 v6.0.0, 0.24 v5.5.0, 0.26 v5.4.0, 0.07 v5.3.0, 0.08 v5.2.0, 0.14 v5.1.0, 0.13 v5.0.0, 0.14 v4.1.0, 0.18 v4.0.1, 0.14 v4.0.0, 0.15 v3.7.0, 0.11 v3.4.0, 0.12 v3.3.0, 0.07 v3.1.0, 0.11 v2.7.0, 0.00 v2.2.1, 0.22 v2.2.0, 0.29 v2.1.0, 0.71 v2.0.0 % 98.82/98.91 % Syntax : Number of clauses : 3 ( 3 unt; 0 nHn; 1 RR) % 98.82/98.91 % Number of literals : 3 ( 3 equ; 1 neg) % 98.82/98.91 % Maximal clause size : 1 ( 1 avg) % 98.82/98.91 % Maximal term depth : 11 ( 2 avg) % 98.82/98.91 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty) % 98.82/98.91 % Number of functors : 6 ( 6 usr; 5 con; 0-2 aty) % 98.82/98.91 % Number of variables : 5 ( 0 sgn) % 98.82/98.91 % SPC : CNF_UNS_RFO_PEQ_UEQ % 98.82/98.91 % 98.82/98.91 % Comments : % 98.82/98.91 % Bugfixes : v1.2.0 : Redundant [fgh]_substitution axioms removed. % 98.82/98.91 %-------------------------------------------------------------------------- % 98.82/98.91 cnf(b_definition,axiom, % 98.82/98.91 apply(apply(apply(b,X),Y),Z) = apply(X,apply(Y,Z)) ). % 98.82/98.91 % 98.82/98.91 cnf(t_definition,axiom, % 98.82/98.91 apply(apply(t,X),Y) = apply(Y,X) ). % 98.82/98.91 % 98.82/98.91 %----This is the V equivalent % 98.82/98.91 cnf(prove_v_combinator,negated_conjecture, % 98.82/98.91 apply(apply(apply(apply(apply(b,apply(apply(b,apply(t,apply(apply(b,b),t))),apply(apply(b,b),t))),t),x),y),z) != apply(apply(z,x),y) ). % 98.82/98.91 % 98.82/98.91 %-------------------------------------------------------------------------- % 98.89/98.91 %------------------------------------------- % 98.89/98.91 % Proof found % 98.89/98.91 % SZS status Theorem for theBenchmark % 98.89/98.91 % SZS output start Proof % 98.89/98.92 %ClaNum:8(EqnAxiom:5) % 98.89/98.92 %VarNum:10(SingletonVarNum:5) % 98.89/98.92 %MaxLitNum:1 % 98.89/98.92 %MaxfuncDepth:8 % 98.89/98.92 %SharedTerms:18 % 98.89/98.92 %goalClause: 8 % 98.89/98.92 %singleGoalClaCount:1 % 98.89/98.92 [8]~E(f2(f2(f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(f2(a3,a3),a1))),f2(f2(a3,a3),a1))),a1),a4),a5),a6),f2(f2(a6,a4),a5)) % 98.89/98.92 [6]E(f2(f2(a1,x61),x62),f2(x62,x61)) % 98.89/98.92 [7]E(f2(f2(f2(a3,x71),x72),x73),f2(x71,f2(x72,x73))) % 98.89/98.92 %EqnAxiom % 98.89/98.92 [1]E(x11,x11) % 98.89/98.92 [2]E(x22,x21)+~E(x21,x22) % 98.89/98.92 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 98.89/98.92 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43)) % 98.89/98.92 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52)) % 98.89/98.92 % 98.89/98.92 %------------------------------------------- % 98.89/98.94 cnf(9,plain, % 98.89/98.94 (E(f2(x91,x92),f2(f2(a1,x92),x91))), % 98.89/98.94 inference(scs_inference,[],[6,2])). % 98.89/98.94 cnf(10,plain, % 98.89/98.94 (~E(f2(f2(f2(f2(f2(a3,f2(f2(a3,f2(a1,f2(f2(a3,a3),a1))),f2(f2(a3,a3),a1))),a1),a4),a5),a6),f2(f2(a1,a5),f2(a6,a4)))), % 98.89/98.94 inference(scs_inference,[],[8,6,2,3])). % 98.89/98.94 cnf(12,plain, % 98.89/98.94 (E(f2(x121,f2(x122,x123)),f2(f2(f2(a3,x121),x122),x123))), % 98.89/98.94 inference(scs_inference,[],[7,2])). % 98.89/98.94 cnf(13,plain, % 98.89/98.94 (E(f2(f2(x131,x132),x133),f2(f2(f2(a3,f2(a1,x133)),x131),x132))), % 98.89/98.94 inference(scs_inference,[],[9,7,2,3])). % 98.89/98.94 cnf(15,plain, % 98.89/98.94 (E(f2(f2(f2(a3,f2(a1,x151)),x152),x153),f2(f2(x152,x153),x151))), % 98.89/98.94 inference(scs_inference,[],[13,2])). % 98.89/98.94 cnf(16,plain, % 98.89/98.94 (E(f2(x161,f2(x162,x163)),f2(f2(f2(a3,f2(a1,x163)),f2(a3,x161)),x162))), % 98.89/98.94 inference(scs_inference,[],[12,13,2,3])). % 98.89/98.94 cnf(18,plain, % 98.89/98.94 (E(f2(f2(f2(a3,f2(a1,x181)),f2(a3,x182)),x183),f2(x182,f2(x183,x181)))), % 98.89/98.94 inference(scs_inference,[],[16,2])). % 98.89/98.94 cnf(19,plain, % 98.89/98.94 (E(f2(f2(f2(a3,f2(a1,f2(x191,x192))),x193),x194),f2(f2(f2(a3,f2(x193,x194)),x191),x192))), % 98.89/98.94 inference(scs_inference,[],[15,12,16,2,3])). % 98.89/98.94 cnf(22,plain, % 98.89/98.94 (E(f2(f2(f2(a3,f2(x221,x222)),x223),x224),f2(f2(f2(a3,f2(a1,f2(x223,x224))),x221),x222))), % 98.89/98.94 inference(scs_inference,[],[19,2])). % 98.89/98.94 cnf(23,plain, % 98.89/98.94 (E(f2(f2(f2(a3,f2(a1,x231)),f2(a3,f2(f2(a3,f2(a1,f2(x232,x233))),x234))),x235),f2(f2(f2(a3,f2(x234,f2(x235,x231))),x232),x233))), % 98.89/98.94 inference(scs_inference,[],[18,19,2,3])). % 98.89/98.94 cnf(26,plain, % 98.89/98.94 (E(f2(f2(f2(a3,f2(a1,x261)),f2(a3,f2(x262,x263))),x264),f2(f2(f2(a3,f2(a1,f2(x264,x261))),x262),x263))), % 98.89/98.94 inference(scs_inference,[],[22,15,3])). % 98.89/98.94 cnf(29,plain, % 98.89/98.94 (E(f2(f2(f2(a3,f2(a1,f2(x291,x292))),x293),x294),f2(f2(f2(a3,f2(a1,x292)),f2(a3,f2(x293,x294))),x291))), % 98.89/98.94 inference(scs_inference,[],[22,15,3,2])). % 98.89/98.94 cnf(35,plain, % 98.89/98.94 (E(f2(f2(f2(a3,f2(a1,f2(f2(a3,f2(x351,x352)),x353))),a1),x354),f2(f2(f2(a3,f2(a1,f2(x353,x354))),x351),x352))), % 98.89/98.94 inference(scs_inference,[],[22,29,3,2])). % 98.89/98.94 cnf(39,plain, % 98.89/98.94 (E(f2(f2(f2(a3,f2(a1,f2(x391,x392))),x393),x394),f2(f2(a1,f2(f2(a3,f2(x393,x394)),x391)),f2(a1,x392)))), % 98.89/98.94 inference(scs_inference,[],[35,12,3,2])). % 98.89/98.94 cnf(48,plain, % 98.89/98.94 (E(f2(f2(a1,f2(f2(a3,f2(x481,x482)),x483)),f2(a1,x484)),f2(f2(f2(a3,f2(x481,x482)),x483),x484))), % 98.89/98.94 inference(scs_inference,[],[39,22,3,2])). % 98.89/98.94 cnf(52,plain, % 98.89/98.94 (E(f2(f2(f2(a3,f2(a1,x521)),f2(a3,f2(x522,x523))),x524),f2(f2(a1,f2(f2(a3,f2(a1,f2(x524,x521))),x522)),f2(a1,x523)))), % 98.89/98.94 inference(scs_inference,[],[48,29,3,2])). % 98.89/98.94 cnf(56,plain, % 98.89/98.94 (E(f2(f2(a1,f2(f2(a3,f2(a1,f2(x561,x562))),x563)),f2(a1,x564)),f2(f2(a1,f2(f2(a3,f2(a1,x562)),f2(a3,f2(x563,x564)))),f2(a1,x561)))), % 98.89/98.94 inference(scs_inference,[],[52,48,3,2])). % 98.89/98.94 cnf(59,plain, % 98.89/98.94 (E(f2(f2(a1,f2(f2(a3,f2(a1,x591)),f2(a3,f2(x592,x593)))),f2(a1,x594)),f2(f2(a1,x593),f2(f2(a3,f2(a1,f2(x594,x591))),x592)))), % 98.89/98.94 inference(scs_inference,[],[56,9,3,2])). % 98.89/98.94 cnf(63,plain, % 98.89/98.94 (E(f2(f2(a1,x631),f2(f2(a3,f2(a1,f2(x632,f2(x633,x634)))),x635)),f2(f2(f2(a3,f2(a1,x634)),f2(a3,f2(f2(a3,f2(x635,x631)),x632))),x633))), % 98.89/98.94 inference(scs_inference,[],[59,52,3,2])). % 98.89/98.94 cnf(67,plain, % 98.89/98.94 (E(f2(f2(a1,f2(x671,x672)),f2(f2(a3,f2(a1,f2(x673,f2(x674,x675)))),a1)),f2(f2(f2(a3,f2(x673,f2(x674,x675))),x671),x672))), % 98.89/98.94 inference(scs_inference,[],[63,23,3])). % 98.89/98.94 cnf(70,plain, % 98.89/98.94 (E(f2(f2(f2(a3,f2(x701,f2(x702,x703))),x704),x705),f2(f2(a1,f2(x704,x705)),f2(f2(a3,f2(a1,f2(x701,f2(x702,x703)))),a1)))), % 98.89/98.94 inference(scs_inference,[],[67,2])). % 98.89/98.94 cnf(71,plain, % 98.89/98.94 (E(f2(f2(a1,x711),f2(f2(a3,f2(a1,f2(x712,f2(x713,x714)))),x715)),f2(f2(f2(a3,f2(a1,f2(x713,x714))),f2(a3,f2(x715,x711))),x712))), % 98.89/98.94 inference(scs_inference,[],[63,26,67,2,3])). % 98.89/98.94 cnf(73,plain, % 98.89/98.94 (E(f2(f2(f2(a3,f2(a1,f2(x731,x732))),f2(a3,f2(x733,x734))),x735),f2(f2(a1,x734),f2(f2(a3,f2(a1,f2(x735,f2(x731,x732)))),x733)))), % 98.89/98.94 inference(scs_inference,[],[71,2])). % 98.89/98.94 cnf(79,plain, % 98.89/98.94 (E(f2(f2(a1,x791),f2(f2(a3,f2(a1,f2(x792,f2(x793,x794)))),x795)),f2(f2(a1,f2(x793,x794)),f2(f2(a3,f2(x795,x791)),x792)))), % 98.89/98.94 inference(scs_inference,[],[73,12,3,2])). % 98.89/98.94 cnf(84,plain, % 98.89/98.94 (E(f2(f2(f2(a3,f2(x841,f2(x842,x843))),x844),x845),f2(f2(a1,f2(x842,x843)),f2(f2(a3,f2(a1,f2(x844,x845))),x841)))), % 98.89/98.94 inference(scs_inference,[],[79,70,3])). % 98.89/98.94 cnf(86,plain, % 98.89/98.94 (E(f2(f2(a1,f2(x861,x862)),f2(f2(a3,f2(a1,f2(x863,x864))),x865)),f2(f2(f2(a3,f2(x865,f2(x861,x862))),x863),x864))), % 98.89/98.94 inference(scs_inference,[],[79,70,3,2])). % 98.89/98.94 cnf(110,plain, % 98.89/98.94 (E(f2(f2(a1,f2(f2(a3,f2(x1101,x1102)),x1103)),f2(a1,x1104)),f2(f2(a1,f2(x1103,x1104)),f2(f2(a3,f2(a1,f2(x1101,x1102))),a1)))), % 98.89/98.94 inference(scs_inference,[],[86,39,3,2])). % 98.89/98.94 cnf(120,plain, % 98.89/98.94 (E(f2(f2(a1,f2(x1201,x1202)),f2(f2(a3,f2(a1,f2(x1203,x1204))),a1)),f2(f2(a1,x1202),f2(f2(a3,f2(x1203,x1204)),x1201)))), % 98.89/98.94 inference(scs_inference,[],[110,9,3,2])). % 98.89/98.94 cnf(124,plain, % 98.89/98.94 (E(f2(f2(a1,x1241),f2(f2(a3,f2(x1242,x1243)),x1244)),f2(f2(a1,f2(x1242,x1243)),f2(f2(a3,f2(a1,f2(a1,f2(x1244,x1241)))),a1)))), % 98.89/98.94 inference(scs_inference,[],[120,79,3,2])). % 98.89/98.94 cnf(130,plain, % 98.89/98.94 (E(f2(f2(a1,x1301),f2(f2(a3,f2(a1,f2(x1302,x1303))),x1304)),f2(f2(a1,x1303),f2(f2(a3,f2(x1304,x1301)),x1302)))), % 98.89/98.94 inference(scs_inference,[],[120,124,3,2])). % 98.89/98.94 cnf(504,plain, % 98.89/98.94 (E(f2(f2(a1,f2(f2(a3,f2(x5041,x5042)),x5043)),f2(a1,x5044)),f2(f2(a1,x5042),f2(f2(a3,f2(a1,f2(x5043,x5044))),x5041)))), % 98.89/98.94 inference(scs_inference,[],[6,39,3,2])). % 98.89/98.94 cnf(507,plain, % 98.89/98.94 (E(f2(f2(a1,x5071),f2(f2(a3,f2(a1,f2(x5072,x5073))),x5074)),f2(f2(a1,f2(a1,x5073)),f2(a1,f2(f2(a3,f2(x5074,x5071)),x5072))))), % 98.89/98.94 inference(scs_inference,[],[6,504,3,2])). % 98.89/98.94 cnf(579,plain, % 98.89/98.94 (E(f2(f2(a1,f2(x5791,x5792)),x5793),f2(f2(f2(a3,x5793),x5791),x5792))), % 98.89/98.94 inference(scs_inference,[],[6,12,3])). % 98.89/98.94 cnf(582,plain, % 98.89/98.94 (E(f2(f2(f2(a3,x5821),x5822),x5823),f2(f2(a1,f2(x5822,x5823)),x5821))), % 98.89/98.94 inference(scs_inference,[],[6,12,3,2])). % 98.89/98.94 cnf(586,plain, % 98.89/98.94 (E(f2(f2(a1,f2(x5861,x5862)),x5863),f2(f2(a1,x5862),f2(f2(a3,x5863),x5861)))), % 98.89/98.94 inference(scs_inference,[],[6,582,3,2])). % 98.89/98.94 cnf(590,plain, % 98.89/98.94 (E(f2(f2(a1,x5901),f2(f2(a3,x5902),x5903)),f2(f2(a1,x5902),f2(a1,f2(x5903,x5901))))), % 98.89/98.94 inference(scs_inference,[],[6,586,3,2])). % 98.89/98.94 cnf(593,plain, % 98.89/98.94 (E(f2(f2(a1,x5931),f2(a1,f2(x5932,x5933))),f2(f2(a1,f2(f2(a3,x5931),x5932)),f2(a1,x5933)))), % 98.89/98.94 inference(scs_inference,[],[6,590,3,2])). % 98.89/98.94 cnf(635,plain, % 98.89/98.94 (E(f2(f2(f2(a3,f2(a1,x6351)),f2(a3,f2(x6352,x6353))),x6354),f2(f2(a1,x6353),f2(f2(a3,f2(a1,f2(x6354,x6351))),x6352)))), % 98.89/98.94 inference(scs_inference,[],[6,29,3,2])). % 98.89/98.94 cnf(639,plain, % 98.89/98.94 (E(f2(f2(a1,x6391),f2(f2(a3,f2(a1,f2(x6392,x6393))),x6394)),f2(f2(a1,x6392),f2(f2(a3,f2(a1,x6393)),f2(a3,f2(x6394,x6391)))))), % 98.89/98.94 inference(scs_inference,[],[6,635,3,2])). % 98.89/98.94 cnf(725,plain, % 98.89/98.94 (E(f2(f2(a1,x7251),f2(f2(a3,f2(a1,x7252)),f2(a3,f2(x7253,x7254)))),f2(f2(f2(a3,f2(a1,x7254)),f2(a3,f2(a1,f2(x7251,x7252)))),x7253))), % 98.89/98.94 inference(scs_inference,[],[7,639,3,2])). % 98.89/98.94 cnf(726,plain, % 98.89/98.94 (E(f2(f2(f2(a3,f2(a1,x7261)),f2(a3,f2(a1,x7262))),f2(a3,f2(x7263,x7264))),f2(f2(f2(a3,f2(a1,x7264)),f2(a3,f2(a1,f2(x7261,x7262)))),x7263))), % 98.89/98.94 inference(scs_inference,[],[7,725,3])). % 98.89/98.94 cnf(739,plain, % 98.89/98.94 (E(f2(f2(f2(a3,f2(f2(a3,x7391),x7392)),x7393),x7394),f2(f2(a1,f2(x7392,f2(x7393,x7394))),x7391))), % 98.89/98.94 inference(scs_inference,[],[7,582,3])). % 98.89/98.94 cnf(790,plain, % 98.89/98.94 (E(f2(f2(f2(a3,f2(a1,x7901)),f2(a3,x7902)),x7903),f2(f2(a1,x7902),f2(a1,f2(x7903,x7901))))), % 98.89/98.94 inference(scs_inference,[],[7,590,3])). % 98.89/98.94 cnf(818,plain, % 98.89/98.94 (E(f2(f2(f2(a3,f2(a1,x8181)),f2(a3,f2(a1,f2(x8182,x8183)))),x8184),f2(f2(a1,f2(a1,x8183)),f2(a1,f2(f2(a3,f2(x8184,x8181)),x8182))))), % 98.89/98.94 inference(scs_inference,[],[7,507,3])). % 98.89/98.94 cnf(877,plain, % 98.89/98.94 (E(f2(f2(f2(a3,f2(a1,x8771)),a1),f2(x8772,x8773)),f2(f2(a1,f2(f2(a3,x8771),x8772)),f2(a1,x8773)))), % 98.89/98.94 inference(scs_inference,[],[7,593,3])). % 98.89/98.94 cnf(1067,plain, % 98.89/98.94 (E(f2(f2(a1,x10671),f2(f2(a3,f2(x10672,x10673)),x10674)),f2(f2(f2(a3,f2(a1,x10673)),f2(a3,f2(a1,f2(x10674,x10671)))),x10672))), % 98.89/98.94 inference(scs_inference,[],[7,130,3,2])). % 98.89/98.94 cnf(1068,plain, % 98.89/98.94 (E(f2(f2(f2(a3,f2(a1,x10681)),f2(a3,f2(x10682,x10683))),x10684),f2(f2(f2(a3,f2(a1,x10683)),f2(a3,f2(a1,f2(x10684,x10681)))),x10682))), % 98.89/98.94 inference(scs_inference,[],[7,1067,3])). % 98.89/98.94 cnf(1268,plain, % 98.89/98.94 (E(f2(f2(f2(a1,f2(x12681,x12682)),x12683),x12684),f2(f2(f2(f2(a3,x12683),x12681),x12682),x12684))), % 98.89/98.94 inference(scs_inference,[],[579,4])). % 98.89/98.94 cnf(1275,plain, % 98.89/98.94 (E(f2(f2(f2(f2(a3,f2(a1,x12751)),f2(a3,x12752)),x12753),x12754),f2(f2(f2(a1,x12752),f2(a1,f2(x12753,x12751))),x12754))), % 98.89/98.94 inference(scs_inference,[],[790,4])). % 98.89/98.94 cnf(1280,plain, % 98.89/98.94 (E(f2(x12801,f2(f2(f2(a3,f2(a1,x12802)),a1),f2(x12803,x12804))),f2(x12801,f2(f2(a1,f2(f2(a3,x12802),x12803)),f2(a1,x12804))))), % 98.89/98.94 inference(scs_inference,[],[877,4,5])). % 98.89/98.94 cnf(1300,plain, % 98.89/98.94 (E(f2(f2(f2(f2(a1,f2(x13001,x13002)),x13003),x13004),x13005),f2(f2(f2(f2(f2(a3,x13003),x13001),x13002),x13004),x13005))), % 98.89/98.94 inference(scs_inference,[],[1268,5,4])). % 98.89/98.94 cnf(1318,plain, % 98.89/98.94 (E(f2(f2(f2(f2(f2(a3,f2(a1,x13181)),f2(a3,x13182)),x13183),x13184),x13185),f2(f2(f2(f2(a1,x13182),f2(a1,f2(x13183,x13181))),x13184),x13185))), % 98.89/98.94 inference(scs_inference,[],[1275,5,4])). % 98.89/98.94 cnf(1323,plain, % 98.89/98.94 (E(f2(f2(f2(f2(a3,f2(f2(a3,x13231),x13232)),x13233),x13234),x13235),f2(f2(f2(a1,f2(x13232,f2(x13233,x13234))),x13231),x13235))), % 98.89/98.94 inference(scs_inference,[],[739,4])). % 98.89/98.94 cnf(1415,plain, % 98.89/98.94 (E(f2(f2(f2(f2(f2(a3,f2(f2(a3,x14151),x14152)),x14153),x14154),x14155),x14156),f2(f2(f2(f2(a1,f2(x14152,f2(x14153,x14154))),x14151),x14155),x14156))), % 98.89/98.94 inference(scs_inference,[],[1323,5,4])). % 98.89/98.94 cnf(1416,plain, % 98.89/98.94 (E(f2(f2(f2(a1,x14161),x14162),x14163),f2(f2(x14162,x14161),x14163))), % 98.89/98.94 inference(scs_inference,[],[6,4])). % 98.89/98.94 cnf(1417,plain, % 98.89/98.94 (E(f2(x14171,f2(f2(a1,x14172),x14173)),f2(x14171,f2(x14173,x14172)))), % 98.89/98.94 inference(scs_inference,[],[6,4,5])). % 98.89/98.94 cnf(1418,plain, % 98.89/98.94 (~E(f2(f2(f2(f2(a1,f2(f2(f2(a3,a3),a1),f2(a1,a4))),f2(a1,f2(f2(a3,a3),a1))),a5),a6),f2(f2(a1,a5),f2(a6,a4)))), % 98.89/98.94 inference(scs_inference,[],[6,10,1415,4,5,3])). % 98.89/98.94 cnf(1421,plain, % 98.89/98.94 (E(f2(f2(f2(f2(a1,x14211),x14212),x14213),x14214),f2(f2(f2(x14212,x14211),x14213),x14214))), % 98.89/98.94 inference(scs_inference,[],[1416,1418,2,4])). % 98.89/98.94 cnf(1422,plain, % 98.89/98.94 (E(f2(x14221,f2(f2(f2(a1,x14222),x14223),x14224)),f2(x14221,f2(f2(x14223,x14222),x14224)))), % 98.89/98.94 inference(scs_inference,[],[1416,1418,2,4,5])). % 98.89/98.94 cnf(1423,plain, % 98.89/98.94 (~E(f2(f2(a6,a4),a5),f2(f2(f2(f2(a1,f2(f2(f2(a3,a3),a1),f2(a1,a4))),f2(a1,f2(f2(a3,a3),a1))),a5),a6))), % 98.89/98.94 inference(scs_inference,[],[6,1416,1418,2,4,5,3])). % 98.89/98.94 cnf(1425,plain, % 98.89/98.94 (~E(f2(f2(f2(f2(a1,f2(f2(f2(a3,a3),a1),f2(a1,a4))),f2(a1,f2(f2(a3,a3),a1))),a5),a6),f2(f2(a6,a4),a5))), % 98.89/98.95 inference(scs_inference,[],[1423,2])). % 98.89/98.95 cnf(1426,plain, % 98.89/98.95 (E(f2(f2(x14261,f2(f2(a1,x14262),x14263)),x14264),f2(f2(x14261,f2(x14263,x14262)),x14264))), % 98.89/98.95 inference(scs_inference,[],[1417,1423,2,4])). % 98.89/98.95 cnf(1427,plain, % 98.89/98.95 (E(f2(x14271,f2(x14272,f2(f2(a1,x14273),x14274))),f2(x14271,f2(x14272,f2(x14274,x14273))))), % 98.89/98.95 inference(scs_inference,[],[1417,1423,2,4,5])). % 98.89/98.95 cnf(1428,plain, % 98.89/98.95 (~E(f2(f2(f2(a3,f2(a1,a5)),a6),a4),f2(f2(f2(f2(a1,f2(f2(f2(a3,a3),a1),f2(a1,a4))),f2(a1,f2(f2(a3,a3),a1))),a5),a6))), % 98.89/98.95 inference(scs_inference,[],[1417,1423,13,2,4,5,3])). % 98.89/98.95 cnf(1431,plain, % 98.89/98.95 (E(f2(f2(f2(f2(f2(a1,x14311),x14312),x14313),x14314),x14315),f2(f2(f2(f2(x14312,x14311),x14313),x14314),x14315))), % 98.89/98.95 inference(scs_inference,[],[1421,1428,2,4])). % 98.89/98.95 cnf(1432,plain, % 98.89/98.95 (E(f2(x14321,f2(f2(f2(f2(a1,x14322),x14323),x14324),x14325)),f2(x14321,f2(f2(f2(x14323,x14322),x14324),x14325)))), % 98.89/98.95 inference(scs_inference,[],[1421,1428,2,4,5])). % 98.89/98.95 cnf(1433,plain, % 98.89/98.95 (~E(f2(f2(f2(f2(a1,f2(f2(a3,a3),a1)),f2(f2(f2(a3,a3),a1),f2(a1,a4))),a5),a6),f2(f2(a6,a4),a5))), % 98.89/98.95 inference(scs_inference,[],[1421,1425,1428,2,4,5,3])). % 98.89/98.95 cnf(1435,plain, % 98.89/98.95 (~E(f2(f2(a6,a4),a5),f2(f2(f2(f2(a1,f2(f2(a3,a3),a1)),f2(f2(f2(a3,a3),a1),f2(a1,a4))),a5),a6))), % 98.89/98.95 inference(scs_inference,[],[1433,2])). % 98.89/98.95 cnf(1436,plain, % 98.89/98.95 (E(f2(f2(x14361,f2(f2(f2(a1,x14362),x14363),x14364)),x14365),f2(f2(x14361,f2(f2(x14363,x14362),x14364)),x14365))), % 98.89/98.95 inference(scs_inference,[],[1422,1433,2,4])). % 98.89/98.95 cnf(1437,plain, % 98.89/98.95 (E(f2(x14371,f2(x14372,f2(f2(f2(a1,x14373),x14374),x14375))),f2(x14371,f2(x14372,f2(f2(x14374,x14373),x14375))))), % 98.89/98.95 inference(scs_inference,[],[1422,1433,2,4,5])). % 98.89/98.95 cnf(1438,plain, % 98.89/98.95 (~E(f2(f2(f2(f2(f2(a3,f2(f2(f2(a3,a3),a1),f2(a1,a4))),f2(a3,a3)),a1),a5),a6),f2(f2(a6,a4),a5))), % 98.89/98.95 inference(scs_inference,[],[1422,1433,1300,2,4,5,3])). % 98.89/98.95 cnf(1440,plain, % 98.89/98.95 (~E(f2(f2(a6,a4),a5),f2(f2(f2(f2(f2(a3,f2(f2(f2(a3,a3),a1),f2(a1,a4))),f2(a3,a3)),a1),a5),a6))), % 98.89/98.95 inference(scs_inference,[],[1438,2])). % 98.89/98.95 cnf(1441,plain, % 98.89/98.95 (E(f2(f2(f2(x14411,f2(f2(a1,x14412),x14413)),x14414),x14415),f2(f2(f2(x14411,f2(x14413,x14412)),x14414),x14415))), % 98.89/98.95 inference(scs_inference,[],[1426,1438,2,4])). % 98.89/98.95 cnf(1442,plain, % 98.89/98.95 (E(f2(x14421,f2(f2(x14422,f2(f2(a1,x14423),x14424)),x14425)),f2(x14421,f2(f2(x14422,f2(x14424,x14423)),x14425)))), % 98.89/98.95 inference(scs_inference,[],[1426,1438,2,4,5])). % 98.89/98.95 cnf(1443,plain, % 98.89/98.95 (E(f2(f2(a1,f2(f2(a1,x14431),x14432)),x14433),f2(x14433,f2(x14432,x14431)))), % 98.89/98.95 inference(scs_inference,[],[6,1426,1438,2,4,5,3])). % 98.89/98.95 cnf(1446,plain, % 98.89/98.95 (E(f2(f2(f2(a1,f2(f2(a1,x14461),x14462)),x14463),x14464),f2(f2(x14463,f2(x14462,x14461)),x14464))), % 98.89/98.95 inference(scs_inference,[],[1443,4])). % 98.89/98.95 cnf(1447,plain, % 98.89/98.95 (E(f2(x14471,f2(f2(a1,f2(f2(a1,x14472),x14473)),x14474)),f2(x14471,f2(x14474,f2(x14473,x14472))))), % 98.89/98.95 inference(scs_inference,[],[1443,4,5])). % 98.89/98.95 cnf(1448,plain, % 98.89/98.95 (~E(f2(f2(f2(a3,f2(a1,a5)),a6),a4),f2(f2(f2(f2(a1,f2(f2(a3,a3),a1)),f2(f2(f2(a3,a3),a1),f2(a1,a4))),a5),a6))), % 98.89/98.95 inference(scs_inference,[],[1443,1435,13,4,5,3])). % 98.89/98.95 cnf(1450,plain, % 98.89/98.95 (~E(f2(f2(f2(f2(a1,f2(f2(a3,a3),a1)),f2(f2(f2(a3,a3),a1),f2(a1,a4))),a5),a6),f2(f2(f2(a3,f2(a1,a5)),a6),a4))), % 98.89/98.95 inference(scs_inference,[],[1443,1435,13,4,5,3,2])). % 98.89/98.95 cnf(1451,plain, % 98.89/98.95 (E(f2(f2(x14511,f2(x14512,f2(f2(a1,x14513),x14514))),x14515),f2(f2(x14511,f2(x14512,f2(x14514,x14513))),x14515))), % 98.89/98.95 inference(scs_inference,[],[1427,4])). % 98.89/98.95 cnf(1452,plain, % 98.89/98.95 (E(f2(x14521,f2(x14522,f2(x14523,f2(f2(a1,x14524),x14525)))),f2(x14521,f2(x14522,f2(x14523,f2(x14525,x14524)))))), % 98.89/98.95 inference(scs_inference,[],[1427,4,5])). % 98.89/98.95 cnf(1453,plain, % 98.89/98.95 (E(f2(f2(a1,x14531),f2(x14532,f2(f2(a1,x14533),x14534))),f2(f2(x14532,f2(x14534,x14533)),x14531))), % 98.89/98.95 inference(scs_inference,[],[6,1427,4,5,3])). % 98.89/98.95 cnf(1457,plain, % 98.89/98.95 (E(f2(x14571,f2(f2(a1,x14572),f2(x14573,f2(f2(a1,x14574),x14575)))),f2(x14571,f2(f2(x14573,f2(x14575,x14574)),x14572)))), % 98.89/98.95 inference(scs_inference,[],[1453,4,5])). % 98.89/98.95 cnf(1458,plain, % 98.89/98.95 (~E(f2(f2(f2(a3,f2(a1,a5)),a6),a4),f2(f2(f2(f2(f2(a3,f2(f2(f2(a3,a3),a1),f2(a1,a4))),f2(a3,a3)),a1),a5),a6))), % 98.89/98.95 inference(scs_inference,[],[1453,1440,13,4,5,3])). % 98.89/98.95 cnf(1461,plain, % 98.89/98.95 (E(f2(f2(f2(f2(a1,f2(f2(a1,x14611),x14612)),x14613),x14614),x14615),f2(f2(f2(x14613,f2(x14612,x14611)),x14614),x14615))), % 98.89/98.95 inference(scs_inference,[],[1446,4])). % 98.89/98.95 cnf(1462,plain, % 98.89/98.95 (E(f2(x14621,f2(f2(f2(a1,f2(f2(a1,x14622),x14623)),x14624),x14625)),f2(x14621,f2(f2(x14624,f2(x14623,x14622)),x14625)))), % 98.89/98.95 inference(scs_inference,[],[1446,4,5])). % 98.89/98.95 cnf(1463,plain, % 98.89/98.95 (E(f2(f2(f2(a1,f2(f2(a1,x14631),x14632)),a1),x14633),f2(x14633,f2(x14632,x14631)))), % 98.89/98.95 inference(scs_inference,[],[6,1446,4,5,3])). % 98.89/98.95 cnf(1468,plain, % 98.89/98.95 (~E(f2(f2(f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1)),a5),a6),f2(f2(f2(a3,f2(a1,a5)),a6),a4))), % 98.89/98.95 inference(scs_inference,[],[1463,1450,1421,4,5,3])). % 98.89/98.95 cnf(1470,plain, % 98.89/98.95 (~E(f2(f2(f2(a3,f2(a1,a5)),a6),a4),f2(f2(f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1)),a5),a6))), % 98.89/98.95 inference(scs_inference,[],[1463,1450,1421,4,5,3,2])). % 98.89/98.95 cnf(1471,plain, % 98.89/98.95 (E(f2(f2(f2(f2(a3,x14711),x14712),x14713),x14714),f2(f2(x14711,f2(x14712,x14713)),x14714))), % 98.89/98.95 inference(scs_inference,[],[7,4])). % 98.89/98.95 cnf(1472,plain, % 98.89/98.95 (E(f2(x14721,f2(f2(f2(a3,x14722),x14723),x14724)),f2(x14721,f2(x14722,f2(x14723,x14724))))), % 98.89/98.95 inference(scs_inference,[],[7,4,5])). % 98.89/98.95 cnf(1473,plain, % 98.89/98.95 (~E(f2(f2(a1,a5),f2(a6,a4)),f2(f2(f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1)),a5),a6))), % 98.89/98.95 inference(scs_inference,[],[7,1470,4,5,3])). % 98.89/98.95 cnf(1475,plain, % 98.89/98.95 (~E(f2(f2(f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1)),a5),a6),f2(f2(a1,a5),f2(a6,a4)))), % 98.89/98.95 inference(scs_inference,[],[7,1470,4,5,3,2])). % 98.89/98.95 cnf(1476,plain, % 98.89/98.95 (E(f2(f2(f2(f2(f2(a3,x14761),x14762),x14763),x14764),x14765),f2(f2(f2(x14761,f2(x14762,x14763)),x14764),x14765))), % 98.89/98.95 inference(scs_inference,[],[1471,4])). % 98.89/98.95 cnf(1477,plain, % 98.89/98.95 (E(f2(x14771,f2(f2(f2(f2(a3,x14772),x14773),x14774),x14775)),f2(x14771,f2(f2(x14772,f2(x14773,x14774)),x14775)))), % 98.89/98.95 inference(scs_inference,[],[1471,4,5])). % 98.89/98.95 cnf(1478,plain, % 98.89/98.95 (~E(f2(f2(f2(a3,f2(a1,a6)),f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1))),a5),f2(f2(a1,a5),f2(a6,a4)))), % 98.89/98.95 inference(scs_inference,[],[1471,1475,13,4,5,3])). % 98.89/98.95 cnf(1480,plain, % 98.89/98.95 (~E(f2(f2(a1,a5),f2(a6,a4)),f2(f2(f2(a3,f2(a1,a6)),f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1))),a5))), % 98.89/98.95 inference(scs_inference,[],[1471,1475,13,4,5,3,2])). % 98.89/98.95 cnf(1481,plain, % 98.89/98.95 (E(f2(x14811,f2(x14812,f2(f2(f2(a3,x14813),x14814),x14815))),f2(x14811,f2(x14812,f2(x14813,f2(x14814,x14815)))))), % 98.89/98.95 inference(scs_inference,[],[1472,5])). % 98.89/98.95 cnf(1483,plain, % 98.89/98.95 (~E(f2(f2(a1,a6),f2(f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1)),a5)),f2(f2(a1,a5),f2(a6,a4)))), % 98.89/98.95 inference(scs_inference,[],[7,1472,1478,5,4,3])). % 98.89/98.95 cnf(1485,plain, % 98.89/98.95 (~E(f2(f2(a1,a5),f2(a6,a4)),f2(f2(a1,a6),f2(f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1)),a5)))), % 98.89/98.95 inference(scs_inference,[],[7,1472,1478,5,4,3,2])). % 98.89/98.95 cnf(1488,plain, % 98.89/98.95 (~E(f2(f2(f2(a3,f2(a1,a5)),f2(a3,f2(a1,a6))),f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1))),f2(f2(a1,a5),f2(a6,a4)))), % 98.89/98.95 inference(scs_inference,[],[1483,1447,16,4,5,3])). % 98.89/98.95 cnf(1490,plain, % 98.89/98.95 (~E(f2(f2(a1,a5),f2(a6,a4)),f2(f2(f2(a3,f2(a1,a5)),f2(a3,f2(a1,a6))),f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1))))), % 98.89/98.95 inference(scs_inference,[],[1483,1447,16,4,5,3,2])). % 98.89/98.95 cnf(1493,plain, % 98.89/98.95 (~E(f2(f2(a1,a5),f2(f2(a3,f2(a1,a6)),f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1)))),f2(f2(a1,a5),f2(a6,a4)))), % 98.89/98.95 inference(scs_inference,[],[7,1488,1431,5,4,3])). % 98.89/98.95 cnf(1495,plain, % 98.89/98.95 (~E(f2(f2(a1,a5),f2(a6,a4)),f2(f2(a1,a5),f2(f2(a3,f2(a1,a6)),f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1)))))), % 98.89/98.95 inference(scs_inference,[],[1493,2])). % 98.89/98.95 cnf(1498,plain, % 98.89/98.95 (~E(f2(f2(f2(a3,f2(a1,a4)),f2(a3,f2(a1,a5))),a6),f2(f2(f2(a3,f2(a1,a5)),f2(a3,f2(a1,a6))),f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1))))), % 98.89/98.95 inference(scs_inference,[],[1490,1493,1432,16,2,4,5,3])). % 98.89/98.95 cnf(1500,plain, % 98.89/98.95 (~E(f2(f2(f2(a3,f2(a1,a5)),f2(a3,f2(a1,a6))),f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1))),f2(f2(f2(a3,f2(a1,a4)),f2(a3,f2(a1,a5))),a6))), % 98.89/98.95 inference(scs_inference,[],[1498,2])). % 98.89/98.95 cnf(1502,plain, % 98.89/98.95 (E(f2(x15021,f2(f2(x15022,f2(f2(f2(a1,x15023),x15024),x15025)),x15026)),f2(x15021,f2(f2(x15022,f2(f2(x15024,x15023),x15025)),x15026)))), % 98.89/98.95 inference(scs_inference,[],[1436,1498,2,4,5])). % 98.89/98.95 cnf(1503,plain, % 98.89/98.95 (~E(f2(f2(a1,a4),f2(f2(a3,f2(a1,a5)),a6)),f2(f2(f2(a3,f2(a1,a5)),f2(a3,f2(a1,a6))),f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1))))), % 98.89/98.95 inference(scs_inference,[],[7,1436,1498,2,4,5,3])). % 98.89/98.95 cnf(1505,plain, % 98.89/98.95 (E(f2(f2(x15051,f2(x15052,f2(f2(f2(a1,x15053),x15054),x15055))),x15056),f2(f2(x15051,f2(x15052,f2(f2(x15054,x15053),x15055))),x15056))), % 98.89/98.95 inference(scs_inference,[],[1437,4])). % 98.89/98.95 cnf(1506,plain, % 98.89/98.95 (~E(f2(f2(f2(a3,f2(a1,a5)),f2(a3,f2(a1,a6))),f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1))),f2(f2(a1,a4),f2(f2(a3,f2(a1,a5)),a6)))), % 98.89/98.95 inference(scs_inference,[],[1437,1503,4,2])). % 98.89/98.95 cnf(1507,plain, % 98.89/98.95 (E(f2(x15071,f2(x15072,f2(x15073,f2(f2(f2(a1,x15074),x15075),x15076)))),f2(x15071,f2(x15072,f2(x15073,f2(f2(x15075,x15074),x15076)))))), % 98.89/98.95 inference(scs_inference,[],[1437,1503,4,2,5])). % 98.89/98.95 cnf(1508,plain, % 98.89/98.95 (~E(f2(f2(f2(a3,f2(a1,a4)),f2(a3,f2(a1,a5))),a6),f2(f2(f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1)),a5),a6))), % 98.89/98.95 inference(scs_inference,[],[1473,1437,1503,16,4,2,5,3])). % 98.89/98.95 cnf(1510,plain, % 98.89/98.95 (~E(f2(f2(f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1)),a5),a6),f2(f2(f2(a3,f2(a1,a4)),f2(a3,f2(a1,a5))),a6))), % 98.89/98.95 inference(scs_inference,[],[1508,2])). % 98.89/98.95 cnf(1511,plain, % 98.89/98.95 (E(f2(f2(f2(f2(x15111,f2(f2(a1,x15112),x15113)),x15114),x15115),x15116),f2(f2(f2(f2(x15111,f2(x15113,x15112)),x15114),x15115),x15116))), % 98.89/98.95 inference(scs_inference,[],[1441,1508,2,4])). % 98.89/98.95 cnf(1512,plain, % 98.89/98.95 (E(f2(x15121,f2(f2(f2(x15122,f2(f2(a1,x15123),x15124)),x15125),x15126)),f2(x15121,f2(f2(f2(x15122,f2(x15124,x15123)),x15125),x15126)))), % 98.89/98.95 inference(scs_inference,[],[1441,1508,2,4,5])). % 98.89/98.95 cnf(1513,plain, % 98.89/98.95 (~E(f2(f2(a1,a5),f2(f2(a3,f2(a1,a6)),f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1)))),f2(f2(a1,a4),f2(f2(a3,f2(a1,a5)),a6)))), % 98.89/98.95 inference(scs_inference,[],[7,1441,1506,1508,2,4,5,3])). % 98.89/98.95 cnf(1518,plain, % 98.89/98.95 (~E(f2(f2(f2(a3,f2(a1,a4)),f2(a3,f2(a1,a5))),a6),f2(f2(a1,a6),f2(f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1)),a5)))), % 98.89/98.95 inference(scs_inference,[],[1485,1442,1513,16,4,2,5,3])). % 98.89/98.95 cnf(1520,plain, % 98.89/98.95 (~E(f2(f2(a1,a6),f2(f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1)),a5)),f2(f2(f2(a3,f2(a1,a4)),f2(a3,f2(a1,a5))),a6))), % 98.89/98.95 inference(scs_inference,[],[1518,2])). % 98.89/98.95 cnf(1523,plain, % 98.89/98.95 (~E(f2(f2(a1,a5),f2(f2(a3,f2(a1,a6)),f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1)))),f2(f2(f2(a3,f2(a1,a4)),f2(a3,f2(a1,a5))),a6))), % 98.89/98.95 inference(scs_inference,[],[7,1451,1500,1518,2,4,5,3])). % 98.89/98.95 cnf(1525,plain, % 98.89/98.95 (~E(f2(f2(f2(a3,f2(a1,a4)),f2(a3,f2(a1,a5))),a6),f2(f2(a1,a5),f2(f2(a3,f2(a1,a6)),f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1)))))), % 98.89/98.95 inference(scs_inference,[],[1523,2])). % 98.89/98.95 cnf(1526,plain, % 98.89/98.95 (E(f2(f2(x15261,x15262),x15263),f2(f2(f2(a1,x15262),x15261),x15263))), % 98.89/98.95 inference(scs_inference,[],[9,1523,2,4])). % 98.89/98.95 cnf(1527,plain, % 98.89/98.95 (E(f2(x15271,f2(x15272,x15273)),f2(x15271,f2(f2(a1,x15273),x15272)))), % 98.89/98.95 inference(scs_inference,[],[9,1523,2,4,5])). % 98.89/98.95 cnf(1528,plain, % 98.89/98.95 (~E(f2(f2(a1,f2(a6,a4)),f2(a1,a5)),f2(f2(f2(a3,f2(a1,a6)),f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1))),a5))), % 98.89/98.95 inference(scs_inference,[],[9,1480,1523,2,4,5,3])). % 98.89/98.95 cnf(1530,plain, % 98.89/98.95 (~E(f2(f2(f2(a3,f2(a1,a6)),f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1))),a5),f2(f2(a1,f2(a6,a4)),f2(a1,a5)))), % 98.89/98.95 inference(scs_inference,[],[1528,2])). % 98.89/98.95 cnf(1531,plain, % 98.89/98.95 (E(f2(f2(f2(x15311,x15312),x15313),x15314),f2(f2(f2(f2(a1,x15312),x15311),x15313),x15314))), % 98.89/98.95 inference(scs_inference,[],[1526,1528,2,4])). % 98.89/98.95 cnf(1532,plain, % 98.89/98.95 (E(f2(x15321,f2(f2(x15322,x15323),x15324)),f2(x15321,f2(f2(f2(a1,x15323),x15322),x15324)))), % 98.89/98.95 inference(scs_inference,[],[1526,1528,2,4,5])). % 98.89/98.95 cnf(1533,plain, % 98.89/98.95 (~E(f2(f2(a1,f2(a6,a4)),f2(a1,a5)),f2(f2(a1,a5),f2(f2(a3,f2(a1,a6)),f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1)))))), % 98.89/98.95 inference(scs_inference,[],[9,1526,1495,1528,2,4,5,3])). % 98.89/98.95 cnf(1535,plain, % 98.89/98.95 (~E(f2(f2(a1,a5),f2(f2(a3,f2(a1,a6)),f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1)))),f2(f2(a1,f2(a6,a4)),f2(a1,a5)))), % 98.89/98.95 inference(scs_inference,[],[1533,2])). % 98.89/98.95 cnf(1536,plain, % 98.89/98.95 (E(f2(f2(x15361,f2(x15362,x15363)),x15364),f2(f2(x15361,f2(f2(a1,x15363),x15362)),x15364))), % 98.89/98.95 inference(scs_inference,[],[1527,1533,2,4])). % 98.89/98.95 cnf(1537,plain, % 98.89/98.95 (E(f2(x15371,f2(x15372,f2(x15373,x15374))),f2(x15371,f2(x15372,f2(f2(a1,x15374),x15373))))), % 98.89/98.95 inference(scs_inference,[],[1527,1533,2,4,5])). % 98.89/98.95 cnf(1538,plain, % 98.89/98.95 (~E(f2(f2(a1,f2(a1,a5)),f2(a1,f2(a6,a4))),f2(f2(a1,a5),f2(f2(a3,f2(a1,a6)),f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1)))))), % 98.89/98.95 inference(scs_inference,[],[9,1527,1533,2,4,5,3])). % 98.89/98.95 cnf(1540,plain, % 98.89/98.95 (~E(f2(f2(a1,a5),f2(f2(a3,f2(a1,a6)),f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1)))),f2(f2(a1,f2(a1,a5)),f2(a1,f2(a6,a4))))), % 98.89/98.95 inference(scs_inference,[],[1538,2])). % 98.89/98.95 cnf(1541,plain, % 98.89/98.95 (E(f2(x15411,f2(f2(f2(x15412,x15413),x15414),x15415)),f2(x15411,f2(f2(f2(f2(a1,x15413),x15412),x15414),x15415)))), % 98.89/98.95 inference(scs_inference,[],[1531,1538,2,5])). % 98.89/98.95 cnf(1542,plain, % 98.89/98.95 (E(f2(f2(f2(f2(x15421,x15422),x15423),x15424),x15425),f2(f2(f2(f2(f2(a1,x15422),x15421),x15423),x15424),x15425))), % 98.89/98.95 inference(scs_inference,[],[1531,1538,2,5,4])). % 98.89/98.95 cnf(1543,plain, % 98.89/98.95 (~E(f2(f2(a1,f2(f2(a3,f2(a1,a6)),f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1)))),f2(a1,a5)),f2(f2(a1,f2(a6,a4)),f2(a1,a5)))), % 98.89/98.95 inference(scs_inference,[],[9,1531,1535,1538,2,5,4,3])). % 98.89/98.95 cnf(1545,plain, % 98.89/98.95 (~E(f2(f2(a1,f2(a6,a4)),f2(a1,a5)),f2(f2(a1,f2(f2(a3,f2(a1,a6)),f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1)))),f2(a1,a5)))), % 98.89/98.95 inference(scs_inference,[],[1543,2])). % 98.89/98.95 cnf(1546,plain, % 98.89/98.95 (E(f2(f2(x15461,f2(f2(x15462,x15463),x15464)),x15465),f2(f2(x15461,f2(f2(f2(a1,x15463),x15462),x15464)),x15465))), % 98.89/98.95 inference(scs_inference,[],[1532,1543,2,4])). % 98.89/98.95 cnf(1547,plain, % 98.89/98.95 (E(f2(x15471,f2(x15472,f2(f2(x15473,x15474),x15475))),f2(x15471,f2(x15472,f2(f2(f2(a1,x15474),x15473),x15475))))), % 98.89/98.95 inference(scs_inference,[],[1532,1543,2,4,5])). % 98.89/98.95 cnf(1548,plain, % 98.89/98.95 (~E(f2(f2(a1,f2(a1,a5)),f2(a1,f2(f2(a3,f2(a1,a6)),f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1))))),f2(f2(a1,f2(a6,a4)),f2(a1,a5)))), % 98.89/98.95 inference(scs_inference,[],[9,1532,1543,2,4,5,3])). % 98.89/98.95 cnf(1551,plain, % 98.89/98.95 (E(f2(x15511,f2(f2(x15512,f2(x15513,x15514)),x15515)),f2(x15511,f2(f2(x15512,f2(f2(a1,x15514),x15513)),x15515)))), % 98.89/98.95 inference(scs_inference,[],[1536,1548,2,5])). % 98.89/98.95 cnf(1552,plain, % 98.89/98.95 (E(f2(f2(f2(x15521,f2(x15522,x15523)),x15524),x15525),f2(f2(f2(x15521,f2(f2(a1,x15523),x15522)),x15524),x15525))), % 98.89/98.95 inference(scs_inference,[],[1536,1548,2,5,4])). % 98.89/98.95 cnf(1553,plain, % 98.89/98.95 (~E(f2(f2(f2(a3,f2(a1,a6)),f2(f2(a1,f2(f2(a3,a3),a1)),f2(f2(f2(a3,a3),a1),f2(a1,a4)))),a5),f2(f2(a1,f2(a6,a4)),f2(a1,a5)))), % 98.89/98.95 inference(scs_inference,[],[1536,1530,1548,2,5,4,3])). % 98.89/98.95 cnf(1556,plain, % 98.89/98.95 (E(f2(f2(x15561,f2(x15562,f2(x15563,x15564))),x15565),f2(f2(x15561,f2(x15562,f2(f2(a1,x15564),x15563))),x15565))), % 98.89/98.95 inference(scs_inference,[],[1537,1553,2,4])). % 98.89/98.95 cnf(1558,plain, % 98.89/98.95 (~E(f2(f2(a1,f2(a1,a5)),f2(a1,f2(a6,a4))),f2(f2(a1,f2(f2(a3,f2(a1,a6)),f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1)))),f2(a1,a5)))), % 98.89/98.95 inference(scs_inference,[],[9,1537,1545,1553,2,4,5,3])). % 98.89/98.95 cnf(1560,plain, % 98.89/98.95 (~E(f2(f2(a1,f2(f2(a3,f2(a1,a6)),f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1)))),f2(a1,a5)),f2(f2(a1,f2(a1,a5)),f2(a1,f2(a6,a4))))), % 98.89/98.95 inference(scs_inference,[],[1558,2])). % 98.89/98.95 cnf(1563,plain, % 98.89/98.95 (E(f2(x15631,f2(x15632,f2(x15633,f2(f2(a1,x15634),x15635)))),f2(f2(a1,f2(x15632,f2(x15633,f2(x15635,x15634)))),x15631))), % 98.89/98.95 inference(scs_inference,[],[9,1452,1558,2,5,4,3])). % 98.89/98.95 cnf(1566,plain, % 98.89/98.95 (E(f2(f2(f2(f2(f2(f2(a3,x15661),x15662),x15663),x15664),x15665),x15666),f2(f2(f2(f2(x15661,f2(x15662,x15663)),x15664),x15665),x15666))), % 98.89/98.95 inference(scs_inference,[],[1476,4])). % 98.89/98.95 cnf(1571,plain, % 98.89/98.95 (E(f2(f2(x15711,f2(f2(f2(f2(a3,x15712),x15713),x15714),x15715)),x15716),f2(f2(x15711,f2(f2(x15712,f2(x15713,x15714)),x15715)),x15716))), % 98.89/98.95 inference(scs_inference,[],[1477,4])). % 98.89/98.95 cnf(1573,plain, % 98.89/98.95 (~E(f2(f2(f2(a3,f2(a1,a5)),f2(a3,f2(a1,a6))),f2(f2(a3,f2(a1,f2(a1,a4))),f2(f2(a3,a3),a1))),f2(f2(a1,a5),f2(a6,a4)))), % 98.89/98.95 inference(scs_inference,[],[1477,1488,4,5,3])). % 98.89/98.95 cnf(1575,plain, % 98.89/98.95 (~E(f2(f2(a1,a5),f2(a6,a4)),f2(f2(f2(a3,f2(a1,a5)),f2(a3,f2(a1,a6))),f2(f2(a3,f2(a1,f2(a1,a4))),f2(f2(a3,a3),a1))))), % 98.89/98.95 inference(scs_inference,[],[1477,1488,4,5,3,2])). % 98.89/98.95 cnf(1578,plain, % 98.89/98.95 (~E(f2(f2(a1,f2(f2(a3,f2(a1,f2(a1,a4))),f2(f2(a3,a3),a1))),f2(f2(a3,f2(a1,a5)),f2(a3,f2(a1,a6)))),f2(f2(a1,a5),f2(a6,a4)))), % 98.89/98.95 inference(scs_inference,[],[9,1573,1481,4,5,3])). % 98.89/98.95 cnf(1580,plain, % 98.89/98.95 (~E(f2(f2(a1,a5),f2(a6,a4)),f2(f2(a1,f2(f2(a3,f2(a1,f2(a1,a4))),f2(f2(a3,a3),a1))),f2(f2(a3,f2(a1,a5)),f2(a3,f2(a1,a6)))))), % 98.89/98.95 inference(scs_inference,[],[9,1573,1481,4,5,3,2])). % 98.89/98.95 cnf(1589,plain, % 98.89/98.95 (~E(f2(f2(f2(a3,f2(a1,a5)),f2(a3,f2(a1,a6))),f2(f2(a3,f2(a1,f2(a1,a4))),f2(f2(a3,a3),a1))),f2(f2(f2(a1,a5),a1),f2(a6,a4)))), % 98.89/98.95 inference(scs_inference,[],[1575,1457,1526,4,5,3,2])). % 98.89/98.95 cnf(1590,plain, % 98.89/98.95 (E(f2(f2(x15901,f2(f2(f2(x15902,x15903),x15904),x15905)),x15906),f2(f2(x15901,f2(f2(f2(f2(a1,x15903),x15902),x15904),x15905)),x15906))), % 98.89/98.95 inference(scs_inference,[],[1541,4])). % 98.89/98.95 cnf(1595,plain, % 98.89/98.95 (E(f2(f2(f2(f2(f2(x15951,x15952),x15953),x15954),x15955),x15956),f2(f2(f2(f2(f2(f2(a1,x15952),x15951),x15953),x15954),x15955),x15956))), % 98.89/98.95 inference(scs_inference,[],[1542,4])). % 98.89/98.95 cnf(1597,plain, % 98.89/98.95 (~E(f2(f2(f2(a3,f2(a1,a5)),f2(a3,f2(a1,a6))),f2(f2(a3,f2(a1,f2(a1,a4))),f2(f2(f2(a1,a3),a3),a1))),f2(f2(f2(a1,a5),a1),f2(a6,a4)))), % 98.89/98.95 inference(scs_inference,[],[1589,1542,1547,4,5,3])). % 98.89/98.95 cnf(1602,plain, % 98.89/98.95 (~E(f2(f2(a1,f2(f2(f2(a1,f2(a1,f2(a1,a4))),a3),f2(f2(a3,a3),a1))),f2(f2(a3,f2(a1,a5)),f2(a3,f2(a1,a6)))),f2(f2(a1,a5),f2(a6,a4)))), % 98.89/98.95 inference(scs_inference,[],[1546,1578,1597,2,4,5,3])). % 98.89/98.95 cnf(1607,plain, % 98.89/98.95 (~E(f2(f2(a1,a5),f2(f2(a3,f2(f2(a1,a6),a1)),f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1)))),f2(f2(a1,f2(a1,a5)),f2(a1,f2(a6,a4))))), % 98.89/98.95 inference(scs_inference,[],[1551,1540,1602,2,4,5,3])). % 98.89/98.95 cnf(1611,plain, % 98.89/98.95 (E(f2(x16111,f2(f2(f2(x16112,f2(x16113,x16114)),x16115),x16116)),f2(x16111,f2(f2(f2(x16112,f2(f2(a1,x16114),x16113)),x16115),x16116)))), % 98.89/98.95 inference(scs_inference,[],[1552,1607,2,4,5])). % 98.89/98.95 cnf(1612,plain, % 98.89/98.95 (~E(f2(f2(f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a1,a1),f2(a3,a3))),a5),a6),f2(f2(f2(a3,f2(a1,a5)),a6),a4))), % 98.89/98.95 inference(scs_inference,[],[1552,1468,1607,2,4,5,3])). % 98.89/98.95 cnf(1615,plain, % 98.89/98.95 (E(f2(f2(f2(x16151,f2(x16152,f2(x16153,x16154))),x16155),x16156),f2(f2(f2(x16151,f2(x16152,f2(f2(a1,x16154),x16153))),x16155),x16156))), % 98.89/98.95 inference(scs_inference,[],[1556,1612,2,4])). % 98.89/98.95 cnf(1617,plain, % 98.89/98.95 (~E(f2(f2(a1,a5),f2(f2(a1,a4),a6)),f2(f2(a1,f2(f2(a3,f2(a1,f2(a1,a4))),f2(f2(a3,a3),a1))),f2(f2(a3,f2(a1,a5)),f2(a3,f2(a1,a6)))))), % 98.89/98.95 inference(scs_inference,[],[1556,1580,1612,1527,2,4,5,3])). % 98.89/98.95 cnf(1619,plain, % 98.89/98.95 (~E(f2(f2(a1,f2(f2(a3,f2(a1,f2(a1,a4))),f2(f2(a3,a3),a1))),f2(f2(a3,f2(a1,a5)),f2(a3,f2(a1,a6)))),f2(f2(a1,a5),f2(f2(a1,a4),a6)))), % 98.89/98.95 inference(scs_inference,[],[1617,2])). % 98.89/98.95 cnf(1631,plain, % 98.89/98.95 (~E(f2(f2(f2(a3,f2(a1,a5)),f2(a3,f2(a1,f2(a6,a4)))),a1),f2(f2(a1,a5),f2(f2(a3,f2(a1,a6)),f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1)))))), % 98.89/98.95 inference(scs_inference,[],[1068,1525,1563,5,4,3])). % 98.89/98.95 cnf(1634,plain, % 98.89/98.95 (E(f2(f2(x16341,f2(x16342,x16343)),x16344),f2(f2(f2(f2(a3,x16341),x16342),x16343),x16344))), % 98.89/98.95 inference(scs_inference,[],[12,4])). % 98.89/98.95 cnf(1635,plain, % 98.89/98.95 (E(f2(x16351,f2(x16352,f2(x16353,x16354))),f2(x16351,f2(f2(f2(a3,x16352),x16353),x16354)))), % 98.89/98.95 inference(scs_inference,[],[12,4,5])). % 98.89/98.95 cnf(1639,plain, % 98.89/98.95 (E(f2(f2(f2(x16391,f2(x16392,x16393)),x16394),x16395),f2(f2(f2(f2(f2(a3,x16391),x16392),x16393),x16394),x16395))), % 98.89/98.95 inference(scs_inference,[],[1634,4])). % 98.89/98.95 cnf(1641,plain, % 98.89/98.95 (~E(f2(f2(f2(f2(a3,a1),f2(a3,f2(a1,a6))),f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1))),f2(a1,a5)),f2(f2(a1,f2(a1,a5)),f2(a1,f2(a6,a4))))), % 98.89/98.95 inference(scs_inference,[],[1634,1560,4,5,3])). % 98.89/98.95 cnf(1645,plain, % 98.89/98.95 (E(f2(x16451,f2(x16452,f2(x16453,f2(x16454,x16455)))),f2(x16451,f2(x16452,f2(f2(f2(a3,x16453),x16454),x16455))))), % 98.89/98.95 inference(scs_inference,[],[1635,4,5])). % 98.89/98.95 cnf(1651,plain, % 98.89/98.95 (~E(f2(f2(f2(a3,f2(f2(f2(a3,a1),f2(a3,f2(a1,a6))),f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1)))),a1),a5),f2(f2(a1,f2(a1,a5)),f2(a1,f2(a6,a4))))), % 98.89/98.95 inference(scs_inference,[],[12,1641,1639,4,5,3])). % 98.89/98.95 cnf(1663,plain, % 98.89/98.95 (~E(f2(f2(f2(a3,f2(a1,f2(f2(a3,f2(a1,f2(a1,a4))),f2(f2(a3,a3),a1)))),f2(a3,f2(a1,a5))),f2(a3,f2(a1,a6))),f2(f2(a1,a5),f2(f2(a1,a4),a6)))), % 98.89/98.95 inference(scs_inference,[],[12,1645,1619,4,5,3])). % 98.89/98.95 cnf(1668,plain, % 98.89/98.95 (~E(f2(f2(f2(a3,f2(a1,a6)),f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1))),a5),f2(f2(f2(a3,f2(a1,a4)),f2(a3,f2(a1,a5))),a6))), % 98.89/98.95 inference(scs_inference,[],[12,1520,1461,1663,2,4,5,3])). % 98.89/98.95 cnf(1670,plain, % 98.89/98.95 (~E(f2(f2(f2(a3,f2(a1,a4)),f2(a3,f2(a1,a5))),a6),f2(f2(f2(a3,f2(a1,a6)),f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1))),a5))), % 98.89/98.95 inference(scs_inference,[],[1668,2])). % 98.89/98.95 cnf(1673,plain, % 98.89/98.95 (~E(f2(f2(f2(f2(a3,f2(a1,f2(a1,a4))),f2(f2(a3,a3),a1)),a5),a6),f2(f2(f2(a3,f2(a1,a4)),f2(a3,f2(a1,a5))),a6))), % 98.89/98.95 inference(scs_inference,[],[1510,1668,1462,1566,2,4,5,3])). % 98.89/98.95 cnf(1675,plain, % 98.89/98.95 (~E(f2(f2(f2(a3,f2(a1,a4)),f2(a3,f2(a1,a5))),a6),f2(f2(f2(f2(a3,f2(a1,f2(a1,a4))),f2(f2(a3,a3),a1)),a5),a6))), % 98.89/98.95 inference(scs_inference,[],[1673,2])). % 98.89/98.95 cnf(1686,plain, % 98.89/98.95 (E(f2(f2(f2(x16861,x16862),x16863),x16864),f2(f2(f2(f2(a3,f2(a1,x16863)),x16861),x16862),x16864))), % 98.89/98.95 inference(scs_inference,[],[13,4])). % 98.89/98.95 cnf(1691,plain, % 98.89/98.95 (E(f2(f2(f2(f2(x16911,x16912),x16913),x16914),x16915),f2(f2(f2(f2(f2(a3,f2(a1,x16913)),x16911),x16912),x16914),x16915))), % 98.89/98.95 inference(scs_inference,[],[1686,4])). % 98.89/98.95 cnf(1729,plain, % 98.89/98.95 (~E(f2(f2(f2(f2(f2(a3,f2(f2(f2(a3,a3),a1),f2(a1,a4))),f2(a3,a3)),a1),a5),a6),f2(f2(f2(a3,f2(a1,a4)),f2(a3,f2(a1,a5))),a6))), % 98.89/98.95 inference(scs_inference,[],[13,1458,1502,4,5,3,2])). % 98.89/98.95 cnf(1732,plain, % 98.89/98.95 (~E(f2(f2(f2(a3,f2(a1,a4)),f2(a3,f2(a1,a5))),a6),f2(f2(f2(f2(a1,f2(f2(a3,a3),a1)),f2(f2(f2(a3,a3),a1),f2(a1,a4))),a5),a6))), % 98.89/98.95 inference(scs_inference,[],[13,1448,1505,4,5,3])). % 98.89/98.95 cnf(1734,plain, % 98.89/98.95 (~E(f2(f2(f2(f2(a1,f2(f2(a3,a3),a1)),f2(f2(f2(a3,a3),a1),f2(a1,a4))),a5),a6),f2(f2(f2(a3,f2(a1,a4)),f2(a3,f2(a1,a5))),a6))), % 98.89/98.95 inference(scs_inference,[],[13,1448,1505,4,5,3,2])). % 98.89/98.95 cnf(1735,plain, % 98.89/98.95 (~E(f2(f2(a3,f2(a1,a4)),f2(a3,f2(a1,a5))),f2(f2(f2(a3,f2(a1,f2(a1,a4))),f2(f2(a3,a3),a1)),a5))), % 98.89/98.95 inference(scs_inference,[],[1675,4])). % 98.89/98.95 cnf(1736,plain, % 98.89/98.95 (~E(f2(f2(a3,f2(a1,a6)),f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1))),f2(a6,a4))), % 98.89/98.95 inference(scs_inference,[],[1675,1493,4,5])). % 98.89/98.95 cnf(1737,plain, % 98.89/98.95 (~E(f2(f2(f2(a3,f2(a1,a6)),f2(a3,f2(a1,a4))),f2(a3,f2(a1,a5))),f2(f2(f2(a3,f2(a1,a6)),f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1))),a5))), % 98.89/98.95 inference(scs_inference,[],[13,1670,1675,1493,4,5,3])). % 98.89/98.95 cnf(1739,plain, % 98.89/98.95 (~E(f2(f2(f2(a3,f2(a1,f2(a1,a4))),f2(f2(a3,a3),a1)),a5),f2(f2(a3,f2(a1,a4)),f2(a3,f2(a1,a5))))), % 98.89/98.95 inference(scs_inference,[],[13,1670,1675,1493,4,5,3,2])). % 98.89/98.95 cnf(1740,plain, % 98.89/98.95 (~E(f2(a6,a4),f2(f2(a3,f2(a1,a6)),f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1))))), % 98.89/98.95 inference(scs_inference,[],[1736,2])). % 98.89/98.95 cnf(1741,plain, % 98.89/98.95 (E(f2(f2(f2(f2(a3,f2(a1,x17411)),x17412),x17413),x17414),f2(f2(f2(x17412,x17413),x17411),x17414))), % 98.89/98.95 inference(scs_inference,[],[15,1736,2,4])). % 98.89/98.95 cnf(1742,plain, % 98.89/98.95 (E(f2(x17421,f2(f2(f2(a3,f2(a1,x17422)),x17423),x17424)),f2(x17421,f2(f2(x17423,x17424),x17422)))), % 98.89/98.95 inference(scs_inference,[],[15,1736,2,4,5])). % 98.89/98.95 cnf(1743,plain, % 98.89/98.95 (~E(f2(f2(f2(f2(a3,a3),a1),a5),f2(a1,a4)),f2(f2(a3,f2(a1,a4)),f2(a3,f2(a1,a5))))), % 98.89/98.95 inference(scs_inference,[],[15,1736,1739,2,4,5,3])). % 98.89/98.95 cnf(1746,plain, % 98.89/98.95 (~E(f2(f2(f2(f2(a3,f2(f2(f2(a3,a3),a1),f2(a1,a4))),f2(a3,a3)),a1),a5),f2(f2(a3,f2(a1,a4)),f2(a3,f2(a1,a5))))), % 98.89/98.95 inference(scs_inference,[],[1743,1729,2,4])). % 98.89/98.95 cnf(1747,plain, % 98.89/98.95 (~E(f2(f2(f2(f2(f2(a3,a3),a1),a5),f2(a1,a4)),a6),f2(f2(f2(a3,f2(a1,a4)),f2(a3,f2(a1,a5))),a6))), % 98.89/98.95 inference(scs_inference,[],[1743,1741,1729,1673,2,4,3])). % 98.89/98.95 cnf(1749,plain, % 98.89/98.95 (~E(f2(f2(f2(a3,f2(a1,a4)),f2(a3,f2(a1,a5))),a6),f2(f2(f2(f2(f2(a3,a3),a1),a5),f2(a1,a4)),a6))), % 98.89/98.95 inference(scs_inference,[],[1747,2])). % 98.89/98.95 cnf(1750,plain, % 98.89/98.95 (E(f2(f2(x17501,f2(f2(f2(a3,f2(a1,x17502)),x17503),x17504)),x17505),f2(f2(x17501,f2(f2(x17503,x17504),x17502)),x17505))), % 98.89/98.95 inference(scs_inference,[],[1742,1747,2,4])). % 98.89/98.95 cnf(1753,plain, % 98.89/98.95 (~E(f2(f2(a3,f2(a1,a4)),f2(a3,f2(a1,a5))),f2(f2(f2(f2(a3,f2(f2(f2(a3,a3),a1),f2(a1,a4))),f2(a3,a3)),a1),a5))), % 98.89/98.95 inference(scs_inference,[],[1746,2])). % 98.89/98.95 cnf(1754,plain, % 98.89/98.95 (~E(f2(f2(f2(a1,f2(f2(a3,a3),a1)),f2(f2(f2(a3,a3),a1),f2(a1,a4))),a5),f2(f2(a3,f2(a1,a4)),f2(a3,f2(a1,a5))))), % 98.89/98.95 inference(scs_inference,[],[1746,1734,2,4])). % 98.89/98.95 cnf(1755,plain, % 98.89/98.95 (~E(f2(f2(f2(a3,f2(a1,a5)),a6),a4),f2(f2(f2(f2(f2(a3,a3),a1),a5),f2(a1,a4)),a6))), % 98.89/98.95 inference(scs_inference,[],[15,1749,1746,1734,2,4,3])). % 98.89/98.95 cnf(1757,plain, % 98.89/98.95 (~E(f2(f2(f2(f2(f2(a3,a3),a1),a5),f2(a1,a4)),a6),f2(f2(f2(a3,f2(a1,a5)),a6),a4))), % 98.89/98.95 inference(scs_inference,[],[1755,2])). % 98.89/98.95 cnf(1760,plain, % 98.89/98.95 (~E(f2(f2(a1,a4),a6),f2(f2(a3,f2(a1,a6)),f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1))))), % 98.89/98.95 inference(scs_inference,[],[1740,1755,1750,9,2,4,5,3])). % 98.89/98.95 cnf(1762,plain, % 98.89/98.95 (~E(f2(f2(a3,f2(a1,a6)),f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1))),f2(f2(a1,a4),a6))), % 98.89/98.95 inference(scs_inference,[],[1760,2])). % 98.89/98.95 cnf(1763,plain, % 98.89/98.95 (~E(f2(f2(a3,f2(a1,a4)),f2(a3,f2(a1,a5))),f2(f2(f2(a1,f2(f2(a3,a3),a1)),f2(f2(f2(a3,a3),a1),f2(a1,a4))),a5))), % 98.89/98.95 inference(scs_inference,[],[1760,1732,2,4])). % 98.89/98.95 cnf(1764,plain, % 98.89/98.95 (~E(f2(f2(f2(a3,f2(a1,a5)),f2(a3,f2(a1,f2(a6,a4)))),a1),f2(f2(f2(a3,f2(a1,a6)),f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1))),a5))), % 98.89/98.95 inference(scs_inference,[],[1760,726,1737,1732,2,4,3])). % 98.89/98.95 cnf(1768,plain, % 98.89/98.95 (~E(f2(f2(f2(f2(f2(a3,f2(a1,a5)),f2(a3,a3)),a1),f2(a1,a4)),a6),f2(f2(f2(a3,f2(a1,a5)),a6),a4))), % 98.89/98.95 inference(scs_inference,[],[1757,1691,1764,1507,2,4,3])). % 98.89/98.95 cnf(1770,plain, % 98.89/98.95 (~E(f2(f2(f2(a3,f2(a1,a5)),a6),a4),f2(f2(f2(f2(f2(a3,f2(a1,a5)),f2(a3,a3)),a1),f2(a1,a4)),a6))), % 98.89/98.95 inference(scs_inference,[],[1768,2])). % 98.89/98.95 cnf(1771,plain, % 98.89/98.95 (~E(f2(a1,f2(a6,a4)),f2(a1,f2(f2(a3,f2(a1,a6)),f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1)))))), % 98.89/98.95 inference(scs_inference,[],[1768,1545,2,4])). % 98.89/98.95 cnf(1775,plain, % 98.89/98.95 (~E(f2(a1,f2(f2(a3,f2(a1,a6)),f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1)))),f2(a1,f2(a6,a4)))), % 98.89/98.95 inference(scs_inference,[],[1771,2])). % 98.89/98.95 cnf(1777,plain, % 98.89/98.95 (~E(f2(f2(a6,a4),a5),f2(f2(f2(f2(f2(a3,f2(a1,a5)),f2(a3,a3)),a1),f2(a1,a4)),a6))), % 98.89/98.95 inference(scs_inference,[],[15,1770,1771,1511,2,4,3])). % 98.89/98.95 cnf(1780,plain, % 98.89/98.95 (~E(f2(f2(f2(f2(f2(a3,f2(a1,a5)),f2(a3,a3)),a1),f2(a1,a4)),a6),f2(f2(a6,a4),a5))), % 98.89/98.95 inference(scs_inference,[],[1777,2])). % 98.89/98.95 cnf(1781,plain, % 98.89/98.95 (~E(f2(f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1)),a5),f2(f2(a3,f2(a1,a4)),f2(a3,f2(a1,a5))))), % 98.89/98.95 inference(scs_inference,[],[1777,1510,2,4])). % 98.89/98.95 cnf(1785,plain, % 98.89/98.95 (~E(f2(f2(a3,f2(a1,a4)),f2(a3,f2(a1,a5))),f2(f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1)),a5))), % 98.89/98.95 inference(scs_inference,[],[1781,2])). % 98.89/98.95 cnf(1787,plain, % 98.89/98.95 (~E(f2(f2(f2(f2(a1,a3),f2(a1,f2(a1,a5))),f2(a1,a4)),a6),f2(f2(a6,a4),a5))), % 98.89/98.95 inference(scs_inference,[],[1780,1781,1318,1512,2,4,3])). % 98.89/98.95 cnf(1789,plain, % 98.89/98.95 (~E(f2(f2(a6,a4),a5),f2(f2(f2(f2(a1,a3),f2(a1,f2(a1,a5))),f2(a1,a4)),a6))), % 98.89/98.95 inference(scs_inference,[],[1787,2])). % 98.89/98.95 cnf(1790,plain, % 98.89/98.95 (~E(f2(f2(f2(a3,f2(a1,f2(f2(a3,a3),a1))),f2(a3,f2(a3,f2(a1,a6)))),f2(f2(f2(a3,a3),a1),f2(a1,a4))),f2(f2(a1,a4),a6))), % 98.89/98.95 inference(scs_inference,[],[16,1787,1762,2,3])). % 98.89/98.95 cnf(1793,plain, % 98.89/98.95 (~E(f2(f2(f2(a1,a4),a6),a5),f2(f2(f2(f2(a1,a3),f2(a1,f2(a1,a5))),f2(a1,a4)),a6))), % 98.89/98.95 inference(scs_inference,[],[1789,1790,1526,2,3])). % 98.89/98.95 cnf(1795,plain, % 98.89/98.95 (E(f2(x17951,f2(x17952,f2(x17953,x17954))),f2(x17951,f2(f2(f2(a3,f2(a1,x17954)),f2(a3,x17952)),x17953)))), % 98.89/98.95 inference(scs_inference,[],[16,1789,1790,1526,2,3,5])). % 98.89/98.95 cnf(1796,plain, % 98.89/98.95 (~E(f2(f2(f2(f2(a1,a3),f2(a1,f2(a1,a5))),f2(a1,a4)),a6),f2(f2(f2(a1,a4),a6),a5))), % 98.89/98.95 inference(scs_inference,[],[1793,2])). % 98.89/98.95 cnf(1797,plain, % 98.89/98.95 (~E(f2(f2(f2(a3,f2(a1,f2(a1,a5))),f2(a3,f2(a3,f2(a1,a4)))),a3),f2(f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1)),a5))), % 98.89/98.95 inference(scs_inference,[],[16,1793,1785,2,3])). % 98.89/98.95 cnf(1800,plain, % 98.89/98.95 (E(f2(f2(x18001,f2(x18002,x18003)),x18004),f2(f2(f2(f2(a3,f2(a1,x18003)),f2(a3,x18001)),x18002),x18004))), % 98.89/98.95 inference(scs_inference,[],[16,1797,2,4])). % 98.89/98.95 cnf(1801,plain, % 98.89/98.95 (~E(f2(f2(f2(f2(a1,a3),f2(a1,f2(f2(a1,a5),a1))),f2(a1,a4)),a6),f2(f2(f2(a1,a4),a6),a5))), % 98.89/98.95 inference(scs_inference,[],[16,1796,1797,1615,2,4,3])). % 98.89/98.95 cnf(1803,plain, % 98.89/98.95 (~E(f2(f2(f2(a1,a4),a6),a5),f2(f2(f2(f2(a1,a3),f2(a1,f2(f2(a1,a5),a1))),f2(a1,a4)),a6))), % 98.89/98.95 inference(scs_inference,[],[1801,2])). % 98.89/98.95 cnf(1804,plain, % 98.89/98.95 (~E(f2(f2(f2(a3,f2(a1,f2(a1,a5))),f2(a3,f2(a3,f2(a1,a4)))),a3),f2(f2(f2(a3,f2(a1,f2(a1,a4))),f2(f2(a3,a3),a1)),a5))), % 98.89/98.95 inference(scs_inference,[],[16,1801,1735,2,3])). % 98.89/98.95 cnf(1807,plain, % 98.89/98.95 (~E(f2(f2(a6,a4),a5),f2(f2(f2(f2(a1,a3),f2(a1,f2(f2(a1,a5),a1))),f2(a1,a4)),a6))), % 98.89/98.95 inference(scs_inference,[],[1803,1804,1416,2,3])). % 98.89/98.95 cnf(1811,plain, % 98.89/98.95 (~E(f2(f2(f2(a3,f2(a1,f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1)))),f2(a3,a1)),f2(a3,f2(a1,a6))),f2(a1,f2(a6,a4)))), % 98.89/98.95 inference(scs_inference,[],[16,1807,1775,2,3])). % 98.89/98.95 cnf(1813,plain, % 98.89/98.95 (~E(f2(a1,f2(a6,a4)),f2(f2(f2(a3,f2(a1,f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1)))),f2(a3,a1)),f2(a3,f2(a1,a6))))), % 98.89/98.95 inference(scs_inference,[],[1811,2])). % 98.89/98.95 cnf(1814,plain, % 98.89/98.95 (~E(f2(f2(f2(a3,f2(a1,f2(a1,a5))),f2(a3,f2(a3,f2(a1,a4)))),a3),f2(f2(f2(a1,f2(f2(a3,a3),a1)),f2(f2(f2(a3,a3),a1),f2(a1,a4))),a5))), % 98.89/98.95 inference(scs_inference,[],[16,1763,1811,2,3])). % 98.89/98.95 cnf(1816,plain, % 98.89/98.95 (E(f2(f2(f2(x18161,f2(x18162,x18163)),x18164),x18165),f2(f2(f2(f2(f2(a3,f2(a1,x18163)),f2(a3,x18161)),x18162),x18164),x18165))), % 98.89/98.95 inference(scs_inference,[],[16,1800,1763,1811,2,3,4])). % 98.89/98.95 cnf(1818,plain, % 98.89/98.95 (~E(f2(f2(f2(a3,f2(a1,f2(a1,a5))),f2(a3,f2(a3,f2(a1,a4)))),a3),f2(f2(f2(f2(a3,f2(f2(f2(a3,a3),a1),f2(a1,a4))),f2(a3,a3)),a1),a5))), % 98.89/98.95 inference(scs_inference,[],[16,1753,1814,2,3])). % 98.89/98.95 cnf(1821,plain, % 98.89/98.95 (~E(f2(f2(f2(f2(f2(a3,f2(a1,a1)),f2(a3,a1)),f2(a3,a3)),f2(f2(f2(a3,a3),a1),f2(a1,a4))),a5),f2(f2(a3,f2(a1,a4)),f2(a3,f2(a1,a5))))), % 98.89/98.95 inference(scs_inference,[],[1754,1816,1818,2,3])). % 98.89/98.95 cnf(1824,plain, % 98.89/98.95 (~E(f2(f2(a3,f2(a1,a4)),f2(a3,f2(a1,a5))),f2(f2(f2(f2(f2(a3,f2(a1,a1)),f2(a3,a1)),f2(a3,a3)),f2(f2(f2(a3,a3),a1),f2(a1,a4))),a5))), % 98.89/98.95 inference(scs_inference,[],[1821,2])). % 98.89/98.95 cnf(1825,plain, % 98.89/98.95 (~E(f2(f2(f2(a3,f2(a1,a4)),f2(a3,a1)),a6),f2(f2(f2(a3,f2(a1,f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1)))),f2(a3,a1)),f2(a3,f2(a1,a6))))), % 98.89/98.95 inference(scs_inference,[],[16,1821,1813,2,3])). % 98.89/98.95 cnf(1828,plain, % 98.89/98.95 (~E(f2(f2(a3,f2(a1,a4)),f2(f2(f2(a3,f2(a1,a5)),f2(a3,a3)),a1)),f2(f2(f2(f2(f2(a3,f2(a1,a1)),f2(a3,a1)),f2(a3,a3)),f2(f2(f2(a3,a3),a1),f2(a1,a4))),a5))), % 98.89/98.95 inference(scs_inference,[],[1824,1825,1795,2,3])). % 98.89/98.95 cnf(1830,plain, % 98.89/98.95 (E(f2(f2(f2(f2(a3,f2(a1,x18301)),f2(a3,x18302)),x18303),x18304),f2(f2(x18302,f2(x18303,x18301)),x18304))), % 98.89/98.95 inference(scs_inference,[],[18,1824,1825,1795,2,3,4])). % 98.89/98.95 cnf(1831,plain, % 98.89/98.95 (~E(f2(f2(f2(f2(f2(a3,f2(a1,a1)),f2(a3,a1)),f2(a3,a3)),f2(f2(f2(a3,a3),a1),f2(a1,a4))),a5),f2(f2(a3,f2(a1,a4)),f2(f2(f2(a3,f2(a1,a5)),f2(a3,a3)),a1)))), % 98.89/98.95 inference(scs_inference,[],[1828,2])). % 98.89/98.95 cnf(1841,plain, % 98.89/98.95 (~E(f2(f2(f2(a3,f2(a1,a6)),f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1))),a5),f2(f2(f2(a3,f2(a1,a6)),f2(a3,f2(a1,a4))),f2(a3,f2(a1,a5))))), % 98.89/98.95 inference(scs_inference,[],[1737,2])). % 98.89/98.95 cnf(1906,plain, % 98.89/98.95 (~E(f2(f2(f2(f2(f2(a3,f2(a1,a1)),f2(a3,a1)),f2(a3,a3)),f2(f2(f2(f2(a1,a3),a3),a1),f2(a1,a4))),a5),f2(f2(a3,f2(a1,a4)),f2(f2(f2(a3,f2(a1,a5)),f2(a3,a3)),a1)))), % 98.89/98.95 inference(scs_inference,[],[1831,1590,3])). % 98.89/98.95 cnf(1910,plain, % 98.89/98.95 (~E(f2(f2(a3,f2(a1,a4)),f2(f2(f2(a3,f2(a1,a5)),f2(a3,a3)),a1)),f2(f2(f2(f2(f2(a3,f2(a1,a1)),f2(a3,a1)),f2(a3,a3)),f2(f2(f2(f2(a1,a3),a3),a1),f2(a1,a4))),a5))), % 98.89/98.95 inference(scs_inference,[],[1906,2])). % 98.89/98.95 cnf(1946,plain, % 98.89/98.95 (~E(f2(f2(f2(a3,f2(a1,a6)),f2(f2(a3,f2(a1,f2(a1,a4))),f2(f2(a3,a3),a1))),a5),f2(f2(f2(a3,f2(a1,a6)),f2(a3,f2(a1,a4))),f2(a3,f2(a1,a5))))), % 98.89/98.95 inference(scs_inference,[],[1841,1571,3])). % 98.89/98.95 cnf(1950,plain, % 98.89/98.95 (~E(f2(f2(f2(a3,f2(a1,a6)),f2(a3,f2(a1,a4))),f2(a3,f2(a1,a5))),f2(f2(f2(a3,f2(a1,a6)),f2(f2(a3,f2(a1,f2(a1,a4))),f2(f2(a3,a3),a1))),a5))), % 98.89/98.95 inference(scs_inference,[],[1946,2])). % 98.89/98.95 cnf(1968,plain, % 98.89/98.95 (~E(f2(f2(a3,f2(a1,a4)),f2(f2(f2(a3,f2(f2(a1,a5),a1)),f2(a3,a3)),a1)),f2(f2(f2(f2(f2(a3,f2(a1,a1)),f2(a3,a1)),f2(a3,a3)),f2(f2(f2(f2(a1,a3),a3),a1),f2(a1,a4))),a5))), % 98.89/98.95 inference(scs_inference,[],[1910,1611,3])). % 98.89/98.95 cnf(1970,plain, % 98.89/98.95 (~E(f2(f2(f2(f2(f2(a3,f2(a1,a1)),f2(a3,a1)),f2(a3,a3)),f2(f2(f2(f2(a1,a3),a3),a1),f2(a1,a4))),a5),f2(f2(a3,f2(a1,a4)),f2(f2(f2(a3,f2(f2(a1,a5),a1)),f2(a3,a3)),a1)))), % 98.89/98.95 inference(scs_inference,[],[1968,2])). % 98.89/98.95 cnf(1974,plain, % 98.89/98.95 (~E(f2(f2(f2(f2(f2(f2(a1,f2(a1,a1)),a3),f2(a3,a1)),f2(a3,a3)),f2(f2(f2(f2(a1,a3),a3),a1),f2(a1,a4))),a5),f2(f2(a3,f2(a1,a4)),f2(f2(f2(a3,f2(f2(a1,a5),a1)),f2(a3,a3)),a1)))), % 98.89/98.95 inference(scs_inference,[],[1970,1595,3])). % 98.89/98.95 cnf(1979,plain, % 98.89/98.95 (~E(f2(f2(a1,f2(a1,a4)),f2(a1,f2(f2(a3,f2(a1,a5)),a6))),f2(f2(a1,a5),f2(f2(a3,f2(a1,a6)),f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1)))))), % 98.89/98.95 inference(scs_inference,[],[818,1974,1631,2,3])). % 98.89/98.95 cnf(1982,plain, % 98.89/98.95 (~E(f2(f2(f2(a3,f2(a1,f2(f2(a3,f2(a1,a5)),a6))),a1),a4),f2(f2(f2(a3,f2(a1,a6)),f2(f2(a3,f2(a1,f2(a1,a4))),f2(f2(a3,a3),a1))),a5))), % 98.89/98.95 inference(scs_inference,[],[26,1950,1979,2,3])). % 98.89/98.95 cnf(2114,plain, % 98.89/98.95 (~E(f2(f2(a1,f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1))),f2(f2(a3,f2(a1,f2(a1,a5))),f2(f2(a3,a1),f2(a3,f2(a1,a6))))),f2(f2(a1,f2(a1,a5)),f2(a1,f2(a6,a4))))), % 98.89/98.95 inference(scs_inference,[],[84,1651,3])). % 98.89/98.95 cnf(2116,plain, % 98.89/98.95 (~E(f2(f2(a1,f2(a1,a5)),f2(a1,f2(a6,a4))),f2(f2(a1,f2(f2(f2(f2(a3,a3),a1),f2(a1,a4)),f2(f2(a3,a3),a1))),f2(f2(a3,f2(a1,f2(a1,a5))),f2(f2(a3,a1),f2(a3,f2(a1,a6))))))), % 98.89/98.95 inference(scs_inference,[],[2114,2])). % 98.89/98.95 cnf(2123,plain, % 98.89/98.95 (E(f2(f2(f2(f2(f2(a3,f2(a1,x21231)),f2(a3,x21232)),x21233),x21234),x21235),f2(f2(f2(x21232,f2(x21233,x21231)),x21234),x21235))), % 98.89/98.95 inference(scs_inference,[],[2116,1830,586,3,5,4])). % 98.89/98.95 cnf(2127,plain, % 98.89/98.95 (~E(f2(f2(a6,a4),a5),f2(f2(f2(a3,f2(a1,a5)),f2(a1,a4)),a6))), % 98.89/98.95 inference(scs_inference,[],[2123,1780,3,2])). % 98.89/98.95 cnf(2147,plain, % 98.89/98.95 (~E(f2(f2(a3,f2(a1,f2(a6,a4))),a1),f2(f2(a3,f2(a1,a6)),f2(f2(a3,f2(a1,f2(a1,a4))),f2(f2(a3,a3),a1))))), % 98.89/98.95 inference(scs_inference,[],[35,1982,3,4])). % 98.89/98.95 cnf(2151,plain, % 98.89/98.95 ($false), % 98.89/98.95 inference(scs_inference,[],[2127,2147,1280,1526,13,4,2,3]), % 98.89/98.95 ['proof']). % 98.89/98.95 % SZS output end Proof % 98.89/98.95 % Total time :98.280000s %------------------------------------------------------------------------------