%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : NUM476+1 : 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 : n002.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 12.37s 2.87s % Output : CNFRefutation 12.37s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM476+1 : 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.09/0.36 % Computer : n002.cluster.edu % 0.09/0.36 % Model : x86_64 x86_64 % 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.36 % Memory : 8046.5625MB % 0.09/0.36 % OS : Linux 6.8.0-71-generic % 0.09/0.36 % CPULimit : 300 % 0.09/0.36 % WCLimit : 300 % 0.09/0.36 % DateTime : Sat Sep 26 02:57:35 UTC 2026 % 0.09/0.36 % CPUTime : % 0.09/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 12.37/2.87 % SZS status Theorem for theBenchmark.p % 12.37/2.87 % SZS output start CNFRefutation for theBenchmark.p % 12.37/2.87 fof(mSortsC, axiom, aNaturalNumber0(sz00)). % 12.37/2.87 fof(mSortsB, axiom, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => aNaturalNumber0(sdtpldt0(X0,X1))))). % 12.37/2.87 fof(m_AddZero, axiom, ! [X0] : ((aNaturalNumber0(X0) => (sdtpldt0(X0,sz00) = X0 & X0 = sdtpldt0(sz00,X0))))). % 12.37/2.87 fof(m_MulZero, axiom, ! [X0] : ((aNaturalNumber0(X0) => (sdtasdt0(X0,sz00) = sz00 & sz00 = sdtasdt0(sz00,X0))))). % 12.37/2.87 fof(mDefDiff, definition, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => (sdtlseqdt0(X0,X1) => ! [X2] : ((X2 = sdtmndt0(X1,X0) <=> (aNaturalNumber0(X2) & sdtpldt0(X0,X2) = X1))))))). % 12.37/2.87 fof(mDefDiv, definition, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => (doDivides0(X0,X1) <=> ? [X2] : ((aNaturalNumber0(X2) & X1 = sdtasdt0(X0,X2))))))). % 12.37/2.87 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)))))))). % 12.37/2.87 fof(m__1324, hypothesis, (aNaturalNumber0(xl) & (aNaturalNumber0(xm) & aNaturalNumber0(xn)))). % 12.37/2.87 fof(m__1324_04, hypothesis, (doDivides0(xl,xm) & doDivides0(xl,sdtpldt0(xm,xn)))). % 12.37/2.87 fof(m__, conjecture, ((xl != sz00 => ? [X0] : ((X0 = sdtsldt0(xm,xl) & ? [X1] : ((X1 = sdtsldt0(sdtpldt0(xm,xn),xl) & (sdtlseqdt0(X0,X1) & ? [X2] : ((X2 = sdtmndt0(X1,X0) & (sdtpldt0(sdtasdt0(xl,X0),sdtasdt0(xl,X2)) = sdtpldt0(sdtasdt0(xl,X0),xn) & xn = sdtasdt0(xl,X2)))))))))) => doDivides0(xl,xn))). % 12.37/2.87 fof(negated_conjecture, negated_conjecture, ~(((xl != sz00 => ? [X0] : ((X0 = sdtsldt0(xm,xl) & ? [X1] : ((X1 = sdtsldt0(sdtpldt0(xm,xn),xl) & (sdtlseqdt0(X0,X1) & ? [X2] : ((X2 = sdtmndt0(X1,X0) & (sdtpldt0(sdtasdt0(xl,X0),sdtasdt0(xl,X2)) = sdtpldt0(sdtasdt0(xl,X0),xn) & xn = sdtasdt0(xl,X2)))))))))) => doDivides0(xl,xn))), inference(negate_conjecture, [status(cth)], [m__])). % 12.37/2.87 cnf(c0, plain, aNaturalNumber0(sz00), inference(clausification, [status(esa)], [mSortsC])). % 12.37/2.87 cnf(c3, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | aNaturalNumber0(sdtpldt0(X0,X1)), inference(clausification, [status(esa)], [mSortsB])). % 12.37/2.87 cnf(c8, plain, ~aNaturalNumber0(X0) | X0 = sdtpldt0(sz00,X0), inference(clausification, [status(esa)], [m_AddZero])). % 12.37/2.87 cnf(c14, plain, ~aNaturalNumber0(X0) | sz00 = sdtasdt0(sz00,X0), inference(clausification, [status(esa)], [m_MulZero])). % 12.37/2.87 cnf(c27, plain, ~aNaturalNumber0(X0) | X1 != sdtmndt0(X2,X0) | ~aNaturalNumber0(X2) | ~sdtlseqdt0(X0,X2) | aNaturalNumber0(X1), inference(clausification, [status(esa)], [mDefDiff])). % 12.37/2.87 cnf(c47, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | ~doDivides0(X0,X1) | aNaturalNumber0(sK61(X0,X1)), inference(clausification, [status(esa)], [mDefDiv])). % 12.37/2.87 cnf(c48, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | ~doDivides0(X0,X1) | X1 = sdtasdt0(X0,sK61(X0,X1)), inference(clausification, [status(esa)], [mDefDiv])). % 12.37/2.87 cnf(c49, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | doDivides0(X0,X1) | ~aNaturalNumber0(X2) | X1 != sdtasdt0(X0,X2), inference(clausification, [status(esa)], [mDefDiv])). % 12.37/2.87 cnf(c50, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | X2 != sdtsldt0(X1,X0) | aNaturalNumber0(X2) | ~doDivides0(X0,X1) | X0 = sz00, inference(clausification, [status(esa)], [mDefQuot])). % 12.37/2.87 cnf(c55, plain, aNaturalNumber0(xl), inference(clausification, [status(esa)], [m__1324])). % 12.37/2.87 cnf(c56, plain, aNaturalNumber0(xm), inference(clausification, [status(esa)], [m__1324])). % 12.37/2.87 cnf(c57, plain, aNaturalNumber0(xn), inference(clausification, [status(esa)], [m__1324])). % 12.37/2.87 cnf(c58, plain, doDivides0(xl,xm), inference(clausification, [status(esa)], [m__1324_04])). % 12.37/2.87 cnf(c59, plain, doDivides0(xl,sdtpldt0(xm,xn)), inference(clausification, [status(esa)], [m__1324_04])). % 12.37/2.87 cnf(c60, plain, xl = sz00 | X0, inference(clausification, [status(esa)], [negated_conjecture])). % 12.37/2.87 cnf(c61, plain, ~doDivides0(xl,xn), inference(clausification, [status(esa)], [negated_conjecture])). % 12.37/2.87 cnf(c62, plain, ~X0 | sK73 = sdtsldt0(xm,xl), inference(clausification, [status(esa)], [negated_conjecture])). % 12.37/2.87 cnf(c63, plain, ~X0 | sK74 = sdtsldt0(sdtpldt0(xm,xn),xl), inference(clausification, [status(esa)], [negated_conjecture])). % 12.37/2.87 cnf(c64, plain, ~X0 | sdtlseqdt0(sK73,sK74), inference(clausification, [status(esa)], [negated_conjecture])). % 12.37/2.87 cnf(c65, plain, ~X0 | sK75 = sdtmndt0(sK74,sK73), inference(clausification, [status(esa)], [negated_conjecture])). % 12.37/2.87 cnf(c67, plain, ~X0 | xn = sdtasdt0(xl,sK75), inference(clausification, [status(esa)], [negated_conjecture])). % 12.37/2.87 cnf(d0, plain, xn = sdtpldt0(sz00,xn), inference(resolution, [status(thm)], [c57,c8])). % 12.37/2.87 cnf(d1, plain, xn = sdtasdt0(xl,sK75) | xl = sz00, inference(resolution, [status(thm)], [c67,c60])). % 12.37/2.87 cnf(d2, plain, X0 != xn | ~aNaturalNumber0(sK75) | ~aNaturalNumber0(X0) | ~aNaturalNumber0(xl) | doDivides0(xl,X0) | xl = sz00, inference(superposition, [status(thm)], [d1,c49])). % 12.37/2.87 cnf(d3, plain, X0 != xn | xl = sz00 | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sK75) | doDivides0(xl,X0), inference(resolution, [status(thm)], [c55,d2])). % 12.37/2.87 cnf(d4, plain, xl = sz00 | ~aNaturalNumber0(xn) | ~aNaturalNumber0(sK75) | doDivides0(xl,xn), inference(equality_resolution, [status(thm)], [d3])). % 12.37/2.87 cnf(d5, plain, xl = sz00 | ~aNaturalNumber0(xn) | ~aNaturalNumber0(sK75), inference(resolution, [status(thm)], [c61,d4])). % 12.37/2.87 cnf(d6, plain, xl = sz00 | ~aNaturalNumber0(sK75), inference(resolution, [status(thm)], [c57,d5])). % 12.37/2.87 cnf(d7, plain, sK73 = sdtsldt0(xm,xl) | xl = sz00, inference(resolution, [status(thm)], [c62,c60])). % 12.37/2.87 cnf(d8, plain, X0 != sK73 | xl = sz00 | ~aNaturalNumber0(xl) | aNaturalNumber0(X0) | ~aNaturalNumber0(xm) | ~doDivides0(xl,xm) | xl = sz00, inference(superposition, [status(thm)], [d7,c50])). % 12.37/2.87 cnf(d9, plain, X0 != sK73 | xl = sz00 | aNaturalNumber0(X0) | ~aNaturalNumber0(xm) | ~doDivides0(xl,xm), inference(resolution, [status(thm)], [c55,d8])). % 12.37/2.87 cnf(d10, plain, X0 != sK73 | xl = sz00 | aNaturalNumber0(X0) | ~doDivides0(xl,xm), inference(resolution, [status(thm)], [c56,d9])). % 12.37/2.87 cnf(d11, plain, xl = sz00 | aNaturalNumber0(sK73) | ~doDivides0(xl,xm), inference(equality_resolution, [status(thm)], [d10])). % 12.37/2.87 cnf(d12, plain, xl = sz00 | aNaturalNumber0(sK73), inference(resolution, [status(thm)], [c58,d11])). % 12.37/2.87 cnf(d13, plain, sK75 = sdtmndt0(sK74,sK73) | xl = sz00, inference(resolution, [status(thm)], [c65,c60])). % 12.37/2.87 cnf(d14, plain, X0 != sK75 | aNaturalNumber0(X0) | ~aNaturalNumber0(sK74) | ~aNaturalNumber0(sK73) | ~sdtlseqdt0(sK73,sK74) | xl = sz00, inference(superposition, [status(thm)], [d13,c27])). % 12.37/2.87 cnf(d15, plain, xl = sz00 | aNaturalNumber0(sK75) | ~aNaturalNumber0(sK73) | ~aNaturalNumber0(sK74) | ~sdtlseqdt0(sK73,sK74), inference(equality_resolution, [status(thm)], [d14])). % 12.37/2.87 cnf(d16, plain, xl = sz00 | ~aNaturalNumber0(sK73) | ~aNaturalNumber0(sK74) | aNaturalNumber0(sK75) | ~'Ts72', inference(resolution, [status(thm)], [d15,c64])). % 12.37/2.87 cnf(d17, plain, sK74 = sdtsldt0(sdtpldt0(xm,xn),xl) | xl = sz00, inference(resolution, [status(thm)], [c63,c60])). % 12.37/2.87 cnf(d18, plain, X0 != sK74 | xl = sz00 | ~aNaturalNumber0(xl) | aNaturalNumber0(X0) | ~aNaturalNumber0(sdtpldt0(xm,xn)) | ~doDivides0(xl,sdtpldt0(xm,xn)) | xl = sz00, inference(superposition, [status(thm)], [d17,c50])). % 12.37/2.87 cnf(d19, plain, X0 != sK74 | xl = sz00 | aNaturalNumber0(X0) | ~aNaturalNumber0(sdtpldt0(xm,xn)) | ~doDivides0(xl,sdtpldt0(xm,xn)), inference(resolution, [status(thm)], [c55,d18])). % 12.37/2.87 cnf(d20, plain, X0 != sK74 | xl = sz00 | aNaturalNumber0(X0) | ~aNaturalNumber0(sdtpldt0(xm,xn)), inference(resolution, [status(thm)], [c59,d19])). % 12.37/2.87 cnf(d21, plain, xl = sz00 | aNaturalNumber0(sK74) | ~aNaturalNumber0(sdtpldt0(xm,xn)), inference(equality_resolution, [status(thm)], [d20])). % 12.37/2.87 cnf(d22, plain, xl = sz00 | aNaturalNumber0(sK74) | ~aNaturalNumber0(xn) | ~aNaturalNumber0(xm), inference(resolution, [status(thm)], [d21,c3])). % 12.37/2.87 cnf(d23, plain, xl = sz00 | ~aNaturalNumber0(xn) | aNaturalNumber0(sK74), inference(resolution, [status(thm)], [c56,d22])). % 12.37/2.87 cnf(d24, plain, xl = sz00 | aNaturalNumber0(sK74), inference(resolution, [status(thm)], [c57,d23])). % 12.37/2.87 cnf(d25, plain, xl = sz00 | xl = sz00 | ~aNaturalNumber0(sK73) | aNaturalNumber0(sK75) | ~'Ts72', inference(resolution, [status(thm)], [d24,d16])). % 12.37/2.87 cnf(d26, plain, xl = sz00 | aNaturalNumber0(sK75) | ~'Ts72' | xl = sz00, inference(resolution, [status(thm)], [d25,d12])). % 12.37/2.87 cnf(d27, plain, xl = sz00 | ~'Ts72' | xl = sz00, inference(resolution, [status(thm)], [d26,d6])). % 12.37/2.87 cnf(d28, plain, xl = sz00 | xl = sz00, inference(resolution, [status(thm)], [d27,c60])). % 12.37/2.87 cnf(d29, plain, xm = sdtasdt0(xl,sK61(xl,xm)) | ~aNaturalNumber0(xm) | ~aNaturalNumber0(xl), inference(resolution, [status(thm)], [c58,c48])). % 12.37/2.87 cnf(d30, plain, xm = sdtasdt0(xl,sK61(xl,xm)) | ~aNaturalNumber0(xm), inference(resolution, [status(thm)], [c55,d29])). % 12.37/2.87 cnf(d31, plain, xm = sdtasdt0(xl,sK61(xl,xm)), inference(resolution, [status(thm)], [c56,d30])). % 12.37/2.87 cnf(d32, plain, xm = sdtasdt0(sz00,sK61(xl,xm)), inference(demodulation, [status(thm)], [d31,d28])). % 12.37/2.87 cnf(d33, plain, xm = sdtasdt0(sz00,sK61(sz00,xm)), inference(demodulation, [status(thm)], [d32,d28])). % 12.37/2.87 cnf(d34, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | ~doDivides0(X1,X0) | sz00 = sdtasdt0(sz00,sK61(X1,X0)), inference(resolution, [status(thm)], [c47,c14])). % 12.37/2.87 cnf(d35, plain, doDivides0(sz00,xm), inference(demodulation, [status(thm)], [c58,d28])). % 12.37/2.87 cnf(d36, plain, sz00 = sdtasdt0(sz00,sK61(sz00,xm)) | ~aNaturalNumber0(sz00) | ~aNaturalNumber0(xm), inference(resolution, [status(thm)], [d35,d34])). % 12.37/2.87 cnf(d37, plain, sz00 = xm | ~aNaturalNumber0(sz00) | ~aNaturalNumber0(xm), inference(demodulation, [status(thm)], [d36,d33])). % 12.37/2.87 cnf(d38, plain, sz00 = xm | ~aNaturalNumber0(xm), inference(resolution, [status(thm)], [c0,d37])). % 12.37/2.87 cnf(d39, plain, sz00 = xm, inference(resolution, [status(thm)], [c56,d38])). % 12.37/2.87 cnf(d40, plain, doDivides0(sz00,sdtpldt0(xm,xn)), inference(demodulation, [status(thm)], [c59,d28])). % 12.37/2.87 cnf(d41, plain, doDivides0(sz00,sdtpldt0(sz00,xn)), inference(demodulation, [status(thm)], [d40,d39])). % 12.37/2.87 cnf(d42, plain, doDivides0(sz00,xn), inference(demodulation, [status(thm)], [d41,d0])). % 12.37/2.87 cnf(d43, plain, ~doDivides0(sz00,xn), inference(demodulation, [status(thm)], [c61,d28])). % 12.37/2.87 cnf(d44, plain, $false, inference(resolution, [status(thm)], [d43,d42])). % 12.37/2.87 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------