%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : RNG112+1 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/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:25:55 AM UTC 2026 % Result : Theorem 54.46s 7.97s % Output : CNFRefutation 54.46s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : RNG112+1 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.09/0.36 % Computer : n007.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 06:06:09 UTC 2026 % 0.12/0.36 % CPUTime : % 0.12/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 54.46/7.97 % SZS status Theorem for theBenchmark.p % 54.46/7.97 % SZS output start CNFRefutation for theBenchmark.p % 54.46/7.97 fof(mSortsC, axiom, aElement0(sz00)). % 54.46/7.97 fof(mSortsC_01, axiom, aElement0(sz10)). % 54.46/7.97 fof(mSortsU, axiom, ! [X0] : ((aElement0(X0) => aElement0(smndt0(X0))))). % 54.46/7.97 fof(mSortsB_02, axiom, ! [X0] : ! [X1] : (((aElement0(X0) & aElement0(X1)) => aElement0(sdtasdt0(X0,X1))))). % 54.46/7.97 fof(mAddZero, axiom, ! [X0] : ((aElement0(X0) => (sdtpldt0(X0,sz00) = X0 & X0 = sdtpldt0(sz00,X0))))). % 54.46/7.97 fof(mAddInvr, axiom, ! [X0] : ((aElement0(X0) => (sdtpldt0(X0,smndt0(X0)) = sz00 & sz00 = sdtpldt0(smndt0(X0),X0))))). % 54.46/7.97 fof(mMulMnOne, axiom, ! [X0] : ((aElement0(X0) => (sdtasdt0(smndt0(sz10),X0) = smndt0(X0) & smndt0(X0) = sdtasdt0(X0,smndt0(sz10)))))). % 54.46/7.97 fof(mMulZero, axiom, ! [X0] : ((aElement0(X0) => (sdtasdt0(X0,sz00) = sz00 & sz00 = sdtasdt0(sz00,X0))))). % 54.46/7.97 fof(mEOfElem, axiom, ! [X0] : ((aSet0(X0) => ! [X1] : ((aElementOf0(X1,X0) => aElement0(X1)))))). % 54.46/7.97 fof(mDefIdeal, definition, ! [X0] : ((aIdeal0(X0) <=> (aSet0(X0) & ! [X1] : ((aElementOf0(X1,X0) => (! [X2] : ((aElementOf0(X2,X0) => aElementOf0(sdtpldt0(X1,X2),X0))) & ! [X2] : ((aElement0(X2) => aElementOf0(sdtasdt0(X2,X1),X0)))))))))). % 54.46/7.97 fof(mDefDiv, definition, ! [X0] : ! [X1] : (((aElement0(X0) & aElement0(X1)) => (doDivides0(X0,X1) <=> ? [X2] : ((aElement0(X2) & sdtasdt0(X0,X2) = X1)))))). % 54.46/7.97 fof(m__2174, hypothesis, (aIdeal0(xI) & xI = sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)))). % 54.46/7.97 fof(m__2228, hypothesis, ? [X0] : ((aElementOf0(X0,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))) & X0 != sz00))). % 54.46/7.97 fof(m__2351, hypothesis, ! [X0] : (((aElementOf0(X0,xI) & X0 != sz00) => ? [X1] : ((aElementOf0(X1,xI) & (X1 != sz00 & ! [X2] : (((aElementOf0(X2,xI) & X2 != sz00) => ~iLess0(sbrdtbr0(X2),sbrdtbr0(X1)))))))))). % 54.46/7.97 fof(m__, conjecture, ? [X0] : ((aElementOf0(X0,xI) & (X0 != sz00 & ! [X1] : (((aElementOf0(X1,xI) & X1 != sz00) => ~iLess0(sbrdtbr0(X1),sbrdtbr0(X0)))))))). % 54.46/7.97 fof(negated_conjecture, negated_conjecture, ~? [X0] : ((aElementOf0(X0,xI) & (X0 != sz00 & ! [X1] : (((aElementOf0(X1,xI) & X1 != sz00) => ~iLess0(sbrdtbr0(X1),sbrdtbr0(X0))))))), inference(negate_conjecture, [status(cth)], [m__])). % 54.46/7.97 cnf(c0, plain, aElement0(sz00), inference(clausification, [status(esa)], [mSortsC])). % 54.46/7.97 cnf(c1, plain, aElement0(sz10), inference(clausification, [status(esa)], [mSortsC_01])). % 54.46/7.97 cnf(c2, plain, ~aElement0(X0) | aElement0(smndt0(X0)), inference(clausification, [status(esa)], [mSortsU])). % 54.46/7.97 cnf(c4, plain, ~aElement0(X0) | ~aElement0(X1) | aElement0(sdtasdt0(X0,X1)), inference(clausification, [status(esa)], [mSortsB_02])). % 54.46/7.97 cnf(c8, plain, ~aElement0(X0) | X0 = sdtpldt0(sz00,X0), inference(clausification, [status(esa)], [mAddZero])). % 54.46/7.97 cnf(c9, plain, ~aElement0(X0) | sdtpldt0(X0,smndt0(X0)) = sz00, inference(clausification, [status(esa)], [mAddInvr])). % 54.46/7.97 cnf(c17, plain, ~aElement0(X0) | sdtasdt0(smndt0(sz10),X0) = smndt0(X0), inference(clausification, [status(esa)], [mMulMnOne])). % 54.46/7.97 cnf(c18, plain, ~aElement0(X0) | smndt0(X0) = sdtasdt0(X0,smndt0(sz10)), inference(clausification, [status(esa)], [mMulMnOne])). % 54.46/7.97 cnf(c20, plain, ~aElement0(X0) | sz00 = sdtasdt0(sz00,X0), inference(clausification, [status(esa)], [mMulZero])). % 54.46/7.97 cnf(c23, plain, ~aSet0(X0) | ~aElementOf0(X1,X0) | aElement0(X1), inference(clausification, [status(esa)], [mEOfElem])). % 54.46/7.97 cnf(c55, plain, ~aIdeal0(X0) | aSet0(X0), inference(clausification, [status(esa)], [mDefIdeal])). % 54.46/7.97 cnf(c56, plain, ~aIdeal0(X0) | X1(X0), inference(clausification, [status(esa)], [mDefIdeal])). % 54.46/7.97 cnf(c59, plain, ~X0(X1) | ~aElementOf0(X2,X1) | ~aElement0(X3) | aElementOf0(sdtasdt0(X3,X2),X1), inference(clausification, [status(esa)], [mDefIdeal])). % 54.46/7.97 cnf(c79, plain, ~aElement0(X0) | ~aElement0(X1) | ~doDivides0(X0,X1) | aElement0(sK85(X0,X1)), inference(clausification, [status(esa)], [mDefDiv])). % 54.46/7.97 cnf(c80, plain, ~aElement0(X0) | ~aElement0(X1) | ~doDivides0(X0,X1) | sdtasdt0(X0,sK85(X0,X1)) = X1, inference(clausification, [status(esa)], [mDefDiv])). % 54.46/7.97 cnf(c81, plain, doDivides0(X0,X1) | ~aElement0(X1) | sdtasdt0(X0,X2) != X1 | ~aElement0(X2) | ~aElement0(X0), inference(clausification, [status(esa)], [mDefDiv])). % 54.46/7.97 cnf(c112, plain, aIdeal0(xI), inference(clausification, [status(esa)], [m__2174])). % 54.46/7.97 cnf(c113, plain, xI = sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)), inference(clausification, [status(esa)], [m__2174])). % 54.46/7.97 cnf(c118, plain, aElementOf0(sK107,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))), inference(clausification, [status(esa)], [m__2228])). % 54.46/7.97 cnf(c119, plain, sK107 != sz00, inference(clausification, [status(esa)], [m__2228])). % 54.46/7.97 cnf(c120, plain, ~aElementOf0(X0,xI) | X0 = sz00 | aElementOf0(sK109,xI), inference(clausification, [status(esa)], [m__2351])). % 54.46/7.97 cnf(c121, plain, ~aElementOf0(X0,xI) | X0 = sz00 | sK109 != sz00, inference(clausification, [status(esa)], [m__2351])). % 54.46/7.97 cnf(c122, plain, ~aElementOf0(X0,xI) | ~iLess0(sbrdtbr0(X1),sbrdtbr0(sK109)) | ~aElementOf0(X1,xI) | X0 = sz00 | X1 = sz00, inference(clausification, [status(esa)], [m__2351])). % 54.46/7.97 cnf(c123, plain, ~aElementOf0(X0,xI) | X0 = sz00 | aElementOf0(sK112(X0),xI), inference(clausification, [status(esa)], [negated_conjecture])). % 54.46/7.97 cnf(c124, plain, ~aElementOf0(X0,xI) | X0 = sz00 | sK112(X0) != sz00, inference(clausification, [status(esa)], [negated_conjecture])). % 54.46/7.97 cnf(c125, plain, ~aElementOf0(X0,xI) | X0 = sz00 | iLess0(sbrdtbr0(sK112(X0)),sbrdtbr0(X0)), inference(clausification, [status(esa)], [negated_conjecture])). % 54.46/7.97 cnf(d0, plain, aElementOf0(sK107,xI), inference(demodulation, [status(thm)], [c118,c113])). % 54.46/7.97 cnf(d1, plain, X0 = sz00 | ~aElementOf0(X0,xI) | ~aElementOf0(X0,xI) | ~iLess0(sbrdtbr0(X0),sbrdtbr0(sK109)), inference(factoring, [status(thm)], [c122])). % 54.46/7.97 cnf(d2, plain, sK112(sK109) = sz00 | ~aElementOf0(sK112(sK109),xI) | sK109 = sz00 | ~aElementOf0(sK109,xI), inference(resolution, [status(thm)], [d1,c125])). % 54.46/7.97 cnf(d3, plain, sK107 = sz00 | aElementOf0(sK109,xI), inference(resolution, [status(thm)], [c120,d0])). % 54.46/7.97 cnf(d4, plain, aElementOf0(sK109,xI), inference(resolution, [status(thm)], [c119,d3])). % 54.46/7.97 cnf(d5, plain, sK109 = sz00 | sK112(sK109) = sz00 | ~aElementOf0(sK112(sK109),xI), inference(resolution, [status(thm)], [d4,d2])). % 54.46/7.97 cnf(d6, plain, sK109 = sz00 | sK112(sK109) = sz00 | sK109 = sz00 | ~aElementOf0(sK109,xI), inference(resolution, [status(thm)], [d5,c123])). % 54.46/7.97 cnf(d7, plain, sK109 = sz00 | sK112(sK109) = sz00, inference(resolution, [status(thm)], [d4,d6])). % 54.46/7.97 cnf(d8, plain, sz00 != sz00 | sK109 = sz00 | ~aElementOf0(sK109,xI) | sK109 = sz00, inference(superposition, [status(thm)], [d7,c124])). % 54.46/7.97 cnf(d9, plain, ~aElement0(X0) | ~aElement0(X1) | ~doDivides0(X0,X1) | sz00 = sdtasdt0(sz00,sK85(X0,X1)), inference(resolution, [status(thm)], [c79,c20])). % 54.46/7.97 cnf(d10, plain, ~aElement0(X0) | ~aElement0(X1) | ~aElement0(sdtasdt0(X0,X1)) | doDivides0(X0,sdtasdt0(X0,X1)), inference(equality_resolution, [status(thm)], [c81])). % 54.46/7.97 cnf(d11, plain, ~aElement0(X0) | ~aElement0(X1) | ~aElement0(X0) | ~aElement0(X1) | doDivides0(X1,sdtasdt0(X1,X0)), inference(resolution, [status(thm)], [c4,d10])). % 54.46/7.97 cnf(d12, plain, sdtpldt0(sz00,smndt0(sz00)) = sz00, inference(resolution, [status(thm)], [c9,c0])). % 54.46/7.97 cnf(d13, plain, aElement0(sK112(X0)) | ~aSet0(xI) | X0 = sz00 | ~aElementOf0(X0,xI), inference(resolution, [status(thm)], [c23,c123])). % 54.46/7.97 cnf(d14, plain, aSet0(xI), inference(resolution, [status(thm)], [c55,c112])). % 54.46/7.97 cnf(d15, plain, X0 = sz00 | aElement0(sK112(X0)) | ~aElementOf0(X0,xI), inference(resolution, [status(thm)], [d14,d13])). % 54.46/7.97 cnf(d16, plain, sK107 = sz00 | aElement0(sK112(sK107)), inference(resolution, [status(thm)], [d0,d15])). % 54.46/7.97 cnf(d17, plain, aElement0(sK112(sK107)), inference(resolution, [status(thm)], [c119,d16])). % 54.46/7.97 cnf(d18, plain, sz00 = sdtasdt0(sz00,sK112(sK107)), inference(resolution, [status(thm)], [d17,c20])). % 54.46/7.97 cnf(d19, plain, aElementOf0(sz00,X0) | ~aElement0(sz00) | ~aElementOf0(sK112(sK107),X0) | ~'Ts53'(X0), inference(superposition, [status(thm)], [d18,c59])). % 54.46/7.97 cnf(d20, plain, aElementOf0(sz00,X0) | ~aElementOf0(sK112(sK107),X0) | ~'Ts53'(X0), inference(resolution, [status(thm)], [c0,d19])). % 54.46/7.97 cnf(d21, plain, aElementOf0(sz00,xI) | ~'Ts53'(xI) | sK107 = sz00 | ~aElementOf0(sK107,xI), inference(resolution, [status(thm)], [d20,c123])). % 54.46/7.97 cnf(d22, plain, aElementOf0(sz00,xI) | ~aElementOf0(sK107,xI) | ~'Ts53'(xI), inference(resolution, [status(thm)], [c119,d21])). % 54.46/7.97 cnf(d23, plain, 'Ts53'(xI), inference(resolution, [status(thm)], [c56,c112])). % 54.46/7.97 cnf(d24, plain, aElementOf0(sz00,xI) | ~aElementOf0(sK107,xI), inference(resolution, [status(thm)], [d23,d22])). % 54.46/7.97 cnf(d25, plain, aElementOf0(sz00,xI), inference(resolution, [status(thm)], [d0,d24])). % 54.46/7.97 cnf(d26, plain, ~aElement0(X0) | ~aElementOf0(X1,X2) | ~'Ts53'(X2) | aElement0(sdtasdt0(X0,X1)) | ~aSet0(X2), inference(resolution, [status(thm)], [c59,c23])). % 54.46/7.97 cnf(d27, plain, ~aElement0(X0) | aElement0(sdtasdt0(X0,sz00)) | ~aSet0(xI) | ~'Ts53'(xI), inference(resolution, [status(thm)], [d26,d25])). % 54.46/7.97 cnf(d28, plain, ~aElement0(X0) | aElement0(sdtasdt0(X0,sz00)) | ~aSet0(xI), inference(resolution, [status(thm)], [d23,d27])). % 54.46/7.97 cnf(d29, plain, ~aElement0(X0) | aElement0(sdtasdt0(X0,sz00)), inference(resolution, [status(thm)], [d14,d28])). % 54.46/7.97 cnf(d30, plain, sdtasdt0(smndt0(sz10),sz00) = smndt0(sz00), inference(resolution, [status(thm)], [c17,c0])). % 54.46/7.97 cnf(d31, plain, aElement0(smndt0(sz00)) | ~aElement0(smndt0(sz10)), inference(superposition, [status(thm)], [d30,d29])). % 54.46/7.97 cnf(d32, plain, aElement0(smndt0(sz00)) | ~aElement0(sz10), inference(resolution, [status(thm)], [d31,c2])). % 54.46/7.97 cnf(d33, plain, aElement0(smndt0(sz00)), inference(resolution, [status(thm)], [c1,d32])). % 54.46/7.97 cnf(d34, plain, smndt0(sz00) = sdtpldt0(sz00,smndt0(sz00)), inference(resolution, [status(thm)], [d33,c8])). % 54.46/7.97 cnf(d35, plain, smndt0(sz00) = sz00, inference(demodulation, [status(thm)], [d34,d12])). % 54.46/7.97 cnf(d36, plain, smndt0(sz00) = sdtasdt0(sz00,smndt0(sz10)), inference(resolution, [status(thm)], [c18,c0])). % 54.46/7.97 cnf(d37, plain, sz00 = sdtasdt0(sz00,smndt0(sz10)), inference(demodulation, [status(thm)], [d36,d35])). % 54.46/7.97 cnf(d38, plain, doDivides0(sz00,sz00) | ~aElement0(sz00) | ~aElement0(smndt0(sz10)), inference(superposition, [status(thm)], [d37,d11])). % 54.46/7.97 cnf(d39, plain, ~aElement0(smndt0(sz10)) | doDivides0(sz00,sz00), inference(resolution, [status(thm)], [c0,d38])). % 54.46/7.97 cnf(d40, plain, doDivides0(sz00,sz00) | ~aElement0(sz10), inference(resolution, [status(thm)], [d39,c2])). % 54.46/7.97 cnf(d41, plain, doDivides0(sz00,sz00), inference(resolution, [status(thm)], [c1,d40])). % 54.46/7.97 cnf(d42, plain, sz00 = sdtasdt0(sz00,sK85(sz00,sz00)) | ~aElement0(sz00) | ~aElement0(sz00), inference(resolution, [status(thm)], [d41,d9])). % 54.46/7.97 cnf(d43, plain, sz00 = sdtasdt0(sz00,sK85(sz00,sz00)), inference(resolution, [status(thm)], [c0,d42])). % 54.46/7.97 cnf(d44, plain, sdtasdt0(sz00,sK85(sz00,sz00)) = sz00 | ~aElement0(sz00) | ~aElement0(sz00), inference(resolution, [status(thm)], [d41,c80])). % 54.46/7.97 cnf(d45, plain, sz00 = sz00 | ~aElement0(sz00), inference(demodulation, [status(thm)], [d44,d43])). % 54.46/7.97 cnf(d46, plain, sz00 = sz00, inference(resolution, [status(thm)], [c0,d45])). % 54.46/7.97 cnf(d47, plain, sK109 = sz00 | ~aElementOf0(sK109,xI), inference(resolution, [status(thm)], [d46,d8])). % 54.46/7.97 cnf(d48, plain, sK109 = sz00, inference(resolution, [status(thm)], [d4,d47])). % 54.46/7.97 cnf(d49, plain, X0 = sz00 | ~aElementOf0(X0,xI), inference(resolution, [status(thm)], [d48,c121])). % 54.46/7.97 cnf(d50, plain, sK107 = sz00, inference(resolution, [status(thm)], [d49,d0])). % 54.46/7.97 cnf(d51, plain, $false, inference(resolution, [status(thm)], [c119,d50])). % 54.46/7.97 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------