%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : RNG046+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 : n010.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:25:42 AM UTC 2026 % Result : Theorem 3.31s 13.86s % Output : CNFRefutation 3.31s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : RNG046+1 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.03 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.11/10.58 % Computer : n010.cluster.edu % 0.11/10.58 % Model : x86_64 x86_64 % 0.11/10.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/10.58 % Memory : 8046.5625MB % 0.11/10.58 % OS : Linux 6.8.0-71-generic % 0.11/10.58 % CPULimit : 300 % 0.11/10.58 % WCLimit : 300 % 0.11/10.58 % DateTime : Sat Sep 26 05:52:28 UTC 2026 % 0.11/10.58 % CPUTime : % 0.11/10.58 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 3.31/13.86 % SZS status Theorem for theBenchmark.p % 3.31/13.86 % SZS output start CNFRefutation for theBenchmark.p % 3.31/13.86 fof(mNegSc, axiom, ! [X0] : ((aScalar0(X0) => aScalar0(smndt0(X0))))). % 3.31/13.86 fof(mScZero, axiom, ! [X0] : ((aScalar0(X0) => (sdtpldt0(X0,sz0z00) = X0 & (sdtpldt0(sz0z00,X0) = X0 & (sdtasdt0(X0,sz0z00) = sz0z00 & (sdtasdt0(sz0z00,X0) = sz0z00 & (sdtpldt0(X0,smndt0(X0)) = sz0z00 & (sdtpldt0(smndt0(X0),X0) = sz0z00 & (smndt0(smndt0(X0)) = X0 & smndt0(sz0z00) = sz0z00)))))))))). % 3.31/13.86 fof(mMNeg, axiom, ! [X0] : ! [X1] : (((aScalar0(X0) & aScalar0(X1)) => (sdtasdt0(X0,smndt0(X1)) = smndt0(sdtasdt0(X0,X1)) & sdtasdt0(smndt0(X0),X1) = smndt0(sdtasdt0(X0,X1)))))). % 3.31/13.86 fof(m__799, hypothesis, (aScalar0(xx) & aScalar0(xy))). % 3.31/13.86 fof(m__, conjecture, sdtasdt0(smndt0(xx),smndt0(xy)) = sdtasdt0(xx,xy)). % 3.31/13.86 fof(negated_conjecture, negated_conjecture, sdtasdt0(smndt0(xx),smndt0(xy)) != sdtasdt0(xx,xy), inference(negate_conjecture, [status(cth)], [m__])). % 3.31/13.86 cnf(c10, plain, ~aScalar0(X0) | aScalar0(smndt0(X0)), inference(clausification, [status(esa)], [mNegSc])). % 3.31/13.86 cnf(c11, plain, ~aScalar0(X0) | X1(X0), inference(clausification, [status(esa)], [mScZero])). % 3.31/13.86 cnf(c18, plain, ~X0(X1) | smndt0(smndt0(X1)) = X1, inference(clausification, [status(esa)], [mScZero])). % 3.31/13.86 cnf(c27, plain, ~aScalar0(X0) | ~aScalar0(X1) | sdtasdt0(X0,smndt0(X1)) = smndt0(sdtasdt0(X0,X1)), inference(clausification, [status(esa)], [mMNeg])). % 3.31/13.86 cnf(c28, plain, ~aScalar0(X0) | ~aScalar0(X1) | sdtasdt0(smndt0(X0),X1) = smndt0(sdtasdt0(X0,X1)), inference(clausification, [status(esa)], [mMNeg])). % 3.31/13.86 cnf(c29, plain, aScalar0(xx), inference(clausification, [status(esa)], [m__799])). % 3.31/13.86 cnf(c30, plain, aScalar0(xy), inference(clausification, [status(esa)], [m__799])). % 3.31/13.86 cnf(c31, plain, sdtasdt0(smndt0(xx),smndt0(xy)) != sdtasdt0(xx,xy), inference(clausification, [status(esa)], [negated_conjecture])). % 3.31/13.86 cnf(d0, plain, sdtasdt0(xx,smndt0(X0)) = smndt0(sdtasdt0(xx,X0)) | ~aScalar0(X0), inference(resolution, [status(thm)], [c27,c29])). % 3.31/13.86 cnf(d1, plain, sdtasdt0(xx,smndt0(xy)) = smndt0(sdtasdt0(xx,xy)), inference(resolution, [status(thm)], [d0,c30])). % 3.31/13.86 cnf(d2, plain, sdtasdt0(smndt0(xx),X0) = smndt0(sdtasdt0(xx,X0)) | ~aScalar0(X0), inference(resolution, [status(thm)], [c28,c29])). % 3.31/13.86 cnf(d3, plain, sdtasdt0(smndt0(xx),xy) = smndt0(sdtasdt0(xx,xy)), inference(resolution, [status(thm)], [d2,c30])). % 3.31/13.86 cnf(d4, plain, sdtasdt0(smndt0(xx),xy) = sdtasdt0(xx,smndt0(xy)), inference(demodulation, [status(thm)], [d3,d1])). % 3.31/13.86 cnf(d5, plain, 'Ts15'(xx), inference(resolution, [status(thm)], [c11,c29])). % 3.31/13.86 cnf(d6, plain, smndt0(smndt0(xx)) = xx, inference(resolution, [status(thm)], [c18,d5])). % 3.31/13.86 cnf(d7, plain, sdtasdt0(smndt0(smndt0(X0)),X1) = smndt0(sdtasdt0(smndt0(X0),X1)) | ~aScalar0(X1) | ~aScalar0(X0), inference(resolution, [status(thm)], [c28,c10])). % 3.31/13.86 cnf(d8, plain, sdtasdt0(smndt0(smndt0(xx)),X0) = smndt0(sdtasdt0(smndt0(xx),X0)) | ~aScalar0(X0), inference(resolution, [status(thm)], [d7,c29])). % 3.31/13.86 cnf(d9, plain, sdtasdt0(xx,X0) = smndt0(sdtasdt0(smndt0(xx),X0)) | ~aScalar0(X0), inference(demodulation, [status(thm)], [d8,d6])). % 3.31/13.86 cnf(d10, plain, sdtasdt0(xx,xy) = smndt0(sdtasdt0(smndt0(xx),xy)), inference(resolution, [status(thm)], [d9,c30])). % 3.31/13.86 cnf(d11, plain, sdtasdt0(xx,xy) = smndt0(sdtasdt0(xx,smndt0(xy))), inference(demodulation, [status(thm)], [d10,d4])). % 3.31/13.86 cnf(d12, plain, sdtasdt0(smndt0(X0),smndt0(X1)) = smndt0(sdtasdt0(smndt0(X0),X1)) | ~aScalar0(X1) | ~aScalar0(X0), inference(resolution, [status(thm)], [c27,c10])). % 3.31/13.86 cnf(d13, plain, sdtasdt0(smndt0(xx),smndt0(X0)) = smndt0(sdtasdt0(smndt0(xx),X0)) | ~aScalar0(X0), inference(resolution, [status(thm)], [d12,c29])). % 3.31/13.86 cnf(d14, plain, sdtasdt0(smndt0(xx),smndt0(xy)) = smndt0(sdtasdt0(smndt0(xx),xy)), inference(resolution, [status(thm)], [d13,c30])). % 3.31/13.86 cnf(d15, plain, sdtasdt0(smndt0(xx),smndt0(xy)) = smndt0(sdtasdt0(xx,smndt0(xy))), inference(demodulation, [status(thm)], [d14,d4])). % 3.31/13.86 cnf(d16, plain, sdtasdt0(smndt0(xx),smndt0(xy)) = sdtasdt0(xx,xy), inference(demodulation, [status(thm)], [d15,d11])). % 3.31/13.86 cnf(d17, plain, $false, inference(resolution, [status(thm)], [c31,d16])). % 3.31/13.86 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------