%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SWV352-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 : n027.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:55 EDT 2024 % Result : Unsatisfiable 60.13s 60.22s % Output : CNFRefutation 60.25s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SWV352-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 : n027.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 17:47:24 EDT 2024 % 0.12/0.34 % CPUTime : % 0.45/0.60 start to proof:theBenchmark % 60.13/60.20 %------------------------------------------- % 60.13/60.21 % File :CSE---1.7 % 60.13/60.21 % Problem :theBenchmark % 60.13/60.21 % Transform :cnf % 60.13/60.21 % Format :tptp:raw % 60.13/60.21 % Command :java -jar mcs_scs.jar %d %s % 60.13/60.21 % 60.13/60.21 % Result :Theorem 59.580000s % 60.13/60.21 % Output :CNFRefutation 59.580000s % 60.13/60.21 %------------------------------------------- % 60.13/60.22 %------------------------------------------------------------------------------ % 60.13/60.22 % File : SWV352-2 : TPTP v8.2.0. Released v3.2.0. % 60.13/60.22 % Domain : Software Verification (Security) % 60.13/60.22 % Problem : Cryptographic protocol problem for Yahalom % 60.13/60.22 % Version : [Pau06] axioms : Reduced > Especial. % 60.13/60.22 % English : % 60.13/60.22 % 60.13/60.22 % Refs : [Pau06] Paulson (2006), Email to G. Sutcliffe % 60.13/60.22 % Source : [Pau06] % 60.13/60.22 % Names : % 60.13/60.22 % 60.13/60.22 % Status : Unsatisfiable % 60.13/60.22 % Rating : 0.00 v7.0.0, 0.14 v6.3.0, 0.17 v6.2.0, 0.00 v5.5.0, 0.12 v5.4.0, 0.07 v5.3.0, 0.17 v5.2.0, 0.00 v5.0.0, 0.14 v4.1.0, 0.33 v4.0.1, 0.17 v3.3.0, 0.14 v3.2.0 % 60.13/60.22 % Syntax : Number of clauses : 11 ( 5 unt; 0 nHn; 10 RR) % 60.13/60.22 % Number of literals : 21 ( 1 equ; 11 neg) % 60.13/60.22 % Maximal clause size : 4 ( 1 avg) % 60.13/60.22 % Maximal term depth : 8 ( 2 avg) % 60.13/60.22 % Number of predicates : 2 ( 1 usr; 0 prp; 2-3 aty) % 60.13/60.22 % Number of functors : 28 ( 28 usr; 15 con; 0-3 aty) % 60.13/60.22 % Number of variables : 28 ( 12 sgn) % 60.13/60.22 % SPC : CNF_UNS_RFO_SEQ_HRN % 60.13/60.22 % 60.13/60.22 % Comments : The problems in the [Pau06] collection each have very many axioms, % 60.13/60.22 % of which only a small selection are required for the refutation. % 60.13/60.22 % The mission is to find those few axioms, after which a refutation % 60.13/60.22 % can be quite easily found. This version has only the necessary % 60.13/60.22 % axioms. % 60.13/60.22 %------------------------------------------------------------------------------ % 60.13/60.22 cnf(cls_conjecture_2,negated_conjecture, % 60.13/60.22 c_in(v_evso,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)) ). % 60.13/60.22 % 60.13/60.22 cnf(cls_conjecture_3,negated_conjecture, % 60.13/60.22 c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_Aa,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(v_K),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NBa))))),v_X)),c_List_Oset(v_evso,tc_Event_Oevent),tc_Event_Oevent) ). % 60.13/60.22 % 60.13/60.22 cnf(cls_conjecture_5,negated_conjecture, % 60.13/60.22 c_in(c_Event_Oevent_OSays(v_B,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OCrypt(c_Public_OshrK(v_B),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_ONonce(v_NB)))))),c_List_Oset(v_evso,tc_Event_Oevent),tc_Event_Oevent) ). % 60.13/60.22 % 60.13/60.22 cnf(cls_conjecture_6,negated_conjecture, % 60.13/60.22 ~ c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evso)),tc_Message_Omsg) ). % 60.13/60.22 % 60.13/60.22 cnf(cls_Event_OSays__imp__spies_0,axiom, % 60.13/60.22 ( ~ c_in(c_Event_Oevent_OSays(V_A,V_B,V_X),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent) % 60.13/60.22 | c_in(V_X,c_Event_Oknows(c_Message_Oagent_OSpy,V_evs),tc_Message_Omsg) ) ). % 60.13/60.22 % 60.13/60.22 cnf(cls_Message_OMPair__parts_0,axiom, % 60.13/60.22 ( ~ c_in(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Oparts(V_H),tc_Message_Omsg) % 60.13/60.22 | c_in(V_Y,c_Message_Oparts(V_H),tc_Message_Omsg) ) ). % 60.13/60.22 % 60.13/60.22 cnf(cls_Message_Oparts_OInj_0,axiom, % 60.13/60.22 ( ~ c_in(V_X,V_H,tc_Message_Omsg) % 60.13/60.22 | c_in(V_X,c_Message_Oparts(V_H),tc_Message_Omsg) ) ). % 60.13/60.22 % 60.13/60.22 cnf(cls_Message_Oparts__analz_0,axiom, % 60.13/60.22 c_Message_Oparts(c_Message_Oanalz(V_H)) = c_Message_Oparts(V_H) ). % 60.13/60.22 % 60.13/60.22 cnf(cls_Yahalom_OGets__imp__analz__Spy__dest_0,axiom, % 60.13/60.22 ( ~ c_in(V_evs,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)) % 60.13/60.22 | ~ c_in(c_Event_Oevent_OGets(V_B,V_X),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent) % 60.13/60.22 | c_in(V_X,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg) ) ). % 60.13/60.22 % 60.13/60.22 cnf(cls_Yahalom_OSays__Server__imp__YM2_0,axiom, % 60.13/60.22 ( ~ c_in(V_evs,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)) % 60.13/60.22 | ~ c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,V_A,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(V_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_B),c_Message_Omsg_OMPair(V_k,c_Message_Omsg_OMPair(V_na,V_nb)))),V_X)),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent) % 60.13/60.22 | c_in(c_Event_Oevent_OGets(c_Message_Oagent_OServer,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_B),c_Message_Omsg_OCrypt(c_Public_OshrK(V_B),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_A),c_Message_Omsg_OMPair(V_na,V_nb))))),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent) ) ). % 60.13/60.22 % 60.13/60.22 cnf(cls_Yahalom_Ono__nonce__YM1__YM2_0,axiom, % 60.13/60.22 ( ~ c_in(V_evs,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)) % 60.13/60.22 | ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(V_B),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_A),c_Message_Omsg_OMPair(V_na,c_Message_Omsg_ONonce(V_NB)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg) % 60.13/60.22 | ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(V_B_H),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_A_H),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(V_NB),V_nb_H))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg) % 60.13/60.22 | c_in(c_Message_Omsg_ONonce(V_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg) ) ). % 60.13/60.22 % 60.13/60.22 %------------------------------------------------------------------------------ % 60.13/60.22 %------------------------------------------- % 60.13/60.22 % Proof found % 60.13/60.22 % SZS status Theorem for theBenchmark % 60.13/60.22 % SZS output start Proof % 60.13/60.22 %ClaNum:37(EqnAxiom:26) % 60.13/60.22 %VarNum:51(SingletonVarNum:28) % 60.13/60.22 %MaxLitNum:4 % 60.13/60.22 %MaxfuncDepth:7 % 60.13/60.22 %SharedTerms:43 % 60.13/60.22 %goalClause: 28 29 30 31 % 60.13/60.22 %singleGoalClaCount:4 % 60.13/60.22 [28]P1(a14,a15,f18(a17)) % 60.13/60.22 [31]~P1(f10(a26),f1(f6(a7,a14)),a21) % 60.13/60.22 [29]P1(f3(a19,a2,f11(f9(a19),f12(f16(a19),f11(f9(a20),f11(f10(a23),f10(a26)))))),f5(a14,a17),a17) % 60.13/60.22 [30]P1(f3(a2,a22,f11(f12(f16(a22),f11(f9(a24),f11(f13(a25),f11(f10(a26),f10(a27))))),a28)),f5(a14,a17),a17) % 60.13/60.22 [27]E(f8(f1(x271)),f8(x271)) % 60.13/60.22 [32]~P1(x321,x322,a21)+P1(x321,f8(x322),a21) % 60.13/60.22 [33]P1(x331,f8(x332),a21)+~P1(f11(x333,x331),f8(x332),a21) % 60.13/60.22 [35]P1(x351,f6(a7,x352),a21)+~P1(f3(x353,x354,x351),f5(x352,a17),a17) % 60.13/60.22 [34]~P1(f4(x343,x341),f5(x342,a17),a17)+~P1(x342,a15,f18(a17))+P1(x341,f1(f6(a7,x342)),a21) % 60.13/60.22 [37]~P1(x375,a15,f18(a17))+P1(f4(a2,f11(f9(x371),f12(f16(x371),f11(f9(x372),f11(x373,x374))))),f5(x375,a17),a17)+~P1(f3(a2,x372,f11(f12(f16(x372),f11(f9(x371),f11(x376,f11(x373,x374)))),x377)),f5(x375,a17),a17) % 60.13/60.22 [36]~P1(x362,a15,f18(a17))+P1(f10(x361),f1(f6(a7,x362)),a21)+~P1(f12(f16(x363),f11(f9(x364),f11(x365,f10(x361)))),f8(f6(a7,x362)),a21)+~P1(f12(f16(x366),f11(f9(x367),f11(f10(x361),x368))),f8(f6(a7,x362)),a21) % 60.13/60.22 %EqnAxiom % 60.13/60.22 [1]E(x11,x11) % 60.13/60.22 [2]E(x22,x21)+~E(x21,x22) % 60.13/60.22 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 60.13/60.22 [4]~E(x41,x42)+E(f1(x41),f1(x42)) % 60.13/60.23 [5]~E(x51,x52)+E(f8(x51),f8(x52)) % 60.13/60.23 [6]~E(x61,x62)+E(f12(x61,x63),f12(x62,x63)) % 60.13/60.23 [7]~E(x71,x72)+E(f12(x73,x71),f12(x73,x72)) % 60.13/60.23 [8]~E(x81,x82)+E(f18(x81),f18(x82)) % 60.13/60.23 [9]~E(x91,x92)+E(f9(x91),f9(x92)) % 60.13/60.23 [10]~E(x101,x102)+E(f16(x101),f16(x102)) % 60.13/60.23 [11]~E(x111,x112)+E(f10(x111),f10(x112)) % 60.13/60.23 [12]~E(x121,x122)+E(f4(x121,x123),f4(x122,x123)) % 60.13/60.23 [13]~E(x131,x132)+E(f4(x133,x131),f4(x133,x132)) % 60.13/60.23 [14]~E(x141,x142)+E(f11(x141,x143),f11(x142,x143)) % 60.13/60.23 [15]~E(x151,x152)+E(f11(x153,x151),f11(x153,x152)) % 60.13/60.23 [16]~E(x161,x162)+E(f6(x161,x163),f6(x162,x163)) % 60.13/60.23 [17]~E(x171,x172)+E(f6(x173,x171),f6(x173,x172)) % 60.13/60.23 [18]~E(x181,x182)+E(f3(x181,x183,x184),f3(x182,x183,x184)) % 60.13/60.23 [19]~E(x191,x192)+E(f3(x193,x191,x194),f3(x193,x192,x194)) % 60.13/60.23 [20]~E(x201,x202)+E(f3(x203,x204,x201),f3(x203,x204,x202)) % 60.13/60.23 [21]~E(x211,x212)+E(f5(x211,x213),f5(x212,x213)) % 60.13/60.23 [22]~E(x221,x222)+E(f5(x223,x221),f5(x223,x222)) % 60.13/60.23 [23]~E(x231,x232)+E(f13(x231),f13(x232)) % 60.13/60.23 [24]P1(x242,x243,x244)+~E(x241,x242)+~P1(x241,x243,x244) % 60.13/60.23 [25]P1(x253,x252,x254)+~E(x251,x252)+~P1(x253,x251,x254) % 60.13/60.23 [26]P1(x263,x264,x262)+~E(x261,x262)+~P1(x263,x264,x261) % 60.13/60.23 % 60.13/60.23 %------------------------------------------- % 60.25/60.24 cnf(38,plain, % 60.25/60.24 (E(f8(x381),f8(f1(x381)))), % 60.25/60.24 inference(scs_inference,[],[27,2])). % 60.25/60.24 cnf(41,plain, % 60.25/60.24 (~E(f3(a19,a2,f11(f9(a19),f12(f16(a19),f11(f9(a20),f11(f10(a23),f10(a26)))))),f4(x411,f10(a26)))), % 60.25/60.24 inference(scs_inference,[],[28,31,29,27,2,34,24])). % 60.25/60.24 cnf(57,plain, % 60.25/60.24 (E(f1(f8(f1(x571))),f1(f8(x571)))), % 60.25/60.24 inference(scs_inference,[],[38,4,2])). % 60.25/60.24 cnf(59,plain, % 60.25/60.24 (P1(f4(a2,f11(f9(a24),f12(f16(a24),f11(f9(a22),f11(f10(a26),f10(a27)))))),f5(a14,a17),a17)), % 60.25/60.24 inference(scs_inference,[],[28,30,57,2,37])). % 60.25/60.24 cnf(67,plain, % 60.25/60.24 (E(f8(f12(f8(x671),x672)),f8(f12(f8(f1(x671)),x672)))), % 60.25/60.24 inference(scs_inference,[],[38,5,6])). % 60.25/60.24 cnf(68,plain, % 60.25/60.24 (E(f8(f12(f8(f1(x681)),x682)),f8(f12(f8(x681),x682)))), % 60.25/60.24 inference(scs_inference,[],[67,2])). % 60.25/60.24 cnf(69,plain, % 60.25/60.24 (E(f8(f1(f12(f8(x691),x692))),f8(f12(f8(f1(x691)),x692)))), % 60.25/60.24 inference(scs_inference,[],[27,67,2,3])). % 60.25/60.24 cnf(73,plain, % 60.25/60.24 (E(f8(f1(f12(f8(f1(x731)),x732))),f8(f12(f8(x731),x732)))), % 60.25/60.24 inference(scs_inference,[],[27,68,69,2,3])). % 60.25/60.24 cnf(75,plain, % 60.25/60.24 (E(f9(f16(f8(x751))),f9(f16(f8(f1(x751)))))), % 60.25/60.24 inference(scs_inference,[],[38,9,10])). % 60.25/60.24 cnf(79,plain, % 60.25/60.24 (E(f10(f4(f8(x791),x792)),f10(f4(f8(f1(x791)),x792)))), % 60.25/60.24 inference(scs_inference,[],[38,11,12])). % 60.25/60.24 cnf(83,plain, % 60.25/60.24 (E(f13(f4(x831,f8(x832))),f13(f4(x831,f8(f1(x832)))))), % 60.25/60.24 inference(scs_inference,[],[38,23,13])). % 60.25/60.24 cnf(87,plain, % 60.25/60.24 (P1(f11(f9(a19),f12(f16(a19),f11(f9(a20),f11(f10(a23),f10(a26))))),f8(f6(a7,a14)),a21)), % 60.25/60.24 inference(scs_inference,[],[29,32,35])). % 60.25/60.24 cnf(89,plain, % 60.25/60.24 (P1(f11(f9(a19),f12(f16(a19),f11(f9(a20),f11(f10(a23),f10(a26))))),f8(f1(f6(a7,a14))),a21)), % 60.25/60.24 inference(scs_inference,[],[38,75,87,2,25])). % 60.25/60.24 cnf(99,plain, % 60.25/60.24 (E(f11(f11(x991,f8(x992)),x993),f11(f11(x991,f8(f1(x992))),x993))), % 60.25/60.24 inference(scs_inference,[],[38,14,15])). % 60.25/60.24 cnf(107,plain, % 60.25/60.24 (E(f13(f4(x1071,f8(f1(x1072)))),f13(f4(x1071,f8(x1072))))), % 60.25/60.24 inference(scs_inference,[],[83,2])). % 60.25/60.24 cnf(108,plain, % 60.25/60.24 (P1(f11(f9(a19),f12(f16(a19),f11(f9(a20),f11(f10(a23),f10(a26))))),f8(f1(f1(f6(a7,a14)))),a21)), % 60.25/60.24 inference(scs_inference,[],[89,38,83,2,25])). % 60.25/60.24 cnf(116,plain, % 60.25/60.24 (E(f11(f11(x1161,f8(f1(x1162))),x1163),f11(f11(x1161,f8(x1162)),x1163))), % 60.25/60.24 inference(scs_inference,[],[99,2])). % 60.25/60.24 cnf(117,plain, % 60.25/60.24 (P1(f11(f9(a19),f12(f16(a19),f11(f9(a20),f11(f10(a23),f10(a26))))),f8(f1(f1(f1(f6(a7,a14))))),a21)), % 60.25/60.24 inference(scs_inference,[],[38,99,108,2,25])). % 60.25/60.24 cnf(176,plain, % 60.25/60.24 (E(f12(x1761,f8(f12(f8(f1(x1762)),x1763))),f12(x1761,f8(f1(f12(f8(x1762),x1763)))))), % 60.25/60.24 inference(scs_inference,[],[69,2,7])). % 60.25/60.24 cnf(192,plain, % 60.25/60.24 (E(f10(f8(f12(f8(f1(x1921)),x1922))),f10(f8(f1(f12(f8(x1921),x1922)))))), % 60.25/60.24 inference(scs_inference,[],[69,2,11])). % 60.25/60.24 cnf(262,plain, % 60.25/60.24 (E(f12(x2621,f10(f4(f8(f1(x2622)),x2623))),f12(x2621,f10(f4(f8(x2622),x2623))))), % 60.25/60.24 inference(scs_inference,[],[79,2,7])). % 60.25/60.24 cnf(263,plain, % 60.25/60.24 (E(f12(x2631,f10(f4(f8(x2632),x2633))),f12(x2631,f10(f4(f8(f1(x2632)),x2633))))), % 60.25/60.24 inference(scs_inference,[],[262,2])). % 60.25/60.24 cnf(281,plain, % 60.25/60.24 (E(f3(f13(f4(x2811,f8(f1(x2812)))),x2813,x2814),f3(f13(f4(x2811,f8(x2812))),x2813,x2814))), % 60.25/60.24 inference(scs_inference,[],[83,2,18])). % 60.25/60.24 cnf(282,plain, % 60.25/60.24 (E(f3(f13(f4(x2821,f8(x2822))),x2823,x2824),f3(f13(f4(x2821,f8(f1(x2822)))),x2823,x2824))), % 60.25/60.24 inference(scs_inference,[],[281,2])). % 60.25/60.24 cnf(285,plain, % 60.25/60.24 (E(f3(x2851,x2852,f13(f4(x2853,f8(f1(x2854))))),f3(x2851,x2852,f13(f4(x2853,f8(x2854)))))), % 60.25/60.24 inference(scs_inference,[],[83,2,20])). % 60.25/60.24 cnf(286,plain, % 60.25/60.24 (E(f3(x2861,x2862,f13(f4(x2863,f8(x2864)))),f3(x2861,x2862,f13(f4(x2863,f8(f1(x2864))))))), % 60.25/60.24 inference(scs_inference,[],[285,2])). % 60.25/60.24 cnf(287,plain, % 60.25/60.24 (E(f5(f13(f4(x2871,f8(f1(x2872)))),x2873),f5(f13(f4(x2871,f8(x2872))),x2873))), % 60.25/60.24 inference(scs_inference,[],[83,2,21])). % 60.25/60.24 cnf(288,plain, % 60.25/60.24 (E(f5(f13(f4(x2881,f8(x2882))),x2883),f5(f13(f4(x2881,f8(f1(x2882)))),x2883))), % 60.25/60.24 inference(scs_inference,[],[287,2])). % 60.25/60.24 cnf(334,plain, % 60.25/60.24 (E(f11(f13(f4(x3341,f8(x3342))),x3343),f11(f13(f4(x3341,f8(f1(x3342)))),x3343))), % 60.25/60.24 inference(scs_inference,[],[107,2,14])). % 60.25/60.24 cnf(335,plain, % 60.25/60.24 (E(f11(f13(f4(x3351,f8(f1(x3352)))),x3353),f11(f13(f4(x3351,f8(x3352))),x3353))), % 60.25/60.24 inference(scs_inference,[],[334,2])). % 60.25/60.24 cnf(523,plain, % 60.25/60.24 (E(f11(f8(f12(f8(x5231),x5232)),x5233),f11(f8(f1(f12(f8(f1(x5231)),x5232))),x5233))), % 60.25/60.24 inference(scs_inference,[],[73,2,14])). % 60.25/60.24 cnf(524,plain, % 60.25/60.24 (E(f11(f8(f1(f12(f8(f1(x5241)),x5242))),x5243),f11(f8(f12(f8(x5241),x5242)),x5243))), % 60.25/60.24 inference(scs_inference,[],[523,2])). % 60.25/60.24 cnf(747,plain, % 60.25/60.24 (E(f4(f8(f12(f8(f1(x7471)),x7472)),x7473),f4(f8(f1(f12(f8(x7471),x7472))),x7473))), % 60.25/60.24 inference(scs_inference,[],[69,2,12])). % 60.25/60.24 cnf(748,plain, % 60.25/60.24 (E(f4(f8(f1(f12(f8(x7481),x7482))),x7483),f4(f8(f12(f8(f1(x7481)),x7482)),x7483))), % 60.25/60.24 inference(scs_inference,[],[747,2])). % 60.25/60.24 cnf(750,plain, % 60.25/60.24 (E(f11(x7501,f8(f12(f8(x7502),x7503))),f11(x7501,f8(f1(f12(f8(f1(x7502)),x7503)))))), % 60.25/60.24 inference(scs_inference,[],[73,2,15])). % 60.25/60.24 cnf(751,plain, % 60.25/60.24 (E(f11(x7511,f8(f1(f12(f8(f1(x7512)),x7513)))),f11(x7511,f8(f12(f8(x7512),x7513))))), % 60.25/60.24 inference(scs_inference,[],[750,2])). % 60.25/60.24 cnf(755,plain, % 60.25/60.24 (E(f11(f8(f12(f8(f1(x7551)),x7552)),x7553),f11(f8(f1(f12(f8(x7551),x7552))),x7553))), % 60.25/60.24 inference(scs_inference,[],[69,2,14])). % 60.25/60.24 cnf(756,plain, % 60.25/60.24 (E(f11(f8(f1(f12(f8(x7561),x7562))),x7563),f11(f8(f12(f8(f1(x7561)),x7562)),x7563))), % 60.25/60.24 inference(scs_inference,[],[755,2])). % 60.25/60.24 cnf(758,plain, % 60.25/60.24 (E(f8(f8(x7581)),f8(f8(f1(x7581))))), % 60.25/60.24 inference(scs_inference,[],[27,2,5])). % 60.25/60.24 cnf(759,plain, % 60.25/60.24 (E(f8(f8(f1(x7591))),f8(f8(x7591)))), % 60.25/60.24 inference(scs_inference,[],[758,2])). % 60.25/60.24 cnf(760,plain, % 60.25/60.24 (E(f8(f1(f8(x7601))),f8(f8(f1(x7601))))), % 60.25/60.24 inference(scs_inference,[],[27,758,2,3])). % 60.25/60.24 cnf(762,plain, % 60.25/60.24 (E(f10(f8(x7621)),f10(f8(f1(x7621))))), % 60.25/60.24 inference(scs_inference,[],[27,2,11])). % 60.25/60.24 cnf(763,plain, % 60.25/60.24 (E(f8(f8(f1(x7631))),f8(f1(f8(x7631))))), % 60.25/60.24 inference(scs_inference,[],[760,2])). % 60.25/60.24 cnf(764,plain, % 60.25/60.24 (E(f8(f1(f8(f1(x7641)))),f8(f8(x7641)))), % 60.25/60.24 inference(scs_inference,[],[27,759,760,2,3])). % 60.25/60.24 cnf(766,plain, % 60.25/60.24 (E(f4(x7661,f8(x7662)),f4(x7661,f8(f1(x7662))))), % 60.25/60.24 inference(scs_inference,[],[27,2,13])). % 60.25/60.24 cnf(768,plain, % 60.25/60.24 (E(f8(f1(f1(f8(f1(x7681))))),f8(f8(x7681)))), % 60.25/60.24 inference(scs_inference,[],[27,764,2,3])). % 60.25/60.24 cnf(770,plain, % 60.25/60.24 (E(f6(f8(x7701),x7702),f6(f8(f1(x7701)),x7702))), % 60.25/60.24 inference(scs_inference,[],[27,2,16])). % 60.25/60.24 cnf(771,plain, % 60.25/60.24 (E(f8(f8(x7711)),f8(f1(f1(f8(f1(x7711))))))), % 60.25/60.24 inference(scs_inference,[],[768,2])). % 60.25/60.24 cnf(772,plain, % 60.25/60.24 (E(f8(f1(f1(f1(f8(f1(x7721)))))),f8(f8(x7721)))), % 60.25/60.24 inference(scs_inference,[],[27,768,2,3])). % 60.25/60.24 cnf(774,plain, % 60.25/60.24 (E(f6(x7741,f8(x7742)),f6(x7741,f8(f1(x7742))))), % 60.25/60.24 inference(scs_inference,[],[27,2,17])). % 60.25/60.24 cnf(776,plain, % 60.25/60.24 (E(f8(f1(f1(f1(f1(f8(f1(x7761))))))),f8(f8(x7761)))), % 60.25/60.24 inference(scs_inference,[],[27,772,2,3])). % 60.25/60.24 cnf(778,plain, % 60.25/60.24 (E(f3(f8(x7781),x7782,x7783),f3(f8(f1(x7781)),x7782,x7783))), % 60.25/60.24 inference(scs_inference,[],[27,2,18])). % 60.25/60.24 cnf(780,plain, % 60.25/60.24 (E(f8(f1(f8(f1(x7801)))),f8(f1(f8(x7801))))), % 60.25/60.24 inference(scs_inference,[],[27,776,763,2,3])). % 60.25/60.24 cnf(782,plain, % 60.25/60.24 (E(f3(x7821,f8(x7822),x7823),f3(x7821,f8(f1(x7822)),x7823))), % 60.25/60.24 inference(scs_inference,[],[27,2,19])). % 60.25/60.24 cnf(783,plain, % 60.25/60.24 (E(f10(f8(f1(x7831))),f10(f8(x7831)))), % 60.25/60.24 inference(scs_inference,[],[762,2])). % 60.25/60.24 cnf(784,plain, % 60.25/60.24 (E(f4(f8(f1(f12(f8(x7841),x7842))),f8(x7843)),f4(f8(f12(f8(f1(x7841)),x7842)),f8(f1(x7843))))), % 60.25/60.24 inference(scs_inference,[],[762,766,748,2,3])). % 60.25/60.24 cnf(787,plain, % 60.25/60.24 (E(f3(x7871,x7872,f8(x7873)),f3(x7871,x7872,f8(f1(x7873))))), % 60.25/60.24 inference(scs_inference,[],[27,2,20])). % 60.25/60.24 cnf(788,plain, % 60.25/60.24 (E(f6(f8(f1(x7881)),x7882),f6(f8(x7881),x7882))), % 60.25/60.24 inference(scs_inference,[],[770,2])). % 60.25/60.24 cnf(789,plain, % 60.25/60.24 (E(f10(f8(f12(f8(f1(x7891)),x7892))),f10(f8(f12(f8(x7891),x7892))))), % 60.25/60.24 inference(scs_inference,[],[192,783,770,2,3])). % 60.25/60.24 cnf(791,plain, % 60.25/60.24 (E(f5(f8(x7911),x7912),f5(f8(f1(x7911)),x7912))), % 60.25/60.24 inference(scs_inference,[],[27,2,21])). % 60.25/60.24 cnf(792,plain, % 60.25/60.24 (E(f6(x7921,f8(f1(x7922))),f6(x7921,f8(x7922)))), % 60.25/60.24 inference(scs_inference,[],[774,2])). % 60.25/60.24 cnf(793,plain, % 60.25/60.24 (E(f6(f8(f1(x7931)),f8(x7932)),f6(f8(x7931),f8(f1(x7932))))), % 60.25/60.24 inference(scs_inference,[],[788,774,2,3])). % 60.25/60.24 cnf(796,plain, % 60.25/60.24 (E(f5(x7961,f8(x7962)),f5(x7961,f8(f1(x7962))))), % 60.25/60.24 inference(scs_inference,[],[27,2,22])). % 60.25/60.24 cnf(797,plain, % 60.25/60.24 (E(f3(f8(f1(x7971)),x7972,x7973),f3(f8(x7971),x7972,x7973))), % 60.25/60.24 inference(scs_inference,[],[778,2])). % 60.25/60.24 cnf(798,plain, % 60.25/60.24 (E(f3(f8(x7981),f8(x7982),x7983),f3(f8(f1(x7981)),f8(f1(x7982)),x7983))), % 60.25/60.24 inference(scs_inference,[],[778,782,2,3])). % 60.25/60.24 cnf(801,plain, % 60.25/60.24 (E(f13(f8(x8011)),f13(f8(f1(x8011))))), % 60.25/60.24 inference(scs_inference,[],[27,2,23])). % 60.25/60.24 cnf(802,plain, % 60.25/60.24 (E(f8(f1(f8(x8021))),f8(f1(f8(f1(x8021)))))), % 60.25/60.24 inference(scs_inference,[],[780,2])). % 60.25/60.24 cnf(803,plain, % 60.25/60.24 (E(f3(f8(f1(x8031)),x8032,f8(x8033)),f3(f8(x8031),x8032,f8(f1(x8033))))), % 60.25/60.24 inference(scs_inference,[],[797,780,787,2,3])). % 60.25/60.24 cnf(806,plain, % 60.25/60.24 (E(f12(f8(x8061),x8062),f12(f8(f1(x8061)),x8062))), % 60.25/60.24 inference(scs_inference,[],[27,2,6])). % 60.25/60.24 cnf(807,plain, % 60.25/60.24 (E(f4(f8(f12(f8(f1(x8071)),x8072)),f8(f1(x8073))),f4(f8(f1(f12(f8(x8071),x8072))),f8(x8073)))), % 60.25/60.24 inference(scs_inference,[],[784,2])). % 60.25/60.24 cnf(808,plain, % 60.25/60.24 (E(f4(f8(f1(f12(f8(x8081),x8082))),f8(x8083)),f4(f8(f12(f8(f1(x8081)),x8082)),f8(f1(f1(x8083)))))), % 60.25/60.24 inference(scs_inference,[],[784,766,2,3])). % 60.25/60.24 cnf(811,plain, % 60.25/60.24 (E(f12(x8111,f8(x8112)),f12(x8111,f8(f1(x8112))))), % 60.25/60.24 inference(scs_inference,[],[27,2,7])). % 60.25/60.24 cnf(812,plain, % 60.25/60.24 (E(f5(f8(f1(x8121)),x8122),f5(f8(x8121),x8122))), % 60.25/60.24 inference(scs_inference,[],[791,2])). % 60.25/60.24 cnf(813,plain, % 60.25/60.24 (E(f5(f8(x8131),f8(x8132)),f5(f8(f1(x8131)),f8(f1(x8132))))), % 60.25/60.24 inference(scs_inference,[],[791,796,2,3])). % 60.25/60.24 cnf(816,plain, % 60.25/60.24 (E(f18(f8(x8161)),f18(f8(f1(x8161))))), % 60.25/60.24 inference(scs_inference,[],[27,2,8])). % 60.25/60.24 cnf(817,plain, % 60.25/60.24 (E(f6(f8(x8171),f8(f1(x8172))),f6(f8(f1(x8171)),f8(x8172)))), % 60.25/60.24 inference(scs_inference,[],[793,2])). % 60.25/60.24 cnf(818,plain, % 60.25/60.24 (E(f3(f8(f1(x8181)),f8(x8182),f8(x8183)),f3(f8(f1(x8181)),f8(f1(x8182)),f8(f1(x8183))))), % 60.25/60.24 inference(scs_inference,[],[793,798,803,2,3])). % 60.25/60.24 cnf(821,plain, % 60.25/60.24 (E(f9(f8(x8211)),f9(f8(f1(x8211))))), % 60.25/60.24 inference(scs_inference,[],[27,2,9])). % 60.25/60.24 cnf(822,plain, % 60.25/60.24 (E(f13(f8(f1(x8221))),f13(f8(x8221)))), % 60.25/60.24 inference(scs_inference,[],[801,2])). % 60.25/60.24 cnf(823,plain, % 60.25/60.24 (E(f6(f8(x8231),f8(f1(f1(x8232)))),f6(f8(f1(x8231)),f8(x8232)))), % 60.25/60.24 inference(scs_inference,[],[792,817,801,2,3])). % 60.25/60.24 cnf(826,plain, % 60.25/60.24 (E(f16(f8(x8261)),f16(f8(f1(x8261))))), % 60.25/60.24 inference(scs_inference,[],[27,2,10])). % 60.25/60.24 cnf(827,plain, % 60.25/60.24 (E(f6(f8(f1(x8271)),f8(x8272)),f6(f8(x8271),f8(f1(f1(x8272)))))), % 60.25/60.24 inference(scs_inference,[],[823,2])). % 60.25/60.24 cnf(828,plain, % 60.25/60.24 (E(f6(f8(f1(x8281)),f8(f1(f1(x8282)))),f6(f8(f1(x8281)),f8(x8282)))), % 60.25/60.24 inference(scs_inference,[],[823,788,2,3])). % 60.25/60.24 cnf(831,plain, % 60.25/60.24 (E(f4(f8(x8311),x8312),f4(f8(f1(x8311)),x8312))), % 60.25/60.24 inference(scs_inference,[],[27,2,12])). % 60.25/60.24 cnf(832,plain, % 60.25/60.24 (E(f6(f8(f1(x8321)),f8(x8322)),f6(f8(f1(x8321)),f8(f1(f1(x8322)))))), % 60.25/60.24 inference(scs_inference,[],[828,2])). % 60.25/60.24 cnf(836,plain, % 60.25/60.24 (E(f11(f8(x8361),x8362),f11(f8(f1(x8361)),x8362))), % 60.25/60.24 inference(scs_inference,[],[27,2,14])). % 60.25/60.24 cnf(837,plain, % 60.25/60.24 (E(f12(x8371,f8(f1(x8372))),f12(x8371,f8(x8372)))), % 60.25/60.24 inference(scs_inference,[],[811,2])). % 60.25/60.24 cnf(838,plain, % 60.25/60.24 (E(f3(f8(f1(f1(x8381))),f8(x8382),f8(x8383)),f3(f8(f1(x8381)),f8(f1(x8382)),f8(f1(x8383))))), % 60.25/60.24 inference(scs_inference,[],[811,818,797,2,3])). % 60.25/60.24 cnf(840,plain, % 60.25/60.24 (E(f11(x8401,f8(x8402)),f11(x8401,f8(f1(x8402))))), % 60.25/60.24 inference(scs_inference,[],[27,2,15])). % 60.25/60.24 cnf(841,plain, % 60.25/60.24 (E(f5(f8(f1(x8411)),f8(f1(x8412))),f5(f8(x8411),f8(x8412)))), % 60.25/60.24 inference(scs_inference,[],[813,2])). % 60.25/60.24 cnf(842,plain, % 60.25/60.24 (E(f11(f8(x8421),f8(x8422)),f11(f8(f1(x8421)),f8(f1(x8422))))), % 60.25/60.24 inference(scs_inference,[],[813,836,840,2,3])). % 60.25/60.24 cnf(847,plain, % 60.25/60.24 (E(f5(f8(f1(f1(x8471))),f8(f1(x8472))),f5(f8(x8471),f8(x8472)))), % 60.25/60.24 inference(scs_inference,[],[812,841,816,2,3])). % 60.25/60.24 cnf(851,plain, % 60.25/60.24 (E(f5(f8(x8511),f8(x8512)),f5(f8(f1(f1(x8511))),f8(f1(x8512))))), % 60.25/60.24 inference(scs_inference,[],[847,2])). % 60.25/60.25 cnf(852,plain, % 60.25/60.25 (E(f5(f8(f1(f1(f1(x8521)))),f8(f1(x8522))),f5(f8(x8521),f8(x8522)))), % 60.25/60.25 inference(scs_inference,[],[847,812,2,3])). % 60.25/60.25 cnf(855,plain, % 60.25/60.25 (E(f5(f8(x8551),f8(x8552)),f5(f8(f1(f1(f1(x8551)))),f8(f1(x8552))))), % 60.25/60.25 inference(scs_inference,[],[852,2])). % 60.25/60.25 cnf(856,plain, % 60.25/60.25 (E(f3(f8(f1(f1(x8561))),f8(x8562),f8(x8563)),f3(f8(f1(x8561)),f8(f1(f1(x8562))),f8(f1(x8563))))), % 60.25/60.25 inference(scs_inference,[],[852,838,782,2,3])). % 60.25/60.25 cnf(861,plain, % 60.25/60.25 (E(f5(f8(x8611),f8(x8612)),f5(f8(f1(f1(f1(f1(f1(x8611)))))),f8(f1(f1(x8612)))))), % 60.25/60.25 inference(scs_inference,[],[821,851,855,2,3])). % 60.25/60.25 cnf(865,plain, % 60.25/60.25 (E(f3(f8(f1(f1(x8651))),f8(x8652),f8(x8653)),f3(f8(f1(x8651)),f8(f1(f1(x8652))),f8(f1(f1(x8653)))))), % 60.25/60.25 inference(scs_inference,[],[826,856,787,2,3])). % 60.25/60.25 cnf(869,plain, % 60.25/60.25 (E(f11(f8(f1(x8691)),f8(f1(x8692))),f11(f8(x8691),f8(x8692)))), % 60.25/60.25 inference(scs_inference,[],[842,2])). % 60.25/60.25 cnf(870,plain, % 60.25/60.25 (E(f8(f1(f1(f8(x8701)))),f8(f1(f8(f1(x8701)))))), % 60.25/60.25 inference(scs_inference,[],[27,842,802,2,3])). % 60.25/60.25 cnf(874,plain, % 60.25/60.25 (E(f11(f8(x8741),f8(f1(x8742))),f11(f8(x8741),f8(x8742)))), % 60.25/60.25 inference(scs_inference,[],[869,789,836,2,3])). % 60.25/60.25 cnf(878,plain, % 60.25/60.25 (E(f11(f8(f1(f12(f8(x8781),x8782))),f8(f1(x8783))),f11(f8(f12(f8(f1(x8781)),x8782)),f8(x8783)))), % 60.25/60.25 inference(scs_inference,[],[874,808,756,2,3])). % 60.25/60.25 cnf(882,plain, % 60.25/60.25 (E(f11(f8(f12(f8(f1(x8821)),x8822)),f8(x8823)),f11(f8(f1(f12(f8(x8821),x8822))),f8(f1(x8823))))), % 60.25/60.25 inference(scs_inference,[],[878,2])). % 60.25/60.25 cnf(883,plain, % 60.25/60.25 (E(f6(f8(f1(x8831)),f8(x8832)),f6(f8(x8831),f8(f1(f1(f1(f1(x8832)))))))), % 60.25/60.25 inference(scs_inference,[],[878,827,832,2,3])). % 60.25/60.25 cnf(887,plain, % 60.25/60.25 (E(f3(f8(f1(x8871)),f8(x8872),f8(x8873)),f3(f8(f1(x8871)),f8(f1(f1(f1(x8872)))),f8(f1(f1(x8873)))))), % 60.25/60.25 inference(scs_inference,[],[861,865,798,2,3])). % 60.25/60.25 cnf(891,plain, % 60.25/60.25 (E(f8(f1(f8(f1(x8911)))),f8(f1(f1(f8(x8911)))))), % 60.25/60.25 inference(scs_inference,[],[870,2])). % 60.25/60.25 cnf(892,plain, % 60.25/60.25 (E(f8(f1(f1(f1(f8(x8921))))),f8(f1(f8(f1(x8921)))))), % 60.25/60.25 inference(scs_inference,[],[27,870,2,3])). % 60.25/60.25 cnf(895,plain, % 60.25/60.25 (E(f3(f8(f1(x8951)),f8(f1(f1(f1(x8952)))),f8(f1(f1(x8953)))),f3(f8(f1(x8951)),f8(x8952),f8(x8953)))), % 60.25/60.25 inference(scs_inference,[],[887,2])). % 60.25/60.25 cnf(896,plain, % 60.25/60.25 (E(f3(f8(f1(f1(x8961))),f8(x8962),f8(x8963)),f3(f8(f1(x8961)),f8(f1(f1(f1(x8962)))),f8(f1(f1(f1(x8963))))))), % 60.25/60.25 inference(scs_inference,[],[887,803,2,3])). % 60.25/60.25 cnf(901,plain, % 60.25/60.25 (E(f8(f1(f1(f8(f1(x9011))))),f8(f1(f1(f8(x9011)))))), % 60.25/60.25 inference(scs_inference,[],[27,891,892,2,3])). % 60.25/60.25 cnf(905,plain, % 60.25/60.25 (E(f8(f1(f1(f1(f8(f1(x9051)))))),f8(f1(f1(f8(x9051)))))), % 60.25/60.25 inference(scs_inference,[],[27,901,2,3])). % 60.25/60.25 cnf(909,plain, % 60.25/60.25 (E(f8(f1(f8(x9091))),f8(f1(f1(f8(f1(x9091))))))), % 60.25/60.25 inference(scs_inference,[],[27,905,771,2,3])). % 60.25/60.25 cnf(916,plain, % 60.25/60.25 (E(f3(f8(f1(x9161)),f8(f1(f1(f1(x9162)))),f8(f1(f1(f1(x9163))))),f3(f8(f1(f1(x9161))),f8(x9162),f8(x9163)))), % 60.25/60.25 inference(scs_inference,[],[896,2])). % 60.25/60.25 cnf(920,plain, % 60.25/60.25 (E(f8(f1(f1(f8(f1(x9201))))),f8(f1(f8(x9201))))), % 60.25/60.25 inference(scs_inference,[],[909,2])). % 60.25/60.25 cnf(925,plain, % 60.25/60.25 (E(f6(f8(x9251),f8(f1(f1(f1(f1(x9252)))))),f6(f8(f1(x9251)),f8(x9252)))), % 60.25/60.25 inference(scs_inference,[],[883,2])). % 60.25/60.25 cnf(926,plain, % 60.25/60.25 (E(f8(f1(f1(f1(f8(f1(x9261)))))),f8(f1(f8(x9261))))), % 60.25/60.25 inference(scs_inference,[],[27,920,883,2,3])). % 60.25/60.25 cnf(930,plain, % 60.25/60.25 (E(f11(f8(f12(f8(f1(x9301)),x9302)),f8(x9303)),f11(f8(f12(f8(x9301),x9302)),f8(x9303)))), % 60.25/60.25 inference(scs_inference,[],[882,926,869,2,3])). % 60.25/60.25 cnf(933,plain, % 60.25/60.25 (E(f11(f8(f12(f8(x9331),x9332)),f8(x9333)),f11(f8(f12(f8(f1(x9331)),x9332)),f8(x9333)))), % 60.25/60.25 inference(scs_inference,[],[930,2])). % 60.25/60.25 cnf(934,plain, % 60.25/60.25 (E(f11(f8(f12(f8(f1(x9341)),x9342)),f8(f1(x9343))),f11(f8(f12(f8(x9341),x9342)),f8(x9343)))), % 60.25/60.25 inference(scs_inference,[],[930,874,2,3])). % 60.25/60.25 cnf(938,plain, % 60.25/60.25 (E(f11(f8(f12(f8(x9381),x9382)),f8(x9383)),f11(f8(f12(f8(f1(x9381)),x9382)),f8(f1(x9383))))), % 60.25/60.25 inference(scs_inference,[],[934,2])). % 60.25/60.25 cnf(939,plain, % 60.25/60.25 (E(f8(f1(f1(f8(x9391)))),f8(f8(f1(x9391))))), % 60.25/60.25 inference(scs_inference,[],[27,934,760,2,3])). % 60.25/60.25 cnf(943,plain, % 60.25/60.25 (E(f11(f8(f12(f8(x9431),x9432)),f8(x9433)),f11(f8(f12(f8(f1(f1(x9431))),x9432)),f8(f1(x9433))))), % 60.25/60.25 inference(scs_inference,[],[933,938,939,2,3])). % 60.25/60.25 cnf(946,plain, % 60.25/60.25 (E(f11(f8(f12(f8(f1(f1(x9461))),x9462)),f8(f1(x9463))),f11(f8(f12(f8(x9461),x9462)),f8(x9463)))), % 60.25/60.25 inference(scs_inference,[],[943,2])). % 60.25/60.25 cnf(947,plain, % 60.25/60.25 (E(f11(f8(f12(f8(x9471),x9472)),f8(x9473)),f11(f8(f12(f8(f1(f1(f1(x9471)))),x9472)),f8(f1(x9473))))), % 60.25/60.25 inference(scs_inference,[],[943,933,2,3])). % 60.25/60.25 cnf(950,plain, % 60.25/60.25 (E(f11(f8(f12(f8(f1(f1(f1(x9501)))),x9502)),f8(f1(x9503))),f11(f8(f12(f8(x9501),x9502)),f8(x9503)))), % 60.25/60.25 inference(scs_inference,[],[947,2])). % 60.25/60.25 cnf(951,plain, % 60.25/60.25 (E(f6(f8(x9511),f8(f1(f1(f1(f1(x9512)))))),f6(f8(f1(f1(x9511))),f8(x9512)))), % 60.25/60.25 inference(scs_inference,[],[925,947,770,2,3])). % 60.25/60.25 cnf(954,plain, % 60.25/60.25 (E(f6(f8(f1(f1(x9541))),f8(x9542)),f6(f8(x9541),f8(f1(f1(f1(f1(x9542)))))))), % 60.25/60.25 inference(scs_inference,[],[951,2])). % 60.25/60.25 cnf(955,plain, % 60.25/60.25 (E(f6(f8(x9551),f8(f1(f1(f1(f1(x9552)))))),f6(f8(f1(x9551)),f8(f1(x9552))))), % 60.25/60.25 inference(scs_inference,[],[951,793,2,3])). % 60.25/60.25 cnf(957,plain, % 60.25/60.25 (E(f6(f8(f1(x9571)),f8(f1(x9572))),f6(f8(x9571),f8(f1(f1(f1(f1(x9572)))))))), % 60.25/60.25 inference(scs_inference,[],[955,2])). % 60.25/60.25 cnf(958,plain, % 60.25/60.25 (E(f12(f8(x9581),f8(f12(f8(f1(x9582)),x9583))),f12(f8(f1(x9581)),f8(f1(f12(f8(x9582),x9583)))))), % 60.25/60.25 inference(scs_inference,[],[176,955,806,2,3])). % 60.25/60.25 cnf(963,plain, % 60.25/60.25 (E(f6(f8(f1(f1(x9631))),f8(x9632)),f6(f8(x9631),f8(f1(f1(f1(x9632))))))), % 60.25/60.25 inference(scs_inference,[],[958,954,792,2,3])). % 60.25/60.25 cnf(966,plain, % 60.25/60.25 (E(f6(f8(x9661),f8(f1(f1(f1(x9662))))),f6(f8(f1(f1(x9661))),f8(x9662)))), % 60.25/60.25 inference(scs_inference,[],[963,2])). % 60.25/60.25 cnf(971,plain, % 60.25/60.25 (E(f5(x9711,f8(f1(x9712))),f5(x9711,f8(x9712)))), % 60.25/60.25 inference(scs_inference,[],[796,2])). % 60.25/60.25 cnf(972,plain, % 60.25/60.25 (E(f6(f8(x9721),f8(f1(f1(f1(f1(x9722)))))),f6(f8(f1(f1(f1(x9721)))),f8(x9722)))), % 60.25/60.25 inference(scs_inference,[],[966,817,796,2,3])). % 60.25/60.25 cnf(976,plain, % 60.25/60.25 (E(f6(f8(f1(f1(f1(x9761)))),f8(x9762)),f6(f8(x9761),f8(f1(f1(f1(f1(x9762)))))))), % 60.25/60.25 inference(scs_inference,[],[972,2])). % 60.25/60.25 cnf(977,plain, % 60.25/60.25 (E(f6(f8(f1(x9771)),f8(f1(x9772))),f6(f8(f1(f1(f1(x9771)))),f8(x9772)))), % 60.25/60.25 inference(scs_inference,[],[972,957,2,3])). % 60.25/60.25 cnf(980,plain, % 60.25/60.25 (E(f6(f8(f1(f1(f1(x9801)))),f8(x9802)),f6(f8(f1(x9801)),f8(f1(x9802))))), % 60.25/60.25 inference(scs_inference,[],[977,2])). % 60.25/60.25 cnf(981,plain, % 60.25/60.25 (E(f3(f8(f1(x9811)),f8(f1(f1(f1(x9812)))),f8(f1(f1(x9813)))),f3(f8(f1(x9811)),f8(f1(x9812)),f8(f1(x9813))))), % 60.25/60.25 inference(scs_inference,[],[895,977,818,2,3])). % 60.25/60.25 cnf(983,plain, % 60.25/60.25 (E(f3(f8(f1(x9831)),f8(f1(x9832)),f8(f1(x9833))),f3(f8(f1(x9831)),f8(f1(f1(f1(x9832)))),f8(f1(f1(x9833)))))), % 60.25/60.25 inference(scs_inference,[],[981,2])). % 60.25/60.25 cnf(984,plain, % 60.25/60.25 (E(f6(f8(f1(f1(f1(x9841)))),f8(f1(x9842))),f6(f8(f1(x9841)),f8(x9842)))), % 60.25/60.25 inference(scs_inference,[],[980,981,828,2,3])). % 60.25/60.25 cnf(988,plain, % 60.25/60.25 (E(f6(f8(f1(x9881)),f8(x9882)),f6(f8(f1(f1(f1(x9881)))),f8(f1(x9882))))), % 60.25/60.25 inference(scs_inference,[],[984,2])). % 60.25/60.25 cnf(989,plain, % 60.25/60.25 (E(f3(f8(f1(x9891)),f8(f1(x9892)),f8(f1(f1(x9893)))),f3(f8(f1(f1(x9891))),f8(x9892),f8(x9893)))), % 60.25/60.25 inference(scs_inference,[],[916,984,983,2,3])). % 60.25/60.25 cnf(993,plain, % 60.25/60.25 (E(f3(f8(f1(f1(x9931))),f8(x9932),f8(x9933)),f3(f8(f1(x9931)),f8(f1(x9932)),f8(f1(f1(x9933)))))), % 60.25/60.25 inference(scs_inference,[],[989,2])). % 60.25/60.25 cnf(994,plain, % 60.25/60.25 (E(f6(f8(f1(x9941)),f8(f1(f1(f1(x9942))))),f6(f8(f1(f1(f1(f1(x9941))))),f8(x9942)))), % 60.25/60.25 inference(scs_inference,[],[989,988,925,2,3])). % 60.25/60.25 cnf(998,plain, % 60.25/60.25 (E(f6(f8(f1(f1(f1(f1(x9981))))),f8(x9982)),f6(f8(f1(x9981)),f8(f1(f1(f1(x9982))))))), % 60.25/60.25 inference(scs_inference,[],[994,2])). % 60.25/60.25 cnf(999,plain, % 60.25/60.25 (E(f3(f8(f1(f1(x9991))),f8(f1(f1(x9992))),f8(x9993)),f3(f8(f1(x9991)),f8(x9992),f8(x9993)))), % 60.25/60.25 inference(scs_inference,[],[994,993,895,2,3])). % 60.25/60.25 cnf(1003,plain, % 60.25/60.25 (E(f3(f8(f1(x10031)),f8(x10032),f8(x10033)),f3(f8(f1(f1(x10031))),f8(f1(f1(x10032))),f8(x10033)))), % 60.25/60.25 inference(scs_inference,[],[999,2])). % 60.25/60.25 cnf(1004,plain, % 60.25/60.25 (E(f3(f8(f1(f1(f1(x10041)))),f8(f1(f1(x10042))),f8(x10043)),f3(f8(f1(x10041)),f8(f1(x10042)),f8(f1(x10043))))), % 60.25/60.25 inference(scs_inference,[],[999,838,2,3])). % 60.25/60.25 cnf(1008,plain, % 60.25/60.25 (E(f3(f8(f1(x10081)),f8(f1(x10082)),f8(f1(x10083))),f3(f8(f1(f1(f1(x10081)))),f8(f1(f1(x10082))),f8(x10083)))), % 60.25/60.25 inference(scs_inference,[],[1004,2])). % 60.25/60.25 cnf(1009,plain, % 60.25/60.25 (E(f3(f8(f1(x10091)),f8(f1(x10092)),f8(f1(f1(f1(x10093))))),f3(f8(f1(f1(f1(x10091)))),f8(x10092),f8(x10093)))), % 60.25/60.25 inference(scs_inference,[],[1003,1004,916,2,3])). % 60.25/60.25 cnf(1012,plain, % 60.25/60.25 (E(f3(f8(f1(f1(f1(x10121)))),f8(x10122),f8(x10123)),f3(f8(f1(x10121)),f8(f1(x10122)),f8(f1(f1(f1(x10123))))))), % 60.25/60.25 inference(scs_inference,[],[1009,2])). % 60.25/60.25 cnf(1013,plain, % 60.25/60.25 (E(f11(f11(x10131,f8(x10132)),f8(x10133)),f11(f11(x10131,f8(f1(x10132))),f8(f1(x10133))))), % 60.25/60.25 inference(scs_inference,[],[99,1009,840,2,3])). % 60.25/60.25 cnf(1017,plain, % 60.25/60.25 (E(f11(f11(x10171,f8(f1(x10172))),f8(f1(x10173))),f11(f11(x10171,f8(x10172)),f8(x10173)))), % 60.25/60.25 inference(scs_inference,[],[1013,2])). % 60.25/60.25 cnf(1018,plain, % 60.25/60.25 (E(f3(f8(f1(f1(f1(x10181)))),f8(x10182),f8(x10183)),f3(f8(f1(f1(f1(x10181)))),f8(f1(f1(x10182))),f8(f1(f1(x10183)))))), % 60.25/60.25 inference(scs_inference,[],[1008,1013,1012,2,3])). % 60.25/60.25 cnf(1021,plain, % 60.25/60.25 (E(f3(f8(f1(f1(f1(x10211)))),f8(f1(f1(x10212))),f8(f1(f1(x10213)))),f3(f8(f1(f1(f1(x10211)))),f8(x10212),f8(x10213)))), % 60.25/60.25 inference(scs_inference,[],[1018,2])). % 60.25/60.25 cnf(1022,plain, % 60.25/60.25 (E(f11(f11(x10221,f8(f1(f1(x10222)))),f8(f1(x10223))),f11(f11(x10221,f8(x10222)),f8(x10223)))), % 60.25/60.25 inference(scs_inference,[],[116,1017,1018,2,3])). % 60.25/60.25 cnf(1027,plain, % 60.25/60.25 (E(f11(f11(x10271,f8(x10272)),f8(f1(x10273))),f11(f11(x10271,f8(x10272)),f8(x10273)))), % 60.25/60.25 inference(scs_inference,[],[99,1022,1017,2,3])). % 60.25/60.25 cnf(1031,plain, % 60.25/60.25 (E(f4(f8(f1(x10311)),x10312),f4(f8(x10311),x10312))), % 60.25/60.25 inference(scs_inference,[],[831,2])). % 60.25/60.25 cnf(1032,plain, % 60.25/60.25 (E(f11(f11(x10321,f8(f1(f1(f1(x10322))))),f8(f1(x10323))),f11(f11(x10321,f8(x10322)),f8(x10323)))), % 60.25/60.25 inference(scs_inference,[],[116,1022,831,2,3])). % 60.25/60.25 cnf(1036,plain, % 60.25/60.25 (E(f4(f8(f1(f12(f8(f1(x10361)),x10362))),f8(f1(x10363))),f4(f8(f1(f12(f8(x10361),x10362))),f8(x10363)))), % 60.25/60.25 inference(scs_inference,[],[807,1031,1032,2,3])). % 60.25/60.25 cnf(1039,plain, % 60.25/60.25 (E(f4(f8(f1(f12(f8(x10391),x10392))),f8(x10393)),f4(f8(f1(f12(f8(f1(x10391)),x10392))),f8(f1(x10393))))), % 60.25/60.25 inference(scs_inference,[],[1036,2])). % 60.25/60.25 cnf(1040,plain, % 60.25/60.25 (E(f11(f11(x10401,f8(x10402)),f8(f1(x10403))),f11(f11(x10401,f8(f1(x10402))),f8(x10403)))), % 60.25/60.25 inference(scs_inference,[],[99,1027,1036,2,3])). % 60.25/60.25 cnf(1045,plain, % 60.25/60.25 (E(f11(f11(x10451,f8(f1(f1(f1(f1(x10452)))))),f8(f1(x10453))),f11(f11(x10451,f8(x10452)),f8(x10453)))), % 60.25/60.25 inference(scs_inference,[],[116,1040,1032,2,3])). % 60.25/60.25 cnf(1050,plain, % 60.25/60.25 (E(f11(f11(x10501,f8(x10502)),f8(f1(x10503))),f11(f11(x10501,f8(f1(f1(x10502)))),f8(x10503)))), % 60.25/60.25 inference(scs_inference,[],[99,1045,1040,2,3])). % 60.25/60.25 cnf(1054,plain, % 60.25/60.25 (E(f11(f11(x10541,f8(f1(f1(x10542)))),f8(x10543)),f11(f11(x10541,f8(x10542)),f8(f1(x10543))))), % 60.25/60.25 inference(scs_inference,[],[1050,2])). % 60.25/60.25 cnf(1055,plain, % 60.25/60.25 (E(f11(f8(f12(f8(f1(f1(x10551))),x10552)),f8(f1(x10553))),f11(f8(f1(f12(f8(x10551),x10552))),f8(f1(x10553))))), % 60.25/60.25 inference(scs_inference,[],[946,1050,842,2,3])). % 60.25/60.25 cnf(1058,plain, % 60.25/60.25 (E(f11(f8(f1(f12(f8(x10581),x10582))),f8(f1(x10583))),f11(f8(f12(f8(f1(f1(x10581))),x10582)),f8(f1(x10583))))), % 60.25/60.25 inference(scs_inference,[],[1055,2])). % 60.25/60.25 cnf(1059,plain, % 60.25/60.25 (E(f11(f11(x10591,f8(f1(f1(f1(x10592))))),f8(x10593)),f11(f11(x10591,f8(x10592)),f8(f1(x10593))))), % 60.25/60.25 inference(scs_inference,[],[116,1054,1055,2,3])). % 60.25/60.25 cnf(1063,plain, % 60.25/60.25 (E(f11(f11(x10631,f8(x10632)),f8(f1(x10633))),f11(f11(x10631,f8(f1(f1(f1(x10632))))),f8(x10633)))), % 60.25/60.25 inference(scs_inference,[],[1059,2])). % 60.25/60.25 cnf(1064,plain, % 60.25/60.25 (E(f11(f8(f1(f12(f8(f1(x10641)),x10642))),f8(f1(x10643))),f11(f8(f12(f8(x10641),x10642)),f8(x10643)))), % 60.25/60.25 inference(scs_inference,[],[950,1058,1059,2,3])). % 60.25/60.25 cnf(1067,plain, % 60.25/60.25 (E(f11(f8(f12(f8(x10671),x10672)),f8(x10673)),f11(f8(f1(f12(f8(f1(x10671)),x10672))),f8(f1(x10673))))), % 60.25/60.25 inference(scs_inference,[],[1064,2])). % 60.25/60.25 cnf(1068,plain, % 60.25/60.25 (E(f11(f11(x10681,f8(x10682)),f8(f1(x10683))),f11(f11(x10681,f8(f1(f1(f1(f1(x10682)))))),f8(x10683)))), % 60.25/60.25 inference(scs_inference,[],[99,1063,1064,2,3])). % 60.25/60.25 cnf(1073,plain, % 60.25/60.25 (E(f11(f8(f1(f12(f8(x10731),x10732))),f8(f1(f1(x10733)))),f11(f8(f12(f8(x10731),x10732)),f8(x10733)))), % 60.25/60.25 inference(scs_inference,[],[1068,878,934,2,3])). % 60.25/60.25 cnf(1077,plain, % 60.25/60.25 (E(f11(f8(f12(f8(x10771),x10772)),f8(x10773)),f11(f8(f1(f12(f8(x10771),x10772))),f8(f1(f1(x10773)))))), % 60.25/60.25 inference(scs_inference,[],[1073,2])). % 60.25/60.25 cnf(1078,plain, % 60.25/60.25 (E(f11(f8(f12(f8(x10781),x10782)),f8(f1(x10783))),f11(f8(f12(f8(f1(x10781)),x10782)),f8(x10783)))), % 60.25/60.25 inference(scs_inference,[],[1073,1067,2,3])). % 60.25/60.25 cnf(1082,plain, % 60.25/60.25 (E(f11(f8(f12(f8(f1(x10821)),x10822)),f8(x10823)),f11(f8(f12(f8(x10821),x10822)),f8(f1(x10823))))), % 60.25/60.25 inference(scs_inference,[],[1078,2])). % 60.25/60.25 cnf(1083,plain, % 60.25/60.25 (E(f11(f8(f12(f8(f1(x10831)),x10832)),f8(f1(f1(x10833)))),f11(f8(f12(f8(x10831),x10832)),f8(x10833)))), % 60.25/60.25 inference(scs_inference,[],[1078,946,2,3])). % 60.25/60.25 cnf(1087,plain, % 60.25/60.25 (E(f11(f8(f12(f8(x10871),x10872)),f8(x10873)),f11(f8(f12(f8(f1(x10871)),x10872)),f8(f1(f1(x10873)))))), % 60.25/60.25 inference(scs_inference,[],[1083,2])). % 60.25/60.25 cnf(1088,plain, % 60.25/60.25 (E(f8(f1(f1(f1(f8(x10881))))),f8(f8(f1(x10881))))), % 60.25/60.25 inference(scs_inference,[],[27,1083,939,2,3])). % 60.25/60.25 cnf(1092,plain, % 60.25/60.25 (E(f8(f1(f1(f1(f1(f8(x10921)))))),f8(f8(f1(x10921))))), % 60.25/60.25 inference(scs_inference,[],[27,1088,2,3])). % 60.25/60.25 cnf(1094,plain, % 60.25/60.25 (E(f8(f8(f1(x10941))),f8(f1(f1(f1(f1(f8(x10941)))))))), % 60.25/60.25 inference(scs_inference,[],[1092,2])). % 60.25/60.25 cnf(1095,plain, % 60.25/60.25 (E(f11(f8(f12(f8(f1(x10951)),x10952)),f8(x10953)),f11(f8(f12(f8(f1(x10951)),x10952)),f8(f1(f1(x10953)))))), % 60.25/60.25 inference(scs_inference,[],[1082,1092,938,2,3])). % 60.25/60.25 cnf(1098,plain, % 60.25/60.25 (E(f11(f8(f12(f8(f1(x10981)),x10982)),f8(f1(f1(x10983)))),f11(f8(f12(f8(f1(x10981)),x10982)),f8(x10983)))), % 60.25/60.25 inference(scs_inference,[],[1095,2])). % 60.25/60.25 cnf(1099,plain, % 60.25/60.25 (E(f8(f1(f8(f1(x10991)))),f8(f1(f1(f1(f1(f8(x10991)))))))), % 60.25/60.25 inference(scs_inference,[],[27,1095,1094,2,3])). % 60.25/60.25 cnf(1103,plain, % 60.25/60.25 (E(f11(f8(f12(f8(f1(x11031)),x11032)),f8(f1(f1(x11033)))),f11(f8(f1(f12(f8(x11031),x11032))),f8(f1(x11033))))), % 60.25/60.25 inference(scs_inference,[],[1098,1099,882,2,3])). % 60.25/60.25 cnf(1106,plain, % 60.25/60.25 (E(f11(f8(f1(f12(f8(x11061),x11062))),f8(f1(x11063))),f11(f8(f12(f8(f1(x11061)),x11062)),f8(f1(f1(x11063)))))), % 60.25/60.25 inference(scs_inference,[],[1103,2])). % 60.25/60.25 cnf(1107,plain, % 60.25/60.25 (E(f11(f8(f12(f8(f1(f1(x11071))),x11072)),f8(x11073)),f11(f8(f12(f8(x11071),x11072)),f8(f1(x11073))))), % 60.25/60.25 inference(scs_inference,[],[1103,1087,950,2,3])). % 60.25/60.25 cnf(1110,plain, % 60.25/60.25 (E(f11(f8(f12(f8(x11101),x11102)),f8(f1(x11103))),f11(f8(f12(f8(f1(f1(x11101))),x11102)),f8(x11103)))), % 60.25/60.25 inference(scs_inference,[],[1107,2])). % 60.25/60.25 cnf(1111,plain, % 60.25/60.25 (E(f11(f8(f12(f8(x11111),x11112)),f8(x11113)),f11(f8(f12(f8(f1(x11111)),x11112)),f8(f1(f1(f1(x11113))))))), % 60.25/60.25 inference(scs_inference,[],[1107,1077,1106,2,3])). % 60.25/60.25 cnf(1115,plain, % 60.25/60.25 (E(f11(f8(f12(f8(x11151),x11152)),f8(f1(f1(f1(x11153))))),f11(f8(f12(f8(f1(x11151)),x11152)),f8(x11153)))), % 60.25/60.25 inference(scs_inference,[],[1110,1111,1083,2,3])). % 60.25/60.25 cnf(1120,plain, % 60.25/60.25 (E(f6(f8(f1(f1(f1(f1(x11201))))),f8(f1(x11202))),f6(f8(f1(f1(x11201))),f8(f1(x11202))))), % 60.25/60.25 inference(scs_inference,[],[1115,998,955,2,3])). % 60.25/60.25 cnf(1124,plain, % 60.25/60.25 (E(f6(f8(f1(f1(x11241))),f8(f1(x11242))),f6(f8(f1(f1(f1(f1(x11241))))),f8(f1(x11242))))), % 60.25/60.25 inference(scs_inference,[],[1120,2])). % 60.25/60.25 cnf(1125,plain, % 60.25/60.25 (E(f6(f8(f1(f1(f1(f1(f1(x11251)))))),f8(f1(x11252))),f6(f8(f1(x11251)),f8(x11252)))), % 60.25/60.25 inference(scs_inference,[],[1120,984,2,3])). % 60.25/60.25 cnf(1128,plain, % 60.25/60.25 (E(f6(f8(f1(x11281)),f8(x11282)),f6(f8(f1(f1(f1(f1(f1(x11281)))))),f8(f1(x11282))))), % 60.25/60.25 inference(scs_inference,[],[1125,2])). % 60.25/60.25 cnf(1129,plain, % 60.25/60.25 (E(f5(f13(f4(x11291,f8(x11292))),f8(f1(x11293))),f5(f13(f4(x11291,f8(f1(x11292)))),f8(x11293)))), % 60.25/60.25 inference(scs_inference,[],[971,1125,288,2,3])). % 60.25/60.25 cnf(1133,plain, % 60.25/60.25 (E(f5(f13(f4(x11331,f8(f1(x11332)))),f8(x11333)),f5(f13(f4(x11331,f8(x11332))),f8(f1(x11333))))), % 60.25/60.25 inference(scs_inference,[],[1129,2])). % 60.25/60.25 cnf(1134,plain, % 60.25/60.25 (E(f5(f13(f4(x11341,f8(x11342))),f8(f1(f1(x11343)))),f5(f13(f4(x11341,f8(f1(x11342)))),f8(x11343)))), % 60.25/60.25 inference(scs_inference,[],[1129,971,2,3])). % 60.25/60.25 cnf(1137,plain, % 60.25/60.25 (E(f5(f13(f4(x11371,f8(f1(x11372)))),f8(x11373)),f5(f13(f4(x11371,f8(x11372))),f8(f1(f1(x11373)))))), % 60.25/60.25 inference(scs_inference,[],[1134,2])). % 60.25/60.25 cnf(1138,plain, % 60.25/60.25 (E(f6(f8(f1(f1(x11381))),f8(f1(x11382))),f6(f8(f1(f1(f1(x11381)))),f8(f1(f1(f1(x11382))))))), % 60.25/60.25 inference(scs_inference,[],[1134,1124,827,2,3])). % 60.25/60.25 cnf(1141,plain, % 60.25/60.25 (E(f6(f8(f1(f1(f1(x11411)))),f8(f1(f1(f1(x11412))))),f6(f8(f1(f1(x11411))),f8(f1(x11412))))), % 60.25/60.25 inference(scs_inference,[],[1138,2])). % 60.25/60.25 cnf(1142,plain, % 60.25/60.25 (E(f6(f8(f1(x11421)),f8(x11422)),f6(f8(f1(f1(f1(x11421)))),f8(f1(f1(x11422)))))), % 60.25/60.25 inference(scs_inference,[],[1128,1138,980,2,3])). % 60.25/60.25 cnf(1145,plain, % 60.25/60.25 (E(f6(f8(f1(f1(f1(x11451)))),f8(f1(f1(x11452)))),f6(f8(f1(x11451)),f8(x11452)))), % 60.25/60.25 inference(scs_inference,[],[1142,2])). % 60.25/60.25 cnf(1146,plain, % 60.25/60.25 (E(f6(f8(f1(f1(f1(x11461)))),f8(f1(f1(f1(x11462))))),f6(f8(f1(f1(x11461))),f8(x11462)))), % 60.25/60.25 inference(scs_inference,[],[1141,1142,792,2,3])). % 60.25/60.25 cnf(1149,plain, % 60.25/60.25 (E(f6(f8(f1(f1(x11491))),f8(x11492)),f6(f8(f1(f1(f1(x11491)))),f8(f1(f1(f1(x11492))))))), % 60.25/60.25 inference(scs_inference,[],[1146,2])). % 60.25/60.25 cnf(1150,plain, % 60.25/60.25 (E(f6(f8(f1(f1(f1(x11501)))),f8(f1(f1(x11502)))),f6(f8(f1(x11501)),f8(f1(f1(x11502)))))), % 60.25/60.25 inference(scs_inference,[],[1145,1146,832,2,3])). % 60.25/60.25 cnf(1153,plain, % 60.25/60.25 (E(f6(f8(f1(x11531)),f8(f1(f1(x11532)))),f6(f8(f1(f1(f1(x11531)))),f8(f1(f1(x11532)))))), % 60.25/60.25 inference(scs_inference,[],[1150,2])). % 60.25/60.25 cnf(1154,plain, % 60.25/60.25 (E(f6(f8(f1(f1(x11541))),f8(x11542)),f6(f8(f1(x11541)),f8(f1(f1(f1(x11542))))))), % 60.25/60.25 inference(scs_inference,[],[1150,1149,2,3])). % 60.25/60.25 cnf(1157,plain, % 60.25/60.25 (E(f6(f8(f1(x11571)),f8(f1(f1(f1(x11572))))),f6(f8(f1(f1(x11571))),f8(x11572)))), % 60.25/60.25 inference(scs_inference,[],[1154,2])). % 60.25/60.25 cnf(1158,plain, % 60.25/60.25 (E(f3(f8(f1(f1(f1(x11581)))),f8(f1(f1(x11582))),f8(f1(f1(x11583)))),f3(f8(f1(f1(x11581))),f8(x11582),f8(x11583)))), % 60.25/60.25 inference(scs_inference,[],[1021,1154,797,2,3])). % 60.25/60.25 cnf(1161,plain, % 60.25/60.25 (E(f3(f8(f1(f1(x11611))),f8(x11612),f8(x11613)),f3(f8(f1(f1(f1(x11611)))),f8(f1(f1(x11612))),f8(f1(f1(x11613)))))), % 60.25/60.25 inference(scs_inference,[],[1158,2])). % 60.25/60.25 cnf(1162,plain, % 60.25/60.25 (E(f3(f8(f1(f1(f1(x11621)))),f8(f1(f1(x11622))),f8(f1(f1(x11623)))),f3(f8(f1(x11621)),f8(f1(f1(x11622))),f8(f1(x11623))))), % 60.25/60.25 inference(scs_inference,[],[1158,856,2,3])). % 60.25/60.25 cnf(1165,plain, % 60.25/60.25 (E(f3(f8(f1(x11651)),f8(f1(f1(x11652))),f8(f1(x11653))),f3(f8(f1(f1(f1(x11651)))),f8(f1(f1(x11652))),f8(f1(f1(x11653)))))), % 60.25/60.25 inference(scs_inference,[],[1162,2])). % 60.25/60.25 cnf(1166,plain, % 60.25/60.25 (E(f6(f8(f1(x11661)),f8(f1(f1(f1(x11662))))),f6(f8(f1(x11661)),f8(x11662)))), % 60.25/60.25 inference(scs_inference,[],[1157,1162,788,2,3])). % 60.25/60.25 cnf(1169,plain, % 60.25/60.25 (E(f6(f8(f1(x11691)),f8(x11692)),f6(f8(f1(x11691)),f8(f1(f1(f1(x11692))))))), % 60.25/60.25 inference(scs_inference,[],[1166,2])). % 60.25/60.25 cnf(1170,plain, % 60.25/60.25 (E(f3(f8(f1(f1(x11701))),f8(x11702),f8(x11703)),f3(f8(f1(f1(f1(f1(x11701))))),f8(f1(x11702)),f8(x11703)))), % 60.25/60.25 inference(scs_inference,[],[1166,1161,989,2,3])). % 60.25/60.25 cnf(1173,plain, % 60.25/60.25 (E(f3(f8(f1(f1(f1(f1(x11731))))),f8(f1(x11732)),f8(x11733)),f3(f8(f1(f1(x11731))),f8(x11732),f8(x11733)))), % 60.25/60.25 inference(scs_inference,[],[1170,2])). % 60.25/60.25 cnf(1174,plain, % 60.25/60.25 (E(f6(f8(f1(x11741)),f8(x11742)),f6(f8(f1(f1(f1(x11741)))),f8(f1(f1(f1(x11742))))))), % 60.25/60.25 inference(scs_inference,[],[1170,1153,1169,2,3])). % 60.25/60.25 cnf(1177,plain, % 60.25/60.25 (E(f6(f8(f1(f1(f1(x11771)))),f8(f1(f1(f1(x11772))))),f6(f8(f1(x11771)),f8(x11772)))), % 60.25/60.25 inference(scs_inference,[],[1174,2])). % 60.25/60.25 cnf(1178,plain, % 60.25/60.25 (E(f3(f8(f1(f1(x11781))),f8(f1(f1(x11782))),f8(f1(x11783))),f3(f8(f1(f1(x11781))),f8(f1(x11782)),f8(f1(f1(x11783)))))), % 60.25/60.25 inference(scs_inference,[],[1173,1165,1174,2,3])). % 60.25/60.25 cnf(1182,plain, % 60.25/60.25 (E(f3(f8(f1(f1(x11821))),f8(f1(x11822)),f8(f1(f1(x11823)))),f3(f8(f1(f1(x11821))),f8(f1(f1(x11822))),f8(f1(x11823))))), % 60.25/60.25 inference(scs_inference,[],[1178,2])). % 60.25/60.25 cnf(1183,plain, % 60.25/60.25 (E(f3(f8(f1(x11831)),f8(x11832),f8(f1(x11833))),f3(f8(f1(f1(x11831))),f8(f1(x11832)),f8(f1(f1(x11833)))))), % 60.25/60.25 inference(scs_inference,[],[1178,1003,2,3])). % 60.25/60.25 cnf(1187,plain, % 60.25/60.25 (E(f3(f8(f1(f1(x11871))),f8(f1(x11872)),f8(f1(f1(x11873)))),f3(f8(f1(x11871)),f8(x11872),f8(f1(x11873))))), % 60.25/60.25 inference(scs_inference,[],[1183,2])). % 60.25/60.25 cnf(1188,plain, % 60.25/60.25 (E(f3(f8(f1(f1(f1(x11881)))),f8(f1(x11882)),f8(f1(f1(x11883)))),f3(f8(f1(x11881)),f8(f1(x11882)),f8(f1(f1(x11883)))))), % 60.25/60.25 inference(scs_inference,[],[1182,1183,1004,2,3])). % 60.25/60.25 cnf(1192,plain, % 60.25/60.25 (E(f3(f8(f1(x11921)),f8(f1(x11922)),f8(f1(f1(x11923)))),f3(f8(f1(f1(f1(x11921)))),f8(f1(x11922)),f8(f1(f1(x11923)))))), % 60.25/60.25 inference(scs_inference,[],[1188,2])). % 60.25/60.25 cnf(1193,plain, % 60.25/60.25 (E(f3(f8(f1(f1(f1(f1(x11931))))),f8(f1(x11932)),f8(f1(f1(x11933)))),f3(f8(f1(x11931)),f8(x11932),f8(f1(x11933))))), % 60.25/60.25 inference(scs_inference,[],[1187,1188,2,3])). % 60.25/60.25 cnf(1196,plain, % 60.25/60.25 (E(f3(f8(f1(x11961)),f8(x11962),f8(f1(x11963))),f3(f8(f1(f1(f1(f1(x11961))))),f8(f1(x11962)),f8(f1(f1(x11963)))))), % 60.25/60.25 inference(scs_inference,[],[1193,2])). % 60.25/60.25 cnf(1197,plain, % 60.25/60.25 (E(f11(f8(f12(f8(f1(f1(x11971))),x11972)),f8(f1(f1(x11973)))),f11(f8(f12(f8(x11971),x11972)),f8(x11973)))), % 60.25/60.25 inference(scs_inference,[],[1193,1055,1073,2,3])). % 60.25/60.25 cnf(1202,plain, % 60.25/60.25 (E(f3(f8(f1(x12021)),f8(f1(f1(x12022))),f8(f1(f1(x12023)))),f3(f8(f1(f1(f1(x12021)))),f8(x12022),f8(x12023)))), % 60.25/60.25 inference(scs_inference,[],[1197,1192,1021,2,3])). % 60.25/60.25 cnf(1206,plain, % 60.25/60.25 (E(f3(f8(f1(f1(f1(x12061)))),f8(x12062),f8(x12063)),f3(f8(f1(x12061)),f8(f1(f1(x12062))),f8(f1(f1(x12063)))))), % 60.25/60.25 inference(scs_inference,[],[1202,2])). % 60.25/60.25 cnf(1207,plain, % 60.25/60.25 (E(f3(f8(f1(x12071)),f8(f1(f1(x12072))),f8(f1(f1(x12073)))),f3(f8(f1(f1(x12071))),f8(f1(x12072)),f8(f1(f1(x12073)))))), % 60.25/60.25 inference(scs_inference,[],[1202,993,2,3])). % 60.25/60.25 cnf(1210,plain, % 60.25/60.25 (E(f3(f8(f1(f1(x12101))),f8(f1(x12102)),f8(f1(f1(x12103)))),f3(f8(f1(x12101)),f8(f1(f1(x12102))),f8(f1(f1(x12103)))))), % 60.25/60.25 inference(scs_inference,[],[1207,2])). % 60.25/60.25 cnf(1211,plain, % 60.25/60.25 (E(f3(f8(f1(x12111)),f8(x12112),f8(f1(x12113))),f3(f8(f1(f1(x12111))),f8(x12112),f8(f1(f1(x12113)))))), % 60.25/60.25 inference(scs_inference,[],[1196,1207,1173,2,3])). % 60.25/60.25 cnf(1214,plain, % 60.25/60.25 (E(f3(f8(f1(f1(x12141))),f8(x12142),f8(f1(f1(x12143)))),f3(f8(f1(x12141)),f8(x12142),f8(f1(x12143))))), % 60.25/60.25 inference(scs_inference,[],[1211,2])). % 60.25/60.25 cnf(1215,plain, % 60.25/60.25 (E(f3(f8(f1(f1(f1(x12151)))),f8(x12152),f8(x12153)),f3(f8(f1(f1(f1(x12151)))),f8(f1(f1(f1(x12152)))),f8(f1(x12153))))), % 60.25/60.25 inference(scs_inference,[],[1206,1211,1008,2,3])). % 60.25/60.25 cnf(1218,plain, % 60.25/60.25 (E(f3(f8(f1(f1(f1(x12181)))),f8(f1(f1(f1(x12182)))),f8(f1(x12183))),f3(f8(f1(f1(f1(x12181)))),f8(x12182),f8(x12183)))), % 60.25/60.25 inference(scs_inference,[],[1215,2])). % 60.25/60.25 cnf(1219,plain, % 60.25/60.25 (E(f3(f8(f1(f1(f1(x12191)))),f8(x12192),f8(f1(x12193))),f3(f8(f1(f1(x12191))),f8(f1(f1(f1(x12192)))),f8(f1(x12193))))), % 60.25/60.25 inference(scs_inference,[],[1214,1215,2,3])). % 60.25/60.25 cnf(1223,plain, % 60.25/60.25 (E(f3(f8(f1(f1(x12231))),f8(f1(f1(f1(x12232)))),f8(f1(x12233))),f3(f8(f1(f1(f1(x12231)))),f8(x12232),f8(f1(x12233))))), % 60.25/60.25 inference(scs_inference,[],[1219,2])). % 60.25/60.25 cnf(1224,plain, % 60.25/60.25 (E(f3(f8(f1(f1(f1(f1(x12241))))),f8(x12242),f8(f1(x12243))),f3(f8(f1(f1(f1(x12241)))),f8(x12242),f8(x12243)))), % 60.25/60.25 inference(scs_inference,[],[1218,1219,2,3])). % 60.25/60.25 cnf(1228,plain, % 60.25/60.25 (E(f3(f8(f1(f1(f1(x12281)))),f8(x12282),f8(x12283)),f3(f8(f1(f1(f1(f1(x12281))))),f8(x12282),f8(f1(x12283))))), % 60.25/60.25 inference(scs_inference,[],[1224,2])). % 60.25/60.25 cnf(1229,plain, % 60.25/60.25 (E(f3(f8(f1(f1(f1(f1(x12291))))),f8(f1(f1(x12292))),f8(f1(x12293))),f3(f8(f1(f1(x12291))),f8(x12292),f8(x12293)))), % 60.25/60.25 inference(scs_inference,[],[1224,999,2,3])). % 60.25/60.25 cnf(1233,plain, % 60.25/60.25 (E(f3(f8(f1(f1(x12331))),f8(x12332),f8(x12333)),f3(f8(f1(f1(f1(f1(x12331))))),f8(f1(f1(x12332))),f8(f1(x12333))))), % 60.25/60.25 inference(scs_inference,[],[1229,2])). % 60.25/60.25 cnf(1234,plain, % 60.25/60.25 (E(f3(f8(f1(f1(f1(f1(x12341))))),f8(f1(f1(x12342))),f8(f1(x12343))),f3(f8(f1(f1(x12341))),f8(f1(x12342)),f8(x12343)))), % 60.25/60.25 inference(scs_inference,[],[1229,782,2,3])). % 60.25/60.25 cnf(1241,plain, % 60.25/60.25 (E(f3(f8(f1(x12411)),f8(f1(f1(x12412))),f8(f1(f1(x12413)))),f3(f8(f1(f1(x12411))),f8(x12412),f8(x12413)))), % 60.25/60.25 inference(scs_inference,[],[865,2])). % 60.25/60.25 cnf(1242,plain, % 60.25/60.25 (E(f3(f8(f1(f1(x12421))),f8(f1(f1(f1(x12422)))),f8(f1(f1(x12423)))),f3(f8(f1(f1(x12421))),f8(x12422),f8(f1(x12423))))), % 60.25/60.25 inference(scs_inference,[],[1223,1214,865,2,3])). % 60.25/60.25 cnf(1246,plain, % 60.25/60.25 (E(f3(f8(f1(f1(x12461))),f8(x12462),f8(f1(x12463))),f3(f8(f1(f1(x12461))),f8(f1(f1(f1(x12462)))),f8(f1(f1(x12463)))))), % 60.25/60.25 inference(scs_inference,[],[1242,2])). % 60.25/60.25 cnf(1247,plain, % 60.25/60.25 (E(f3(f8(f1(x12471)),f8(f1(f1(x12472))),f8(f1(f1(x12473)))),f3(f8(f1(f1(f1(f1(x12471))))),f8(f1(x12472)),f8(x12473)))), % 60.25/60.25 inference(scs_inference,[],[1241,1242,1170,2,3])). % 60.25/60.25 cnf(1251,plain, % 60.25/60.25 (E(f3(f8(f1(x12511)),f8(f1(f1(f1(x12512)))),f8(f1(f1(f1(x12513))))),f3(f8(f1(f1(x12511))),f8(f1(x12512)),f8(x12513)))), % 60.25/60.25 inference(scs_inference,[],[1247,1234,2,3])). % 60.25/60.25 cnf(1256,plain, % 60.25/60.25 (E(f6(f8(f1(f1(f1(x12561)))),f8(f1(f1(f1(x12562))))),f6(f8(x12561),f8(f1(x12562))))), % 60.25/60.25 inference(scs_inference,[],[1177,1251,793,2,3])). % 60.25/60.25 cnf(1259,plain, % 60.25/60.25 (E(f6(f8(x12591),f8(f1(x12592))),f6(f8(f1(f1(f1(x12591)))),f8(f1(f1(f1(x12592))))))), % 60.25/60.25 inference(scs_inference,[],[1256,2])). % 60.25/60.25 cnf(1260,plain, % 60.25/60.25 (E(f3(f8(f1(f1(f1(x12601)))),f8(f1(x12602)),f8(f1(x12603))),f3(f8(f1(f1(f1(x12601)))),f8(x12602),f8(f1(x12603))))), % 60.25/60.25 inference(scs_inference,[],[1228,1256,1187,2,3])). % 60.25/60.25 cnf(1264,plain, % 60.25/60.25 (E(f4(x12641,f8(f1(x12642))),f4(x12641,f8(x12642)))), % 60.25/60.25 inference(scs_inference,[],[766,2])). % 60.25/60.25 cnf(1265,plain, % 60.25/60.25 (E(f3(f8(f1(f1(x12651))),f8(x12652),f8(x12653)),f3(f8(f1(f1(f1(f1(x12651))))),f8(f1(x12652)),f8(f1(x12653))))), % 60.25/60.25 inference(scs_inference,[],[1233,1260,766,2,3])). % 60.25/60.25 cnf(1268,plain, % 60.25/60.26 (E(f3(f8(f1(f1(f1(f1(x12681))))),f8(f1(x12682)),f8(f1(x12683))),f3(f8(f1(f1(x12681))),f8(x12682),f8(x12683)))), % 60.25/60.26 inference(scs_inference,[],[1265,2])). % 60.25/60.26 cnf(1269,plain, % 60.25/60.26 (E(f4(f8(f1(f12(f8(x12691),x12692))),f8(x12693)),f4(f8(f1(f12(f8(f1(x12691)),x12692))),f8(x12693)))), % 60.25/60.26 inference(scs_inference,[],[1264,1039,1265,2,3])). % 60.25/60.26 cnf(1273,plain, % 60.25/60.26 (E(f4(f8(f12(f8(f1(x12731)),x12732)),f8(f1(x12733))),f4(f8(f1(f12(f8(f1(x12731)),x12732))),f8(x12733)))), % 60.25/60.26 inference(scs_inference,[],[1269,807,2,3])). % 60.25/60.26 cnf(1277,plain, % 60.25/60.26 (E(f6(f8(x12771),f8(f1(x12772))),f6(f8(f1(f1(f1(f1(f1(x12771)))))),f8(x12772)))), % 60.25/60.26 inference(scs_inference,[],[1273,1259,966,2,3])). % 60.25/60.26 cnf(1280,plain, % 60.25/60.26 (E(f6(f8(f1(f1(f1(f1(f1(x12801)))))),f8(x12802)),f6(f8(x12801),f8(f1(x12802))))), % 60.25/60.26 inference(scs_inference,[],[1277,2])). % 60.25/60.26 cnf(1281,plain, % 60.25/60.26 (E(f6(f8(x12811),f8(f1(x12812))),f6(f8(f1(f1(x12811))),f8(f1(f1(f1(f1(x12812)))))))), % 60.25/60.26 inference(scs_inference,[],[1277,976,2,3])). % 60.25/60.26 cnf(1284,plain, % 60.25/60.26 (E(f6(f8(f1(f1(x12841))),f8(f1(f1(f1(f1(x12842)))))),f6(f8(x12841),f8(f1(x12842))))), % 60.25/60.26 inference(scs_inference,[],[1281,2])). % 60.25/60.26 cnf(1285,plain, % 60.25/60.26 (E(f6(f8(f1(f1(f1(f1(f1(x12851)))))),f8(x12852)),f6(f8(f1(x12851)),f8(x12852)))), % 60.25/60.26 inference(scs_inference,[],[1280,1281,817,2,3])). % 60.25/60.26 cnf(1288,plain, % 60.25/60.26 (E(f6(f8(f1(x12881)),f8(x12882)),f6(f8(f1(f1(f1(f1(f1(x12881)))))),f8(x12882)))), % 60.25/60.26 inference(scs_inference,[],[1285,2])). % 60.25/60.26 cnf(1289,plain, % 60.25/60.26 (E(f6(f8(f1(f1(f1(f1(f1(x12891)))))),f8(x12892)),f6(f8(f1(f1(x12891))),f8(x12892)))), % 60.25/60.26 inference(scs_inference,[],[1285,770,2,3])). % 60.25/60.26 cnf(1292,plain, % 60.25/60.26 (E(f6(f8(f1(f1(x12921))),f8(x12922)),f6(f8(f1(f1(f1(f1(f1(x12921)))))),f8(x12922)))), % 60.25/60.26 inference(scs_inference,[],[1289,2])). % 60.25/60.26 cnf(1293,plain, % 60.25/60.26 (E(f6(f8(f1(x12931)),f8(f1(f1(x12932)))),f6(f8(f1(f1(f1(x12931)))),f8(x12932)))), % 60.25/60.26 inference(scs_inference,[],[1288,1289,1145,2,3])). % 60.25/60.26 cnf(1296,plain, % 60.25/60.26 (E(f6(f8(f1(f1(f1(x12961)))),f8(x12962)),f6(f8(f1(x12961)),f8(f1(f1(x12962)))))), % 60.25/60.26 inference(scs_inference,[],[1293,2])). % 60.25/60.26 cnf(1297,plain, % 60.25/60.26 (E(f6(f8(f1(f1(x12971))),f8(f1(x12972))),f6(f8(f1(x12971)),f8(x12972)))), % 60.25/60.26 inference(scs_inference,[],[1292,1293,1125,2,3])). % 60.25/60.26 cnf(1300,plain, % 60.25/60.26 (E(f12(f8(f1(x13001)),x13002),f12(f8(x13001),x13002))), % 60.25/60.26 inference(scs_inference,[],[38,2,6])). % 60.25/60.26 cnf(1301,plain, % 60.25/60.26 (E(f6(f8(f1(x13011)),f8(x13012)),f6(f8(f1(f1(x13011))),f8(f1(x13012))))), % 60.25/60.26 inference(scs_inference,[],[1297,2])). % 60.25/60.26 cnf(1302,plain, % 60.25/60.26 (E(f6(f8(f1(f1(f1(f1(x13021))))),f8(f1(x13022))),f6(f8(f1(x13021)),f8(f1(f1(x13022)))))), % 60.25/60.26 inference(scs_inference,[],[1297,1296,2,3])). % 60.25/60.26 cnf(1305,plain, % 60.25/60.26 (E(f11(f8(f1(x13051)),x13052),f11(f8(x13051),x13052))), % 60.25/60.26 inference(scs_inference,[],[38,2,14])). % 60.25/60.26 cnf(1306,plain, % 60.25/60.26 (E(f6(f8(f1(x13061)),f8(f1(f1(x13062)))),f6(f8(f1(f1(f1(f1(x13061))))),f8(f1(x13062))))), % 60.25/60.26 inference(scs_inference,[],[1302,2])). % 60.25/60.26 cnf(1307,plain, % 60.25/60.26 (E(f11(f8(f1(x13071)),f8(f1(f12(f8(f1(x13072)),x13073)))),f11(f8(x13071),f8(f12(f8(x13072),x13073))))), % 60.25/60.26 inference(scs_inference,[],[1305,751,1302,2,3])). % 60.25/60.26 cnf(1310,plain, % 60.25/60.26 (E(f11(x13101,f8(f1(x13102))),f11(x13101,f8(x13102)))), % 60.25/60.26 inference(scs_inference,[],[38,2,15])). % 60.25/60.26 cnf(1312,plain, % 60.25/60.26 (E(f6(f8(f1(x13121)),f8(f1(f1(f1(x13122))))),f6(f8(x13121),f8(f1(x13122))))), % 60.25/60.26 inference(scs_inference,[],[1284,1301,1307,2,3])). % 60.25/60.26 cnf(1315,plain, % 60.25/60.26 (E(f3(x13151,f8(f1(x13152)),x13153),f3(x13151,f8(x13152),x13153))), % 60.25/60.26 inference(scs_inference,[],[38,2,19])). % 60.25/60.26 cnf(1316,plain, % 60.25/60.26 (E(f6(f8(x13161),f8(f1(x13162))),f6(f8(f1(x13161)),f8(f1(f1(f1(x13162))))))), % 60.25/60.26 inference(scs_inference,[],[1312,2])). % 60.25/60.26 cnf(1317,plain, % 60.25/60.26 (E(f11(f8(f1(f12(f8(f1(x13171)),x13172))),f8(f1(f1(x13173)))),f11(f8(f12(f8(x13171),x13172)),f8(x13173)))), % 60.25/60.26 inference(scs_inference,[],[1310,1312,1064,2,3])). % 60.25/60.26 cnf(1319,plain, % 60.25/60.26 (E(f3(x13191,x13192,f8(f1(x13193))),f3(x13191,x13192,f8(x13193)))), % 60.25/60.26 inference(scs_inference,[],[38,2,20])). % 60.25/60.26 cnf(1320,plain, % 60.25/60.26 (E(f11(f8(f12(f8(x13201),x13202)),f8(x13203)),f11(f8(f1(f12(f8(f1(x13201)),x13202))),f8(f1(f1(x13203)))))), % 60.25/60.26 inference(scs_inference,[],[1317,2])). % 60.25/60.26 cnf(1321,plain, % 60.25/60.26 (E(f3(f8(f1(f1(f1(f1(x13211))))),f8(f1(x13212)),f8(f1(f1(x13213)))),f3(f8(f1(f1(x13211))),f8(x13212),f8(x13213)))), % 60.25/60.26 inference(scs_inference,[],[1268,1317,1319,2,3])). % 60.25/60.26 cnf(1325,plain, % 60.25/60.26 (E(f3(f8(f1(f1(x13251))),f8(x13252),f8(x13253)),f3(f8(f1(f1(f1(f1(x13251))))),f8(f1(x13252)),f8(f1(f1(x13253)))))), % 60.25/60.26 inference(scs_inference,[],[1321,2])). % 60.25/60.26 cnf(1326,plain, % 60.25/60.26 (E(f6(f8(x13261),f8(f1(x13262))),f6(f8(f1(f1(f1(f1(x13261))))),f8(f1(f1(x13262)))))), % 60.25/60.26 inference(scs_inference,[],[1321,1306,1316,2,3])). % 60.25/60.26 cnf(1329,plain, % 60.25/60.26 (E(f6(f8(f1(f1(f1(f1(x13291))))),f8(f1(f1(x13292)))),f6(f8(x13291),f8(f1(x13292))))), % 60.25/60.26 inference(scs_inference,[],[1326,2])). % 60.25/60.26 cnf(1330,plain, % 60.25/60.26 (E(f3(f8(f1(f1(x13301))),f8(f1(x13302)),f8(x13303)),f3(f8(f1(f1(f1(f1(x13301))))),f8(f1(x13302)),f8(f1(f1(x13303)))))), % 60.25/60.26 inference(scs_inference,[],[1315,1325,1326,2,3])). % 60.25/60.26 cnf(1334,plain, % 60.25/60.26 (E(f3(f8(f1(f1(f1(f1(x13341))))),f8(f1(x13342)),f8(f1(f1(x13343)))),f3(f8(f1(f1(x13341))),f8(f1(x13342)),f8(x13343)))), % 60.25/60.26 inference(scs_inference,[],[1330,2])). % 60.25/60.26 cnf(1335,plain, % 60.25/60.26 (E(f6(f8(f1(f1(x13351))),f8(f1(f1(f1(x13352))))),f6(f8(x13351),f8(f1(x13352))))), % 60.25/60.26 inference(scs_inference,[],[1329,1330,977,2,3])). % 60.25/60.26 cnf(1338,plain, % 60.25/60.26 (E(f6(f8(x13381),f8(f1(x13382))),f6(f8(f1(f1(x13381))),f8(f1(f1(f1(x13382))))))), % 60.25/60.26 inference(scs_inference,[],[1335,2])). % 60.25/60.26 cnf(1339,plain, % 60.25/60.26 (E(f11(f13(f4(x13391,f8(f1(x13392)))),f8(f1(x13393))),f11(f13(f4(x13391,f8(x13392))),f8(x13393)))), % 60.25/60.26 inference(scs_inference,[],[1335,1310,335,2,3])). % 60.25/60.26 cnf(1343,plain, % 60.25/60.26 (E(f11(f13(f4(x13431,f8(x13432))),f8(x13433)),f11(f13(f4(x13431,f8(f1(x13432)))),f8(f1(x13433))))), % 60.25/60.26 inference(scs_inference,[],[1339,2])). % 60.25/60.26 cnf(1344,plain, % 60.25/60.26 (E(f6(f8(x13441),f8(f1(x13442))),f6(f8(f1(f1(f1(x13441)))),f8(x13442)))), % 60.25/60.26 inference(scs_inference,[],[1339,1338,1157,2,3])). % 60.25/60.26 cnf(1346,plain, % 60.25/60.26 (E(f6(f8(f1(f1(f1(x13461)))),f8(x13462)),f6(f8(x13461),f8(f1(x13462))))), % 60.25/60.26 inference(scs_inference,[],[1344,2])). % 60.25/60.26 cnf(1347,plain, % 60.25/60.26 (E(f6(f8(x13471),f8(f1(x13472))),f6(f8(f1(f1(f1(f1(f1(x13471)))))),f8(f1(x13472))))), % 60.25/60.26 inference(scs_inference,[],[1344,988,2,3])). % 60.25/60.26 cnf(1350,plain, % 60.25/60.26 (E(f6(f8(f1(f1(f1(f1(f1(x13501)))))),f8(f1(x13502))),f6(f8(x13501),f8(f1(x13502))))), % 60.25/60.26 inference(scs_inference,[],[1347,2])). % 60.25/60.26 cnf(1351,plain, % 60.25/60.26 (E(f6(f8(x13511),f8(f1(x13512))),f6(f8(f1(f1(x13511))),f8(f1(f1(x13512)))))), % 60.25/60.26 inference(scs_inference,[],[1346,1347,2,3])). % 60.25/60.26 cnf(1354,plain, % 60.25/60.26 (E(f6(f8(f1(f1(x13541))),f8(f1(f1(x13542)))),f6(f8(x13541),f8(f1(x13542))))), % 60.25/60.26 inference(scs_inference,[],[1351,2])). % 60.25/60.26 cnf(1355,plain, % 60.25/60.26 (E(f11(f8(f12(f8(x13551),x13552)),f8(x13553)),f11(f8(f12(f8(x13551),x13552)),f8(f1(f1(x13553)))))), % 60.25/60.26 inference(scs_inference,[],[1320,1351,524,2,3])). % 60.25/60.26 cnf(1358,plain, % 60.25/60.26 (E(f12(f8(f1(x13581)),f10(f4(f8(x13582),x13583))),f12(f8(x13581),f10(f4(f8(f1(x13582)),x13583))))), % 60.25/60.26 inference(scs_inference,[],[1300,1355,263,2,3])). % 60.25/60.26 cnf(1362,plain, % 60.25/60.26 (E(f12(f8(x13621),f10(f4(f8(f1(x13622)),x13623))),f12(f8(f1(x13621)),f10(f4(f8(x13622),x13623))))), % 60.25/60.26 inference(scs_inference,[],[1358,2])). % 60.25/60.26 cnf(1363,plain, % 60.25/60.26 (E(f12(f8(f1(f1(x13631))),f10(f4(f8(x13632),x13633))),f12(f8(x13631),f10(f4(f8(f1(x13632)),x13633))))), % 60.25/60.26 inference(scs_inference,[],[1358,1300,2,3])). % 60.25/60.26 cnf(1367,plain, % 60.25/60.26 (E(f3(f13(f4(x13671,f8(x13672))),f8(f1(x13673)),x13674),f3(f13(f4(x13671,f8(f1(x13672)))),f8(x13673),x13674))), % 60.25/60.26 inference(scs_inference,[],[1363,1315,282,2,3])). % 60.25/60.26 cnf(1371,plain, % 60.25/60.26 (E(f3(f13(f4(x13711,f8(f1(x13712)))),f8(x13713),x13714),f3(f13(f4(x13711,f8(x13712))),f8(f1(x13713)),x13714))), % 60.25/60.26 inference(scs_inference,[],[1367,2])). % 60.25/60.26 cnf(1372,plain, % 60.25/60.26 (E(f3(f13(f4(x13721,f8(x13722))),f8(f1(x13723)),f8(f1(x13724))),f3(f13(f4(x13721,f8(f1(x13722)))),f8(x13723),f8(x13724)))), % 60.25/60.26 inference(scs_inference,[],[1367,1319,2,3])). % 60.25/60.26 cnf(1376,plain, % 60.25/60.26 (E(f3(f13(f4(x13761,f8(f1(x13762)))),f8(x13763),f8(x13764)),f3(f13(f4(x13761,f8(x13762))),f8(f1(x13763)),f8(f1(x13764))))), % 60.25/60.26 inference(scs_inference,[],[1372,2])). % 60.25/60.26 cnf(1377,plain, % 60.25/60.26 (E(f3(f13(f4(x13771,f8(x13772))),f8(f1(f1(x13773))),f8(f1(x13774))),f3(f13(f4(x13771,f8(f1(f1(x13772))))),f8(x13773),f8(x13774)))), % 60.25/60.26 inference(scs_inference,[],[1372,1367,2,3])). % 60.25/60.26 cnf(1380,plain, % 60.25/60.26 (E(f3(f13(f4(x13801,f8(f1(f1(x13802))))),f8(x13803),f8(x13804)),f3(f13(f4(x13801,f8(x13802))),f8(f1(f1(x13803))),f8(f1(x13804))))), % 60.25/60.26 inference(scs_inference,[],[1377,2])). % 60.25/60.26 cnf(1381,plain, % 60.25/60.26 (E(f3(f8(f1(f1(f1(f1(x13811))))),f8(f1(x13812)),f8(f1(f1(x13813)))),f3(f8(f1(x13811)),f8(f1(x13812)),f8(f1(x13813))))), % 60.25/60.26 inference(scs_inference,[],[1334,1377,803,2,3])). % 60.25/60.26 cnf(1385,plain, % 60.25/60.26 (E(f3(f13(f4(x13851,f8(f1(x13852)))),f8(x13853),f8(f1(x13854))),f3(f13(f4(x13851,f8(x13852))),f8(f1(x13853)),f8(x13854)))), % 60.25/60.26 inference(scs_inference,[],[1371,1381,1319,2,3])). % 60.25/60.26 cnf(1389,plain, % 60.25/60.26 (E(f3(f13(f4(x13891,f8(x13892))),f8(f1(x13893)),f8(x13894)),f3(f13(f4(x13891,f8(f1(x13892)))),f8(x13893),f8(f1(x13894))))), % 60.25/60.26 inference(scs_inference,[],[1385,2])). % 60.25/60.26 cnf(1390,plain, % 60.25/60.26 (E(f3(f13(f4(x13901,f8(f1(f1(x13902))))),f8(x13903),f8(x13904)),f3(f13(f4(x13901,f8(x13902))),f8(f1(f1(x13903))),f8(x13904)))), % 60.25/60.26 inference(scs_inference,[],[1385,1376,2,3])). % 60.25/60.26 cnf(1394,plain, % 60.25/60.26 (E(f3(f13(f4(x13941,f8(x13942))),f8(f1(f1(x13943))),f8(x13944)),f3(f13(f4(x13941,f8(f1(f1(x13942))))),f8(x13943),f8(x13944)))), % 60.25/60.26 inference(scs_inference,[],[1390,2])). % 60.25/60.26 cnf(1395,plain, % 60.25/60.26 (E(f3(f8(f1(f1(x13951))),f8(f1(x13952)),f8(f1(f1(f1(x13953))))),f3(f8(f1(f1(f1(x13951)))),f8(f1(x13952)),f8(x13953)))), % 60.25/60.26 inference(scs_inference,[],[1390,1210,1009,2,3])). % 60.25/60.26 cnf(1400,plain, % 60.25/60.26 (E(f3(f8(f1(f1(x14001))),f8(x14002),f8(f1(f1(x14003)))),f3(f8(f1(f1(f1(x14001)))),f8(f1(f1(f1(x14002)))),f8(x14003)))), % 60.25/60.26 inference(scs_inference,[],[1395,1246,2,3])). % 60.25/60.26 cnf(1404,plain, % 60.25/60.26 (E(f3(f8(f1(f1(x14041))),f8(x14042),f8(f1(f1(f1(x14043))))),f3(f8(f1(f1(f1(x14041)))),f8(x14042),f8(x14043)))), % 60.25/60.26 inference(scs_inference,[],[1400,1218,2,3])). % 60.25/60.26 cnf(1409,plain, % 60.25/60.26 (E(f3(f8(f1(f1(f1(x14091)))),f8(f1(x14092)),f8(f1(f1(f1(x14093))))),f3(f8(f1(f1(x14091))),f8(x14092),f8(x14093)))), % 60.25/60.26 inference(scs_inference,[],[1404,1173,2,3])). % 60.25/60.26 cnf(1414,plain, % 60.25/60.26 (E(f3(f13(f4(x14141,f8(x14142))),f8(f1(f1(f1(x14143)))),f8(x14144)),f3(f13(f4(x14141,f8(f1(f1(x14142))))),f8(x14143),f8(x14144)))), % 60.25/60.26 inference(scs_inference,[],[1394,1409,1315,2,3])). % 60.25/60.26 cnf(1417,plain, % 60.25/60.26 (E(f3(f13(f4(x14171,f8(f1(f1(x14172))))),f8(x14173),f8(x14174)),f3(f13(f4(x14171,f8(x14172))),f8(f1(f1(f1(x14173)))),f8(x14174)))), % 60.25/60.26 inference(scs_inference,[],[1414,2])). % 60.25/60.26 cnf(1418,plain, % 60.25/60.26 (E(f3(f13(f4(x14181,f8(x14182))),f8(f1(f1(f1(x14183)))),f8(x14184)),f3(f13(f4(x14181,f8(x14182))),f8(f1(f1(x14183))),f8(f1(x14184))))), % 60.25/60.26 inference(scs_inference,[],[1414,1380,2,3])). % 60.25/60.26 cnf(1421,plain, % 60.25/60.26 (E(f3(f13(f4(x14211,f8(x14212))),f8(f1(f1(x14213))),f8(f1(x14214))),f3(f13(f4(x14211,f8(x14212))),f8(f1(f1(f1(x14213)))),f8(x14214)))), % 60.25/60.26 inference(scs_inference,[],[1418,2])). % 60.25/60.26 cnf(1422,plain, % 60.25/60.26 (E(f3(f13(f4(x14221,f8(f1(x14222)))),f8(f1(x14223)),f8(x14224)),f3(f13(f4(x14221,f8(x14222))),f8(f1(f1(f1(x14223)))),f8(f1(x14224))))), % 60.25/60.26 inference(scs_inference,[],[1417,1389,1418,2,3])). % 60.25/60.26 cnf(1426,plain, % 60.25/60.26 (E(f3(f13(f4(x14261,f8(x14262))),f8(f1(f1(f1(x14263)))),f8(f1(x14264))),f3(f13(f4(x14261,f8(f1(x14262)))),f8(f1(x14263)),f8(x14264)))), % 60.25/60.26 inference(scs_inference,[],[1422,2])). % 60.25/60.26 cnf(1427,plain, % 60.25/60.26 (E(f3(f13(f4(x14271,f8(f1(x14272)))),f8(f1(x14273)),f8(x14274)),f3(f13(f4(x14271,f8(x14272))),f8(f1(f1(f1(f1(x14273))))),f8(x14274)))), % 60.25/60.26 inference(scs_inference,[],[1421,1422,2,3])). % 60.25/60.26 cnf(1430,plain, % 60.25/60.26 (E(f3(f13(f4(x14301,f8(x14302))),f8(f1(f1(f1(f1(x14303))))),f8(x14304)),f3(f13(f4(x14301,f8(f1(x14302)))),f8(f1(x14303)),f8(x14304)))), % 60.25/60.26 inference(scs_inference,[],[1427,2])). % 60.25/60.26 cnf(1431,plain, % 60.25/60.26 (E(f3(f13(f4(x14311,f8(f1(x14312)))),f8(f1(x14313)),f8(f1(x14314))),f3(f13(f4(x14311,f8(f1(x14312)))),f8(f1(f1(x14313))),f8(x14314)))), % 60.25/60.26 inference(scs_inference,[],[1426,1427,2,3])). % 60.25/60.26 cnf(1435,plain, % 60.25/60.26 (E(f3(f13(f4(x14351,f8(f1(x14352)))),f8(f1(f1(x14353))),f8(x14354)),f3(f13(f4(x14351,f8(f1(x14352)))),f8(f1(x14353)),f8(f1(x14354))))), % 60.25/60.26 inference(scs_inference,[],[1431,2])). % 60.25/60.26 cnf(1453,plain, % 60.25/60.26 (E(f3(f8(f1(x14531)),f8(f1(x14532)),x14533),f3(f8(x14531),f8(x14532),x14533))), % 60.25/60.26 inference(scs_inference,[],[798,2])). % 60.25/60.26 cnf(1454,plain, % 60.25/60.26 (E(f3(f13(f4(x14541,f8(x14542))),f8(f1(f1(f1(f1(x14543))))),f8(x14544)),f3(f13(f4(x14541,f8(x14542))),f8(f1(f1(x14543))),f8(x14544)))), % 60.25/60.26 inference(scs_inference,[],[1430,1371,798,2,3])). % 60.25/60.26 cnf(1457,plain, % 60.25/60.26 (E(f3(f13(f4(x14571,f8(x14572))),f8(f1(f1(x14573))),f8(x14574)),f3(f13(f4(x14571,f8(x14572))),f8(f1(f1(f1(f1(x14573))))),f8(x14574)))), % 60.25/60.26 inference(scs_inference,[],[1454,2])). % 60.25/60.26 cnf(1463,plain, % 60.25/60.26 (E(f3(f13(f4(x14631,f8(x14632))),f8(f1(f1(x14633))),f8(x14634)),f3(f13(f4(x14631,f8(f1(f1(x14632))))),f8(f1(f1(x14633))),f8(x14634)))), % 60.25/60.26 inference(scs_inference,[],[1457,1394,818,2,3])). % 60.25/60.26 cnf(1467,plain, % 60.25/60.26 (E(f3(f13(f4(x14671,f8(x14672))),f8(f1(f1(x14673))),f8(x14674)),f3(f13(f4(x14671,f8(f1(f1(x14672))))),f8(f1(x14673)),f8(f1(x14674))))), % 60.25/60.26 inference(scs_inference,[],[1463,1435,2,3])). % 60.25/60.26 cnf(1470,plain, % 60.25/60.26 (E(f3(f8(f1(x14701)),f8(f1(x14702)),f13(f4(x14703,f8(x14704)))),f3(f8(x14701),f8(x14702),f13(f4(x14703,f8(f1(x14704))))))), % 60.25/60.26 inference(scs_inference,[],[1467,1453,286,2,3])). % 60.25/60.26 cnf(1475,plain, % 60.25/60.26 (E(f3(f8(f1(f1(x14751))),f8(f1(f1(x14752))),f13(f4(x14753,f8(x14754)))),f3(f8(x14751),f8(x14752),f13(f4(x14753,f8(f1(x14754))))))), % 60.25/60.26 inference(scs_inference,[],[1470,1453,2,3])). % 60.25/60.26 cnf(1479,plain, % 60.25/60.26 (E(f12(f8(x14791),f10(f4(f8(f1(f1(x14792))),x14793))),f12(f8(f1(x14791)),f10(f4(f8(x14792),x14793))))), % 60.25/60.26 inference(scs_inference,[],[1362,1475,262,2,3])). % 60.25/60.26 cnf(1484,plain, % 60.25/60.26 (E(f5(f13(f4(x14841,f8(f1(f1(x14842))))),f8(x14843)),f5(f13(f4(x14841,f8(x14842))),f8(f1(x14843))))), % 60.25/60.26 inference(scs_inference,[],[1133,1479,287,2,3])). % 60.25/60.26 cnf(1488,plain, % 60.25/60.26 (E(f5(f13(f4(x14881,f8(x14882))),f8(f1(x14883))),f5(f13(f4(x14881,f8(f1(f1(x14882))))),f8(x14883)))), % 60.25/60.26 inference(scs_inference,[],[1484,2])). % 60.25/60.26 cnf(1489,plain, % 60.25/60.26 (E(f5(f13(f4(x14891,f8(f1(f1(x14892))))),f8(f1(x14893))),f5(f13(f4(x14891,f8(f1(x14892)))),f8(x14893)))), % 60.25/60.26 inference(scs_inference,[],[1484,1134,2,3])). % 60.25/60.26 cnf(1492,plain, % 60.25/60.26 (E(f5(f13(f4(x14921,f8(f1(x14922)))),f8(x14923)),f5(f13(f4(x14921,f8(f1(f1(x14922))))),f8(f1(x14923))))), % 60.25/60.26 inference(scs_inference,[],[1489,2])). % 60.25/60.26 cnf(1493,plain, % 60.25/60.26 (E(f5(f13(f4(x14931,f8(x14932))),f8(f1(x14933))),f5(f13(f4(x14931,f8(f1(x14932)))),f8(f1(f1(x14933)))))), % 60.25/60.26 inference(scs_inference,[],[1488,1489,1137,2,3])). % 60.25/60.26 cnf(1497,plain, % 60.25/60.26 (E(f5(f13(f4(x14971,f8(f1(x14972)))),f8(x14973)),f5(f13(f4(x14971,f8(f1(x14972)))),f8(f1(f1(x14973)))))), % 60.25/60.26 inference(scs_inference,[],[1492,1493,1133,2,3])). % 60.25/60.26 cnf(1500,plain, % 60.25/60.26 (E(f5(f13(f4(x15001,f8(f1(x15002)))),f8(f1(f1(x15003)))),f5(f13(f4(x15001,f8(f1(x15002)))),f8(x15003)))), % 60.25/60.26 inference(scs_inference,[],[1497,2])). % 60.25/60.26 cnf(1501,plain, % 60.25/60.26 (E(f11(f13(f4(x15011,f8(x15012))),f8(x15013)),f11(f13(f4(x15011,f8(f1(f1(x15012))))),f8(f1(x15013))))), % 60.25/60.26 inference(scs_inference,[],[1343,1497,334,2,3])). % 60.25/60.26 cnf(1504,plain, % 60.25/60.26 (E(f11(f13(f4(x15041,f8(f1(f1(x15042))))),f8(f1(x15043))),f11(f13(f4(x15041,f8(x15042))),f8(x15043)))), % 60.25/60.26 inference(scs_inference,[],[1501,2])). % 60.25/60.26 cnf(1505,plain, % 60.25/60.26 (E(f5(f13(f4(x15051,f8(f1(f1(x15052))))),f8(f1(f1(x15053)))),f5(f13(f4(x15051,f8(x15052))),f8(f1(x15053))))), % 60.25/60.26 inference(scs_inference,[],[1500,1501,1484,2,3])). % 60.25/60.26 cnf(1510,plain, % 60.25/60.26 (E(f11(f13(f4(x15101,f8(f1(f1(f1(x15102)))))),f8(f1(x15103))),f11(f13(f4(x15101,f8(x15102))),f8(x15103)))), % 60.25/60.26 inference(scs_inference,[],[1504,1505,335,2,3])). % 60.25/60.26 cnf(1514,plain, % 60.25/60.26 (E(f11(f13(f4(x15141,f8(x15142))),f8(x15143)),f11(f13(f4(x15141,f8(f1(f1(f1(x15142)))))),f8(f1(x15143))))), % 60.25/60.26 inference(scs_inference,[],[1510,2])). % 60.25/60.26 cnf(1515,plain, % 60.25/60.26 (E(f6(f8(f1(f1(f1(f1(f1(x15151)))))),f8(f1(x15152))),f6(f8(x15151),f8(x15152)))), % 60.25/60.26 inference(scs_inference,[],[1510,1350,792,2,3])). % 60.25/60.26 cnf(1518,plain, % 60.25/60.26 (E(f6(f8(x15181),f8(x15182)),f6(f8(f1(f1(f1(f1(f1(x15181)))))),f8(f1(x15182))))), % 60.25/60.26 inference(scs_inference,[],[1515,2])). % 60.25/60.26 cnf(1519,plain, % 60.25/60.26 (E(f11(f13(f4(x15191,f8(x15192))),f8(x15193)),f11(f13(f4(x15191,f8(f1(f1(x15192))))),f8(x15193)))), % 60.25/60.26 inference(scs_inference,[],[1515,1514,1339,2,3])). % 60.25/60.26 cnf(1522,plain, % 60.25/60.26 (E(f11(f13(f4(x15221,f8(f1(f1(x15222))))),f8(x15223)),f11(f13(f4(x15221,f8(x15222))),f8(x15223)))), % 60.25/60.26 inference(scs_inference,[],[1519,2])). % 60.25/60.26 cnf(1523,plain, % 60.25/60.26 (E(f6(f8(x15231),f8(f1(x15232))),f6(f8(f1(f1(f1(x15231)))),f8(f1(x15232))))), % 60.25/60.26 inference(scs_inference,[],[1519,1354,1518,2,3])). % 60.25/60.26 cnf(1527,plain, % 60.25/60.26 (E(f6(f8(f1(f1(f1(x15271)))),f8(f1(x15272))),f6(f8(x15271),f8(f1(x15272))))), % 60.25/60.26 inference(scs_inference,[],[1523,2])). % 60.25/60.26 cnf(1528,plain, % 60.25/60.26 (E(f6(f8(x15281),f8(f1(f1(f1(x15282))))),f6(f8(f1(f1(f1(x15281)))),f8(x15282)))), % 60.25/60.26 inference(scs_inference,[],[1523,1166,2,3])). % 60.25/60.26 cnf(1532,plain, % 60.25/60.26 (E(f6(f8(f1(f1(f1(x15321)))),f8(x15322)),f6(f8(x15321),f8(f1(f1(f1(x15322))))))), % 60.25/60.26 inference(scs_inference,[],[1528,2])). % 60.25/60.26 cnf(1533,plain, % 60.25/60.26 (E(f6(f8(x15331),f8(f1(f1(f1(f1(x15332)))))),f6(f8(x15331),f8(f1(x15332))))), % 60.25/60.26 inference(scs_inference,[],[1528,1527,2,3])). % 60.25/60.26 cnf(1538,plain, % 60.25/60.26 (E(f11(f13(f4(x15381,f8(f1(f1(x15382))))),f8(x15383)),f11(f13(f4(x15381,f8(f1(x15382)))),f8(f1(x15383))))), % 60.25/60.26 inference(scs_inference,[],[1522,1533,1343,2,3])). % 60.25/60.26 cnf(1541,plain, % 60.25/60.26 (E(f11(f13(f4(x15411,f8(f1(x15412)))),f8(f1(x15413))),f11(f13(f4(x15411,f8(f1(f1(x15412))))),f8(x15413)))), % 60.25/60.26 inference(scs_inference,[],[1538,2])). % 60.25/60.26 cnf(1542,plain, % 60.25/60.26 (E(f11(f13(f4(x15421,f8(f1(f1(f1(x15422)))))),f8(x15423)),f11(f13(f4(x15421,f8(x15422))),f8(x15423)))), % 60.25/60.26 inference(scs_inference,[],[1538,1504,2,3])). % 60.25/60.26 cnf(1545,plain, % 60.25/60.26 (E(f11(f13(f4(x15451,f8(x15452))),f8(x15453)),f11(f13(f4(x15451,f8(f1(f1(f1(x15452)))))),f8(x15453)))), % 60.25/60.26 inference(scs_inference,[],[1542,2])). % 60.25/60.26 cnf(1546,plain, % 60.25/60.26 (E(f11(f13(f4(x15461,f8(f1(f1(x15462))))),f8(f1(f1(x15463)))),f11(f13(f4(x15461,f8(x15462))),f8(x15463)))), % 60.25/60.26 inference(scs_inference,[],[1541,1542,1510,2,3])). % 60.25/60.26 cnf(1550,plain, % 60.25/60.26 (E(f11(f13(f4(x15501,f8(x15502))),f8(x15503)),f11(f13(f4(x15501,f8(f1(f1(x15502))))),f8(f1(f1(x15503)))))), % 60.25/60.26 inference(scs_inference,[],[1546,2])). % 60.25/60.26 cnf(1551,plain, % 60.25/60.26 (E(f11(f13(f4(x15511,f8(x15512))),f8(f1(f1(x15513)))),f11(f13(f4(x15511,f8(f1(x15512)))),f8(x15513)))), % 60.25/60.26 inference(scs_inference,[],[1545,1546,2,3])). % 60.25/60.26 cnf(1556,plain, % 60.25/60.26 (E(f11(f13(f4(x15561,f8(f1(x15562)))),f8(f1(f1(x15563)))),f11(f13(f4(x15561,f8(x15562))),f8(x15563)))), % 60.25/60.26 inference(scs_inference,[],[1551,1522,2,3])). % 60.25/60.26 cnf(1560,plain, % 60.25/60.26 (E(f6(f8(f1(f1(f1(f1(x15601))))),f8(x15602)),f6(f8(x15601),f8(f1(x15602))))), % 60.25/60.26 inference(scs_inference,[],[1556,1532,1312,2,3])). % 60.25/60.26 cnf(1564,plain, % 60.25/60.26 (E(f6(f8(x15641),f8(f1(x15642))),f6(f8(f1(f1(f1(f1(x15641))))),f8(x15642)))), % 60.25/60.26 inference(scs_inference,[],[1560,2])). % 60.25/60.26 cnf(1565,plain, % 60.25/60.26 (E(f6(f8(f1(f1(f1(f1(x15651))))),f8(f1(x15652))),f6(f8(f1(x15651)),f8(x15652)))), % 60.25/60.26 inference(scs_inference,[],[1560,823,2,3])). % 60.25/60.26 cnf(1569,plain, % 60.25/60.26 (E(f6(f8(f1(x15691)),f8(x15692)),f6(f8(f1(f1(f1(f1(x15691))))),f8(f1(x15692))))), % 60.25/60.26 inference(scs_inference,[],[1565,2])). % 60.25/60.26 cnf(1570,plain, % 60.25/60.26 (E(f6(f8(f1(x15701)),f8(f1(f1(x15702)))),f6(f8(x15701),f8(x15702)))), % 60.25/60.26 inference(scs_inference,[],[1564,1565,1515,2,3])). % 60.25/60.26 cnf(1572,plain, % 60.25/60.26 (E(f6(f8(x15721),f8(x15722)),f6(f8(f1(x15721)),f8(f1(f1(x15722)))))), % 60.25/60.26 inference(scs_inference,[],[1570,2])). % 60.25/60.26 cnf(1573,plain, % 60.25/60.26 (E(f6(f8(f1(f1(x15731))),f8(f1(f1(f1(f1(x15732)))))),f6(f8(f1(x15731)),f8(x15732)))), % 60.25/60.26 inference(scs_inference,[],[1570,828,2,3])). % 60.25/60.26 cnf(1577,plain, % 60.25/60.26 (E(f11(f13(f4(x15771,f8(f1(x15772)))),f8(x15773)),f11(f13(f4(x15771,f8(x15772))),f8(f1(x15773))))), % 60.25/60.26 inference(scs_inference,[],[1573,1550,1510,2,3])). % 60.25/60.26 cnf(1581,plain, % 60.25/60.26 (E(f11(f13(f4(x15811,f8(x15812))),f8(f1(x15813))),f11(f13(f4(x15811,f8(f1(x15812)))),f8(x15813)))), % 60.25/60.26 inference(scs_inference,[],[1577,2])). % 60.25/60.26 cnf(1582,plain, % 60.25/60.26 (E(f6(f8(x15821),f8(x15822)),f6(f8(f1(f1(f1(f1(x15821))))),f8(f1(f1(f1(x15822))))))), % 60.25/60.26 inference(scs_inference,[],[1569,1577,1572,2,3])). % 60.25/60.26 cnf(1584,plain, % 60.25/60.26 (E(f6(f8(f1(f1(f1(f1(x15841))))),f8(f1(f1(f1(x15842))))),f6(f8(x15841),f8(x15842)))), % 60.25/60.26 inference(scs_inference,[],[1582,2])). % 60.25/60.26 cnf(1585,plain, % 60.25/60.26 (E(f6(f8(x15851),f8(x15852)),f6(f8(f1(f1(f1(x15851)))),f8(x15852)))), % 60.25/60.26 inference(scs_inference,[],[1582,1146,2,3])). % 60.25/60.26 cnf(1588,plain, % 60.25/60.26 (E(f6(f8(f1(f1(f1(x15881)))),f8(x15882)),f6(f8(x15881),f8(x15882)))), % 60.25/60.26 inference(scs_inference,[],[1585,2])). % 60.25/60.26 cnf(1589,plain, % 60.25/60.26 (E(f6(f8(f1(x15891)),f8(f1(f1(f1(x15892))))),f6(f8(x15891),f8(x15892)))), % 60.25/60.26 inference(scs_inference,[],[1584,1585,2,3])). % 60.25/60.26 cnf(1592,plain, % 60.25/60.26 (E(f6(f8(x15921),f8(x15922)),f6(f8(f1(x15921)),f8(f1(f1(f1(x15922))))))), % 60.25/60.26 inference(scs_inference,[],[1589,2])). % 60.25/60.26 cnf(1593,plain, % 60.25/60.26 (E(f11(f13(f4(x15931,f8(x15932))),f8(f1(x15933))),f11(f13(f4(x15931,f8(f1(f1(f1(x15932)))))),f8(x15933)))), % 60.25/60.26 inference(scs_inference,[],[1581,1589,1519,2,3])). % 60.25/60.26 cnf(1596,plain, % 60.25/60.26 (E(f6(f8(f1(f1(f1(f1(x15961))))),f8(f1(f1(f1(x15962))))),f6(f8(f1(x15961)),f8(x15962)))), % 60.25/60.26 inference(scs_inference,[],[1588,1593,1166,2,3])). % 60.25/60.26 cnf(1600,plain, % 60.25/60.26 (E(f6(f8(f1(f1(f1(x16001)))),f8(x16002)),f6(f8(f1(x16001)),f8(x16002)))), % 60.25/60.26 inference(scs_inference,[],[1596,1592,2,3])). % 60.25/60.26 cnf(1603,plain, % 60.25/60.26 (E(f6(f8(f1(x16031)),f8(x16032)),f6(f8(f1(f1(f1(x16031)))),f8(x16032)))), % 60.25/60.26 inference(scs_inference,[],[1600,2])). % 60.25/60.26 cnf(1615,plain, % 60.25/60.26 (P1(f11(f9(a19),f12(f16(a19),f11(f9(a20),f11(f10(a23),f10(a26))))),f8(f8(f1(f1(f1(f6(a7,a14)))))),a21)), % 60.25/60.26 inference(scs_inference,[],[822,117,4,5,8,9,10,11,23,32])). % 60.25/60.26 cnf(1635,plain, % 60.25/60.26 (P1(f11(f9(a24),f12(f16(a24),f11(f9(a22),f11(f10(a26),f10(a27))))),f1(f6(a7,a14)),a21)), % 60.25/60.26 inference(scs_inference,[],[28,822,41,117,59,29,4,5,8,9,10,11,23,32,6,7,12,14,15,16,17,21,22,18,19,20,33,35,13,2,34])). % 60.25/60.26 cnf(1652,plain, % 60.25/60.26 (P1(f11(f9(a24),f12(f16(a24),f11(f9(a22),f11(f10(a26),f10(a27))))),f8(f1(f6(a7,a14))),a21)), % 60.25/60.26 inference(scs_inference,[],[837,1635,1615,30,35,18,15,33,23,32])). % 60.25/60.26 cnf(1676,plain, % 60.25/60.26 (P1(f12(f16(a24),f11(f9(a22),f11(f10(a26),f10(a27)))),f8(f1(f6(a7,a14))),a21)), % 60.25/60.26 inference(scs_inference,[],[1652,33])). % 60.25/60.26 cnf(1739,plain, % 60.25/60.26 (P1(f12(f16(a19),f11(f9(a20),f11(f10(a23),f10(a26)))),f8(f6(a7,a14)),a21)), % 60.25/60.26 inference(scs_inference,[],[87,33])). % 60.25/60.26 cnf(1795,plain, % 60.25/60.26 ($false), % 60.25/60.26 inference(scs_inference,[],[28,1739,1603,1676,89,31,27,32,33,15,18,4,16,21,22,23,20,6,5,12,7,17,9,10,19,14,11,8,13,36,25]), % 60.25/60.26 ['proof']). % 60.25/60.26 % SZS output end Proof % 60.25/60.26 % Total time :59.580000s %------------------------------------------------------------------------------