%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SWV343-2 : TPTP v8.2.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n001.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:51 EDT 2024 % Result : Unsatisfiable 63.11s 63.16s % Output : CNFRefutation 63.11s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWV343-2 : TPTP v8.2.0. Released v3.2.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n001.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Thu Jun 20 17:52:09 EDT 2024 % 0.12/0.33 % CPUTime : % 0.51/0.56 start to proof:theBenchmark % 63.11/63.15 %------------------------------------------- % 63.11/63.15 % File :CSE---1.7 % 63.11/63.15 % Problem :theBenchmark % 63.11/63.15 % Transform :cnf % 63.11/63.15 % Format :tptp:raw % 63.11/63.15 % Command :java -jar mcs_scs.jar %d %s % 63.11/63.15 % 63.11/63.15 % Result :Theorem 62.560000s % 63.11/63.15 % Output :CNFRefutation 62.560000s % 63.11/63.15 %------------------------------------------- % 63.11/63.16 %------------------------------------------------------------------------------ % 63.11/63.16 % File : SWV343-2 : TPTP v8.2.0. Released v3.2.0. % 63.11/63.16 % Domain : Software Verification (Security) % 63.11/63.16 % Problem : Cryptographic protocol problem for Yahalom % 63.11/63.16 % Version : [Pau06] axioms : Reduced > Especial. % 63.11/63.16 % English : % 63.11/63.16 % 63.11/63.16 % Refs : [Pau06] Paulson (2006), Email to G. Sutcliffe % 63.11/63.16 % Source : [Pau06] % 63.11/63.16 % Names : % 63.11/63.16 % 63.11/63.16 % Status : Unsatisfiable % 63.11/63.16 % Rating : 0.00 v5.5.0, 0.12 v5.4.0, 0.13 v5.3.0, 0.17 v5.2.0, 0.00 v4.1.0, 0.11 v4.0.1, 0.17 v3.3.0, 0.14 v3.2.0 % 63.11/63.16 % Syntax : Number of clauses : 9 ( 3 unt; 0 nHn; 8 RR) % 63.11/63.16 % Number of literals : 15 ( 1 equ; 7 neg) % 63.11/63.16 % Maximal clause size : 2 ( 1 avg) % 63.11/63.16 % Maximal term depth : 7 ( 2 avg) % 63.11/63.16 % Number of predicates : 2 ( 1 usr; 0 prp; 2-3 aty) % 63.11/63.16 % Number of functors : 21 ( 21 usr; 10 con; 0-3 aty) % 63.11/63.16 % Number of variables : 18 ( 5 sgn) % 63.11/63.16 % SPC : CNF_UNS_RFO_SEQ_HRN % 63.11/63.16 % 63.11/63.16 % Comments : The problems in the [Pau06] collection each have very many axioms, % 63.11/63.16 % of which only a small selection are required for the refutation. % 63.11/63.16 % The mission is to find those few axioms, after which a refutation % 63.11/63.16 % can be quite easily found. This version has only the necessary % 63.11/63.16 % axioms. % 63.11/63.16 %------------------------------------------------------------------------------ % 63.11/63.16 cnf(cls_conjecture_10,negated_conjecture, % 63.11/63.16 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) ). % 63.11/63.16 % 63.11/63.16 cnf(cls_conjecture_3,negated_conjecture, % 63.11/63.16 ~ c_in(c_Message_Omsg_OKey(v_K),c_Event_Oused(v_evs3),tc_Message_Omsg) ). % 63.11/63.16 % 63.11/63.16 cnf(cls_Event_OSays__imp__analz__Spy__dest_0,axiom, % 63.11/63.16 ( ~ c_in(c_Event_Oevent_OSays(V_A,V_B,V_X),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent) % 63.11/63.16 | c_in(V_X,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg) ) ). % 63.11/63.16 % 63.11/63.16 cnf(cls_Event_Oc_A_58_Aparts_A_Iknows_ASpy_Aevs1_J_A_61_61_62_Ac_A_58_Aused_Aevs1_0,axiom, % 63.11/63.16 ( ~ c_in(V_c,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg) % 63.11/63.16 | c_in(V_c,c_Event_Oused(V_evs),tc_Message_Omsg) ) ). % 63.11/63.16 % 63.11/63.16 cnf(cls_Message_OMPair__analz_0,axiom, % 63.11/63.16 ( ~ c_in(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Oanalz(V_H),tc_Message_Omsg) % 63.11/63.16 | c_in(V_Y,c_Message_Oanalz(V_H),tc_Message_Omsg) ) ). % 63.11/63.16 % 63.11/63.16 cnf(cls_Message_OMPair__parts_0,axiom, % 63.11/63.16 ( ~ c_in(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Oparts(V_H),tc_Message_Omsg) % 63.11/63.16 | c_in(V_Y,c_Message_Oparts(V_H),tc_Message_Omsg) ) ). % 63.11/63.16 % 63.11/63.16 cnf(cls_Message_Oparts_OBody__dest_0,axiom, % 63.11/63.16 ( ~ c_in(c_Message_Omsg_OCrypt(V_K,V_X),c_Message_Oparts(V_H),tc_Message_Omsg) % 63.11/63.16 | c_in(V_X,c_Message_Oparts(V_H),tc_Message_Omsg) ) ). % 63.11/63.16 % 63.11/63.16 cnf(cls_Message_Oparts_OInj_0,axiom, % 63.11/63.16 ( ~ c_in(V_X,V_H,tc_Message_Omsg) % 63.11/63.16 | c_in(V_X,c_Message_Oparts(V_H),tc_Message_Omsg) ) ). % 63.11/63.16 % 63.11/63.16 cnf(cls_Message_Oparts__analz_0,axiom, % 63.11/63.16 c_Message_Oparts(c_Message_Oanalz(V_H)) = c_Message_Oparts(V_H) ). % 63.11/63.16 % 63.11/63.16 %------------------------------------------------------------------------------ % 63.11/63.16 %------------------------------------------- % 63.11/63.16 % Proof found % 63.11/63.16 % SZS status Theorem for theBenchmark % 63.11/63.16 % SZS output start Proof % 63.11/63.17 %ClaNum:32(EqnAxiom:23) % 63.11/63.17 %VarNum:31(SingletonVarNum:18) % 63.11/63.17 %MaxLitNum:2 % 63.11/63.17 %MaxfuncDepth:5 % 63.11/63.17 %SharedTerms:27 % 63.11/63.17 %goalClause: 25 26 % 63.11/63.17 %singleGoalClaCount:2 % 63.11/63.17 [26]~P1(f10(a18),f5(a20),a16) % 63.11/63.17 [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) % 63.11/63.17 [24]E(f8(f1(x241)),f8(x241)) % 63.11/63.17 [27]~P1(x271,x272,a16)+P1(x271,f8(x272),a16) % 63.11/63.17 [31]P1(x311,f5(x312),a16)+~P1(x311,f8(f6(a7,x312)),a16) % 63.11/63.17 [28]P1(x281,f1(x282),a16)+~P1(f12(x283,x281),f1(x282),a16) % 63.11/63.17 [29]P1(x291,f8(x292),a16)+~P1(f12(x293,x291),f8(x292),a16) % 63.11/63.17 [30]P1(x301,f8(x302),a16)+~P1(f11(x303,x301),f8(x302),a16) % 63.11/63.17 [32]~P1(f3(x323,x324,x321),f4(x322,a15),a15)+P1(x321,f1(f6(a7,x322)),a16) % 63.11/63.17 %EqnAxiom % 63.11/63.17 [1]E(x11,x11) % 63.11/63.17 [2]E(x22,x21)+~E(x21,x22) % 63.11/63.17 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 63.11/63.17 [4]~E(x41,x42)+E(f1(x41),f1(x42)) % 63.11/63.17 [5]~E(x51,x52)+E(f8(x51),f8(x52)) % 63.11/63.17 [6]~E(x61,x62)+E(f6(x61,x63),f6(x62,x63)) % 63.11/63.17 [7]~E(x71,x72)+E(f6(x73,x71),f6(x73,x72)) % 63.11/63.17 [8]~E(x81,x82)+E(f14(x81),f14(x82)) % 63.11/63.17 [9]~E(x91,x92)+E(f9(x91),f9(x92)) % 63.11/63.17 [10]~E(x101,x102)+E(f10(x101),f10(x102)) % 63.11/63.17 [11]~E(x111,x112)+E(f12(x111,x113),f12(x112,x113)) % 63.11/63.17 [12]~E(x121,x122)+E(f12(x123,x121),f12(x123,x122)) % 63.11/63.17 [13]~E(x131,x132)+E(f4(x131,x133),f4(x132,x133)) % 63.11/63.17 [14]~E(x141,x142)+E(f4(x143,x141),f4(x143,x142)) % 63.11/63.17 [15]~E(x151,x152)+E(f11(x151,x153),f11(x152,x153)) % 63.11/63.17 [16]~E(x161,x162)+E(f11(x163,x161),f11(x163,x162)) % 63.11/63.17 [17]~E(x171,x172)+E(f3(x171,x173,x174),f3(x172,x173,x174)) % 63.11/63.17 [18]~E(x181,x182)+E(f3(x183,x181,x184),f3(x183,x182,x184)) % 63.11/63.17 [19]~E(x191,x192)+E(f3(x193,x194,x191),f3(x193,x194,x192)) % 63.11/63.17 [20]~E(x201,x202)+E(f5(x201),f5(x202)) % 63.11/63.17 [21]P1(x212,x213,x214)+~E(x211,x212)+~P1(x211,x213,x214) % 63.11/63.17 [22]P1(x223,x222,x224)+~E(x221,x222)+~P1(x223,x221,x224) % 63.11/63.17 [23]P1(x233,x234,x232)+~E(x231,x232)+~P1(x233,x234,x231) % 63.11/63.17 % 63.11/63.17 %------------------------------------------- % 63.11/63.18 cnf(33,plain, % 63.11/63.18 (E(f8(x331),f8(f1(x331)))), % 63.11/63.18 inference(scs_inference,[],[24,2])). % 63.11/63.18 cnf(40,plain, % 63.11/63.18 (E(f1(f8(f1(x401))),f1(f8(x401)))), % 63.11/63.18 inference(scs_inference,[],[33,4,2])). % 63.11/63.18 cnf(41,plain, % 63.11/63.18 (E(f1(f8(x411)),f1(f8(f1(x411))))), % 63.11/63.18 inference(scs_inference,[],[40,2])). % 63.11/63.18 cnf(42,plain, % 63.11/63.18 (E(f8(f6(f1(f8(x421)),x422)),f8(f6(f1(f8(f1(x421))),x422)))), % 63.11/63.18 inference(scs_inference,[],[41,5,6])). % 63.11/63.18 cnf(43,plain, % 63.11/63.18 (E(f8(f6(f1(f8(f1(x431))),x432)),f8(f6(f1(f8(x431)),x432)))), % 63.11/63.18 inference(scs_inference,[],[42,2])). % 63.11/63.18 cnf(45,plain, % 63.11/63.18 (E(f9(f10(f8(f1(x451)))),f9(f10(f8(x451))))), % 63.11/63.18 inference(scs_inference,[],[24,9,10])). % 63.11/63.18 cnf(46,plain, % 63.11/63.18 (E(f9(f10(f8(x461))),f9(f10(f8(f1(x461)))))), % 63.11/63.18 inference(scs_inference,[],[45,2])). % 63.11/63.18 cnf(47,plain, % 63.11/63.18 (E(f5(f12(f8(f1(x471)),x472)),f5(f12(f8(x471),x472)))), % 63.11/63.18 inference(scs_inference,[],[24,20,11])). % 63.11/63.18 cnf(49,plain, % 63.11/63.18 (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)), % 63.11/63.18 inference(scs_inference,[],[25,27,32])). % 63.11/63.18 cnf(50,plain, % 63.11/63.18 (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)), % 63.11/63.18 inference(scs_inference,[],[24,49,22])). % 63.11/63.18 cnf(55,plain, % 63.11/63.18 (~E(f12(f11(f14(a13),f12(f9(a17),f12(f10(a18),f12(a19,a21)))),f11(f14(a17),f12(f9(a13),f10(a18)))),f10(a18))), % 63.11/63.18 inference(scs_inference,[],[24,26,49,22,31,23,21])). % 63.11/63.18 cnf(57,plain, % 63.11/63.18 (E(f12(x571,f4(f8(f1(x572)),x573)),f12(x571,f4(f8(x572),x573)))), % 63.11/63.18 inference(scs_inference,[],[24,12,13])). % 63.11/63.18 cnf(58,plain, % 63.11/63.18 (E(f12(x581,f4(f8(x582),x583)),f12(x581,f4(f8(f1(x582)),x583)))), % 63.11/63.18 inference(scs_inference,[],[57,2])). % 63.11/63.18 cnf(65,plain, % 63.11/63.18 (E(f4(x651,f11(f8(f1(x652)),x653)),f4(x651,f11(f8(x652),x653)))), % 63.11/63.18 inference(scs_inference,[],[24,14,15])). % 63.11/63.18 cnf(73,plain, % 63.11/63.18 (E(f3(x731,f3(x732,x733,f8(f1(x734))),x735),f3(x731,f3(x732,x733,f8(x734)),x735))), % 63.11/63.18 inference(scs_inference,[],[24,18,19])). % 63.11/63.18 cnf(74,plain, % 63.11/63.18 (E(f3(x741,f3(x742,x743,f8(x744)),x745),f3(x741,f3(x742,x743,f8(f1(x744))),x745))), % 63.11/63.18 inference(scs_inference,[],[73,2])). % 63.11/63.18 cnf(76,plain, % 63.11/63.18 (P1(f12(f9(a13),f10(a18)),f8(f6(a7,a20)),a16)), % 63.11/63.18 inference(scs_inference,[],[50,29,30])). % 63.11/63.18 cnf(77,plain, % 63.11/63.18 (P1(f12(f9(a13),f10(a18)),f5(a20),a16)), % 63.11/63.18 inference(scs_inference,[],[76,31])). % 63.11/63.18 cnf(79,plain, % 63.11/63.18 (P1(f12(f9(a13),f10(a18)),f8(f1(f6(a7,a20))),a16)), % 63.11/63.18 inference(scs_inference,[],[33,76,31,22])). % 63.11/63.18 cnf(81,plain, % 63.11/63.18 (~E(f12(f9(a13),f10(a18)),f10(a18))), % 63.11/63.18 inference(scs_inference,[],[33,26,76,31,22,21])). % 63.11/63.18 cnf(85,plain, % 63.11/63.18 (P1(f12(f9(a13),f10(a18)),f8(f1(f1(f6(a7,a20)))),a16)), % 63.11/63.18 inference(scs_inference,[],[33,79,22])). % 63.11/63.18 cnf(92,plain, % 63.11/63.18 (P1(f12(f9(a13),f10(a18)),f8(f1(f1(f1(f6(a7,a20))))),a16)), % 63.11/63.18 inference(scs_inference,[],[33,85,22])). % 63.11/63.18 cnf(99,plain, % 63.11/63.18 (P1(f12(f9(a13),f10(a18)),f8(f1(f1(f1(f1(f6(a7,a20)))))),a16)), % 63.11/63.18 inference(scs_inference,[],[33,92,22])). % 63.11/63.18 cnf(164,plain, % 63.11/63.18 (E(f12(f9(f10(f8(f1(x1641)))),x1642),f12(f9(f10(f8(x1641))),x1642))), % 63.11/63.18 inference(scs_inference,[],[46,2,11])). % 63.11/63.18 cnf(253,plain, % 63.11/63.18 (E(f3(f9(f10(f8(x2531))),x2532,x2533),f3(f9(f10(f8(f1(x2531)))),x2532,x2533))), % 63.11/63.18 inference(scs_inference,[],[45,2,17])). % 63.11/63.18 cnf(254,plain, % 63.11/63.18 (E(f3(f9(f10(f8(f1(x2541)))),x2542,x2543),f3(f9(f10(f8(x2541))),x2542,x2543))), % 63.11/63.18 inference(scs_inference,[],[253,2])). % 63.11/63.18 cnf(258,plain, % 63.11/63.18 (E(f3(x2581,f5(f12(f8(x2582),x2583)),x2584),f3(x2581,f5(f12(f8(f1(x2582)),x2583)),x2584))), % 63.11/63.18 inference(scs_inference,[],[47,2,18])). % 63.11/63.18 cnf(282,plain, % 63.11/63.18 (E(f3(x2821,f5(f12(f8(f1(x2822)),x2823)),x2824),f3(x2821,f5(f12(f8(x2822),x2823)),x2824))), % 63.11/63.18 inference(scs_inference,[],[258,2])). % 63.11/63.18 cnf(296,plain, % 63.11/63.18 (E(f10(f8(x2961)),f10(f8(f1(x2961))))), % 63.11/63.18 inference(scs_inference,[],[24,2,10])). % 63.11/63.18 cnf(297,plain, % 63.11/63.18 (E(f10(f8(f1(x2971))),f10(f8(x2971)))), % 63.11/63.18 inference(scs_inference,[],[296,2])). % 63.11/63.18 cnf(298,plain, % 63.11/63.18 (E(f12(x2981,f8(x2982)),f12(x2981,f8(f1(x2982))))), % 63.11/63.18 inference(scs_inference,[],[24,2,12])). % 63.11/63.18 cnf(299,plain, % 63.11/63.18 (E(f12(x2991,f8(f1(x2992))),f12(x2991,f8(x2992)))), % 63.11/63.18 inference(scs_inference,[],[298,2])). % 63.11/63.18 cnf(300,plain, % 63.11/63.18 (E(f12(f9(f10(f8(f1(x3001)))),f8(x3002)),f12(f9(f10(f8(x3001))),f8(f1(x3002))))), % 63.11/63.18 inference(scs_inference,[],[298,164,2,3])). % 63.11/63.18 cnf(303,plain, % 63.11/63.18 (E(f4(f8(x3031),x3032),f4(f8(f1(x3031)),x3032))), % 63.11/63.18 inference(scs_inference,[],[24,2,13])). % 63.11/63.18 cnf(304,plain, % 63.11/63.18 (E(f12(f9(f10(f8(x3041))),f8(f1(x3042))),f12(f9(f10(f8(f1(x3041)))),f8(x3042)))), % 63.11/63.18 inference(scs_inference,[],[300,2])). % 63.11/63.18 cnf(308,plain, % 63.11/63.18 (E(f4(x3081,f8(x3082)),f4(x3081,f8(f1(x3082))))), % 63.11/63.18 inference(scs_inference,[],[24,2,14])). % 63.11/63.18 cnf(309,plain, % 63.11/63.18 (E(f4(x3091,f8(f1(x3092))),f4(x3091,f8(x3092)))), % 63.11/63.18 inference(scs_inference,[],[308,2])). % 63.11/63.18 cnf(310,plain, % 63.11/63.18 (E(f12(f9(f10(f8(x3101))),f8(f1(f1(x3102)))),f12(f9(f10(f8(f1(x3101)))),f8(x3102)))), % 63.11/63.18 inference(scs_inference,[],[299,304,308,2,3])). % 63.11/63.18 cnf(313,plain, % 63.11/63.18 (E(f11(f8(x3131),x3132),f11(f8(f1(x3131)),x3132))), % 63.11/63.18 inference(scs_inference,[],[24,2,15])). % 63.11/63.18 cnf(315,plain, % 63.11/63.18 (E(f4(f8(x3151),f8(f1(x3152))),f4(f8(f1(x3151)),f8(x3152)))), % 63.11/63.18 inference(scs_inference,[],[309,310,303,2,3])). % 63.11/63.18 cnf(318,plain, % 63.11/63.18 (E(f11(x3181,f8(x3182)),f11(x3181,f8(f1(x3182))))), % 63.11/63.18 inference(scs_inference,[],[24,2,16])). % 63.11/63.18 cnf(319,plain, % 63.11/63.18 (E(f4(f8(f1(x3191)),f8(x3192)),f4(f8(x3191),f8(f1(x3192))))), % 63.11/63.18 inference(scs_inference,[],[315,2])). % 63.11/63.18 cnf(320,plain, % 63.11/63.18 (E(f4(f8(x3201),f8(f1(f1(x3202)))),f4(f8(f1(x3201)),f8(x3202)))), % 63.11/63.18 inference(scs_inference,[],[315,309,2,3])). % 63.11/63.18 cnf(322,plain, % 63.11/63.18 (E(f3(f8(x3221),x3222,x3223),f3(f8(f1(x3221)),x3222,x3223))), % 63.11/63.18 inference(scs_inference,[],[24,2,17])). % 63.11/63.18 cnf(323,plain, % 63.11/63.18 (E(f4(f8(f1(x3231)),f8(x3232)),f4(f8(x3231),f8(f1(f1(x3232)))))), % 63.11/63.18 inference(scs_inference,[],[320,2])). % 63.11/63.18 cnf(327,plain, % 63.11/63.18 (E(f3(x3271,f8(x3272),x3273),f3(x3271,f8(f1(x3272)),x3273))), % 63.11/63.18 inference(scs_inference,[],[24,2,18])). % 63.11/63.18 cnf(328,plain, % 63.11/63.18 (E(f11(x3281,f8(f1(x3282))),f11(x3281,f8(x3282)))), % 63.11/63.18 inference(scs_inference,[],[318,2])). % 63.11/63.18 cnf(329,plain, % 63.11/63.18 (E(f11(f8(x3291),f8(x3292)),f11(f8(f1(x3291)),f8(f1(x3292))))), % 63.11/63.18 inference(scs_inference,[],[318,313,2,3])). % 63.11/63.18 cnf(332,plain, % 63.11/63.18 (E(f3(x3321,x3322,f8(x3323)),f3(x3321,x3322,f8(f1(x3323))))), % 63.11/63.18 inference(scs_inference,[],[24,2,19])). % 63.11/63.18 cnf(333,plain, % 63.11/63.18 (E(f3(f8(f1(x3331)),x3332,x3333),f3(f8(x3331),x3332,x3333))), % 63.11/63.18 inference(scs_inference,[],[322,2])). % 63.11/63.18 cnf(334,plain, % 63.11/63.18 (E(f4(f8(f1(f1(x3341))),f8(x3342)),f4(f8(x3341),f8(f1(f1(f1(x3342))))))), % 63.11/63.18 inference(scs_inference,[],[319,322,323,2,3])). % 63.11/63.18 cnf(337,plain, % 63.11/63.18 (E(f5(f8(x3371)),f5(f8(f1(x3371))))), % 63.11/63.18 inference(scs_inference,[],[24,2,20])). % 63.11/63.18 cnf(338,plain, % 63.11/63.18 (E(f3(x3381,f8(f1(x3382)),x3383),f3(x3381,f8(x3382),x3383))), % 63.11/63.18 inference(scs_inference,[],[327,2])). % 63.11/63.18 cnf(342,plain, % 63.11/63.18 (E(f8(f8(x3421)),f8(f8(f1(x3421))))), % 63.11/63.18 inference(scs_inference,[],[24,2,5])). % 63.11/63.18 cnf(343,plain, % 63.11/63.18 (E(f11(f8(f1(x3431)),f8(f1(x3432))),f11(f8(x3431),f8(x3432)))), % 63.11/63.18 inference(scs_inference,[],[329,2])). % 63.11/63.18 cnf(344,plain, % 63.11/63.18 (E(f3(x3441,f8(f1(x3442)),f8(x3443)),f3(x3441,f8(x3442),f8(f1(x3443))))), % 63.11/63.18 inference(scs_inference,[],[338,329,332,2,3])). % 63.11/63.18 cnf(347,plain, % 63.11/63.18 (E(f6(f8(x3471),x3472),f6(f8(f1(x3471)),x3472))), % 63.11/63.18 inference(scs_inference,[],[24,2,6])). % 63.11/63.18 cnf(348,plain, % 63.11/63.18 (E(f5(f8(f1(x3481))),f5(f8(x3481)))), % 63.11/63.18 inference(scs_inference,[],[337,2])). % 63.11/63.18 cnf(349,plain, % 63.11/63.18 (E(f11(f8(f1(x3491)),f8(f1(f1(x3492)))),f11(f8(x3491),f8(x3492)))), % 63.11/63.18 inference(scs_inference,[],[328,343,337,2,3])). % 63.11/63.18 cnf(352,plain, % 63.11/63.18 (E(f6(x3521,f8(x3522)),f6(x3521,f8(f1(x3522))))), % 63.11/63.18 inference(scs_inference,[],[24,2,7])). % 63.11/63.18 cnf(353,plain, % 63.11/63.18 (E(f11(f8(x3531),f8(x3532)),f11(f8(f1(x3531)),f8(f1(f1(x3532)))))), % 63.11/63.18 inference(scs_inference,[],[349,2])). % 63.11/63.18 cnf(354,plain, % 63.11/63.18 (E(f11(f8(f1(x3541)),f8(f1(f1(f1(x3542))))),f11(f8(x3541),f8(x3542)))), % 63.11/63.18 inference(scs_inference,[],[349,328,2,3])). % 63.11/63.19 cnf(356,plain, % 63.11/63.19 (E(f14(f8(x3561)),f14(f8(f1(x3561))))), % 63.11/63.19 inference(scs_inference,[],[24,2,8])). % 63.11/63.19 cnf(357,plain, % 63.11/63.19 (E(f11(f8(x3571),f8(x3572)),f11(f8(f1(x3571)),f8(f1(f1(f1(x3572))))))), % 63.11/63.19 inference(scs_inference,[],[354,2])). % 63.11/63.19 cnf(358,plain, % 63.11/63.19 (E(f8(f1(f8(x3581))),f8(f8(f1(x3581))))), % 63.11/63.19 inference(scs_inference,[],[24,354,342,2,3])). % 63.11/63.19 cnf(360,plain, % 63.11/63.19 (E(f9(f8(x3601)),f9(f8(f1(x3601))))), % 63.11/63.19 inference(scs_inference,[],[24,2,9])). % 63.11/63.19 cnf(362,plain, % 63.11/63.19 (E(f3(f9(f10(f8(f1(x3621)))),f8(f1(x3622)),f8(x3623)),f3(f9(f10(f8(x3621))),f8(x3622),f8(f1(x3623))))), % 63.11/63.19 inference(scs_inference,[],[344,254,2,3])). % 63.11/63.19 cnf(365,plain, % 63.11/63.19 (E(f12(f8(x3651),x3652),f12(f8(f1(x3651)),x3652))), % 63.11/63.19 inference(scs_inference,[],[24,2,11])). % 63.11/63.19 cnf(366,plain, % 63.11/63.19 (E(f6(f8(f1(x3661)),x3662),f6(f8(x3661),x3662))), % 63.11/63.19 inference(scs_inference,[],[347,2])). % 63.11/63.19 cnf(367,plain, % 63.11/63.19 (E(f6(f8(x3671),f8(x3672)),f6(f8(f1(x3671)),f8(f1(x3672))))), % 63.11/63.19 inference(scs_inference,[],[347,352,2,3])). % 63.11/63.19 cnf(371,plain, % 63.11/63.19 (E(f14(f8(f1(x3711))),f14(f8(x3711)))), % 63.11/63.19 inference(scs_inference,[],[356,2])). % 63.11/63.19 cnf(372,plain, % 63.11/63.19 (E(f8(f1(f1(f8(x3721)))),f8(f8(f1(x3721))))), % 63.11/63.19 inference(scs_inference,[],[24,356,358,2,3])). % 63.11/63.19 cnf(375,plain, % 63.11/63.19 (E(f9(f8(f1(x3751))),f9(f8(x3751)))), % 63.11/63.19 inference(scs_inference,[],[360,2])). % 63.11/63.19 cnf(376,plain, % 63.11/63.19 (E(f12(f8(x3761),f4(f8(x3762),x3763)),f12(f8(f1(x3761)),f4(f8(f1(x3762)),x3763)))), % 63.11/63.19 inference(scs_inference,[],[58,360,365,2,3])). % 63.11/63.19 cnf(381,plain, % 63.11/63.19 (E(f8(f1(f1(f1(f8(x3811))))),f8(f8(f1(x3811))))), % 63.11/63.19 inference(scs_inference,[],[24,362,372,2,3])). % 63.11/63.19 cnf(384,plain, % 63.11/63.19 (E(f6(f8(f1(x3841)),f8(f1(x3842))),f6(f8(x3841),f8(x3842)))), % 63.11/63.19 inference(scs_inference,[],[367,2])). % 63.11/63.19 cnf(385,plain, % 63.11/63.19 (E(f3(f8(f1(x3851)),f5(f12(f8(f1(x3852)),x3853)),x3854),f3(f8(x3851),f5(f12(f8(x3852),x3853)),x3854))), % 63.11/63.19 inference(scs_inference,[],[367,282,333,2,3])). % 63.11/63.19 cnf(389,plain, % 63.11/63.19 (E(f8(f8(f1(x3891))),f8(f1(f1(f1(f8(x3891))))))), % 63.11/63.19 inference(scs_inference,[],[381,2])). % 63.11/63.19 cnf(390,plain, % 63.11/63.19 (E(f6(f8(f1(f1(x3901))),f8(f1(x3902))),f6(f8(x3901),f8(x3902)))), % 63.11/63.19 inference(scs_inference,[],[366,384,381,2,3])). % 63.11/63.19 cnf(394,plain, % 63.11/63.19 (E(f6(f8(x3941),f8(x3942)),f6(f8(f1(f1(x3941))),f8(f1(x3942))))), % 63.11/63.19 inference(scs_inference,[],[390,2])). % 63.11/63.19 cnf(395,plain, % 63.11/63.19 (E(f6(f8(f1(f1(f1(x3951)))),f8(f1(x3952))),f6(f8(x3951),f8(x3952)))), % 63.11/63.19 inference(scs_inference,[],[390,366,2,3])). % 63.11/63.19 cnf(398,plain, % 63.11/63.19 (E(f6(f8(x3981),f8(x3982)),f6(f8(f1(f1(f1(x3981)))),f8(f1(x3982))))), % 63.11/63.19 inference(scs_inference,[],[395,2])). % 63.11/63.19 cnf(399,plain, % 63.11/63.19 (E(f8(f1(f8(f1(x3991)))),f8(f1(f1(f1(f8(x3991))))))), % 63.11/63.19 inference(scs_inference,[],[24,395,389,2,3])). % 63.11/63.19 cnf(429,plain, % 63.11/63.19 (E(f12(f8(f1(x4291)),f4(f8(f1(x4292)),x4293)),f12(f8(x4291),f4(f8(x4292),x4293)))), % 63.11/63.19 inference(scs_inference,[],[376,2])). % 63.11/63.19 cnf(434,plain, % 63.11/63.19 (E(f3(f8(x4341),f5(f12(f8(x4342),x4343)),x4344),f3(f8(f1(x4341)),f5(f12(f8(f1(x4342)),x4343)),x4344))), % 63.11/63.19 inference(scs_inference,[],[385,2])). % 63.11/63.19 cnf(438,plain, % 63.11/63.19 (E(f4(f8(x4381),f8(f1(f1(f1(x4382))))),f4(f8(f1(f1(x4381))),f8(x4382)))), % 63.11/63.19 inference(scs_inference,[],[334,2])). % 63.11/63.19 cnf(439,plain, % 63.11/63.19 (E(f12(f8(f1(x4391)),f4(f8(f1(f1(x4392))),x4393)),f12(f8(x4391),f4(f8(x4392),x4393)))), % 63.11/63.19 inference(scs_inference,[],[57,429,334,2,3])). % 63.11/63.19 cnf(444,plain, % 63.11/63.19 (E(f3(f8(x4441),f5(f12(f8(x4442),x4443)),f8(x4444)),f3(f8(f1(x4441)),f5(f12(f8(f1(x4442)),x4443)),f8(f1(x4444))))), % 63.11/63.19 inference(scs_inference,[],[439,434,332,2,3])). % 63.11/63.19 cnf(449,plain, % 63.11/63.19 (E(f3(f8(x4491),f5(f12(f8(f1(x4492)),x4493)),f8(x4494)),f3(f8(f1(x4491)),f5(f12(f8(f1(x4492)),x4493)),f8(f1(x4494))))), % 63.11/63.19 inference(scs_inference,[],[444,282,2,3])). % 63.11/63.19 cnf(454,plain, % 63.11/63.19 (E(f4(f8(x4541),f8(f1(f1(f1(x4542))))),f4(f8(f1(f1(x4541))),f8(f1(x4542))))), % 63.11/63.19 inference(scs_inference,[],[438,449,308,2,3])). % 63.11/63.19 cnf(457,plain, % 63.11/63.19 (E(f4(f8(f1(f1(x4571))),f8(f1(x4572))),f4(f8(x4571),f8(f1(f1(f1(x4572))))))), % 63.11/63.19 inference(scs_inference,[],[454,2])). % 63.11/63.19 cnf(458,plain, % 63.11/63.19 (E(f11(f8(x4581),f8(x4582)),f11(f8(f1(f1(x4581))),f8(f1(f1(f1(x4582))))))), % 63.11/63.19 inference(scs_inference,[],[454,353,329,2,3])). % 63.11/63.19 cnf(462,plain, % 63.11/63.19 (E(f4(f8(f1(f1(x4621))),f8(f1(x4622))),f4(f8(f1(x4621)),f8(f1(x4622))))), % 63.11/63.19 inference(scs_inference,[],[399,457,320,2,3])). % 63.11/63.19 cnf(465,plain, % 63.11/63.19 (E(f11(f8(f1(f1(x4651))),f8(f1(f1(f1(x4652))))),f11(f8(x4651),f8(x4652)))), % 63.11/63.19 inference(scs_inference,[],[458,2])). % 63.11/63.19 cnf(466,plain, % 63.11/63.19 (E(f11(f8(x4661),f8(x4662)),f11(f8(x4661),f8(f1(f1(x4662)))))), % 63.11/63.19 inference(scs_inference,[],[357,458,343,2,3])). % 63.11/63.19 cnf(469,plain, % 63.11/63.19 (E(f11(f8(x4691),f8(f1(f1(x4692)))),f11(f8(x4691),f8(x4692)))), % 63.11/63.19 inference(scs_inference,[],[466,2])). % 63.11/63.19 cnf(470,plain, % 63.11/63.19 (E(f11(f8(f1(f1(x4701))),f8(f1(x4702))),f11(f8(x4701),f8(x4702)))), % 63.11/63.19 inference(scs_inference,[],[465,466,2,3])). % 63.11/63.19 cnf(473,plain, % 63.11/63.19 (E(f11(f8(x4731),f8(x4732)),f11(f8(f1(f1(x4731))),f8(f1(x4732))))), % 63.11/63.19 inference(scs_inference,[],[470,2])). % 63.11/63.19 cnf(474,plain, % 63.11/63.19 (E(f4(f8(f1(f1(x4741))),f8(f1(x4742))),f4(f8(x4741),f8(f1(f1(x4742)))))), % 63.11/63.19 inference(scs_inference,[],[470,462,319,2,3])). % 63.11/63.19 cnf(477,plain, % 63.11/63.19 (E(f4(f8(x4771),f8(f1(f1(x4772)))),f4(f8(f1(f1(x4771))),f8(f1(x4772))))), % 63.11/63.19 inference(scs_inference,[],[474,2])). % 63.11/63.19 cnf(478,plain, % 63.11/63.19 (E(f11(f8(x4781),f8(f1(x4782))),f11(f8(f1(f1(x4781))),f8(x4782)))), % 63.11/63.19 inference(scs_inference,[],[469,473,474,2,3])). % 63.11/63.19 cnf(482,plain, % 63.11/63.19 (E(f11(f8(f1(f1(x4821))),f8(x4822)),f11(f8(x4821),f8(f1(x4822))))), % 63.11/63.19 inference(scs_inference,[],[478,2])). % 63.11/63.19 cnf(483,plain, % 63.11/63.19 (E(f11(f8(x4831),f8(f1(f1(f1(f1(x4832)))))),f11(f8(f1(x4831)),f8(x4832)))), % 63.11/63.19 inference(scs_inference,[],[478,354,2,3])). % 63.11/63.19 cnf(488,plain, % 63.11/63.19 (E(f6(f8(x4881),f8(x4882)),f6(f8(f1(f1(x4881))),f8(f1(f1(x4882)))))), % 63.11/63.19 inference(scs_inference,[],[483,394,352,2,3])). % 63.11/63.19 cnf(491,plain, % 63.11/63.19 (E(f6(f8(f1(f1(x4911))),f8(f1(f1(x4912)))),f6(f8(x4911),f8(x4912)))), % 63.11/63.19 inference(scs_inference,[],[488,2])). % 63.11/63.19 cnf(492,plain, % 63.11/63.19 (E(f6(f8(x4921),f8(x4922)),f6(f8(f1(f1(x4921))),f8(x4922)))), % 63.11/63.19 inference(scs_inference,[],[398,488,384,2,3])). % 63.11/63.19 cnf(495,plain, % 63.11/63.19 (E(f6(f8(f1(f1(x4951))),f8(x4952)),f6(f8(x4951),f8(x4952)))), % 63.11/63.19 inference(scs_inference,[],[492,2])). % 63.11/63.19 cnf(496,plain, % 63.11/63.19 (E(f6(f8(x4961),f8(f1(f1(x4962)))),f6(f8(x4961),f8(x4962)))), % 63.11/63.19 inference(scs_inference,[],[491,492,2,3])). % 63.11/63.19 cnf(500,plain, % 63.11/63.19 (E(f6(f8(x5001),f8(x5002)),f6(f8(x5001),f8(f1(f1(x5002)))))), % 63.11/63.19 inference(scs_inference,[],[496,2])). % 63.11/63.19 cnf(501,plain, % 63.11/63.19 (E(f11(f8(f1(f1(f1(f1(x5011))))),f8(f1(f1(x5012)))),f11(f8(x5011),f8(x5012)))), % 63.11/63.19 inference(scs_inference,[],[496,482,465,2,3])). % 63.11/63.19 cnf(504,plain, % 63.11/63.19 (E(f11(f8(x5041),f8(x5042)),f11(f8(f1(f1(f1(f1(x5041))))),f8(f1(f1(x5042)))))), % 63.11/63.19 inference(scs_inference,[],[501,2])). % 63.11/63.19 cnf(505,plain, % 63.11/63.19 (E(f6(f8(f1(f1(x5051))),f8(x5052)),f6(f8(x5051),f8(f1(f1(x5052)))))), % 63.11/63.19 inference(scs_inference,[],[495,501,500,2,3])). % 63.11/63.19 cnf(509,plain, % 63.11/63.19 (E(f6(f8(x5091),f8(f1(f1(x5092)))),f6(f8(f1(f1(x5091))),f8(x5092)))), % 63.11/63.19 inference(scs_inference,[],[505,2])). % 63.11/63.19 cnf(510,plain, % 63.11/63.19 (E(f11(f8(x5101),f8(x5102)),f11(f8(f1(f1(f1(f1(x5101))))),f8(x5102)))), % 63.11/63.19 inference(scs_inference,[],[504,505,469,2,3])). % 63.11/63.19 cnf(514,plain, % 63.11/63.19 (E(f6(f8(f1(x5141)),f8(f1(f1(f1(x5142))))),f6(f8(x5141),f8(x5142)))), % 63.11/63.19 inference(scs_inference,[],[509,510,395,2,3])). % 63.11/63.19 cnf(517,plain, % 63.11/63.19 (E(f6(f8(x5171),f8(x5172)),f6(f8(f1(x5171)),f8(f1(f1(f1(x5172))))))), % 63.11/63.19 inference(scs_inference,[],[514,2])). % 63.11/63.19 cnf(518,plain, % 63.11/63.19 (E(f6(f8(f1(f1(f1(x5181)))),f8(f1(f1(f1(x5182))))),f6(f8(x5181),f8(x5182)))), % 63.11/63.19 inference(scs_inference,[],[514,495,2,3])). % 63.11/63.19 cnf(522,plain, % 63.11/63.19 (E(f6(f8(x5221),f8(x5222)),f6(f8(f1(f1(f1(x5221)))),f8(f1(f1(f1(x5222))))))), % 63.11/63.19 inference(scs_inference,[],[518,2])). % 63.11/63.19 cnf(527,plain, % 63.11/63.19 (E(f8(f8(f1(x5271))),f8(f8(x5271)))), % 63.11/63.19 inference(scs_inference,[],[342,2])). % 63.11/63.19 cnf(528,plain, % 63.11/63.19 (E(f6(f8(f1(x5281)),f8(x5282)),f6(f8(x5281),f8(f1(x5282))))), % 63.11/63.19 inference(scs_inference,[],[517,491,342,2,3])). % 63.11/63.19 cnf(532,plain, % 63.11/63.19 (E(f6(f8(x5321),f8(f1(x5322))),f6(f8(f1(x5321)),f8(x5322)))), % 63.11/63.19 inference(scs_inference,[],[528,2])). % 63.11/63.19 cnf(533,plain, % 63.11/63.19 (E(f8(f1(f8(f1(x5331)))),f8(f8(x5331)))), % 63.11/63.19 inference(scs_inference,[],[24,527,528,2,3])). % 63.11/63.19 cnf(536,plain, % 63.11/63.19 (E(f8(f8(x5361)),f8(f1(f8(f1(x5361)))))), % 63.11/63.19 inference(scs_inference,[],[533,2])). % 63.11/63.19 cnf(537,plain, % 63.11/63.19 (E(f6(f8(x5371),f8(x5372)),f6(f8(f1(f1(f1(f1(x5371))))),f8(f1(f1(x5372)))))), % 63.11/63.19 inference(scs_inference,[],[532,533,522,2,3])). % 63.11/63.19 cnf(541,plain, % 63.11/63.19 (E(f8(f1(f8(x5411))),f8(f1(f8(f1(x5411)))))), % 63.11/63.19 inference(scs_inference,[],[24,536,537,2,3])). % 63.11/63.19 cnf(544,plain, % 63.11/63.19 (E(f8(f1(f8(f1(x5441)))),f8(f1(f8(x5441))))), % 63.11/63.19 inference(scs_inference,[],[541,2])). % 63.11/63.19 cnf(545,plain, % 63.11/63.19 (E(f8(f1(f1(f8(x5451)))),f8(f1(f8(f1(x5451)))))), % 63.11/63.19 inference(scs_inference,[],[24,541,2,3])). % 63.11/63.19 cnf(548,plain, % 63.11/63.19 (E(f8(f1(f8(f1(x5481)))),f8(f1(f1(f8(x5481)))))), % 63.11/63.19 inference(scs_inference,[],[545,2])). % 63.11/63.19 cnf(549,plain, % 63.11/63.19 (E(f8(f1(f1(f8(f1(x5491))))),f8(f1(f8(x5491))))), % 63.11/63.19 inference(scs_inference,[],[24,544,545,2,3])). % 63.11/63.19 cnf(553,plain, % 63.11/63.19 (E(f8(f1(f1(f8(f1(x5531))))),f8(f1(f1(f8(x5531)))))), % 63.11/63.19 inference(scs_inference,[],[24,549,548,2,3])). % 63.11/63.19 cnf(557,plain, % 63.11/63.19 (E(f8(f1(f1(f8(f1(x5571))))),f8(f8(x5571)))), % 63.11/63.19 inference(scs_inference,[],[24,553,533,2,3])). % 63.11/63.19 cnf(559,plain, % 63.11/63.19 (E(f8(f8(x5591)),f8(f1(f1(f8(f1(x5591))))))), % 63.11/63.19 inference(scs_inference,[],[557,2])). % 63.11/63.19 cnf(568,plain, % 63.11/63.19 (E(f8(f8(f1(x5681))),f8(f1(f8(x5681))))), % 63.11/63.19 inference(scs_inference,[],[358,2])). % 63.11/63.19 cnf(573,plain, % 63.11/63.19 (E(f12(f8(f1(x5731)),x5732),f12(f8(x5731),x5732))), % 63.11/63.19 inference(scs_inference,[],[365,2])). % 63.11/63.19 cnf(574,plain, % 63.11/63.19 (E(f12(f8(x5741),f4(f8(f1(x5742)),x5743)),f12(f8(f1(x5741)),f4(f8(x5742),x5743)))), % 63.11/63.19 inference(scs_inference,[],[57,365,2,3])). % 63.11/63.19 cnf(577,plain, % 63.11/63.19 (E(f12(f8(f1(x5771)),f4(f8(x5772),x5773)),f12(f8(x5771),f4(f8(f1(x5772)),x5773)))), % 63.11/63.19 inference(scs_inference,[],[574,2])). % 63.11/63.19 cnf(578,plain, % 63.11/63.19 (E(f12(f8(f1(x5781)),f8(f1(x5782))),f12(f8(x5781),f8(x5782)))), % 63.11/63.19 inference(scs_inference,[],[573,574,299,2,3])). % 63.11/63.19 cnf(582,plain, % 63.11/63.19 (E(f12(f8(x5821),f8(x5822)),f12(f8(f1(x5821)),f8(f1(x5822))))), % 63.11/63.19 inference(scs_inference,[],[578,2])). % 63.11/63.19 cnf(583,plain, % 63.11/63.19 (E(f12(f8(f1(f1(x5831))),f8(f1(x5832))),f12(f8(x5831),f8(x5832)))), % 63.11/63.19 inference(scs_inference,[],[578,573,2,3])). % 63.11/63.19 cnf(586,plain, % 63.11/63.19 (E(f12(f8(x5861),f8(x5862)),f12(f8(f1(f1(x5861))),f8(f1(x5862))))), % 63.11/63.19 inference(scs_inference,[],[583,2])). % 63.11/63.19 cnf(587,plain, % 63.11/63.19 (E(f12(f8(f1(x5871)),f4(f8(x5872),x5873)),f12(f8(x5871),f4(f8(f1(f1(x5872))),x5873)))), % 63.11/63.19 inference(scs_inference,[],[58,583,577,2,3])). % 63.11/63.19 cnf(592,plain, % 63.11/63.19 (E(f12(f8(x5921),f8(x5922)),f12(f8(f1(f1(f1(x5921)))),f8(f1(f1(x5922)))))), % 63.11/63.19 inference(scs_inference,[],[582,586,587,2,3])). % 63.11/63.19 cnf(594,plain, % 63.11/63.19 (E(f12(f8(f1(f1(f1(x5941)))),f8(f1(f1(x5942)))),f12(f8(x5941),f8(x5942)))), % 63.11/63.19 inference(scs_inference,[],[592,2])). % 63.11/63.19 cnf(595,plain, % 63.11/63.19 (E(f4(f8(x5951),f8(f1(f1(x5952)))),f4(f8(f1(x5951)),f8(f1(f1(f1(x5952))))))), % 63.11/63.19 inference(scs_inference,[],[477,592,323,2,3])). % 63.11/63.19 cnf(598,plain, % 63.11/63.19 (E(f4(f8(f1(x5981)),f8(f1(f1(f1(x5982))))),f4(f8(x5981),f8(f1(f1(x5982)))))), % 63.11/63.19 inference(scs_inference,[],[595,2])). % 63.11/63.19 cnf(599,plain, % 63.11/63.19 (E(f4(f8(x5991),f8(f1(f1(x5992)))),f4(f8(f1(f1(f1(x5991)))),f8(x5992)))), % 63.11/63.19 inference(scs_inference,[],[595,438,2,3])). % 63.11/63.19 cnf(602,plain, % 63.11/63.19 (E(f4(f8(f1(f1(f1(x6021)))),f8(x6022)),f4(f8(x6021),f8(f1(f1(x6022)))))), % 63.11/63.19 inference(scs_inference,[],[599,2])). % 63.11/63.19 cnf(603,plain, % 63.11/63.19 (E(f12(f8(f1(f1(f1(x6031)))),f8(f1(f1(f1(x6032))))),f12(f8(x6031),f8(x6032)))), % 63.11/63.19 inference(scs_inference,[],[594,599,299,2,3])). % 63.11/63.19 cnf(607,plain, % 63.11/63.19 (E(f12(f8(x6071),f8(x6072)),f12(f8(f1(f1(f1(x6071)))),f8(f1(f1(f1(x6072))))))), % 63.11/63.19 inference(scs_inference,[],[603,2])). % 63.11/63.19 cnf(608,plain, % 63.11/63.19 (E(f4(f8(f1(x6081)),f8(f1(f1(f1(x6082))))),f4(f8(x6081),f8(f1(x6082))))), % 63.11/63.19 inference(scs_inference,[],[603,598,309,2,3])). % 63.11/63.19 cnf(610,plain, % 63.11/63.19 (E(f4(f8(x6101),f8(f1(x6102))),f4(f8(f1(x6101)),f8(f1(f1(f1(x6102))))))), % 63.11/63.19 inference(scs_inference,[],[608,2])). % 63.11/63.19 cnf(611,plain, % 63.11/63.19 (E(f4(f8(f1(f1(f1(f1(x6111))))),f8(f1(x6112))),f4(f8(x6111),f8(f1(x6112))))), % 63.11/63.19 inference(scs_inference,[],[608,602,2,3])). % 63.11/63.19 cnf(614,plain, % 63.11/63.19 (E(f4(f8(x6141),f8(f1(x6142))),f4(f8(f1(f1(f1(f1(x6141))))),f8(f1(x6142))))), % 63.11/63.19 inference(scs_inference,[],[611,2])). % 63.11/63.19 cnf(615,plain, % 63.11/63.19 (E(f12(f8(x6151),f8(x6152)),f12(f8(f1(x6151)),f8(f1(f1(x6152)))))), % 63.11/63.19 inference(scs_inference,[],[611,607,583,2,3])). % 63.11/63.19 cnf(618,plain, % 63.11/63.19 (E(f12(f8(f1(x6181)),f8(f1(f1(x6182)))),f12(f8(x6181),f8(x6182)))), % 63.11/63.19 inference(scs_inference,[],[615,2])). % 63.11/63.19 cnf(619,plain, % 63.11/63.19 (E(f12(f8(f1(f1(x6191))),f8(x6192)),f12(f8(x6191),f8(x6192)))), % 63.11/63.19 inference(scs_inference,[],[615,594,2,3])). % 63.11/63.19 cnf(623,plain, % 63.11/63.19 (E(f12(f8(x6231),f8(x6232)),f12(f8(f1(f1(x6231))),f8(x6232)))), % 63.11/63.19 inference(scs_inference,[],[619,2])). % 63.11/63.19 cnf(624,plain, % 63.11/63.19 (E(f4(f8(x6241),f8(f1(x6242))),f4(f8(f1(f1(f1(x6241)))),f8(f1(x6242))))), % 63.11/63.19 inference(scs_inference,[],[619,614,462,2,3])). % 63.11/63.19 cnf(626,plain, % 63.11/63.19 (E(f4(f8(f1(f1(f1(x6261)))),f8(f1(x6262))),f4(f8(x6261),f8(f1(x6262))))), % 63.11/63.19 inference(scs_inference,[],[624,2])). % 63.11/63.19 cnf(627,plain, % 63.11/63.19 (E(f12(f8(x6271),f8(f1(f1(x6272)))),f12(f8(f1(x6271)),f8(x6272)))), % 63.11/63.19 inference(scs_inference,[],[618,623,624,2,3])). % 63.11/63.19 cnf(631,plain, % 63.11/63.19 (E(f12(f8(f1(x6311)),f8(x6312)),f12(f8(x6311),f8(f1(f1(x6312)))))), % 63.11/63.19 inference(scs_inference,[],[627,2])). % 63.11/63.19 cnf(632,plain, % 63.11/63.19 (E(f12(f8(x6321),f8(f1(f1(f1(f1(x6322)))))),f12(f8(x6321),f8(x6322)))), % 63.11/63.19 inference(scs_inference,[],[627,618,2,3])). % 63.11/63.19 cnf(637,plain, % 63.11/63.19 (E(f4(f8(f1(f1(f1(x6371)))),f8(f1(x6372))),f4(f8(f1(x6371)),f8(x6372)))), % 63.11/63.19 inference(scs_inference,[],[632,626,315,2,3])). % 63.11/63.19 cnf(640,plain, % 63.11/63.19 (E(f4(f8(f1(x6401)),f8(x6402)),f4(f8(f1(f1(f1(x6401)))),f8(f1(x6402))))), % 63.11/63.19 inference(scs_inference,[],[637,2])). % 63.11/63.19 cnf(641,plain, % 63.11/63.19 (E(f12(f8(f1(f1(f1(f1(x6411))))),f8(f1(x6412))),f12(f8(x6411),f8(x6412)))), % 63.11/63.19 inference(scs_inference,[],[637,631,603,2,3])). % 63.11/63.19 cnf(643,plain, % 63.11/63.19 (E(f12(f8(x6431),f8(x6432)),f12(f8(f1(f1(f1(f1(x6431))))),f8(f1(x6432))))), % 63.11/63.19 inference(scs_inference,[],[641,2])). % 63.11/63.19 cnf(644,plain, % 63.11/63.19 (E(f12(f8(f1(f1(f1(f1(x6441))))),f8(f1(x6442))),f12(f8(f1(x6441)),f8(f1(x6442))))), % 63.11/63.19 inference(scs_inference,[],[641,582,2,3])). % 63.11/63.19 cnf(648,plain, % 63.11/63.19 (E(f4(f8(f1(f1(x6481))),f8(x6482)),f4(f8(x6481),f8(f1(x6482))))), % 63.11/63.19 inference(scs_inference,[],[640,644,611,2,3])). % 63.11/63.19 cnf(652,plain, % 63.11/63.19 (E(f4(f8(x6521),f8(f1(x6522))),f4(f8(f1(f1(x6521))),f8(x6522)))), % 63.11/63.19 inference(scs_inference,[],[648,2])). % 63.11/63.19 cnf(653,plain, % 63.11/63.19 (E(f4(f8(f1(f1(x6531))),f8(x6532)),f4(f8(f1(x6531)),f8(f1(f1(f1(x6532))))))), % 63.11/63.19 inference(scs_inference,[],[648,610,2,3])). % 63.11/63.19 cnf(656,plain, % 63.11/63.19 (E(f4(f8(f1(x6561)),f8(f1(f1(f1(x6562))))),f4(f8(f1(f1(x6561))),f8(x6562)))), % 63.11/63.19 inference(scs_inference,[],[653,2])). % 63.11/63.19 cnf(657,plain, % 63.11/63.19 (E(f4(f8(f1(f1(x6571))),f8(x6572)),f4(f8(f1(f1(f1(x6571)))),f8(f1(f1(x6572)))))), % 63.11/63.19 inference(scs_inference,[],[652,653,2,3])). % 63.11/63.19 cnf(659,plain, % 63.11/63.19 (E(f4(f8(f1(f1(f1(x6591)))),f8(f1(f1(x6592)))),f4(f8(f1(f1(x6591))),f8(x6592)))), % 63.11/63.19 inference(scs_inference,[],[657,2])). % 63.11/63.19 cnf(682,plain, % 63.11/63.19 (E(f10(f1(f8(f1(x6821)))),f10(f1(f8(x6821))))), % 63.11/63.19 inference(scs_inference,[],[24,4,10])). % 63.11/63.19 cnf(686,plain, % 63.11/63.19 (E(f1(f8(f8(f1(x6861)))),f1(f8(f8(x6861))))), % 63.11/63.19 inference(scs_inference,[],[24,4,5])). % 63.11/63.19 cnf(688,plain, % 63.11/63.19 (E(f1(f8(f1(f8(f1(x6881))))),f1(f8(f8(x6881))))), % 63.11/63.19 inference(scs_inference,[],[40,682,686,2,3])). % 63.11/63.19 cnf(695,plain, % 63.11/63.19 (E(f1(f6(f8(f1(x6951)),x6952)),f1(f6(f8(x6951),x6952)))), % 63.11/63.19 inference(scs_inference,[],[24,4,6])). % 63.11/63.19 cnf(696,plain, % 63.11/63.19 (E(f1(f8(f8(x6961))),f1(f8(f1(f8(f1(x6961))))))), % 63.11/63.19 inference(scs_inference,[],[688,2])). % 63.11/63.19 cnf(705,plain, % 63.11/63.19 (E(f1(f6(x7051,f8(f1(x7052)))),f1(f6(x7051,f8(x7052))))), % 63.11/63.19 inference(scs_inference,[],[24,4,7])). % 63.11/63.19 cnf(706,plain, % 63.11/63.19 (E(f1(f6(f8(x7061),x7062)),f1(f6(f8(f1(x7061)),x7062)))), % 63.11/63.19 inference(scs_inference,[],[695,2])). % 63.11/63.19 cnf(707,plain, % 63.11/63.19 (E(f1(f6(f8(f1(x7071)),f8(f1(x7072)))),f1(f6(f8(x7071),f8(x7072))))), % 63.11/63.19 inference(scs_inference,[],[695,705,2,3])). % 63.11/63.19 cnf(710,plain, % 63.11/63.19 (E(f4(f1(f8(f1(x7101))),x7102),f4(f1(f8(x7101)),x7102))), % 63.11/63.19 inference(scs_inference,[],[24,4,13])). % 63.11/63.19 cnf(715,plain, % 63.11/63.19 (E(f1(f6(f8(x7151),f8(x7152))),f1(f6(f8(f1(x7151)),f8(f1(x7152)))))), % 63.11/63.19 inference(scs_inference,[],[707,2])). % 63.11/63.19 cnf(716,plain, % 63.11/63.19 (E(f4(f1(f8(f1(x7161))),f11(f8(f1(x7162)),x7163)),f4(f1(f8(x7161)),f11(f8(x7162),x7163)))), % 63.11/63.19 inference(scs_inference,[],[65,707,710,2,3])). % 63.11/63.19 cnf(719,plain, % 63.11/63.19 (E(f4(x7191,f1(f8(f1(x7192)))),f4(x7191,f1(f8(x7192))))), % 63.11/63.19 inference(scs_inference,[],[24,4,14])). % 63.11/63.19 cnf(724,plain, % 63.11/63.19 (E(f1(f9(f8(f1(x7241)))),f1(f9(f8(x7241))))), % 63.11/63.19 inference(scs_inference,[],[24,4,9])). % 63.11/63.19 cnf(729,plain, % 63.11/63.19 (E(f3(f1(f8(f1(x7291))),x7292,x7293),f3(f1(f8(x7291)),x7292,x7293))), % 63.11/63.19 inference(scs_inference,[],[24,4,17])). % 63.11/63.19 cnf(730,plain, % 63.11/63.19 (E(f4(x7301,f1(f8(x7302))),f4(x7301,f1(f8(f1(x7302)))))), % 63.11/63.19 inference(scs_inference,[],[719,2])). % 63.11/63.19 cnf(731,plain, % 63.11/63.19 (E(f4(f1(f8(f1(x7311))),f1(f8(f1(x7312)))),f4(f1(f8(x7311)),f1(f8(x7312))))), % 63.11/63.19 inference(scs_inference,[],[719,710,2,3])). % 63.11/63.19 cnf(736,plain, % 63.11/63.19 (E(f3(f1(f8(f1(x7361))),f3(x7362,x7363,f8(x7364)),x7365),f3(f1(f8(x7361)),f3(x7362,x7363,f8(f1(x7364))),x7365))), % 63.11/63.19 inference(scs_inference,[],[74,724,729,2,3])). % 63.11/63.19 cnf(745,plain, % 63.11/63.19 (E(f4(f1(f8(x7451)),f1(f8(x7452))),f4(f1(f8(f1(x7451))),f1(f8(f1(x7452)))))), % 63.11/63.19 inference(scs_inference,[],[731,2])). % 63.11/63.19 cnf(749,plain, % 63.11/63.19 (E(f3(x7491,x7492,f1(f8(f1(x7493)))),f3(x7491,x7492,f1(f8(x7493))))), % 63.11/63.19 inference(scs_inference,[],[24,4,19])). % 63.11/63.19 cnf(754,plain, % 63.11/63.19 (E(f1(f5(f8(f1(x7541)))),f1(f5(f8(x7541))))), % 63.11/63.19 inference(scs_inference,[],[24,4,20])). % 63.11/63.19 cnf(758,plain, % 63.11/63.19 (E(f5(f1(f8(f1(x7581)))),f5(f1(f8(x7581))))), % 63.11/63.19 inference(scs_inference,[],[24,4,20])). % 63.11/63.19 cnf(765,plain, % 63.11/63.19 (E(f1(f6(f8(x7651),f8(x7652))),f1(f6(f8(f1(f1(x7651))),f8(f1(x7652)))))), % 63.11/63.19 inference(scs_inference,[],[754,706,715,2,3])). % 63.11/63.19 cnf(774,plain, % 63.11/63.19 (E(f4(f1(f8(x7741)),f1(f8(x7742))),f4(f1(f8(f1(x7741))),f1(f8(f1(f1(x7742))))))), % 63.11/63.19 inference(scs_inference,[],[758,730,745,2,3])). % 63.11/63.19 cnf(777,plain, % 63.11/63.19 (E(f3(f1(f8(x7771)),f3(x7772,x7773,f8(f1(x7774))),x7775),f3(f1(f8(f1(x7771))),f3(x7772,x7773,f8(x7774)),x7775))), % 63.11/63.19 inference(scs_inference,[],[736,2])). % 63.11/63.19 cnf(778,plain, % 63.11/63.19 (E(f1(f6(f8(x7781),f8(f1(x7782)))),f1(f6(f8(f1(f1(x7781))),f8(f1(x7782)))))), % 63.11/63.19 inference(scs_inference,[],[736,765,705,2,3])). % 63.11/63.19 cnf(783,plain, % 63.11/63.19 (E(f3(f1(f8(x7831)),f3(x7832,x7833,f8(f1(f1(x7834)))),x7835),f3(f1(f8(f1(x7831))),f3(x7832,x7833,f8(x7834)),x7835))), % 63.11/63.19 inference(scs_inference,[],[73,777,778,2,3])). % 63.11/63.19 cnf(788,plain, % 63.11/63.19 (E(f1(f8(f1(f8(x7881)))),f1(f8(f1(f8(f1(x7881))))))), % 63.11/63.19 inference(scs_inference,[],[40,783,696,2,3])). % 63.11/63.19 cnf(804,plain, % 63.11/63.19 (E(f4(f1(f8(f1(x8041))),f1(f8(f1(f1(x8042))))),f4(f1(f8(x8041)),f1(f8(x8042))))), % 63.11/63.19 inference(scs_inference,[],[774,2])). % 63.11/63.19 cnf(807,plain, % 63.11/63.19 (E(f1(f8(f1(f8(f1(x8071))))),f1(f8(f1(f8(x8071)))))), % 63.11/63.19 inference(scs_inference,[],[788,2])). % 63.11/63.19 cnf(814,plain, % 63.11/63.19 (E(f12(f1(f8(x8141)),x8142),f12(f1(f8(f1(x8141))),x8142))), % 63.11/63.19 inference(scs_inference,[],[33,4,11])). % 63.11/63.19 cnf(821,plain, % 63.11/63.19 (E(f1(f8(f8(f1(x8211)))),f1(f8(f1(f8(x8211)))))), % 63.11/63.19 inference(scs_inference,[],[41,807,716,2,3])). % 63.11/63.19 cnf(824,plain, % 63.11/63.19 (E(f1(f8(f1(f8(x8241)))),f1(f8(f8(f1(x8241)))))), % 63.11/63.19 inference(scs_inference,[],[821,2])). % 63.11/63.19 cnf(828,plain, % 63.11/63.19 (E(f1(f10(f8(x8281))),f1(f10(f8(f1(x8281)))))), % 63.11/63.19 inference(scs_inference,[],[33,4,10])). % 63.11/63.19 cnf(829,plain, % 63.11/63.19 (E(f1(f10(f8(f1(x8291)))),f1(f10(f8(x8291))))), % 63.11/63.19 inference(scs_inference,[],[828,2])). % 63.11/63.19 cnf(833,plain, % 63.11/63.19 (E(f4(f1(f8(x8331)),x8332),f4(f1(f8(f1(x8331))),x8332))), % 63.11/63.19 inference(scs_inference,[],[33,4,13])). % 63.11/63.19 cnf(834,plain, % 63.11/63.19 (E(f3(x8341,x8342,f1(f8(x8343))),f3(x8341,x8342,f1(f8(f1(x8343)))))), % 63.11/63.19 inference(scs_inference,[],[749,2])). % 63.11/63.19 cnf(835,plain, % 63.11/63.19 (E(f4(f1(f8(x8351)),f1(f8(f1(f1(x8352))))),f4(f1(f8(x8351)),f1(f8(x8352))))), % 63.11/63.19 inference(scs_inference,[],[804,833,749,2,3])). % 63.11/63.19 cnf(838,plain, % 63.11/63.19 (E(f1(f4(x8381,f8(x8382))),f1(f4(x8381,f8(f1(x8382)))))), % 63.11/63.19 inference(scs_inference,[],[33,4,14])). % 63.11/63.19 cnf(839,plain, % 63.11/63.19 (E(f4(f1(f8(x8391)),f1(f8(x8392))),f4(f1(f8(x8391)),f1(f8(f1(f1(x8392))))))), % 63.11/63.19 inference(scs_inference,[],[835,2])). % 63.11/63.19 cnf(840,plain, % 63.11/63.19 (E(f3(x8401,f3(x8402,x8403,f8(x8404)),f1(f8(x8405))),f3(x8401,f3(x8402,x8403,f8(f1(x8404))),f1(f8(f1(x8405)))))), % 63.11/63.19 inference(scs_inference,[],[74,835,834,2,3])). % 63.11/63.19 cnf(843,plain, % 63.11/63.19 (E(f3(f1(f8(x8431)),x8432,x8433),f3(f1(f8(f1(x8431))),x8432,x8433))), % 63.11/63.19 inference(scs_inference,[],[33,4,17])). % 63.11/63.19 cnf(844,plain, % 63.11/63.19 (E(f1(f4(x8441,f8(f1(x8442)))),f1(f4(x8441,f8(x8442))))), % 63.11/63.19 inference(scs_inference,[],[838,2])). % 63.11/63.19 cnf(845,plain, % 63.11/63.19 (E(f4(f1(f8(f1(x8451))),f1(f8(x8452))),f4(f1(f8(x8451)),f1(f8(f1(x8452)))))), % 63.11/63.19 inference(scs_inference,[],[838,839,731,2,3])). % 63.11/63.19 cnf(849,plain, % 63.11/63.19 (E(f3(x8491,f3(x8492,x8493,f8(f1(x8494))),f1(f8(f1(x8495)))),f3(x8491,f3(x8492,x8493,f8(x8494)),f1(f8(x8495))))), % 63.11/63.19 inference(scs_inference,[],[840,2])). % 63.11/63.19 cnf(850,plain, % 63.11/63.19 (E(f4(f1(f8(f1(f1(x8501)))),f1(f8(f1(x8502)))),f4(f1(f8(x8501)),f1(f8(x8502))))), % 63.11/63.19 inference(scs_inference,[],[840,845,804,2,3])). % 63.11/63.19 cnf(853,plain, % 63.11/63.19 (E(f4(f1(f8(x8531)),f1(f8(x8532))),f4(f1(f8(f1(f1(x8531)))),f1(f8(f1(x8532)))))), % 63.11/63.19 inference(scs_inference,[],[850,2])). % 63.11/63.19 cnf(854,plain, % 63.11/63.19 (E(f3(x8541,f3(x8542,x8543,f8(f1(f1(x8544)))),f1(f8(f1(x8545)))),f3(x8541,f3(x8542,x8543,f8(x8544)),f1(f8(x8545))))), % 63.11/63.19 inference(scs_inference,[],[73,849,850,2,3])). % 63.11/63.19 cnf(859,plain, % 63.11/63.19 (E(f3(f1(f8(x8591)),f3(x8592,x8593,f8(x8594)),x8595),f3(f1(f8(f1(x8591))),f3(x8592,x8593,f8(f1(x8594))),x8595))), % 63.11/63.19 inference(scs_inference,[],[74,854,843,2,3])). % 63.11/63.19 cnf(862,plain, % 63.11/63.19 (E(f1(f8(x8621)),f1(f8(f1(f1(x8621)))))), % 63.11/63.19 inference(scs_inference,[],[33,41,4,3])). % 63.11/63.19 cnf(863,plain, % 63.11/63.19 (E(f3(f1(f8(f1(x8631))),f3(x8632,x8633,f8(f1(x8634))),x8635),f3(f1(f8(x8631)),f3(x8632,x8633,f8(x8634)),x8635))), % 63.11/63.19 inference(scs_inference,[],[859,2])). % 63.11/63.19 cnf(864,plain, % 63.11/63.19 (E(f1(f8(f1(f1(f8(x8641))))),f1(f8(f8(f1(x8641)))))), % 63.11/63.19 inference(scs_inference,[],[40,824,859,2,3])). % 63.11/63.19 cnf(866,plain, % 63.11/63.19 (E(f1(f3(x8661,x8662,f8(x8663))),f1(f3(x8661,x8662,f8(f1(x8663)))))), % 63.11/63.19 inference(scs_inference,[],[33,4,19])). % 63.11/63.19 cnf(867,plain, % 63.11/63.19 (E(f1(f8(f1(f1(x8671)))),f1(f8(x8671)))), % 63.11/63.19 inference(scs_inference,[],[862,2])). % 63.11/63.19 cnf(868,plain, % 63.11/63.19 (E(f3(f1(f8(f1(x8681))),f3(x8682,x8683,f8(f1(f1(x8684)))),x8685),f3(f1(f8(x8681)),f3(x8682,x8683,f8(x8684)),x8685))), % 63.11/63.19 inference(scs_inference,[],[73,863,862,2,3])). % 63.11/63.19 cnf(873,plain, % 63.11/63.19 (E(f4(f1(f8(x8731)),f1(f8(f1(x8732)))),f4(f1(f8(f1(f1(x8731)))),f1(f8(x8732))))), % 63.11/63.19 inference(scs_inference,[],[868,853,835,2,3])). % 63.11/63.19 cnf(876,plain, % 63.11/63.19 (E(f1(f12(f8(x8761),x8762)),f1(f12(f8(f1(x8761)),x8762)))), % 63.11/63.19 inference(scs_inference,[],[33,4,11])). % 63.11/63.19 cnf(878,plain, % 63.11/63.19 (E(f12(f1(f8(x8781)),f4(f8(f1(x8782)),x8783)),f12(f1(f8(f1(x8781))),f4(f8(x8782),x8783)))), % 63.11/63.19 inference(scs_inference,[],[57,873,814,2,3])). % 63.11/63.19 cnf(881,plain, % 63.11/63.19 (E(f1(f12(x8811,f8(x8812))),f1(f12(x8811,f8(f1(x8812)))))), % 63.11/63.19 inference(scs_inference,[],[33,4,12])). % 63.11/63.19 cnf(883,plain, % 63.11/63.19 (E(f1(f12(f8(x8831),f8(x8832))),f1(f12(f8(f1(x8831)),f8(f1(x8832)))))), % 63.11/63.19 inference(scs_inference,[],[878,876,881,2,3])). % 63.11/63.19 cnf(886,plain, % 63.11/63.19 (E(f1(f4(f8(x8861),x8862)),f1(f4(f8(f1(x8861)),x8862)))), % 63.11/63.19 inference(scs_inference,[],[33,4,13])). % 63.11/63.19 cnf(888,plain, % 63.11/63.19 (E(f1(f4(f8(x8881),f8(f1(x8882)))),f1(f4(f8(f1(x8881)),f8(x8882))))), % 63.11/63.19 inference(scs_inference,[],[844,864,886,2,3])). % 63.11/63.19 cnf(891,plain, % 63.11/63.19 (E(f1(f3(f8(x8911),x8912,x8913)),f1(f3(f8(f1(x8911)),x8912,x8913)))), % 63.11/63.19 inference(scs_inference,[],[33,4,17])). % 63.11/63.19 cnf(893,plain, % 63.11/63.19 (E(f1(f4(f8(x8931),f8(f1(f1(x8932))))),f1(f4(f8(f1(x8931)),f8(x8932))))), % 63.11/63.19 inference(scs_inference,[],[888,844,2,3])). % 63.11/63.19 cnf(895,plain, % 63.11/63.19 (E(f1(f3(x8951,f8(x8952),x8953)),f1(f3(x8951,f8(f1(x8952)),x8953)))), % 63.11/63.19 inference(scs_inference,[],[33,4,18])). % 63.11/63.19 cnf(897,plain, % 63.11/63.19 (E(f1(f3(f8(x8971),x8972,f8(x8973))),f1(f3(f8(f1(x8971)),x8972,f8(f1(x8973)))))), % 63.11/63.19 inference(scs_inference,[],[893,866,891,2,3])). % 63.11/63.19 cnf(901,plain, % 63.11/63.19 (E(f1(f12(f8(f1(x9011)),f8(f1(x9012)))),f1(f12(f8(x9011),f8(x9012))))), % 63.11/63.19 inference(scs_inference,[],[883,2])). % 63.11/63.19 cnf(906,plain, % 63.11/63.19 (E(f1(f3(x9061,f8(f1(x9062)),x9063)),f1(f3(x9061,f8(x9062),x9063)))), % 63.11/63.19 inference(scs_inference,[],[895,2])). % 63.11/63.19 cnf(907,plain, % 63.11/63.19 (E(f1(f12(f8(x9071),f8(f1(x9072)))),f1(f12(f8(x9071),f8(x9072))))), % 63.11/63.19 inference(scs_inference,[],[901,895,876,2,3])). % 63.11/63.19 cnf(910,plain, % 63.11/63.19 (E(f1(f3(f8(f1(x9101)),x9102,f8(f1(x9103)))),f1(f3(f8(x9101),x9102,f8(x9103))))), % 63.11/63.19 inference(scs_inference,[],[897,2])). % 63.11/63.19 cnf(911,plain, % 63.11/63.19 (E(f1(f3(f8(x9111),f8(f1(x9112)),f8(x9113))),f1(f3(f8(f1(x9111)),f8(x9112),f8(f1(x9113)))))), % 63.11/63.19 inference(scs_inference,[],[906,897,2,3])). % 63.11/63.19 cnf(914,plain, % 63.11/63.19 (E(f6(f8(f8(x9141)),x9142),f6(f8(f8(f1(x9141))),x9142))), % 63.11/63.19 inference(scs_inference,[],[33,5,6])). % 63.11/63.19 cnf(915,plain, % 63.11/63.19 (E(f1(f3(f8(f1(x9151)),f8(x9152),f8(f1(x9153)))),f1(f3(f8(x9151),f8(f1(x9152)),f8(x9153))))), % 63.11/63.19 inference(scs_inference,[],[911,2])). % 63.11/63.19 cnf(916,plain, % 63.11/63.19 (E(f1(f12(f8(f1(x9161)),f8(f1(f1(x9162))))),f1(f12(f8(x9161),f8(x9162))))), % 63.11/63.19 inference(scs_inference,[],[907,911,901,2,3])). % 63.11/63.19 cnf(919,plain, % 63.11/63.19 (E(f8(f6(x9191,f8(x9192))),f8(f6(x9191,f8(f1(x9192)))))), % 63.11/63.19 inference(scs_inference,[],[33,5,7])). % 63.11/63.19 cnf(921,plain, % 63.11/63.19 (E(f1(f3(f8(f1(f1(x9211))),f8(x9212),f8(f1(f1(x9213))))),f1(f3(f8(x9211),f8(f1(x9212)),f8(x9213))))), % 63.11/63.19 inference(scs_inference,[],[910,915,916,2,3])). % 63.11/63.19 cnf(924,plain, % 63.11/63.19 (E(f14(f8(f8(x9241))),f14(f8(f8(f1(x9241)))))), % 63.11/63.19 inference(scs_inference,[],[33,5,8])). % 63.11/63.19 cnf(926,plain, % 63.11/63.19 (E(f8(f6(f1(f8(x9261)),f8(x9262))),f8(f6(f1(f8(f1(x9261))),f8(f1(x9262)))))), % 63.11/63.19 inference(scs_inference,[],[42,921,919,2,3])). % 63.11/63.19 cnf(929,plain, % 63.11/63.19 (E(f8(f9(f8(x9291))),f8(f9(f8(f1(x9291)))))), % 63.11/63.19 inference(scs_inference,[],[33,5,9])). % 63.11/63.19 cnf(931,plain, % 63.11/63.19 (E(f14(f8(f1(f8(x9311)))),f14(f8(f8(f1(x9311)))))), % 63.11/63.19 inference(scs_inference,[],[371,914,924,2,3])). % 63.11/63.19 cnf(933,plain, % 63.11/63.19 (E(f10(f8(f8(x9331))),f10(f8(f8(f1(x9331)))))), % 63.11/63.19 inference(scs_inference,[],[33,5,10])). % 63.11/63.19 cnf(934,plain, % 63.11/63.19 (E(f8(f6(f1(f8(f1(x9341))),f8(f1(x9342)))),f8(f6(f1(f8(x9341)),f8(x9342))))), % 63.11/63.19 inference(scs_inference,[],[926,2])). % 63.11/63.19 cnf(935,plain, % 63.11/63.19 (E(f8(f1(f9(f8(x9351)))),f8(f9(f8(f1(x9351)))))), % 63.11/63.19 inference(scs_inference,[],[24,926,929,2,3])). % 63.11/63.19 cnf(937,plain, % 63.11/63.19 (E(f8(f12(f8(x9371),x9372)),f8(f12(f8(f1(x9371)),x9372)))), % 63.11/63.19 inference(scs_inference,[],[33,5,11])). % 63.11/63.19 cnf(938,plain, % 63.11/63.19 (E(f14(f8(f8(f1(x9381)))),f14(f8(f1(f8(x9381)))))), % 63.11/63.19 inference(scs_inference,[],[931,2])). % 63.11/63.19 cnf(939,plain, % 63.11/63.19 (E(f8(f6(f1(f8(f1(f1(x9391)))),f8(f1(x9392)))),f8(f6(f1(f8(x9391)),f8(x9392))))), % 63.11/63.19 inference(scs_inference,[],[43,934,931,2,3])). % 63.11/63.19 cnf(941,plain, % 63.11/63.19 (E(f12(x9411,f8(f8(x9412))),f12(x9411,f8(f8(f1(x9412)))))), % 63.11/63.19 inference(scs_inference,[],[33,5,12])). % 63.11/63.19 cnf(943,plain, % 63.11/63.19 (E(f10(f8(f1(f8(x9431)))),f10(f8(f8(f1(x9431)))))), % 63.11/63.19 inference(scs_inference,[],[297,939,933,2,3])). % 63.11/63.19 cnf(945,plain, % 63.11/63.19 (E(f8(f4(f8(x9451),x9452)),f8(f4(f8(f1(x9451)),x9452)))), % 63.11/63.19 inference(scs_inference,[],[33,5,13])). % 63.11/63.19 cnf(946,plain, % 63.11/63.19 (E(f8(f9(f8(f1(x9461)))),f8(f1(f9(f8(x9461)))))), % 63.11/63.19 inference(scs_inference,[],[935,2])). % 63.11/63.19 cnf(947,plain, % 63.11/63.19 (E(f8(f1(f12(f8(x9471),x9472))),f8(f12(f8(f1(x9471)),x9472)))), % 63.11/63.19 inference(scs_inference,[],[24,935,937,2,3])). % 63.11/63.19 cnf(949,plain, % 63.11/63.19 (E(f4(x9491,f8(f8(x9492))),f4(x9491,f8(f8(f1(x9492)))))), % 63.11/63.19 inference(scs_inference,[],[33,5,14])). % 63.11/63.19 cnf(950,plain, % 63.11/63.19 (E(f12(x9501,f8(f8(f1(x9502)))),f12(x9501,f8(f8(x9502))))), % 63.11/63.19 inference(scs_inference,[],[941,2])). % 63.11/63.19 cnf(951,plain, % 63.11/63.19 (E(f14(f8(f1(f8(f1(x9511))))),f14(f8(f1(f8(x9511)))))), % 63.11/63.19 inference(scs_inference,[],[938,941,371,2,3])). % 63.11/63.19 cnf(953,plain, % 63.11/63.19 (E(f8(f11(f8(x9531),x9532)),f8(f11(f8(f1(x9531)),x9532)))), % 63.11/63.19 inference(scs_inference,[],[33,5,15])). % 63.11/63.19 cnf(955,plain, % 63.11/63.19 (E(f10(f8(f1(f1(f8(x9551))))),f10(f8(f8(f1(x9551)))))), % 63.11/63.19 inference(scs_inference,[],[943,297,2,3])). % 63.11/63.19 cnf(957,plain, % 63.11/63.19 (E(f11(x9571,f8(f8(x9572))),f11(x9571,f8(f8(f1(x9572)))))), % 63.11/63.19 inference(scs_inference,[],[33,5,16])). % 63.11/63.20 cnf(958,plain, % 63.11/63.20 (E(f8(f4(f8(f1(x9581)),x9582)),f8(f4(f8(x9581),x9582)))), % 63.11/63.20 inference(scs_inference,[],[945,2])). % 63.11/63.20 cnf(959,plain, % 63.11/63.20 (E(f8(f1(f4(f8(x9591),x9592))),f8(f4(f8(f1(x9591)),x9592)))), % 63.11/63.20 inference(scs_inference,[],[24,945,2,3])). % 63.11/63.20 cnf(961,plain, % 63.11/63.20 (E(f8(f3(f8(x9611),x9612,x9613)),f8(f3(f8(f1(x9611)),x9612,x9613)))), % 63.11/63.20 inference(scs_inference,[],[33,5,17])). % 63.11/63.20 cnf(962,plain, % 63.11/63.20 (E(f8(f12(f8(f1(x9621)),x9622)),f8(f1(f12(f8(x9621),x9622))))), % 63.11/63.20 inference(scs_inference,[],[947,2])). % 63.11/63.20 cnf(963,plain, % 63.11/63.20 (E(f8(f1(f4(f8(f1(x9631)),x9632))),f8(f4(f8(x9631),x9632)))), % 63.11/63.20 inference(scs_inference,[],[24,958,947,2,3])). % 63.11/63.20 cnf(965,plain, % 63.11/63.20 (E(f3(x9651,f8(f8(x9652)),x9653),f3(x9651,f8(f8(f1(x9652))),x9653))), % 63.11/63.20 inference(scs_inference,[],[33,5,18])). % 63.11/63.20 cnf(967,plain, % 63.11/63.20 (E(f8(f1(f9(f8(f1(x9671))))),f8(f1(f9(f8(x9671)))))), % 63.11/63.20 inference(scs_inference,[],[24,963,946,2,3])). % 63.11/63.20 cnf(969,plain, % 63.11/63.20 (E(f8(f3(x9691,x9692,f8(x9693))),f8(f3(x9691,x9692,f8(f1(x9693)))))), % 63.11/63.20 inference(scs_inference,[],[33,5,19])). % 63.11/63.20 cnf(970,plain, % 63.11/63.20 (E(f4(x9701,f8(f8(f1(x9702)))),f4(x9701,f8(f8(x9702))))), % 63.11/63.20 inference(scs_inference,[],[949,2])). % 63.11/63.20 cnf(971,plain, % 63.11/63.20 (E(f8(f1(f11(f8(x9711),x9712))),f8(f11(f8(f1(x9711)),x9712)))), % 63.11/63.20 inference(scs_inference,[],[24,949,953,2,3])). % 63.11/63.20 cnf(973,plain, % 63.11/63.20 (E(f5(f8(f8(x9731))),f5(f8(f8(f1(x9731)))))), % 63.11/63.20 inference(scs_inference,[],[33,5,20])). % 63.11/63.20 cnf(975,plain, % 63.11/63.20 (E(f8(f1(f3(f8(x9751),x9752,x9753))),f8(f3(f8(f1(x9751)),x9752,x9753)))), % 63.11/63.20 inference(scs_inference,[],[24,951,961,2,3])). % 63.11/63.20 cnf(979,plain, % 63.11/63.20 (E(f8(f1(f12(f8(f1(x9791)),x9792))),f8(f1(f12(f8(x9791),x9792))))), % 63.11/63.20 inference(scs_inference,[],[24,955,962,2,3])). % 63.11/63.20 cnf(981,plain, % 63.11/63.20 (E(f6(x9811,f8(f8(x9812))),f6(x9811,f8(f8(f1(x9812)))))), % 63.11/63.20 inference(scs_inference,[],[33,5,7])). % 63.11/63.20 cnf(982,plain, % 63.11/63.20 (E(f11(x9821,f8(f8(f1(x9822)))),f11(x9821,f8(f8(x9822))))), % 63.11/63.20 inference(scs_inference,[],[957,2])). % 63.11/63.20 cnf(983,plain, % 63.11/63.20 (E(f8(f1(f3(x9831,x9832,f8(x9833)))),f8(f3(x9831,x9832,f8(f1(x9833)))))), % 63.11/63.20 inference(scs_inference,[],[24,957,969,2,3])). % 63.11/63.20 cnf(987,plain, % 63.11/63.20 (E(f5(f8(f1(f8(x9871)))),f5(f8(f8(f1(x9871)))))), % 63.11/63.20 inference(scs_inference,[],[348,959,973,2,3])). % 63.11/63.20 cnf(989,plain, % 63.11/63.20 (E(f9(f8(f8(x9891))),f9(f8(f8(f1(x9891)))))), % 63.11/63.20 inference(scs_inference,[],[33,5,9])). % 63.11/63.20 cnf(990,plain, % 63.11/63.20 (E(f3(x9901,f8(f8(f1(x9902))),x9903),f3(x9901,f8(f8(x9902)),x9903))), % 63.11/63.20 inference(scs_inference,[],[965,2])). % 63.11/63.20 cnf(995,plain, % 63.11/63.20 (E(f5(f8(f1(f1(f8(x9951))))),f5(f8(f8(f1(x9951)))))), % 63.11/63.20 inference(scs_inference,[],[967,987,348,2,3])). % 63.11/63.20 cnf(997,plain, % 63.11/63.20 (E(f12(f8(f8(x9971)),x9972),f12(f8(f8(f1(x9971))),x9972))), % 63.11/63.20 inference(scs_inference,[],[33,5,11])). % 63.11/63.20 cnf(999,plain, % 63.11/63.20 (E(f12(f8(f8(x9991)),f8(f8(f1(x9992)))),f12(f8(f8(f1(x9991))),f8(f8(x9992))))), % 63.11/63.20 inference(scs_inference,[],[950,971,997,2,3])). % 63.11/63.20 cnf(1002,plain, % 63.11/63.20 (E(f8(f14(f8(x10021))),f8(f14(f8(f1(x10021)))))), % 63.11/63.20 inference(scs_inference,[],[33,5,8])). % 63.11/63.20 cnf(1004,plain, % 63.11/63.20 (E(f9(f8(f1(f8(x10041)))),f9(f8(f8(f1(x10041)))))), % 63.11/63.20 inference(scs_inference,[],[375,999,989,2,3])). % 63.11/63.20 cnf(1010,plain, % 63.11/63.20 (E(f8(f10(f8(x10101))),f8(f10(f8(f1(x10101)))))), % 63.11/63.20 inference(scs_inference,[],[33,5,10])). % 63.11/63.20 cnf(1011,plain, % 63.11/63.20 (E(f8(f1(f12(f8(x10111),x10112))),f8(f1(f12(f8(f1(x10111)),x10112))))), % 63.11/63.20 inference(scs_inference,[],[979,2])). % 63.11/63.20 cnf(1014,plain, % 63.11/63.20 (E(f11(f8(f8(x10141)),x10142),f11(f8(f8(f1(x10141))),x10142))), % 63.11/63.20 inference(scs_inference,[],[33,5,15])). % 63.11/63.20 cnf(1016,plain, % 63.11/63.20 (E(f8(f1(f14(f8(x10161)))),f8(f14(f8(f1(x10161)))))), % 63.11/63.20 inference(scs_inference,[],[24,981,1002,2,3])). % 63.11/63.20 cnf(1019,plain, % 63.11/63.20 (E(f8(f3(x10191,x10192,f8(f1(x10193)))),f8(f1(f3(x10191,x10192,f8(x10193)))))), % 63.11/63.20 inference(scs_inference,[],[983,2])). % 63.11/63.20 cnf(1020,plain, % 63.11/63.20 (E(f9(f8(f1(f1(f8(x10201))))),f9(f8(f8(f1(x10201)))))), % 63.11/63.20 inference(scs_inference,[],[983,1004,375,2,3])). % 63.11/63.20 cnf(1022,plain, % 63.11/63.20 (E(f3(f8(f8(x10221)),x10222,x10223),f3(f8(f8(f1(x10221))),x10222,x10223))), % 63.11/63.20 inference(scs_inference,[],[33,5,17])). % 63.11/63.20 cnf(1027,plain, % 63.11/63.20 (E(f8(f4(x10271,f8(x10272))),f8(f4(x10271,f8(f1(x10272)))))), % 63.11/63.20 inference(scs_inference,[],[33,5,14])). % 63.11/63.20 cnf(1033,plain, % 63.11/63.20 (E(f8(f1(f10(f8(x10331)))),f8(f10(f8(f1(x10331)))))), % 63.11/63.20 inference(scs_inference,[],[24,995,1010,2,3])). % 63.11/63.20 cnf(1035,plain, % 63.11/63.20 (E(f8(f11(x10351,f8(x10352))),f8(f11(x10351,f8(f1(x10352)))))), % 63.11/63.20 inference(scs_inference,[],[33,5,16])). % 63.11/63.20 cnf(1050,plain, % 63.11/63.20 (E(f8(f14(f8(f1(x10501)))),f8(f1(f14(f8(x10501)))))), % 63.11/63.20 inference(scs_inference,[],[1016,2])). % 63.11/63.20 cnf(1051,plain, % 63.11/63.20 (E(f8(f1(f3(x10511,x10512,f8(f1(x10513))))),f8(f1(f3(x10511,x10512,f8(x10513)))))), % 63.11/63.20 inference(scs_inference,[],[24,1016,1019,2,3])). % 63.11/63.20 cnf(1055,plain, % 63.11/63.20 (E(f3(f8(f8(x10551)),f3(x10552,x10553,f8(x10554)),x10555),f3(f8(f8(f1(x10551))),f3(x10552,x10553,f8(f1(x10554))),x10555))), % 63.11/63.20 inference(scs_inference,[],[74,1020,1022,2,3])). % 63.11/63.20 cnf(1060,plain, % 63.11/63.20 (E(f8(f1(f4(x10601,f8(x10602)))),f8(f4(x10601,f8(f1(x10602)))))), % 63.11/63.20 inference(scs_inference,[],[24,1027,2,3])). % 63.11/63.20 cnf(1076,plain, % 63.11/63.20 (E(f8(f10(f8(f1(x10761)))),f8(f1(f10(f8(x10761)))))), % 63.11/63.20 inference(scs_inference,[],[1033,2])). % 63.11/63.20 cnf(1080,plain, % 63.11/63.20 (E(f8(f3(x10801,f8(x10802),x10803)),f8(f3(x10801,f8(f1(x10802)),x10803)))), % 63.11/63.20 inference(scs_inference,[],[33,5,18])). % 63.11/63.20 cnf(1082,plain, % 63.11/63.20 (E(f8(f1(f11(x10821,f8(x10822)))),f8(f11(x10821,f8(f1(x10822)))))), % 63.11/63.20 inference(scs_inference,[],[24,1035,2,3])). % 63.11/63.20 cnf(1084,plain, % 63.11/63.20 (~P1(x10841,f8(f8(x10842)),x10843)+P1(x10841,f8(f8(f1(x10842))),x10843)), % 63.11/63.20 inference(scs_inference,[],[33,5,22])). % 63.11/63.20 cnf(1088,plain, % 63.11/63.20 (~P1(x10881,f8(f8(x10882)),a16)+P1(x10881,f8(f8(f8(f1(x10882)))),a16)), % 63.11/63.20 inference(scs_inference,[],[1084,27])). % 63.11/63.20 cnf(1093,plain, % 63.11/63.20 (~P1(f12(x10931,x10932),f8(f8(x10933)),a16)+P1(x10932,f8(f8(f8(f1(x10933)))),a16)), % 63.11/63.20 inference(scs_inference,[],[1088,29])). % 63.11/63.20 cnf(1104,plain, % 63.11/63.20 (E(f8(f1(f14(f8(f1(x11041))))),f8(f1(f14(f8(x11041)))))), % 63.11/63.20 inference(scs_inference,[],[24,1050,1051,2,3])). % 63.11/63.20 cnf(1107,plain, % 63.11/63.20 (E(f3(f8(f8(f1(x11071))),f3(x11072,x11073,f8(f1(x11074))),x11075),f3(f8(f8(x11071)),f3(x11072,x11073,f8(x11074)),x11075))), % 63.11/63.20 inference(scs_inference,[],[1055,2])). % 63.11/63.20 cnf(1117,plain, % 63.11/63.20 (E(f8(f3(x11171,f8(f1(x11172)),x11173)),f8(f3(x11171,f8(x11172),x11173)))), % 63.11/63.20 inference(scs_inference,[],[1080,2])). % 63.11/63.20 cnf(1118,plain, % 63.11/63.20 (E(f1(f8(f1(f1(f1(x11181))))),f1(f8(x11181)))), % 63.11/63.20 inference(scs_inference,[],[40,867,1080,2,3])). % 63.11/63.20 cnf(1121,plain, % 63.11/63.20 (E(f3(f8(f8(f1(x11211))),f3(x11212,x11213,f8(f1(f1(x11214)))),x11215),f3(f8(f8(x11211)),f3(x11212,x11213,f8(x11214)),x11215))), % 63.11/63.20 inference(scs_inference,[],[73,1118,1107,2,3])). % 63.11/63.20 cnf(1124,plain, % 63.11/63.20 (E(f8(f5(f8(x11241))),f8(f5(f8(f1(x11241)))))), % 63.11/63.20 inference(scs_inference,[],[33,5,20])). % 63.11/63.20 cnf(1126,plain, % 63.11/63.20 (E(f8(f1(f3(x11261,f8(f1(x11262)),x11263))),f8(f3(x11261,f8(x11262),x11263)))), % 63.11/63.20 inference(scs_inference,[],[24,1117,1121,2,3])). % 63.11/63.20 cnf(1130,plain, % 63.11/63.20 (E(f8(f1(f10(f8(f1(x11301))))),f8(f1(f10(f8(x11301)))))), % 63.11/63.20 inference(scs_inference,[],[24,1126,1076,2,3])). % 63.11/63.20 cnf(1133,plain, % 63.11/63.20 (E(f8(f11(x11331,f8(f1(x11332)))),f8(f1(f11(x11331,f8(x11332)))))), % 63.11/63.20 inference(scs_inference,[],[1082,2])). % 63.11/63.20 cnf(1142,plain, % 63.11/63.20 (E(f8(f1(f5(f8(x11421)))),f8(f5(f8(f1(x11421)))))), % 63.11/63.20 inference(scs_inference,[],[24,1104,1124,2,3])). % 63.11/63.20 cnf(1146,plain, % 63.11/63.20 (E(f8(f1(f11(x11461,f8(f1(x11462))))),f8(f1(f11(x11461,f8(x11462)))))), % 63.11/63.20 inference(scs_inference,[],[24,1130,1133,2,3])). % 63.11/63.20 cnf(1156,plain, % 63.11/63.20 (E(f8(f5(f8(f1(x11561)))),f8(f1(f5(f8(x11561)))))), % 63.11/63.20 inference(scs_inference,[],[1142,2])). % 63.11/63.20 cnf(1161,plain, % 63.11/63.20 (E(f8(f1(f5(f8(f1(x11611))))),f8(f1(f5(f8(x11611)))))), % 63.11/63.20 inference(scs_inference,[],[24,1146,1156,2,3])). % 63.11/63.20 cnf(1164,plain, % 63.11/63.20 (E(f8(f12(f8(x11641),x11642)),f8(f1(f12(f8(f1(x11641)),x11642))))), % 63.11/63.20 inference(scs_inference,[],[33,1161,1011,2,3])). % 63.11/63.20 cnf(1207,plain, % 63.11/63.20 (E(f14(f11(x12071,f8(x12072))),f14(f11(x12071,f8(f1(x12072)))))), % 63.11/63.20 inference(scs_inference,[],[33,8,16])). % 63.11/63.20 cnf(1212,plain, % 63.11/63.20 (E(f3(f14(f8(x12121)),x12122,x12123),f3(f14(f8(f1(x12121))),x12122,x12123))), % 63.11/63.20 inference(scs_inference,[],[33,8,17])). % 63.11/63.20 cnf(1217,plain, % 63.11/63.20 (E(f14(f3(x12171,f8(x12172),x12173)),f14(f3(x12171,f8(f1(x12172)),x12173)))), % 63.11/63.20 inference(scs_inference,[],[33,8,18])). % 63.11/63.20 cnf(1218,plain, % 63.11/63.20 (E(f14(f11(x12181,f8(f1(x12182)))),f14(f11(x12181,f8(x12182))))), % 63.11/63.20 inference(scs_inference,[],[1207,2])). % 63.11/63.20 cnf(1219,plain, % 63.11/63.20 (E(f3(f14(f8(x12191)),f3(x12192,x12193,f8(x12194)),x12195),f3(f14(f8(f1(x12191))),f3(x12192,x12193,f8(f1(x12194))),x12195))), % 63.11/63.20 inference(scs_inference,[],[74,1207,1212,2,3])). % 63.11/63.20 cnf(1223,plain, % 63.11/63.20 (E(f14(f3(x12231,f8(f1(x12232)),x12233)),f14(f3(x12231,f8(x12232),x12233)))), % 63.11/63.20 inference(scs_inference,[],[1217,2])). % 63.11/63.20 cnf(1228,plain, % 63.11/63.20 (E(f3(f14(f8(f1(x12281))),f3(x12282,x12283,f8(f1(x12284))),x12285),f3(f14(f8(x12281)),f3(x12282,x12283,f8(x12284)),x12285))), % 63.11/63.20 inference(scs_inference,[],[1219,2])). % 63.11/63.20 cnf(1247,plain, % 63.11/63.20 (E(f14(f6(f8(x12471),x12472)),f14(f6(f8(f1(x12471)),x12472)))), % 63.11/63.20 inference(scs_inference,[],[33,8,6])). % 63.11/63.20 cnf(1267,plain, % 63.11/63.20 (E(f14(f12(f8(x12671),x12672)),f14(f12(f8(f1(x12671)),x12672)))), % 63.11/63.20 inference(scs_inference,[],[33,8,11])). % 63.11/63.20 cnf(1272,plain, % 63.11/63.20 (E(f4(x12721,f14(f8(x12722))),f4(x12721,f14(f8(f1(x12722)))))), % 63.11/63.20 inference(scs_inference,[],[33,8,14])). % 63.11/63.20 cnf(1276,plain, % 63.11/63.20 (E(f14(f4(f8(x12761),x12762)),f14(f4(f8(f1(x12761)),x12762)))), % 63.11/63.20 inference(scs_inference,[],[33,8,13])). % 63.11/63.20 cnf(1281,plain, % 63.11/63.20 (E(f11(x12811,f14(f8(x12812))),f11(x12811,f14(f8(f1(x12812)))))), % 63.11/63.20 inference(scs_inference,[],[33,8,16])). % 63.11/63.20 cnf(1285,plain, % 63.11/63.20 (E(f14(f1(f1(f8(f1(x12851))))),f14(f1(f1(f8(x12851)))))), % 63.11/63.20 inference(scs_inference,[],[40,8,4])). % 63.11/63.20 cnf(1290,plain, % 63.11/63.20 (E(f8(f14(f1(f8(f1(x12901))))),f8(f14(f1(f8(x12901)))))), % 63.11/63.20 inference(scs_inference,[],[40,8,5])). % 63.11/63.20 cnf(1291,plain, % 63.11/63.20 (E(f4(x12911,f14(f8(f1(x12912)))),f4(x12911,f14(f8(x12912))))), % 63.11/63.20 inference(scs_inference,[],[1272,2])). % 63.11/63.20 cnf(1292,plain, % 63.11/63.20 (E(f4(f1(f8(x12921)),f14(f8(x12922))),f4(f1(f8(f1(x12921))),f14(f8(f1(x12922)))))), % 63.11/63.20 inference(scs_inference,[],[1272,833,2,3])). % 63.11/63.20 cnf(1295,plain, % 63.11/63.20 (E(f14(f11(f1(f8(f1(x12951))),x12952)),f14(f11(f1(f8(x12951)),x12952)))), % 63.11/63.20 inference(scs_inference,[],[40,8,15])). % 63.11/63.20 cnf(1296,plain, % 63.11/63.20 (E(f11(x12961,f14(f8(f1(x12962)))),f11(x12961,f14(f8(x12962))))), % 63.11/63.20 inference(scs_inference,[],[1281,2])). % 63.11/63.20 cnf(1297,plain, % 63.11/63.20 (E(f14(f11(f1(f8(f1(x12971))),f8(f1(x12972)))),f14(f11(f1(f8(x12971)),f8(x12972))))), % 63.11/63.20 inference(scs_inference,[],[1218,1281,1295,2,3])). % 63.11/63.20 cnf(1300,plain, % 63.11/63.20 (E(f1(f14(f1(f8(f1(x13001))))),f1(f14(f1(f8(x13001)))))), % 63.11/63.20 inference(scs_inference,[],[40,8,4])). % 63.11/63.20 cnf(1301,plain, % 63.11/63.20 (E(f14(f11(f1(f8(x13011)),f8(x13012))),f14(f11(f1(f8(f1(x13011))),f8(f1(x13012)))))), % 63.11/63.20 inference(scs_inference,[],[1297,2])). % 63.11/63.20 cnf(1302,plain, % 63.11/63.20 (E(f11(f8(f8(x13021)),f14(f8(f1(x13022)))),f11(f8(f8(f1(x13021))),f14(f8(x13022))))), % 63.11/63.20 inference(scs_inference,[],[1296,1297,1014,2,3])). % 63.11/63.20 cnf(1305,plain, % 63.11/63.20 (E(f14(f3(f1(f8(f1(x13051))),x13052,x13053)),f14(f3(f1(f8(x13051)),x13052,x13053)))), % 63.11/63.20 inference(scs_inference,[],[40,8,17])). % 63.11/63.20 cnf(1306,plain, % 63.11/63.20 (E(f11(f8(f8(f1(x13061))),f14(f8(x13062))),f11(f8(f8(x13061)),f14(f8(f1(x13062)))))), % 63.11/63.20 inference(scs_inference,[],[1302,2])). % 63.11/63.20 cnf(1307,plain, % 63.11/63.20 (E(f14(f3(f1(f8(f1(x13071))),f8(f1(x13072)),x13073)),f14(f3(f1(f8(x13071)),f8(x13072),x13073)))), % 63.11/63.20 inference(scs_inference,[],[1223,1302,1305,2,3])). % 63.11/63.20 cnf(1311,plain, % 63.11/63.20 (E(f14(f3(f1(f8(x13111)),f8(x13112),x13113)),f14(f3(f1(f8(f1(x13111))),f8(f1(x13112)),x13113)))), % 63.11/63.20 inference(scs_inference,[],[1307,2])). % 63.11/63.20 cnf(1312,plain, % 63.11/63.20 (E(f14(f3(f1(f8(f1(x13121))),f8(f1(f1(x13122))),x13123)),f14(f3(f1(f8(x13121)),f8(x13122),x13123)))), % 63.11/63.20 inference(scs_inference,[],[1307,1223,2,3])). % 63.11/63.20 cnf(1315,plain, % 63.11/63.20 (E(f14(f3(x13151,x13152,f1(f8(f1(x13153))))),f14(f3(x13151,x13152,f1(f8(x13153)))))), % 63.11/63.20 inference(scs_inference,[],[40,8,19])). % 63.11/63.20 cnf(1316,plain, % 63.11/63.20 (E(f14(f3(f1(f8(x13161)),f8(x13162),x13163)),f14(f3(f1(f8(f1(x13161))),f8(f1(f1(x13162))),x13163)))), % 63.11/63.20 inference(scs_inference,[],[1312,2])). % 63.11/63.20 cnf(1322,plain, % 63.11/63.20 (E(f14(f11(f1(f8(x13221)),f8(f1(x13222)))),f14(f11(f1(f8(f1(x13221))),f8(f1(x13222)))))), % 63.11/63.20 inference(scs_inference,[],[1285,1301,1218,2,3])). % 63.11/63.20 cnf(1327,plain, % 63.11/63.20 (E(f11(f8(f8(f1(x13271))),f14(f8(f1(x13272)))),f11(f8(f8(x13271)),f14(f8(f1(x13272)))))), % 63.11/63.20 inference(scs_inference,[],[1290,1306,1296,2,3])). % 63.11/63.20 cnf(1330,plain, % 63.11/63.20 (E(f6(f14(f1(f8(f1(x13301)))),x13302),f6(f14(f1(f8(x13301))),x13302))), % 63.11/63.20 inference(scs_inference,[],[40,8,6])). % 63.11/63.20 cnf(1331,plain, % 63.11/63.20 (E(f4(f1(f8(f1(x13311))),f14(f8(f1(x13312)))),f4(f1(f8(x13311)),f14(f8(x13312))))), % 63.11/63.20 inference(scs_inference,[],[1292,2])). % 63.11/63.20 cnf(1334,plain, % 63.11/63.20 (E(f14(f6(x13341,f1(f8(f1(x13342))))),f14(f6(x13341,f1(f8(x13342)))))), % 63.11/63.20 inference(scs_inference,[],[40,8,7])). % 63.11/63.20 cnf(1336,plain, % 63.11/63.20 (E(f4(f1(f8(f1(x13361))),f14(f8(f1(f1(x13362))))),f4(f1(f8(x13361)),f14(f8(x13362))))), % 63.11/63.20 inference(scs_inference,[],[1291,1331,1300,2,3])). % 63.11/63.20 cnf(1341,plain, % 63.11/63.20 (E(f14(f6(f8(x13411),f1(f8(f1(x13412))))),f14(f6(f8(f1(x13411)),f1(f8(x13412)))))), % 63.11/63.20 inference(scs_inference,[],[1336,1334,1247,2,3])). % 63.11/63.20 cnf(1353,plain, % 63.11/63.20 (E(f14(f12(x13531,f1(f8(f1(x13532))))),f14(f12(x13531,f1(f8(x13532)))))), % 63.11/63.20 inference(scs_inference,[],[40,8,12])). % 63.11/63.20 cnf(1355,plain, % 63.11/63.20 (E(f14(f12(f8(x13551),f1(f8(f1(x13552))))),f14(f12(f8(f1(x13551)),f1(f8(x13552)))))), % 63.11/63.20 inference(scs_inference,[],[1315,1353,1267,2,3])). % 63.11/63.20 cnf(1363,plain, % 63.11/63.20 (E(f14(f4(x13631,f1(f8(f1(x13632))))),f14(f4(x13631,f1(f8(x13632)))))), % 63.11/63.20 inference(scs_inference,[],[40,8,14])). % 63.11/63.20 cnf(1365,plain, % 63.11/63.20 (E(f14(f4(f8(x13651),f1(f8(f1(x13652))))),f14(f4(f8(f1(x13651)),f1(f8(x13652)))))), % 63.11/63.20 inference(scs_inference,[],[1330,1363,1276,2,3])). % 63.11/63.20 cnf(1373,plain, % 63.11/63.20 (E(f14(f6(f8(f1(x13731)),f1(f8(x13732)))),f14(f6(f8(x13731),f1(f8(f1(x13732))))))), % 63.11/63.20 inference(scs_inference,[],[1341,2])). % 63.11/63.20 cnf(1396,plain, % 63.11/63.20 (E(f6(x13961,f14(f1(f8(f1(x13962))))),f6(x13961,f14(f1(f8(x13962)))))), % 63.11/63.20 inference(scs_inference,[],[40,8,7])). % 63.11/63.20 cnf(1397,plain, % 63.11/63.20 (E(f14(f12(f8(f1(x13971)),f1(f8(x13972)))),f14(f12(f8(x13971),f1(f8(f1(x13972))))))), % 63.11/63.20 inference(scs_inference,[],[1355,2])). % 63.11/63.20 cnf(1407,plain, % 63.11/63.20 (E(f14(f4(f8(f1(x14071)),f1(f8(x14072)))),f14(f4(f8(x14071),f1(f8(f1(x14072))))))), % 63.11/63.20 inference(scs_inference,[],[1365,2])). % 63.11/63.20 cnf(1411,plain, % 63.11/63.20 (E(f14(f9(f1(f8(f1(x14111))))),f14(f9(f1(f8(x14111)))))), % 63.11/63.20 inference(scs_inference,[],[40,8,9])). % 63.11/63.20 cnf(1449,plain, % 63.11/63.20 (E(f3(f14(f8(f1(x14491))),f3(x14492,x14493,f8(x14494)),x14495),f3(f14(f8(x14491)),f3(x14492,x14493,f8(x14494)),x14495))), % 63.11/63.20 inference(scs_inference,[],[74,1396,1228,2,3])). % 63.11/63.20 cnf(1459,plain, % 63.11/63.20 (E(f3(f14(f8(f1(x14591))),f3(x14592,x14593,f8(x14594)),x14595),f3(f14(f8(x14591)),f3(x14592,x14593,f8(f1(x14594))),x14595))), % 63.11/63.20 inference(scs_inference,[],[74,1449,1411,2,3])). % 63.11/63.20 cnf(1462,plain, % 63.11/63.20 (E(f9(f6(x14621,f1(f8(f1(x14622))))),f9(f6(x14621,f1(f8(x14622)))))), % 63.11/63.20 inference(scs_inference,[],[40,9,7])). % 63.11/63.20 cnf(1475,plain, % 63.11/63.20 (E(f12(x14751,f9(f1(f8(f1(x14752))))),f12(x14751,f9(f1(f8(x14752)))))), % 63.11/63.20 inference(scs_inference,[],[40,9,12])). % 63.11/63.20 cnf(1502,plain, % 63.11/63.20 (E(f3(f14(f8(x15021)),f3(x15022,x15023,f8(f1(x15024))),x15025),f3(f14(f8(f1(x15021))),f3(x15022,x15023,f8(x15024)),x15025))), % 63.11/63.20 inference(scs_inference,[],[1459,2])). % 63.11/63.20 cnf(1507,plain, % 63.11/63.20 (E(f3(f14(f8(x15071)),f3(x15072,x15073,f8(f1(f1(x15074)))),x15075),f3(f14(f8(f1(x15071))),f3(x15072,x15073,f8(x15074)),x15075))), % 63.11/63.20 inference(scs_inference,[],[73,1502,1462,2,3])). % 63.11/63.20 cnf(1512,plain, % 63.11/63.20 (E(f8(f1(f1(f12(f8(x15121),x15122)))),f8(f12(f8(f1(x15121)),x15122)))), % 63.11/63.20 inference(scs_inference,[],[24,1507,947,2,3])). % 63.11/63.20 cnf(1524,plain, % 63.11/63.20 (E(f8(f1(f1(f3(f8(x15241),x15242,x15243)))),f8(f3(f8(f1(x15241)),x15242,x15243)))), % 63.11/63.20 inference(scs_inference,[],[24,1475,975,2,3])). % 63.11/63.20 cnf(1568,plain, % 63.11/63.20 (E(f8(f1(f1(f4(x15681,f8(x15682))))),f8(f4(x15681,f8(f1(x15682)))))), % 63.11/63.20 inference(scs_inference,[],[24,1512,1060,2,3])). % 63.11/63.20 cnf(1570,plain, % 63.11/63.20 (E(f3(f9(f1(f8(f1(x15701)))),x15702,x15703),f3(f9(f1(f8(x15701))),x15702,x15703))), % 63.11/63.20 inference(scs_inference,[],[40,9,17])). % 63.11/63.20 cnf(1574,plain, % 63.11/63.20 (E(f9(f3(x15741,f1(f8(f1(x15742))),x15743)),f9(f3(x15741,f1(f8(x15742)),x15743)))), % 63.11/63.20 inference(scs_inference,[],[40,9,18])). % 63.11/63.20 cnf(1584,plain, % 63.11/63.20 (E(f8(f1(f1(f5(f8(x15841))))),f8(f5(f8(f1(x15841)))))), % 63.11/63.20 inference(scs_inference,[],[24,1524,1142,2,3])). % 63.11/63.20 cnf(1662,plain, % 63.11/63.20 (E(f14(f6(f8(f1(x16621)),f1(f8(x16622)))),f14(f6(f8(x16621),f1(f8(x16622)))))), % 63.11/63.20 inference(scs_inference,[],[1568,1373,1334,2,3])). % 63.11/63.20 cnf(1665,plain, % 63.11/63.20 (E(f14(f12(f8(f1(x16651)),f1(f8(x16652)))),f14(f12(f8(x16651),f1(f8(x16652)))))), % 63.11/63.20 inference(scs_inference,[],[1570,1397,1353,2,3])). % 63.11/63.20 cnf(1669,plain, % 63.11/63.20 (E(f14(f4(f8(f1(x16691)),f1(f8(x16692)))),f14(f4(f8(x16691),f1(f8(x16692)))))), % 63.11/63.20 inference(scs_inference,[],[1574,1407,1363,2,3])). % 63.11/63.20 cnf(1689,plain, % 63.11/63.20 (E(f12(f8(x16891),f8(x16892)),f12(f8(f1(f1(f1(x16891)))),f8(x16892)))), % 63.11/63.20 inference(scs_inference,[],[643,1584,578,2,3])). % 63.11/63.20 cnf(1692,plain, % 63.11/63.20 (E(f12(f8(f1(f1(f1(x16921)))),f8(x16922)),f12(f8(x16921),f8(x16922)))), % 63.11/63.20 inference(scs_inference,[],[1689,2])). % 63.11/63.20 cnf(1693,plain, % 63.11/63.20 (E(f12(f8(x16931),f8(x16932)),f12(f8(f1(f1(f1(f1(f1(x16931)))))),f8(x16932)))), % 63.11/63.20 inference(scs_inference,[],[1689,623,2,3])). % 63.11/63.20 cnf(1696,plain, % 63.11/63.20 (E(f12(f8(f1(f1(f1(x16961)))),f8(x16962)),f12(f8(f1(f1(x16961))),f8(f1(x16962))))), % 63.11/63.20 inference(scs_inference,[],[1692,1693,586,2,3])). % 63.11/63.20 cnf(1699,plain, % 63.11/63.20 (E(f4(f8(f1(x16991)),f8(f1(f1(f1(x16992))))),f4(f8(f1(x16991)),f8(f1(x16992))))), % 63.11/63.20 inference(scs_inference,[],[656,1696,319,2,3])). % 63.11/63.20 cnf(1703,plain, % 63.11/63.20 (E(f3(f8(x17031),f3(x17032,x17033,f8(x17034)),x17035),f3(f8(f1(x17031)),f3(x17032,x17033,f8(f1(x17034))),x17035))), % 63.11/63.20 inference(scs_inference,[],[74,1699,322,2,3])). % 63.11/63.20 cnf(1711,plain, % 63.11/63.20 (E(f10(f6(f1(f8(f1(x17111))),x17112)),f10(f6(f1(f8(x17111)),x17112)))), % 63.11/63.20 inference(scs_inference,[],[40,10,6])). % 63.11/63.20 cnf(1716,plain, % 63.11/63.20 (E(f6(x17161,f10(f1(f8(f1(x17162))))),f6(x17161,f10(f1(f8(x17162)))))), % 63.11/63.20 inference(scs_inference,[],[40,10,7])). % 63.11/63.20 cnf(1721,plain, % 63.11/63.20 (E(f10(f12(f1(f8(f1(x17211))),x17212)),f10(f12(f1(f8(x17211)),x17212)))), % 63.11/63.20 inference(scs_inference,[],[40,10,11])). % 63.11/63.20 cnf(1728,plain, % 63.11/63.20 (E(f3(x17281,f3(x17282,x17283,f8(f1(x17284))),f8(x17285)),f3(x17281,f3(x17282,x17283,f8(x17284)),f8(f1(x17285))))), % 63.11/63.20 inference(scs_inference,[],[73,1711,332,2,3])). % 63.11/63.20 cnf(1732,plain, % 63.11/63.20 (E(f3(x17321,f3(x17322,x17323,f8(x17324)),f8(f1(x17325))),f3(x17321,f3(x17322,x17323,f8(f1(x17324))),f8(x17325)))), % 63.11/63.20 inference(scs_inference,[],[1728,2])). % 63.11/63.20 cnf(1733,plain, % 63.11/63.20 (E(f4(f8(f1(f1(f1(x17331)))),f8(f1(f1(x17332)))),f4(f8(x17331),f8(f1(x17332))))), % 63.11/63.20 inference(scs_inference,[],[659,1728,648,2,3])). % 63.11/63.20 cnf(1736,plain, % 63.11/63.20 (E(f4(f8(x17361),f8(f1(x17362))),f4(f8(f1(f1(f1(x17361)))),f8(f1(f1(x17362)))))), % 63.11/63.20 inference(scs_inference,[],[1733,2])). % 63.11/63.20 cnf(1737,plain, % 63.11/63.20 (E(f3(x17371,f3(x17372,x17373,f8(x17374)),f8(f1(x17375))),f3(x17371,f3(x17372,x17373,f8(f1(f1(x17374)))),f8(x17375)))), % 63.11/63.20 inference(scs_inference,[],[74,1732,1733,2,3])). % 63.11/63.20 cnf(1741,plain, % 63.11/63.20 (E(f3(x17411,f3(x17412,x17413,f8(f1(f1(x17414)))),f8(x17415)),f3(x17411,f3(x17412,x17413,f8(x17414)),f8(f1(x17415))))), % 63.11/63.20 inference(scs_inference,[],[1737,2])). % 63.11/63.20 cnf(1742,plain, % 63.11/63.20 (E(f4(f8(x17421),f8(f1(f1(x17422)))),f4(f8(f1(f1(f1(f1(x17421))))),f8(x17422)))), % 63.11/63.20 inference(scs_inference,[],[1737,1736,656,2,3])). % 63.11/63.20 cnf(1746,plain, % 63.11/63.20 (E(f4(f8(f1(f1(f1(f1(x17461))))),f8(x17462)),f4(f8(x17461),f8(f1(f1(x17462)))))), % 63.11/63.20 inference(scs_inference,[],[1742,2])). % 63.11/63.20 cnf(1747,plain, % 63.11/63.20 (E(f3(x17471,f3(x17472,x17473,f8(f1(f1(f1(x17474))))),f8(x17475)),f3(x17471,f3(x17472,x17473,f8(x17474)),f8(f1(x17475))))), % 63.11/63.20 inference(scs_inference,[],[73,1742,1741,2,3])). % 63.11/63.20 cnf(1750,plain, % 63.11/63.20 (E(f10(f3(f1(f8(f1(x17501))),x17502,x17503)),f10(f3(f1(f8(x17501)),x17502,x17503)))), % 63.11/63.20 inference(scs_inference,[],[40,10,17])). % 63.11/63.20 cnf(1752,plain, % 63.11/63.20 (E(f4(f8(f1(f1(f1(f1(x17521))))),f8(x17522)),f4(f8(f1(x17521)),f8(x17522)))), % 63.11/63.20 inference(scs_inference,[],[1747,1746,320,2,3])). % 63.11/63.20 cnf(1755,plain, % 63.11/63.20 (E(f4(f8(f1(x17551)),f8(x17552)),f4(f8(f1(f1(f1(f1(x17551))))),f8(x17552)))), % 63.11/63.20 inference(scs_inference,[],[1752,2])). % 63.11/63.20 cnf(1756,plain, % 63.11/63.20 (E(f4(f8(f1(f1(f1(f1(x17561))))),f8(x17562)),f4(f8(f1(x17561)),f8(f1(x17562))))), % 63.11/63.20 inference(scs_inference,[],[1752,308,2,3])). % 63.11/63.20 cnf(1759,plain, % 63.11/63.20 (E(f4(f8(f1(x17591)),f8(f1(x17592))),f4(f8(f1(f1(f1(f1(x17591))))),f8(x17592)))), % 63.11/63.20 inference(scs_inference,[],[1756,2])). % 63.11/63.20 cnf(1760,plain, % 63.11/63.20 (E(f4(f8(f1(x17601)),f8(f1(f1(x17602)))),f4(f8(f1(f1(f1(x17601)))),f8(x17602)))), % 63.11/63.20 inference(scs_inference,[],[1755,1756,659,2,3])). % 63.11/63.20 cnf(1764,plain, % 63.11/63.20 (E(f4(f8(f1(f1(f1(x17641)))),f8(x17642)),f4(f8(f1(x17641)),f8(f1(f1(x17642)))))), % 63.11/63.20 inference(scs_inference,[],[1760,2])). % 63.11/63.20 cnf(1765,plain, % 63.11/63.20 (E(f4(f8(f1(x17651)),f8(f1(f1(x17652)))),f4(f8(x17651),f8(f1(x17652))))), % 63.11/63.20 inference(scs_inference,[],[1759,1760,611,2,3])). % 63.11/63.20 cnf(1769,plain, % 63.11/63.20 (E(f4(f8(x17691),f8(f1(x17692))),f4(f8(f1(x17691)),f8(f1(f1(x17692)))))), % 63.11/63.20 inference(scs_inference,[],[1765,2])). % 63.11/63.20 cnf(1770,plain, % 63.11/63.20 (E(f4(f8(f1(f1(f1(x17701)))),f8(x17702)),f4(f8(x17701),f8(f1(x17702))))), % 63.11/63.20 inference(scs_inference,[],[1765,1764,2,3])). % 63.11/63.20 cnf(1773,plain, % 63.11/63.20 (E(f4(f8(x17731),f8(f1(x17732))),f4(f8(f1(f1(f1(x17731)))),f8(x17732)))), % 63.11/63.20 inference(scs_inference,[],[1770,2])). % 63.11/63.20 cnf(1774,plain, % 63.11/63.20 (E(f4(f8(f1(f1(f1(x17741)))),f8(x17742)),f4(f8(f1(f1(x17741))),f8(x17742)))), % 63.11/63.20 inference(scs_inference,[],[1770,652,2,3])). % 63.11/63.20 cnf(1778,plain, % 63.11/63.20 (E(f4(f8(x17781),f8(f1(f1(f1(x17782))))),f4(f8(x17781),f8(f1(x17782))))), % 63.11/63.20 inference(scs_inference,[],[1773,1716,1733,2,3])). % 63.11/63.20 cnf(1782,plain, % 63.11/63.20 (E(f4(f8(x17821),f8(f1(x17822))),f4(f8(x17821),f8(f1(f1(f1(x17822))))))), % 63.11/63.20 inference(scs_inference,[],[1778,2])). % 63.11/63.20 cnf(1783,plain, % 63.11/63.20 (E(f4(f8(f1(f1(f1(f1(x17831))))),f8(f1(x17832))),f4(f8(f1(x17831)),f8(x17832)))), % 63.11/63.20 inference(scs_inference,[],[1774,1778,637,2,3])). % 63.11/63.20 cnf(1786,plain, % 63.11/63.20 (E(f4(f8(f1(x17861)),f8(x17862)),f4(f8(f1(f1(f1(f1(x17861))))),f8(f1(x17862))))), % 63.11/63.20 inference(scs_inference,[],[1783,2])). % 63.11/63.20 cnf(1787,plain, % 63.11/63.20 (E(f4(f8(f1(f1(f1(x17871)))),f8(f1(x17872))),f4(f8(f1(x17871)),f8(f1(x17872))))), % 63.11/63.20 inference(scs_inference,[],[1783,1769,2,3])). % 63.11/63.20 cnf(1791,plain, % 63.11/63.20 (E(f4(f8(f1(x17911)),f8(f1(x17912))),f4(f8(f1(f1(f1(x17911)))),f8(f1(x17912))))), % 63.11/63.20 inference(scs_inference,[],[1787,2])). % 63.11/63.20 cnf(1792,plain, % 63.11/63.20 (E(f4(f8(f1(x17921)),f8(x17922)),f4(f8(f1(f1(x17921))),f8(f1(x17922))))), % 63.11/63.20 inference(scs_inference,[],[1786,1787,2,3])). % 63.11/63.20 cnf(1795,plain, % 63.11/63.20 (E(f4(f8(f1(f1(x17951))),f8(f1(x17952))),f4(f8(f1(x17951)),f8(x17952)))), % 63.11/63.20 inference(scs_inference,[],[1792,2])). % 63.11/63.20 cnf(1801,plain, % 63.11/63.20 (E(f4(f8(f1(f1(x18011))),f8(f1(f8(f1(x18012))))),f4(f8(f1(x18011)),f8(f8(x18012))))), % 63.11/63.20 inference(scs_inference,[],[1795,1721,970,2,3])). % 63.11/63.20 cnf(1806,plain, % 63.11/63.20 (E(f4(f8(f1(x18061)),f8(f1(f8(f1(x18062))))),f4(f8(f1(f1(x18061))),f8(f8(x18062))))), % 63.11/63.20 inference(scs_inference,[],[1791,1801,2,3])). % 63.11/63.20 cnf(1811,plain, % 63.11/63.20 (E(f4(f8(x18111),f8(f1(x18112))),f4(f8(f1(f1(x18111))),f8(f1(x18112))))), % 63.11/63.20 inference(scs_inference,[],[1806,1782,454,2,3])). % 63.11/63.20 cnf(1814,plain, % 63.11/63.20 (E(f4(f8(f1(f1(x18141))),f8(f1(x18142))),f4(f8(x18141),f8(f1(x18142))))), % 63.11/63.20 inference(scs_inference,[],[1811,2])). % 63.11/63.20 cnf(1820,plain, % 63.11/63.20 (E(f4(f8(f1(f1(x18201))),f8(f1(f1(f1(x18202))))),f4(f8(x18201),f8(f1(x18202))))), % 63.11/63.20 inference(scs_inference,[],[1814,1750,1778,2,3])). % 63.11/63.20 cnf(1824,plain, % 63.11/63.20 (E(f4(f8(x18241),f8(f1(x18242))),f4(f8(f1(f1(x18241))),f8(f1(f1(f1(x18242))))))), % 63.11/63.20 inference(scs_inference,[],[1820,2])). % 63.11/63.20 cnf(1862,plain, % 63.11/63.20 (E(f4(f10(f1(f8(x18621))),x18622),f4(f10(f1(f8(f1(x18621)))),x18622))), % 63.11/63.20 inference(scs_inference,[],[41,10,13])). % 63.11/63.20 cnf(1866,plain, % 63.11/63.20 (E(f10(f11(x18661,f1(f8(x18662)))),f10(f11(x18661,f1(f8(f1(x18662))))))), % 63.11/63.20 inference(scs_inference,[],[41,10,16])). % 63.11/63.20 cnf(1880,plain, % 63.11/63.20 (E(f4(f8(x18801),f8(f1(x18802))),f4(f8(f1(f1(f1(f1(x18801))))),f8(x18802)))), % 63.11/63.20 inference(scs_inference,[],[1164,1824,438,2,3])). % 63.11/63.20 cnf(1884,plain, % 63.11/63.20 (E(f4(f8(x18841),f8(f1(x18842))),f4(f8(f1(f1(x18841))),f8(f1(f1(x18842)))))), % 63.11/63.20 inference(scs_inference,[],[1880,1764,2,3])). % 63.11/63.20 cnf(1887,plain, % 63.11/63.20 (E(f4(f8(f1(f1(x18871))),f8(f1(f1(x18872)))),f4(f8(x18871),f8(f1(x18872))))), % 63.11/63.20 inference(scs_inference,[],[1884,2])). % 63.11/63.20 cnf(2016,plain, % 63.11/63.21 (E(f14(f11(f1(f8(x20161)),f8(f1(x20162)))),f14(f11(f1(f8(f1(x20161))),f8(x20162))))), % 63.11/63.21 inference(scs_inference,[],[1322,1862,1218,2,3])). % 63.11/63.21 cnf(2019,plain, % 63.11/63.21 (E(f14(f11(f1(f8(f1(x20191))),f8(x20192))),f14(f11(f1(f8(x20191)),f8(f1(x20192)))))), % 63.11/63.21 inference(scs_inference,[],[2016,2])). % 63.11/63.21 cnf(2020,plain, % 63.11/63.21 (E(f14(f11(f1(f8(x20201)),f8(f1(f1(x20202))))),f14(f11(f1(f8(x20201)),f8(x20202))))), % 63.11/63.21 inference(scs_inference,[],[2016,1297,2,3])). % 63.11/63.21 cnf(2024,plain, % 63.11/63.21 (E(f14(f11(f1(f8(x20241)),f8(x20242))),f14(f11(f1(f8(x20241)),f8(f1(f1(x20242))))))), % 63.11/63.21 inference(scs_inference,[],[2020,2])). % 63.11/63.21 cnf(2025,plain, % 63.11/63.21 (E(f14(f11(f1(f8(f1(x20251))),f8(f1(f1(x20252))))),f14(f11(f1(f8(x20251)),f8(x20252))))), % 63.11/63.21 inference(scs_inference,[],[2020,1295,2,3])). % 63.11/63.21 cnf(2030,plain, % 63.11/63.21 (E(f14(f11(f1(f8(f1(f1(x20301)))),f8(f1(x20302)))),f14(f11(f1(f8(x20301)),f8(x20302))))), % 63.11/63.21 inference(scs_inference,[],[2025,2019,2,3])). % 63.11/63.21 cnf(2034,plain, % 63.11/63.21 (E(f14(f11(f1(f8(f1(f1(x20341)))),f8(x20342))),f14(f11(f1(f8(x20341)),f8(f1(x20342)))))), % 63.11/63.21 inference(scs_inference,[],[2030,2024,2,3])). % 63.11/63.21 cnf(2039,plain, % 63.11/63.21 (E(f14(f3(f1(f8(x20391)),f8(x20392),x20393)),f14(f3(f1(f8(f1(x20391))),f8(x20392),x20393)))), % 63.11/63.21 inference(scs_inference,[],[1311,2034,1223,2,3])). % 63.11/63.21 cnf(2043,plain, % 63.11/63.21 (E(f14(f3(f1(f8(x20431)),f8(f1(f1(x20432))),x20433)),f14(f3(f1(f8(x20431)),f8(x20432),x20433)))), % 63.11/63.21 inference(scs_inference,[],[2039,1866,1312,2,3])). % 63.11/63.21 cnf(2047,plain, % 63.11/63.21 (E(f14(f3(f1(f8(x20471)),f8(f1(f1(x20472))),x20473)),f14(f3(f1(f8(f1(x20471))),f8(x20472),x20473)))), % 63.11/63.21 inference(scs_inference,[],[2043,2039,2,3])). % 63.11/63.21 cnf(2051,plain, % 63.11/63.21 (E(f14(f3(f1(f8(x20511)),f8(x20512),x20513)),f14(f3(f1(f8(f1(f1(x20511)))),f8(x20512),x20513)))), % 63.11/63.21 inference(scs_inference,[],[2047,1316,2,3])). % 63.11/63.21 cnf(2054,plain, % 63.11/63.21 (E(f14(f3(f1(f8(f1(f1(x20541)))),f8(x20542),x20543)),f14(f3(f1(f8(x20541)),f8(x20542),x20543)))), % 63.11/63.21 inference(scs_inference,[],[2051,2])). % 63.11/63.21 cnf(2055,plain, % 63.11/63.21 (E(f14(f3(f1(f8(x20551)),f8(x20552),x20553)),f14(f3(f1(f8(f1(f1(x20551)))),f8(f1(x20552)),x20553)))), % 63.11/63.21 inference(scs_inference,[],[2051,1217,2,3])). % 63.11/63.21 cnf(2058,plain, % 63.11/63.21 (E(f14(f3(f1(f8(f1(f1(x20581)))),f8(f1(x20582)),x20583)),f14(f3(f1(f8(x20581)),f8(x20582),x20583)))), % 63.11/63.21 inference(scs_inference,[],[2055,2])). % 63.11/63.21 cnf(2059,plain, % 63.11/63.21 (E(f14(f3(f1(f8(f1(f1(f1(x20591))))),f8(x20592),x20593)),f14(f3(f1(f8(x20591)),f8(x20592),x20593)))), % 63.11/63.21 inference(scs_inference,[],[2054,2055,1305,2,3])). % 63.11/63.21 cnf(2062,plain, % 63.11/63.21 (E(f14(f3(f1(f8(x20621)),f8(x20622),x20623)),f14(f3(f1(f8(f1(f1(f1(x20621))))),f8(x20622),x20623)))), % 63.11/63.21 inference(scs_inference,[],[2059,2])). % 63.11/63.21 cnf(2063,plain, % 63.11/63.21 (E(f11(f8(f8(f1(x20631))),f14(f8(f1(x20632)))),f11(f8(f8(x20631)),f14(f8(x20632))))), % 63.11/63.21 inference(scs_inference,[],[2059,1327,1296,2,3])). % 63.11/63.21 cnf(2066,plain, % 63.11/63.21 (E(f11(f8(f8(x20661)),f14(f8(x20662))),f11(f8(f8(f1(x20661))),f14(f8(f1(x20662)))))), % 63.11/63.21 inference(scs_inference,[],[2063,2])). % 63.11/63.21 cnf(2067,plain, % 63.11/63.21 (E(f14(f3(f1(f8(x20671)),f8(f1(x20672)),x20673)),f14(f3(f1(f8(f1(x20671))),f8(x20672),x20673)))), % 63.11/63.21 inference(scs_inference,[],[2058,2062,2063,2,3])). % 63.11/63.21 cnf(2071,plain, % 63.11/63.21 (E(f14(f3(f1(f8(f1(x20711))),f8(x20712),x20713)),f14(f3(f1(f8(x20711)),f8(f1(x20712)),x20713)))), % 63.11/63.21 inference(scs_inference,[],[2067,2])). % 63.11/63.21 cnf(2072,plain, % 63.11/63.21 (E(f11(f8(f8(x20721)),f14(f8(x20722))),f11(f8(f8(f1(f1(x20721)))),f14(f8(x20722))))), % 63.11/63.21 inference(scs_inference,[],[2067,2066,1302,2,3])). % 63.11/63.21 cnf(2075,plain, % 63.11/63.21 (E(f11(f8(f8(f1(f1(x20751)))),f14(f8(x20752))),f11(f8(f8(x20751)),f14(f8(x20752))))), % 63.11/63.21 inference(scs_inference,[],[2072,2])). % 63.11/63.21 cnf(2076,plain, % 63.11/63.21 (E(f11(f8(f8(x20761)),f14(f8(x20762))),f11(f8(f8(f1(f1(x20761)))),f14(f8(f1(x20762)))))), % 63.11/63.21 inference(scs_inference,[],[2072,1281,2,3])). % 63.11/63.21 cnf(2078,plain, % 63.11/63.21 (E(f11(f8(f8(f1(f1(x20781)))),f14(f8(f1(x20782)))),f11(f8(f8(x20781)),f14(f8(x20782))))), % 63.11/63.21 inference(scs_inference,[],[2076,2])). % 63.11/63.21 cnf(2157,plain, % 63.11/63.21 (E(f11(f5(f1(f8(x21571))),x21572),f11(f5(f1(f8(f1(x21571)))),x21572))), % 63.11/63.21 inference(scs_inference,[],[41,20,15])). % 63.11/63.21 cnf(2161,plain, % 63.11/63.21 (E(f5(f11(x21611,f1(f8(x21612)))),f5(f11(x21611,f1(f8(f1(x21612))))))), % 63.11/63.21 inference(scs_inference,[],[41,20,16])). % 63.11/63.21 cnf(2165,plain, % 63.11/63.21 (E(f3(f5(f1(f8(x21651))),x21652,x21653),f3(f5(f1(f8(f1(x21651)))),x21652,x21653))), % 63.11/63.21 inference(scs_inference,[],[41,20,17])). % 63.11/63.21 cnf(2224,plain, % 63.11/63.21 (E(f11(f8(f8(f1(f1(x22241)))),f14(f8(x22242))),f11(f8(f8(x22241)),f14(f8(f1(x22242)))))), % 63.11/63.21 inference(scs_inference,[],[2075,2157,1281,2,3])). % 63.11/63.21 cnf(2227,plain, % 63.11/63.21 (E(f11(f8(f8(x22271)),f14(f8(f1(x22272)))),f11(f8(f8(f1(f1(x22271)))),f14(f8(x22272))))), % 63.11/63.21 inference(scs_inference,[],[2224,2])). % 63.11/63.21 cnf(2228,plain, % 63.11/63.21 (E(f14(f3(f1(f8(f1(f1(x22281)))),f8(x22282),x22283)),f14(f3(f1(f8(x22281)),f8(f1(x22282)),x22283)))), % 63.11/63.21 inference(scs_inference,[],[2071,2224,1305,2,3])). % 63.11/63.21 cnf(2233,plain, % 63.11/63.21 (E(f11(f8(f8(x22331)),f14(f8(f1(f1(x22332))))),f11(f8(f8(x22331)),f14(f8(x22332))))), % 63.11/63.21 inference(scs_inference,[],[2078,2227,2228,2,3])). % 63.11/63.21 cnf(2237,plain, % 63.11/63.21 (E(f11(f8(f8(x22371)),f14(f8(x22372))),f11(f8(f8(x22371)),f14(f8(f1(f1(x22372))))))), % 63.11/63.21 inference(scs_inference,[],[2233,2])). % 63.11/63.21 cnf(2238,plain, % 63.11/63.21 (E(f14(f6(f8(f1(x22381)),f1(f8(f1(x22382))))),f14(f6(f8(x22381),f1(f8(x22382)))))), % 63.11/63.21 inference(scs_inference,[],[2233,1662,1334,2,3])). % 63.11/63.21 cnf(2242,plain, % 63.11/63.21 (E(f14(f6(f8(x22421),f1(f8(x22422)))),f14(f6(f8(f1(x22421)),f1(f8(f1(x22422))))))), % 63.11/63.21 inference(scs_inference,[],[2238,2])). % 63.11/63.21 cnf(2243,plain, % 63.11/63.21 (E(f11(f8(f8(f1(x22431))),f14(f8(x22432))),f11(f8(f8(x22431)),f14(f8(f1(f1(x22432))))))), % 63.11/63.21 inference(scs_inference,[],[2238,2237,1327,2,3])). % 63.11/63.21 cnf(2248,plain, % 63.11/63.21 (E(f11(f8(f8(f1(x22481))),f14(f8(x22482))),f11(f8(f8(x22481)),f14(f8(x22482))))), % 63.11/63.21 inference(scs_inference,[],[2161,2243,2233,2,3])). % 63.11/63.21 cnf(2252,plain, % 63.11/63.21 (E(f11(f8(f8(f1(f1(f1(x22521))))),f14(f8(x22522))),f11(f8(f8(x22521)),f14(f8(x22522))))), % 63.11/63.21 inference(scs_inference,[],[2248,2165,2075,2,3])). % 63.11/63.21 cnf(2257,plain, % 63.11/63.21 (E(f14(f6(f8(x22571),f1(f8(x22572)))),f14(f6(f8(f1(f1(x22571))),f1(f8(x22572)))))), % 63.11/63.21 inference(scs_inference,[],[2252,2242,1341,2,3])). % 63.11/63.21 cnf(2261,plain, % 63.11/63.21 (E(f14(f12(f8(f1(x22611)),f1(f8(f1(x22612))))),f14(f12(f8(x22611),f1(f8(x22612)))))), % 63.11/63.21 inference(scs_inference,[],[1665,2257,1353,2,3])). % 63.11/63.21 cnf(2265,plain, % 63.11/63.21 (E(f14(f12(f8(x22651),f1(f8(x22652)))),f14(f12(f8(f1(x22651)),f1(f8(f1(x22652))))))), % 63.11/63.21 inference(scs_inference,[],[2261,2])). % 63.11/63.21 cnf(2266,plain, % 63.11/63.21 (E(f14(f4(f8(f1(x22661)),f1(f8(f1(x22662))))),f14(f4(f8(x22661),f1(f8(x22662)))))), % 63.11/63.21 inference(scs_inference,[],[1669,2261,1363,2,3])). % 63.11/63.21 cnf(2270,plain, % 63.11/63.21 (E(f14(f4(f8(x22701),f1(f8(x22702)))),f14(f4(f8(f1(x22701)),f1(f8(f1(x22702))))))), % 63.11/63.21 inference(scs_inference,[],[2266,2])). % 63.11/63.21 cnf(2271,plain, % 63.11/63.21 (E(f14(f12(f8(x22711),f1(f8(x22712)))),f14(f12(f8(f1(f1(x22711))),f1(f8(x22712)))))), % 63.11/63.21 inference(scs_inference,[],[2266,2265,1355,2,3])). % 63.11/63.21 cnf(2275,plain, % 63.11/63.21 (E(f14(f4(f8(x22751),f1(f8(x22752)))),f14(f4(f8(f1(f1(x22751))),f1(f8(x22752)))))), % 63.11/63.21 inference(scs_inference,[],[2271,2270,1365,2,3])). % 63.11/63.21 cnf(2279,plain, % 63.11/63.21 (E(f4(f8(f1(f1(x22791))),f8(f1(f1(x22792)))),f4(f8(x22791),f8(x22792)))), % 63.11/63.21 inference(scs_inference,[],[1887,2275,309,2,3])). % 63.11/63.21 cnf(2282,plain, % 63.11/63.21 (E(f4(f8(x22821),f8(x22822)),f4(f8(f1(f1(x22821))),f8(f1(f1(x22822)))))), % 63.11/63.21 inference(scs_inference,[],[2279,2])). % 63.11/63.21 cnf(2283,plain, % 63.11/63.21 (E(f4(f8(f1(f1(x22831))),f8(f1(f1(f1(x22832))))),f4(f8(f1(x22831)),f8(x22832)))), % 63.11/63.21 inference(scs_inference,[],[2279,315,2,3])). % 63.11/63.21 cnf(2287,plain, % 63.11/63.21 (E(f3(x22871,f3(x22872,x22873,f8(x22874)),f8(x22875)),f3(x22871,f3(x22872,x22873,f8(f1(x22874))),f8(f1(x22875))))), % 63.11/63.21 inference(scs_inference,[],[74,2283,332,2,3])). % 63.11/63.21 cnf(2291,plain, % 63.11/63.21 (E(f3(x22911,f3(x22912,x22913,f8(f1(x22914))),f8(f1(x22915))),f3(x22911,f3(x22912,x22913,f8(x22914)),f8(x22915)))), % 63.11/63.21 inference(scs_inference,[],[2287,2])). % 63.11/63.21 cnf(2292,plain, % 63.11/63.21 (E(f4(f8(x22921),f8(x22922)),f4(f8(f1(f1(f1(f1(f1(x22921)))))),f8(x22922)))), % 63.11/63.21 inference(scs_inference,[],[2287,2282,599,2,3])). % 63.11/63.21 cnf(2296,plain, % 63.11/63.21 (E(f3(x22961,f3(x22962,x22963,f8(f1(f1(x22964)))),f8(f1(x22965))),f3(x22961,f3(x22962,x22963,f8(x22964)),f8(x22965)))), % 63.11/63.21 inference(scs_inference,[],[73,2291,2292,2,3])). % 63.11/63.21 cnf(2301,plain, % 63.11/63.21 (E(f3(x23011,f3(x23012,x23013,f8(x23014)),f8(f1(x23015))),f3(x23011,f3(x23012,x23013,f8(x23014)),f8(x23015)))), % 63.11/63.21 inference(scs_inference,[],[74,2296,2291,2,3])). % 63.11/63.21 cnf(2362,plain, % 63.11/63.21 (P1(f12(f9(a13),f10(a18)),f8(f5(a20)),a16)), % 63.11/63.21 inference(scs_inference,[],[2301,77,4,5,8,9,10,20,27])). % 63.11/63.21 cnf(2370,plain, % 63.11/63.21 (E(f11(f3(x23701,f3(x23702,x23703,f8(x23704)),f8(f1(x23705))),x23706),f11(f3(x23701,f3(x23702,x23703,f8(x23704)),f8(x23705)),x23706))), % 63.11/63.21 inference(scs_inference,[],[2301,77,4,5,8,9,10,20,27,6,7,11,12,13,14,15])). % 63.11/63.21 cnf(2379,plain, % 63.11/63.21 (~P1(f10(a18),f8(f6(a7,a20)),a16)), % 63.11/63.21 inference(scs_inference,[],[25,2301,568,26,99,77,4,5,8,9,10,20,27,6,7,11,12,13,14,15,16,17,18,19,29,32,31])). % 63.11/63.21 cnf(2382,plain, % 63.11/63.21 (~E(f8(f1(f1(f1(f1(f6(a7,a20)))))),f5(a20))), % 63.11/63.21 inference(scs_inference,[],[25,2301,568,81,26,99,77,4,5,8,9,10,20,27,6,7,11,12,13,14,15,16,17,18,19,29,32,31,2,22])). % 63.11/63.21 cnf(2383,plain, % 63.11/63.21 (E(f3(f8(x23831),f3(x23832,x23833,f8(x23834)),f8(f1(x23835))),f3(f8(f1(x23831)),f3(x23832,x23833,f8(f1(x23834))),f8(x23835)))), % 63.11/63.21 inference(scs_inference,[],[25,2301,568,1703,81,26,99,77,4,5,8,9,10,20,27,6,7,11,12,13,14,15,16,17,18,19,29,32,31,2,22,3])). % 63.11/63.21 cnf(2396,plain, % 63.11/63.21 (P1(f12(f9(a13),f10(a18)),f8(f8(f5(a20))),a16)), % 63.11/63.21 inference(scs_inference,[],[2362,29,27])). % 63.11/63.21 cnf(2421,plain, % 63.11/63.21 (P1(f12(f9(a13),f10(a18)),f8(f8(f1(f5(a20)))),a16)), % 63.11/63.21 inference(scs_inference,[],[2362,2383,982,2370,559,2382,29,27,4,11,14,6,12,19,13,16,5,10,18,15,20,9,8,17,7,2,22,3,1084])). % 63.11/63.21 cnf(2458,plain, % 63.11/63.21 (~P1(f10(a18),f8(f1(f6(a7,a20))),a16)), % 63.11/63.21 inference(scs_inference,[],[2379,2396,2421,829,990,55,24,1093,29,1088,27,1084,16,19,5,14,12,18,10,6,11,20,4,7,15,17,13,8,9,2,22])). % 63.11/63.21 cnf(2671,plain, % 63.11/63.21 ($false), % 63.11/63.21 inference(scs_inference,[],[2458,79,29]), % 63.11/63.21 ['proof']). % 63.11/63.21 % SZS output end Proof % 63.11/63.21 % Total time :62.560000s %------------------------------------------------------------------------------