%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : LAT385+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 : n011.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 15.62s 2.57s % Output : CNFRefutation 15.62s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LAT385+4 : 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.37 % Computer : n011.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:38:30 UTC 2026 % 0.09/0.37 % CPUTime : % 0.09/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 15.62/2.57 % SZS status Theorem for theBenchmark.p % 15.62/2.57 % SZS output start CNFRefutation for theBenchmark.p % 15.62/2.57 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)))))))))). % 15.62/2.57 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)))). % 15.62/2.57 fof(m__, conjecture, ? [X0] : (((aElementOf0(X0,xU) & (((aElementOf0(X0,xU) & ! [X1] : ((aElementOf0(X1,xP) => sdtlseqdt0(X0,X1)))) | aLowerBoundOfIn0(X0,xP,xU)) & ! [X1] : (((aElementOf0(X1,xU) & (! [X2] : ((aElementOf0(X2,xP) => sdtlseqdt0(X1,X2))) & aLowerBoundOfIn0(X1,xP,xU))) => sdtlseqdt0(X1,X0))))) | aInfimumOfIn0(X0,xP,xU)))). % 15.62/2.57 fof(negated_conjecture, negated_conjecture, ~? [X0] : (((aElementOf0(X0,xU) & (((aElementOf0(X0,xU) & ! [X1] : ((aElementOf0(X1,xP) => sdtlseqdt0(X0,X1)))) | aLowerBoundOfIn0(X0,xP,xU)) & ! [X1] : (((aElementOf0(X1,xU) & (! [X2] : ((aElementOf0(X2,xP) => sdtlseqdt0(X1,X2))) & aLowerBoundOfIn0(X1,xP,xU))) => sdtlseqdt0(X1,X0))))) | aInfimumOfIn0(X0,xP,xU))), inference(negate_conjecture, [status(cth)], [m__])). % 15.62/2.57 cnf(c58, plain, ~aSet0(X0) | aElementOf0(sK74(X0),X0) | X1(X0), inference(clausification, [status(esa)], [m__1123])). % 15.62/2.57 cnf(c59, plain, ~aSet0(X0) | ~aElementOf0(sK74(X0),xU) | X1(X0), inference(clausification, [status(esa)], [m__1123])). % 15.62/2.57 cnf(c75, plain, ~X0(X1) | aInfimumOfIn0(sK77(X1),X1,xU), inference(clausification, [status(esa)], [m__1123])). % 15.62/2.57 cnf(c94, plain, aSet0(xP), inference(clausification, [status(esa)], [m__1244])). % 15.62/2.57 cnf(c95, plain, ~aElementOf0(X0,xP) | aElementOf0(X0,xU), inference(clausification, [status(esa)], [m__1244])). % 15.62/2.57 cnf(c106, plain, ~aInfimumOfIn0(X0,xP,xU), inference(clausification, [status(esa)], [negated_conjecture])). % 15.62/2.57 cnf(d0, plain, aElementOf0(sK74(xP),xU) | ~aSet0(xP) | 'Ts72'(xP), inference(resolution, [status(thm)], [c95,c58])). % 15.62/2.57 cnf(d1, plain, aElementOf0(sK74(xP),xU) | 'Ts72'(xP), inference(resolution, [status(thm)], [c94,d0])). % 15.62/2.57 cnf(d2, plain, ~'Ts72'(xP), inference(resolution, [status(thm)], [c75,c106])). % 15.62/2.57 cnf(d3, plain, aElementOf0(sK74(xP),xU), inference(resolution, [status(thm)], [d2,d1])). % 15.62/2.57 cnf(d4, plain, ~aSet0(xP) | 'Ts72'(xP), inference(resolution, [status(thm)], [d3,c59])). % 15.62/2.57 cnf(d5, plain, 'Ts72'(xP), inference(resolution, [status(thm)], [c94,d4])). % 15.62/2.57 cnf(d6, plain, $false, inference(resolution, [status(thm)], [d2,d5])). % 15.62/2.57 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------