%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SWV361-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 : n023.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:58 EDT 2024 % Result : Unsatisfiable 62.11s 62.28s % Output : CNFRefutation 62.16s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : SWV361-2 : TPTP v8.2.0. Released v3.2.0. % 0.03/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.35 % Computer : n023.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Thu Jun 20 20:50:54 EDT 2024 % 0.13/0.35 % CPUTime : % 0.51/0.57 start to proof:theBenchmark % 62.11/62.27 %------------------------------------------- % 62.11/62.27 % File :CSE---1.7 % 62.11/62.27 % Problem :theBenchmark % 62.11/62.27 % Transform :cnf % 62.11/62.27 % Format :tptp:raw % 62.11/62.27 % Command :java -jar mcs_scs.jar %d %s % 62.11/62.27 % 62.11/62.27 % Result :Theorem 61.560000s % 62.11/62.27 % Output :CNFRefutation 61.560000s % 62.11/62.27 %------------------------------------------- % 62.11/62.28 %------------------------------------------------------------------------------ % 62.11/62.28 % File : SWV361-2 : TPTP v8.2.0. Released v3.2.0. % 62.11/62.28 % Domain : Software Verification (Security) % 62.11/62.28 % Problem : Cryptographic protocol problem for Yahalom % 62.11/62.28 % Version : [Pau06] axioms : Reduced > Especial. % 62.11/62.28 % English : % 62.11/62.28 % 62.11/62.28 % Refs : [Pau06] Paulson (2006), Email to G. Sutcliffe % 62.11/62.28 % Source : [Pau06] % 62.11/62.28 % Names : % 62.11/62.28 % 62.11/62.28 % Status : Unsatisfiable % 62.11/62.28 % 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.22 v4.0.1, 0.17 v3.3.0, 0.14 v3.2.0 % 62.11/62.28 % Syntax : Number of clauses : 10 ( 5 unt; 0 nHn; 9 RR) % 62.11/62.28 % Number of literals : 18 ( 1 equ; 9 neg) % 62.11/62.28 % Maximal clause size : 4 ( 1 avg) % 62.11/62.28 % Maximal term depth : 7 ( 2 avg) % 62.11/62.28 % Number of predicates : 2 ( 1 usr; 0 prp; 2-3 aty) % 62.11/62.28 % Number of functors : 25 ( 25 usr; 13 con; 0-3 aty) % 62.11/62.28 % Number of variables : 21 ( 10 sgn) % 62.11/62.28 % SPC : CNF_UNS_RFO_SEQ_HRN % 62.11/62.28 % 62.11/62.28 % Comments : The problems in the [Pau06] collection each have very many axioms, % 62.11/62.28 % of which only a small selection are required for the refutation. % 62.11/62.28 % The mission is to find those few axioms, after which a refutation % 62.11/62.28 % can be quite easily found. This version has only the necessary % 62.11/62.28 % axioms. % 62.11/62.28 %------------------------------------------------------------------------------ % 62.11/62.28 cnf(cls_Event_OSays__imp__spies_0,axiom, % 62.11/62.28 ( ~ c_in(c_Event_Oevent_OSays(V_A,V_B,V_X),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent) % 62.11/62.28 | c_in(V_X,c_Event_Oknows(c_Message_Oagent_OSpy,V_evs),tc_Message_Omsg) ) ). % 62.11/62.28 % 62.11/62.28 cnf(cls_Message_OMPair__parts_0,axiom, % 62.11/62.28 ( ~ c_in(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Oparts(V_H),tc_Message_Omsg) % 62.11/62.28 | c_in(V_Y,c_Message_Oparts(V_H),tc_Message_Omsg) ) ). % 62.11/62.28 % 62.11/62.28 cnf(cls_Message_Oparts_OInj_0,axiom, % 62.11/62.28 ( ~ c_in(V_X,V_H,tc_Message_Omsg) % 62.11/62.28 | c_in(V_X,c_Message_Oparts(V_H),tc_Message_Omsg) ) ). % 62.11/62.28 % 62.11/62.28 cnf(cls_Message_Oparts__analz_0,axiom, % 62.11/62.28 c_Message_Oparts(c_Message_Oanalz(V_H)) = c_Message_Oparts(V_H) ). % 62.11/62.28 % 62.11/62.28 cnf(cls_Yahalom_OGets__imp__analz__Spy__dest_0,axiom, % 62.11/62.28 ( ~ c_in(V_evs,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)) % 62.11/62.28 | ~ c_in(c_Event_Oevent_OGets(V_B,V_X),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent) % 62.11/62.28 | c_in(V_X,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg) ) ). % 62.11/62.28 % 62.11/62.28 cnf(cls_Yahalom_Ono__nonce__YM1__YM2_0,axiom, % 62.11/62.28 ( ~ c_in(V_evs,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)) % 62.11/62.28 | ~ 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) % 62.11/62.28 | ~ 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) % 62.11/62.28 | c_in(c_Message_Omsg_ONonce(V_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg) ) ). % 62.11/62.28 % 62.11/62.28 cnf(cls_conjecture_2,negated_conjecture, % 62.11/62.28 c_in(v_evs3,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)) ). % 62.11/62.28 % 62.11/62.28 cnf(cls_conjecture_5,negated_conjecture, % 62.11/62.28 c_in(c_Event_Oevent_OGets(c_Message_Oagent_OServer,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NBa)))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent) ). % 62.11/62.28 % 62.11/62.28 cnf(cls_conjecture_7,negated_conjecture, % 62.11/62.28 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_evs3,tc_Event_Oevent),tc_Event_Oevent) ). % 62.11/62.28 % 62.11/62.28 cnf(cls_conjecture_8,negated_conjecture, % 62.11/62.28 ~ c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ). % 62.11/62.28 % 62.11/62.28 %------------------------------------------------------------------------------ % 62.11/62.28 %------------------------------------------- % 62.11/62.28 % Proof found % 62.11/62.28 % SZS status Theorem for theBenchmark % 62.11/62.28 % SZS output start Proof % 62.11/62.28 %ClaNum:35(EqnAxiom:25) % 62.11/62.28 %VarNum:36(SingletonVarNum:21) % 62.11/62.28 %MaxLitNum:4 % 62.11/62.28 %MaxfuncDepth:6 % 62.11/62.28 %SharedTerms:40 % 62.11/62.28 %goalClause: 27 28 29 30 % 62.11/62.28 %singleGoalClaCount:4 % 62.11/62.28 [27]P1(a13,a14,f17(a16)) % 62.11/62.28 [30]~P1(f10(a23),f1(f6(a7,a13)),a21) % 62.11/62.28 [28]P1(f3(a2,f11(f9(a18),f12(f15(a18),f11(f9(a19),f11(f10(a23),f10(a25)))))),f4(a13,a16),a16) % 62.11/62.28 [29]P1(f5(a22,a2,f11(f9(a22),f12(f15(a22),f11(f9(a20),f11(f10(a24),f10(a23)))))),f4(a13,a16),a16) % 62.11/62.28 [26]E(f8(f1(x261)),f8(x261)) % 62.11/62.28 [31]~P1(x311,x312,a21)+P1(x311,f8(x312),a21) % 62.11/62.28 [32]P1(x321,f8(x322),a21)+~P1(f11(x323,x321),f8(x322),a21) % 62.11/62.28 [34]P1(x341,f6(a7,x342),a21)+~P1(f5(x343,x344,x341),f4(x342,a16),a16) % 62.11/62.28 [33]~P1(f3(x333,x331),f4(x332,a16),a16)+~P1(x332,a14,f17(a16))+P1(x331,f1(f6(a7,x332)),a21) % 62.11/62.28 [35]~P1(x352,a14,f17(a16))+P1(f10(x351),f1(f6(a7,x352)),a21)+~P1(f12(f15(x353),f11(f9(x354),f11(x355,f10(x351)))),f8(f6(a7,x352)),a21)+~P1(f12(f15(x356),f11(f9(x357),f11(f10(x351),x358))),f8(f6(a7,x352)),a21) % 62.11/62.28 %EqnAxiom % 62.11/62.28 [1]E(x11,x11) % 62.11/62.28 [2]E(x22,x21)+~E(x21,x22) % 62.11/62.28 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 62.11/62.28 [4]~E(x41,x42)+E(f1(x41),f1(x42)) % 62.11/62.28 [5]~E(x51,x52)+E(f8(x51),f8(x52)) % 62.11/62.28 [6]~E(x61,x62)+E(f11(x61,x63),f11(x62,x63)) % 62.11/62.28 [7]~E(x71,x72)+E(f11(x73,x71),f11(x73,x72)) % 62.11/62.28 [8]~E(x81,x82)+E(f17(x81),f17(x82)) % 62.11/62.28 [9]~E(x91,x92)+E(f9(x91),f9(x92)) % 62.11/62.28 [10]~E(x101,x102)+E(f15(x101),f15(x102)) % 62.11/62.28 [11]~E(x111,x112)+E(f5(x111,x113,x114),f5(x112,x113,x114)) % 62.11/62.28 [12]~E(x121,x122)+E(f5(x123,x121,x124),f5(x123,x122,x124)) % 62.11/62.28 [13]~E(x131,x132)+E(f5(x133,x134,x131),f5(x133,x134,x132)) % 62.11/62.28 [14]~E(x141,x142)+E(f10(x141),f10(x142)) % 62.11/62.28 [15]~E(x151,x152)+E(f4(x151,x153),f4(x152,x153)) % 62.11/62.28 [16]~E(x161,x162)+E(f4(x163,x161),f4(x163,x162)) % 62.11/62.28 [17]~E(x171,x172)+E(f6(x171,x173),f6(x172,x173)) % 62.11/62.28 [18]~E(x181,x182)+E(f6(x183,x181),f6(x183,x182)) % 62.11/62.28 [19]~E(x191,x192)+E(f12(x191,x193),f12(x192,x193)) % 62.11/62.28 [20]~E(x201,x202)+E(f12(x203,x201),f12(x203,x202)) % 62.11/62.28 [21]~E(x211,x212)+E(f3(x211,x213),f3(x212,x213)) % 62.11/62.28 [22]~E(x221,x222)+E(f3(x223,x221),f3(x223,x222)) % 62.11/62.28 [23]P1(x232,x233,x234)+~E(x231,x232)+~P1(x231,x233,x234) % 62.11/62.28 [24]P1(x243,x242,x244)+~E(x241,x242)+~P1(x243,x241,x244) % 62.11/62.28 [25]P1(x253,x254,x252)+~E(x251,x252)+~P1(x253,x254,x251) % 62.11/62.28 % 62.11/62.28 %------------------------------------------- % 62.16/62.29 cnf(36,plain, % 62.16/62.29 (E(f8(x361),f8(f1(x361)))), % 62.16/62.29 inference(scs_inference,[],[26,2])). % 62.16/62.30 cnf(39,plain, % 62.16/62.30 (~E(f5(a22,a2,f11(f9(a22),f12(f15(a22),f11(f9(a20),f11(f10(a24),f10(a23)))))),f3(x391,f10(a23)))), % 62.16/62.30 inference(scs_inference,[],[27,30,29,26,2,33,23])). % 62.16/62.30 cnf(66,plain, % 62.16/62.30 (E(f9(f15(f8(x661))),f9(f15(f8(f1(x661)))))), % 62.16/62.30 inference(scs_inference,[],[36,9,10])). % 62.16/62.30 cnf(74,plain, % 62.16/62.30 (P1(f11(f9(a22),f12(f15(a22),f11(f9(a20),f11(f10(a24),f10(a23))))),f8(f6(a7,a13)),a21)), % 62.16/62.30 inference(scs_inference,[],[29,31,34])). % 62.16/62.30 cnf(76,plain, % 62.16/62.30 (P1(f11(f9(a22),f12(f15(a22),f11(f9(a20),f11(f10(a24),f10(a23))))),f8(f1(f6(a7,a13))),a21)), % 62.16/62.30 inference(scs_inference,[],[36,66,74,2,24])). % 62.16/62.30 cnf(98,plain, % 62.16/62.30 (E(f4(x981,f5(x982,x983,f8(f1(x984)))),f4(x981,f5(x982,x983,f8(x984))))), % 62.16/62.30 inference(scs_inference,[],[26,16,13])). % 62.16/62.30 cnf(99,plain, % 62.16/62.30 (E(f4(x991,f5(x992,x993,f8(x994))),f4(x991,f5(x992,x993,f8(f1(x994)))))), % 62.16/62.30 inference(scs_inference,[],[98,2])). % 62.16/62.30 cnf(100,plain, % 62.16/62.30 (E(f6(f6(x1001,f8(f1(x1002))),x1003),f6(f6(x1001,f8(x1002)),x1003))), % 62.16/62.30 inference(scs_inference,[],[26,17,18])). % 62.16/62.30 cnf(101,plain, % 62.16/62.30 (E(f6(f6(x1011,f8(x1012)),x1013),f6(f6(x1011,f8(f1(x1012))),x1013))), % 62.16/62.30 inference(scs_inference,[],[100,2])). % 62.16/62.30 cnf(102,plain, % 62.16/62.30 (E(f12(f12(x1021,f8(f1(x1022))),x1023),f12(f12(x1021,f8(x1022)),x1023))), % 62.16/62.30 inference(scs_inference,[],[26,19,20])). % 62.16/62.30 cnf(103,plain, % 62.16/62.30 (E(f12(f12(x1031,f8(x1032)),x1033),f12(f12(x1031,f8(f1(x1032))),x1033))), % 62.16/62.30 inference(scs_inference,[],[102,2])). % 62.16/62.30 cnf(104,plain, % 62.16/62.30 (E(f3(f3(x1041,f8(f1(x1042))),x1043),f3(f3(x1041,f8(x1042)),x1043))), % 62.16/62.30 inference(scs_inference,[],[26,21,22])). % 62.16/62.30 cnf(105,plain, % 62.16/62.30 (E(f3(f3(x1051,f8(x1052)),x1053),f3(f3(x1051,f8(f1(x1052))),x1053))), % 62.16/62.30 inference(scs_inference,[],[104,2])). % 62.16/62.30 cnf(125,plain, % 62.16/62.30 (P1(f11(f9(a22),f12(f15(a22),f11(f9(a20),f11(f10(a24),f10(a23))))),f8(f1(f1(f6(a7,a13)))),a21)), % 62.16/62.30 inference(scs_inference,[],[36,76,24])). % 62.16/62.30 cnf(174,plain, % 62.16/62.30 (E(f11(f6(f6(x1741,f8(x1742)),x1743),x1744),f11(f6(f6(x1741,f8(f1(x1742))),x1743),x1744))), % 62.16/62.30 inference(scs_inference,[],[100,2,6])). % 62.16/62.30 cnf(175,plain, % 62.16/62.30 (E(f11(f6(f6(x1751,f8(f1(x1752))),x1753),x1754),f11(f6(f6(x1751,f8(x1752)),x1753),x1754))), % 62.16/62.30 inference(scs_inference,[],[174,2])). % 62.16/62.30 cnf(186,plain, % 62.16/62.30 (E(f5(x1861,f6(f6(x1862,f8(x1863)),x1864),x1865),f5(x1861,f6(f6(x1862,f8(f1(x1863))),x1864),x1865))), % 62.16/62.30 inference(scs_inference,[],[100,2,12])). % 62.16/62.30 cnf(187,plain, % 62.16/62.30 (E(f5(x1871,f6(f6(x1872,f8(f1(x1873))),x1874),x1875),f5(x1871,f6(f6(x1872,f8(x1873)),x1874),x1875))), % 62.16/62.30 inference(scs_inference,[],[186,2])). % 62.16/62.30 cnf(196,plain, % 62.16/62.30 (E(f6(f6(f6(x1961,f8(x1962)),x1963),x1964),f6(f6(f6(x1961,f8(f1(x1962))),x1963),x1964))), % 62.16/62.30 inference(scs_inference,[],[100,2,17])). % 62.16/62.30 cnf(197,plain, % 62.16/62.30 (E(f6(f6(f6(x1971,f8(f1(x1972))),x1973),x1974),f6(f6(f6(x1971,f8(x1972)),x1973),x1974))), % 62.16/62.30 inference(scs_inference,[],[196,2])). % 62.16/62.30 cnf(198,plain, % 62.16/62.30 (E(f6(f6(f6(x1981,f8(x1982)),f8(f1(x1983))),x1984),f6(f6(f6(x1981,f8(f1(x1982))),f8(x1983)),x1984))), % 62.16/62.30 inference(scs_inference,[],[100,196,2,3])). % 62.16/62.30 cnf(203,plain, % 62.16/62.30 (E(f6(f6(f6(x2031,f8(f1(x2032))),f8(f1(x2033))),x2034),f6(f6(f6(x2031,f8(x2032)),f8(x2033)),x2034))), % 62.16/62.30 inference(scs_inference,[],[100,198,197,2,3])). % 62.16/62.30 cnf(206,plain, % 62.16/62.30 (E(f12(f6(f6(x2061,f8(x2062)),x2063),x2064),f12(f6(f6(x2061,f8(f1(x2062))),x2063),x2064))), % 62.16/62.30 inference(scs_inference,[],[100,2,19])). % 62.16/62.30 cnf(208,plain, % 62.16/62.30 (E(x2081,f12(f6(f6(x2082,f8(f1(x2083))),x2084),x2085))+~E(x2081,f12(f6(f6(x2082,f8(x2083)),x2084),x2085))), % 62.16/62.30 inference(scs_inference,[],[203,206,2,3])). % 62.16/62.30 cnf(242,plain, % 62.16/62.30 (E(f6(f12(f12(x2421,f8(f1(x2422))),x2423),x2424),f6(f12(f12(x2421,f8(x2422)),x2423),x2424))), % 62.16/62.30 inference(scs_inference,[],[103,2,17])). % 62.16/62.30 cnf(243,plain, % 62.16/62.30 (E(f6(f12(f12(x2431,f8(x2432)),x2433),x2434),f6(f12(f12(x2431,f8(f1(x2432))),x2433),x2434))), % 62.16/62.30 inference(scs_inference,[],[242,2])). % 62.16/62.30 cnf(421,plain, % 62.16/62.30 (E(f8(f8(x4211)),f8(f8(f1(x4211))))), % 62.16/62.30 inference(scs_inference,[],[26,2,5])). % 62.16/62.30 cnf(422,plain, % 62.16/62.30 (E(f8(f8(f1(x4221))),f8(f8(x4221)))), % 62.16/62.30 inference(scs_inference,[],[421,2])). % 62.16/62.30 cnf(423,plain, % 62.16/62.30 (E(f8(f1(f8(x4231))),f8(f8(f1(x4231))))), % 62.16/62.30 inference(scs_inference,[],[26,421,2,3])). % 62.16/62.30 cnf(425,plain, % 62.16/62.30 (E(f11(f8(x4251),x4252),f11(f8(f1(x4251)),x4252))), % 62.16/62.30 inference(scs_inference,[],[26,2,6])). % 62.16/62.30 cnf(426,plain, % 62.16/62.30 (E(f8(f8(f1(x4261))),f8(f1(f8(x4261))))), % 62.16/62.30 inference(scs_inference,[],[423,2])). % 62.16/62.30 cnf(427,plain, % 62.16/62.30 (E(f8(f1(f8(f1(x4271)))),f8(f8(x4271)))), % 62.16/62.30 inference(scs_inference,[],[26,422,423,2,3])). % 62.16/62.30 cnf(429,plain, % 62.16/62.30 (E(f11(x4291,f8(x4292)),f11(x4291,f8(f1(x4292))))), % 62.16/62.30 inference(scs_inference,[],[26,2,7])). % 62.16/62.30 cnf(430,plain, % 62.16/62.30 (E(f8(f8(x4301)),f8(f1(f8(f1(x4301)))))), % 62.16/62.30 inference(scs_inference,[],[427,2])). % 62.16/62.30 cnf(431,plain, % 62.16/62.30 (E(f8(f1(f1(f8(f1(x4311))))),f8(f8(x4311)))), % 62.16/62.30 inference(scs_inference,[],[26,427,2,3])). % 62.16/62.30 cnf(433,plain, % 62.16/62.30 (E(f17(f8(x4331)),f17(f8(f1(x4331))))), % 62.16/62.30 inference(scs_inference,[],[26,2,8])). % 62.16/62.30 cnf(435,plain, % 62.16/62.30 (E(f8(f1(f1(f1(f8(f1(x4351)))))),f8(f8(x4351)))), % 62.16/62.30 inference(scs_inference,[],[26,431,2,3])). % 62.16/62.30 cnf(437,plain, % 62.16/62.30 (E(f9(f8(x4371)),f9(f8(f1(x4371))))), % 62.16/62.30 inference(scs_inference,[],[26,2,9])). % 62.16/62.30 cnf(439,plain, % 62.16/62.30 (E(f11(f8(x4391),f8(x4392)),f11(f8(f1(x4391)),f8(f1(x4392))))), % 62.16/62.30 inference(scs_inference,[],[435,425,429,2,3])). % 62.16/62.30 cnf(442,plain, % 62.16/62.30 (E(f15(f8(x4421)),f15(f8(f1(x4421))))), % 62.16/62.30 inference(scs_inference,[],[26,2,10])). % 62.16/62.30 cnf(444,plain, % 62.16/62.30 (E(f8(f1(f8(f1(x4441)))),f8(f1(f8(x4441))))), % 62.16/62.30 inference(scs_inference,[],[26,426,433,2,3])). % 62.16/62.30 cnf(446,plain, % 62.16/62.30 (E(f5(f8(x4461),x4462,x4463),f5(f8(f1(x4461)),x4462,x4463))), % 62.16/62.30 inference(scs_inference,[],[26,2,11])). % 62.16/62.30 cnf(447,plain, % 62.16/62.30 (E(f9(f8(f1(x4471))),f9(f8(x4471)))), % 62.16/62.30 inference(scs_inference,[],[437,2])). % 62.16/62.30 cnf(448,plain, % 62.16/62.30 (E(f11(f8(x4481),f8(x4482)),f11(f8(f1(f1(x4481))),f8(f1(x4482))))), % 62.16/62.30 inference(scs_inference,[],[437,439,425,2,3])). % 62.16/62.30 cnf(451,plain, % 62.16/62.30 (E(f5(x4511,f8(x4512),x4513),f5(x4511,f8(f1(x4512)),x4513))), % 62.16/62.30 inference(scs_inference,[],[26,2,12])). % 62.16/62.30 cnf(452,plain, % 62.16/62.30 (E(f15(f8(f1(x4521))),f15(f8(x4521)))), % 62.16/62.30 inference(scs_inference,[],[442,2])). % 62.16/62.30 cnf(453,plain, % 62.16/62.30 (E(f8(f1(f1(f8(f1(x4531))))),f8(f1(f8(x4531))))), % 62.16/62.30 inference(scs_inference,[],[26,442,444,2,3])). % 62.16/62.30 cnf(455,plain, % 62.16/62.30 (E(f5(x4551,x4552,f8(x4553)),f5(x4551,x4552,f8(f1(x4553))))), % 62.16/62.30 inference(scs_inference,[],[26,2,13])). % 62.16/62.30 cnf(456,plain, % 62.16/62.30 (E(f5(f8(f1(x4561)),x4562,x4563),f5(f8(x4561),x4562,x4563))), % 62.16/62.30 inference(scs_inference,[],[446,2])). % 62.16/62.30 cnf(457,plain, % 62.16/62.30 (E(f5(f8(x4571),f8(x4572),x4573),f5(f8(f1(x4571)),f8(f1(x4572)),x4573))), % 62.16/62.30 inference(scs_inference,[],[446,451,2,3])). % 62.16/62.30 cnf(460,plain, % 62.16/62.30 (E(f10(f8(x4601)),f10(f8(f1(x4601))))), % 62.16/62.30 inference(scs_inference,[],[26,2,14])). % 62.16/62.30 cnf(461,plain, % 62.16/62.30 (E(f11(f8(f1(f1(x4611))),f8(f1(x4612))),f11(f8(x4611),f8(x4612)))), % 62.16/62.30 inference(scs_inference,[],[448,2])). % 62.16/62.30 cnf(462,plain, % 62.16/62.30 (E(f5(f8(f1(x4621)),x4622,f8(x4623)),f5(f8(x4621),x4622,f8(f1(x4623))))), % 62.16/62.30 inference(scs_inference,[],[456,448,455,2,3])). % 62.16/62.30 cnf(465,plain, % 62.16/62.30 (E(f4(f8(x4651),x4652),f4(f8(f1(x4651)),x4652))), % 62.16/62.30 inference(scs_inference,[],[26,2,15])). % 62.16/62.30 cnf(466,plain, % 62.16/62.30 (E(f8(f1(f8(x4661))),f8(f1(f1(f8(f1(x4661))))))), % 62.16/62.30 inference(scs_inference,[],[453,2])). % 62.16/62.30 cnf(467,plain, % 62.16/62.30 (E(f11(f8(f1(f1(x4671))),f8(x4672)),f11(f8(x4671),f8(x4672)))), % 62.16/62.30 inference(scs_inference,[],[461,453,429,2,3])). % 62.16/62.30 cnf(470,plain, % 62.16/62.30 (E(f4(x4701,f8(x4702)),f4(x4701,f8(f1(x4702))))), % 62.16/62.30 inference(scs_inference,[],[26,2,16])). % 62.16/62.30 cnf(471,plain, % 62.16/62.30 (E(f11(f8(x4711),f8(x4712)),f11(f8(f1(f1(x4711))),f8(x4712)))), % 62.16/62.30 inference(scs_inference,[],[467,2])). % 62.16/62.30 cnf(472,plain, % 62.16/62.30 (E(f11(f8(f1(f1(f1(f1(x4721))))),f8(f1(x4722))),f11(f8(x4721),f8(x4722)))), % 62.16/62.30 inference(scs_inference,[],[467,461,2,3])). % 62.16/62.30 cnf(475,plain, % 62.16/62.30 (E(f6(f8(x4751),x4752),f6(f8(f1(x4751)),x4752))), % 62.16/62.30 inference(scs_inference,[],[26,2,17])). % 62.16/62.30 cnf(476,plain, % 62.16/62.30 (E(f11(f8(x4761),f8(x4762)),f11(f8(f1(f1(f1(f1(x4761))))),f8(f1(x4762))))), % 62.16/62.30 inference(scs_inference,[],[472,2])). % 62.16/62.30 cnf(477,plain, % 62.16/62.30 (E(f5(f8(f1(x4771)),f8(x4772),f8(x4773)),f5(f8(f1(x4771)),f8(f1(x4772)),f8(f1(x4773))))), % 62.16/62.30 inference(scs_inference,[],[472,457,462,2,3])). % 62.16/62.30 cnf(480,plain, % 62.16/62.30 (E(f6(x4801,f8(x4802)),f6(x4801,f8(f1(x4802))))), % 62.16/62.30 inference(scs_inference,[],[26,2,18])). % 62.16/62.30 cnf(481,plain, % 62.16/62.30 (E(f10(f8(f1(x4811))),f10(f8(x4811)))), % 62.16/62.30 inference(scs_inference,[],[460,2])). % 62.16/62.30 cnf(482,plain, % 62.16/62.30 (E(f4(f8(x4821),f5(x4822,x4823,f8(x4824))),f4(f8(f1(x4821)),f5(x4822,x4823,f8(f1(x4824)))))), % 62.16/62.30 inference(scs_inference,[],[99,460,465,2,3])). % 62.16/62.30 cnf(485,plain, % 62.16/62.30 (E(f12(f8(x4851),x4852),f12(f8(f1(x4851)),x4852))), % 62.16/62.30 inference(scs_inference,[],[26,2,19])). % 62.16/62.30 cnf(486,plain, % 62.16/62.30 (E(f4(x4861,f8(f1(x4862))),f4(x4861,f8(x4862)))), % 62.16/62.30 inference(scs_inference,[],[470,2])). % 62.16/62.30 cnf(487,plain, % 62.16/62.30 (E(f6(f8(x4871),f8(x4872)),f6(f8(f1(x4871)),f8(f1(x4872))))), % 62.16/62.30 inference(scs_inference,[],[470,475,480,2,3])). % 62.16/62.30 cnf(490,plain, % 62.16/62.30 (E(f12(x4901,f8(x4902)),f12(x4901,f8(f1(x4902))))), % 62.16/62.30 inference(scs_inference,[],[26,2,20])). % 62.16/62.30 cnf(491,plain, % 62.16/62.30 (E(f5(f8(f1(x4911)),f8(f1(x4912)),f8(f1(x4913))),f5(f8(f1(x4911)),f8(x4912),f8(x4913)))), % 62.16/62.30 inference(scs_inference,[],[477,2])). % 62.16/62.30 cnf(492,plain, % 62.16/62.30 (E(f12(f6(f6(x4921,f8(x4922)),x4923),f8(x4924)),f12(f6(f6(x4921,f8(f1(x4922))),x4923),f8(f1(x4924))))), % 62.16/62.30 inference(scs_inference,[],[206,477,490,2,3])). % 62.16/62.30 cnf(495,plain, % 62.16/62.30 (E(f3(f8(x4951),x4952),f3(f8(f1(x4951)),x4952))), % 62.16/62.30 inference(scs_inference,[],[26,2,21])). % 62.16/62.30 cnf(496,plain, % 62.16/62.30 (E(f12(f8(f1(x4961)),x4962),f12(f8(x4961),x4962))), % 62.16/62.30 inference(scs_inference,[],[485,2])). % 62.16/62.30 cnf(497,plain, % 62.16/62.30 (E(f4(f8(x4971),f8(f1(x4972))),f4(f8(f1(x4971)),f8(x4972)))), % 62.16/62.30 inference(scs_inference,[],[486,485,465,2,3])). % 62.16/62.30 cnf(500,plain, % 62.16/62.30 (E(f3(x5001,f8(x5002)),f3(x5001,f8(f1(x5002))))), % 62.16/62.30 inference(scs_inference,[],[26,2,22])). % 62.16/62.30 cnf(501,plain, % 62.16/62.30 (E(f4(f8(f1(x5011)),f8(x5012)),f4(f8(x5011),f8(f1(x5012))))), % 62.16/62.30 inference(scs_inference,[],[497,2])). % 62.16/62.30 cnf(502,plain, % 62.16/62.30 (E(f5(f8(f1(f1(x5021))),f8(f1(x5022)),f8(f1(x5023))),f5(f8(f1(x5021)),f8(x5022),f8(x5023)))), % 62.16/62.30 inference(scs_inference,[],[491,497,456,2,3])). % 62.16/62.30 cnf(505,plain, % 62.16/62.30 (E(f5(f8(f1(x5051)),f8(x5052),f8(x5053)),f5(f8(f1(f1(x5051))),f8(f1(x5052)),f8(f1(x5053))))), % 62.16/62.30 inference(scs_inference,[],[502,2])). % 62.16/62.30 cnf(506,plain, % 62.16/62.30 (E(f5(f8(f1(f1(x5061))),f8(f1(f1(x5062))),f8(f1(f1(x5063)))),f5(f8(f1(x5061)),f8(x5062),f8(x5063)))), % 62.16/62.30 inference(scs_inference,[],[502,491,2,3])). % 62.16/62.30 cnf(509,plain, % 62.16/62.30 (E(f5(f8(f1(x5091)),f8(x5092),f8(x5093)),f5(f8(f1(f1(x5091))),f8(f1(f1(x5092))),f8(f1(f1(x5093)))))), % 62.16/62.30 inference(scs_inference,[],[506,2])). % 62.16/62.30 cnf(510,plain, % 62.16/62.30 (E(f6(f8(x5101),f8(x5102)),f6(f8(f1(f1(x5101))),f8(f1(x5102))))), % 62.16/62.30 inference(scs_inference,[],[506,487,475,2,3])). % 62.16/62.30 cnf(514,plain, % 62.16/62.30 (E(f12(f6(f6(x5141,f8(f1(x5142))),x5143),f8(f1(x5144))),f12(f6(f6(x5141,f8(x5142)),x5143),f8(x5144)))), % 62.16/62.30 inference(scs_inference,[],[492,2])). % 62.16/62.30 cnf(515,plain, % 62.16/62.30 (E(f3(f3(x5151,f8(f1(x5152))),f8(x5153)),f3(f3(x5151,f8(x5152)),f8(f1(x5153))))), % 62.16/62.30 inference(scs_inference,[],[104,492,500,2,3])). % 62.16/62.30 cnf(520,plain, % 62.16/62.30 (E(f12(f6(f6(x5201,f8(f1(x5202))),x5203),f8(f1(x5204))),f12(f6(f6(x5201,f8(f1(x5202))),x5203),f8(x5204)))), % 62.16/62.30 inference(scs_inference,[],[206,514,495,2,3])). % 62.16/62.30 cnf(523,plain, % 62.16/62.30 (E(f6(f8(f1(f1(x5231))),f8(f1(x5232))),f6(f8(x5231),f8(x5232)))), % 62.16/62.30 inference(scs_inference,[],[510,2])). % 62.16/62.30 cnf(524,plain, % 62.16/62.30 (E(f12(f6(f6(x5241,f8(x5242)),x5243),f8(f1(x5244))),f12(f6(f6(x5241,f8(f1(x5242))),x5243),f8(x5244)))), % 62.16/62.30 inference(scs_inference,[],[206,520,510,2,3])). % 62.16/62.30 cnf(529,plain, % 62.16/62.30 (E(f6(f8(f1(f1(x5291))),f8(x5292)),f6(f8(x5291),f8(x5292)))), % 62.16/62.30 inference(scs_inference,[],[523,524,480,2,3])). % 62.16/62.30 cnf(533,plain, % 62.16/62.30 (E(f6(f8(x5331),f8(x5332)),f6(f8(f1(f1(x5331))),f8(x5332)))), % 62.16/62.30 inference(scs_inference,[],[529,2])). % 62.16/62.30 cnf(534,plain, % 62.16/62.30 (E(f6(f8(f1(f1(f1(f1(x5341))))),f8(f1(x5342))),f6(f8(x5341),f8(x5342)))), % 62.16/62.30 inference(scs_inference,[],[529,523,2,3])). % 62.16/62.30 cnf(537,plain, % 62.16/62.30 (E(f6(f8(x5371),f8(x5372)),f6(f8(f1(f1(f1(f1(x5371))))),f8(f1(x5372))))), % 62.16/62.30 inference(scs_inference,[],[534,2])). % 62.16/62.30 cnf(538,plain, % 62.16/62.30 (E(f8(f1(f8(x5381))),f8(f1(f8(f1(x5381)))))), % 62.16/62.30 inference(scs_inference,[],[26,534,430,2,3])). % 62.16/62.30 cnf(541,plain, % 62.16/62.30 (E(f3(f3(x5411,f8(x5412)),f8(f1(x5413))),f3(f3(x5411,f8(f1(x5412))),f8(x5413)))), % 62.16/62.30 inference(scs_inference,[],[515,2])). % 62.16/62.30 cnf(542,plain, % 62.16/62.30 (E(f8(f1(f1(f8(x5421)))),f8(f1(f8(f1(x5421)))))), % 62.16/62.30 inference(scs_inference,[],[26,515,538,2,3])). % 62.16/62.30 cnf(545,plain, % 62.16/62.30 (E(f4(f8(f1(x5451)),f5(x5452,x5453,f8(f1(x5454)))),f4(f8(x5451),f5(x5452,x5453,f8(x5454))))), % 62.16/62.30 inference(scs_inference,[],[482,2])). % 62.16/62.30 cnf(546,plain, % 62.16/62.30 (E(f3(f3(x5461,f8(x5462)),f8(f1(x5463))),f3(f3(x5461,f8(f1(f1(x5462)))),f8(x5463)))), % 62.16/62.30 inference(scs_inference,[],[105,541,482,2,3])). % 62.16/62.30 cnf(550,plain, % 62.16/62.30 (E(f3(f3(x5501,f8(f1(f1(x5502)))),f8(x5503)),f3(f3(x5501,f8(x5502)),f8(f1(x5503))))), % 62.16/62.30 inference(scs_inference,[],[546,2])). % 62.16/62.30 cnf(551,plain, % 62.16/62.30 (E(f4(f8(f1(x5511)),f5(x5512,x5513,f8(f1(f1(x5514))))),f4(f8(x5511),f5(x5512,x5513,f8(x5514))))), % 62.16/62.30 inference(scs_inference,[],[98,546,545,2,3])). % 62.16/62.30 cnf(556,plain, % 62.16/62.30 (E(f3(f3(x5561,f8(f1(f1(f1(x5562))))),f8(x5563)),f3(f3(x5561,f8(x5562)),f8(f1(x5563))))), % 62.16/62.30 inference(scs_inference,[],[104,550,551,2,3])). % 62.16/62.30 cnf(561,plain, % 62.16/62.30 (E(f8(f1(f1(f1(f8(x5611))))),f8(f1(f8(f1(x5611)))))), % 62.16/62.30 inference(scs_inference,[],[26,556,542,2,3])). % 62.16/62.30 cnf(565,plain, % 62.16/62.30 (E(f8(f1(f1(f8(x5651)))),f8(f1(f1(f8(f1(x5651))))))), % 62.16/62.30 inference(scs_inference,[],[26,561,466,2,3])). % 62.16/62.30 cnf(569,plain, % 62.16/62.30 (E(f4(f8(f1(x5691)),f8(x5692)),f4(f8(x5691),f8(x5692)))), % 62.16/62.30 inference(scs_inference,[],[501,565,486,2,3])). % 62.16/62.30 cnf(571,plain, % 62.16/62.30 (E(f11(f8(f1(x5711)),f8(f1(x5712))),f11(f8(x5711),f8(x5712)))), % 62.16/62.30 inference(scs_inference,[],[439,2])). % 62.16/62.30 cnf(576,plain, % 62.16/62.30 (E(f5(x5761,f8(f1(x5762)),x5763),f5(x5761,f8(x5762),x5763))), % 62.16/62.30 inference(scs_inference,[],[451,2])). % 62.16/62.31 cnf(577,plain, % 62.16/62.31 (E(f11(f8(f1(x5771)),f8(f1(x5772))),f11(f8(f1(f1(x5771))),f8(x5772)))), % 62.16/62.31 inference(scs_inference,[],[471,571,451,2,3])). % 62.16/62.31 cnf(580,plain, % 62.16/62.31 (E(f11(f8(f1(f1(x5801))),f8(x5802)),f11(f8(f1(x5801)),f8(f1(x5802))))), % 62.16/62.31 inference(scs_inference,[],[577,2])). % 62.16/62.31 cnf(581,plain, % 62.16/62.31 (E(f5(f8(f1(x5811)),f8(x5812),f8(x5813)),f5(f8(f1(f1(x5811))),f8(x5812),f8(f1(x5813))))), % 62.16/62.31 inference(scs_inference,[],[576,577,505,2,3])). % 62.16/62.31 cnf(584,plain, % 62.16/62.31 (E(f5(f8(f1(f1(x5841))),f8(x5842),f8(f1(x5843))),f5(f8(f1(x5841)),f8(x5842),f8(x5843)))), % 62.16/62.31 inference(scs_inference,[],[581,2])). % 62.16/62.31 cnf(585,plain, % 62.16/62.31 (E(f11(f8(x5851),f8(x5852)),f11(f8(f1(f1(f1(x5851)))),f8(f1(f1(x5852)))))), % 62.16/62.31 inference(scs_inference,[],[476,580,581,2,3])). % 62.16/62.31 cnf(588,plain, % 62.16/62.31 (E(f11(f8(f1(f1(f1(x5881)))),f8(f1(f1(x5882)))),f11(f8(x5881),f8(x5882)))), % 62.16/62.31 inference(scs_inference,[],[585,2])). % 62.16/62.31 cnf(589,plain, % 62.16/62.31 (E(f5(f8(f1(x5891)),f8(x5892),f8(x5893)),f5(f8(f1(x5891)),f8(f1(f1(x5892))),f8(f1(x5893))))), % 62.16/62.31 inference(scs_inference,[],[584,509,585,2,3])). % 62.16/62.31 cnf(592,plain, % 62.16/62.31 (E(f5(f8(f1(x5921)),f8(f1(f1(x5922))),f8(f1(x5923))),f5(f8(f1(x5921)),f8(x5922),f8(x5923)))), % 62.16/62.31 inference(scs_inference,[],[589,2])). % 62.16/62.31 cnf(593,plain, % 62.16/62.31 (E(f11(f8(f1(x5931)),f8(f1(f1(x5932)))),f11(f8(x5931),f8(x5932)))), % 62.16/62.31 inference(scs_inference,[],[588,589,471,2,3])). % 62.16/62.31 cnf(596,plain, % 62.16/62.31 (E(f11(f8(x5961),f8(x5962)),f11(f8(f1(x5961)),f8(f1(f1(x5962)))))), % 62.16/62.31 inference(scs_inference,[],[593,2])). % 62.16/62.31 cnf(597,plain, % 62.16/62.31 (E(f11(f8(f1(f1(x5971))),f8(f1(f1(f1(x5972))))),f11(f8(x5971),f8(x5972)))), % 62.16/62.31 inference(scs_inference,[],[593,571,2,3])). % 62.16/62.31 cnf(600,plain, % 62.16/62.31 (E(f11(f8(x6001),f8(x6002)),f11(f8(f1(f1(x6001))),f8(f1(f1(f1(x6002))))))), % 62.16/62.31 inference(scs_inference,[],[597,2])). % 62.16/62.31 cnf(601,plain, % 62.16/62.31 (E(f5(f8(f1(x6011)),f8(f1(f1(f1(x6012)))),f8(f1(x6013))),f5(f8(f1(x6011)),f8(x6012),f8(x6013)))), % 62.16/62.31 inference(scs_inference,[],[592,597,576,2,3])). % 62.16/62.31 cnf(605,plain, % 62.16/62.31 (E(f5(f8(f1(x6051)),f8(x6052),f8(x6053)),f5(f8(f1(x6051)),f8(f1(f1(f1(x6052)))),f8(f1(x6053))))), % 62.16/62.31 inference(scs_inference,[],[601,2])). % 62.16/62.31 cnf(606,plain, % 62.16/62.31 (E(f11(f8(f1(f1(f1(x6061)))),f8(x6062)),f11(f8(x6061),f8(f1(x6062))))), % 62.16/62.31 inference(scs_inference,[],[601,596,472,2,3])). % 62.16/62.31 cnf(610,plain, % 62.16/62.31 (E(f11(f8(x6101),f8(f1(x6102))),f11(f8(f1(f1(f1(x6101)))),f8(x6102)))), % 62.16/62.31 inference(scs_inference,[],[606,2])). % 62.16/62.31 cnf(611,plain, % 62.16/62.31 (E(f5(f8(f1(f1(x6111))),f8(x6112),f8(f1(x6113))),f5(f8(f1(x6111)),f8(f1(x6112)),f8(x6113)))), % 62.16/62.31 inference(scs_inference,[],[605,606,506,2,3])). % 62.16/62.31 cnf(615,plain, % 62.16/62.31 (E(f5(f8(f1(x6151)),f8(f1(x6152)),f8(x6153)),f5(f8(f1(f1(x6151))),f8(x6152),f8(f1(x6153))))), % 62.16/62.31 inference(scs_inference,[],[611,2])). % 62.16/62.31 cnf(616,plain, % 62.16/62.31 (E(f5(f8(f1(f1(f1(x6161)))),f8(x6162),f8(f1(f1(x6163)))),f5(f8(f1(x6161)),f8(f1(x6162)),f8(x6163)))), % 62.16/62.31 inference(scs_inference,[],[611,584,2,3])). % 62.16/62.31 cnf(620,plain, % 62.16/62.31 (E(f5(f8(f1(x6201)),f8(f1(x6202)),f8(x6203)),f5(f8(f1(f1(f1(x6201)))),f8(x6202),f8(f1(f1(x6203)))))), % 62.16/62.31 inference(scs_inference,[],[616,2])). % 62.16/62.31 cnf(621,plain, % 62.16/62.31 (E(f11(f8(x6211),f8(f1(f1(f1(x6212))))),f11(f8(x6211),f8(x6212)))), % 62.16/62.31 inference(scs_inference,[],[610,616,588,2,3])). % 62.16/62.31 cnf(625,plain, % 62.16/62.31 (E(f11(f8(x6251),f8(x6252)),f11(f8(x6251),f8(f1(f1(f1(x6252))))))), % 62.16/62.31 inference(scs_inference,[],[621,2])). % 62.16/62.31 cnf(626,plain, % 62.16/62.31 (E(f5(f8(f1(x6261)),f8(f1(f1(f1(x6262)))),f8(x6263)),f5(f8(f1(f1(x6261))),f8(x6262),f8(x6263)))), % 62.16/62.31 inference(scs_inference,[],[621,615,592,2,3])). % 62.16/62.31 cnf(630,plain, % 62.16/62.31 (E(f5(f8(f1(f1(x6301))),f8(x6302),f8(x6303)),f5(f8(f1(x6301)),f8(f1(f1(f1(x6302)))),f8(x6303)))), % 62.16/62.31 inference(scs_inference,[],[626,2])). % 62.16/62.31 cnf(642,plain, % 62.16/62.31 (E(f5(x6421,x6422,f8(f1(x6423))),f5(x6421,x6422,f8(x6423)))), % 62.16/62.31 inference(scs_inference,[],[455,2])). % 62.16/62.31 cnf(643,plain, % 62.16/62.31 (E(f5(f8(f1(f1(x6431))),f8(x6432),f8(x6433)),f5(f8(f1(x6431)),f8(f1(f1(f1(x6432)))),f8(f1(x6433))))), % 62.16/62.31 inference(scs_inference,[],[630,455,2,3])). % 62.16/62.31 cnf(646,plain, % 62.16/62.31 (E(f5(f8(f1(x6461)),f8(f1(f1(f1(x6462)))),f8(f1(x6463))),f5(f8(f1(f1(x6461))),f8(x6462),f8(x6463)))), % 62.16/62.31 inference(scs_inference,[],[643,2])). % 62.16/62.31 cnf(647,plain, % 62.16/62.31 (E(f5(f8(f1(x6471)),f8(f1(f1(f1(x6472)))),f8(f1(f1(x6473)))),f5(f8(f1(x6471)),f8(x6472),f8(x6473)))), % 62.16/62.31 inference(scs_inference,[],[642,643,601,2,3])). % 62.16/62.31 cnf(650,plain, % 62.16/62.31 (E(f5(f8(f1(x6501)),f8(x6502),f8(x6503)),f5(f8(f1(x6501)),f8(f1(f1(f1(x6502)))),f8(f1(f1(x6503)))))), % 62.16/62.31 inference(scs_inference,[],[647,2])). % 62.16/62.31 cnf(651,plain, % 62.16/62.31 (E(f5(f8(f1(x6511)),f8(f1(f1(f1(x6512)))),f8(f1(x6513))),f5(f8(f1(x6511)),f8(x6512),f8(f1(x6513))))), % 62.16/62.31 inference(scs_inference,[],[646,647,462,2,3])). % 62.16/62.31 cnf(654,plain, % 62.16/62.31 (E(f5(f8(f1(x6541)),f8(x6542),f8(f1(x6543))),f5(f8(f1(x6541)),f8(f1(f1(f1(x6542)))),f8(f1(x6543))))), % 62.16/62.31 inference(scs_inference,[],[651,2])). % 62.16/62.31 cnf(655,plain, % 62.16/62.31 (E(f6(f8(x6551),f8(x6552)),f6(f8(f1(f1(f1(x6551)))),f8(f1(x6552))))), % 62.16/62.31 inference(scs_inference,[],[533,651,487,2,3])). % 62.16/62.31 cnf(657,plain, % 62.16/62.31 (E(f6(f8(f1(f1(f1(x6571)))),f8(f1(x6572))),f6(f8(x6571),f8(x6572)))), % 62.16/62.31 inference(scs_inference,[],[655,2])). % 62.16/62.31 cnf(658,plain, % 62.16/62.31 (E(f5(f8(f1(x6581)),f8(x6582),f8(f1(x6583))),f5(f8(f1(x6581)),f8(f1(f1(f1(x6582)))),f8(x6583)))), % 62.16/62.31 inference(scs_inference,[],[654,655,642,2,3])). % 62.16/62.31 cnf(661,plain, % 62.16/62.31 (E(f5(f8(f1(x6611)),f8(f1(f1(f1(x6612)))),f8(x6613)),f5(f8(f1(x6611)),f8(x6612),f8(f1(x6613))))), % 62.16/62.31 inference(scs_inference,[],[658,2])). % 62.16/62.31 cnf(662,plain, % 62.16/62.31 (E(f6(f8(f1(f1(f1(x6621)))),f8(f1(x6622))),f6(f8(f1(f1(x6621))),f8(x6622)))), % 62.16/62.31 inference(scs_inference,[],[657,658,533,2,3])). % 62.16/62.31 cnf(665,plain, % 62.16/62.31 (E(f5(f8(f1(x6651)),f8(f1(x6652)),x6653),f5(f8(x6651),f8(x6652),x6653))), % 62.16/62.31 inference(scs_inference,[],[457,2])). % 62.16/62.31 cnf(666,plain, % 62.16/62.31 (E(f6(f8(x6661),f8(x6662)),f6(f8(f1(f1(f1(x6661)))),f8(x6662)))), % 62.16/62.31 inference(scs_inference,[],[662,537,457,2,3])). % 62.16/62.31 cnf(669,plain, % 62.16/62.31 (E(f6(f8(f1(f1(f1(x6691)))),f8(x6692)),f6(f8(x6691),f8(x6692)))), % 62.16/62.31 inference(scs_inference,[],[666,2])). % 62.16/62.31 cnf(670,plain, % 62.16/62.31 (E(f5(f8(f1(x6701)),f8(f1(f1(f1(f1(x6702))))),f8(x6703)),f5(f8(x6701),f8(x6702),f8(f1(x6703))))), % 62.16/62.31 inference(scs_inference,[],[665,666,661,2,3])). % 62.16/62.31 cnf(674,plain, % 62.16/62.31 (E(f5(f8(x6741),f8(x6742),f8(f1(x6743))),f5(f8(f1(x6741)),f8(f1(f1(f1(f1(x6742))))),f8(x6743)))), % 62.16/62.31 inference(scs_inference,[],[670,2])). % 62.16/62.31 cnf(675,plain, % 62.16/62.31 (E(f12(f12(x6751,f8(f1(x6752))),f8(x6753)),f12(f12(x6751,f8(x6752)),f8(f1(x6753))))), % 62.16/62.31 inference(scs_inference,[],[102,670,490,2,3])). % 62.16/62.31 cnf(679,plain, % 62.16/62.31 (E(f12(f12(x6791,f8(x6792)),f8(f1(x6793))),f12(f12(x6791,f8(f1(x6792))),f8(x6793)))), % 62.16/62.31 inference(scs_inference,[],[675,2])). % 62.16/62.31 cnf(680,plain, % 62.16/62.31 (E(f12(f12(x6801,f8(f1(f1(x6802)))),f8(x6803)),f12(f12(x6801,f8(x6802)),f8(f1(x6803))))), % 62.16/62.31 inference(scs_inference,[],[102,675,2,3])). % 62.16/62.31 cnf(685,plain, % 62.16/62.31 (E(f12(f12(x6851,f8(f1(x6852))),f8(f1(x6853))),f12(f12(x6851,f8(f1(x6852))),f8(x6853)))), % 62.16/62.31 inference(scs_inference,[],[102,679,680,2,3])). % 62.16/62.31 cnf(690,plain, % 62.16/62.31 (E(f12(f12(x6901,f8(f1(f1(x6902)))),f8(f1(x6903))),f12(f12(x6901,f8(f1(x6902))),f8(x6903)))), % 62.16/62.31 inference(scs_inference,[],[102,685,500,2,3])). % 62.16/62.31 cnf(695,plain, % 62.16/62.31 (E(f5(f8(x6951),f8(x6952),f8(f1(x6953))),f5(f8(f1(f1(x6951))),f8(f1(x6952)),f8(x6953)))), % 62.16/62.31 inference(scs_inference,[],[674,690,626,2,3])). % 62.16/62.31 cnf(698,plain, % 62.16/62.31 (E(f5(f8(f1(f1(x6981))),f8(f1(x6982)),f8(x6983)),f5(f8(x6981),f8(x6982),f8(f1(x6983))))), % 62.16/62.31 inference(scs_inference,[],[695,2])). % 62.16/62.31 cnf(699,plain, % 62.16/62.31 (E(f5(f8(f1(x6991)),f8(x6992),f8(f1(f1(f1(x6993))))),f5(f8(f1(x6991)),f8(f1(f1(x6992))),f8(x6993)))), % 62.16/62.31 inference(scs_inference,[],[695,616,2,3])). % 62.16/62.31 cnf(703,plain, % 62.16/62.31 (E(f5(f8(f1(x7031)),f8(f1(f1(x7032))),f8(x7033)),f5(f8(f1(x7031)),f8(x7032),f8(f1(f1(f1(x7033))))))), % 62.16/62.31 inference(scs_inference,[],[699,2])). % 62.16/62.31 cnf(704,plain, % 62.16/62.31 (E(f5(f8(f1(x7041)),f8(x7042),f8(f1(f1(f1(x7043))))),f5(f8(x7041),f8(f1(x7042)),f8(x7043)))), % 62.16/62.31 inference(scs_inference,[],[699,665,2,3])). % 62.16/62.31 cnf(707,plain, % 62.16/62.31 (E(f5(f8(x7071),f8(f1(x7072)),f8(x7073)),f5(f8(f1(x7071)),f8(x7072),f8(f1(f1(f1(x7073))))))), % 62.16/62.31 inference(scs_inference,[],[704,2])). % 62.16/62.31 cnf(708,plain, % 62.16/62.31 (E(f5(f8(f1(f1(f1(x7081)))),f8(f1(x7082)),f8(f1(f1(x7083)))),f5(f8(x7081),f8(f1(x7082)),f8(x7083)))), % 62.16/62.31 inference(scs_inference,[],[704,698,2,3])). % 62.16/62.31 cnf(712,plain, % 62.16/62.31 (E(f5(f8(x7121),f8(f1(x7122)),f8(x7123)),f5(f8(f1(f1(f1(x7121)))),f8(f1(x7122)),f8(f1(f1(x7123)))))), % 62.16/62.31 inference(scs_inference,[],[708,2])). % 62.16/62.31 cnf(713,plain, % 62.16/62.31 (E(f4(f8(f1(f1(x7131))),f8(x7132)),f4(f8(x7131),f8(f1(x7132))))), % 62.16/62.31 inference(scs_inference,[],[569,708,501,2,3])). % 62.16/62.31 cnf(717,plain, % 62.16/62.31 (E(f4(f8(x7171),f8(f1(x7172))),f4(f8(f1(f1(x7171))),f8(x7172)))), % 62.16/62.31 inference(scs_inference,[],[713,2])). % 62.16/62.31 cnf(718,plain, % 62.16/62.31 (E(f4(f8(f1(f1(f1(x7181)))),f8(x7182)),f4(f8(x7181),f8(f1(x7182))))), % 62.16/62.31 inference(scs_inference,[],[713,569,2,3])). % 62.16/62.31 cnf(722,plain, % 62.16/62.31 (E(f4(f8(x7221),f8(f1(x7222))),f4(f8(f1(f1(f1(x7221)))),f8(x7222)))), % 62.16/62.31 inference(scs_inference,[],[718,2])). % 62.16/62.31 cnf(723,plain, % 62.16/62.31 (E(f4(f8(x7231),f8(f1(f1(x7232)))),f4(f8(f1(f1(f1(x7231)))),f8(x7232)))), % 62.16/62.31 inference(scs_inference,[],[717,718,497,2,3])). % 62.16/62.31 cnf(727,plain, % 62.16/62.31 (E(f4(f8(f1(f1(f1(x7271)))),f8(x7272)),f4(f8(x7271),f8(f1(f1(x7272)))))), % 62.16/62.31 inference(scs_inference,[],[723,2])). % 62.16/62.31 cnf(728,plain, % 62.16/62.31 (E(f4(f8(x7281),f8(f1(x7282))),f4(f8(f1(f1(f1(x7281)))),f8(f1(x7282))))), % 62.16/62.31 inference(scs_inference,[],[722,723,470,2,3])). % 62.16/62.31 cnf(731,plain, % 62.16/62.31 (E(f4(f8(f1(f1(f1(x7311)))),f8(f1(x7312))),f4(f8(x7311),f8(f1(x7312))))), % 62.16/62.31 inference(scs_inference,[],[728,2])). % 62.16/62.31 cnf(732,plain, % 62.16/62.31 (E(f4(f8(x7321),f8(f1(x7322))),f4(f8(x7321),f8(f1(f1(f1(x7322))))))), % 62.16/62.31 inference(scs_inference,[],[728,727,2,3])). % 62.16/62.31 cnf(735,plain, % 62.16/62.31 (E(f4(f8(x7351),f8(f1(f1(f1(x7352))))),f4(f8(x7351),f8(f1(x7352))))), % 62.16/62.31 inference(scs_inference,[],[732,2])). % 62.16/62.31 cnf(736,plain, % 62.16/62.31 (E(f4(f8(f1(f1(f1(x7361)))),f8(f1(x7362))),f4(f8(f1(f1(x7361))),f8(x7362)))), % 62.16/62.31 inference(scs_inference,[],[731,732,717,2,3])). % 62.16/62.31 cnf(739,plain, % 62.16/62.31 (E(f4(f8(f1(f1(x7391))),f8(x7392)),f4(f8(f1(f1(f1(x7391)))),f8(f1(x7392))))), % 62.16/62.31 inference(scs_inference,[],[736,2])). % 62.16/62.31 cnf(740,plain, % 62.16/62.31 (E(f6(f8(f1(f1(f1(x7401)))),f8(x7402)),f6(f8(f1(f1(x7401))),f8(f1(x7402))))), % 62.16/62.31 inference(scs_inference,[],[669,736,510,2,3])). % 62.16/62.31 cnf(742,plain, % 62.16/62.31 (E(f6(f8(f1(f1(x7421))),f8(f1(x7422))),f6(f8(f1(f1(f1(x7421)))),f8(x7422)))), % 62.16/62.31 inference(scs_inference,[],[740,2])). % 62.16/62.31 cnf(743,plain, % 62.16/62.31 (E(f6(f8(f1(f1(f1(f1(x7431))))),f8(x7432)),f6(f8(x7431),f8(x7432)))), % 62.16/62.31 inference(scs_inference,[],[740,657,2,3])). % 62.16/62.31 cnf(747,plain, % 62.16/62.31 (E(f6(f8(x7471),f8(x7472)),f6(f8(f1(f1(f1(f1(x7471))))),f8(x7472)))), % 62.16/62.31 inference(scs_inference,[],[743,2])). % 62.16/62.31 cnf(748,plain, % 62.16/62.31 (E(f6(f8(f1(f1(f1(x7481)))),f8(f1(f1(x7482)))),f6(f8(x7481),f8(x7482)))), % 62.16/62.31 inference(scs_inference,[],[742,743,534,2,3])). % 62.16/62.31 cnf(751,plain, % 62.16/62.31 (E(f6(f8(x7511),f8(x7512)),f6(f8(f1(f1(f1(x7511)))),f8(f1(f1(x7512)))))), % 62.16/62.31 inference(scs_inference,[],[748,2])). % 62.16/62.31 cnf(752,plain, % 62.16/62.31 (E(f6(f8(x7521),f8(f1(f1(x7522)))),f6(f8(f1(x7521)),f8(x7522)))), % 62.16/62.31 inference(scs_inference,[],[747,748,2,3])). % 62.16/62.31 cnf(756,plain, % 62.16/62.31 (E(f6(f8(f1(x7561)),f8(x7562)),f6(f8(x7561),f8(f1(f1(x7562)))))), % 62.16/62.31 inference(scs_inference,[],[752,2])). % 62.16/62.31 cnf(757,plain, % 62.16/62.31 (E(f6(f8(f1(f1(x7571))),f8(f1(f1(x7572)))),f6(f8(x7571),f8(x7572)))), % 62.16/62.31 inference(scs_inference,[],[752,669,2,3])). % 62.16/62.31 cnf(761,plain, % 62.16/62.31 (E(f6(f8(x7611),f8(x7612)),f6(f8(f1(f1(x7611))),f8(f1(f1(x7612)))))), % 62.16/62.31 inference(scs_inference,[],[757,2])). % 62.16/62.31 cnf(765,plain, % 62.16/62.31 (E(f11(f8(f1(x7651)),x7652),f11(f8(x7651),x7652))), % 62.16/62.31 inference(scs_inference,[],[425,2])). % 62.16/62.31 cnf(766,plain, % 62.16/62.31 (E(f12(f12(x7661,f8(f1(f1(f1(x7662))))),f8(x7663)),f12(f12(x7661,f8(x7662)),f8(f1(x7663))))), % 62.16/62.31 inference(scs_inference,[],[102,680,425,2,3])). % 62.16/62.31 cnf(771,plain, % 62.16/62.31 (E(f11(f8(x7711),f8(x7712)),f11(f8(f1(x7711)),f8(f1(f1(f1(x7712))))))), % 62.16/62.31 inference(scs_inference,[],[765,766,600,2,3])). % 62.16/62.31 cnf(774,plain, % 62.16/62.31 (E(f11(f8(f1(x7741)),f8(f1(f1(f1(x7742))))),f11(f8(x7741),f8(x7742)))), % 62.16/62.31 inference(scs_inference,[],[771,2])). % 62.16/62.31 cnf(775,plain, % 62.16/62.31 (E(f11(f8(f1(x7751)),f8(x7752)),f11(f8(x7751),f8(f1(f1(f1(x7752))))))), % 62.16/62.31 inference(scs_inference,[],[625,771,765,2,3])). % 62.16/62.31 cnf(779,plain, % 62.16/62.31 (E(f11(f8(x7791),f8(f1(f1(f1(x7792))))),f11(f8(f1(x7791)),f8(x7792)))), % 62.16/62.31 inference(scs_inference,[],[775,2])). % 62.16/62.31 cnf(780,plain, % 62.16/62.31 (E(f5(f8(f1(x7801)),f8(f1(x7802)),f8(x7803)),f5(f8(f1(f1(x7801))),f8(x7802),f8(f1(f1(x7803)))))), % 62.16/62.31 inference(scs_inference,[],[620,775,456,2,3])). % 62.16/62.31 cnf(783,plain, % 62.16/62.31 (E(f5(f8(f1(f1(x7831))),f8(x7832),f8(f1(f1(x7833)))),f5(f8(f1(x7831)),f8(f1(x7832)),f8(x7833)))), % 62.16/62.31 inference(scs_inference,[],[780,2])). % 62.16/62.31 cnf(784,plain, % 62.16/62.31 (E(f5(f8(f1(f1(f1(x7841)))),f8(x7842),f8(x7843)),f5(f8(x7841),f8(f1(f1(f1(x7842)))),f8(x7843)))), % 62.16/62.31 inference(scs_inference,[],[650,780,708,2,3])). % 62.16/62.31 cnf(787,plain, % 62.16/62.31 (E(f5(f8(x7871),f8(f1(f1(f1(x7872)))),f8(x7873)),f5(f8(f1(f1(f1(x7871)))),f8(x7872),f8(x7873)))), % 62.16/62.31 inference(scs_inference,[],[784,2])). % 62.16/62.31 cnf(788,plain, % 62.16/62.31 (E(f5(f8(f1(f1(x7881))),f8(x7882),f8(f1(f1(x7883)))),f5(f8(f1(x7881)),f8(f1(f1(x7882))),f8(f1(x7883))))), % 62.16/62.31 inference(scs_inference,[],[783,784,477,2,3])). % 62.16/62.31 cnf(791,plain, % 62.16/62.31 (E(f5(f8(f1(x7911)),f8(f1(f1(x7912))),f8(f1(x7913))),f5(f8(f1(f1(x7911))),f8(x7912),f8(f1(f1(x7913)))))), % 62.16/62.31 inference(scs_inference,[],[788,2])). % 62.16/62.31 cnf(792,plain, % 62.16/62.31 (E(f5(f8(x7921),f8(f1(f1(f1(f1(x7922))))),f8(x7923)),f5(f8(f1(x7921)),f8(x7922),f8(f1(x7923))))), % 62.16/62.31 inference(scs_inference,[],[787,788,698,2,3])). % 62.16/62.31 cnf(796,plain, % 62.16/62.31 (E(f5(f8(f1(x7961)),f8(x7962),f8(f1(x7963))),f5(f8(x7961),f8(f1(f1(f1(f1(x7962))))),f8(x7963)))), % 62.16/62.31 inference(scs_inference,[],[792,2])). % 62.16/62.31 cnf(797,plain, % 62.16/62.31 (E(f4(f8(x7971),f8(f1(f1(f1(x7972))))),f4(f8(x7971),f8(x7972)))), % 62.16/62.31 inference(scs_inference,[],[735,792,486,2,3])). % 62.16/62.31 cnf(799,plain, % 62.16/62.31 (E(f4(f8(x7991),f8(x7992)),f4(f8(x7991),f8(f1(f1(f1(x7992))))))), % 62.16/62.31 inference(scs_inference,[],[797,2])). % 62.16/62.31 cnf(800,plain, % 62.16/62.31 (E(f4(f8(f1(f1(x8001))),f8(f1(f1(x8002)))),f4(f8(f1(f1(f1(x8001)))),f8(x8002)))), % 62.16/62.31 inference(scs_inference,[],[797,739,2,3])). % 62.16/62.31 cnf(805,plain, % 62.16/62.31 (E(f5(f8(f1(f1(x8051))),f8(x8052),f8(f1(f1(x8053)))),f5(f8(f1(f1(x8051))),f8(f1(x8052)),f8(x8053)))), % 62.16/62.31 inference(scs_inference,[],[796,800,646,2,3])). % 62.16/62.31 cnf(809,plain, % 62.16/62.31 (E(f5(f8(f1(f1(x8091))),f8(f1(x8092)),f8(x8093)),f5(f8(f1(f1(x8091))),f8(x8092),f8(f1(f1(x8093)))))), % 62.16/62.31 inference(scs_inference,[],[805,2])). % 62.16/62.31 cnf(810,plain, % 62.16/62.31 (E(f5(f8(x8101),f8(f1(x8102)),f8(x8103)),f5(f8(f1(f1(f1(x8101)))),f8(f1(f1(x8102))),f8(x8103)))), % 62.16/62.31 inference(scs_inference,[],[805,712,2,3])). % 62.16/62.31 cnf(813,plain, % 62.16/62.31 (E(f5(f8(f1(f1(f1(x8131)))),f8(f1(f1(x8132))),f8(x8133)),f5(f8(x8131),f8(f1(x8132)),f8(x8133)))), % 62.16/62.31 inference(scs_inference,[],[810,2])). % 62.16/62.31 cnf(814,plain, % 62.16/62.31 (E(f5(f8(x8141),f8(f1(f1(x8142))),f8(f1(f1(x8143)))),f5(f8(f1(f1(f1(x8141)))),f8(x8142),f8(x8143)))), % 62.16/62.31 inference(scs_inference,[],[810,647,2,3])). % 62.16/62.31 cnf(818,plain, % 62.16/62.31 (E(f5(f8(f1(f1(f1(x8181)))),f8(x8182),f8(x8183)),f5(f8(x8181),f8(f1(f1(x8182))),f8(f1(f1(x8183)))))), % 62.16/62.31 inference(scs_inference,[],[814,2])). % 62.16/62.31 cnf(819,plain, % 62.16/62.31 (E(f6(f8(x8191),f8(x8192)),f6(f8(f1(x8191)),f8(f1(f1(x8192)))))), % 62.16/62.31 inference(scs_inference,[],[814,751,529,2,3])). % 62.16/62.31 cnf(822,plain, % 62.16/62.31 (E(f6(f8(f1(x8221)),f8(f1(f1(x8222)))),f6(f8(x8221),f8(x8222)))), % 62.16/62.31 inference(scs_inference,[],[819,2])). % 62.16/62.31 cnf(823,plain, % 62.16/62.31 (E(f6(f8(f1(f1(f1(x8231)))),f8(x8232)),f6(f8(x8231),f8(f1(x8232))))), % 62.16/62.31 inference(scs_inference,[],[756,819,523,2,3])). % 62.16/62.31 cnf(827,plain, % 62.16/62.31 (E(f6(f8(x8271),f8(f1(x8272))),f6(f8(f1(f1(f1(x8271)))),f8(x8272)))), % 62.16/62.31 inference(scs_inference,[],[823,2])). % 62.16/62.31 cnf(828,plain, % 62.16/62.31 (E(f6(f8(f1(x8281)),f8(f1(f1(x8282)))),f6(f8(f1(f1(f1(x8281)))),f8(x8282)))), % 62.16/62.31 inference(scs_inference,[],[822,823,666,2,3])). % 62.16/62.31 cnf(832,plain, % 62.16/62.31 (E(f6(f8(x8321),f8(f1(f1(x8322)))),f6(f8(f1(f1(x8321))),f8(x8322)))), % 62.16/62.31 inference(scs_inference,[],[827,828,662,2,3])). % 62.16/62.31 cnf(836,plain, % 62.16/62.31 (E(f6(f8(f1(f1(x8361))),f8(x8362)),f6(f8(x8361),f8(f1(f1(x8362)))))), % 62.16/62.31 inference(scs_inference,[],[832,2])). % 62.16/62.31 cnf(837,plain, % 62.16/62.31 (E(f6(f8(x8371),f8(f1(f1(f1(f1(x8372)))))),f6(f8(x8371),f8(x8372)))), % 62.16/62.31 inference(scs_inference,[],[832,757,2,3])). % 62.16/62.31 cnf(841,plain, % 62.16/62.31 (E(f6(f8(x8411),f8(x8412)),f6(f8(x8411),f8(f1(f1(f1(f1(x8412)))))))), % 62.16/62.31 inference(scs_inference,[],[837,2])). % 62.16/62.31 cnf(842,plain, % 62.16/62.31 (E(f5(f8(f1(f1(f1(x8421)))),f8(f1(f1(x8422))),f8(x8423)),f5(f8(x8421),f8(x8422),f8(x8423)))), % 62.16/62.31 inference(scs_inference,[],[813,837,576,2,3])). % 62.16/62.31 cnf(845,plain, % 62.16/62.31 (E(f5(f8(x8451),f8(x8452),f8(x8453)),f5(f8(f1(f1(f1(x8451)))),f8(f1(f1(x8452))),f8(x8453)))), % 62.16/62.31 inference(scs_inference,[],[842,2])). % 62.16/62.31 cnf(846,plain, % 62.16/62.31 (E(f6(f8(f1(x8461)),f8(x8462)),f6(f8(x8461),f8(f1(f1(f1(x8462))))))), % 62.16/62.31 inference(scs_inference,[],[842,761,823,2,3])). % 62.16/62.31 cnf(849,plain, % 62.16/62.31 (E(f6(f8(x8491),f8(f1(f1(f1(x8492))))),f6(f8(f1(x8491)),f8(x8492)))), % 62.16/62.31 inference(scs_inference,[],[846,2])). % 62.16/62.31 cnf(850,plain, % 62.16/62.31 (E(f5(f8(x8501),f8(x8502),f8(x8503)),f5(f8(f1(f1(f1(x8501)))),f8(f1(x8502)),f8(f1(f1(x8503)))))), % 62.16/62.31 inference(scs_inference,[],[845,809,846,2,3])). % 62.16/62.31 cnf(853,plain, % 62.16/62.31 (E(f5(f8(f1(f1(f1(x8531)))),f8(f1(x8532)),f8(f1(f1(x8533)))),f5(f8(x8531),f8(x8532),f8(x8533)))), % 62.16/62.31 inference(scs_inference,[],[850,2])). % 62.16/62.31 cnf(854,plain, % 62.16/62.31 (E(f6(f8(f1(f1(x8541))),f8(f1(x8542))),f6(f8(f1(x8541)),f8(x8542)))), % 62.16/62.31 inference(scs_inference,[],[849,836,850,2,3])). % 62.16/62.31 cnf(858,plain, % 62.16/62.31 (E(f11(x8581,f8(f1(x8582))),f11(x8581,f8(x8582)))), % 62.16/62.31 inference(scs_inference,[],[429,2])). % 62.16/62.31 cnf(859,plain, % 62.16/62.31 (E(f5(f8(f1(f1(x8591))),f8(f1(f1(f1(x8592)))),f8(f1(x8593))),f5(f8(x8591),f8(x8592),f8(x8593)))), % 62.16/62.31 inference(scs_inference,[],[853,791,429,2,3])). % 62.16/62.31 cnf(862,plain, % 62.16/62.31 (E(f5(f8(x8621),f8(x8622),f8(x8623)),f5(f8(f1(f1(x8621))),f8(f1(f1(f1(x8622)))),f8(f1(x8623))))), % 62.16/62.31 inference(scs_inference,[],[859,2])). % 62.16/62.31 cnf(863,plain, % 62.16/62.31 (E(f6(f8(f1(f1(x8631))),f8(f1(f1(f1(x8632))))),f6(f8(x8631),f8(x8632)))), % 62.16/62.31 inference(scs_inference,[],[854,859,822,2,3])). % 62.16/62.31 cnf(867,plain, % 62.16/62.31 (E(f6(f8(x8671),f8(x8672)),f6(f8(f1(f1(x8671))),f8(f1(f1(f1(x8672))))))), % 62.16/62.31 inference(scs_inference,[],[863,2])). % 62.16/62.31 cnf(868,plain, % 62.16/62.31 (E(f6(f8(f1(f1(x8681))),f8(x8682)),f6(f8(x8681),f8(f1(x8682))))), % 62.16/62.31 inference(scs_inference,[],[863,841,2,3])). % 62.16/62.31 cnf(872,plain, % 62.16/62.31 (E(f6(f8(x8721),f8(f1(x8722))),f6(f8(f1(f1(x8721))),f8(x8722)))), % 62.16/62.31 inference(scs_inference,[],[868,2])). % 62.16/62.31 cnf(873,plain, % 62.16/62.31 (E(f5(f8(f1(x8731)),f8(x8732),f8(x8733)),f5(f8(x8731),f8(f1(f1(x8732))),f8(f1(x8733))))), % 62.16/62.31 inference(scs_inference,[],[862,868,813,2,3])). % 62.16/62.31 cnf(877,plain, % 62.16/62.31 (E(f5(f8(x8771),f8(f1(f1(x8772))),f8(f1(x8773))),f5(f8(f1(x8771)),f8(x8772),f8(x8773)))), % 62.16/62.31 inference(scs_inference,[],[873,2])). % 62.16/62.31 cnf(878,plain, % 62.16/62.31 (E(f6(f8(x8781),f8(f1(f1(x8782)))),f6(f8(f1(f1(f1(x8781)))),f8(x8782)))), % 62.16/62.31 inference(scs_inference,[],[872,873,742,2,3])). % 62.16/62.31 cnf(882,plain, % 62.16/62.31 (E(f6(f8(f1(f1(f1(x8821)))),f8(x8822)),f6(f8(x8821),f8(f1(f1(x8822)))))), % 62.16/62.31 inference(scs_inference,[],[878,2])). % 62.16/62.31 cnf(883,plain, % 62.16/62.31 (E(f5(f8(f1(f1(f1(x8831)))),f8(x8832),f8(x8833)),f5(f8(f1(x8831)),f8(x8832),f8(f1(x8833))))), % 62.16/62.31 inference(scs_inference,[],[877,878,818,2,3])). % 62.16/62.31 cnf(886,plain, % 62.16/62.31 (E(f5(f8(f1(x8861)),f8(x8862),f8(f1(x8863))),f5(f8(f1(f1(f1(x8861)))),f8(x8862),f8(x8863)))), % 62.16/62.31 inference(scs_inference,[],[883,2])). % 62.16/62.31 cnf(887,plain, % 62.16/62.31 (E(f5(f8(f1(f1(f1(x8871)))),f8(x8872),f8(x8873)),f5(f8(f1(x8871)),f8(f1(f1(f1(x8872)))),f8(x8873)))), % 62.16/62.31 inference(scs_inference,[],[883,658,2,3])). % 62.16/62.31 cnf(890,plain, % 62.16/62.31 (E(f5(f8(f1(x8901)),f8(f1(f1(f1(x8902)))),f8(x8903)),f5(f8(f1(f1(f1(x8901)))),f8(x8902),f8(x8903)))), % 62.16/62.31 inference(scs_inference,[],[887,2])). % 62.16/62.31 cnf(891,plain, % 62.16/62.31 (E(f5(f8(f1(x8911)),f8(x8912),f8(f1(x8913))),f5(f8(f1(f1(x8911))),f8(f1(f1(f1(x8912)))),f8(x8913)))), % 62.16/62.31 inference(scs_inference,[],[886,887,630,2,3])). % 62.16/62.31 cnf(894,plain, % 62.16/62.31 (E(f5(f8(f1(f1(x8941))),f8(f1(f1(f1(x8942)))),f8(x8943)),f5(f8(f1(x8941)),f8(x8942),f8(f1(x8943))))), % 62.16/62.31 inference(scs_inference,[],[891,2])). % 62.16/62.31 cnf(895,plain, % 62.16/62.31 (E(f5(f8(f1(x8951)),f8(x8952),f8(f1(x8953))),f5(f8(f1(f1(f1(f1(x8951))))),f8(x8952),f8(x8953)))), % 62.16/62.31 inference(scs_inference,[],[890,891,2,3])). % 62.16/62.31 cnf(898,plain, % 62.16/62.31 (E(f5(f8(f1(f1(f1(f1(x8981))))),f8(x8982),f8(x8983)),f5(f8(f1(x8981)),f8(x8982),f8(f1(x8983))))), % 62.16/62.31 inference(scs_inference,[],[895,2])). % 62.16/62.31 cnf(899,plain, % 62.16/62.31 (E(f5(f8(f1(x8991)),f8(f1(x8992)),f8(f1(f1(f1(x8993))))),f5(f8(f1(x8991)),f8(x8992),f8(x8993)))), % 62.16/62.31 inference(scs_inference,[],[895,853,2,3])). % 62.16/62.31 cnf(904,plain, % 62.16/62.31 (E(f11(f6(f6(x9041,f8(f1(x9042))),x9043),f8(f1(x9044))),f11(f6(f6(x9041,f8(x9042)),x9043),f8(x9044)))), % 62.16/62.31 inference(scs_inference,[],[858,899,175,2,3])). % 62.16/62.31 cnf(909,plain, % 62.16/62.31 (E(f11(f6(f6(x9091,f8(f1(x9092))),x9093),f8(f1(f1(x9094)))),f11(f6(f6(x9091,f8(x9092)),x9093),f8(x9094)))), % 62.16/62.31 inference(scs_inference,[],[904,858,2,3])). % 62.16/62.31 cnf(913,plain, % 62.16/62.31 (E(f5(f8(f1(f1(x9131))),f8(f1(f1(f1(f1(x9132))))),f8(x9133)),f5(f8(f1(x9131)),f8(x9132),f8(x9133)))), % 62.16/62.31 inference(scs_inference,[],[909,894,491,2,3])). % 62.16/62.31 cnf(917,plain, % 62.16/62.31 (E(f5(f8(f1(x9171)),f8(x9172),f8(x9173)),f5(f8(f1(f1(x9171))),f8(f1(f1(f1(f1(x9172))))),f8(x9173)))), % 62.16/62.31 inference(scs_inference,[],[913,2])). % 62.16/62.31 cnf(918,plain, % 62.16/62.31 (E(f6(f8(f1(f1(f1(x9181)))),f8(x9182)),f6(f8(f1(f1(x9181))),f8(x9182)))), % 62.16/62.31 inference(scs_inference,[],[913,882,832,2,3])). % 62.16/62.31 cnf(921,plain, % 62.16/62.31 (E(f5(f8(x9211),x9212,f8(f1(x9213))),f5(f8(f1(x9211)),x9212,f8(x9213)))), % 62.16/62.31 inference(scs_inference,[],[462,2])). % 62.16/62.31 cnf(922,plain, % 62.16/62.31 (E(f6(f8(f1(x9221)),f8(x9222)),f6(f8(f1(f1(x9221))),f8(f1(f1(f1(x9222))))))), % 62.16/62.31 inference(scs_inference,[],[918,867,462,2,3])). % 62.16/62.31 cnf(927,plain, % 62.16/62.31 (E(f6(f8(f1(x9271)),f8(f1(x9272))),f6(f8(f1(f1(x9271))),f8(x9272)))), % 62.16/62.31 inference(scs_inference,[],[922,837,2,3])). % 62.16/62.31 cnf(932,plain, % 62.16/62.31 (E(f5(f8(f1(f1(x9321))),f8(x9322),f8(x9323)),f5(f8(x9321),f8(f1(f1(x9322))),f8(x9323)))), % 62.16/62.31 inference(scs_inference,[],[917,927,842,2,3])). % 62.16/62.31 cnf(936,plain, % 62.16/62.31 (E(f5(f8(x9361),f8(f1(f1(x9362))),f8(x9363)),f5(f8(f1(f1(x9361))),f8(x9362),f8(x9363)))), % 62.16/62.31 inference(scs_inference,[],[932,2])). % 62.16/62.31 cnf(937,plain, % 62.16/62.31 (E(f5(f8(f1(f1(x9371))),f8(x9372),f8(f1(x9373))),f5(f8(f1(x9371)),f8(f1(f1(x9372))),f8(x9373)))), % 62.16/62.31 inference(scs_inference,[],[921,932,2,3])). % 62.16/62.31 cnf(941,plain, % 62.16/62.31 (E(f5(f8(f1(x9411)),f8(f1(f1(x9412))),f8(x9413)),f5(f8(f1(f1(x9411))),f8(x9412),f8(f1(x9413))))), % 62.16/62.31 inference(scs_inference,[],[937,2])). % 62.16/62.31 cnf(942,plain, % 62.16/62.31 (E(f5(f8(f1(f1(x9421))),f8(f1(f1(x9422))),f8(x9423)),f5(f8(f1(x9421)),f8(x9422),f8(f1(x9423))))), % 62.16/62.31 inference(scs_inference,[],[936,937,898,2,3])). % 62.16/62.31 cnf(945,plain, % 62.16/62.31 (E(f5(f8(f1(x9451)),f8(x9452),f8(f1(x9453))),f5(f8(f1(f1(x9451))),f8(f1(f1(x9452))),f8(x9453)))), % 62.16/62.31 inference(scs_inference,[],[942,2])). % 62.16/62.31 cnf(946,plain, % 62.16/62.31 (E(f5(f8(f1(f1(x9461))),f8(f1(f1(x9462))),f8(x9463)),f5(f8(x9461),f8(f1(f1(f1(x9462)))),f8(f1(x9463))))), % 62.16/62.31 inference(scs_inference,[],[941,942,784,2,3])). % 62.16/62.31 cnf(949,plain, % 62.16/62.31 (E(f4(f8(f1(x9491)),x9492),f4(f8(x9491),x9492))), % 62.16/62.31 inference(scs_inference,[],[36,2,15])). % 62.16/62.31 cnf(950,plain, % 62.16/62.31 (E(f5(f8(x9501),f8(f1(f1(f1(x9502)))),f8(f1(x9503))),f5(f8(f1(f1(x9501))),f8(f1(f1(x9502))),f8(x9503)))), % 62.16/62.31 inference(scs_inference,[],[946,2])). % 62.16/62.31 cnf(951,plain, % 62.16/62.31 (E(f5(f8(f1(x9511)),f8(x9512),f8(f1(x9513))),f5(f8(x9511),f8(f1(f1(f1(x9512)))),f8(f1(x9513))))), % 62.16/62.31 inference(scs_inference,[],[945,946,2,3])). % 62.16/62.31 cnf(953,plain, % 62.16/62.31 (E(f6(f8(f1(x9531)),x9532),f6(f8(x9531),x9532))), % 62.16/62.31 inference(scs_inference,[],[36,2,17])). % 62.16/62.31 cnf(954,plain, % 62.16/62.31 (E(f5(f8(x9541),f8(f1(f1(f1(x9542)))),f8(f1(x9543))),f5(f8(f1(x9541)),f8(x9542),f8(f1(x9543))))), % 62.16/62.31 inference(scs_inference,[],[951,2])). % 62.16/62.31 cnf(955,plain, % 62.16/62.31 (E(f4(f8(f1(x9551)),f8(x9552)),f4(f8(x9551),f8(f1(f1(f1(x9552))))))), % 62.16/62.31 inference(scs_inference,[],[949,951,799,2,3])). % 62.16/62.31 cnf(958,plain, % 62.16/62.31 (E(f6(x9581,f8(f1(x9582))),f6(x9581,f8(x9582)))), % 62.16/62.31 inference(scs_inference,[],[36,2,18])). % 62.16/62.31 cnf(959,plain, % 62.16/62.31 (E(f4(f8(x9591),f8(f1(f1(f1(x9592))))),f4(f8(f1(x9591)),f8(x9592)))), % 62.16/62.31 inference(scs_inference,[],[955,2])). % 62.16/62.31 cnf(960,plain, % 62.16/62.31 (E(f6(f6(x9601,f8(x9602)),f8(f1(x9603))),f6(f6(x9601,f8(f1(x9602))),f8(x9603)))), % 62.16/62.31 inference(scs_inference,[],[101,958,955,2,3])). % 62.16/62.31 cnf(963,plain, % 62.16/62.31 (E(f12(x9631,f8(f1(x9632))),f12(x9631,f8(x9632)))), % 62.16/62.31 inference(scs_inference,[],[36,2,20])). % 62.16/62.31 cnf(965,plain, % 62.16/62.31 (E(f12(f8(f1(x9651)),f8(f1(x9652))),f12(f8(x9651),f8(x9652)))), % 62.16/62.31 inference(scs_inference,[],[496,960,963,2,3])). % 62.16/62.31 cnf(969,plain, % 62.16/62.31 (E(f12(f8(x9691),f8(x9692)),f12(f8(f1(x9691)),f8(f1(x9692))))), % 62.16/62.31 inference(scs_inference,[],[965,2])). % 62.16/62.31 cnf(970,plain, % 62.16/62.31 (E(f12(f8(f1(f1(x9701))),f8(f1(x9702))),f12(f8(x9701),f8(x9702)))), % 62.16/62.31 inference(scs_inference,[],[965,496,2,3])). % 62.16/62.31 cnf(973,plain, % 62.16/62.31 (E(f12(f8(x9731),f8(x9732)),f12(f8(f1(f1(x9731))),f8(f1(x9732))))), % 62.16/62.31 inference(scs_inference,[],[970,2])). % 62.16/62.31 cnf(974,plain, % 62.16/62.31 (E(f6(f6(x9741,f8(x9742)),f8(f1(x9743))),f6(f6(x9741,f8(f1(f1(x9742)))),f8(x9743)))), % 62.16/62.31 inference(scs_inference,[],[101,970,960,2,3])). % 62.16/62.31 cnf(979,plain, % 62.16/62.31 (E(f6(f6(x9791,f8(x9792)),f8(f1(x9793))),f6(f6(x9791,f8(f1(f1(f1(x9792))))),f8(x9793)))), % 62.16/62.31 inference(scs_inference,[],[101,974,2,3])). % 62.16/62.31 cnf(984,plain, % 62.16/62.31 (E(f12(f8(x9841),f8(x9842)),f12(f8(f1(f1(f1(x9841)))),f8(f1(f1(x9842)))))), % 62.16/62.31 inference(scs_inference,[],[979,969,973,2,3])). % 62.16/62.31 cnf(986,plain, % 62.16/62.31 (E(f12(f8(f1(f1(f1(x9861)))),f8(f1(f1(x9862)))),f12(f8(x9861),f8(x9862)))), % 62.16/62.31 inference(scs_inference,[],[984,2])). % 62.16/62.31 cnf(987,plain, % 62.16/62.31 (E(f12(f12(x9871,f8(f1(x9872))),f8(f1(x9873))),f12(f12(x9871,f8(x9872)),f8(x9873)))), % 62.16/62.31 inference(scs_inference,[],[102,984,963,2,3])). % 62.16/62.31 cnf(992,plain, % 62.16/62.31 (E(f12(f12(x9921,f8(f1(f1(x9922)))),f8(f1(x9923))),f12(f12(x9921,f8(x9922)),f8(x9923)))), % 62.16/62.31 inference(scs_inference,[],[102,987,2,3])). % 62.16/62.31 cnf(997,plain, % 62.16/62.31 (E(f12(f12(x9971,f8(f1(f1(f1(x9972))))),f8(f1(x9973))),f12(f12(x9971,f8(x9972)),f8(x9973)))), % 62.16/62.31 inference(scs_inference,[],[102,992,2,3])). % 62.16/62.31 cnf(1002,plain, % 62.16/62.31 (E(f12(f8(f1(f1(f1(x10021)))),f8(f1(f1(x10022)))),f12(f8(f1(x10021)),f8(x10022)))), % 62.16/62.31 inference(scs_inference,[],[986,997,485,2,3])). % 62.16/62.31 cnf(1006,plain, % 62.16/62.31 (E(f4(f8(f1(f1(x10061))),f8(f1(f1(f1(x10062))))),f4(f8(x10061),f8(f1(x10062))))), % 62.16/62.31 inference(scs_inference,[],[959,1002,718,2,3])). % 62.16/62.31 cnf(1011,plain, % 62.16/62.31 (E(f5(f8(x10111),f6(f6(x10112,f8(f1(x10113))),x10114),f8(f1(x10115))),f5(f8(f1(x10111)),f6(f6(x10112,f8(x10113)),x10114),f8(x10115)))), % 62.16/62.31 inference(scs_inference,[],[1006,921,187,2,3])). % 62.16/62.31 cnf(1016,plain, % 62.16/62.31 (E(f6(f12(f12(x10161,f8(x10162)),x10163),f8(f1(x10164))),f6(f12(f12(x10161,f8(f1(x10162))),x10163),f8(x10164)))), % 62.16/62.31 inference(scs_inference,[],[1011,958,243,2,3])). % 62.16/62.31 cnf(1021,plain, % 62.16/62.32 (E(f6(f12(f12(x10211,f8(x10212)),x10213),f8(f1(f1(x10214)))),f6(f12(f12(x10211,f8(f1(x10212))),x10213),f8(x10214)))), % 62.16/62.32 inference(scs_inference,[],[1016,958,2,3])). % 62.16/62.32 cnf(1025,plain, % 62.16/62.32 (E(f5(f8(x10251),f8(f1(f1(f1(x10252)))),f8(f1(f1(x10253)))),f5(f8(f1(x10251)),f8(f1(x10252)),f8(x10253)))), % 62.16/62.32 inference(scs_inference,[],[950,1021,502,2,3])). % 62.16/62.32 cnf(1029,plain, % 62.16/62.32 (E(f5(f8(f1(x10291)),f8(f1(x10292)),f8(x10293)),f5(f8(x10291),f8(f1(f1(f1(x10292)))),f8(f1(f1(x10293)))))), % 62.16/62.32 inference(scs_inference,[],[1025,2])). % 62.16/62.32 cnf(1030,plain, % 62.16/62.32 (E(f5(f8(x10301),f8(f1(f1(f1(x10302)))),f8(f1(f1(x10303)))),f5(f8(x10301),f8(x10302),f8(x10303)))), % 62.16/62.32 inference(scs_inference,[],[1025,665,2,3])). % 62.16/62.32 cnf(1033,plain, % 62.16/62.32 (E(f5(f8(x10331),f8(x10332),f8(x10333)),f5(f8(x10331),f8(f1(f1(f1(x10332)))),f8(f1(f1(x10333)))))), % 62.16/62.32 inference(scs_inference,[],[1030,2])). % 62.16/62.32 cnf(1034,plain, % 62.16/62.32 (E(f11(f8(f1(x10341)),f8(f1(f1(f1(x10342))))),f11(f8(f1(x10341)),f8(f1(x10342))))), % 62.16/62.32 inference(scs_inference,[],[774,1030,439,2,3])). % 62.16/62.32 cnf(1037,plain, % 62.16/62.32 (E(f11(f8(f1(x10371)),f8(f1(x10372))),f11(f8(f1(x10371)),f8(f1(f1(f1(x10372))))))), % 62.16/62.32 inference(scs_inference,[],[1034,2])). % 62.16/62.32 cnf(1038,plain, % 62.16/62.32 (E(f5(f8(f1(x10381)),f8(f1(x10382)),f8(x10383)),f5(f8(f1(x10381)),f8(x10382),f8(f1(f1(x10383)))))), % 62.16/62.32 inference(scs_inference,[],[954,1034,1029,2,3])). % 62.16/62.32 cnf(1041,plain, % 62.16/62.32 (E(f5(f8(f1(x10411)),f8(x10412),f8(f1(f1(x10413)))),f5(f8(f1(x10411)),f8(f1(x10412)),f8(x10413)))), % 62.16/62.32 inference(scs_inference,[],[1038,2])). % 62.16/62.32 cnf(1042,plain, % 62.16/62.32 (E(f5(f8(f1(f1(x10421))),f8(x10422),f8(x10423)),f5(f8(f1(x10421)),f8(f1(f1(f1(f1(x10422))))),f8(x10423)))), % 62.16/62.32 inference(scs_inference,[],[1033,1038,783,2,3])). % 62.16/62.32 cnf(1046,plain, % 62.16/62.32 (E(f5(f8(f1(x10461)),f8(f1(f1(f1(f1(x10462))))),f8(x10463)),f5(f8(f1(f1(x10461))),f8(x10462),f8(x10463)))), % 62.16/62.32 inference(scs_inference,[],[1042,2])). % 62.16/62.32 cnf(1047,plain, % 62.16/62.32 (E(f5(f8(f1(x10471)),f8(f1(x10472)),f8(f1(f1(f1(x10473))))),f5(f8(f1(f1(x10471))),f8(x10472),f8(x10473)))), % 62.16/62.32 inference(scs_inference,[],[1041,1042,877,2,3])). % 62.16/62.32 cnf(1052,plain, % 62.16/62.32 (E(f11(f8(f1(f1(x10521))),f8(f1(f1(f1(x10522))))),f11(f8(x10521),f8(f1(x10522))))), % 62.16/62.32 inference(scs_inference,[],[779,1047,606,2,3])). % 62.16/62.32 cnf(1057,plain, % 62.16/62.32 (E(f5(f8(f1(x10571)),f8(f1(f1(f1(f1(x10572))))),f8(f1(x10573))),f5(f8(f1(x10571)),f8(x10572),f8(x10573)))), % 62.16/62.32 inference(scs_inference,[],[1046,1052,584,2,3])). % 62.16/62.32 cnf(1061,plain, % 62.16/62.32 (E(f5(f8(f1(x10611)),f8(x10612),f8(x10613)),f5(f8(f1(x10611)),f8(f1(f1(f1(f1(x10612))))),f8(f1(x10613))))), % 62.16/62.32 inference(scs_inference,[],[1057,2])). % 62.16/62.32 cnf(1062,plain, % 62.16/62.32 (E(f11(f8(f1(f1(x10621))),f8(f1(x10622))),f11(f8(x10621),f8(f1(f1(x10622)))))), % 62.16/62.32 inference(scs_inference,[],[1057,1037,461,2,3])). % 62.16/62.32 cnf(1065,plain, % 62.16/62.32 (E(f11(f8(x10651),f8(f1(f1(x10652)))),f11(f8(f1(f1(x10651))),f8(f1(x10652))))), % 62.16/62.32 inference(scs_inference,[],[1062,2])). % 62.16/62.32 cnf(1066,plain, % 62.16/62.32 (E(f11(f8(f1(f1(x10661))),f8(f1(f1(x10662)))),f11(f8(x10661),f8(x10662)))), % 62.16/62.32 inference(scs_inference,[],[1062,621,2,3])). % 62.16/62.32 cnf(1070,plain, % 62.16/62.32 (E(f11(f8(x10701),f8(x10702)),f11(f8(f1(f1(x10701))),f8(f1(f1(x10702)))))), % 62.16/62.32 inference(scs_inference,[],[1066,2])). % 62.16/62.32 cnf(1071,plain, % 62.16/62.32 (E(f5(f8(f1(x10711)),f8(x10712),f8(x10713)),f5(f8(f1(f1(f1(f1(x10711))))),f8(f1(x10712)),f8(f1(x10713))))), % 62.16/62.32 inference(scs_inference,[],[1066,1061,787,2,3])). % 62.16/62.32 cnf(1074,plain, % 62.16/62.32 (E(f5(f8(f1(f1(f1(f1(x10741))))),f8(f1(x10742)),f8(f1(x10743))),f5(f8(f1(x10741)),f8(x10742),f8(x10743)))), % 62.16/62.32 inference(scs_inference,[],[1071,2])). % 62.16/62.32 cnf(1075,plain, % 62.16/62.32 (E(f11(f8(x10751),f8(f1(f1(x10752)))),f11(f8(f1(f1(f1(x10751)))),f8(x10752)))), % 62.16/62.32 inference(scs_inference,[],[1065,1071,577,2,3])). % 62.16/62.32 cnf(1078,plain, % 62.16/62.32 (E(f11(f8(f1(f1(f1(x10781)))),f8(x10782)),f11(f8(x10781),f8(f1(f1(x10782)))))), % 62.16/62.32 inference(scs_inference,[],[1075,2])). % 62.16/62.32 cnf(1079,plain, % 62.16/62.32 (E(f11(f8(x10791),f8(f1(f1(x10792)))),f11(f8(f1(x10791)),f8(x10792)))), % 62.16/62.32 inference(scs_inference,[],[1075,467,2,3])). % 62.16/62.32 cnf(1082,plain, % 62.16/62.32 (E(f11(f8(f1(x10821)),f8(x10822)),f11(f8(x10821),f8(f1(f1(x10822)))))), % 62.16/62.32 inference(scs_inference,[],[1079,2])). % 62.16/62.32 cnf(1083,plain, % 62.16/62.32 (E(f11(f8(x10831),f8(x10832)),f11(f8(f1(f1(f1(x10831)))),f8(x10832)))), % 62.16/62.32 inference(scs_inference,[],[1079,1070,2,3])). % 62.16/62.32 cnf(1086,plain, % 62.16/62.32 (E(f11(f8(f1(f1(f1(x10861)))),f8(x10862)),f11(f8(x10861),f8(x10862)))), % 62.16/62.32 inference(scs_inference,[],[1083,2])). % 62.16/62.32 cnf(1087,plain, % 62.16/62.32 (E(f11(f8(x10871),f8(x10872)),f11(f8(x10871),f8(f1(f1(x10872)))))), % 62.16/62.32 inference(scs_inference,[],[1083,1078,2,3])). % 62.16/62.32 cnf(1090,plain, % 62.16/62.32 (E(f11(f8(x10901),f8(f1(f1(x10902)))),f11(f8(x10901),f8(x10902)))), % 62.16/62.32 inference(scs_inference,[],[1087,2])). % 62.16/62.32 cnf(1091,plain, % 62.16/62.32 (E(f11(f8(f1(f1(f1(x10911)))),f8(x10912)),f11(f8(f1(x10911)),f8(f1(f1(x10912)))))), % 62.16/62.32 inference(scs_inference,[],[1086,1087,596,2,3])). % 62.16/62.32 cnf(1095,plain, % 62.16/62.32 (E(f11(f8(x10951),f8(f1(f1(x10952)))),f11(f8(f1(f1(x10951))),f8(x10952)))), % 62.16/62.32 inference(scs_inference,[],[1090,1091,471,2,3])). % 62.16/62.32 cnf(1099,plain, % 62.16/62.32 (E(f11(f8(x10991),f8(f1(f1(f1(f1(x10992)))))),f11(f8(x10991),f8(x10992)))), % 62.16/62.32 inference(scs_inference,[],[1095,1066,2,3])). % 62.16/62.32 cnf(1104,plain, % 62.16/62.32 (E(f4(f8(x11041),f5(x11042,x11043,f8(f1(x11044)))),f4(f8(f1(x11041)),f5(x11042,x11043,f8(x11044))))), % 62.16/62.32 inference(scs_inference,[],[98,1099,465,2,3])). % 62.16/62.32 cnf(1108,plain, % 62.16/62.32 (E(f4(f8(f1(x11081)),f5(x11082,x11083,f8(x11084))),f4(f8(x11081),f5(x11082,x11083,f8(f1(x11084)))))), % 62.16/62.32 inference(scs_inference,[],[1104,2])). % 62.16/62.32 cnf(1109,plain, % 62.16/62.32 (E(f11(f8(f1(f1(f1(x11091)))),f8(f1(x11092))),f11(f8(x11091),f8(x11092)))), % 62.16/62.32 inference(scs_inference,[],[1104,1082,597,2,3])). % 62.16/62.32 cnf(1112,plain, % 62.16/62.32 (E(f11(f8(x11121),f8(x11122)),f11(f8(f1(f1(f1(x11121)))),f8(f1(x11122))))), % 62.16/62.32 inference(scs_inference,[],[1109,2])). % 62.16/62.32 cnf(1113,plain, % 62.16/62.32 (E(f4(f8(f1(x11131)),f5(x11132,x11133,f8(x11134))),f4(f8(x11131),f5(x11132,x11133,f8(f1(f1(x11134))))))), % 62.16/62.32 inference(scs_inference,[],[99,1109,1108,2,3])). % 62.16/62.32 cnf(1118,plain, % 62.16/62.32 (E(f11(f8(x11181),f8(x11182)),f11(f8(f1(f1(f1(f1(x11181))))),f8(x11182)))), % 62.16/62.32 inference(scs_inference,[],[1112,1113,577,2,3])). % 62.16/62.32 cnf(1121,plain, % 62.16/62.32 (E(f11(f8(f1(f1(f1(f1(x11211))))),f8(x11212)),f11(f8(x11211),f8(x11212)))), % 62.16/62.32 inference(scs_inference,[],[1118,2])). % 62.16/62.32 cnf(1122,plain, % 62.16/62.32 (E(f11(f8(x11221),f8(f1(x11222))),f11(f8(f1(x11221)),f8(x11222)))), % 62.16/62.32 inference(scs_inference,[],[1118,1109,2,3])). % 62.16/62.32 cnf(1126,plain, % 62.16/62.32 (E(f11(f8(f1(x11261)),f8(x11262)),f11(f8(x11261),f8(f1(x11262))))), % 62.16/62.32 inference(scs_inference,[],[1122,2])). % 62.16/62.32 cnf(1127,plain, % 62.16/62.32 (E(f6(f6(x11271,f8(x11272)),f8(x11273)),f6(f6(x11271,f8(f1(x11272))),f8(f1(x11273))))), % 62.16/62.32 inference(scs_inference,[],[101,1122,480,2,3])). % 62.16/62.32 cnf(1132,plain, % 62.16/62.32 (E(f6(f6(x11321,f8(x11322)),f8(x11323)),f6(f6(x11321,f8(f1(f1(x11322)))),f8(f1(x11323))))), % 62.16/62.32 inference(scs_inference,[],[101,1127,2,3])). % 62.16/62.32 cnf(1137,plain, % 62.16/62.32 (E(f6(f6(x11371,f8(x11372)),f8(x11373)),f6(f6(x11371,f8(f1(f1(f1(x11372))))),f8(f1(x11373))))), % 62.16/62.32 inference(scs_inference,[],[101,1132,2,3])). % 62.16/62.32 cnf(1142,plain, % 62.16/62.32 (E(f3(f3(x11421,f8(x11422)),f8(x11423)),f3(f3(x11421,f8(f1(x11422))),f8(f1(x11423))))), % 62.16/62.32 inference(scs_inference,[],[105,1137,500,2,3])). % 62.16/62.32 cnf(1146,plain, % 62.16/62.32 (E(f3(f3(x11461,f8(f1(x11462))),f8(f1(x11463))),f3(f3(x11461,f8(x11462)),f8(x11463)))), % 62.16/62.32 inference(scs_inference,[],[1142,2])). % 62.16/62.32 cnf(1147,plain, % 62.16/62.32 (E(f5(f8(f1(f1(f1(f1(x11471))))),f8(f1(x11472)),f8(f1(x11473))),f5(f8(x11471),f8(x11472),f8(x11473)))), % 62.16/62.32 inference(scs_inference,[],[1074,1142,456,2,3])). % 62.16/62.32 cnf(1150,plain, % 62.16/62.32 (E(f5(f8(x11501),f8(x11502),f8(x11503)),f5(f8(f1(f1(f1(f1(x11501))))),f8(f1(x11502)),f8(f1(x11503))))), % 62.16/62.32 inference(scs_inference,[],[1147,2])). % 62.16/62.32 cnf(1151,plain, % 62.16/62.32 (E(f3(f3(x11511,f8(f1(f1(x11512)))),f8(f1(x11513))),f3(f3(x11511,f8(x11512)),f8(x11513)))), % 62.16/62.32 inference(scs_inference,[],[104,1146,1147,2,3])). % 62.16/62.32 cnf(1155,plain, % 62.16/62.32 (E(f3(f3(x11551,f8(x11552)),f8(x11553)),f3(f3(x11551,f8(f1(f1(x11552)))),f8(f1(x11553))))), % 62.16/62.32 inference(scs_inference,[],[1151,2])). % 62.16/62.32 cnf(1156,plain, % 62.16/62.32 (E(f5(f8(x11561),f8(f1(f1(f1(x11562)))),f8(x11563)),f5(f8(f1(f1(f1(x11561)))),f8(x11562),f8(f1(x11563))))), % 62.16/62.32 inference(scs_inference,[],[1151,1150,913,2,3])). % 62.16/62.32 cnf(1160,plain, % 62.16/62.32 (E(f5(f8(f1(f1(f1(x11601)))),f8(x11602),f8(f1(x11603))),f5(f8(x11601),f8(f1(f1(f1(x11602)))),f8(x11603)))), % 62.16/62.32 inference(scs_inference,[],[1156,2])). % 62.16/62.32 cnf(1161,plain, % 62.16/62.32 (E(f3(f3(x11611,f8(x11612)),f8(x11613)),f3(f3(x11611,f8(f1(f1(f1(x11612))))),f8(f1(x11613))))), % 62.16/62.32 inference(scs_inference,[],[105,1155,1156,2,3])). % 62.16/62.32 cnf(1165,plain, % 62.16/62.32 (E(f5(f8(f1(f1(f1(x11651)))),f8(f1(x11652)),f8(f1(x11653))),f5(f8(f1(x11651)),f8(x11652),f8(f1(x11653))))), % 62.16/62.32 inference(scs_inference,[],[1160,1161,792,2,3])). % 62.16/62.32 cnf(1169,plain, % 62.16/62.32 (E(f5(f8(f1(x11691)),f8(x11692),f8(f1(x11693))),f5(f8(f1(f1(f1(x11691)))),f8(f1(x11692)),f8(f1(x11693))))), % 62.16/62.32 inference(scs_inference,[],[1165,2])). % 62.16/62.32 cnf(1170,plain, % 62.16/62.32 (E(f5(f8(f1(f1(f1(x11701)))),f8(f1(x11702)),f8(f1(f1(x11703)))),f5(f8(f1(x11701)),f8(f1(x11702)),f8(x11703)))), % 62.16/62.32 inference(scs_inference,[],[1165,1041,2,3])). % 62.16/62.32 cnf(1174,plain, % 62.16/62.32 (E(f5(f8(f1(x11741)),f8(f1(x11742)),f8(x11743)),f5(f8(f1(f1(f1(x11741)))),f8(f1(x11742)),f8(f1(f1(x11743)))))), % 62.16/62.32 inference(scs_inference,[],[1170,2])). % 62.16/62.32 cnf(1175,plain, % 62.16/62.32 (E(f5(f8(f1(f1(f1(x11751)))),f8(f1(x11752)),f8(f1(f1(x11753)))),f5(f8(f1(x11751)),f8(x11752),f8(x11753)))), % 62.16/62.32 inference(scs_inference,[],[1170,576,2,3])). % 62.16/62.32 cnf(1178,plain, % 62.16/62.32 (E(f5(f8(f1(x11781)),f8(x11782),f8(x11783)),f5(f8(f1(f1(f1(x11781)))),f8(f1(x11782)),f8(f1(f1(x11783)))))), % 62.16/62.32 inference(scs_inference,[],[1175,2])). % 62.16/62.32 cnf(1179,plain, % 62.16/62.32 (E(f5(f8(f1(x11791)),f8(x11792),f8(f1(f1(x11793)))),f5(f8(f1(x11791)),f8(x11792),f8(x11793)))), % 62.16/62.32 inference(scs_inference,[],[1175,1169,2,3])). % 62.16/62.32 cnf(1183,plain, % 62.16/62.32 (E(f5(f8(f1(x11831)),f8(x11832),f8(x11833)),f5(f8(f1(x11831)),f8(x11832),f8(f1(f1(x11833)))))), % 62.16/62.32 inference(scs_inference,[],[1179,2])). % 62.16/62.32 cnf(1184,plain, % 62.16/62.32 (E(f5(f8(f1(x11841)),f8(f1(x11842)),f8(x11843)),f5(f8(f1(f1(f1(x11841)))),f8(f1(x11842)),f8(x11843)))), % 62.16/62.32 inference(scs_inference,[],[1179,1174,2,3])). % 62.16/62.32 cnf(1187,plain, % 62.16/62.32 (E(f5(f8(f1(f1(f1(x11871)))),f8(f1(x11872)),f8(x11873)),f5(f8(f1(x11871)),f8(f1(x11872)),f8(x11873)))), % 62.16/62.32 inference(scs_inference,[],[1184,2])). % 62.16/62.32 cnf(1188,plain, % 62.16/62.32 (E(f5(f8(f1(x11881)),f8(f1(x11882)),f8(x11883)),f5(f8(f1(x11881)),f8(f1(f1(f1(f1(x11882))))),f8(x11883)))), % 62.16/62.32 inference(scs_inference,[],[1184,887,2,3])). % 62.16/62.32 cnf(1191,plain, % 62.16/62.32 (E(f5(f8(f1(x11911)),f8(f1(f1(f1(f1(x11912))))),f8(x11913)),f5(f8(f1(x11911)),f8(f1(x11912)),f8(x11913)))), % 62.16/62.32 inference(scs_inference,[],[1188,2])). % 62.16/62.32 cnf(1192,plain, % 62.16/62.32 (E(f5(f8(f1(f1(f1(x11921)))),f8(f1(x11922)),f8(x11923)),f5(f8(f1(x11921)),f8(f1(x11922)),f8(f1(f1(x11923)))))), % 62.16/62.32 inference(scs_inference,[],[1187,1188,1183,2,3])). % 62.16/62.32 cnf(1195,plain, % 62.16/62.32 (E(f5(f8(f1(x11951)),f8(f1(x11952)),f8(f1(f1(x11953)))),f5(f8(f1(f1(f1(x11951)))),f8(f1(x11952)),f8(x11953)))), % 62.16/62.32 inference(scs_inference,[],[1192,2])). % 62.16/62.32 cnf(1196,plain, % 62.16/62.32 (E(f5(f8(f1(x11961)),f8(f1(f1(f1(f1(x11962))))),f8(x11963)),f5(f8(x11961),f8(x11962),f8(x11963)))), % 62.16/62.32 inference(scs_inference,[],[1191,1192,665,2,3])). % 62.16/62.32 cnf(1199,plain, % 62.16/62.32 (E(f5(f8(x11991),f8(x11992),f8(x11993)),f5(f8(f1(x11991)),f8(f1(f1(f1(f1(x11992))))),f8(x11993)))), % 62.16/62.32 inference(scs_inference,[],[1196,2])). % 62.16/62.32 cnf(1200,plain, % 62.16/62.32 (E(f5(f8(f1(f1(x12001))),f8(f1(x12002)),f8(f1(f1(f1(x12003))))),f5(f8(f1(x12001)),f8(x12002),f8(x12003)))), % 62.16/62.32 inference(scs_inference,[],[1195,1196,1074,2,3])). % 62.16/62.32 cnf(1205,plain, % 62.16/62.32 (E(f5(f8(x12051),f8(x12052),f8(x12053)),f5(f8(f1(x12051)),f8(f1(f1(x12052))),f8(f1(f1(f1(x12053))))))), % 62.16/62.32 inference(scs_inference,[],[1199,1200,703,2,3])). % 62.16/62.32 cnf(1208,plain, % 62.16/62.32 (E(f5(f8(f1(x12081)),f8(f1(f1(x12082))),f8(f1(f1(f1(x12083))))),f5(f8(x12081),f8(x12082),f8(x12083)))), % 62.16/62.32 inference(scs_inference,[],[1205,2])). % 62.16/62.32 cnf(1209,plain, % 62.16/62.32 (E(f5(f8(f1(x12091)),f8(f1(f1(x12092))),f8(x12093)),f5(f8(f1(x12091)),f8(x12092),f8(f1(x12093))))), % 62.16/62.32 inference(scs_inference,[],[1178,1205,859,2,3])). % 62.16/62.32 cnf(1213,plain, % 62.16/62.32 (E(f5(f8(f1(x12131)),f8(x12132),f8(f1(x12133))),f5(f8(f1(x12131)),f8(f1(f1(x12132))),f8(x12133)))), % 62.16/62.32 inference(scs_inference,[],[1209,2])). % 62.16/62.32 cnf(1214,plain, % 62.16/62.32 (E(f5(f8(f1(x12141)),f8(f1(f1(x12142))),f8(f1(f1(f1(x12143))))),f5(f8(f1(x12141)),f8(x12142),f8(x12143)))), % 62.16/62.32 inference(scs_inference,[],[1208,1209,446,2,3])). % 62.16/62.32 cnf(1218,plain, % 62.16/62.32 (E(f5(f8(f1(x12181)),f8(f1(x12182)),f8(f1(x12183))),f5(f8(f1(f1(f1(x12181)))),f8(x12182),f8(x12183)))), % 62.16/62.32 inference(scs_inference,[],[1213,1214,890,2,3])). % 62.16/62.32 cnf(1221,plain, % 62.16/62.32 (E(f5(f8(f1(f1(f1(x12211)))),f8(x12212),f8(x12213)),f5(f8(f1(x12211)),f8(f1(x12212)),f8(f1(x12213))))), % 62.16/62.32 inference(scs_inference,[],[1218,2])). % 62.16/62.32 cnf(1222,plain, % 62.16/62.32 (E(f5(f8(x12221),f8(f1(f1(x12222))),f8(x12223)),f5(f8(f1(f1(f1(x12221)))),f8(x12222),f8(f1(f1(x12223)))))), % 62.16/62.32 inference(scs_inference,[],[1218,707,2,3])). % 62.16/62.32 cnf(1226,plain, % 62.16/62.32 (E(f5(f8(f1(f1(f1(x12261)))),f8(x12262),f8(f1(f1(x12263)))),f5(f8(x12261),f8(f1(f1(x12262))),f8(x12263)))), % 62.16/62.32 inference(scs_inference,[],[1222,2])). % 62.16/62.32 cnf(1227,plain, % 62.16/62.32 (E(f5(f8(f1(f1(f1(x12271)))),f8(x12272),f8(f1(f1(x12273)))),f5(f8(f1(x12271)),f8(x12272),f8(x12273)))), % 62.16/62.32 inference(scs_inference,[],[1221,1222,899,2,3])). % 62.16/62.32 cnf(1231,plain, % 62.16/62.32 (E(f5(f8(f1(x12311)),f8(x12312),f8(x12313)),f5(f8(f1(f1(f1(x12311)))),f8(x12312),f8(f1(f1(x12313)))))), % 62.16/62.32 inference(scs_inference,[],[1227,2])). % 62.16/62.32 cnf(1232,plain, % 62.16/62.32 (E(f5(f8(f1(f1(f1(x12321)))),f8(x12322),f8(f1(f1(x12323)))),f5(f8(f1(f1(x12321))),f8(x12322),f8(x12323)))), % 62.16/62.32 inference(scs_inference,[],[1226,1227,936,2,3])). % 62.16/62.32 cnf(1235,plain, % 62.16/62.32 (E(f5(f8(f1(f1(x12351))),f8(x12352),f8(x12353)),f5(f8(f1(f1(f1(x12351)))),f8(x12352),f8(f1(f1(x12353)))))), % 62.16/62.32 inference(scs_inference,[],[1232,2])). % 62.16/62.32 cnf(1236,plain, % 62.16/62.32 (E(f5(f8(f1(f1(f1(x12361)))),f8(f1(x12362)),f8(f1(f1(x12363)))),f5(f8(x12361),f8(x12362),f8(f1(x12363))))), % 62.16/62.32 inference(scs_inference,[],[1232,698,2,3])). % 62.16/62.32 cnf(1240,plain, % 62.16/62.32 (E(f5(f8(x12401),f8(x12402),f8(f1(x12403))),f5(f8(f1(f1(f1(x12401)))),f8(f1(x12402)),f8(f1(f1(x12403)))))), % 62.16/62.32 inference(scs_inference,[],[1236,2])). % 62.16/62.32 cnf(1241,plain, % 62.16/62.32 (E(f5(f8(f1(x12411)),f8(f1(x12412)),f8(x12413)),f5(f8(x12411),f8(x12412),f8(f1(x12413))))), % 62.16/62.32 inference(scs_inference,[],[1236,1231,2,3])). % 62.16/62.32 cnf(1245,plain, % 62.16/62.32 (E(f5(f8(x12451),f8(x12452),f8(f1(x12453))),f5(f8(f1(x12451)),f8(f1(x12452)),f8(x12453)))), % 62.16/62.32 inference(scs_inference,[],[1241,2])). % 62.16/62.32 cnf(1246,plain, % 62.16/62.32 (E(f5(f8(f1(f1(x12461))),f8(f1(x12462)),f8(x12463)),f5(f8(x12461),f8(f1(f1(f1(f1(x12462))))),f8(x12463)))), % 62.16/62.32 inference(scs_inference,[],[1241,796,2,3])). % 62.16/62.32 cnf(1250,plain, % 62.16/62.32 (E(f5(f8(x12501),f8(f1(f1(f1(f1(x12502))))),f8(x12503)),f5(f8(f1(f1(x12501))),f8(f1(x12502)),f8(x12503)))), % 62.16/62.32 inference(scs_inference,[],[1246,2])). % 62.16/62.32 cnf(1251,plain, % 62.16/62.32 (E(f5(f8(x12511),f8(x12512),f8(f1(f1(x12513)))),f5(f8(f1(f1(f1(x12511)))),f8(f1(x12512)),f8(x12513)))), % 62.16/62.32 inference(scs_inference,[],[1245,1246,886,2,3])). % 62.16/62.32 cnf(1255,plain, % 62.16/62.32 (E(f5(f8(f1(f1(f1(x12551)))),f8(f1(x12552)),f8(x12553)),f5(f8(x12551),f8(x12552),f8(f1(f1(x12553)))))), % 62.16/62.32 inference(scs_inference,[],[1251,2])). % 62.16/62.32 cnf(1256,plain, % 62.16/62.32 (E(f5(f8(x12561),f8(f1(f1(f1(f1(x12562))))),f8(f1(x12563))),f5(f8(f1(x12561)),f8(x12562),f8(x12563)))), % 62.16/62.32 inference(scs_inference,[],[1250,1251,502,2,3])). % 62.16/62.32 cnf(1260,plain, % 62.16/62.32 (E(f5(f8(f1(x12601)),f8(x12602),f8(x12603)),f5(f8(x12601),f8(f1(f1(f1(f1(x12602))))),f8(f1(x12603))))), % 62.16/62.32 inference(scs_inference,[],[1256,2])). % 62.16/62.32 cnf(1261,plain, % 62.16/62.32 (E(f5(f8(x12611),f8(f1(f1(f1(f1(x12612))))),f8(f1(x12613))),f5(f8(f1(x12611)),f8(f1(x12612)),f8(x12613)))), % 62.16/62.32 inference(scs_inference,[],[1256,451,2,3])). % 62.16/62.32 cnf(1264,plain, % 62.16/62.32 (E(f5(f8(f1(x12641)),f8(f1(x12642)),f8(x12643)),f5(f8(x12641),f8(f1(f1(f1(f1(x12642))))),f8(f1(x12643))))), % 62.16/62.32 inference(scs_inference,[],[1261,2])). % 62.16/62.32 cnf(1265,plain, % 62.16/62.32 (E(f5(f8(x12651),f8(f1(f1(f1(f1(x12652))))),f8(f1(x12653))),f5(f8(x12651),f8(x12652),f8(f1(x12653))))), % 62.16/62.32 inference(scs_inference,[],[1261,1241,2,3])). % 62.16/62.32 cnf(1268,plain, % 62.16/62.32 (E(f5(f8(x12681),f8(x12682),f8(f1(x12683))),f5(f8(x12681),f8(f1(f1(f1(f1(x12682))))),f8(f1(x12683))))), % 62.16/62.32 inference(scs_inference,[],[1265,2])). % 62.16/62.32 cnf(1269,plain, % 62.16/62.32 (E(f5(f8(f1(x12691)),f8(x12692),f8(f1(x12693))),f5(f8(f1(f1(f1(x12691)))),f8(f1(f1(x12692))),f8(x12693)))), % 62.16/62.32 inference(scs_inference,[],[1260,1265,814,2,3])). % 62.16/62.32 cnf(1273,plain, % 62.16/62.32 (E(f5(f8(f1(f1(f1(x12731)))),f8(f1(f1(x12732))),f8(x12733)),f5(f8(f1(x12731)),f8(x12732),f8(f1(x12733))))), % 62.16/62.32 inference(scs_inference,[],[1269,2])). % 62.16/62.32 cnf(1274,plain, % 62.16/62.32 (E(f5(f8(f1(x12741)),f8(x12742),f8(f1(x12743))),f5(f8(x12741),f8(f1(x12742)),f8(f1(f1(x12743)))))), % 62.16/62.32 inference(scs_inference,[],[1269,1255,2,3])). % 62.16/62.32 cnf(1277,plain, % 62.16/62.32 (E(f5(f8(x12771),f8(f1(x12772)),f8(f1(f1(x12773)))),f5(f8(f1(x12771)),f8(x12772),f8(f1(x12773))))), % 62.16/62.32 inference(scs_inference,[],[1274,2])). % 62.16/62.32 cnf(1278,plain, % 62.16/62.32 (E(f5(f8(f1(x12781)),f8(f1(x12782)),f8(x12783)),f5(f8(f1(f1(x12781))),f8(f1(f1(f1(x12782)))),f8(x12783)))), % 62.16/62.32 inference(scs_inference,[],[1264,1274,950,2,3])). % 62.16/62.32 cnf(1281,plain, % 62.16/62.32 (E(f5(f8(f1(f1(x12811))),f8(f1(f1(f1(x12812)))),f8(x12813)),f5(f8(f1(x12811)),f8(f1(x12812)),f8(x12813)))), % 62.16/62.32 inference(scs_inference,[],[1278,2])). % 62.16/62.32 cnf(1282,plain, % 62.16/62.32 (E(f5(f8(f1(x12821)),f8(f1(x12822)),f8(f1(f1(x12823)))),f5(f8(f1(f1(x12821))),f8(x12822),f8(x12823)))), % 62.16/62.32 inference(scs_inference,[],[1278,1030,2,3])). % 62.16/62.32 cnf(1286,plain, % 62.16/62.32 (E(f5(f8(f1(f1(x12861))),f8(x12862),f8(x12863)),f5(f8(f1(x12861)),f8(f1(x12862)),f8(f1(f1(x12863)))))), % 62.16/62.32 inference(scs_inference,[],[1282,2])). % 62.16/62.32 cnf(1287,plain, % 62.16/62.32 (E(f5(f8(f1(f1(x12871))),f8(f1(f1(f1(x12872)))),f8(f1(x12873))),f5(f8(f1(x12871)),f8(f1(x12872)),f8(x12873)))), % 62.16/62.32 inference(scs_inference,[],[1281,1282,642,2,3])). % 62.16/62.32 cnf(1291,plain, % 62.16/62.32 (E(f5(f8(f1(x12911)),f8(f1(x12912)),f8(x12913)),f5(f8(f1(f1(x12911))),f8(f1(f1(f1(x12912)))),f8(f1(x12913))))), % 62.16/62.32 inference(scs_inference,[],[1287,2])). % 62.16/62.32 cnf(1292,plain, % 62.16/62.32 (E(f11(f8(f1(f1(f1(f1(x12921))))),f8(x12922)),f11(f8(x12921),f8(f1(x12922))))), % 62.16/62.32 inference(scs_inference,[],[1121,1287,429,2,3])). % 62.16/62.32 cnf(1295,plain, % 62.16/62.32 (E(f11(f8(x12951),f8(f1(x12952))),f11(f8(f1(f1(f1(f1(x12951))))),f8(x12952)))), % 62.16/62.32 inference(scs_inference,[],[1292,2])). % 62.16/62.32 cnf(1296,plain, % 62.16/62.32 (E(f5(f8(x12961),f8(x12962),f8(f1(f1(x12963)))),f5(f8(f1(x12961)),f8(f1(f1(f1(x12962)))),f8(f1(x12963))))), % 62.16/62.32 inference(scs_inference,[],[1268,1277,1292,2,3])). % 62.16/62.32 cnf(1300,plain, % 62.16/62.32 (E(f5(f8(f1(x13001)),f8(f1(f1(f1(x13002)))),f8(f1(x13003))),f5(f8(x13001),f8(x13002),f8(f1(f1(x13003)))))), % 62.16/62.32 inference(scs_inference,[],[1296,2])). % 62.16/62.32 cnf(1301,plain, % 62.16/62.32 (E(f5(f8(f1(f1(x13011))),f8(f1(x13012)),f8(x13013)),f5(f8(f1(x13011)),f8(f1(x13012)),f8(f1(f1(x13013)))))), % 62.16/62.32 inference(scs_inference,[],[1273,1291,1296,2,3])). % 62.16/62.32 cnf(1305,plain, % 62.16/62.32 (E(f5(f8(f1(x13051)),f8(f1(x13052)),f8(f1(f1(x13053)))),f5(f8(f1(f1(x13051))),f8(f1(x13052)),f8(x13053)))), % 62.16/62.32 inference(scs_inference,[],[1301,2])). % 62.16/62.32 cnf(1306,plain, % 62.16/62.32 (E(f5(f8(f1(f1(f1(x13061)))),f8(f1(x13062)),f8(x13063)),f5(f8(x13061),f8(x13062),f8(f1(x13063))))), % 62.16/62.32 inference(scs_inference,[],[1235,1301,1147,2,3])). % 62.16/62.32 cnf(1310,plain, % 62.16/62.32 (E(f5(f8(x13101),f8(x13102),f8(f1(x13103))),f5(f8(f1(f1(f1(x13101)))),f8(f1(x13102)),f8(x13103)))), % 62.16/62.32 inference(scs_inference,[],[1306,2])). % 62.16/62.32 cnf(1311,plain, % 62.16/62.32 (E(f5(f8(f1(f1(x13111))),f8(f1(x13112)),f8(f1(f1(x13113)))),f5(f8(x13111),f8(x13112),f8(f1(x13113))))), % 62.16/62.32 inference(scs_inference,[],[1305,1306,2,3])). % 62.16/62.32 cnf(1315,plain, % 62.16/62.32 (E(f5(f8(x13151),f8(x13152),f8(f1(x13153))),f5(f8(f1(f1(x13151))),f8(f1(x13152)),f8(f1(f1(x13153)))))), % 62.16/62.32 inference(scs_inference,[],[1311,2])). % 62.16/62.32 cnf(1316,plain, % 62.16/62.32 (E(f5(f8(x13161),f8(x13162),f8(f1(f1(f1(x13163))))),f5(f8(f1(x13161)),f8(x13162),f8(f1(x13163))))), % 62.16/62.32 inference(scs_inference,[],[1310,1311,2,3])). % 62.16/62.32 cnf(1321,plain, % 62.16/62.32 (E(f5(f8(x13211),f8(x13212),f8(f1(f1(f1(x13213))))),f5(f8(f1(x13211)),f8(f1(f1(x13212))),f8(x13213)))), % 62.16/62.32 inference(scs_inference,[],[1316,1213,2,3])). % 62.16/62.32 cnf(1324,plain, % 62.16/62.32 (E(f5(f8(x13241),f8(f1(f1(x13242))),f8(f1(f1(f1(x13243))))),f5(f8(f1(x13241)),f8(f1(x13242)),f8(x13243)))), % 62.16/62.32 inference(scs_inference,[],[1321,1191,2,3])). % 62.16/62.32 cnf(1329,plain, % 62.16/62.32 (E(f11(f8(x13291),f8(f1(f1(f1(x13292))))),f11(f8(f1(f1(x13291))),f8(x13292)))), % 62.16/62.32 inference(scs_inference,[],[1295,1324,1066,2,3])). % 62.16/62.32 cnf(1334,plain, % 62.16/62.32 (E(f5(f8(x13341),f8(x13342),f8(f1(x13343))),f5(f8(f1(f1(x13341))),f8(f1(f1(f1(x13342)))),f8(f1(x13343))))), % 62.16/62.32 inference(scs_inference,[],[1329,1240,937,2,3])). % 62.16/62.32 cnf(1337,plain, % 62.16/62.32 (E(f5(f8(f1(f1(x13371))),f8(f1(f1(f1(x13372)))),f8(f1(x13373))),f5(f8(x13371),f8(x13372),f8(f1(x13373))))), % 62.16/62.32 inference(scs_inference,[],[1334,2])). % 62.16/62.32 cnf(1338,plain, % 62.16/62.32 (E(f5(f8(x13381),f8(x13382),f8(f1(x13383))),f5(f8(f1(x13381)),f8(x13382),f8(f1(f1(x13383)))))), % 62.16/62.32 inference(scs_inference,[],[1334,1300,2,3])). % 62.16/62.32 cnf(1341,plain, % 62.16/62.32 (E(f5(f8(f1(x13411)),f8(x13412),f8(f1(f1(x13413)))),f5(f8(x13411),f8(x13412),f8(f1(x13413))))), % 62.16/62.32 inference(scs_inference,[],[1338,2])). % 62.16/62.32 cnf(1342,plain, % 62.16/62.32 (E(f5(f8(f1(f1(f1(x13421)))),f8(f1(f1(x13422))),f8(x13423)),f5(f8(x13421),f8(x13422),f8(f1(f1(x13423)))))), % 62.16/62.32 inference(scs_inference,[],[1337,1286,1338,2,3])). % 62.16/62.32 cnf(1346,plain, % 62.16/62.32 (E(f5(f8(x13461),f8(x13462),f8(f1(f1(x13463)))),f5(f8(f1(f1(f1(x13461)))),f8(f1(f1(x13462))),f8(x13463)))), % 62.16/62.32 inference(scs_inference,[],[1342,2])). % 62.16/62.32 cnf(1347,plain, % 62.16/62.32 (E(f5(f8(f1(f1(x13471))),f8(x13472),f8(f1(f1(x13473)))),f5(f8(f1(f1(x13471))),f8(f1(f1(x13472))),f8(x13473)))), % 62.16/62.32 inference(scs_inference,[],[1341,1342,945,2,3])). % 62.16/62.32 cnf(1352,plain, % 62.16/62.32 (E(f5(f8(x13521),f8(x13522),f8(f1(f1(x13523)))),f5(f8(f1(x13521)),f8(f1(f1(x13522))),f8(x13523)))), % 62.16/62.32 inference(scs_inference,[],[1346,1347,1187,2,3])). % 62.16/62.32 cnf(1356,plain, % 62.16/62.32 (E(f5(f8(x13561),f8(x13562),f8(f1(x13563))),f5(f8(f1(f1(f1(x13561)))),f8(f1(f1(f1(x13562)))),f8(x13563)))), % 62.16/62.32 inference(scs_inference,[],[1352,1315,2,3])). % 62.16/62.32 cnf(1359,plain, % 62.16/62.32 (E(f5(f8(f1(f1(f1(x13591)))),f8(f1(f1(f1(x13592)))),f8(x13593)),f5(f8(x13591),f8(x13592),f8(f1(x13593))))), % 62.16/62.32 inference(scs_inference,[],[1356,2])). % 62.16/62.32 cnf(1360,plain, % 62.16/62.32 (E(f5(f8(x13601),f8(f1(x13602)),f8(f1(x13603))),f5(f8(f1(f1(f1(f1(x13601))))),f8(x13602),f8(x13603)))), % 62.16/62.32 inference(scs_inference,[],[1356,1046,2,3])). % 62.16/62.32 cnf(1365,plain, % 62.16/62.32 (E(f5(f8(x13651),f8(f1(x13652)),f8(f1(f1(f1(x13653))))),f5(f8(f1(x13651)),f8(f1(f1(x13652))),f8(x13653)))), % 62.16/62.32 inference(scs_inference,[],[1360,1226,2,3])). % 62.16/62.32 cnf(1370,plain, % 62.16/62.32 (E(f5(f8(f1(x13701)),f8(f1(x13702)),f8(f1(f1(f1(x13703))))),f5(f8(f1(x13701)),f8(x13702),f8(f1(x13703))))), % 62.16/62.32 inference(scs_inference,[],[1365,942,2,3])). % 62.16/62.32 cnf(1375,plain, % 62.16/62.32 (E(f5(f8(f1(f1(f1(x13751)))),f8(f1(f1(f1(x13752)))),f8(x13753)),f5(f8(f1(x13751)),f8(f1(x13752)),f8(x13753)))), % 62.16/62.32 inference(scs_inference,[],[1359,1370,1245,2,3])). % 62.16/62.32 cnf(1379,plain, % 62.16/62.32 (E(f11(f8(f1(f1(x13791))),f8(x13792)),f11(f8(x13791),f8(f1(x13792))))), % 62.16/62.32 inference(scs_inference,[],[1375,1126,765,2,3])). % 62.16/62.32 cnf(1383,plain, % 62.16/62.32 (E(f11(f8(x13831),f8(f1(x13832))),f11(f8(f1(f1(x13831))),f8(x13832)))), % 62.16/62.32 inference(scs_inference,[],[1379,2])). % 62.16/62.32 cnf(1422,plain, % 62.16/62.32 (E(f6(f8(f1(x14221)),f8(f1(x14222))),f6(f8(x14221),f8(x14222)))), % 62.16/62.32 inference(scs_inference,[],[487,2])). % 62.16/62.32 cnf(1442,plain, % 62.16/62.32 (E(f1(f9(f8(f1(x14421)))),f1(f9(f8(x14421))))), % 62.16/62.32 inference(scs_inference,[],[447,4])). % 62.16/62.32 cnf(1448,plain, % 62.16/62.32 (P1(f11(f9(a22),f12(f15(a22),f11(f9(a20),f11(f10(a24),f10(a23))))),f8(f8(f1(f1(f6(a7,a13))))),a21)), % 62.16/62.32 inference(scs_inference,[],[447,125,4,5,8,9,10,14,31])). % 62.16/62.32 cnf(1450,plain, % 62.16/62.32 (E(f11(f9(f8(f1(x14501))),x14502),f11(f9(f8(x14501)),x14502))), % 62.16/62.32 inference(scs_inference,[],[447,125,4,5,8,9,10,14,31,6])). % 62.16/62.32 cnf(1451,plain, % 62.16/62.32 (E(f11(x14511,f9(f8(f1(x14512)))),f11(x14511,f9(f8(x14512))))), % 62.16/62.32 inference(scs_inference,[],[447,125,4,5,8,9,10,14,31,6,7])). % 62.16/62.32 cnf(1457,plain, % 62.16/62.32 (E(f12(x14571,f9(f8(f1(x14572)))),f12(x14571,f9(f8(x14572))))), % 62.16/62.32 inference(scs_inference,[],[447,125,4,5,8,9,10,14,31,6,7,15,16,17,18,19,20])). % 62.16/62.32 cnf(1469,plain, % 62.16/62.32 (P1(f11(f9(a18),f12(f15(a18),f11(f9(a19),f11(f10(a23),f10(a25))))),f1(f6(a7,a13)),a21)), % 62.16/62.32 inference(scs_inference,[],[28,447,39,125,524,29,27,4,5,8,9,10,14,31,6,7,15,16,17,18,19,20,21,11,12,13,32,34,208,22,2,33])). % 62.16/62.32 cnf(1480,plain, % 62.16/62.32 (P1(f11(f9(a18),f12(f15(a18),f11(f9(a19),f11(f10(a23),f10(a25))))),f8(f1(f6(a7,a13))),a21)), % 62.16/62.32 inference(scs_inference,[],[1469,31])). % 62.16/62.32 cnf(1487,plain, % 62.16/62.32 (P1(f12(f15(a22),f11(f9(a20),f11(f10(a24),f10(a23)))),f8(f8(f1(f1(f6(a7,a13))))),a21)), % 62.16/62.32 inference(scs_inference,[],[452,481,1469,1448,31,17,9,5,14,7,32])). % 62.16/62.32 cnf(1499,plain, % 62.16/62.32 (E(f12(f6(f6(x14991,f8(x14992)),x14993),f9(f8(f1(x14994)))),f12(f6(f6(x14991,f8(f1(x14992))),x14993),f9(f8(x14994))))), % 62.16/62.32 inference(scs_inference,[],[452,481,1457,1469,1448,31,17,9,5,14,7,32,15,20,21,18,11,12,4,8,6,13,208])). % 62.16/62.32 cnf(1516,plain, % 62.16/62.32 (P1(f12(f15(a18),f11(f9(a19),f11(f10(a23),f10(a25)))),f8(f1(f6(a7,a13))),a21)), % 62.16/62.32 inference(scs_inference,[],[1480,31,32])). % 62.16/62.32 cnf(1521,plain, % 62.16/62.32 (E(f12(x15211,f6(f8(f1(x15212)),x15213)),f12(x15211,f6(f8(x15212),x15213)))), % 62.16/62.32 inference(scs_inference,[],[953,1480,31,32,17,5,7,20])). % 62.16/62.32 cnf(1550,plain, % 62.16/62.32 (P1(f12(f15(a22),f11(f9(a20),f11(f10(a24),f10(a23)))),f8(f6(a7,a13)),a21)), % 62.16/62.32 inference(scs_inference,[],[1516,74,31,32])). % 62.16/62.32 cnf(1569,plain, % 62.16/62.32 (E(f12(f6(f6(x15691,f8(x15692)),x15693),f6(f8(f1(x15694)),x15695)),f12(f6(f6(x15691,f8(f1(x15692))),x15693),f6(f8(x15694),x15695)))), % 62.16/62.32 inference(scs_inference,[],[1422,1521,1516,74,31,32,5,7,8,20,21,17,14,11,19,9,6,13,10,16,15,18,12,208])). % 62.16/62.32 cnf(1582,plain, % 62.16/62.32 (P1(f12(f15(a22),f11(f9(a20),f11(f10(a24),f10(a23)))),f8(f8(f6(a7,a13))),a21)), % 62.16/62.32 inference(scs_inference,[],[1550,31])). % 62.16/62.32 cnf(1638,plain, % 62.16/62.32 (~P1(f12(f15(x16381),f11(f9(x16382),f11(f10(a23),x16383))),f8(f6(a7,a13)),a21)), % 62.16/62.32 inference(scs_inference,[],[1383,1450,1451,1582,1499,1550,30,27,31,8,11,20,21,7,17,14,9,5,6,19,12,10,208,15,18,4,16,13,22,3,35])). % 62.16/62.32 cnf(1698,plain, % 62.16/62.32 ($false), % 62.16/62.32 inference(scs_inference,[],[1638,1442,1487,1569,1516,26,31,8,19,12,9,7,17,20,11,5,6,10,14,21,16,208,13,4,15,18,22,24]), % 62.16/62.32 ['proof']). % 62.16/62.32 % SZS output end Proof % 62.16/62.32 % Total time :61.560000s %------------------------------------------------------------------------------