%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SWV342-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:50 EDT 2024 % Result : Unsatisfiable 58.95s 58.99s % Output : CNFRefutation 58.95s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.10 % Problem : SWV342-2 : TPTP v8.2.0. Released v3.2.0. % 0.00/0.10 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.10/0.31 % Computer : n027.cluster.edu % 0.10/0.31 % Model : x86_64 x86_64 % 0.10/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.31 % Memory : 8042.1875MB % 0.10/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.31 % CPULimit : 300 % 0.10/0.31 % WCLimit : 300 % 0.10/0.31 % DateTime : Thu Jun 20 20:34:39 EDT 2024 % 0.10/0.31 % CPUTime : % 0.16/0.50 start to proof:theBenchmark % 58.88/58.98 %------------------------------------------- % 58.88/58.98 % File :CSE---1.7 % 58.88/58.98 % Problem :theBenchmark % 58.88/58.98 % Transform :cnf % 58.88/58.98 % Format :tptp:raw % 58.88/58.98 % Command :java -jar mcs_scs.jar %d %s % 58.88/58.98 % 58.88/58.98 % Result :Theorem 58.440000s % 58.88/58.98 % Output :CNFRefutation 58.440000s % 58.88/58.98 %------------------------------------------- % 58.95/58.99 %------------------------------------------------------------------------------ % 58.95/58.99 % File : SWV342-2 : TPTP v8.2.0. Released v3.2.0. % 58.95/58.99 % Domain : Software Verification (Security) % 58.95/58.99 % Problem : Cryptographic protocol problem for Yahalom % 58.95/58.99 % Version : [Pau06] axioms : Reduced > Especial. % 58.95/58.99 % English : % 58.95/58.99 % 58.95/58.99 % Refs : [Pau06] Paulson (2006), Email to G. Sutcliffe % 58.95/58.99 % Source : [Pau06] % 58.95/58.99 % Names : % 58.95/58.99 % 58.95/58.99 % Status : Unsatisfiable % 58.95/58.99 % Rating : 0.00 v5.5.0, 0.12 v5.4.0, 0.13 v5.3.0, 0.25 v5.2.0, 0.00 v4.1.0, 0.11 v4.0.1, 0.17 v3.3.0, 0.14 v3.2.0 % 58.95/58.99 % Syntax : Number of clauses : 9 ( 3 unt; 0 nHn; 8 RR) % 58.95/58.99 % Number of literals : 15 ( 1 equ; 7 neg) % 58.95/58.99 % Maximal clause size : 2 ( 1 avg) % 58.95/58.99 % Maximal term depth : 7 ( 2 avg) % 58.95/58.99 % Number of predicates : 2 ( 1 usr; 0 prp; 2-3 aty) % 58.95/58.99 % Number of functors : 21 ( 21 usr; 10 con; 0-3 aty) % 58.95/58.99 % Number of variables : 18 ( 5 sgn) % 58.95/58.99 % SPC : CNF_UNS_RFO_SEQ_HRN % 58.95/58.99 % 58.95/58.99 % Comments : The problems in the [Pau06] collection each have very many axioms, % 58.95/58.99 % of which only a small selection are required for the refutation. % 58.95/58.99 % The mission is to find those few axioms, after which a refutation % 58.95/58.99 % can be quite easily found. This version has only the necessary % 58.95/58.99 % axioms. % 58.95/58.99 %------------------------------------------------------------------------------ % 58.95/58.99 cnf(cls_conjecture_3,negated_conjecture, % 58.95/58.99 ~ c_in(c_Message_Omsg_OKey(v_K),c_Event_Oused(v_evs3),tc_Message_Omsg) ). % 58.95/58.99 % 58.95/58.99 cnf(cls_conjecture_9,negated_conjecture, % 58.95/58.99 c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_A,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(v_K),c_Message_Omsg_OMPair(v_na,v_nb)))),c_Message_Omsg_OCrypt(c_Public_OshrK(v_B),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OKey(v_K))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent) ). % 58.95/58.99 % 58.95/58.99 cnf(cls_Event_OSays__imp__analz__Spy__dest_0,axiom, % 58.95/58.99 ( ~ c_in(c_Event_Oevent_OSays(V_A,V_B,V_X),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent) % 58.95/58.99 | c_in(V_X,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg) ) ). % 58.95/58.99 % 58.95/58.99 cnf(cls_Event_Oc_A_58_Aparts_A_Iknows_ASpy_Aevs1_J_A_61_61_62_Ac_A_58_Aused_Aevs1_0,axiom, % 58.95/58.99 ( ~ c_in(V_c,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg) % 58.95/58.99 | c_in(V_c,c_Event_Oused(V_evs),tc_Message_Omsg) ) ). % 58.95/58.99 % 58.95/58.99 cnf(cls_Message_OMPair__analz_0,axiom, % 58.95/58.99 ( ~ c_in(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Oanalz(V_H),tc_Message_Omsg) % 58.95/58.99 | c_in(V_Y,c_Message_Oanalz(V_H),tc_Message_Omsg) ) ). % 58.95/58.99 % 58.95/58.99 cnf(cls_Message_OMPair__parts_0,axiom, % 58.95/58.99 ( ~ c_in(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Oparts(V_H),tc_Message_Omsg) % 58.95/58.99 | c_in(V_Y,c_Message_Oparts(V_H),tc_Message_Omsg) ) ). % 58.95/58.99 % 58.95/58.99 cnf(cls_Message_Oparts_OBody__dest_0,axiom, % 58.95/58.99 ( ~ c_in(c_Message_Omsg_OCrypt(V_K,V_X),c_Message_Oparts(V_H),tc_Message_Omsg) % 58.95/58.99 | c_in(V_X,c_Message_Oparts(V_H),tc_Message_Omsg) ) ). % 58.95/58.99 % 58.95/58.99 cnf(cls_Message_Oparts_OInj_0,axiom, % 58.95/58.99 ( ~ c_in(V_X,V_H,tc_Message_Omsg) % 58.95/58.99 | c_in(V_X,c_Message_Oparts(V_H),tc_Message_Omsg) ) ). % 58.95/58.99 % 58.95/58.99 cnf(cls_Message_Oparts__analz_0,axiom, % 58.95/58.99 c_Message_Oparts(c_Message_Oanalz(V_H)) = c_Message_Oparts(V_H) ). % 58.95/58.99 % 58.95/58.99 %------------------------------------------------------------------------------ % 58.95/58.99 %------------------------------------------- % 58.95/58.99 % Proof found % 58.95/58.99 % SZS status Theorem for theBenchmark % 58.95/58.99 % SZS output start Proof % 58.95/58.99 %ClaNum:32(EqnAxiom:23) % 58.95/58.99 %VarNum:31(SingletonVarNum:18) % 58.95/58.99 %MaxLitNum:2 % 58.95/58.99 %MaxfuncDepth:5 % 58.95/58.99 %SharedTerms:27 % 58.95/58.99 %goalClause: 25 26 % 58.95/58.99 %singleGoalClaCount:2 % 58.95/58.99 [26]~P1(f10(a18),f5(a20),a16) % 58.95/58.99 [25]P1(f3(a2,a13,f12(f11(f14(a13),f12(f9(a17),f12(f10(a18),f12(a19,a21)))),f11(f14(a17),f12(f9(a13),f10(a18))))),f4(a20,a15),a15) % 58.95/58.99 [24]E(f8(f1(x241)),f8(x241)) % 58.95/58.99 [27]~P1(x271,x272,a16)+P1(x271,f8(x272),a16) % 58.95/58.99 [31]P1(x311,f5(x312),a16)+~P1(x311,f8(f6(a7,x312)),a16) % 58.95/58.99 [28]P1(x281,f1(x282),a16)+~P1(f12(x283,x281),f1(x282),a16) % 58.95/58.99 [29]P1(x291,f8(x292),a16)+~P1(f12(x293,x291),f8(x292),a16) % 58.95/58.99 [30]P1(x301,f8(x302),a16)+~P1(f11(x303,x301),f8(x302),a16) % 58.95/58.99 [32]~P1(f3(x323,x324,x321),f4(x322,a15),a15)+P1(x321,f1(f6(a7,x322)),a16) % 58.95/58.99 %EqnAxiom % 58.95/58.99 [1]E(x11,x11) % 58.95/58.99 [2]E(x22,x21)+~E(x21,x22) % 58.95/58.99 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 58.95/58.99 [4]~E(x41,x42)+E(f1(x41),f1(x42)) % 58.95/58.99 [5]~E(x51,x52)+E(f8(x51),f8(x52)) % 58.95/58.99 [6]~E(x61,x62)+E(f6(x61,x63),f6(x62,x63)) % 58.95/58.99 [7]~E(x71,x72)+E(f6(x73,x71),f6(x73,x72)) % 58.95/58.99 [8]~E(x81,x82)+E(f14(x81),f14(x82)) % 58.95/58.99 [9]~E(x91,x92)+E(f9(x91),f9(x92)) % 58.95/58.99 [10]~E(x101,x102)+E(f10(x101),f10(x102)) % 58.95/58.99 [11]~E(x111,x112)+E(f12(x111,x113),f12(x112,x113)) % 58.95/58.99 [12]~E(x121,x122)+E(f12(x123,x121),f12(x123,x122)) % 58.95/58.99 [13]~E(x131,x132)+E(f4(x131,x133),f4(x132,x133)) % 58.95/58.99 [14]~E(x141,x142)+E(f4(x143,x141),f4(x143,x142)) % 58.95/58.99 [15]~E(x151,x152)+E(f11(x151,x153),f11(x152,x153)) % 58.95/58.99 [16]~E(x161,x162)+E(f11(x163,x161),f11(x163,x162)) % 58.95/58.99 [17]~E(x171,x172)+E(f3(x171,x173,x174),f3(x172,x173,x174)) % 58.95/58.99 [18]~E(x181,x182)+E(f3(x183,x181,x184),f3(x183,x182,x184)) % 58.95/58.99 [19]~E(x191,x192)+E(f3(x193,x194,x191),f3(x193,x194,x192)) % 58.95/58.99 [20]~E(x201,x202)+E(f5(x201),f5(x202)) % 58.95/58.99 [21]P1(x212,x213,x214)+~E(x211,x212)+~P1(x211,x213,x214) % 58.95/58.99 [22]P1(x223,x222,x224)+~E(x221,x222)+~P1(x223,x221,x224) % 58.95/58.99 [23]P1(x233,x234,x232)+~E(x231,x232)+~P1(x233,x234,x231) % 58.95/58.99 % 58.95/58.99 %------------------------------------------- % 58.95/59.00 cnf(33,plain, % 58.95/59.00 (E(f8(x331),f8(f1(x331)))), % 58.95/59.00 inference(scs_inference,[],[24,2])). % 58.95/59.00 cnf(40,plain, % 58.95/59.00 (E(f1(f8(f1(x401))),f1(f8(x401)))), % 58.95/59.00 inference(scs_inference,[],[33,4,2])). % 58.95/59.00 cnf(41,plain, % 58.95/59.00 (E(f1(f8(x411)),f1(f8(f1(x411))))), % 58.95/59.00 inference(scs_inference,[],[40,2])). % 58.95/59.00 cnf(49,plain, % 58.95/59.00 (P1(f12(f11(f14(a13),f12(f9(a17),f12(f10(a18),f12(a19,a21)))),f11(f14(a17),f12(f9(a13),f10(a18)))),f8(f1(f6(a7,a20))),a16)), % 58.95/59.00 inference(scs_inference,[],[25,27,32])). % 58.95/59.00 cnf(50,plain, % 58.95/59.00 (P1(f12(f11(f14(a13),f12(f9(a17),f12(f10(a18),f12(a19,a21)))),f11(f14(a17),f12(f9(a13),f10(a18)))),f8(f6(a7,a20)),a16)), % 58.95/59.00 inference(scs_inference,[],[24,49,22])). % 58.95/59.00 cnf(57,plain, % 58.95/59.00 (E(f12(x571,f4(f8(f1(x572)),x573)),f12(x571,f4(f8(x572),x573)))), % 58.95/59.00 inference(scs_inference,[],[24,12,13])). % 58.95/59.00 cnf(58,plain, % 58.95/59.00 (E(f12(x581,f4(f8(x582),x583)),f12(x581,f4(f8(f1(x582)),x583)))), % 58.95/59.00 inference(scs_inference,[],[57,2])). % 58.95/59.00 cnf(64,plain, % 58.95/59.00 (E(f4(x641,f11(f8(f1(x642)),x643)),f4(x641,f11(f8(x642),x643)))), % 58.95/59.00 inference(scs_inference,[],[24,14,15])). % 58.95/59.00 cnf(65,plain, % 58.95/59.00 (E(f4(x651,f11(f8(x652),x653)),f4(x651,f11(f8(f1(x652)),x653)))), % 58.95/59.00 inference(scs_inference,[],[64,2])). % 58.95/59.00 cnf(74,plain, % 58.95/59.00 (E(f11(x741,f3(f8(x742),x743,x744)),f11(x741,f3(f8(f1(x742)),x743,x744)))), % 58.95/59.00 inference(scs_inference,[],[33,16,17])). % 58.95/59.00 cnf(75,plain, % 58.95/59.00 (E(f11(x751,f3(f8(f1(x752)),x753,x754)),f11(x751,f3(f8(x752),x753,x754)))), % 58.95/59.00 inference(scs_inference,[],[74,2])). % 58.95/59.00 cnf(76,plain, % 58.95/59.00 (E(f3(x761,f3(x762,x763,f8(x764)),x765),f3(x761,f3(x762,x763,f8(f1(x764))),x765))), % 58.95/59.00 inference(scs_inference,[],[33,18,19])). % 58.95/59.00 cnf(77,plain, % 58.95/59.00 (E(f3(x771,f3(x772,x773,f8(f1(x774))),x775),f3(x771,f3(x772,x773,f8(x774)),x775))), % 58.95/59.00 inference(scs_inference,[],[76,2])). % 58.95/59.00 cnf(78,plain, % 58.95/59.00 (P1(x781,f8(f1(x782)),a16)+~P1(f12(x783,x781),f1(x782),a16)), % 58.95/59.00 inference(scs_inference,[],[28,27])). % 58.95/59.00 cnf(79,plain, % 58.95/59.00 (P1(f12(f9(a13),f10(a18)),f8(f6(a7,a20)),a16)), % 58.95/59.00 inference(scs_inference,[],[50,29,30])). % 58.95/59.00 cnf(82,plain, % 58.95/59.00 (P1(f12(f9(a13),f10(a18)),f8(f1(f6(a7,a20))),a16)), % 58.95/59.00 inference(scs_inference,[],[33,79,31,22])). % 58.95/59.00 cnf(88,plain, % 58.95/59.00 (P1(f12(f9(a13),f10(a18)),f8(f1(f1(f6(a7,a20)))),a16)), % 58.95/59.00 inference(scs_inference,[],[33,82,22])). % 58.95/59.00 cnf(110,plain, % 58.95/59.00 (P1(x1101,f8(f1(f1(f6(a7,a20)))),x1102)+~E(a16,x1102)+~E(f12(f9(a13),f10(a18)),x1101)), % 58.95/59.00 inference(scs_inference,[],[88,23,21])). % 58.95/59.00 cnf(138,plain, % 58.95/59.00 (P1(f12(f9(a13),f10(a18)),f8(f1(f1(f1(f6(a7,a20))))),a16)), % 58.95/59.00 inference(scs_inference,[],[33,88,22])). % 58.95/59.00 cnf(145,plain, % 58.95/59.00 (P1(f12(f9(a13),f10(a18)),f8(f1(f1(f1(f1(f6(a7,a20)))))),a16)), % 58.95/59.00 inference(scs_inference,[],[33,138,22])). % 58.95/59.00 cnf(180,plain, % 58.95/59.00 (~E(f12(f9(a13),f10(a18)),x1801)+P1(x1801,f8(f8(f1(f1(f6(a7,a20))))),a16)), % 58.95/59.00 inference(scs_inference,[],[110,27])). % 58.95/59.00 cnf(181,plain, % 58.95/59.00 (P1(f12(f9(a13),f10(a18)),f8(f8(f1(f1(f6(a7,a20))))),a16)), % 58.95/59.00 inference(equality_inference,[],[180])). % 58.95/59.00 cnf(182,plain, % 58.95/59.00 (P1(f12(f9(a13),f10(a18)),f8(f1(f8(f1(f1(f6(a7,a20)))))),a16)), % 58.95/59.00 inference(scs_inference,[],[33,181,22])). % 58.95/59.00 cnf(188,plain, % 58.95/59.00 (E(f8(f8(x1881)),f8(f8(f1(x1881))))), % 58.95/59.00 inference(scs_inference,[],[24,2,5])). % 58.95/59.00 cnf(189,plain, % 58.95/59.00 (E(f8(f8(f1(x1891))),f8(f8(x1891)))), % 58.95/59.00 inference(scs_inference,[],[188,2])). % 58.95/59.00 cnf(190,plain, % 58.95/59.00 (E(f8(f1(f8(x1901))),f8(f8(f1(x1901))))), % 58.95/59.00 inference(scs_inference,[],[24,188,2,3])). % 58.95/59.00 cnf(193,plain, % 58.95/59.00 (P1(x1931,f8(f1(f8(f1(f1(f6(a7,a20)))))),x1932)+~E(a16,x1932)+~E(f12(f9(a13),f10(a18)),x1931)), % 58.95/59.00 inference(scs_inference,[],[24,188,182,2,3,23,21])). % 58.95/59.00 cnf(195,plain, % 58.95/59.00 (~E(f12(f9(a13),f10(a18)),f12(x1951,x1952))+P1(x1952,f8(f1(f8(f1(f1(f6(a7,a20)))))),a16)), % 58.95/59.00 inference(scs_inference,[],[193,29])). % 58.95/59.00 cnf(196,plain, % 58.95/59.00 (P1(f10(a18),f8(f1(f8(f1(f1(f6(a7,a20)))))),a16)), % 58.95/59.00 inference(equality_inference,[],[195])). % 58.95/59.00 cnf(197,plain, % 58.95/59.00 (E(f8(f8(f1(x1971))),f8(f1(f8(x1971))))), % 58.95/59.00 inference(scs_inference,[],[190,2])). % 58.95/59.00 cnf(198,plain, % 58.95/59.00 (E(f8(f1(f8(f1(x1981)))),f8(f8(x1981)))), % 58.95/59.00 inference(scs_inference,[],[24,189,190,2,3])). % 58.95/59.00 cnf(200,plain, % 58.95/59.00 (~E(f8(f1(f8(f1(f1(f6(a7,a20)))))),f5(a20))), % 58.95/59.00 inference(scs_inference,[],[24,26,189,190,196,2,3,22])). % 58.95/59.00 cnf(205,plain, % 58.95/59.00 (E(f8(f8(x2051)),f8(f1(f8(f1(x2051)))))), % 58.95/59.00 inference(scs_inference,[],[198,2])). % 58.95/59.00 cnf(206,plain, % 58.95/59.00 (E(f8(f1(f1(f8(f1(x2061))))),f8(f8(x2061)))), % 58.95/59.00 inference(scs_inference,[],[24,198,2,3])). % 58.95/59.00 cnf(209,plain, % 58.95/59.00 (E(f8(f1(f1(f1(f8(f1(x2091)))))),f8(f8(x2091)))), % 58.95/59.00 inference(scs_inference,[],[24,206,2,3])). % 58.95/59.00 cnf(212,plain, % 58.95/59.00 (E(f8(f1(f8(f1(x2121)))),f8(f1(f8(x2121))))), % 58.95/59.00 inference(scs_inference,[],[24,209,197,2,3])). % 58.95/59.00 cnf(214,plain, % 58.95/59.00 (E(f8(f1(f8(x2141))),f8(f1(f8(f1(x2141)))))), % 58.95/59.00 inference(scs_inference,[],[212,2])). % 58.95/59.00 cnf(215,plain, % 58.95/59.00 (E(f8(f1(f1(f8(f1(x2151))))),f8(f1(f8(x2151))))), % 58.95/59.00 inference(scs_inference,[],[24,212,2,3])). % 58.95/59.00 cnf(217,plain, % 58.95/59.00 (E(f8(f1(f8(x2171))),f8(f1(f1(f8(f1(x2171))))))), % 58.95/59.00 inference(scs_inference,[],[215,2])). % 58.95/59.00 cnf(218,plain, % 58.95/59.00 (E(f8(f1(f1(f8(x2181)))),f8(f1(f8(f1(x2181)))))), % 58.95/59.00 inference(scs_inference,[],[24,215,214,2,3])). % 58.95/59.00 cnf(220,plain, % 58.95/59.00 (E(f8(f1(f8(f1(x2201)))),f8(f1(f1(f8(x2201)))))), % 58.95/59.00 inference(scs_inference,[],[218,2])). % 58.95/59.00 cnf(233,plain, % 58.95/59.00 (E(f6(f8(f1(x2331)),x2332),f6(f8(x2331),x2332))), % 58.95/59.00 inference(scs_inference,[],[33,2,6])). % 58.95/59.00 cnf(234,plain, % 58.95/59.00 (E(f6(f8(x2341),x2342),f6(f8(f1(x2341)),x2342))), % 58.95/59.00 inference(scs_inference,[],[233,2])). % 58.95/59.00 cnf(235,plain, % 58.95/59.00 (E(f6(x2351,f8(f1(x2352))),f6(x2351,f8(x2352)))), % 58.95/59.00 inference(scs_inference,[],[33,2,7])). % 58.95/59.00 cnf(236,plain, % 58.95/59.00 (E(f6(x2361,f8(x2362)),f6(x2361,f8(f1(x2362))))), % 58.95/59.00 inference(scs_inference,[],[235,2])). % 58.95/59.00 cnf(237,plain, % 58.95/59.00 (E(f6(f8(x2371),f8(f1(x2372))),f6(f8(f1(x2371)),f8(x2372)))), % 58.95/59.00 inference(scs_inference,[],[235,234,2,3])). % 58.95/59.00 cnf(240,plain, % 58.95/59.00 (E(f14(f8(f1(x2401))),f14(f8(x2401)))), % 58.95/59.00 inference(scs_inference,[],[33,2,8])). % 58.95/59.00 cnf(241,plain, % 58.95/59.00 (E(f6(f8(f1(x2411)),f8(x2412)),f6(f8(x2411),f8(f1(x2412))))), % 58.95/59.00 inference(scs_inference,[],[237,2])). % 58.95/59.00 cnf(242,plain, % 58.95/59.00 (E(f6(f8(x2421),f8(f1(x2422))),f6(f8(f1(f1(x2421))),f8(x2422)))), % 58.95/59.00 inference(scs_inference,[],[237,234,2,3])). % 58.95/59.00 cnf(244,plain, % 58.95/59.00 (E(f9(f8(f1(x2441))),f9(f8(x2441)))), % 58.95/59.00 inference(scs_inference,[],[33,2,9])). % 58.95/59.00 cnf(246,plain, % 58.95/59.00 (E(f6(f8(x2461),f8(x2462)),f6(f8(f1(f1(x2461))),f8(x2462)))), % 58.95/59.00 inference(scs_inference,[],[240,242,236,2,3])). % 58.95/59.00 cnf(249,plain, % 58.95/59.00 (E(f10(f8(f1(x2491))),f10(f8(x2491)))), % 58.95/59.00 inference(scs_inference,[],[33,2,10])). % 58.95/59.00 cnf(250,plain, % 58.95/59.00 (E(f9(f8(x2501)),f9(f8(f1(x2501))))), % 58.95/59.00 inference(scs_inference,[],[244,2])). % 58.95/59.00 cnf(251,plain, % 58.95/59.00 (E(f6(f8(f1(x2511)),f8(x2512)),f6(f8(f1(f1(x2511))),f8(f1(x2512))))), % 58.95/59.00 inference(scs_inference,[],[244,246,241,2,3])). % 58.95/59.00 cnf(253,plain, % 58.95/59.00 (E(f12(f8(f1(x2531)),x2532),f12(f8(x2531),x2532))), % 58.95/59.00 inference(scs_inference,[],[33,2,11])). % 58.95/59.00 cnf(254,plain, % 58.95/59.00 (E(f10(f8(x2541)),f10(f8(f1(x2541))))), % 58.95/59.00 inference(scs_inference,[],[249,2])). % 58.95/59.00 cnf(255,plain, % 58.95/59.00 (E(f12(f8(f1(x2551)),f4(f8(x2552),x2553)),f12(f8(x2551),f4(f8(f1(x2552)),x2553)))), % 58.95/59.00 inference(scs_inference,[],[58,249,253,2,3])). % 58.95/59.00 cnf(258,plain, % 58.95/59.00 (E(f12(x2581,f8(f1(x2582))),f12(x2581,f8(x2582)))), % 58.95/59.00 inference(scs_inference,[],[33,2,12])). % 58.95/59.00 cnf(259,plain, % 58.95/59.00 (E(f12(x2591,f8(x2592)),f12(x2591,f8(f1(x2592))))), % 58.95/59.00 inference(scs_inference,[],[258,2])). % 58.95/59.00 cnf(260,plain, % 58.95/59.00 (E(f12(f8(f1(x2601)),f8(f1(x2602))),f12(f8(x2601),f8(x2602)))), % 58.95/59.00 inference(scs_inference,[],[258,253,2,3])). % 58.95/59.00 cnf(263,plain, % 58.95/59.00 (E(f4(f8(f1(x2631)),x2632),f4(f8(x2631),x2632))), % 58.95/59.00 inference(scs_inference,[],[33,2,13])). % 58.95/59.00 cnf(264,plain, % 58.95/59.00 (E(f12(f8(x2641),f8(x2642)),f12(f8(f1(x2641)),f8(f1(x2642))))), % 58.95/59.00 inference(scs_inference,[],[260,2])). % 58.95/59.00 cnf(265,plain, % 58.95/59.00 (E(f4(f8(f1(x2651)),f11(f8(x2652),x2653)),f4(f8(x2651),f11(f8(f1(x2652)),x2653)))), % 58.95/59.00 inference(scs_inference,[],[65,260,263,2,3])). % 58.95/59.00 cnf(268,plain, % 58.95/59.00 (E(f4(x2681,f8(f1(x2682))),f4(x2681,f8(x2682)))), % 58.95/59.00 inference(scs_inference,[],[33,2,14])). % 58.95/59.01 cnf(269,plain, % 58.95/59.01 (E(f4(x2691,f8(x2692)),f4(x2691,f8(f1(x2692))))), % 58.95/59.01 inference(scs_inference,[],[268,2])). % 58.95/59.01 cnf(270,plain, % 58.95/59.01 (E(f4(f8(f1(x2701)),f8(f1(x2702))),f4(f8(x2701),f8(x2702)))), % 58.95/59.01 inference(scs_inference,[],[268,263,2,3])). % 58.95/59.01 cnf(273,plain, % 58.95/59.01 (E(f11(f8(f1(x2731)),x2732),f11(f8(x2731),x2732))), % 58.95/59.01 inference(scs_inference,[],[33,2,15])). % 58.95/59.01 cnf(274,plain, % 58.95/59.01 (E(f4(f8(x2741),f8(x2742)),f4(f8(f1(x2741)),f8(f1(x2742))))), % 58.95/59.01 inference(scs_inference,[],[270,2])). % 58.95/59.01 cnf(275,plain, % 58.95/59.01 (E(f11(f8(f1(x2751)),f3(f8(f1(x2752)),x2753,x2754)),f11(f8(x2751),f3(f8(x2752),x2753,x2754)))), % 58.95/59.01 inference(scs_inference,[],[75,270,273,2,3])). % 58.95/59.01 cnf(278,plain, % 58.95/59.01 (E(f11(x2781,f8(f1(x2782))),f11(x2781,f8(x2782)))), % 58.95/59.01 inference(scs_inference,[],[33,2,16])). % 58.95/59.01 cnf(279,plain, % 58.95/59.01 (E(f11(x2791,f8(x2792)),f11(x2791,f8(f1(x2792))))), % 58.95/59.01 inference(scs_inference,[],[278,2])). % 58.95/59.01 cnf(280,plain, % 58.95/59.01 (E(f11(f8(f1(x2801)),f8(f1(x2802))),f11(f8(x2801),f8(x2802)))), % 58.95/59.01 inference(scs_inference,[],[278,273,2,3])). % 58.95/59.01 cnf(283,plain, % 58.95/59.01 (E(f3(f8(f1(x2831)),x2832,x2833),f3(f8(x2831),x2832,x2833))), % 58.95/59.01 inference(scs_inference,[],[33,2,17])). % 58.95/59.01 cnf(284,plain, % 58.95/59.01 (E(f11(f8(x2841),f8(x2842)),f11(f8(f1(x2841)),f8(f1(x2842))))), % 58.95/59.01 inference(scs_inference,[],[280,2])). % 58.95/59.01 cnf(285,plain, % 58.95/59.01 (E(f3(f8(f1(x2851)),f3(x2852,x2853,f8(f1(x2854))),x2855),f3(f8(x2851),f3(x2852,x2853,f8(x2854)),x2855))), % 58.95/59.01 inference(scs_inference,[],[77,280,283,2,3])). % 58.95/59.01 cnf(288,plain, % 58.95/59.01 (E(f3(x2881,f8(f1(x2882)),x2883),f3(x2881,f8(x2882),x2883))), % 58.95/59.01 inference(scs_inference,[],[33,2,18])). % 58.95/59.01 cnf(289,plain, % 58.95/59.01 (E(f3(x2891,f8(x2892),x2893),f3(x2891,f8(f1(x2892)),x2893))), % 58.95/59.01 inference(scs_inference,[],[288,2])). % 58.95/59.01 cnf(290,plain, % 58.95/59.01 (E(f3(f8(f1(x2901)),f8(f1(x2902)),x2903),f3(f8(x2901),f8(x2902),x2903))), % 58.95/59.01 inference(scs_inference,[],[288,283,2,3])). % 58.95/59.01 cnf(293,plain, % 58.95/59.01 (E(f3(x2931,x2932,f8(f1(x2933))),f3(x2931,x2932,f8(x2933)))), % 58.95/59.01 inference(scs_inference,[],[33,2,19])). % 58.95/59.01 cnf(294,plain, % 58.95/59.01 (E(f3(f8(x2941),f8(x2942),x2943),f3(f8(f1(x2941)),f8(f1(x2942)),x2943))), % 58.95/59.01 inference(scs_inference,[],[290,2])). % 58.95/59.01 cnf(295,plain, % 58.95/59.01 (E(f3(f8(f1(x2951)),f8(f1(x2952)),f8(f1(x2953))),f3(f8(x2951),f8(x2952),f8(x2953)))), % 58.95/59.01 inference(scs_inference,[],[290,293,2,3])). % 58.95/59.01 cnf(298,plain, % 58.95/59.01 (E(f5(f8(f1(x2981))),f5(f8(x2981)))), % 58.95/59.01 inference(scs_inference,[],[33,2,20])). % 58.95/59.01 cnf(299,plain, % 58.95/59.01 (E(f3(f8(x2991),f8(x2992),f8(x2993)),f3(f8(f1(x2991)),f8(f1(x2992)),f8(f1(x2993))))), % 58.95/59.01 inference(scs_inference,[],[295,2])). % 58.95/59.01 cnf(300,plain, % 58.95/59.01 (E(f3(f8(f1(x3001)),f8(x3002),f8(f1(x3003))),f3(f8(x3001),f8(x3002),f8(x3003)))), % 58.95/59.01 inference(scs_inference,[],[295,289,2,3])). % 58.95/59.01 cnf(304,plain, % 58.95/59.01 (E(f5(f8(x3041)),f5(f8(f1(x3041))))), % 58.95/59.01 inference(scs_inference,[],[298,2])). % 58.95/59.01 cnf(305,plain, % 58.95/59.01 (E(f3(f8(x3051),f8(x3052),f8(f1(x3053))),f3(f8(x3051),f8(f1(x3052)),f8(x3053)))), % 58.95/59.01 inference(scs_inference,[],[298,300,294,2,3])). % 58.95/59.01 cnf(309,plain, % 58.95/59.01 (E(f3(f8(x3091),f8(f1(x3092)),f8(x3093)),f3(f8(x3091),f8(x3092),f8(f1(x3093))))), % 58.95/59.01 inference(scs_inference,[],[305,2])). % 58.95/59.01 cnf(310,plain, % 58.95/59.01 (E(f3(f8(x3101),f8(x3102),f8(x3103)),f3(f8(f1(x3101)),f8(f1(f1(x3102))),f8(x3103)))), % 58.95/59.01 inference(scs_inference,[],[305,299,2,3])). % 58.95/59.01 cnf(313,plain, % 58.95/59.01 (E(f3(f8(f1(x3131)),f8(f1(f1(x3132))),f8(x3133)),f3(f8(x3131),f8(x3132),f8(x3133)))), % 58.95/59.01 inference(scs_inference,[],[310,2])). % 58.95/59.01 cnf(314,plain, % 58.95/59.01 (E(f12(f8(x3141),f8(x3142)),f12(f8(f1(x3141)),f8(f1(f1(x3142)))))), % 58.95/59.01 inference(scs_inference,[],[310,259,264,2,3])). % 58.95/59.01 cnf(317,plain, % 58.95/59.01 (E(f6(f8(f1(f1(x3171))),f8(f1(x3172))),f6(f8(f1(x3171)),f8(x3172)))), % 58.95/59.01 inference(scs_inference,[],[251,2])). % 58.95/59.01 cnf(318,plain, % 58.95/59.01 (E(f3(f8(f1(x3181)),f8(f1(f1(f1(x3182)))),f8(x3183)),f3(f8(x3181),f8(x3182),f8(f1(x3183))))), % 58.95/59.01 inference(scs_inference,[],[313,251,309,2,3])). % 58.95/59.01 cnf(322,plain, % 58.95/59.01 (E(f11(f8(x3221),f3(f8(x3222),x3223,x3224)),f11(f8(f1(x3221)),f3(f8(f1(x3222)),x3223,x3224)))), % 58.95/59.01 inference(scs_inference,[],[275,2])). % 58.95/59.01 cnf(323,plain, % 58.95/59.01 (E(f6(f8(f1(f1(f1(x3231)))),f8(f1(x3232))),f6(f8(f1(x3231)),f8(x3232)))), % 58.95/59.01 inference(scs_inference,[],[317,275,233,2,3])). % 58.95/59.01 cnf(326,plain, % 58.95/59.01 (E(f6(f8(f1(x3261)),f8(x3262)),f6(f8(f1(f1(f1(x3261)))),f8(f1(x3262))))), % 58.95/59.01 inference(scs_inference,[],[323,2])). % 58.95/59.01 cnf(327,plain, % 58.95/59.01 (E(f6(f8(f1(x3271)),f8(f1(f1(x3272)))),f6(f8(f1(x3271)),f8(x3272)))), % 58.95/59.01 inference(scs_inference,[],[323,242,2,3])). % 58.95/59.01 cnf(330,plain, % 58.95/59.01 (E(f6(f8(f1(x3301)),f8(x3302)),f6(f8(f1(x3301)),f8(f1(f1(x3302)))))), % 58.95/59.01 inference(scs_inference,[],[327,2])). % 58.95/59.01 cnf(331,plain, % 58.95/59.01 (E(f4(f8(x3311),f8(x3312)),f4(f8(f1(x3311)),f8(f1(f1(x3312)))))), % 58.95/59.01 inference(scs_inference,[],[327,269,274,2,3])). % 58.95/59.01 cnf(334,plain, % 58.95/59.01 (E(f3(f8(x3341),f3(x3342,x3343,f8(x3344)),x3345),f3(f8(f1(x3341)),f3(x3342,x3343,f8(f1(x3344))),x3345))), % 58.95/59.01 inference(scs_inference,[],[285,2])). % 58.95/59.01 cnf(335,plain, % 58.95/59.01 (E(f11(f8(x3351),f8(x3352)),f11(f8(f1(x3351)),f8(f1(f1(x3352)))))), % 58.95/59.01 inference(scs_inference,[],[279,284,285,2,3])). % 58.95/59.01 cnf(338,plain, % 58.95/59.01 (E(f3(f8(x3381),f8(x3382),f8(f1(x3383))),f3(f8(f1(x3381)),f8(f1(f1(f1(x3382)))),f8(x3383)))), % 58.95/59.01 inference(scs_inference,[],[318,2])). % 58.95/59.01 cnf(339,plain, % 58.95/59.01 (E(f3(f8(f1(x3391)),f8(f1(f1(f1(x3392)))),f8(f1(x3393))),f3(f8(x3391),f8(x3392),f8(f1(x3393))))), % 58.95/59.01 inference(scs_inference,[],[318,293,2,3])). % 58.95/59.01 cnf(343,plain, % 58.95/59.01 (E(f3(f8(x3431),f8(x3432),f8(f1(x3433))),f3(f8(f1(x3431)),f8(f1(f1(f1(x3432)))),f8(f1(x3433))))), % 58.95/59.01 inference(scs_inference,[],[339,2])). % 58.95/59.01 cnf(344,plain, % 58.95/59.01 (E(f11(f8(x3441),f3(f8(f1(x3442)),x3443,x3444)),f11(f8(f1(x3441)),f3(f8(f1(x3442)),x3443,x3444)))), % 58.95/59.01 inference(scs_inference,[],[75,339,322,2,3])). % 58.95/59.01 cnf(348,plain, % 58.95/59.01 (E(f12(f8(x3481),f4(f8(f1(x3482)),x3483)),f12(f8(f1(x3481)),f4(f8(x3482),x3483)))), % 58.95/59.01 inference(scs_inference,[],[255,2])). % 58.95/59.01 cnf(349,plain, % 58.95/59.01 (E(f3(f8(x3491),f3(x3492,x3493,f8(f1(x3494))),x3495),f3(f8(f1(x3491)),f3(x3492,x3493,f8(f1(x3494))),x3495))), % 58.95/59.01 inference(scs_inference,[],[77,255,334,2,3])). % 58.95/59.01 cnf(353,plain, % 58.95/59.01 (E(f4(f8(x3531),f11(f8(f1(x3532)),x3533)),f4(f8(f1(x3531)),f11(f8(x3532),x3533)))), % 58.95/59.01 inference(scs_inference,[],[265,2])). % 58.95/59.01 cnf(354,plain, % 58.95/59.01 (E(f12(f8(x3541),f4(f8(f1(f1(x3542))),x3543)),f12(f8(f1(x3541)),f4(f8(x3542),x3543)))), % 58.95/59.01 inference(scs_inference,[],[57,348,265,2,3])). % 58.95/59.01 cnf(359,plain, % 58.95/59.01 (E(f4(f8(x3591),f11(f8(f1(f1(x3592))),x3593)),f4(f8(f1(x3591)),f11(f8(x3592),x3593)))), % 58.95/59.01 inference(scs_inference,[],[64,353,354,2,3])). % 58.95/59.01 cnf(364,plain, % 58.95/59.01 (E(f3(f8(x3641),f8(x3642),f8(f1(f1(x3643)))),f3(f8(x3641),f8(f1(f1(f1(x3642)))),f8(x3643)))), % 58.95/59.01 inference(scs_inference,[],[338,359,300,2,3])). % 58.95/59.01 cnf(368,plain, % 58.95/59.01 (E(f3(f8(x3681),f8(f1(f1(f1(x3682)))),f8(x3683)),f3(f8(x3681),f8(x3682),f8(f1(f1(x3683)))))), % 58.95/59.01 inference(scs_inference,[],[364,2])). % 58.95/59.01 cnf(369,plain, % 58.95/59.01 (E(f3(f8(f1(x3691)),f8(x3692),f8(f1(f1(x3693)))),f3(f8(x3691),f8(f1(x3692)),f8(x3693)))), % 58.95/59.01 inference(scs_inference,[],[364,313,2,3])). % 58.95/59.01 cnf(373,plain, % 58.95/59.01 (E(f3(f8(x3731),f8(f1(x3732)),f8(x3733)),f3(f8(f1(x3731)),f8(x3732),f8(f1(f1(x3733)))))), % 58.95/59.01 inference(scs_inference,[],[369,2])). % 58.95/59.01 cnf(374,plain, % 58.95/59.01 (E(f3(f8(x3741),f8(x3742),f8(f1(f1(x3743)))),f3(f8(x3741),f8(f1(f1(f1(f1(x3742))))),f8(x3743)))), % 58.95/59.01 inference(scs_inference,[],[369,343,2,3])). % 58.95/59.01 cnf(378,plain, % 58.95/59.01 (E(f3(f8(x3781),f8(f1(f1(f1(f1(x3782))))),f8(x3783)),f3(f8(x3781),f8(x3782),f8(f1(f1(x3783)))))), % 58.95/59.01 inference(scs_inference,[],[374,2])). % 58.95/59.01 cnf(379,plain, % 58.95/59.01 (E(f6(f8(f1(x3791)),f8(x3792)),f6(f8(f1(f1(f1(x3791)))),f8(f1(f1(x3792)))))), % 58.95/59.01 inference(scs_inference,[],[374,326,236,2,3])). % 58.95/59.01 cnf(382,plain, % 58.95/59.01 (E(f12(f8(f1(x3821)),f8(f1(f1(x3822)))),f12(f8(x3821),f8(x3822)))), % 58.95/59.01 inference(scs_inference,[],[314,2])). % 58.95/59.01 cnf(383,plain, % 58.95/59.01 (E(f3(f8(x3831),f8(f1(f1(f1(x3832)))),f8(x3833)),f3(f8(f1(x3831)),f8(f1(f1(f1(x3832)))),f8(f1(x3833))))), % 58.95/59.01 inference(scs_inference,[],[314,368,338,2,3])). % 58.95/59.01 cnf(386,plain, % 58.95/59.01 (E(f4(f8(f1(x3861)),f8(f1(f1(x3862)))),f4(f8(x3861),f8(x3862)))), % 58.95/59.01 inference(scs_inference,[],[331,2])). % 58.95/59.01 cnf(387,plain, % 58.95/59.01 (E(f12(f8(f1(f1(x3871))),f8(f1(f1(f1(x3872))))),f12(f8(x3871),f8(x3872)))), % 58.95/59.01 inference(scs_inference,[],[382,331,260,2,3])). % 58.95/59.01 cnf(390,plain, % 58.95/59.01 (E(f12(f8(x3901),f8(x3902)),f12(f8(f1(f1(x3901))),f8(f1(f1(f1(x3902))))))), % 58.95/59.01 inference(scs_inference,[],[387,2])). % 58.95/59.01 cnf(391,plain, % 58.95/59.01 (E(f4(f8(f1(f1(x3911))),f8(f1(f1(f1(x3912))))),f4(f8(x3911),f8(x3912)))), % 58.95/59.01 inference(scs_inference,[],[386,387,270,2,3])). % 58.95/59.01 cnf(394,plain, % 58.95/59.01 (E(f4(f8(x3941),f8(x3942)),f4(f8(f1(f1(x3941))),f8(f1(f1(f1(x3942))))))), % 58.95/59.01 inference(scs_inference,[],[391,2])). % 58.95/59.01 cnf(395,plain, % 58.95/59.01 (E(f6(f8(f1(x3951)),f8(x3952)),f6(f8(x3951),f8(f1(f1(f1(x3952))))))), % 58.95/59.01 inference(scs_inference,[],[391,330,241,2,3])). % 58.95/59.01 cnf(398,plain, % 58.95/59.01 (E(f11(f8(f1(x3981)),f8(f1(f1(x3982)))),f11(f8(x3981),f8(x3982)))), % 58.95/59.01 inference(scs_inference,[],[335,2])). % 58.95/59.01 cnf(399,plain, % 58.95/59.01 (E(f11(f8(x3991),f8(x3992)),f11(f8(f1(x3991)),f8(f1(f1(f1(x3992))))))), % 58.95/59.01 inference(scs_inference,[],[335,279,2,3])). % 58.95/59.01 cnf(402,plain, % 58.95/59.01 (E(f6(f8(f1(f1(f1(x4021)))),f8(f1(f1(x4022)))),f6(f8(f1(x4021)),f8(x4022)))), % 58.95/59.01 inference(scs_inference,[],[379,2])). % 58.95/59.01 cnf(403,plain, % 58.95/59.01 (E(f11(f8(f1(f1(x4031))),f8(f1(f1(f1(x4032))))),f11(f8(x4031),f8(x4032)))), % 58.95/59.01 inference(scs_inference,[],[398,379,280,2,3])). % 58.95/59.01 cnf(406,plain, % 58.95/59.01 (E(f11(f8(x4061),f8(x4062)),f11(f8(f1(f1(x4061))),f8(f1(f1(f1(x4062))))))), % 58.95/59.01 inference(scs_inference,[],[403,2])). % 58.95/59.01 cnf(407,plain, % 58.95/59.01 (E(f6(f8(f1(f1(f1(f1(x4071))))),f8(x4072)),f6(f8(f1(x4071)),f8(f1(x4072))))), % 58.95/59.01 inference(scs_inference,[],[402,403,395,2,3])). % 58.95/59.01 cnf(411,plain, % 58.95/59.01 (E(f6(f8(f1(x4111)),f8(f1(x4112))),f6(f8(f1(f1(f1(f1(x4111))))),f8(x4112)))), % 58.95/59.01 inference(scs_inference,[],[407,2])). % 58.95/59.01 cnf(412,plain, % 58.95/59.01 (E(f6(f8(f1(f1(f1(f1(x4121))))),f8(f1(x4122))),f6(f8(f1(x4121)),f8(x4122)))), % 58.95/59.01 inference(scs_inference,[],[407,327,2,3])). % 58.95/59.01 cnf(416,plain, % 58.95/59.01 (E(f6(f8(f1(x4161)),f8(x4162)),f6(f8(f1(f1(f1(f1(x4161))))),f8(f1(x4162))))), % 58.95/59.01 inference(scs_inference,[],[412,2])). % 58.95/59.01 cnf(417,plain, % 58.95/59.01 (E(f6(f8(f1(x4171)),f8(f1(f1(x4172)))),f6(f8(f1(f1(f1(x4171)))),f8(x4172)))), % 58.95/59.01 inference(scs_inference,[],[411,412,317,2,3])). % 58.95/59.01 cnf(421,plain, % 58.95/59.01 (E(f6(f8(f1(f1(f1(x4211)))),f8(x4212)),f6(f8(f1(x4211)),f8(f1(f1(x4212)))))), % 58.95/59.01 inference(scs_inference,[],[417,2])). % 58.95/59.01 cnf(422,plain, % 58.95/59.01 (E(f6(f8(f1(f1(x4221))),f8(f1(f1(f1(x4222))))),f6(f8(f1(x4221)),f8(x4222)))), % 58.95/59.01 inference(scs_inference,[],[417,412,2,3])). % 58.95/59.01 cnf(426,plain, % 58.95/59.01 (E(f3(f8(x4261),f8(f1(f1(f1(x4262)))),f8(x4263)),f3(f8(x4261),f8(x4262),f8(f1(x4263))))), % 58.95/59.01 inference(scs_inference,[],[422,383,339,2,3])). % 58.95/59.01 cnf(429,plain, % 58.95/59.01 (E(f3(f8(x4291),f8(x4292),f8(f1(x4293))),f3(f8(x4291),f8(f1(f1(f1(x4292)))),f8(x4293)))), % 58.95/59.01 inference(scs_inference,[],[426,2])). % 58.95/59.01 cnf(430,plain, % 58.95/59.01 (E(f3(f8(x4301),f8(f1(f1(f1(x4302)))),f8(x4303)),f3(f8(f1(x4301)),f8(f1(f1(x4302))),f8(f1(x4303))))), % 58.95/59.01 inference(scs_inference,[],[426,310,2,3])). % 58.95/59.01 cnf(433,plain, % 58.95/59.01 (E(f3(f8(f1(x4331)),f8(f1(f1(x4332))),f8(f1(x4333))),f3(f8(x4331),f8(f1(f1(f1(x4332)))),f8(x4333)))), % 58.95/59.01 inference(scs_inference,[],[430,2])). % 58.95/59.01 cnf(434,plain, % 58.95/59.01 (E(f3(f8(x4341),f8(x4342),f8(f1(x4343))),f3(f8(f1(x4341)),f8(f1(f1(x4342))),f8(f1(f1(x4343)))))), % 58.95/59.01 inference(scs_inference,[],[429,430,373,2,3])). % 58.95/59.01 cnf(437,plain, % 58.95/59.01 (E(f3(f8(f1(x4371)),f8(f1(f1(x4372))),f8(f1(f1(x4373)))),f3(f8(x4371),f8(x4372),f8(f1(x4373))))), % 58.95/59.01 inference(scs_inference,[],[434,2])). % 58.95/59.01 cnf(442,plain, % 58.95/59.01 (E(f11(f8(f1(x4421)),f8(f1(f1(f1(x4422))))),f11(f8(x4421),f8(x4422)))), % 58.95/59.01 inference(scs_inference,[],[399,2])). % 58.95/59.01 cnf(446,plain, % 58.95/59.01 (E(f6(f8(f1(f1(x4461))),f8(x4462)),f6(f8(x4461),f8(x4462)))), % 58.95/59.01 inference(scs_inference,[],[246,2])). % 58.95/59.01 cnf(447,plain, % 58.95/59.01 (E(f11(f8(x4471),f8(x4472)),f11(f8(f1(x4471)),f8(x4472)))), % 58.95/59.01 inference(scs_inference,[],[442,406,246,2,3])). % 58.95/59.01 cnf(450,plain, % 58.95/59.01 (E(f6(f8(x4501),f8(f1(f1(f1(x4502))))),f6(f8(f1(x4501)),f8(x4502)))), % 58.95/59.01 inference(scs_inference,[],[395,2])). % 58.95/59.01 cnf(451,plain, % 58.95/59.01 (E(f11(f8(f1(x4511)),f8(f1(f1(x4512)))),f11(f8(f1(x4511)),f8(x4512)))), % 58.95/59.01 inference(scs_inference,[],[447,398,395,2,3])). % 58.95/59.01 cnf(454,plain, % 58.95/59.01 (E(f11(f8(f1(x4541)),f8(x4542)),f11(f8(f1(x4541)),f8(f1(f1(x4542)))))), % 58.95/59.01 inference(scs_inference,[],[451,2])). % 58.95/59.01 cnf(455,plain, % 58.95/59.01 (E(f6(f8(f1(x4551)),f8(f1(f1(f1(x4552))))),f6(f8(x4551),f8(x4552)))), % 58.95/59.01 inference(scs_inference,[],[446,450,451,2,3])). % 58.95/59.01 cnf(459,plain, % 58.95/59.01 (E(f6(f8(x4591),f8(x4592)),f6(f8(f1(x4591)),f8(f1(f1(f1(x4592))))))), % 58.95/59.01 inference(scs_inference,[],[455,2])). % 58.95/59.01 cnf(460,plain, % 58.95/59.01 (E(f11(f8(f1(f1(x4601))),f8(f1(x4602))),f11(f8(x4601),f8(x4602)))), % 58.95/59.01 inference(scs_inference,[],[455,454,403,2,3])). % 58.95/59.01 cnf(463,plain, % 58.95/59.01 (E(f11(f8(x4631),f8(x4632)),f11(f8(f1(f1(x4631))),f8(f1(x4632))))), % 58.95/59.01 inference(scs_inference,[],[460,2])). % 58.95/59.01 cnf(464,plain, % 58.95/59.01 (E(f11(f8(x4641),f3(f8(x4642),x4643,x4644)),f11(f8(f1(x4641)),f3(f8(f1(f1(x4642))),x4643,x4644)))), % 58.95/59.01 inference(scs_inference,[],[74,460,322,2,3])). % 58.95/59.01 cnf(469,plain, % 58.95/59.01 (E(f11(f8(f1(x4691)),f8(f1(f1(f1(x4692))))),f11(f8(f1(f1(x4691))),f8(f1(x4692))))), % 58.95/59.01 inference(scs_inference,[],[463,464,442,2,3])). % 58.95/59.01 cnf(472,plain, % 58.95/59.01 (E(f11(f8(f1(f1(x4721))),f8(f1(x4722))),f11(f8(f1(x4721)),f8(f1(f1(f1(x4722))))))), % 58.95/59.01 inference(scs_inference,[],[469,2])). % 58.95/59.01 cnf(473,plain, % 58.95/59.01 (E(f11(f8(x4731),f8(f1(f1(f1(x4732))))),f11(f8(f1(f1(x4731))),f8(f1(x4732))))), % 58.95/59.01 inference(scs_inference,[],[469,447,2,3])). % 58.95/59.01 cnf(476,plain, % 58.95/59.01 (E(f11(f8(f1(f1(x4761))),f8(f1(x4762))),f11(f8(x4761),f8(f1(f1(f1(x4762))))))), % 58.95/59.01 inference(scs_inference,[],[473,2])). % 58.95/59.01 cnf(477,plain, % 58.95/59.01 (E(f11(f8(x4771),f3(f8(f1(f1(x4772))),x4773,x4774)),f11(f8(f1(x4771)),f3(f8(f1(x4772)),x4773,x4774)))), % 58.95/59.01 inference(scs_inference,[],[75,473,344,2,3])). % 58.95/59.01 cnf(481,plain, % 58.95/59.01 (E(f11(f8(f1(x4811)),f3(f8(f1(x4812)),x4813,x4814)),f11(f8(x4811),f3(f8(f1(f1(x4812))),x4813,x4814)))), % 58.95/59.01 inference(scs_inference,[],[477,2])). % 58.95/59.01 cnf(482,plain, % 58.95/59.01 (E(f11(f8(f1(f1(f1(x4821)))),f8(f1(x4822))),f11(f8(x4821),f8(f1(f1(x4822)))))), % 58.95/59.01 inference(scs_inference,[],[477,472,460,2,3])). % 58.95/59.01 cnf(486,plain, % 58.95/59.01 (E(f11(f8(x4861),f8(f1(f1(x4862)))),f11(f8(f1(f1(f1(x4861)))),f8(f1(x4862))))), % 58.95/59.01 inference(scs_inference,[],[482,2])). % 58.95/59.01 cnf(487,plain, % 58.95/59.01 (E(f11(f8(f1(x4871)),f3(f8(x4872),x4873,x4874)),f11(f8(x4871),f3(f8(f1(f1(x4872))),x4873,x4874)))), % 58.95/59.01 inference(scs_inference,[],[74,482,481,2,3])). % 58.95/59.01 cnf(492,plain, % 58.95/59.01 (E(f11(f8(x4921),f8(f1(f1(f1(x4922))))),f11(f8(f1(f1(f1(x4921)))),f8(x4922)))), % 58.95/59.01 inference(scs_inference,[],[486,487,451,2,3])). % 58.95/59.01 cnf(497,plain, % 58.95/59.01 (E(f11(f8(f1(f1(x4971))),f8(f1(x4972))),f11(f8(f1(f1(f1(x4971)))),f8(x4972)))), % 58.95/59.01 inference(scs_inference,[],[492,476,2,3])). % 58.95/59.01 cnf(500,plain, % 58.95/59.01 (E(f11(f8(f1(f1(f1(x5001)))),f8(x5002)),f11(f8(f1(f1(x5001))),f8(f1(x5002))))), % 58.95/59.01 inference(scs_inference,[],[497,2])). % 58.95/59.01 cnf(501,plain, % 58.95/59.01 (E(f3(f8(x5011),f3(x5012,x5013,f8(x5014)),x5015),f3(f8(f1(x5011)),f3(x5012,x5013,f8(f1(f1(x5014)))),x5015))), % 58.95/59.01 inference(scs_inference,[],[76,497,334,2,3])). % 58.95/59.01 cnf(506,plain, % 58.95/59.01 (E(f3(f8(x5061),f3(x5062,x5063,f8(f1(f1(x5064)))),x5065),f3(f8(f1(x5061)),f3(x5062,x5063,f8(f1(x5064))),x5065))), % 58.95/59.01 inference(scs_inference,[],[77,349,501,2,3])). % 58.95/59.01 cnf(510,plain, % 58.95/59.01 (E(f3(f8(f1(x5101)),f3(x5102,x5103,f8(f1(x5104))),x5105),f3(f8(x5101),f3(x5102,x5103,f8(f1(f1(x5104)))),x5105))), % 58.95/59.01 inference(scs_inference,[],[506,2])). % 58.95/59.01 cnf(511,plain, % 58.95/59.01 (E(f3(f8(f1(x5111)),f8(f1(f1(x5112))),f8(f1(x5113))),f3(f8(x5111),f8(x5112),f8(f1(f1(x5113)))))), % 58.95/59.01 inference(scs_inference,[],[433,506,368,2,3])). % 58.95/59.01 cnf(514,plain, % 58.95/59.01 (E(f3(f8(x5141),f8(x5142),f8(f1(f1(x5143)))),f3(f8(f1(x5141)),f8(f1(f1(x5142))),f8(f1(x5143))))), % 58.95/59.01 inference(scs_inference,[],[511,2])). % 58.95/59.01 cnf(515,plain, % 58.95/59.01 (E(f3(f8(f1(x5151)),f3(x5152,x5153,f8(x5154)),x5155),f3(f8(x5151),f3(x5152,x5153,f8(f1(f1(x5154)))),x5155))), % 58.95/59.01 inference(scs_inference,[],[76,511,510,2,3])). % 58.95/59.01 cnf(519,plain, % 58.95/59.01 (E(f3(f8(x5191),f3(x5192,x5193,f8(f1(f1(x5194)))),x5195),f3(f8(f1(x5191)),f3(x5192,x5193,f8(x5194)),x5195))), % 58.95/59.01 inference(scs_inference,[],[515,2])). % 58.95/59.01 cnf(520,plain, % 58.95/59.01 (E(f3(f8(x5201),f8(x5202),f8(f1(f1(f1(x5203))))),f3(f8(x5201),f8(x5202),f8(f1(x5203))))), % 58.95/59.01 inference(scs_inference,[],[437,514,515,2,3])). % 58.95/59.01 cnf(525,plain, % 58.95/59.01 (E(f3(f8(x5251),f8(f1(f1(f1(f1(x5252))))),f8(f1(x5253))),f3(f8(x5251),f8(x5252),f8(f1(x5253))))), % 58.95/59.01 inference(scs_inference,[],[520,378,2,3])). % 58.95/59.01 cnf(529,plain, % 58.95/59.01 (E(f3(f8(x5291),f8(x5292),f8(f1(x5293))),f3(f8(x5291),f8(f1(f1(f1(f1(x5292))))),f8(f1(x5293))))), % 58.95/59.01 inference(scs_inference,[],[525,2])). % 58.95/59.01 cnf(530,plain, % 58.95/59.01 (E(f3(f8(x5301),f8(f1(f1(f1(f1(x5302))))),f8(f1(x5303))),f3(f8(x5301),f8(f1(x5302)),f8(f1(x5303))))), % 58.95/59.01 inference(scs_inference,[],[525,289,2,3])). % 58.95/59.01 cnf(533,plain, % 58.95/59.01 (E(f3(f8(x5331),f8(f1(x5332)),f8(f1(x5333))),f3(f8(x5331),f8(f1(f1(f1(f1(x5332))))),f8(f1(x5333))))), % 58.95/59.01 inference(scs_inference,[],[530,2])). % 58.95/59.01 cnf(534,plain, % 58.95/59.01 (E(f3(f8(x5341),f8(x5342),f8(f1(x5343))),f3(f8(x5341),f8(f1(f1(f1(x5342)))),f8(f1(f1(x5343)))))), % 58.95/59.01 inference(scs_inference,[],[529,530,309,2,3])). % 58.95/59.01 cnf(537,plain, % 58.95/59.01 (E(f3(f8(x5371),f8(f1(f1(f1(x5372)))),f8(f1(f1(x5373)))),f3(f8(x5371),f8(x5372),f8(f1(x5373))))), % 58.95/59.01 inference(scs_inference,[],[534,2])). % 58.95/59.01 cnf(538,plain, % 58.95/59.01 (E(f3(f8(f1(x5381)),f8(f1(x5382)),f8(f1(f1(x5383)))),f3(f8(x5381),f8(f1(f1(x5382))),f8(f1(x5383))))), % 58.95/59.01 inference(scs_inference,[],[533,534,437,2,3])). % 58.95/59.01 cnf(542,plain, % 58.95/59.01 (E(f3(f8(x5421),f8(f1(f1(x5422))),f8(f1(x5423))),f3(f8(f1(x5421)),f8(f1(x5422)),f8(f1(f1(x5423)))))), % 58.95/59.01 inference(scs_inference,[],[538,2])). % 58.95/59.01 cnf(543,plain, % 58.95/59.01 (E(f3(f8(f1(x5431)),f8(f1(f1(x5432))),f8(f1(f1(f1(x5433))))),f3(f8(x5431),f8(x5432),f8(f1(x5433))))), % 58.95/59.01 inference(scs_inference,[],[537,538,2,3])). % 58.95/59.01 cnf(548,plain, % 58.95/59.01 (E(f11(f8(f1(f1(f1(f1(x5481))))),f8(x5482)),f11(f8(x5481),f8(f1(f1(x5482)))))), % 58.95/59.01 inference(scs_inference,[],[500,543,482,2,3])). % 58.95/59.01 cnf(552,plain, % 58.95/59.01 (E(f3(f8(x5521),f8(f1(f1(f1(f1(x5522))))),f8(f1(x5523))),f3(f8(f1(x5521)),f8(x5522),f8(f1(x5523))))), % 58.95/59.01 inference(scs_inference,[],[542,548,537,2,3])). % 58.95/59.01 cnf(555,plain, % 58.95/59.01 (~E(x5551,a16)+P1(x5552,f8(f1(f1(f6(a7,a20)))),x5551)+~E(f12(f9(a13),f10(a18)),x5552)), % 58.95/59.01 inference(scs_inference,[],[2,110])). % 58.95/59.01 cnf(556,plain, % 58.95/59.01 (E(f3(f8(f1(x5561)),f8(x5562),f8(f1(x5563))),f3(f8(x5561),f8(f1(f1(f1(f1(x5562))))),f8(f1(x5563))))), % 58.95/59.01 inference(scs_inference,[],[552,2])). % 58.95/59.01 cnf(557,plain, % 58.95/59.01 (E(f6(f8(f1(x5571)),f8(x5572)),f6(f8(f1(f1(f1(f1(x5571))))),f8(x5572)))), % 58.95/59.01 inference(scs_inference,[],[416,552,235,2,3])). % 58.95/59.01 cnf(559,plain, % 58.95/59.01 (~E(f12(f9(a13),f10(a18)),f12(x5591,x5592))+P1(x5592,f8(f1(f1(f6(a7,a20)))),a16)), % 58.95/59.01 inference(scs_inference,[],[555,29])). % 58.95/59.01 cnf(560,plain, % 58.95/59.01 (P1(f10(a18),f8(f1(f1(f6(a7,a20)))),a16)), % 58.95/59.01 inference(equality_inference,[],[559])). % 58.95/59.01 cnf(561,plain, % 58.95/59.01 (E(f6(f8(f1(f1(f1(f1(x5611))))),f8(x5612)),f6(f8(f1(x5611)),f8(x5612)))), % 58.95/59.01 inference(scs_inference,[],[557,2])). % 58.95/59.01 cnf(562,plain, % 58.95/59.01 (~E(f8(f1(f1(f6(a7,a20)))),f5(a20))), % 58.95/59.01 inference(scs_inference,[],[26,557,560,2,22])). % 58.95/59.01 cnf(563,plain, % 58.95/59.01 (E(f6(f8(f1(x5631)),f8(x5632)),f6(f8(f1(f1(x5631))),f8(f1(f1(x5632)))))), % 58.95/59.01 inference(scs_inference,[],[26,557,421,560,2,22,3])). % 58.95/59.01 cnf(570,plain, % 58.95/59.02 (E(f6(f8(f1(f1(x5701))),f8(f1(f1(x5702)))),f6(f8(f1(x5701)),f8(x5702)))), % 58.95/59.02 inference(scs_inference,[],[563,2])). % 58.95/59.02 cnf(571,plain, % 58.95/59.02 (E(f6(f8(f1(f1(f1(f1(f1(x5711)))))),f8(x5712)),f6(f8(x5711),f8(x5712)))), % 58.95/59.02 inference(scs_inference,[],[561,563,446,2,3])). % 58.95/59.02 cnf(576,plain, % 58.95/59.02 (E(f6(f8(x5761),f8(x5762)),f6(f8(f1(f1(f1(f1(f1(x5761)))))),f8(x5762)))), % 58.95/59.02 inference(scs_inference,[],[571,2])). % 58.95/59.02 cnf(577,plain, % 58.95/59.02 (E(f3(f8(f1(x5771)),f8(x5772),f8(f1(x5773))),f3(f8(x5771),f8(f1(x5772)),f8(f1(x5773))))), % 58.95/59.02 inference(scs_inference,[],[571,556,530,2,3])). % 58.95/59.02 cnf(580,plain, % 58.95/59.02 (E(f3(f8(x5801),f8(f1(x5802)),f8(f1(x5803))),f3(f8(f1(x5801)),f8(x5802),f8(f1(x5803))))), % 58.95/59.02 inference(scs_inference,[],[577,2])). % 58.95/59.02 cnf(581,plain, % 58.95/59.02 (E(f6(f8(x5811),f8(f1(f1(x5812)))),f6(f8(f1(f1(f1(f1(x5811))))),f8(x5812)))), % 58.95/59.02 inference(scs_inference,[],[570,576,577,2,3])). % 58.95/59.02 cnf(585,plain, % 58.95/59.02 (E(f6(f8(f1(f1(f1(f1(x5851))))),f8(x5852)),f6(f8(x5851),f8(f1(f1(x5852)))))), % 58.95/59.02 inference(scs_inference,[],[581,2])). % 58.95/59.02 cnf(586,plain, % 58.95/59.02 (E(f3(f8(x5861),f8(f1(x5862)),f8(f1(x5863))),f3(f8(f1(x5861)),f8(f1(f1(f1(x5862)))),f8(x5863)))), % 58.95/59.02 inference(scs_inference,[],[581,580,429,2,3])). % 58.95/59.02 cnf(589,plain, % 58.95/59.02 (E(f3(f8(f1(x5891)),f8(f1(f1(f1(x5892)))),f8(x5893)),f3(f8(x5891),f8(f1(x5892)),f8(f1(x5893))))), % 58.95/59.02 inference(scs_inference,[],[586,2])). % 58.95/59.02 cnf(590,plain, % 58.95/59.02 (E(f3(f8(x5901),f8(f1(x5902)),f8(f1(x5903))),f3(f8(f1(f1(x5901))),f8(f1(f1(f1(x5902)))),f8(f1(x5903))))), % 58.95/59.02 inference(scs_inference,[],[586,383,2,3])). % 58.95/59.02 cnf(593,plain, % 58.95/59.02 (E(f3(f8(f1(f1(x5931))),f8(f1(f1(f1(x5932)))),f8(f1(x5933))),f3(f8(x5931),f8(f1(x5932)),f8(f1(x5933))))), % 58.95/59.02 inference(scs_inference,[],[590,2])). % 58.95/59.02 cnf(594,plain, % 58.95/59.02 (E(f3(f8(x5941),f8(f1(x5942)),f8(f1(x5943))),f3(f8(f1(x5941)),f8(f1(x5942)),f8(f1(f1(x5943)))))), % 58.95/59.02 inference(scs_inference,[],[589,590,2,3])). % 58.95/59.02 cnf(597,plain, % 58.95/59.02 (E(f6(f8(f1(f1(x5971))),f8(x5972)),f6(f8(x5971),f8(f1(x5972))))), % 58.95/59.02 inference(scs_inference,[],[242,2])). % 58.95/59.02 cnf(598,plain, % 58.95/59.02 (E(f12(f8(f1(x5981)),f4(f8(f1(x5982)),x5983)),f12(f8(x5981),f4(f8(x5982),x5983)))), % 58.95/59.02 inference(scs_inference,[],[57,242,253,2,3])). % 58.95/59.02 cnf(602,plain, % 58.95/59.02 (E(f12(f8(x6021),f4(f8(x6022),x6023)),f12(f8(f1(x6021)),f4(f8(f1(x6022)),x6023)))), % 58.95/59.02 inference(scs_inference,[],[598,2])). % 58.95/59.02 cnf(603,plain, % 58.95/59.02 (E(f6(f8(f1(f1(f1(x6031)))),f8(f1(f1(x6032)))),f6(f8(x6031),f8(x6032)))), % 58.95/59.02 inference(scs_inference,[],[597,598,455,2,3])). % 58.95/59.02 cnf(606,plain, % 58.95/59.02 (E(f6(f8(x6061),f8(x6062)),f6(f8(f1(f1(f1(x6061)))),f8(f1(f1(x6062)))))), % 58.95/59.02 inference(scs_inference,[],[603,2])). % 58.95/59.02 cnf(607,plain, % 58.95/59.02 (E(f12(f8(x6071),f4(f8(x6072),x6073)),f12(f8(f1(x6071)),f4(f8(f1(f1(x6072))),x6073)))), % 58.95/59.02 inference(scs_inference,[],[58,603,602,2,3])). % 58.95/59.02 cnf(612,plain, % 58.95/59.02 (E(f6(f8(f1(x6121)),f8(x6122)),f6(f8(x6121),f8(f1(f1(f1(f1(x6122)))))))), % 58.95/59.02 inference(scs_inference,[],[585,606,607,2,3])). % 58.95/59.02 cnf(616,plain, % 58.95/59.02 (E(f6(f8(x6161),f8(f1(f1(f1(f1(x6162)))))),f6(f8(f1(x6161)),f8(x6162)))), % 58.95/59.02 inference(scs_inference,[],[612,2])). % 58.95/59.02 cnf(617,plain, % 58.95/59.02 (E(f6(f8(x6171),f8(x6172)),f6(f8(f1(f1(f1(f1(x6171))))),f8(f1(f1(x6172)))))), % 58.95/59.02 inference(scs_inference,[],[459,612,411,2,3])). % 58.95/59.02 cnf(621,plain, % 58.95/59.02 (E(f6(f8(x6211),f8(f1(f1(f1(f1(x6212)))))),f6(f8(x6211),f8(x6212)))), % 58.95/59.02 inference(scs_inference,[],[616,617,233,2,3])). % 58.95/59.02 cnf(625,plain, % 58.95/59.02 (E(f12(f8(x6251),f8(x6252)),f12(f8(f1(f1(x6251))),f8(f1(f1(x6252)))))), % 58.95/59.02 inference(scs_inference,[],[621,390,258,2,3])). % 58.95/59.02 cnf(628,plain, % 58.95/59.02 (E(f12(f8(f1(f1(x6281))),f8(f1(f1(x6282)))),f12(f8(x6281),f8(x6282)))), % 58.95/59.02 inference(scs_inference,[],[625,2])). % 58.95/59.02 cnf(629,plain, % 58.95/59.02 (E(f12(f8(f1(x6291)),f8(f1(f1(x6292)))),f12(f8(f1(f1(x6291))),f8(f1(f1(x6292)))))), % 58.95/59.02 inference(scs_inference,[],[625,382,2,3])). % 58.95/59.02 cnf(632,plain, % 58.95/59.02 (E(f4(f8(x6321),x6322),f4(f8(f1(x6321)),x6322))), % 58.95/59.02 inference(scs_inference,[],[263,2])). % 58.95/59.02 cnf(633,plain, % 58.95/59.02 (E(f12(f8(f1(f1(x6331))),f8(f1(f1(x6332)))),f12(f8(x6331),f8(f1(x6332))))), % 58.95/59.02 inference(scs_inference,[],[628,259,263,2,3])). % 58.95/59.02 cnf(636,plain, % 58.95/59.02 (E(f12(f8(x6361),f8(f1(x6362))),f12(f8(f1(f1(x6361))),f8(f1(f1(x6362)))))), % 58.95/59.02 inference(scs_inference,[],[633,2])). % 58.95/59.02 cnf(637,plain, % 58.95/59.02 (E(f4(f8(x6371),f8(x6372)),f4(f8(f1(f1(f1(x6371)))),f8(f1(f1(f1(x6372))))))), % 58.95/59.02 inference(scs_inference,[],[632,633,394,2,3])). % 58.95/59.02 cnf(642,plain, % 58.95/59.02 (E(f12(f8(x6421),f8(f1(x6422))),f12(f8(f1(f1(f1(x6421)))),f8(f1(f1(x6422)))))), % 58.95/59.02 inference(scs_inference,[],[629,636,637,2,3])). % 58.95/59.02 cnf(645,plain, % 58.95/59.02 (E(f12(f8(f1(f1(f1(x6451)))),f8(f1(f1(x6452)))),f12(f8(x6451),f8(f1(x6452))))), % 58.95/59.02 inference(scs_inference,[],[642,2])). % 58.95/59.02 cnf(646,plain, % 58.95/59.02 (E(f12(f8(x6461),f8(f1(f1(x6462)))),f12(f8(f1(x6461)),f8(x6462)))), % 58.95/59.02 inference(scs_inference,[],[642,387,2,3])). % 58.95/59.02 cnf(650,plain, % 58.95/59.02 (E(f12(f8(f1(x6501)),f8(x6502)),f12(f8(x6501),f8(f1(f1(x6502)))))), % 58.95/59.02 inference(scs_inference,[],[646,2])). % 58.95/59.02 cnf(651,plain, % 58.95/59.02 (E(f12(f8(f1(x6511)),f8(f1(f1(f1(f1(x6512)))))),f12(f8(x6511),f8(x6512)))), % 58.95/59.02 inference(scs_inference,[],[646,628,2,3])). % 58.95/59.02 cnf(654,plain, % 58.95/59.02 (E(f12(f8(x6541),f8(x6542)),f12(f8(f1(x6541)),f8(f1(f1(f1(f1(x6542)))))))), % 58.95/59.02 inference(scs_inference,[],[651,2])). % 58.95/59.02 cnf(655,plain, % 58.95/59.02 (E(f3(f8(f1(f1(x6551))),f8(f1(f1(f1(x6552)))),f8(f1(x6553))),f3(f8(x6551),f8(x6552),f8(f1(x6553))))), % 58.95/59.02 inference(scs_inference,[],[651,593,288,2,3])). % 58.95/59.02 cnf(658,plain, % 58.95/59.02 (E(f3(f8(x6581),f8(x6582),f8(f1(x6583))),f3(f8(f1(f1(x6581))),f8(f1(f1(f1(x6582)))),f8(f1(x6583))))), % 58.95/59.02 inference(scs_inference,[],[655,2])). % 58.95/59.02 cnf(659,plain, % 58.95/59.02 (E(f12(f8(f1(f1(f1(f1(x6591))))),f8(x6592)),f12(f8(x6591),f8(f1(x6592))))), % 58.95/59.02 inference(scs_inference,[],[645,655,650,2,3])). % 58.95/59.02 cnf(663,plain, % 58.95/59.02 (E(f12(f8(x6631),f8(f1(x6632))),f12(f8(f1(f1(f1(f1(x6631))))),f8(x6632)))), % 58.95/59.02 inference(scs_inference,[],[659,2])). % 58.95/59.02 cnf(664,plain, % 58.95/59.02 (E(f3(f8(x6641),f8(x6642),f8(f1(x6643))),f3(f8(f1(x6641)),f8(f1(f1(f1(f1(x6642))))),f8(x6643)))), % 58.95/59.02 inference(scs_inference,[],[658,659,433,2,3])). % 58.95/59.02 cnf(667,plain, % 58.95/59.02 (E(f3(f8(f1(x6671)),f8(f1(f1(f1(f1(x6672))))),f8(x6673)),f3(f8(x6671),f8(x6672),f8(f1(x6673))))), % 58.95/59.02 inference(scs_inference,[],[664,2])). % 58.95/59.02 cnf(668,plain, % 58.95/59.02 (E(f3(f8(x6681),f8(x6682),f8(f1(f1(x6683)))),f3(f8(f1(f1(x6681))),f8(x6682),f8(f1(x6683))))), % 58.95/59.02 inference(scs_inference,[],[664,552,2,3])). % 58.95/59.02 cnf(673,plain, % 58.95/59.02 (E(f12(f8(x6731),f8(f1(f1(f1(x6732))))),f12(f8(f1(f1(x6731))),f8(f1(x6732))))), % 58.95/59.02 inference(scs_inference,[],[663,668,633,2,3])). % 58.95/59.02 cnf(678,plain, % 58.95/59.02 (E(f12(f8(x6781),f8(x6782)),f12(f8(f1(f1(f1(x6781)))),f8(f1(f1(x6782)))))), % 58.95/59.02 inference(scs_inference,[],[673,654,2,3])). % 58.95/59.02 cnf(681,plain, % 58.95/59.02 (E(f12(f8(f1(f1(f1(x6811)))),f8(f1(f1(x6812)))),f12(f8(x6811),f8(x6812)))), % 58.95/59.02 inference(scs_inference,[],[678,2])). % 58.95/59.02 cnf(682,plain, % 58.95/59.02 (E(f12(f8(x6821),f8(f1(f1(x6822)))),f12(f8(f1(f1(x6821))),f8(x6822)))), % 58.95/59.02 inference(scs_inference,[],[678,651,2,3])). % 58.95/59.02 cnf(686,plain, % 58.95/59.02 (E(f12(f8(f1(f1(x6861))),f8(x6862)),f12(f8(x6861),f8(f1(f1(x6862)))))), % 58.95/59.02 inference(scs_inference,[],[682,2])). % 58.95/59.02 cnf(687,plain, % 58.95/59.02 (E(f3(x6871,f3(x6872,x6873,f8(f1(x6874))),f8(f1(x6875))),f3(x6871,f3(x6872,x6873,f8(x6874)),f8(x6875)))), % 58.95/59.02 inference(scs_inference,[],[77,682,293,2,3])). % 58.95/59.02 cnf(691,plain, % 58.95/59.02 (E(f3(x6911,f3(x6912,x6913,f8(x6914)),f8(x6915)),f3(x6911,f3(x6912,x6913,f8(f1(x6914))),f8(f1(x6915))))), % 58.95/59.02 inference(scs_inference,[],[687,2])). % 58.95/59.02 cnf(692,plain, % 58.95/59.02 (E(f12(f8(f1(f1(f1(f1(f1(x6921)))))),f8(x6922)),f12(f8(x6921),f8(x6922)))), % 58.95/59.02 inference(scs_inference,[],[681,687,686,2,3])). % 58.95/59.02 cnf(696,plain, % 58.95/59.02 (E(f12(f8(x6961),f8(x6962)),f12(f8(f1(f1(f1(f1(f1(x6961)))))),f8(x6962)))), % 58.95/59.02 inference(scs_inference,[],[692,2])). % 58.95/59.02 cnf(697,plain, % 58.95/59.02 (E(f3(f8(x6971),f3(x6972,x6973,f8(f1(x6974))),x6975),f3(f8(f1(x6971)),f3(x6972,x6973,f8(x6974)),x6975))), % 58.95/59.02 inference(scs_inference,[],[76,692,519,2,3])). % 58.95/59.02 cnf(702,plain, % 58.95/59.02 (E(f3(x7021,f3(x7022,x7023,f8(f1(x7024))),f8(x7025)),f3(x7021,f3(x7022,x7023,f8(f1(x7024))),f8(f1(x7025))))), % 58.95/59.02 inference(scs_inference,[],[77,691,697,2,3])). % 58.95/59.02 cnf(705,plain, % 58.95/59.02 (E(f11(f8(x7051),x7052),f11(f8(f1(x7051)),x7052))), % 58.95/59.02 inference(scs_inference,[],[273,2])). % 58.95/59.02 cnf(706,plain, % 58.95/59.02 (E(f12(f8(x7061),f8(f1(f1(x7062)))),f12(f8(f1(f1(x7061))),f8(f1(x7062))))), % 58.95/59.02 inference(scs_inference,[],[696,645,273,2,3])). % 58.95/59.02 cnf(710,plain, % 58.95/59.02 (E(f12(f8(f1(f1(x7101))),f8(f1(x7102))),f12(f8(x7101),f8(f1(f1(x7102)))))), % 58.95/59.02 inference(scs_inference,[],[706,2])). % 58.95/59.02 cnf(711,plain, % 58.95/59.02 (E(f11(f8(x7111),f3(f8(f1(x7112)),x7113,x7114)),f11(f8(f1(x7111)),f3(f8(x7112),x7113,x7114)))), % 58.95/59.02 inference(scs_inference,[],[75,705,706,2,3])). % 58.95/59.02 cnf(717,plain, % 58.95/59.02 (E(f12(f8(x7171),f8(f1(f1(x7172)))),f12(f8(f1(f1(x7171))),f8(f1(f1(x7172)))))), % 58.95/59.02 inference(scs_inference,[],[711,710,663,2,3])). % 58.95/59.02 cnf(722,plain, % 58.95/59.02 (E(f12(f8(x7221),f8(f1(f1(x7222)))),f12(f8(f1(f1(f1(f1(x7221))))),f8(x7222)))), % 58.95/59.02 inference(scs_inference,[],[717,682,2,3])). % 58.95/59.02 cnf(727,plain, % 58.95/59.02 (E(f12(f8(x7271),f8(f1(f1(f1(f1(x7272)))))),f12(f8(f1(x7271)),f8(x7272)))), % 58.95/59.02 inference(scs_inference,[],[722,681,2,3])). % 58.95/59.02 cnf(732,plain, % 58.95/59.02 (E(f3(x7321,f3(x7322,x7323,f8(x7324)),f8(x7325)),f3(x7321,f3(x7322,x7323,f8(f1(f1(x7324)))),f8(f1(x7325))))), % 58.95/59.02 inference(scs_inference,[],[76,727,691,2,3])). % 58.95/59.02 cnf(736,plain, % 58.95/59.02 (E(f3(x7361,f3(x7362,x7363,f8(f1(f1(x7364)))),f8(f1(x7365))),f3(x7361,f3(x7362,x7363,f8(x7364)),f8(x7365)))), % 58.95/59.02 inference(scs_inference,[],[732,2])). % 58.95/59.02 cnf(737,plain, % 58.95/59.02 (E(f3(x7371,f3(x7372,x7373,f8(f1(f1(x7374)))),f8(x7375)),f3(x7371,f3(x7372,x7373,f8(f1(x7374))),f8(f1(x7375))))), % 58.95/59.02 inference(scs_inference,[],[77,702,732,2,3])). % 58.95/59.02 cnf(741,plain, % 58.95/59.02 (E(f3(x7411,f3(x7412,x7413,f8(f1(x7414))),f8(f1(x7415))),f3(x7411,f3(x7412,x7413,f8(f1(f1(x7414)))),f8(x7415)))), % 58.95/59.02 inference(scs_inference,[],[737,2])). % 58.95/59.02 cnf(746,plain, % 58.95/59.02 (E(f3(f8(x7461),x7462,x7463),f3(f8(f1(x7461)),x7462,x7463))), % 58.95/59.02 inference(scs_inference,[],[283,2])). % 58.95/59.02 cnf(747,plain, % 58.95/59.02 (E(f3(x7471,f3(x7472,x7473,f8(f1(f1(f1(x7474))))),f8(f1(x7475))),f3(x7471,f3(x7472,x7473,f8(x7474)),f8(x7475)))), % 58.95/59.02 inference(scs_inference,[],[77,736,283,2,3])). % 58.95/59.02 cnf(752,plain, % 58.95/59.02 (E(f3(x7521,f3(x7522,x7523,f8(x7524)),f8(f1(x7525))),f3(x7521,f3(x7522,x7523,f8(f1(f1(x7524)))),f8(x7525)))), % 58.95/59.02 inference(scs_inference,[],[76,741,747,2,3])). % 58.95/59.02 cnf(756,plain, % 58.95/59.02 (E(f3(x7561,f3(x7562,x7563,f8(f1(f1(x7564)))),f8(x7565)),f3(x7561,f3(x7562,x7563,f8(x7564)),f8(f1(x7565))))), % 58.95/59.02 inference(scs_inference,[],[752,2])). % 58.95/59.02 cnf(757,plain, % 58.95/59.02 (E(f3(f8(x7571),f8(f1(f1(f1(f1(x7572))))),f8(x7573)),f3(f8(x7571),f8(x7572),f8(f1(x7573))))), % 58.95/59.02 inference(scs_inference,[],[752,667,746,2,3])). % 58.95/59.02 cnf(761,plain, % 58.95/59.02 (E(f3(f8(x7611),f8(x7612),f8(f1(x7613))),f3(f8(x7611),f8(f1(f1(f1(f1(x7612))))),f8(x7613)))), % 58.95/59.02 inference(scs_inference,[],[757,2])). % 58.95/59.02 cnf(762,plain, % 58.95/59.02 (E(f3(x7621,f3(x7622,x7623,f8(f1(f1(f1(x7624))))),f8(x7625)),f3(x7621,f3(x7622,x7623,f8(x7624)),f8(f1(x7625))))), % 58.95/59.02 inference(scs_inference,[],[77,756,757,2,3])). % 58.95/59.02 cnf(766,plain, % 58.95/59.02 (E(f3(f8(f1(x7661)),f8(x7662),f8(f1(x7663))),f3(f8(x7661),f8(f1(f1(x7662))),f8(f1(x7663))))), % 58.95/59.02 inference(scs_inference,[],[761,762,589,2,3])). % 58.95/59.02 cnf(769,plain, % 58.95/59.02 (E(f1(f1(f8(x7691))),f1(f1(f8(f1(x7691)))))), % 58.95/59.02 inference(scs_inference,[],[40,2,4])). % 58.95/59.02 cnf(771,plain, % 58.95/59.02 (E(f3(f8(x7711),f8(f1(x7712)),f8(f1(x7713))),f3(f8(x7711),f8(f1(f1(f1(x7712)))),f8(f1(f1(x7713)))))), % 58.95/59.02 inference(scs_inference,[],[766,594,2,3])). % 58.95/59.02 cnf(773,plain, % 58.95/59.02 (E(f6(f1(f8(x7731)),x7732),f6(f1(f8(f1(x7731))),x7732))), % 58.95/59.02 inference(scs_inference,[],[40,2,6])). % 58.95/59.02 cnf(775,plain, % 58.95/59.02 (E(f6(f1(f8(x7751)),f8(x7752)),f6(f1(f8(f1(x7751))),f8(f1(x7752))))), % 58.95/59.02 inference(scs_inference,[],[769,773,236,2,3])). % 58.95/59.02 cnf(779,plain, % 58.95/59.02 (E(f6(f1(f8(f1(x7791))),f8(f1(x7792))),f6(f1(f8(x7791)),f8(x7792)))), % 58.95/59.02 inference(scs_inference,[],[775,2])). % 58.95/59.02 cnf(789,plain, % 58.95/59.02 (E(f3(f8(x7891),f8(f1(f1(f1(x7892)))),f8(f1(f1(x7893)))),f3(f8(x7891),f8(f1(x7892)),f8(f1(x7893))))), % 58.95/59.02 inference(scs_inference,[],[771,2])). % 58.95/59.02 cnf(807,plain, % 58.95/59.02 (E(f4(f1(f8(x8071)),x8072),f4(f1(f8(f1(x8071))),x8072))), % 58.95/59.02 inference(scs_inference,[],[40,2,13])). % 58.95/59.02 cnf(812,plain, % 58.95/59.02 (E(f4(x8121,f1(f8(x8122))),f4(x8121,f1(f8(f1(x8122)))))), % 58.95/59.02 inference(scs_inference,[],[40,2,14])). % 58.95/59.02 cnf(817,plain, % 58.95/59.02 (E(f11(f1(f8(x8171)),x8172),f11(f1(f8(f1(x8171))),x8172))), % 58.95/59.02 inference(scs_inference,[],[40,2,15])). % 58.95/59.02 cnf(818,plain, % 58.95/59.02 (E(f4(f1(f8(f1(x8181))),x8182),f4(f1(f8(x8181)),x8182))), % 58.95/59.02 inference(scs_inference,[],[807,2])). % 58.95/59.02 cnf(819,plain, % 58.95/59.02 (E(f4(f1(f8(x8191)),f11(f8(f1(x8192)),x8193)),f4(f1(f8(f1(x8191))),f11(f8(x8192),x8193)))), % 58.95/59.02 inference(scs_inference,[],[64,807,2,3])). % 58.95/59.02 cnf(822,plain, % 58.95/59.02 (E(f11(x8221,f1(f8(x8222))),f11(x8221,f1(f8(f1(x8222)))))), % 58.95/59.02 inference(scs_inference,[],[40,2,16])). % 58.95/59.02 cnf(824,plain, % 58.95/59.02 (E(f4(f1(f8(f1(x8241))),f1(f8(x8242))),f4(f1(f8(x8241)),f1(f8(f1(x8242)))))), % 58.95/59.02 inference(scs_inference,[],[818,819,812,2,3])). % 58.95/59.02 cnf(827,plain, % 58.95/59.02 (E(f3(f1(f8(x8271)),x8272,x8273),f3(f1(f8(f1(x8271))),x8272,x8273))), % 58.95/59.02 inference(scs_inference,[],[40,2,17])). % 58.95/59.02 cnf(828,plain, % 58.95/59.02 (E(f11(f1(f8(f1(x8281))),x8282),f11(f1(f8(x8281)),x8282))), % 58.95/59.02 inference(scs_inference,[],[817,2])). % 58.95/59.02 cnf(832,plain, % 58.95/59.02 (E(f3(x8321,f1(f8(x8322)),x8323),f3(x8321,f1(f8(f1(x8322))),x8323))), % 58.95/59.02 inference(scs_inference,[],[40,2,18])). % 58.95/59.02 cnf(833,plain, % 58.95/59.02 (E(f11(x8331,f1(f8(f1(x8332)))),f11(x8331,f1(f8(x8332))))), % 58.95/59.02 inference(scs_inference,[],[822,2])). % 58.95/59.02 cnf(837,plain, % 58.95/59.02 (E(f3(x8371,x8372,f1(f8(x8373))),f3(x8371,x8372,f1(f8(f1(x8373)))))), % 58.95/59.02 inference(scs_inference,[],[40,2,19])). % 58.95/59.02 cnf(838,plain, % 58.95/59.02 (E(f4(f1(f8(x8381)),f1(f8(f1(x8382)))),f4(f1(f8(f1(x8381))),f1(f8(x8382))))), % 58.95/59.02 inference(scs_inference,[],[824,2])). % 58.95/59.02 cnf(839,plain, % 58.95/59.02 (E(f11(f8(x8391),f1(f8(f1(x8392)))),f11(f8(f1(x8391)),f1(f8(x8392))))), % 58.95/59.02 inference(scs_inference,[],[833,824,705,2,3])). % 58.95/59.02 cnf(842,plain, % 58.95/59.02 (E(f5(f1(f8(x8421))),f5(f1(f8(f1(x8421)))))), % 58.95/59.02 inference(scs_inference,[],[40,2,20])). % 58.95/59.02 cnf(844,plain, % 58.95/59.02 (E(f4(f1(f8(f1(x8441))),f1(f8(f1(x8442)))),f4(f1(f8(f1(x8441))),f1(f8(x8442))))), % 58.95/59.02 inference(scs_inference,[],[838,839,818,2,3])). % 58.95/59.02 cnf(848,plain, % 58.95/59.02 (E(f3(f1(f8(f1(x8481))),x8482,x8483),f3(f1(f8(x8481)),x8482,x8483))), % 58.95/59.02 inference(scs_inference,[],[827,2])). % 58.95/59.02 cnf(849,plain, % 58.95/59.02 (E(f4(f1(f8(x8491)),f1(f8(f1(f1(x8492))))),f4(f1(f8(f1(x8491))),f1(f8(x8492))))), % 58.95/59.02 inference(scs_inference,[],[844,827,838,2,3])). % 58.95/59.02 cnf(854,plain, % 58.95/59.02 (E(f3(f1(f8(f1(x8541))),f3(x8542,x8543,f8(x8544)),x8545),f3(f1(f8(x8541)),f3(x8542,x8543,f8(f1(x8544))),x8545))), % 58.95/59.02 inference(scs_inference,[],[76,848,849,2,3])). % 58.95/59.02 cnf(858,plain, % 58.95/59.02 (E(f3(x8581,f1(f8(f1(x8582))),x8583),f3(x8581,f1(f8(x8582)),x8583))), % 58.95/59.02 inference(scs_inference,[],[832,2])). % 58.95/59.02 cnf(863,plain, % 58.95/59.02 (E(f3(x8631,x8632,f1(f8(f1(x8633)))),f3(x8631,x8632,f1(f8(x8633))))), % 58.95/59.02 inference(scs_inference,[],[837,2])). % 58.95/59.02 cnf(864,plain, % 58.95/59.02 (E(f3(x8641,f1(f8(f1(x8642))),f1(f8(x8643))),f3(x8641,f1(f8(x8642)),f1(f8(f1(x8643)))))), % 58.95/59.02 inference(scs_inference,[],[858,837,2,3])). % 58.95/59.02 cnf(869,plain, % 58.95/59.02 (E(f3(x8691,f3(x8692,x8693,f8(f1(x8694))),f1(f8(f1(x8695)))),f3(x8691,f3(x8692,x8693,f8(x8694)),f1(f8(x8695))))), % 58.95/59.02 inference(scs_inference,[],[77,863,842,2,3])). % 58.95/59.02 cnf(873,plain, % 58.95/59.02 (E(f3(x8731,f3(x8732,x8733,f8(x8734)),f1(f8(x8735))),f3(x8731,f3(x8732,x8733,f8(f1(x8734))),f1(f8(f1(x8735)))))), % 58.95/59.02 inference(scs_inference,[],[869,2])). % 58.95/59.02 cnf(878,plain, % 58.95/59.02 (E(f3(f1(f8(x8781)),f3(x8782,x8783,f8(f1(x8784))),x8785),f3(f1(f8(f1(x8781))),f3(x8782,x8783,f8(x8784)),x8785))), % 58.95/59.02 inference(scs_inference,[],[854,2])). % 58.95/59.02 cnf(884,plain, % 58.95/59.02 (E(f3(f8(x8841),f1(f8(f1(x8842))),f1(f8(x8843))),f3(f8(f1(x8841)),f1(f8(x8842)),f1(f8(f1(x8843)))))), % 58.95/59.02 inference(scs_inference,[],[864,746,2,3])). % 58.95/59.02 cnf(888,plain, % 58.95/59.02 (E(f3(x8881,f3(x8882,x8883,f8(x8884)),f1(f8(x8885))),f3(x8881,f3(x8882,x8883,f8(f1(f1(x8884)))),f1(f8(f1(x8885)))))), % 58.95/59.02 inference(scs_inference,[],[76,873,884,2,3])). % 58.95/59.02 cnf(894,plain, % 58.95/59.02 (E(f3(f1(f8(x8941)),f3(x8942,x8943,f8(f1(f1(x8944)))),x8945),f3(f1(f8(f1(x8941))),f3(x8942,x8943,f8(x8944)),x8945))), % 58.95/59.02 inference(scs_inference,[],[77,878,888,2,3])). % 58.95/59.02 cnf(900,plain, % 58.95/59.02 (E(f3(f8(x9001),f8(f1(f1(f1(x9002)))),f8(f1(f1(x9003)))),f3(f8(f1(x9001)),f8(x9002),f8(f1(x9003))))), % 58.95/59.02 inference(scs_inference,[],[789,894,580,2,3])). % 58.95/59.02 cnf(905,plain, % 58.95/59.02 (E(f3(x9051,f3(x9052,x9053,f8(f1(x9054))),f8(x9055)),f3(x9051,f3(x9052,x9053,f8(x9054)),f8(f1(x9055))))), % 58.95/59.02 inference(scs_inference,[],[76,900,756,2,3])). % 58.95/59.02 cnf(956,plain, % 58.95/59.02 (E(f4(f8(x9561),f11(f8(x9562),x9563)),f4(f8(f1(x9561)),f11(f8(f1(x9562)),x9563)))), % 58.95/59.02 inference(scs_inference,[],[65,632,812,2,3])). % 58.95/59.02 cnf(961,plain, % 58.95/59.02 (E(f4(f8(f1(x9611)),f11(f8(f1(x9612)),x9613)),f4(f8(x9611),f11(f8(x9612),x9613)))), % 58.95/59.02 inference(scs_inference,[],[956,2])). % 58.95/59.02 cnf(962,plain, % 58.95/59.02 (E(f11(f1(f8(f1(x9621))),f3(f8(x9622),x9623,x9624)),f11(f1(f8(x9621)),f3(f8(f1(x9622)),x9623,x9624)))), % 58.95/59.02 inference(scs_inference,[],[74,956,828,2,3])). % 58.95/59.02 cnf(967,plain, % 58.95/59.02 (E(f11(f1(f8(x9671)),f3(f8(f1(x9672)),x9673,x9674)),f11(f1(f8(f1(x9671))),f3(f8(x9672),x9673,x9674)))), % 58.95/59.02 inference(scs_inference,[],[962,2])). % 58.95/59.02 cnf(968,plain, % 58.95/59.02 (E(f4(f8(f1(x9681)),f11(f8(f1(f1(x9682))),x9683)),f4(f8(x9681),f11(f8(x9682),x9683)))), % 58.95/59.02 inference(scs_inference,[],[64,961,962,2,3])). % 58.95/59.02 cnf(974,plain, % 58.95/59.02 (E(f11(f1(f8(x9741)),f3(f8(f1(f1(x9742))),x9743,x9744)),f11(f1(f8(f1(x9741))),f3(f8(x9742),x9743,x9744)))), % 58.95/59.02 inference(scs_inference,[],[75,967,968,2,3])). % 58.95/59.02 cnf(980,plain, % 58.95/59.02 (E(f3(f1(f8(f1(x9801))),f3(x9802,x9803,f8(f1(x9804))),x9805),f3(f1(f8(x9801)),f3(x9802,x9803,f8(x9804)),x9805))), % 58.95/59.02 inference(scs_inference,[],[77,974,848,2,3])). % 58.95/59.02 cnf(986,plain, % 58.95/59.02 (E(f3(x9861,f3(x9862,x9863,f8(x9864)),f1(f8(f1(x9865)))),f3(x9861,f3(x9862,x9863,f8(f1(x9864))),f1(f8(x9865))))), % 58.95/59.02 inference(scs_inference,[],[76,980,863,2,3])). % 58.95/59.02 cnf(992,plain, % 58.95/59.02 (E(f3(f1(f8(f1(x9921))),f3(x9922,x9923,f8(f1(f1(x9924)))),x9925),f3(f1(f8(x9921)),f3(x9922,x9923,f8(x9924)),x9925))), % 58.95/59.02 inference(scs_inference,[],[77,986,980,2,3])). % 58.95/59.02 cnf(998,plain, % 58.95/59.02 (E(f3(x9981,f3(x9982,x9983,f8(x9984)),f8(x9985)),f3(x9981,f3(x9982,x9983,f8(x9984)),f8(f1(x9985))))), % 58.95/59.02 inference(scs_inference,[],[76,992,905,2,3])). % 58.95/59.02 cnf(1297,plain, % 58.95/59.02 (E(f12(x12971,f1(f8(f1(x12972)))),f12(x12971,f1(f8(x12972))))), % 58.95/59.02 inference(scs_inference,[],[41,2,12])). % 58.95/59.02 cnf(1551,plain, % 58.95/59.02 (E(f12(f8(x15511),x15512),f12(f8(f1(x15511)),x15512))), % 58.95/59.02 inference(scs_inference,[],[253,2])). % 58.95/59.02 cnf(1673,plain, % 58.95/59.02 (P1(f12(f9(a13),f10(a18)),f8(f8(f1(f1(f1(f6(a7,a20)))))),a16)), % 58.95/59.02 inference(scs_inference,[],[250,138,4,5,8,9,10,20,27])). % 58.95/59.02 cnf(1693,plain, % 58.95/59.02 (~P1(f10(a18),f8(f1(f6(a7,a20))),a16)), % 58.95/59.02 inference(scs_inference,[],[25,250,562,145,138,26,24,4,5,8,9,10,20,27,6,7,11,12,13,14,15,16,17,18,19,29,32,31,2,22])). % 58.95/59.02 cnf(1700,plain, % 58.95/59.02 (P1(f11(f14(a17),f12(f9(a13),f10(a18))),f8(f1(f6(a7,a20))),a16)), % 58.95/59.02 inference(scs_inference,[],[25,250,1551,562,1297,145,138,26,24,4,5,8,9,10,20,27,6,7,11,12,13,14,15,16,17,18,19,29,32,31,2,22,3,28,78])). % 58.95/59.02 cnf(1733,plain, % 58.95/59.02 (~E(f11(f14(a17),f12(f9(a13),f10(a18))),f10(a18))), % 58.95/59.02 inference(scs_inference,[],[1693,254,304,1700,200,1673,29,8,20,18,11,6,27,12,10,19,5,13,17,14,4,9,7,15,16,2,21])). % 58.95/59.02 cnf(1738,plain, % 58.95/59.02 (P1(f12(f9(a13),f10(a18)),f8(f8(f1(f6(a7,a20)))),a16)), % 58.95/59.02 inference(scs_inference,[],[1693,254,304,1700,205,217,200,1673,220,182,29,8,20,18,11,6,27,12,10,19,5,13,17,14,4,9,7,15,16,2,21,22,3,30])). % 58.95/59.02 cnf(1768,plain, % 58.95/59.02 ($false), % 58.95/59.02 inference(scs_inference,[],[1733,998,1738,779,1693,560,24,20,6,29,11,12,27,19,8,5,18,7,13,10,16,17,15,9,14,4,2,22]), % 58.95/59.02 ['proof']). % 58.95/59.02 % SZS output end Proof % 58.95/59.02 % Total time :58.440000s %------------------------------------------------------------------------------