%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : NUM494+3 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n017.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:47 EDT 2022 % Result : Theorem 18.28s 18.46s % Output : Refutation 18.28s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : NUM494+3 : TPTP v8.1.0. Released v4.0.0. % 0.07/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n017.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Thu Jul 7 07:38:15 EDT 2022 % 0.12/0.33 % CPUTime : % 18.28/18.46 % 18.28/18.46 SPASS V 3.9 % 18.28/18.46 SPASS beiseite: Proof found. % 18.28/18.46 % SZS status Theorem % 18.28/18.46 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 18.28/18.46 SPASS derived 24796 clauses, backtracked 4299 clauses, performed 53 splits and kept 11024 clauses. % 18.28/18.46 SPASS allocated 122861 KBytes. % 18.28/18.46 SPASS spent 0:0:13.24 on the problem. % 18.28/18.46 0:00:00.04 for the input. % 18.28/18.46 0:00:00.05 for the FLOTTER CNF translation. % 18.28/18.46 0:00:00.26 for inferences. % 18.28/18.46 0:00:00.36 for the backtracking. % 18.28/18.46 0:0:12.42 for the reduction. % 18.28/18.46 % 18.28/18.46 % 18.28/18.46 Here is a proof with depth 4, length 69 : % 18.28/18.46 % SZS output start Refutation % 18.28/18.46 1[0:Inp] || -> aNaturalNumber0(sz00)*. % 18.28/18.46 3[0:Inp] || -> aNaturalNumber0(xn)*. % 18.28/18.46 4[0:Inp] || -> aNaturalNumber0(xm)*. % 18.28/18.46 5[0:Inp] || -> aNaturalNumber0(xp)*. % 18.28/18.46 7[0:Inp] || -> isPrime0(xp)*. % 18.28/18.46 9[0:Inp] || -> aNaturalNumber0(xr)*. % 18.28/18.46 15[0:Inp] || -> aNaturalNumber0(skf11(u))*. % 18.28/18.46 22[0:Inp] || equal(xp,sz00)** -> . % 18.28/18.46 23[0:Inp] || equal(xp,sz10)** -> . % 18.28/18.46 25[0:Inp] isPrime0(u) || -> SkP1(u)*. % 18.28/18.46 28[0:Inp] || -> equal(sdtpldt0(xp,xr),xn)**. % 18.28/18.46 37[0:Inp] aNaturalNumber0(u) || -> equal(sdtpldt0(sz00,u),u)**. % 18.28/18.46 42[0:Inp] aNaturalNumber0(u) aNaturalNumber0(v) || -> aNaturalNumber0(sdtpldt0(v,u))*. % 18.28/18.46 50[0:Inp] || -> SkP1(u) equal(u,sz10) equal(u,sz00) doDivides0(skf11(u),u)*. % 18.28/18.46 51[0:Inp] aNaturalNumber0(u) aNaturalNumber0(v) || -> equal(sdtpldt0(v,u),sdtpldt0(u,v))*. % 18.28/18.46 59[0:Inp] aNaturalNumber0(u) || doDivides0(u,xp)* -> equal(u,xp) equal(u,sz10). % 18.28/18.46 73[0:Inp] aNaturalNumber0(u) aNaturalNumber0(v) aNaturalNumber0(w) || equal(sdtpldt0(v,w),u)*+ -> sdtlseqdt0(v,u)*. % 18.28/18.46 81[0:Inp] aNaturalNumber0(u) aNaturalNumber0(v) aNaturalNumber0(w) || equal(sdtpldt0(v,w),sdtpldt0(u,w))* -> equal(v,u). % 18.28/18.46 84[0:Inp] aNaturalNumber0(u) aNaturalNumber0(v) aNaturalNumber0(w) || -> equal(sdtpldt0(sdtpldt0(w,v),u),sdtpldt0(w,sdtpldt0(v,u)))**. % 18.28/18.46 95[0:Inp] || sdtlseqdt0(sdtpldt0(sdtpldt0(xr,xm),xp),sdtpldt0(sdtpldt0(xn,xm),xp))* -> equal(sdtpldt0(sdtpldt0(xr,xm),xp),sdtpldt0(sdtpldt0(xn,xm),xp)). % 18.28/18.46 130[1:Spt:95.1] || -> equal(sdtpldt0(sdtpldt0(xr,xm),xp),sdtpldt0(sdtpldt0(xn,xm),xp))**. % 18.28/18.46 210[0:Res:50.3,59.1] aNaturalNumber0(skf11(xp)) || -> SkP1(xp) equal(xp,sz10) equal(xp,sz00) equal(skf11(xp),xp)** equal(skf11(xp),sz10). % 18.28/18.46 211[0:SSi:210.0,15.0,7.0,5.0] || -> SkP1(xp) equal(xp,sz10) equal(xp,sz00) equal(skf11(xp),xp)** equal(skf11(xp),sz10). % 18.28/18.46 212[0:MRR:211.1,211.2,23.0,22.0] || -> SkP1(xp) equal(skf11(xp),xp)** equal(skf11(xp),sz10). % 18.28/18.46 215[0:SpR:212.1,50.3] || -> SkP1(xp) equal(skf11(xp),sz10)** SkP1(xp) equal(xp,sz10) equal(xp,sz00) doDivides0(xp,xp). % 18.28/18.46 217[0:Obv:215.0] || -> equal(skf11(xp),sz10)** SkP1(xp) equal(xp,sz10) equal(xp,sz00) doDivides0(xp,xp). % 18.28/18.46 218[0:MRR:217.2,217.3,23.0,22.0] || -> equal(skf11(xp),sz10)** SkP1(xp) doDivides0(xp,xp). % 18.28/18.46 220[0:SpR:218.0,50.3] || -> SkP1(xp)* doDivides0(xp,xp) SkP1(xp)* equal(xp,sz10) equal(xp,sz00) doDivides0(sz10,xp). % 18.28/18.46 224[0:Obv:220.0] || -> doDivides0(xp,xp) SkP1(xp)* equal(xp,sz10) equal(xp,sz00) doDivides0(sz10,xp). % 18.28/18.46 225[0:MRR:224.2,224.3,23.0,22.0] || -> doDivides0(xp,xp) SkP1(xp)* doDivides0(sz10,xp). % 18.28/18.46 226[2:Spt:225.1] || -> SkP1(xp)*. % 18.28/18.46 289[1:SpR:51.2,130.0] aNaturalNumber0(xp) aNaturalNumber0(sdtpldt0(xr,xm)) || -> equal(sdtpldt0(sdtpldt0(xn,xm),xp),sdtpldt0(xp,sdtpldt0(xr,xm)))**. % 18.28/18.46 310[2:SSi:289.1,289.0,42.0,9.0,4.0,7.0,5.0,226.2] || -> equal(sdtpldt0(sdtpldt0(xn,xm),xp),sdtpldt0(xp,sdtpldt0(xr,xm)))**. % 18.28/18.46 311[2:Rew:310.0,130.0] || -> equal(sdtpldt0(sdtpldt0(xr,xm),xp),sdtpldt0(xp,sdtpldt0(xr,xm)))**. % 18.28/18.46 322[2:SpR:310.0,51.2] aNaturalNumber0(xp) aNaturalNumber0(sdtpldt0(xn,xm)) || -> equal(sdtpldt0(xp,sdtpldt0(xr,xm)),sdtpldt0(xp,sdtpldt0(xn,xm)))**. % 18.28/18.46 325[2:SSi:322.1,322.0,42.0,3.0,4.0,7.0,5.0,226.2] || -> equal(sdtpldt0(xp,sdtpldt0(xr,xm)),sdtpldt0(xp,sdtpldt0(xn,xm)))**. % 18.28/18.46 328[2:Rew:325.0,311.0] || -> equal(sdtpldt0(sdtpldt0(xr,xm),xp),sdtpldt0(xp,sdtpldt0(xn,xm)))**. % 18.28/18.46 1411[0:EqR:73.3] aNaturalNumber0(sdtpldt0(u,v)) aNaturalNumber0(u) aNaturalNumber0(v) || -> sdtlseqdt0(u,sdtpldt0(u,v))*. % 18.28/18.46 1426[0:SSi:1411.0,42.2] aNaturalNumber0(u) aNaturalNumber0(v) || -> sdtlseqdt0(u,sdtpldt0(u,v))*. % 18.28/18.46 1637[0:SpR:84.3,51.2] aNaturalNumber0(u) aNaturalNumber0(v) aNaturalNumber0(w) aNaturalNumber0(sdtpldt0(w,v)) aNaturalNumber0(u) || -> equal(sdtpldt0(u,sdtpldt0(w,v)),sdtpldt0(w,sdtpldt0(v,u)))*. % 18.28/18.46 1699[0:Obv:1637.0] aNaturalNumber0(u) aNaturalNumber0(v) aNaturalNumber0(sdtpldt0(v,u)) aNaturalNumber0(w) || -> equal(sdtpldt0(w,sdtpldt0(v,u)),sdtpldt0(v,sdtpldt0(u,w)))*. % 18.28/18.46 1700[0:SSi:1699.2,42.2] aNaturalNumber0(u) aNaturalNumber0(v) aNaturalNumber0(w) || -> equal(sdtpldt0(w,sdtpldt0(v,u)),sdtpldt0(v,sdtpldt0(u,w)))*. % 18.28/18.46 2029[0:SpL:37.1,81.3] aNaturalNumber0(u) aNaturalNumber0(sz00) aNaturalNumber0(v) aNaturalNumber0(u) || equal(sdtpldt0(v,u),u)** -> equal(v,sz00). % 18.28/18.46 2048[0:Obv:2029.0] aNaturalNumber0(sz00) aNaturalNumber0(u) aNaturalNumber0(v) || equal(sdtpldt0(u,v),v)** -> equal(u,sz00). % 18.28/18.46 2049[0:SSi:2048.0,1.0] aNaturalNumber0(u) aNaturalNumber0(v) || equal(sdtpldt0(u,v),v)** -> equal(u,sz00). % 18.28/18.46 22937[2:SpR:328.0,84.3] aNaturalNumber0(xp) aNaturalNumber0(xm) aNaturalNumber0(xr) || -> equal(sdtpldt0(xr,sdtpldt0(xm,xp)),sdtpldt0(xp,sdtpldt0(xn,xm)))**. % 18.28/18.46 22967[2:Rew:1700.3,22937.3] aNaturalNumber0(xp) aNaturalNumber0(xm) aNaturalNumber0(xr) || -> equal(sdtpldt0(xp,sdtpldt0(xn,xm)),sdtpldt0(xm,sdtpldt0(xp,xr)))**. % 18.28/18.46 22968[2:Rew:28.0,22967.3] aNaturalNumber0(xp) aNaturalNumber0(xm) aNaturalNumber0(xr) || -> equal(sdtpldt0(xp,sdtpldt0(xn,xm)),sdtpldt0(xm,xn))**. % 18.28/18.46 22969[2:SSi:22968.2,22968.1,22968.0,9.0,4.0,7.0,5.0,226.0] || -> equal(sdtpldt0(xp,sdtpldt0(xn,xm)),sdtpldt0(xm,xn))**. % 18.28/18.46 23467[2:SpL:22969.0,2049.2] aNaturalNumber0(xp) aNaturalNumber0(sdtpldt0(xn,xm)) || equal(sdtpldt0(xm,xn),sdtpldt0(xn,xm))** -> equal(xp,sz00). % 18.28/18.46 23481[2:SSi:23467.1,23467.0,42.0,3.0,4.0,7.0,5.0,226.2] || equal(sdtpldt0(xm,xn),sdtpldt0(xn,xm))** -> equal(xp,sz00). % 18.28/18.46 23482[2:MRR:23481.1,22.0] || equal(sdtpldt0(xm,xn),sdtpldt0(xn,xm))** -> . % 18.28/18.46 23652[2:SpL:51.2,23482.0] aNaturalNumber0(xm) aNaturalNumber0(xn) || equal(sdtpldt0(xn,xm),sdtpldt0(xn,xm))* -> . % 18.28/18.46 23655[2:Obv:23652.2] aNaturalNumber0(xm) aNaturalNumber0(xn) || -> . % 18.28/18.46 23656[2:SSi:23655.1,23655.0,3.0,4.0] || -> . % 18.28/18.46 23657[2:Spt:23656.0,225.1,226.0] || SkP1(xp)* -> . % 18.28/18.46 23658[2:Spt:23656.0,225.0,225.2] || -> doDivides0(xp,xp)* doDivides0(sz10,xp). % 18.28/18.46 23798[2:Res:25.1,23657.0] isPrime0(xp) || -> . % 18.28/18.46 23799[2:SSi:23798.0,7.0,5.0] || -> . % 18.28/18.46 23801[1:Spt:23799.0,95.1,130.0] || equal(sdtpldt0(sdtpldt0(xr,xm),xp),sdtpldt0(sdtpldt0(xn,xm),xp))** -> . % 18.28/18.46 23802[1:Spt:23799.0,95.0] || sdtlseqdt0(sdtpldt0(sdtpldt0(xr,xm),xp),sdtpldt0(sdtpldt0(xn,xm),xp))* -> . % 18.28/18.46 23826[1:SpL:84.3,23802.0] aNaturalNumber0(xp) aNaturalNumber0(xm) aNaturalNumber0(xr) || sdtlseqdt0(sdtpldt0(xr,sdtpldt0(xm,xp)),sdtpldt0(sdtpldt0(xn,xm),xp))* -> . % 18.28/18.46 23835[1:Rew:1700.3,23826.3] aNaturalNumber0(xp) aNaturalNumber0(xm) aNaturalNumber0(xr) || sdtlseqdt0(sdtpldt0(xm,sdtpldt0(xp,xr)),sdtpldt0(sdtpldt0(xn,xm),xp))* -> . % 18.28/18.46 23836[1:Rew:28.0,23835.3] aNaturalNumber0(xp) aNaturalNumber0(xm) aNaturalNumber0(xr) || sdtlseqdt0(sdtpldt0(xm,xn),sdtpldt0(sdtpldt0(xn,xm),xp))* -> . % 18.28/18.46 23837[1:SSi:23836.2,23836.1,23836.0,9.0,4.0,7.0,5.0] || sdtlseqdt0(sdtpldt0(xm,xn),sdtpldt0(sdtpldt0(xn,xm),xp))* -> . % 18.28/18.46 34785[1:SpL:51.2,23837.0] aNaturalNumber0(xn) aNaturalNumber0(xm) || sdtlseqdt0(sdtpldt0(xn,xm),sdtpldt0(sdtpldt0(xn,xm),xp))* -> . % 18.28/18.46 34788[1:SSi:34785.1,34785.0,4.0,3.0] || sdtlseqdt0(sdtpldt0(xn,xm),sdtpldt0(sdtpldt0(xn,xm),xp))* -> . % 18.28/18.46 34806[1:Res:1426.2,34788.0] aNaturalNumber0(sdtpldt0(xn,xm)) aNaturalNumber0(xp) || -> . % 18.28/18.46 34814[1:SSi:34806.1,34806.0,5.0,7.0,42.2,3.0,4.0] || -> . % 18.28/18.46 % SZS output end Refutation % 18.28/18.46 Formulae used in the proof : mSortsC m__1837 m__1860 m__1883 m__1799 m__1913 m_AddZero mSortsB mAddComm mDefLE mAddCanc mAddAsso m__ % 18.28/18.46 %------------------------------------------------------------------------------