%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : NUM500+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 : n003.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:12:56 AM UTC 2026 % Result : Theorem 20.34s 3.30s % Output : CNFRefutation 20.34s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : NUM500+1 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.05 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.11/0.36 % Computer : n003.cluster.edu % 0.11/0.36 % Model : x86_64 x86_64 % 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.36 % Memory : 8046.5625MB % 0.11/0.36 % OS : Linux 6.8.0-71-generic % 0.11/0.36 % CPULimit : 300 % 0.11/0.36 % WCLimit : 300 % 0.11/0.36 % DateTime : Sat Sep 26 03:02:08 UTC 2026 % 0.11/0.37 % CPUTime : % 0.11/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 20.34/3.30 % SZS status Theorem for theBenchmark.p % 20.34/3.30 % SZS output start CNFRefutation for theBenchmark.p % 20.34/3.30 fof(mSortsB_02, axiom, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => aNaturalNumber0(sdtasdt0(X0,X1))))). % 20.34/3.30 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)))))))). % 20.34/3.30 fof(mDefPrime, definition, ! [X0] : ((aNaturalNumber0(X0) => (isPrime0(X0) <=> (X0 != sz00 & (X0 != sz10 & ! [X1] : (((aNaturalNumber0(X1) & doDivides0(X1,X0)) => (X1 = sz10 | X1 = X0))))))))). % 20.34/3.30 fof(mPrimDiv, axiom, ! [X0] : (((aNaturalNumber0(X0) & (X0 != sz00 & X0 != sz10)) => ? [X1] : ((aNaturalNumber0(X1) & (doDivides0(X1,X0) & isPrime0(X1))))))). % 20.34/3.30 fof(m__1837, hypothesis, (aNaturalNumber0(xn) & (aNaturalNumber0(xm) & aNaturalNumber0(xp)))). % 20.34/3.30 fof(m__1860, hypothesis, (isPrime0(xp) & doDivides0(xp,sdtasdt0(xn,xm)))). % 20.34/3.30 fof(m__2306, hypothesis, xk = sdtsldt0(sdtasdt0(xn,xm),xp)). % 20.34/3.30 fof(m__2315, hypothesis, ~((xk = sz00 | xk = sz10))). % 20.34/3.30 fof(m__, conjecture, ? [X0] : ((aNaturalNumber0(X0) & (doDivides0(X0,xk) & isPrime0(X0))))). % 20.34/3.30 fof(negated_conjecture, negated_conjecture, ~? [X0] : ((aNaturalNumber0(X0) & (doDivides0(X0,xk) & isPrime0(X0)))), inference(negate_conjecture, [status(cth)], [m__])). % 20.34/3.30 cnf(c4, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | aNaturalNumber0(sdtasdt0(X0,X1)), inference(clausification, [status(esa)], [mSortsB_02])). % 20.34/3.30 cnf(c50, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | X2 != sdtsldt0(X1,X0) | aNaturalNumber0(X2) | ~doDivides0(X0,X1) | X0 = sz00, inference(clausification, [status(esa)], [mDefQuot])). % 20.34/3.30 cnf(c58, plain, ~aNaturalNumber0(X0) | ~isPrime0(X0) | X1(X0), inference(clausification, [status(esa)], [mDefPrime])). % 20.34/3.30 cnf(c60, plain, ~X0(X1) | X1 != sz00, inference(clausification, [status(esa)], [mDefPrime])). % 20.34/3.30 cnf(c67, plain, ~aNaturalNumber0(X0) | X0 = sz00 | X0 = sz10 | aNaturalNumber0(sK85(X0)), inference(clausification, [status(esa)], [mPrimDiv])). % 20.34/3.30 cnf(c68, plain, ~aNaturalNumber0(X0) | X0 = sz00 | X0 = sz10 | doDivides0(sK85(X0),X0), inference(clausification, [status(esa)], [mPrimDiv])). % 20.34/3.30 cnf(c69, plain, ~aNaturalNumber0(X0) | X0 = sz00 | X0 = sz10 | isPrime0(sK85(X0)), inference(clausification, [status(esa)], [mPrimDiv])). % 20.34/3.30 cnf(c70, plain, aNaturalNumber0(xn), inference(clausification, [status(esa)], [m__1837])). % 20.34/3.30 cnf(c71, plain, aNaturalNumber0(xm), inference(clausification, [status(esa)], [m__1837])). % 20.34/3.30 cnf(c72, plain, aNaturalNumber0(xp), inference(clausification, [status(esa)], [m__1837])). % 20.34/3.30 cnf(c74, plain, isPrime0(xp), inference(clausification, [status(esa)], [m__1860])). % 20.34/3.30 cnf(c75, plain, doDivides0(xp,sdtasdt0(xn,xm)), inference(clausification, [status(esa)], [m__1860])). % 20.34/3.30 cnf(c82, plain, xk = sdtsldt0(sdtasdt0(xn,xm),xp), inference(clausification, [status(esa)], [m__2306])). % 20.34/3.30 cnf(c83, plain, xk != sz00, inference(clausification, [status(esa)], [m__2315])). % 20.34/3.30 cnf(c84, plain, xk != sz10, inference(clausification, [status(esa)], [m__2315])). % 20.34/3.30 cnf(c87, plain, ~aNaturalNumber0(X0) | ~doDivides0(X0,xk) | ~isPrime0(X0), inference(clausification, [status(esa)], [negated_conjecture])). % 20.34/3.30 cnf(d0, plain, X0 != xk | xp = sz00 | ~aNaturalNumber0(xp) | aNaturalNumber0(X0) | ~aNaturalNumber0(sdtasdt0(xn,xm)) | ~doDivides0(xp,sdtasdt0(xn,xm)), inference(superposition, [status(thm)], [c82,c50])). % 20.34/3.30 cnf(d1, plain, X0 != xk | xp = sz00 | aNaturalNumber0(X0) | ~aNaturalNumber0(sdtasdt0(xn,xm)) | ~doDivides0(xp,sdtasdt0(xn,xm)), inference(resolution, [status(thm)], [c72,d0])). % 20.34/3.30 cnf(d2, plain, X0 != xk | xp = sz00 | aNaturalNumber0(X0) | ~aNaturalNumber0(sdtasdt0(xn,xm)), inference(resolution, [status(thm)], [c75,d1])). % 20.34/3.30 cnf(d3, plain, xp = sz00 | aNaturalNumber0(xk) | ~aNaturalNumber0(sdtasdt0(xn,xm)), inference(equality_resolution, [status(thm)], [d2])). % 20.34/3.30 cnf(d4, plain, xk = sz00 | xk = sz10 | ~aNaturalNumber0(xk) | ~aNaturalNumber0(sK85(xk)) | ~isPrime0(sK85(xk)), inference(resolution, [status(thm)], [c68,c87])). % 20.34/3.30 cnf(d5, plain, xk = sz10 | ~aNaturalNumber0(sK85(xk)) | ~aNaturalNumber0(xk) | ~isPrime0(sK85(xk)), inference(resolution, [status(thm)], [c83,d4])). % 20.34/3.30 cnf(d6, plain, ~aNaturalNumber0(sK85(xk)) | ~aNaturalNumber0(xk) | ~isPrime0(sK85(xk)), inference(resolution, [status(thm)], [c84,d5])). % 20.34/3.30 cnf(d7, plain, xk = sz00 | xk = sz10 | ~aNaturalNumber0(xk) | ~aNaturalNumber0(sK85(xk)) | ~aNaturalNumber0(xk), inference(resolution, [status(thm)], [c69,d6])). % 20.34/3.30 cnf(d8, plain, xk = sz10 | ~aNaturalNumber0(sK85(xk)) | ~aNaturalNumber0(xk), inference(resolution, [status(thm)], [c83,d7])). % 20.34/3.30 cnf(d9, plain, ~aNaturalNumber0(sK85(xk)) | ~aNaturalNumber0(xk), inference(resolution, [status(thm)], [c84,d8])). % 20.34/3.30 cnf(d10, plain, ~aNaturalNumber0(xk) | xk = sz00 | xk = sz10 | ~aNaturalNumber0(xk), inference(resolution, [status(thm)], [d9,c67])). % 20.34/3.30 cnf(d11, plain, xk = sz10 | ~aNaturalNumber0(xk), inference(resolution, [status(thm)], [c83,d10])). % 20.34/3.30 cnf(d12, plain, ~aNaturalNumber0(xk), inference(resolution, [status(thm)], [c84,d11])). % 20.34/3.30 cnf(d13, plain, xp = sz00 | ~aNaturalNumber0(sdtasdt0(xn,xm)), inference(resolution, [status(thm)], [d12,d3])). % 20.34/3.30 cnf(d14, plain, xp = sz00 | ~aNaturalNumber0(xm) | ~aNaturalNumber0(xn), inference(resolution, [status(thm)], [d13,c4])). % 20.34/3.30 cnf(d15, plain, xp = sz00 | ~aNaturalNumber0(xm), inference(resolution, [status(thm)], [c70,d14])). % 20.34/3.30 cnf(d16, plain, xp = sz00, inference(resolution, [status(thm)], [c71,d15])). % 20.34/3.30 cnf(d17, plain, ~aNaturalNumber0(xp) | 'Ts80'(xp), inference(resolution, [status(thm)], [c58,c74])). % 20.34/3.30 cnf(d18, plain, 'Ts80'(xp), inference(resolution, [status(thm)], [c72,d17])). % 20.34/3.30 cnf(d19, plain, 'Ts80'(sz00), inference(demodulation, [status(thm)], [d18,d16])). % 20.34/3.30 cnf(d20, plain, ~'Ts80'(sz00), inference(equality_resolution, [status(thm)], [c60])). % 20.34/3.30 cnf(d21, plain, $false, inference(resolution, [status(thm)], [d20,d19])). % 20.34/3.30 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------