%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : LAT276-2 : TPTP v8.2.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n023.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Jun 24 10:18:32 EDT 2024 % Result : Unsatisfiable 60.29s 60.41s % Output : CNFRefutation 60.29s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : LAT276-2 : TPTP v8.2.0. Released v3.2.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n023.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Fri Jun 21 22:12:09 EDT 2024 % 0.12/0.34 % CPUTime : % 0.43/0.60 start to proof:theBenchmark % 60.29/60.40 %------------------------------------------- % 60.29/60.40 % File :CSE---1.7 % 60.29/60.40 % Problem :theBenchmark % 60.29/60.40 % Transform :cnf % 60.29/60.40 % Format :tptp:raw % 60.29/60.40 % Command :java -jar mcs_scs.jar %d %s % 60.29/60.40 % 60.29/60.40 % Result :Theorem 59.710000s % 60.29/60.40 % Output :CNFRefutation 59.710000s % 60.29/60.40 %------------------------------------------- % 60.29/60.41 %------------------------------------------------------------------------------ % 60.29/60.41 % File : LAT276-2 : TPTP v8.2.0. Released v3.2.0. % 60.29/60.41 % Domain : Analysis % 60.29/60.41 % Problem : Problem about Tarski's fixed point theorem % 60.29/60.41 % Version : [Pau06] axioms : Reduced > Especial. % 60.29/60.41 % English : % 60.29/60.41 % 60.29/60.41 % Refs : [Pau06] Paulson (2006), Email to G. Sutcliffe % 60.29/60.41 % Source : [Pau06] % 60.29/60.41 % Names : % 60.29/60.41 % 60.29/60.41 % Status : Unsatisfiable % 60.29/60.41 % Rating : 0.15 v8.2.0, 0.10 v8.1.0, 0.00 v7.5.0, 0.05 v7.4.0, 0.12 v7.3.0, 0.08 v7.0.0, 0.13 v6.4.0, 0.07 v6.3.0, 0.00 v5.5.0, 0.15 v5.4.0, 0.20 v5.3.0, 0.11 v5.2.0, 0.06 v5.0.0, 0.07 v4.1.0, 0.08 v4.0.1, 0.00 v4.0.0, 0.09 v3.7.0, 0.10 v3.5.0, 0.09 v3.4.0, 0.25 v3.3.0, 0.21 v3.2.0 % 60.29/60.41 % Syntax : Number of clauses : 12 ( 3 unt; 3 nHn; 12 RR) % 60.29/60.41 % Number of literals : 29 ( 2 equ; 15 neg) % 60.29/60.41 % Maximal clause size : 4 ( 2 avg) % 60.29/60.41 % Maximal term depth : 3 ( 1 avg) % 60.29/60.41 % Number of predicates : 3 ( 2 usr; 0 prp; 2-3 aty) % 60.29/60.41 % Number of functors : 14 ( 14 usr; 7 con; 0-4 aty) % 60.29/60.41 % Number of variables : 12 ( 0 sgn) % 60.29/60.41 % SPC : CNF_UNS_RFO_SEQ_NHN % 60.29/60.41 % 60.29/60.41 % Comments : The problems in the [Pau06] collection each have very many axioms, % 60.29/60.41 % of which only a small selection are required for the refutation. % 60.29/60.41 % The mission is to find those few axioms, after which a refutation % 60.29/60.41 % can be quite easily found. This version has only the necessary % 60.29/60.41 % axioms. % 60.29/60.41 %------------------------------------------------------------------------------ % 60.29/60.41 cnf(cls_conjecture_0,negated_conjecture, % 60.29/60.41 c_lessequals(v_S,v_A,tc_set(t_a)) ). % 60.29/60.41 % 60.29/60.41 cnf(cls_conjecture_10,negated_conjecture, % 60.29/60.41 ( c_in(c_Pair(V_V,v_xa,t_a,t_a),c_Tarski_Opotype_Oorder(v_cl,t_a,tc_Product__Type_Ounit),tc_prod(t_a,t_a)) % 60.29/60.41 | ~ c_in(V_V,v_S,t_a) % 60.29/60.41 | ~ c_in(c_Pair(v_xa,c_Tarski_Olub(v_S,v_cl,t_a),t_a,t_a),c_Tarski_Opotype_Oorder(v_cl,t_a,tc_Product__Type_Ounit),tc_prod(t_a,t_a)) ) ). % 60.29/60.41 % 60.29/60.41 cnf(cls_conjecture_3,negated_conjecture, % 60.29/60.41 ( c_in(v_xa,c_Tarski_Opotype_Opset(v_cl,t_a,tc_Product__Type_Ounit),t_a) % 60.29/60.41 | c_in(v_xa,v_S,t_a) ) ). % 60.29/60.41 % 60.29/60.41 cnf(cls_conjecture_4,negated_conjecture, % 60.29/60.41 ( ~ c_in(c_Pair(c_Tarski_Olub(v_S,v_cl,t_a),v_xa,t_a,t_a),c_Tarski_Opotype_Oorder(v_cl,t_a,tc_Product__Type_Ounit),tc_prod(t_a,t_a)) % 60.29/60.41 | c_in(v_xa,v_S,t_a) ) ). % 60.29/60.41 % 60.29/60.41 cnf(cls_conjecture_6,negated_conjecture, % 60.29/60.41 ( ~ c_in(c_Pair(c_Tarski_Olub(v_S,v_cl,t_a),v_xa,t_a,t_a),c_Tarski_Opotype_Oorder(v_cl,t_a,tc_Product__Type_Ounit),tc_prod(t_a,t_a)) % 60.29/60.41 | ~ c_in(c_Pair(v_xa,c_Tarski_Olub(v_S,v_cl,t_a),t_a,t_a),c_Tarski_Opotype_Oorder(v_cl,t_a,tc_Product__Type_Ounit),tc_prod(t_a,t_a)) ) ). % 60.29/60.41 % 60.29/60.41 cnf(cls_conjecture_9,negated_conjecture, % 60.29/60.41 ( c_in(c_Pair(V_U,v_xa,t_a,t_a),c_Tarski_Opotype_Oorder(v_cl,t_a,tc_Product__Type_Ounit),tc_prod(t_a,t_a)) % 60.29/60.41 | ~ c_in(V_U,v_S,t_a) % 60.29/60.41 | c_in(v_xa,v_S,t_a) ) ). % 60.29/60.41 % 60.29/60.41 cnf(cls_Set_OsubsetD_0,axiom, % 60.29/60.41 ( ~ c_in(V_c,V_A,T_a) % 60.29/60.41 | ~ c_lessequals(V_A,V_B,tc_set(T_a)) % 60.29/60.41 | c_in(V_c,V_B,T_a) ) ). % 60.29/60.41 % 60.29/60.41 cnf(cls_Tarski_OA_A_61_61_Apset_Acl_0,axiom, % 60.29/60.41 v_A = c_Tarski_Opotype_Opset(v_cl,t_a,tc_Product__Type_Ounit) ). % 60.29/60.41 % 60.29/60.41 cnf(cls_Tarski_O_91_124_AS1_A_60_61_AA_59_AL1_A_58_AA_59_AALL_Ax_58S1_O_A_Ix_M_AL1_J_A_58_Ar_A_124_93_A_61_61_62_A_Ilub_AS1_Acl_M_AL1_J_A_58_Ar_A_61_61_ATrue_0,axiom, % 60.29/60.41 ( ~ c_in(V_L,v_A,t_a) % 60.29/60.41 | ~ c_lessequals(V_S,v_A,tc_set(t_a)) % 60.29/60.41 | c_in(c_Pair(c_Tarski_Olub(V_S,v_cl,t_a),V_L,t_a,t_a),v_r,tc_prod(t_a,t_a)) % 60.29/60.41 | c_in(v_sko__4mP(V_L,V_S,v_r),V_S,t_a) ) ). % 60.29/60.41 % 60.29/60.41 cnf(cls_Tarski_O_91_124_AS1_A_60_61_AA_59_AL1_A_58_AA_59_AALL_Ax_58S1_O_A_Ix_M_AL1_J_A_58_Ar_A_124_93_A_61_61_62_A_Ilub_AS1_Acl_M_AL1_J_A_58_Ar_A_61_61_ATrue_1,axiom, % 60.29/60.41 ( ~ c_in(V_L,v_A,t_a) % 60.29/60.41 | ~ c_in(c_Pair(v_sko__4mP(V_L,V_S,v_r),V_L,t_a,t_a),v_r,tc_prod(t_a,t_a)) % 60.29/60.41 | ~ c_lessequals(V_S,v_A,tc_set(t_a)) % 60.29/60.41 | c_in(c_Pair(c_Tarski_Olub(V_S,v_cl,t_a),V_L,t_a,t_a),v_r,tc_prod(t_a,t_a)) ) ). % 60.29/60.41 % 60.29/60.41 cnf(cls_Tarski_O_91_124_AS1_A_60_61_AA_59_Ax1_A_58_AS1_A_124_93_A_61_61_62_A_Ix1_M_Alub_AS1_Acl_J_A_58_Ar_A_61_61_ATrue_0,axiom, % 60.29/60.41 ( ~ c_in(V_x,V_S,t_a) % 60.29/60.41 | ~ c_lessequals(V_S,v_A,tc_set(t_a)) % 60.29/60.41 | c_in(c_Pair(V_x,c_Tarski_Olub(V_S,v_cl,t_a),t_a,t_a),v_r,tc_prod(t_a,t_a)) ) ). % 60.29/60.41 % 60.29/60.41 cnf(cls_Tarski_Or_A_61_61_Aorder_Acl_0,axiom, % 60.29/60.41 v_r = c_Tarski_Opotype_Oorder(v_cl,t_a,tc_Product__Type_Ounit) ). % 60.29/60.41 % 60.29/60.41 %------------------------------------------------------------------------------ % 60.29/60.41 %------------------------------------------- % 60.29/60.41 % Proof found % 60.29/60.41 % SZS status Theorem for theBenchmark % 60.29/60.41 % SZS output start Proof % 60.29/60.41 %ClaNum:40(EqnAxiom:28) % 60.29/60.41 %VarNum:32(SingletonVarNum:12) % 60.29/60.41 %MaxLitNum:4 % 60.29/60.41 %MaxfuncDepth:2 % 60.29/60.41 %SharedTerms:21 % 60.29/60.41 %goalClause: 31 32 34 37 38 40 % 60.29/60.41 %singleGoalClaCount:1 % 60.29/60.41 [29]E(f3(a1,a2,a7),a8) % 60.29/60.41 [30]E(f4(a1,a2,a7),a12) % 60.29/60.41 [31]P1(a11,a8,f9(a2)) % 60.29/60.41 [32]P2(a13,a11,a2)+P2(a13,f3(a1,a2,a7),a2) % 60.29/60.41 [37]P2(a13,a11,a2)+~P2(f5(f6(a11,a1,a2),a13,a2,a2),f4(a1,a2,a7),f10(a2,a2)) % 60.29/60.41 [40]~P2(f5(a13,f6(a11,a1,a2),a2,a2),f4(a1,a2,a7),f10(a2,a2))+~P2(f5(f6(a11,a1,a2),a13,a2,a2),f4(a1,a2,a7),f10(a2,a2)) % 60.29/60.41 [34]P2(a13,a11,a2)+~P2(x341,a11,a2)+P2(f5(x341,a13,a2,a2),f4(a1,a2,a7),f10(a2,a2)) % 60.29/60.41 [38]P2(f5(x381,a13,a2,a2),f4(a1,a2,a7),f10(a2,a2))+~P2(x381,a11,a2)+~P2(f5(a13,f6(a11,a1,a2),a2,a2),f4(a1,a2,a7),f10(a2,a2)) % 60.29/60.41 [35]~P2(x351,x352,a2)+~P1(x352,a8,f9(a2))+P2(f5(x351,f6(x352,a1,a2),a2,a2),a12,f10(a2,a2)) % 60.29/60.41 [33]P2(x331,x332,x333)+~P2(x331,x334,x333)+~P1(x334,x332,f9(x333)) % 60.29/60.41 [36]~P2(x361,a8,a2)+P2(f14(x361,x362,a12),x362,a2)+~P1(x362,a8,f9(a2))+P2(f5(f6(x362,a1,a2),x361,a2,a2),a12,f10(a2,a2)) % 60.29/60.41 [39]~P2(x392,a8,a2)+~P1(x391,a8,f9(a2))+~P2(f5(f14(x392,x391,a12),x392,a2,a2),a12,f10(a2,a2))+P2(f5(f6(x391,a1,a2),x392,a2,a2),a12,f10(a2,a2)) % 60.29/60.41 %EqnAxiom % 60.29/60.41 [1]E(x11,x11) % 60.29/60.41 [2]E(x22,x21)+~E(x21,x22) % 60.29/60.41 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 60.29/60.41 [4]~E(x41,x42)+E(f3(x41,x43,x44),f3(x42,x43,x44)) % 60.29/60.41 [5]~E(x51,x52)+E(f3(x53,x51,x54),f3(x53,x52,x54)) % 60.29/60.41 [6]~E(x61,x62)+E(f3(x63,x64,x61),f3(x63,x64,x62)) % 60.29/60.41 [7]~E(x71,x72)+E(f4(x71,x73,x74),f4(x72,x73,x74)) % 60.29/60.41 [8]~E(x81,x82)+E(f4(x83,x81,x84),f4(x83,x82,x84)) % 60.29/60.41 [9]~E(x91,x92)+E(f4(x93,x94,x91),f4(x93,x94,x92)) % 60.29/60.41 [10]~E(x101,x102)+E(f9(x101),f9(x102)) % 60.29/60.41 [11]~E(x111,x112)+E(f10(x111,x113),f10(x112,x113)) % 60.29/60.41 [12]~E(x121,x122)+E(f10(x123,x121),f10(x123,x122)) % 60.29/60.41 [13]~E(x131,x132)+E(f6(x131,x133,x134),f6(x132,x133,x134)) % 60.29/60.41 [14]~E(x141,x142)+E(f6(x143,x141,x144),f6(x143,x142,x144)) % 60.29/60.41 [15]~E(x151,x152)+E(f6(x153,x154,x151),f6(x153,x154,x152)) % 60.29/60.41 [16]~E(x161,x162)+E(f5(x161,x163,x164,x165),f5(x162,x163,x164,x165)) % 60.29/60.41 [17]~E(x171,x172)+E(f5(x173,x171,x174,x175),f5(x173,x172,x174,x175)) % 60.29/60.41 [18]~E(x181,x182)+E(f5(x183,x184,x181,x185),f5(x183,x184,x182,x185)) % 60.29/60.41 [19]~E(x191,x192)+E(f5(x193,x194,x195,x191),f5(x193,x194,x195,x192)) % 60.29/60.41 [20]~E(x201,x202)+E(f14(x201,x203,x204),f14(x202,x203,x204)) % 60.29/60.41 [21]~E(x211,x212)+E(f14(x213,x211,x214),f14(x213,x212,x214)) % 60.29/60.41 [22]~E(x221,x222)+E(f14(x223,x224,x221),f14(x223,x224,x222)) % 60.29/60.41 [23]P1(x232,x233,x234)+~E(x231,x232)+~P1(x231,x233,x234) % 60.29/60.41 [24]P1(x243,x242,x244)+~E(x241,x242)+~P1(x243,x241,x244) % 60.29/60.41 [25]P1(x253,x254,x252)+~E(x251,x252)+~P1(x253,x254,x251) % 60.29/60.41 [26]P2(x262,x263,x264)+~E(x261,x262)+~P2(x261,x263,x264) % 60.29/60.41 [27]P2(x273,x272,x274)+~E(x271,x272)+~P2(x273,x271,x274) % 60.29/60.41 [28]P2(x283,x284,x282)+~E(x281,x282)+~P2(x283,x284,x281) % 60.29/60.41 % 60.29/60.41 %------------------------------------------- % 60.29/60.42 cnf(41,plain, % 60.29/60.42 (E(a8,f3(a1,a2,a7))), % 60.29/60.42 inference(scs_inference,[],[29,2])). % 60.29/60.42 cnf(42,plain, % 60.29/60.42 (P1(a11,f3(a1,a2,a7),f9(a2))), % 60.29/60.42 inference(scs_inference,[],[31,29,2,24])). % 60.29/60.42 cnf(43,plain, % 60.29/60.42 (P2(x431,a8,a2)+~P2(x431,a11,a2)), % 60.29/60.42 inference(scs_inference,[],[31,29,2,24,33])). % 60.29/60.42 cnf(49,plain, % 60.29/60.42 (E(a12,f4(a1,a2,a7))), % 60.29/60.42 inference(scs_inference,[],[30,2])). % 60.29/60.42 cnf(50,plain, % 60.29/60.42 (P2(x501,f3(a1,a2,a7),a2)+~P2(x501,a11,a2)), % 60.29/60.42 inference(scs_inference,[],[42,30,2,33])). % 60.29/60.42 cnf(72,plain, % 60.29/60.42 (P2(a13,a8,a2)+P2(a13,f3(a1,a2,a7),a2)), % 60.29/60.42 inference(scs_inference,[],[43,32])). % 60.29/60.42 cnf(80,plain, % 60.29/60.42 (P2(a13,f3(a1,a2,a7),a2)), % 60.29/60.42 inference(scs_inference,[],[41,72,27])). % 60.29/60.42 cnf(81,plain, % 60.29/60.42 (P2(a13,a8,a2)), % 60.29/60.42 inference(scs_inference,[],[80,29,27])). % 60.29/60.42 cnf(87,plain, % 60.29/60.42 (P2(x871,a8,a2)+~E(a13,x871)), % 60.29/60.42 inference(scs_inference,[],[81,26])). % 60.29/60.42 cnf(101,plain, % 60.29/60.42 (~P2(f5(f6(a11,a1,a2),a13,a2,a2),f4(a1,a2,a7),f10(a2,a2))+P2(f5(a13,f6(a11,a1,a2),a2,a2),a12,f10(a2,a2))), % 60.29/60.42 inference(scs_inference,[],[31,37,35])). % 60.29/60.42 cnf(102,plain, % 60.29/60.42 (P2(f5(a13,f6(a11,a1,a2),a2,a2),f4(a1,a2,a7),f10(a2,a2))+~P2(f5(f6(a11,a1,a2),a13,a2,a2),f4(a1,a2,a7),f10(a2,a2))), % 60.29/60.42 inference(scs_inference,[],[49,101,27])). % 60.29/60.42 cnf(103,plain, % 60.29/60.42 (~P2(f5(f6(a11,a1,a2),a13,a2,a2),f4(a1,a2,a7),f10(a2,a2))), % 60.29/60.42 inference(scs_inference,[],[40,102])). % 60.29/60.42 cnf(212,plain, % 60.29/60.42 (~E(f5(x2121,a13,a2,a2),f5(f6(a11,a1,a2),a13,a2,a2))+~P2(x2121,a11,a2)+~P2(f5(a13,f6(a11,a1,a2),a2,a2),f4(a1,a2,a7),f10(a2,a2))), % 60.29/60.42 inference(scs_inference,[],[103,38,26])). % 60.29/60.42 cnf(213,plain, % 60.29/60.42 (~P2(f6(a11,a1,a2),a11,a2)+~P2(f5(a13,f6(a11,a1,a2),a2,a2),f4(a1,a2,a7),f10(a2,a2))), % 60.29/60.42 inference(equality_inference,[],[212])). % 60.29/60.42 cnf(216,plain, % 60.29/60.42 (E(f3(a8,x2161,x2162),f3(f3(a1,a2,a7),x2161,x2162))), % 60.29/60.42 inference(scs_inference,[],[29,2,4])). % 60.29/60.42 cnf(217,plain, % 60.29/60.42 (E(f3(f3(a1,a2,a7),x2171,x2172),f3(a8,x2171,x2172))), % 60.29/60.42 inference(scs_inference,[],[216,2])). % 60.29/60.42 cnf(218,plain, % 60.29/60.42 (E(f3(x2181,a8,x2182),f3(x2181,f3(a1,a2,a7),x2182))), % 60.29/60.42 inference(scs_inference,[],[29,2,5])). % 60.29/60.42 cnf(219,plain, % 60.29/60.42 (E(f3(x2191,f3(a1,a2,a7),x2192),f3(x2191,a8,x2192))), % 60.29/60.42 inference(scs_inference,[],[218,2])). % 60.29/60.42 cnf(220,plain, % 60.29/60.42 (E(f3(f3(a1,a2,a7),a8,x2201),f3(a8,f3(a1,a2,a7),x2201))), % 60.29/60.42 inference(scs_inference,[],[217,218,2,3])). % 60.29/60.42 cnf(223,plain, % 60.29/60.42 (E(f3(x2231,x2232,a8),f3(x2231,x2232,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[29,2,6])). % 60.29/60.42 cnf(224,plain, % 60.29/60.42 (E(f3(x2241,x2242,f3(a1,a2,a7)),f3(x2241,x2242,a8))), % 60.29/60.42 inference(scs_inference,[],[223,2])). % 60.29/60.42 cnf(225,plain, % 60.29/60.42 (E(f3(x2251,f3(a1,a2,a7),a8),f3(x2251,a8,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[219,223,2,3])). % 60.29/60.42 cnf(228,plain, % 60.29/60.42 (E(f4(f3(a1,a2,a7),x2281,x2282),f4(a8,x2281,x2282))), % 60.29/60.42 inference(scs_inference,[],[41,2,7])). % 60.29/60.42 cnf(229,plain, % 60.29/60.42 (E(f4(a8,x2291,x2292),f4(f3(a1,a2,a7),x2291,x2292))), % 60.29/60.42 inference(scs_inference,[],[228,2])). % 60.29/60.42 cnf(230,plain, % 60.29/60.42 (E(f3(f3(a1,a2,a7),a8,f3(a1,a2,a7)),f3(a8,f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[224,228,220,2,3])). % 60.29/60.42 cnf(233,plain, % 60.29/60.42 (E(f4(x2331,a8,x2332),f4(x2331,f3(a1,a2,a7),x2332))), % 60.29/60.42 inference(scs_inference,[],[29,2,8])). % 60.29/60.42 cnf(234,plain, % 60.29/60.42 (E(f4(x2341,f3(a1,a2,a7),x2342),f4(x2341,a8,x2342))), % 60.29/60.42 inference(scs_inference,[],[233,2])). % 60.29/60.42 cnf(235,plain, % 60.29/60.42 (E(f4(a8,a8,x2351),f4(f3(a1,a2,a7),f3(a1,a2,a7),x2351))), % 60.29/60.42 inference(scs_inference,[],[229,233,2,3])). % 60.29/60.42 cnf(238,plain, % 60.29/60.42 (E(f4(x2381,x2382,f3(a1,a2,a7)),f4(x2381,x2382,a8))), % 60.29/60.42 inference(scs_inference,[],[41,2,9])). % 60.29/60.42 cnf(239,plain, % 60.29/60.42 (E(f4(x2391,x2392,a8),f4(x2391,x2392,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[238,2])). % 60.29/60.42 cnf(240,plain, % 60.29/60.42 (E(f4(x2401,f3(a1,a2,a7),f3(a1,a2,a7)),f4(x2401,a8,a8))), % 60.29/60.42 inference(scs_inference,[],[234,238,2,3])). % 60.29/60.42 cnf(243,plain, % 60.29/60.42 (E(f10(a8,x2431),f10(f3(a1,a2,a7),x2431))), % 60.29/60.42 inference(scs_inference,[],[29,2,11])). % 60.29/60.42 cnf(245,plain, % 60.29/60.42 (E(f4(a8,a8,a8),f4(f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[239,230,235,2,3])). % 60.29/60.42 cnf(248,plain, % 60.29/60.42 (E(f10(x2481,f3(a1,a2,a7)),f10(x2481,a8))), % 60.29/60.42 inference(scs_inference,[],[41,2,12])). % 60.29/60.42 cnf(249,plain, % 60.29/60.42 (E(f10(x2491,a8),f10(x2491,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[248,2])). % 60.29/60.42 cnf(250,plain, % 60.29/60.42 (E(f10(a8,f3(a1,a2,a7)),f10(f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[248,243,2,3])). % 60.29/60.42 cnf(253,plain, % 60.29/60.42 (E(f6(a8,x2531,x2532),f6(f3(a1,a2,a7),x2531,x2532))), % 60.29/60.42 inference(scs_inference,[],[29,2,13])). % 60.29/60.42 cnf(254,plain, % 60.29/60.42 (E(f6(f3(a1,a2,a7),x2541,x2542),f6(a8,x2541,x2542))), % 60.29/60.42 inference(scs_inference,[],[253,2])). % 60.29/60.42 cnf(255,plain, % 60.29/60.42 (E(f3(f3(a1,a2,a7),a8,f3(a1,a2,a7)),f3(a8,a8,a8))), % 60.29/60.42 inference(scs_inference,[],[253,230,219,2,3])). % 60.29/60.42 cnf(257,plain, % 60.29/60.42 (E(f6(x2571,f3(a1,a2,a7),x2572),f6(x2571,a8,x2572))), % 60.29/60.42 inference(scs_inference,[],[41,2,14])). % 60.29/60.42 cnf(258,plain, % 60.29/60.42 (E(f6(x2581,a8,x2582),f6(x2581,f3(a1,a2,a7),x2582))), % 60.29/60.42 inference(scs_inference,[],[257,2])). % 60.29/60.42 cnf(259,plain, % 60.29/60.42 (E(f6(f3(a1,a2,a7),f3(a1,a2,a7),x2591),f6(a8,a8,x2591))), % 60.29/60.42 inference(scs_inference,[],[254,257,2,3])). % 60.29/60.42 cnf(262,plain, % 60.29/60.42 (E(f6(x2621,x2622,a8),f6(x2621,x2622,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[29,2,15])). % 60.29/60.42 cnf(263,plain, % 60.29/60.42 (E(f6(x2631,x2632,f3(a1,a2,a7)),f6(x2631,x2632,a8))), % 60.29/60.42 inference(scs_inference,[],[262,2])). % 60.29/60.42 cnf(264,plain, % 60.29/60.42 (E(f6(x2641,a8,a8),f6(x2641,f3(a1,a2,a7),f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[258,262,2,3])). % 60.29/60.42 cnf(267,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),x2671,x2672,x2673),f5(a8,x2671,x2672,x2673))), % 60.29/60.42 inference(scs_inference,[],[41,2,16])). % 60.29/60.42 cnf(268,plain, % 60.29/60.42 (E(f5(a8,x2681,x2682,x2683),f5(f3(a1,a2,a7),x2681,x2682,x2683))), % 60.29/60.42 inference(scs_inference,[],[267,2])). % 60.29/60.42 cnf(269,plain, % 60.29/60.42 (E(f6(f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7)),f6(a8,a8,a8))), % 60.29/60.42 inference(scs_inference,[],[267,263,259,2,3])). % 60.29/60.42 cnf(272,plain, % 60.29/60.42 (E(f5(x2721,a8,x2722,x2723),f5(x2721,f3(a1,a2,a7),x2722,x2723))), % 60.29/60.42 inference(scs_inference,[],[29,2,17])). % 60.29/60.42 cnf(273,plain, % 60.29/60.42 (E(f5(x2731,f3(a1,a2,a7),x2732,x2733),f5(x2731,a8,x2732,x2733))), % 60.29/60.42 inference(scs_inference,[],[272,2])). % 60.29/60.42 cnf(274,plain, % 60.29/60.42 (E(f5(a8,a8,x2741,x2742),f5(f3(a1,a2,a7),f3(a1,a2,a7),x2741,x2742))), % 60.29/60.42 inference(scs_inference,[],[268,272,2,3])). % 60.29/60.42 cnf(277,plain, % 60.29/60.42 (E(f5(x2771,x2772,f3(a1,a2,a7),x2773),f5(x2771,x2772,a8,x2773))), % 60.29/60.42 inference(scs_inference,[],[41,2,18])). % 60.29/60.42 cnf(278,plain, % 60.29/60.42 (E(f5(x2781,x2782,a8,x2783),f5(x2781,x2782,f3(a1,a2,a7),x2783))), % 60.29/60.42 inference(scs_inference,[],[277,2])). % 60.29/60.42 cnf(279,plain, % 60.29/60.42 (E(f5(x2791,f3(a1,a2,a7),f3(a1,a2,a7),x2792),f5(x2791,a8,a8,x2792))), % 60.29/60.42 inference(scs_inference,[],[273,277,2,3])). % 60.29/60.42 cnf(282,plain, % 60.29/60.42 (E(f5(x2821,x2822,x2823,a8),f5(x2821,x2822,x2823,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[29,2,19])). % 60.29/60.42 cnf(283,plain, % 60.29/60.42 (E(f5(x2831,x2832,x2833,f3(a1,a2,a7)),f5(x2831,x2832,x2833,a8))), % 60.29/60.42 inference(scs_inference,[],[282,2])). % 60.29/60.42 cnf(284,plain, % 60.29/60.42 (E(f5(x2841,x2842,a8,a8),f5(x2841,x2842,f3(a1,a2,a7),f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[278,282,2,3])). % 60.29/60.42 cnf(287,plain, % 60.29/60.42 (E(f14(f3(a1,a2,a7),x2871,x2872),f14(a8,x2871,x2872))), % 60.29/60.42 inference(scs_inference,[],[41,2,20])). % 60.29/60.42 cnf(288,plain, % 60.29/60.42 (E(f14(a8,x2881,x2882),f14(f3(a1,a2,a7),x2881,x2882))), % 60.29/60.42 inference(scs_inference,[],[287,2])). % 60.29/60.42 cnf(289,plain, % 60.29/60.42 (E(f5(x2891,f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7)),f5(x2891,a8,a8,a8))), % 60.29/60.42 inference(scs_inference,[],[283,287,279,2,3])). % 60.29/60.42 cnf(292,plain, % 60.29/60.42 (E(f14(x2921,a8,x2922),f14(x2921,f3(a1,a2,a7),x2922))), % 60.29/60.42 inference(scs_inference,[],[29,2,21])). % 60.29/60.42 cnf(293,plain, % 60.29/60.42 (E(f14(x2931,f3(a1,a2,a7),x2932),f14(x2931,a8,x2932))), % 60.29/60.42 inference(scs_inference,[],[292,2])). % 60.29/60.42 cnf(294,plain, % 60.29/60.42 (E(f14(a8,a8,x2941),f14(f3(a1,a2,a7),f3(a1,a2,a7),x2941))), % 60.29/60.42 inference(scs_inference,[],[288,292,2,3])). % 60.29/60.42 cnf(297,plain, % 60.29/60.42 (E(f14(x2971,x2972,f3(a1,a2,a7)),f14(x2971,x2972,a8))), % 60.29/60.42 inference(scs_inference,[],[41,2,22])). % 60.29/60.42 cnf(298,plain, % 60.29/60.42 (E(f14(x2981,x2982,a8),f14(x2981,x2982,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[297,2])). % 60.29/60.42 cnf(299,plain, % 60.29/60.42 (E(f14(x2991,f3(a1,a2,a7),f3(a1,a2,a7)),f14(x2991,a8,a8))), % 60.29/60.42 inference(scs_inference,[],[293,297,2,3])). % 60.29/60.42 cnf(302,plain, % 60.29/60.42 (E(f3(a8,a8,a8),f3(f3(a1,a2,a7),a8,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[255,2])). % 60.29/60.42 cnf(303,plain, % 60.29/60.42 (E(f5(a8,a8,a8,a8),f5(f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[255,274,284,2,3])). % 60.29/60.42 cnf(309,plain, % 60.29/60.42 (E(f3(f3(a1,a2,a7),f3(a1,a2,a7),a8),f3(a8,a8,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[269,225,217,2,3])). % 60.29/60.42 cnf(313,plain, % 60.29/60.42 (E(f3(a8,a8,f3(a1,a2,a7)),f3(f3(a1,a2,a7),f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[309,2])). % 60.29/60.42 cnf(314,plain, % 60.29/60.42 (E(f3(f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7)),f3(a8,a8,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[309,224,2,3])). % 60.29/60.42 cnf(318,plain, % 60.29/60.42 (E(f6(f3(a1,a2,a7),a8,a8),f6(a8,f3(a1,a2,a7),f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[314,264,254,2,3])). % 60.29/60.42 cnf(322,plain, % 60.29/60.42 (E(f6(a8,f3(a1,a2,a7),f3(a1,a2,a7)),f6(f3(a1,a2,a7),a8,a8))), % 60.29/60.42 inference(scs_inference,[],[318,2])). % 60.29/60.42 cnf(323,plain, % 60.29/60.42 (E(f6(f3(a1,a2,a7),a8,f3(a1,a2,a7)),f6(a8,f3(a1,a2,a7),f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[318,263,2,3])). % 60.29/60.42 cnf(327,plain, % 60.29/60.42 (E(f14(a8,a8,a8),f14(f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[323,298,294,2,3])). % 60.29/60.42 cnf(332,plain, % 60.29/60.42 (E(f5(a8,a8,a8,a8),f5(a8,f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[245,303,267,2,3])). % 60.29/60.42 cnf(336,plain, % 60.29/60.42 (E(f5(a8,a8,a8,a8),f5(a8,f3(a1,a2,a7),f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[332,250,283,2,3])). % 60.29/60.42 cnf(340,plain, % 60.29/60.42 (E(f10(a8,a8),f10(f3(a1,a2,a7),f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[249,327,243,2,3])). % 60.29/60.42 cnf(345,plain, % 60.29/60.42 (E(f5(a8,a8,a8,a8),f5(f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[340,336,268,2,3])). % 60.29/60.42 cnf(348,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7),a8),f5(a8,a8,a8,a8))), % 60.29/60.42 inference(scs_inference,[],[345,2])). % 60.29/60.42 cnf(349,plain, % 60.29/60.42 (E(f5(a8,f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7)),f5(f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[345,289,2,3])). % 60.29/60.42 cnf(352,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7),a8),f5(a8,f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[349,2])). % 60.29/60.42 cnf(353,plain, % 60.29/60.42 (E(f5(a8,f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7)),f5(f3(a1,a2,a7),a8,f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[349,273,2,3])). % 60.29/60.42 cnf(356,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),a8,f3(a1,a2,a7),a8),f5(a8,f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[353,2])). % 60.29/60.42 cnf(357,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),f3(a1,a2,a7),a8,a8),f5(a8,f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[352,353,278,2,3])). % 60.29/60.42 cnf(360,plain, % 60.29/60.42 (E(f5(a8,f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7)),f5(f3(a1,a2,a7),f3(a1,a2,a7),a8,a8))), % 60.29/60.42 inference(scs_inference,[],[357,2])). % 60.29/60.42 cnf(361,plain, % 60.29/60.42 (E(f5(a8,a8,f3(a1,a2,a7),a8),f5(a8,f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[357,352,274,2,3])). % 60.29/60.42 cnf(364,plain, % 60.29/60.42 (E(f5(a8,f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7)),f5(a8,a8,f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[361,2])). % 60.29/60.42 cnf(365,plain, % 60.29/60.42 (E(f5(a8,a8,f3(a1,a2,a7),a8),f5(f3(a1,a2,a7),f3(a1,a2,a7),a8,a8))), % 60.29/60.42 inference(scs_inference,[],[361,360,2,3])). % 60.29/60.42 cnf(367,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),f3(a1,a2,a7),a8,a8),f5(a8,a8,f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[365,2])). % 60.29/60.42 cnf(368,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),a8,f3(a1,a2,a7),a8),f5(f3(a1,a2,a7),f3(a1,a2,a7),a8,a8))), % 60.29/60.42 inference(scs_inference,[],[356,365,360,2,3])). % 60.29/60.42 cnf(370,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),f3(a1,a2,a7),a8,a8),f5(f3(a1,a2,a7),a8,f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[368,2])). % 60.29/60.42 cnf(371,plain, % 60.29/60.42 (E(f5(a8,a8,a8,a8),f5(f3(a1,a2,a7),a8,f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[368,332,353,2,3])). % 60.29/60.42 cnf(373,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),a8,f3(a1,a2,a7),a8),f5(a8,a8,a8,a8))), % 60.29/60.42 inference(scs_inference,[],[371,2])). % 60.29/60.42 cnf(374,plain, % 60.29/60.42 (E(f4(a8,a8,a8),f4(f3(a1,a2,a7),a8,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[371,245,234,2,3])). % 60.29/60.42 cnf(377,plain, % 60.29/60.42 (E(f4(f3(a1,a2,a7),a8,f3(a1,a2,a7)),f4(a8,a8,a8))), % 60.29/60.42 inference(scs_inference,[],[374,2])). % 60.29/60.42 cnf(378,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),f3(a1,a2,a7),a8,a8),f5(a8,a8,a8,a8))), % 60.29/60.42 inference(scs_inference,[],[373,370,374,2,3])). % 60.29/60.42 cnf(380,plain, % 60.29/60.42 (E(f4(x3801,a8,a8),f4(x3801,f3(a1,a2,a7),f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[240,2])). % 60.29/60.42 cnf(381,plain, % 60.29/60.42 (E(f14(a8,a8,a8),f14(f3(a1,a2,a7),a8,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[240,327,293,2,3])). % 60.29/60.42 cnf(384,plain, % 60.29/60.42 (E(f14(f3(a1,a2,a7),a8,f3(a1,a2,a7)),f14(a8,a8,a8))), % 60.29/60.42 inference(scs_inference,[],[381,2])). % 60.29/60.42 cnf(385,plain, % 60.29/60.42 (E(f4(f3(a1,a2,a7),a8,a8),f4(a8,f3(a1,a2,a7),f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[381,380,228,2,3])). % 60.29/60.42 cnf(389,plain, % 60.29/60.42 (E(f4(a8,f3(a1,a2,a7),f3(a1,a2,a7)),f4(f3(a1,a2,a7),a8,a8))), % 60.29/60.42 inference(scs_inference,[],[385,2])). % 60.29/60.42 cnf(393,plain, % 60.29/60.42 (E(f14(x3931,a8,a8),f14(x3931,f3(a1,a2,a7),f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[299,2])). % 60.29/60.42 cnf(394,plain, % 60.29/60.42 (E(f6(a8,f3(a1,a2,a7),f3(a1,a2,a7)),f6(f3(a1,a2,a7),f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[322,299,258,2,3])). % 60.29/60.42 cnf(398,plain, % 60.29/60.42 (E(f6(f3(a1,a2,a7),a8,f3(a1,a2,a7)),f6(f3(a1,a2,a7),f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[394,323,2,3])). % 60.29/60.42 cnf(400,plain, % 60.29/60.42 (E(f6(f3(a1,a2,a7),f3(a1,a2,a7),a8),f6(f3(a1,a2,a7),a8,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[398,2])). % 60.29/60.42 cnf(401,plain, % 60.29/60.42 (E(f14(f3(a1,a2,a7),a8,a8),f14(a8,f3(a1,a2,a7),f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[398,393,287,2,3])). % 60.29/60.42 cnf(405,plain, % 60.29/60.42 (E(f14(a8,f3(a1,a2,a7),f3(a1,a2,a7)),f14(f3(a1,a2,a7),a8,a8))), % 60.29/60.42 inference(scs_inference,[],[401,2])). % 60.29/60.42 cnf(409,plain, % 60.29/60.42 (E(f5(x4091,a8,a8,x4092),f5(x4091,f3(a1,a2,a7),f3(a1,a2,a7),x4092))), % 60.29/60.42 inference(scs_inference,[],[279,2])). % 60.29/60.42 cnf(410,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),f3(a1,a2,a7),a8,a8),f5(a8,f3(a1,a2,a7),f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[378,336,279,2,3])). % 60.29/60.42 cnf(412,plain, % 60.29/60.42 (E(f5(a8,f3(a1,a2,a7),f3(a1,a2,a7),a8),f5(f3(a1,a2,a7),f3(a1,a2,a7),a8,a8))), % 60.29/60.42 inference(scs_inference,[],[410,2])). % 60.29/60.42 cnf(413,plain, % 60.29/60.42 (E(f5(a8,a8,a8,f3(a1,a2,a7)),f5(a8,a8,f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[364,410,409,2,3])). % 60.29/60.42 cnf(416,plain, % 60.29/60.42 (E(f5(a8,a8,f3(a1,a2,a7),a8),f5(a8,a8,a8,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[413,2])). % 60.29/60.42 cnf(417,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),a8,a8,f3(a1,a2,a7)),f5(a8,a8,f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[413,267,2,3])). % 60.29/60.42 cnf(420,plain, % 60.29/60.42 (E(f5(a8,a8,f3(a1,a2,a7),a8),f5(f3(a1,a2,a7),a8,a8,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[417,2])). % 60.29/60.42 cnf(421,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),f3(a1,a2,a7),a8,a8),f5(a8,a8,a8,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[367,416,417,2,3])). % 60.29/60.42 cnf(423,plain, % 60.29/60.42 (E(f5(a8,a8,a8,f3(a1,a2,a7)),f5(f3(a1,a2,a7),f3(a1,a2,a7),a8,a8))), % 60.29/60.42 inference(scs_inference,[],[421,2])). % 60.29/60.42 cnf(424,plain, % 60.29/60.42 (E(f5(a8,f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7)),f5(f3(a1,a2,a7),a8,a8,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[420,421,364,2,3])). % 60.29/60.42 cnf(426,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),a8,a8,f3(a1,a2,a7)),f5(a8,f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[424,2])). % 60.29/60.42 cnf(427,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),f3(a1,a2,a7),a8,a8),f5(f3(a1,a2,a7),a8,a8,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[424,357,2,3])). % 60.29/60.42 cnf(429,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),a8,a8,f3(a1,a2,a7)),f5(f3(a1,a2,a7),f3(a1,a2,a7),a8,a8))), % 60.29/60.42 inference(scs_inference,[],[427,2])). % 60.29/60.42 cnf(430,plain, % 60.29/60.42 (E(f5(a8,f3(a1,a2,a7),f3(a1,a2,a7),a8),f5(f3(a1,a2,a7),a8,a8,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[427,412,2,3])). % 60.29/60.42 cnf(432,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),a8,a8,f3(a1,a2,a7)),f5(a8,f3(a1,a2,a7),f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[430,2])). % 60.29/60.42 cnf(433,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),a8,a8,f3(a1,a2,a7)),f5(f3(a1,a2,a7),a8,f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[430,429,370,2,3])). % 60.29/60.42 cnf(435,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),a8,f3(a1,a2,a7),a8),f5(f3(a1,a2,a7),a8,a8,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[433,2])). % 60.29/60.42 cnf(436,plain, % 60.29/60.42 (E(f5(a8,f3(a1,a2,a7),f3(a1,a2,a7),a8),f5(f3(a1,a2,a7),a8,f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[433,430,2,3])). % 60.29/60.42 cnf(438,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),a8,f3(a1,a2,a7),a8),f5(a8,f3(a1,a2,a7),f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[436,2])). % 60.29/60.42 cnf(439,plain, % 60.29/60.42 (E(f5(a8,a8,a8,f3(a1,a2,a7)),f5(a8,f3(a1,a2,a7),f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[436,423,410,2,3])). % 60.29/60.42 cnf(441,plain, % 60.29/60.42 (E(f5(a8,f3(a1,a2,a7),f3(a1,a2,a7),a8),f5(a8,a8,a8,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[439,2])). % 60.29/60.42 cnf(442,plain, % 60.29/60.42 (E(f5(a8,a8,a8,a8),f5(f3(a1,a2,a7),a8,a8,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[439,435,371,2,3])). % 60.29/60.42 cnf(444,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),a8,a8,f3(a1,a2,a7)),f5(a8,a8,a8,a8))), % 60.29/60.42 inference(scs_inference,[],[442,2])). % 60.29/60.42 cnf(445,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7),a8),f5(f3(a1,a2,a7),a8,a8,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[442,348,2,3])). % 60.29/60.42 cnf(447,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),a8,a8,f3(a1,a2,a7)),f5(f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[445,2])). % 60.29/60.42 cnf(448,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),a8,f3(a1,a2,a7),a8),f5(a8,a8,a8,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[438,445,441,2,3])). % 60.29/60.42 cnf(450,plain, % 60.29/60.42 (E(f5(a8,a8,a8,f3(a1,a2,a7)),f5(f3(a1,a2,a7),a8,f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[448,2])). % 60.29/60.42 cnf(451,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7),a8),f5(a8,a8,f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[448,445,417,2,3])). % 60.29/60.42 cnf(453,plain, % 60.29/60.42 (E(f5(x4531,x4532,f3(a1,a2,a7),f3(a1,a2,a7)),f5(x4531,x4532,a8,a8))), % 60.29/60.42 inference(scs_inference,[],[284,2])). % 60.29/60.42 cnf(454,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7),a8),f5(a8,a8,a8,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[451,416,284,2,3])). % 60.29/60.42 cnf(456,plain, % 60.29/60.42 (E(f5(a8,a8,a8,f3(a1,a2,a7)),f5(f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[454,2])). % 60.29/60.42 cnf(457,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),a8,a8,f3(a1,a2,a7)),f5(a8,f3(a1,a2,a7),a8,a8))), % 60.29/60.42 inference(scs_inference,[],[454,426,453,2,3])). % 60.29/60.42 cnf(460,plain, % 60.29/60.42 (E(f5(a8,f3(a1,a2,a7),a8,a8),f5(f3(a1,a2,a7),a8,a8,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[457,2])). % 60.29/60.42 cnf(461,plain, % 60.29/60.42 (E(f5(a8,a8,f3(a1,a2,a7),a8),f5(a8,f3(a1,a2,a7),a8,a8))), % 60.29/60.42 inference(scs_inference,[],[457,420,2,3])). % 60.29/60.42 cnf(463,plain, % 60.29/60.42 (E(f5(a8,f3(a1,a2,a7),a8,a8),f5(a8,a8,f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[461,2])). % 60.29/60.42 cnf(464,plain, % 60.29/60.42 (E(f5(a8,f3(a1,a2,a7),a8,a8),f5(f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[461,447,460,2,3])). % 60.29/60.42 cnf(466,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7),a8),f5(a8,f3(a1,a2,a7),a8,a8))), % 60.29/60.42 inference(scs_inference,[],[464,2])). % 60.29/60.42 cnf(467,plain, % 60.29/60.42 (E(f5(a8,f3(a1,a2,a7),a8,a8),f5(a8,a8,a8,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[464,454,2,3])). % 60.29/60.42 cnf(469,plain, % 60.29/60.42 (E(f5(a8,a8,a8,f3(a1,a2,a7)),f5(a8,f3(a1,a2,a7),a8,a8))), % 60.29/60.42 inference(scs_inference,[],[467,2])). % 60.29/60.42 cnf(470,plain, % 60.29/60.42 (E(f5(a8,f3(a1,a2,a7),a8,a8),f5(f3(a1,a2,a7),a8,f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[450,467,2,3])). % 60.29/60.42 cnf(472,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),a8,f3(a1,a2,a7),a8),f5(a8,f3(a1,a2,a7),a8,a8))), % 60.29/60.42 inference(scs_inference,[],[470,2])). % 60.29/60.42 cnf(476,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7)),f5(a8,a8,a8,a8))), % 60.29/60.42 inference(scs_inference,[],[303,2])). % 60.29/60.42 cnf(477,plain, % 60.29/60.42 (E(f3(a8,a8,a8),f3(a8,f3(a1,a2,a7),f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[302,303,220,2,3])). % 60.29/60.42 cnf(480,plain, % 60.29/60.42 (E(f3(a8,f3(a1,a2,a7),f3(a1,a2,a7)),f3(a8,a8,a8))), % 60.29/60.42 inference(scs_inference,[],[477,2])). % 60.29/60.42 cnf(481,plain, % 60.29/60.42 (E(f3(a8,a8,a8),f3(f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[477,216,2,3])). % 60.29/60.42 cnf(485,plain, % 60.29/60.42 (E(f3(a8,f3(a1,a2,a7),f3(a1,a2,a7)),f3(f3(a1,a2,a7),a8,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[481,480,302,2,3])). % 60.29/60.42 cnf(487,plain, % 60.29/60.42 (E(f3(x4871,a8,f3(a1,a2,a7)),f3(x4871,f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[225,2])). % 60.29/60.42 cnf(488,plain, % 60.29/60.42 (E(f4(f3(a1,a2,a7),a8,f3(a1,a2,a7)),f4(f3(a1,a2,a7),f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[377,225,235,2,3])). % 60.29/60.42 cnf(491,plain, % 60.29/60.42 (E(f4(f3(a1,a2,a7),f3(a1,a2,a7),a8),f4(f3(a1,a2,a7),a8,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[488,2])). % 60.29/60.42 cnf(492,plain, % 60.29/60.42 (E(f3(a8,f3(a1,a2,a7),f3(a1,a2,a7)),f3(f3(a1,a2,a7),f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[485,488,487,2,3])). % 60.29/60.42 cnf(496,plain, % 60.29/60.42 (E(f3(a8,a8,a8),f3(f3(a1,a2,a7),f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[492,477,2,3])). % 60.29/60.42 cnf(499,plain, % 60.29/60.42 (E(f4(f3(a1,a2,a7),f3(a1,a2,a7),a8),f4(a8,a8,a8))), % 60.29/60.42 inference(scs_inference,[],[496,491,377,2,3])). % 60.29/60.42 cnf(500,plain, % 60.29/60.42 (E(f6(a8,a8,x5001),f6(f3(a1,a2,a7),f3(a1,a2,a7),x5001))), % 60.29/60.42 inference(scs_inference,[],[259,2])). % 60.29/60.42 cnf(501,plain, % 60.29/60.42 (E(f14(f3(a1,a2,a7),a8,f3(a1,a2,a7)),f14(f3(a1,a2,a7),f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[384,259,294,2,3])). % 60.29/60.42 cnf(504,plain, % 60.29/60.42 (E(f14(f3(a1,a2,a7),f3(a1,a2,a7),a8),f14(f3(a1,a2,a7),a8,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[501,2])). % 60.29/60.42 cnf(505,plain, % 60.29/60.42 (E(f6(a8,a8,a8),f6(f3(a1,a2,a7),a8,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[400,501,500,2,3])). % 60.29/60.42 cnf(508,plain, % 60.29/60.42 (E(f6(f3(a1,a2,a7),a8,f3(a1,a2,a7)),f6(a8,a8,a8))), % 60.29/60.42 inference(scs_inference,[],[505,2])). % 60.29/60.42 cnf(512,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),a8,f3(a1,a2,a7),a8),f5(a8,f3(a1,a2,a7),a8,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[472,264,282,2,3])). % 60.29/60.42 cnf(515,plain, % 60.29/60.42 (E(f5(a8,f3(a1,a2,a7),a8,f3(a1,a2,a7)),f5(f3(a1,a2,a7),a8,f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[512,2])). % 60.29/60.42 cnf(516,plain, % 60.29/60.42 (E(f4(f3(a1,a2,a7),a8,a8),f4(a8,a8,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[512,385,234,2,3])). % 60.29/60.42 cnf(519,plain, % 60.29/60.42 (E(f5(a8,f3(a1,a2,a7),a8,f3(a1,a2,a7)),f5(a8,f3(a1,a2,a7),f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[516,515,438,2,3])). % 60.29/60.42 cnf(522,plain, % 60.29/60.42 (E(f5(a8,f3(a1,a2,a7),f3(a1,a2,a7),a8),f5(a8,f3(a1,a2,a7),a8,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[519,2])). % 60.29/60.42 cnf(523,plain, % 60.29/60.42 (E(f14(f3(a1,a2,a7),a8,a8),f14(a8,a8,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[519,401,293,2,3])). % 60.29/60.42 cnf(528,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),a8,a8,f3(a1,a2,a7)),f5(a8,f3(a1,a2,a7),a8,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[432,523,522,2,3])). % 60.29/60.42 cnf(531,plain, % 60.29/60.42 (E(f5(a8,f3(a1,a2,a7),a8,f3(a1,a2,a7)),f5(f3(a1,a2,a7),a8,a8,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[528,2])). % 60.29/60.42 cnf(532,plain, % 60.29/60.42 (E(f4(a8,f3(a1,a2,a7),f3(a1,a2,a7)),f4(f3(a1,a2,a7),f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[389,528,233,2,3])). % 60.29/60.42 cnf(536,plain, % 60.29/60.42 (E(f5(a8,f3(a1,a2,a7),a8,f3(a1,a2,a7)),f5(a8,a8,a8,a8))), % 60.29/60.42 inference(scs_inference,[],[444,532,531,2,3])). % 60.29/60.42 cnf(538,plain, % 60.29/60.42 (E(f5(a8,a8,a8,a8),f5(a8,f3(a1,a2,a7),a8,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[536,2])). % 60.29/60.42 cnf(539,plain, % 60.29/60.42 (E(f4(a8,f3(a1,a2,a7),f3(a1,a2,a7)),f4(f3(a1,a2,a7),a8,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[536,491,532,2,3])). % 60.29/60.42 cnf(541,plain, % 60.29/60.42 (E(f4(f3(a1,a2,a7),a8,f3(a1,a2,a7)),f4(a8,f3(a1,a2,a7),f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[539,2])). % 60.29/60.42 cnf(542,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7)),f5(a8,f3(a1,a2,a7),a8,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[539,476,538,2,3])). % 60.29/60.42 cnf(544,plain, % 60.29/60.42 (E(f5(a8,f3(a1,a2,a7),a8,f3(a1,a2,a7)),f5(f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[542,2])). % 60.29/60.42 cnf(545,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7)),f5(a8,f3(a1,a2,a7),f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[542,519,2,3])). % 60.29/60.42 cnf(547,plain, % 60.29/60.42 (E(f5(a8,f3(a1,a2,a7),f3(a1,a2,a7),a8),f5(f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[545,2])). % 60.29/60.42 cnf(548,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7)),f5(a8,a8,a8,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[545,441,2,3])). % 60.29/60.42 cnf(550,plain, % 60.29/60.42 (E(f5(a8,a8,a8,f3(a1,a2,a7)),f5(f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[548,2])). % 60.29/60.42 cnf(551,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7)),f5(a8,f3(a1,a2,a7),a8,a8))), % 60.29/60.42 inference(scs_inference,[],[469,548,2,3])). % 60.29/60.42 cnf(553,plain, % 60.29/60.42 (E(f5(a8,f3(a1,a2,a7),a8,a8),f5(f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[551,2])). % 60.29/60.42 cnf(554,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7)),f5(a8,a8,f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[463,551,2,3])). % 60.29/60.42 cnf(555,plain, % 60.29/60.42 (E(f5(a8,a8,f3(a1,a2,a7),a8),f5(f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[554,2])). % 60.29/60.42 cnf(556,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),a8,f3(a1,a2,a7),a8),f5(f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[554,550,448,2,3])). % 60.29/60.42 cnf(558,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7)),f5(f3(a1,a2,a7),a8,f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[556,2])). % 60.29/60.42 cnf(559,plain, % 60.29/60.42 (E(f4(f3(a1,a2,a7),a8,f3(a1,a2,a7)),f4(a8,f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[541,556,238,2,3])). % 60.29/60.42 cnf(563,plain, % 60.29/60.42 (E(f5(a8,f3(a1,a2,a7),a8,a8),f5(f3(a1,a2,a7),a8,a8,a8))), % 60.29/60.42 inference(scs_inference,[],[553,559,289,2,3])). % 60.29/60.42 cnf(565,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),a8,a8,a8),f5(a8,f3(a1,a2,a7),a8,a8))), % 60.29/60.42 inference(scs_inference,[],[563,2])). % 60.29/60.42 cnf(566,plain, % 60.29/60.42 (E(f6(f3(a1,a2,a7),a8,f3(a1,a2,a7)),f6(a8,f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[563,508,258,2,3])). % 60.29/60.42 cnf(570,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),a8,a8,a8),f5(a8,a8,f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[565,566,463,2,3])). % 60.29/60.42 cnf(572,plain, % 60.29/60.42 (E(f5(a8,a8,f3(a1,a2,a7),a8),f5(f3(a1,a2,a7),a8,a8,a8))), % 60.29/60.42 inference(scs_inference,[],[570,2])). % 60.29/60.42 cnf(573,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),a8,a8,a8),f5(f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[570,555,2,3])). % 60.29/60.42 cnf(576,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),a8,a8,a8),f5(a8,f3(a1,a2,a7),f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[573,545,243,2,3])). % 60.29/60.42 cnf(578,plain, % 60.29/60.42 (E(f5(a8,f3(a1,a2,a7),f3(a1,a2,a7),a8),f5(f3(a1,a2,a7),a8,a8,a8))), % 60.29/60.42 inference(scs_inference,[],[576,2])). % 60.29/60.42 cnf(579,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),a8,a8,a8),f5(a8,f3(a1,a2,a7),a8,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[576,522,2,3])). % 60.29/60.42 cnf(581,plain, % 60.29/60.42 (E(f5(a8,f3(a1,a2,a7),a8,f3(a1,a2,a7)),f5(f3(a1,a2,a7),a8,a8,a8))), % 60.29/60.42 inference(scs_inference,[],[579,2])). % 60.29/60.42 cnf(582,plain, % 60.29/60.42 (E(f5(a8,a8,a8,f3(a1,a2,a7)),f5(f3(a1,a2,a7),a8,a8,a8))), % 60.29/60.42 inference(scs_inference,[],[578,579,439,2,3])). % 60.29/60.42 cnf(584,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),a8,a8,a8),f5(a8,a8,a8,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[582,2])). % 60.29/60.42 cnf(585,plain, % 60.29/60.42 (E(f5(a8,a8,f3(a1,a2,a7),a8),f5(a8,f3(a1,a2,a7),a8,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[572,582,579,2,3])). % 60.29/60.42 cnf(588,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),f3(a1,a2,a7),a8,a8),f5(a8,f3(a1,a2,a7),a8,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[585,367,2,3])). % 60.29/60.42 cnf(590,plain, % 60.29/60.42 (E(f5(a8,f3(a1,a2,a7),a8,f3(a1,a2,a7)),f5(f3(a1,a2,a7),f3(a1,a2,a7),a8,a8))), % 60.29/60.42 inference(scs_inference,[],[588,2])). % 60.29/60.42 cnf(591,plain, % 60.29/60.42 (E(f5(a8,f3(a1,a2,a7),a8,f3(a1,a2,a7)),f5(f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[588,581,409,2,3])). % 60.29/60.42 cnf(593,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7),a8),f5(a8,f3(a1,a2,a7),a8,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[591,2])). % 60.29/60.42 cnf(594,plain, % 60.29/60.42 (E(f4(f3(a1,a2,a7),f3(a1,a2,a7),a8),f4(a8,a8,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[499,591,239,2,3])). % 60.29/60.42 cnf(598,plain, % 60.29/60.42 (E(f5(a8,f3(a1,a2,a7),a8,f3(a1,a2,a7)),f5(f3(a1,a2,a7),a8,f3(a1,a2,a7),f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[544,594,273,2,3])). % 60.29/60.42 cnf(601,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),a8,f3(a1,a2,a7),f3(a1,a2,a7)),f5(a8,f3(a1,a2,a7),a8,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[598,2])). % 60.29/60.42 cnf(602,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7),a8),f5(f3(a1,a2,a7),a8,f3(a1,a2,a7),f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[593,598,2,3])). % 60.29/60.42 cnf(605,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),a8,f3(a1,a2,a7),f3(a1,a2,a7)),f5(f3(a1,a2,a7),f3(a1,a2,a7),a8,a8))), % 60.29/60.42 inference(scs_inference,[],[590,602,601,2,3])). % 60.29/60.42 cnf(608,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),a8,f3(a1,a2,a7),f3(a1,a2,a7)),f5(a8,a8,a8,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[605,421,2,3])). % 60.29/60.42 cnf(611,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),a8,f3(a1,a2,a7),f3(a1,a2,a7)),f5(a8,f3(a1,a2,a7),a8,a8))), % 60.29/60.42 inference(scs_inference,[],[608,469,2,3])). % 60.29/60.42 cnf(614,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),a8,f3(a1,a2,a7),f3(a1,a2,a7)),f5(a8,a8,f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[611,463,2,3])). % 60.29/60.42 cnf(617,plain, % 60.29/60.42 (E(f3(a8,a8,f3(a1,a2,a7)),f3(f3(a1,a2,a7),a8,a8))), % 60.29/60.42 inference(scs_inference,[],[313,614,219,2,3])). % 60.29/60.42 cnf(619,plain, % 60.29/60.42 (E(f3(f3(a1,a2,a7),a8,a8),f3(a8,a8,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[617,2])). % 60.29/60.42 cnf(620,plain, % 60.29/60.42 (E(f3(f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7)),f3(f3(a1,a2,a7),a8,a8))), % 60.29/60.42 inference(scs_inference,[],[617,314,2,3])). % 60.29/60.42 cnf(623,plain, % 60.29/60.42 (E(f3(f3(a1,a2,a7),a8,a8),f3(a8,f3(a1,a2,a7),f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[619,620,218,2,3])). % 60.29/60.42 cnf(627,plain, % 60.29/60.42 (E(f14(a8,f3(a1,a2,a7),f3(a1,a2,a7)),f14(f3(a1,a2,a7),f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[405,623,292,2,3])). % 60.29/60.42 cnf(631,plain, % 60.29/60.42 (E(f14(a8,f3(a1,a2,a7),f3(a1,a2,a7)),f14(f3(a1,a2,a7),a8,f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[627,504,2,3])). % 60.29/60.42 cnf(634,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),a8,a8,a8),f5(a8,f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[631,584,409,2,3])). % 60.29/60.42 cnf(637,plain, % 60.29/60.42 (E(f5(a8,f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7)),f5(f3(a1,a2,a7),a8,a8,a8))), % 60.29/60.42 inference(scs_inference,[],[634,2])). % 60.29/60.42 cnf(638,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),a8,a8,a8),f5(a8,a8,f3(a1,a2,a7),f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[634,273,2,3])). % 60.29/60.42 cnf(641,plain, % 60.29/60.42 (E(f5(a8,a8,f3(a1,a2,a7),f3(a1,a2,a7)),f5(f3(a1,a2,a7),a8,a8,a8))), % 60.29/60.42 inference(scs_inference,[],[638,2])). % 60.29/60.42 cnf(642,plain, % 60.29/60.42 (E(f5(a8,f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7)),f5(f3(a1,a2,a7),a8,f3(a1,a2,a7),f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[637,638,284,2,3])). % 60.29/60.42 cnf(646,plain, % 60.29/60.42 (E(f5(a8,a8,f3(a1,a2,a7),f3(a1,a2,a7)),f5(a8,f3(a1,a2,a7),a8,a8))), % 60.29/60.42 inference(scs_inference,[],[642,641,565,2,3])). % 60.29/60.42 cnf(648,plain, % 60.29/60.42 (E(f5(a8,f3(a1,a2,a7),a8,a8),f5(a8,a8,f3(a1,a2,a7),f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[646,2])). % 60.29/60.42 cnf(649,plain, % 60.29/60.42 (E(f5(a8,a8,f3(a1,a2,a7),f3(a1,a2,a7)),f5(f3(a1,a2,a7),a8,f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[646,470,2,3])). % 60.29/60.42 cnf(650,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),a8,f3(a1,a2,a7),a8),f5(a8,a8,f3(a1,a2,a7),f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[649,2])). % 60.29/60.42 cnf(651,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7),a8),f5(a8,a8,f3(a1,a2,a7),f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[649,648,466,2,3])). % 60.29/60.42 cnf(652,plain, % 60.29/60.42 (~E(a13,x6521)+P2(f14(x6521,a11,a12),a11,a2)+P2(f5(f6(a11,a1,a2),x6521,a2,a2),a12,f10(a2,a2))), % 60.29/60.42 inference(scs_inference,[],[31,87,36])). % 60.29/60.42 cnf(653,plain, % 60.29/60.42 (P2(f5(f6(a11,a1,a2),a13,a2,a2),a12,f10(a2,a2))+P2(f14(a13,a11,a12),a11,a2)), % 60.29/60.42 inference(equality_inference,[],[652])). % 60.29/60.42 cnf(655,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7)),f5(a8,a8,f3(a1,a2,a7),f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[651,650,558,2,3])). % 60.29/60.42 cnf(656,plain, % 60.29/60.42 (P2(f14(a13,a11,a12),a11,a2)), % 60.29/60.42 inference(scs_inference,[],[103,49,653,27])). % 60.29/60.42 cnf(661,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),f3(a1,a2,a7),x6611,x6612),f5(a8,a8,x6611,x6612))), % 60.29/60.42 inference(scs_inference,[],[656,274,43,50,2])). % 60.29/60.42 cnf(662,plain, % 60.29/60.42 (E(f5(a8,f3(a1,a2,a7),f3(a1,a2,a7),a8),f5(a8,a8,f3(a1,a2,a7),f3(a1,a2,a7)))), % 60.29/60.42 inference(scs_inference,[],[656,655,547,274,43,50,2,3])). % 60.29/60.42 cnf(666,plain, % 60.29/60.42 (P2(f5(f14(a13,a11,a12),a13,a2,a2),a12,f10(a2,a2))+P2(a13,a11,a2)), % 60.29/60.42 inference(scs_inference,[],[103,656,30,655,547,274,43,50,2,3,34,26,27])). % 60.29/60.42 cnf(667,plain, % 60.29/60.42 (~E(f14(a13,a11,a12),f6(a11,a1,a2))+P2(a13,a11,a2)), % 60.29/60.42 inference(scs_inference,[],[103,656,30,655,547,274,43,50,2,3,34,26,27,16])). % 60.29/60.42 cnf(670,plain, % 60.29/60.42 (~E(f14(a13,a11,a12),f6(a11,a1,a2))+P2(f5(a13,f6(a11,a1,a2),a2,a2),a12,f10(a2,a2))), % 60.29/60.42 inference(scs_inference,[],[31,667,35])). % 60.29/60.42 cnf(671,plain, % 60.29/60.42 (E(f5(a8,a8,f3(a1,a2,a7),f3(a1,a2,a7)),f5(a8,f3(a1,a2,a7),f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[662,2])). % 60.29/60.42 cnf(672,plain, % 60.29/60.42 (E(f5(f3(a1,a2,a7),f3(a1,a2,a7),a8,f3(a1,a2,a7)),f5(f3(a1,a2,a7),f3(a1,a2,a7),f3(a1,a2,a7),a8))), % 60.29/60.42 inference(scs_inference,[],[456,662,661,2,3])). % 60.29/60.42 cnf(680,plain, % 60.29/60.42 (P2(x6801,a11,a2)+~E(f14(a13,a11,a12),x6801)), % 60.29/60.42 inference(scs_inference,[],[656,671,672,412,2,3,26])). % 60.29/60.42 cnf(746,plain, % 60.29/60.42 (P2(f5(f14(a13,a11,a12),a13,a2,a2),a12,f10(a2,a2))+P2(f5(a13,f6(a11,a1,a2),a2,a2),a12,f10(a2,a2))), % 60.29/60.42 inference(scs_inference,[],[31,666,35])). % 60.29/60.42 cnf(766,plain, % 60.29/60.42 (P2(f5(a13,f6(a11,a1,a2),a2,a2),f4(a1,a2,a7),f10(a2,a2))+~E(f14(a13,a11,a12),f6(a11,a1,a2))), % 60.29/60.42 inference(scs_inference,[],[49,670,27])). % 60.29/60.42 cnf(768,plain, % 60.29/60.42 (~P2(f6(a11,a1,a2),a11,a2)+~E(f14(a13,a11,a12),f6(a11,a1,a2))), % 60.29/60.42 inference(scs_inference,[],[766,213])). % 60.29/60.42 cnf(769,plain, % 60.29/60.42 (~E(f14(a13,a11,a12),f6(a11,a1,a2))), % 60.29/60.42 inference(scs_inference,[],[768,680])). % 60.29/60.42 cnf(784,plain, % 60.29/60.42 (P2(f5(a13,f6(a11,a1,a2),a2,a2),f4(a1,a2,a7),f10(a2,a2))+P2(f5(f14(a13,a11,a12),a13,a2,a2),a12,f10(a2,a2))), % 60.29/60.42 inference(scs_inference,[],[49,746,27])). % 60.29/60.42 cnf(1390,plain, % 60.29/60.42 (E(f3(f4(a1,a2,a7),x13901,x13902),f3(a12,x13901,x13902))), % 60.29/60.42 inference(scs_inference,[],[30,10,11,12,4])). % 60.29/60.42 cnf(1391,plain, % 60.29/60.42 (E(f3(x13911,f4(a1,a2,a7),x13912),f3(x13911,a12,x13912))), % 60.29/60.42 inference(scs_inference,[],[30,10,11,12,4,5])). % 60.29/60.42 cnf(1404,plain, % 60.29/60.42 (E(f5(x14041,x14042,x14043,f4(a1,a2,a7)),f5(x14041,x14042,x14043,a12))), % 60.29/60.42 inference(scs_inference,[],[30,10,11,12,4,5,6,7,8,9,13,14,15,20,21,22,17,18,19])). % 60.29/60.42 cnf(1405,plain, % 60.29/60.42 (E(f5(f4(a1,a2,a7),x14051,x14052,x14053),f5(a12,x14051,x14052,x14053))), % 60.29/60.42 inference(scs_inference,[],[30,10,11,12,4,5,6,7,8,9,13,14,15,20,21,22,17,18,19,16])). % 60.29/60.42 cnf(1409,plain, % 60.29/60.42 (~P2(f5(f6(a11,a1,a2),a13,a2,a2),a12,f10(a2,a2))), % 60.29/60.42 inference(scs_inference,[],[769,103,656,31,30,49,10,11,12,4,5,6,7,8,9,13,14,15,20,21,22,17,18,19,16,2,35,27])). % 60.29/60.42 cnf(1414,plain, % 60.29/60.42 (P2(f5(f14(a13,a11,a12),a13,a2,a2),f4(a1,a2,a7),f10(a2,a2))+~P2(f5(a13,f6(a11,a1,a2),a2,a2),f4(a1,a2,a7),f10(a2,a2))), % 60.29/60.42 inference(scs_inference,[],[769,248,103,656,31,30,49,10,11,12,4,5,6,7,8,9,13,14,15,20,21,22,17,18,19,16,2,35,27,3,33,38])). % 60.29/60.42 cnf(1454,plain, % 60.29/60.42 (~P2(f5(f14(a13,a11,a12),a13,a2,a2),a12,f10(a2,a2))), % 60.29/60.42 inference(scs_inference,[],[1404,1405,1409,81,31,3,39])). % 60.29/60.42 cnf(1463,plain, % 60.29/60.42 (P2(f5(a13,f6(a11,a1,a2),a2,a2),f4(a1,a2,a7),f10(a2,a2))), % 60.29/60.42 inference(scs_inference,[],[1454,784])). % 60.29/60.42 cnf(1470,plain, % 60.29/60.42 (~P2(f5(a13,f6(a11,a1,a2),a2,a2),f4(a1,a2,a7),f10(a2,a2))), % 60.29/60.42 inference(scs_inference,[],[1390,1391,1454,30,27,3,1414])). % 60.29/60.42 cnf(1475,plain, % 60.29/60.42 ($false), % 60.29/60.42 inference(scs_inference,[],[1463,1470]), % 60.29/60.42 ['proof']). % 60.29/60.42 % SZS output end Proof % 60.29/60.42 % Total time :59.710000s %------------------------------------------------------------------------------