%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : NUM498+3 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n011.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 : 600s % DateTime : Mon Jul 18 14:26:50 EDT 2022 % Result : Theorem 0.18s 0.53s % Output : Refutation 0.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : NUM498+3 : TPTP v8.1.0. Released v4.0.0. % 0.11/0.13 % Command : run_spass %d %s % 0.12/0.34 % Computer : n011.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 : 600 % 0.12/0.34 % DateTime : Tue Jul 5 12:14:37 EDT 2022 % 0.12/0.34 % CPUTime : % 0.18/0.53 % 0.18/0.53 SPASS V 3.9 % 0.18/0.53 SPASS beiseite: Proof found. % 0.18/0.53 % SZS status Theorem % 0.18/0.53 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.18/0.53 SPASS derived 533 clauses, backtracked 77 clauses, performed 3 splits and kept 361 clauses. % 0.18/0.53 SPASS allocated 98301 KBytes. % 0.18/0.53 SPASS spent 0:00:00.18 on the problem. % 0.18/0.53 0:00:00.04 for the input. % 0.18/0.53 0:00:00.04 for the FLOTTER CNF translation. % 0.18/0.53 0:00:00.01 for inferences. % 0.18/0.53 0:00:00.00 for the backtracking. % 0.18/0.53 0:00:00.06 for the reduction. % 0.18/0.53 % 0.18/0.53 % 0.18/0.53 Here is a proof with depth 3, length 66 : % 0.18/0.53 % SZS output start Refutation % 0.18/0.53 1[0:Inp] || -> aNaturalNumber0(sz00)*. % 0.18/0.53 3[0:Inp] || -> aNaturalNumber0(xn)*. % 0.18/0.53 4[0:Inp] || -> aNaturalNumber0(xm)*. % 0.18/0.53 5[0:Inp] || -> aNaturalNumber0(xp)*. % 0.18/0.53 7[0:Inp] || -> isPrime0(xp)*. % 0.18/0.53 14[0:Inp] || -> aNaturalNumber0(skf11(u))*. % 0.18/0.53 17[0:Inp] || doDivides0(xp,xn)* -> . % 0.18/0.53 23[0:Inp] || equal(xp,sz00)** -> . % 0.18/0.53 24[0:Inp] || equal(xp,sz10)** -> . % 0.18/0.53 27[0:Inp] || equal(xp,xn)** -> . % 0.18/0.53 28[0:Inp] || equal(xp,xm)** -> . % 0.18/0.53 33[0:Inp] || -> equal(xk,sz10)** equal(xk,sz00). % 0.18/0.53 37[0:Inp] || -> equal(sdtasdt0(xp,xk),sdtasdt0(xn,xm))**. % 0.18/0.53 41[0:Inp] aNaturalNumber0(u) || -> equal(sdtasdt0(u,sz10),u)**. % 0.18/0.53 42[0:Inp] aNaturalNumber0(u) || -> equal(sdtasdt0(sz10,u),u)**. % 0.18/0.53 43[0:Inp] aNaturalNumber0(u) || -> equal(sdtasdt0(u,sz00),sz00)**. % 0.18/0.53 45[0:Inp] aNaturalNumber0(u) || equal(sdtasdt0(xp,u),xn)** -> . % 0.18/0.53 46[0:Inp] aNaturalNumber0(u) || equal(sdtasdt0(xp,u),xm)** -> . % 0.18/0.53 57[0:Inp] || -> SkP1(u) equal(u,sz10) equal(u,sz00) doDivides0(skf11(u),u)*. % 0.18/0.53 64[0:Inp] || equal(skf11(u),sz10)** -> SkP1(u) equal(u,sz10) equal(u,sz00). % 0.18/0.53 65[0:Inp] || equal(skf11(u),u)** -> SkP1(u) equal(u,sz10) equal(u,sz00). % 0.18/0.53 66[0:Inp] aNaturalNumber0(u) || doDivides0(u,xp)* -> equal(u,xp) equal(u,sz10). % 0.18/0.53 79[0:Inp] aNaturalNumber0(u) aNaturalNumber0(v) || equal(sdtasdt0(v,u),sz00)** -> equal(u,sz00) equal(v,sz00). % 0.18/0.53 84[0:Inp] aNaturalNumber0(u) aNaturalNumber0(v) || equal(sdtasdt0(u,v),xp)** -> equal(u,xp) equal(u,sz10). % 0.18/0.53 86[0:Inp] aNaturalNumber0(u) aNaturalNumber0(v) aNaturalNumber0(w) || doDivides0(v,u)* doDivides0(w,v)* -> doDivides0(w,u)*. % 0.18/0.53 122[0:Res:86.5,17.0] aNaturalNumber0(xp) aNaturalNumber0(u) aNaturalNumber0(xn) || doDivides0(xp,u)* doDivides0(u,xn)* -> . % 0.18/0.53 132[0:Res:1.0,46.0] || equal(sdtasdt0(xp,sz00),xm)** -> . % 0.18/0.53 148[0:Res:1.0,45.0] || equal(sdtasdt0(xp,sz00),xn)** -> . % 0.18/0.53 161[0:MRR:122.0,122.2,5.0,3.0] aNaturalNumber0(u) || doDivides0(u,xn)*+ doDivides0(xp,u)* -> . % 0.18/0.53 164[1:Spt:33.0] || -> equal(xk,sz10)**. % 0.18/0.53 167[1:Rew:164.0,37.0] || -> equal(sdtasdt0(xp,sz10),sdtasdt0(xn,xm))**. % 0.18/0.53 179[0:SpL:43.1,148.0] aNaturalNumber0(xp) || equal(xn,sz00)** -> . % 0.18/0.53 180[0:SpL:43.1,132.0] aNaturalNumber0(xp) || equal(xm,sz00)** -> . % 0.18/0.53 181[0:SSi:179.0,7.0,5.0] || equal(xn,sz00)** -> . % 0.18/0.53 182[0:SSi:180.0,7.0,5.0] || equal(xm,sz00)** -> . % 0.18/0.53 186[1:SpR:41.1,167.0] aNaturalNumber0(xp) || -> equal(sdtasdt0(xn,xm),xp)**. % 0.18/0.53 190[1:SSi:186.0,7.0,5.0] || -> equal(sdtasdt0(xn,xm),xp)**. % 0.18/0.53 250[0:Res:57.3,161.1] aNaturalNumber0(skf11(xn)) || doDivides0(xp,skf11(xn))* -> SkP1(xn) equal(xn,sz10) equal(xn,sz00). % 0.18/0.53 252[0:SSi:250.0,14.0,3.0] || doDivides0(xp,skf11(xn))* -> SkP1(xn) equal(xn,sz10) equal(xn,sz00). % 0.18/0.53 253[0:MRR:252.3,181.0] || doDivides0(xp,skf11(xn))* -> SkP1(xn) equal(xn,sz10). % 0.18/0.53 256[2:Spt:253.2] || -> equal(xn,sz10)**. % 0.18/0.53 272[2:Rew:256.0,190.0] || -> equal(sdtasdt0(sz10,xm),xp)**. % 0.18/0.53 285[2:SpR:272.0,42.1] aNaturalNumber0(xm) || -> equal(xp,xm)**. % 0.18/0.53 288[2:SSi:285.0,4.0] || -> equal(xp,xm)**. % 0.18/0.53 289[2:MRR:288.0,28.0] || -> . % 0.18/0.53 291[2:Spt:289.0,253.2,256.0] || equal(xn,sz10)** -> . % 0.18/0.53 292[2:Spt:289.0,253.0,253.1] || doDivides0(xp,skf11(xn))* -> SkP1(xn). % 0.18/0.53 379[0:Res:57.3,66.1] aNaturalNumber0(skf11(xp)) || -> SkP1(xp) equal(xp,sz10) equal(xp,sz00) equal(skf11(xp),xp)** equal(skf11(xp),sz10). % 0.18/0.53 380[0:SSi:379.0,14.0,7.0,5.0] || -> SkP1(xp) equal(xp,sz10) equal(xp,sz00) equal(skf11(xp),xp)** equal(skf11(xp),sz10). % 0.18/0.53 381[0:MRR:380.1,380.2,24.0,23.0] || -> SkP1(xp) equal(skf11(xp),xp)** equal(skf11(xp),sz10). % 0.18/0.53 402[0:SpL:381.1,65.0] || equal(xp,xp) -> SkP1(xp) equal(skf11(xp),sz10)** SkP1(xp) equal(xp,sz10) equal(xp,sz00). % 0.18/0.53 403[0:Obv:402.1] || -> equal(skf11(xp),sz10)** SkP1(xp) equal(xp,sz10) equal(xp,sz00). % 0.18/0.53 404[0:MRR:403.0,403.2,403.3,64.0,24.0,23.0] || -> SkP1(xp)*. % 0.18/0.53 786[1:SpL:190.0,84.2] aNaturalNumber0(xn) aNaturalNumber0(xm) || equal(xp,xp)* -> equal(xp,xn) equal(xn,sz10). % 0.18/0.53 789[1:Obv:786.2] aNaturalNumber0(xn) aNaturalNumber0(xm) || -> equal(xp,xn)** equal(xn,sz10). % 0.18/0.53 790[1:SSi:789.1,789.0,4.0,3.0] || -> equal(xp,xn)** equal(xn,sz10). % 0.18/0.53 791[2:MRR:790.0,790.1,27.0,291.0] || -> . % 0.18/0.53 800[1:Spt:791.0,33.0,164.0] || equal(xk,sz10)** -> . % 0.18/0.53 801[1:Spt:791.0,33.1] || -> equal(xk,sz00)**. % 0.18/0.53 804[1:Rew:801.0,37.0] || -> equal(sdtasdt0(xp,sz00),sdtasdt0(xn,xm))**. % 0.18/0.53 831[1:SpR:804.0,43.1] aNaturalNumber0(xp) || -> equal(sdtasdt0(xn,xm),sz00)**. % 0.18/0.53 838[1:SSi:831.0,7.0,5.0,404.0] || -> equal(sdtasdt0(xn,xm),sz00)**. % 0.18/0.53 906[1:SpL:838.0,79.2] aNaturalNumber0(xm) aNaturalNumber0(xn) || equal(sz00,sz00) -> equal(xm,sz00)** equal(xn,sz00). % 0.18/0.53 916[1:Obv:906.2] aNaturalNumber0(xm) aNaturalNumber0(xn) || -> equal(xm,sz00)** equal(xn,sz00). % 0.18/0.53 917[1:SSi:916.1,916.0,3.0,4.0] || -> equal(xm,sz00)** equal(xn,sz00). % 0.18/0.53 918[1:MRR:917.0,917.1,182.0,181.0] || -> . % 0.18/0.53 % SZS output end Refutation % 0.18/0.53 Formulae used in the proof : mSortsC m__1837 m__1860 m__1799 m__2306 m__ m__2287 m_MulUnit m_MulZero mZeroMul mDivTrans % 0.18/0.53 %------------------------------------------------------------------------------