%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : RNG108+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 : 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:25:54 AM UTC 2026 % Result : Theorem 19.26s 2.89s % Output : CNFRefutation 19.26s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : RNG108+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.08/0.35 % Computer : n003.cluster.edu % 0.08/0.35 % Model : x86_64 x86_64 % 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.35 % Memory : 8046.5625MB % 0.08/0.35 % OS : Linux 6.8.0-71-generic % 0.08/0.35 % CPULimit : 300 % 0.08/0.35 % WCLimit : 300 % 0.08/0.35 % DateTime : Sat Sep 26 06:08:53 UTC 2026 % 0.08/0.35 % CPUTime : % 0.08/0.35 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 19.26/2.89 % SZS status Theorem for theBenchmark.p % 19.26/2.89 % SZS output start CNFRefutation for theBenchmark.p % 19.26/2.89 fof(mSortsC, axiom, aElement0(sz00)). % 19.26/2.89 fof(mSortsC_01, axiom, aElement0(sz10)). % 19.26/2.89 fof(mMulUnit, axiom, ! [X0] : ((aElement0(X0) => (sdtasdt0(X0,sz10) = X0 & X0 = sdtasdt0(sz10,X0))))). % 19.26/2.89 fof(mMulZero, axiom, ! [X0] : ((aElement0(X0) => (sdtasdt0(X0,sz00) = sz00 & sz00 = sdtasdt0(sz00,X0))))). % 19.26/2.89 fof(mDefPrIdeal, definition, ! [X0] : ((aElement0(X0) => ! [X1] : ((X1 = slsdtgt0(X0) <=> (aSet0(X1) & ! [X2] : ((aElementOf0(X2,X1) <=> ? [X3] : ((aElement0(X3) & sdtasdt0(X0,X3) = X2)))))))))). % 19.26/2.89 fof(m__2091, hypothesis, (aElement0(xa) & aElement0(xb))). % 19.26/2.89 fof(m__, conjecture, (aElementOf0(sz00,slsdtgt0(xa)) & (aElementOf0(xa,slsdtgt0(xa)) & (aElementOf0(sz00,slsdtgt0(xb)) & aElementOf0(xb,slsdtgt0(xb)))))). % 19.26/2.89 fof(negated_conjecture, negated_conjecture, ~((aElementOf0(sz00,slsdtgt0(xa)) & (aElementOf0(xa,slsdtgt0(xa)) & (aElementOf0(sz00,slsdtgt0(xb)) & aElementOf0(xb,slsdtgt0(xb)))))), inference(negate_conjecture, [status(cth)], [m__])). % 19.26/2.89 cnf(c0, plain, aElement0(sz00), inference(clausification, [status(esa)], [mSortsC])). % 19.26/2.89 cnf(c1, plain, aElement0(sz10), inference(clausification, [status(esa)], [mSortsC_01])). % 19.26/2.89 cnf(c13, plain, ~aElement0(X0) | sdtasdt0(X0,sz10) = X0, inference(clausification, [status(esa)], [mMulUnit])). % 19.26/2.89 cnf(c19, plain, ~aElement0(X0) | sdtasdt0(X0,sz00) = sz00, inference(clausification, [status(esa)], [mMulZero])). % 19.26/2.89 cnf(c95, plain, ~aElement0(X0) | X1 != slsdtgt0(X0) | X2(X0,X1), inference(clausification, [status(esa)], [mDefPrIdeal])). % 19.26/2.89 cnf(c100, plain, ~X0(X1,X2) | aElementOf0(X3,X2) | ~aElement0(X4) | sdtasdt0(X1,X4) != X3, inference(clausification, [status(esa)], [mDefPrIdeal])). % 19.26/2.89 cnf(c108, plain, aElement0(xa), inference(clausification, [status(esa)], [m__2091])). % 19.26/2.89 cnf(c109, plain, aElement0(xb), inference(clausification, [status(esa)], [m__2091])). % 19.26/2.89 cnf(c114, plain, ~aElementOf0(sz00,slsdtgt0(xa)) | ~aElementOf0(xa,slsdtgt0(xa)) | ~aElementOf0(sz00,slsdtgt0(xb)) | ~aElementOf0(xb,slsdtgt0(xb)), inference(clausification, [status(esa)], [negated_conjecture])). % 19.26/2.89 cnf(d0, plain, ~aElement0(X0) | 'Ts97'(X0,slsdtgt0(X0)), inference(equality_resolution, [status(thm)], [c95])). % 19.26/2.89 cnf(d1, plain, sdtasdt0(xb,sz10) = xb, inference(resolution, [status(thm)], [c13,c109])). % 19.26/2.89 cnf(d2, plain, xb != X0 | ~aElement0(sz10) | aElementOf0(X0,X1) | ~'Ts97'(xb,X1), inference(superposition, [status(thm)], [d1,c100])). % 19.26/2.89 cnf(d3, plain, xb != X0 | aElementOf0(X0,X1) | ~'Ts97'(xb,X1), inference(resolution, [status(thm)], [c1,d2])). % 19.26/2.89 cnf(d4, plain, aElementOf0(xb,X0) | ~'Ts97'(xb,X0), inference(equality_resolution, [status(thm)], [d3])). % 19.26/2.89 cnf(d5, plain, aElementOf0(xb,slsdtgt0(xb)) | ~aElement0(xb), inference(resolution, [status(thm)], [d4,d0])). % 19.26/2.89 cnf(d6, plain, aElementOf0(xb,slsdtgt0(xb)), inference(resolution, [status(thm)], [c109,d5])). % 19.26/2.89 cnf(d7, plain, sdtasdt0(xa,sz00) = sz00, inference(resolution, [status(thm)], [c19,c108])). % 19.26/2.89 cnf(d8, plain, sz00 != X0 | ~aElement0(sz00) | aElementOf0(X0,X1) | ~'Ts97'(xa,X1), inference(superposition, [status(thm)], [d7,c100])). % 19.26/2.89 cnf(d9, plain, sz00 != X0 | aElementOf0(X0,X1) | ~'Ts97'(xa,X1), inference(resolution, [status(thm)], [c0,d8])). % 19.26/2.89 cnf(d10, plain, aElementOf0(sz00,X0) | ~'Ts97'(xa,X0), inference(equality_resolution, [status(thm)], [d9])). % 19.26/2.89 cnf(d11, plain, aElementOf0(sz00,slsdtgt0(xa)) | ~aElement0(xa), inference(resolution, [status(thm)], [d10,d0])). % 19.26/2.89 cnf(d12, plain, aElementOf0(sz00,slsdtgt0(xa)), inference(resolution, [status(thm)], [c108,d11])). % 19.26/2.89 cnf(d13, plain, ~aElementOf0(sz00,slsdtgt0(xb)) | ~aElementOf0(xa,slsdtgt0(xa)) | ~aElementOf0(xb,slsdtgt0(xb)), inference(resolution, [status(thm)], [d12,c114])). % 19.26/2.89 cnf(d14, plain, sdtasdt0(xa,sz10) = xa, inference(resolution, [status(thm)], [c13,c108])). % 19.26/2.89 cnf(d15, plain, xa != X0 | ~aElement0(sz10) | aElementOf0(X0,X1) | ~'Ts97'(xa,X1), inference(superposition, [status(thm)], [d14,c100])). % 19.26/2.89 cnf(d16, plain, xa != X0 | aElementOf0(X0,X1) | ~'Ts97'(xa,X1), inference(resolution, [status(thm)], [c1,d15])). % 19.26/2.89 cnf(d17, plain, aElementOf0(xa,X0) | ~'Ts97'(xa,X0), inference(equality_resolution, [status(thm)], [d16])). % 19.26/2.89 cnf(d18, plain, aElementOf0(xa,slsdtgt0(xa)) | ~aElement0(xa), inference(resolution, [status(thm)], [d17,d0])). % 19.26/2.89 cnf(d19, plain, aElementOf0(xa,slsdtgt0(xa)), inference(resolution, [status(thm)], [c108,d18])). % 19.26/2.89 cnf(d20, plain, ~aElementOf0(sz00,slsdtgt0(xb)) | ~aElementOf0(xb,slsdtgt0(xb)), inference(resolution, [status(thm)], [d19,d13])). % 19.26/2.89 cnf(d21, plain, sdtasdt0(xb,sz00) = sz00, inference(resolution, [status(thm)], [c19,c109])). % 19.26/2.89 cnf(d22, plain, sz00 != X0 | ~aElement0(sz00) | aElementOf0(X0,X1) | ~'Ts97'(xb,X1), inference(superposition, [status(thm)], [d21,c100])). % 19.26/2.89 cnf(d23, plain, sz00 != X0 | aElementOf0(X0,X1) | ~'Ts97'(xb,X1), inference(resolution, [status(thm)], [c0,d22])). % 19.26/2.89 cnf(d24, plain, aElementOf0(sz00,X0) | ~'Ts97'(xb,X0), inference(equality_resolution, [status(thm)], [d23])). % 19.26/2.89 cnf(d25, plain, aElementOf0(sz00,slsdtgt0(xb)) | ~aElement0(xb), inference(resolution, [status(thm)], [d24,d0])). % 19.26/2.89 cnf(d26, plain, aElementOf0(sz00,slsdtgt0(xb)), inference(resolution, [status(thm)], [c109,d25])). % 19.26/2.89 cnf(d27, plain, ~aElementOf0(xb,slsdtgt0(xb)), inference(resolution, [status(thm)], [d26,d20])). % 19.26/2.89 cnf(d28, plain, $false, inference(resolution, [status(thm)], [d27,d6])). % 19.26/2.89 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------