%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : ANA031-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 : n021.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:58 EDT 2024 % Result : Unsatisfiable 79.91s 80.18s % Output : CNFRefutation 79.97s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : ANA031-2 : TPTP v8.2.0. Released v3.2.0. % 0.03/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n021.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 : Sun Jun 23 04:23:38 EDT 2024 % 0.12/0.34 % CPUTime : % 0.50/0.60 start to proof:theBenchmark % 79.91/80.16 %------------------------------------------- % 79.91/80.16 % File :CSE---1.7 % 79.91/80.16 % Problem :theBenchmark % 79.91/80.16 % Transform :cnf % 79.91/80.16 % Format :tptp:raw % 79.91/80.16 % Command :java -jar mcs_scs.jar %d %s % 79.91/80.16 % 79.91/80.16 % Result :Theorem 79.330000s % 79.91/80.16 % Output :CNFRefutation 79.330000s % 79.91/80.16 %------------------------------------------- % 79.91/80.18 %------------------------------------------------------------------------------ % 79.91/80.18 % File : ANA031-2 : TPTP v8.2.0. Released v3.2.0. % 79.91/80.18 % Domain : Analysis % 79.91/80.18 % Problem : Problem about Big-O notation % 79.91/80.18 % Version : [Pau06] axioms : Reduced > Especial. % 79.91/80.18 % English : % 79.91/80.18 % 79.91/80.18 % Refs : [Pau06] Paulson (2006), Email to G. Sutcliffe % 79.91/80.18 % Source : [Pau06] % 79.91/80.18 % Names : % 79.91/80.18 % 79.91/80.18 % Status : Unsatisfiable % 79.91/80.18 % Rating : 0.06 v8.2.0, 0.17 v8.1.0, 0.00 v7.5.0, 0.10 v7.4.0, 0.11 v7.2.0, 0.12 v7.1.0, 0.14 v6.3.0, 0.17 v6.2.0, 0.00 v6.1.0, 0.20 v6.0.0, 0.22 v5.5.0, 0.44 v5.4.0, 0.47 v5.3.0, 0.58 v5.2.0, 0.25 v5.1.0, 0.29 v4.1.0, 0.33 v3.3.0, 0.43 v3.2.0 % 79.91/80.18 % Syntax : Number of clauses : 11 ( 3 unt; 0 nHn; 7 RR) % 79.91/80.18 % Number of literals : 21 ( 2 equ; 11 neg) % 79.91/80.18 % Maximal clause size : 4 ( 1 avg) % 79.91/80.18 % Maximal term depth : 6 ( 2 avg) % 79.91/80.18 % Number of predicates : 7 ( 6 usr; 0 prp; 1-3 aty) % 79.91/80.18 % Number of functors : 9 ( 9 usr; 3 con; 0-3 aty) % 79.91/80.18 % Number of variables : 19 ( 1 sgn) % 79.91/80.18 % SPC : CNF_UNS_RFO_SEQ_HRN % 79.91/80.18 % 79.91/80.18 % Comments : The problems in the [Pau06] collection each have very many axioms, % 79.91/80.18 % of which only a small selection are required for the refutation. % 79.91/80.18 % The mission is to find those few axioms, after which a refutation % 79.91/80.18 % can be quite easily found. This version has only the necessary % 79.91/80.18 % axioms. % 79.91/80.18 %------------------------------------------------------------------------------ % 79.91/80.18 cnf(cls_conjecture_0,negated_conjecture, % 79.91/80.18 c_lessequals(c_HOL_Oabs(v_b(V_U),t_b),c_times(v_c,c_HOL_Oabs(v_g(V_U),t_b),t_b),t_b) ). % 79.91/80.18 % 79.91/80.18 cnf(cls_conjecture_1,negated_conjecture, % 79.91/80.18 ~ c_lessequals(c_times(c_HOL_Oabs(v_b(v_x(V_U)),t_b),c_HOL_Oabs(v_f(v_x(V_U)),t_b),t_b),c_times(V_U,c_times(c_HOL_Oabs(v_f(v_x(V_U)),t_b),c_HOL_Oabs(v_g(v_x(V_U)),t_b),t_b),t_b),t_b) ). % 79.91/80.18 % 79.91/80.18 cnf(cls_OrderedGroup_Oabs__ge__zero_0,axiom, % 79.91/80.18 ( ~ class_OrderedGroup_Olordered__ab__group__abs(T_a) % 79.91/80.18 | c_lessequals(c_0,c_HOL_Oabs(V_a,T_a),T_a) ) ). % 79.91/80.18 % 79.91/80.18 cnf(cls_OrderedGroup_Omult__ac__1_0,axiom, % 79.91/80.18 ( ~ class_OrderedGroup_Osemigroup__mult(T_a) % 79.91/80.18 | 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) ) ). % 79.91/80.18 % 79.91/80.18 cnf(cls_OrderedGroup_Omult__ac__2_0,axiom, % 79.91/80.18 ( ~ class_OrderedGroup_Oab__semigroup__mult(T_a) % 79.91/80.18 | c_times(V_a,V_b,T_a) = c_times(V_b,V_a,T_a) ) ). % 79.91/80.18 % 79.91/80.18 cnf(cls_Ring__and__Field_Opordered__semiring__class_Omult__left__mono_0,axiom, % 79.91/80.18 ( ~ class_Ring__and__Field_Opordered__semiring(T_a) % 79.91/80.18 | ~ c_lessequals(V_a,V_b,T_a) % 79.91/80.18 | ~ c_lessequals(c_0,V_c,T_a) % 79.91/80.18 | c_lessequals(c_times(V_c,V_a,T_a),c_times(V_c,V_b,T_a),T_a) ) ). % 79.91/80.18 % 79.91/80.18 cnf(clsrel_Ring__and__Field_Oordered__idom_17,axiom, % 79.91/80.18 ( ~ class_Ring__and__Field_Oordered__idom(T) % 79.91/80.18 | class_OrderedGroup_Oab__semigroup__mult(T) ) ). % 79.91/80.18 % 79.91/80.18 cnf(clsrel_Ring__and__Field_Oordered__idom_21,axiom, % 79.91/80.18 ( ~ class_Ring__and__Field_Oordered__idom(T) % 79.91/80.18 | class_OrderedGroup_Osemigroup__mult(T) ) ). % 79.91/80.18 % 79.91/80.18 cnf(clsrel_Ring__and__Field_Oordered__idom_42,axiom, % 79.91/80.18 ( ~ class_Ring__and__Field_Oordered__idom(T) % 79.91/80.18 | class_Ring__and__Field_Opordered__semiring(T) ) ). % 79.91/80.18 % 79.91/80.18 cnf(clsrel_Ring__and__Field_Oordered__idom_50,axiom, % 79.91/80.18 ( ~ class_Ring__and__Field_Oordered__idom(T) % 79.91/80.18 | class_OrderedGroup_Olordered__ab__group__abs(T) ) ). % 79.91/80.18 % 79.91/80.18 cnf(tfree_tcs,negated_conjecture, % 79.91/80.18 class_Ring__and__Field_Oordered__idom(t_b) ). % 79.91/80.18 % 79.91/80.18 %------------------------------------------------------------------------------ % 79.91/80.18 %------------------------------------------- % 79.91/80.18 % Proof found % 79.91/80.18 % SZS status Theorem for theBenchmark % 79.91/80.18 % SZS output start Proof % 79.91/80.19 %ClaNum:31(EqnAxiom:20) % 79.91/80.19 %VarNum:50(SingletonVarNum:19) % 79.91/80.19 %MaxLitNum:4 % 79.91/80.19 %MaxfuncDepth:5 % 79.91/80.19 %SharedTerms:4 % 79.91/80.19 %goalClause: 21 22 23 % 79.91/80.19 %singleGoalClaCount:3 % 79.91/80.19 [21]P1(a1) % 79.91/80.19 [22]P2(f2(f5(x221),a1),f4(a6,f2(f7(x221),a1),a1),a1) % 79.91/80.19 [23]~P2(f4(f2(f5(f9(x231)),a1),f2(f8(f9(x231)),a1),a1),f4(x231,f4(f2(f8(f9(x231)),a1),f2(f7(f9(x231)),a1),a1),a1),a1) % 79.91/80.19 [24]~P1(x241)+P3(x241) % 79.91/80.19 [25]~P1(x251)+P5(x251) % 79.91/80.19 [26]~P1(x261)+P4(x261) % 79.91/80.19 [27]~P1(x271)+P6(x271) % 79.91/80.19 [28]~P3(x282)+P2(a3,f2(x281,x282),x282) % 79.91/80.19 [29]~P4(x293)+E(f4(x291,x292,x293),f4(x292,x291,x293)) % 79.91/80.19 [30]~P5(x303)+E(f4(f4(x301,x302,x303),x304,x303),f4(x301,f4(x302,x304,x303),x303)) % 79.91/80.19 [31]~P6(x313)+~P2(x312,x314,x313)+~P2(a3,x311,x313)+P2(f4(x311,x312,x313),f4(x311,x314,x313),x313) % 79.91/80.19 %EqnAxiom % 79.91/80.19 [1]E(x11,x11) % 79.91/80.19 [2]E(x22,x21)+~E(x21,x22) % 79.91/80.19 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 79.91/80.19 [4]~E(x41,x42)+E(f5(x41),f5(x42)) % 79.91/80.19 [5]~E(x51,x52)+E(f2(x51,x53),f2(x52,x53)) % 79.91/80.19 [6]~E(x61,x62)+E(f2(x63,x61),f2(x63,x62)) % 79.91/80.19 [7]~E(x71,x72)+E(f7(x71),f7(x72)) % 79.91/80.19 [8]~E(x81,x82)+E(f4(x81,x83,x84),f4(x82,x83,x84)) % 79.91/80.19 [9]~E(x91,x92)+E(f4(x93,x91,x94),f4(x93,x92,x94)) % 79.91/80.19 [10]~E(x101,x102)+E(f4(x103,x104,x101),f4(x103,x104,x102)) % 79.91/80.19 [11]~E(x111,x112)+E(f9(x111),f9(x112)) % 79.91/80.19 [12]~E(x121,x122)+E(f8(x121),f8(x122)) % 79.91/80.19 [13]~P1(x131)+P1(x132)+~E(x131,x132) % 79.91/80.19 [14]P2(x142,x143,x144)+~E(x141,x142)+~P2(x141,x143,x144) % 79.91/80.19 [15]P2(x153,x152,x154)+~E(x151,x152)+~P2(x153,x151,x154) % 79.91/80.19 [16]P2(x163,x164,x162)+~E(x161,x162)+~P2(x163,x164,x161) % 79.91/80.19 [17]~P5(x171)+P5(x172)+~E(x171,x172) % 79.91/80.19 [18]~P3(x181)+P3(x182)+~E(x181,x182) % 79.91/80.19 [19]~P4(x191)+P4(x192)+~E(x191,x192) % 79.91/80.19 [20]~P6(x201)+P6(x202)+~E(x201,x202) % 79.91/80.19 % 79.91/80.19 %------------------------------------------- % 79.97/80.22 cnf(41,plain, % 79.97/80.22 (P2(a3,f2(x411,a1),a1)), % 79.97/80.22 inference(scs_inference,[],[21,24,28])). % 79.97/80.22 cnf(46,plain, % 79.97/80.22 (E(f4(f4(x461,x462,a1),x463,a1),f4(x461,f4(x462,x463,a1),a1))), % 79.97/80.22 inference(scs_inference,[],[21,25,30])). % 79.97/80.22 cnf(47,plain, % 79.97/80.22 (E(f4(x471,f4(x472,x473,a1),a1),f4(f4(x471,x472,a1),x473,a1))), % 79.97/80.22 inference(scs_inference,[],[46,2])). % 79.97/80.22 cnf(163,plain, % 79.97/80.22 (E(f4(x1631,x1632,a1),f4(x1632,x1631,a1))), % 79.97/80.22 inference(scs_inference,[],[21,29,26])). % 79.97/80.22 cnf(164,plain, % 79.97/80.22 (P2(f2(f5(x1641),a1),f4(f2(f7(x1641),a1),a6,a1),a1)), % 79.97/80.22 inference(scs_inference,[],[22,163,15])). % 79.97/80.22 cnf(286,plain, % 79.97/80.22 (E(f4(x2861,f4(x2862,x2863,a1),a1),f4(x2862,f4(x2863,x2861,a1),a1))), % 79.97/80.22 inference(scs_inference,[],[163,46,3])). % 79.97/80.22 cnf(289,plain, % 79.97/80.22 (E(f4(x2891,f4(x2892,x2893,a1),a1),f4(x2893,f4(x2891,x2892,a1),a1))), % 79.97/80.22 inference(scs_inference,[],[163,46,3,2])). % 79.97/80.22 cnf(299,plain, % 79.97/80.22 (E(f4(f4(x2991,x2992,a1),x2993,a1),f4(f4(x2992,x2993,a1),x2991,a1))), % 79.97/80.22 inference(scs_inference,[],[163,47,3,2])). % 79.97/80.22 cnf(572,plain, % 79.97/80.22 (E(f4(x5721,f4(f4(x5722,x5723,a1),x5724,a1),a1),f4(x5722,f4(x5723,f4(x5724,x5721,a1),a1),a1))), % 79.97/80.22 inference(scs_inference,[],[286,46,3])). % 79.97/80.22 cnf(575,plain, % 79.97/80.22 (E(f4(x5751,f4(x5752,f4(x5753,x5754,a1),a1),a1),f4(x5754,f4(f4(x5751,x5752,a1),x5753,a1),a1))), % 79.97/80.22 inference(scs_inference,[],[286,46,3,2])). % 79.97/80.22 cnf(626,plain, % 79.97/80.22 (E(f4(x6261,f4(x6262,f4(x6263,x6264,a1),a1),a1),f4(x6263,f4(x6264,f4(x6261,x6262,a1),a1),a1))), % 79.97/80.22 inference(scs_inference,[],[286,572,3])). % 79.97/80.22 cnf(1304,plain, % 79.97/80.22 (E(f4(x13041,f4(x13042,x13043,a1),a1),f4(f4(x13043,x13041,a1),x13042,a1))), % 79.97/80.22 inference(scs_inference,[],[289,47,3])). % 79.97/80.22 cnf(1306,plain, % 79.97/80.22 (E(f4(f4(x13061,x13062,a1),x13063,a1),f4(x13062,f4(x13063,x13061,a1),a1))), % 79.97/80.22 inference(scs_inference,[],[289,47,3,2])). % 79.97/80.22 cnf(4016,plain, % 79.97/80.22 (E(f4(x40161,f4(f4(x40162,f4(x40163,x40164,a1),a1),x40165,a1),a1),f4(x40164,f4(f4(f4(x40165,x40161,a1),x40162,a1),x40163,a1),a1))), % 79.97/80.22 inference(scs_inference,[],[572,1306,3,2])). % 79.97/80.22 cnf(6029,plain, % 79.97/80.22 (E(f4(x60291,f4(x60292,f4(x60293,f4(x60294,x60295,a1),a1),a1),a1),f4(x60294,f4(x60295,f4(f4(x60291,x60292,a1),x60293,a1),a1),a1))), % 79.97/80.22 inference(scs_inference,[],[575,46,3])). % 79.97/80.22 cnf(6032,plain, % 79.97/80.22 (E(f4(x60321,f4(x60322,f4(f4(x60323,x60324,a1),x60325,a1),a1),a1),f4(x60323,f4(x60324,f4(x60325,f4(x60321,x60322,a1),a1),a1),a1))), % 79.97/80.22 inference(scs_inference,[],[575,46,3,2])). % 79.97/80.22 cnf(6810,plain, % 79.97/80.22 (P6(a1)), % 79.97/80.22 inference(scs_inference,[],[21,4016,4,7,11,12,5,6,8,10,9,24,27])). % 79.97/80.22 cnf(6816,plain, % 79.97/80.22 (~P2(f4(f2(f8(f9(x68161)),a1),f2(f5(f9(x68161)),a1),a1),f4(x68161,f4(f2(f8(f9(x68161)),a1),f2(f7(f9(x68161)),a1),a1),a1),a1)), % 79.97/80.22 inference(scs_inference,[],[21,4016,23,163,4,7,11,12,5,6,8,10,9,24,27,26,25,14])). % 79.97/80.22 cnf(6818,plain, % 79.97/80.22 (P2(f4(f2(x68181,a1),a3,a1),f4(f2(x68181,a1),f2(x68181,a1),a1),a1)), % 79.97/80.22 inference(scs_inference,[],[21,4016,23,163,41,4,7,11,12,5,6,8,10,9,24,27,26,25,14,31])). % 79.97/80.22 cnf(6836,plain, % 79.97/80.22 (P2(f4(f2(x68361,a1),f4(f2(x68362,a1),a3,a1),a1),f4(f2(x68361,a1),f4(f2(x68362,a1),f2(x68362,a1),a1),a1),a1)), % 79.97/80.22 inference(scs_inference,[],[6810,6818,6029,41,4,6,12,11,5,7,8,10,9,31])). % 79.97/80.22 cnf(6850,plain, % 79.97/80.22 (P2(f4(f2(x68501,a1),f2(f5(x68502),a1),a1),f4(f2(x68501,a1),f4(f2(f7(x68502),a1),a6,a1),a1),a1)), % 79.97/80.22 inference(scs_inference,[],[164,6810,6032,41,4,7,6,11,12,5,8,10,9,31])). % 79.97/80.22 cnf(6894,plain, % 79.97/80.22 (E(f4(f4(f4(x68941,x68942,a1),x68943,a1),x68944,x68945),f4(f4(f4(x68942,x68943,a1),x68941,a1),x68944,x68945))), % 79.97/80.22 inference(scs_inference,[],[299,4,11,6,12,7,5,9,10,8])). % 79.97/80.22 cnf(6937,plain, % 79.97/80.22 (P2(f4(f4(a3,f2(x69371,a1),a1),f2(x69372,a1),a1),f4(f2(x69371,a1),f4(f2(x69372,a1),f2(x69372,a1),a1),a1),a1)), % 79.97/80.22 inference(scs_inference,[],[6894,6836,1304,4,11,6,12,5,7,9,10,8,14])). % 79.97/80.22 cnf(8018,plain, % 79.97/80.22 (E(f9(f4(x80181,f4(x80182,f4(x80183,x80184,a1),a1),a1)),f9(f4(x80183,f4(x80184,f4(x80181,x80182,a1),a1),a1)))), % 79.97/80.22 inference(scs_inference,[],[626,5,6,11])). % 79.97/80.22 cnf(8072,plain, % 79.97/80.22 (E(f4(f4(f4(x80721,x80722,a1),x80723,a1),x80724,x80725),f4(f4(x80721,f4(x80722,x80723,a1),a1),x80724,x80725))), % 79.97/80.22 inference(scs_inference,[],[46,8])). % 79.97/80.22 cnf(8074,plain, % 79.97/80.22 (E(f4(x80741,f4(f4(x80742,x80743,a1),x80744,a1),x80745),f4(x80741,f4(x80742,f4(x80743,x80744,a1),a1),x80745))), % 79.97/80.22 inference(scs_inference,[],[46,8,7,9])). % 79.97/80.22 cnf(8081,plain, % 79.97/80.22 (~P2(f4(f2(f8(f9(x80811)),a1),f2(f5(f9(x80811)),a1),a1),f4(f4(x80811,f2(f8(f9(x80811)),a1),a1),f2(f7(f9(x80811)),a1),a1),a1)), % 79.97/80.22 inference(scs_inference,[],[46,8018,6816,8,7,9,5,6,11,10,4,12,15])). % 79.97/80.22 cnf(8101,plain, % 79.97/80.22 ($false), % 79.97/80.22 inference(scs_inference,[],[46,6937,8072,8074,6850,8081,1304,8,7,9,5,6,11,10,4,12,14,15]), % 79.97/80.22 ['proof']). % 79.97/80.23 % SZS output end Proof % 79.97/80.23 % Total time :79.330000s %------------------------------------------------------------------------------