%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : NUM836+2 : TPTP v8.2.0. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 12:26:39 EDT 2024
% Result : Theorem 1.62s 1.73s
% Output : CNFRefutation 1.62s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : NUM836+2 : TPTP v8.2.0. Released v4.1.0.
% 0.04/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.13/0.34 % Computer : n001.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 02:21:54 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.53/0.58 start to proof:theBenchmark
% 1.62/1.72 %-------------------------------------------
% 1.62/1.72 % File :CSE---1.7
% 1.62/1.72 % Problem :theBenchmark
% 1.62/1.72 % Transform :cnf
% 1.62/1.72 % Format :tptp:raw
% 1.62/1.72 % Command :java -jar mcs_scs.jar %d %s
% 1.62/1.72
% 1.62/1.72 % Result :Theorem 1.090000s
% 1.62/1.72 % Output :CNFRefutation 1.090000s
% 1.62/1.72 %-------------------------------------------
% 1.62/1.72 %------------------------------------------------------------------------------
% 1.62/1.72 % File : NUM836+2 : TPTP v8.2.0. Released v4.1.0.
% 1.62/1.72 % Domain : Number Theory
% 1.62/1.72 % Problem : dis(ex(cond(conseq(131),0),1))
% 1.62/1.72 % Version : Especial: Reduced > Especial.
% 1.62/1.72 % English :
% 1.62/1.72
% 1.62/1.72 % Refs : [Lan30] Landau (1930), Grundlagen der Analysis
% 1.62/1.72 % : [Kue09] Kuehlwein (2009), Email to Geoff Sutcliffe
% 1.62/1.72 % : [KC+10] Kuehlwein et al. (2010), Premise Selection in the Napr
% 1.62/1.72 % Source : [Kue09]
% 1.62/1.72 % Names :
% 1.62/1.72
% 1.62/1.72 % Status : Theorem
% 1.62/1.72 % Rating : 0.14 v8.2.0, 0.17 v8.1.0, 0.19 v7.4.0, 0.17 v7.3.0, 0.21 v7.1.0, 0.26 v7.0.0, 0.23 v6.4.0, 0.31 v6.3.0, 0.29 v6.2.0, 0.36 v6.1.0, 0.33 v6.0.0, 0.30 v5.5.0, 0.33 v5.4.0, 0.32 v5.3.0, 0.37 v5.2.0, 0.25 v5.1.0, 0.29 v5.0.0, 0.25 v4.1.0
% 1.62/1.72 % Syntax : Number of formulae : 11 ( 1 unt; 0 def)
% 1.62/1.72 % Number of atoms : 22 ( 17 equ)
% 1.62/1.72 % Maximal formula atoms : 3 ( 2 avg)
% 1.62/1.72 % Number of connectives : 23 ( 12 ~; 7 |; 1 &)
% 1.62/1.72 % ( 2 <=>; 1 =>; 0 <=; 0 <~>)
% 1.62/1.72 % Maximal formula depth : 6 ( 5 avg)
% 1.62/1.72 % Maximal term depth : 3 ( 1 avg)
% 1.62/1.72 % Number of predicates : 3 ( 2 usr; 0 prp; 2-2 aty)
% 1.62/1.72 % Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% 1.62/1.72 % Number of variables : 28 ( 20 !; 8 ?)
% 1.62/1.72 % SPC : FOF_THM_RFO_SEQ
% 1.62/1.72
% 1.62/1.72 % Comments : From the Landau in Naproche 0.45 collection.
% 1.62/1.72 % : This version uses a filtered set of axioms.
% 1.62/1.72 %------------------------------------------------------------------------------
% 1.62/1.72 fof('dis(ex(cond(conseq(131), 0), 1))',conjecture,
% 1.62/1.72 ( ~ greater(vd203,vd204)
% 1.62/1.72 | ~ less(vd203,vd204) ) ).
% 1.62/1.72
% 1.62/1.72 fof('dis(ex(cond(conseq(131), 0), 0))',axiom,
% 1.62/1.72 ( vd203 != vd204
% 1.62/1.72 | ~ greater(vd203,vd204) ) ).
% 1.62/1.72
% 1.62/1.72 fof('def(cond(conseq(axiom(3)), 12), 1)',axiom,
% 1.62/1.72 ! [Vd198,Vd199] :
% 1.62/1.72 ( less(Vd199,Vd198)
% 1.62/1.72 <=> ? [Vd201] : Vd198 = vplus(Vd199,Vd201) ) ).
% 1.62/1.72
% 1.62/1.72 fof('def(cond(conseq(axiom(3)), 11), 1)',axiom,
% 1.62/1.72 ! [Vd193,Vd194] :
% 1.62/1.72 ( greater(Vd194,Vd193)
% 1.62/1.72 <=> ? [Vd196] : Vd194 = vplus(Vd193,Vd196) ) ).
% 1.62/1.72
% 1.62/1.72 fof('ass(cond(goal(88), 0), 0)',axiom,
% 1.62/1.72 ! [Vd120,Vd121] :
% 1.62/1.72 ( Vd120 = Vd121
% 1.62/1.72 | ? [Vd123] : Vd120 = vplus(Vd121,Vd123)
% 1.62/1.72 | ? [Vd125] : Vd121 = vplus(Vd120,Vd125) ) ).
% 1.62/1.72
% 1.62/1.72 fof('ass(cond(goal(88), 0), 1)',axiom,
% 1.62/1.72 ! [Vd120,Vd121] :
% 1.62/1.72 ( Vd120 != Vd121
% 1.62/1.72 | ~ ? [Vd125] : Vd121 = vplus(Vd120,Vd125) ) ).
% 1.62/1.72
% 1.62/1.72 fof('ass(cond(goal(88), 0), 2)',axiom,
% 1.62/1.72 ! [Vd120,Vd121] :
% 1.62/1.72 ( ~ ? [Vd123] : Vd120 = vplus(Vd121,Vd123)
% 1.62/1.72 | ~ ? [Vd125] : Vd121 = vplus(Vd120,Vd125) ) ).
% 1.62/1.72
% 1.62/1.72 fof('ass(cond(goal(88), 0), 3)',axiom,
% 1.62/1.72 ! [Vd120,Vd121] :
% 1.62/1.72 ( Vd120 != Vd121
% 1.62/1.72 | ~ ? [Vd123] : Vd120 = vplus(Vd121,Vd123) ) ).
% 1.62/1.72
% 1.62/1.72 fof('ass(cond(81, 0), 0)',axiom,
% 1.62/1.72 ! [Vd104,Vd105] :
% 1.62/1.72 ( Vd104 != Vd105
% 1.62/1.72 => ! [Vd107] : vplus(Vd107,Vd104) != vplus(Vd107,Vd105) ) ).
% 1.62/1.72
% 1.62/1.72 fof('ass(cond(33, 0), 0)',axiom,
% 1.62/1.72 ! [Vd46,Vd47,Vd48] : vplus(vplus(Vd46,Vd47),Vd48) = vplus(Vd46,vplus(Vd47,Vd48)) ).
% 1.62/1.72
% 1.62/1.72 fof('qu(cond(conseq(axiom(3)), 3), and(holds(definiens(29), 45, 0), holds(definiens(29), 44, 0)))',axiom,
% 1.62/1.72 ! [Vd42,Vd43] :
% 1.62/1.72 ( vplus(Vd42,vsucc(Vd43)) = vsucc(vplus(Vd42,Vd43))
% 1.62/1.72 & vplus(Vd42,v1) = vsucc(Vd42) ) ).
% 1.62/1.72
% 1.62/1.72 %------------------------------------------------------------------------------
% 1.62/1.72 %-------------------------------------------
% 1.62/1.72 % Proof found
% 1.62/1.73 % SZS status Theorem for theBenchmark
% 1.62/1.73 % SZS output start Proof
% 1.62/1.73 %ClaNum:31(EqnAxiom:17)
% 1.62/1.73 %VarNum:60(SingletonVarNum:28)
% 1.62/1.73 %MaxLitNum:3
% 1.62/1.73 %MaxfuncDepth:2
% 1.62/1.73 %SharedTerms:7
% 1.62/1.73 %goalClause: 18 19
% 1.62/1.73 %singleGoalClaCount:2
% 1.62/1.73 [18]P1(a1,a7)
% 1.62/1.73 [19]P2(a1,a7)
% 1.62/1.73 [21]E(f8(f8(x211,x212),x213),f8(x211,f8(x212,x213)))
% 1.62/1.73 [22]~E(a1,a7)+~P1(a1,a7)
% 1.62/1.73 [29]~P2(x291,x292)+E(f8(x291,f3(x292,x291)),x292)
% 1.62/1.73 [30]~P1(x302,x301)+E(f8(x301,f4(x301,x302)),x302)
% 1.62/1.73 [23]~E(x231,x232)+~E(x232,f8(x231,x233))
% 1.62/1.73 [24]~E(x241,x242)+~E(x241,f8(x242,x243))
% 1.62/1.73 [25]P1(x251,x252)+~E(x251,f8(x252,x253))
% 1.62/1.73 [26]P2(x261,x262)+~E(x262,f8(x261,x263))
% 1.62/1.73 [27]E(x271,x272)+~E(f8(x273,x271),f8(x273,x272))
% 1.62/1.73 [28]~E(x281,f8(x282,x283))+~E(x282,f8(x281,x284))
% 1.62/1.73 [31]E(x311,x312)+E(f8(x311,f5(x311,x312)),x312)+E(f8(x312,f6(x311,x312)),x311)
% 1.62/1.73 %EqnAxiom
% 1.62/1.73 [1]E(x11,x11)
% 1.62/1.73 [2]E(x22,x21)+~E(x21,x22)
% 1.62/1.73 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 1.62/1.73 [4]~E(x41,x42)+E(f8(x41,x43),f8(x42,x43))
% 1.62/1.73 [5]~E(x51,x52)+E(f8(x53,x51),f8(x53,x52))
% 1.62/1.73 [6]~E(x61,x62)+E(f6(x61,x63),f6(x62,x63))
% 1.62/1.73 [7]~E(x71,x72)+E(f6(x73,x71),f6(x73,x72))
% 1.62/1.73 [8]~E(x81,x82)+E(f5(x81,x83),f5(x82,x83))
% 1.62/1.73 [9]~E(x91,x92)+E(f5(x93,x91),f5(x93,x92))
% 1.62/1.73 [10]~E(x101,x102)+E(f4(x101,x103),f4(x102,x103))
% 1.62/1.73 [11]~E(x111,x112)+E(f4(x113,x111),f4(x113,x112))
% 1.62/1.73 [12]~E(x121,x122)+E(f3(x121,x123),f3(x122,x123))
% 1.62/1.73 [13]~E(x131,x132)+E(f3(x133,x131),f3(x133,x132))
% 1.62/1.73 [14]P1(x142,x143)+~E(x141,x142)+~P1(x141,x143)
% 1.62/1.73 [15]P1(x153,x152)+~E(x151,x152)+~P1(x153,x151)
% 1.62/1.73 [16]P2(x162,x163)+~E(x161,x162)+~P2(x161,x163)
% 1.62/1.73 [17]P2(x173,x172)+~E(x171,x172)+~P2(x173,x171)
% 1.62/1.73
% 1.62/1.73 %-------------------------------------------
% 1.62/1.73 cnf(33,plain,
% 1.62/1.73 (P2(x331,f8(x331,x332))),
% 1.62/1.73 inference(equality_inference,[],[26])).
% 1.62/1.73 cnf(47,plain,
% 1.62/1.73 (~E(a1,f8(a7,x471))),
% 1.62/1.73 inference(scs_inference,[],[19,21,23,24,25,26,28,29,16])).
% 1.62/1.73 cnf(158,plain,
% 1.62/1.73 (~P2(a7,a1)),
% 1.62/1.73 inference(scs_inference,[],[47,2,29])).
% 1.62/1.73 cnf(301,plain,
% 1.62/1.73 ($false),
% 1.62/1.73 inference(scs_inference,[],[158,18,33,17,30]),
% 1.62/1.73 ['proof']).
% 1.62/1.73 % SZS output end Proof
% 1.62/1.73 % Total time :1.090000s
%------------------------------------------------------------------------------