%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : NUM518+3 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % Computer : n017.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Sun Sep 27 08:13:00 AM UTC 2026 % Result : Theorem 27.29s 5.31s % Output : CNFRefutation 27.29s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM518+3 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.09/0.35 % Computer : n017.cluster.edu % 0.09/0.35 % Model : x86_64 x86_64 % 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.35 % Memory : 8046.5625MB % 0.09/0.35 % OS : Linux 6.8.0-71-generic % 0.09/0.35 % CPULimit : 300 % 0.09/0.35 % WCLimit : 300 % 0.09/0.35 % DateTime : Sat Sep 26 03:00:32 UTC 2026 % 0.09/0.36 % CPUTime : % 0.09/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 27.29/5.31 % SZS status Theorem for theBenchmark.p % 27.29/5.31 % SZS output start CNFRefutation for theBenchmark.p % 27.29/5.31 fof(mSortsC, axiom, aNaturalNumber0(sz00)). % 27.29/5.31 fof(m_MulZero, axiom, ! [X0] : ((aNaturalNumber0(X0) => (sdtasdt0(X0,sz00) = sz00 & sz00 = sdtasdt0(sz00,X0))))). % 27.29/5.31 fof(mLETran, axiom, ! [X0] : ! [X1] : ! [X2] : (((aNaturalNumber0(X0) & (aNaturalNumber0(X1) & aNaturalNumber0(X2))) => ((sdtlseqdt0(X0,X1) & sdtlseqdt0(X1,X2)) => sdtlseqdt0(X0,X2))))). % 27.29/5.31 fof(mDivLE, axiom, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => ((doDivides0(X0,X1) & X1 != sz00) => sdtlseqdt0(X0,X1))))). % 27.29/5.31 fof(m__1837, hypothesis, (aNaturalNumber0(xn) & (aNaturalNumber0(xm) & aNaturalNumber0(xp)))). % 27.29/5.31 fof(m__1870, hypothesis, ~((? [X0] : ((aNaturalNumber0(X0) & sdtpldt0(xp,X0) = xn)) | sdtlseqdt0(xp,xn)))). % 27.29/5.31 fof(m__2342, hypothesis, (aNaturalNumber0(xr) & (? [X0] : ((aNaturalNumber0(X0) & xk = sdtasdt0(xr,X0))) & (doDivides0(xr,xk) & (xr != sz00 & (xr != sz10 & (! [X0] : (((aNaturalNumber0(X0) & (? [X1] : ((aNaturalNumber0(X1) & xr = sdtasdt0(X0,X1))) | doDivides0(X0,xr))) => (X0 = sz10 | X0 = xr))) & isPrime0(xr)))))))). % 27.29/5.31 fof(m__2504, hypothesis, (~(((aNaturalNumber0(sdtsldt0(xn,xr)) & xn = sdtasdt0(xr,sdtsldt0(xn,xr))) => sdtsldt0(xn,xr) = xn)) & (aNaturalNumber0(sdtsldt0(xn,xr)) & (xn = sdtasdt0(xr,sdtsldt0(xn,xr)) & (? [X0] : ((aNaturalNumber0(X0) & sdtpldt0(sdtsldt0(xn,xr),X0) = xn)) & sdtlseqdt0(sdtsldt0(xn,xr),xn)))))). % 27.29/5.31 fof(m__2645, hypothesis, ((aNaturalNumber0(sdtsldt0(xn,xr)) & (xn = sdtasdt0(xr,sdtsldt0(xn,xr)) & (? [X0] : ((aNaturalNumber0(X0) & sdtsldt0(xn,xr) = sdtasdt0(xp,X0))) & doDivides0(xp,sdtsldt0(xn,xr))))) | (? [X0] : ((aNaturalNumber0(X0) & xm = sdtasdt0(xp,X0))) & doDivides0(xp,xm)))). % 27.29/5.31 fof(m__, conjecture, (? [X0] : ((aNaturalNumber0(X0) & xn = sdtasdt0(xp,X0))) | (doDivides0(xp,xn) | (? [X0] : ((aNaturalNumber0(X0) & xm = sdtasdt0(xp,X0))) | doDivides0(xp,xm))))). % 27.29/5.31 fof(negated_conjecture, negated_conjecture, ~((? [X0] : ((aNaturalNumber0(X0) & xn = sdtasdt0(xp,X0))) | (doDivides0(xp,xn) | (? [X0] : ((aNaturalNumber0(X0) & xm = sdtasdt0(xp,X0))) | doDivides0(xp,xm))))), inference(negate_conjecture, [status(cth)], [m__])). % 27.29/5.31 cnf(c0, plain, aNaturalNumber0(sz00), inference(clausification, [status(esa)], [mSortsC])). % 27.29/5.31 cnf(c13, plain, ~aNaturalNumber0(X0) | sdtasdt0(X0,sz00) = sz00, inference(clausification, [status(esa)], [m_MulZero])). % 27.29/5.31 cnf(c32, plain, sdtlseqdt0(X0,X1) | ~sdtlseqdt0(X2,X1) | ~aNaturalNumber0(X0) | ~aNaturalNumber0(X2) | ~sdtlseqdt0(X0,X2) | ~aNaturalNumber0(X1), inference(clausification, [status(esa)], [mLETran])). % 27.29/5.31 cnf(c56, plain, ~aNaturalNumber0(X0) | X1 = sz00 | sdtlseqdt0(X0,X1) | ~doDivides0(X0,X1) | ~aNaturalNumber0(X1), inference(clausification, [status(esa)], [mDivLE])). % 27.29/5.31 cnf(c70, plain, aNaturalNumber0(xn), inference(clausification, [status(esa)], [m__1837])). % 27.29/5.31 cnf(c72, plain, aNaturalNumber0(xp), inference(clausification, [status(esa)], [m__1837])). % 27.29/5.31 cnf(c98, plain, ~sdtlseqdt0(xp,xn), inference(clausification, [status(esa)], [m__1870])). % 27.29/5.31 cnf(c116, plain, aNaturalNumber0(xr), inference(clausification, [status(esa)], [m__2342])). % 27.29/5.31 cnf(c143, plain, aNaturalNumber0(sdtsldt0(xn,xr)), inference(clausification, [status(esa)], [m__2504])). % 27.29/5.31 cnf(c144, plain, xn = sdtasdt0(xr,sdtsldt0(xn,xr)), inference(clausification, [status(esa)], [m__2504])). % 27.29/5.31 cnf(c150, plain, sdtlseqdt0(sdtsldt0(xn,xr),xn), inference(clausification, [status(esa)], [m__2504])). % 27.29/5.31 cnf(c158, plain, X0 | doDivides0(xp,xm), inference(clausification, [status(esa)], [m__2645])). % 27.29/5.31 cnf(c163, plain, ~X0 | doDivides0(xp,sdtsldt0(xn,xr)), inference(clausification, [status(esa)], [m__2645])). % 27.29/5.31 cnf(c164, plain, ~aNaturalNumber0(X0) | xn != sdtasdt0(xp,X0), inference(clausification, [status(esa)], [negated_conjecture])). % 27.29/5.31 cnf(c167, plain, ~doDivides0(xp,xm), inference(clausification, [status(esa)], [negated_conjecture])). % 27.29/5.31 cnf(d0, plain, 'Ts116', inference(resolution, [status(thm)], [c167,c158])). % 27.29/5.31 cnf(d1, plain, doDivides0(xp,sdtsldt0(xn,xr)), inference(resolution, [status(thm)], [d0,c163])). % 27.29/5.31 cnf(d2, plain, sdtsldt0(xn,xr) = sz00 | ~aNaturalNumber0(xp) | ~aNaturalNumber0(sdtsldt0(xn,xr)) | sdtlseqdt0(xp,sdtsldt0(xn,xr)), inference(resolution, [status(thm)], [c56,d1])). % 27.29/5.31 cnf(d3, plain, sdtsldt0(xn,xr) = sz00 | ~aNaturalNumber0(sdtsldt0(xn,xr)) | sdtlseqdt0(xp,sdtsldt0(xn,xr)), inference(resolution, [status(thm)], [c72,d2])). % 27.29/5.31 cnf(d4, plain, sdtsldt0(xn,xr) = sz00 | sdtlseqdt0(xp,sdtsldt0(xn,xr)), inference(resolution, [status(thm)], [c143,d3])). % 27.29/5.31 cnf(d5, plain, sdtsldt0(xn,xr) = sz00 | ~aNaturalNumber0(sdtsldt0(xn,xr)) | ~aNaturalNumber0(xp) | ~aNaturalNumber0(X0) | ~sdtlseqdt0(sdtsldt0(xn,xr),X0) | sdtlseqdt0(xp,X0), inference(resolution, [status(thm)], [d4,c32])). % 27.29/5.31 cnf(d6, plain, sdtsldt0(xn,xr) = sz00 | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sdtsldt0(xn,xr)) | ~sdtlseqdt0(sdtsldt0(xn,xr),X0) | sdtlseqdt0(xp,X0), inference(resolution, [status(thm)], [c72,d5])). % 27.29/5.31 cnf(d7, plain, sdtsldt0(xn,xr) = sz00 | ~aNaturalNumber0(X0) | ~sdtlseqdt0(sdtsldt0(xn,xr),X0) | sdtlseqdt0(xp,X0), inference(resolution, [status(thm)], [c143,d6])). % 27.29/5.31 cnf(d8, plain, sdtsldt0(xn,xr) = sz00 | ~aNaturalNumber0(xn) | sdtlseqdt0(xp,xn), inference(resolution, [status(thm)], [d7,c150])). % 27.29/5.31 cnf(d9, plain, sdtsldt0(xn,xr) = sz00 | sdtlseqdt0(xp,xn), inference(resolution, [status(thm)], [c70,d8])). % 27.29/5.31 cnf(d10, plain, sdtsldt0(xn,xr) = sz00, inference(resolution, [status(thm)], [c98,d9])). % 27.29/5.31 cnf(d11, plain, xn = sdtasdt0(xr,sz00), inference(demodulation, [status(thm)], [c144,d10])). % 27.29/5.31 cnf(d12, plain, xn = sz00 | ~aNaturalNumber0(xr), inference(superposition, [status(thm)], [d11,c13])). % 27.29/5.31 cnf(d13, plain, xn = sz00, inference(resolution, [status(thm)], [c116,d12])). % 27.29/5.31 cnf(d14, plain, xn != sz00 | ~aNaturalNumber0(sz00) | ~aNaturalNumber0(xp), inference(superposition, [status(thm)], [c13,c164])). % 27.29/5.31 cnf(d15, plain, xn != sz00 | ~aNaturalNumber0(xp), inference(resolution, [status(thm)], [c0,d14])). % 27.29/5.31 cnf(d16, plain, xn != sz00, inference(resolution, [status(thm)], [c72,d15])). % 27.29/5.31 cnf(d17, plain, $false, inference(resolution, [status(thm)], [d16,d13])). % 27.29/5.31 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------