%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : NUM518+1 : 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 : n026.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 32.31s 9.39s % Output : CNFRefutation 32.31s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM518+1 : 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/5.37 % Computer : n026.cluster.edu % 0.09/5.37 % Model : x86_64 x86_64 % 0.09/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/5.37 % Memory : 8046.5625MB % 0.09/5.37 % OS : Linux 6.8.0-71-generic % 0.09/5.37 % CPULimit : 300 % 0.09/5.37 % WCLimit : 300 % 0.09/5.37 % DateTime : Sat Sep 26 03:08:18 UTC 2026 % 0.09/5.37 % CPUTime : % 0.09/5.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 32.31/9.39 % SZS status Theorem for theBenchmark.p % 32.31/9.39 % SZS output start CNFRefutation for theBenchmark.p % 32.31/9.39 fof(m_MulZero, axiom, ! [X0] : ((aNaturalNumber0(X0) => (sdtasdt0(X0,sz00) = sz00 & sz00 = sdtasdt0(sz00,X0))))). % 32.31/9.39 fof(mLETran, axiom, ! [X0] : ! [X1] : ! [X2] : (((aNaturalNumber0(X0) & (aNaturalNumber0(X1) & aNaturalNumber0(X2))) => ((sdtlseqdt0(X0,X1) & sdtlseqdt0(X1,X2)) => sdtlseqdt0(X0,X2))))). % 32.31/9.39 fof(mDefQuot, definition, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => ((X0 != sz00 & doDivides0(X0,X1)) => ! [X2] : ((X2 = sdtsldt0(X1,X0) <=> (aNaturalNumber0(X2) & X1 = sdtasdt0(X0,X2)))))))). % 32.31/9.39 fof(mDivLE, axiom, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => ((doDivides0(X0,X1) & X1 != sz00) => sdtlseqdt0(X0,X1))))). % 32.31/9.39 fof(mDefPrime, definition, ! [X0] : ((aNaturalNumber0(X0) => (isPrime0(X0) <=> (X0 != sz00 & (X0 != sz10 & ! [X1] : (((aNaturalNumber0(X1) & doDivides0(X1,X0)) => (X1 = sz10 | X1 = X0))))))))). % 32.31/9.39 fof(m__1837, hypothesis, (aNaturalNumber0(xn) & (aNaturalNumber0(xm) & aNaturalNumber0(xp)))). % 32.31/9.39 fof(m__1870, hypothesis, ~sdtlseqdt0(xp,xn)). % 32.31/9.39 fof(m__2342, hypothesis, (aNaturalNumber0(xr) & (doDivides0(xr,xk) & isPrime0(xr)))). % 32.31/9.39 fof(m__2487, hypothesis, doDivides0(xr,xn)). % 32.31/9.39 fof(m__2504, hypothesis, (sdtsldt0(xn,xr) != xn & sdtlseqdt0(sdtsldt0(xn,xr),xn))). % 32.31/9.39 fof(m__2645, hypothesis, (doDivides0(xp,sdtsldt0(xn,xr)) | doDivides0(xp,xm))). % 32.31/9.39 fof(m__, conjecture, (doDivides0(xp,xn) | doDivides0(xp,xm))). % 32.31/9.39 fof(negated_conjecture, negated_conjecture, ~((doDivides0(xp,xn) | doDivides0(xp,xm))), inference(negate_conjecture, [status(cth)], [m__])). % 32.31/9.39 cnf(c13, plain, ~aNaturalNumber0(X0) | sdtasdt0(X0,sz00) = sz00, inference(clausification, [status(esa)], [m_MulZero])). % 32.31/9.39 cnf(c32, plain, sdtlseqdt0(X0,X1) | ~sdtlseqdt0(X2,X1) | ~aNaturalNumber0(X0) | ~aNaturalNumber0(X2) | ~sdtlseqdt0(X0,X2) | ~aNaturalNumber0(X1), inference(clausification, [status(esa)], [mLETran])). % 32.31/9.39 cnf(c50, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | X2 != sdtsldt0(X1,X0) | aNaturalNumber0(X2) | ~doDivides0(X0,X1) | X0 = sz00, inference(clausification, [status(esa)], [mDefQuot])). % 32.31/9.39 cnf(c51, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | X2 != sdtsldt0(X1,X0) | X1 = sdtasdt0(X0,X2) | ~doDivides0(X0,X1) | X0 = sz00, inference(clausification, [status(esa)], [mDefQuot])). % 32.31/9.39 cnf(c56, plain, ~aNaturalNumber0(X0) | X1 = sz00 | sdtlseqdt0(X0,X1) | ~doDivides0(X0,X1) | ~aNaturalNumber0(X1), inference(clausification, [status(esa)], [mDivLE])). % 32.31/9.39 cnf(c58, plain, ~aNaturalNumber0(X0) | ~isPrime0(X0) | X1(X0), inference(clausification, [status(esa)], [mDefPrime])). % 32.31/9.39 cnf(c60, plain, ~X0(X1) | X1 != sz00, inference(clausification, [status(esa)], [mDefPrime])). % 32.31/9.39 cnf(c70, plain, aNaturalNumber0(xn), inference(clausification, [status(esa)], [m__1837])). % 32.31/9.39 cnf(c72, plain, aNaturalNumber0(xp), inference(clausification, [status(esa)], [m__1837])). % 32.31/9.39 cnf(c76, plain, ~sdtlseqdt0(xp,xn), inference(clausification, [status(esa)], [m__1870])). % 32.31/9.39 cnf(c87, plain, aNaturalNumber0(xr), inference(clausification, [status(esa)], [m__2342])). % 32.31/9.39 cnf(c89, plain, isPrime0(xr), inference(clausification, [status(esa)], [m__2342])). % 32.31/9.39 cnf(c95, plain, doDivides0(xr,xn), inference(clausification, [status(esa)], [m__2487])). % 32.31/9.39 cnf(c97, plain, sdtlseqdt0(sdtsldt0(xn,xr),xn), inference(clausification, [status(esa)], [m__2504])). % 32.31/9.39 cnf(c99, plain, doDivides0(xp,sdtsldt0(xn,xr)) | doDivides0(xp,xm), inference(clausification, [status(esa)], [m__2645])). % 32.31/9.39 cnf(c100, plain, ~doDivides0(xp,xn), inference(clausification, [status(esa)], [negated_conjecture])). % 32.31/9.39 cnf(c101, plain, ~doDivides0(xp,xm), inference(clausification, [status(esa)], [negated_conjecture])). % 32.31/9.39 cnf(d0, plain, doDivides0(xp,sdtsldt0(xn,xr)), inference(resolution, [status(thm)], [c101,c99])). % 32.31/9.39 cnf(d1, plain, sdtsldt0(xn,xr) = sz00 | ~aNaturalNumber0(xp) | ~aNaturalNumber0(sdtsldt0(xn,xr)) | sdtlseqdt0(xp,sdtsldt0(xn,xr)), inference(resolution, [status(thm)], [d0,c56])). % 32.31/9.39 cnf(d2, plain, sdtsldt0(xn,xr) = sz00 | ~aNaturalNumber0(sdtsldt0(xn,xr)) | sdtlseqdt0(xp,sdtsldt0(xn,xr)), inference(resolution, [status(thm)], [c72,d1])). % 32.31/9.39 cnf(d3, plain, sdtsldt0(xn,xr) = sz00 | ~aNaturalNumber0(sdtsldt0(xn,xr)) | ~aNaturalNumber0(sdtsldt0(xn,xr)) | ~aNaturalNumber0(xp) | ~aNaturalNumber0(X0) | ~sdtlseqdt0(sdtsldt0(xn,xr),X0) | sdtlseqdt0(xp,X0), inference(resolution, [status(thm)], [d2,c32])). % 32.31/9.39 cnf(d4, plain, sdtsldt0(xn,xr) = sz00 | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sdtsldt0(xn,xr)) | ~sdtlseqdt0(sdtsldt0(xn,xr),X0) | sdtlseqdt0(xp,X0), inference(resolution, [status(thm)], [c72,d3])). % 32.31/9.39 cnf(d5, plain, sdtsldt0(xn,xr) = sz00 | ~aNaturalNumber0(xn) | ~aNaturalNumber0(sdtsldt0(xn,xr)) | sdtlseqdt0(xp,xn), inference(resolution, [status(thm)], [d4,c97])). % 32.31/9.39 cnf(d6, plain, sdtsldt0(xn,xr) = sz00 | ~aNaturalNumber0(sdtsldt0(xn,xr)) | sdtlseqdt0(xp,xn), inference(resolution, [status(thm)], [c70,d5])). % 32.31/9.39 cnf(d7, plain, sdtsldt0(xn,xr) = sz00 | ~aNaturalNumber0(sdtsldt0(xn,xr)), inference(resolution, [status(thm)], [c76,d6])). % 32.31/9.39 cnf(d8, plain, X0 = sz00 | ~aNaturalNumber0(X0) | aNaturalNumber0(sdtsldt0(X1,X0)) | ~aNaturalNumber0(X1) | ~doDivides0(X0,X1), inference(equality_resolution, [status(thm)], [c50])). % 32.31/9.39 cnf(d9, plain, xr = sz00 | ~aNaturalNumber0(xn) | ~aNaturalNumber0(xr) | ~doDivides0(xr,xn) | sdtsldt0(xn,xr) = sz00, inference(resolution, [status(thm)], [d8,d7])). % 32.31/9.39 cnf(d10, plain, sdtsldt0(xn,xr) = sz00 | xr = sz00 | ~aNaturalNumber0(xr) | ~doDivides0(xr,xn), inference(resolution, [status(thm)], [c70,d9])). % 32.31/9.39 cnf(d11, plain, sdtsldt0(xn,xr) = sz00 | xr = sz00 | ~doDivides0(xr,xn), inference(resolution, [status(thm)], [c87,d10])). % 32.31/9.39 cnf(d12, plain, sdtsldt0(xn,xr) = sz00 | xr = sz00, inference(resolution, [status(thm)], [c95,d11])). % 32.31/9.39 cnf(d13, plain, doDivides0(xp,sz00) | xr = sz00, inference(superposition, [status(thm)], [d12,d0])). % 32.31/9.39 cnf(d14, plain, ~aNaturalNumber0(xr) | 'Ts80'(xr), inference(resolution, [status(thm)], [c58,c89])). % 32.31/9.39 cnf(d15, plain, 'Ts80'(xr), inference(resolution, [status(thm)], [c87,d14])). % 32.31/9.39 cnf(d16, plain, sdtasdt0(xr,sz00) = sz00, inference(resolution, [status(thm)], [c13,c87])). % 32.31/9.39 cnf(d17, plain, X0 != sz00 | xr = sz00 | xn = sdtasdt0(xr,X0) | ~aNaturalNumber0(xr) | ~aNaturalNumber0(xn) | ~doDivides0(xr,xn) | xr = sz00, inference(superposition, [status(thm)], [d12,c51])). % 32.31/9.39 cnf(d18, plain, X0 != sz00 | xn = sdtasdt0(xr,X0) | xr = sz00 | ~aNaturalNumber0(xr) | ~doDivides0(xr,xn), inference(resolution, [status(thm)], [c70,d17])). % 32.31/9.39 cnf(d19, plain, X0 != sz00 | xn = sdtasdt0(xr,X0) | xr = sz00 | ~doDivides0(xr,xn), inference(resolution, [status(thm)], [c87,d18])). % 32.31/9.39 cnf(d20, plain, X0 != sz00 | xn = sdtasdt0(xr,X0) | xr = sz00, inference(resolution, [status(thm)], [c95,d19])). % 32.31/9.39 cnf(d21, plain, xn = sdtasdt0(xr,sz00) | xr = sz00, inference(equality_resolution, [status(thm)], [d20])). % 32.31/9.39 cnf(d22, plain, xn = sz00 | xr = sz00, inference(demodulation, [status(thm)], [d21,d16])). % 32.31/9.39 cnf(d23, plain, 'Ts80'(sz00) | xn = sz00, inference(superposition, [status(thm)], [d22,d15])). % 32.31/9.39 cnf(d24, plain, ~'Ts80'(sz00), inference(equality_resolution, [status(thm)], [c60])). % 32.31/9.39 cnf(d25, plain, xn = sz00, inference(resolution, [status(thm)], [d24,d23])). % 32.31/9.39 cnf(d26, plain, ~doDivides0(xp,sz00), inference(demodulation, [status(thm)], [c100,d25])). % 32.31/9.39 cnf(d27, plain, xr = sz00, inference(resolution, [status(thm)], [d26,d13])). % 32.31/9.39 cnf(d28, plain, 'Ts80'(sz00), inference(demodulation, [status(thm)], [d15,d27])). % 32.31/9.39 cnf(d29, plain, $false, inference(resolution, [status(thm)], [d24,d28])). % 32.31/9.39 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------