%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : NUM487+3 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n005.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:42 EDT 2022 % Result : Theorem 0.67s 0.92s % Output : Refutation 0.67s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : NUM487+3 : TPTP v8.1.0. Released v4.0.0. % 0.07/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n005.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 : 600 % 0.13/0.34 % DateTime : Wed Jul 6 09:25:07 EDT 2022 % 0.13/0.34 % CPUTime : % 0.67/0.92 % 0.67/0.92 SPASS V 3.9 % 0.67/0.92 SPASS beiseite: Proof found. % 0.67/0.92 % SZS status Theorem % 0.67/0.92 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.67/0.92 SPASS derived 1575 clauses, backtracked 47 clauses, performed 7 splits and kept 734 clauses. % 0.67/0.92 SPASS allocated 100136 KBytes. % 0.67/0.92 SPASS spent 0:00:00.54 on the problem. % 0.67/0.92 0:00:00.03 for the input. % 0.67/0.92 0:00:00.04 for the FLOTTER CNF translation. % 0.67/0.92 0:00:00.02 for inferences. % 0.67/0.92 0:00:00.00 for the backtracking. % 0.67/0.92 0:00:00.42 for the reduction. % 0.67/0.92 % 0.67/0.92 % 0.67/0.92 Here is a proof with depth 2, length 69 : % 0.67/0.92 % SZS output start Refutation % 0.67/0.92 1[0:Inp] || -> aNaturalNumber0(sz00)*. % 0.67/0.92 5[0:Inp] || -> aNaturalNumber0(xp)*. % 0.67/0.92 7[0:Inp] || -> isPrime0(xp)*. % 0.67/0.92 8[0:Inp] || -> aNaturalNumber0(skc3)*. % 0.67/0.92 9[0:Inp] || -> aNaturalNumber0(xr)*. % 0.67/0.92 13[0:Inp] || -> aNaturalNumber0(skf11(u))*. % 0.67/0.92 14[0:Inp] || -> sdtlseqdt0(xp,xn)*. % 0.67/0.92 19[0:Inp] || equal(xp,sz00)** -> . % 0.67/0.92 20[0:Inp] || equal(xp,sz10)** -> . % 0.67/0.92 23[0:Inp] || -> equal(sdtpldt0(xp,skc3),xn)**. % 0.67/0.92 24[0:Inp] || -> equal(sdtpldt0(xp,xr),xn)**. % 0.67/0.92 25[0:Inp] || -> equal(sdtmndt0(xn,xp),xr)**. % 0.67/0.92 27[0:Inp] || sdtlseqdt0(xr,xn)* -> equal(xn,xr). % 0.67/0.92 30[0:Inp] aNaturalNumber0(u) || -> equal(sdtpldt0(u,sz00),u)**. % 0.67/0.92 31[0:Inp] aNaturalNumber0(u) || -> equal(sdtpldt0(sz00,u),u)**. % 0.67/0.92 41[0:Inp] aNaturalNumber0(u) || equal(sdtpldt0(xr,u),xn)** -> equal(xn,xr). % 0.67/0.92 45[0:Inp] || -> SkP1(u) equal(u,sz10) equal(u,sz00) doDivides0(skf11(u),u)*. % 0.67/0.92 46[0:Inp] aNaturalNumber0(u) aNaturalNumber0(v) || -> equal(sdtpldt0(v,u),sdtpldt0(u,v))*. % 0.67/0.92 52[0:Inp] || equal(skf11(u),sz10)** -> SkP1(u) equal(u,sz10) equal(u,sz00). % 0.67/0.92 53[0:Inp] || equal(skf11(u),u)** -> SkP1(u) equal(u,sz10) equal(u,sz00). % 0.67/0.92 54[0:Inp] aNaturalNumber0(u) || doDivides0(u,xp)* -> equal(u,xp) equal(u,sz10). % 0.67/0.92 68[0:Inp] aNaturalNumber0(u) aNaturalNumber0(v) aNaturalNumber0(w) || equal(sdtpldt0(v,w),u)*+ -> sdtlseqdt0(v,u)*. % 0.67/0.92 69[0:Inp] aNaturalNumber0(u) aNaturalNumber0(v) || sdtlseqdt0(v,u) equal(w,sdtmndt0(u,v))*+ -> aNaturalNumber0(w)*. % 0.67/0.92 76[0:Inp] aNaturalNumber0(u) aNaturalNumber0(v) aNaturalNumber0(w) || equal(sdtpldt0(v,w),sdtpldt0(u,w))* -> equal(v,u). % 0.67/0.92 93[0:Inp] aNaturalNumber0(u) aNaturalNumber0(v) aNaturalNumber0(w) || sdtlseqdt0(v,w) equal(sdtpldt0(v,u),w)* -> equal(u,sdtmndt0(w,v))*. % 0.67/0.92 102[0:MRR:93.3,68.4] aNaturalNumber0(u) aNaturalNumber0(v) aNaturalNumber0(w) || equal(sdtpldt0(v,w),u)*+ -> equal(w,sdtmndt0(u,v))*. % 0.67/0.92 108[0:Res:5.0,41.0] || equal(sdtpldt0(xr,xp),xn)** -> equal(xn,xr). % 0.67/0.92 120[1:Spt:41.0,41.1] aNaturalNumber0(u) || equal(sdtpldt0(xr,u),xn)** -> . % 0.67/0.92 121[2:Spt:27.1] || -> equal(xn,xr)**. % 0.67/0.92 122[2:Rew:121.0,120.1] aNaturalNumber0(u) || equal(sdtpldt0(xr,u),xr)** -> . % 0.67/0.92 146[2:SpL:30.1,122.1] aNaturalNumber0(xr) aNaturalNumber0(sz00) || equal(xr,xr)* -> . % 0.67/0.92 147[2:Obv:146.2] aNaturalNumber0(xr) aNaturalNumber0(sz00) || -> . % 0.67/0.92 148[2:SSi:147.1,147.0,1.0,9.0] || -> . % 0.67/0.92 149[2:Spt:148.0,27.1,121.0] || equal(xn,xr)** -> . % 0.67/0.92 150[2:Spt:148.0,27.0] || sdtlseqdt0(xr,xn)* -> . % 0.67/0.92 155[2:MRR:108.1,149.0] || equal(sdtpldt0(xr,xp),xn)** -> . % 0.67/0.92 216[0:Res:45.3,54.1] aNaturalNumber0(skf11(xp)) || -> SkP1(xp) equal(xp,sz10) equal(xp,sz00) equal(skf11(xp),xp)** equal(skf11(xp),sz10). % 0.67/0.92 217[0:SSi:216.0,13.0,7.0,5.0] || -> SkP1(xp) equal(xp,sz10) equal(xp,sz00) equal(skf11(xp),xp)** equal(skf11(xp),sz10). % 0.67/0.92 218[0:MRR:217.1,217.2,20.0,19.0] || -> SkP1(xp) equal(skf11(xp),xp)** equal(skf11(xp),sz10). % 0.67/0.92 255[0:SpL:218.1,53.0] || equal(xp,xp) -> SkP1(xp) equal(skf11(xp),sz10)** SkP1(xp) equal(xp,sz10) equal(xp,sz00). % 0.67/0.92 256[0:Obv:255.1] || -> equal(skf11(xp),sz10)** SkP1(xp) equal(xp,sz10) equal(xp,sz00). % 0.67/0.92 257[0:MRR:256.0,256.2,256.3,52.0,20.0,19.0] || -> SkP1(xp)*. % 0.67/0.92 330[2:SpL:46.2,155.0] aNaturalNumber0(xr) aNaturalNumber0(xp) || equal(sdtpldt0(xp,xr),xn)** -> . % 0.67/0.92 345[2:Rew:24.0,330.2] aNaturalNumber0(xr) aNaturalNumber0(xp) || equal(xn,xn)* -> . % 0.67/0.92 346[2:Obv:345.2] aNaturalNumber0(xr) aNaturalNumber0(xp) || -> . % 0.67/0.92 347[2:SSi:346.1,346.0,7.0,5.0,257.0,9.0] || -> . % 0.67/0.92 358[1:Spt:347.0,41.2] || -> equal(xn,xr)**. % 0.67/0.92 360[1:Rew:358.0,14.0] || -> sdtlseqdt0(xp,xr)*. % 0.67/0.92 361[1:Rew:358.0,23.0] || -> equal(sdtpldt0(xp,skc3),xr)**. % 0.67/0.92 362[1:Rew:358.0,24.0] || -> equal(sdtpldt0(xp,xr),xr)**. % 0.67/0.92 363[1:Rew:358.0,25.0] || -> equal(sdtmndt0(xr,xp),xr)**. % 0.67/0.92 960[1:SpL:363.0,69.3] aNaturalNumber0(xr) aNaturalNumber0(xp) || sdtlseqdt0(xp,xr)* equal(u,xr) -> aNaturalNumber0(u)*. % 0.67/0.92 961[1:SSi:960.1,960.0,7.0,5.0,257.0,9.0] || sdtlseqdt0(xp,xr)* equal(u,xr) -> aNaturalNumber0(u)*. % 0.67/0.92 962[1:MRR:961.0,360.0] || equal(u,xr) -> aNaturalNumber0(u)*. % 0.67/0.92 1263[1:SpL:362.0,102.3] aNaturalNumber0(u) aNaturalNumber0(xp) aNaturalNumber0(xr) || equal(xr,u) -> equal(sdtmndt0(u,xp),xr)**. % 0.67/0.92 1264[1:SpL:361.0,102.3] aNaturalNumber0(u) aNaturalNumber0(xp) aNaturalNumber0(skc3) || equal(xr,u) -> equal(sdtmndt0(u,xp),skc3)**. % 0.67/0.92 1267[1:SSi:1263.2,1263.1,9.0,7.0,5.0,257.0] aNaturalNumber0(u) || equal(xr,u) -> equal(sdtmndt0(u,xp),xr)**. % 0.67/0.92 1268[1:MRR:1267.0,962.1] || equal(xr,u) -> equal(sdtmndt0(u,xp),xr)**. % 0.67/0.92 1269[1:Rew:1268.1,1264.4] aNaturalNumber0(u) aNaturalNumber0(xp) aNaturalNumber0(skc3) || equal(xr,u)* -> equal(xr,skc3)**. % 0.67/0.92 1270[1:SSi:1269.2,1269.1,8.0,7.0,5.0,257.0] aNaturalNumber0(u) || equal(xr,u)* -> equal(xr,skc3)**. % 0.67/0.92 1271[1:MRR:1270.0,962.1] || equal(xr,u)*+ -> equal(xr,skc3)**. % 0.67/0.92 1285[1:EqR:1271.0] || -> equal(xr,skc3)**. % 0.67/0.92 1294[1:Rew:1285.0,362.0] || -> equal(sdtpldt0(xp,skc3),skc3)**. % 0.67/0.92 1444[1:SpL:1294.0,76.3] aNaturalNumber0(u) aNaturalNumber0(xp) aNaturalNumber0(skc3) || equal(sdtpldt0(u,skc3),skc3)** -> equal(xp,u). % 0.67/0.92 1452[1:SSi:1444.2,1444.1,8.0,7.0,5.0,257.0] aNaturalNumber0(u) || equal(sdtpldt0(u,skc3),skc3)** -> equal(xp,u). % 0.67/0.92 2630[1:SpL:31.1,1452.1] aNaturalNumber0(skc3) aNaturalNumber0(sz00) || equal(skc3,skc3)* -> equal(xp,sz00). % 0.67/0.92 2636[1:Obv:2630.2] aNaturalNumber0(skc3) aNaturalNumber0(sz00) || -> equal(xp,sz00)**. % 0.67/0.92 2637[1:SSi:2636.1,2636.0,1.0,8.0] || -> equal(xp,sz00)**. % 0.67/0.92 2638[1:MRR:2637.0,19.0] || -> . % 0.67/0.92 % SZS output end Refutation % 0.67/0.92 Formulae used in the proof : mSortsC m__1837 m__1860 m__1870 m__1883 m__1799 m__ m_AddZero mAddComm mDefLE mDefDiff mAddCanc % 0.67/0.92 %------------------------------------------------------------------------------