%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : RNG109+4 : 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 : n004.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 38.29s 5.76s % Output : CNFRefutation 38.29s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : RNG109+4 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.03 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.08/0.35 % Computer : n004.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.36 % CPULimit : 300 % 0.08/0.36 % WCLimit : 300 % 0.08/0.36 % DateTime : Sat Sep 26 06:07:36 UTC 2026 % 0.08/0.36 % CPUTime : % 0.08/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 38.29/5.76 % SZS status Theorem for theBenchmark.p % 38.29/5.76 % SZS output start CNFRefutation for theBenchmark.p % 38.29/5.76 fof(mSortsC, axiom, aElement0(sz00)). % 38.29/5.76 fof(mSortsC_01, axiom, aElement0(sz10)). % 38.29/5.76 fof(mSortsU, axiom, ! [X0] : ((aElement0(X0) => aElement0(smndt0(X0))))). % 38.29/5.76 fof(mSortsB_02, axiom, ! [X0] : ! [X1] : (((aElement0(X0) & aElement0(X1)) => aElement0(sdtasdt0(X0,X1))))). % 38.29/5.76 fof(mAddZero, axiom, ! [X0] : ((aElement0(X0) => (sdtpldt0(X0,sz00) = X0 & X0 = sdtpldt0(sz00,X0))))). % 38.29/5.76 fof(mAddInvr, axiom, ! [X0] : ((aElement0(X0) => (sdtpldt0(X0,smndt0(X0)) = sz00 & sz00 = sdtpldt0(smndt0(X0),X0))))). % 38.29/5.76 fof(mMulComm, axiom, ! [X0] : ! [X1] : (((aElement0(X0) & aElement0(X1)) => sdtasdt0(X0,X1) = sdtasdt0(X1,X0)))). % 38.29/5.76 fof(mMulUnit, axiom, ! [X0] : ((aElement0(X0) => (sdtasdt0(X0,sz10) = X0 & X0 = sdtasdt0(sz10,X0))))). % 38.29/5.76 fof(mMulMnOne, axiom, ! [X0] : ((aElement0(X0) => (sdtasdt0(smndt0(sz10),X0) = smndt0(X0) & smndt0(X0) = sdtasdt0(X0,smndt0(sz10)))))). % 38.29/5.76 fof(mMulZero, axiom, ! [X0] : ((aElement0(X0) => (sdtasdt0(X0,sz00) = sz00 & sz00 = sdtasdt0(sz00,X0))))). % 38.29/5.76 fof(m__2091, hypothesis, (aElement0(xa) & aElement0(xb))). % 38.29/5.76 fof(m__2110, hypothesis, (xa != sz00 | xb != sz00)). % 38.29/5.76 fof(m__2129, hypothesis, (aElement0(xc) & (? [X0] : ((aElement0(X0) & sdtasdt0(xc,X0) = xa)) & (doDivides0(xc,xa) & (aDivisorOf0(xc,xa) & (aElement0(xc) & (? [X0] : ((aElement0(X0) & sdtasdt0(xc,X0) = xb)) & (doDivides0(xc,xb) & (aDivisorOf0(xc,xb) & (! [X0] : (((((aElement0(X0) & (? [X1] : ((aElement0(X1) & sdtasdt0(X0,X1) = xa)) | doDivides0(X0,xa))) | aDivisorOf0(X0,xa)) & (? [X1] : ((aElement0(X1) & sdtasdt0(X0,X1) = xb)) | (doDivides0(X0,xb) | aDivisorOf0(X0,xb)))) => (? [X1] : ((aElement0(X1) & sdtasdt0(X0,X1) = xc)) & doDivides0(X0,xc)))) & aGcdOfAnd0(xc,xa,xb))))))))))). % 38.29/5.76 fof(m__2203, hypothesis, (? [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)))))))))). % 38.29/5.76 fof(m__, conjecture, ? [X0] : (((! [X1] : ((aElementOf0(X1,slsdtgt0(xa)) <=> ? [X2] : ((aElement0(X2) & sdtasdt0(xa,X2) = X1)))) => (! [X1] : ((aElementOf0(X1,slsdtgt0(xb)) <=> ? [X2] : ((aElement0(X2) & sdtasdt0(xb,X2) = X1)))) => (? [X1] : ? [X2] : ((aElementOf0(X1,slsdtgt0(xa)) & (aElementOf0(X2,slsdtgt0(xb)) & sdtpldt0(X1,X2) = X0))) | aElementOf0(X0,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)))))) & X0 != sz00))). % 38.29/5.76 fof(negated_conjecture, negated_conjecture, ~? [X0] : (((! [X1] : ((aElementOf0(X1,slsdtgt0(xa)) <=> ? [X2] : ((aElement0(X2) & sdtasdt0(xa,X2) = X1)))) => (! [X1] : ((aElementOf0(X1,slsdtgt0(xb)) <=> ? [X2] : ((aElement0(X2) & sdtasdt0(xb,X2) = X1)))) => (? [X1] : ? [X2] : ((aElementOf0(X1,slsdtgt0(xa)) & (aElementOf0(X2,slsdtgt0(xb)) & sdtpldt0(X1,X2) = X0))) | aElementOf0(X0,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)))))) & X0 != sz00)), inference(negate_conjecture, [status(cth)], [m__])). % 38.29/5.76 cnf(c0, plain, aElement0(sz00), inference(clausification, [status(esa)], [mSortsC])). % 38.29/5.76 cnf(c1, plain, aElement0(sz10), inference(clausification, [status(esa)], [mSortsC_01])). % 38.29/5.76 cnf(c2, plain, ~aElement0(X0) | aElement0(smndt0(X0)), inference(clausification, [status(esa)], [mSortsU])). % 38.29/5.76 cnf(c4, plain, ~aElement0(X0) | ~aElement0(X1) | aElement0(sdtasdt0(X0,X1)), inference(clausification, [status(esa)], [mSortsB_02])). % 38.29/5.76 cnf(c7, plain, ~aElement0(X0) | sdtpldt0(X0,sz00) = X0, inference(clausification, [status(esa)], [mAddZero])). % 38.29/5.76 cnf(c8, plain, ~aElement0(X0) | X0 = sdtpldt0(sz00,X0), inference(clausification, [status(esa)], [mAddZero])). % 38.29/5.76 cnf(c9, plain, ~aElement0(X0) | sdtpldt0(X0,smndt0(X0)) = sz00, inference(clausification, [status(esa)], [mAddInvr])). % 38.29/5.76 cnf(c11, plain, ~aElement0(X0) | ~aElement0(X1) | sdtasdt0(X0,X1) = sdtasdt0(X1,X0), inference(clausification, [status(esa)], [mMulComm])). % 38.29/5.76 cnf(c13, plain, ~aElement0(X0) | sdtasdt0(X0,sz10) = X0, inference(clausification, [status(esa)], [mMulUnit])). % 38.29/5.76 cnf(c17, plain, ~aElement0(X0) | sdtasdt0(smndt0(sz10),X0) = smndt0(X0), inference(clausification, [status(esa)], [mMulMnOne])). % 38.29/5.76 cnf(c19, plain, ~aElement0(X0) | sdtasdt0(X0,sz00) = sz00, inference(clausification, [status(esa)], [mMulZero])). % 38.29/5.76 cnf(c20, plain, ~aElement0(X0) | sz00 = sdtasdt0(sz00,X0), inference(clausification, [status(esa)], [mMulZero])). % 38.29/5.76 cnf(c108, plain, aElement0(xa), inference(clausification, [status(esa)], [m__2091])). % 38.29/5.76 cnf(c109, plain, aElement0(xb), inference(clausification, [status(esa)], [m__2091])). % 38.29/5.76 cnf(c110, plain, xa != sz00 | xb != sz00, inference(clausification, [status(esa)], [m__2110])). % 38.29/5.76 cnf(c112, plain, aElement0(sK109), inference(clausification, [status(esa)], [m__2129])). % 38.29/5.76 cnf(c113, plain, sdtasdt0(xc,sK109) = xa, inference(clausification, [status(esa)], [m__2129])). % 38.29/5.76 cnf(c117, plain, aElement0(sK110), inference(clausification, [status(esa)], [m__2129])). % 38.29/5.76 cnf(c118, plain, sdtasdt0(xc,sK110) = xb, inference(clausification, [status(esa)], [m__2129])). % 38.29/5.76 cnf(c148, plain, aElementOf0(sz00,slsdtgt0(xa)), inference(clausification, [status(esa)], [m__2203])). % 38.29/5.76 cnf(c158, plain, ~X0(X1) | X1 = sz00, inference(clausification, [status(esa)], [negated_conjecture])). % 38.29/5.76 cnf(c161, plain, X0(X1) | aElementOf0(X2,slsdtgt0(xa)) | ~aElement0(X3) | sdtasdt0(xa,X3) != X2, inference(clausification, [status(esa)], [negated_conjecture])). % 38.29/5.76 cnf(c164, plain, X0(X1) | aElementOf0(X2,slsdtgt0(xb)) | ~aElement0(X3) | sdtasdt0(xb,X3) != X2, inference(clausification, [status(esa)], [negated_conjecture])). % 38.29/5.76 cnf(c165, plain, X0(X1) | ~aElementOf0(X2,slsdtgt0(xa)) | ~aElementOf0(X3,slsdtgt0(xb)) | sdtpldt0(X2,X3) != X1, inference(clausification, [status(esa)], [negated_conjecture])). % 38.29/5.76 cnf(d0, plain, sz00 = sdtasdt0(X0,X1) | ~aElement0(X1) | ~'Ts133'(X0), inference(superposition, [status(thm)], [c158,c20])). % 38.29/5.76 cnf(d1, plain, sz00 = xb | ~aElement0(sK110) | ~'Ts133'(xc), inference(superposition, [status(thm)], [c118,d0])). % 38.29/5.76 cnf(d2, plain, sz00 = xb | ~'Ts133'(xc), inference(resolution, [status(thm)], [c117,d1])). % 38.29/5.76 cnf(d3, plain, xb != xb | xa != sz00 | ~'Ts133'(xc), inference(superposition, [status(thm)], [d2,c110])). % 38.29/5.76 cnf(d4, plain, xa != sz00 | ~'Ts133'(xc), inference(equality_resolution, [status(thm)], [d3])). % 38.29/5.76 cnf(d5, plain, sz00 = xa | ~aElement0(sK109) | ~'Ts133'(xc), inference(superposition, [status(thm)], [c113,d0])). % 38.29/5.76 cnf(d6, plain, sz00 = xa | ~'Ts133'(xc), inference(resolution, [status(thm)], [c112,d5])). % 38.29/5.76 cnf(d7, plain, xa != xa | ~'Ts133'(xc) | ~'Ts133'(xc), inference(superposition, [status(thm)], [d6,d4])). % 38.29/5.76 cnf(d8, plain, ~'Ts133'(xc), inference(equality_resolution, [status(thm)], [d7])). % 38.29/5.76 cnf(d9, plain, ~aElementOf0(X0,slsdtgt0(xa)) | ~aElementOf0(X1,slsdtgt0(xb)) | 'Ts133'(sdtpldt0(X0,X1)), inference(equality_resolution, [status(thm)], [c165])). % 38.29/5.76 cnf(d10, plain, ~aElement0(X0) | aElementOf0(sdtasdt0(xa,X0),slsdtgt0(xa)) | 'Ts133'(X1), inference(equality_resolution, [status(thm)], [c161])). % 38.29/5.76 cnf(d11, plain, aElementOf0(xa,slsdtgt0(xa)) | ~aElement0(sz10) | 'Ts133'(X0) | ~aElement0(xa), inference(superposition, [status(thm)], [c13,d10])). % 38.29/5.76 cnf(d12, plain, ~aElement0(xa) | aElementOf0(xa,slsdtgt0(xa)) | 'Ts133'(X0), inference(resolution, [status(thm)], [c1,d11])). % 38.29/5.76 cnf(d13, plain, aElementOf0(xa,slsdtgt0(xa)) | 'Ts133'(X0), inference(resolution, [status(thm)], [c108,d12])). % 38.29/5.76 cnf(d14, plain, 'Ts133'(X0) | ~aElementOf0(X1,slsdtgt0(xb)) | 'Ts133'(sdtpldt0(xa,X1)), inference(resolution, [status(thm)], [d13,d9])). % 38.29/5.76 cnf(d15, plain, ~aElement0(X0) | aElementOf0(sdtasdt0(xb,X0),slsdtgt0(xb)) | 'Ts133'(X1), inference(equality_resolution, [status(thm)], [c164])). % 38.29/5.76 cnf(d16, plain, aElementOf0(sz00,slsdtgt0(xb)) | ~aElement0(sz00) | 'Ts133'(X0) | ~aElement0(xb), inference(superposition, [status(thm)], [c19,d15])). % 38.29/5.76 cnf(d17, plain, ~aElement0(xb) | aElementOf0(sz00,slsdtgt0(xb)) | 'Ts133'(X0), inference(resolution, [status(thm)], [c0,d16])). % 38.29/5.76 cnf(d18, plain, aElementOf0(sz00,slsdtgt0(xb)) | 'Ts133'(X0), inference(resolution, [status(thm)], [c109,d17])). % 38.29/5.76 cnf(d19, plain, 'Ts133'(X0) | 'Ts133'(X1) | 'Ts133'(sdtpldt0(xa,sz00)), inference(resolution, [status(thm)], [d18,d14])). % 38.29/5.76 cnf(d20, plain, 'Ts133'(xa) | 'Ts133'(X0) | 'Ts133'(X1) | ~aElement0(xa), inference(superposition, [status(thm)], [c7,d19])). % 38.29/5.76 cnf(d21, plain, 'Ts133'(X0) | 'Ts133'(X1) | 'Ts133'(xa), inference(resolution, [status(thm)], [c108,d20])). % 38.29/5.76 cnf(d22, plain, sdtpldt0(X1,X0) = X1 | ~aElement0(X1) | ~'Ts133'(X0), inference(superposition, [status(thm)], [c158,c7])). % 38.29/5.76 cnf(d23, plain, X0 = sz00 | ~aElement0(X0) | ~aElement0(X0) | ~'Ts133'(smndt0(X0)), inference(superposition, [status(thm)], [d22,c9])). % 38.29/5.76 cnf(d24, plain, ~aElementOf0(X0,slsdtgt0(xb)) | 'Ts133'(sdtpldt0(sz00,X0)), inference(resolution, [status(thm)], [c148,d9])). % 38.29/5.76 cnf(d25, plain, 'Ts133'(sdtpldt0(sz00,sdtasdt0(xb,X0))) | ~aElement0(X0) | 'Ts133'(X1), inference(resolution, [status(thm)], [d24,d15])). % 38.29/5.76 cnf(d26, plain, 'Ts133'(sdtasdt0(xb,X0)) | ~aElement0(X0) | 'Ts133'(X1) | ~aElement0(sdtasdt0(xb,X0)), inference(superposition, [status(thm)], [c8,d25])). % 38.29/5.76 cnf(d27, plain, ~aElement0(X0) | 'Ts133'(X1) | 'Ts133'(sdtasdt0(xb,X0)) | ~aElement0(X0) | ~aElement0(xb), inference(resolution, [status(thm)], [d26,c4])). % 38.29/5.76 cnf(d28, plain, ~aElement0(X0) | 'Ts133'(X1) | 'Ts133'(sdtasdt0(xb,X0)), inference(resolution, [status(thm)], [c109,d27])). % 38.29/5.76 cnf(d29, plain, 'Ts133'(sdtasdt0(X0,xb)) | ~aElement0(X0) | 'Ts133'(X1) | ~aElement0(X0) | ~aElement0(xb), inference(superposition, [status(thm)], [c11,d28])). % 38.29/5.76 cnf(d30, plain, ~aElement0(X0) | 'Ts133'(X1) | 'Ts133'(sdtasdt0(X0,xb)), inference(resolution, [status(thm)], [c109,d29])). % 38.29/5.76 cnf(d31, plain, 'Ts133'(smndt0(xb)) | ~aElement0(smndt0(sz10)) | 'Ts133'(X0) | ~aElement0(xb), inference(superposition, [status(thm)], [c17,d30])). % 38.29/5.76 cnf(d32, plain, ~aElement0(smndt0(sz10)) | 'Ts133'(X0) | 'Ts133'(smndt0(xb)), inference(resolution, [status(thm)], [c109,d31])). % 38.29/5.76 cnf(d33, plain, 'Ts133'(X0) | 'Ts133'(smndt0(xb)) | ~aElement0(sz10), inference(resolution, [status(thm)], [d32,c2])). % 38.29/5.76 cnf(d34, plain, 'Ts133'(X0) | 'Ts133'(smndt0(xb)), inference(resolution, [status(thm)], [c1,d33])). % 38.29/5.76 cnf(d35, plain, 'Ts133'(X0) | xb = sz00 | ~aElement0(xb), inference(resolution, [status(thm)], [d34,d23])). % 38.29/5.76 cnf(d36, plain, xb = sz00 | 'Ts133'(X0), inference(resolution, [status(thm)], [c109,d35])). % 38.29/5.76 cnf(d37, plain, xb != xb | xa != sz00 | 'Ts133'(X0), inference(superposition, [status(thm)], [d36,c110])). % 38.29/5.76 cnf(d38, plain, xa != sz00 | 'Ts133'(X0), inference(equality_resolution, [status(thm)], [d37])). % 38.29/5.76 cnf(d39, plain, xa != X0 | 'Ts133'(X1) | ~'Ts133'(X0), inference(superposition, [status(thm)], [c158,d38])). % 38.29/5.76 cnf(d40, plain, 'Ts133'(X0) | ~'Ts133'(xa), inference(equality_resolution, [status(thm)], [d39])). % 38.29/5.76 cnf(d41, plain, 'Ts133'(X0) | 'Ts133'(X1) | 'Ts133'(X2), inference(resolution, [status(thm)], [d40,d21])). % 38.29/5.76 cnf(d42, plain, 'Ts133'(X0) | 'Ts133'(X1), inference(resolution, [status(thm)], [d8,d41])). % 38.29/5.76 cnf(d43, plain, 'Ts133'(X0), inference(resolution, [status(thm)], [d42,d8])). % 38.29/5.76 cnf(d44, plain, $false, inference(resolution, [status(thm)], [d43,d8])). % 38.29/5.76 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------