%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : ANA015-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 : n025.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 04:13:53 EDT 2024 % Result : Unsatisfiable 262.69s 262.69s % Output : CNFRefutation 262.80s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : ANA015-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.13/0.34 % Computer : n025.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Sun Jun 23 04:45:09 EDT 2024 % 0.13/0.34 % CPUTime : % 0.52/0.57 start to proof:theBenchmark % 262.65/262.67 %------------------------------------------- % 262.65/262.67 % File :CSE---1.7 % 262.65/262.67 % Problem :theBenchmark % 262.65/262.67 % Transform :cnf % 262.65/262.67 % Format :tptp:raw % 262.65/262.67 % Command :java -jar mcs_scs.jar %d %s % 262.65/262.67 % 262.65/262.67 % Result :Theorem 261.940000s % 262.65/262.67 % Output :CNFRefutation 261.940000s % 262.65/262.67 %------------------------------------------- % 262.69/262.69 %------------------------------------------------------------------------------ % 262.69/262.69 % File : ANA015-2 : TPTP v8.2.0. Released v3.2.0. % 262.69/262.69 % Domain : Analysis % 262.69/262.69 % Problem : Problem about Big-O notation % 262.69/262.69 % Version : [Pau06] axioms : Reduced > Especial. % 262.69/262.69 % English : % 262.69/262.69 % 262.69/262.69 % Refs : [Pau06] Paulson (2006), Email to G. Sutcliffe % 262.69/262.69 % Source : [Pau06] % 262.69/262.69 % Names : % 262.69/262.69 % 262.69/262.69 % Status : Unsatisfiable % 262.69/262.69 % Rating : 0.12 v8.2.0, 0.08 v8.1.0, 0.00 v7.5.0, 0.10 v7.4.0, 0.22 v7.3.0, 0.33 v7.2.0, 0.25 v7.1.0, 0.29 v7.0.0, 0.14 v6.3.0, 0.00 v6.0.0, 0.11 v5.5.0, 0.06 v5.4.0, 0.07 v5.3.0, 0.17 v5.2.0, 0.12 v5.1.0, 0.14 v4.1.0, 0.22 v4.0.1, 0.17 v3.3.0, 0.29 v3.2.0 % 262.69/262.69 % Syntax : Number of clauses : 12 ( 3 unt; 0 nHn; 8 RR) % 262.69/262.69 % Number of literals : 23 ( 2 equ; 12 neg) % 262.69/262.69 % Maximal clause size : 4 ( 1 avg) % 262.69/262.69 % Maximal term depth : 5 ( 1 avg) % 262.69/262.69 % Number of predicates : 8 ( 7 usr; 0 prp; 1-3 aty) % 262.69/262.69 % Number of functors : 10 ( 10 usr; 4 con; 0-3 aty) % 262.69/262.69 % Number of variables : 20 ( 1 sgn) % 262.69/262.69 % SPC : CNF_UNS_RFO_SEQ_HRN % 262.69/262.69 % 262.69/262.69 % Comments : The problems in the [Pau06] collection each have very many axioms, % 262.69/262.69 % of which only a small selection are required for the refutation. % 262.69/262.69 % The mission is to find those few axioms, after which a refutation % 262.69/262.69 % can be quite easily found. This version has only the necessary % 262.69/262.69 % axioms. % 262.69/262.69 %------------------------------------------------------------------------------ % 262.69/262.69 cnf(cls_OrderedGroup_Oabs__ge__zero_0,axiom, % 262.69/262.69 ( ~ class_OrderedGroup_Olordered__ab__group__abs(T_a) % 262.69/262.69 | c_lessequals(c_0,c_HOL_Oabs(V_a,T_a),T_a) ) ). % 262.69/262.69 % 262.69/262.69 cnf(cls_OrderedGroup_Osemigroup__mult__class_Omult__assoc_0,axiom, % 262.69/262.69 ( ~ class_OrderedGroup_Osemigroup__mult(T_a) % 262.69/262.69 | c_times(c_times(V_a,V_b,T_a),V_c,T_a) = c_times(V_a,c_times(V_b,V_c,T_a),T_a) ) ). % 262.69/262.69 % 262.69/262.69 cnf(cls_Ring__and__Field_Oabs__mult_0,axiom, % 262.69/262.69 ( ~ class_Ring__and__Field_Oordered__idom(T_a) % 262.69/262.69 | c_HOL_Oabs(c_times(V_a,V_b,T_a),T_a) = c_times(c_HOL_Oabs(V_a,T_a),c_HOL_Oabs(V_b,T_a),T_a) ) ). % 262.69/262.69 % 262.69/262.69 cnf(cls_Ring__and__Field_Opordered__semiring__class_Omult__left__mono_0,axiom, % 262.69/262.69 ( ~ class_Ring__and__Field_Opordered__semiring(T_a) % 262.69/262.69 | ~ c_lessequals(V_a,V_b,T_a) % 262.69/262.69 | ~ c_lessequals(c_0,V_c,T_a) % 262.69/262.69 | c_lessequals(c_times(V_c,V_a,T_a),c_times(V_c,V_b,T_a),T_a) ) ). % 262.69/262.69 % 262.69/262.69 cnf(cls_conjecture_1,negated_conjecture, % 262.69/262.69 c_lessequals(c_HOL_Oabs(v_g(V_U),t_a),c_times(v_d,c_HOL_Oabs(v_f(V_U),t_a),t_a),t_a) ). % 262.69/262.69 % 262.69/262.69 cnf(cls_conjecture_2,negated_conjecture, % 262.69/262.69 ~ c_lessequals(c_HOL_Oabs(c_times(c_HOL_Oinverse(v_c,t_a),v_g(v_x(V_U)),t_a),t_a),c_times(V_U,c_HOL_Oabs(v_f(v_x(V_U)),t_a),t_a),t_a) ). % 262.69/262.69 % 262.69/262.69 cnf(clsrel_Ring__and__Field_Ofield_21,axiom, % 262.69/262.69 ( ~ class_Ring__and__Field_Ofield(T) % 262.69/262.69 | class_OrderedGroup_Osemigroup__mult(T) ) ). % 262.69/262.69 % 262.69/262.69 cnf(clsrel_Ring__and__Field_Oordered__field_0,axiom, % 262.69/262.69 ( ~ class_Ring__and__Field_Oordered__field(T) % 262.69/262.69 | class_Ring__and__Field_Ofield(T) ) ). % 262.69/262.69 % 262.69/262.69 cnf(clsrel_Ring__and__Field_Oordered__field_34,axiom, % 262.69/262.69 ( ~ class_Ring__and__Field_Oordered__field(T) % 262.69/262.69 | class_Ring__and__Field_Oordered__idom(T) ) ). % 262.69/262.69 % 262.69/262.69 cnf(clsrel_Ring__and__Field_Oordered__field_46,axiom, % 262.69/262.69 ( ~ class_Ring__and__Field_Oordered__field(T) % 262.69/262.69 | class_Ring__and__Field_Opordered__semiring(T) ) ). % 262.69/262.69 % 262.69/262.69 cnf(clsrel_Ring__and__Field_Oordered__field_47,axiom, % 262.69/262.69 ( ~ class_Ring__and__Field_Oordered__field(T) % 262.69/262.69 | class_OrderedGroup_Olordered__ab__group__abs(T) ) ). % 262.69/262.69 % 262.69/262.69 cnf(tfree_tcs,negated_conjecture, % 262.69/262.69 class_Ring__and__Field_Oordered__field(t_a) ). % 262.69/262.69 % 262.69/262.69 %------------------------------------------------------------------------------ % 262.69/262.69 %------------------------------------------- % 262.69/262.69 % Proof found % 262.69/262.69 % SZS status Theorem for theBenchmark % 262.69/262.69 % SZS output start Proof % 262.69/262.71 %ClaNum:34(EqnAxiom:22) % 262.69/262.71 %VarNum:53(SingletonVarNum:20) % 262.69/262.71 %MaxLitNum:4 % 262.69/262.71 %MaxfuncDepth:4 % 262.69/262.71 %SharedTerms:6 % 262.69/262.71 %goalClause: 23 24 25 % 262.69/262.71 %singleGoalClaCount:3 % 262.69/262.71 [23]P1(a1) % 262.69/262.71 [24]P2(f2(f6(x241),a1),f4(a7,f2(f9(x241),a1),a1),a1) % 262.69/262.71 [25]~P2(f2(f4(f5(a8,a1),f6(f10(x251)),a1),a1),f4(x251,f2(f9(f10(x251)),a1),a1),a1) % 262.69/262.71 [26]~P1(x261)+P3(x261) % 262.69/262.71 [27]~P5(x271)+P4(x271) % 262.69/262.71 [28]~P1(x281)+P6(x281) % 262.69/262.71 [29]~P1(x291)+P7(x291) % 262.69/262.71 [30]~P1(x301)+P5(x301) % 262.69/262.71 [31]~P3(x312)+P2(a3,f2(x311,x312),x312) % 262.69/262.71 [32]~P6(x322)+E(f4(f2(x321,x322),f2(x323,x322),x322),f2(f4(x321,x323,x322),x322)) % 262.69/262.71 [33]~P4(x333)+E(f4(f4(x331,x332,x333),x334,x333),f4(x331,f4(x332,x334,x333),x333)) % 262.69/262.71 [34]~P7(x343)+~P2(x342,x344,x343)+~P2(a3,x341,x343)+P2(f4(x341,x342,x343),f4(x341,x344,x343),x343) % 262.69/262.71 %EqnAxiom % 262.69/262.71 [1]E(x11,x11) % 262.69/262.71 [2]E(x22,x21)+~E(x21,x22) % 262.69/262.71 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 262.69/262.71 [4]~E(x41,x42)+E(f6(x41),f6(x42)) % 262.69/262.71 [5]~E(x51,x52)+E(f2(x51,x53),f2(x52,x53)) % 262.69/262.71 [6]~E(x61,x62)+E(f2(x63,x61),f2(x63,x62)) % 262.69/262.71 [7]~E(x71,x72)+E(f9(x71),f9(x72)) % 262.69/262.71 [8]~E(x81,x82)+E(f4(x81,x83,x84),f4(x82,x83,x84)) % 262.69/262.71 [9]~E(x91,x92)+E(f4(x93,x91,x94),f4(x93,x92,x94)) % 262.69/262.71 [10]~E(x101,x102)+E(f4(x103,x104,x101),f4(x103,x104,x102)) % 262.69/262.71 [11]~E(x111,x112)+E(f10(x111),f10(x112)) % 262.69/262.71 [12]~E(x121,x122)+E(f5(x121,x123),f5(x122,x123)) % 262.69/262.71 [13]~E(x131,x132)+E(f5(x133,x131),f5(x133,x132)) % 262.69/262.71 [14]~P1(x141)+P1(x142)+~E(x141,x142) % 262.69/262.71 [15]P2(x152,x153,x154)+~E(x151,x152)+~P2(x151,x153,x154) % 262.69/262.71 [16]P2(x163,x162,x164)+~E(x161,x162)+~P2(x163,x161,x164) % 262.69/262.71 [17]P2(x173,x174,x172)+~E(x171,x172)+~P2(x173,x174,x171) % 262.69/262.71 [18]~P4(x181)+P4(x182)+~E(x181,x182) % 262.69/262.71 [19]~P3(x191)+P3(x192)+~E(x191,x192) % 262.69/262.71 [20]~P6(x201)+P6(x202)+~E(x201,x202) % 262.69/262.71 [21]~P5(x211)+P5(x212)+~E(x211,x212) % 262.69/262.71 [22]~P7(x221)+P7(x222)+~E(x221,x222) % 262.69/262.71 % 262.69/262.71 %------------------------------------------- % 262.76/262.74 cnf(35,plain, % 262.76/262.74 (~E(f2(f6(f10(a7)),a1),f2(f4(f5(a8,a1),f6(f10(a7)),a1),a1))), % 262.76/262.74 inference(scs_inference,[],[24,25,15])). % 262.76/262.74 cnf(38,plain, % 262.76/262.74 (~E(f6(f10(a7)),f4(f5(a8,a1),f6(f10(a7)),a1))), % 262.76/262.74 inference(scs_inference,[],[24,25,15,5])). % 262.76/262.74 cnf(43,plain, % 262.76/262.74 (P2(a3,f2(x431,a1),a1)), % 262.76/262.74 inference(scs_inference,[],[23,26,31])). % 262.76/262.74 cnf(45,plain, % 262.76/262.74 (~E(a3,f2(f4(f5(a8,a1),f6(f10(x451)),a1),a1))+~E(f2(x452,a1),f4(x451,f2(f9(f10(x451)),a1),a1))), % 262.76/262.74 inference(scs_inference,[],[25,43,16,15])). % 262.76/262.74 cnf(48,plain, % 262.76/262.74 (~P5(x481)+E(f4(f4(x482,x483,x481),x484,x481),f4(x482,f4(x483,x484,x481),x481))), % 262.76/262.74 inference(scs_inference,[],[27,33])). % 262.76/262.74 cnf(55,plain, % 262.76/262.74 (E(f4(f2(x551,a1),f2(x552,a1),a1),f2(f4(x551,x552,a1),a1))), % 262.76/262.74 inference(scs_inference,[],[23,28,32])). % 262.76/262.74 cnf(56,plain, % 262.76/262.74 (E(f2(f4(x561,x562,a1),a1),f4(f2(x561,a1),f2(x562,a1),a1))), % 262.76/262.74 inference(scs_inference,[],[55,2])). % 262.76/262.74 cnf(57,plain, % 262.76/262.74 (~E(f2(f6(f10(a7)),a1),f4(f2(f5(a8,a1),a1),f2(f6(f10(a7)),a1),a1))), % 262.76/262.74 inference(scs_inference,[],[35,55,2,3])). % 262.76/262.74 cnf(72,plain, % 262.76/262.74 (P2(a3,f4(f2(x721,a1),f2(x722,a1),a1),a1)), % 262.76/262.74 inference(scs_inference,[],[43,56,16])). % 262.76/262.74 cnf(80,plain, % 262.76/262.74 (E(f4(f4(x801,x802,a1),x803,a1),f4(x801,f4(x802,x803,a1),a1))), % 262.76/262.74 inference(scs_inference,[],[23,30,48])). % 262.76/262.74 cnf(81,plain, % 262.76/262.74 (E(f4(x811,f4(x812,x813,a1),a1),f4(f4(x811,x812,a1),x813,a1))), % 262.76/262.74 inference(scs_inference,[],[80,2])). % 262.76/262.74 cnf(90,plain, % 262.76/262.74 (E(f6(f2(f4(x901,x902,a1),a1)),f6(f4(f2(x901,a1),f2(x902,a1),a1)))), % 262.76/262.74 inference(scs_inference,[],[55,4,2])). % 262.76/262.74 cnf(91,plain, % 262.76/262.74 (E(f6(f4(f2(x911,a1),f2(x912,a1),a1)),f6(f2(f4(x911,x912,a1),a1)))), % 262.76/262.74 inference(scs_inference,[],[90,2])). % 262.76/262.74 cnf(158,plain, % 262.76/262.74 (E(f9(f2(f4(f2(x1581,a1),f2(x1582,a1),a1),x1583)),f9(f2(f2(f4(x1581,x1582,a1),a1),x1583)))), % 262.76/262.74 inference(scs_inference,[],[55,7,5])). % 262.76/262.74 cnf(159,plain, % 262.76/262.74 (E(f9(f2(f2(f4(x1591,x1592,a1),a1),x1593)),f9(f2(f4(f2(x1591,a1),f2(x1592,a1),a1),x1593)))), % 262.76/262.74 inference(scs_inference,[],[158,2])). % 262.76/262.74 cnf(239,plain, % 262.76/262.74 (E(f4(x2391,x2392,f2(f4(x2393,x2394,a1),a1)),f4(x2391,x2392,f4(f2(x2393,a1),f2(x2394,a1),a1)))), % 262.76/262.74 inference(scs_inference,[],[55,10,2])). % 262.76/262.74 cnf(240,plain, % 262.76/262.74 (E(f4(x2401,x2402,f4(f2(x2403,a1),f2(x2404,a1),a1)),f4(x2401,x2402,f2(f4(x2403,x2404,a1),a1)))), % 262.76/262.74 inference(scs_inference,[],[239,2])). % 262.76/262.74 cnf(413,plain, % 262.76/262.74 (~E(f2(f4(f5(a8,a1),f6(f10(f2(x4131,a1))),a1),a1),a3)), % 262.76/262.74 inference(scs_inference,[],[56,45,2])). % 262.76/262.74 cnf(538,plain, % 262.76/262.74 (~E(a1,x5381)+P3(x5381)), % 262.76/262.74 inference(scs_inference,[],[23,26,19])). % 262.76/262.74 cnf(572,plain, % 262.76/262.74 (P2(f4(f4(f2(x5721,a1),f2(x5722,a1),a1),f2(f6(x5723),a1),a1),f4(f4(f2(x5721,a1),f2(x5722,a1),a1),f4(a7,f2(f9(x5723),a1),a1),a1),a1)), % 262.76/262.74 inference(scs_inference,[],[23,72,24,29,34])). % 262.76/262.74 cnf(575,plain, % 262.76/262.74 (P2(f4(f2(x5751,a1),f4(f2(x5752,a1),f2(f6(x5753),a1),a1),a1),f4(f4(f2(x5751,a1),f2(x5752,a1),a1),f4(a7,f2(f9(x5753),a1),a1),a1),a1)), % 262.76/262.74 inference(scs_inference,[],[572,81,80,16,15])). % 262.76/262.74 cnf(590,plain, % 262.76/262.74 (P2(f4(f4(f2(x5901,a1),f2(x5902,a1),a1),a3,a1),f4(f4(f2(x5901,a1),f2(x5902,a1),a1),f4(f2(x5901,a1),f2(x5902,a1),a1),a1),a1)), % 262.76/262.74 inference(scs_inference,[],[23,72,29,34])). % 262.76/262.74 cnf(592,plain, % 262.76/262.74 (E(f4(f4(x5921,x5922,a1),x5923,a1),f4(x5921,f4(x5922,x5923,a1),a1))), % 262.76/262.74 inference(rename_variables,[],[80])). % 262.76/262.74 cnf(593,plain, % 262.76/262.74 (P2(f4(f4(f2(x5931,a1),f2(x5932,a1),a1),a3,a1),f4(f2(x5931,a1),f4(f2(x5932,a1),f4(f2(x5931,a1),f2(x5932,a1),a1),a1),a1),a1)), % 262.76/262.74 inference(scs_inference,[],[590,80,592,15,16])). % 262.76/262.74 cnf(598,plain, % 262.76/262.74 (P2(f4(f2(x5981,a1),f4(f2(x5982,a1),a3,a1),a1),f4(f2(x5981,a1),f4(f2(x5982,a1),f4(f2(x5981,a1),f2(x5982,a1),a1),a1),a1),a1)), % 262.76/262.74 inference(scs_inference,[],[593,80,15])). % 262.76/262.74 cnf(1195,plain, % 262.76/262.74 (~E(f4(f5(a8,a1),f6(f10(a7)),a1),f6(f10(a7)))), % 262.76/262.74 inference(scs_inference,[],[35,2,5])). % 262.76/262.74 cnf(1196,plain, % 262.76/262.74 (E(f2(x11961,f2(f4(x11962,x11963,a1),a1)),f2(x11961,f4(f2(x11962,a1),f2(x11963,a1),a1)))), % 262.76/262.74 inference(scs_inference,[],[55,2,6])). % 262.76/262.74 cnf(1197,plain, % 262.76/262.74 (E(f2(x11971,f4(f2(x11972,a1),f2(x11973,a1),a1)),f2(x11971,f2(f4(x11972,x11973,a1),a1)))), % 262.76/262.74 inference(scs_inference,[],[1196,2])). % 262.76/262.74 cnf(1199,plain, % 262.76/262.74 (~P3(f2(x11991,f2(f4(x11992,x11993,a1),a1)))+P3(f2(x11991,f4(f2(x11992,a1),f2(x11993,a1),a1)))), % 262.76/262.74 inference(scs_inference,[],[1196,2,14,19])). % 262.76/262.74 cnf(1208,plain, % 262.76/262.74 (~P3(f2(x12081,f2(f4(x12082,x12083,a1),a1)))+P2(a3,f2(x12084,f2(x12081,f4(f2(x12082,a1),f2(x12083,a1),a1))),f2(x12081,f4(f2(x12082,a1),f2(x12083,a1),a1)))), % 262.76/262.74 inference(scs_inference,[],[1199,31])). % 262.76/262.74 cnf(1251,plain, % 262.76/262.74 (P2(a3,f2(x12511,f2(x12512,f4(f2(x12513,a1),f2(x12514,a1),a1))),f2(x12512,f4(f2(x12513,a1),f2(x12514,a1),a1)))+~E(a1,f2(x12512,f2(f4(x12513,x12514,a1),a1)))), % 262.76/262.74 inference(scs_inference,[],[1208,538])). % 262.76/262.74 cnf(1254,plain, % 262.76/262.74 (P2(a3,f2(x12541,f2(x12542,f4(f2(x12543,a1),f2(x12544,a1),a1))),f2(x12542,f2(f4(x12543,x12544,a1),a1)))+~E(a1,f2(x12542,f2(f4(x12543,x12544,a1),a1)))), % 262.76/262.74 inference(scs_inference,[],[1197,1251,17])). % 262.76/262.74 cnf(1255,plain, % 262.76/262.74 (P2(a3,x12551,f2(x12552,f2(f4(x12553,x12554,a1),a1)))+~E(f2(x12555,f2(x12552,f4(f2(x12553,a1),f2(x12554,a1),a1))),x12551)+~E(a1,f2(x12552,f2(f4(x12553,x12554,a1),a1)))), % 262.76/262.74 inference(scs_inference,[],[1254,16])). % 262.76/262.74 cnf(1258,plain, % 262.76/262.74 (P2(a3,x12581,f2(x12582,f4(f2(x12583,a1),f2(x12584,a1),a1)))+~E(f2(x12585,f2(x12582,f4(f2(x12583,a1),f2(x12584,a1),a1))),x12581)+~E(a1,f2(x12582,f2(f4(x12583,x12584,a1),a1)))), % 262.76/262.74 inference(scs_inference,[],[1196,1255,17])). % 262.76/262.74 cnf(1302,plain, % 262.76/262.74 (E(f2(f2(f4(x13021,x13022,a1),a1),x13023),f2(f4(f2(x13021,a1),f2(x13022,a1),a1),x13023))), % 262.76/262.74 inference(scs_inference,[],[55,2,5])). % 262.76/262.74 cnf(1303,plain, % 262.76/262.74 (E(f2(f4(f2(x13031,a1),f2(x13032,a1),a1),x13033),f2(f2(f4(x13031,x13032,a1),a1),x13033))), % 262.76/262.74 inference(scs_inference,[],[1302,2])). % 262.76/262.74 cnf(1304,plain, % 262.76/262.74 (E(f2(f2(f4(x13041,x13042,a1),a1),f4(f2(x13043,a1),f2(x13044,a1),a1)),f2(f4(f2(x13041,a1),f2(x13042,a1),a1),f2(f4(x13043,x13044,a1),a1)))), % 262.76/262.74 inference(scs_inference,[],[1197,1302,2,3])). % 262.76/262.75 cnf(1332,plain, % 262.76/262.75 (E(f4(f2(f2(x13321,a1),a1),f2(f2(x13322,a1),a1),a1),f2(f2(f4(x13321,x13322,a1),a1),a1))), % 262.76/262.75 inference(scs_inference,[],[55,1303,1304,2,3])). % 262.76/262.75 cnf(1344,plain, % 262.76/262.75 (E(f2(f2(f4(x13441,x13442,a1),a1),a1),f4(f2(f2(x13441,a1),a1),f2(f2(x13442,a1),a1),a1))), % 262.76/262.75 inference(scs_inference,[],[1332,2])). % 262.76/262.75 cnf(1345,plain, % 262.76/262.75 (E(f2(f2(f4(x13451,x13452,a1),a1),f2(f4(x13453,x13454,a1),a1)),f2(f4(f2(x13451,a1),f2(x13452,a1),a1),f4(f2(x13453,a1),f2(x13454,a1),a1)))), % 262.76/262.75 inference(scs_inference,[],[1196,1332,1302,2,3])). % 262.76/262.75 cnf(1352,plain, % 262.76/262.75 (E(f2(f4(f2(x13521,a1),f2(x13522,a1),a1),f4(f2(x13523,a1),f2(x13524,a1),a1)),f2(f2(f4(x13521,x13522,a1),a1),f2(f4(x13523,x13524,a1),a1)))), % 262.76/262.75 inference(scs_inference,[],[1345,2])). % 262.76/262.75 cnf(1859,plain, % 262.76/262.75 (P2(f4(f2(x18591,a1),f4(f2(x18592,a1),f2(f6(x18593),a1),a1),a1),f4(f2(x18591,a1),f4(f2(x18592,a1),f4(a7,f2(f9(x18593),a1),a1),a1),a1),a1)), % 262.76/262.75 inference(scs_inference,[],[575,80,16])). % 262.76/262.75 cnf(1861,plain, % 262.76/262.75 (P2(f4(f4(f2(x18611,a1),f2(x18612,a1),a1),f2(f6(x18613),a1),a1),f4(f2(x18611,a1),f4(f2(x18612,a1),f4(a7,f2(f9(x18613),a1),a1),a1),a1),a1)), % 262.76/262.75 inference(scs_inference,[],[575,80,81,16,15])). % 262.76/262.75 cnf(1869,plain, % 262.76/262.75 (E(f9(f4(f2(f2(x18691,a1),a1),f2(f2(x18692,a1),a1),a1)),f9(f2(f2(f4(x18691,x18692,a1),a1),a1)))), % 262.76/262.75 inference(scs_inference,[],[1332,4,7])). % 262.76/262.75 cnf(1874,plain, % 262.76/262.75 (E(f4(f4(f2(f2(x18741,a1),a1),f2(f2(x18742,a1),a1),a1),x18743,x18744),f4(f2(f2(f4(x18741,x18742,a1),a1),a1),x18743,x18744))), % 262.76/262.75 inference(scs_inference,[],[1332,4,7,11,6,12,13,8])). % 262.76/262.75 cnf(1878,plain, % 262.76/262.75 (P7(a1)), % 262.76/262.75 inference(scs_inference,[],[1332,23,4,7,11,6,12,13,8,9,10,5,29])). % 262.76/262.75 cnf(1883,plain, % 262.76/262.75 (~P2(f4(f2(f5(a8,a1),a1),f2(f6(f10(x18831)),a1),a1),f4(x18831,f2(f9(f10(x18831)),a1),a1),a1)), % 262.76/262.75 inference(scs_inference,[],[57,413,25,1332,23,56,55,4,7,11,6,12,13,8,9,10,5,29,2,3,15])). % 262.76/262.75 cnf(1885,plain, % 262.76/262.75 (P2(f4(f2(x18851,a1),a3,a1),f4(f2(x18851,a1),f2(x18851,a1),a1),a1)), % 262.76/262.75 inference(scs_inference,[],[57,413,25,1332,23,56,43,55,4,7,11,6,12,13,8,9,10,5,29,2,3,15,34])). % 262.76/262.75 cnf(1907,plain, % 262.76/262.75 (E(f2(x19071,f2(f4(f2(x19072,a1),f2(x19073,a1),a1),f4(f2(x19074,a1),f2(x19075,a1),a1))),f2(x19071,f2(f2(f4(x19072,x19073,a1),a1),f2(f4(x19074,x19075,a1),a1))))), % 262.76/262.75 inference(scs_inference,[],[1352,4,13,6])). % 262.76/262.75 cnf(1909,plain, % 262.76/262.75 (E(f9(f2(f4(f2(x19091,a1),f2(x19092,a1),a1),f4(f2(x19093,a1),f2(x19094,a1),a1))),f9(f2(f2(f4(x19091,x19092,a1),a1),f2(f4(x19093,x19094,a1),a1))))), % 262.76/262.75 inference(scs_inference,[],[1352,4,13,6,12,7])). % 262.76/262.75 cnf(1919,plain, % 262.76/262.75 (P2(f4(f4(f2(x19191,a1),f2(x19192,a1),a1),f4(f2(x19193,a1),a3,a1),a1),f4(f4(f2(x19191,a1),f2(x19192,a1),a1),f4(f2(x19193,a1),f2(x19193,a1),a1),a1),a1)), % 262.76/262.75 inference(scs_inference,[],[1878,1885,1869,35,72,1352,159,4,13,6,12,7,11,10,8,9,5,2,3,34])). % 262.76/262.75 cnf(1945,plain, % 262.76/262.75 (E(f2(x19451,f2(f2(f4(x19452,x19453,a1),a1),f4(f2(x19454,a1),f2(x19455,a1),a1))),f2(x19451,f2(f4(f2(x19452,a1),f2(x19453,a1),a1),f2(f4(x19454,x19455,a1),a1))))), % 262.76/262.75 inference(scs_inference,[],[1304,4,6])). % 262.76/262.75 cnf(1957,plain, % 262.76/262.75 (P2(f4(f2(f2(f4(x19571,x19572,a1),a1),a1),f4(f2(x19573,a1),a3,a1),a1),f4(f4(f2(f2(x19571,a1),a1),f2(f2(x19572,a1),a1),a1),f4(f2(x19573,a1),f2(x19573,a1),a1),a1),a1)), % 262.76/262.75 inference(scs_inference,[],[1919,1874,1909,1304,159,4,6,13,12,7,11,10,8,9,5,3,15])). % 262.76/262.75 cnf(1986,plain, % 262.76/262.75 (E(f4(f2(f2(f4(x19861,x19862,a1),a1),a1),x19863,x19864),f4(f4(f2(f2(x19861,a1),a1),f2(f2(x19862,a1),a1),a1),x19863,x19864))), % 262.76/262.75 inference(scs_inference,[],[1344,4,13,11,12,7,6,10,8])). % 262.76/262.75 cnf(1987,plain, % 262.76/262.75 (E(f4(x19871,f2(f2(f4(x19872,x19873,a1),a1),a1),x19874),f4(x19871,f4(f2(f2(x19872,a1),a1),f2(f2(x19873,a1),a1),a1),x19874))), % 262.76/262.75 inference(scs_inference,[],[1344,4,13,11,12,7,6,10,8,9])). % 262.76/262.75 cnf(2004,plain, % 262.76/262.75 (E(f4(f2(f2(f4(x20041,x20042,a1),a1),x20043),x20044,x20045),f4(f2(f4(f2(x20041,a1),f2(x20042,a1),a1),x20043),x20044,x20045))), % 262.76/262.75 inference(scs_inference,[],[1302,81,4,6,13,12,7,11,10,9,8])). % 262.76/262.75 cnf(2007,plain, % 262.76/262.75 (P2(f4(f2(f2(f4(x20071,x20072,a1),a1),a1),a3,a1),f4(f2(f2(f4(x20071,x20072,a1),a1),a1),f4(f2(f2(x20071,a1),a1),f2(f2(x20072,a1),a1),a1),a1),a1)), % 262.76/262.75 inference(scs_inference,[],[1987,1195,1885,1302,81,4,6,13,12,7,11,10,9,8,5,3,16])). % 262.76/262.75 cnf(2035,plain, % 262.76/262.75 (E(f2(x20351,f2(f4(f2(x20352,a1),f2(x20353,a1),a1),x20354)),f2(x20351,f2(f2(f4(x20352,x20353,a1),a1),x20354)))), % 262.76/262.75 inference(scs_inference,[],[1303,1197,4,7,11,12,13,6])). % 262.76/262.75 cnf(2041,plain, % 262.76/262.75 (P2(f4(f2(f4(f2(x20411,a1),f2(x20412,a1),a1),a1),f4(f2(x20413,a1),a3,a1),a1),f4(f4(f2(f2(x20411,a1),a1),f2(f2(x20412,a1),a1),a1),f4(f2(x20413,a1),f2(x20413,a1),a1),a1),a1)), % 262.76/262.75 inference(scs_inference,[],[2004,1957,38,1303,1197,4,7,11,12,13,6,10,9,8,5,3,15])). % 262.76/262.75 cnf(2045,plain, % 262.76/262.75 (E(f6(f4(x20451,f4(x20452,x20453,a1),a1)),f6(f4(f4(x20451,x20452,a1),x20453,a1)))), % 262.76/262.75 inference(scs_inference,[],[81,4])). % 262.76/262.75 cnf(2046,plain, % 262.76/262.75 (E(f2(x20461,f4(x20462,f4(x20463,x20464,a1),a1)),f2(x20461,f4(f4(x20462,x20463,a1),x20464,a1)))), % 262.76/262.75 inference(scs_inference,[],[81,4,6])). % 262.76/262.75 cnf(2050,plain, % 262.76/262.75 (E(f5(x20501,f4(x20502,f4(x20503,x20504,a1),a1)),f5(x20501,f4(f4(x20502,x20503,a1),x20504,a1)))), % 262.76/262.75 inference(scs_inference,[],[81,1196,4,6,7,12,11,13])). % 262.76/262.75 cnf(2051,plain, % 262.76/262.75 (E(f4(x20511,x20512,f4(x20513,f4(x20514,x20515,a1),a1)),f4(x20511,x20512,f4(f4(x20513,x20514,a1),x20515,a1)))), % 262.76/262.75 inference(scs_inference,[],[81,1196,4,6,7,12,11,13,10])). % 262.76/262.75 cnf(2052,plain, % 262.76/262.75 (E(f4(f4(x20521,f4(x20522,x20523,a1),a1),x20524,x20525),f4(f4(f4(x20521,x20522,a1),x20523,a1),x20524,x20525))), % 262.76/262.75 inference(scs_inference,[],[81,1196,4,6,7,12,11,13,10,8])). % 262.76/262.75 cnf(2053,plain, % 262.76/262.75 (E(f4(x20531,f4(x20532,f4(x20533,x20534,a1),a1),x20535),f4(x20531,f4(f4(x20532,x20533,a1),x20534,a1),x20535))), % 262.76/262.75 inference(scs_inference,[],[81,1196,4,6,7,12,11,13,10,8,9])). % 262.76/262.75 cnf(2054,plain, % 262.76/262.75 (E(f2(f4(x20541,f4(x20542,x20543,a1),a1),x20544),f2(f4(f4(x20541,x20542,a1),x20543,a1),x20544))), % 262.76/262.75 inference(scs_inference,[],[81,1196,4,6,7,12,11,13,10,8,9,5])). % 262.76/262.75 cnf(2061,plain, % 262.76/262.75 (E(f5(f4(x20611,x20612,f4(x20613,f4(x20614,x20615,a1),a1)),x20616),f5(f4(x20611,x20612,f4(f4(x20613,x20614,a1),x20615,a1)),x20616))), % 262.76/262.75 inference(scs_inference,[],[2051,4,6,11,12])). % 262.76/262.75 cnf(2072,plain, % 262.76/262.75 (E(f6(f4(f4(x20721,f4(x20722,x20723,a1),a1),x20724,x20725)),f6(f4(f4(f4(x20721,x20722,a1),x20723,a1),x20724,x20725)))), % 262.76/262.75 inference(scs_inference,[],[2052,4])). % 262.76/262.75 cnf(2074,plain, % 262.76/262.75 (E(f5(f4(f4(x20741,f4(x20742,x20743,a1),a1),x20744,x20745),x20746),f5(f4(f4(f4(x20741,x20742,a1),x20743,a1),x20744,x20745),x20746))), % 262.76/262.75 inference(scs_inference,[],[2052,4,6,12])). % 262.76/262.75 cnf(2076,plain, % 262.76/262.75 (E(f10(f4(f4(x20761,f4(x20762,x20763,a1),a1),x20764,x20765)),f10(f4(f4(f4(x20761,x20762,a1),x20763,a1),x20764,x20765)))), % 262.76/262.75 inference(scs_inference,[],[2052,4,6,12,13,11])). % 262.76/262.75 cnf(2082,plain, % 262.76/262.75 (P2(f4(f2(x20821,a1),f4(f2(x20822,a1),f2(f6(x20823),a1),a1),a1),f4(f2(x20821,a1),f4(f4(f2(x20822,a1),a7,a1),f2(f9(x20823),a1),a1),a1),a1)), % 262.76/262.75 inference(scs_inference,[],[2052,2053,1859,4,6,12,13,11,7,9,8,10,5,16])). % 262.76/262.75 cnf(2083,plain, % 262.76/262.75 (E(f4(x20831,f4(x20832,f4(x20833,x20834,a1),a1),x20835),f4(x20831,f4(f4(x20832,x20833,a1),x20834,a1),x20835))), % 262.76/262.75 inference(rename_variables,[],[2053])). % 262.76/262.75 cnf(2087,plain, % 262.76/262.75 (E(f4(f4(x20871,f4(x20872,x20873,a1),a1),f4(x20874,f4(x20875,x20876,a1),a1),x20877),f4(f4(f4(x20871,x20872,a1),x20873,a1),f4(f4(x20874,x20875,a1),x20876,a1),x20877))), % 262.76/262.75 inference(scs_inference,[],[2052,2053,2083,1859,2035,4,6,12,13,11,7,9,8,10,5,16,1258,3])). % 262.76/262.75 cnf(2103,plain, % 262.76/262.75 (P2(f4(f4(f2(f4(f2(x21031,a1),f2(x21032,a1),a1),a1),f2(x21033,a1),a1),a3,a1),f4(f4(f2(f2(x21031,a1),a1),f2(f2(x21032,a1),a1),a1),f4(f2(x21033,a1),f2(x21033,a1),a1),a1),a1)), % 262.76/262.75 inference(scs_inference,[],[2046,2041,1907,81,4,6,13,11,12,7,9,10,8,5,1255,15])). % 262.76/262.75 cnf(2142,plain, % 262.76/262.75 (P2(f4(f4(f2(x21421,a1),f2(x21422,a1),a1),f2(f6(x21423),a1),a1),f4(f2(x21421,a1),f4(f4(f2(x21422,a1),a7,a1),f2(f9(x21423),a1),a1),a1),a1)), % 262.76/262.75 inference(scs_inference,[],[2045,2072,2053,1945,1861,4,6,13,11,12,7,9,8,10,5,1258,3,16])). % 262.76/262.75 cnf(2205,plain, % 262.76/262.75 (E(f10(f4(f4(x22051,x22052,a1),x22053,a1)),f10(f4(x22051,f4(x22052,x22053,a1),a1)))), % 262.76/262.75 inference(scs_inference,[],[1197,80,6,4,12,7,11])). % 262.76/262.75 cnf(2253,plain, % 262.76/262.75 (E(f10(f4(f4(f4(x22531,f4(x22532,x22533,a1),a1),x22534,a1),x22535,a1)),f10(f4(f4(f4(x22531,x22532,a1),x22533,a1),f4(x22534,x22535,a1),a1)))), % 262.76/262.75 inference(scs_inference,[],[2205,2076,1907,4,6,11,13,12,9,7,8,10,5,1258,3])). % 262.76/262.75 cnf(2256,plain, % 262.76/262.75 (P2(f4(f2(f2(x22561,a1),a1),a3,a1),f2(f2(f4(x22561,x22561,a1),a1),a1),a1)), % 262.76/262.75 inference(scs_inference,[],[2205,2076,1907,1885,1332,4,6,11,13,12,9,7,8,10,5,1258,3,16])). % 262.76/262.75 cnf(2269,plain, % 262.76/262.75 (P2(f4(f4(f2(x22691,a1),f2(x22692,a1),a1),f4(f2(f2(x22693,a1),a1),a3,a1),a1),f4(f4(f2(x22691,a1),f2(x22692,a1),a1),f2(f2(f4(x22693,x22693,a1),a1),a1),a1),a1)), % 262.76/262.75 inference(scs_inference,[],[2256,1878,72,1196,240,6,4,12,13,7,11,9,10,8,5,34])). % 262.76/262.75 cnf(2274,plain, % 262.76/262.75 (P2(f4(f4(f2(f2(x22741,a1),a1),f2(f2(x22742,a1),a1),a1),a3,a1),f2(f2(f4(f4(x22741,x22742,a1),f4(x22741,x22742,a1),a1),a1),a1),a1)), % 262.76/262.75 inference(scs_inference,[],[2256,1986,2035,1878,72,1196,240,6,4,12,13,7,11,9,10,8,5,34,1255,15])). % 262.76/262.75 cnf(2281,plain, % 262.76/262.75 (E(f2(x22811,f4(f4(x22812,x22813,a1),x22814,a1)),f2(x22811,f4(x22812,f4(x22813,x22814,a1),a1)))), % 262.76/262.75 inference(scs_inference,[],[80,91,4,6])). % 262.76/262.75 cnf(2282,plain, % 262.76/262.75 (E(f5(x22821,f4(f4(x22822,x22823,a1),x22824,a1)),f5(x22821,f4(x22822,f4(x22823,x22824,a1),a1)))), % 262.76/262.75 inference(scs_inference,[],[80,91,4,6,13])). % 262.76/262.75 cnf(2284,plain, % 262.76/262.75 (E(f4(x22841,f4(f4(x22842,x22843,a1),x22844,a1),x22845),f4(x22841,f4(x22842,f4(x22843,x22844,a1),a1),x22845))), % 262.76/262.75 inference(scs_inference,[],[80,91,4,6,13,7,9])). % 262.76/262.75 cnf(2285,plain, % 262.76/262.75 (E(f5(f4(f4(x22851,x22852,a1),x22853,a1),x22854),f5(f4(x22851,f4(x22852,x22853,a1),a1),x22854))), % 262.76/262.75 inference(scs_inference,[],[80,91,4,6,13,7,9,12])). % 262.76/262.75 cnf(2287,plain, % 262.76/262.75 (E(f4(f4(f4(x22871,x22872,a1),x22873,a1),x22874,x22875),f4(f4(x22871,f4(x22872,x22873,a1),a1),x22874,x22875))), % 262.76/262.75 inference(scs_inference,[],[80,91,4,6,13,7,9,12,11,8])). % 262.76/262.75 cnf(2288,plain, % 262.76/262.75 (E(f4(x22881,x22882,f4(f4(x22883,x22884,a1),x22885,a1)),f4(x22881,x22882,f4(x22883,f4(x22884,x22885,a1),a1)))), % 262.76/262.75 inference(scs_inference,[],[80,91,4,6,13,7,9,12,11,8,10])). % 262.76/262.75 cnf(2289,plain, % 262.76/262.75 (E(f2(f4(f4(x22891,x22892,a1),x22893,a1),x22894),f2(f4(x22891,f4(x22892,x22893,a1),a1),x22894))), % 262.76/262.75 inference(scs_inference,[],[80,91,4,6,13,7,9,12,11,8,10,5])). % 262.76/262.75 cnf(2342,plain, % 262.76/262.75 (E(f5(f4(f4(x23421,x23422,a1),x23423,a1),f4(f4(x23424,x23425,a1),x23426,a1)),f5(f4(x23421,f4(x23422,x23423,a1),a1),f4(x23424,f4(x23425,x23426,a1),a1)))), % 262.76/262.75 inference(scs_inference,[],[2282,2285,4,6,11,13,7,9,8,12,10,5,3])). % 262.76/262.75 cnf(2465,plain, % 262.76/262.75 (E(f4(f2(f4(x24651,x24652,a1),a1),x24653,x24654),f4(f4(f2(x24651,a1),f2(x24652,a1),a1),x24653,x24654))), % 262.76/262.75 inference(scs_inference,[],[56,239,6,8])). % 262.76/262.75 cnf(2468,plain, % 262.80/262.75 (E(f4(x24681,f2(f4(x24682,x24683,a1),a1),x24684),f4(x24681,f4(f2(x24682,a1),f2(x24683,a1),a1),x24684))), % 262.80/262.75 inference(scs_inference,[],[56,239,6,8,10,12,9])). % 262.80/262.75 cnf(2470,plain, % 262.80/262.75 (E(f5(x24701,f2(f4(x24702,x24703,a1),a1)),f5(x24701,f4(f2(x24702,a1),f2(x24703,a1),a1)))), % 262.80/262.75 inference(scs_inference,[],[56,239,55,6,8,10,12,9,7,13])). % 262.80/262.75 cnf(2485,plain, % 262.80/262.75 (P2(f4(f4(f2(x24851,a1),f2(x24852,a1),a1),f4(f2(x24853,a1),f2(f6(x24854),a1),a1),a1),f4(f2(f4(x24851,x24852,a1),a1),f4(f4(f2(x24853,a1),a7,a1),f2(f9(x24854),a1),a1),a1),a1)), % 262.80/262.75 inference(scs_inference,[],[2465,2468,2082,4,6,8,10,12,11,7,13,9,5,15])). % 262.80/262.75 cnf(2514,plain, % 262.80/262.75 (E(f5(f4(x25141,x25142,f4(x25143,f4(x25144,x25145,a1),a1)),f2(f4(x25146,x25147,a1),a1)),f5(f4(x25141,x25142,f4(f4(x25143,x25144,a1),x25145,a1)),f4(f2(x25146,a1),f2(x25147,a1),a1)))), % 262.80/262.75 inference(scs_inference,[],[2470,2061,4,6,8,10,12,13,9,11,7,5,3])). % 262.80/262.75 cnf(2546,plain, % 262.80/262.75 (E(f4(f4(x25461,f2(f4(x25462,x25463,a1),a1),x25464),x25465,x25466),f4(f4(x25461,f4(f2(x25462,a1),f2(x25463,a1),a1),x25464),x25465,x25466))), % 262.80/262.75 inference(scs_inference,[],[2468,6,8])). % 262.80/262.75 cnf(2563,plain, % 262.80/262.75 (E(f5(f4(f4(x25631,f4(x25632,x25633,a1),a1),x25634,f4(x25635,f4(x25636,x25637,a1),a1)),f2(f4(x25638,x25639,a1),a1)),f5(f4(f4(f4(x25631,x25632,a1),x25633,a1),x25634,f4(f4(x25635,x25636,a1),x25637,a1)),f4(f2(x25638,a1),f2(x25639,a1),a1)))), % 262.80/262.75 inference(scs_inference,[],[2514,2074,239,55,8,12,10,13,11,7,9,5,4,6,3])). % 262.80/262.75 cnf(2585,plain, % 262.80/262.75 (E(f4(f4(f2(x25851,a1),f2(x25852,a1),a1),x25853,x25854),f4(f2(f4(x25851,x25852,a1),a1),x25853,x25854))), % 262.80/262.75 inference(scs_inference,[],[55,8])). % 262.80/262.75 cnf(2590,plain, % 262.80/262.75 (E(f4(x25901,f4(f2(x25902,a1),f2(x25903,a1),a1),x25904),f4(x25901,f2(f4(x25902,x25903,a1),a1),x25904))), % 262.80/262.75 inference(scs_inference,[],[55,8,10,11,7,13,9])). % 262.80/262.75 cnf(2603,plain, % 262.80/262.75 (E(f4(f4(f2(x26031,a1),f2(x26032,a1),a1),f4(f2(x26033,a1),f2(x26034,a1),a1),x26035),f4(f2(f4(x26031,x26032,a1),a1),f2(f4(x26033,x26034,a1),a1),x26035))), % 262.80/262.75 inference(scs_inference,[],[2585,2590,5,4,6,8,10,11,7,9,3])). % 262.80/262.75 cnf(2616,plain, % 262.80/262.75 (P2(f4(f4(f2(f4(f2(x26161,a1),f2(x26162,a1),a1),a1),f2(x26163,a1),a1),a3,a1),f4(f2(f4(f2(x26161,a1),f2(x26162,a1),a1),a1),f2(f4(x26163,x26163,a1),a1),a1),a1)), % 262.80/262.75 inference(scs_inference,[],[2603,2103,5,4,6,12,8,10,11,13,7,9,16])). % 262.80/262.75 cnf(2618,plain, % 262.80/262.75 (P2(f4(f2(x26181,a1),f4(f2(f2(x26182,a1),a1),a3,a1),a1),f4(f2(x26181,a1),f2(f2(f4(x26182,x26182,a1),a1),a1),a1),a1)), % 262.80/262.75 inference(scs_inference,[],[43,2603,2103,2256,1878,5,4,6,12,8,10,11,13,7,9,16,34])). % 262.80/262.75 cnf(2620,plain, % 262.80/262.75 (E(f4(f4(x26201,f4(f2(x26202,a1),f2(x26203,a1),a1),x26204),x26205,x26206),f4(f4(x26201,f2(f4(x26202,x26203,a1),a1),x26204),x26205,x26206))), % 262.80/262.75 inference(scs_inference,[],[2590,8])). % 262.80/262.75 cnf(2621,plain, % 262.80/262.75 (E(f4(x26211,f4(x26212,f4(f2(x26213,a1),f2(x26214,a1),a1),x26215),x26216),f4(x26211,f4(x26212,f2(f4(x26213,x26214,a1),a1),x26215),x26216))), % 262.80/262.75 inference(scs_inference,[],[2590,8,9])). % 262.80/262.75 cnf(2632,plain, % 262.80/262.75 (P2(f4(f4(f2(f4(f2(x26321,a1),f2(x26322,a1),a1),a1),f2(x26323,a1),a1),a3,a1),f2(f4(f4(f2(x26321,a1),f2(x26322,a1),a1),f4(x26323,x26323,a1),a1),a1),a1)), % 262.80/262.75 inference(scs_inference,[],[55,2616,16])). % 262.80/262.75 cnf(2661,plain, % 262.80/262.75 (P2(f4(f4(f2(f4(f2(x26611,a1),f2(x26612,a1),a1),a1),f4(f2(x26613,a1),f2(x26614,a1),a1),a1),a3,a1),f2(f4(f4(f2(x26611,a1),f2(x26612,a1),a1),f4(f4(x26613,x26614,a1),f4(x26613,x26614,a1),a1),a1),a1),a1)), % 262.80/262.75 inference(scs_inference,[],[2632,2546,17,15])). % 262.80/262.75 cnf(2670,plain, % 262.80/262.75 (P2(f4(f2(x26701,a1),f4(f2(x26702,a1),a3,a1),a1),f4(f2(x26701,a1),f4(f2(x26702,a1),f2(f4(x26701,x26702,a1),a1),a1),a1),a1)), % 262.80/262.75 inference(scs_inference,[],[2621,598,16])). % 262.80/262.75 cnf(2703,plain, % 262.80/262.75 (P2(f4(f2(f2(x27031,a1),a1),a3,a1),f2(f2(f4(x27031,x27031,a1),a1),a1),a1)), % 262.80/262.75 inference(rename_variables,[],[2256])). % 262.80/262.75 cnf(2704,plain, % 262.80/262.75 (E(f2(f2(f4(x27041,x27042,a1),a1),x27043),f2(f4(f2(x27041,a1),f2(x27042,a1),a1),x27043))), % 262.80/262.75 inference(rename_variables,[],[1302])). % 262.80/262.75 cnf(2711,plain, % 262.80/262.75 (~P2(f2(f6(f10(f2(f5(a8,a1),a1))),a1),f2(f9(f10(f2(f5(a8,a1),a1))),a1),a1)), % 262.80/262.75 inference(scs_inference,[],[43,1302,2704,2281,2603,1878,2256,2703,2004,1883,2,16,15,3,34])). % 262.80/262.75 cnf(2721,plain, % 262.80/262.75 (E(f4(f4(f4(x27211,x27212,a1),x27213,a1),f4(f4(x27214,x27215,a1),x27216,a1),x27217),f4(f4(x27211,f4(x27212,x27213,a1),a1),f4(x27214,f4(x27215,x27216,a1),a1),x27217))), % 262.80/262.75 inference(scs_inference,[],[2087,2])). % 262.80/262.75 cnf(2725,plain, % 262.80/262.75 (~E(a3,f2(f6(f10(f2(f5(a8,a1),a1))),a1))), % 262.80/262.75 inference(scs_inference,[],[55,43,2087,1885,2711,2,16,15])). % 262.80/262.75 cnf(2741,plain, % 262.80/262.75 (P2(f4(f4(f2(x27411,a1),f2(x27412,a1),a1),a3,a1),f4(f2(f4(x27411,x27412,a1),a1),f2(f4(x27411,x27412,a1),a1),a1),a1)), % 262.80/262.75 inference(scs_inference,[],[81,2342,2465,1885,2082,2,16,15])). % 262.80/262.75 cnf(2744,plain, % 262.80/262.75 (E(f4(x27441,f4(x27442,f4(x27443,x27444,a1),a1),f2(f4(x27445,x27446,a1),a1)),f4(x27441,f4(f4(x27442,x27443,a1),x27444,a1),f4(f2(x27445,a1),f2(x27446,a1),a1)))), % 262.80/262.75 inference(scs_inference,[],[239,81,2053,2342,2465,1885,2082,2,16,15,3])). % 262.80/262.75 cnf(2756,plain, % 262.80/262.75 (E(f4(f4(x27561,f4(x27562,x27563,a1),a1),x27564,f2(f4(x27565,x27566,a1),a1)),f4(f4(f4(x27561,x27562,a1),x27563,a1),x27564,f4(f2(x27565,a1),f2(x27566,a1),a1)))), % 262.80/262.75 inference(scs_inference,[],[55,239,80,2052,1919,2514,2741,2,15,16,3])). % 262.80/262.75 cnf(2773,plain, % 262.80/262.75 (E(f4(x27731,f4(x27732,x27733,a1),a1),f4(f4(x27731,x27732,a1),x27733,a1))), % 262.80/262.75 inference(rename_variables,[],[81])). % 262.80/262.75 cnf(2776,plain, % 262.80/262.75 (E(f4(x27761,f4(x27762,f4(x27763,x27764,a1),a1),f4(f4(x27765,x27766,a1),x27767,a1)),f4(x27761,f4(f4(x27762,x27763,a1),x27764,a1),f4(x27765,f4(x27766,x27767,a1),a1)))), % 262.80/262.75 inference(scs_inference,[],[81,2773,2053,2288,1957,2744,2142,2,16,15,3])). % 262.80/262.75 cnf(2800,plain, % 262.80/262.75 (P2(f4(f2(x28001,a1),f4(f2(x28002,a1),a3,a1),a1),f4(f2(f4(x28001,x28002,a1),a1),f2(f4(x28001,x28002,a1),a1),a1),a1)), % 262.80/262.75 inference(scs_inference,[],[80,2741,2776,2,15])). % 262.80/262.75 cnf(2804,plain, % 262.80/262.75 (E(f4(f4(x28041,f4(x28042,x28043,a1),a1),f4(x28044,f4(x28045,x28046,a1),a1),f2(f4(x28047,x28048,a1),a1)),f4(f4(f4(x28041,x28042,a1),x28043,a1),f4(f4(x28044,x28045,a1),x28046,a1),f4(f2(x28047,a1),f2(x28048,a1),a1)))), % 262.80/262.75 inference(scs_inference,[],[239,80,81,2087,2741,2776,2670,2,15,16,3])). % 262.80/262.75 cnf(2822,plain, % 262.80/262.75 (E(f5(f4(f4(x28221,x28222,a1),x28223,a1),f2(f4(x28224,x28225,a1),a1)),f5(f4(x28221,f4(x28222,x28223,a1),a1),f4(f2(x28224,a1),f2(x28225,a1),a1)))), % 262.80/262.75 inference(scs_inference,[],[55,80,2285,2470,2616,2756,2800,2,16,15,3])). % 262.80/262.75 cnf(2861,plain, % 262.80/262.75 (E(f5(f4(f4(f4(x28611,x28612,a1),x28613,a1),x28614,a1),f4(f4(x28615,x28616,a1),x28617,a1)),f5(f4(x28611,f4(x28612,f4(x28613,x28614,a1),a1),a1),f4(x28615,f4(x28616,x28617,a1),a1)))), % 262.80/262.75 inference(scs_inference,[],[80,81,2285,2342,2632,2563,2485,2,15,16,3])). % 262.80/262.75 cnf(2870,plain, % 262.80/262.75 (P2(f4(f2(f2(f4(x28701,x28702,a1),a1),a1),a3,a1),f4(f4(f2(f2(f4(x28701,x28702,a1),a1),a1),f2(f2(x28701,a1),a1),a1),f2(f2(x28702,a1),a1),a1),a1)), % 262.80/262.75 inference(scs_inference,[],[81,2861,2007,2,16])). % 262.80/262.75 cnf(2871,plain, % 262.80/262.75 (E(f4(x28711,f4(x28712,x28713,a1),a1),f4(f4(x28711,x28712,a1),x28713,a1))), % 262.80/262.75 inference(rename_variables,[],[81])). % 262.80/262.75 cnf(2872,plain, % 262.80/262.75 (P2(f4(f4(f2(x28721,a1),f2(x28722,a1),a1),a3,a1),f4(f2(x28721,a1),f4(f2(x28722,a1),f2(f4(x28721,x28722,a1),a1),a1),a1),a1)), % 262.80/262.75 inference(scs_inference,[],[81,2871,2670,2861,2007,2,16,15])). % 262.80/262.75 cnf(2874,plain, % 262.80/262.75 (E(f4(f2(f4(x28741,x28742,a1),a1),f2(x28743,a1),a1),f2(f4(x28741,f4(x28742,x28743,a1),a1),a1))), % 262.80/262.75 inference(scs_inference,[],[55,81,2871,2289,2670,2861,2007,2,16,15,3])). % 262.80/262.75 cnf(2882,plain, % 262.80/262.75 (P2(f4(f4(f2(x28821,a1),f2(f2(x28822,a1),a1),a1),a3,a1),f4(f2(x28821,a1),f2(f2(f4(x28822,x28822,a1),a1),a1),a1),a1)), % 262.80/262.75 inference(scs_inference,[],[81,2618,2253,2,15])). % 262.80/262.75 cnf(2883,plain, % 262.80/262.75 (E(f4(x28831,f4(x28832,x28833,a1),a1),f4(f4(x28831,x28832,a1),x28833,a1))), % 262.80/262.75 inference(rename_variables,[],[81])). % 262.80/262.75 cnf(2886,plain, % 262.80/262.75 (E(f4(x28861,f4(x28862,f4(x28863,x28864,a1),a1),f4(x28865,f4(x28866,x28867,a1),a1)),f4(x28861,f4(f4(x28862,x28863,a1),x28864,a1),f4(f4(x28865,x28866,a1),x28867,a1)))), % 262.80/262.75 inference(scs_inference,[],[81,2883,2053,2051,2618,2253,2872,2,15,16,3])). % 262.80/262.75 cnf(2899,plain, % 262.80/262.75 (E(f4(x28991,f4(f4(x28992,x28993,a1),x28994,a1),f2(f4(x28995,x28996,a1),a1)),f4(x28991,f4(x28992,f4(x28993,x28994,a1),a1),f4(f2(x28995,a1),f2(x28996,a1),a1)))), % 262.80/262.75 inference(scs_inference,[],[55,239,2284,2004,2007,2886,2882,2,16,15,3])). % 262.80/262.75 cnf(2914,plain, % 262.80/262.75 (E(f4(f4(f4(x29141,x29142,a1),x29143,a1),x29144,f2(f4(x29145,x29146,a1),a1)),f4(f4(x29141,f4(x29142,x29143,a1),a1),x29144,f4(f2(x29145,a1),f2(x29146,a1),a1)))), % 262.80/262.75 inference(scs_inference,[],[239,56,2287,2004,2899,2870,2661,2,15,16,3])). % 262.80/262.75 cnf(2924,plain, % 262.80/262.75 (P2(f4(f2(f4(f2(x29241,a1),f2(x29242,a1),a1),a1),f4(f4(f2(x29243,a1),f2(x29244,a1),a1),a3,a1),a1),f2(f4(f4(f2(x29241,a1),f2(x29242,a1),a1),f4(f4(x29243,x29244,a1),f4(x29243,x29244,a1),a1),a1),a1),a1)), % 262.80/262.75 inference(scs_inference,[],[80,1302,2661,2914,2274,2,16,15])). % 262.80/262.75 cnf(2940,plain, % 262.80/262.75 (P2(f4(f2(f2(x29401,a1),a1),f4(f2(f2(x29402,a1),a1),a3,a1),a1),f2(f2(f4(f4(x29401,x29402,a1),f4(x29401,x29402,a1),a1),a1),a1),a1)), % 262.80/262.75 inference(scs_inference,[],[80,2274,2804,2,15])). % 262.80/262.75 cnf(2944,plain, % 262.80/262.75 (E(f5(f4(f4(x29441,x29442,a1),x29443,a1),f4(x29444,f4(x29445,x29446,a1),a1)),f5(f4(x29441,f4(x29442,x29443,a1),a1),f4(f4(x29444,x29445,a1),x29446,a1)))), % 262.80/262.75 inference(scs_inference,[],[56,80,2285,2050,2274,2804,2924,2,15,16,3])). % 262.80/262.75 cnf(2952,plain, % 262.80/262.75 (P2(f4(f2(f2(x29521,a1),a1),f4(f2(f2(x29522,a1),a1),a3,a1),a1),f2(f4(f2(f4(x29521,x29522,a1),a1),f2(f4(x29521,x29522,a1),a1),a1),a1),a1)), % 262.80/262.75 inference(scs_inference,[],[1302,2944,2940,2,16])). % 262.80/262.75 cnf(2992,plain, % 262.80/262.75 (E(f4(f2(x29921,a1),f2(f4(x29922,x29923,a1),a1),a1),f2(f4(f4(x29921,x29922,a1),x29923,a1),a1))), % 262.80/262.75 inference(scs_inference,[],[55,56,80,2054,2822,2269,2952,2,15,16,3])). % 262.80/262.75 cnf(3153,plain, % 262.80/262.75 (E(f2(f4(x31531,f4(x31532,x31533,a1),a1),a1),f4(f2(f4(x31531,x31532,a1),a1),f2(x31533,a1),a1))), % 262.80/262.75 inference(scs_inference,[],[2874,2])). % 262.80/262.75 cnf(4536,plain, % 262.80/262.75 (P2(f4(f2(x45361,a1),f2(f6(x45362),a1),a1),f4(f2(x45361,a1),f4(a7,f2(f9(x45362),a1),a1),a1),a1)), % 262.80/262.75 inference(scs_inference,[],[24,3153,1878,43,12,10,8,11,13,7,9,5,4,6,34])). % 262.80/262.75 cnf(4539,plain, % 262.80/262.75 (E(f4(f4(f4(x45391,f2(x45392,a1),a1),f2(x45393,a1),a1),f4(f4(x45394,x45395,a1),x45396,a1),x45397),f4(f4(x45391,f2(f4(x45392,x45393,a1),a1),a1),f4(x45394,f4(x45395,x45396,a1),a1),x45397))), % 262.80/262.75 inference(scs_inference,[],[24,2725,2620,2721,3153,1878,43,12,10,8,11,13,7,9,5,4,6,34,2,3])). % 262.80/262.75 cnf(5734,plain, % 262.80/262.75 ($false), % 262.80/262.75 inference(scs_inference,[],[81,4536,1883,2992,4539,4,9,5,12,8,10,7,11,13,2,16]), % 262.80/262.75 ['proof']). % 262.80/262.75 % SZS output end Proof % 262.80/262.75 % Total time :261.940000s %------------------------------------------------------------------------------