%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : ANA023-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 : 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 04:13:56 EDT 2024 % Result : Unsatisfiable 59.27s 59.48s % Output : CNFRefutation 59.27s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : ANA023-2 : TPTP v8.2.0. Released v3.2.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n023.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Sun Jun 23 04:32:54 EDT 2024 % 0.12/0.33 % CPUTime : % 0.42/0.62 start to proof:theBenchmark % 59.27/59.47 %------------------------------------------- % 59.27/59.47 % File :CSE---1.7 % 59.27/59.47 % Problem :theBenchmark % 59.27/59.47 % Transform :cnf % 59.27/59.47 % Format :tptp:raw % 59.27/59.47 % Command :java -jar mcs_scs.jar %d %s % 59.27/59.47 % 59.27/59.47 % Result :Theorem 58.690000s % 59.27/59.47 % Output :CNFRefutation 58.690000s % 59.27/59.47 %------------------------------------------- % 59.27/59.48 %------------------------------------------------------------------------------ % 59.27/59.48 % File : ANA023-2 : TPTP v8.2.0. Released v3.2.0. % 59.27/59.48 % Domain : Analysis % 59.27/59.48 % Problem : Problem about Big-O notation % 59.27/59.48 % Version : [Pau06] axioms : Reduced > Especial. % 59.27/59.48 % English : % 59.27/59.48 % 59.27/59.48 % Refs : [Pau06] Paulson (2006), Email to G. Sutcliffe % 59.27/59.48 % Source : [Pau06] % 59.27/59.48 % Names : % 59.27/59.48 % 59.27/59.48 % Status : Unsatisfiable % 59.27/59.48 % Rating : 0.00 v5.3.0, 0.08 v5.2.0, 0.00 v5.0.0, 0.14 v4.1.0, 0.11 v4.0.1, 0.17 v3.3.0, 0.14 v3.2.0 % 59.27/59.48 % Syntax : Number of clauses : 12 ( 4 unt; 0 nHn; 11 RR) % 59.27/59.48 % Number of literals : 24 ( 1 equ; 13 neg) % 59.27/59.48 % Maximal clause size : 4 ( 2 avg) % 59.27/59.48 % Maximal term depth : 3 ( 1 avg) % 59.27/59.48 % Number of predicates : 7 ( 6 usr; 0 prp; 1-3 aty) % 59.27/59.48 % Number of functors : 8 ( 8 usr; 3 con; 0-3 aty) % 59.27/59.48 % Number of variables : 18 ( 0 sgn) % 59.27/59.48 % SPC : CNF_UNS_RFO_SEQ_HRN % 59.27/59.48 % 59.27/59.48 % Comments : The problems in the [Pau06] collection each have very many axioms, % 59.27/59.48 % of which only a small selection are required for the refutation. % 59.27/59.48 % The mission is to find those few axioms, after which a refutation % 59.27/59.48 % can be quite easily found. This version has only the necessary % 59.27/59.48 % axioms. % 59.27/59.48 %------------------------------------------------------------------------------ % 59.27/59.48 cnf(cls_OrderedGroup_Ocomm__monoid__add__class_Oaxioms_0,axiom, % 59.27/59.48 ( ~ class_OrderedGroup_Ocomm__monoid__add(T_a) % 59.27/59.48 | c_plus(c_0,V_y,T_a) = V_y ) ). % 59.27/59.48 % 59.27/59.48 cnf(cls_OrderedGroup_Ocompare__rls__9_0,axiom, % 59.27/59.48 ( ~ class_OrderedGroup_Opordered__ab__group__add(T_a) % 59.27/59.48 | ~ c_lessequals(V_a,c_minus(V_c,V_b,T_a),T_a) % 59.27/59.48 | c_lessequals(c_plus(V_a,V_b,T_a),V_c,T_a) ) ). % 59.27/59.48 % 59.27/59.48 cnf(cls_OrderedGroup_Ocompare__rls__9_1,axiom, % 59.27/59.48 ( ~ class_OrderedGroup_Opordered__ab__group__add(T_a) % 59.27/59.48 | ~ c_lessequals(c_plus(V_a,V_b,T_a),V_c,T_a) % 59.27/59.48 | c_lessequals(V_a,c_minus(V_c,V_b,T_a),T_a) ) ). % 59.27/59.48 % 59.27/59.48 cnf(cls_Orderings_Oorder__class_Oorder__trans_0,axiom, % 59.27/59.48 ( ~ class_Orderings_Oorder(T_a) % 59.27/59.48 | ~ c_lessequals(V_y,V_z,T_a) % 59.27/59.48 | ~ c_lessequals(V_x,V_y,T_a) % 59.27/59.48 | c_lessequals(V_x,V_z,T_a) ) ). % 59.27/59.48 % 59.27/59.48 cnf(cls_conjecture_1,negated_conjecture, % 59.27/59.48 c_lessequals(c_0,c_minus(v_k(v_x),v_g(v_x),t_b),t_b) ). % 59.27/59.48 % 59.27/59.48 cnf(cls_conjecture_2,negated_conjecture, % 59.27/59.48 c_lessequals(v_k(v_x),v_f(v_x),t_b) ). % 59.27/59.48 % 59.27/59.48 cnf(cls_conjecture_3,negated_conjecture, % 59.27/59.48 ~ c_lessequals(c_0,c_minus(v_f(v_x),v_g(v_x),t_b),t_b) ). % 59.27/59.48 % 59.27/59.48 cnf(clsrel_Orderings_Olinorder_4,axiom, % 59.27/59.48 ( ~ class_Orderings_Olinorder(T) % 59.27/59.48 | class_Orderings_Oorder(T) ) ). % 59.27/59.48 % 59.27/59.48 cnf(clsrel_Ring__and__Field_Oordered__idom_23,axiom, % 59.27/59.48 ( ~ class_Ring__and__Field_Oordered__idom(T) % 59.27/59.48 | class_OrderedGroup_Ocomm__monoid__add(T) ) ). % 59.27/59.48 % 59.27/59.48 cnf(clsrel_Ring__and__Field_Oordered__idom_33,axiom, % 59.27/59.48 ( ~ class_Ring__and__Field_Oordered__idom(T) % 59.27/59.48 | class_Orderings_Olinorder(T) ) ). % 59.27/59.48 % 59.27/59.48 cnf(clsrel_Ring__and__Field_Oordered__idom_54,axiom, % 59.27/59.48 ( ~ class_Ring__and__Field_Oordered__idom(T) % 59.27/59.48 | class_OrderedGroup_Opordered__ab__group__add(T) ) ). % 59.27/59.48 % 59.27/59.48 cnf(tfree_tcs,negated_conjecture, % 59.27/59.48 class_Ring__and__Field_Oordered__idom(t_b) ). % 59.27/59.48 % 59.27/59.48 %------------------------------------------------------------------------------ % 59.27/59.48 %------------------------------------------- % 59.27/59.48 % Proof found % 59.27/59.48 % SZS status Theorem for theBenchmark % 59.27/59.48 % SZS output start Proof % 59.27/59.49 %ClaNum:32(EqnAxiom:20) % 59.27/59.49 %VarNum:44(SingletonVarNum:18) % 59.27/59.49 %MaxLitNum:4 % 59.27/59.49 %MaxfuncDepth:2 % 59.27/59.49 %SharedTerms:12 % 59.27/59.49 %goalClause: 21 22 23 24 % 59.27/59.49 %singleGoalClaCount:4 % 59.27/59.49 [21]P1(a1) % 59.27/59.49 [22]P2(f6(a5),f7(a5),a1) % 59.27/59.49 [23]P2(a2,f3(f6(a5),f8(a5),a1),a1) % 59.27/59.49 [24]~P2(a2,f3(f7(a5),f8(a5),a1),a1) % 59.27/59.49 [25]~P1(x251)+P3(x251) % 59.27/59.49 [26]~P1(x261)+P4(x261) % 59.27/59.49 [27]~P6(x271)+P5(x271) % 59.27/59.49 [28]~P1(x281)+P6(x281) % 59.27/59.49 [29]~P3(x292)+E(f4(a2,x291,x292),x291) % 59.27/59.49 [31]~P4(x314)+~P2(f4(x311,x313,x314),x312,x314)+P2(x311,f3(x312,x313,x314),x314) % 59.27/59.49 [32]~P4(x323)+~P2(x321,f3(x324,x322,x323),x323)+P2(f4(x321,x322,x323),x324,x323) % 59.27/59.49 [30]~P5(x303)+~P2(x304,x302,x303)+P2(x301,x302,x303)+~P2(x301,x304,x303) % 59.27/59.49 %EqnAxiom % 59.27/59.49 [1]E(x11,x11) % 59.27/59.49 [2]E(x22,x21)+~E(x21,x22) % 59.27/59.49 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 59.27/59.49 [4]~E(x41,x42)+E(f6(x41),f6(x42)) % 59.27/59.49 [5]~E(x51,x52)+E(f7(x51),f7(x52)) % 59.27/59.49 [6]~E(x61,x62)+E(f3(x61,x63,x64),f3(x62,x63,x64)) % 59.27/59.49 [7]~E(x71,x72)+E(f3(x73,x71,x74),f3(x73,x72,x74)) % 59.27/59.49 [8]~E(x81,x82)+E(f3(x83,x84,x81),f3(x83,x84,x82)) % 59.27/59.49 [9]~E(x91,x92)+E(f8(x91),f8(x92)) % 59.27/59.49 [10]~E(x101,x102)+E(f4(x101,x103,x104),f4(x102,x103,x104)) % 59.27/59.49 [11]~E(x111,x112)+E(f4(x113,x111,x114),f4(x113,x112,x114)) % 59.27/59.49 [12]~E(x121,x122)+E(f4(x123,x124,x121),f4(x123,x124,x122)) % 59.27/59.49 [13]~P1(x131)+P1(x132)+~E(x131,x132) % 59.27/59.49 [14]P2(x142,x143,x144)+~E(x141,x142)+~P2(x141,x143,x144) % 59.27/59.49 [15]P2(x153,x152,x154)+~E(x151,x152)+~P2(x153,x151,x154) % 59.27/59.49 [16]P2(x163,x164,x162)+~E(x161,x162)+~P2(x163,x164,x161) % 59.27/59.49 [17]~P4(x171)+P4(x172)+~E(x171,x172) % 59.27/59.49 [18]~P5(x181)+P5(x182)+~E(x181,x182) % 59.27/59.49 [19]~P3(x191)+P3(x192)+~E(x191,x192) % 59.27/59.49 [20]~P6(x201)+P6(x202)+~E(x201,x202) % 59.27/59.49 % 59.27/59.49 %------------------------------------------- % 59.27/59.50 cnf(34,plain, % 59.27/59.50 (~E(f6(a5),f7(a5))), % 59.27/59.50 inference(scs_inference,[],[23,24,15,6])). % 59.27/59.50 cnf(35,plain, % 59.27/59.50 (~P4(a1)+~P2(f4(a2,f8(a5),a1),f7(a5),a1)), % 59.27/59.50 inference(scs_inference,[],[23,24,15,6,31])). % 59.27/59.50 cnf(37,plain, % 59.27/59.50 (~P4(a1)+~E(f6(a5),f4(a2,f8(a5),a1))), % 59.27/59.50 inference(scs_inference,[],[22,23,24,15,6,31,14])). % 59.27/59.50 cnf(40,plain, % 59.27/59.50 (P2(x401,f3(f6(a5),f8(a5),a1),a1)+~E(a2,x401)), % 59.27/59.50 inference(scs_inference,[],[23,14])). % 59.27/59.50 cnf(48,plain, % 59.27/59.50 (P2(f6(a5),f7(a5),x481)+~E(a1,x481)), % 59.27/59.50 inference(scs_inference,[],[22,16])). % 59.27/59.50 cnf(59,plain, % 59.27/59.50 (~P6(a1)+~P2(f3(f6(a5),f8(a5),a1),f3(f7(a5),f8(a5),a1),a1)), % 59.27/59.50 inference(scs_inference,[],[24,23,30,27])). % 59.27/59.50 cnf(73,plain, % 59.27/59.50 (E(f4(a2,x731,a1),x731)), % 59.27/59.50 inference(scs_inference,[],[21,25,29])). % 59.27/59.50 cnf(74,plain, % 59.27/59.50 (E(x741,f4(a2,x741,a1))), % 59.27/59.50 inference(scs_inference,[],[73,2])). % 59.27/59.50 cnf(75,plain, % 59.27/59.50 (P1(f4(a2,a1,a1))), % 59.27/59.50 inference(scs_inference,[],[21,73,2,13])). % 59.27/59.50 cnf(76,plain, % 59.27/59.50 (P2(a2,f3(f6(a5),f8(a5),a1),f4(a2,a1,a1))), % 59.27/59.50 inference(scs_inference,[],[21,23,73,2,13,16])). % 59.27/59.50 cnf(77,plain, % 59.27/59.50 (P2(f6(a5),f7(a5),f4(a2,a1,a1))), % 59.27/59.50 inference(scs_inference,[],[21,23,73,2,13,16,48])). % 59.27/59.50 cnf(82,plain, % 59.27/59.50 (P2(f4(a2,a2,a1),f3(f6(a5),f8(a5),a1),a1)), % 59.27/59.50 inference(scs_inference,[],[74,40])). % 59.27/59.50 cnf(83,plain, % 59.27/59.50 (E(x831,f4(a2,x831,a1))), % 59.27/59.50 inference(rename_variables,[],[74])). % 59.27/59.50 cnf(84,plain, % 59.27/59.50 (P2(f4(a2,f6(a5),a1),f7(a5),a1)), % 59.27/59.50 inference(scs_inference,[],[22,74,83,40,14])). % 59.27/59.50 cnf(85,plain, % 59.27/59.50 (E(x851,f4(a2,x851,a1))), % 59.27/59.50 inference(rename_variables,[],[74])). % 59.27/59.50 cnf(87,plain, % 59.27/59.50 (E(x871,f4(a2,x871,a1))), % 59.27/59.50 inference(rename_variables,[],[74])). % 59.27/59.50 cnf(88,plain, % 59.27/59.50 (P2(a2,f3(f6(a5),f8(a5),a1),f4(a2,f4(a2,a1,a1),a1))), % 59.27/59.50 inference(scs_inference,[],[22,76,74,83,85,87,40,14,15,16])). % 59.27/59.50 cnf(94,plain, % 59.27/59.50 (P2(f4(a2,f6(a5),a1),f7(a5),f4(a2,a1,a1))), % 59.27/59.50 inference(scs_inference,[],[77,74,14])). % 59.27/59.50 cnf(95,plain, % 59.27/59.50 (E(x951,f4(a2,x951,a1))), % 59.27/59.50 inference(rename_variables,[],[74])). % 59.27/59.50 cnf(96,plain, % 59.27/59.50 (P2(f6(a5),f4(a2,f7(a5),a1),f4(a2,a1,a1))), % 59.27/59.50 inference(scs_inference,[],[77,74,95,14,15])). % 59.27/59.50 cnf(97,plain, % 59.27/59.50 (E(x971,f4(a2,x971,a1))), % 59.27/59.50 inference(rename_variables,[],[74])). % 59.27/59.50 cnf(98,plain, % 59.27/59.50 (P2(f4(a2,a2,a1),f3(f6(a5),f8(a5),a1),f4(a2,a1,a1))), % 59.27/59.50 inference(scs_inference,[],[77,82,74,95,97,14,15,16])). % 59.27/59.50 cnf(100,plain, % 59.27/59.50 (~P6(f4(a2,x1001,a1))+P6(x1001)), % 59.27/59.50 inference(scs_inference,[],[73,77,82,74,95,97,14,15,16,20])). % 59.27/59.50 cnf(105,plain, % 59.27/59.50 (E(x1051,f4(a2,x1051,a1))), % 59.27/59.50 inference(rename_variables,[],[74])). % 59.27/59.50 cnf(109,plain, % 59.27/59.50 (E(x1091,f4(a2,x1091,a1))), % 59.27/59.50 inference(rename_variables,[],[74])). % 59.27/59.50 cnf(110,plain, % 59.27/59.50 (~P6(x1101)+P6(f4(a2,x1101,a1))), % 59.27/59.50 inference(scs_inference,[],[73,94,88,74,105,109,15,16,14,20])). % 59.27/59.50 cnf(113,plain, % 59.27/59.50 (~P4(f4(a2,x1131,a1))+P4(x1131)), % 59.27/59.50 inference(scs_inference,[],[73,17])). % 59.27/59.50 cnf(118,plain, % 59.27/59.50 (P2(f6(a5),f4(a2,f7(a5),a1),f4(a2,f4(a2,a1,a1),a1))), % 59.27/59.50 inference(scs_inference,[],[74,96,16])). % 59.27/59.50 cnf(119,plain, % 59.27/59.50 (E(x1191,f4(a2,x1191,a1))), % 59.27/59.50 inference(rename_variables,[],[74])). % 59.27/59.50 cnf(120,plain, % 59.27/59.50 (P2(f4(a2,f4(a2,a2,a1),a1),f3(f6(a5),f8(a5),a1),f4(a2,a1,a1))), % 59.27/59.50 inference(scs_inference,[],[74,119,96,98,16,14])). % 59.27/59.50 cnf(121,plain, % 59.27/59.50 (E(x1211,f4(a2,x1211,a1))), % 59.27/59.50 inference(rename_variables,[],[74])). % 59.27/59.50 cnf(122,plain, % 59.27/59.50 (~P4(x1221)+P4(f4(a2,x1221,a1))), % 59.27/59.50 inference(scs_inference,[],[74,119,121,96,98,16,14,17])). % 59.27/59.50 cnf(126,plain, % 59.27/59.50 (P2(f6(a5),f7(a5),f4(a2,f4(a2,a1,a1),a1))), % 59.27/59.50 inference(scs_inference,[],[73,118,15])). % 59.27/59.50 cnf(127,plain, % 59.27/59.50 (E(f4(a2,x1271,a1),x1271)), % 59.27/59.50 inference(rename_variables,[],[73])). % 59.27/59.50 cnf(129,plain, % 59.27/59.50 (E(f4(a2,x1291,a1),x1291)), % 59.27/59.50 inference(rename_variables,[],[73])). % 59.27/59.50 cnf(130,plain, % 59.27/59.50 (~P3(f4(a2,x1301,a1))+P3(x1301)), % 59.27/59.50 inference(scs_inference,[],[73,127,129,118,120,15,16,19])). % 59.27/59.50 cnf(138,plain, % 59.27/59.50 (~P6(f4(a2,x1381,a1))+P5(x1381)), % 59.27/59.50 inference(scs_inference,[],[73,18,27])). % 59.27/59.50 cnf(173,plain, % 59.27/59.50 (~P2(f3(f6(a5),f8(a5),a1),f3(f7(a5),f8(a5),a1),a1)+~P6(f4(a2,a1,a1))), % 59.27/59.50 inference(scs_inference,[],[100,59])). % 59.27/59.50 cnf(189,plain, % 59.27/59.50 (P6(f4(a2,a1,a1))), % 59.27/59.50 inference(scs_inference,[],[21,110,28])). % 59.27/59.50 cnf(190,plain, % 59.27/59.50 (~P2(f3(f6(a5),f8(a5),a1),f3(f7(a5),f8(a5),a1),a1)), % 59.27/59.50 inference(scs_inference,[],[189,173])). % 59.27/59.50 cnf(192,plain, % 59.27/59.50 (P5(a1)), % 59.27/59.50 inference(scs_inference,[],[189,100,138])). % 59.27/59.50 cnf(195,plain, % 59.27/59.50 (E(x1951,f4(a2,x1951,a1))), % 59.27/59.50 inference(rename_variables,[],[74])). % 59.27/59.50 cnf(196,plain, % 59.27/59.50 (P5(f4(a2,a1,a1))), % 59.27/59.50 inference(scs_inference,[],[74,195,189,100,138,20,18])). % 59.27/59.50 cnf(209,plain, % 59.27/59.50 (~P4(a1)+~P2(f4(f3(f6(a5),f8(a5),a1),f8(a5),a1),f7(a5),a1)), % 59.27/59.50 inference(scs_inference,[],[190,74,196,18,31])). % 59.27/59.50 cnf(211,plain, % 59.27/59.50 (~P4(a1)+~E(f6(a5),f4(f3(f6(a5),f8(a5),a1),f8(a5),a1))), % 59.27/59.50 inference(scs_inference,[],[22,190,74,196,18,31,14])). % 59.27/59.50 cnf(280,plain, % 59.27/59.50 (~P2(f4(a2,f8(a5),a1),f7(a5),a1)+~P4(f4(a2,a1,a1))), % 59.27/59.50 inference(scs_inference,[],[113,35])). % 59.27/59.50 cnf(320,plain, % 59.27/59.50 (P4(f4(a2,a1,a1))), % 59.27/59.50 inference(scs_inference,[],[21,122,26])). % 59.27/59.50 cnf(321,plain, % 59.27/59.50 (~P2(f4(a2,f8(a5),a1),f7(a5),a1)), % 59.27/59.50 inference(scs_inference,[],[320,280])). % 59.27/59.50 cnf(322,plain, % 59.27/59.50 (P4(a1)), % 59.27/59.50 inference(scs_inference,[],[320,113])). % 59.27/59.50 cnf(326,plain, % 59.27/59.50 (E(x3261,f4(a2,x3261,a1))), % 59.27/59.50 inference(rename_variables,[],[74])). % 59.27/59.50 cnf(327,plain, % 59.27/59.50 (~E(f6(a5),f4(a2,f8(a5),a1))), % 59.27/59.50 inference(scs_inference,[],[74,320,113,209,211,17,37])). % 59.27/59.50 cnf(328,plain, % 59.27/59.50 (~E(f6(a5),f8(a5))), % 59.27/59.50 inference(scs_inference,[],[74,326,320,113,209,211,17,37,3])). % 59.27/59.50 cnf(330,plain, % 59.27/59.50 (~P2(f4(a2,f8(a5),a1),f7(a5),a1)), % 59.27/59.50 inference(scs_inference,[],[322,35])). % 59.27/59.50 cnf(331,plain, % 59.27/59.50 (~P3(f4(a2,x3311,a1))+E(f4(a2,x3312,x3311),x3312)), % 59.27/59.50 inference(scs_inference,[],[130,29])). % 59.27/59.50 cnf(332,plain, % 59.27/59.50 (~E(f4(a2,f6(a5),a1),f4(a2,f8(a5),a1))), % 59.27/59.50 inference(scs_inference,[],[84,321,14])). % 59.27/59.50 cnf(333,plain, % 59.27/59.50 (~E(f4(a2,f6(a5),a1),f8(a5))), % 59.27/59.50 inference(scs_inference,[],[74,332,3])). % 59.27/59.50 cnf(337,plain, % 59.27/59.50 (E(f6(f4(a2,x3371,a1)),f6(x3371))), % 59.27/59.50 inference(scs_inference,[],[74,4,2])). % 59.27/59.50 cnf(338,plain, % 59.27/59.50 (E(f6(x3381),f6(f4(a2,x3381,a1)))), % 59.27/59.50 inference(scs_inference,[],[337,2])). % 59.27/59.50 cnf(401,plain, % 59.27/59.50 (~E(f6(a5),f4(a2,f7(a5),a1))), % 59.27/59.50 inference(scs_inference,[],[34,73,3])). % 59.27/59.50 cnf(407,plain, % 59.27/59.50 (P1(f4(a2,f4(a2,a1,a1),a1))), % 59.27/59.50 inference(scs_inference,[],[75,74,13])). % 59.27/59.50 cnf(412,plain, % 59.27/59.50 (~P3(f4(a2,x4121,a1))+E(f3(x4122,x4123,f4(a2,x4124,x4121)),f3(x4122,x4123,x4124))), % 59.27/59.50 inference(scs_inference,[],[331,8])). % 59.27/59.50 cnf(414,plain, % 59.27/59.50 (E(f4(x4141,x4142,f4(a2,x4143,a1)),f4(x4141,x4142,x4143))), % 59.27/59.50 inference(scs_inference,[],[74,12,2])). % 59.27/59.50 cnf(415,plain, % 59.27/59.50 (E(f4(x4151,x4152,x4153),f4(x4151,x4152,f4(a2,x4153,a1)))), % 59.27/59.50 inference(scs_inference,[],[414,2])). % 59.27/59.50 cnf(417,plain, % 59.27/59.50 (E(f4(x4171,x4172,f4(a2,x4173,a1)),f4(x4171,x4172,x4173))), % 59.27/59.50 inference(rename_variables,[],[414])). % 59.27/59.50 cnf(418,plain, % 59.27/59.50 (~P1(f4(x4181,x4182,f4(a2,x4183,a1)))+P1(f4(x4181,x4182,x4183))), % 59.27/59.51 inference(scs_inference,[],[332,414,417,2,3,13])). % 59.27/59.51 cnf(432,plain, % 59.27/59.51 (P1(f4(a2,f4(a2,a1,a1),f4(a2,a1,a1)))), % 59.27/59.51 inference(scs_inference,[],[407,415,13])). % 59.27/59.51 cnf(472,plain, % 59.27/59.51 (P3(f4(a2,f4(a2,a1,a1),a1))), % 59.27/59.51 inference(scs_inference,[],[432,418,25])). % 59.27/59.51 cnf(473,plain, % 59.27/59.51 (P3(f4(a2,a1,a1))), % 59.27/59.51 inference(scs_inference,[],[472,130])). % 59.27/59.51 cnf(476,plain, % 59.27/59.51 (E(f3(x4761,x4762,f4(a2,x4763,a1)),f3(x4761,x4762,x4763))), % 59.27/59.51 inference(scs_inference,[],[472,130,331,412])). % 59.27/59.51 cnf(478,plain, % 59.27/59.51 (E(x4781,f4(a2,x4781,f4(a2,a1,a1)))), % 59.27/59.51 inference(scs_inference,[],[472,130,331,412,2])). % 59.27/59.51 cnf(501,plain, % 59.27/59.51 (E(f3(x5011,x5012,x5013),f3(x5011,x5012,f4(a2,x5013,a1)))), % 59.27/59.51 inference(scs_inference,[],[473,476,478,130,40,2])). % 59.27/59.51 cnf(606,plain, % 59.27/59.51 (~E(f6(a5),f4(a2,f7(a5),f4(a2,a1,a1)))), % 59.27/59.51 inference(scs_inference,[],[401,414,3])). % 59.27/59.51 cnf(682,plain, % 59.27/59.51 (E(f4(x6821,x6822,x6823),f4(x6821,x6822,f4(a2,x6823,a1)))), % 59.27/59.51 inference(rename_variables,[],[415])). % 59.27/59.51 cnf(683,plain, % 59.27/59.51 (P2(f6(a5),f4(a2,f7(a5),f4(a2,a1,a1)),f4(a2,a1,a1))), % 59.27/59.51 inference(scs_inference,[],[415,682,96,126,16,15])). % 59.27/59.51 cnf(684,plain, % 59.27/59.51 (E(f4(x6841,x6842,x6843),f4(x6841,x6842,f4(a2,x6843,a1)))), % 59.27/59.51 inference(rename_variables,[],[415])). % 59.27/59.51 cnf(685,plain, % 59.27/59.51 (P2(f4(a2,f6(a5),f4(a2,a1,a1)),f7(a5),f4(a2,a1,a1))), % 59.27/59.51 inference(scs_inference,[],[415,682,684,94,96,126,16,15,14])). % 59.27/59.51 cnf(1176,plain, % 59.27/59.51 (P2(a2,f3(f6(a5),f8(a5),f4(a2,a1,a1)),f4(a2,a1,a1))), % 59.27/59.51 inference(scs_inference,[],[501,76,15])). % 59.27/59.51 cnf(1182,plain, % 59.27/59.51 (P2(f4(a2,a2,a1),f3(f6(a5),f8(a5),f4(a2,a1,a1)),f4(a2,a1,a1))), % 59.27/59.51 inference(scs_inference,[],[501,98,15])). % 59.27/59.51 cnf(1883,plain, % 59.27/59.51 (E(f4(f4(a2,x18831,a1),x18832,x18833),f4(x18831,x18832,x18833))), % 59.27/59.51 inference(scs_inference,[],[73,5,9,7,10])). % 59.27/59.51 cnf(1886,plain, % 59.27/59.51 (~E(f8(a5),f6(a5))), % 59.27/59.51 inference(scs_inference,[],[328,73,5,9,7,10,11,6,2])). % 59.27/59.51 cnf(1891,plain, % 59.27/59.51 (~P2(f4(a2,f8(a5),a1),f7(a5),f4(a2,a1,a1))), % 59.27/59.51 inference(scs_inference,[],[328,330,1182,320,476,73,24,5,9,7,10,11,6,2,32,15,16])). % 59.27/59.51 cnf(1899,plain, % 59.27/59.51 (~P2(f4(a2,f8(a5),a1),f6(a5),a1)), % 59.27/59.51 inference(scs_inference,[],[22,328,330,1182,685,320,414,476,338,73,192,24,5,9,7,10,11,6,2,32,15,16,14,31,3,30])). % 59.27/59.51 cnf(1903,plain, % 59.27/59.51 (E(f4(x19031,x19032,x19033),f4(f4(a2,x19031,a1),x19032,x19033))), % 59.27/59.51 inference(scs_inference,[],[74,5,10])). % 59.27/59.51 cnf(1905,plain, % 59.27/59.51 (E(f8(x19051),f8(f4(a2,x19051,a1)))), % 59.27/59.51 inference(scs_inference,[],[74,5,10,11,9])). % 59.27/59.51 cnf(1906,plain, % 59.27/59.51 (E(f3(x19061,x19062,x19063),f3(x19061,f4(a2,x19062,a1),x19063))), % 59.27/59.51 inference(scs_inference,[],[74,5,10,11,9,7])). % 59.27/59.51 cnf(1907,plain, % 59.27/59.51 (E(f3(x19071,x19072,x19073),f3(f4(a2,x19071,a1),x19072,x19073))), % 59.27/59.51 inference(scs_inference,[],[74,5,10,11,9,7,6])). % 59.27/59.51 cnf(1915,plain, % 59.27/59.51 (~E(f4(a2,f8(a5),f4(a2,a1,a1)),f6(a5))), % 59.27/59.51 inference(scs_inference,[],[1886,333,1883,1891,1176,84,322,320,478,74,5,10,11,9,7,6,2,32,14,31,3])). % 59.27/59.51 cnf(1953,plain, % 59.27/59.51 (~E(f6(f4(a2,a5,a1)),f7(a5))), % 59.27/59.51 inference(scs_inference,[],[1899,606,34,1903,683,338,73,2,15,16,3])). % 59.27/59.51 cnf(1958,plain, % 59.27/59.51 (~E(f4(f4(a2,a2,a1),f8(a5),f4(a2,a1,a1)),f6(a5))), % 59.27/59.51 inference(scs_inference,[],[1915,1953,1903,2,3])). % 59.27/59.51 cnf(1963,plain, % 59.27/59.51 (~E(f8(f4(a2,a5,a1)),f6(a5))), % 59.27/59.51 inference(scs_inference,[],[1958,1905,1886,2,3])). % 59.27/59.51 cnf(1979,plain, % 59.27/59.51 (P2(f4(f4(a2,a2,a1),f8(a5),a1),f6(a5),a1)), % 59.27/59.51 inference(scs_inference,[],[1963,1906,1907,82,322,2,3,32])). % 59.27/59.51 cnf(2010,plain, % 59.27/59.51 ($false), % 59.27/59.51 inference(scs_inference,[],[1979,1899,1883,327,2,14]), % 59.27/59.51 ['proof']). % 59.27/59.51 % SZS output end Proof % 59.27/59.51 % Total time :58.690000s %------------------------------------------------------------------------------