%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : NUM512+3 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n014.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:59 AM UTC 2026 % Result : Theorem 43.55s 6.09s % Output : CNFRefutation 43.55s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM512+3 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.05 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.17/0.44 % Computer : n014.cluster.edu % 0.17/0.44 % Model : x86_64 x86_64 % 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.44 % Memory : 8046.5625MB % 0.17/0.44 % OS : Linux 6.8.0-71-generic % 0.17/0.44 % CPULimit : 300 % 0.17/0.44 % WCLimit : 300 % 0.17/0.44 % DateTime : Sat Sep 26 03:03:47 UTC 2026 % 0.17/0.44 % CPUTime : % 0.17/0.45 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 43.55/6.09 % SZS status Theorem for theBenchmark.p % 43.55/6.09 % SZS output start CNFRefutation for theBenchmark.p % 43.55/6.09 fof(mMulComm, axiom, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => sdtasdt0(X0,X1) = sdtasdt0(X1,X0)))). % 43.55/6.09 fof(mMulAsso, axiom, ! [X0] : ! [X1] : ! [X2] : (((aNaturalNumber0(X0) & (aNaturalNumber0(X1) & aNaturalNumber0(X2))) => sdtasdt0(sdtasdt0(X0,X1),X2) = sdtasdt0(X0,sdtasdt0(X1,X2))))). % 43.55/6.09 fof(m__1837, hypothesis, (aNaturalNumber0(xn) & (aNaturalNumber0(xm) & aNaturalNumber0(xp)))). % 43.55/6.09 fof(m__2306, hypothesis, (aNaturalNumber0(xk) & (sdtasdt0(xn,xm) = sdtasdt0(xp,xk) & xk = sdtsldt0(sdtasdt0(xn,xm),xp)))). % 43.55/6.09 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)))))))). % 43.55/6.09 fof(m__2362, hypothesis, (? [X0] : ((aNaturalNumber0(X0) & sdtpldt0(xr,X0) = xk)) & (? [X0] : ((aNaturalNumber0(X0) & sdtasdt0(xn,xm) = sdtasdt0(xr,X0))) & doDivides0(xr,sdtasdt0(xn,xm))))). % 43.55/6.09 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)))))). % 43.55/6.09 fof(m__, conjecture, (((aNaturalNumber0(sdtsldt0(xn,xr)) & xn = sdtasdt0(xr,sdtsldt0(xn,xr))) => sdtasdt0(sdtasdt0(sdtsldt0(xn,xr),xm),xr) = sdtasdt0(xn,xm)) & ((aNaturalNumber0(sdtsldt0(sdtasdt0(xp,xk),xr)) & sdtasdt0(xp,xk) = sdtasdt0(xr,sdtsldt0(sdtasdt0(xp,xk),xr))) => sdtasdt0(xn,xm) = sdtasdt0(sdtsldt0(sdtasdt0(xp,xk),xr),xr)))). % 43.55/6.09 fof(negated_conjecture, negated_conjecture, ~((((aNaturalNumber0(sdtsldt0(xn,xr)) & xn = sdtasdt0(xr,sdtsldt0(xn,xr))) => sdtasdt0(sdtasdt0(sdtsldt0(xn,xr),xm),xr) = sdtasdt0(xn,xm)) & ((aNaturalNumber0(sdtsldt0(sdtasdt0(xp,xk),xr)) & sdtasdt0(xp,xk) = sdtasdt0(xr,sdtsldt0(sdtasdt0(xp,xk),xr))) => sdtasdt0(xn,xm) = sdtasdt0(sdtsldt0(sdtasdt0(xp,xk),xr),xr)))), inference(negate_conjecture, [status(cth)], [m__])). % 43.55/6.09 cnf(c9, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | sdtasdt0(X0,X1) = sdtasdt0(X1,X0), inference(clausification, [status(esa)], [mMulComm])). % 43.55/6.09 cnf(c10, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | ~aNaturalNumber0(X2) | sdtasdt0(sdtasdt0(X0,X1),X2) = sdtasdt0(X0,sdtasdt0(X1,X2)), inference(clausification, [status(esa)], [mMulAsso])). % 43.55/6.09 cnf(c70, plain, aNaturalNumber0(xn), inference(clausification, [status(esa)], [m__1837])). % 43.55/6.09 cnf(c71, plain, aNaturalNumber0(xm), inference(clausification, [status(esa)], [m__1837])). % 43.55/6.09 cnf(c110, plain, sdtasdt0(xn,xm) = sdtasdt0(xp,xk), inference(clausification, [status(esa)], [m__2306])). % 43.55/6.09 cnf(c116, plain, aNaturalNumber0(xr), inference(clausification, [status(esa)], [m__2342])). % 43.55/6.09 cnf(c128, plain, sdtasdt0(xn,xm) = sdtasdt0(xr,sK108), inference(clausification, [status(esa)], [m__2362])). % 43.55/6.09 cnf(c143, plain, aNaturalNumber0(sdtsldt0(xn,xr)), inference(clausification, [status(esa)], [m__2504])). % 43.55/6.09 cnf(c144, plain, xn = sdtasdt0(xr,sdtsldt0(xn,xr)), inference(clausification, [status(esa)], [m__2504])). % 43.55/6.09 cnf(c151, plain, ~X0 | aNaturalNumber0(sdtsldt0(sdtasdt0(xp,xk),xr)), inference(clausification, [status(esa)], [negated_conjecture])). % 43.55/6.09 cnf(c152, plain, ~X0 | sdtasdt0(xp,xk) = sdtasdt0(xr,sdtsldt0(sdtasdt0(xp,xk),xr)), inference(clausification, [status(esa)], [negated_conjecture])). % 43.55/6.09 cnf(c153, plain, ~X0 | sdtasdt0(xn,xm) != sdtasdt0(sdtsldt0(sdtasdt0(xp,xk),xr),xr), inference(clausification, [status(esa)], [negated_conjecture])). % 43.55/6.09 cnf(c156, plain, X0 | sdtasdt0(sdtasdt0(sdtsldt0(xn,xr),xm),xr) != sdtasdt0(xn,xm), inference(clausification, [status(esa)], [negated_conjecture])). % 43.55/6.09 cnf(d0, plain, sdtasdt0(sdtasdt0(sdtsldt0(xn,xr),xm),xr) != sdtasdt0(xr,sK108) | 'Ts115', inference(demodulation, [status(thm)], [c156,c128])). % 43.55/6.09 cnf(d1, plain, sdtasdt0(sdtasdt0(xm,sdtsldt0(xn,xr)),xr) != sdtasdt0(xr,sK108) | 'Ts115' | ~aNaturalNumber0(sdtsldt0(xn,xr)) | ~aNaturalNumber0(xm), inference(superposition, [status(thm)], [c9,d0])). % 43.55/6.09 cnf(d2, plain, sdtasdt0(sdtasdt0(xm,sdtsldt0(xn,xr)),xr) != sdtasdt0(xr,sK108) | ~aNaturalNumber0(sdtsldt0(xn,xr)) | 'Ts115', inference(resolution, [status(thm)], [c71,d1])). % 43.55/6.09 cnf(d3, plain, sdtasdt0(sdtasdt0(xm,sdtsldt0(xn,xr)),xr) != sdtasdt0(xr,sK108) | 'Ts115', inference(resolution, [status(thm)], [c143,d2])). % 43.55/6.09 cnf(d4, plain, aNaturalNumber0(sdtsldt0(sdtasdt0(xn,xm),xr)) | ~'Ts115', inference(demodulation, [status(thm)], [c151,c110])). % 43.55/6.09 cnf(d5, plain, aNaturalNumber0(sdtsldt0(sdtasdt0(xr,sK108),xr)) | ~'Ts115', inference(demodulation, [status(thm)], [d4,c128])). % 43.55/6.09 cnf(d6, plain, sdtasdt0(xn,xm) != sdtasdt0(sdtsldt0(sdtasdt0(xn,xm),xr),xr) | ~'Ts115', inference(demodulation, [status(thm)], [c153,c110])). % 43.55/6.09 cnf(d7, plain, sdtasdt0(xr,sK108) != sdtasdt0(sdtsldt0(sdtasdt0(xn,xm),xr),xr) | ~'Ts115', inference(demodulation, [status(thm)], [d6,c128])). % 43.55/6.09 cnf(d8, plain, sdtasdt0(xr,sK108) != sdtasdt0(sdtsldt0(sdtasdt0(xr,sK108),xr),xr) | ~'Ts115', inference(demodulation, [status(thm)], [d7,c128])). % 43.55/6.09 cnf(d9, plain, sdtasdt0(xr,sK108) != sdtasdt0(xr,sdtsldt0(sdtasdt0(xr,sK108),xr)) | ~'Ts115' | ~aNaturalNumber0(sdtsldt0(sdtasdt0(xr,sK108),xr)) | ~aNaturalNumber0(xr), inference(superposition, [status(thm)], [c9,d8])). % 43.55/6.09 cnf(d10, plain, sdtasdt0(xr,sK108) != sdtasdt0(xr,sdtsldt0(sdtasdt0(xr,sK108),xr)) | ~aNaturalNumber0(sdtsldt0(sdtasdt0(xr,sK108),xr)) | ~'Ts115', inference(resolution, [status(thm)], [c116,d9])). % 43.55/6.09 cnf(d11, plain, sdtasdt0(xn,xm) = sdtasdt0(xr,sdtsldt0(sdtasdt0(xp,xk),xr)) | ~'Ts115', inference(demodulation, [status(thm)], [c152,c110])). % 43.55/6.09 cnf(d12, plain, sdtasdt0(xn,xm) = sdtasdt0(xr,sdtsldt0(sdtasdt0(xn,xm),xr)) | ~'Ts115', inference(demodulation, [status(thm)], [d11,c110])). % 43.55/6.09 cnf(d13, plain, sdtasdt0(xr,sK108) = sdtasdt0(xr,sdtsldt0(sdtasdt0(xn,xm),xr)) | ~'Ts115', inference(demodulation, [status(thm)], [d12,c128])). % 43.55/6.09 cnf(d14, plain, sdtasdt0(xr,sK108) = sdtasdt0(xr,sdtsldt0(sdtasdt0(xr,sK108),xr)) | ~'Ts115', inference(demodulation, [status(thm)], [d13,c128])). % 43.55/6.09 cnf(d15, plain, sdtasdt0(xr,sK108) != sdtasdt0(xr,sK108) | ~aNaturalNumber0(sdtsldt0(sdtasdt0(xr,sK108),xr)) | ~'Ts115' | ~'Ts115', inference(superposition, [status(thm)], [d14,d10])). % 43.55/6.09 cnf(d16, plain, ~aNaturalNumber0(sdtsldt0(sdtasdt0(xr,sK108),xr)) | ~'Ts115', inference(equality_resolution, [status(thm)], [d15])). % 43.55/6.09 cnf(d17, plain, ~'Ts115' | ~'Ts115', inference(resolution, [status(thm)], [d16,d5])). % 43.55/6.09 cnf(d18, plain, sdtasdt0(sdtasdt0(xm,sdtsldt0(xn,xr)),xr) != sdtasdt0(xr,sK108), inference(resolution, [status(thm)], [d17,d3])). % 43.55/6.09 cnf(d19, plain, sdtasdt0(xm,sdtasdt0(sdtsldt0(xn,xr),xr)) != sdtasdt0(xr,sK108) | ~aNaturalNumber0(xr) | ~aNaturalNumber0(sdtsldt0(xn,xr)) | ~aNaturalNumber0(xm), inference(superposition, [status(thm)], [c10,d18])). % 43.55/6.09 cnf(d20, plain, sdtasdt0(xm,sdtasdt0(sdtsldt0(xn,xr),xr)) != sdtasdt0(xr,sK108) | ~aNaturalNumber0(sdtsldt0(xn,xr)) | ~aNaturalNumber0(xr), inference(resolution, [status(thm)], [c71,d19])). % 43.55/6.09 cnf(d21, plain, sdtasdt0(xm,sdtasdt0(sdtsldt0(xn,xr),xr)) != sdtasdt0(xr,sK108) | ~aNaturalNumber0(sdtsldt0(xn,xr)), inference(resolution, [status(thm)], [c116,d20])). % 43.55/6.09 cnf(d22, plain, sdtasdt0(xm,sdtasdt0(sdtsldt0(xn,xr),xr)) != sdtasdt0(xr,sK108), inference(resolution, [status(thm)], [c143,d21])). % 43.55/6.09 cnf(d23, plain, sdtasdt0(xm,sdtasdt0(xr,sdtsldt0(xn,xr))) != sdtasdt0(xr,sK108) | ~aNaturalNumber0(sdtsldt0(xn,xr)) | ~aNaturalNumber0(xr), inference(superposition, [status(thm)], [c9,d22])). % 43.55/6.09 cnf(d24, plain, sdtasdt0(xm,xn) != sdtasdt0(xr,sK108) | ~aNaturalNumber0(sdtsldt0(xn,xr)) | ~aNaturalNumber0(xr), inference(demodulation, [status(thm)], [d23,c144])). % 43.55/6.09 cnf(d25, plain, sdtasdt0(xm,xn) != sdtasdt0(xr,sK108) | ~aNaturalNumber0(sdtsldt0(xn,xr)), inference(resolution, [status(thm)], [c116,d24])). % 43.55/6.09 cnf(d26, plain, sdtasdt0(xm,xn) != sdtasdt0(xr,sK108), inference(resolution, [status(thm)], [c143,d25])). % 43.55/6.09 cnf(d27, plain, sdtasdt0(xn,xm) != sdtasdt0(xr,sK108) | ~aNaturalNumber0(xm) | ~aNaturalNumber0(xn), inference(superposition, [status(thm)], [c9,d26])). % 43.55/6.09 cnf(d28, plain, sdtasdt0(xr,sK108) != sdtasdt0(xr,sK108) | ~aNaturalNumber0(xn) | ~aNaturalNumber0(xm), inference(demodulation, [status(thm)], [d27,c128])). % 43.55/6.09 cnf(d29, plain, sdtasdt0(xr,sK108) != sdtasdt0(xr,sK108) | ~aNaturalNumber0(xm), inference(resolution, [status(thm)], [c70,d28])). % 43.55/6.09 cnf(d30, plain, sdtasdt0(xr,sK108) != sdtasdt0(xr,sK108), inference(resolution, [status(thm)], [c71,d29])). % 43.55/6.09 cnf(d31, plain, $false, inference(equality_resolution, [status(thm)], [d30])). % 43.55/6.09 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------