%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : RNG108+4 : 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 : n008.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 14.80s 3.35s % Output : CNFRefutation 14.80s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : RNG108+4 : 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.36 % Computer : n008.cluster.edu % 0.10/0.36 % Model : x86_64 x86_64 % 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.36 % Memory : 8046.5625MB % 0.10/0.36 % OS : Linux 6.8.0-71-generic % 0.10/0.36 % CPULimit : 300 % 0.10/0.36 % WCLimit : 300 % 0.10/0.36 % DateTime : Sat Sep 26 06:07:54 UTC 2026 % 0.10/0.36 % CPUTime : % 0.10/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 14.80/3.35 % SZS status Theorem for theBenchmark.p % 14.80/3.35 % SZS output start CNFRefutation for theBenchmark.p % 14.80/3.35 fof(mSortsC, axiom, aElement0(sz00)). % 14.80/3.35 fof(mSortsC_01, axiom, aElement0(sz10)). % 14.80/3.35 fof(mMulUnit, axiom, ! [X0] : ((aElement0(X0) => (sdtasdt0(X0,sz10) = X0 & X0 = sdtasdt0(sz10,X0))))). % 14.80/3.35 fof(mMulZero, axiom, ! [X0] : ((aElement0(X0) => (sdtasdt0(X0,sz00) = sz00 & sz00 = sdtasdt0(sz00,X0))))). % 14.80/3.35 fof(m__2091, hypothesis, (aElement0(xa) & aElement0(xb))). % 14.80/3.35 fof(m__, conjecture, ((? [X0] : ((aElement0(X0) & sdtasdt0(xa,X0) = sz00)) | aElementOf0(sz00,slsdtgt0(xa))) & ((? [X0] : ((aElement0(X0) & sdtasdt0(xa,X0) = xa)) | aElementOf0(xa,slsdtgt0(xa))) & ((? [X0] : ((aElement0(X0) & sdtasdt0(xb,X0) = sz00)) | aElementOf0(sz00,slsdtgt0(xb))) & (? [X0] : ((aElement0(X0) & sdtasdt0(xb,X0) = xb)) | aElementOf0(xb,slsdtgt0(xb))))))). % 14.80/3.35 fof(negated_conjecture, negated_conjecture, ~(((? [X0] : ((aElement0(X0) & sdtasdt0(xa,X0) = sz00)) | aElementOf0(sz00,slsdtgt0(xa))) & ((? [X0] : ((aElement0(X0) & sdtasdt0(xa,X0) = xa)) | aElementOf0(xa,slsdtgt0(xa))) & ((? [X0] : ((aElement0(X0) & sdtasdt0(xb,X0) = sz00)) | aElementOf0(sz00,slsdtgt0(xb))) & (? [X0] : ((aElement0(X0) & sdtasdt0(xb,X0) = xb)) | aElementOf0(xb,slsdtgt0(xb))))))), inference(negate_conjecture, [status(cth)], [m__])). % 14.80/3.35 cnf(c0, plain, aElement0(sz00), inference(clausification, [status(esa)], [mSortsC])). % 14.80/3.35 cnf(c1, plain, aElement0(sz10), inference(clausification, [status(esa)], [mSortsC_01])). % 14.80/3.35 cnf(c13, plain, ~aElement0(X0) | sdtasdt0(X0,sz10) = X0, inference(clausification, [status(esa)], [mMulUnit])). % 14.80/3.35 cnf(c19, plain, ~aElement0(X0) | sdtasdt0(X0,sz00) = sz00, inference(clausification, [status(esa)], [mMulZero])). % 14.80/3.35 cnf(c108, plain, aElement0(xa), inference(clausification, [status(esa)], [m__2091])). % 14.80/3.35 cnf(c109, plain, aElement0(xb), inference(clausification, [status(esa)], [m__2091])). % 14.80/3.35 cnf(c146, plain, ~aElement0(X0) | sdtasdt0(xa,X1) != sz00 | sdtasdt0(xa,X0) != xa | ~X2 | ~aElement0(X1), inference(clausification, [status(esa)], [negated_conjecture])). % 14.80/3.35 cnf(c150, plain, sdtasdt0(xb,X0) != sz00 | sdtasdt0(xb,X1) != xb | ~aElement0(X0) | ~aElement0(X1) | X2, inference(clausification, [status(esa)], [negated_conjecture])). % 14.80/3.35 cnf(d0, plain, sdtasdt0(xb,sz10) = xb, inference(resolution, [status(thm)], [c13,c109])). % 14.80/3.35 cnf(d1, plain, xb != xb | sdtasdt0(xb,X0) != sz00 | ~aElement0(X0) | ~aElement0(sz10) | 'Ts129', inference(superposition, [status(thm)], [d0,c150])). % 14.80/3.35 cnf(d2, plain, sdtasdt0(xb,X0) != sz00 | xb != xb | ~aElement0(X0) | 'Ts129', inference(resolution, [status(thm)], [c1,d1])). % 14.80/3.35 cnf(d3, plain, sdtasdt0(xa,sz00) = sz00, inference(resolution, [status(thm)], [c19,c108])). % 14.80/3.35 cnf(d4, plain, sz00 != sz00 | sdtasdt0(xa,X0) != xa | ~aElement0(X0) | ~aElement0(sz00) | ~'Ts129', inference(superposition, [status(thm)], [d3,c146])). % 14.80/3.35 cnf(d5, plain, sz00 != sz00 | sdtasdt0(xa,X0) != xa | ~aElement0(X0) | ~'Ts129', inference(resolution, [status(thm)], [c0,d4])). % 14.80/3.35 cnf(d6, plain, sdtasdt0(xa,sz10) = xa, inference(resolution, [status(thm)], [c13,c108])). % 14.80/3.35 cnf(d7, plain, xa != xa | sz00 != sz00 | ~aElement0(sz10) | ~'Ts129', inference(superposition, [status(thm)], [d6,d5])). % 14.80/3.35 cnf(d8, plain, sz00 != sz00 | xa != xa | ~'Ts129', inference(resolution, [status(thm)], [c1,d7])). % 14.80/3.35 cnf(d9, plain, sz00 != sz00 | ~'Ts129', inference(equality_resolution, [status(thm)], [d8])). % 14.80/3.35 cnf(d10, plain, ~'Ts129', inference(equality_resolution, [status(thm)], [d9])). % 14.80/3.35 cnf(d11, plain, sdtasdt0(xb,X0) != sz00 | xb != xb | ~aElement0(X0), inference(resolution, [status(thm)], [d10,d2])). % 14.80/3.35 cnf(d12, plain, sdtasdt0(xb,sz00) = sz00, inference(resolution, [status(thm)], [c19,c109])). % 14.80/3.35 cnf(d13, plain, sz00 != sz00 | xb != xb | ~aElement0(sz00), inference(superposition, [status(thm)], [d12,d11])). % 14.80/3.35 cnf(d14, plain, sz00 != sz00 | xb != xb, inference(resolution, [status(thm)], [c0,d13])). % 14.80/3.35 cnf(d15, plain, sz00 != sz00, inference(equality_resolution, [status(thm)], [d14])). % 14.80/3.35 cnf(d16, plain, $false, inference(equality_resolution, [status(thm)], [d15])). % 14.80/3.35 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------