%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : NUM476+2 : 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 : n007.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:51 AM UTC 2026 % Result : Theorem 23.34s 3.43s % Output : CNFRefutation 23.34s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM476+2 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.10/0.35 % Computer : n007.cluster.edu % 0.10/0.35 % Model : x86_64 x86_64 % 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.35 % Memory : 8046.5625MB % 0.10/0.35 % OS : Linux 6.8.0-71-generic % 0.10/0.35 % CPULimit : 300 % 0.10/0.35 % WCLimit : 300 % 0.10/0.35 % DateTime : Sat Sep 26 02:52:39 UTC 2026 % 0.10/0.35 % CPUTime : % 0.10/0.35 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 23.34/3.43 % SZS status Theorem for theBenchmark.p % 23.34/3.43 % SZS output start CNFRefutation for theBenchmark.p % 23.34/3.43 fof(m_AddZero, axiom, ! [X0] : ((aNaturalNumber0(X0) => (sdtpldt0(X0,sz00) = X0 & X0 = sdtpldt0(sz00,X0))))). % 23.34/3.43 fof(m_MulZero, axiom, ! [X0] : ((aNaturalNumber0(X0) => (sdtasdt0(X0,sz00) = sz00 & sz00 = sdtasdt0(sz00,X0))))). % 23.34/3.43 fof(m__1324, hypothesis, (aNaturalNumber0(xl) & (aNaturalNumber0(xm) & aNaturalNumber0(xn)))). % 23.34/3.43 fof(m__1324_04, hypothesis, (? [X0] : ((aNaturalNumber0(X0) & xm = sdtasdt0(xl,X0))) & (doDivides0(xl,xm) & (? [X0] : ((aNaturalNumber0(X0) & sdtpldt0(xm,xn) = sdtasdt0(xl,X0))) & doDivides0(xl,sdtpldt0(xm,xn)))))). % 23.34/3.43 fof(m__, conjecture, ((xl != sz00 => ? [X0] : ((aNaturalNumber0(X0) & (xm = sdtasdt0(xl,X0) & (X0 = sdtsldt0(xm,xl) & ? [X1] : ((aNaturalNumber0(X1) & (sdtpldt0(xm,xn) = sdtasdt0(xl,X1) & (X1 = sdtsldt0(sdtpldt0(xm,xn),xl) & (? [X2] : ((aNaturalNumber0(X2) & sdtpldt0(X0,X2) = X1)) & (sdtlseqdt0(X0,X1) & ? [X2] : ((aNaturalNumber0(X2) & (sdtpldt0(X0,X2) = X1 & (X2 = sdtmndt0(X1,X0) & (sdtpldt0(sdtasdt0(xl,X0),sdtasdt0(xl,X2)) = sdtpldt0(sdtasdt0(xl,X0),xn) & xn = sdtasdt0(xl,X2))))))))))))))))) => (? [X0] : ((aNaturalNumber0(X0) & xn = sdtasdt0(xl,X0))) | doDivides0(xl,xn)))). % 23.34/3.43 fof(negated_conjecture, negated_conjecture, ~(((xl != sz00 => ? [X0] : ((aNaturalNumber0(X0) & (xm = sdtasdt0(xl,X0) & (X0 = sdtsldt0(xm,xl) & ? [X1] : ((aNaturalNumber0(X1) & (sdtpldt0(xm,xn) = sdtasdt0(xl,X1) & (X1 = sdtsldt0(sdtpldt0(xm,xn),xl) & (? [X2] : ((aNaturalNumber0(X2) & sdtpldt0(X0,X2) = X1)) & (sdtlseqdt0(X0,X1) & ? [X2] : ((aNaturalNumber0(X2) & (sdtpldt0(X0,X2) = X1 & (X2 = sdtmndt0(X1,X0) & (sdtpldt0(sdtasdt0(xl,X0),sdtasdt0(xl,X2)) = sdtpldt0(sdtasdt0(xl,X0),xn) & xn = sdtasdt0(xl,X2))))))))))))))))) => (? [X0] : ((aNaturalNumber0(X0) & xn = sdtasdt0(xl,X0))) | doDivides0(xl,xn)))), inference(negate_conjecture, [status(cth)], [m__])). % 23.34/3.43 cnf(c8, plain, ~aNaturalNumber0(X0) | X0 = sdtpldt0(sz00,X0), inference(clausification, [status(esa)], [m_AddZero])). % 23.34/3.43 cnf(c14, plain, ~aNaturalNumber0(X0) | sz00 = sdtasdt0(sz00,X0), inference(clausification, [status(esa)], [m_MulZero])). % 23.34/3.43 cnf(c57, plain, aNaturalNumber0(xn), inference(clausification, [status(esa)], [m__1324])). % 23.34/3.43 cnf(c58, plain, aNaturalNumber0(sK72), inference(clausification, [status(esa)], [m__1324_04])). % 23.34/3.43 cnf(c59, plain, xm = sdtasdt0(xl,sK72), inference(clausification, [status(esa)], [m__1324_04])). % 23.34/3.43 cnf(c62, plain, sdtpldt0(xm,xn) = sdtasdt0(xl,sK73), inference(clausification, [status(esa)], [m__1324_04])). % 23.34/3.43 cnf(c63, plain, doDivides0(xl,sdtpldt0(xm,xn)), inference(clausification, [status(esa)], [m__1324_04])). % 23.34/3.43 cnf(c64, plain, xl = sz00 | X0, inference(clausification, [status(esa)], [negated_conjecture])). % 23.34/3.43 cnf(c65, plain, ~aNaturalNumber0(X0) | xn != sdtasdt0(xl,X0), inference(clausification, [status(esa)], [negated_conjecture])). % 23.34/3.43 cnf(c66, plain, ~doDivides0(xl,xn), inference(clausification, [status(esa)], [negated_conjecture])). % 23.34/3.43 cnf(c76, plain, ~X0 | aNaturalNumber0(sK79), inference(clausification, [status(esa)], [negated_conjecture])). % 23.34/3.43 cnf(c80, plain, ~X0 | xn = sdtasdt0(xl,sK79), inference(clausification, [status(esa)], [negated_conjecture])). % 23.34/3.43 cnf(d0, plain, xn = sdtpldt0(sz00,xn), inference(resolution, [status(thm)], [c57,c8])). % 23.34/3.43 cnf(d1, plain, sz00 = sdtasdt0(sz00,sK72), inference(resolution, [status(thm)], [c58,c14])). % 23.34/3.43 cnf(d2, plain, xn = sdtasdt0(xl,sK79) | xl = sz00, inference(resolution, [status(thm)], [c80,c64])). % 23.34/3.43 cnf(d3, plain, xn != xn | ~aNaturalNumber0(sK79) | xl = sz00, inference(superposition, [status(thm)], [d2,c65])). % 23.34/3.43 cnf(d4, plain, xl = sz00 | ~aNaturalNumber0(sK79), inference(equality_resolution, [status(thm)], [d3])). % 23.34/3.43 cnf(d5, plain, xl = sz00 | ~'Ts74', inference(resolution, [status(thm)], [d4,c76])). % 23.34/3.43 cnf(d6, plain, xl = sz00 | xl = sz00, inference(resolution, [status(thm)], [d5,c64])). % 23.34/3.43 cnf(d7, plain, xm = sdtasdt0(sz00,sK72), inference(demodulation, [status(thm)], [c59,d6])). % 23.34/3.43 cnf(d8, plain, xm = sz00, inference(demodulation, [status(thm)], [d7,d1])). % 23.34/3.43 cnf(d9, plain, sdtpldt0(xm,xn) = sdtasdt0(sz00,sK73), inference(demodulation, [status(thm)], [c62,d6])). % 23.34/3.43 cnf(d10, plain, sdtpldt0(sz00,xn) = sdtasdt0(sz00,sK73), inference(demodulation, [status(thm)], [d9,d8])). % 23.34/3.43 cnf(d11, plain, xn = sdtasdt0(sz00,sK73), inference(demodulation, [status(thm)], [d10,d0])). % 23.34/3.43 cnf(d12, plain, doDivides0(xl,sdtasdt0(xl,sK73)), inference(demodulation, [status(thm)], [c63,c62])). % 23.34/3.43 cnf(d13, plain, doDivides0(sz00,sdtasdt0(xl,sK73)), inference(demodulation, [status(thm)], [d12,d6])). % 23.34/3.43 cnf(d14, plain, doDivides0(sz00,sdtasdt0(sz00,sK73)), inference(demodulation, [status(thm)], [d13,d6])). % 23.34/3.43 cnf(d15, plain, doDivides0(sz00,xn), inference(demodulation, [status(thm)], [d14,d11])). % 23.34/3.43 cnf(d16, plain, ~doDivides0(sz00,xn), inference(demodulation, [status(thm)], [c66,d6])). % 23.34/3.43 cnf(d17, plain, $false, inference(resolution, [status(thm)], [d16,d15])). % 23.34/3.43 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------