%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SWV324-2 : TPTP v8.2.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n025.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 16:46:43 EDT 2024 % Result : Unsatisfiable 59.40s 59.48s % Output : CNFRefutation 59.46s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SWV324-2 : TPTP v8.2.0. Released v3.2.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n025.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 : Thu Jun 20 19:01:09 EDT 2024 % 0.12/0.33 % CPUTime : % 0.48/0.56 start to proof:theBenchmark % 59.40/59.47 %------------------------------------------- % 59.40/59.47 % File :CSE---1.7 % 59.40/59.47 % Problem :theBenchmark % 59.40/59.47 % Transform :cnf % 59.40/59.47 % Format :tptp:raw % 59.40/59.47 % Command :java -jar mcs_scs.jar %d %s % 59.40/59.47 % 59.40/59.47 % Result :Theorem 58.870000s % 59.40/59.47 % Output :CNFRefutation 58.870000s % 59.40/59.47 %------------------------------------------- % 59.40/59.48 %------------------------------------------------------------------------------ % 59.40/59.48 % File : SWV324-2 : TPTP v8.2.0. Released v3.2.0. % 59.40/59.48 % Domain : Software Verification (Security) % 59.40/59.48 % Problem : Cryptographic protocol problem for Otway Rees % 59.40/59.48 % Version : [Pau06] axioms : Reduced > Especial. % 59.40/59.48 % English : % 59.40/59.48 % 59.40/59.48 % Refs : [Pau06] Paulson (2006), Email to G. Sutcliffe % 59.40/59.48 % Source : [Pau06] % 59.40/59.48 % Names : % 59.40/59.48 % 59.40/59.48 % Status : Unsatisfiable % 59.40/59.48 % Rating : 0.10 v8.1.0, 0.00 v7.5.0, 0.05 v7.4.0, 0.06 v7.3.0, 0.08 v7.1.0, 0.00 v7.0.0, 0.20 v6.4.0, 0.13 v6.3.0, 0.00 v6.2.0, 0.10 v6.1.0, 0.14 v6.0.0, 0.10 v5.5.0, 0.20 v5.4.0, 0.25 v5.3.0, 0.17 v5.2.0, 0.12 v5.0.0, 0.14 v4.1.0, 0.08 v4.0.1, 0.00 v4.0.0, 0.09 v3.7.0, 0.00 v3.5.0, 0.09 v3.4.0, 0.25 v3.3.0, 0.29 v3.2.0 % 59.40/59.48 % Syntax : Number of clauses : 8 ( 2 unt; 1 nHn; 8 RR) % 59.40/59.48 % Number of literals : 14 ( 1 equ; 6 neg) % 59.40/59.48 % Maximal clause size : 2 ( 1 avg) % 59.40/59.48 % Maximal term depth : 7 ( 2 avg) % 59.40/59.48 % Number of predicates : 2 ( 1 usr; 0 prp; 2-3 aty) % 59.40/59.48 % Number of functors : 23 ( 23 usr; 13 con; 0-3 aty) % 59.40/59.48 % Number of variables : 12 ( 4 sgn) % 59.40/59.48 % SPC : CNF_UNS_RFO_SEQ_NHN % 59.40/59.48 % 59.40/59.48 % Comments : The problems in the [Pau06] collection each have very many axioms, % 59.40/59.48 % of which only a small selection are required for the refutation. % 59.40/59.48 % The mission is to find those few axioms, after which a refutation % 59.40/59.48 % can be quite easily found. This version has only the necessary % 59.40/59.48 % axioms. % 59.40/59.48 %------------------------------------------------------------------------------ % 59.40/59.48 cnf(cls_conjecture_1,negated_conjecture, % 59.40/59.48 c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_B,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_OMPair(v_X,c_Message_Omsg_OCrypt(c_Public_OshrK(v_B),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_OKey(v_K)))))),c_List_Oset(v_evso,tc_Event_Oevent),tc_Event_Oevent) ). % 59.40/59.48 % 59.40/59.48 cnf(cls_conjecture_2,negated_conjecture, % 59.40/59.48 ~ c_in(v_A,c_Event_Obad,tc_Message_Oagent) ). % 59.40/59.48 % 59.40/59.48 cnf(cls_conjecture_3,negated_conjecture, % 59.40/59.48 ( c_in(v_A,c_Event_Obad,tc_Message_Oagent) % 59.40/59.48 | ~ c_in(c_Message_Omsg_OKey(c_Public_OshrK(v_A)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evso)),tc_Message_Omsg) ) ). % 59.40/59.48 % 59.40/59.48 cnf(cls_conjecture_6,negated_conjecture, % 59.40/59.48 ( c_Public_OshrK(v_A) = v_K % 59.40/59.48 | c_in(v_A,c_Event_Obad,tc_Message_Oagent) ) ). % 59.40/59.48 % 59.40/59.48 cnf(cls_Event_OSays__imp__analz__Spy__dest_0,axiom, % 59.40/59.48 ( ~ c_in(c_Event_Oevent_OSays(V_A,V_B,V_X),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent) % 59.40/59.48 | c_in(V_X,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg) ) ). % 59.40/59.48 % 59.40/59.48 cnf(cls_Message_OMPair__parts_0,axiom, % 59.40/59.48 ( ~ c_in(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Oparts(V_H),tc_Message_Omsg) % 59.40/59.48 | c_in(V_Y,c_Message_Oparts(V_H),tc_Message_Omsg) ) ). % 59.40/59.48 % 59.40/59.48 cnf(cls_Message_Oanalz__into__parts__dest_0,axiom, % 59.40/59.48 ( ~ c_in(V_c,c_Message_Oanalz(V_H),tc_Message_Omsg) % 59.40/59.48 | c_in(V_c,c_Message_Oparts(V_H),tc_Message_Omsg) ) ). % 59.40/59.48 % 59.40/59.48 cnf(cls_Message_Oparts_OBody__dest_0,axiom, % 59.40/59.48 ( ~ c_in(c_Message_Omsg_OCrypt(V_K,V_X),c_Message_Oparts(V_H),tc_Message_Omsg) % 59.40/59.48 | c_in(V_X,c_Message_Oparts(V_H),tc_Message_Omsg) ) ). % 59.40/59.48 % 59.40/59.48 %------------------------------------------------------------------------------ % 59.40/59.48 %------------------------------------------- % 59.40/59.48 % Proof found % 59.40/59.48 % SZS status Theorem for theBenchmark % 59.40/59.48 % SZS output start Proof % 59.46/59.49 %ClaNum:30(EqnAxiom:22) % 59.46/59.49 %VarNum:20(SingletonVarNum:12) % 59.46/59.49 %MaxLitNum:2 % 59.46/59.49 %MaxfuncDepth:6 % 59.46/59.49 %SharedTerms:32 % 59.46/59.49 %goalClause: 23 24 25 29 % 59.46/59.49 %singleGoalClaCount:2 % 59.46/59.49 [24]~P1(a16,a3,a17) % 59.46/59.49 [23]P1(f2(a1,a6,f12(f7(a19),f12(a21,f9(f13(a6),f12(f7(a22),f8(a20)))))),f4(a23,a15),a15) % 59.46/59.49 [25]P1(a16,a3,a17)+E(f13(a16),a20) % 59.46/59.49 [29]P1(a16,a3,a17)+~P1(f8(f13(a16)),f14(f5(a11,a23)),a18) % 59.46/59.49 [26]~P1(x261,f10(x262),a18)+P1(x261,f14(x262),a18) % 59.46/59.49 [27]P1(x271,f14(x272),a18)+~P1(f12(x273,x271),f14(x272),a18) % 59.46/59.49 [28]P1(x281,f14(x282),a18)+~P1(f9(x283,x281),f14(x282),a18) % 59.46/59.49 [30]~P1(f2(x303,x304,x301),f4(x302,a15),a15)+P1(x301,f10(f5(a11,x302)),a18) % 59.46/59.49 %EqnAxiom % 59.46/59.49 [1]E(x11,x11) % 59.46/59.49 [2]E(x22,x21)+~E(x21,x22) % 59.46/59.49 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 59.46/59.49 [4]~E(x41,x42)+E(f7(x41),f7(x42)) % 59.46/59.49 [5]~E(x51,x52)+E(f13(x51),f13(x52)) % 59.46/59.49 [6]~E(x61,x62)+E(f4(x61,x63),f4(x62,x63)) % 59.46/59.49 [7]~E(x71,x72)+E(f4(x73,x71),f4(x73,x72)) % 59.46/59.49 [8]~E(x81,x82)+E(f8(x81),f8(x82)) % 59.46/59.49 [9]~E(x91,x92)+E(f12(x91,x93),f12(x92,x93)) % 59.46/59.49 [10]~E(x101,x102)+E(f12(x103,x101),f12(x103,x102)) % 59.46/59.49 [11]~E(x111,x112)+E(f9(x111,x113),f9(x112,x113)) % 59.46/59.49 [12]~E(x121,x122)+E(f9(x123,x121),f9(x123,x122)) % 59.46/59.49 [13]~E(x131,x132)+E(f5(x131,x133),f5(x132,x133)) % 59.46/59.49 [14]~E(x141,x142)+E(f5(x143,x141),f5(x143,x142)) % 59.46/59.49 [15]~E(x151,x152)+E(f14(x151),f14(x152)) % 59.46/59.49 [16]~E(x161,x162)+E(f2(x161,x163,x164),f2(x162,x163,x164)) % 59.46/59.49 [17]~E(x171,x172)+E(f2(x173,x171,x174),f2(x173,x172,x174)) % 59.46/59.49 [18]~E(x181,x182)+E(f2(x183,x184,x181),f2(x183,x184,x182)) % 59.46/59.49 [19]~E(x191,x192)+E(f10(x191),f10(x192)) % 59.46/59.49 [20]P1(x202,x203,x204)+~E(x201,x202)+~P1(x201,x203,x204) % 59.46/59.49 [21]P1(x213,x212,x214)+~E(x211,x212)+~P1(x213,x211,x214) % 59.46/59.49 [22]P1(x223,x224,x222)+~E(x221,x222)+~P1(x223,x224,x221) % 59.46/59.49 % 59.46/59.49 %------------------------------------------- % 59.46/59.50 cnf(37,plain, % 59.46/59.50 (E(f13(a16),a20)), % 59.46/59.50 inference(scs_inference,[],[24,25])). % 59.46/59.50 cnf(38,plain, % 59.46/59.50 (~P1(f8(f13(a16)),f14(f5(a11,a23)),a18)), % 59.46/59.50 inference(scs_inference,[],[24,29])). % 59.46/59.50 cnf(39,plain, % 59.46/59.50 (~P1(f8(f13(a16)),f10(f5(a11,a23)),a18)), % 59.46/59.50 inference(scs_inference,[],[38,26])). % 59.46/59.50 cnf(41,plain, % 59.46/59.50 (~P1(f12(x411,f8(f13(a16))),f14(f5(a11,a23)),a18)), % 59.46/59.50 inference(scs_inference,[],[38,26,27])). % 59.46/59.50 cnf(48,plain, % 59.46/59.50 (E(f7(a20),f7(f13(a16)))), % 59.46/59.50 inference(scs_inference,[],[37,4,2])). % 59.46/59.50 cnf(49,plain, % 59.46/59.50 (~P1(f12(x491,f12(x492,f8(f13(a16)))),f14(f5(a11,a23)),a18)), % 59.46/59.50 inference(scs_inference,[],[41,27])). % 59.46/59.50 cnf(53,plain, % 59.46/59.50 (~P1(f9(x531,f12(x532,f8(f13(a16)))),f14(f5(a11,a23)),a18)), % 59.46/59.50 inference(scs_inference,[],[41,27,26,28])). % 59.46/59.50 cnf(55,plain, % 59.46/59.50 (E(f7(f13(a16)),f7(a20))), % 59.46/59.50 inference(scs_inference,[],[48,41,27,26,28,2])). % 59.46/59.50 cnf(58,plain, % 59.46/59.50 (E(f13(f4(f13(a16),x581)),f13(f4(a20,x581)))), % 59.46/59.50 inference(scs_inference,[],[37,5,6])). % 59.46/59.50 cnf(61,plain, % 59.46/59.50 (~P1(f12(x611,f12(x612,f12(x613,f8(f13(a16))))),f14(f5(a11,a23)),a18)), % 59.46/59.50 inference(scs_inference,[],[49,26,27])). % 59.46/59.50 cnf(63,plain, % 59.46/59.50 (~P1(f9(x631,f12(x632,f12(x633,f8(f13(a16))))),f14(f5(a11,a23)),a18)), % 59.46/59.50 inference(scs_inference,[],[49,26,27,28])). % 59.46/59.50 cnf(69,plain, % 59.46/59.50 (~P1(f12(x691,f12(x692,f12(x693,f12(x694,f8(f13(a16)))))),f14(f5(a11,a23)),a18)), % 59.46/59.50 inference(scs_inference,[],[61,27])). % 59.46/59.50 cnf(73,plain, % 59.46/59.50 (~P1(f9(x731,f12(x732,f12(x733,f12(x734,f8(f13(a16)))))),f14(f5(a11,a23)),a18)), % 59.46/59.50 inference(scs_inference,[],[61,27,26,28])). % 59.46/59.50 cnf(83,plain, % 59.46/59.50 (~P1(f9(x831,f9(x832,f12(x833,f12(x834,f8(f13(a16)))))),f14(f5(a11,a23)),a18)), % 59.46/59.50 inference(scs_inference,[],[69,63,26,27,28])). % 59.46/59.50 cnf(91,plain, % 59.46/59.50 (~P1(f9(x911,f9(x912,f12(x913,f8(f13(a16))))),f14(f5(a11,a23)),a18)), % 59.46/59.50 inference(scs_inference,[],[73,53,27,26,28])). % 59.46/59.50 cnf(94,plain, % 59.46/59.50 (E(f9(f9(x941,f13(a16)),x942),f9(f9(x941,a20),x942))), % 59.46/59.50 inference(scs_inference,[],[37,11,12])). % 59.46/59.50 cnf(102,plain, % 59.46/59.50 (E(f5(f5(x1021,f13(a16)),x1022),f5(f5(x1021,a20),x1022))), % 59.46/59.50 inference(scs_inference,[],[37,13,14])). % 59.46/59.50 cnf(109,plain, % 59.46/59.50 (E(f5(f5(x1091,a20),x1092),f5(f5(x1091,f13(a16)),x1092))), % 59.46/59.50 inference(scs_inference,[],[102,83,91,27,26,28,2])). % 59.46/59.50 cnf(110,plain, % 59.46/59.50 (E(f2(f2(x1101,f13(a16),x1102),x1103,x1104),f2(f2(x1101,a20,x1102),x1103,x1104))), % 59.46/59.50 inference(scs_inference,[],[37,16,17])). % 59.46/59.50 cnf(231,plain, % 59.46/59.50 (E(f4(a20,x2311),f4(f13(a16),x2311))), % 59.46/59.50 inference(scs_inference,[],[37,2,6])). % 59.46/59.50 cnf(232,plain, % 59.46/59.50 (E(f4(f13(a16),x2321),f4(a20,x2321))), % 59.46/59.50 inference(scs_inference,[],[231,2])). % 59.46/59.50 cnf(233,plain, % 59.46/59.50 (E(f4(x2331,a20),f4(x2331,f13(a16)))), % 59.46/59.50 inference(scs_inference,[],[37,2,7])). % 59.46/59.50 cnf(234,plain, % 59.46/59.50 (E(f4(x2341,f13(a16)),f4(x2341,a20))), % 59.46/59.50 inference(scs_inference,[],[233,2])). % 59.46/59.50 cnf(235,plain, % 59.46/59.50 (E(f4(f13(a16),a20),f4(a20,f13(a16)))), % 59.46/59.50 inference(scs_inference,[],[232,233,2,3])). % 59.46/59.50 cnf(238,plain, % 59.46/59.50 (E(f8(a20),f8(f13(a16)))), % 59.46/59.50 inference(scs_inference,[],[37,2,8])). % 59.46/59.50 cnf(239,plain, % 59.46/59.50 (E(f4(a20,f13(a16)),f4(f13(a16),a20))), % 59.46/59.50 inference(scs_inference,[],[235,2])). % 59.46/59.50 cnf(240,plain, % 59.46/59.50 (E(f4(f13(a16),f13(a16)),f4(a20,a20))), % 59.46/59.50 inference(scs_inference,[],[234,235,232,2,3])). % 59.46/59.50 cnf(243,plain, % 59.46/59.50 (E(f12(a20,x2431),f12(f13(a16),x2431))), % 59.46/59.50 inference(scs_inference,[],[37,2,9])). % 59.46/59.50 cnf(244,plain, % 59.46/59.50 (E(f4(a20,a20),f4(f13(a16),f13(a16)))), % 59.46/59.50 inference(scs_inference,[],[240,2])). % 59.46/59.50 cnf(245,plain, % 59.46/59.50 (E(x2451,f12(f13(a16),x2452))+~E(x2451,f12(a20,x2452))), % 59.46/59.50 inference(scs_inference,[],[240,243,2,3])). % 59.46/59.50 cnf(262,plain, % 59.46/59.50 (E(f4(f13(f4(a20,x2621)),x2622),f4(f13(f4(f13(a16),x2621)),x2622))), % 59.46/59.50 inference(scs_inference,[],[58,2,6])). % 59.46/59.50 cnf(263,plain, % 59.46/59.50 (E(f4(f13(f4(f13(a16),x2631)),x2632),f4(f13(f4(a20,x2631)),x2632))), % 59.46/59.50 inference(scs_inference,[],[262,2])). % 59.46/59.50 cnf(267,plain, % 59.46/59.50 (E(f4(x2671,f13(f4(a20,x2672))),f4(x2671,f13(f4(f13(a16),x2672))))), % 59.46/59.50 inference(scs_inference,[],[58,2,7])). % 59.46/59.50 cnf(268,plain, % 59.46/59.50 (E(f4(x2681,f13(f4(f13(a16),x2682))),f4(x2681,f13(f4(a20,x2682))))), % 59.46/59.50 inference(scs_inference,[],[267,2])). % 59.46/59.50 cnf(269,plain, % 59.46/59.50 (E(f4(f13(f4(f13(a16),x2691)),f13(f4(a20,x2692))),f4(f13(f4(a20,x2691)),f13(f4(f13(a16),x2692))))), % 59.46/59.50 inference(scs_inference,[],[263,267,2,3])). % 59.46/59.50 cnf(274,plain, % 59.46/59.50 (E(f4(f13(f4(f13(a16),x2741)),f13(f4(f13(a16),x2742))),f4(f13(f4(a20,x2741)),f13(f4(a20,x2742))))), % 59.46/59.50 inference(scs_inference,[],[268,269,263,2,3])). % 59.46/59.50 cnf(305,plain, % 59.46/59.50 (E(f5(x3051,f13(f4(a20,x3052))),f5(x3051,f13(f4(f13(a16),x3052))))), % 59.46/59.50 inference(scs_inference,[],[58,2,14])). % 59.46/59.50 cnf(306,plain, % 59.46/59.50 (E(f5(x3061,f13(f4(f13(a16),x3062))),f5(x3061,f13(f4(a20,x3062))))), % 59.46/59.50 inference(scs_inference,[],[305,2])). % 59.46/59.50 cnf(312,plain, % 59.46/59.50 (E(f5(f5(x3121,a20),f13(f4(f13(a16),x3122))),f5(f5(x3121,f13(a16)),f13(f4(a20,x3122))))), % 59.46/59.50 inference(scs_inference,[],[306,109,274,2,3])). % 59.46/59.50 cnf(430,plain, % 59.46/59.50 (E(f5(f5(x4301,f13(a16)),f13(f4(a20,x4302))),f5(f5(x4301,a20),f13(f4(f13(a16),x4302))))), % 59.46/59.50 inference(scs_inference,[],[312,2])). % 59.46/59.50 cnf(541,plain, % 59.46/59.50 (E(f14(a20),f14(f13(a16)))), % 59.46/59.50 inference(scs_inference,[],[37,2,15])). % 59.46/59.50 cnf(556,plain, % 59.46/59.50 (E(f10(a20),f10(f13(a16)))), % 59.46/59.50 inference(scs_inference,[],[37,2,19])). % 59.46/59.50 cnf(562,plain, % 59.46/59.50 (E(f14(f13(a16)),f14(a20))), % 59.46/59.50 inference(scs_inference,[],[541,2])). % 59.46/59.50 cnf(567,plain, % 59.46/59.50 (E(f10(f13(a16)),f10(a20))), % 59.46/59.50 inference(scs_inference,[],[556,2])). % 59.46/59.50 cnf(678,plain, % 59.46/59.50 (E(f7(f9(f9(x6781,a20),x6782)),f7(f9(f9(x6781,f13(a16)),x6782)))), % 59.46/59.50 inference(scs_inference,[],[94,2,4])). % 59.46/59.50 cnf(679,plain, % 59.46/59.50 (E(f7(f9(f9(x6791,f13(a16)),x6792)),f7(f9(f9(x6791,a20),x6792)))), % 59.46/59.50 inference(scs_inference,[],[678,2])). % 59.46/59.50 cnf(690,plain, % 59.46/59.50 (E(f4(x6901,f9(f9(x6902,a20),x6903)),f4(x6901,f9(f9(x6902,f13(a16)),x6903)))), % 59.46/59.50 inference(scs_inference,[],[94,2,7])). % 59.46/59.50 cnf(691,plain, % 59.46/59.50 (E(f4(x6911,f9(f9(x6912,f13(a16)),x6913)),f4(x6911,f9(f9(x6912,a20),x6913)))), % 59.46/59.50 inference(scs_inference,[],[690,2])). % 59.46/59.50 cnf(705,plain, % 59.46/59.50 (E(f12(x7051,f9(f9(x7052,a20),x7053)),f12(x7051,f9(f9(x7052,f13(a16)),x7053)))), % 59.46/59.50 inference(scs_inference,[],[94,2,10])). % 59.46/59.50 cnf(707,plain, % 59.46/59.50 (E(f12(x7071,f9(f9(x7072,a20),x7073)),f12(x7071,f9(f9(x7072,f13(a16)),x7073)))), % 59.46/59.50 inference(rename_variables,[],[705])). % 59.46/59.50 cnf(708,plain, % 59.46/59.50 (E(f12(x7081,f9(f9(x7082,f13(a16)),x7083)),f12(x7081,f9(f9(x7082,a20),x7083)))), % 59.46/59.50 inference(scs_inference,[],[705,707,245,2])). % 59.46/59.50 cnf(724,plain, % 59.46/59.50 (E(f5(f9(f9(x7241,a20),x7242),x7243),f5(f9(f9(x7241,f13(a16)),x7242),x7243))), % 59.46/59.50 inference(scs_inference,[],[94,2,13])). % 59.46/59.50 cnf(729,plain, % 59.46/59.50 (E(f5(x7291,f9(f9(x7292,a20),x7293)),f5(x7291,f9(f9(x7292,f13(a16)),x7293)))), % 59.46/59.50 inference(scs_inference,[],[94,2,14])). % 59.46/59.50 cnf(730,plain, % 59.46/59.50 (E(f5(x7301,f9(f9(x7302,f13(a16)),x7303)),f5(x7301,f9(f9(x7302,a20),x7303)))), % 59.46/59.50 inference(scs_inference,[],[729,2])). % 59.46/59.50 cnf(739,plain, % 59.46/59.50 (E(f2(f9(f9(x7391,a20),x7392),x7393,x7394),f2(f9(f9(x7391,f13(a16)),x7392),x7393,x7394))), % 59.46/59.50 inference(scs_inference,[],[94,2,16])). % 59.46/59.50 cnf(740,plain, % 59.46/59.50 (E(f2(f9(f9(x7401,f13(a16)),x7402),x7403,x7404),f2(f9(f9(x7401,a20),x7402),x7403,x7404))), % 59.46/59.50 inference(scs_inference,[],[739,2])). % 59.46/59.50 cnf(744,plain, % 59.46/59.50 (E(f2(x7441,f9(f9(x7442,a20),x7443),x7444),f2(x7441,f9(f9(x7442,f13(a16)),x7443),x7444))), % 59.46/59.50 inference(scs_inference,[],[94,2,17])). % 59.46/59.50 cnf(745,plain, % 59.46/59.50 (E(f2(x7451,f9(f9(x7452,f13(a16)),x7453),x7454),f2(x7451,f9(f9(x7452,a20),x7453),x7454))), % 59.46/59.50 inference(scs_inference,[],[744,2])). % 59.46/59.50 cnf(749,plain, % 59.46/59.50 (E(f2(x7491,x7492,f9(f9(x7493,a20),x7494)),f2(x7491,x7492,f9(f9(x7493,f13(a16)),x7494)))), % 59.46/59.50 inference(scs_inference,[],[94,2,18])). % 59.46/59.50 cnf(750,plain, % 59.46/59.50 (E(f2(x7501,x7502,f9(f9(x7503,f13(a16)),x7504)),f2(x7501,x7502,f9(f9(x7503,a20),x7504)))), % 59.46/59.50 inference(scs_inference,[],[749,2])). % 59.46/59.50 cnf(751,plain, % 59.46/59.50 (E(f2(x7511,f9(f9(x7512,f13(a16)),x7513),f9(f9(x7514,a20),x7515)),f2(x7511,f9(f9(x7512,a20),x7513),f9(f9(x7514,f13(a16)),x7515)))), % 59.46/59.50 inference(scs_inference,[],[745,749,2,3])). % 59.46/59.50 cnf(760,plain, % 59.46/59.50 (E(f2(x7601,f9(f9(x7602,a20),x7603),f9(f9(x7604,f13(a16)),x7605)),f2(x7601,f9(f9(x7602,f13(a16)),x7603),f9(f9(x7604,a20),x7605)))), % 59.46/59.50 inference(scs_inference,[],[751,2])). % 59.46/59.50 cnf(954,plain, % 59.46/59.50 (E(f4(f5(f5(x9541,f13(a16)),x9542),x9543),f4(f5(f5(x9541,a20),x9542),x9543))), % 59.46/59.50 inference(scs_inference,[],[109,2,6])). % 59.46/59.50 cnf(955,plain, % 59.46/59.50 (E(f4(f5(f5(x9551,a20),x9552),x9553),f4(f5(f5(x9551,f13(a16)),x9552),x9553))), % 59.46/59.50 inference(scs_inference,[],[954,2])). % 59.46/59.50 cnf(956,plain, % 59.46/59.50 (E(f4(f5(f5(x9561,f13(a16)),x9562),f9(f9(x9563,f13(a16)),x9564)),f4(f5(f5(x9561,a20),x9562),f9(f9(x9563,a20),x9564)))), % 59.46/59.50 inference(scs_inference,[],[954,691,2,3])). % 59.46/59.50 cnf(959,plain, % 59.46/59.50 (E(f4(x9591,f5(f5(x9592,f13(a16)),x9593)),f4(x9591,f5(f5(x9592,a20),x9593)))), % 59.46/59.50 inference(scs_inference,[],[109,2,7])). % 59.46/59.50 cnf(960,plain, % 59.46/59.50 (E(f4(x9601,f5(f5(x9602,a20),x9603)),f4(x9601,f5(f5(x9602,f13(a16)),x9603)))), % 59.46/59.50 inference(scs_inference,[],[959,2])). % 59.46/59.50 cnf(961,plain, % 59.46/59.50 (E(f4(f5(f5(x9611,a20),x9612),f5(f5(x9613,f13(a16)),x9614)),f4(f5(f5(x9611,f13(a16)),x9612),f5(f5(x9613,a20),x9614)))), % 59.46/59.50 inference(scs_inference,[],[959,955,2,3])). % 59.46/59.50 cnf(966,plain, % 59.46/59.50 (E(f4(f5(f5(x9661,a20),x9662),f5(f5(x9663,a20),x9664)),f4(f5(f5(x9661,f13(a16)),x9662),f5(f5(x9663,f13(a16)),x9664)))), % 59.46/59.50 inference(scs_inference,[],[960,956,955,2,3])). % 59.46/59.50 cnf(969,plain, % 59.46/59.50 (E(f12(f5(f5(x9691,f13(a16)),x9692),x9693),f12(f5(f5(x9691,a20),x9692),x9693))), % 59.46/59.50 inference(scs_inference,[],[109,2,9])). % 59.46/59.50 cnf(971,plain, % 59.46/59.50 (E(f12(f5(f5(x9711,f13(a16)),x9712),f9(f9(x9713,a20),x9714)),f12(f5(f5(x9711,a20),x9712),f9(f9(x9713,f13(a16)),x9714)))), % 59.46/59.50 inference(scs_inference,[],[969,705,2,3])). % 59.46/59.50 cnf(974,plain, % 59.46/59.50 (E(f12(x9741,f5(f5(x9742,f13(a16)),x9743)),f12(x9741,f5(f5(x9742,a20),x9743)))), % 59.46/59.50 inference(scs_inference,[],[109,2,10])). % 59.46/59.50 cnf(976,plain, % 59.46/59.50 (E(f12(x9761,f5(f5(x9762,f13(a16)),x9763)),f12(x9761,f5(f5(x9762,a20),x9763)))), % 59.46/59.50 inference(rename_variables,[],[974])). % 59.46/59.50 cnf(977,plain, % 59.46/59.50 (E(f12(x9771,f5(f5(x9772,a20),x9773)),f12(x9771,f5(f5(x9772,f13(a16)),x9773)))), % 59.46/59.50 inference(scs_inference,[],[974,976,245,2])). % 59.46/59.50 cnf(981,plain, % 59.46/59.50 (E(f9(f5(f5(x9811,f13(a16)),x9812),x9813),f9(f5(f5(x9811,a20),x9812),x9813))), % 59.46/59.50 inference(scs_inference,[],[109,2,11])). % 59.46/59.50 cnf(982,plain, % 59.46/59.50 (E(f12(a20,f5(f5(x9821,a20),x9822)),f12(f13(a16),f5(f5(x9821,f13(a16)),x9822)))), % 59.46/59.50 inference(scs_inference,[],[977,245])). % 59.46/59.50 cnf(984,plain, % 59.46/59.50 (E(f9(f5(f5(x9841,a20),x9842),x9843),f9(f5(f5(x9841,f13(a16)),x9842),x9843))), % 59.46/59.50 inference(scs_inference,[],[981,977,245,2])). % 59.46/59.50 cnf(988,plain, % 59.46/59.50 (E(f9(x9881,f5(f5(x9882,f13(a16)),x9883)),f9(x9881,f5(f5(x9882,a20),x9883)))), % 59.46/59.50 inference(scs_inference,[],[109,2,12])). % 59.46/59.50 cnf(989,plain, % 59.46/59.50 (E(f9(x9891,f5(f5(x9892,a20),x9893)),f9(x9891,f5(f5(x9892,f13(a16)),x9893)))), % 59.46/59.50 inference(scs_inference,[],[988,2])). % 59.46/59.50 cnf(993,plain, % 59.46/59.50 (E(f5(f5(f5(x9931,f13(a16)),x9932),x9933),f5(f5(f5(x9931,a20),x9932),x9933))), % 59.46/59.50 inference(scs_inference,[],[109,2,13])). % 59.46/59.50 cnf(994,plain, % 59.46/59.50 (E(f5(f5(f5(x9941,a20),x9942),x9943),f5(f5(f5(x9941,f13(a16)),x9942),x9943))), % 59.46/59.50 inference(scs_inference,[],[993,2])). % 59.46/59.50 cnf(995,plain, % 59.46/59.50 (E(f5(f5(f5(x9951,f13(a16)),a20),x9952),f5(f5(f5(x9951,a20),f13(a16)),x9952))), % 59.46/59.50 inference(scs_inference,[],[109,993,2,3])). % 59.46/59.50 cnf(998,plain, % 59.46/59.50 (E(f5(x9981,f5(f5(x9982,f13(a16)),x9983)),f5(x9981,f5(f5(x9982,a20),x9983)))), % 59.46/59.50 inference(scs_inference,[],[109,2,14])). % 59.46/59.50 cnf(999,plain, % 59.46/59.50 (E(f5(x9991,f5(f5(x9992,a20),x9993)),f5(x9991,f5(f5(x9992,f13(a16)),x9993)))), % 59.46/59.50 inference(scs_inference,[],[998,2])). % 59.46/59.50 cnf(1003,plain, % 59.46/59.50 (E(f14(f5(f5(x10031,f13(a16)),x10032)),f14(f5(f5(x10031,a20),x10032)))), % 59.46/59.50 inference(scs_inference,[],[109,2,15])). % 59.46/59.50 cnf(1005,plain, % 59.46/59.50 (E(f5(f5(f5(x10051,a20),a20),x10052),f5(f5(f5(x10051,f13(a16)),f13(a16)),x10052))), % 59.46/59.50 inference(scs_inference,[],[109,994,961,2,3])). % 59.46/59.50 cnf(1008,plain, % 59.46/59.50 (E(f2(f5(f5(x10081,f13(a16)),x10082),x10083,x10084),f2(f5(f5(x10081,a20),x10082),x10083,x10084))), % 59.46/59.50 inference(scs_inference,[],[109,2,16])). % 59.46/59.50 cnf(1009,plain, % 59.46/59.50 (E(f2(f5(f5(x10091,a20),x10092),x10093,x10094),f2(f5(f5(x10091,f13(a16)),x10092),x10093,x10094))), % 59.46/59.50 inference(scs_inference,[],[1008,2])). % 59.46/59.50 cnf(1010,plain, % 59.46/59.50 (E(f5(f5(x10101,a20),f5(f5(x10102,a20),x10103)),f5(f5(x10101,f13(a16)),f5(f5(x10102,f13(a16)),x10103)))), % 59.46/59.50 inference(scs_inference,[],[109,1008,999,2,3])). % 59.46/59.50 cnf(1013,plain, % 59.46/59.50 (E(f2(x10131,f5(f5(x10132,f13(a16)),x10133),x10134),f2(x10131,f5(f5(x10132,a20),x10133),x10134))), % 59.46/59.50 inference(scs_inference,[],[109,2,17])). % 59.46/59.50 cnf(1014,plain, % 59.46/59.50 (E(f2(x10141,f5(f5(x10142,a20),x10143),x10144),f2(x10141,f5(f5(x10142,f13(a16)),x10143),x10144))), % 59.46/59.50 inference(scs_inference,[],[1013,2])). % 59.46/59.50 cnf(1015,plain, % 59.46/59.50 (E(f2(f5(f5(x10151,a20),x10152),f5(f5(x10153,f13(a16)),x10154),x10155),f2(f5(f5(x10151,f13(a16)),x10152),f5(f5(x10153,a20),x10154),x10155))), % 59.46/59.50 inference(scs_inference,[],[1013,1009,2,3])). % 59.46/59.51 cnf(1018,plain, % 59.46/59.51 (E(f2(x10181,x10182,f5(f5(x10183,f13(a16)),x10184)),f2(x10181,x10182,f5(f5(x10183,a20),x10184)))), % 59.46/59.51 inference(scs_inference,[],[109,2,18])). % 59.46/59.51 cnf(1019,plain, % 59.46/59.51 (E(f2(x10191,x10192,f5(f5(x10193,a20),x10194)),f2(x10191,x10192,f5(f5(x10193,f13(a16)),x10194)))), % 59.46/59.51 inference(scs_inference,[],[1018,2])). % 59.46/59.51 cnf(1024,plain, % 59.46/59.51 (E(f2(f5(f5(x10241,f13(a16)),x10242),f5(f5(x10243,a20),x10244),x10245),f2(f5(f5(x10241,a20),x10242),f5(f5(x10243,f13(a16)),x10244),x10245))), % 59.46/59.51 inference(scs_inference,[],[1015,2])). % 59.46/59.51 cnf(1054,plain, % 59.46/59.51 (E(f9(f5(f5(x10541,a20),x10542),f5(f5(x10543,a20),x10544)),f9(f5(f5(x10541,f13(a16)),x10542),f5(f5(x10543,f13(a16)),x10544)))), % 59.46/59.51 inference(scs_inference,[],[989,1003,984,2,3])). % 59.46/59.51 cnf(1063,plain, % 59.46/59.51 (E(f5(f5(f5(x10631,f13(a16)),a20),f5(f5(x10632,a20),x10633)),f5(f5(f5(x10631,a20),f13(a16)),f5(f5(x10632,f13(a16)),x10633)))), % 59.46/59.51 inference(scs_inference,[],[966,1010,993,2,3])). % 59.46/59.51 cnf(1068,plain, % 59.46/59.51 (E(f2(f5(f5(x10681,f13(a16)),x10682),x10683,f5(f5(x10684,a20),x10685)),f2(f5(f5(x10681,a20),x10682),x10683,f5(f5(x10684,f13(a16)),x10685)))), % 59.46/59.51 inference(scs_inference,[],[971,1008,1019,2,3])). % 59.46/59.51 cnf(1072,plain, % 59.46/59.51 (E(f2(f5(f5(x10721,a20),x10722),x10723,f5(f5(x10724,f13(a16)),x10725)),f2(f5(f5(x10721,f13(a16)),x10722),x10723,f5(f5(x10724,a20),x10725)))), % 59.46/59.51 inference(scs_inference,[],[1068,2])). % 59.46/59.51 cnf(1073,plain, % 59.46/59.51 (E(f5(f9(f9(x10731,a20),x10732),f5(f5(x10733,a20),x10734)),f5(f9(f9(x10731,f13(a16)),x10732),f5(f5(x10733,f13(a16)),x10734)))), % 59.46/59.51 inference(scs_inference,[],[1068,724,999,2,3])). % 59.46/59.51 cnf(1078,plain, % 59.46/59.51 (E(f2(f5(f5(x10781,a20),x10782),f5(f5(x10783,a20),x10784),x10785),f2(f5(f5(x10781,f13(a16)),x10782),f5(f5(x10783,f13(a16)),x10784),x10785))), % 59.46/59.51 inference(scs_inference,[],[1054,1009,1014,2,3])). % 59.46/59.51 cnf(1082,plain, % 59.46/59.51 (E(f2(f5(f5(x10821,f13(a16)),x10822),f5(f5(x10823,f13(a16)),x10824),x10825),f2(f5(f5(x10821,a20),x10822),f5(f5(x10823,a20),x10824),x10825))), % 59.46/59.51 inference(scs_inference,[],[1078,2])). % 59.46/59.51 cnf(1083,plain, % 59.46/59.51 (E(f5(f5(f5(x10831,f13(a16)),f13(a16)),f13(f4(a20,x10832))),f5(f5(f5(x10831,a20),f13(a16)),f13(f4(f13(a16),x10832))))), % 59.46/59.51 inference(scs_inference,[],[1078,430,995,2,3])). % 59.46/59.51 cnf(1088,plain, % 59.46/59.51 (E(f2(f5(f5(x10881,a20),x10882),f5(f5(x10883,f13(a16)),x10884),f5(f5(x10885,f13(a16)),x10886)),f2(f5(f5(x10881,a20),x10882),f5(f5(x10883,a20),x10884),f5(f5(x10885,a20),x10886)))), % 59.46/59.51 inference(scs_inference,[],[1072,1082,1073,2,3])). % 59.46/59.51 cnf(1093,plain, % 59.46/59.51 (E(f2(f5(f5(x10931,f13(a16)),x10932),f5(f5(x10933,a20),x10934),f5(f5(x10935,f13(a16)),x10936)),f2(f5(f5(x10931,a20),x10932),f5(f5(x10933,a20),x10934),f5(f5(x10935,a20),x10936)))), % 59.46/59.51 inference(scs_inference,[],[1088,1024,2,3])). % 59.46/59.51 cnf(1098,plain, % 59.46/59.51 (E(f5(f5(f5(x10981,f13(a16)),a20),f13(f4(a20,x10982))),f5(f5(f5(x10981,a20),f13(a16)),f13(f4(f13(a16),x10982))))), % 59.46/59.51 inference(scs_inference,[],[109,1093,1083,2,3])). % 59.46/59.51 cnf(1118,plain, % 59.46/59.51 (E(f5(f5(f5(x11181,a20),f13(a16)),f5(f5(x11182,f13(a16)),x11183)),f5(f5(f5(x11181,f13(a16)),a20),f5(f5(x11182,a20),x11183)))), % 59.46/59.51 inference(scs_inference,[],[1063,2])). % 59.46/59.51 cnf(1121,plain, % 59.46/59.51 (E(f5(f5(f5(x11211,a20),f13(a16)),f13(f4(f13(a16),x11212))),f5(f5(f5(x11211,f13(a16)),a20),f13(f4(a20,x11212))))), % 59.46/59.51 inference(scs_inference,[],[1098,2])). % 59.46/59.51 cnf(1122,plain, % 59.46/59.51 (E(f5(f5(f5(x11221,a20),a20),f5(f5(x11222,f13(a16)),x11223)),f5(f5(f5(x11221,f13(a16)),a20),f5(f5(x11222,a20),x11223)))), % 59.46/59.51 inference(scs_inference,[],[109,1118,1098,2,3])). % 59.46/59.51 cnf(1126,plain, % 59.46/59.51 (E(f5(f5(f5(x11261,a20),f13(a16)),f13(f4(f13(a16),x11262))),f5(f5(f5(x11261,f13(a16)),f13(a16)),f13(f4(a20,x11262))))), % 59.46/59.51 inference(scs_inference,[],[109,1121,1122,2,3])). % 59.46/59.51 cnf(1130,plain, % 59.46/59.51 (E(f5(f5(f5(x11301,a20),a20),f13(f4(f13(a16),x11302))),f5(f5(f5(x11301,f13(a16)),f13(a16)),f13(f4(a20,x11302))))), % 59.46/59.51 inference(scs_inference,[],[109,1126,982,2,3])). % 59.46/59.51 cnf(1134,plain, % 59.46/59.51 (E(f5(f5(f5(x11341,a20),a20),f13(f4(f13(a16),x11342))),f5(f5(f5(x11341,f13(a16)),a20),f13(f4(a20,x11342))))), % 59.46/59.51 inference(scs_inference,[],[109,1130,1121,2,3])). % 59.46/59.51 cnf(1138,plain, % 59.46/59.51 (E(f2(f9(f9(x11381,a20),x11382),x11383,f5(f5(x11384,a20),x11385)),f2(f9(f9(x11381,f13(a16)),x11382),x11383,f5(f5(x11384,f13(a16)),x11385)))), % 59.46/59.51 inference(scs_inference,[],[1134,739,1019,2,3])). % 59.46/59.51 cnf(1142,plain, % 59.46/59.51 (E(f2(f9(f9(x11421,f13(a16)),x11422),x11423,f5(f5(x11424,f13(a16)),x11425)),f2(f9(f9(x11421,a20),x11422),x11423,f5(f5(x11424,a20),x11425)))), % 59.46/59.51 inference(scs_inference,[],[1138,2])). % 59.46/59.51 cnf(1268,plain, % 59.46/59.51 (E(f5(f5(f5(x12681,f13(a16)),f13(a16)),x12682),f5(f5(f5(x12681,a20),a20),x12682))), % 59.46/59.51 inference(scs_inference,[],[1005,2])). % 59.46/59.51 cnf(1274,plain, % 59.46/59.51 (E(f2(f2(x12741,a20,x12742),f9(f9(x12743,f13(a16)),x12744),f9(f9(x12745,a20),x12746)),f2(f2(x12741,f13(a16),x12742),f9(f9(x12743,a20),x12744),f9(f9(x12745,f13(a16)),x12746)))), % 59.46/59.51 inference(scs_inference,[],[110,760,3,2])). % 59.46/59.51 cnf(1286,plain, % 59.46/59.51 (E(f2(f2(x12861,f13(a16),x12862),f9(f9(x12863,f13(a16)),x12864),x12865),f2(f2(x12861,a20,x12862),f9(f9(x12863,a20),x12864),x12865))), % 59.46/59.51 inference(scs_inference,[],[110,745,3])). % 59.46/59.51 cnf(1289,plain, % 59.46/59.51 (E(f2(f2(x12891,a20,x12892),f9(f9(x12893,a20),x12894),x12895),f2(f2(x12891,f13(a16),x12892),f9(f9(x12893,f13(a16)),x12894),x12895))), % 59.46/59.51 inference(scs_inference,[],[110,745,3,2])). % 59.46/59.51 cnf(1291,plain, % 59.46/59.51 (E(f2(f2(x12911,f13(a16),x12912),x12913,f9(f9(x12914,f13(a16)),x12915)),f2(f2(x12911,a20,x12912),x12913,f9(f9(x12914,a20),x12915)))), % 59.46/59.51 inference(scs_inference,[],[110,750,3])). % 59.46/59.51 cnf(1294,plain, % 59.46/59.51 (E(f2(f2(x12941,a20,x12942),x12943,f9(f9(x12944,a20),x12945)),f2(f2(x12941,f13(a16),x12942),x12943,f9(f9(x12944,f13(a16)),x12945)))), % 59.46/59.51 inference(scs_inference,[],[110,750,3,2])). % 59.46/59.51 cnf(1296,plain, % 59.46/59.51 (E(f2(f2(x12961,f13(a16),x12962),f5(f5(x12963,f13(a16)),x12964),x12965),f2(f2(x12961,a20,x12962),f5(f5(x12963,a20),x12964),x12965))), % 59.46/59.51 inference(scs_inference,[],[110,1013,3])). % 59.46/59.51 cnf(1299,plain, % 59.46/59.51 (E(f2(f2(x12991,a20,x12992),f5(f5(x12993,a20),x12994),x12995),f2(f2(x12991,f13(a16),x12992),f5(f5(x12993,f13(a16)),x12994),x12995))), % 59.46/59.51 inference(scs_inference,[],[110,1013,3,2])). % 59.46/59.51 cnf(1300,plain, % 59.46/59.51 (E(f2(f2(x13001,a20,x13002),f5(f5(x13003,f13(a16)),x13004),f9(f9(x13005,a20),x13006)),f2(f2(x13001,a20,x13002),f5(f5(x13003,a20),x13004),f9(f9(x13005,f13(a16)),x13006)))), % 59.46/59.51 inference(scs_inference,[],[1296,1294,3])). % 59.46/59.51 cnf(1303,plain, % 59.46/59.51 (E(f2(f2(x13031,a20,x13032),f5(f5(x13033,a20),x13034),f9(f9(x13035,f13(a16)),x13036)),f2(f2(x13031,a20,x13032),f5(f5(x13033,f13(a16)),x13034),f9(f9(x13035,a20),x13036)))), % 59.46/59.51 inference(scs_inference,[],[1296,1294,3,2])). % 59.46/59.51 cnf(1304,plain, % 59.46/59.51 (E(f7(f2(f2(x13041,a20,x13042),x13043,x13044)),f7(f2(f2(x13041,f13(a16),x13042),x13043,x13044)))), % 59.46/59.51 inference(scs_inference,[],[110,2,4])). % 59.46/59.51 cnf(1305,plain, % 59.46/59.51 (E(f7(f2(f2(x13051,f13(a16),x13052),x13053,x13054)),f7(f2(f2(x13051,a20,x13052),x13053,x13054)))), % 59.46/59.51 inference(scs_inference,[],[1304,2])). % 59.46/59.51 cnf(1306,plain, % 59.46/59.51 (E(f2(f2(x13061,f13(a16),x13062),f5(f5(x13063,a20),x13064),f9(f9(x13065,f13(a16)),x13066)),f2(f2(x13061,a20,x13062),f5(f5(x13063,f13(a16)),x13064),f9(f9(x13065,a20),x13066)))), % 59.46/59.51 inference(scs_inference,[],[110,1304,1303,2,3])). % 59.46/59.51 cnf(1309,plain, % 59.46/59.51 (E(f13(f2(f2(x13091,a20,x13092),x13093,x13094)),f13(f2(f2(x13091,f13(a16),x13092),x13093,x13094)))), % 59.46/59.51 inference(scs_inference,[],[110,2,5])). % 59.46/59.51 cnf(1311,plain, % 59.46/59.51 (E(f2(f2(x13111,f13(a16),x13112),f5(f5(x13113,f13(a16)),x13114),f9(f9(x13115,a20),x13116)),f2(f2(x13111,a20,x13112),f5(f5(x13113,a20),x13114),f9(f9(x13115,f13(a16)),x13116)))), % 59.46/59.51 inference(scs_inference,[],[110,1309,1300,2,3])). % 59.46/59.51 cnf(1314,plain, % 59.46/59.51 (E(f4(f2(f2(x13141,a20,x13142),x13143,x13144),x13145),f4(f2(f2(x13141,f13(a16),x13142),x13143,x13144),x13145))), % 59.46/59.51 inference(scs_inference,[],[110,2,6])). % 59.46/59.51 cnf(1315,plain, % 59.46/59.51 (E(f4(f2(f2(x13151,f13(a16),x13152),x13153,x13154),x13155),f4(f2(f2(x13151,a20,x13152),x13153,x13154),x13155))), % 59.46/59.51 inference(scs_inference,[],[1314,2])). % 59.46/59.51 cnf(1316,plain, % 59.46/59.51 (E(f4(f2(f2(x13161,a20,x13162),x13163,x13164),f5(f5(x13165,a20),x13166)),f4(f2(f2(x13161,f13(a16),x13162),x13163,x13164),f5(f5(x13165,f13(a16)),x13166)))), % 59.46/59.51 inference(scs_inference,[],[1314,960,2,3])). % 59.46/59.51 cnf(1319,plain, % 59.46/59.51 (E(f4(x13191,f2(f2(x13192,a20,x13193),x13194,x13195)),f4(x13191,f2(f2(x13192,f13(a16),x13193),x13194,x13195)))), % 59.46/59.51 inference(scs_inference,[],[110,2,7])). % 59.46/59.51 cnf(1320,plain, % 59.46/59.51 (E(f4(x13201,f2(f2(x13202,f13(a16),x13203),x13204,x13205)),f4(x13201,f2(f2(x13202,a20,x13203),x13204,x13205)))), % 59.46/59.51 inference(scs_inference,[],[1319,2])). % 59.46/59.51 cnf(1321,plain, % 59.46/59.51 (E(f4(f2(f2(x13211,f13(a16),x13212),x13213,x13214),f2(f2(x13215,a20,x13216),x13217,x13218)),f4(f2(f2(x13211,a20,x13212),x13213,x13214),f2(f2(x13215,f13(a16),x13216),x13217,x13218)))), % 59.46/59.51 inference(scs_inference,[],[1315,1319,2,3])). % 59.46/59.51 cnf(1324,plain, % 59.46/59.51 (E(f8(f2(f2(x13241,a20,x13242),x13243,x13244)),f8(f2(f2(x13241,f13(a16),x13242),x13243,x13244)))), % 59.46/59.51 inference(scs_inference,[],[110,2,8])). % 59.46/59.51 cnf(1326,plain, % 59.46/59.51 (E(f4(f2(f2(x13261,f13(a16),x13262),x13263,x13264),f2(f2(x13265,f13(a16),x13266),x13267,x13268)),f4(f2(f2(x13261,a20,x13262),x13263,x13264),f2(f2(x13265,a20,x13266),x13267,x13268)))), % 59.46/59.51 inference(scs_inference,[],[1320,1321,1315,2,3])). % 59.46/59.51 cnf(1329,plain, % 59.46/59.51 (E(f12(f2(f2(x13291,a20,x13292),x13293,x13294),x13295),f12(f2(f2(x13291,f13(a16),x13292),x13293,x13294),x13295))), % 59.46/59.51 inference(scs_inference,[],[110,2,9])). % 59.46/59.51 cnf(1330,plain, % 59.46/59.51 (E(f12(f2(f2(x13301,f13(a16),x13302),x13303,x13304),x13305),f12(f2(f2(x13301,a20,x13302),x13303,x13304),x13305))), % 59.46/59.51 inference(scs_inference,[],[1329,2])). % 59.46/59.51 cnf(1331,plain, % 59.46/59.51 (E(f12(f2(f2(x13311,a20,x13312),x13313,x13314),f9(f9(x13315,f13(a16)),x13316)),f12(f2(f2(x13311,f13(a16),x13312),x13313,x13314),f9(f9(x13315,a20),x13316)))), % 59.46/59.51 inference(scs_inference,[],[1329,708,2,3])). % 59.46/59.51 cnf(1334,plain, % 59.46/59.51 (E(f12(x13341,f2(f2(x13342,a20,x13343),x13344,x13345)),f12(x13341,f2(f2(x13342,f13(a16),x13343),x13344,x13345)))), % 59.46/59.51 inference(scs_inference,[],[110,2,10])). % 59.46/59.51 cnf(1336,plain, % 59.46/59.51 (E(f12(x13361,f2(f2(x13362,a20,x13363),x13364,x13365)),f12(x13361,f2(f2(x13362,f13(a16),x13363),x13364,x13365)))), % 59.46/59.51 inference(rename_variables,[],[1334])). % 59.46/59.51 cnf(1337,plain, % 59.46/59.51 (E(f12(x13371,f2(f2(x13372,f13(a16),x13373),x13374,x13375)),f12(x13371,f2(f2(x13372,a20,x13373),x13374,x13375)))), % 59.46/59.51 inference(scs_inference,[],[1334,1336,245,2])). % 59.46/59.51 cnf(1338,plain, % 59.46/59.51 (E(f12(f2(f2(x13381,f13(a16),x13382),x13383,x13384),f2(f2(x13385,a20,x13386),x13387,x13388)),f12(f2(f2(x13381,a20,x13382),x13383,x13384),f2(f2(x13385,f13(a16),x13386),x13387,x13388)))), % 59.46/59.51 inference(scs_inference,[],[1330,1334,1336,245,2,3])). % 59.46/59.51 cnf(1341,plain, % 59.46/59.51 (E(f9(f2(f2(x13411,a20,x13412),x13413,x13414),x13415),f9(f2(f2(x13411,f13(a16),x13412),x13413,x13414),x13415))), % 59.46/59.51 inference(scs_inference,[],[110,2,11])). % 59.46/59.51 cnf(1344,plain, % 59.46/59.51 (E(f9(f2(f2(x13441,f13(a16),x13442),x13443,x13444),x13445),f9(f2(f2(x13441,a20,x13442),x13443,x13444),x13445))), % 59.46/59.51 inference(scs_inference,[],[1337,1341,245,2])). % 59.46/59.51 cnf(1345,plain, % 59.46/59.51 (E(f9(f2(f2(x13451,a20,x13452),x13453,x13454),f5(f5(x13455,f13(a16)),x13456)),f9(f2(f2(x13451,f13(a16),x13452),x13453,x13454),f5(f5(x13455,a20),x13456)))), % 59.46/59.51 inference(scs_inference,[],[1337,1341,988,245,2,3])). % 59.46/59.51 cnf(1348,plain, % 59.46/59.51 (E(f9(x13481,f2(f2(x13482,a20,x13483),x13484,x13485)),f9(x13481,f2(f2(x13482,f13(a16),x13483),x13484,x13485)))), % 59.46/59.51 inference(scs_inference,[],[110,2,12])). % 59.46/59.51 cnf(1349,plain, % 59.46/59.51 (E(f9(x13491,f2(f2(x13492,f13(a16),x13493),x13494,x13495)),f9(x13491,f2(f2(x13492,a20,x13493),x13494,x13495)))), % 59.46/59.51 inference(scs_inference,[],[1348,2])). % 59.46/59.51 cnf(1350,plain, % 59.46/59.51 (E(f9(f2(f2(x13501,f13(a16),x13502),x13503,x13504),f2(f2(x13505,a20,x13506),x13507,x13508)),f9(f2(f2(x13501,a20,x13502),x13503,x13504),f2(f2(x13505,f13(a16),x13506),x13507,x13508)))), % 59.46/59.51 inference(scs_inference,[],[1344,1348,2,3])). % 59.46/59.51 cnf(1353,plain, % 59.46/59.51 (E(f5(f2(f2(x13531,a20,x13532),x13533,x13534),x13535),f5(f2(f2(x13531,f13(a16),x13532),x13533,x13534),x13535))), % 59.46/59.51 inference(scs_inference,[],[110,2,13])). % 59.46/59.51 cnf(1354,plain, % 59.46/59.51 (E(f5(f2(f2(x13541,f13(a16),x13542),x13543,x13544),x13545),f5(f2(f2(x13541,a20,x13542),x13543,x13544),x13545))), % 59.46/59.51 inference(scs_inference,[],[1353,2])). % 59.46/59.51 cnf(1355,plain, % 59.46/59.51 (E(f5(f2(f2(x13551,a20,x13552),x13553,x13554),f9(f9(x13555,f13(a16)),x13556)),f5(f2(f2(x13551,f13(a16),x13552),x13553,x13554),f9(f9(x13555,a20),x13556)))), % 59.46/59.51 inference(scs_inference,[],[1353,730,2,3])). % 59.46/59.51 cnf(1358,plain, % 59.46/59.51 (E(f5(x13581,f2(f2(x13582,a20,x13583),x13584,x13585)),f5(x13581,f2(f2(x13582,f13(a16),x13583),x13584,x13585)))), % 59.46/59.51 inference(scs_inference,[],[110,2,14])). % 59.46/59.51 cnf(1359,plain, % 59.46/59.51 (E(f5(x13591,f2(f2(x13592,f13(a16),x13593),x13594,x13595)),f5(x13591,f2(f2(x13592,a20,x13593),x13594,x13595)))), % 59.46/59.51 inference(scs_inference,[],[1358,2])). % 59.46/59.51 cnf(1360,plain, % 59.46/59.51 (E(f5(f2(f2(x13601,f13(a16),x13602),x13603,x13604),f2(f2(x13605,a20,x13606),x13607,x13608)),f5(f2(f2(x13601,a20,x13602),x13603,x13604),f2(f2(x13605,f13(a16),x13606),x13607,x13608)))), % 59.46/59.51 inference(scs_inference,[],[1354,1358,2,3])). % 59.46/59.51 cnf(1363,plain, % 59.46/59.51 (E(f14(f2(f2(x13631,a20,x13632),x13633,x13634)),f14(f2(f2(x13631,f13(a16),x13632),x13633,x13634)))), % 59.46/59.51 inference(scs_inference,[],[110,2,15])). % 59.46/59.51 cnf(1365,plain, % 59.46/59.51 (E(f5(f5(f5(x13651,f13(a16)),f13(a16)),f2(f2(x13652,f13(a16),x13653),x13654,x13655)),f5(f5(f5(x13651,a20),a20),f2(f2(x13652,a20,x13653),x13654,x13655)))), % 59.46/59.51 inference(scs_inference,[],[1359,1326,1268,2,3])). % 59.46/59.51 cnf(1368,plain, % 59.46/59.51 (E(f2(f2(f2(x13681,a20,x13682),x13683,x13684),x13685,x13686),f2(f2(f2(x13681,f13(a16),x13682),x13683,x13684),x13685,x13686))), % 59.46/59.51 inference(scs_inference,[],[110,2,16])). % 59.46/59.51 cnf(1369,plain, % 59.46/59.51 (E(f2(f2(f2(x13691,f13(a16),x13692),x13693,x13694),x13695,x13696),f2(f2(f2(x13691,a20,x13692),x13693,x13694),x13695,x13696))), % 59.46/59.51 inference(scs_inference,[],[1368,2])). % 59.46/59.51 cnf(1370,plain, % 59.46/59.51 (E(f2(f2(f2(x13701,a20,x13702),f13(a16),x13703),x13704,x13705),f2(f2(f2(x13701,f13(a16),x13702),a20,x13703),x13704,x13705))), % 59.46/59.51 inference(scs_inference,[],[110,1368,2,3])). % 59.46/59.51 cnf(1373,plain, % 59.46/59.51 (E(f2(x13731,f2(f2(x13732,a20,x13733),x13734,x13735),x13736),f2(x13731,f2(f2(x13732,f13(a16),x13733),x13734,x13735),x13736))), % 59.46/59.51 inference(scs_inference,[],[110,2,17])). % 59.46/59.51 cnf(1374,plain, % 59.46/59.51 (E(f2(x13741,f2(f2(x13742,f13(a16),x13743),x13744,x13745),x13746),f2(x13741,f2(f2(x13742,a20,x13743),x13744,x13745),x13746))), % 59.46/59.51 inference(scs_inference,[],[1373,2])). % 59.46/59.51 cnf(1375,plain, % 59.46/59.51 (E(f2(f2(f2(x13751,f13(a16),x13752),f13(a16),x13753),x13754,x13755),f2(f2(f2(x13751,a20,x13752),a20,x13753),x13754,x13755))), % 59.46/59.51 inference(scs_inference,[],[110,1369,1373,2,3])). % 59.46/59.51 cnf(1378,plain, % 59.46/59.51 (E(f2(x13781,x13782,f2(f2(x13783,a20,x13784),x13785,x13786)),f2(x13781,x13782,f2(f2(x13783,f13(a16),x13784),x13785,x13786)))), % 59.46/59.51 inference(scs_inference,[],[110,2,18])). % 59.46/59.51 cnf(1379,plain, % 59.46/59.51 (E(f2(x13791,x13792,f2(f2(x13793,f13(a16),x13794),x13795,x13796)),f2(x13791,x13792,f2(f2(x13793,a20,x13794),x13795,x13796)))), % 59.46/59.51 inference(scs_inference,[],[1378,2])). % 59.46/59.51 cnf(1380,plain, % 59.46/59.51 (E(f2(f2(x13801,f13(a16),x13802),f2(f2(x13803,f13(a16),x13804),x13805,x13806),x13807),f2(f2(x13801,a20,x13802),f2(f2(x13803,a20,x13804),x13805,x13806),x13807))), % 59.46/59.51 inference(scs_inference,[],[110,1374,1378,2,3])). % 59.46/59.51 cnf(1383,plain, % 59.46/59.51 (E(f10(f2(f2(x13831,a20,x13832),x13833,x13834)),f10(f2(f2(x13831,f13(a16),x13832),x13833,x13834)))), % 59.46/59.51 inference(scs_inference,[],[110,2,19])). % 59.46/59.51 cnf(1385,plain, % 59.46/59.51 (E(f2(f2(x13851,f13(a16),x13852),x13853,f2(f2(x13854,f13(a16),x13855),x13856,x13857)),f2(f2(x13851,a20,x13852),x13853,f2(f2(x13854,a20,x13855),x13856,x13857)))), % 59.46/59.51 inference(scs_inference,[],[110,1379,1324,2,3])). % 59.46/59.51 cnf(1390,plain, % 59.46/59.51 (E(f2(f2(f2(x13901,f13(a16),x13902),a20,x13903),f9(f9(x13904,a20),x13905),x13906),f2(f2(f2(x13901,a20,x13902),a20,x13903),f9(f9(x13904,f13(a16)),x13905),x13906))), % 59.46/59.51 inference(scs_inference,[],[1338,1375,1289,2,3])). % 59.46/59.51 cnf(1395,plain, % 59.46/59.51 (E(f2(f2(f2(x13951,f13(a16),x13952),f13(a16),x13953),f2(f2(x13954,f13(a16),x13955),x13956,x13957),x13958),f2(f2(f2(x13951,a20,x13952),a20,x13953),f2(f2(x13954,a20,x13955),x13956,x13957),x13958))), % 59.46/59.51 inference(scs_inference,[],[1350,1380,1369,2,3])). % 59.46/59.51 cnf(1400,plain, % 59.46/59.51 (E(f9(f2(f2(x14001,f13(a16),x14002),x14003,x14004),f2(f2(x14005,f13(a16),x14006),x14007,x14008)),f9(f2(f2(x14001,a20,x14002),x14003,x14004),f2(f2(x14005,a20,x14006),x14007,x14008)))), % 59.46/59.51 inference(scs_inference,[],[1349,1360,1344,2,3])). % 59.46/59.51 cnf(1405,plain, % 59.46/59.51 (E(f2(f2(x14051,a20,x14052),f5(f5(x14053,a20),x14054),f2(f2(x14055,f13(a16),x14056),x14057,x14058)),f2(f2(x14051,a20,x14052),f5(f5(x14053,f13(a16)),x14054),f2(f2(x14055,a20,x14056),x14057,x14058)))), % 59.46/59.51 inference(scs_inference,[],[1400,1385,1299,2,3])). % 59.46/59.51 cnf(1410,plain, % 59.46/59.51 (E(f2(f2(f2(x14101,f13(a16),x14102),f13(a16),x14103),f2(f2(x14104,f13(a16),x14105),x14106,x14107),f2(f2(x14108,f13(a16),x14109),x141010,x141011)),f2(f2(f2(x14101,a20,x14102),a20,x14103),f2(f2(x14104,a20,x14105),x14106,x14107),f2(f2(x14108,a20,x14109),x141010,x141011)))), % 59.46/59.51 inference(scs_inference,[],[1363,1395,1379,2,3])). % 59.46/59.51 cnf(1415,plain, % 59.46/59.51 (E(f2(f2(x14151,f13(a16),x14152),f9(f9(x14153,f13(a16)),x14154),f2(f2(x14155,a20,x14156),x14157,x14158)),f2(f2(x14151,a20,x14152),f9(f9(x14153,a20),x14154),f2(f2(x14155,f13(a16),x14156),x14157,x14158)))), % 59.46/59.51 inference(scs_inference,[],[1383,1286,1378,2,3])). % 59.46/59.51 cnf(1419,plain, % 59.46/59.51 (E(f2(f2(x14191,f13(a16),x14192),f5(f5(x14193,a20),x14194),f2(f2(x14195,f13(a16),x14196),x14197,x14198)),f2(f2(x14191,a20,x14192),f5(f5(x14193,f13(a16)),x14194),f2(f2(x14195,a20,x14196),x14197,x14198)))), % 59.46/59.51 inference(scs_inference,[],[110,1331,1405,2,3])). % 59.46/59.51 cnf(1424,plain, % 59.46/59.51 (E(f2(f2(f2(x14241,f13(a16),x14242),f13(a16),x14243),f2(f2(x14244,a20,x14245),x14246,x14247),f2(f2(x14248,f13(a16),x14249),x142410,x142411)),f2(f2(f2(x14241,a20,x14242),a20,x14243),f2(f2(x14244,a20,x14245),x14246,x14247),f2(f2(x14248,a20,x14249),x142410,x142411)))), % 59.46/59.51 inference(scs_inference,[],[1345,1410,1373,2,3])). % 59.46/59.51 cnf(1429,plain, % 59.46/59.51 (E(f2(f2(f2(x14291,f13(a16),x14292),f13(a16),x14293),f5(f5(x14294,a20),x14295),f2(f2(x14296,f13(a16),x14297),x14298,x14299)),f2(f2(f2(x14291,a20,x14292),a20,x14293),f5(f5(x14294,f13(a16)),x14295),f2(f2(x14296,a20,x14297),x14298,x14299)))), % 59.46/59.51 inference(scs_inference,[],[1355,1419,1369,2,3])). % 59.46/59.51 cnf(1434,plain, % 59.46/59.51 (E(f2(f2(f2(x14341,f13(a16),x14342),f13(a16),x14343),f9(f9(x14344,a20),x14345),x14346),f2(f2(f2(x14341,a20,x14342),a20,x14343),f9(f9(x14344,f13(a16)),x14345),x14346))), % 59.46/59.51 inference(scs_inference,[],[110,1316,1390,2,3])). % 59.46/59.51 cnf(1438,plain, % 59.46/59.51 (E(f2(f2(f2(x14381,f13(a16),x14382),a20,x14383),x14384,x14385),f2(f2(f2(x14381,a20,x14382),f13(a16),x14383),x14384,x14385))), % 59.46/59.51 inference(scs_inference,[],[1370,2])). % 59.46/59.51 cnf(1439,plain, % 59.46/59.51 (E(f5(f2(f2(x14391,f13(a16),x14392),x14393,x14394),f2(f2(x14395,f13(a16),x14396),x14397,x14398)),f5(f2(f2(x14391,a20,x14392),x14393,x14394),f2(f2(x14395,a20,x14396),x14397,x14398)))), % 59.46/59.51 inference(scs_inference,[],[1370,1354,1359,2,3])). % 59.46/59.51 cnf(1444,plain, % 59.46/59.51 (E(f2(f2(f2(x14441,f13(a16),x14442),a20,x14443),x14444,f9(f9(x14445,f13(a16)),x14446)),f2(f2(f2(x14441,a20,x14442),a20,x14443),x14444,f9(f9(x14445,a20),x14446)))), % 59.46/59.51 inference(scs_inference,[],[1439,1438,1291,2,3])). % 59.46/59.51 cnf(1448,plain, % 59.46/59.51 (E(f2(f2(f2(x14481,a20,x14482),a20,x14483),f2(f2(x14484,a20,x14485),x14486,x14487),f2(f2(x14488,a20,x14489),x144810,x144811)),f2(f2(f2(x14481,f13(a16),x14482),f13(a16),x14483),f2(f2(x14484,a20,x14485),x14486,x14487),f2(f2(x14488,f13(a16),x14489),x144810,x144811)))), % 59.46/59.51 inference(scs_inference,[],[1424,2])). % 59.46/59.51 cnf(1449,plain, % 59.46/59.51 (E(f2(f2(f2(x14491,f13(a16),x14492),f13(a16),x14493),x14494,f9(f9(x14495,f13(a16)),x14496)),f2(f2(f2(x14491,a20,x14492),a20,x14493),x14494,f9(f9(x14495,a20),x14496)))), % 59.46/59.51 inference(scs_inference,[],[110,1424,1444,2,3])). % 59.46/59.51 cnf(1453,plain, % 59.46/59.51 (E(f2(f2(f2(x14531,a20,x14532),a20,x14533),x14534,f9(f9(x14535,a20),x14536)),f2(f2(f2(x14531,f13(a16),x14532),f13(a16),x14533),x14534,f9(f9(x14535,f13(a16)),x14536)))), % 59.46/59.51 inference(scs_inference,[],[1449,2])). % 59.46/59.51 cnf(1454,plain, % 59.46/59.51 (E(f2(f2(f2(x14541,a20,x14542),a20,x14543),f2(f2(x14544,a20,x14545),x14546,x14547),f2(f2(x14548,a20,x14549),x145410,x145411)),f2(f2(f2(x14541,f13(a16),x14542),a20,x14543),f2(f2(x14544,a20,x14545),x14546,x14547),f2(f2(x14548,f13(a16),x14549),x145410,x145411)))), % 59.46/59.51 inference(scs_inference,[],[110,1448,1449,2,3])). % 59.46/59.51 cnf(1456,plain, % 59.46/59.51 (E(f2(f2(f2(x14561,a20,x14562),a20,x14563),f9(f9(x14564,f13(a16)),x14565),x14566),f2(f2(f2(x14561,f13(a16),x14562),f13(a16),x14563),f9(f9(x14564,a20),x14565),x14566))), % 59.46/59.51 inference(scs_inference,[],[1434,2])). % 59.46/59.51 cnf(1457,plain, % 59.46/59.51 (E(f2(f2(f2(x14571,a20,x14572),a20,x14573),x14574,f9(f9(x14575,a20),x14576)),f2(f2(f2(x14571,f13(a16),x14572),a20,x14573),x14574,f9(f9(x14575,f13(a16)),x14576)))), % 59.46/59.51 inference(scs_inference,[],[110,1434,1453,2,3])). % 59.46/59.51 cnf(1460,plain, % 59.46/59.51 (E(f2(f2(x14601,a20,x14602),f9(f9(x14603,a20),x14604),f2(f2(x14605,f13(a16),x14606),x14607,x14608)),f2(f2(x14601,f13(a16),x14602),f9(f9(x14603,f13(a16)),x14604),f2(f2(x14605,a20,x14606),x14607,x14608)))), % 59.46/59.51 inference(scs_inference,[],[1415,2])). % 59.46/59.51 cnf(1461,plain, % 59.46/59.51 (E(f2(f2(f2(x14611,a20,x14612),a20,x14613),f9(f9(x14614,f13(a16)),x14615),x14616),f2(f2(f2(x14611,f13(a16),x14612),a20,x14613),f9(f9(x14614,a20),x14615),x14616))), % 59.46/59.51 inference(scs_inference,[],[110,1456,1415,2,3])). % 59.46/59.51 cnf(1463,plain, % 59.46/59.51 (E(f2(f2(f2(x14631,a20,x14632),a20,x14633),f5(f5(x14634,f13(a16)),x14635),f2(f2(x14636,a20,x14637),x14638,x14639)),f2(f2(f2(x14631,f13(a16),x14632),f13(a16),x14633),f5(f5(x14634,a20),x14635),f2(f2(x14636,f13(a16),x14637),x14638,x14639)))), % 59.46/59.51 inference(scs_inference,[],[1429,2])). % 59.46/59.51 cnf(1464,plain, % 59.46/59.51 (E(f2(f2(x14641,a20,x14642),f9(f9(x14643,a20),x14644),f2(f2(x14645,f13(a16),x14646),x14647,x14648)),f2(f2(x14641,a20,x14642),f9(f9(x14643,f13(a16)),x14644),f2(f2(x14645,a20,x14646),x14647,x14648)))), % 59.46/59.51 inference(scs_inference,[],[110,1460,1429,2,3])). % 59.46/59.51 cnf(1467,plain, % 59.46/59.51 (E(f2(f2(x14671,a20,x14672),f9(f9(x14673,f13(a16)),x14674),f2(f2(x14675,a20,x14676),x14677,x14678)),f2(f2(x14671,a20,x14672),f9(f9(x14673,a20),x14674),f2(f2(x14675,f13(a16),x14676),x14677,x14678)))), % 59.46/59.51 inference(scs_inference,[],[1464,2])). % 59.46/59.51 cnf(1468,plain, % 59.46/59.51 (E(f2(f2(x14681,f13(a16),x14682),f9(f9(x14683,a20),x14684),f2(f2(x14685,f13(a16),x14686),x14687,x14688)),f2(f2(x14681,a20,x14682),f9(f9(x14683,f13(a16)),x14684),f2(f2(x14685,a20,x14686),x14687,x14688)))), % 59.46/59.51 inference(scs_inference,[],[110,1464,2,3])). % 59.46/59.51 cnf(1472,plain, % 59.46/59.51 (E(f2(f2(x14721,a20,x14722),f9(f9(x14723,f13(a16)),x14724),f2(f2(x14725,a20,x14726),x14727,x14728)),f2(f2(x14721,f13(a16),x14722),f9(f9(x14723,a20),x14724),f2(f2(x14725,f13(a16),x14726),x14727,x14728)))), % 59.46/59.51 inference(scs_inference,[],[1468,2])). % 59.46/59.51 cnf(1473,plain, % 59.46/59.51 (E(f2(f2(f2(x14731,a20,x14732),f13(a16),x14733),f2(f2(x14734,a20,x14735),x14736,x14737),f2(f2(x14738,a20,x14739),x147310,x147311)),f2(f2(f2(x14731,f13(a16),x14732),a20,x14733),f2(f2(x14734,a20,x14735),x14736,x14737),f2(f2(x14738,f13(a16),x14739),x147310,x147311)))), % 59.46/59.51 inference(scs_inference,[],[110,1468,1454,2,3])). % 59.46/59.51 cnf(1477,plain, % 59.46/59.51 (E(f2(f2(f2(x14771,f13(a16),x14772),a20,x14773),f2(f2(x14774,a20,x14775),x14776,x14777),f2(f2(x14778,f13(a16),x14779),x147710,x147711)),f2(f2(f2(x14771,a20,x14772),f13(a16),x14773),f2(f2(x14774,a20,x14775),x14776,x14777),f2(f2(x14778,a20,x14779),x147710,x147711)))), % 59.46/59.51 inference(scs_inference,[],[1473,2])). % 59.46/59.51 cnf(1478,plain, % 59.46/59.51 (E(f2(f2(x14781,f13(a16),x14782),f9(f9(x14783,f13(a16)),x14784),f2(f2(x14785,a20,x14786),x14787,x14788)),f2(f2(x14781,f13(a16),x14782),f9(f9(x14783,a20),x14784),f2(f2(x14785,f13(a16),x14786),x14787,x14788)))), % 59.46/59.51 inference(scs_inference,[],[110,1473,1472,2,3])). % 59.46/59.51 cnf(1481,plain, % 59.46/59.51 (E(f2(f2(x14811,f13(a16),x14812),f9(f9(x14813,a20),x14814),f2(f2(x14815,f13(a16),x14816),x14817,x14818)),f2(f2(x14811,f13(a16),x14812),f9(f9(x14813,f13(a16)),x14814),f2(f2(x14815,a20,x14816),x14817,x14818)))), % 59.46/59.51 inference(scs_inference,[],[1478,2])). % 59.46/59.51 cnf(1482,plain, % 59.46/59.51 (E(f2(f2(f2(x14821,f13(a16),x14822),f13(a16),x14823),f2(f2(x14824,a20,x14825),x14826,x14827),f2(f2(x14828,f13(a16),x14829),x148210,x148211)),f2(f2(f2(x14821,a20,x14822),f13(a16),x14823),f2(f2(x14824,a20,x14825),x14826,x14827),f2(f2(x14828,a20,x14829),x148210,x148211)))), % 59.46/59.51 inference(scs_inference,[],[110,1478,1477,2,3])). % 59.46/59.51 cnf(1486,plain, % 59.46/59.51 (E(f2(f2(f2(x14861,a20,x14862),f13(a16),x14863),f2(f2(x14864,a20,x14865),x14866,x14867),f2(f2(x14868,a20,x14869),x148610,x148611)),f2(f2(f2(x14861,f13(a16),x14862),f13(a16),x14863),f2(f2(x14864,a20,x14865),x14866,x14867),f2(f2(x14868,f13(a16),x14869),x148610,x148611)))), % 59.46/59.51 inference(scs_inference,[],[1482,2])). % 59.46/59.51 cnf(1487,plain, % 59.46/59.51 (E(f2(f2(f2(x14871,f13(a16),x14872),f13(a16),x14873),f2(f2(x14874,f13(a16),x14875),x14876,x14877),f2(f2(x14878,f13(a16),x14879),x148710,x148711)),f2(f2(f2(x14871,a20,x14872),f13(a16),x14873),f2(f2(x14874,a20,x14875),x14876,x14877),f2(f2(x14878,a20,x14879),x148710,x148711)))), % 59.46/59.51 inference(scs_inference,[],[1482,1374,2,3])). % 59.46/59.51 cnf(1491,plain, % 59.46/59.51 (E(f2(f2(f2(x14911,a20,x14912),f13(a16),x14913),f2(f2(x14914,a20,x14915),x14916,x14917),f2(f2(x14918,a20,x14919),x149110,x149111)),f2(f2(f2(x14911,f13(a16),x14912),f13(a16),x14913),f2(f2(x14914,f13(a16),x14915),x14916,x14917),f2(f2(x14918,f13(a16),x14919),x149110,x149111)))), % 59.46/59.51 inference(scs_inference,[],[1487,2])). % 59.46/59.51 cnf(1492,plain, % 59.46/59.51 (E(f2(f2(f2(x14921,a20,x14922),f13(a16),x14923),f2(f2(x14924,f13(a16),x14925),x14926,x14927),f2(f2(x14928,f13(a16),x14929),x149210,x149211)),f2(f2(f2(x14921,a20,x14922),f13(a16),x14923),f2(f2(x14924,a20,x14925),x14926,x14927),f2(f2(x14928,a20,x14929),x149210,x149211)))), % 59.46/59.51 inference(scs_inference,[],[1487,1368,2,3])). % 59.46/59.51 cnf(1496,plain, % 59.46/59.51 (E(f2(f2(f2(x14961,a20,x14962),f13(a16),x14963),f2(f2(x14964,a20,x14965),x14966,x14967),f2(f2(x14968,a20,x14969),x149610,x149611)),f2(f2(f2(x14961,a20,x14962),f13(a16),x14963),f2(f2(x14964,f13(a16),x14965),x14966,x14967),f2(f2(x14968,f13(a16),x14969),x149610,x149611)))), % 59.46/59.51 inference(scs_inference,[],[1492,2])). % 59.46/59.51 cnf(1497,plain, % 59.46/59.51 (E(f2(f2(f2(x14971,a20,x14972),f13(a16),x14973),f2(f2(x14974,f13(a16),x14975),x14976,x14977),f2(f2(x14978,f13(a16),x14979),x149710,x149711)),f2(f2(f2(x14971,a20,x14972),a20,x14973),f2(f2(x14974,a20,x14975),x14976,x14977),f2(f2(x14978,a20,x14979),x149710,x149711)))), % 59.46/59.51 inference(scs_inference,[],[110,1492,2,3])). % 59.46/59.51 cnf(1501,plain, % 59.46/59.51 (E(f2(f2(f2(x15011,a20,x15012),f13(a16),x15013),f2(f2(x15014,a20,x15015),x15016,x15017),f2(f2(x15018,a20,x15019),x150110,x150111)),f2(f2(f2(x15011,a20,x15012),a20,x15013),f2(f2(x15014,f13(a16),x15015),x15016,x15017),f2(f2(x15018,f13(a16),x15019),x150110,x150111)))), % 59.46/59.51 inference(scs_inference,[],[110,1496,1497,2,3])). % 59.46/59.51 cnf(1505,plain, % 59.46/59.51 (E(f2(f2(f2(x15051,f13(a16),x15052),a20,x15053),f2(f2(x15054,a20,x15055),x15056,x15057),f2(f2(x15058,a20,x15059),x150510,x150511)),f2(f2(f2(x15051,f13(a16),x15052),f13(a16),x15053),f2(f2(x15054,a20,x15055),x15056,x15057),f2(f2(x15058,f13(a16),x15059),x150510,x150511)))), % 59.46/59.51 inference(scs_inference,[],[1486,1501,1438,2,3])). % 59.46/59.51 cnf(1509,plain, % 59.46/59.51 (E(f2(f2(x15091,a20,x15092),f5(f5(x15093,f13(a16)),x15094),f9(f9(x15095,a20),x15096)),f2(f2(x15091,f13(a16),x15092),f5(f5(x15093,a20),x15094),f9(f9(x15095,f13(a16)),x15096)))), % 59.46/59.51 inference(scs_inference,[],[1306,2])). % 59.46/59.51 cnf(1510,plain, % 59.46/59.51 (E(f2(f2(f2(x15101,a20,x15102),f13(a16),x15103),f9(f9(x15104,f13(a16)),x15105),x15106),f2(f2(f2(x15101,f13(a16),x15102),a20,x15103),f9(f9(x15104,a20),x15105),x15106))), % 59.46/59.51 inference(scs_inference,[],[110,1306,1461,2,3])). % 59.46/59.51 cnf(1514,plain, % 59.46/59.51 (E(f2(f2(f2(x15141,f13(a16),x15142),a20,x15143),f9(f9(x15144,a20),x15145),x15146),f2(f2(f2(x15141,a20,x15142),f13(a16),x15143),f9(f9(x15144,f13(a16)),x15145),x15146))), % 59.46/59.51 inference(scs_inference,[],[1510,2])). % 59.46/59.51 cnf(1515,plain, % 59.46/59.51 (E(f2(f2(f2(x15151,a20,x15152),f13(a16),x15153),f9(f9(x15154,a20),x15155),f2(f2(x15156,f13(a16),x15157),x15158,x15159)),f2(f2(f2(x15151,f13(a16),x15152),a20,x15153),f9(f9(x15154,a20),x15155),f2(f2(x15156,a20,x15157),x15158,x15159)))), % 59.46/59.51 inference(scs_inference,[],[1481,1510,2,3])). % 59.46/59.51 cnf(1519,plain, % 59.46/59.51 (E(f2(f2(f2(x15191,f13(a16),x15192),a20,x15193),f9(f9(x15194,a20),x15195),f2(f2(x15196,a20,x15197),x15198,x15199)),f2(f2(f2(x15191,a20,x15192),f13(a16),x15193),f9(f9(x15194,a20),x15195),f2(f2(x15196,f13(a16),x15197),x15198,x15199)))), % 59.46/59.51 inference(scs_inference,[],[1515,2])). % 59.46/59.51 cnf(1520,plain, % 59.46/59.51 (E(f2(f2(f2(x15201,f13(a16),x15202),f13(a16),x15203),f9(f9(x15204,a20),x15205),x15206),f2(f2(f2(x15201,a20,x15202),f13(a16),x15203),f9(f9(x15204,f13(a16)),x15205),x15206))), % 59.46/59.51 inference(scs_inference,[],[110,1514,1515,2,3])). % 59.46/59.51 cnf(1524,plain, % 59.46/59.51 (E(f2(f2(f2(x15241,a20,x15242),f13(a16),x15243),f9(f9(x15244,f13(a16)),x15245),x15246),f2(f2(f2(x15241,f13(a16),x15242),f13(a16),x15243),f9(f9(x15244,a20),x15245),x15246))), % 59.46/59.51 inference(scs_inference,[],[1520,2])). % 59.46/59.51 cnf(1525,plain, % 59.46/59.51 (E(f2(f2(f2(x15251,f13(a16),x15252),f13(a16),x15253),f9(f9(x15254,a20),x15255),f2(f2(x15256,a20,x15257),x15258,x15259)),f2(f2(f2(x15251,a20,x15252),f13(a16),x15253),f9(f9(x15254,a20),x15255),f2(f2(x15256,f13(a16),x15257),x15258,x15259)))), % 59.46/59.51 inference(scs_inference,[],[110,1520,1519,2,3])). % 59.46/59.51 cnf(1529,plain, % 59.46/59.51 (E(f2(f2(f2(x15291,a20,x15292),f13(a16),x15293),f9(f9(x15294,a20),x15295),f2(f2(x15296,f13(a16),x15297),x15298,x15299)),f2(f2(f2(x15291,f13(a16),x15292),f13(a16),x15293),f9(f9(x15294,a20),x15295),f2(f2(x15296,a20,x15297),x15298,x15299)))), % 59.46/59.51 inference(scs_inference,[],[1525,2])). % 59.46/59.51 cnf(1530,plain, % 59.46/59.51 (E(f2(f2(x15301,f13(a16),x15302),f5(f5(x15303,f13(a16)),x15304),f9(f9(x15305,a20),x15306)),f2(f2(x15301,f13(a16),x15302),f5(f5(x15303,a20),x15304),f9(f9(x15305,f13(a16)),x15306)))), % 59.46/59.51 inference(scs_inference,[],[110,1525,1509,2,3])). % 59.46/59.51 cnf(1534,plain, % 59.46/59.51 (E(f2(f2(x15341,f13(a16),x15342),f5(f5(x15343,a20),x15344),f9(f9(x15345,f13(a16)),x15346)),f2(f2(x15341,f13(a16),x15342),f5(f5(x15343,f13(a16)),x15344),f9(f9(x15345,a20),x15346)))), % 59.46/59.51 inference(scs_inference,[],[1530,2])). % 59.46/59.51 cnf(1535,plain, % 59.46/59.51 (E(f2(f2(f2(x15351,a20,x15352),f13(a16),x15353),x15354,f9(f9(x15355,a20),x15356)),f2(f2(f2(x15351,f13(a16),x15352),a20,x15353),x15354,f9(f9(x15355,f13(a16)),x15356)))), % 59.46/59.51 inference(scs_inference,[],[110,1530,1457,2,3])). % 59.46/59.51 cnf(1539,plain, % 59.46/59.51 (E(f2(f2(f2(x15391,f13(a16),x15392),a20,x15393),x15394,f9(f9(x15395,f13(a16)),x15396)),f2(f2(f2(x15391,a20,x15392),f13(a16),x15393),x15394,f9(f9(x15395,a20),x15396)))), % 59.46/59.51 inference(scs_inference,[],[1535,2])). % 59.46/59.51 cnf(1540,plain, % 59.46/59.51 (E(f2(f2(f2(x15401,a20,x15402),f13(a16),x15403),f2(f2(x15404,a20,x15405),x15406,x15407),f2(f2(x15408,a20,x15409),x154010,x154011)),f2(f2(f2(x15401,f13(a16),x15402),a20,x15403),f2(f2(x15404,f13(a16),x15405),x15406,x15407),f2(f2(x15408,a20,x15409),x154010,x154011)))), % 59.46/59.51 inference(scs_inference,[],[1491,1535,1385,2,3])). % 59.46/59.51 cnf(1543,plain, % 59.46/59.51 (E(f2(f2(f2(x15431,f13(a16),x15432),a20,x15433),f2(f2(x15434,f13(a16),x15435),x15436,x15437),f2(f2(x15438,a20,x15439),x154310,x154311)),f2(f2(f2(x15431,a20,x15432),f13(a16),x15433),f2(f2(x15434,a20,x15435),x15436,x15437),f2(f2(x15438,a20,x15439),x154310,x154311)))), % 59.46/59.51 inference(scs_inference,[],[1540,2])). % 59.46/59.51 cnf(1544,plain, % 59.46/59.51 (E(f2(f2(f2(x15441,f13(a16),x15442),f13(a16),x15443),x15444,f9(f9(x15445,f13(a16)),x15446)),f2(f2(f2(x15441,a20,x15442),f13(a16),x15443),x15444,f9(f9(x15445,a20),x15446)))), % 59.46/59.51 inference(scs_inference,[],[110,1540,1539,2,3])). % 59.46/59.51 cnf(1548,plain, % 59.46/59.51 (E(f2(f2(f2(x15481,a20,x15482),f13(a16),x15483),x15484,f9(f9(x15485,a20),x15486)),f2(f2(f2(x15481,f13(a16),x15482),f13(a16),x15483),x15484,f9(f9(x15485,f13(a16)),x15486)))), % 59.46/59.51 inference(scs_inference,[],[1544,2])). % 59.46/59.51 cnf(1549,plain, % 59.46/59.51 (E(f2(f2(f2(x15491,a20,x15492),f13(a16),x15493),f9(f9(x15494,f13(a16)),x15495),f9(f9(x15496,f13(a16)),x15497)),f2(f2(f2(x15491,a20,x15492),f13(a16),x15493),f9(f9(x15494,a20),x15495),f9(f9(x15496,a20),x15497)))), % 59.46/59.52 inference(scs_inference,[],[1524,1544,2,3])). % 59.46/59.52 cnf(1553,plain, % 59.46/59.52 (E(f2(f2(f2(x15531,a20,x15532),f13(a16),x15533),f9(f9(x15534,a20),x15535),f9(f9(x15536,a20),x15537)),f2(f2(f2(x15531,a20,x15532),f13(a16),x15533),f9(f9(x15534,f13(a16)),x15535),f9(f9(x15536,f13(a16)),x15537)))), % 59.46/59.52 inference(scs_inference,[],[1549,2])). % 59.46/59.52 cnf(1554,plain, % 59.46/59.52 (E(f2(f2(f2(x15541,a20,x15542),f13(a16),x15543),f5(f5(x15544,a20),x15545),f9(f9(x15546,a20),x15547)),f2(f2(f2(x15541,f13(a16),x15542),f13(a16),x15543),f5(f5(x15544,f13(a16)),x15545),f9(f9(x15546,a20),x15547)))), % 59.46/59.52 inference(scs_inference,[],[1534,1548,1549,2,3])). % 59.46/59.52 cnf(1559,plain, % 59.46/59.52 (E(f2(f2(f2(x15591,a20,x15592),f13(a16),x15593),f9(f9(x15594,a20),x15595),f9(f9(x15596,a20),x15597)),f2(f2(f2(x15591,a20,x15592),a20,x15593),f9(f9(x15594,f13(a16)),x15595),f9(f9(x15596,f13(a16)),x15597)))), % 59.46/59.52 inference(scs_inference,[],[110,1553,1554,2,3])). % 59.46/59.52 cnf(1562,plain, % 59.46/59.52 (E(f2(f2(f2(x15621,f13(a16),x15622),f13(a16),x15623),f2(f2(x15624,f13(a16),x15625),x15626,x15627),f2(f2(x15628,a20,x15629),x156210,x156211)),f2(f2(f2(x15621,a20,x15622),f13(a16),x15623),f2(f2(x15624,a20,x15625),x15626,x15627),f2(f2(x15628,a20,x15629),x156210,x156211)))), % 59.46/59.52 inference(scs_inference,[],[110,1543,1311,2,3])). % 59.46/59.52 cnf(1565,plain, % 59.46/59.52 (E(f2(f2(f2(x15651,a20,x15652),a20,x15653),f2(f2(x15654,a20,x15655),x15656,x15657),f2(f2(x15658,a20,x15659),x156510,x156511)),f2(f2(f2(x15651,f13(a16),x15652),f13(a16),x15653),f2(f2(x15654,f13(a16),x15655),x15656,x15657),f2(f2(x15658,a20,x15659),x156510,x156511)))), % 59.46/59.52 inference(scs_inference,[],[110,1562,2,3])). % 59.46/59.52 cnf(1567,plain, % 59.46/59.52 (E(f2(f2(f2(x15671,a20,x15672),f13(a16),x15673),f2(f2(x15674,a20,x15675),x15676,x15677),f2(f2(x15678,a20,x15679),x156710,x156711)),f2(f2(f2(x15671,f13(a16),x15672),f13(a16),x15673),f2(f2(x15674,f13(a16),x15675),x15676,x15677),f2(f2(x15678,a20,x15679),x156710,x156711)))), % 59.46/59.52 inference(scs_inference,[],[110,1565,1559,2,3])). % 59.46/59.52 cnf(1572,plain, % 59.46/59.52 (E(f2(f2(f2(x15721,a20,x15722),f13(a16),x15723),f2(f2(x15724,a20,x15725),x15726,x15727),f2(f2(x15728,a20,x15729),x157210,x157211)),f2(f2(f2(x15721,a20,x15722),a20,x15723),f2(f2(x15724,f13(a16),x15725),x15726,x15727),f2(f2(x15728,a20,x15729),x157210,x157211)))), % 59.46/59.52 inference(scs_inference,[],[1567,1365,1375,2,3])). % 59.46/59.52 cnf(1575,plain, % 59.46/59.52 (E(f2(f2(f2(x15751,a20,x15752),a20,x15753),f2(f2(x15754,f13(a16),x15755),x15756,x15757),f2(f2(x15758,a20,x15759),x157510,x157511)),f2(f2(f2(x15751,a20,x15752),f13(a16),x15753),f2(f2(x15754,a20,x15755),x15756,x15757),f2(f2(x15758,a20,x15759),x157510,x157511)))), % 59.46/59.52 inference(scs_inference,[],[1572,2])). % 59.46/59.52 cnf(1576,plain, % 59.46/59.52 (E(f2(f2(f2(x15761,f13(a16),x15762),a20,x15763),f9(f9(x15764,f13(a16)),x15765),f9(f9(x15766,a20),x15767)),f2(f2(f2(x15761,a20,x15762),a20,x15763),f9(f9(x15764,a20),x15765),f9(f9(x15766,a20),x15767)))), % 59.46/59.52 inference(scs_inference,[],[1572,1274,1449,2,3])). % 59.46/59.52 cnf(1580,plain, % 59.46/59.52 (E(f2(f2(f2(x15801,a20,x15802),a20,x15803),f9(f9(x15804,a20),x15805),f9(f9(x15806,a20),x15807)),f2(f2(f2(x15801,f13(a16),x15802),a20,x15803),f9(f9(x15804,f13(a16)),x15805),f9(f9(x15806,a20),x15807)))), % 59.46/59.52 inference(scs_inference,[],[1576,2])). % 59.46/59.52 cnf(1581,plain, % 59.46/59.52 (E(f2(f2(f2(x15811,f13(a16),x15812),f13(a16),x15813),f9(f9(x15814,f13(a16)),x15815),f9(f9(x15816,a20),x15817)),f2(f2(f2(x15811,a20,x15812),a20,x15813),f9(f9(x15814,a20),x15815),f9(f9(x15816,a20),x15817)))), % 59.46/59.52 inference(scs_inference,[],[110,1576,2,3])). % 59.46/59.52 cnf(1585,plain, % 59.46/59.52 (E(f2(f2(f2(x15851,a20,x15852),a20,x15853),f9(f9(x15854,a20),x15855),f9(f9(x15856,a20),x15857)),f2(f2(f2(x15851,f13(a16),x15852),f13(a16),x15853),f9(f9(x15854,f13(a16)),x15855),f9(f9(x15856,a20),x15857)))), % 59.46/59.52 inference(scs_inference,[],[1581,2])). % 59.46/59.52 cnf(1586,plain, % 59.46/59.52 (E(f2(f2(f2(x15861,a20,x15862),f13(a16),x15863),f9(f9(x15864,a20),x15865),f9(f9(x15866,a20),x15867)),f2(f2(f2(x15861,f13(a16),x15862),a20,x15863),f9(f9(x15864,f13(a16)),x15865),f9(f9(x15866,a20),x15867)))), % 59.46/59.52 inference(scs_inference,[],[110,1581,1580,2,3])). % 59.46/59.52 cnf(1591,plain, % 59.46/59.52 (E(f2(f2(f2(x15911,a20,x15912),f13(a16),x15913),f9(f9(x15914,a20),x15915),f9(f9(x15916,a20),x15917)),f2(f2(f2(x15911,f13(a16),x15912),f13(a16),x15913),f9(f9(x15914,f13(a16)),x15915),f9(f9(x15916,a20),x15917)))), % 59.46/59.52 inference(scs_inference,[],[110,1585,1586,2,3])). % 59.46/59.52 cnf(1596,plain, % 59.46/59.52 (E(f2(f2(f2(x15961,a20,x15962),a20,x15963),f2(f2(x15964,f13(a16),x15965),x15966,x15967),f2(f2(x15968,a20,x15969),x159610,x159611)),f2(f2(f2(x15961,f13(a16),x15962),f13(a16),x15963),f2(f2(x15964,f13(a16),x15965),x15966,x15967),f2(f2(x15968,a20,x15969),x159610,x159611)))), % 59.46/59.52 inference(scs_inference,[],[1575,1591,1567,2,3])). % 59.46/59.52 cnf(1599,plain, % 59.46/59.52 (E(f2(f2(x15991,a20,x15992),f2(f2(x15993,a20,x15994),x15995,x15996),x15997),f2(f2(x15991,f13(a16),x15992),f2(f2(x15993,f13(a16),x15994),x15995,x15996),x15997))), % 59.46/59.52 inference(scs_inference,[],[1380,2])). % 59.46/59.52 cnf(1600,plain, % 59.46/59.52 (E(f2(f2(f2(x16001,a20,x16002),a20,x16003),f2(f2(x16004,f13(a16),x16005),x16006,x16007),f2(f2(x16008,a20,x16009),x160010,x160011)),f2(f2(f2(x16001,f13(a16),x16002),a20,x16003),f2(f2(x16004,a20,x16005),x16006,x16007),f2(f2(x16008,a20,x16009),x160010,x160011)))), % 59.46/59.52 inference(scs_inference,[],[1596,1380,2,3])). % 59.46/59.52 cnf(1603,plain, % 59.46/59.52 (E(f2(f2(f2(x16031,a20,x16032),f13(a16),x16033),f2(f2(x16034,f13(a16),x16035),x16036,x16037),f2(f2(x16038,a20,x16039),x160310,x160311)),f2(f2(f2(x16031,f13(a16),x16032),a20,x16033),f2(f2(x16034,a20,x16035),x16036,x16037),f2(f2(x16038,a20,x16039),x160310,x160311)))), % 59.46/59.52 inference(scs_inference,[],[110,1600,2,3])). % 59.46/59.52 cnf(1626,plain, % 59.46/59.52 (E(f2(f2(f2(x16261,a20,x16262),a20,x16263),f2(f2(x16264,a20,x16265),x16266,x16267),x16268),f2(f2(f2(x16261,f13(a16),x16262),f13(a16),x16263),f2(f2(x16264,f13(a16),x16265),x16266,x16267),x16268))), % 59.46/59.52 inference(scs_inference,[],[1395,2])). % 59.46/59.52 cnf(1627,plain, % 59.46/59.52 (E(f2(f2(f2(x16271,a20,x16272),f13(a16),x16273),f2(f2(x16274,a20,x16275),x16276,x16277),f2(f2(x16278,a20,x16279),x162710,x162711)),f2(f2(f2(x16271,a20,x16272),a20,x16273),f2(f2(x16274,a20,x16275),x16276,x16277),f2(f2(x16278,f13(a16),x16279),x162710,x162711)))), % 59.46/59.52 inference(scs_inference,[],[1491,1395,2,3])). % 59.46/59.52 cnf(1631,plain, % 59.46/59.52 (E(f2(f2(f2(x16311,a20,x16312),a20,x16313),f2(f2(x16314,a20,x16315),x16316,x16317),x16318),f2(f2(f2(x16311,f13(a16),x16312),a20,x16313),f2(f2(x16314,f13(a16),x16315),x16316,x16317),x16318))), % 59.46/59.52 inference(scs_inference,[],[110,1626,1627,2,3])). % 59.46/59.52 cnf(1634,plain, % 59.46/59.52 (E(f2(f2(f2(x16341,f13(a16),x16342),a20,x16343),f2(f2(x16344,f13(a16),x16345),x16346,x16347),x16348),f2(f2(f2(x16341,a20,x16342),a20,x16343),f2(f2(x16344,a20,x16345),x16346,x16347),x16348))), % 59.46/59.52 inference(scs_inference,[],[1631,2])). % 59.46/59.52 cnf(1635,plain, % 59.46/59.52 (E(f2(f2(f2(x16351,a20,x16352),f13(a16),x16353),f2(f2(x16354,a20,x16355),x16356,x16357),x16358),f2(f2(f2(x16351,f13(a16),x16352),a20,x16353),f2(f2(x16354,f13(a16),x16355),x16356,x16357),x16358))), % 59.46/59.52 inference(scs_inference,[],[110,1631,2,3])). % 59.46/59.52 cnf(1639,plain, % 59.46/59.52 (E(f2(f2(f2(x16391,f13(a16),x16392),a20,x16393),f2(f2(x16394,f13(a16),x16395),x16396,x16397),x16398),f2(f2(f2(x16391,a20,x16392),f13(a16),x16393),f2(f2(x16394,a20,x16395),x16396,x16397),x16398))), % 59.46/59.52 inference(scs_inference,[],[1635,2])). % 59.46/59.52 cnf(1640,plain, % 59.46/59.52 (E(f2(f2(f2(x16401,a20,x16402),f13(a16),x16403),f2(f2(x16404,a20,x16405),x16406,x16407),x16408),f2(f2(f2(x16401,f13(a16),x16402),f13(a16),x16403),f2(f2(x16404,f13(a16),x16405),x16406,x16407),x16408))), % 59.46/59.52 inference(scs_inference,[],[110,1635,1626,2,3])). % 59.46/59.52 cnf(1644,plain, % 59.46/59.52 (E(f2(f2(f2(x16441,f13(a16),x16442),f13(a16),x16443),f2(f2(x16444,f13(a16),x16445),x16446,x16447),x16448),f2(f2(f2(x16441,a20,x16442),f13(a16),x16443),f2(f2(x16444,a20,x16445),x16446,x16447),x16448))), % 59.46/59.52 inference(scs_inference,[],[1640,2])). % 59.46/59.52 cnf(1645,plain, % 59.46/59.52 (E(f2(f2(f2(x16451,a20,x16452),f13(a16),x16453),f5(f5(x16454,f13(a16)),x16455),f2(f2(x16456,a20,x16457),x16458,x16459)),f2(f2(f2(x16451,f13(a16),x16452),f13(a16),x16453),f5(f5(x16454,a20),x16455),f2(f2(x16456,f13(a16),x16457),x16458,x16459)))), % 59.46/59.52 inference(scs_inference,[],[110,1640,1463,2,3])). % 59.46/59.52 cnf(1649,plain, % 59.46/59.52 (E(f2(f2(f2(x16491,f13(a16),x16492),f13(a16),x16493),f5(f5(x16494,a20),x16495),f2(f2(x16496,f13(a16),x16497),x16498,x16499)),f2(f2(f2(x16491,a20,x16492),f13(a16),x16493),f5(f5(x16494,f13(a16)),x16495),f2(f2(x16496,a20,x16497),x16498,x16499)))), % 59.46/59.52 inference(scs_inference,[],[1645,2])). % 59.46/59.52 cnf(1650,plain, % 59.46/59.52 (E(f2(f2(f2(x16501,a20,x16502),a20,x16503),f5(f5(x16504,a20),x16505),f2(f2(x16506,a20,x16507),x16508,x16509)),f2(f2(f2(x16501,f13(a16),x16502),f13(a16),x16503),f5(f5(x16504,a20),x16505),f2(f2(x16506,f13(a16),x16507),x16508,x16509)))), % 59.46/59.52 inference(scs_inference,[],[1645,1299,2,3])). % 59.46/59.52 cnf(1655,plain, % 59.46/59.52 (E(f2(f2(f2(x16551,a20,x16552),f13(a16),x16553),f5(f5(x16554,a20),x16555),f2(f2(x16556,a20,x16557),x16558,x16559)),f2(f2(f2(x16551,f13(a16),x16552),f13(a16),x16553),f5(f5(x16554,a20),x16555),f2(f2(x16556,f13(a16),x16557),x16558,x16559)))), % 59.46/59.52 inference(scs_inference,[],[110,1650,2,3])). % 59.46/59.52 cnf(1660,plain, % 59.46/59.52 (E(f2(f2(f2(x16601,f13(a16),x16602),f13(a16),x16603),f2(f2(x16604,f13(a16),x16605),x16606,x16607),f9(f9(x16608,f13(a16)),x16609)),f2(f2(f2(x16601,a20,x16602),a20,x16603),f2(f2(x16604,a20,x16605),x16606,x16607),f9(f9(x16608,a20),x16609)))), % 59.46/59.52 inference(scs_inference,[],[1644,1655,1291,2,3])). % 59.46/59.52 cnf(1664,plain, % 59.46/59.52 (E(f2(f2(f2(x16641,a20,x16642),a20,x16643),f2(f2(x16644,a20,x16645),x16646,x16647),f9(f9(x16648,a20),x16649)),f2(f2(f2(x16641,f13(a16),x16642),f13(a16),x16643),f2(f2(x16644,f13(a16),x16645),x16646,x16647),f9(f9(x16648,f13(a16)),x16649)))), % 59.46/59.52 inference(scs_inference,[],[1660,2])). % 59.46/59.52 cnf(1665,plain, % 59.46/59.52 (E(f2(f2(f2(x16651,a20,x16652),f13(a16),x16653),f5(f5(x16654,a20),x16655),f2(f2(x16656,a20,x16657),x16658,x16659)),f2(f2(f2(x16651,f13(a16),x16652),a20,x16653),f5(f5(x16654,f13(a16)),x16655),f2(f2(x16656,a20,x16657),x16658,x16659)))), % 59.46/59.52 inference(scs_inference,[],[1660,1655,1419,2,3])). % 59.46/59.52 cnf(1668,plain, % 59.46/59.52 (E(f2(f2(f2(x16681,f13(a16),x16682),a20,x16683),f5(f5(x16684,f13(a16)),x16685),f2(f2(x16686,a20,x16687),x16688,x16689)),f2(f2(f2(x16681,a20,x16682),f13(a16),x16683),f5(f5(x16684,a20),x16685),f2(f2(x16686,a20,x16687),x16688,x16689)))), % 59.46/59.52 inference(scs_inference,[],[1665,2])). % 59.46/59.52 cnf(1669,plain, % 59.46/59.52 (E(f2(f2(f2(x16691,f13(a16),x16692),f13(a16),x16693),f5(f5(x16694,a20),x16695),f2(f2(x16696,a20,x16697),x16698,x16699)),f2(f2(f2(x16691,a20,x16692),f13(a16),x16693),f5(f5(x16694,f13(a16)),x16695),f2(f2(x16696,a20,x16697),x16698,x16699)))), % 59.46/59.52 inference(scs_inference,[],[1649,1665,1378,2,3])). % 59.46/59.52 cnf(1674,plain, % 59.46/59.52 (E(f2(f2(f2(x16741,f13(a16),x16742),f13(a16),x16743),f5(f5(x16744,f13(a16)),x16745),f2(f2(x16746,a20,x16747),x16748,x16749)),f2(f2(f2(x16741,a20,x16742),f13(a16),x16743),f5(f5(x16744,a20),x16745),f2(f2(x16746,a20,x16747),x16748,x16749)))), % 59.46/59.52 inference(scs_inference,[],[110,1669,1668,2,3])). % 59.46/59.52 cnf(1679,plain, % 59.46/59.52 (E(f2(f2(f2(x16791,f13(a16),x16792),f13(a16),x16793),f5(f5(x16794,f13(a16)),x16795),f2(f2(x16796,f13(a16),x16797),x16798,x16799)),f2(f2(f2(x16791,a20,x16792),f13(a16),x16793),f5(f5(x16794,a20),x16795),f2(f2(x16796,a20,x16797),x16798,x16799)))), % 59.46/59.52 inference(scs_inference,[],[1674,1379,2,3])). % 59.46/59.52 cnf(1684,plain, % 59.46/59.52 (E(f2(f2(f2(x16841,a20,x16842),f13(a16),x16843),f2(f2(x16844,a20,x16845),x16846,x16847),f9(f9(x16848,a20),x16849)),f2(f2(f2(x16841,f13(a16),x16842),f13(a16),x16843),f2(f2(x16844,f13(a16),x16845),x16846,x16847),f9(f9(x16848,f13(a16)),x16849)))), % 59.46/59.52 inference(scs_inference,[],[110,1679,1664,2,3])). % 59.46/59.52 cnf(1689,plain, % 59.46/59.52 (E(f2(f2(x16891,f13(a16),x16892),f2(f2(x16893,a20,x16894),x16895,x16896),x16897),f2(f2(x16891,a20,x16892),f2(f2(x16893,f13(a16),x16894),x16895,x16896),x16897))), % 59.46/59.52 inference(scs_inference,[],[110,1684,1373,2,3])). % 59.46/59.52 cnf(1693,plain, % 59.46/59.52 (E(f2(f2(x16931,a20,x16932),f2(f2(x16933,f13(a16),x16934),x16935,x16936),x16937),f2(f2(x16931,f13(a16),x16932),f2(f2(x16933,a20,x16934),x16935,x16936),x16937))), % 59.46/59.52 inference(scs_inference,[],[1689,2])). % 59.46/59.52 cnf(1694,plain, % 59.46/59.52 (E(f2(f2(x16941,f13(a16),x16942),x16943,f5(f5(x16944,f13(a16)),x16945)),f2(f2(x16941,a20,x16942),x16943,f5(f5(x16944,a20),x16945)))), % 59.46/59.52 inference(scs_inference,[],[110,1689,1018,2,3])). % 59.46/59.52 cnf(1698,plain, % 59.46/59.52 (E(f2(f2(x16981,a20,x16982),x16983,f5(f5(x16984,a20),x16985)),f2(f2(x16981,f13(a16),x16982),x16983,f5(f5(x16984,f13(a16)),x16985)))), % 59.46/59.52 inference(scs_inference,[],[1694,2])). % 59.46/59.52 cnf(1699,plain, % 59.46/59.52 (E(f2(f2(x16991,a20,x16992),f2(f2(x16993,f13(a16),x16994),x16995,x16996),f5(f5(x16997,f13(a16)),x16998)),f2(f2(x16991,a20,x16992),f2(f2(x16993,a20,x16994),x16995,x16996),f5(f5(x16997,a20),x16998)))), % 59.46/59.52 inference(scs_inference,[],[1693,1694,2,3])). % 59.46/59.52 cnf(1703,plain, % 59.46/59.52 (E(f2(f2(x17031,a20,x17032),f2(f2(x17033,a20,x17034),x17035,x17036),f5(f5(x17037,a20),x17038)),f2(f2(x17031,a20,x17032),f2(f2(x17033,f13(a16),x17034),x17035,x17036),f5(f5(x17037,f13(a16)),x17038)))), % 59.46/59.52 inference(scs_inference,[],[1699,2])). % 59.46/59.52 cnf(1704,plain, % 59.46/59.52 (E(f2(f2(x17041,f13(a16),x17042),f2(f2(x17043,f13(a16),x17044),x17045,x17046),f5(f5(x17047,f13(a16)),x17048)),f2(f2(x17041,a20,x17042),f2(f2(x17043,a20,x17044),x17045,x17046),f5(f5(x17047,a20),x17048)))), % 59.46/59.52 inference(scs_inference,[],[110,1699,2,3])). % 59.46/59.52 cnf(1708,plain, % 59.46/59.52 (E(f2(f2(x17081,a20,x17082),f2(f2(x17083,a20,x17084),x17085,x17086),f5(f5(x17087,a20),x17088)),f2(f2(x17081,f13(a16),x17082),f2(f2(x17083,f13(a16),x17084),x17085,x17086),f5(f5(x17087,f13(a16)),x17088)))), % 59.46/59.52 inference(scs_inference,[],[1704,2])). % 59.46/59.52 cnf(1709,plain, % 59.46/59.52 (E(f2(f2(x17091,f13(a16),x17092),f2(f2(x17093,a20,x17094),x17095,x17096),f5(f5(x17097,a20),x17098)),f2(f2(x17091,a20,x17092),f2(f2(x17093,f13(a16),x17094),x17095,x17096),f5(f5(x17097,f13(a16)),x17098)))), % 59.46/59.52 inference(scs_inference,[],[110,1703,1704,2,3])). % 59.46/59.52 cnf(1713,plain, % 59.46/59.52 (E(f2(f2(x17131,a20,x17132),f2(f2(x17133,f13(a16),x17134),x17135,x17136),f5(f5(x17137,f13(a16)),x17138)),f2(f2(x17131,f13(a16),x17132),f2(f2(x17133,a20,x17134),x17135,x17136),f5(f5(x17137,a20),x17138)))), % 59.46/59.52 inference(scs_inference,[],[1709,2])). % 59.46/59.52 cnf(1714,plain, % 59.46/59.52 (E(f2(f2(x17141,f13(a16),x17142),f2(f2(x17143,a20,x17144),x17145,x17146),f5(f5(x17147,a20),x17148)),f2(f2(x17141,f13(a16),x17142),f2(f2(x17143,f13(a16),x17144),x17145,x17146),f5(f5(x17147,f13(a16)),x17148)))), % 59.46/59.52 inference(scs_inference,[],[110,1708,1709,2,3])). % 59.46/59.52 cnf(1718,plain, % 59.46/59.52 (E(f2(f2(x17181,f13(a16),x17182),f2(f2(x17183,f13(a16),x17184),x17185,x17186),f5(f5(x17187,f13(a16)),x17188)),f2(f2(x17181,f13(a16),x17182),f2(f2(x17183,a20,x17184),x17185,x17186),f5(f5(x17187,a20),x17188)))), % 59.46/59.52 inference(scs_inference,[],[1714,2])). % 59.46/59.52 cnf(1719,plain, % 59.46/59.52 (E(f2(f2(f2(x17191,f13(a16),x17192),f13(a16),x17193),f2(f2(x17194,a20,x17195),x17196,x17197),f5(f5(x17198,a20),x17199)),f2(f2(f2(x17191,a20,x17192),f13(a16),x17193),f2(f2(x17194,a20,x17195),x17196,x17197),f5(f5(x17198,f13(a16)),x17199)))), % 59.46/59.52 inference(scs_inference,[],[1714,1644,2,3])). % 59.46/59.52 cnf(1723,plain, % 59.46/59.52 (E(f2(f2(f2(x17231,a20,x17232),f13(a16),x17233),f2(f2(x17234,a20,x17235),x17236,x17237),f5(f5(x17238,f13(a16)),x17239)),f2(f2(f2(x17231,f13(a16),x17232),f13(a16),x17233),f2(f2(x17234,a20,x17235),x17236,x17237),f5(f5(x17238,a20),x17239)))), % 59.46/59.52 inference(scs_inference,[],[1719,2])). % 59.46/59.52 cnf(1724,plain, % 59.46/59.52 (E(f2(f2(f2(x17241,a20,x17242),a20,x17243),f9(f9(x17244,f13(a16)),x17245),f5(f5(x17246,a20),x17247)),f2(f2(f2(x17241,f13(a16),x17242),f13(a16),x17243),f9(f9(x17244,a20),x17245),f5(f5(x17246,f13(a16)),x17247)))), % 59.46/59.52 inference(scs_inference,[],[1719,1698,1524,2,3])). % 59.46/59.52 cnf(1729,plain, % 59.46/59.52 (E(f2(f2(f2(x17291,a20,x17292),f13(a16),x17293),f9(f9(x17294,f13(a16)),x17295),f5(f5(x17296,a20),x17297)),f2(f2(f2(x17291,f13(a16),x17292),f13(a16),x17293),f9(f9(x17294,a20),x17295),f5(f5(x17296,f13(a16)),x17297)))), % 59.46/59.52 inference(scs_inference,[],[110,1724,2,3])). % 59.46/59.52 cnf(1733,plain, % 59.46/59.52 (E(f2(f2(f2(x17331,f13(a16),x17332),f13(a16),x17333),f9(f9(x17334,a20),x17335),f5(f5(x17336,f13(a16)),x17337)),f2(f2(f2(x17331,a20,x17332),f13(a16),x17333),f9(f9(x17334,f13(a16)),x17335),f5(f5(x17336,a20),x17337)))), % 59.46/59.52 inference(scs_inference,[],[1729,2])). % 59.46/59.52 cnf(1734,plain, % 59.46/59.52 (E(f2(f2(f2(x17341,a20,x17342),f13(a16),x17343),f2(f2(x17344,a20,x17345),x17346,x17347),f5(f5(x17348,f13(a16)),x17349)),f2(f2(f2(x17341,f13(a16),x17342),a20,x17343),f2(f2(x17344,a20,x17345),x17346,x17347),f5(f5(x17348,a20),x17349)))), % 59.46/59.52 inference(scs_inference,[],[1729,1640,1704,2,3])). % 59.46/59.52 cnf(1738,plain, % 59.46/59.52 (E(f2(f2(f2(x17381,f13(a16),x17382),a20,x17383),f2(f2(x17384,a20,x17385),x17386,x17387),f5(f5(x17388,a20),x17389)),f2(f2(f2(x17381,a20,x17382),f13(a16),x17383),f2(f2(x17384,a20,x17385),x17386,x17387),f5(f5(x17388,f13(a16)),x17389)))), % 59.46/59.52 inference(scs_inference,[],[1734,2])). % 59.46/59.52 cnf(1739,plain, % 59.46/59.52 (E(f2(f2(x17391,a20,x17392),f2(f2(x17393,a20,x17394),x17395,x17396),f5(f5(x17397,f13(a16)),x17398)),f2(f2(x17391,f13(a16),x17392),f2(f2(x17393,a20,x17394),x17395,x17396),f5(f5(x17397,a20),x17398)))), % 59.46/59.52 inference(scs_inference,[],[1718,1734,1599,2,3])). % 59.46/59.52 cnf(1744,plain, % 59.46/59.52 (E(f2(f2(f2(x17441,f13(a16),x17442),f13(a16),x17443),f9(f9(x17444,a20),x17445),f5(f5(x17446,f13(a16)),x17447)),f2(f2(f2(x17441,a20,x17442),a20,x17443),f9(f9(x17444,a20),x17445),f5(f5(x17446,a20),x17447)))), % 59.46/59.52 inference(scs_inference,[],[1739,1733,1286,2,3])). % 59.46/59.52 cnf(1747,plain, % 59.46/59.52 (E(f2(f2(f2(x17471,a20,x17472),a20,x17473),f9(f9(x17474,a20),x17475),f5(f5(x17476,a20),x17477)),f2(f2(f2(x17471,f13(a16),x17472),f13(a16),x17473),f9(f9(x17474,a20),x17475),f5(f5(x17476,f13(a16)),x17477)))), % 59.46/59.52 inference(scs_inference,[],[1744,2])). % 59.46/59.52 cnf(1748,plain, % 59.46/59.52 (E(f2(f2(x17481,f13(a16),x17482),f9(f9(x17483,a20),x17484),x17485),f2(f2(x17481,a20,x17482),f9(f9(x17483,f13(a16)),x17484),x17485))), % 59.46/59.52 inference(scs_inference,[],[110,1744,744,2,3])). % 59.46/59.52 cnf(1752,plain, % 59.46/59.52 (E(f2(f2(x17521,a20,x17522),f9(f9(x17523,f13(a16)),x17524),x17525),f2(f2(x17521,f13(a16),x17522),f9(f9(x17523,a20),x17524),x17525))), % 59.46/59.52 inference(scs_inference,[],[1748,2])). % 59.46/59.52 cnf(1753,plain, % 59.46/59.52 (E(f2(f2(f2(x17531,a20,x17532),f13(a16),x17533),f9(f9(x17534,a20),x17535),f5(f5(x17536,a20),x17537)),f2(f2(f2(x17531,f13(a16),x17532),f13(a16),x17533),f9(f9(x17534,a20),x17535),f5(f5(x17536,f13(a16)),x17537)))), % 59.46/59.52 inference(scs_inference,[],[110,1748,1747,2,3])). % 59.46/59.52 cnf(1758,plain, % 59.46/59.52 (E(f2(f2(f2(x17581,a20,x17582),a20,x17583),f9(f9(x17584,f13(a16)),x17585),f2(f2(x17586,f13(a16),x17587),x17588,x17589)),f2(f2(f2(x17581,f13(a16),x17582),f13(a16),x17583),f9(f9(x17584,a20),x17585),f2(f2(x17586,a20,x17587),x17588,x17589)))), % 59.46/59.52 inference(scs_inference,[],[1529,1752,1753,2,3])). % 59.46/59.52 cnf(1763,plain, % 59.46/59.52 (E(f2(f2(f2(x17631,a20,x17632),f13(a16),x17633),f9(f9(x17634,f13(a16)),x17635),f2(f2(x17636,f13(a16),x17637),x17638,x17639)),f2(f2(f2(x17631,f13(a16),x17632),f13(a16),x17633),f9(f9(x17634,a20),x17635),f2(f2(x17636,a20,x17637),x17638,x17639)))), % 59.46/59.52 inference(scs_inference,[],[110,1758,2,3])). % 59.46/59.52 cnf(1768,plain, % 59.46/59.52 (E(f2(f2(x17681,f13(a16),x17682),x17683,f9(f9(x17684,a20),x17685)),f2(f2(x17681,a20,x17682),x17683,f9(f9(x17684,f13(a16)),x17685)))), % 59.46/59.52 inference(scs_inference,[],[110,1763,749,2,3])). % 59.46/59.52 cnf(1773,plain, % 59.46/59.52 (E(f2(f2(x17731,f13(a16),x17732),f5(f5(x17733,a20),x17734),x17735),f2(f2(x17731,a20,x17732),f5(f5(x17733,f13(a16)),x17734),x17735))), % 59.46/59.52 inference(scs_inference,[],[110,1768,1014,2,3])). % 59.46/59.52 cnf(1777,plain, % 59.46/59.52 (E(f2(f2(x17771,a20,x17772),f5(f5(x17773,f13(a16)),x17774),x17775),f2(f2(x17771,f13(a16),x17772),f5(f5(x17773,a20),x17774),x17775))), % 59.46/59.52 inference(scs_inference,[],[1773,2])). % 59.46/59.52 cnf(1812,plain, % 59.46/59.52 (E(f2(f2(x18121,a20,x18122),f5(f5(x18123,f13(a16)),x18124),f2(f2(x18125,a20,x18126),x18127,x18128)),f2(f2(x18121,a20,x18122),f5(f5(x18123,a20),x18124),f2(f2(x18125,f13(a16),x18126),x18127,x18128)))), % 59.46/59.52 inference(scs_inference,[],[1405,2])). % 59.46/59.52 cnf(1813,plain, % 59.46/59.52 (E(f2(f2(f2(x18131,a20,x18132),f13(a16),x18133),f2(f2(x18134,f13(a16),x18135),x18136,x18137),f2(f2(x18138,a20,x18139),x181310,x181311)),f2(f2(f2(x18131,f13(a16),x18132),f13(a16),x18133),f2(f2(x18134,a20,x18135),x18136,x18137),f2(f2(x18138,f13(a16),x18139),x181310,x181311)))), % 59.46/59.52 inference(scs_inference,[],[1505,1405,1603,2,3])). % 59.46/59.52 cnf(1817,plain, % 59.46/59.52 (E(f2(f2(x18171,f13(a16),x18172),f9(f9(x18173,a20),x18174),f2(f2(x18175,a20,x18176),x18177,x18178)),f2(f2(x18171,a20,x18172),f9(f9(x18173,a20),x18174),f2(f2(x18175,f13(a16),x18176),x18177,x18178)))), % 59.46/59.52 inference(scs_inference,[],[1813,1467,1748,2,3])). % 59.46/59.52 cnf(1822,plain, % 59.46/59.52 (E(f2(f2(x18221,f13(a16),x18222),f5(f5(x18223,a20),x18224),f2(f2(x18225,a20,x18226),x18227,x18228)),f2(f2(x18221,a20,x18222),f5(f5(x18223,a20),x18224),f2(f2(x18225,f13(a16),x18226),x18227,x18228)))), % 59.46/59.52 inference(scs_inference,[],[1812,1817,1773,2,3])). % 59.46/59.52 cnf(1826,plain, % 59.46/59.52 (E(f2(f2(x18261,a20,x18262),f5(f5(x18263,a20),x18264),f2(f2(x18265,f13(a16),x18266),x18267,x18268)),f2(f2(x18261,f13(a16),x18262),f5(f5(x18263,a20),x18264),f2(f2(x18265,a20,x18266),x18267,x18268)))), % 59.46/59.52 inference(scs_inference,[],[1822,2])). % 59.46/59.52 cnf(1827,plain, % 59.46/59.52 (E(f2(f2(x18271,f13(a16),x18272),f9(f9(x18273,a20),x18274),f9(f9(x18275,a20),x18276)),f2(f2(x18271,f13(a16),x18272),f9(f9(x18273,f13(a16)),x18274),f9(f9(x18275,f13(a16)),x18276)))), % 59.46/59.52 inference(scs_inference,[],[1822,1289,1768,2,3])). % 59.46/59.52 cnf(1832,plain, % 59.46/59.52 (E(f2(f2(x18321,f13(a16),x18322),f5(f5(x18323,f13(a16)),x18324),f2(f2(x18325,f13(a16),x18326),x18327,x18328)),f2(f2(x18321,f13(a16),x18322),f5(f5(x18323,a20),x18324),f2(f2(x18325,a20,x18326),x18327,x18328)))), % 59.46/59.52 inference(scs_inference,[],[1827,1826,1296,2,3])). % 59.46/59.52 cnf(1837,plain, % 59.46/59.52 (E(f2(f2(f2(x18371,f13(a16),x18372),f13(a16),x18373),f9(f9(x18374,a20),x18375),f2(f2(x18376,a20,x18377),x18378,x18379)),f2(f2(f2(x18371,a20,x18372),a20,x18373),f9(f9(x18374,a20),x18375),f2(f2(x18376,f13(a16),x18377),x18378,x18379)))), % 59.46/59.52 inference(scs_inference,[],[1832,1467,1434,2,3])). % 59.46/59.52 cnf(1842,plain, % 59.46/59.52 (E(f2(f2(f2(x18421,a20,x18422),f13(a16),x18423),f5(f5(x18424,a20),x18425),f2(f2(x18426,a20,x18427),x18428,x18429)),f2(f2(f2(x18421,f13(a16),x18422),a20,x18423),f5(f5(x18424,a20),x18425),f2(f2(x18426,f13(a16),x18427),x18428,x18429)))), % 59.46/59.52 inference(scs_inference,[],[1837,1812,1665,2,3])). % 59.46/59.52 cnf(1846,plain, % 59.46/59.52 (E(f2(f2(f2(x18461,f13(a16),x18462),f13(a16),x18463),f2(f2(x18464,a20,x18465),x18466,x18467),f9(f9(x18468,f13(a16)),x18469)),f2(f2(f2(x18461,a20,x18462),f13(a16),x18463),f2(f2(x18464,f13(a16),x18465),x18466,x18467),f9(f9(x18468,a20),x18469)))), % 59.46/59.52 inference(scs_inference,[],[1842,1689,1539,2,3])). % 59.46/59.52 cnf(1850,plain, % 59.46/59.52 (E(f2(f2(f2(x18501,a20,x18502),f13(a16),x18503),f2(f2(x18504,f13(a16),x18505),x18506,x18507),f9(f9(x18508,a20),x18509)),f2(f2(f2(x18501,f13(a16),x18502),f13(a16),x18503),f2(f2(x18504,a20,x18505),x18506,x18507),f9(f9(x18508,f13(a16)),x18509)))), % 59.46/59.52 inference(scs_inference,[],[1846,2])). % 59.46/59.52 cnf(1851,plain, % 59.46/59.52 (E(f2(f2(f2(x18511,a20,x18512),f13(a16),x18513),f2(f2(x18514,a20,x18515),x18516,x18517),f9(f9(x18518,f13(a16)),x18519)),f2(f2(f2(x18511,a20,x18512),a20,x18513),f2(f2(x18514,f13(a16),x18515),x18516,x18517),f9(f9(x18518,a20),x18519)))), % 59.46/59.52 inference(scs_inference,[],[1846,1635,1444,2,3])). % 59.46/59.52 cnf(1855,plain, % 59.46/59.52 (E(f2(f2(f2(x18551,a20,x18552),a20,x18553),f2(f2(x18554,f13(a16),x18555),x18556,x18557),f9(f9(x18558,a20),x18559)),f2(f2(f2(x18551,a20,x18552),f13(a16),x18553),f2(f2(x18554,a20,x18555),x18556,x18557),f9(f9(x18558,f13(a16)),x18559)))), % 59.46/59.52 inference(scs_inference,[],[1851,2])). % 59.46/59.52 cnf(1856,plain, % 59.46/59.52 (E(f2(f2(f2(x18561,f13(a16),x18562),a20,x18563),f2(f2(x18564,a20,x18565),x18566,x18567),f5(f5(x18568,a20),x18569)),f2(f2(f2(x18561,a20,x18562),a20,x18563),f2(f2(x18564,a20,x18565),x18566,x18567),f5(f5(x18568,f13(a16)),x18569)))), % 59.46/59.52 inference(scs_inference,[],[1634,1851,1703,2,3])). % 59.46/59.52 cnf(1860,plain, % 59.46/59.52 (E(f2(f2(f2(x18601,a20,x18602),a20,x18603),f2(f2(x18604,a20,x18605),x18606,x18607),f5(f5(x18608,f13(a16)),x18609)),f2(f2(f2(x18601,f13(a16),x18602),a20,x18603),f2(f2(x18604,a20,x18605),x18606,x18607),f5(f5(x18608,a20),x18609)))), % 59.46/59.52 inference(scs_inference,[],[1856,2])). % 59.46/59.52 cnf(1861,plain, % 59.46/59.52 (E(f2(f2(f2(x18611,a20,x18612),f13(a16),x18613),f2(f2(x18614,f13(a16),x18615),x18616,x18617),f9(f9(x18618,a20),x18619)),f2(f2(f2(x18611,a20,x18612),f13(a16),x18613),f2(f2(x18614,a20,x18615),x18616,x18617),f9(f9(x18618,f13(a16)),x18619)))), % 59.46/59.52 inference(scs_inference,[],[1639,1856,1535,2,3])). % 59.46/59.52 cnf(1865,plain, % 59.46/59.52 (E(f2(f2(f2(x18651,a20,x18652),f13(a16),x18653),f2(f2(x18654,a20,x18655),x18656,x18657),f9(f9(x18658,f13(a16)),x18659)),f2(f2(f2(x18651,a20,x18652),f13(a16),x18653),f2(f2(x18654,f13(a16),x18655),x18656,x18657),f9(f9(x18658,a20),x18659)))), % 59.46/59.52 inference(scs_inference,[],[1861,2])). % 59.46/59.52 cnf(1866,plain, % 59.46/59.52 (E(f2(f2(f2(x18661,f13(a16),x18662),f13(a16),x18663),f2(f2(x18664,a20,x18665),x18666,x18667),f5(f5(x18668,a20),x18669)),f2(f2(f2(x18661,a20,x18662),a20,x18663),f2(f2(x18664,a20,x18665),x18666,x18667),f5(f5(x18668,f13(a16)),x18669)))), % 59.46/59.52 inference(scs_inference,[],[1861,1709,1634,2,3])). % 59.46/59.52 cnf(1871,plain, % 59.46/59.52 (E(f2(f2(f2(x18711,f13(a16),x18712),f13(a16),x18713),f2(f2(x18714,f13(a16),x18715),x18716,x18717),f5(f5(x18718,f13(a16)),x18719)),f2(f2(f2(x18711,a20,x18712),f13(a16),x18713),f2(f2(x18714,a20,x18715),x18716,x18717),f5(f5(x18718,a20),x18719)))), % 59.46/59.52 inference(scs_inference,[],[1713,1866,1375,2,3])). % 59.46/59.52 cnf(1876,plain, % 59.46/59.52 (E(f2(f2(f2(x18761,a20,x18762),f13(a16),x18763),f2(f2(x18764,f13(a16),x18765),x18766,x18767),f5(f5(x18768,f13(a16)),x18769)),f2(f2(f2(x18761,f13(a16),x18762),f13(a16),x18763),f2(f2(x18764,a20,x18765),x18766,x18767),f5(f5(x18768,a20),x18769)))), % 59.46/59.52 inference(scs_inference,[],[1871,1713,1370,2,3])). % 59.46/59.52 cnf(1881,plain, % 59.46/59.52 (E(f2(f2(f2(x18811,a20,x18812),a20,x18813),f2(f2(x18814,f13(a16),x18815),x18816,x18817),f5(f5(x18818,a20),x18819)),f2(f2(f2(x18811,f13(a16),x18812),f13(a16),x18813),f2(f2(x18814,a20,x18815),x18816,x18817),f5(f5(x18818,a20),x18819)))), % 59.46/59.52 inference(scs_inference,[],[1876,1698,2,3])). % 59.46/59.52 cnf(1885,plain, % 59.46/59.52 (E(f2(f2(f2(x18851,f13(a16),x18852),f13(a16),x18853),f2(f2(x18854,a20,x18855),x18856,x18857),f5(f5(x18858,a20),x18859)),f2(f2(f2(x18851,a20,x18852),a20,x18853),f2(f2(x18854,f13(a16),x18855),x18856,x18857),f5(f5(x18858,a20),x18859)))), % 59.46/59.52 inference(scs_inference,[],[1881,2])). % 59.46/59.52 cnf(1886,plain, % 59.46/59.52 (E(f2(f2(f2(x18861,a20,x18862),f13(a16),x18863),f2(f2(x18864,f13(a16),x18865),x18866,x18867),f9(f9(x18868,a20),x18869)),f2(f2(f2(x18861,f13(a16),x18862),a20,x18863),f2(f2(x18864,a20,x18865),x18866,x18867),f9(f9(x18868,a20),x18869)))), % 59.46/59.52 inference(scs_inference,[],[1850,1881,1291,2,3])). % 59.46/59.52 cnf(1889,plain, % 59.46/59.52 (E(f2(f2(f2(x18891,f13(a16),x18892),a20,x18893),f2(f2(x18894,a20,x18895),x18896,x18897),f9(f9(x18898,a20),x18899)),f2(f2(f2(x18891,a20,x18892),f13(a16),x18893),f2(f2(x18894,f13(a16),x18895),x18896,x18897),f9(f9(x18898,a20),x18899)))), % 59.46/59.52 inference(scs_inference,[],[1886,2])). % 59.46/59.52 cnf(1890,plain, % 59.46/59.52 (E(f2(f2(f2(x18901,a20,x18902),f13(a16),x18903),f2(f2(x18904,a20,x18905),x18906,x18907),f5(f5(x18908,f13(a16)),x18909)),f2(f2(f2(x18901,a20,x18902),a20,x18903),f2(f2(x18904,f13(a16),x18905),x18906,x18907),f5(f5(x18908,a20),x18909)))), % 59.46/59.52 inference(scs_inference,[],[1723,1885,1886,2,3])). % 59.46/59.52 cnf(1894,plain, % 59.46/59.52 (E(f2(f2(f2(x18941,f13(a16),x18942),a20,x18943),f2(f2(x18944,a20,x18945),x18946,x18947),f5(f5(x18948,a20),x18949)),f2(f2(f2(x18941,a20,x18942),a20,x18943),f2(f2(x18944,f13(a16),x18945),x18946,x18947),f5(f5(x18948,a20),x18949)))), % 59.46/59.52 inference(scs_inference,[],[1890,1738,2,3])). % 59.46/59.52 cnf(1897,plain, % 59.46/59.52 (E(f2(f2(f2(x18971,a20,x18972),a20,x18973),f2(f2(x18974,a20,x18975),x18976,x18977),f5(f5(x18978,f13(a16)),x18979)),f2(f2(f2(x18971,a20,x18972),a20,x18973),f2(f2(x18974,f13(a16),x18975),x18976,x18977),f5(f5(x18978,a20),x18979)))), % 59.46/59.52 inference(scs_inference,[],[1860,1894,2,3])). % 59.46/59.52 cnf(1901,plain, % 59.46/59.52 (E(f2(f2(f2(x19011,a20,x19012),f13(a16),x19013),f2(f2(x19014,a20,x19015),x19016,x19017),f9(f9(x19018,f13(a16)),x19019)),f2(f2(f2(x19011,f13(a16),x19012),a20,x19013),f2(f2(x19014,a20,x19015),x19016,x19017),f9(f9(x19018,a20),x19019)))), % 59.46/59.52 inference(scs_inference,[],[1865,1897,1886,2,3])). % 59.46/59.52 cnf(1905,plain, % 59.46/59.52 (E(f2(f2(f2(x19051,a20,x19052),a20,x19053),f2(f2(x19054,f13(a16),x19055),x19056,x19057),f9(f9(x19058,a20),x19059)),f2(f2(f2(x19051,f13(a16),x19052),a20,x19053),f2(f2(x19054,a20,x19055),x19056,x19057),f9(f9(x19058,a20),x19059)))), % 59.46/59.52 inference(scs_inference,[],[1901,1855,2,3])). % 59.46/59.52 cnf(1908,plain, % 59.46/59.52 (E(f2(f2(f2(x19081,f13(a16),x19082),a20,x19083),f2(f2(x19084,a20,x19085),x19086,x19087),f9(f9(x19088,a20),x19089)),f2(f2(f2(x19081,a20,x19082),a20,x19083),f2(f2(x19084,f13(a16),x19085),x19086,x19087),f9(f9(x19088,a20),x19089)))), % 59.46/59.52 inference(scs_inference,[],[1905,2])). % 59.46/59.52 cnf(1909,plain, % 59.46/59.52 (E(f2(f2(f2(x19091,f13(a16),x19092),a20,x19093),f5(f5(x19094,f13(a16)),x19095),f9(f9(x19096,a20),x19097)),f2(f2(f2(x19091,a20,x19092),f13(a16),x19093),f5(f5(x19094,a20),x19095),f9(f9(x19096,a20),x19097)))), % 59.46/59.52 inference(scs_inference,[],[1905,1300,1539,2,3])). % 59.46/59.52 cnf(1913,plain, % 59.46/59.52 (E(f2(f2(f2(x19131,a20,x19132),a20,x19133),f5(f5(x19134,f13(a16)),x19135),f9(f9(x19136,a20),x19137)),f2(f2(f2(x19131,f13(a16),x19132),f13(a16),x19133),f5(f5(x19134,f13(a16)),x19135),f9(f9(x19136,a20),x19137)))), % 59.46/59.52 inference(scs_inference,[],[1777,1909,1554,2,3])). % 59.46/59.52 cnf(1917,plain, % 59.46/59.52 (E(f2(f2(f2(x19171,a20,x19172),a20,x19173),f5(f5(x19174,f13(a16)),x19175),f9(f9(x19176,a20),x19177)),f2(f2(f2(x19171,f13(a16),x19172),f13(a16),x19173),f5(f5(x19174,a20),x19175),f9(f9(x19176,f13(a16)),x19177)))), % 59.46/59.52 inference(scs_inference,[],[1913,1530,1410,2,3])). % 59.46/59.52 cnf(1919,plain, % 59.46/59.52 (E(f13(f7(f13(a16))),f13(f7(a20)))), % 59.46/59.52 inference(scs_inference,[],[37,4,5])). % 59.46/59.52 cnf(1921,plain, % 59.46/59.52 (E(f2(f2(f2(x19211,a20,x19212),a20,x19213),f2(f2(x19214,f13(a16),x19215),x19216,x19217),f9(f9(x19218,a20),x19219)),f2(f2(f2(x19211,a20,x19212),a20,x19213),f2(f2(x19214,a20,x19215),x19216,x19217),f9(f9(x19218,f13(a16)),x19219)))), % 59.46/59.52 inference(scs_inference,[],[1917,1457,1634,2,3])). % 59.46/59.52 cnf(1924,plain, % 59.46/59.52 (E(f7(f4(f13(a16),x19241)),f7(f4(a20,x19241)))), % 59.46/59.52 inference(scs_inference,[],[37,4,6])). % 59.46/59.52 cnf(1926,plain, % 59.46/59.52 (E(f2(f2(f2(x19261,f13(a16),x19262),a20,x19263),f2(f2(x19264,a20,x19265),x19266,x19267),f9(f9(x19268,a20),x19269)),f2(f2(f2(x19261,a20,x19262),a20,x19263),f2(f2(x19264,a20,x19265),x19266,x19267),f9(f9(x19268,f13(a16)),x19269)))), % 59.46/59.52 inference(scs_inference,[],[1921,1908,2,3])). % 59.46/59.52 cnf(1928,plain, % 59.46/59.52 (E(f4(x19281,f7(f13(a16))),f4(x19281,f7(a20)))), % 59.46/59.52 inference(scs_inference,[],[37,4,7])). % 59.46/59.52 cnf(1929,plain, % 59.46/59.52 (E(f2(f2(f2(x19291,a20,x19292),a20,x19293),f2(f2(x19294,a20,x19295),x19296,x19297),f9(f9(x19298,f13(a16)),x19299)),f2(f2(f2(x19291,f13(a16),x19292),a20,x19293),f2(f2(x19294,a20,x19295),x19296,x19297),f9(f9(x19298,a20),x19299)))), % 59.46/59.52 inference(scs_inference,[],[1926,2])). % 59.46/59.52 cnf(1933,plain, % 59.46/59.52 (E(f7(f8(f13(a16))),f7(f8(a20)))), % 59.46/59.52 inference(scs_inference,[],[37,4,8])). % 59.46/59.52 cnf(1935,plain, % 59.46/59.52 (E(f2(f2(f2(x19351,a20,x19352),a20,x19353),f2(f2(x19354,a20,x19355),x19356,x19357),f9(f9(x19358,f13(a16)),x19359)),f2(f2(f2(x19351,a20,x19352),f13(a16),x19353),f2(f2(x19354,f13(a16),x19355),x19356,x19357),f9(f9(x19358,a20),x19359)))), % 59.46/59.52 inference(scs_inference,[],[1889,1929,1924,2,3])). % 59.46/59.52 cnf(1937,plain, % 59.46/59.52 (E(f12(f7(f13(a16)),x19371),f12(f7(a20),x19371))), % 59.46/59.52 inference(scs_inference,[],[37,4,9])). % 59.46/59.52 cnf(1939,plain, % 59.46/59.52 (E(f12(f7(f13(a16)),f2(f2(x19391,f13(a16),x19392),x19393,x19394)),f12(f7(a20),f2(f2(x19391,a20,x19392),x19393,x19394)))), % 59.46/59.52 inference(scs_inference,[],[1935,1937,1337,2,3])). % 59.46/59.52 cnf(1942,plain, % 59.46/59.52 (E(f7(f12(x19421,f13(a16))),f7(f12(x19421,a20)))), % 59.46/59.52 inference(scs_inference,[],[37,4,10])). % 59.46/59.52 cnf(1943,plain, % 59.46/59.52 (E(f7(f12(x19431,a20)),f7(f12(x19431,f13(a16))))), % 59.46/59.52 inference(scs_inference,[],[1942,2])). % 59.46/59.52 cnf(1944,plain, % 59.46/59.52 (E(f4(f2(f2(x19441,a20,x19442),x19443,x19444),f7(f13(a16))),f4(f2(f2(x19441,f13(a16),x19442),x19443,x19444),f7(a20)))), % 59.46/59.52 inference(scs_inference,[],[1942,1928,1314,2,3])). % 59.46/59.52 cnf(1952,plain, % 59.46/59.52 (E(f7(f9(x19521,f13(a16))),f7(f9(x19521,a20)))), % 59.46/59.52 inference(scs_inference,[],[37,4,12])). % 59.46/59.52 cnf(1954,plain, % 59.46/59.52 (E(f7(f9(f9(x19541,f13(a16)),f13(a16))),f7(f9(f9(x19541,a20),a20)))), % 59.46/59.52 inference(scs_inference,[],[679,1952,2,3])). % 59.46/59.52 cnf(1967,plain, % 59.46/59.52 (E(f14(f7(f13(a16))),f14(f7(a20)))), % 59.46/59.52 inference(scs_inference,[],[37,4,15])). % 59.46/59.52 cnf(1972,plain, % 59.46/59.52 (E(f7(f2(f13(a16),x19721,x19722)),f7(f2(a20,x19721,x19722)))), % 59.46/59.52 inference(scs_inference,[],[37,4,16])). % 59.46/59.52 cnf(1973,plain, % 59.46/59.52 (E(f7(f2(a20,x19731,x19732)),f7(f2(f13(a16),x19731,x19732)))), % 59.46/59.52 inference(scs_inference,[],[1972,2])). % 59.46/59.52 cnf(1977,plain, % 59.46/59.52 (E(f2(x19771,f7(f13(a16)),x19772),f2(x19771,f7(a20),x19772))), % 59.46/59.52 inference(scs_inference,[],[37,4,17])). % 59.46/59.52 cnf(1978,plain, % 59.46/59.52 (E(f2(x19781,f7(a20),x19782),f2(x19781,f7(f13(a16)),x19782))), % 59.46/59.52 inference(scs_inference,[],[1977,2])). % 59.46/59.52 cnf(1982,plain, % 59.46/59.52 (E(f7(f2(x19821,x19822,f13(a16))),f7(f2(x19821,x19822,a20)))), % 59.46/59.52 inference(scs_inference,[],[37,4,18])). % 59.46/59.52 cnf(1983,plain, % 59.46/59.52 (E(f7(f2(x19831,x19832,a20)),f7(f2(x19831,x19832,f13(a16))))), % 59.46/59.52 inference(scs_inference,[],[1982,2])). % 59.46/59.52 cnf(1984,plain, % 59.46/59.52 (E(f7(f2(f2(x19841,f13(a16),x19842),x19843,f13(a16))),f7(f2(f2(x19841,a20,x19842),x19843,a20)))), % 59.46/59.52 inference(scs_inference,[],[1305,1982,2,3])). % 59.46/59.52 cnf(1989,plain, % 59.46/59.52 (E(f7(f2(a20,x19891,a20)),f7(f2(f13(a16),x19891,f13(a16))))), % 59.46/59.52 inference(scs_inference,[],[1973,1983,1984,2,3])). % 59.46/59.52 cnf(2002,plain, % 59.46/59.52 (E(f7(f12(f13(a16),x20021)),f7(f12(a20,x20021)))), % 59.46/59.52 inference(scs_inference,[],[37,4,9])). % 59.46/59.52 cnf(2004,plain, % 59.46/59.52 (E(f7(f12(f13(a16),a20)),f7(f12(a20,f13(a16))))), % 59.46/59.52 inference(scs_inference,[],[1919,2002,1943,2,3])). % 59.46/59.52 cnf(2009,plain, % 59.46/59.52 (E(f2(f9(f9(x20091,a20),x20092),f7(a20),f5(f5(x20093,a20),x20094)),f2(f9(f9(x20091,f13(a16)),x20092),f7(f13(a16)),f5(f5(x20093,f13(a16)),x20094)))), % 59.46/59.52 inference(scs_inference,[],[2004,1978,1138,2,3])). % 59.46/59.52 cnf(2014,plain, % 59.46/59.52 (E(f2(f9(f9(x20141,f13(a16)),x20142),f7(a20),f5(f5(x20143,a20),x20144)),f2(f9(f9(x20141,f13(a16)),x20142),f7(f13(a16)),f5(f5(x20143,f13(a16)),x20144)))), % 59.46/59.52 inference(scs_inference,[],[2009,740,2,3])). % 59.46/59.52 cnf(2035,plain, % 59.46/59.52 (E(f7(f14(f13(a16))),f7(f14(a20)))), % 59.46/59.52 inference(scs_inference,[],[37,4,15])). % 59.46/59.52 cnf(2045,plain, % 59.46/59.52 (E(f7(f2(x20451,f13(a16),x20452)),f7(f2(x20451,a20,x20452)))), % 59.46/59.52 inference(scs_inference,[],[37,4,17])). % 59.46/59.52 cnf(2046,plain, % 59.46/59.52 (E(f7(f2(x20461,a20,x20462)),f7(f2(x20461,f13(a16),x20462)))), % 59.46/59.52 inference(scs_inference,[],[2045,2])). % 59.46/59.52 cnf(2050,plain, % 59.46/59.52 (E(f2(f7(f13(a16)),x20501,x20502),f2(f7(a20),x20501,x20502))), % 59.46/59.52 inference(scs_inference,[],[37,4,16])). % 59.46/59.52 cnf(2051,plain, % 59.46/59.52 (E(f2(f7(a20),x20511,x20512),f2(f7(f13(a16)),x20511,x20512))), % 59.46/59.52 inference(scs_inference,[],[2050,2])). % 59.46/59.52 cnf(2052,plain, % 59.46/59.52 (E(f2(f7(f13(a16)),f7(a20),x20521),f2(f7(a20),f7(f13(a16)),x20521))), % 59.46/59.52 inference(scs_inference,[],[2050,1978,2,3])). % 59.46/59.52 cnf(2057,plain, % 59.46/59.52 (E(f7(f2(a20,a20,a20)),f7(f2(f13(a16),f13(a16),f13(a16))))), % 59.46/59.52 inference(scs_inference,[],[2046,1933,1989,2,3])). % 59.46/59.52 cnf(2060,plain, % 59.46/59.52 (E(f2(x20601,x20602,f7(f13(a16))),f2(x20601,x20602,f7(a20)))), % 59.46/59.52 inference(scs_inference,[],[37,4,18])). % 59.46/59.52 cnf(2061,plain, % 59.46/59.52 (E(f2(x20611,x20612,f7(a20)),f2(x20611,x20612,f7(f13(a16))))), % 59.46/59.52 inference(scs_inference,[],[2060,2])). % 59.46/59.52 cnf(2062,plain, % 59.46/59.52 (E(f2(f7(a20),x20621,f7(f13(a16))),f2(f7(f13(a16)),x20621,f7(a20)))), % 59.46/59.52 inference(scs_inference,[],[2060,2051,2,3])). % 59.46/59.52 cnf(2067,plain, % 59.46/59.52 (E(f7(f2(f13(a16),a20,a20)),f7(f2(f13(a16),f13(a16),f13(a16))))), % 59.46/59.52 inference(scs_inference,[],[1967,2057,1972,2,3])). % 59.46/59.52 cnf(2070,plain, % 59.46/59.52 (E(f7(f2(f13(a16),f13(a16),f13(a16))),f7(f2(f13(a16),a20,a20)))), % 59.46/59.52 inference(scs_inference,[],[2067,2])). % 59.46/59.52 cnf(2071,plain, % 59.46/59.52 (E(f2(f7(f13(a16)),f7(a20),f7(a20)),f2(f7(a20),f7(f13(a16)),f7(f13(a16))))), % 59.46/59.52 inference(scs_inference,[],[2061,2067,2052,2,3])). % 59.46/59.52 cnf(2086,plain, % 59.46/59.52 (E(f2(f7(f13(a16)),f7(a20),f7(a20)),f2(f7(f13(a16)),f7(f13(a16)),f7(f13(a16))))), % 59.46/59.52 inference(scs_inference,[],[2035,2071,2051,2,3])). % 59.46/59.52 cnf(2090,plain, % 59.46/59.52 (E(f2(f7(f13(a16)),f7(f13(a16)),f7(f13(a16))),f2(f7(f13(a16)),f7(a20),f7(a20)))), % 59.46/59.52 inference(scs_inference,[],[2086,2])). % 59.46/59.52 cnf(2091,plain, % 59.46/59.52 (E(f2(f7(a20),f7(a20),f7(f13(a16))),f2(f7(f13(a16)),f7(f13(a16)),f7(f13(a16))))), % 59.46/59.52 inference(scs_inference,[],[2086,2062,2,3])). % 59.46/59.52 cnf(2107,plain, % 59.46/59.52 (E(f7(f2(a20,a20,x21071)),f7(f2(f13(a16),f13(a16),x21071)))), % 59.46/59.52 inference(scs_inference,[],[1944,1973,2046,2,3])). % 59.46/59.52 cnf(2112,plain, % 59.46/59.52 (E(f7(f2(a20,a20,f13(a16))),f7(f2(f13(a16),a20,a20)))), % 59.46/59.52 inference(scs_inference,[],[1939,2107,2070,2,3])). % 59.46/59.52 cnf(2146,plain, % 59.46/59.52 (E(f2(f7(f13(a16)),f7(f13(a16)),f7(f13(a16))),f2(f7(a20),f7(f13(a16)),f7(a20)))), % 59.46/59.52 inference(scs_inference,[],[2090,2112,2052,2,3])). % 59.46/59.52 cnf(2148,plain, % 59.46/59.52 (E(f2(f7(a20),f7(f13(a16)),f7(a20)),f2(f7(f13(a16)),f7(f13(a16)),f7(f13(a16))))), % 59.46/59.52 inference(scs_inference,[],[2146,2])). % 59.46/59.52 cnf(2149,plain, % 59.46/59.52 (E(f2(f7(a20),f7(a20),f7(f13(a16))),f2(f7(a20),f7(f13(a16)),f7(a20)))), % 59.46/59.52 inference(scs_inference,[],[2146,2091,2,3])). % 59.46/59.52 cnf(2152,plain, % 59.46/59.52 (E(f2(f7(a20),f7(f13(a16)),f7(a20)),f2(f7(f13(a16)),f7(a20),f7(a20)))), % 59.46/59.52 inference(scs_inference,[],[2149,2148,2090,2,3])). % 59.46/59.52 cnf(2155,plain, % 59.46/59.52 (E(f2(f9(f9(x21551,f13(a16)),x21552),f7(a20),f5(f5(x21553,a20),x21554)),f2(f9(f9(x21551,a20),x21552),f7(f13(a16)),f5(f5(x21553,a20),x21554)))), % 59.46/59.52 inference(scs_inference,[],[1954,2014,1142,2,3])). % 59.46/59.52 cnf(2159,plain, % 59.46/59.52 (E(f2(f2(f2(x21591,f13(a16),x21592),f13(a16),x21593),f5(f5(x21594,f13(a16)),x21595),f9(f9(x21596,a20),x21597)),f2(f2(f2(x21591,a20,x21592),a20,x21593),f5(f5(x21594,a20),x21595),f9(f9(x21596,a20),x21597)))), % 59.46/59.52 inference(scs_inference,[],[2155,1311,1444,2,3])). % 59.46/59.52 cnf(2163,plain, % 59.46/59.52 (E(f7(f2(f13(a16),a20,a20)),f7(f2(a20,f13(a16),f13(a16))))), % 59.46/59.52 inference(scs_inference,[],[2159,2067,1972,2,3])). % 59.46/59.52 cnf(2183,plain, % 59.46/59.52 (E(f2(f14(f13(a16)),x21831,x21832),f2(f14(a20),x21831,x21832))), % 59.46/59.52 inference(scs_inference,[],[55,562,4,5,8,15,19,6,7,9,10,11,12,13,14,16])). % 59.46/59.52 cnf(2184,plain, % 59.46/59.52 (E(f2(x21841,f14(f13(a16)),x21842),f2(x21841,f14(a20),x21842))), % 59.46/59.52 inference(scs_inference,[],[55,562,4,5,8,15,19,6,7,9,10,11,12,13,14,16,17])). % 59.46/59.52 cnf(2193,plain, % 59.46/59.52 (P1(f12(a21,f9(f13(a6),f12(f7(a22),f8(a20)))),f14(f5(a11,a23)),a18)), % 59.46/59.52 inference(scs_inference,[],[23,55,562,2163,39,1982,238,4,5,8,15,19,6,7,9,10,11,12,13,14,16,17,18,30,26,20,3,27])). % 59.46/59.52 cnf(2220,plain, % 59.46/59.52 (P1(f12(f7(a22),f8(a20)),f14(f5(a11,a23)),a18)), % 59.46/59.52 inference(scs_inference,[],[567,244,2183,2184,2193,5,4,10,9,12,11,14,17,7,16,13,8,19,15,6,18,27,3,28])). % 59.46/59.52 cnf(2223,plain, % 59.46/59.52 (~P1(f8(a20),f14(f5(a11,a23)),a18)), % 59.46/59.52 inference(scs_inference,[],[24,567,244,2183,2184,2193,238,38,5,4,10,9,12,11,14,17,7,16,13,8,19,15,6,18,27,3,28,21,20])). % 59.46/59.52 cnf(2233,plain, % 59.46/59.52 ($false), % 59.46/59.52 inference(scs_inference,[],[2223,239,2220,2152,4,5,7,17,10,27]), % 59.46/59.52 ['proof']). % 59.46/59.52 % SZS output end Proof % 59.46/59.52 % Total time :58.870000s %------------------------------------------------------------------------------