%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : NUM512+3 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n015.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:58 EDT 2022 % Result : Theorem 4.00s 4.17s % Output : Refutation 4.00s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : NUM512+3 : TPTP v8.1.0. Released v4.0.0. % 0.07/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n015.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 : Tue Jul 5 10:52:47 EDT 2022 % 0.13/0.34 % CPUTime : % 4.00/4.17 % 4.00/4.17 SPASS V 3.9 % 4.00/4.17 SPASS beiseite: Proof found. % 4.00/4.17 % SZS status Theorem % 4.00/4.17 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 4.00/4.17 SPASS derived 6800 clauses, backtracked 1555 clauses, performed 26 splits and kept 3779 clauses. % 4.00/4.17 SPASS allocated 105711 KBytes. % 4.00/4.17 SPASS spent 0:00:03.49 on the problem. % 4.00/4.17 0:00:00.03 for the input. % 4.00/4.17 0:00:00.05 for the FLOTTER CNF translation. % 4.00/4.17 0:00:00.08 for inferences. % 4.00/4.17 0:00:00.05 for the backtracking. % 4.00/4.17 0:00:03.22 for the reduction. % 4.00/4.17 % 4.00/4.17 % 4.00/4.17 Here is a proof with depth 4, length 54 : % 4.00/4.17 % SZS output start Refutation % 4.00/4.17 3[0:Inp] || -> aNaturalNumber0(xn)*. % 4.00/4.17 4[0:Inp] || -> aNaturalNumber0(xm)*. % 4.00/4.17 12[0:Inp] || -> aNaturalNumber0(xr)*. % 4.00/4.17 13[0:Inp] || -> isPrime0(xr)*. % 4.00/4.17 24[0:Inp] || -> aNaturalNumber0(skf11(u))*. % 4.00/4.17 44[0:Inp] || equal(xr,sz00)** -> . % 4.00/4.17 45[0:Inp] || equal(xr,sz10)** -> . % 4.00/4.17 48[0:Inp] || -> aNaturalNumber0(sdtsldt0(xn,xr))*. % 4.00/4.17 50[0:Inp] isPrime0(u) || -> SkP1(u)*. % 4.00/4.17 66[0:Inp] || -> equal(sdtasdt0(xp,xk),sdtasdt0(xn,xm))**. % 4.00/4.17 70[0:Inp] || -> equal(sdtasdt0(xr,sdtsldt0(xn,xr)),xn)**. % 4.00/4.17 72[0:Inp] || SkC1 -> aNaturalNumber0(sdtsldt0(sdtasdt0(xp,xk),xr))*. % 4.00/4.17 90[0:Inp] || -> SkP1(u) equal(u,sz10) equal(u,sz00) doDivides0(skf11(u),u)*. % 4.00/4.17 91[0:Inp] || SkC1 -> equal(sdtasdt0(xr,sdtsldt0(sdtasdt0(xp,xk),xr)),sdtasdt0(xp,xk))**. % 4.00/4.17 92[0:Inp] || equal(sdtasdt0(sdtasdt0(sdtsldt0(xn,xr),xm),xr),sdtasdt0(xn,xm))** -> SkC1. % 4.00/4.17 94[0:Inp] aNaturalNumber0(u) aNaturalNumber0(v) || -> equal(sdtasdt0(v,u),sdtasdt0(u,v))*. % 4.00/4.17 102[0:Inp] aNaturalNumber0(u) || doDivides0(u,xr)* -> equal(u,xr) equal(u,sz10). % 4.00/4.17 103[0:Inp] || equal(sdtasdt0(sdtsldt0(sdtasdt0(xp,xk),xr),xr),sdtasdt0(xn,xm))** SkC1 -> . % 4.00/4.17 128[0:Inp] aNaturalNumber0(u) aNaturalNumber0(v) aNaturalNumber0(w) || -> equal(sdtasdt0(sdtasdt0(w,v),u),sdtasdt0(w,sdtasdt0(v,u)))**. % 4.00/4.17 151[0:Rew:66.0,72.1] || SkC1 -> aNaturalNumber0(sdtsldt0(sdtasdt0(xn,xm),xr))*. % 4.00/4.17 152[0:Rew:66.0,91.1] || SkC1 -> equal(sdtasdt0(xr,sdtsldt0(sdtasdt0(xn,xm),xr)),sdtasdt0(xn,xm))**. % 4.00/4.17 153[0:Rew:66.0,103.0] || SkC1 equal(sdtasdt0(sdtsldt0(sdtasdt0(xn,xm),xr),xr),sdtasdt0(xn,xm))** -> . % 4.00/4.17 157[1:Spt:151.0] || SkC1* -> . % 4.00/4.17 158[1:MRR:92.1,157.0] || equal(sdtasdt0(sdtasdt0(sdtsldt0(xn,xr),xm),xr),sdtasdt0(xn,xm))** -> . % 4.00/4.17 264[0:Res:90.3,102.1] aNaturalNumber0(skf11(xr)) || -> SkP1(xr) equal(xr,sz10) equal(xr,sz00) equal(skf11(xr),xr)** equal(skf11(xr),sz10). % 4.00/4.17 265[0:SSi:264.0,24.0,13.0,12.0] || -> SkP1(xr) equal(xr,sz10) equal(xr,sz00) equal(skf11(xr),xr)** equal(skf11(xr),sz10). % 4.00/4.17 266[0:MRR:265.1,265.2,45.0,44.0] || -> SkP1(xr) equal(skf11(xr),xr)** equal(skf11(xr),sz10). % 4.00/4.17 269[0:SpR:266.1,90.3] || -> SkP1(xr) equal(skf11(xr),sz10)** SkP1(xr) equal(xr,sz10) equal(xr,sz00) doDivides0(xr,xr). % 4.00/4.17 271[0:Obv:269.0] || -> equal(skf11(xr),sz10)** SkP1(xr) equal(xr,sz10) equal(xr,sz00) doDivides0(xr,xr). % 4.00/4.17 272[0:MRR:271.2,271.3,45.0,44.0] || -> equal(skf11(xr),sz10)** SkP1(xr) doDivides0(xr,xr). % 4.00/4.17 274[0:SpR:272.0,90.3] || -> SkP1(xr)* doDivides0(xr,xr) SkP1(xr)* equal(xr,sz10) equal(xr,sz00) doDivides0(sz10,xr). % 4.00/4.17 278[0:Obv:274.0] || -> doDivides0(xr,xr) SkP1(xr)* equal(xr,sz10) equal(xr,sz00) doDivides0(sz10,xr). % 4.00/4.17 279[0:MRR:278.2,278.3,45.0,44.0] || -> doDivides0(xr,xr) SkP1(xr)* doDivides0(sz10,xr). % 4.00/4.17 283[2:Spt:279.1] || -> SkP1(xr)*. % 4.00/4.17 358[1:SpL:94.2,158.0] aNaturalNumber0(sdtsldt0(xn,xr)) aNaturalNumber0(xm) || equal(sdtasdt0(sdtasdt0(xm,sdtsldt0(xn,xr)),xr),sdtasdt0(xn,xm))** -> . % 4.00/4.17 370[1:SSi:358.1,358.0,4.0,48.0] || equal(sdtasdt0(sdtasdt0(xm,sdtsldt0(xn,xr)),xr),sdtasdt0(xn,xm))** -> . % 4.00/4.17 9404[1:SpL:128.3,370.0] aNaturalNumber0(xr) aNaturalNumber0(sdtsldt0(xn,xr)) aNaturalNumber0(xm) || equal(sdtasdt0(xm,sdtasdt0(sdtsldt0(xn,xr),xr)),sdtasdt0(xn,xm))** -> . % 4.00/4.17 9406[1:Rew:70.0,9404.3,94.2,9404.3] aNaturalNumber0(xr) aNaturalNumber0(sdtsldt0(xn,xr)) aNaturalNumber0(xm) || equal(sdtasdt0(xm,xn),sdtasdt0(xn,xm))** -> . % 4.00/4.17 9407[2:SSi:9406.2,9406.1,9406.0,4.0,48.0,283.0,12.0,13.0] || equal(sdtasdt0(xm,xn),sdtasdt0(xn,xm))** -> . % 4.00/4.17 9412[2:SpL:94.2,9407.0] aNaturalNumber0(xm) aNaturalNumber0(xn) || equal(sdtasdt0(xn,xm),sdtasdt0(xn,xm))* -> . % 4.00/4.17 9415[2:Obv:9412.2] aNaturalNumber0(xm) aNaturalNumber0(xn) || -> . % 4.00/4.17 9416[2:SSi:9415.1,9415.0,3.0,4.0] || -> . % 4.00/4.17 9417[2:Spt:9416.0,279.1,283.0] || SkP1(xr)* -> . % 4.00/4.17 9418[2:Spt:9416.0,279.0,279.2] || -> doDivides0(xr,xr)* doDivides0(sz10,xr). % 4.00/4.17 9712[2:Res:50.1,9417.0] isPrime0(xr) || -> . % 4.00/4.17 9713[2:SSi:9712.0,12.0,13.0] || -> . % 4.00/4.17 9714[1:Spt:9713.0,151.0,157.0] || -> SkC1*. % 4.00/4.17 9715[1:Spt:9713.0,151.1] || -> aNaturalNumber0(sdtsldt0(sdtasdt0(xn,xm),xr))*. % 4.00/4.17 9716[1:MRR:152.0,9714.0] || -> equal(sdtasdt0(xr,sdtsldt0(sdtasdt0(xn,xm),xr)),sdtasdt0(xn,xm))**. % 4.00/4.17 9717[1:MRR:153.0,9714.0] || equal(sdtasdt0(sdtsldt0(sdtasdt0(xn,xm),xr),xr),sdtasdt0(xn,xm))** -> . % 4.00/4.17 10046[1:SpL:94.2,9717.0] aNaturalNumber0(xr) aNaturalNumber0(sdtsldt0(sdtasdt0(xn,xm),xr)) || equal(sdtasdt0(xr,sdtsldt0(sdtasdt0(xn,xm),xr)),sdtasdt0(xn,xm))** -> . % 4.00/4.17 10051[1:Rew:9716.0,10046.2] aNaturalNumber0(xr) aNaturalNumber0(sdtsldt0(sdtasdt0(xn,xm),xr)) || equal(sdtasdt0(xn,xm),sdtasdt0(xn,xm))* -> . % 4.00/4.17 10052[1:Obv:10051.2] aNaturalNumber0(xr) aNaturalNumber0(sdtsldt0(sdtasdt0(xn,xm),xr)) || -> . % 4.00/4.17 10053[1:SSi:10052.1,10052.0,9715.0,12.0,13.0] || -> . % 4.00/4.17 % SZS output end Refutation % 4.00/4.17 Formulae used in the proof : m__1837 m__2342 m__1799 m__2504 m__2306 m__ mMulComm mMulAsso % 4.00/4.17 %------------------------------------------------------------------------------