%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SWV363-2 : TPTP v8.2.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/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:59 EDT 2024 % Result : Unsatisfiable 59.43s 59.55s % Output : CNFRefutation 59.52s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWV363-2 : TPTP v8.2.0. Released v3.2.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox/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 15:27:23 EDT 2024 % 0.12/0.34 % CPUTime : % 0.46/0.57 start to proof:theBenchmark % 59.43/59.54 %------------------------------------------- % 59.43/59.54 % File :CSE---1.7 % 59.43/59.54 % Problem :theBenchmark % 59.43/59.54 % Transform :cnf % 59.43/59.54 % Format :tptp:raw % 59.43/59.54 % Command :java -jar mcs_scs.jar %d %s % 59.43/59.54 % 59.43/59.54 % Result :Theorem 58.910000s % 59.43/59.54 % Output :CNFRefutation 58.910000s % 59.43/59.54 %------------------------------------------- % 59.43/59.55 %------------------------------------------------------------------------------ % 59.43/59.55 % File : SWV363-2 : TPTP v8.2.0. Released v3.2.0. % 59.43/59.55 % Domain : Software Verification (Security) % 59.43/59.55 % Problem : Cryptographic protocol problem for Yahalom % 59.43/59.55 % Version : [Pau06] axioms : Reduced > Especial. % 59.43/59.55 % English : % 59.43/59.55 % 59.43/59.55 % Refs : [Pau06] Paulson (2006), Email to G. Sutcliffe % 59.43/59.55 % Source : [Pau06] % 59.43/59.55 % Names : % 59.43/59.55 % 59.43/59.55 % Status : Unsatisfiable % 59.43/59.55 % 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 % 59.43/59.55 % Syntax : Number of clauses : 10 ( 5 unt; 0 nHn; 9 RR) % 59.43/59.55 % Number of literals : 18 ( 1 equ; 9 neg) % 59.43/59.55 % Maximal clause size : 4 ( 1 avg) % 59.43/59.55 % Maximal term depth : 7 ( 2 avg) % 59.43/59.55 % Number of predicates : 2 ( 1 usr; 0 prp; 2-3 aty) % 59.43/59.55 % Number of functors : 25 ( 25 usr; 13 con; 0-3 aty) % 59.43/59.55 % Number of variables : 21 ( 10 sgn) % 59.43/59.55 % SPC : CNF_UNS_RFO_SEQ_HRN % 59.43/59.55 % 59.43/59.55 % Comments : The problems in the [Pau06] collection each have very many axioms, % 59.43/59.55 % of which only a small selection are required for the refutation. % 59.43/59.55 % The mission is to find those few axioms, after which a refutation % 59.43/59.55 % can be quite easily found. This version has only the necessary % 59.43/59.55 % axioms. % 59.43/59.55 %------------------------------------------------------------------------------ % 59.43/59.55 cnf(cls_Event_OSays__imp__spies_0,axiom, % 59.43/59.55 ( ~ c_in(c_Event_Oevent_OSays(V_A,V_B,V_X),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent) % 59.43/59.55 | c_in(V_X,c_Event_Oknows(c_Message_Oagent_OSpy,V_evs),tc_Message_Omsg) ) ). % 59.43/59.55 % 59.43/59.55 cnf(cls_Message_OMPair__parts_0,axiom, % 59.43/59.55 ( ~ c_in(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Oparts(V_H),tc_Message_Omsg) % 59.43/59.55 | c_in(V_Y,c_Message_Oparts(V_H),tc_Message_Omsg) ) ). % 59.43/59.55 % 59.43/59.55 cnf(cls_Message_Oparts_OInj_0,axiom, % 59.43/59.55 ( ~ c_in(V_X,V_H,tc_Message_Omsg) % 59.43/59.55 | c_in(V_X,c_Message_Oparts(V_H),tc_Message_Omsg) ) ). % 59.43/59.55 % 59.43/59.55 cnf(cls_Message_Oparts__analz_0,axiom, % 59.43/59.55 c_Message_Oparts(c_Message_Oanalz(V_H)) = c_Message_Oparts(V_H) ). % 59.43/59.55 % 59.43/59.55 cnf(cls_Yahalom_OGets__imp__analz__Spy__dest_0,axiom, % 59.43/59.55 ( ~ c_in(V_evs,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)) % 59.43/59.55 | ~ c_in(c_Event_Oevent_OGets(V_B,V_X),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent) % 59.43/59.55 | c_in(V_X,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg) ) ). % 59.43/59.55 % 59.43/59.55 cnf(cls_Yahalom_Ono__nonce__YM1__YM2_0,axiom, % 59.43/59.55 ( ~ c_in(V_evs,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)) % 59.43/59.55 | ~ 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) % 59.43/59.55 | ~ 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) % 59.43/59.55 | c_in(c_Message_Omsg_ONonce(V_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg) ) ). % 59.43/59.55 % 59.43/59.55 cnf(cls_conjecture_2,negated_conjecture, % 59.43/59.55 c_in(v_evs3,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)) ). % 59.43/59.55 % 59.43/59.55 cnf(cls_conjecture_5,negated_conjecture, % 59.43/59.55 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) ). % 59.43/59.55 % 59.43/59.55 cnf(cls_conjecture_7,negated_conjecture, % 59.43/59.55 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) ). % 59.43/59.55 % 59.43/59.55 cnf(cls_conjecture_8,negated_conjecture, % 59.43/59.55 ~ c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ). % 59.43/59.55 % 59.43/59.55 %------------------------------------------------------------------------------ % 59.43/59.55 %------------------------------------------- % 59.43/59.55 % Proof found % 59.43/59.55 % SZS status Theorem for theBenchmark % 59.43/59.55 % SZS output start Proof % 59.50/59.55 %ClaNum:35(EqnAxiom:25) % 59.50/59.55 %VarNum:36(SingletonVarNum:21) % 59.50/59.55 %MaxLitNum:4 % 59.50/59.55 %MaxfuncDepth:6 % 59.50/59.55 %SharedTerms:40 % 59.50/59.55 %goalClause: 27 28 29 30 % 59.50/59.55 %singleGoalClaCount:4 % 59.50/59.55 [27]P1(a13,a14,f17(a16)) % 59.50/59.55 [30]~P1(f10(a23),f1(f6(a7,a13)),a21) % 59.50/59.55 [28]P1(f3(a2,f11(f9(a18),f12(f15(a18),f11(f9(a19),f11(f10(a23),f10(a25)))))),f4(a13,a16),a16) % 59.50/59.55 [29]P1(f5(a22,a2,f11(f9(a22),f12(f15(a22),f11(f9(a20),f11(f10(a24),f10(a23)))))),f4(a13,a16),a16) % 59.50/59.55 [26]E(f8(f1(x261)),f8(x261)) % 59.50/59.55 [31]~P1(x311,x312,a21)+P1(x311,f8(x312),a21) % 59.50/59.55 [32]P1(x321,f8(x322),a21)+~P1(f11(x323,x321),f8(x322),a21) % 59.50/59.55 [34]P1(x341,f6(a7,x342),a21)+~P1(f5(x343,x344,x341),f4(x342,a16),a16) % 59.50/59.55 [33]~P1(f3(x333,x331),f4(x332,a16),a16)+~P1(x332,a14,f17(a16))+P1(x331,f1(f6(a7,x332)),a21) % 59.50/59.55 [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) % 59.50/59.55 %EqnAxiom % 59.50/59.55 [1]E(x11,x11) % 59.50/59.55 [2]E(x22,x21)+~E(x21,x22) % 59.50/59.55 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 59.50/59.55 [4]~E(x41,x42)+E(f1(x41),f1(x42)) % 59.50/59.55 [5]~E(x51,x52)+E(f8(x51),f8(x52)) % 59.50/59.55 [6]~E(x61,x62)+E(f11(x61,x63),f11(x62,x63)) % 59.50/59.55 [7]~E(x71,x72)+E(f11(x73,x71),f11(x73,x72)) % 59.50/59.55 [8]~E(x81,x82)+E(f17(x81),f17(x82)) % 59.50/59.55 [9]~E(x91,x92)+E(f9(x91),f9(x92)) % 59.50/59.55 [10]~E(x101,x102)+E(f15(x101),f15(x102)) % 59.50/59.55 [11]~E(x111,x112)+E(f5(x111,x113,x114),f5(x112,x113,x114)) % 59.50/59.55 [12]~E(x121,x122)+E(f5(x123,x121,x124),f5(x123,x122,x124)) % 59.50/59.55 [13]~E(x131,x132)+E(f5(x133,x134,x131),f5(x133,x134,x132)) % 59.50/59.55 [14]~E(x141,x142)+E(f10(x141),f10(x142)) % 59.50/59.55 [15]~E(x151,x152)+E(f4(x151,x153),f4(x152,x153)) % 59.50/59.55 [16]~E(x161,x162)+E(f4(x163,x161),f4(x163,x162)) % 59.50/59.55 [17]~E(x171,x172)+E(f6(x171,x173),f6(x172,x173)) % 59.50/59.55 [18]~E(x181,x182)+E(f6(x183,x181),f6(x183,x182)) % 59.50/59.55 [19]~E(x191,x192)+E(f12(x191,x193),f12(x192,x193)) % 59.50/59.55 [20]~E(x201,x202)+E(f12(x203,x201),f12(x203,x202)) % 59.50/59.55 [21]~E(x211,x212)+E(f3(x211,x213),f3(x212,x213)) % 59.50/59.55 [22]~E(x221,x222)+E(f3(x223,x221),f3(x223,x222)) % 59.50/59.55 [23]P1(x232,x233,x234)+~E(x231,x232)+~P1(x231,x233,x234) % 59.50/59.55 [24]P1(x243,x242,x244)+~E(x241,x242)+~P1(x243,x241,x244) % 59.50/59.56 [25]P1(x253,x254,x252)+~E(x251,x252)+~P1(x253,x254,x251) % 59.50/59.56 % 59.50/59.56 %------------------------------------------- % 59.50/59.56 cnf(36,plain, % 59.50/59.56 (E(f8(x361),f8(f1(x361)))), % 59.50/59.56 inference(scs_inference,[],[26,2])). % 59.50/59.56 cnf(66,plain, % 59.50/59.56 (E(f9(f15(f8(x661))),f9(f15(f8(f1(x661)))))), % 59.50/59.56 inference(scs_inference,[],[36,9,10])). % 59.50/59.56 cnf(70,plain, % 59.50/59.56 (E(f10(f5(f8(x701),x702,x703)),f10(f5(f8(f1(x701)),x702,x703)))), % 59.50/59.56 inference(scs_inference,[],[36,14,11])). % 59.50/59.56 cnf(74,plain, % 59.50/59.56 (P1(f11(f9(a22),f12(f15(a22),f11(f9(a20),f11(f10(a24),f10(a23))))),f8(f6(a7,a13)),a21)), % 59.50/59.56 inference(scs_inference,[],[29,31,34])). % 59.50/59.56 cnf(75,plain, % 59.50/59.56 (E(f9(f15(f8(f1(x751)))),f9(f15(f8(x751))))), % 59.50/59.57 inference(scs_inference,[],[66,2])). % 59.50/59.57 cnf(76,plain, % 59.50/59.57 (P1(f11(f9(a22),f12(f15(a22),f11(f9(a20),f11(f10(a24),f10(a23))))),f8(f1(f6(a7,a13))),a21)), % 59.50/59.57 inference(scs_inference,[],[36,66,74,2,24])). % 59.50/59.57 cnf(82,plain, % 59.50/59.57 (~E(f11(f9(a22),f12(f15(a22),f11(f9(a20),f11(f10(a24),f10(a23))))),f12(f15(x821),f11(f9(x822),f11(f10(a23),f10(a23)))))), % 59.50/59.57 inference(scs_inference,[],[27,30,36,66,70,74,2,24,23,35])). % 59.50/59.57 cnf(100,plain, % 59.50/59.57 (E(f4(x1001,f5(x1002,x1003,f8(f1(x1004)))),f4(x1001,f5(x1002,x1003,f8(x1004))))), % 59.50/59.57 inference(scs_inference,[],[26,16,13])). % 59.50/59.57 cnf(101,plain, % 59.50/59.57 (E(f4(x1011,f5(x1012,x1013,f8(x1014))),f4(x1011,f5(x1012,x1013,f8(f1(x1014)))))), % 59.50/59.57 inference(scs_inference,[],[100,2])). % 59.50/59.57 cnf(102,plain, % 59.50/59.57 (E(f6(f6(x1021,f8(f1(x1022))),x1023),f6(f6(x1021,f8(x1022)),x1023))), % 59.52/59.57 inference(scs_inference,[],[26,17,18])). % 59.52/59.57 cnf(103,plain, % 59.52/59.57 (E(f6(f6(x1031,f8(x1032)),x1033),f6(f6(x1031,f8(f1(x1032))),x1033))), % 59.52/59.57 inference(scs_inference,[],[102,2])). % 59.52/59.57 cnf(104,plain, % 59.52/59.57 (E(f12(f12(x1041,f8(f1(x1042))),x1043),f12(f12(x1041,f8(x1042)),x1043))), % 59.52/59.57 inference(scs_inference,[],[26,19,20])). % 59.52/59.57 cnf(105,plain, % 59.52/59.57 (E(f12(f12(x1051,f8(x1052)),x1053),f12(f12(x1051,f8(f1(x1052))),x1053))), % 59.52/59.57 inference(scs_inference,[],[104,2])). % 59.52/59.57 cnf(106,plain, % 59.52/59.57 (E(f3(f3(x1061,f8(f1(x1062))),x1063),f3(f3(x1061,f8(x1062)),x1063))), % 59.52/59.57 inference(scs_inference,[],[26,21,22])). % 59.52/59.57 cnf(107,plain, % 59.52/59.57 (E(f3(f3(x1071,f8(x1072)),x1073),f3(f3(x1071,f8(f1(x1072))),x1073))), % 59.52/59.57 inference(scs_inference,[],[106,2])). % 59.52/59.57 cnf(127,plain, % 59.52/59.57 (P1(f11(f9(a22),f12(f15(a22),f11(f9(a20),f11(f10(a24),f10(a23))))),f8(f1(f1(f6(a7,a13)))),a21)), % 59.52/59.57 inference(scs_inference,[],[36,76,24])). % 59.52/59.57 cnf(196,plain, % 59.52/59.57 (E(f11(f9(f15(f8(x1961))),x1962),f11(f9(f15(f8(f1(x1961)))),x1962))), % 59.52/59.57 inference(scs_inference,[],[75,2,6])). % 59.52/59.57 cnf(197,plain, % 59.52/59.57 (E(f11(f9(f15(f8(f1(x1971)))),x1972),f11(f9(f15(f8(x1971))),x1972))), % 59.52/59.57 inference(scs_inference,[],[196,2])). % 59.52/59.57 cnf(218,plain, % 59.52/59.57 (E(f6(f9(f15(f8(x2181))),x2182),f6(f9(f15(f8(f1(x2181)))),x2182))), % 59.52/59.57 inference(scs_inference,[],[75,2,17])). % 59.52/59.57 cnf(219,plain, % 59.52/59.57 (E(f6(f9(f15(f8(f1(x2191)))),x2192),f6(f9(f15(f8(x2191))),x2192))), % 59.52/59.57 inference(scs_inference,[],[218,2])). % 59.52/59.57 cnf(222,plain, % 59.52/59.57 (E(f12(f9(f15(f8(x2221))),x2222),f12(f9(f15(f8(f1(x2221)))),x2222))), % 59.52/59.57 inference(scs_inference,[],[75,2,19])). % 59.52/59.57 cnf(223,plain, % 59.52/59.57 (E(f12(f9(f15(f8(f1(x2231)))),x2232),f12(f9(f15(f8(x2231))),x2232))), % 59.52/59.57 inference(scs_inference,[],[222,2])). % 59.52/59.57 cnf(450,plain, % 59.52/59.57 (E(f6(x4501,f8(x4502)),f6(x4501,f8(f1(x4502))))), % 59.52/59.57 inference(scs_inference,[],[26,2,18])). % 59.52/59.57 cnf(451,plain, % 59.52/59.57 (E(f6(x4511,f8(f1(x4512))),f6(x4511,f8(x4512)))), % 59.52/59.57 inference(scs_inference,[],[450,2])). % 59.52/59.57 cnf(452,plain, % 59.52/59.57 (E(f6(f6(x4521,f8(x4522)),f8(x4523)),f6(f6(x4521,f8(f1(x4522))),f8(f1(x4523))))), % 59.52/59.57 inference(scs_inference,[],[103,450,2,3])). % 59.52/59.57 cnf(455,plain, % 59.52/59.57 (E(f3(f8(x4551),x4552),f3(f8(f1(x4551)),x4552))), % 59.52/59.57 inference(scs_inference,[],[26,2,21])). % 59.52/59.57 cnf(456,plain, % 59.52/59.57 (E(f6(f6(x4561,f8(f1(x4562))),f8(f1(x4563))),f6(f6(x4561,f8(x4562)),f8(x4563)))), % 59.52/59.57 inference(scs_inference,[],[452,2])). % 59.52/59.57 cnf(457,plain, % 59.52/59.57 (E(f6(f9(f15(f8(f1(x4571)))),f8(f1(x4572))),f6(f9(f15(f8(x4571))),f8(x4572)))), % 59.52/59.57 inference(scs_inference,[],[451,452,219,2,3])). % 59.52/59.57 cnf(460,plain, % 59.52/59.57 (E(f8(f8(x4601)),f8(f8(f1(x4601))))), % 59.52/59.57 inference(scs_inference,[],[26,2,5])). % 59.52/59.57 cnf(462,plain, % 59.52/59.57 (E(f6(f6(x4621,f8(f1(f1(x4622)))),f8(f1(x4623))),f6(f6(x4621,f8(x4622)),f8(x4623)))), % 59.52/59.57 inference(scs_inference,[],[102,456,457,2,3])). % 59.52/59.57 cnf(465,plain, % 59.52/59.57 (E(f3(x4651,f8(x4652)),f3(x4651,f8(f1(x4652))))), % 59.52/59.57 inference(scs_inference,[],[26,2,22])). % 59.52/59.57 cnf(466,plain, % 59.52/59.57 (E(f6(f6(x4661,f8(x4662)),f8(x4663)),f6(f6(x4661,f8(f1(f1(x4662)))),f8(f1(x4663))))), % 59.52/59.57 inference(scs_inference,[],[462,2])). % 59.52/59.57 cnf(467,plain, % 59.52/59.57 (E(f8(f1(f8(x4671))),f8(f8(f1(x4671))))), % 59.52/59.57 inference(scs_inference,[],[26,462,460,2,3])). % 59.52/59.57 cnf(469,plain, % 59.52/59.57 (E(f11(f8(x4691),x4692),f11(f8(f1(x4691)),x4692))), % 59.52/59.57 inference(scs_inference,[],[26,2,6])). % 59.52/59.57 cnf(471,plain, % 59.52/59.57 (E(f3(f3(x4711,f8(x4712)),f8(x4713)),f3(f3(x4711,f8(f1(x4712))),f8(f1(x4713))))), % 59.52/59.57 inference(scs_inference,[],[107,455,465,2,3])). % 59.52/59.57 cnf(474,plain, % 59.52/59.57 (E(f11(x4741,f8(x4742)),f11(x4741,f8(f1(x4742))))), % 59.52/59.57 inference(scs_inference,[],[26,2,7])). % 59.52/59.57 cnf(475,plain, % 59.52/59.57 (E(f8(f8(f1(x4751))),f8(f1(f8(x4751))))), % 59.52/59.57 inference(scs_inference,[],[467,2])). % 59.52/59.57 cnf(476,plain, % 59.52/59.57 (E(f6(f6(x4761,f8(x4762)),f8(x4763)),f6(f6(x4761,f8(f1(f1(f1(x4762))))),f8(f1(x4763))))), % 59.52/59.57 inference(scs_inference,[],[103,466,467,2,3])). % 59.52/59.57 cnf(479,plain, % 59.52/59.57 (E(f17(f8(x4791)),f17(f8(f1(x4791))))), % 59.52/59.57 inference(scs_inference,[],[26,2,8])). % 59.52/59.57 cnf(480,plain, % 59.52/59.57 (E(f11(f8(f1(x4801)),x4802),f11(f8(x4801),x4802))), % 59.52/59.57 inference(scs_inference,[],[469,2])). % 59.52/59.57 cnf(481,plain, % 59.52/59.57 (E(f11(f8(x4811),f8(x4812)),f11(f8(f1(x4811)),f8(f1(x4812))))), % 59.52/59.57 inference(scs_inference,[],[469,474,2,3])). % 59.52/59.57 cnf(484,plain, % 59.52/59.57 (E(f9(f8(x4841)),f9(f8(f1(x4841))))), % 59.52/59.57 inference(scs_inference,[],[26,2,9])). % 59.52/59.57 cnf(485,plain, % 59.52/59.57 (E(f3(f3(x4851,f8(f1(x4852))),f8(f1(x4853))),f3(f3(x4851,f8(x4852)),f8(x4853)))), % 59.52/59.57 inference(scs_inference,[],[471,2])). % 59.52/59.57 cnf(486,plain, % 59.52/59.57 (E(f8(f1(f8(f1(x4861)))),f8(f1(f8(x4861))))), % 59.52/59.57 inference(scs_inference,[],[26,471,475,2,3])). % 59.52/59.57 cnf(488,plain, % 59.52/59.57 (E(f15(f8(x4881)),f15(f8(f1(x4881))))), % 59.52/59.57 inference(scs_inference,[],[26,2,10])). % 59.52/59.57 cnf(490,plain, % 59.52/59.57 (E(f3(f3(x4901,f8(f1(f1(x4902)))),f8(f1(x4903))),f3(f3(x4901,f8(x4902)),f8(x4903)))), % 59.52/59.57 inference(scs_inference,[],[106,485,476,2,3])). % 59.52/59.57 cnf(493,plain, % 59.52/59.57 (E(f5(f8(x4931),x4932,x4933),f5(f8(f1(x4931)),x4932,x4933))), % 59.52/59.57 inference(scs_inference,[],[26,2,11])). % 59.52/59.57 cnf(494,plain, % 59.52/59.57 (E(f3(f3(x4941,f8(x4942)),f8(x4943)),f3(f3(x4941,f8(f1(f1(x4942)))),f8(f1(x4943))))), % 59.52/59.57 inference(scs_inference,[],[490,2])). % 59.52/59.57 cnf(495,plain, % 59.52/59.57 (E(f8(f1(f1(f8(f1(x4951))))),f8(f1(f8(x4951))))), % 59.52/59.57 inference(scs_inference,[],[26,490,486,2,3])). % 59.52/59.57 cnf(497,plain, % 59.52/59.57 (E(f5(x4971,f8(x4972),x4973),f5(x4971,f8(f1(x4972)),x4973))), % 59.52/59.57 inference(scs_inference,[],[26,2,12])). % 59.52/59.57 cnf(498,plain, % 59.52/59.57 (E(f17(f8(f1(x4981))),f17(f8(x4981)))), % 59.52/59.57 inference(scs_inference,[],[479,2])). % 59.52/59.57 cnf(499,plain, % 59.52/59.57 (E(f5(f8(x4991),f8(x4992),x4993),f5(f8(f1(x4991)),f8(f1(x4992)),x4993))), % 59.52/59.57 inference(scs_inference,[],[479,493,497,2,3])). % 59.52/59.57 cnf(502,plain, % 59.52/59.57 (E(f5(x5021,x5022,f8(x5023)),f5(x5021,x5022,f8(f1(x5023))))), % 59.52/59.57 inference(scs_inference,[],[26,2,13])). % 59.52/59.57 cnf(503,plain, % 59.52/59.57 (E(f11(f8(f1(x5031)),f8(f1(x5032))),f11(f8(x5031),f8(x5032)))), % 59.52/59.57 inference(scs_inference,[],[481,2])). % 59.52/59.57 cnf(504,plain, % 59.52/59.57 (E(f3(f3(x5041,f8(x5042)),f8(x5043)),f3(f3(x5041,f8(f1(f1(f1(x5042))))),f8(f1(x5043))))), % 59.52/59.57 inference(scs_inference,[],[107,481,494,2,3])). % 59.52/59.57 cnf(507,plain, % 59.52/59.57 (E(f10(f8(x5071)),f10(f8(f1(x5071))))), % 59.52/59.57 inference(scs_inference,[],[26,2,14])). % 59.52/59.57 cnf(509,plain, % 59.52/59.57 (E(f11(f8(f1(f1(x5091))),f8(f1(x5092))),f11(f8(x5091),f8(x5092)))), % 59.52/59.57 inference(scs_inference,[],[480,503,484,2,3])). % 59.52/59.57 cnf(512,plain, % 59.52/59.57 (E(f4(f8(x5121),x5122),f4(f8(f1(x5121)),x5122))), % 59.52/59.57 inference(scs_inference,[],[26,2,15])). % 59.52/59.57 cnf(513,plain, % 59.52/59.57 (E(f11(f8(x5131),f8(x5132)),f11(f8(f1(f1(x5131))),f8(f1(x5132))))), % 59.52/59.57 inference(scs_inference,[],[509,2])). % 59.52/59.57 cnf(514,plain, % 59.52/59.57 (E(f11(f8(f1(f1(f1(x5141)))),f8(f1(x5142))),f11(f8(x5141),f8(x5142)))), % 59.52/59.57 inference(scs_inference,[],[509,480,2,3])). % 59.52/59.57 cnf(516,plain, % 59.52/59.57 (E(f4(x5161,f8(x5162)),f4(x5161,f8(f1(x5162))))), % 59.52/59.57 inference(scs_inference,[],[26,2,16])). % 59.52/59.57 cnf(517,plain, % 59.52/59.57 (E(f11(f8(x5171),f8(x5172)),f11(f8(f1(f1(f1(x5171)))),f8(f1(x5172))))), % 59.52/59.57 inference(scs_inference,[],[514,2])). % 59.52/59.57 cnf(518,plain, % 59.52/59.57 (E(f5(f8(x5181),f8(x5182),f8(x5183)),f5(f8(f1(x5181)),f8(f1(x5182)),f8(f1(x5183))))), % 59.52/59.57 inference(scs_inference,[],[514,499,502,2,3])). % 59.52/59.57 cnf(521,plain, % 59.52/59.57 (E(f6(f8(x5211),x5212),f6(f8(f1(x5211)),x5212))), % 59.52/59.57 inference(scs_inference,[],[26,2,17])). % 59.52/59.57 cnf(522,plain, % 59.52/59.57 (E(f15(f8(f1(x5221))),f15(f8(x5221)))), % 59.52/59.57 inference(scs_inference,[],[488,2])). % 59.52/59.57 cnf(523,plain, % 59.52/59.57 (E(f4(f8(x5231),f5(x5232,x5233,f8(x5234))),f4(f8(f1(x5231)),f5(x5232,x5233,f8(f1(x5234)))))), % 59.52/59.57 inference(scs_inference,[],[101,488,512,2,3])). % 59.52/59.57 cnf(526,plain, % 59.52/59.57 (E(f12(f8(x5261),x5262),f12(f8(f1(x5261)),x5262))), % 59.52/59.57 inference(scs_inference,[],[26,2,19])). % 59.52/59.57 cnf(527,plain, % 59.52/59.57 (E(f8(f1(f8(x5271))),f8(f1(f1(f8(f1(x5271))))))), % 59.52/59.57 inference(scs_inference,[],[495,2])). % 59.52/59.57 cnf(528,plain, % 59.52/59.57 (E(f4(f8(x5281),f8(x5282)),f4(f8(f1(x5281)),f8(f1(x5282))))), % 59.52/59.57 inference(scs_inference,[],[495,516,512,2,3])). % 59.52/59.57 cnf(531,plain, % 59.52/59.57 (E(f12(x5311,f8(x5312)),f12(x5311,f8(f1(x5312))))), % 59.52/59.57 inference(scs_inference,[],[26,2,20])). % 59.52/59.57 cnf(533,plain, % 59.52/59.57 (E(f5(f8(x5331),f8(x5332),f8(x5333)),f5(f8(f1(f1(x5331))),f8(f1(x5332)),f8(f1(x5333))))), % 59.52/59.57 inference(scs_inference,[],[504,518,493,2,3])). % 59.52/59.57 cnf(538,plain, % 59.52/59.57 (E(f6(f8(x5381),f8(f1(x5382))),f6(f8(f1(x5381)),f8(x5382)))), % 59.52/59.57 inference(scs_inference,[],[507,521,451,2,3])). % 59.52/59.57 cnf(542,plain, % 59.52/59.57 (E(f6(f8(f1(x5421)),f8(x5422)),f6(f8(x5421),f8(f1(x5422))))), % 59.52/59.57 inference(scs_inference,[],[538,2])). % 59.52/59.57 cnf(543,plain, % 59.52/59.57 (E(f6(f8(x5431),f8(f1(x5432))),f6(f8(f1(f1(x5431))),f8(x5432)))), % 59.52/59.57 inference(scs_inference,[],[538,521,2,3])). % 59.52/59.57 cnf(547,plain, % 59.52/59.57 (E(f6(f8(f1(f1(x5471))),f8(x5472)),f6(f8(x5471),f8(f1(x5472))))), % 59.52/59.57 inference(scs_inference,[],[543,2])). % 59.52/59.57 cnf(548,plain, % 59.52/59.57 (E(f12(f8(x5481),f8(x5482)),f12(f8(f1(x5481)),f8(f1(x5482))))), % 59.52/59.57 inference(scs_inference,[],[543,526,531,2,3])). % 59.52/59.57 cnf(552,plain, % 59.52/59.57 (E(f4(f8(f1(x5521)),f8(f1(x5522))),f4(f8(x5521),f8(x5522)))), % 59.52/59.57 inference(scs_inference,[],[528,2])). % 59.52/59.57 cnf(553,plain, % 59.52/59.57 (E(f4(f8(x5531),f8(x5532)),f4(f8(f1(x5531)),f8(f1(f1(x5532)))))), % 59.52/59.57 inference(scs_inference,[],[528,516,2,3])). % 59.52/59.57 cnf(557,plain, % 59.52/59.57 (E(f5(f8(f1(f1(x5571))),f8(f1(x5572)),f8(f1(x5573))),f5(f8(x5571),f8(x5572),f8(x5573)))), % 59.52/59.57 inference(scs_inference,[],[533,2])). % 59.52/59.57 cnf(558,plain, % 59.52/59.57 (E(f5(f8(x5581),f8(x5582),f8(x5583)),f5(f8(f1(f1(x5581))),f8(f1(f1(x5582))),f8(f1(x5583))))), % 59.52/59.57 inference(scs_inference,[],[533,497,2,3])). % 59.52/59.57 cnf(561,plain, % 59.52/59.57 (E(f12(f8(f1(x5611)),f8(f1(x5612))),f12(f8(x5611),f8(x5612)))), % 59.52/59.57 inference(scs_inference,[],[548,2])). % 59.52/59.57 cnf(562,plain, % 59.52/59.57 (E(f6(f8(f1(f1(f1(x5621)))),f8(x5622)),f6(f8(x5621),f8(f1(f1(x5622)))))), % 59.52/59.57 inference(scs_inference,[],[542,547,548,2,3])). % 59.52/59.57 cnf(566,plain, % 59.52/59.57 (E(f5(f8(f1(f1(x5661))),f8(f1(f1(x5662))),f8(f1(x5663))),f5(f8(x5661),f8(x5662),f8(x5663)))), % 59.52/59.57 inference(scs_inference,[],[558,2])). % 59.52/59.57 cnf(567,plain, % 59.52/59.57 (E(f12(f8(x5671),f8(f1(x5672))),f12(f8(x5671),f8(x5672)))), % 59.52/59.57 inference(scs_inference,[],[561,558,526,2,3])). % 59.52/59.57 cnf(571,plain, % 59.52/59.57 (E(f4(f8(f1(x5711)),f5(x5712,x5713,f8(f1(x5714)))),f4(f8(x5711),f5(x5712,x5713,f8(x5714))))), % 59.52/59.57 inference(scs_inference,[],[523,2])). % 59.52/59.57 cnf(572,plain, % 59.52/59.57 (E(f12(f8(f1(x5721)),f8(f1(f1(x5722)))),f12(f8(x5721),f8(x5722)))), % 59.52/59.57 inference(scs_inference,[],[567,523,561,2,3])). % 59.52/59.57 cnf(576,plain, % 59.52/59.57 (E(f12(f8(x5761),f8(x5762)),f12(f8(f1(x5761)),f8(f1(f1(x5762)))))), % 59.52/59.57 inference(scs_inference,[],[572,2])). % 59.52/59.57 cnf(577,plain, % 59.52/59.57 (E(f12(f8(f1(x5771)),f8(f1(f1(f1(x5772))))),f12(f8(x5771),f8(x5772)))), % 59.52/59.57 inference(scs_inference,[],[572,567,2,3])). % 59.52/59.57 cnf(580,plain, % 59.52/59.57 (E(f12(f8(x5801),f8(x5802)),f12(f8(f1(x5801)),f8(f1(f1(f1(x5802))))))), % 59.52/59.57 inference(scs_inference,[],[577,2])). % 59.52/59.57 cnf(581,plain, % 59.52/59.57 (E(f4(f8(f1(x5811)),f5(x5812,x5813,f8(f1(f1(x5814))))),f4(f8(x5811),f5(x5812,x5813,f8(x5814))))), % 59.52/59.57 inference(scs_inference,[],[100,577,571,2,3])). % 59.52/59.57 cnf(586,plain, % 59.52/59.57 (E(f8(f1(f1(f8(x5861)))),f8(f1(f1(f8(f1(x5861))))))), % 59.52/59.57 inference(scs_inference,[],[26,581,527,2,3])). % 59.52/59.57 cnf(589,plain, % 59.52/59.57 (E(f4(f8(f1(x5891)),f8(f1(f1(x5892)))),f4(f8(x5891),f8(x5892)))), % 59.52/59.57 inference(scs_inference,[],[553,2])). % 59.52/59.57 cnf(590,plain, % 59.52/59.57 (E(f3(f3(x5901,f8(f1(x5902))),f8(x5903)),f3(f3(x5901,f8(x5902)),f8(f1(x5903))))), % 59.52/59.57 inference(scs_inference,[],[106,553,465,2,3])). % 59.52/59.57 cnf(594,plain, % 59.52/59.57 (E(f3(f3(x5941,f8(x5942)),f8(f1(x5943))),f3(f3(x5941,f8(f1(x5942))),f8(x5943)))), % 59.52/59.57 inference(scs_inference,[],[590,2])). % 59.52/59.57 cnf(595,plain, % 59.52/59.57 (E(f4(f8(f1(f1(x5951))),f8(f1(f1(f1(x5952))))),f4(f8(x5951),f8(x5952)))), % 59.52/59.57 inference(scs_inference,[],[552,589,590,2,3])). % 59.52/59.57 cnf(598,plain, % 59.52/59.57 (E(f4(f8(x5981),f8(x5982)),f4(f8(f1(f1(x5981))),f8(f1(f1(f1(x5982))))))), % 59.52/59.57 inference(scs_inference,[],[595,2])). % 59.52/59.57 cnf(599,plain, % 59.52/59.57 (E(f3(f3(x5991,f8(x5992)),f8(f1(x5993))),f3(f3(x5991,f8(f1(f1(x5992)))),f8(x5993)))), % 59.52/59.57 inference(scs_inference,[],[107,594,595,2,3])). % 59.52/59.57 cnf(603,plain, % 59.52/59.57 (E(f3(f3(x6031,f8(f1(f1(x6032)))),f8(x6033)),f3(f3(x6031,f8(x6032)),f8(f1(x6033))))), % 59.52/59.57 inference(scs_inference,[],[599,2])). % 59.52/59.57 cnf(608,plain, % 59.52/59.57 (E(f6(f8(x6081),f8(f1(f1(x6082)))),f6(f8(f1(f1(f1(x6081)))),f8(x6082)))), % 59.52/59.57 inference(scs_inference,[],[562,2])). % 59.52/59.57 cnf(614,plain, % 59.52/59.57 (E(f3(f3(x6141,f8(f1(f1(f1(x6142))))),f8(x6143)),f3(f3(x6141,f8(x6142)),f8(f1(x6143))))), % 59.52/59.57 inference(scs_inference,[],[106,603,586,2,3])). % 59.52/59.57 cnf(619,plain, % 59.52/59.57 (E(f8(f1(f1(f8(x6191)))),f8(f8(f1(x6191))))), % 59.52/59.57 inference(scs_inference,[],[26,614,467,2,3])). % 59.52/59.57 cnf(622,plain, % 59.52/59.57 (E(f8(f8(f1(x6221))),f8(f1(f1(f8(x6221)))))), % 59.52/59.57 inference(scs_inference,[],[619,2])). % 59.52/59.57 cnf(623,plain, % 59.52/59.57 (E(f8(f1(f1(f1(f8(x6231))))),f8(f8(f1(x6231))))), % 59.52/59.57 inference(scs_inference,[],[26,619,2,3])). % 59.52/59.57 cnf(626,plain, % 59.52/59.57 (E(f8(f8(f1(x6261))),f8(f1(f1(f1(f8(x6261))))))), % 59.52/59.57 inference(scs_inference,[],[623,2])). % 59.52/59.57 cnf(627,plain, % 59.52/59.57 (E(f8(f1(f8(f1(x6271)))),f8(f1(f1(f8(x6271)))))), % 59.52/59.57 inference(scs_inference,[],[26,623,622,2,3])). % 59.52/59.57 cnf(631,plain, % 59.52/59.57 (E(f8(f1(f8(f1(x6311)))),f8(f1(f1(f1(f8(x6311))))))), % 59.52/59.57 inference(scs_inference,[],[26,627,626,2,3])). % 59.52/59.57 cnf(635,plain, % 59.52/59.57 (E(f11(f8(x6351),f8(x6352)),f11(f8(f1(f1(x6351))),f8(f1(f1(x6352)))))), % 59.52/59.57 inference(scs_inference,[],[513,631,474,2,3])). % 59.52/59.57 cnf(638,plain, % 59.52/59.57 (E(f11(f8(f1(f1(x6381))),f8(f1(f1(x6382)))),f11(f8(x6381),f8(x6382)))), % 59.52/59.57 inference(scs_inference,[],[635,2])). % 59.52/59.57 cnf(639,plain, % 59.52/59.57 (E(f11(f8(x6391),f8(x6392)),f11(f8(f1(f1(x6391))),f8(x6392)))), % 59.52/59.57 inference(scs_inference,[],[517,635,503,2,3])). % 59.52/59.57 cnf(642,plain, % 59.52/59.57 (E(f11(f8(f1(f1(x6421))),f8(x6422)),f11(f8(x6421),f8(x6422)))), % 59.52/59.57 inference(scs_inference,[],[639,2])). % 59.52/59.57 cnf(643,plain, % 59.52/59.57 (E(f11(f8(x6431),f8(f1(f1(x6432)))),f11(f8(x6431),f8(x6432)))), % 59.52/59.57 inference(scs_inference,[],[638,639,2,3])). % 59.52/59.57 cnf(647,plain, % 59.52/59.57 (E(f11(f8(x6471),f8(x6472)),f11(f8(x6471),f8(f1(f1(x6472)))))), % 59.52/59.57 inference(scs_inference,[],[643,2])). % 59.52/59.57 cnf(648,plain, % 59.52/59.57 (E(f11(f8(f1(f1(x6481))),f8(x6482)),f11(f8(f1(x6481)),f8(f1(x6482))))), % 59.52/59.57 inference(scs_inference,[],[642,643,481,2,3])). % 59.52/59.57 cnf(651,plain, % 59.52/59.57 (E(f11(f8(f1(x6511)),f8(f1(x6512))),f11(f8(f1(f1(x6511))),f8(x6512)))), % 59.52/59.57 inference(scs_inference,[],[648,2])). % 59.52/59.57 cnf(652,plain, % 59.52/59.57 (E(f11(f8(f1(f1(x6521))),f8(x6522)),f11(f8(f1(x6521)),f8(f1(f1(f1(x6522))))))), % 59.52/59.57 inference(scs_inference,[],[648,647,2,3])). % 59.52/59.57 cnf(655,plain, % 59.52/59.57 (E(f11(f8(f1(x6551)),f8(f1(f1(f1(x6552))))),f11(f8(f1(f1(x6551))),f8(x6552)))), % 59.52/59.57 inference(scs_inference,[],[652,2])). % 59.52/59.57 cnf(656,plain, % 59.52/59.57 (E(f11(f8(f1(x6561)),f8(f1(f1(f1(x6562))))),f11(f8(x6561),f8(x6562)))), % 59.52/59.57 inference(scs_inference,[],[651,652,638,2,3])). % 59.52/59.57 cnf(660,plain, % 59.52/59.57 (E(f11(f8(x6601),f8(x6602)),f11(f8(f1(x6601)),f8(f1(f1(f1(x6602))))))), % 59.52/59.57 inference(scs_inference,[],[656,2])). % 59.52/59.57 cnf(661,plain, % 59.52/59.57 (E(f5(f8(f1(f1(x6611))),f8(f1(x6612)),f8(f1(x6613))),f5(f8(f1(x6611)),f8(f1(x6612)),f8(x6613)))), % 59.52/59.57 inference(scs_inference,[],[557,656,499,2,3])). % 59.52/59.57 cnf(664,plain, % 59.52/59.57 (E(f5(f8(f1(x6641)),f8(f1(x6642)),f8(x6643)),f5(f8(f1(f1(x6641))),f8(f1(x6642)),f8(f1(x6643))))), % 59.52/59.57 inference(scs_inference,[],[661,2])). % 59.52/59.57 cnf(665,plain, % 59.52/59.57 (E(f5(f8(f1(f1(f1(x6651)))),f8(f1(f1(x6652))),f8(f1(f1(x6653)))),f5(f8(x6651),f8(x6652),f8(x6653)))), % 59.52/59.57 inference(scs_inference,[],[566,661,2,3])). % 59.52/59.57 cnf(668,plain, % 59.52/59.57 (E(f5(f8(x6681),f8(x6682),f8(x6683)),f5(f8(f1(f1(f1(x6681)))),f8(f1(f1(x6682))),f8(f1(f1(x6683)))))), % 59.52/59.57 inference(scs_inference,[],[665,2])). % 59.52/59.57 cnf(669,plain, % 59.52/59.57 (E(f12(f12(x6691,f8(x6692)),f8(x6693)),f12(f12(x6691,f8(f1(x6692))),f8(f1(x6693))))), % 59.52/59.57 inference(scs_inference,[],[105,665,531,2,3])). % 59.52/59.57 cnf(673,plain, % 59.52/59.57 (E(f12(f12(x6731,f8(f1(x6732))),f8(f1(x6733))),f12(f12(x6731,f8(x6732)),f8(x6733)))), % 59.52/59.57 inference(scs_inference,[],[669,2])). % 59.52/59.57 cnf(674,plain, % 59.52/59.58 (E(f12(f12(x6741,f8(x6742)),f8(x6743)),f12(f12(x6741,f8(f1(f1(x6742)))),f8(f1(x6743))))), % 59.52/59.58 inference(scs_inference,[],[105,669,2,3])). % 59.52/59.58 cnf(678,plain, % 59.52/59.58 (E(f12(f12(x6781,f8(f1(f1(x6782)))),f8(f1(x6783))),f12(f12(x6781,f8(x6782)),f8(x6783)))), % 59.52/59.58 inference(scs_inference,[],[674,2])). % 59.52/59.58 cnf(679,plain, % 59.52/59.58 (E(f12(f12(x6791,f8(x6792)),f8(f1(x6793))),f12(f12(x6791,f8(x6792)),f8(x6793)))), % 59.52/59.58 inference(scs_inference,[],[105,673,674,2,3])). % 59.52/59.58 cnf(684,plain, % 59.52/59.58 (E(f12(f12(x6841,f8(x6842)),f8(f1(x6843))),f12(f12(x6841,f8(f1(x6842))),f8(x6843)))), % 59.52/59.58 inference(scs_inference,[],[105,679,460,2,3])). % 59.52/59.58 cnf(688,plain, % 59.52/59.58 (E(f12(f12(x6881,f8(f1(x6882))),f8(x6883)),f12(f12(x6881,f8(x6882)),f8(f1(x6883))))), % 59.52/59.58 inference(scs_inference,[],[684,2])). % 59.52/59.58 cnf(704,plain, % 59.52/59.58 (E(f5(x7041,x7042,f8(f1(x7043))),f5(x7041,x7042,f8(x7043)))), % 59.52/59.58 inference(scs_inference,[],[502,2])). % 59.52/59.58 cnf(705,plain, % 59.52/59.58 (E(f5(f8(f1(x7051)),f8(f1(x7052)),f8(x7053)),f5(f8(x7051),f8(x7052),f8(x7053)))), % 59.52/59.58 inference(scs_inference,[],[664,557,502,2,3])). % 59.52/59.58 cnf(708,plain, % 59.52/59.58 (E(f5(f8(f1(x7081)),f8(f1(x7082)),f8(f1(x7083))),f5(f8(x7081),f8(x7082),f8(x7083)))), % 59.52/59.58 inference(scs_inference,[],[518,2])). % 59.52/59.58 cnf(709,plain, % 59.52/59.58 (E(f5(f8(f1(f1(x7091))),f8(f1(f1(x7092))),f8(f1(f1(x7093)))),f5(f8(x7091),f8(x7092),f8(x7093)))), % 59.52/59.58 inference(scs_inference,[],[704,566,518,2,3])). % 59.52/59.58 cnf(712,plain, % 59.52/59.58 (E(f5(f8(x7121),f8(x7122),f8(x7123)),f5(f8(f1(f1(x7121))),f8(f1(f1(x7122))),f8(f1(f1(x7123)))))), % 59.52/59.58 inference(scs_inference,[],[709,2])). % 59.52/59.58 cnf(713,plain, % 59.52/59.58 (E(f12(f12(x7131,f8(x7132)),f8(f1(x7133))),f12(f12(x7131,f8(f1(f1(x7132)))),f8(x7133)))), % 59.52/59.58 inference(scs_inference,[],[105,709,684,2,3])). % 59.52/59.58 cnf(718,plain, % 59.52/59.58 (E(f12(f12(x7181,f8(x7182)),f8(f1(x7183))),f12(f12(x7181,f8(f1(f1(f1(x7182))))),f8(x7183)))), % 59.52/59.58 inference(scs_inference,[],[105,713,2,3])). % 59.52/59.58 cnf(723,plain, % 59.52/59.58 (E(f5(f8(f1(x7231)),f8(f1(x7232)),f8(x7233)),f5(f8(f1(f1(x7231))),f8(f1(f1(x7232))),f8(f1(f1(x7233)))))), % 59.52/59.58 inference(scs_inference,[],[705,718,712,2,3])). % 59.52/59.58 cnf(727,plain, % 59.52/59.58 (E(f5(f8(f1(x7271)),f8(f1(x7272)),f8(f1(f1(x7273)))),f5(f8(x7271),f8(x7272),f8(x7273)))), % 59.52/59.58 inference(scs_inference,[],[708,723,704,2,3])). % 59.52/59.58 cnf(731,plain, % 59.52/59.58 (E(f5(f8(x7311),f8(x7312),f8(x7313)),f5(f8(f1(x7311)),f8(f1(x7312)),f8(f1(f1(x7313)))))), % 59.52/59.58 inference(scs_inference,[],[727,2])). % 59.52/59.58 cnf(732,plain, % 59.52/59.58 (E(f5(f8(x7321),f8(x7322),f8(x7323)),f5(f8(f1(f1(x7321))),f8(f1(x7322)),f8(x7323)))), % 59.52/59.58 inference(scs_inference,[],[727,668,2,3])). % 59.52/59.58 cnf(735,plain, % 59.52/59.58 (E(f5(f8(f1(f1(x7351))),f8(f1(x7352)),f8(x7353)),f5(f8(x7351),f8(x7352),f8(x7353)))), % 59.52/59.58 inference(scs_inference,[],[732,2])). % 59.52/59.58 cnf(736,plain, % 59.52/59.58 (E(f5(f8(x7361),f8(x7362),f8(f1(x7363))),f5(f8(f1(x7361)),f8(x7362),f8(x7363)))), % 59.52/59.58 inference(scs_inference,[],[732,708,2,3])). % 59.52/59.58 cnf(740,plain, % 59.52/59.58 (E(f5(f8(f1(x7401)),f8(x7402),f8(x7403)),f5(f8(x7401),f8(x7402),f8(f1(x7403))))), % 59.52/59.58 inference(scs_inference,[],[736,2])). % 59.52/59.58 cnf(741,plain, % 59.52/59.58 (E(f5(f8(f1(f1(x7411))),f8(f1(x7412)),f8(x7413)),f5(f8(f1(x7411)),f8(f1(x7412)),f8(f1(f1(x7413)))))), % 59.52/59.58 inference(scs_inference,[],[735,736,731,2,3])). % 59.52/59.58 cnf(744,plain, % 59.52/59.58 (E(f5(f8(f1(x7441)),f8(f1(x7442)),f8(f1(f1(x7443)))),f5(f8(f1(f1(x7441))),f8(f1(x7442)),f8(x7443)))), % 59.52/59.58 inference(scs_inference,[],[741,2])). % 59.52/59.58 cnf(745,plain, % 59.52/59.58 (E(f5(f8(f1(f1(x7451))),f8(f1(x7452)),f8(x7453)),f5(f8(x7451),f8(f1(x7452)),f8(f1(f1(f1(x7453))))))), % 59.52/59.58 inference(scs_inference,[],[740,741,2,3])). % 59.52/59.58 cnf(747,plain, % 59.52/59.58 (E(f5(f8(x7471),f8(f1(x7472)),f8(f1(f1(f1(x7473))))),f5(f8(f1(f1(x7471))),f8(f1(x7472)),f8(x7473)))), % 59.52/59.58 inference(scs_inference,[],[745,2])). % 59.52/59.58 cnf(748,plain, % 59.52/59.58 (E(f5(f8(f1(x7481)),f8(f1(x7482)),f8(f1(f1(x7483)))),f5(f8(f1(x7481)),f8(x7482),f8(x7483)))), % 59.52/59.58 inference(scs_inference,[],[744,745,705,2,3])). % 59.52/59.58 cnf(751,plain, % 59.52/59.58 (E(f5(f8(f1(x7511)),f8(x7512),f8(x7513)),f5(f8(f1(x7511)),f8(f1(x7512)),f8(f1(f1(x7513)))))), % 59.52/59.58 inference(scs_inference,[],[748,2])). % 59.52/59.58 cnf(752,plain, % 59.52/59.58 (E(f5(f8(x7521),f8(f1(x7522)),f8(f1(f1(f1(x7523))))),f5(f8(x7521),f8(x7522),f8(x7523)))), % 59.52/59.58 inference(scs_inference,[],[747,748,735,2,3])). % 59.52/59.58 cnf(755,plain, % 59.52/59.58 (E(f5(f8(x7551),f8(x7552),f8(x7553)),f5(f8(x7551),f8(f1(x7552)),f8(f1(f1(f1(x7553))))))), % 59.52/59.58 inference(scs_inference,[],[752,2])). % 59.52/59.58 cnf(756,plain, % 59.52/59.58 (E(f12(f8(x7561),f8(x7562)),f12(f8(f1(f1(x7561))),f8(f1(f1(f1(x7562))))))), % 59.52/59.58 inference(scs_inference,[],[752,576,548,2,3])). % 59.52/59.58 cnf(759,plain, % 59.52/59.58 (E(f12(f8(f1(f1(x7591))),f8(f1(f1(f1(x7592))))),f12(f8(x7591),f8(x7592)))), % 59.52/59.58 inference(scs_inference,[],[756,2])). % 59.52/59.58 cnf(760,plain, % 59.52/59.58 (E(f5(f8(f1(f1(f1(x7601)))),f8(f1(x7602)),f8(x7603)),f5(f8(x7601),f8(x7602),f8(x7603)))), % 59.52/59.58 inference(scs_inference,[],[751,756,665,2,3])). % 59.52/59.58 cnf(764,plain, % 59.52/59.58 (E(f5(f8(x7641),f8(x7642),f8(x7643)),f5(f8(f1(f1(f1(x7641)))),f8(f1(x7642)),f8(x7643)))), % 59.52/59.58 inference(scs_inference,[],[760,2])). % 59.52/59.58 cnf(765,plain, % 59.52/59.58 (E(f12(f8(f1(x7651)),f8(x7652)),f12(f8(x7651),f8(x7652)))), % 59.52/59.58 inference(scs_inference,[],[759,760,580,2,3])). % 59.52/59.58 cnf(770,plain, % 59.52/59.58 (E(f5(f8(x7701),f8(f1(x7702)),f8(f1(f1(x7703)))),f5(f8(f1(x7701)),f8(x7702),f8(x7703)))), % 59.52/59.58 inference(scs_inference,[],[764,709,465,2,3])). % 59.52/59.58 cnf(774,plain, % 59.52/59.58 (E(f5(f8(f1(x7741)),f8(x7742),f8(x7743)),f5(f8(x7741),f8(f1(x7742)),f8(f1(f1(x7743)))))), % 59.52/59.58 inference(scs_inference,[],[770,2])). % 59.52/59.58 cnf(775,plain, % 59.52/59.58 (E(f5(f8(x7751),f8(x7752),f8(x7753)),f5(f8(f1(x7751)),f8(x7752),f8(f1(x7753))))), % 59.52/59.58 inference(scs_inference,[],[770,755,2,3])). % 59.52/59.58 cnf(778,plain, % 59.52/59.58 (E(f5(f8(f1(x7781)),f8(x7782),f8(f1(x7783))),f5(f8(x7781),f8(x7782),f8(x7783)))), % 59.52/59.58 inference(scs_inference,[],[775,2])). % 59.52/59.58 cnf(779,plain, % 59.52/59.58 (E(f5(f8(x7791),f8(x7792),f8(x7793)),f5(f8(f1(f1(x7791))),f8(x7792),f8(x7793)))), % 59.52/59.58 inference(scs_inference,[],[775,736,2,3])). % 59.52/59.58 cnf(782,plain, % 59.52/59.58 (E(f5(f8(f1(f1(x7821))),f8(x7822),f8(x7823)),f5(f8(x7821),f8(x7822),f8(x7823)))), % 59.52/59.58 inference(scs_inference,[],[779,2])). % 59.52/59.58 cnf(783,plain, % 59.52/59.58 (E(f5(f8(f1(f1(x7831))),f8(x7832),f8(f1(x7833))),f5(f8(x7831),f8(f1(x7832)),f8(f1(f1(x7833)))))), % 59.52/59.58 inference(scs_inference,[],[778,779,774,2,3])). % 59.52/59.58 cnf(787,plain, % 59.52/59.58 (E(f5(f8(x7871),f8(f1(x7872)),f8(f1(f1(x7873)))),f5(f8(f1(f1(x7871))),f8(x7872),f8(f1(x7873))))), % 59.52/59.58 inference(scs_inference,[],[783,2])). % 59.52/59.58 cnf(788,plain, % 59.52/59.58 (E(f5(f8(f1(f1(f1(x7881)))),f8(f1(x7882)),f8(f1(f1(x7883)))),f5(f8(f1(x7881)),f8(x7882),f8(x7883)))), % 59.52/59.58 inference(scs_inference,[],[782,783,748,2,3])). % 59.52/59.58 cnf(791,plain, % 59.52/59.58 (E(f5(f8(f1(x7911)),f8(x7912),f8(x7913)),f5(f8(f1(f1(f1(x7911)))),f8(f1(x7912)),f8(f1(f1(x7913)))))), % 59.52/59.58 inference(scs_inference,[],[788,2])). % 59.52/59.58 cnf(792,plain, % 59.52/59.58 (E(f5(f8(f1(x7921)),f8(f1(f1(x7922))),f8(f1(f1(f1(x7923))))),f5(f8(f1(x7921)),f8(x7922),f8(x7923)))), % 59.52/59.58 inference(scs_inference,[],[788,787,2,3])). % 59.52/59.58 cnf(795,plain, % 59.52/59.58 (E(f5(f8(f1(x7951)),f8(x7952),f8(x7953)),f5(f8(f1(x7951)),f8(f1(f1(x7952))),f8(f1(f1(f1(x7953))))))), % 59.52/59.58 inference(scs_inference,[],[792,2])). % 59.52/59.58 cnf(796,plain, % 59.52/59.58 (E(f5(f8(f1(x7961)),f8(f1(x7962)),f8(f1(x7963))),f5(f8(f1(f1(f1(x7961)))),f8(x7962),f8(x7963)))), % 59.52/59.58 inference(scs_inference,[],[792,791,2,3])). % 59.52/59.58 cnf(800,plain, % 59.52/59.58 (E(f5(f8(f1(f1(f1(x8001)))),f8(x8002),f8(x8003)),f5(f8(f1(x8001)),f8(f1(x8002)),f8(f1(x8003))))), % 59.52/59.58 inference(scs_inference,[],[796,2])). % 59.52/59.58 cnf(801,plain, % 59.52/59.58 (E(f5(f8(f1(x8011)),f8(f1(f1(x8012))),f8(f1(x8013))),f5(f8(x8011),f8(x8012),f8(x8013)))), % 59.52/59.58 inference(scs_inference,[],[796,760,2,3])). % 59.52/59.58 cnf(804,plain, % 59.52/59.58 (E(f5(f8(x8041),f8(x8042),f8(x8043)),f5(f8(f1(x8041)),f8(f1(f1(x8042))),f8(f1(x8043))))), % 59.52/59.58 inference(scs_inference,[],[801,2])). % 59.52/59.58 cnf(805,plain, % 59.52/59.58 (E(f5(f8(f1(x8051)),f8(f1(f1(x8052))),f8(f1(x8053))),f5(f8(f1(f1(x8051))),f8(x8052),f8(x8053)))), % 59.52/59.58 inference(scs_inference,[],[801,779,2,3])). % 59.52/59.58 cnf(808,plain, % 59.52/59.58 (E(f5(f8(f1(f1(x8081))),f8(x8082),f8(x8083)),f5(f8(f1(x8081)),f8(f1(f1(x8082))),f8(f1(x8083))))), % 59.52/59.58 inference(scs_inference,[],[805,2])). % 59.52/59.58 cnf(809,plain, % 59.52/59.58 (E(f5(f8(f1(x8091)),f8(f1(f1(x8092))),f8(f1(f1(x8093)))),f5(f8(f1(x8091)),f8(x8092),f8(x8093)))), % 59.52/59.58 inference(scs_inference,[],[805,778,2,3])). % 59.52/59.58 cnf(813,plain, % 59.52/59.58 (E(f5(f8(f1(x8131)),f8(x8132),f8(x8133)),f5(f8(f1(x8131)),f8(f1(f1(x8132))),f8(f1(f1(x8133)))))), % 59.52/59.58 inference(scs_inference,[],[809,2])). % 59.52/59.58 cnf(818,plain, % 59.52/59.58 (E(f11(x8181,f8(f1(x8182))),f11(x8181,f8(x8182)))), % 59.52/59.58 inference(scs_inference,[],[474,2])). % 59.52/59.58 cnf(819,plain, % 59.52/59.58 (E(f5(f8(f1(f1(f1(x8191)))),f8(x8192),f8(f1(x8193))),f5(f8(f1(f1(x8191))),f8(f1(x8192)),f8(x8193)))), % 59.52/59.58 inference(scs_inference,[],[800,744,474,2,3])). % 59.52/59.58 cnf(823,plain, % 59.52/59.58 (E(f5(f8(f1(f1(x8231))),f8(f1(x8232)),f8(x8233)),f5(f8(f1(f1(f1(x8231)))),f8(x8232),f8(f1(x8233))))), % 59.52/59.58 inference(scs_inference,[],[819,2])). % 59.52/59.58 cnf(824,plain, % 59.52/59.58 (E(f5(f8(f1(f1(x8241))),f8(x8242),f8(x8243)),f5(f8(f1(f1(x8241))),f8(f1(f1(f1(x8242)))),f8(x8243)))), % 59.52/59.58 inference(scs_inference,[],[819,804,2,3])). % 59.52/59.58 cnf(827,plain, % 59.52/59.58 (E(f5(f8(f1(f1(x8271))),f8(f1(f1(f1(x8272)))),f8(x8273)),f5(f8(f1(f1(x8271))),f8(x8272),f8(x8273)))), % 59.52/59.58 inference(scs_inference,[],[824,2])). % 59.52/59.58 cnf(828,plain, % 59.52/59.58 (E(f5(f8(f1(f1(x8281))),f8(x8282),f8(x8283)),f5(f8(x8281),f8(f1(f1(f1(x8282)))),f8(x8283)))), % 59.52/59.58 inference(scs_inference,[],[824,782,2,3])). % 59.52/59.58 cnf(831,plain, % 59.52/59.58 (E(f5(f8(x8311),f8(f1(f1(f1(x8312)))),f8(x8313)),f5(f8(f1(f1(x8311))),f8(x8312),f8(x8313)))), % 59.52/59.58 inference(scs_inference,[],[828,2])). % 59.52/59.58 cnf(832,plain, % 59.52/59.58 (E(f12(f12(x8321,f8(x8322)),f8(x8323)),f12(f12(x8321,f8(f1(f1(f1(x8322))))),f8(f1(x8323))))), % 59.52/59.58 inference(scs_inference,[],[105,828,674,2,3])). % 59.52/59.58 cnf(837,plain, % 59.52/59.58 (E(f5(f8(f1(f1(x8371))),f8(f1(f1(f1(x8372)))),f8(x8373)),f5(f8(f1(x8371)),f8(x8372),f8(f1(x8373))))), % 59.52/59.58 inference(scs_inference,[],[827,832,740,2,3])). % 59.52/59.58 cnf(840,plain, % 59.52/59.58 (E(f5(f8(f1(x8401)),f8(x8402),f8(f1(x8403))),f5(f8(f1(f1(x8401))),f8(f1(f1(f1(x8402)))),f8(x8403)))), % 59.52/59.58 inference(scs_inference,[],[837,2])). % 59.52/59.58 cnf(841,plain, % 59.52/59.58 (E(f5(f8(x8411),f8(f1(f1(f1(x8412)))),f8(x8413)),f5(f8(f1(x8411)),f8(f1(f1(x8412))),f8(f1(x8413))))), % 59.52/59.58 inference(scs_inference,[],[831,808,837,2,3])). % 59.52/59.58 cnf(844,plain, % 59.52/59.58 (E(f5(f8(f1(x8441)),f8(f1(f1(x8442))),f8(f1(x8443))),f5(f8(x8441),f8(f1(f1(f1(x8442)))),f8(x8443)))), % 59.52/59.58 inference(scs_inference,[],[841,2])). % 59.52/59.58 cnf(845,plain, % 59.52/59.58 (E(f5(f8(f1(x8451)),f8(x8452),f8(f1(x8453))),f5(f8(f1(f1(f1(x8451)))),f8(f1(f1(x8452))),f8(f1(x8453))))), % 59.52/59.58 inference(scs_inference,[],[840,823,841,2,3])). % 59.52/59.58 cnf(847,plain, % 59.52/59.58 (E(f5(f8(f1(f1(f1(x8471)))),f8(f1(f1(x8472))),f8(f1(x8473))),f5(f8(f1(x8471)),f8(x8472),f8(f1(x8473))))), % 59.52/59.58 inference(scs_inference,[],[845,2])). % 59.52/59.58 cnf(848,plain, % 59.52/59.58 (E(f11(f9(f15(f8(f1(x8481)))),f8(f1(x8482))),f11(f9(f15(f8(x8481))),f8(x8482)))), % 59.52/59.58 inference(scs_inference,[],[818,845,197,2,3])). % 59.52/59.58 cnf(853,plain, % 59.52/59.58 (E(f11(f9(f15(f8(f1(x8531)))),f8(f1(f1(x8532)))),f11(f9(f15(f8(x8531))),f8(x8532)))), % 59.52/59.58 inference(scs_inference,[],[848,818,2,3])). % 59.52/59.58 cnf(857,plain, % 59.52/59.58 (E(f12(f8(f1(x8571)),f8(x8572)),f12(f8(f1(x8571)),f8(f1(f1(x8572)))))), % 59.52/59.58 inference(scs_inference,[],[765,853,576,2,3])). % 59.52/59.58 cnf(859,plain, % 59.52/59.58 (E(f12(f8(f1(x8591)),f8(f1(f1(x8592)))),f12(f8(f1(x8591)),f8(x8592)))), % 59.52/59.58 inference(scs_inference,[],[857,2])). % 59.52/59.58 cnf(860,plain, % 59.52/59.58 (E(f12(f8(f1(f1(x8601))),f8(f1(x8602))),f12(f8(x8601),f8(x8602)))), % 59.52/59.58 inference(scs_inference,[],[857,759,2,3])). % 59.52/59.58 cnf(863,plain, % 59.52/59.58 (E(f12(f8(x8631),f8(x8632)),f12(f8(f1(f1(x8631))),f8(f1(x8632))))), % 59.52/59.58 inference(scs_inference,[],[860,2])). % 59.52/59.58 cnf(864,plain, % 59.52/59.58 (E(f11(f8(f1(x8641)),f8(f1(f1(f1(x8642))))),f11(f8(f1(x8641)),f8(x8642)))), % 59.52/59.58 inference(scs_inference,[],[655,860,480,2,3])). % 59.52/59.58 cnf(867,plain, % 59.52/59.58 (E(f11(f8(f1(x8671)),f8(x8672)),f11(f8(f1(x8671)),f8(f1(f1(f1(x8672))))))), % 59.52/59.58 inference(scs_inference,[],[864,2])). % 59.52/59.58 cnf(868,plain, % 59.52/59.58 (E(f12(f8(x8681),f8(f1(x8682))),f12(f8(f1(f1(x8681))),f8(x8682)))), % 59.52/59.58 inference(scs_inference,[],[859,864,863,2,3])). % 59.52/59.58 cnf(872,plain, % 59.52/59.58 (E(f12(f8(f1(f1(x8721))),f8(x8722)),f12(f8(x8721),f8(f1(x8722))))), % 59.52/59.58 inference(scs_inference,[],[868,2])). % 59.52/59.58 cnf(873,plain, % 59.52/59.58 (E(f11(f8(f1(f1(x8731))),f8(x8732)),f11(f8(x8731),f8(f1(f1(x8732)))))), % 59.52/59.58 inference(scs_inference,[],[868,660,514,2,3])). % 59.52/59.58 cnf(877,plain, % 59.52/59.58 (E(f11(f8(x8771),f8(f1(f1(x8772)))),f11(f8(f1(f1(x8771))),f8(x8772)))), % 59.52/59.58 inference(scs_inference,[],[873,2])). % 59.52/59.58 cnf(878,plain, % 59.52/59.58 (E(f12(f8(f1(f1(f1(x8781)))),f8(f1(f1(x8782)))),f12(f8(x8781),f8(x8782)))), % 59.52/59.58 inference(scs_inference,[],[872,873,577,2,3])). % 59.52/59.58 cnf(881,plain, % 59.52/59.58 (E(f12(f8(x8811),f8(x8812)),f12(f8(f1(f1(f1(x8811)))),f8(f1(f1(x8812)))))), % 59.52/59.58 inference(scs_inference,[],[878,2])). % 59.52/59.58 cnf(882,plain, % 59.52/59.58 (E(f11(f8(x8821),f8(f1(f1(f1(x8822))))),f11(f8(f1(x8821)),f8(x8822)))), % 59.52/59.58 inference(scs_inference,[],[877,878,503,2,3])). % 59.52/59.58 cnf(886,plain, % 59.52/59.58 (E(f11(f8(f1(x8861)),f8(x8862)),f11(f8(x8861),f8(f1(f1(f1(x8862))))))), % 59.52/59.58 inference(scs_inference,[],[882,2])). % 59.52/59.58 cnf(887,plain, % 59.52/59.58 (E(f12(f8(f1(x8871)),f8(x8872)),f12(f8(f1(f1(f1(x8871)))),f8(f1(f1(x8872)))))), % 59.52/59.58 inference(scs_inference,[],[882,881,765,2,3])). % 59.52/59.58 cnf(891,plain, % 59.52/59.58 (E(f11(f8(f1(f1(x8911))),f8(x8912)),f11(f8(x8911),f8(f1(f1(f1(x8912))))))), % 59.52/59.58 inference(scs_inference,[],[887,867,642,2,3])). % 59.52/59.58 cnf(895,plain, % 59.52/59.58 (E(f11(f8(x8951),f8(f1(f1(f1(x8952))))),f11(f8(f1(f1(x8951))),f8(x8952)))), % 59.52/59.58 inference(scs_inference,[],[891,2])). % 59.52/59.58 cnf(896,plain, % 59.52/59.58 (E(f11(f8(f1(x8961)),f8(x8962)),f11(f8(x8961),f8(f1(x8962))))), % 59.52/59.58 inference(scs_inference,[],[886,891,643,2,3])). % 59.52/59.58 cnf(899,plain, % 59.52/59.58 (E(f11(f8(x8991),f8(f1(x8992))),f11(f8(f1(x8991)),f8(x8992)))), % 59.52/59.58 inference(scs_inference,[],[896,2])). % 59.52/59.58 cnf(900,plain, % 59.52/59.58 (E(f11(f8(f1(x9001)),f8(f1(f1(x9002)))),f11(f8(f1(f1(x9001))),f8(x9002)))), % 59.52/59.58 inference(scs_inference,[],[895,896,2,3])). % 59.52/59.58 cnf(904,plain, % 59.52/59.58 (E(f11(f8(f1(f1(x9041))),f8(x9042)),f11(f8(f1(x9041)),f8(f1(f1(x9042)))))), % 59.52/59.58 inference(scs_inference,[],[900,2])). % 59.52/59.58 cnf(905,plain, % 59.52/59.58 (E(f11(f8(x9051),f8(f1(f1(f1(f1(x9052)))))),f11(f8(x9051),f8(x9052)))), % 59.52/59.58 inference(scs_inference,[],[899,900,656,2,3])). % 59.52/59.58 cnf(910,plain, % 59.52/59.58 (E(f11(f8(f1(f1(x9101))),f8(f1(f1(x9102)))),f11(f8(f1(x9101)),f8(x9102)))), % 59.52/59.58 inference(scs_inference,[],[905,904,2,3])). % 59.52/59.58 cnf(914,plain, % 59.52/59.58 (E(f11(f8(f1(x9141)),f8(x9142)),f11(f8(f1(f1(x9141))),f8(f1(f1(x9142)))))), % 59.52/59.58 inference(scs_inference,[],[910,2])). % 59.52/59.58 cnf(915,plain, % 59.52/59.58 (E(f11(f8(f1(f1(f1(x9151)))),f8(f1(f1(x9152)))),f11(f8(x9151),f8(x9152)))), % 59.52/59.58 inference(scs_inference,[],[910,642,2,3])). % 59.52/59.58 cnf(918,plain, % 59.52/59.58 (E(f11(f8(x9181),f8(x9182)),f11(f8(f1(f1(f1(x9181)))),f8(f1(f1(x9182)))))), % 59.52/59.58 inference(scs_inference,[],[915,2])). % 59.52/59.58 cnf(919,plain, % 59.52/59.58 (E(f5(f8(f1(f1(x9191))),f8(f1(f1(x9192))),f8(f1(x9193))),f5(f8(x9191),f8(f1(f1(x9192))),f8(x9193)))), % 59.52/59.58 inference(scs_inference,[],[844,915,705,2,3])). % 59.52/59.58 cnf(923,plain, % 59.52/59.58 (E(f5(f8(x9231),f8(f1(f1(x9232))),f8(x9233)),f5(f8(f1(f1(x9231))),f8(f1(f1(x9232))),f8(f1(x9233))))), % 59.52/59.58 inference(scs_inference,[],[919,2])). % 59.52/59.58 cnf(924,plain, % 59.52/59.58 (E(f5(f8(f1(f1(x9241))),f8(f1(f1(f1(x9242)))),f8(f1(x9243))),f5(f8(f1(f1(x9241))),f8(x9242),f8(x9243)))), % 59.52/59.58 inference(scs_inference,[],[919,831,2,3])). % 59.52/59.58 cnf(928,plain, % 59.52/59.58 (E(f5(f8(f1(f1(x9281))),f8(x9282),f8(x9283)),f5(f8(f1(f1(x9281))),f8(f1(f1(f1(x9282)))),f8(f1(x9283))))), % 59.52/59.58 inference(scs_inference,[],[924,2])). % 59.52/59.58 cnf(929,plain, % 59.52/59.58 (E(f11(f8(f1(x9291)),f8(x9292)),f11(f8(f1(f1(f1(f1(x9291))))),f8(x9292)))), % 59.52/59.58 inference(scs_inference,[],[924,914,877,2,3])). % 59.52/59.58 cnf(932,plain, % 59.52/59.58 (E(f11(f8(f1(f1(f1(f1(x9321))))),f8(x9322)),f11(f8(f1(x9321)),f8(x9322)))), % 59.52/59.58 inference(scs_inference,[],[929,2])). % 59.52/59.58 cnf(933,plain, % 59.52/59.58 (E(f5(f8(f1(x9331)),f8(f1(f1(x9332))),f8(x9333)),f5(f8(f1(x9331)),f8(x9332),f8(f1(x9333))))), % 59.52/59.58 inference(scs_inference,[],[929,847,923,2,3])). % 59.52/59.58 cnf(937,plain, % 59.52/59.58 (E(f5(f8(f1(x9371)),f8(x9372),f8(f1(x9373))),f5(f8(f1(x9371)),f8(f1(f1(x9372))),f8(x9373)))), % 59.52/59.58 inference(scs_inference,[],[933,2])). % 59.52/59.58 cnf(938,plain, % 59.52/59.58 (E(f5(f8(f1(f1(x9381))),f8(x9382),f8(f1(f1(x9383)))),f5(f8(f1(f1(x9381))),f8(f1(f1(x9382))),f8(x9383)))), % 59.52/59.58 inference(scs_inference,[],[928,933,752,2,3])). % 59.52/59.58 cnf(942,plain, % 59.52/59.58 (E(f5(f8(f1(f1(x9421))),f8(f1(f1(x9422))),f8(x9423)),f5(f8(f1(f1(x9421))),f8(x9422),f8(f1(f1(x9423)))))), % 59.52/59.58 inference(scs_inference,[],[938,2])). % 59.52/59.58 cnf(943,plain, % 59.52/59.58 (E(f5(f8(f1(x9431)),f8(x9432),f8(f1(f1(f1(x9433))))),f5(f8(f1(x9431)),f8(x9432),f8(x9433)))), % 59.52/59.58 inference(scs_inference,[],[937,938,809,2,3])). % 59.52/59.58 cnf(948,plain, % 59.52/59.58 (E(f5(f8(f1(f1(x9481))),f8(f1(x9482)),f8(f1(f1(f1(x9483))))),f5(f8(x9481),f8(x9482),f8(x9483)))), % 59.52/59.58 inference(scs_inference,[],[943,735,2,3])). % 59.52/59.58 cnf(953,plain, % 59.52/59.58 (E(f5(f8(f1(f1(x9531))),f8(x9532),f8(f1(x9533))),f5(f8(x9531),f8(f1(x9532)),f8(x9533)))), % 59.52/59.58 inference(scs_inference,[],[948,813,2,3])). % 59.52/59.58 cnf(957,plain, % 59.52/59.58 (E(f5(f8(x9571),f8(f1(x9572)),f8(x9573)),f5(f8(f1(f1(x9571))),f8(x9572),f8(f1(x9573))))), % 59.52/59.58 inference(scs_inference,[],[953,2])). % 59.52/59.58 cnf(958,plain, % 59.52/59.58 (E(f5(f8(f1(f1(x9581))),f8(f1(f1(x9582))),f8(x9583)),f5(f8(x9581),f8(f1(x9582)),f8(f1(x9583))))), % 59.52/59.58 inference(scs_inference,[],[953,942,2,3])). % 59.52/59.58 cnf(961,plain, % 59.52/59.58 (E(f5(f8(x9611),f8(f1(x9612)),f8(f1(x9613))),f5(f8(f1(f1(x9611))),f8(f1(f1(x9612))),f8(x9613)))), % 59.52/59.58 inference(scs_inference,[],[958,2])). % 59.52/59.58 cnf(962,plain, % 59.52/59.58 (E(f5(f8(x9621),f8(f1(f1(f1(x9622)))),f8(x9623)),f5(f8(x9621),f8(f1(x9622)),f8(f1(f1(x9623)))))), % 59.52/59.58 inference(scs_inference,[],[957,958,2,3])). % 59.52/59.58 cnf(966,plain, % 59.52/59.58 (E(f5(f8(x9661),f8(f1(x9662)),f8(f1(f1(x9663)))),f5(f8(x9661),f8(f1(f1(f1(x9662)))),f8(x9663)))), % 59.52/59.58 inference(scs_inference,[],[962,2])). % 59.52/59.58 cnf(967,plain, % 59.52/59.58 (E(f5(f8(x9671),f8(f1(f1(x9672))),f8(f1(x9673))),f5(f8(f1(f1(x9671))),f8(x9672),f8(x9673)))), % 59.52/59.58 inference(scs_inference,[],[961,962,827,2,3])). % 59.52/59.58 cnf(971,plain, % 59.52/59.58 (E(f5(f8(f1(f1(x9711))),f8(x9712),f8(x9713)),f5(f8(x9711),f8(f1(f1(x9712))),f8(f1(x9713))))), % 59.52/59.58 inference(scs_inference,[],[967,2])). % 59.52/59.58 cnf(972,plain, % 59.52/59.58 (E(f5(f8(x9721),f8(f1(x9722)),f8(f1(f1(x9723)))),f5(f8(f1(x9721)),f8(f1(f1(x9722))),f8(f1(x9723))))), % 59.52/59.58 inference(scs_inference,[],[966,967,841,2,3])). % 59.52/59.58 cnf(975,plain, % 59.52/59.58 (E(f5(f8(f1(x9751)),f8(f1(f1(x9752))),f8(f1(x9753))),f5(f8(x9751),f8(f1(x9752)),f8(f1(f1(x9753)))))), % 59.52/59.58 inference(scs_inference,[],[972,2])). % 59.52/59.58 cnf(976,plain, % 59.52/59.58 (E(f5(f8(f1(f1(x9761))),f8(x9762),f8(f1(x9763))),f5(f8(f1(x9761)),f8(f1(f1(f1(x9762)))),f8(f1(x9763))))), % 59.52/59.58 inference(scs_inference,[],[971,972,2,3])). % 59.52/59.58 cnf(980,plain, % 59.52/59.58 (E(f5(f8(f1(x9801)),f8(f1(f1(f1(x9802)))),f8(f1(x9803))),f5(f8(f1(f1(x9801))),f8(x9802),f8(f1(x9803))))), % 59.52/59.58 inference(scs_inference,[],[976,2])). % 59.52/59.58 cnf(981,plain, % 59.52/59.58 (E(f5(f8(f1(f1(x9811))),f8(x9812),f8(f1(x9813))),f5(f8(f1(f1(f1(x9811)))),f8(f1(x9812)),f8(x9813)))), % 59.52/59.58 inference(scs_inference,[],[976,967,2,3])). % 59.52/59.58 cnf(984,plain, % 59.52/59.58 (E(f5(f8(f1(f1(f1(x9841)))),f8(f1(x9842)),f8(x9843)),f5(f8(f1(f1(x9841))),f8(x9842),f8(f1(x9843))))), % 59.52/59.58 inference(scs_inference,[],[981,2])). % 59.52/59.58 cnf(985,plain, % 59.52/59.58 (E(f5(f8(f1(f1(x9851))),f8(x9852),f8(f1(x9853))),f5(f8(f1(x9851)),f8(f1(f1(x9852))),f8(f1(x9853))))), % 59.52/59.58 inference(scs_inference,[],[981,800,2,3])). % 59.52/59.58 cnf(988,plain, % 59.52/59.58 (E(f5(f8(f1(x9881)),f8(f1(f1(x9882))),f8(f1(x9883))),f5(f8(f1(f1(x9881))),f8(x9882),f8(f1(x9883))))), % 59.52/59.58 inference(scs_inference,[],[985,2])). % 59.52/59.58 cnf(989,plain, % 59.52/59.58 (E(f5(f8(f1(x9891)),f8(f1(f1(f1(f1(x9892))))),f8(f1(x9893))),f5(f8(x9891),f8(x9892),f8(x9893)))), % 59.52/59.58 inference(scs_inference,[],[980,985,557,2,3])). % 59.52/59.58 cnf(992,plain, % 59.52/59.58 (E(f5(f8(x9921),f8(x9922),f8(x9923)),f5(f8(f1(x9921)),f8(f1(f1(f1(f1(x9922))))),f8(f1(x9923))))), % 59.52/59.58 inference(scs_inference,[],[989,2])). % 59.52/59.58 cnf(993,plain, % 59.52/59.58 (E(f6(f6(x9931,f8(f1(x9932))),f8(x9933)),f6(f6(x9931,f8(x9932)),f8(f1(x9933))))), % 59.52/59.58 inference(scs_inference,[],[102,989,450,2,3])). % 59.52/59.58 cnf(996,plain, % 59.52/59.58 (E(f5(f8(f1(x9961)),x9962,x9963),f5(f8(x9961),x9962,x9963))), % 59.52/59.58 inference(scs_inference,[],[36,2,11])). % 59.52/59.58 cnf(997,plain, % 59.52/59.58 (E(f6(f6(x9971,f8(x9972)),f8(f1(x9973))),f6(f6(x9971,f8(f1(x9972))),f8(x9973)))), % 59.52/59.58 inference(scs_inference,[],[993,2])). % 59.52/59.58 cnf(998,plain, % 59.52/59.58 (E(f5(f8(f1(f1(f1(x9981)))),f8(f1(x9982)),f8(x9983)),f5(f8(f1(x9981)),f8(x9982),f8(f1(x9983))))), % 59.52/59.58 inference(scs_inference,[],[996,984,993,2,3])). % 59.52/59.58 cnf(1000,plain, % 59.52/59.58 (E(f5(x10001,f8(f1(x10002)),x10003),f5(x10001,f8(x10002),x10003))), % 59.52/59.58 inference(scs_inference,[],[36,2,12])). % 59.52/59.58 cnf(1001,plain, % 59.52/59.58 (E(f5(f8(f1(x10011)),f8(x10012),f8(f1(x10013))),f5(f8(f1(f1(f1(x10011)))),f8(f1(x10012)),f8(x10013)))), % 59.52/59.58 inference(scs_inference,[],[998,2])). % 59.52/59.58 cnf(1002,plain, % 59.52/59.58 (E(f6(f6(x10021,f8(x10022)),f8(f1(x10023))),f6(f6(x10021,f8(f1(f1(x10022)))),f8(x10023)))), % 59.52/59.58 inference(scs_inference,[],[103,997,998,2,3])). % 59.52/59.58 cnf(1005,plain, % 59.52/59.58 (E(f4(f8(f1(x10051)),x10052),f4(f8(x10051),x10052))), % 59.52/59.58 inference(scs_inference,[],[36,2,15])). % 59.52/59.58 cnf(1006,plain, % 59.52/59.58 (E(f6(f6(x10061,f8(f1(f1(x10062)))),f8(x10063)),f6(f6(x10061,f8(x10062)),f8(f1(x10063))))), % 59.52/59.58 inference(scs_inference,[],[1002,2])). % 59.52/59.58 cnf(1007,plain, % 59.52/59.58 (E(f5(f8(f1(x10071)),f8(x10072),f8(f1(x10073))),f5(f8(f1(f1(f1(x10071)))),f8(x10072),f8(x10073)))), % 59.52/59.58 inference(scs_inference,[],[1000,1001,1002,2,3])). % 59.52/59.58 cnf(1009,plain, % 59.52/59.58 (E(f4(x10091,f8(f1(x10092))),f4(x10091,f8(x10092)))), % 59.52/59.58 inference(scs_inference,[],[36,2,16])). % 59.52/59.58 cnf(1010,plain, % 59.52/59.58 (E(f5(f8(f1(f1(f1(x10101)))),f8(x10102),f8(x10103)),f5(f8(f1(x10101)),f8(x10102),f8(f1(x10103))))), % 59.52/59.58 inference(scs_inference,[],[1007,2])). % 59.52/59.58 cnf(1011,plain, % 59.52/59.58 (E(f6(f6(x10111,f8(f1(f1(f1(x10112))))),f8(x10113)),f6(f6(x10111,f8(x10112)),f8(f1(x10113))))), % 59.52/59.58 inference(scs_inference,[],[102,1007,1006,2,3])). % 59.52/59.58 cnf(1014,plain, % 59.52/59.58 (E(f6(f8(f1(x10141)),x10142),f6(f8(x10141),x10142))), % 59.52/59.58 inference(scs_inference,[],[36,2,17])). % 59.52/59.58 cnf(1016,plain, % 59.52/59.58 (E(f6(f8(f1(x10161)),f8(f1(f1(x10162)))),f6(f8(f1(f1(f1(x10161)))),f8(x10162)))), % 59.52/59.58 inference(scs_inference,[],[608,1014,1011,2,3])). % 59.52/59.58 cnf(1020,plain, % 59.52/59.58 (E(f6(f8(f1(f1(f1(x10201)))),f8(x10202)),f6(f8(f1(x10201)),f8(f1(f1(x10202)))))), % 59.52/59.58 inference(scs_inference,[],[1016,2])). % 59.52/59.58 cnf(1021,plain, % 59.52/59.58 (E(f5(f8(f1(f1(x10211))),f8(f1(f1(x10212))),f8(f1(x10213))),f5(f8(f1(x10211)),f8(x10212),f8(f1(f1(x10213)))))), % 59.52/59.58 inference(scs_inference,[],[1016,988,1010,2,3])). % 59.52/59.58 cnf(1024,plain, % 59.52/59.58 (E(f12(x10241,f8(f1(x10242))),f12(x10241,f8(x10242)))), % 59.52/59.58 inference(scs_inference,[],[36,2,20])). % 59.52/59.58 cnf(1025,plain, % 59.52/59.58 (E(f5(f8(f1(x10251)),f8(x10252),f8(f1(f1(x10253)))),f5(f8(f1(f1(x10251))),f8(f1(f1(x10252))),f8(f1(x10253))))), % 59.52/59.58 inference(scs_inference,[],[1021,2])). % 59.52/59.58 cnf(1026,plain, % 59.52/59.58 (E(f5(f8(x10261),f8(x10262),f8(x10263)),f5(f8(x10261),f8(f1(f1(f1(x10262)))),f8(f1(f1(x10263)))))), % 59.52/59.58 inference(scs_inference,[],[992,975,1021,2,3])). % 59.52/59.58 cnf(1029,plain, % 59.52/59.58 (E(f5(f8(x10291),f8(f1(f1(f1(x10292)))),f8(f1(f1(x10293)))),f5(f8(x10291),f8(x10292),f8(x10293)))), % 59.52/59.58 inference(scs_inference,[],[1026,2])). % 59.52/59.58 cnf(1030,plain, % 59.52/59.58 (E(f4(f8(f1(x10301)),f8(x10302)),f4(f8(f1(f1(x10301))),f8(f1(f1(f1(x10302))))))), % 59.52/59.58 inference(scs_inference,[],[1005,1026,598,2,3])). % 59.52/59.58 cnf(1035,plain, % 59.52/59.58 (E(f5(f8(f1(x10351)),f8(f1(x10352)),f8(f1(f1(f1(x10353))))),f5(f8(f1(f1(x10351))),f8(x10352),f8(x10353)))), % 59.52/59.58 inference(scs_inference,[],[1029,1025,1030,2,3])). % 59.52/59.58 cnf(1040,plain, % 59.52/59.58 (E(f4(f8(f1(x10401)),f8(f1(f1(f1(x10402))))),f4(f8(x10401),f8(x10402)))), % 59.52/59.58 inference(scs_inference,[],[1009,1035,589,2,3])). % 59.52/59.58 cnf(1043,plain, % 59.52/59.58 (E(f4(f8(x10431),f8(x10432)),f4(f8(f1(x10431)),f8(f1(f1(f1(x10432))))))), % 59.52/59.58 inference(scs_inference,[],[1040,2])). % 59.52/59.58 cnf(1044,plain, % 59.52/59.58 (E(f5(f8(f1(x10441)),f8(x10442),f8(x10443)),f5(f8(f1(f1(f1(x10441)))),f8(f1(f1(x10442))),f8(x10443)))), % 59.52/59.58 inference(scs_inference,[],[1040,795,747,2,3])). % 59.52/59.58 cnf(1046,plain, % 59.52/59.58 (E(f5(f8(f1(f1(f1(x10461)))),f8(f1(f1(x10462))),f8(x10463)),f5(f8(f1(x10461)),f8(x10462),f8(x10463)))), % 59.52/59.58 inference(scs_inference,[],[1044,2])). % 59.52/59.58 cnf(1047,plain, % 59.52/59.58 (E(f4(f8(f1(x10471)),f8(f1(x10472))),f4(f8(f1(x10471)),f8(f1(f1(f1(x10472))))))), % 59.52/59.58 inference(scs_inference,[],[1044,1043,552,2,3])). % 59.52/59.58 cnf(1050,plain, % 59.52/59.58 (E(f4(f8(f1(x10501)),f8(f1(f1(f1(x10502))))),f4(f8(f1(x10501)),f8(f1(x10502))))), % 59.52/59.58 inference(scs_inference,[],[1047,2])). % 59.52/59.58 cnf(1051,plain, % 59.52/59.58 (E(f4(f8(f1(f1(x10511))),f8(f1(x10512))),f4(f8(x10511),f8(x10512)))), % 59.52/59.58 inference(scs_inference,[],[1047,595,2,3])). % 59.52/59.58 cnf(1055,plain, % 59.52/59.58 (E(f4(f8(x10551),f8(x10552)),f4(f8(f1(f1(x10551))),f8(f1(x10552))))), % 59.52/59.58 inference(scs_inference,[],[1051,2])). % 59.52/59.58 cnf(1056,plain, % 59.52/59.58 (E(f5(f8(f1(f1(f1(x10561)))),f8(f1(f1(x10562))),f8(x10563)),f5(f8(x10561),f8(x10562),f8(x10563)))), % 59.52/59.58 inference(scs_inference,[],[1046,1051,996,2,3])). % 59.52/59.58 cnf(1059,plain, % 59.52/59.58 (E(f5(f8(x10591),f8(x10592),f8(x10593)),f5(f8(f1(f1(f1(x10591)))),f8(f1(f1(x10592))),f8(x10593)))), % 59.52/59.58 inference(scs_inference,[],[1056,2])). % 59.52/59.58 cnf(1060,plain, % 59.52/59.58 (E(f4(f8(x10601),f8(f1(f1(x10602)))),f4(f8(f1(f1(x10601))),f8(f1(x10602))))), % 59.52/59.58 inference(scs_inference,[],[1056,1050,1055,2,3])). % 59.52/59.58 cnf(1064,plain, % 59.52/59.58 (E(f4(f8(f1(f1(x10641))),f8(f1(x10642))),f4(f8(x10641),f8(f1(f1(x10642)))))), % 59.52/59.58 inference(scs_inference,[],[1060,2])). % 59.52/59.58 cnf(1065,plain, % 59.52/59.58 (E(f4(f8(f1(x10651)),f8(f1(f1(x10652)))),f4(f8(f1(f1(x10651))),f8(f1(x10652))))), % 59.52/59.58 inference(scs_inference,[],[1060,1005,2,3])). % 59.52/59.58 cnf(1069,plain, % 59.52/59.58 (E(f4(f8(f1(f1(x10691))),f8(f1(x10692))),f4(f8(f1(x10691)),f8(f1(f1(x10692)))))), % 59.52/59.58 inference(scs_inference,[],[1065,2])). % 59.52/59.58 cnf(1070,plain, % 59.52/59.58 (E(f5(f8(x10701),f8(x10702),f8(f1(x10703))),f5(f8(f1(f1(x10701))),f8(f1(f1(f1(x10702)))),f8(x10703)))), % 59.52/59.58 inference(scs_inference,[],[1059,1065,844,2,3])). % 59.52/59.58 cnf(1074,plain, % 59.52/59.58 (E(f5(f8(f1(f1(x10741))),f8(f1(f1(f1(x10742)))),f8(x10743)),f5(f8(x10741),f8(x10742),f8(f1(x10743))))), % 59.52/59.58 inference(scs_inference,[],[1070,2])). % 59.52/59.58 cnf(1075,plain, % 59.52/59.58 (E(f5(f8(x10751),f8(x10752),f8(f1(f1(x10753)))),f5(f8(f1(f1(x10751))),f8(x10752),f8(x10753)))), % 59.52/59.58 inference(scs_inference,[],[1070,924,2,3])). % 59.52/59.58 cnf(1079,plain, % 59.52/59.58 (E(f5(f8(f1(f1(x10791))),f8(x10792),f8(x10793)),f5(f8(x10791),f8(x10792),f8(f1(f1(x10793)))))), % 59.52/59.58 inference(scs_inference,[],[1075,2])). % 59.52/59.58 cnf(1080,plain, % 59.52/59.58 (E(f5(f8(x10801),f8(f1(f1(f1(x10802)))),f8(f1(f1(x10803)))),f5(f8(x10801),f8(x10802),f8(f1(x10803))))), % 59.52/59.58 inference(scs_inference,[],[1075,1074,2,3])). % 59.52/59.58 cnf(1084,plain, % 59.52/59.58 (E(f5(f8(x10841),f8(x10842),f8(f1(x10843))),f5(f8(x10841),f8(f1(f1(f1(x10842)))),f8(f1(f1(x10843)))))), % 59.52/59.58 inference(scs_inference,[],[1080,2])). % 59.52/59.58 cnf(1085,plain, % 59.52/59.58 (E(f4(f8(f1(f1(x10851))),f8(f1(x10852))),f4(f8(x10851),f8(f1(x10852))))), % 59.52/59.58 inference(scs_inference,[],[1080,1064,1009,2,3])). % 59.52/59.58 cnf(1088,plain, % 59.52/59.58 (E(f4(f8(x10881),f8(f1(x10882))),f4(f8(f1(f1(x10881))),f8(f1(x10882))))), % 59.52/59.58 inference(scs_inference,[],[1085,2])). % 59.52/59.58 cnf(1089,plain, % 59.52/59.58 (E(f4(f8(f1(f1(f1(x10891)))),f8(f1(x10892))),f4(f8(x10891),f8(f1(f1(x10892)))))), % 59.52/59.58 inference(scs_inference,[],[1085,1069,2,3])). % 59.52/59.58 cnf(1093,plain, % 59.52/59.58 (E(f4(f8(x10931),f8(f1(f1(x10932)))),f4(f8(f1(f1(f1(x10931)))),f8(f1(x10932))))), % 59.52/59.58 inference(scs_inference,[],[1089,2])). % 59.52/59.58 cnf(1094,plain, % 59.52/59.58 (E(f4(f8(f1(x10941)),f8(f1(x10942))),f4(f8(x10941),f8(f1(f1(x10942)))))), % 59.52/59.58 inference(scs_inference,[],[1088,1089,2,3])). % 59.52/59.58 cnf(1098,plain, % 59.52/59.58 (E(f4(f8(x10981),f8(f1(f1(x10982)))),f4(f8(f1(x10981)),f8(f1(x10982))))), % 59.52/59.58 inference(scs_inference,[],[1094,2])). % 59.52/59.58 cnf(1099,plain, % 59.52/59.58 (E(f5(f8(f1(f1(x10991))),f8(f1(x10992)),f8(x10993)),f5(f8(f1(f1(x10991))),f8(f1(f1(x10992))),f8(f1(x10993))))), % 59.52/59.58 inference(scs_inference,[],[1079,1094,961,2,3])). % 59.52/59.58 cnf(1103,plain, % 59.52/59.58 (E(f5(f8(f1(f1(x11031))),f8(f1(f1(x11032))),f8(f1(x11033))),f5(f8(f1(f1(x11031))),f8(f1(x11032)),f8(x11033)))), % 59.52/59.58 inference(scs_inference,[],[1099,2])). % 59.52/59.58 cnf(1104,plain, % 59.52/59.58 (E(f5(f8(f1(f1(x11041))),f8(f1(f1(f1(x11042)))),f8(x11043)),f5(f8(f1(x11041)),f8(x11042),f8(x11043)))), % 59.52/59.58 inference(scs_inference,[],[1099,989,2,3])). % 59.52/59.58 cnf(1108,plain, % 59.52/59.58 (E(f5(f8(f1(x11081)),f8(x11082),f8(x11083)),f5(f8(f1(f1(x11081))),f8(f1(f1(f1(x11082)))),f8(x11083)))), % 59.52/59.58 inference(scs_inference,[],[1104,2])). % 59.52/59.58 cnf(1109,plain, % 59.52/59.58 (E(f5(f8(f1(f1(x11091))),f8(f1(f1(x11092))),f8(f1(x11093))),f5(f8(f1(f1(x11091))),f8(x11092),f8(x11093)))), % 59.52/59.58 inference(scs_inference,[],[1103,1104,1000,2,3])). % 59.52/59.58 cnf(1112,plain, % 59.52/59.58 (E(f5(f8(f1(f1(x11121))),f8(x11122),f8(x11123)),f5(f8(f1(f1(x11121))),f8(f1(f1(x11122))),f8(f1(x11123))))), % 59.52/59.58 inference(scs_inference,[],[1109,2])). % 59.52/59.58 cnf(1113,plain, % 59.52/59.58 (E(f5(f8(f1(x11131)),f8(x11132),f8(f1(x11133))),f5(f8(f1(f1(x11131))),f8(f1(x11132)),f8(x11133)))), % 59.52/59.58 inference(scs_inference,[],[1108,1109,2,3])). % 59.52/59.58 cnf(1117,plain, % 59.52/59.58 (E(f5(f8(f1(f1(x11171))),f8(f1(x11172)),f8(x11173)),f5(f8(f1(x11171)),f8(x11172),f8(f1(x11173))))), % 59.52/59.58 inference(scs_inference,[],[1113,2])). % 59.52/59.58 cnf(1118,plain, % 59.52/59.58 (E(f5(f8(f1(x11181)),f8(x11182),f8(f1(x11183))),f5(f8(x11181),f8(f1(f1(f1(f1(x11182))))),f8(x11183)))), % 59.52/59.58 inference(scs_inference,[],[1113,828,2,3])). % 59.52/59.58 cnf(1121,plain, % 59.52/59.58 (E(f5(f8(x11211),f8(f1(f1(f1(f1(x11212))))),f8(x11213)),f5(f8(f1(x11211)),f8(x11212),f8(f1(x11213))))), % 59.52/59.58 inference(scs_inference,[],[1118,2])). % 59.52/59.58 cnf(1122,plain, % 59.52/59.58 (E(f5(f8(f1(x11221)),f8(x11222),f8(f1(f1(f1(x11223))))),f5(f8(x11221),f8(f1(x11222)),f8(x11223)))), % 59.52/59.58 inference(scs_inference,[],[1118,1029,2,3])). % 59.52/59.58 cnf(1126,plain, % 59.52/59.58 (E(f4(f8(x11261),f8(f1(f1(x11262)))),f4(f8(f1(x11261)),f8(x11262)))), % 59.52/59.58 inference(scs_inference,[],[1122,1093,1051,2,3])). % 59.52/59.58 cnf(1129,plain, % 59.52/59.58 (E(f4(f8(f1(x11291)),f8(x11292)),f4(f8(x11291),f8(f1(f1(x11292)))))), % 59.52/59.58 inference(scs_inference,[],[1126,2])). % 59.52/59.58 cnf(1130,plain, % 59.52/59.58 (E(f4(f8(x11301),f8(f1(f1(f1(x11302))))),f4(f8(f1(f1(x11301))),f8(x11302)))), % 59.52/59.58 inference(scs_inference,[],[1126,1098,2,3])). % 59.52/59.58 cnf(1134,plain, % 59.52/59.58 (E(f4(f8(f1(f1(x11341))),f8(x11342)),f4(f8(x11341),f8(f1(f1(f1(x11342))))))), % 59.52/59.58 inference(scs_inference,[],[1130,2])). % 59.52/59.58 cnf(1135,plain, % 59.52/59.58 (E(f4(f8(f1(x11351)),f8(f1(x11352))),f4(f8(f1(f1(x11351))),f8(x11352)))), % 59.52/59.58 inference(scs_inference,[],[1130,1129,2,3])). % 59.52/59.58 cnf(1139,plain, % 59.52/59.58 (E(f4(f8(f1(f1(x11391))),f8(x11392)),f4(f8(f1(x11391)),f8(f1(x11392))))), % 59.52/59.58 inference(scs_inference,[],[1135,2])). % 59.52/59.58 cnf(1140,plain, % 59.52/59.58 (E(f5(f8(f1(f1(f1(x11401)))),f8(x11402),f8(x11403)),f5(f8(x11401),f8(x11402),f8(f1(x11403))))), % 59.52/59.58 inference(scs_inference,[],[1135,1112,1056,2,3])). % 59.52/59.58 cnf(1144,plain, % 59.52/59.58 (E(f5(f8(x11441),f8(x11442),f8(f1(x11443))),f5(f8(f1(f1(f1(x11441)))),f8(x11442),f8(x11443)))), % 59.52/59.58 inference(scs_inference,[],[1140,2])). % 59.52/59.58 cnf(1145,plain, % 59.52/59.58 (E(f5(f8(f1(f1(x11451))),f8(f1(x11452)),f8(x11453)),f5(f8(f1(f1(x11451))),f8(f1(f1(f1(x11452)))),f8(x11453)))), % 59.52/59.58 inference(scs_inference,[],[1117,1140,840,2,3])). % 59.52/59.58 cnf(1148,plain, % 59.52/59.58 (E(f5(f8(f1(f1(x11481))),f8(f1(f1(f1(x11482)))),f8(x11483)),f5(f8(f1(f1(x11481))),f8(f1(x11482)),f8(x11483)))), % 59.52/59.58 inference(scs_inference,[],[1145,2])). % 59.52/59.58 cnf(1149,plain, % 59.52/59.58 (E(f5(f8(x11491),f8(x11492),f8(f1(f1(x11493)))),f5(f8(f1(f1(f1(x11491)))),f8(f1(f1(x11492))),f8(x11493)))), % 59.52/59.58 inference(scs_inference,[],[1144,1145,937,2,3])). % 59.52/59.58 cnf(1153,plain, % 59.52/59.58 (E(f5(f8(f1(f1(f1(x11531)))),f8(f1(f1(x11532))),f8(x11533)),f5(f8(x11531),f8(x11532),f8(f1(f1(x11533)))))), % 59.52/59.58 inference(scs_inference,[],[1149,2])). % 59.52/59.58 cnf(1154,plain, % 59.52/59.58 (E(f5(f8(x11541),f8(f1(x11542)),f8(f1(f1(x11543)))),f5(f8(f1(f1(f1(x11541)))),f8(f1(x11542)),f8(x11543)))), % 59.52/59.58 inference(scs_inference,[],[1148,1149,2,3])). % 59.52/59.58 cnf(1158,plain, % 59.52/59.58 (E(f5(f8(f1(f1(f1(x11581)))),f8(f1(x11582)),f8(x11583)),f5(f8(x11581),f8(f1(x11582)),f8(f1(f1(x11583)))))), % 59.52/59.58 inference(scs_inference,[],[1154,2])). % 59.52/59.58 cnf(1159,plain, % 59.52/59.58 (E(f5(f8(x11591),f8(f1(f1(x11592))),f8(f1(f1(x11593)))),f5(f8(x11591),f8(x11592),f8(f1(f1(x11593)))))), % 59.52/59.58 inference(scs_inference,[],[1154,1153,2,3])). % 59.52/59.58 cnf(1163,plain, % 59.52/59.58 (E(f5(f8(x11631),f8(x11632),f8(f1(f1(x11633)))),f5(f8(x11631),f8(f1(f1(x11632))),f8(f1(f1(x11633)))))), % 59.52/59.58 inference(scs_inference,[],[1159,2])). % 59.52/59.58 cnf(1164,plain, % 59.52/59.58 (E(f5(f8(x11641),f8(f1(x11642)),f8(f1(x11643))),f5(f8(f1(x11641)),f8(x11642),f8(f1(f1(f1(x11643))))))), % 59.52/59.58 inference(scs_inference,[],[1121,1084,1159,2,3])). % 59.52/59.58 cnf(1168,plain, % 59.52/59.58 (E(f5(f8(f1(x11681)),f8(x11682),f8(f1(f1(f1(x11683))))),f5(f8(x11681),f8(f1(x11682)),f8(f1(x11683))))), % 59.52/59.58 inference(scs_inference,[],[1164,2])). % 59.52/59.58 cnf(1169,plain, % 59.52/59.58 (E(f5(f8(f1(f1(f1(x11691)))),f8(f1(x11692)),f8(x11693)),f5(f8(x11691),f8(f1(f1(f1(x11692)))),f8(x11693)))), % 59.52/59.58 inference(scs_inference,[],[1158,1164,966,2,3])). % 59.52/59.58 cnf(1172,plain, % 59.52/59.58 (E(f5(f8(x11721),f8(f1(f1(f1(x11722)))),f8(x11723)),f5(f8(f1(f1(f1(x11721)))),f8(f1(x11722)),f8(x11723)))), % 59.52/59.58 inference(scs_inference,[],[1169,2])). % 59.52/59.58 cnf(1173,plain, % 59.52/59.58 (E(f4(f8(f1(f1(x11731))),f8(f1(f1(x11732)))),f4(f8(x11731),f8(x11732)))), % 59.52/59.58 inference(scs_inference,[],[1169,1139,1040,2,3])). % 59.52/59.58 cnf(1177,plain, % 59.52/59.58 (E(f4(f8(x11771),f8(x11772)),f4(f8(f1(f1(x11771))),f8(f1(f1(x11772)))))), % 59.52/59.58 inference(scs_inference,[],[1173,2])). % 59.52/59.58 cnf(1178,plain, % 59.52/59.58 (E(f4(f8(f1(f1(f1(f1(x11781))))),f8(x11782)),f4(f8(x11781),f8(f1(x11782))))), % 59.52/59.58 inference(scs_inference,[],[1173,1134,2,3])). % 59.52/59.58 cnf(1182,plain, % 59.52/59.58 (E(f4(f8(x11821),f8(f1(x11822))),f4(f8(f1(f1(f1(f1(x11821))))),f8(x11822)))), % 59.52/59.58 inference(scs_inference,[],[1178,2])). % 59.52/59.58 cnf(1183,plain, % 59.52/59.58 (E(f5(f8(x11831),f8(f1(f1(f1(f1(x11832))))),f8(x11833)),f5(f8(f1(x11831)),f8(x11832),f8(x11833)))), % 59.52/59.58 inference(scs_inference,[],[1172,1178,1046,2,3])). % 59.52/59.58 cnf(1187,plain, % 59.52/59.58 (E(f5(f8(f1(x11871)),f8(x11872),f8(x11873)),f5(f8(x11871),f8(f1(f1(f1(f1(x11872))))),f8(x11873)))), % 59.52/59.58 inference(scs_inference,[],[1183,2])). % 59.52/59.58 cnf(1188,plain, % 59.52/59.58 (E(f4(f8(x11881),f8(f1(x11882))),f4(f8(f1(f1(f1(x11881)))),f8(f1(x11882))))), % 59.52/59.58 inference(scs_inference,[],[1182,1183,1139,2,3])). % 59.52/59.58 cnf(1191,plain, % 59.52/59.58 (E(f4(f8(f1(f1(f1(x11911)))),f8(f1(x11912))),f4(f8(x11911),f8(f1(x11912))))), % 59.52/59.58 inference(scs_inference,[],[1188,2])). % 59.52/59.58 cnf(1192,plain, % 59.52/59.58 (E(f5(f8(f1(f1(f1(x11921)))),f8(x11922),f8(x11923)),f5(f8(f1(x11921)),f8(f1(x11922)),f8(x11923)))), % 59.52/59.59 inference(scs_inference,[],[1187,1188,1104,2,3])). % 59.52/59.59 cnf(1196,plain, % 59.52/59.59 (E(f5(f8(f1(x11961)),f8(f1(x11962)),f8(x11963)),f5(f8(f1(f1(f1(x11961)))),f8(x11962),f8(x11963)))), % 59.52/59.59 inference(scs_inference,[],[1192,2])). % 59.52/59.59 cnf(1197,plain, % 59.52/59.59 (E(f12(f9(f15(f8(f1(x11971)))),f8(f1(x11972))),f12(f9(f15(f8(x11971))),f8(x11972)))), % 59.52/59.59 inference(scs_inference,[],[1024,1192,223,2,3])). % 59.52/59.59 cnf(1202,plain, % 59.52/59.59 (E(f12(f9(f15(f8(f1(x12021)))),f8(f1(f1(x12022)))),f12(f9(f15(f8(x12021))),f8(x12022)))), % 59.52/59.59 inference(scs_inference,[],[1197,1024,2,3])). % 59.52/59.59 cnf(1206,plain, % 59.52/59.59 (E(f5(f8(f1(x12061)),f8(f1(f1(x12062))),f8(x12063)),f5(f8(x12061),f8(f1(f1(f1(x12062)))),f8(x12063)))), % 59.52/59.59 inference(scs_inference,[],[1196,1202,1169,2,3])). % 59.52/59.59 cnf(1209,plain, % 59.52/59.59 (E(f5(f8(x12091),f8(f1(f1(f1(x12092)))),f8(x12093)),f5(f8(f1(x12091)),f8(f1(f1(x12092))),f8(x12093)))), % 59.52/59.59 inference(scs_inference,[],[1206,2])). % 59.52/59.59 cnf(1210,plain, % 59.52/59.59 (E(f5(f8(f1(x12101)),f8(f1(f1(f1(x12102)))),f8(x12103)),f5(f8(f1(x12101)),f8(x12102),f8(x12103)))), % 59.52/59.59 inference(scs_inference,[],[1206,1183,2,3])). % 59.52/59.59 cnf(1214,plain, % 59.52/59.59 (E(f5(f8(f1(x12141)),f8(x12142),f8(x12143)),f5(f8(f1(x12141)),f8(f1(f1(f1(x12142)))),f8(x12143)))), % 59.52/59.59 inference(scs_inference,[],[1210,2])). % 59.52/59.59 cnf(1215,plain, % 59.52/59.59 (E(f5(f8(f1(x12151)),f8(f1(f1(f1(f1(x12152))))),f8(x12153)),f5(f8(f1(x12151)),f8(x12152),f8(f1(x12153))))), % 59.52/59.59 inference(scs_inference,[],[1209,1210,837,2,3])). % 59.52/59.59 cnf(1219,plain, % 59.52/59.59 (E(f5(f8(f1(x12191)),f8(x12192),f8(f1(x12193))),f5(f8(f1(x12191)),f8(f1(f1(f1(f1(x12192))))),f8(x12193)))), % 59.52/59.59 inference(scs_inference,[],[1215,2])). % 59.52/59.59 cnf(1220,plain, % 59.52/59.59 (E(f5(f8(f1(x12201)),f8(f1(x12202)),f8(x12203)),f5(f8(f1(x12201)),f8(x12202),f8(f1(x12203))))), % 59.52/59.59 inference(scs_inference,[],[1214,1215,2,3])). % 59.52/59.59 cnf(1224,plain, % 59.52/59.59 (E(f5(f8(f1(x12241)),f8(x12242),f8(f1(x12243))),f5(f8(f1(x12241)),f8(f1(x12242)),f8(x12243)))), % 59.52/59.59 inference(scs_inference,[],[1220,2])). % 59.52/59.59 cnf(1225,plain, % 59.52/59.59 (E(f5(f8(f1(x12251)),f8(x12252),f8(f1(x12253))),f5(f8(f1(x12251)),f8(f1(f1(x12252))),f8(f1(x12253))))), % 59.52/59.59 inference(scs_inference,[],[1219,1220,933,2,3])). % 59.52/59.59 cnf(1228,plain, % 59.52/59.59 (E(f5(f8(f1(x12281)),f8(f1(f1(x12282))),f8(f1(x12283))),f5(f8(f1(x12281)),f8(x12282),f8(f1(x12283))))), % 59.52/59.59 inference(scs_inference,[],[1225,2])). % 59.52/59.59 cnf(1229,plain, % 59.52/59.59 (E(f5(f8(f1(x12291)),f8(x12292),f8(f1(f1(x12293)))),f5(f8(f1(f1(f1(x12291)))),f8(f1(x12292)),f8(x12293)))), % 59.52/59.59 inference(scs_inference,[],[1224,1225,1007,2,3])). % 59.52/59.59 cnf(1233,plain, % 59.52/59.59 (E(f5(f8(f1(f1(f1(x12331)))),f8(f1(x12332)),f8(x12333)),f5(f8(f1(x12331)),f8(x12332),f8(f1(f1(x12333)))))), % 59.52/59.59 inference(scs_inference,[],[1229,2])). % 59.52/59.59 cnf(1234,plain, % 59.52/59.59 (E(f5(f8(f1(x12341)),f8(x12342),f8(f1(f1(x12343)))),f5(f8(f1(x12341)),f8(f1(f1(x12342))),f8(x12343)))), % 59.52/59.59 inference(scs_inference,[],[1229,1192,2,3])). % 59.52/59.59 cnf(1237,plain, % 59.52/59.59 (E(f5(f8(f1(x12371)),f8(f1(f1(x12372))),f8(x12373)),f5(f8(f1(x12371)),f8(x12372),f8(f1(f1(x12373)))))), % 59.52/59.59 inference(scs_inference,[],[1234,2])). % 59.52/59.59 cnf(1238,plain, % 59.52/59.59 (E(f5(f8(f1(x12381)),f8(x12382),f8(f1(f1(f1(x12383))))),f5(f8(f1(x12381)),f8(x12382),f8(f1(x12383))))), % 59.52/59.59 inference(scs_inference,[],[1234,1228,2,3])). % 59.52/59.59 cnf(1242,plain, % 59.52/59.59 (E(f4(f8(f1(f1(f1(f1(x12421))))),f8(f1(x12422))),f4(f8(x12421),f8(x12422)))), % 59.52/59.59 inference(scs_inference,[],[1191,1238,552,2,3])). % 59.52/59.59 cnf(1246,plain, % 59.52/59.59 (E(f4(f8(x12461),f8(x12462)),f4(f8(f1(f1(f1(f1(x12461))))),f8(f1(x12462))))), % 59.52/59.59 inference(scs_inference,[],[1242,2])). % 59.52/59.59 cnf(1247,plain, % 59.52/59.59 (E(f4(f8(f1(f1(x12471))),f8(x12472)),f4(f8(x12471),f8(f1(x12472))))), % 59.52/59.59 inference(scs_inference,[],[1242,1177,2,3])). % 59.52/59.59 cnf(1251,plain, % 59.52/59.59 (E(f4(f8(x12511),f8(f1(x12512))),f4(f8(f1(f1(x12511))),f8(x12512)))), % 59.52/59.59 inference(scs_inference,[],[1247,2])). % 59.52/59.59 cnf(1252,plain, % 59.52/59.59 (E(f4(f8(x12521),f8(x12522)),f4(f8(x12521),f8(f1(f1(x12522)))))), % 59.52/59.59 inference(scs_inference,[],[1246,1247,1178,2,3])). % 59.52/59.59 cnf(1255,plain, % 59.52/59.59 (E(f4(f8(x12551),f8(f1(f1(x12552)))),f4(f8(x12551),f8(x12552)))), % 59.52/59.59 inference(scs_inference,[],[1252,2])). % 59.52/59.59 cnf(1256,plain, % 59.52/59.59 (E(f4(f8(x12561),f8(f1(f1(x12562)))),f4(f8(f1(f1(f1(x12561)))),f8(x12562)))), % 59.52/59.59 inference(scs_inference,[],[1251,1252,1135,2,3])). % 59.52/59.59 cnf(1260,plain, % 59.52/59.59 (E(f4(f8(f1(f1(f1(x12601)))),f8(x12602)),f4(f8(x12601),f8(f1(f1(x12602)))))), % 59.52/59.59 inference(scs_inference,[],[1256,2])). % 59.52/59.59 cnf(1261,plain, % 59.52/59.59 (E(f4(f8(x12611),f8(f1(f1(f1(x12612))))),f4(f8(f1(f1(x12611))),f8(f1(x12612))))), % 59.52/59.59 inference(scs_inference,[],[1255,1256,1088,2,3])). % 59.52/59.59 cnf(1266,plain, % 59.52/59.59 (E(f5(f8(f1(f1(x12661))),f8(x12662),f8(f1(f1(f1(x12663))))),f5(f8(x12661),f8(x12662),f8(x12663)))), % 59.52/59.59 inference(scs_inference,[],[1168,1261,708,2,3])). % 59.52/59.59 cnf(1271,plain, % 59.52/59.59 (E(f4(f8(f1(f1(f1(x12711)))),f8(x12712)),f4(f8(x12711),f8(x12712)))), % 59.52/59.59 inference(scs_inference,[],[1266,1260,1255,2,3])). % 59.52/59.59 cnf(1274,plain, % 59.52/59.59 (E(f4(f8(x12741),f8(x12742)),f4(f8(f1(f1(f1(x12741)))),f8(x12742)))), % 59.52/59.59 inference(scs_inference,[],[1271,2])). % 59.52/59.59 cnf(1275,plain, % 59.52/59.59 (E(f5(f8(f1(x12751)),f8(x12752),f8(f1(f1(f1(x12753))))),f5(f8(f1(f1(x12751))),f8(f1(x12752)),f8(x12753)))), % 59.52/59.59 inference(scs_inference,[],[1271,1163,1035,2,3])). % 59.52/59.59 cnf(1279,plain, % 59.52/59.59 (E(f5(f8(f1(f1(x12791))),f8(f1(x12792)),f8(x12793)),f5(f8(f1(x12791)),f8(x12792),f8(f1(f1(f1(x12793))))))), % 59.52/59.59 inference(scs_inference,[],[1275,2])). % 59.52/59.59 cnf(1280,plain, % 59.52/59.59 (E(f4(f8(x12801),f8(x12802)),f4(f8(f1(f1(f1(x12801)))),f8(f1(f1(x12802)))))), % 59.52/59.59 inference(scs_inference,[],[1274,1275,1252,2,3])). % 59.52/59.59 cnf(1283,plain, % 59.52/59.59 (E(f4(f8(f1(f1(f1(x12831)))),f8(f1(f1(x12832)))),f4(f8(x12831),f8(x12832)))), % 59.52/59.59 inference(scs_inference,[],[1280,2])). % 59.52/59.59 cnf(1284,plain, % 59.52/59.59 (E(f5(f8(f1(f1(f1(x12841)))),f8(f1(x12842)),f8(f1(x12843))),f5(f8(x12841),f8(f1(x12842)),f8(x12843)))), % 59.52/59.59 inference(scs_inference,[],[1233,1280,1122,2,3])). % 59.52/59.59 cnf(1287,plain, % 59.52/59.59 (E(f5(f8(x12871),f8(f1(x12872)),f8(x12873)),f5(f8(f1(f1(f1(x12871)))),f8(f1(x12872)),f8(f1(x12873))))), % 59.52/59.59 inference(scs_inference,[],[1284,2])). % 59.52/59.59 cnf(1288,plain, % 59.52/59.59 (E(f5(f8(f1(f1(f1(x12881)))),f8(f1(x12882)),f8(f1(f1(x12883)))),f5(f8(x12881),f8(f1(x12882)),f8(x12883)))), % 59.52/59.59 inference(scs_inference,[],[1284,704,2,3])). % 59.52/59.59 cnf(1292,plain, % 59.52/59.59 (E(f5(f8(x12921),f8(f1(x12922)),f8(x12923)),f5(f8(f1(f1(f1(x12921)))),f8(f1(x12922)),f8(f1(f1(x12923)))))), % 59.52/59.59 inference(scs_inference,[],[1288,2])). % 59.52/59.59 cnf(1293,plain, % 59.52/59.59 (E(f5(f8(f1(f1(f1(x12931)))),f8(f1(x12932)),f8(f1(f1(x12933)))),f5(f8(x12931),f8(x12932),f8(x12933)))), % 59.52/59.59 inference(scs_inference,[],[1288,1000,2,3])). % 59.52/59.59 cnf(1296,plain, % 59.52/59.59 (E(f5(f8(x12961),f8(x12962),f8(x12963)),f5(f8(f1(f1(f1(x12961)))),f8(f1(x12962)),f8(f1(f1(x12963)))))), % 59.52/59.59 inference(scs_inference,[],[1293,2])). % 59.52/59.59 cnf(1297,plain, % 59.52/59.59 (E(f5(f8(x12971),f8(f1(x12972)),f8(f1(x12973))),f5(f8(x12971),f8(x12972),f8(x12973)))), % 59.52/59.59 inference(scs_inference,[],[1293,1287,2,3])). % 59.52/59.59 cnf(1301,plain, % 59.52/59.59 (E(f5(f8(x13011),f8(x13012),f8(x13013)),f5(f8(x13011),f8(f1(x13012)),f8(f1(x13013))))), % 59.52/59.59 inference(scs_inference,[],[1297,2])). % 59.52/59.59 cnf(1302,plain, % 59.52/59.59 (E(f5(f8(f1(x13021)),f8(f1(f1(f1(x13022)))),f8(x13023)),f5(f8(f1(x13021)),f8(x13022),f8(f1(x13023))))), % 59.52/59.59 inference(scs_inference,[],[1297,1237,2,3])). % 59.52/59.59 cnf(1306,plain, % 59.52/59.59 (E(f5(f8(f1(x13061)),f8(x13062),f8(f1(x13063))),f5(f8(f1(x13061)),f8(f1(f1(f1(x13062)))),f8(x13063)))), % 59.52/59.59 inference(scs_inference,[],[1302,2])). % 59.52/59.59 cnf(1307,plain, % 59.52/59.59 (E(f5(f8(x13071),f8(x13072),f8(x13073)),f5(f8(f1(f1(f1(x13071)))),f8(f1(f1(x13072))),f8(f1(x13073))))), % 59.52/59.59 inference(scs_inference,[],[1301,1302,764,2,3])). % 59.52/59.59 cnf(1309,plain, % 59.52/59.59 (E(f5(f8(f1(f1(f1(x13091)))),f8(f1(f1(x13092))),f8(f1(x13093))),f5(f8(x13091),f8(x13092),f8(x13093)))), % 59.52/59.59 inference(scs_inference,[],[1307,2])). % 59.52/59.59 cnf(1310,plain, % 59.52/59.59 (E(f5(f8(f1(x13101)),f8(x13102),f8(f1(x13103))),f5(f8(f1(f1(f1(f1(x13101))))),f8(f1(x13102)),f8(x13103)))), % 59.52/59.59 inference(scs_inference,[],[1306,1307,1172,2,3])). % 59.52/59.59 cnf(1313,plain, % 59.52/59.59 (E(f5(f8(f1(f1(f1(f1(x13131))))),f8(f1(x13132)),f8(x13133)),f5(f8(f1(x13131)),f8(x13132),f8(f1(x13133))))), % 59.52/59.59 inference(scs_inference,[],[1310,2])). % 59.52/59.59 cnf(1314,plain, % 59.52/59.59 (E(f5(f8(f1(f1(f1(x13141)))),f8(f1(f1(x13142))),f8(f1(x13143))),f5(f8(x13141),f8(f1(x13142)),f8(x13143)))), % 59.52/59.59 inference(scs_inference,[],[1309,1310,497,2,3])). % 59.52/59.59 cnf(1317,plain, % 59.52/59.59 (E(f5(f8(x13171),f8(f1(x13172)),f8(x13173)),f5(f8(f1(f1(f1(x13171)))),f8(f1(f1(x13172))),f8(f1(x13173))))), % 59.52/59.59 inference(scs_inference,[],[1314,2])). % 59.52/59.59 cnf(1318,plain, % 59.52/59.59 (E(f4(f8(x13181),f5(x13182,x13183,f8(f1(x13184)))),f4(f8(f1(x13181)),f5(x13182,x13183,f8(x13184))))), % 59.52/59.59 inference(scs_inference,[],[100,1314,512,2,3])). % 59.52/59.59 cnf(1322,plain, % 59.52/59.59 (E(f4(f8(f1(x13221)),f5(x13222,x13223,f8(x13224))),f4(f8(x13221),f5(x13222,x13223,f8(f1(x13224)))))), % 59.52/59.59 inference(scs_inference,[],[1318,2])). % 59.52/59.59 cnf(1323,plain, % 59.52/59.59 (E(f5(f8(f1(x13231)),f8(f1(x13232)),f8(x13233)),f5(f8(f1(x13231)),f8(f1(x13232)),f8(f1(f1(x13233)))))), % 59.52/59.59 inference(scs_inference,[],[1313,1317,1318,2,3])). % 59.52/59.59 cnf(1327,plain, % 59.52/59.59 (E(f5(f8(f1(x13271)),f8(f1(x13272)),f8(f1(f1(x13273)))),f5(f8(f1(x13271)),f8(f1(x13272)),f8(x13273)))), % 59.52/59.59 inference(scs_inference,[],[1323,2])). % 59.52/59.59 cnf(1328,plain, % 59.52/59.59 (E(f4(f8(f1(x13281)),f5(x13282,x13283,f8(x13284))),f4(f8(x13281),f5(x13282,x13283,f8(f1(f1(x13284))))))), % 59.52/59.59 inference(scs_inference,[],[101,1322,1323,2,3])). % 59.52/59.59 cnf(1333,plain, % 59.52/59.59 (E(f5(f8(x13331),f8(f1(x13332)),f8(x13333)),f5(f8(f1(f1(f1(x13331)))),f8(f1(x13332)),f8(x13333)))), % 59.52/59.59 inference(scs_inference,[],[1327,1292,1328,2,3])). % 59.52/59.59 cnf(1335,plain, % 59.52/59.59 (E(f5(f8(f1(f1(f1(x13351)))),f8(f1(x13352)),f8(x13353)),f5(f8(x13351),f8(f1(x13352)),f8(x13353)))), % 59.52/59.59 inference(scs_inference,[],[1333,2])). % 59.52/59.59 cnf(1336,plain, % 59.52/59.59 (E(f5(f8(x13361),f8(f1(x13362)),f8(x13363)),f5(f8(f1(f1(x13361))),f8(x13362),f8(f1(f1(f1(x13363))))))), % 59.52/59.59 inference(scs_inference,[],[1333,1279,2,3])). % 59.52/59.59 cnf(1339,plain, % 59.52/59.59 (E(f5(f8(f1(f1(x13391))),f8(x13392),f8(f1(f1(f1(x13393))))),f5(f8(x13391),f8(f1(x13392)),f8(x13393)))), % 59.52/59.59 inference(scs_inference,[],[1336,2])). % 59.52/59.59 cnf(1340,plain, % 59.52/59.59 (E(f5(f8(x13401),f8(x13402),f8(x13403)),f5(f8(x13401),f8(f1(x13402)),f8(f1(f1(x13403)))))), % 59.52/59.59 inference(scs_inference,[],[1335,1296,1336,2,3])). % 59.52/59.59 cnf(1343,plain, % 59.52/59.59 (E(f5(f8(x13431),f8(f1(x13432)),f8(f1(f1(x13433)))),f5(f8(x13431),f8(x13432),f8(x13433)))), % 59.52/59.59 inference(scs_inference,[],[1340,2])). % 59.52/59.59 cnf(1344,plain, % 59.52/59.59 (E(f5(f8(f1(f1(x13441))),f8(x13442),f8(f1(x13443))),f5(f8(x13441),f8(f1(f1(x13442))),f8(x13443)))), % 59.52/59.59 inference(scs_inference,[],[1339,1340,2,3])). % 59.52/59.59 cnf(1348,plain, % 59.52/59.59 (E(f5(f8(x13481),f8(f1(f1(x13482))),f8(x13483)),f5(f8(f1(f1(x13481))),f8(x13482),f8(f1(x13483))))), % 59.52/59.59 inference(scs_inference,[],[1344,2])). % 59.52/59.59 cnf(1349,plain, % 59.52/59.59 (E(f5(f8(f1(f1(f1(x13491)))),f8(f1(x13492)),f8(f1(f1(x13493)))),f5(f8(x13491),f8(x13492),f8(f1(x13493))))), % 59.52/59.59 inference(scs_inference,[],[1343,1344,1140,2,3])). % 59.52/59.59 cnf(1353,plain, % 59.52/59.59 (E(f5(f8(x13531),f8(x13532),f8(f1(x13533))),f5(f8(f1(f1(f1(x13531)))),f8(f1(x13532)),f8(f1(f1(x13533)))))), % 59.52/59.59 inference(scs_inference,[],[1349,2])). % 59.52/59.59 cnf(1354,plain, % 59.52/59.59 (E(f5(f8(f1(x13541)),f8(f1(f1(f1(x13542)))),f8(f1(x13543))),f5(f8(x13541),f8(x13542),f8(f1(x13543))))), % 59.52/59.59 inference(scs_inference,[],[1348,1349,2,3])). % 59.52/59.59 cnf(1357,plain, % 59.52/59.59 (E(f5(f8(x13571),f8(x13572),f8(f1(x13573))),f5(f8(f1(x13571)),f8(f1(f1(f1(x13572)))),f8(f1(x13573))))), % 59.52/59.59 inference(scs_inference,[],[1354,2])). % 59.52/59.59 cnf(1358,plain, % 59.52/59.59 (E(f5(f8(f1(x13581)),f8(f1(f1(f1(x13582)))),f8(f1(x13583))),f5(f8(f1(x13581)),f8(x13582),f8(x13583)))), % 59.52/59.59 inference(scs_inference,[],[1354,736,2,3])). % 59.52/59.59 cnf(1361,plain, % 59.52/59.59 (E(f5(f8(f1(x13611)),f8(x13612),f8(x13613)),f5(f8(f1(x13611)),f8(f1(f1(f1(x13612)))),f8(f1(x13613))))), % 59.52/59.59 inference(scs_inference,[],[1358,2])). % 59.52/59.59 cnf(1362,plain, % 59.52/59.59 (E(f5(f8(f1(x13621)),f8(f1(f1(f1(x13622)))),f8(f1(f1(x13623)))),f5(f8(x13621),f8(x13622),f8(x13623)))), % 59.52/59.59 inference(scs_inference,[],[1358,778,2,3])). % 59.52/59.59 cnf(1366,plain, % 59.52/59.59 (E(f5(f8(x13661),f8(x13662),f8(x13663)),f5(f8(f1(x13661)),f8(f1(f1(f1(x13662)))),f8(f1(f1(x13663)))))), % 59.52/59.59 inference(scs_inference,[],[1362,2])). % 59.52/59.59 cnf(1367,plain, % 59.52/59.59 (E(f5(f8(x13671),f8(x13672),f8(f1(f1(x13673)))),f5(f8(x13671),f8(x13672),f8(x13673)))), % 59.52/59.59 inference(scs_inference,[],[1362,1357,2,3])). % 59.52/59.59 cnf(1371,plain, % 59.52/59.59 (E(f5(f8(x13711),f8(x13712),f8(x13713)),f5(f8(x13711),f8(x13712),f8(f1(f1(x13713)))))), % 59.52/59.59 inference(scs_inference,[],[1367,2])). % 59.52/59.59 cnf(1372,plain, % 59.52/59.59 (E(f5(f8(f1(x13721)),f8(f1(x13722)),f8(f1(f1(x13723)))),f5(f8(f1(f1(f1(x13721)))),f8(x13722),f8(x13723)))), % 59.52/59.59 inference(scs_inference,[],[1367,1196,2,3])). % 59.52/59.59 cnf(1376,plain, % 59.52/59.59 (E(f5(f8(f1(f1(f1(x13761)))),f8(x13762),f8(x13763)),f5(f8(f1(x13761)),f8(f1(x13762)),f8(f1(f1(x13763)))))), % 59.52/59.59 inference(scs_inference,[],[1372,2])). % 59.52/59.59 cnf(1377,plain, % 59.52/59.59 (E(f5(f8(f1(x13771)),f8(x13772),f8(f1(x13773))),f5(f8(f1(f1(f1(x13771)))),f8(f1(f1(x13772))),f8(x13773)))), % 59.52/59.59 inference(scs_inference,[],[1372,1361,2,3])). % 59.52/59.59 cnf(1381,plain, % 59.52/59.59 (E(f5(f8(f1(f1(f1(x13811)))),f8(f1(f1(x13812))),f8(x13813)),f5(f8(f1(x13811)),f8(x13812),f8(f1(x13813))))), % 59.52/59.59 inference(scs_inference,[],[1377,2])). % 59.52/59.59 cnf(1382,plain, % 59.52/59.59 (E(f5(f8(f1(x13821)),f8(x13822),f8(f1(f1(x13823)))),f5(f8(x13821),f8(x13822),f8(x13823)))), % 59.52/59.59 inference(scs_inference,[],[1377,1309,2,3])). % 59.52/59.59 cnf(1386,plain, % 59.52/59.59 (E(f5(f8(x13861),f8(x13862),f8(x13863)),f5(f8(f1(x13861)),f8(x13862),f8(f1(f1(x13863)))))), % 59.52/59.59 inference(scs_inference,[],[1382,2])). % 59.52/59.59 cnf(1387,plain, % 59.52/59.59 (E(f5(f8(f1(x13871)),f8(f1(x13872)),f8(f1(f1(x13873)))),f5(f8(f1(f1(x13871))),f8(x13872),f8(f1(x13873))))), % 59.52/59.59 inference(scs_inference,[],[1382,957,2,3])). % 59.52/59.59 cnf(1391,plain, % 59.52/59.59 (E(f5(f8(f1(f1(x13911))),f8(x13912),f8(f1(x13913))),f5(f8(f1(x13911)),f8(f1(x13912)),f8(f1(f1(x13913)))))), % 59.52/59.59 inference(scs_inference,[],[1387,2])). % 59.52/59.59 cnf(1392,plain, % 59.52/59.59 (E(f5(f8(f1(f1(f1(x13921)))),f8(f1(f1(f1(x13922)))),f8(f1(x13923))),f5(f8(x13921),f8(x13922),f8(x13923)))), % 59.52/59.59 inference(scs_inference,[],[1381,1387,727,2,3])). % 59.52/59.59 cnf(1396,plain, % 59.52/59.59 (E(f5(f8(x13961),f8(x13962),f8(x13963)),f5(f8(f1(f1(f1(x13961)))),f8(f1(f1(f1(x13962)))),f8(f1(x13963))))), % 59.52/59.59 inference(scs_inference,[],[1392,2])). % 59.52/59.59 cnf(1397,plain, % 59.52/59.59 (E(f5(f8(x13971),f8(f1(f1(x13972))),f8(f1(x13973))),f5(f8(x13971),f8(x13972),f8(f1(x13973))))), % 59.52/59.59 inference(scs_inference,[],[1392,1353,2,3])). % 59.52/59.59 cnf(1401,plain, % 59.52/59.59 (E(f5(f8(x14011),f8(x14012),f8(f1(x14013))),f5(f8(x14011),f8(f1(f1(x14012))),f8(f1(x14013))))), % 59.52/59.59 inference(scs_inference,[],[1397,2])). % 59.52/59.59 cnf(1402,plain, % 59.52/59.59 (E(f5(f8(x14021),f8(x14022),f8(x14023)),f5(f8(f1(f1(f1(x14021)))),f8(f1(x14022)),f8(f1(x14023))))), % 59.52/59.59 inference(scs_inference,[],[1396,1397,2,3])). % 59.52/59.59 cnf(1405,plain, % 59.52/59.59 (E(f5(f8(f1(f1(f1(x14051)))),f8(f1(x14052)),f8(f1(x14053))),f5(f8(x14051),f8(x14052),f8(x14053)))), % 59.52/59.59 inference(scs_inference,[],[1402,2])). % 59.52/59.59 cnf(1406,plain, % 59.52/59.59 (E(f5(f8(x14061),f8(x14062),f8(f1(x14063))),f5(f8(x14061),f8(f1(f1(x14062))),f8(f1(f1(f1(x14063))))))), % 59.52/59.59 inference(scs_inference,[],[1401,1402,1371,2,3])). % 59.52/59.59 cnf(1409,plain, % 59.52/59.59 (E(f5(f8(x14091),f8(f1(f1(x14092))),f8(f1(f1(f1(x14093))))),f5(f8(x14091),f8(x14092),f8(f1(x14093))))), % 59.52/59.59 inference(scs_inference,[],[1406,2])). % 59.52/59.59 cnf(1410,plain, % 59.52/59.59 (E(f5(f8(f1(f1(f1(x14101)))),f8(f1(x14102)),f8(f1(x14103))),f5(f8(x14101),f8(x14102),f8(f1(f1(x14103)))))), % 59.52/59.59 inference(scs_inference,[],[1405,1406,1371,2,3])). % 59.52/59.59 cnf(1413,plain, % 59.52/59.59 (E(f5(f8(x14131),f8(x14132),f8(f1(f1(x14133)))),f5(f8(f1(f1(f1(x14131)))),f8(f1(x14132)),f8(f1(x14133))))), % 59.52/59.59 inference(scs_inference,[],[1410,2])). % 59.52/59.59 cnf(1414,plain, % 59.52/59.59 (E(f4(f8(f1(f1(f1(x14141)))),f8(f1(f1(x14142)))),f4(f8(x14141),f8(f1(x14142))))), % 59.52/59.59 inference(scs_inference,[],[1283,1410,516,2,3])). % 59.52/59.59 cnf(1416,plain, % 59.52/59.59 (E(f4(f8(x14161),f8(f1(x14162))),f4(f8(f1(f1(f1(x14161)))),f8(f1(f1(x14162)))))), % 59.52/59.59 inference(scs_inference,[],[1414,2])). % 59.52/59.59 cnf(1417,plain, % 59.52/59.59 (E(f6(f8(f1(f1(f1(x14171)))),f8(x14172)),f6(f8(f1(f1(x14171))),f8(f1(f1(x14172)))))), % 59.52/59.59 inference(scs_inference,[],[1414,1020,521,2,3])). % 59.52/59.59 cnf(1420,plain, % 59.52/59.59 (E(f6(f8(f1(f1(x14201))),f8(f1(f1(x14202)))),f6(f8(f1(f1(f1(x14201)))),f8(x14202)))), % 59.52/59.59 inference(scs_inference,[],[1417,2])). % 59.52/59.59 cnf(1421,plain, % 59.52/59.59 (E(f6(f8(f1(x14211)),f8(f1(x14212))),f6(f8(f1(f1(x14211))),f8(f1(f1(x14212)))))), % 59.52/59.59 inference(scs_inference,[],[1417,543,2,3])). % 59.52/59.59 cnf(1425,plain, % 59.52/59.59 (E(f6(f8(f1(f1(x14251))),f8(f1(f1(x14252)))),f6(f8(f1(x14251)),f8(f1(x14252))))), % 59.52/59.59 inference(scs_inference,[],[1421,2])). % 59.52/59.59 cnf(1426,plain, % 59.52/59.59 (E(f6(f8(f1(f1(x14261))),f8(f1(f1(x14262)))),f6(f8(f1(f1(x14261))),f8(x14262)))), % 59.52/59.59 inference(scs_inference,[],[1420,1421,1014,2,3])). % 59.52/59.59 cnf(1429,plain, % 59.52/59.59 (E(f6(f8(f1(f1(x14291))),f8(x14292)),f6(f8(f1(f1(x14291))),f8(f1(f1(x14292)))))), % 59.52/59.59 inference(scs_inference,[],[1426,2])). % 59.52/59.59 cnf(1430,plain, % 59.52/59.59 (E(f6(f8(f1(f1(x14301))),f8(f1(f1(x14302)))),f6(f8(x14301),f8(f1(x14302))))), % 59.52/59.59 inference(scs_inference,[],[1426,547,2,3])). % 59.52/59.59 cnf(1433,plain, % 59.52/59.59 (E(f6(f8(x14331),f8(f1(x14332))),f6(f8(f1(f1(x14331))),f8(f1(f1(x14332)))))), % 59.52/59.59 inference(scs_inference,[],[1430,2])). % 59.52/59.59 cnf(1434,plain, % 59.52/59.59 (E(f6(f8(f1(f1(x14341))),f8(f1(f1(x14342)))),f6(f8(x14341),f8(f1(f1(x14342)))))), % 59.52/59.59 inference(scs_inference,[],[1425,1430,542,2,3])). % 59.52/59.59 cnf(1437,plain, % 59.52/59.59 (E(f6(f8(x14371),f8(f1(f1(x14372)))),f6(f8(f1(f1(x14371))),f8(f1(f1(x14372)))))), % 59.52/59.59 inference(scs_inference,[],[1434,2])). % 59.52/59.59 cnf(1438,plain, % 59.52/59.59 (E(f6(f8(f1(f1(x14381))),f8(x14382)),f6(f8(x14381),f8(f1(f1(x14382)))))), % 59.52/59.59 inference(scs_inference,[],[1429,1434,2,3])). % 59.52/59.59 cnf(1441,plain, % 59.52/59.59 (E(f6(f8(x14411),f8(f1(f1(x14412)))),f6(f8(f1(f1(x14411))),f8(x14412)))), % 59.52/59.59 inference(scs_inference,[],[1438,2])). % 59.52/59.59 cnf(1442,plain, % 59.52/59.59 (E(f6(f8(x14421),f8(f1(x14422))),f6(f8(f1(f1(f1(f1(x14421))))),f8(x14422)))), % 59.52/59.59 inference(scs_inference,[],[1433,1438,1016,2,3])). % 59.52/59.59 cnf(1445,plain, % 59.52/59.59 (E(f6(f8(f1(f1(f1(f1(x14451))))),f8(x14452)),f6(f8(x14451),f8(f1(x14452))))), % 59.52/59.59 inference(scs_inference,[],[1442,2])). % 59.52/59.59 cnf(1446,plain, % 59.52/59.59 (E(f4(f8(x14461),f8(f1(x14462))),f4(f8(f1(f1(f1(f1(x14461))))),f8(f1(x14462))))), % 59.52/59.59 inference(scs_inference,[],[1442,1416,1098,2,3])). % 59.52/59.59 cnf(1450,plain, % 59.52/59.59 (E(f6(f8(x14501),f8(f1(f1(x14502)))),f6(f8(f1(x14501)),f8(x14502)))), % 59.52/59.59 inference(scs_inference,[],[1441,1446,1014,2,3])). % 59.52/59.59 cnf(1453,plain, % 59.52/59.59 (E(f6(f8(f1(x14531)),f8(x14532)),f6(f8(x14531),f8(f1(f1(x14532)))))), % 59.52/59.59 inference(scs_inference,[],[1450,2])). % 59.52/59.59 cnf(1454,plain, % 59.52/59.59 (E(f6(f8(f1(f1(f1(f1(x14541))))),f8(f1(x14542))),f6(f8(f1(x14541)),f8(x14542)))), % 59.52/59.59 inference(scs_inference,[],[1450,1445,2,3])). % 59.52/59.59 cnf(1458,plain, % 59.52/59.59 (E(f6(f8(f1(x14581)),f8(x14582)),f6(f8(f1(f1(f1(f1(x14581))))),f8(f1(x14582))))), % 59.52/59.59 inference(scs_inference,[],[1454,2])). % 59.52/59.59 cnf(1459,plain, % 59.52/59.59 (E(f6(f8(f1(f1(f1(f1(x14591))))),f8(f1(x14592))),f6(f8(x14591),f8(f1(x14592))))), % 59.52/59.59 inference(scs_inference,[],[1454,542,2,3])). % 59.52/59.59 cnf(1462,plain, % 59.52/59.59 (E(f6(f8(x14621),f8(f1(x14622))),f6(f8(f1(f1(f1(f1(x14621))))),f8(f1(x14622))))), % 59.52/59.59 inference(scs_inference,[],[1459,2])). % 59.52/59.59 cnf(1463,plain, % 59.52/59.59 (E(f6(f8(f1(x14631)),f8(f1(x14632))),f6(f8(f1(f1(f1(x14631)))),f8(f1(x14632))))), % 59.52/59.59 inference(scs_inference,[],[1458,1459,1425,2,3])). % 59.52/59.59 cnf(1467,plain, % 59.52/59.59 (E(f6(f8(f1(f1(f1(x14671)))),f8(f1(x14672))),f6(f8(f1(x14671)),f8(f1(x14672))))), % 59.52/59.59 inference(scs_inference,[],[1463,2])). % 59.52/59.59 cnf(1468,plain, % 59.52/59.59 (E(f6(f8(x14681),f8(f1(x14682))),f6(f8(f1(x14681)),f8(f1(f1(f1(x14682))))))), % 59.52/59.59 inference(scs_inference,[],[1462,1463,562,2,3])). % 59.52/59.59 cnf(1471,plain, % 59.52/59.59 (E(f6(f8(f1(x14711)),f8(f1(f1(f1(x14712))))),f6(f8(x14711),f8(f1(x14712))))), % 59.52/59.59 inference(scs_inference,[],[1468,2])). % 59.52/59.59 cnf(1472,plain, % 59.52/59.59 (E(f6(f8(f1(f1(f1(x14721)))),f8(f1(x14722))),f6(f8(f1(f1(x14721))),f8(x14722)))), % 59.52/59.59 inference(scs_inference,[],[1467,1468,538,2,3])). % 59.52/59.59 cnf(1475,plain, % 59.52/59.59 (E(f6(f8(f1(f1(x14751))),f8(x14752)),f6(f8(f1(f1(f1(x14751)))),f8(f1(x14752))))), % 59.52/59.59 inference(scs_inference,[],[1472,2])). % 59.52/59.59 cnf(1476,plain, % 59.52/59.59 (E(f6(f8(f1(f1(f1(x14761)))),f8(f1(x14762))),f6(f8(x14761),f8(f1(f1(x14762)))))), % 59.52/59.59 inference(scs_inference,[],[1472,1438,2,3])). % 59.52/59.59 cnf(1479,plain, % 59.52/59.59 (E(f6(f8(f1(x14791)),f8(f1(f1(f1(x14792))))),f6(f8(f1(f1(x14791))),f8(x14792)))), % 59.52/59.59 inference(scs_inference,[],[1471,1476,543,2,3])). % 59.52/59.59 cnf(1482,plain, % 59.52/59.59 (E(f6(f8(f1(f1(x14821))),f8(x14822)),f6(f8(f1(x14821)),f8(f1(f1(f1(x14822))))))), % 59.52/59.59 inference(scs_inference,[],[1479,2])). % 59.52/59.59 cnf(1483,plain, % 59.52/59.59 (E(f11(f8(f1(f1(f1(f1(x14831))))),f8(x14832)),f11(f8(x14831),f8(f1(x14832))))), % 59.52/59.59 inference(scs_inference,[],[932,1479,896,2,3])). % 59.52/59.59 cnf(1486,plain, % 59.52/59.59 (E(f11(f8(x14861),f8(f1(x14862))),f11(f8(f1(f1(f1(f1(x14861))))),f8(x14862)))), % 59.52/59.59 inference(scs_inference,[],[1483,2])). % 59.52/59.59 cnf(1487,plain, % 59.52/59.59 (E(f6(f8(f1(f1(f1(x14871)))),f8(x14872)),f6(f8(x14871),f8(f1(x14872))))), % 59.52/59.59 inference(scs_inference,[],[1475,1483,1459,2,3])). % 59.52/59.59 cnf(1491,plain, % 59.52/59.59 (E(f6(f8(x14911),f8(f1(x14912))),f6(f8(f1(f1(f1(x14911)))),f8(x14912)))), % 59.52/59.59 inference(scs_inference,[],[1487,2])). % 59.52/59.59 cnf(1492,plain, % 59.52/59.59 (E(f11(f8(x14921),f8(f1(f1(x14922)))),f11(f8(f1(x14921)),f8(x14922)))), % 59.52/59.59 inference(scs_inference,[],[1486,1487,514,2,3])). % 59.52/59.59 cnf(1496,plain, % 59.52/59.59 (E(f11(f8(f1(x14961)),f8(x14962)),f11(f8(x14961),f8(f1(f1(x14962)))))), % 59.52/59.59 inference(scs_inference,[],[1492,2])). % 59.52/59.59 cnf(1497,plain, % 59.52/59.59 (E(f11(f8(x14971),f8(x14972)),f11(f8(f1(f1(f1(f1(x14971))))),f8(x14972)))), % 59.52/59.59 inference(scs_inference,[],[1492,918,2,3])). % 59.52/59.59 cnf(1500,plain, % 59.52/59.59 (E(f11(f8(f1(f1(f1(f1(x15001))))),f8(x15002)),f11(f8(x15001),f8(x15002)))), % 59.52/59.59 inference(scs_inference,[],[1497,2])). % 59.52/59.59 cnf(1501,plain, % 59.52/59.59 (E(f6(f8(x15011),f8(f1(x15012))),f6(f8(f1(f1(x15011))),f8(f1(f1(f1(x15012))))))), % 59.52/59.59 inference(scs_inference,[],[1491,1497,1482,2,3])). % 59.52/59.59 cnf(1504,plain, % 59.52/59.59 (E(f6(f8(f1(f1(x15041))),f8(f1(f1(f1(x15042))))),f6(f8(x15041),f8(f1(x15042))))), % 59.52/59.59 inference(scs_inference,[],[1501,2])). % 59.52/59.59 cnf(1505,plain, % 59.52/59.59 (E(f6(f8(f1(x15051)),f8(x15052)),f6(f8(f1(f1(x15051))),f8(f1(f1(x15052)))))), % 59.52/59.59 inference(scs_inference,[],[1437,1453,1501,2,3])). % 59.52/59.59 cnf(1508,plain, % 59.52/59.59 (E(f6(f8(f1(f1(x15081))),f8(f1(f1(x15082)))),f6(f8(f1(x15081)),f8(x15082)))), % 59.52/59.59 inference(scs_inference,[],[1505,2])). % 59.52/59.59 cnf(1509,plain, % 59.52/59.59 (E(f11(f8(f1(f1(f1(f1(x15091))))),f8(f1(x15092))),f11(f8(x15091),f8(x15092)))), % 59.52/59.59 inference(scs_inference,[],[1500,1505,818,2,3])). % 59.52/59.59 cnf(1513,plain, % 59.52/59.59 (E(f11(f8(x15131),f8(x15132)),f11(f8(f1(f1(f1(f1(x15131))))),f8(f1(x15132))))), % 59.52/59.59 inference(scs_inference,[],[1509,2])). % 59.52/59.59 cnf(1514,plain, % 59.52/59.59 (E(f6(f8(f1(f1(f1(x15141)))),f8(f1(f1(x15142)))),f6(f8(x15141),f8(f1(x15142))))), % 59.52/59.59 inference(scs_inference,[],[1508,1509,547,2,3])). % 59.52/59.59 cnf(1518,plain, % 59.52/59.59 (E(f6(f8(x15181),f8(f1(x15182))),f6(f8(f1(f1(f1(x15181)))),f8(f1(f1(x15182)))))), % 59.52/59.59 inference(scs_inference,[],[1514,2])). % 59.52/59.59 cnf(1519,plain, % 59.52/59.59 (E(f11(f8(x15191),f8(x15192)),f11(f8(f1(f1(x15191))),f8(f1(f1(f1(x15192))))))), % 59.52/59.59 inference(scs_inference,[],[1513,1514,873,2,3])). % 59.52/59.59 cnf(1523,plain, % 59.52/59.59 (E(f11(f8(f1(f1(f1(x15231)))),f8(x15232)),f11(f8(x15231),f8(f1(x15232))))), % 59.52/59.59 inference(scs_inference,[],[1496,1519,509,2,3])). % 59.52/59.59 cnf(1528,plain, % 59.52/59.59 (E(f6(f8(f1(f1(x15281))),f8(f1(f1(f1(x15282))))),f6(f8(f1(x15281)),f8(x15282)))), % 59.52/59.59 inference(scs_inference,[],[1504,1523,538,2,3])). % 59.52/59.59 cnf(1530,plain, % 59.52/59.59 (E(f8(f10(f5(f8(f1(x15301)),x15302,x15303))),f8(f10(f5(f8(x15301),x15302,x15303))))), % 59.52/59.59 inference(scs_inference,[],[70,2,5])). % 59.52/59.59 cnf(1531,plain, % 59.52/59.59 (E(f6(f8(f1(x15311)),f8(x15312)),f6(f8(f1(f1(x15311))),f8(f1(f1(f1(x15312))))))), % 59.52/59.59 inference(scs_inference,[],[1528,2])). % 59.52/59.59 cnf(1532,plain, % 59.52/59.59 (E(f5(f8(x15321),f8(f1(f1(x15322))),f8(f1(f1(f1(x15323))))),f5(f8(x15321),f8(x15322),f8(x15323)))), % 59.52/59.59 inference(scs_inference,[],[1528,1409,704,2,3])). % 59.52/59.59 cnf(1536,plain, % 59.52/59.59 (E(f6(f8(x15361),f8(f1(x15362))),f6(f8(f1(x15361)),f8(f1(f1(x15362)))))), % 59.52/59.59 inference(scs_inference,[],[1532,1518,1467,2,3])). % 59.52/59.59 cnf(1538,plain, % 59.52/59.59 (E(f1(f10(f5(f8(f1(x15381)),x15382,x15383))),f1(f10(f5(f8(x15381),x15382,x15383))))), % 59.52/59.59 inference(scs_inference,[],[70,2,4])). % 59.52/59.59 cnf(1540,plain, % 59.52/59.59 (E(f5(f8(x15401),f8(x15402),f8(f1(f1(x15403)))),f5(f8(x15401),f8(f1(x15402)),f8(f1(x15403))))), % 59.52/59.59 inference(scs_inference,[],[1413,1530,1335,2,3])). % 59.52/59.59 cnf(1543,plain, % 59.52/59.59 (E(f5(f8(x15431),f8(f1(x15432)),f8(f1(x15433))),f5(f8(x15431),f8(x15432),f8(f1(f1(x15433)))))), % 59.52/59.59 inference(scs_inference,[],[1540,2])). % 59.52/59.59 cnf(1544,plain, % 59.52/59.59 (E(f5(f8(x15441),f8(x15442),f8(f1(f1(x15443)))),f5(f8(f1(f1(f1(x15441)))),f8(f1(x15442)),f8(x15443)))), % 59.52/59.59 inference(scs_inference,[],[1540,1144,2,3])). % 59.52/59.59 cnf(1546,plain, % 59.52/59.59 (E(f3(x15461,f10(f5(f8(f1(x15462)),x15463,x15464))),f3(x15461,f10(f5(f8(x15462),x15463,x15464))))), % 59.52/59.59 inference(scs_inference,[],[70,2,22])). % 59.52/59.59 cnf(1547,plain, % 59.52/59.59 (E(f5(f8(f1(f1(f1(x15471)))),f8(f1(x15472)),f8(x15473)),f5(f8(x15471),f8(x15472),f8(f1(f1(x15473)))))), % 59.52/59.59 inference(scs_inference,[],[1544,2])). % 59.52/59.59 cnf(1548,plain, % 59.52/59.59 (E(f5(f8(x15481),f8(x15482),f8(f1(f1(x15483)))),f5(f8(f1(x15481)),f8(f1(f1(x15482))),f8(f1(f1(x15483)))))), % 59.52/59.59 inference(scs_inference,[],[1544,1376,2,3])). % 59.52/59.59 cnf(1551,plain, % 59.52/59.59 (E(f6(f8(f1(x15511)),f8(f1(f1(x15512)))),f6(f8(x15511),f8(f1(x15512))))), % 59.52/59.59 inference(scs_inference,[],[1536,2])). % 59.52/59.59 cnf(1552,plain, % 59.52/59.59 (E(f5(f8(x15521),f8(x15522),f8(x15523)),f5(f8(f1(x15521)),f8(f1(f1(x15522))),f8(f1(f1(f1(x15523))))))), % 59.52/59.59 inference(scs_inference,[],[1366,1536,1543,2,3])). % 59.52/59.59 cnf(1556,plain, % 59.52/59.59 (E(f6(f8(f1(x15561)),f8(x15562)),f6(f8(f1(x15561)),f8(f1(f1(x15562)))))), % 59.52/59.59 inference(scs_inference,[],[1551,1538,1531,2,3])). % 59.52/59.59 cnf(1560,plain, % 59.52/59.59 (E(f6(f8(f1(x15601)),f8(x15602)),f6(f8(f1(f1(f1(f1(x15601))))),f8(x15602)))), % 59.52/59.59 inference(scs_inference,[],[1546,1556,608,2,3])). % 59.52/59.59 cnf(1562,plain, % 59.52/59.59 (E(f6(f8(f1(f1(f1(f1(x15621))))),f8(x15622)),f6(f8(f1(x15621)),f8(x15622)))), % 59.52/59.59 inference(scs_inference,[],[1560,2])). % 59.52/59.59 cnf(1563,plain, % 59.52/59.59 (E(f5(f8(x15631),f8(x15632),f8(x15633)),f5(f8(f1(f1(x15631))),f8(f1(f1(f1(x15632)))),f8(f1(f1(x15633)))))), % 59.52/59.59 inference(scs_inference,[],[1560,1386,1108,2,3])). % 59.52/59.59 cnf(1568,plain, % 59.52/59.59 (E(f5(f8(f1(f1(f1(x15681)))),f8(x15682),f8(f1(f1(x15683)))),f5(f8(x15681),f8(f1(x15682)),f8(x15683)))), % 59.52/59.59 inference(scs_inference,[],[1391,1548,1266,2,3])). % 59.52/59.59 cnf(1574,plain, % 59.52/59.59 (E(f5(f8(f1(f1(f1(x15741)))),f8(x15742),f8(f1(f1(x15743)))),f5(f8(f1(x15741)),f8(f1(x15742)),f8(x15743)))), % 59.52/59.59 inference(scs_inference,[],[1568,493,2,3])). % 59.52/59.59 cnf(1579,plain, % 59.52/59.59 (E(f5(f8(f1(f1(f1(x15791)))),f8(x15792),f8(f1(f1(x15793)))),f5(f8(f1(x15791)),f8(x15792),f8(f1(x15793))))), % 59.52/59.59 inference(scs_inference,[],[1574,1220,2,3])). % 59.52/59.59 cnf(1584,plain, % 59.52/59.59 (E(f5(f8(f1(f1(f1(x15841)))),f8(x15842),f8(f1(f1(x15843)))),f5(f8(x15841),f8(x15842),f8(f1(x15843))))), % 59.52/59.59 inference(scs_inference,[],[1579,996,2,3])). % 59.52/59.59 cnf(1589,plain, % 59.52/59.59 (E(f5(f8(f1(f1(f1(x15891)))),f8(x15892),f8(f1(f1(x15893)))),f5(f8(f1(x15891)),f8(x15892),f8(x15893)))), % 59.52/59.59 inference(scs_inference,[],[1584,736,2,3])). % 59.52/59.59 cnf(1594,plain, % 59.52/59.59 (E(f5(f8(f1(f1(f1(x15941)))),f8(x15942),f8(f1(f1(x15943)))),f5(f8(x15941),f8(x15942),f8(x15943)))), % 59.52/59.59 inference(scs_inference,[],[1589,996,2,3])). % 59.52/59.59 cnf(1599,plain, % 59.52/59.59 (E(f5(f8(f1(f1(f1(x15991)))),f8(x15992),f8(f1(f1(x15993)))),f5(f8(x15991),f8(f1(x15992)),f8(f1(x15993))))), % 59.52/59.59 inference(scs_inference,[],[1594,1301,2,3])). % 59.52/59.59 cnf(1604,plain, % 59.52/59.59 (E(f6(f8(f1(f1(f1(f1(x16041))))),f8(x16042)),f6(f8(x16041),f8(x16042)))), % 59.52/59.59 inference(scs_inference,[],[1562,1599,1014,2,3])). % 59.52/59.59 cnf(1608,plain, % 59.52/59.59 (E(f6(f8(x16081),f8(x16082)),f6(f8(f1(f1(f1(f1(x16081))))),f8(x16082)))), % 59.52/59.59 inference(scs_inference,[],[1604,2])). % 59.52/59.59 cnf(1609,plain, % 59.52/59.59 (E(f6(f8(f1(f1(x16091))),f8(f1(f1(x16092)))),f6(f8(x16091),f8(x16092)))), % 59.52/59.59 inference(scs_inference,[],[1604,1441,2,3])). % 59.52/59.59 cnf(1614,plain, % 59.52/59.59 (E(f6(f8(x16141),f8(x16142)),f6(f8(f1(f1(x16141))),f8(f1(f1(x16142)))))), % 59.52/59.59 inference(scs_inference,[],[1609,2])). % 59.52/59.59 cnf(1615,plain, % 59.52/59.59 (E(f5(f8(f1(f1(f1(x16151)))),f8(f1(f1(x16152))),f8(x16153)),f5(f8(f1(f1(x16151))),f8(x16152),f8(f1(x16153))))), % 59.52/59.59 inference(scs_inference,[],[1609,1547,787,2,3])). % 59.52/59.59 cnf(1619,plain, % 59.52/59.59 (E(f5(f8(f1(f1(x16191))),f8(x16192),f8(f1(x16193))),f5(f8(f1(f1(f1(x16191)))),f8(f1(f1(x16192))),f8(x16193)))), % 59.52/59.59 inference(scs_inference,[],[1615,2])). % 59.52/59.59 cnf(1620,plain, % 59.52/59.59 (E(f5(f8(f1(x16201)),f8(x16202),f8(x16203)),f5(f8(f1(f1(x16201))),f8(f1(x16202)),f8(f1(f1(f1(x16203))))))), % 59.52/59.59 inference(scs_inference,[],[1615,1563,2,3])). % 59.52/59.59 cnf(1624,plain, % 59.52/59.59 (E(f5(f8(f1(x16241)),f8(f1(f1(x16242))),f8(f1(f1(f1(x16243))))),f5(f8(x16241),f8(x16242),f8(x16243)))), % 59.52/59.59 inference(scs_inference,[],[1552,2])). % 59.52/59.59 cnf(1625,plain, % 59.52/59.59 (E(f5(f8(f1(f1(x16251))),f8(f1(x16252)),f8(f1(x16253))),f5(f8(f1(f1(f1(x16251)))),f8(x16252),f8(x16253)))), % 59.52/59.59 inference(scs_inference,[],[1619,1552,1210,2,3])). % 59.52/59.59 cnf(1630,plain, % 59.52/59.59 (E(f6(f8(x16301),f8(x16302)),f6(f8(f1(x16301)),f8(f1(x16302))))), % 59.52/59.59 inference(scs_inference,[],[1608,1625,1487,2,3])). % 59.52/59.59 cnf(1633,plain, % 59.52/59.59 (E(f6(f8(f1(x16331)),f8(f1(x16332))),f6(f8(x16331),f8(x16332)))), % 59.52/59.59 inference(scs_inference,[],[1630,2])). % 59.52/59.59 cnf(1634,plain, % 59.52/59.59 (E(f6(f8(f1(x16341)),f8(f1(f1(x16342)))),f6(f8(f1(x16341)),f8(x16342)))), % 59.52/59.59 inference(scs_inference,[],[1630,1528,2,3])). % 59.52/59.59 cnf(1638,plain, % 59.52/59.59 (E(f6(f8(f1(x16381)),f8(f1(f1(f1(x16382))))),f6(f8(x16381),f8(x16382)))), % 59.52/59.59 inference(scs_inference,[],[1633,1634,1620,2,3])). % 59.52/59.59 cnf(1643,plain, % 59.52/59.59 (E(f5(f8(f1(x16431)),f8(f1(f1(x16432))),f8(f1(f1(f1(x16433))))),f5(f8(x16431),f8(f1(x16432)),f8(x16433)))), % 59.52/59.59 inference(scs_inference,[],[1624,1638,497,2,3])). % 59.52/59.59 cnf(1647,plain, % 59.52/59.59 (E(f6(f8(x16471),f8(x16472)),f6(f8(f1(f1(x16471))),f8(x16472)))), % 59.52/59.59 inference(scs_inference,[],[1643,1614,1634,2,3])). % 59.52/59.59 cnf(1651,plain, % 59.52/59.59 (E(f6(f8(x16511),f8(f1(f1(x16512)))),f6(f8(x16511),f8(x16512)))), % 59.52/59.59 inference(scs_inference,[],[1647,1609,2,3])). % 59.52/59.59 cnf(1655,plain, % 59.52/59.59 (E(f6(f8(x16551),f8(x16552)),f6(f8(x16551),f8(f1(f1(x16552)))))), % 59.52/59.59 inference(scs_inference,[],[1651,2])). % 59.52/59.59 cnf(1721,plain, % 59.52/59.59 (E(f17(f17(f8(f1(x17211)))),f17(f17(f8(x17211))))), % 59.52/59.59 inference(scs_inference,[],[498,4,5,8])). % 59.52/59.59 cnf(1745,plain, % 59.52/59.59 (P1(f11(f9(a18),f12(f15(a18),f11(f9(a19),f11(f10(a23),f10(a25))))),f1(f6(a7,a13)),a21)), % 59.52/59.59 inference(scs_inference,[],[27,498,82,127,28,29,4,5,8,9,10,14,31,6,7,15,16,17,18,19,20,21,11,12,13,32,34,22,2,33])). % 59.52/59.59 cnf(1757,plain, % 59.52/59.59 (P1(f11(f9(a18),f12(f15(a18),f11(f9(a19),f11(f10(a23),f10(a25))))),f8(f1(f6(a7,a13))),a21)), % 59.52/59.59 inference(scs_inference,[],[1745,31])). % 59.52/59.59 cnf(1791,plain, % 59.52/59.59 (P1(f12(f15(a18),f11(f9(a19),f11(f10(a23),f10(a25)))),f8(f1(f6(a7,a13))),a21)), % 59.52/59.59 inference(scs_inference,[],[522,1757,31,13,32])). % 59.52/59.59 cnf(1823,plain, % 59.52/59.59 (P1(f12(f15(a22),f11(f9(a20),f11(f10(a24),f10(a23)))),f8(f6(a7,a13)),a21)), % 59.52/59.59 inference(scs_inference,[],[1791,74,31,32])). % 59.52/59.59 cnf(1846,plain, % 59.52/59.59 (~P1(f12(f15(x18461),f11(f9(x18462),f11(f10(a23),x18463))),f8(f6(a7,a13)),a21)), % 59.52/59.59 inference(scs_inference,[],[27,1655,688,1791,678,74,30,31,32,4,13,16,6,14,8,10,12,9,19,11,18,21,7,20,22,17,15,5,3,35])). % 59.52/59.59 cnf(1854,plain, % 59.52/59.59 (P1(f12(f15(a22),f11(f9(a20),f11(f10(a24),f10(a23)))),f8(f8(f6(a7,a13))),a21)), % 59.52/59.59 inference(scs_inference,[],[1823,31])). % 59.52/59.59 cnf(1906,plain, % 59.52/59.59 ($false), % 59.52/59.59 inference(scs_inference,[],[1846,1721,1854,1791,26,31,4,13,6,20,18,7,19,12,14,22,16,5,11,15,8,17,21,9,10,24]), % 59.52/59.59 ['proof']). % 59.52/59.59 % SZS output end Proof % 59.52/59.59 % Total time :58.910000s %------------------------------------------------------------------------------