%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT385+4 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n026.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 : Thu Sep 24 01:03:57 PM UTC 2026
% Result : Theorem 0.17s 0.52s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT385+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.46 % Computer : n026.cluster.edu
% 0.17/0.46 % Model : x86_64 x86_64
% 0.17/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.46 % Memory : 8046.5625MB
% 0.17/0.46 % OS : Linux 6.8.0-71-generic
% 0.17/0.46 % CPULimit : 300
% 0.17/0.46 % WCLimit : 300
% 0.17/0.46 % DateTime : Mon Sep 21 00:00:07 UTC 2026
% 0.17/0.46 % CPUTime :
% 0.17/0.50 % Drodi V4.1.1
% 0.17/0.52 % Refutation found
% 0.17/0.52 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.17/0.52 % SZS output start CNFRefutation for theBenchmark
% 0.17/0.52 fof(f5,definition,(
% 0.17/0.52 (! [W0] :( aSet0(W0)=> (! [W1] :( aSubsetOf0(W1,W0)<=> ( aSet0(W1)& (! [W2] :( aElementOf0(W2,W1)=> aElementOf0(W2,W0) ) )) ) )) )),
% 0.17/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.52 fof(f24,hypothesis,(
% 0.17/0.52 ( aSet0(xU)& (! [W0] :( ( ( aSet0(W0)& (! [W1] :( aElementOf0(W1,W0)=> aElementOf0(W1,xU) ) ))| aSubsetOf0(W0,xU) )=> (? [W1] :( aElementOf0(W1,xU)& aElementOf0(W1,xU)& (! [W2] :( aElementOf0(W2,W0)=> sdtlseqdt0(W1,W2) ))& aLowerBoundOfIn0(W1,W0,xU)& (! [W2] :( ( ( aElementOf0(W2,xU)& (! [W3] :( aElementOf0(W3,W0)=> sdtlseqdt0(W2,W3) ) ))| aLowerBoundOfIn0(W2,W0,xU) )=> sdtlseqdt0(W2,W1) ))& aInfimumOfIn0(W1,W0,xU)& (? [W2] :( aElementOf0(W2,xU)& aElementOf0(W2,xU)& (! [W3] :( aElementOf0(W3,W0)=> sdtlseqdt0(W3,W2) ))& aUpperBoundOfIn0(W2,W0,xU)& (! [W3] :( ( ( aElementOf0(W3,xU)& (! [W4] :( aElementOf0(W4,W0)=> sdtlseqdt0(W4,W3) ) ))| aUpperBoundOfIn0(W3,W0,xU) )=> sdtlseqdt0(W2,W3) ))& aSupremumOfIn0(W2,W0,xU) ) )) )))& aCompleteLattice0(xU)& aFunction0(xf)& (! [W0,W1] :( ( aElementOf0(W0,szDzozmdt0(xf))& aElementOf0(W1,szDzozmdt0(xf)) )=> ( sdtlseqdt0(W0,W1)=> sdtlseqdt0(sdtlpdtrp0(xf,W0),sdtlpdtrp0(xf,W1)) ) ))& isMonotone0(xf)& szDzozmdt0(xf) = szRzazndt0(xf)& szRzazndt0(xf) = xU& isOn0(xf,xU) ) ),
% 0.17/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.52 fof(f27,hypothesis,(
% 0.17/0.52 ( aSet0(xP)& (! [W0] :( ( aElementOf0(W0,xP)=> ( aElementOf0(W0,xU)& sdtlseqdt0(sdtlpdtrp0(xf,W0),W0)& (! [W1] :( aElementOf0(W1,xT)=> sdtlseqdt0(W1,W0) ))& aUpperBoundOfIn0(W0,xT,xU) ) )& ( ( aElementOf0(W0,xU)& sdtlseqdt0(sdtlpdtrp0(xf,W0),W0)& ( (! [W1] :( aElementOf0(W1,xT)=> sdtlseqdt0(W1,W0) ))| aUpperBoundOfIn0(W0,xT,xU) ) )=> aElementOf0(W0,xP) ) ))& xP = cS1241(xU,xf,xT) ) ),
% 0.17/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.52 fof(f28,conjecture,(
% 0.17/0.52 (? [W0] :( ( aElementOf0(W0,xU)& ( ( aElementOf0(W0,xU)& (! [W1] :( aElementOf0(W1,xP)=> sdtlseqdt0(W0,W1) ) ))| aLowerBoundOfIn0(W0,xP,xU) )& (! [W1] :( ( aElementOf0(W1,xU)& (! [W2] :( aElementOf0(W2,xP)=> sdtlseqdt0(W1,W2) ))& aLowerBoundOfIn0(W1,xP,xU) )=> sdtlseqdt0(W1,W0) ) ))| aInfimumOfIn0(W0,xP,xU) ) )),
% 0.17/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.52 fof(f29,negated_conjecture,(
% 0.17/0.52 ~((? [W0] :( ( aElementOf0(W0,xU)& ( ( aElementOf0(W0,xU)& (! [W1] :( aElementOf0(W1,xP)=> sdtlseqdt0(W0,W1) ) ))| aLowerBoundOfIn0(W0,xP,xU) )& (! [W1] :( ( aElementOf0(W1,xU)& (! [W2] :( aElementOf0(W2,xP)=> sdtlseqdt0(W1,W2) ))& aLowerBoundOfIn0(W1,xP,xU) )=> sdtlseqdt0(W1,W0) ) ))| aInfimumOfIn0(W0,xP,xU) ) ))),
% 0.17/0.52 inference(negated_conjecture,[status(cth)],[f28])).
% 0.17/0.52 fof(f43,plain,(
% 0.17/0.52 ![W0]: (~aSet0(W0)|(![W1]: (aSubsetOf0(W1,W0)<=>(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0)))))))),
% 0.17/0.52 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.17/0.52 fof(f44,plain,(
% 0.17/0.52 ![W0]: (~aSet0(W0)|(![W1]: ((~aSubsetOf0(W1,W0)|(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0)))))&(aSubsetOf0(W1,W0)|(~aSet0(W1)|(?[W2]: (aElementOf0(W2,W1)&~aElementOf0(W2,W0))))))))),
% 0.17/0.52 inference(NNF_transformation,[status(thm)],[f43])).
% 0.17/0.52 fof(f45,plain,(
% 0.17/0.52 ![W0]: (~aSet0(W0)|((![W1]: (~aSubsetOf0(W1,W0)|(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0))))))&(![W1]: (aSubsetOf0(W1,W0)|(~aSet0(W1)|(?[W2]: (aElementOf0(W2,W1)&~aElementOf0(W2,W0))))))))),
% 0.17/0.52 inference(miniscoping,[status(thm)],[f44])).
% 0.17/0.52 fof(f46,plain,(
% 0.17/0.52 ![W0]: (~aSet0(W0)|((![W1]: (~aSubsetOf0(W1,W0)|(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0))))))&(![W1]: (aSubsetOf0(W1,W0)|(~aSet0(W1)|(aElementOf0(sK1_skl(W1,W0),W1)&~aElementOf0(sK1_skl(W1,W0),W0)))))))),
% 0.17/0.52 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W2,sK1_skl(W1,W0))],[f45])).
% 0.17/0.52 fof(f49,plain,(
% 0.17/0.52 ![X0,X1]: (~aSet0(X0)|aSubsetOf0(X1,X0)|~aSet0(X1)|aElementOf0(sK1_skl(X1,X0),X1))),
% 0.17/0.52 inference(cnf_transformation,[status(thm)],[f46])).
% 0.17/0.52 fof(f50,plain,(
% 0.17/0.52 ![X0,X1]: (~aSet0(X0)|aSubsetOf0(X1,X0)|~aSet0(X1)|~aElementOf0(sK1_skl(X1,X0),X0))),
% 0.17/0.52 inference(cnf_transformation,[status(thm)],[f46])).
% 0.17/0.52 fof(f134,plain,(
% 0.17/0.52 (((((((aSet0(xU)&(![W0]: (((~aSet0(W0)|(?[W1]: (aElementOf0(W1,W0)&~aElementOf0(W1,xU))))&~aSubsetOf0(W0,xU))|(?[W1]: ((((((aElementOf0(W1,xU)&aElementOf0(W1,xU))&(![W2]: (~aElementOf0(W2,W0)|sdtlseqdt0(W1,W2))))&aLowerBoundOfIn0(W1,W0,xU))&(![W2]: (((~aElementOf0(W2,xU)|(?[W3]: (aElementOf0(W3,W0)&~sdtlseqdt0(W2,W3))))&~aLowerBoundOfIn0(W2,W0,xU))|sdtlseqdt0(W2,W1))))&aInfimumOfIn0(W1,W0,xU))&(?[W2]: (((((aElementOf0(W2,xU)&aElementOf0(W2,xU))&(![W3]: (~aElementOf0(W3,W0)|sdtlseqdt0(W3,W2))))&aUpperBoundOfIn0(W2,W0,xU))&(![W3]: (((~aElementOf0(W3,xU)|(?[W4]: (aElementOf0(W4,W0)&~sdtlseqdt0(W4,W3))))&~aUpperBoundOfIn0(W3,W0,xU))|sdtlseqdt0(W2,W3))))&aSupremumOfIn0(W2,W0,xU))))))))&aCompleteLattice0(xU))&aFunction0(xf))&(![W0,W1]: ((~aElementOf0(W0,szDzozmdt0(xf))|~aElementOf0(W1,szDzozmdt0(xf)))|(~sdtlseqdt0(W0,W1)|sdtlseqdt0(sdtlpdtrp0(xf,W0),sdtlpdtrp0(xf,W1))))))&isMonotone0(xf))&szDzozmdt0(xf)=szRzazndt0(xf))&szRzazndt0(xf)=xU)&isOn0(xf,xU)),
% 0.17/0.52 inference(pre_NNF_transformation,[status(thm)],[f24])).
% 0.17/0.52 fof(f135,definition,(
% 0.17/0.52 ![W0]: (sP0_prd(W0)<=>((~aSet0(W0)|(?[W1]: (aElementOf0(W1,W0)&~aElementOf0(W1,xU))))&~aSubsetOf0(W0,xU)))),
% 0.17/0.52 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.17/0.52 fof(f136,plain,(
% 0.17/0.52 (((((((aSet0(xU)&(![W0]: (sP0_prd(W0)|(?[W1]: ((((((aElementOf0(W1,xU)&aElementOf0(W1,xU))&(![W2]: (~aElementOf0(W2,W0)|sdtlseqdt0(W1,W2))))&aLowerBoundOfIn0(W1,W0,xU))&(![W2]: (((~aElementOf0(W2,xU)|(?[W3]: (aElementOf0(W3,W0)&~sdtlseqdt0(W2,W3))))&~aLowerBoundOfIn0(W2,W0,xU))|sdtlseqdt0(W2,W1))))&aInfimumOfIn0(W1,W0,xU))&(?[W2]: (((((aElementOf0(W2,xU)&aElementOf0(W2,xU))&(![W3]: (~aElementOf0(W3,W0)|sdtlseqdt0(W3,W2))))&aUpperBoundOfIn0(W2,W0,xU))&(![W3]: (((~aElementOf0(W3,xU)|(?[W4]: (aElementOf0(W4,W0)&~sdtlseqdt0(W4,W3))))&~aUpperBoundOfIn0(W3,W0,xU))|sdtlseqdt0(W2,W3))))&aSupremumOfIn0(W2,W0,xU))))))))&aCompleteLattice0(xU))&aFunction0(xf))&(![W0,W1]: ((~aElementOf0(W0,szDzozmdt0(xf))|~aElementOf0(W1,szDzozmdt0(xf)))|(~sdtlseqdt0(W0,W1)|sdtlseqdt0(sdtlpdtrp0(xf,W0),sdtlpdtrp0(xf,W1))))))&isMonotone0(xf))&szDzozmdt0(xf)=szRzazndt0(xf))&szRzazndt0(xf)=xU)&isOn0(xf,xU)),
% 0.17/0.52 inference(formula_renaming,[status(thm)],[f134,f135])).
% 0.17/0.52 fof(f137,plain,(
% 0.17/0.52 (((((((aSet0(xU)&(![W0]: (sP0_prd(W0)|((?[W1]: (((((aElementOf0(W1,xU)&aElementOf0(W1,xU))&(![W2]: (~aElementOf0(W2,W0)|sdtlseqdt0(W1,W2))))&aLowerBoundOfIn0(W1,W0,xU))&(![W2]: (((~aElementOf0(W2,xU)|(?[W3]: (aElementOf0(W3,W0)&~sdtlseqdt0(W2,W3))))&~aLowerBoundOfIn0(W2,W0,xU))|sdtlseqdt0(W2,W1))))&aInfimumOfIn0(W1,W0,xU)))&(?[W2]: (((((aElementOf0(W2,xU)&aElementOf0(W2,xU))&(![W3]: (~aElementOf0(W3,W0)|sdtlseqdt0(W3,W2))))&aUpperBoundOfIn0(W2,W0,xU))&(![W3]: (((~aElementOf0(W3,xU)|(?[W4]: (aElementOf0(W4,W0)&~sdtlseqdt0(W4,W3))))&~aUpperBoundOfIn0(W3,W0,xU))|sdtlseqdt0(W2,W3))))&aSupremumOfIn0(W2,W0,xU)))))))&aCompleteLattice0(xU))&aFunction0(xf))&(![W0,W1]: ((~aElementOf0(W0,szDzozmdt0(xf))|~aElementOf0(W1,szDzozmdt0(xf)))|(~sdtlseqdt0(W0,W1)|sdtlseqdt0(sdtlpdtrp0(xf,W0),sdtlpdtrp0(xf,W1))))))&isMonotone0(xf))&szDzozmdt0(xf)=szRzazndt0(xf))&szRzazndt0(xf)=xU)&isOn0(xf,xU)),
% 0.17/0.52 inference(miniscoping,[status(thm)],[f136])).
% 0.17/0.52 fof(f138,plain,(
% 0.17/0.52 (((((((aSet0(xU)&(![W0]: (sP0_prd(W0)|((((((aElementOf0(sK11_skl(W0),xU)&aElementOf0(sK11_skl(W0),xU))&(![W2]: (~aElementOf0(W2,W0)|sdtlseqdt0(sK11_skl(W0),W2))))&aLowerBoundOfIn0(sK11_skl(W0),W0,xU))&(![W2]: (((~aElementOf0(W2,xU)|(aElementOf0(sK12_skl(W2,W0),W0)&~sdtlseqdt0(W2,sK12_skl(W2,W0))))&~aLowerBoundOfIn0(W2,W0,xU))|sdtlseqdt0(W2,sK11_skl(W0)))))&aInfimumOfIn0(sK11_skl(W0),W0,xU))&(((((aElementOf0(sK13_skl(W0),xU)&aElementOf0(sK13_skl(W0),xU))&(![W3]: (~aElementOf0(W3,W0)|sdtlseqdt0(W3,sK13_skl(W0)))))&aUpperBoundOfIn0(sK13_skl(W0),W0,xU))&(![W3]: (((~aElementOf0(W3,xU)|(aElementOf0(sK14_skl(W3,W0),W0)&~sdtlseqdt0(sK14_skl(W3,W0),W3)))&~aUpperBoundOfIn0(W3,W0,xU))|sdtlseqdt0(sK13_skl(W0),W3))))&aSupremumOfIn0(sK13_skl(W0),W0,xU))))))&aCompleteLattice0(xU))&aFunction0(xf))&(![W0,W1]: ((~aElementOf0(W0,szDzozmdt0(xf))|~aElementOf0(W1,szDzozmdt0(xf)))|(~sdtlseqdt0(W0,W1)|sdtlseqdt0(sdtlpdtrp0(xf,W0),sdtlpdtrp0(xf,W1))))))&isMonotone0(xf))&szDzozmdt0(xf)=szRzazndt0(xf))&szRzazndt0(xf)=xU)&isOn0(xf,xU)),
% 0.17/0.52 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl,sK12_skl,sK13_skl,sK14_skl]),skolemize(W1,sK11_skl(W0)),skolemize(W3,sK12_skl(W2,W0)),skolemize(W2,sK13_skl(W0)),skolemize(W4,sK14_skl(W3,W0))],[f137])).
% 0.17/0.52 fof(f139,plain,(
% 0.17/0.52 aSet0(xU)),
% 0.17/0.52 inference(cnf_transformation,[status(thm)],[f138])).
% 0.17/0.52 fof(f147,plain,(
% 0.17/0.52 ![X0]: (sP0_prd(X0)|aInfimumOfIn0(sK11_skl(X0),X0,xU))),
% 0.17/0.52 inference(cnf_transformation,[status(thm)],[f138])).
% 0.17/0.52 fof(f176,plain,(
% 0.17/0.52 (aSet0(xP)&(![W0]: ((~aElementOf0(W0,xP)|(((aElementOf0(W0,xU)&sdtlseqdt0(sdtlpdtrp0(xf,W0),W0))&(![W1]: (~aElementOf0(W1,xT)|sdtlseqdt0(W1,W0))))&aUpperBoundOfIn0(W0,xT,xU)))&(((~aElementOf0(W0,xU)|~sdtlseqdt0(sdtlpdtrp0(xf,W0),W0))|((?[W1]: (aElementOf0(W1,xT)&~sdtlseqdt0(W1,W0)))&~aUpperBoundOfIn0(W0,xT,xU)))|aElementOf0(W0,xP)))))&xP=cS1241(xU,xf,xT)),
% 0.17/0.52 inference(pre_NNF_transformation,[status(thm)],[f27])).
% 0.17/0.52 fof(f177,plain,(
% 0.17/0.52 (aSet0(xP)&((![W0]: (~aElementOf0(W0,xP)|(((aElementOf0(W0,xU)&sdtlseqdt0(sdtlpdtrp0(xf,W0),W0))&(![W1]: (~aElementOf0(W1,xT)|sdtlseqdt0(W1,W0))))&aUpperBoundOfIn0(W0,xT,xU))))&(![W0]: (((~aElementOf0(W0,xU)|~sdtlseqdt0(sdtlpdtrp0(xf,W0),W0))|((?[W1]: (aElementOf0(W1,xT)&~sdtlseqdt0(W1,W0)))&~aUpperBoundOfIn0(W0,xT,xU)))|aElementOf0(W0,xP)))))&xP=cS1241(xU,xf,xT)),
% 0.17/0.52 inference(miniscoping,[status(thm)],[f176])).
% 0.17/0.52 fof(f178,plain,(
% 0.17/0.52 (aSet0(xP)&((![W0]: (~aElementOf0(W0,xP)|(((aElementOf0(W0,xU)&sdtlseqdt0(sdtlpdtrp0(xf,W0),W0))&(![W1]: (~aElementOf0(W1,xT)|sdtlseqdt0(W1,W0))))&aUpperBoundOfIn0(W0,xT,xU))))&(![W0]: (((~aElementOf0(W0,xU)|~sdtlseqdt0(sdtlpdtrp0(xf,W0),W0))|((aElementOf0(sK15_skl(W0),xT)&~sdtlseqdt0(sK15_skl(W0),W0))&~aUpperBoundOfIn0(W0,xT,xU)))|aElementOf0(W0,xP)))))&xP=cS1241(xU,xf,xT)),
% 0.17/0.52 inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl]),skolemize(W1,sK15_skl(W0))],[f177])).
% 0.17/0.52 fof(f179,plain,(
% 0.17/0.52 aSet0(xP)),
% 0.17/0.52 inference(cnf_transformation,[status(thm)],[f178])).
% 0.17/0.52 fof(f180,plain,(
% 0.17/0.52 ![X0]: (~aElementOf0(X0,xP)|aElementOf0(X0,xU))),
% 0.17/0.52 inference(cnf_transformation,[status(thm)],[f178])).
% 0.17/0.52 fof(f188,plain,(
% 0.17/0.52 (![W0]: (((~aElementOf0(W0,xU)|((~aElementOf0(W0,xU)|(?[W1]: (aElementOf0(W1,xP)&~sdtlseqdt0(W0,W1))))&~aLowerBoundOfIn0(W0,xP,xU)))|(?[W1]: (((aElementOf0(W1,xU)&(![W2]: (~aElementOf0(W2,xP)|sdtlseqdt0(W1,W2))))&aLowerBoundOfIn0(W1,xP,xU))&~sdtlseqdt0(W1,W0))))&~aInfimumOfIn0(W0,xP,xU)))),
% 0.17/0.52 inference(pre_NNF_transformation,[status(thm)],[f29])).
% 0.17/0.52 fof(f189,definition,(
% 0.17/0.52 ![W0]: (sP1_prd(W0)<=>((~aElementOf0(W0,xU)|(?[W1]: (aElementOf0(W1,xP)&~sdtlseqdt0(W0,W1))))&~aLowerBoundOfIn0(W0,xP,xU)))),
% 0.17/0.52 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 0.17/0.52 fof(f190,plain,(
% 0.17/0.52 ![W0]: (((~aElementOf0(W0,xU)|sP1_prd(W0))|(?[W1]: (((aElementOf0(W1,xU)&(![W2]: (~aElementOf0(W2,xP)|sdtlseqdt0(W1,W2))))&aLowerBoundOfIn0(W1,xP,xU))&~sdtlseqdt0(W1,W0))))&~aInfimumOfIn0(W0,xP,xU))),
% 0.17/0.52 inference(formula_renaming,[status(thm)],[f188,f189])).
% 0.17/0.52 fof(f191,plain,(
% 0.17/0.52 (![W0]: ((~aElementOf0(W0,xU)|sP1_prd(W0))|(?[W1]: (((aElementOf0(W1,xU)&(![W2]: (~aElementOf0(W2,xP)|sdtlseqdt0(W1,W2))))&aLowerBoundOfIn0(W1,xP,xU))&~sdtlseqdt0(W1,W0)))))&(![W0]: ~aInfimumOfIn0(W0,xP,xU))),
% 0.17/0.52 inference(miniscoping,[status(thm)],[f190])).
% 0.17/0.52 fof(f192,plain,(
% 0.17/0.52 (![W0]: ((~aElementOf0(W0,xU)|sP1_prd(W0))|(((aElementOf0(sK16_skl(W0),xU)&(![W2]: (~aElementOf0(W2,xP)|sdtlseqdt0(sK16_skl(W0),W2))))&aLowerBoundOfIn0(sK16_skl(W0),xP,xU))&~sdtlseqdt0(sK16_skl(W0),W0))))&(![W0]: ~aInfimumOfIn0(W0,xP,xU))),
% 0.17/0.52 inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl]),skolemize(W1,sK16_skl(W0))],[f191])).
% 0.17/0.52 fof(f197,plain,(
% 0.17/0.52 ![X0]: (~aInfimumOfIn0(X0,xP,xU))),
% 0.17/0.52 inference(cnf_transformation,[status(thm)],[f192])).
% 0.17/0.52 fof(f198,plain,(
% 0.17/0.52 ![W0]: ((~sP0_prd(W0)|((~aSet0(W0)|(?[W1]: (aElementOf0(W1,W0)&~aElementOf0(W1,xU))))&~aSubsetOf0(W0,xU)))&(sP0_prd(W0)|((aSet0(W0)&(![W1]: (~aElementOf0(W1,W0)|aElementOf0(W1,xU))))|aSubsetOf0(W0,xU))))),
% 0.17/0.52 inference(NNF_transformation,[status(thm)],[f135])).
% 0.17/0.52 fof(f199,plain,(
% 0.17/0.52 (![W0]: (~sP0_prd(W0)|((~aSet0(W0)|(?[W1]: (aElementOf0(W1,W0)&~aElementOf0(W1,xU))))&~aSubsetOf0(W0,xU))))&(![W0]: (sP0_prd(W0)|((aSet0(W0)&(![W1]: (~aElementOf0(W1,W0)|aElementOf0(W1,xU))))|aSubsetOf0(W0,xU))))),
% 0.17/0.52 inference(miniscoping,[status(thm)],[f198])).
% 0.17/0.52 fof(f200,plain,(
% 0.17/0.52 (![W0]: (~sP0_prd(W0)|((~aSet0(W0)|(aElementOf0(sK17_skl(W0),W0)&~aElementOf0(sK17_skl(W0),xU)))&~aSubsetOf0(W0,xU))))&(![W0]: (sP0_prd(W0)|((aSet0(W0)&(![W1]: (~aElementOf0(W1,W0)|aElementOf0(W1,xU))))|aSubsetOf0(W0,xU))))),
% 0.17/0.52 inference(skolemize,[status(esa),new_symbols(skolem,[sK17_skl]),skolemize(W1,sK17_skl(W0))],[f199])).
% 0.17/0.52 fof(f203,plain,(
% 0.17/0.52 ![X0]: (~sP0_prd(X0)|~aSubsetOf0(X0,xU))),
% 0.17/0.52 inference(cnf_transformation,[status(thm)],[f200])).
% 0.17/0.52 fof(f252,plain,(
% 0.17/0.52 ![X0]: (~aSet0(X0)|aSubsetOf0(xP,X0)|aElementOf0(sK1_skl(xP,X0),xP))),
% 0.17/0.52 inference(resolution,[status(thm)],[f49,f179])).
% 0.17/0.52 fof(f302,plain,(
% 0.17/0.52 aSubsetOf0(xP,xU)|aElementOf0(sK1_skl(xP,xU),xP)),
% 0.17/0.52 inference(resolution,[status(thm)],[f252,f139])).
% 0.17/0.52 fof(f328,plain,(
% 0.17/0.52 sP0_prd(xP)),
% 0.17/0.52 inference(resolution,[status(thm)],[f147,f197])).
% 0.17/0.52 fof(f332,plain,(
% 0.17/0.52 ~aSubsetOf0(xP,xU)),
% 0.17/0.52 inference(resolution,[status(thm)],[f328,f203])).
% 0.17/0.52 fof(f333,plain,(
% 0.17/0.52 aElementOf0(sK1_skl(xP,xU),xP)),
% 0.17/0.52 inference(backward_subsumption_resolution,[status(thm)],[f302,f332])).
% 0.17/0.52 fof(f336,plain,(
% 0.17/0.52 aElementOf0(sK1_skl(xP,xU),xU)),
% 0.17/0.52 inference(resolution,[status(thm)],[f333,f180])).
% 0.17/0.52 fof(f343,plain,(
% 0.17/0.52 ~aSet0(xU)|aSubsetOf0(xP,xU)|~aSet0(xP)),
% 0.17/0.52 inference(resolution,[status(thm)],[f336,f50])).
% 0.17/0.52 fof(f346,plain,(
% 0.17/0.52 aSubsetOf0(xP,xU)|~aSet0(xP)),
% 0.17/0.52 inference(forward_subsumption_resolution,[status(thm)],[f343,f139])).
% 0.17/0.52 fof(f347,plain,(
% 0.17/0.52 aSubsetOf0(xP,xU)),
% 0.17/0.52 inference(resolution,[status(thm)],[f346,f179])).
% 0.17/0.52 fof(f348,plain,(
% 0.17/0.52 $false),
% 0.17/0.52 inference(forward_subsumption_resolution,[status(thm)],[f347,f332])).
% 0.17/0.52 % SZS output end CNFRefutation for theBenchmark.p
% 0.22/0.56 % Elapsed time: 0.083508 seconds
% 0.22/0.56 % CPU time: 0.188961 seconds
% 0.22/0.56 % Total memory used: 47.292 MB
% 0.22/0.56 % Net memory used: 47.225 MB
%------------------------------------------------------------------------------