%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : NUM528+1 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n004.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:27:08 EDT 2022 % Result : Theorem 9.12s 9.30s % Output : Refutation 9.12s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.14 % Problem : NUM528+1 : TPTP v8.1.0. Released v4.0.0. % 0.08/0.15 % Command : run_spass %d %s % 0.15/0.36 % Computer : n004.cluster.edu % 0.15/0.36 % Model : x86_64 x86_64 % 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.36 % Memory : 8042.1875MB % 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.36 % CPULimit : 300 % 0.15/0.36 % WCLimit : 600 % 0.15/0.36 % DateTime : Wed Jul 6 06:51:22 EDT 2022 % 0.15/0.37 % CPUTime : % 9.12/9.30 % 9.12/9.30 SPASS V 3.9 % 9.12/9.30 SPASS beiseite: Proof found. % 9.12/9.30 % SZS status Theorem % 9.12/9.30 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 9.12/9.30 SPASS derived 12909 clauses, backtracked 2929 clauses, performed 12 splits and kept 6572 clauses. % 9.12/9.30 SPASS allocated 112146 KBytes. % 9.12/9.30 SPASS spent 0:00:07.19 on the problem. % 9.12/9.30 0:00:00.03 for the input. % 9.12/9.30 0:00:00.04 for the FLOTTER CNF translation. % 9.12/9.30 0:00:00.14 for inferences. % 9.12/9.30 0:00:00.10 for the backtracking. % 9.12/9.30 0:00:06.81 for the reduction. % 9.12/9.30 % 9.12/9.30 % 9.12/9.30 Here is a proof with depth 4, length 80 : % 9.12/9.30 % SZS output start Refutation % 9.12/9.30 1[0:Inp] || -> aNaturalNumber0(sz00)*. % 9.12/9.30 2[0:Inp] || -> aNaturalNumber0(sz10)*. % 9.12/9.30 3[0:Inp] || -> aNaturalNumber0(xn)*. % 9.12/9.30 4[0:Inp] || -> aNaturalNumber0(xm)*. % 9.12/9.30 5[0:Inp] || -> aNaturalNumber0(xp)*. % 9.12/9.30 6[0:Inp] || -> isPrime0(xp)*. % 9.12/9.30 11[0:Inp] || -> aNaturalNumber0(skf4(u,v))*. % 9.12/9.30 13[0:Inp] || equal(xn,sz00)** -> . % 9.12/9.30 14[0:Inp] || equal(xm,sz00)** -> . % 9.12/9.30 15[0:Inp] || equal(xp,sz00)** -> . % 9.12/9.30 19[0:Inp] || sdtlseqdt0(xm,xn)* -> equal(xm,xn). % 9.12/9.30 23[0:Inp] aNaturalNumber0(u) || -> equal(sdtasdt0(sz10,u),u)**. % 9.12/9.30 26[0:Inp] || -> equal(sdtasdt0(xp,sdtasdt0(xm,xm)),sdtasdt0(xn,xn))**. % 9.12/9.30 29[0:Inp] aNaturalNumber0(u) aNaturalNumber0(v) || -> aNaturalNumber0(sdtasdt0(v,u))*. % 9.12/9.30 31[0:Inp] aNaturalNumber0(u) isPrime0(u) || equal(u,sz10)* -> . % 9.12/9.30 32[0:Inp] || sdtlseqdt0(xn,xm) -> sdtlseqdt0(sdtasdt0(xn,xn),sdtasdt0(xm,xm))*. % 9.12/9.30 33[0:Inp] aNaturalNumber0(u) aNaturalNumber0(v) || -> sdtlseqdt0(v,u)* sdtlseqdt0(u,v)*. % 9.12/9.30 37[0:Inp] aNaturalNumber0(u) aNaturalNumber0(v) || -> equal(sdtasdt0(v,u),sdtasdt0(u,v))*. % 9.12/9.30 41[0:Inp] aNaturalNumber0(u) aNaturalNumber0(v) || -> equal(v,sz00) sdtlseqdt0(u,sdtasdt0(u,v))*. % 9.12/9.30 42[0:Inp] aNaturalNumber0(u) aNaturalNumber0(v) || equal(sdtpldt0(v,u),sz00)** -> equal(v,sz00). % 9.12/9.30 49[0:Inp] aNaturalNumber0(u) aNaturalNumber0(v) || sdtlseqdt0(v,u) -> equal(sdtpldt0(v,skf4(u,v)),u)**. % 9.12/9.30 50[0:Inp] aNaturalNumber0(u) aNaturalNumber0(v) || sdtlseqdt0(v,u)*+ sdtlseqdt0(u,v)* -> equal(v,u). % 9.12/9.30 52[0:Inp] aNaturalNumber0(u) aNaturalNumber0(v) || equal(sdtasdt0(v,u),sz00)** -> equal(u,sz00) equal(v,sz00). % 9.12/9.30 61[0:Inp] aNaturalNumber0(u) aNaturalNumber0(v) aNaturalNumber0(w) || -> equal(sdtasdt0(sdtasdt0(w,v),u),sdtasdt0(w,sdtasdt0(v,u)))**. % 9.12/9.30 71[0:Inp] aNaturalNumber0(u) aNaturalNumber0(v) aNaturalNumber0(w) || equal(sdtasdt0(v,w),sdtasdt0(u,w))* -> equal(v,u) equal(w,sz00). % 9.12/9.30 88[1:Spt:19.1] || -> equal(xm,xn)**. % 9.12/9.30 90[1:Rew:88.0,26.0] || -> equal(sdtasdt0(xp,sdtasdt0(xn,xn)),sdtasdt0(xn,xn))**. % 9.12/9.30 110[0:EmS:31.0,31.1,5.0,6.0] || equal(xp,sz10)** -> . % 9.12/9.30 198[0:SpR:37.2,41.3] aNaturalNumber0(u) aNaturalNumber0(v) aNaturalNumber0(u) aNaturalNumber0(v) || -> equal(v,sz00) sdtlseqdt0(u,sdtasdt0(v,u))*. % 9.12/9.30 200[1:SpR:90.0,41.3] aNaturalNumber0(xp) aNaturalNumber0(sdtasdt0(xn,xn)) || -> equal(sdtasdt0(xn,xn),sz00) sdtlseqdt0(xp,sdtasdt0(xn,xn))*. % 9.12/9.30 206[1:SSi:200.1,200.0,29.0,3.0,3.0,6.0,5.2] || -> equal(sdtasdt0(xn,xn),sz00) sdtlseqdt0(xp,sdtasdt0(xn,xn))*. % 9.12/9.30 207[0:Obv:198.1] aNaturalNumber0(u) aNaturalNumber0(v) || -> equal(v,sz00) sdtlseqdt0(u,sdtasdt0(v,u))*. % 9.12/9.30 215[2:Spt:206.0] || -> equal(sdtasdt0(xn,xn),sz00)**. % 9.12/9.30 226[2:SpR:215.0,41.3] aNaturalNumber0(xn) aNaturalNumber0(xn) || -> equal(xn,sz00) sdtlseqdt0(xn,sz00)*. % 9.12/9.30 231[2:Obv:226.0] aNaturalNumber0(xn) || -> equal(xn,sz00) sdtlseqdt0(xn,sz00)*. % 9.12/9.30 232[2:SSi:231.0,3.0] || -> equal(xn,sz00) sdtlseqdt0(xn,sz00)*. % 9.12/9.30 233[2:MRR:232.0,13.0] || -> sdtlseqdt0(xn,sz00)*. % 9.12/9.30 307[0:SpL:49.3,42.2] aNaturalNumber0(u) aNaturalNumber0(v) aNaturalNumber0(skf4(u,v)) aNaturalNumber0(v) || sdtlseqdt0(v,u)* equal(u,sz00) -> equal(v,sz00). % 9.12/9.30 310[0:Obv:307.1] aNaturalNumber0(u) aNaturalNumber0(skf4(u,v)) aNaturalNumber0(v) || sdtlseqdt0(v,u)* equal(u,sz00) -> equal(v,sz00). % 9.12/9.30 311[0:SSi:310.1,11.0] aNaturalNumber0(u) aNaturalNumber0(v) || sdtlseqdt0(v,u)* equal(u,sz00) -> equal(v,sz00). % 9.12/9.30 327[2:Res:233.0,311.2] aNaturalNumber0(sz00) aNaturalNumber0(xn) || equal(sz00,sz00) -> equal(xn,sz00)**. % 9.12/9.30 330[2:Obv:327.2] aNaturalNumber0(sz00) aNaturalNumber0(xn) || -> equal(xn,sz00)**. % 9.12/9.30 331[2:SSi:330.1,330.0,3.0,1.0] || -> equal(xn,sz00)**. % 9.12/9.30 332[2:MRR:331.0,13.0] || -> . % 9.12/9.30 338[2:Spt:332.0,206.0,215.0] || equal(sdtasdt0(xn,xn),sz00)** -> . % 9.12/9.30 339[2:Spt:332.0,206.1] || -> sdtlseqdt0(xp,sdtasdt0(xn,xn))*. % 9.12/9.30 755[0:SpR:23.1,61.3] aNaturalNumber0(u) aNaturalNumber0(v) aNaturalNumber0(u) aNaturalNumber0(sz10) || -> equal(sdtasdt0(sz10,sdtasdt0(u,v)),sdtasdt0(u,v))**. % 9.12/9.30 769[0:Obv:755.0] aNaturalNumber0(u) aNaturalNumber0(v) aNaturalNumber0(sz10) || -> equal(sdtasdt0(sz10,sdtasdt0(v,u)),sdtasdt0(v,u))**. % 9.12/9.30 770[0:SSi:769.2,2.0] aNaturalNumber0(u) aNaturalNumber0(v) || -> equal(sdtasdt0(sz10,sdtasdt0(v,u)),sdtasdt0(v,u))**. % 9.12/9.30 1896[1:SpL:90.0,71.3] aNaturalNumber0(xp) aNaturalNumber0(u) aNaturalNumber0(sdtasdt0(xn,xn)) || equal(sdtasdt0(u,sdtasdt0(xn,xn)),sdtasdt0(xn,xn))** -> equal(u,xp) equal(sdtasdt0(xn,xn),sz00). % 9.12/9.30 1912[1:SSi:1896.2,1896.0,29.0,3.0,3.0,6.0,5.2] aNaturalNumber0(u) || equal(sdtasdt0(u,sdtasdt0(xn,xn)),sdtasdt0(xn,xn))** -> equal(u,xp) equal(sdtasdt0(xn,xn),sz00). % 9.12/9.30 1913[2:MRR:1912.3,338.0] aNaturalNumber0(u) || equal(sdtasdt0(u,sdtasdt0(xn,xn)),sdtasdt0(xn,xn))** -> equal(u,xp). % 9.12/9.30 17202[2:SpL:770.2,1913.1] aNaturalNumber0(xn) aNaturalNumber0(xn) aNaturalNumber0(sz10) || equal(sdtasdt0(xn,xn),sdtasdt0(xn,xn))* -> equal(xp,sz10). % 9.12/9.30 17214[2:Obv:17202.3] aNaturalNumber0(xn) aNaturalNumber0(sz10) || -> equal(xp,sz10)**. % 9.12/9.30 17215[2:SSi:17214.1,17214.0,2.0,3.0] || -> equal(xp,sz10)**. % 9.12/9.30 17216[2:MRR:17215.0,110.0] || -> . % 9.12/9.30 17228[1:Spt:17216.0,19.1,88.0] || equal(xm,xn)** -> . % 9.12/9.30 17229[1:Spt:17216.0,19.0] || sdtlseqdt0(xm,xn)* -> . % 9.12/9.30 17311[1:Res:33.2,17229.0] aNaturalNumber0(xn) aNaturalNumber0(xm) || -> sdtlseqdt0(xn,xm)*. % 9.12/9.30 17320[1:SSi:17311.0,3.0] aNaturalNumber0(xm) || -> sdtlseqdt0(xn,xm)*. % 9.12/9.30 17321[1:MRR:17320.0,4.0] || -> sdtlseqdt0(xn,xm)*. % 9.12/9.30 17322[1:MRR:32.0,17321.0] || -> sdtlseqdt0(sdtasdt0(xn,xn),sdtasdt0(xm,xm))*. % 9.12/9.30 17334[1:Res:17322.0,50.2] aNaturalNumber0(sdtasdt0(xm,xm)) aNaturalNumber0(sdtasdt0(xn,xn)) || sdtlseqdt0(sdtasdt0(xm,xm),sdtasdt0(xn,xn))* -> equal(sdtasdt0(xm,xm),sdtasdt0(xn,xn)). % 9.12/9.30 17344[1:SSi:17334.1,17334.0,29.0,3.0,3.2,29.0,4.0,4.2] || sdtlseqdt0(sdtasdt0(xm,xm),sdtasdt0(xn,xn))* -> equal(sdtasdt0(xm,xm),sdtasdt0(xn,xn)). % 9.12/9.30 17356[0:SpR:26.0,207.3] aNaturalNumber0(sdtasdt0(xm,xm)) aNaturalNumber0(xp) || -> equal(xp,sz00) sdtlseqdt0(sdtasdt0(xm,xm),sdtasdt0(xn,xn))*. % 9.12/9.30 17379[0:SpL:26.0,71.3] aNaturalNumber0(u) aNaturalNumber0(xp) aNaturalNumber0(sdtasdt0(xm,xm)) || equal(sdtasdt0(u,sdtasdt0(xm,xm)),sdtasdt0(xn,xn))** -> equal(xp,u) equal(sdtasdt0(xm,xm),sz00). % 9.12/9.30 17399[0:SSi:17356.1,17356.0,5.0,6.0,29.2,4.0,4.0] || -> equal(xp,sz00) sdtlseqdt0(sdtasdt0(xm,xm),sdtasdt0(xn,xn))*. % 9.12/9.30 17400[0:MRR:17399.0,15.0] || -> sdtlseqdt0(sdtasdt0(xm,xm),sdtasdt0(xn,xn))*. % 9.12/9.30 17401[1:MRR:17344.0,17400.0] || -> equal(sdtasdt0(xm,xm),sdtasdt0(xn,xn))**. % 9.12/9.30 17426[1:Rew:17401.0,17379.5,17401.0,17379.3] aNaturalNumber0(u) aNaturalNumber0(xp) aNaturalNumber0(sdtasdt0(xm,xm)) || equal(sdtasdt0(u,sdtasdt0(xn,xn)),sdtasdt0(xn,xn))** -> equal(xp,u) equal(sdtasdt0(xn,xn),sz00). % 9.12/9.30 17427[1:SSi:17426.2,17426.1,29.0,4.0,4.0,5.0,6.2] aNaturalNumber0(u) || equal(sdtasdt0(u,sdtasdt0(xn,xn)),sdtasdt0(xn,xn))** -> equal(xp,u) equal(sdtasdt0(xn,xn),sz00). % 9.12/9.30 18609[1:SpL:17401.0,52.2] aNaturalNumber0(xm) aNaturalNumber0(xm) || equal(sdtasdt0(xn,xn),sz00)** -> equal(xm,sz00) equal(xm,sz00). % 9.12/9.30 18634[1:Obv:18609.3] aNaturalNumber0(xm) || equal(sdtasdt0(xn,xn),sz00)** -> equal(xm,sz00). % 9.12/9.30 18635[1:SSi:18634.0,4.0] || equal(sdtasdt0(xn,xn),sz00)** -> equal(xm,sz00). % 9.12/9.30 18636[1:MRR:18635.1,14.0] || equal(sdtasdt0(xn,xn),sz00)** -> . % 9.12/9.30 18640[1:MRR:17427.3,18636.0] aNaturalNumber0(u) || equal(sdtasdt0(u,sdtasdt0(xn,xn)),sdtasdt0(xn,xn))** -> equal(xp,u). % 9.12/9.30 20253[1:SpL:770.2,18640.1] aNaturalNumber0(xn) aNaturalNumber0(xn) aNaturalNumber0(sz10) || equal(sdtasdt0(xn,xn),sdtasdt0(xn,xn))* -> equal(xp,sz10). % 9.12/9.30 20265[1:Obv:20253.3] aNaturalNumber0(xn) aNaturalNumber0(sz10) || -> equal(xp,sz10)**. % 9.12/9.30 20266[1:SSi:20265.1,20265.0,2.0,3.0] || -> equal(xp,sz10)**. % 9.12/9.30 20267[1:MRR:20266.0,110.0] || -> . % 9.12/9.30 % SZS output end Refutation % 9.12/9.30 Formulae used in the proof : mSortsC mSortsC_01 m__2987 m__3025 mDefLE m__ m_MulUnit m__3014 mSortsB_02 mDefPrime m__3152 mLETotal mMulComm mMonMul2 mZeroAdd mLEAsym mZeroMul mMulAsso mMulCanc % 9.12/9.30 %------------------------------------------------------------------------------