%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : LAT386+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 : n020.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 07:48:35 AM UTC 2026 % Result : Theorem 80.93s 10.76s % Output : CNFRefutation 80.93s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LAT386+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.09/0.37 % Computer : n020.cluster.edu % 0.09/0.37 % Model : x86_64 x86_64 % 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.37 % Memory : 8046.5625MB % 0.09/0.37 % OS : Linux 6.8.0-71-generic % 0.09/0.37 % CPULimit : 300 % 0.09/0.37 % WCLimit : 300 % 0.09/0.37 % DateTime : Fri Sep 25 21:39:49 UTC 2026 % 0.09/0.37 % CPUTime : % 0.09/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 80.93/10.76 % SZS status Theorem for theBenchmark.p % 80.93/10.76 % SZS output start CNFRefutation for theBenchmark.p % 80.93/10.76 fof(mEOfElem, axiom, ! [X0] : ((aSet0(X0) => ! [X1] : ((aElementOf0(X1,X0) => aElement0(X1)))))). % 80.93/10.76 fof(mDefSub, definition, ! [X0] : ((aSet0(X0) => ! [X1] : ((aSubsetOf0(X1,X0) <=> (aSet0(X1) & ! [X2] : ((aElementOf0(X2,X1) => aElementOf0(X2,X0))))))))). % 80.93/10.76 fof(mTrans, axiom, ! [X0] : ! [X1] : ! [X2] : (((aElement0(X0) & (aElement0(X1) & aElement0(X2))) => ((sdtlseqdt0(X0,X1) & sdtlseqdt0(X1,X2)) => sdtlseqdt0(X0,X2))))). % 80.93/10.76 fof(mInfUn, axiom, ! [X0] : ((aSet0(X0) => ! [X1] : ((aSubsetOf0(X1,X0) => ! [X2] : ! [X3] : (((aInfimumOfIn0(X2,X1,X0) & aInfimumOfIn0(X3,X1,X0)) => X2 = X3))))))). % 80.93/10.76 fof(mRanSort, axiom, ! [X0] : ((aFunction0(X0) => aSet0(szRzazndt0(X0))))). % 80.93/10.76 fof(mImgSort, axiom, ! [X0] : ((aFunction0(X0) => ! [X1] : ((aElementOf0(X1,szDzozmdt0(X0)) => aElementOf0(sdtlpdtrp0(X0,X1),szRzazndt0(X0))))))). % 80.93/10.76 fof(mDefFix, definition, ! [X0] : ((aFunction0(X0) => ! [X1] : ((aFixedPointOf0(X1,X0) <=> (aElementOf0(X1,szDzozmdt0(X0)) & sdtlpdtrp0(X0,X1) = X1)))))). % 80.93/10.76 fof(mDefMonot, definition, ! [X0] : ((aFunction0(X0) => (isMonotone0(X0) <=> ! [X1] : ! [X2] : (((aElementOf0(X1,szDzozmdt0(X0)) & aElementOf0(X2,szDzozmdt0(X0))) => (sdtlseqdt0(X1,X2) => sdtlseqdt0(sdtlpdtrp0(X0,X1),sdtlpdtrp0(X0,X2))))))))). % 80.93/10.76 fof(m__1123, hypothesis, (aSet0(xU) & (! [X0] : ((((aSet0(X0) & ! [X1] : ((aElementOf0(X1,X0) => aElementOf0(X1,xU)))) | aSubsetOf0(X0,xU)) => ? [X1] : ((aElementOf0(X1,xU) & (aElementOf0(X1,xU) & (! [X2] : ((aElementOf0(X2,X0) => sdtlseqdt0(X1,X2))) & (aLowerBoundOfIn0(X1,X0,xU) & (! [X2] : ((((aElementOf0(X2,xU) & ! [X3] : ((aElementOf0(X3,X0) => sdtlseqdt0(X2,X3)))) | aLowerBoundOfIn0(X2,X0,xU)) => sdtlseqdt0(X2,X1))) & (aInfimumOfIn0(X1,X0,xU) & ? [X2] : ((aElementOf0(X2,xU) & (aElementOf0(X2,xU) & (! [X3] : ((aElementOf0(X3,X0) => sdtlseqdt0(X3,X2))) & (aUpperBoundOfIn0(X2,X0,xU) & (! [X3] : ((((aElementOf0(X3,xU) & ! [X4] : ((aElementOf0(X4,X0) => sdtlseqdt0(X4,X3)))) | aUpperBoundOfIn0(X3,X0,xU)) => sdtlseqdt0(X2,X3))) & aSupremumOfIn0(X2,X0,xU)))))))))))))))) & (aCompleteLattice0(xU) & (aFunction0(xf) & (! [X0] : ! [X1] : (((aElementOf0(X0,szDzozmdt0(xf)) & aElementOf0(X1,szDzozmdt0(xf))) => (sdtlseqdt0(X0,X1) => sdtlseqdt0(sdtlpdtrp0(xf,X0),sdtlpdtrp0(xf,X1))))) & (isMonotone0(xf) & (szDzozmdt0(xf) = szRzazndt0(xf) & (szRzazndt0(xf) = xU & isOn0(xf,xU)))))))))). % 80.93/10.76 fof(m__1144, hypothesis, (aSet0(xS) & (! [X0] : (((aElementOf0(X0,xS) => (aElementOf0(X0,szDzozmdt0(xf)) & (sdtlpdtrp0(xf,X0) = X0 & aFixedPointOf0(X0,xf)))) & (((aElementOf0(X0,szDzozmdt0(xf)) & sdtlpdtrp0(xf,X0) = X0) | aFixedPointOf0(X0,xf)) => aElementOf0(X0,xS)))) & xS = cS1142(xf)))). % 80.93/10.76 fof(m__1173, hypothesis, (aSet0(xT) & (! [X0] : ((aElementOf0(X0,xT) => aElementOf0(X0,xS))) & aSubsetOf0(xT,xS)))). % 80.93/10.76 fof(m__1244, hypothesis, (aSet0(xP) & (! [X0] : (((aElementOf0(X0,xP) => (aElementOf0(X0,xU) & (sdtlseqdt0(sdtlpdtrp0(xf,X0),X0) & (! [X1] : ((aElementOf0(X1,xT) => sdtlseqdt0(X1,X0))) & aUpperBoundOfIn0(X0,xT,xU))))) & ((aElementOf0(X0,xU) & (sdtlseqdt0(sdtlpdtrp0(xf,X0),X0) & (! [X1] : ((aElementOf0(X1,xT) => sdtlseqdt0(X1,X0))) | aUpperBoundOfIn0(X0,xT,xU)))) => aElementOf0(X0,xP)))) & xP = cS1241(xU,xf,xT)))). % 80.93/10.76 fof(m__1261, hypothesis, (aElementOf0(xp,xU) & (aElementOf0(xp,xU) & (! [X0] : ((aElementOf0(X0,xP) => sdtlseqdt0(xp,X0))) & (aLowerBoundOfIn0(xp,xP,xU) & (! [X0] : ((((aElementOf0(X0,xU) & ! [X1] : ((aElementOf0(X1,xP) => sdtlseqdt0(X0,X1)))) | aLowerBoundOfIn0(X0,xP,xU)) => sdtlseqdt0(X0,xp))) & aInfimumOfIn0(xp,xP,xU))))))). % 80.93/10.76 fof(m__, conjecture, ((! [X0] : ((aElementOf0(X0,xP) => sdtlseqdt0(sdtlpdtrp0(xf,xp),X0))) | aLowerBoundOfIn0(sdtlpdtrp0(xf,xp),xP,xU)) & (! [X0] : ((aElementOf0(X0,xT) => sdtlseqdt0(X0,sdtlpdtrp0(xf,xp)))) | aUpperBoundOfIn0(sdtlpdtrp0(xf,xp),xT,xU)))). % 80.93/10.76 fof(negated_conjecture, negated_conjecture, ~(((! [X0] : ((aElementOf0(X0,xP) => sdtlseqdt0(sdtlpdtrp0(xf,xp),X0))) | aLowerBoundOfIn0(sdtlpdtrp0(xf,xp),xP,xU)) & (! [X0] : ((aElementOf0(X0,xT) => sdtlseqdt0(X0,sdtlpdtrp0(xf,xp)))) | aUpperBoundOfIn0(sdtlpdtrp0(xf,xp),xT,xU)))), inference(negate_conjecture, [status(cth)], [m__])). % 80.93/10.76 cnf(c0, plain, ~aSet0(X0) | ~aElementOf0(X1,X0) | aElement0(X1), inference(clausification, [status(esa)], [mEOfElem])). % 80.93/10.76 cnf(c5, plain, ~aSet0(X0) | aSubsetOf0(X1,X0) | ~aSet0(X1) | aElementOf0(sK10(X0,X1),X1), inference(clausification, [status(esa)], [mDefSub])). % 80.93/10.76 cnf(c6, plain, ~aSet0(X0) | aSubsetOf0(X1,X0) | ~aSet0(X1) | ~aElementOf0(sK10(X0,X1),X0), inference(clausification, [status(esa)], [mDefSub])). % 80.93/10.76 cnf(c9, plain, ~sdtlseqdt0(X0,X1) | ~aElement0(X0) | ~sdtlseqdt0(X2,X0) | sdtlseqdt0(X2,X1) | ~aElement0(X1) | ~aElement0(X2), inference(clausification, [status(esa)], [mTrans])). % 80.93/10.76 cnf(c33, plain, ~aSet0(X0) | ~aInfimumOfIn0(X1,X2,X0) | ~aInfimumOfIn0(X3,X2,X0) | X1 = X3 | ~aSubsetOf0(X2,X0), inference(clausification, [status(esa)], [mInfUn])). % 80.93/10.76 cnf(c42, plain, ~aFunction0(X0) | aSet0(szRzazndt0(X0)), inference(clausification, [status(esa)], [mRanSort])). % 80.93/10.76 cnf(c46, plain, ~aFunction0(X0) | ~aElementOf0(X1,szDzozmdt0(X0)) | aElementOf0(sdtlpdtrp0(X0,X1),szRzazndt0(X0)), inference(clausification, [status(esa)], [mImgSort])). % 80.93/10.76 cnf(c48, plain, ~aFunction0(X0) | ~aFixedPointOf0(X1,X0) | sdtlpdtrp0(X0,X1) = X1, inference(clausification, [status(esa)], [mDefFix])). % 80.93/10.76 cnf(c50, plain, ~aFunction0(X0) | ~isMonotone0(X0) | X1(X0), inference(clausification, [status(esa)], [mDefMonot])). % 80.93/10.76 cnf(c52, plain, ~X0(X1) | ~aElementOf0(X2,szDzozmdt0(X1)) | ~sdtlseqdt0(X3,X2) | ~aElementOf0(X3,szDzozmdt0(X1)) | sdtlseqdt0(sdtlpdtrp0(X1,X3),sdtlpdtrp0(X1,X2)), inference(clausification, [status(esa)], [mDefMonot])). % 80.93/10.76 cnf(c57, plain, aSet0(xU), inference(clausification, [status(esa)], [m__1123])). % 80.93/10.76 cnf(c58, plain, ~aSet0(X0) | aElementOf0(sK74(X0),X0) | X1(X0), inference(clausification, [status(esa)], [m__1123])). % 80.93/10.76 cnf(c59, plain, ~aSet0(X0) | ~aElementOf0(sK74(X0),xU) | X1(X0), inference(clausification, [status(esa)], [m__1123])). % 80.93/10.76 cnf(c62, plain, aFunction0(xf), inference(clausification, [status(esa)], [m__1123])). % 80.93/10.76 cnf(c63, plain, ~aElementOf0(X0,szDzozmdt0(xf)) | ~aElementOf0(X1,szDzozmdt0(xf)) | ~sdtlseqdt0(X0,X1) | sdtlseqdt0(sdtlpdtrp0(xf,X0),sdtlpdtrp0(xf,X1)), inference(clausification, [status(esa)], [m__1123])). % 80.93/10.76 cnf(c64, plain, isMonotone0(xf), inference(clausification, [status(esa)], [m__1123])). % 80.93/10.76 cnf(c65, plain, szDzozmdt0(xf) = szRzazndt0(xf), inference(clausification, [status(esa)], [m__1123])). % 80.93/10.76 cnf(c66, plain, szRzazndt0(xf) = xU, inference(clausification, [status(esa)], [m__1123])). % 80.93/10.76 cnf(c72, plain, ~X0(X1) | ~aElementOf0(X2,xU) | aElementOf0(sK80(X1,X2),X1) | sdtlseqdt0(X2,sK77(X1)), inference(clausification, [status(esa)], [m__1123])). % 80.93/10.76 cnf(c73, plain, ~X0(X1) | ~aElementOf0(X2,xU) | ~sdtlseqdt0(X2,sK80(X1,X2)) | sdtlseqdt0(X2,sK77(X1)), inference(clausification, [status(esa)], [m__1123])). % 80.93/10.76 cnf(c75, plain, ~X0(X1) | aInfimumOfIn0(sK77(X1),X1,xU), inference(clausification, [status(esa)], [m__1123])). % 80.93/10.76 cnf(c85, plain, ~aElementOf0(X0,xS) | aElementOf0(X0,szDzozmdt0(xf)), inference(clausification, [status(esa)], [m__1144])). % 80.93/10.76 cnf(c87, plain, ~aElementOf0(X0,xS) | aFixedPointOf0(X0,xf), inference(clausification, [status(esa)], [m__1144])). % 80.93/10.76 cnf(c92, plain, ~aElementOf0(X0,xT) | aElementOf0(X0,xS), inference(clausification, [status(esa)], [m__1173])). % 80.93/10.76 cnf(c94, plain, aSet0(xP), inference(clausification, [status(esa)], [m__1244])). % 80.93/10.76 cnf(c95, plain, ~aElementOf0(X0,xP) | aElementOf0(X0,xU), inference(clausification, [status(esa)], [m__1244])). % 80.93/10.76 cnf(c96, plain, ~aElementOf0(X0,xP) | sdtlseqdt0(sdtlpdtrp0(xf,X0),X0), inference(clausification, [status(esa)], [m__1244])). % 80.93/10.76 cnf(c97, plain, ~aElementOf0(X0,xP) | ~aElementOf0(X1,xT) | sdtlseqdt0(X1,X0), inference(clausification, [status(esa)], [m__1244])). % 80.93/10.76 cnf(c103, plain, aElementOf0(xp,xU), inference(clausification, [status(esa)], [m__1261])). % 80.93/10.76 cnf(c105, plain, ~aElementOf0(X0,xP) | sdtlseqdt0(xp,X0), inference(clausification, [status(esa)], [m__1261])). % 80.93/10.76 cnf(c110, plain, aInfimumOfIn0(xp,xP,xU), inference(clausification, [status(esa)], [m__1261])). % 80.93/10.76 cnf(c111, plain, ~X0 | aElementOf0(sK94,xT), inference(clausification, [status(esa)], [negated_conjecture])). % 80.93/10.76 cnf(c112, plain, ~X0 | ~sdtlseqdt0(sK94,sdtlpdtrp0(xf,xp)), inference(clausification, [status(esa)], [negated_conjecture])). % 80.93/10.76 cnf(c114, plain, X0 | aElementOf0(sK95,xP), inference(clausification, [status(esa)], [negated_conjecture])). % 80.93/10.76 cnf(c115, plain, X0 | ~sdtlseqdt0(sdtlpdtrp0(xf,xp),sK95), inference(clausification, [status(esa)], [negated_conjecture])). % 80.93/10.76 cnf(d0, plain, ~aElementOf0(X0,szDzozmdt0(X1)) | ~aFunction0(X1) | ~aSet0(szRzazndt0(X1)) | aElement0(sdtlpdtrp0(X1,X0)), inference(resolution, [status(thm)], [c46,c0])). % 80.93/10.76 cnf(d1, plain, ~aFunction0(X0) | ~aElementOf0(X1,szDzozmdt0(X0)) | aElement0(sdtlpdtrp0(X0,X1)) | ~aFunction0(X0), inference(resolution, [status(thm)], [c42,d0])). % 80.93/10.76 cnf(d2, plain, szDzozmdt0(xf) = xU, inference(demodulation, [status(thm)], [c65,c66])). % 80.93/10.76 cnf(d3, plain, ~aElementOf0(X0,xU) | aElement0(sdtlpdtrp0(xf,X0)) | ~aFunction0(xf), inference(superposition, [status(thm)], [d2,d1])). % 80.93/10.76 cnf(d4, plain, ~aElementOf0(X0,xU) | aElement0(sdtlpdtrp0(xf,X0)), inference(resolution, [status(thm)], [c62,d3])). % 80.93/10.76 cnf(d5, plain, ~aElementOf0(X0,xP) | ~aElement0(X0) | ~aElement0(X1) | ~aElement0(sdtlpdtrp0(xf,X0)) | sdtlseqdt0(X1,X0) | ~sdtlseqdt0(X1,sdtlpdtrp0(xf,X0)), inference(resolution, [status(thm)], [c96,c9])). % 80.93/10.76 cnf(d6, plain, ~aElementOf0(X0,xP) | ~aElement0(sdtlpdtrp0(xf,X1)) | ~aElement0(X0) | ~aElement0(sdtlpdtrp0(xf,X0)) | sdtlseqdt0(sdtlpdtrp0(xf,X1),X0) | ~aElementOf0(X0,szDzozmdt0(xf)) | ~aElementOf0(X1,szDzozmdt0(xf)) | ~sdtlseqdt0(X1,X0) | ~'Ts66'(xf), inference(resolution, [status(thm)], [d5,c52])). % 80.93/10.76 cnf(d7, plain, ~aElementOf0(X0,xU) | ~aElementOf0(X1,szDzozmdt0(xf)) | ~aElementOf0(X1,xP) | ~aElement0(X1) | ~aElement0(sdtlpdtrp0(xf,X0)) | ~aElement0(sdtlpdtrp0(xf,X1)) | ~sdtlseqdt0(X0,X1) | sdtlseqdt0(sdtlpdtrp0(xf,X0),X1) | ~'Ts66'(xf), inference(demodulation, [status(thm)], [d6,d2])). % 80.93/10.76 cnf(d8, plain, ~aElementOf0(X0,xU) | ~aElementOf0(X1,xU) | ~aElementOf0(X1,xP) | ~aElement0(X1) | ~aElement0(sdtlpdtrp0(xf,X0)) | ~aElement0(sdtlpdtrp0(xf,X1)) | ~sdtlseqdt0(X0,X1) | sdtlseqdt0(sdtlpdtrp0(xf,X0),X1) | ~'Ts66'(xf), inference(demodulation, [status(thm)], [d7,d2])). % 80.93/10.76 cnf(d9, plain, ~aFunction0(xf) | 'Ts66'(xf), inference(resolution, [status(thm)], [c50,c64])). % 80.93/10.76 cnf(d10, plain, 'Ts66'(xf), inference(resolution, [status(thm)], [c62,d9])). % 80.93/10.76 cnf(d11, plain, ~aElementOf0(X0,xU) | ~aElementOf0(X1,xU) | ~aElementOf0(X1,xP) | ~aElement0(X1) | ~aElement0(sdtlpdtrp0(xf,X0)) | ~aElement0(sdtlpdtrp0(xf,X1)) | ~sdtlseqdt0(X0,X1) | sdtlseqdt0(sdtlpdtrp0(xf,X0),X1), inference(resolution, [status(thm)], [d10,d8])). % 80.93/10.76 cnf(d12, plain, ~aElementOf0(X0,xP) | ~aElementOf0(X0,xP) | ~aElementOf0(X1,xU) | ~aElement0(X0) | ~aElement0(sdtlpdtrp0(xf,X0)) | ~aElement0(sdtlpdtrp0(xf,X1)) | ~sdtlseqdt0(X1,X0) | sdtlseqdt0(sdtlpdtrp0(xf,X1),X0), inference(resolution, [status(thm)], [c95,d11])). % 80.93/10.76 cnf(d13, plain, ~aElementOf0(X0,xU) | ~aElementOf0(X0,xU) | ~aElementOf0(X1,xP) | ~aElement0(X1) | ~aElement0(sdtlpdtrp0(xf,X1)) | ~sdtlseqdt0(X0,X1) | sdtlseqdt0(sdtlpdtrp0(xf,X0),X1), inference(resolution, [status(thm)], [d4,d12])). % 80.93/10.76 cnf(d14, plain, ~aElementOf0(sK95,xP) | ~aElementOf0(xp,xU) | ~aElement0(sK95) | ~aElement0(sdtlpdtrp0(xf,sK95)) | ~sdtlseqdt0(xp,sK95) | 'Ts93', inference(resolution, [status(thm)], [d13,c115])). % 80.93/10.76 cnf(d15, plain, ~aElementOf0(sK95,xP) | ~aElement0(sdtlpdtrp0(xf,sK95)) | ~aElement0(sK95) | ~sdtlseqdt0(xp,sK95) | 'Ts93', inference(resolution, [status(thm)], [c103,d14])). % 80.93/10.76 cnf(d16, plain, 'Ts93' | ~aElement0(sdtlpdtrp0(xf,sK95)) | ~aElement0(sK95) | ~sdtlseqdt0(xp,sK95) | 'Ts93', inference(resolution, [status(thm)], [c114,d15])). % 80.93/10.76 cnf(d17, plain, ~aSet0(xP) | aElement0(sK95) | 'Ts93', inference(resolution, [status(thm)], [c0,c114])). % 80.93/10.76 cnf(d18, plain, aElement0(sK95) | 'Ts93', inference(resolution, [status(thm)], [c94,d17])). % 80.93/10.76 cnf(d19, plain, 'Ts93' | ~aElement0(sdtlpdtrp0(xf,sK95)) | ~sdtlseqdt0(xp,sK95) | 'Ts93', inference(resolution, [status(thm)], [d18,d16])). % 80.93/10.76 cnf(d20, plain, sdtlseqdt0(xp,sK95) | 'Ts93', inference(resolution, [status(thm)], [c105,c114])). % 80.93/10.76 cnf(d21, plain, 'Ts93' | ~aElement0(sdtlpdtrp0(xf,sK95)) | 'Ts93', inference(resolution, [status(thm)], [d20,d19])). % 80.93/10.76 cnf(d22, plain, 'Ts93' | ~aElementOf0(sK95,xU), inference(resolution, [status(thm)], [d21,d4])). % 80.93/10.76 cnf(d23, plain, aElementOf0(sK95,xU) | 'Ts93', inference(resolution, [status(thm)], [c95,c114])). % 80.93/10.76 cnf(d24, plain, 'Ts93' | 'Ts93', inference(resolution, [status(thm)], [d23,d22])). % 80.93/10.76 cnf(d25, plain, ~sdtlseqdt0(sK94,sdtlpdtrp0(xf,xp)), inference(resolution, [status(thm)], [d24,c112])). % 80.93/10.76 cnf(d26, plain, ~aElementOf0(X0,xU) | ~aElementOf0(X1,szDzozmdt0(xf)) | ~sdtlseqdt0(X1,X0) | sdtlseqdt0(sdtlpdtrp0(xf,X1),sdtlpdtrp0(xf,X0)), inference(demodulation, [status(thm)], [c63,d2])). % 80.93/10.76 cnf(d27, plain, ~aElementOf0(X0,xU) | ~aElementOf0(X1,xU) | ~sdtlseqdt0(X1,X0) | sdtlseqdt0(sdtlpdtrp0(xf,X1),sdtlpdtrp0(xf,X0)), inference(demodulation, [status(thm)], [d26,d2])). % 80.93/10.76 cnf(d28, plain, aElementOf0(sK94,xS) | ~'Ts93', inference(resolution, [status(thm)], [c92,c111])). % 80.93/10.76 cnf(d29, plain, ~'Ts93' | aFixedPointOf0(sK94,xf), inference(resolution, [status(thm)], [d28,c87])). % 80.93/10.76 cnf(d30, plain, ~'Ts93' | sdtlpdtrp0(xf,sK94) = sK94 | ~aFunction0(xf), inference(resolution, [status(thm)], [d29,c48])). % 80.93/10.76 cnf(d31, plain, sdtlpdtrp0(xf,sK94) = sK94 | ~'Ts93', inference(resolution, [status(thm)], [c62,d30])). % 80.93/10.76 cnf(d32, plain, sdtlpdtrp0(xf,sK94) = sK94, inference(resolution, [status(thm)], [d24,d31])). % 80.93/10.76 cnf(d33, plain, sdtlseqdt0(sK94,sdtlpdtrp0(xf,X0)) | ~aElementOf0(X0,xU) | ~aElementOf0(sK94,xU) | ~sdtlseqdt0(sK94,X0), inference(superposition, [status(thm)], [d32,d27])). % 80.93/10.76 cnf(d34, plain, aElementOf0(X0,xU) | ~aElementOf0(X0,xS), inference(demodulation, [status(thm)], [c85,d2])). % 80.93/10.76 cnf(d35, plain, aElementOf0(sK94,xU) | ~'Ts93', inference(resolution, [status(thm)], [d34,d28])). % 80.93/10.76 cnf(d36, plain, aElementOf0(sK94,xU), inference(resolution, [status(thm)], [d24,d35])). % 80.93/10.76 cnf(d37, plain, ~aElementOf0(X0,xU) | ~sdtlseqdt0(sK94,X0) | sdtlseqdt0(sK94,sdtlpdtrp0(xf,X0)), inference(resolution, [status(thm)], [d36,d33])). % 80.93/10.76 cnf(d38, plain, ~aElementOf0(xp,xU) | ~sdtlseqdt0(sK94,xp), inference(resolution, [status(thm)], [d37,d25])). % 80.93/10.76 cnf(d39, plain, ~sdtlseqdt0(sK94,xp), inference(resolution, [status(thm)], [c103,d38])). % 80.93/10.76 cnf(d40, plain, X0 = xp | ~aSet0(xU) | ~aSubsetOf0(xP,xU) | ~aInfimumOfIn0(X0,xP,xU), inference(resolution, [status(thm)], [c33,c110])). % 80.93/10.76 cnf(d41, plain, X0 = xp | ~aSubsetOf0(xP,xU) | ~aInfimumOfIn0(X0,xP,xU), inference(resolution, [status(thm)], [c57,d40])). % 80.93/10.76 cnf(d42, plain, sK77(xP) = xp | ~aSubsetOf0(xP,xU) | ~'Ts72'(xP), inference(resolution, [status(thm)], [d41,c75])). % 80.93/10.76 cnf(d43, plain, aElementOf0(sK74(xP),xU) | ~aSet0(xP) | 'Ts72'(xP), inference(resolution, [status(thm)], [c95,c58])). % 80.93/10.76 cnf(d44, plain, aElementOf0(sK74(xP),xU) | 'Ts72'(xP), inference(resolution, [status(thm)], [c94,d43])). % 80.93/10.76 cnf(d45, plain, 'Ts72'(xP) | ~aSet0(xP) | 'Ts72'(xP), inference(resolution, [status(thm)], [d44,c59])). % 80.93/10.76 cnf(d46, plain, 'Ts72'(xP), inference(resolution, [status(thm)], [c94,d45])). % 80.93/10.76 cnf(d47, plain, sK77(xP) = xp | ~aSubsetOf0(xP,xU), inference(resolution, [status(thm)], [d46,d42])). % 80.93/10.76 cnf(d48, plain, aElementOf0(sK10(X0,xP),xU) | ~aSet0(xP) | ~aSet0(X0) | aSubsetOf0(xP,X0), inference(resolution, [status(thm)], [c95,c5])). % 80.93/10.76 cnf(d49, plain, ~aSet0(X0) | aElementOf0(sK10(X0,xP),xU) | aSubsetOf0(xP,X0), inference(resolution, [status(thm)], [c94,d48])). % 80.93/10.76 cnf(d50, plain, ~aSet0(xU) | aSubsetOf0(xP,xU) | ~aSet0(xP) | ~aSet0(xU) | aSubsetOf0(xP,xU), inference(resolution, [status(thm)], [d49,c6])). % 80.93/10.76 cnf(d51, plain, ~aSet0(xP) | aSubsetOf0(xP,xU), inference(resolution, [status(thm)], [c57,d50])). % 80.93/10.76 cnf(d52, plain, aSubsetOf0(xP,xU), inference(resolution, [status(thm)], [c94,d51])). % 80.93/10.76 cnf(d53, plain, sK77(xP) = xp, inference(resolution, [status(thm)], [d52,d47])). % 80.93/10.76 cnf(d54, plain, ~aElementOf0(X0,xT) | sdtlseqdt0(X0,sK80(xP,X1)) | ~aElementOf0(X1,xU) | sdtlseqdt0(X1,sK77(xP)) | ~'Ts72'(xP), inference(resolution, [status(thm)], [c97,c72])). % 80.93/10.76 cnf(d55, plain, ~aElementOf0(X0,xU) | ~aElementOf0(X1,xT) | sdtlseqdt0(X0,sK77(xP)) | sdtlseqdt0(X1,sK80(xP,X0)), inference(resolution, [status(thm)], [d46,d54])). % 80.93/10.76 cnf(d56, plain, ~aElementOf0(X0,xT) | ~aElementOf0(X0,xU) | sdtlseqdt0(X0,sK77(xP)) | ~aElementOf0(X0,xU) | sdtlseqdt0(X0,sK77(xP)) | ~'Ts72'(xP), inference(resolution, [status(thm)], [d55,c73])). % 80.93/10.76 cnf(d57, plain, ~aElementOf0(X0,xU) | ~aElementOf0(X0,xT) | sdtlseqdt0(X0,xp) | ~'Ts72'(xP), inference(demodulation, [status(thm)], [d56,d53])). % 80.93/10.76 cnf(d58, plain, ~aElementOf0(X0,xU) | ~aElementOf0(X0,xT) | sdtlseqdt0(X0,xp), inference(resolution, [status(thm)], [d46,d57])). % 80.93/10.76 cnf(d59, plain, aElementOf0(sK94,xT), inference(resolution, [status(thm)], [d24,c111])). % 80.93/10.76 cnf(d60, plain, ~aElementOf0(sK94,xU) | sdtlseqdt0(sK94,xp), inference(resolution, [status(thm)], [d59,d58])). % 80.93/10.76 cnf(d61, plain, sdtlseqdt0(sK94,xp), inference(resolution, [status(thm)], [d36,d60])). % 80.93/10.76 cnf(d62, plain, $false, inference(resolution, [status(thm)], [d61,d39])). % 80.93/10.76 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------