%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : NUM532+1 : TPTP v8.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n029.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:24:52 EDT 2024 % Result : Theorem 2.31s 2.36s % Output : CNFRefutation 2.31s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.13 % Problem : NUM532+1 : TPTP v8.2.0. Released v4.0.0. % 0.08/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.14/0.35 % Computer : n029.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Sat Jun 22 19:45:24 EDT 2024 % 0.14/0.35 % CPUTime : % 0.21/0.59 start to proof:theBenchmark % 2.24/2.36 %------------------------------------------- % 2.24/2.36 % File :CSE---1.7 % 2.24/2.36 % Problem :theBenchmark % 2.24/2.36 % Transform :cnf % 2.24/2.36 % Format :tptp:raw % 2.24/2.36 % Command :java -jar mcs_scs.jar %d %s % 2.24/2.36 % 2.24/2.36 % Result :Theorem 1.730000s % 2.24/2.36 % Output :CNFRefutation 1.730000s % 2.24/2.36 %------------------------------------------- % 2.24/2.36 %------------------------------------------------------------------------------ % 2.24/2.36 % File : NUM532+1 : TPTP v8.2.0. Released v4.0.0. % 2.24/2.36 % Domain : Number Theory % 2.24/2.36 % Problem : Ramsey's Infinite Theorem 02, 00 expansion % 2.24/2.36 % Version : Especial. % 2.24/2.36 % English : % 2.24/2.36 % 2.24/2.36 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 2.24/2.36 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 2.24/2.36 % Source : [Pas08] % 2.24/2.36 % Names : ramsey_02.00 [Pas08] % 2.24/2.36 % 2.24/2.36 % Status : Theorem % 2.24/2.36 % Rating : 0.06 v8.2.0, 0.08 v8.1.0, 0.06 v7.5.0, 0.09 v7.4.0, 0.13 v7.3.0, 0.10 v7.2.0, 0.07 v7.1.0, 0.00 v7.0.0, 0.07 v6.4.0, 0.12 v6.3.0, 0.04 v6.1.0, 0.07 v6.0.0, 0.00 v5.5.0, 0.04 v5.4.0, 0.07 v5.2.0, 0.05 v5.1.0, 0.14 v5.0.0, 0.21 v4.1.0, 0.26 v4.0.1, 0.57 v4.0.0 % 2.24/2.36 % Syntax : Number of formulae : 13 ( 3 unt; 2 def) % 2.24/2.36 % Number of atoms : 34 ( 2 equ) % 2.24/2.36 % Maximal formula atoms : 5 ( 2 avg) % 2.24/2.36 % Number of connectives : 24 ( 3 ~; 0 |; 5 &) % 2.24/2.36 % ( 2 <=>; 14 =>; 0 <=; 0 <~>) % 2.24/2.36 % Maximal formula depth : 8 ( 4 avg) % 2.24/2.36 % Maximal term depth : 1 ( 1 avg) % 2.24/2.36 % Number of predicates : 8 ( 6 usr; 1 prp; 0-2 aty) % 2.24/2.36 % Number of functors : 2 ( 2 usr; 2 con; 0-0 aty) % 2.24/2.36 % Number of variables : 15 ( 14 !; 1 ?) % 2.24/2.36 % SPC : FOF_THM_RFO_SEQ % 2.24/2.36 % 2.24/2.36 % Comments : Problem generated by the SAD system [VLP07] % 2.24/2.36 %------------------------------------------------------------------------------ % 2.24/2.36 fof(mSetSort,axiom, % 2.24/2.36 ! [W0] : % 2.24/2.36 ( aSet0(W0) % 2.24/2.36 => $true ) ). % 2.24/2.36 % 2.24/2.36 fof(mElmSort,axiom, % 2.24/2.36 ! [W0] : % 2.24/2.36 ( aElement0(W0) % 2.24/2.36 => $true ) ). % 2.24/2.36 % 2.24/2.36 fof(mEOfElem,axiom, % 2.24/2.36 ! [W0] : % 2.24/2.36 ( aSet0(W0) % 2.24/2.36 => ! [W1] : % 2.24/2.36 ( aElementOf0(W1,W0) % 2.24/2.36 => aElement0(W1) ) ) ). % 2.24/2.36 % 2.24/2.36 fof(mFinRel,axiom, % 2.24/2.36 ! [W0] : % 2.24/2.36 ( aSet0(W0) % 2.24/2.36 => ( isFinite0(W0) % 2.24/2.36 => $true ) ) ). % 2.24/2.36 % 2.24/2.36 fof(mDefEmp,definition, % 2.24/2.36 ! [W0] : % 2.24/2.36 ( W0 = slcrc0 % 2.24/2.36 <=> ( aSet0(W0) % 2.24/2.36 & ~ ? [W1] : aElementOf0(W1,W0) ) ) ). % 2.24/2.36 % 2.24/2.36 fof(mEmpFin,axiom, % 2.24/2.36 isFinite0(slcrc0) ). % 2.24/2.36 % 2.24/2.36 fof(mCntRel,axiom, % 2.24/2.36 ! [W0] : % 2.24/2.36 ( aSet0(W0) % 2.24/2.36 => ( isCountable0(W0) % 2.24/2.36 => $true ) ) ). % 2.24/2.36 % 2.24/2.36 fof(mCountNFin,axiom, % 2.24/2.36 ! [W0] : % 2.24/2.36 ( ( aSet0(W0) % 2.24/2.36 & isCountable0(W0) ) % 2.24/2.36 => ~ isFinite0(W0) ) ). % 2.24/2.36 % 2.24/2.36 fof(mCountNFin_01,axiom, % 2.24/2.36 ! [W0] : % 2.24/2.36 ( ( aSet0(W0) % 2.31/2.36 & isCountable0(W0) ) % 2.31/2.36 => W0 != slcrc0 ) ). % 2.31/2.36 % 2.31/2.36 fof(mDefSub,definition, % 2.31/2.36 ! [W0] : % 2.31/2.36 ( aSet0(W0) % 2.31/2.36 => ! [W1] : % 2.31/2.36 ( aSubsetOf0(W1,W0) % 2.31/2.36 <=> ( aSet0(W1) % 2.31/2.36 & ! [W2] : % 2.31/2.36 ( aElementOf0(W2,W1) % 2.31/2.36 => aElementOf0(W2,W0) ) ) ) ) ). % 2.31/2.36 % 2.31/2.36 fof(mSubFSet,axiom, % 2.31/2.36 ! [W0] : % 2.31/2.36 ( ( aSet0(W0) % 2.31/2.36 & isFinite0(W0) ) % 2.31/2.36 => ! [W1] : % 2.31/2.36 ( aSubsetOf0(W1,W0) % 2.31/2.36 => isFinite0(W1) ) ) ). % 2.31/2.36 % 2.31/2.36 fof(m__467,hypothesis, % 2.31/2.36 aSet0(xA) ). % 2.31/2.36 % 2.31/2.36 fof(m__,conjecture, % 2.31/2.36 aSubsetOf0(xA,xA) ). % 2.31/2.36 % 2.31/2.36 %------------------------------------------------------------------------------ % 2.31/2.36 %------------------------------------------- % 2.31/2.36 % Proof found % 2.31/2.36 % SZS status Theorem for theBenchmark % 2.31/2.36 % SZS output start Proof % 2.31/2.36 %ClaNum:28(EqnAxiom:14) % 2.31/2.36 %VarNum:49(SingletonVarNum:19) % 2.31/2.36 %MaxLitNum:4 % 2.31/2.36 %MaxfuncDepth:1 % 2.31/2.36 %SharedTerms:5 % 2.31/2.36 %goalClause: 17 % 2.31/2.36 %singleGoalClaCount:1 % 2.31/2.36 [15]P1(a1) % 2.31/2.36 [16]P4(a2) % 2.31/2.36 [17]~P5(a1,a1) % 2.31/2.36 [18]P1(x181)+~E(x181,a2) % 2.31/2.36 [21]~P2(x212,x211)+~E(x211,a2) % 2.31/2.36 [19]~P1(x191)+~P6(x191)+~E(x191,a2) % 2.31/2.36 [20]~P4(x201)+~P6(x201)+~P1(x201) % 2.31/2.36 [22]~P1(x221)+P2(f3(x221),x221)+E(x221,a2) % 2.31/2.36 [23]~P5(x231,x232)+P1(x231)+~P1(x232) % 2.31/2.36 [24]~P2(x241,x242)+P3(x241)+~P1(x242) % 2.31/2.36 [25]~P4(x252)+~P5(x251,x252)+P4(x251)+~P1(x252) % 2.31/2.37 [27]~P1(x271)+~P1(x272)+P5(x271,x272)+P2(f4(x272,x271),x271) % 2.31/2.37 [28]~P1(x281)+~P1(x282)+P5(x281,x282)+~P2(f4(x282,x281),x282) % 2.31/2.37 [26]~P1(x262)+~P5(x263,x262)+P2(x261,x262)+~P2(x261,x263) % 2.31/2.37 %EqnAxiom % 2.31/2.37 [1]E(x11,x11) % 2.31/2.37 [2]E(x22,x21)+~E(x21,x22) % 2.31/2.37 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 2.31/2.37 [4]~E(x41,x42)+E(f3(x41),f3(x42)) % 2.31/2.37 [5]~E(x51,x52)+E(f4(x51,x53),f4(x52,x53)) % 2.31/2.37 [6]~E(x61,x62)+E(f4(x63,x61),f4(x63,x62)) % 2.31/2.37 [7]~P1(x71)+P1(x72)+~E(x71,x72) % 2.31/2.37 [8]~P4(x81)+P4(x82)+~E(x81,x82) % 2.31/2.37 [9]P5(x92,x93)+~E(x91,x92)+~P5(x91,x93) % 2.31/2.37 [10]P5(x103,x102)+~E(x101,x102)+~P5(x103,x101) % 2.31/2.37 [11]P2(x112,x113)+~E(x111,x112)+~P2(x111,x113) % 2.31/2.37 [12]P2(x123,x122)+~E(x121,x122)+~P2(x123,x121) % 2.31/2.37 [13]~P3(x131)+P3(x132)+~E(x131,x132) % 2.31/2.37 [14]~P6(x141)+P6(x142)+~E(x141,x142) % 2.31/2.37 % 2.31/2.37 %------------------------------------------- % 2.31/2.37 cnf(287,plain, % 2.31/2.37 (~E(x2871,a1)+~P1(a1)+P1(x2871)), % 2.31/2.37 inference(scs_inference,[],[15,7,2])). % 2.31/2.37 cnf(289,plain, % 2.31/2.37 (P1(x2891)+~E(x2891,a1)), % 2.31/2.37 inference(scs_inference,[],[15,287])). % 2.31/2.37 cnf(291,plain, % 2.31/2.37 (~P2(f4(a1,a1),a1)), % 2.31/2.37 inference(scs_inference,[],[17,289,28])). % 2.31/2.37 cnf(292,plain, % 2.31/2.37 ($false), % 2.31/2.37 inference(scs_inference,[],[17,291,15,27]), % 2.31/2.37 ['proof']). % 2.31/2.37 % SZS output end Proof % 2.31/2.37 % Total time :1.730000s %------------------------------------------------------------------------------