%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT387+4 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n003.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 10.86s 1.88s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LAT387+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.37 % Computer : n003.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Sun Sep 20 23:59:30 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.42 % Drodi V4.1.1
% 10.86/1.88 % Refutation found
% 10.86/1.88 % SZS status Theorem for theBenchmark: Theorem is valid
% 10.86/1.88 % SZS output start CNFRefutation for theBenchmark
% 10.86/1.88 fof(f3,axiom,(
% 10.86/1.88 (! [W0] :( aSet0(W0)=> (! [W1] :( aElementOf0(W1,W0)=> aElement0(W1) ) )) )),
% 10.86/1.88 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.86/1.88 fof(f5,definition,(
% 10.86/1.88 (! [W0] :( aSet0(W0)=> (! [W1] :( aSubsetOf0(W1,W0)<=> ( aSet0(W1)& (! [W2] :( aElementOf0(W2,W1)=> aElementOf0(W2,W0) ) )) ) )) )),
% 10.86/1.88 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.86/1.88 fof(f7,axiom,(
% 10.86/1.88 (! [W0] :( aElement0(W0)=> sdtlseqdt0(W0,W0) ) )),
% 10.86/1.88 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.86/1.88 fof(f8,axiom,(
% 10.86/1.88 (! [W0,W1] :( ( aElement0(W0)& aElement0(W1) )=> ( ( sdtlseqdt0(W0,W1)& sdtlseqdt0(W1,W0) )=> W0 = W1 ) ) )),
% 10.86/1.88 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.86/1.88 fof(f9,axiom,(
% 10.86/1.88 (! [W0,W1,W2] :( ( aElement0(W0)& aElement0(W1)& aElement0(W2) )=> ( ( sdtlseqdt0(W0,W1)& sdtlseqdt0(W1,W2) )=> sdtlseqdt0(W0,W2) ) ) )),
% 10.86/1.88 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.86/1.88 fof(f11,definition,(
% 10.86/1.88 (! [W0] :( aSet0(W0)=> (! [W1] :( aSubsetOf0(W1,W0)=> (! [W2] :( aUpperBoundOfIn0(W2,W1,W0)<=> ( aElementOf0(W2,W0)& (! [W3] :( aElementOf0(W3,W1)=> sdtlseqdt0(W3,W2) ) )) ) )) )) )),
% 10.86/1.88 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.86/1.88 fof(f24,hypothesis,(
% 10.86/1.88 ( 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) ) ),
% 10.86/1.88 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.86/1.88 fof(f25,hypothesis,(
% 10.86/1.88 ( aSet0(xS)& (! [W0] :( ( aElementOf0(W0,xS)=> ( aElementOf0(W0,szDzozmdt0(xf))& sdtlpdtrp0(xf,W0) = W0& aFixedPointOf0(W0,xf) ) )& ( ( ( aElementOf0(W0,szDzozmdt0(xf))& sdtlpdtrp0(xf,W0) = W0 )| aFixedPointOf0(W0,xf) )=> aElementOf0(W0,xS) ) ))& xS = cS1142(xf) ) ),
% 10.86/1.88 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.86/1.88 fof(f26,hypothesis,(
% 10.86/1.88 ( aSet0(xT)& (! [W0] :( aElementOf0(W0,xT)=> aElementOf0(W0,xS) ))& aSubsetOf0(xT,xS) ) ),
% 10.86/1.88 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.86/1.88 fof(f27,hypothesis,(
% 10.86/1.88 ( 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) ) ),
% 10.86/1.88 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.86/1.88 fof(f28,hypothesis,(
% 10.86/1.88 ( aElementOf0(xp,xU)& aElementOf0(xp,xU)& (! [W0] :( aElementOf0(W0,xP)=> sdtlseqdt0(xp,W0) ))& aLowerBoundOfIn0(xp,xP,xU)& (! [W0] :( ( ( aElementOf0(W0,xU)& (! [W1] :( aElementOf0(W1,xP)=> sdtlseqdt0(W0,W1) ) ))| aLowerBoundOfIn0(W0,xP,xU) )=> sdtlseqdt0(W0,xp) ))& aInfimumOfIn0(xp,xP,xU) ) ),
% 10.86/1.88 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.86/1.88 fof(f29,hypothesis,(
% 10.86/1.88 ( (! [W0] :( aElementOf0(W0,xP)=> sdtlseqdt0(sdtlpdtrp0(xf,xp),W0) ))& aLowerBoundOfIn0(sdtlpdtrp0(xf,xp),xP,xU)& (! [W0] :( aElementOf0(W0,xT)=> sdtlseqdt0(W0,sdtlpdtrp0(xf,xp)) ))& aUpperBoundOfIn0(sdtlpdtrp0(xf,xp),xT,xU) ) ),
% 10.86/1.88 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.86/1.88 fof(f30,conjecture,(
% 10.86/1.88 ( ( ( aElementOf0(xp,szDzozmdt0(xf))& sdtlpdtrp0(xf,xp) = xp )| aFixedPointOf0(xp,xf) )& ( ( ( (! [W0] :( aElementOf0(W0,xT)=> sdtlseqdt0(W0,xp) ))| aUpperBoundOfIn0(xp,xT,xS) )& (! [W0] :( ( aElementOf0(W0,xS)& (! [W1] :( aElementOf0(W1,xT)=> sdtlseqdt0(W1,W0) ))& aUpperBoundOfIn0(W0,xT,xS) )=> sdtlseqdt0(xp,W0) ) ))| aSupremumOfIn0(xp,xT,xS) ) ) ),
% 10.86/1.88 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.86/1.88 fof(f31,negated_conjecture,(
% 10.86/1.88 ~(( ( ( aElementOf0(xp,szDzozmdt0(xf))& sdtlpdtrp0(xf,xp) = xp )| aFixedPointOf0(xp,xf) )& ( ( ( (! [W0] :( aElementOf0(W0,xT)=> sdtlseqdt0(W0,xp) ))| aUpperBoundOfIn0(xp,xT,xS) )& (! [W0] :( ( aElementOf0(W0,xS)& (! [W1] :( aElementOf0(W1,xT)=> sdtlseqdt0(W1,W0) ))& aUpperBoundOfIn0(W0,xT,xS) )=> sdtlseqdt0(xp,W0) ) ))| aSupremumOfIn0(xp,xT,xS) ) ) )),
% 10.86/1.88 inference(negated_conjecture,[status(cth)],[f30])).
% 10.86/1.88 fof(f38,plain,(
% 10.86/1.88 ![W0]: (~aSet0(W0)|(![W1]: (~aElementOf0(W1,W0)|aElement0(W1))))),
% 10.86/1.88 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 10.86/1.88 fof(f39,plain,(
% 10.86/1.88 ![X0,X1]: (~aSet0(X0)|~aElementOf0(X1,X0)|aElement0(X1))),
% 10.86/1.88 inference(cnf_transformation,[status(thm)],[f38])).
% 10.86/1.88 fof(f45,plain,(
% 10.86/1.88 ![W0]: (~aSet0(W0)|(![W1]: (aSubsetOf0(W1,W0)<=>(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0)))))))),
% 10.86/1.88 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 10.86/1.88 fof(f46,plain,(
% 10.86/1.88 ![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))))))))),
% 10.86/1.88 inference(NNF_transformation,[status(thm)],[f45])).
% 10.86/1.88 fof(f47,plain,(
% 10.86/1.88 ![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))))))))),
% 10.86/1.88 inference(miniscoping,[status(thm)],[f46])).
% 10.86/1.88 fof(f48,plain,(
% 10.86/1.88 ![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)))))))),
% 10.86/1.88 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W2,sK1_skl(W1,W0))],[f47])).
% 10.86/1.88 fof(f50,plain,(
% 10.86/1.88 ![X0,X1,X2]: (~aSet0(X0)|~aSubsetOf0(X1,X0)|~aElementOf0(X2,X1)|aElementOf0(X2,X0))),
% 10.86/1.88 inference(cnf_transformation,[status(thm)],[f48])).
% 10.86/1.88 fof(f51,plain,(
% 10.86/1.88 ![X0,X1]: (~aSet0(X0)|aSubsetOf0(X1,X0)|~aSet0(X1)|aElementOf0(sK1_skl(X1,X0),X1))),
% 10.86/1.88 inference(cnf_transformation,[status(thm)],[f48])).
% 10.86/1.88 fof(f52,plain,(
% 10.86/1.88 ![X0,X1]: (~aSet0(X0)|aSubsetOf0(X1,X0)|~aSet0(X1)|~aElementOf0(sK1_skl(X1,X0),X0))),
% 10.86/1.88 inference(cnf_transformation,[status(thm)],[f48])).
% 10.86/1.88 fof(f55,plain,(
% 10.86/1.88 ![W0]: (~aElement0(W0)|sdtlseqdt0(W0,W0))),
% 10.86/1.88 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 10.86/1.88 fof(f56,plain,(
% 10.86/1.88 ![X0]: (~aElement0(X0)|sdtlseqdt0(X0,X0))),
% 10.86/1.88 inference(cnf_transformation,[status(thm)],[f55])).
% 10.86/1.88 fof(f57,plain,(
% 10.86/1.88 ![W0,W1]: ((~aElement0(W0)|~aElement0(W1))|((~sdtlseqdt0(W0,W1)|~sdtlseqdt0(W1,W0))|W0=W1))),
% 10.86/1.88 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 10.86/1.88 fof(f58,plain,(
% 10.86/1.88 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|~sdtlseqdt0(X0,X1)|~sdtlseqdt0(X1,X0)|X0=X1)),
% 10.86/1.88 inference(cnf_transformation,[status(thm)],[f57])).
% 10.86/1.88 fof(f59,plain,(
% 10.86/1.88 ![W0,W1,W2]: (((~aElement0(W0)|~aElement0(W1))|~aElement0(W2))|((~sdtlseqdt0(W0,W1)|~sdtlseqdt0(W1,W2))|sdtlseqdt0(W0,W2)))),
% 10.86/1.88 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 10.86/1.88 fof(f60,plain,(
% 10.86/1.88 ![X0,X1,X2]: (~aElement0(X0)|~aElement0(X1)|~aElement0(X2)|~sdtlseqdt0(X0,X1)|~sdtlseqdt0(X1,X2)|sdtlseqdt0(X0,X2))),
% 10.86/1.88 inference(cnf_transformation,[status(thm)],[f59])).
% 10.86/1.88 fof(f69,plain,(
% 10.86/1.88 ![W0]: (~aSet0(W0)|(![W1]: (~aSubsetOf0(W1,W0)|(![W2]: (aUpperBoundOfIn0(W2,W1,W0)<=>(aElementOf0(W2,W0)&(![W3]: (~aElementOf0(W3,W1)|sdtlseqdt0(W3,W2)))))))))),
% 10.86/1.88 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 10.86/1.88 fof(f70,plain,(
% 10.86/1.88 ![W0]: (~aSet0(W0)|(![W1]: (~aSubsetOf0(W1,W0)|(![W2]: ((~aUpperBoundOfIn0(W2,W1,W0)|(aElementOf0(W2,W0)&(![W3]: (~aElementOf0(W3,W1)|sdtlseqdt0(W3,W2)))))&(aUpperBoundOfIn0(W2,W1,W0)|(~aElementOf0(W2,W0)|(?[W3]: (aElementOf0(W3,W1)&~sdtlseqdt0(W3,W2))))))))))),
% 10.86/1.88 inference(NNF_transformation,[status(thm)],[f69])).
% 10.86/1.88 fof(f71,plain,(
% 10.86/1.88 ![W0]: (~aSet0(W0)|(![W1]: (~aSubsetOf0(W1,W0)|((![W2]: (~aUpperBoundOfIn0(W2,W1,W0)|(aElementOf0(W2,W0)&(![W3]: (~aElementOf0(W3,W1)|sdtlseqdt0(W3,W2))))))&(![W2]: (aUpperBoundOfIn0(W2,W1,W0)|(~aElementOf0(W2,W0)|(?[W3]: (aElementOf0(W3,W1)&~sdtlseqdt0(W3,W2))))))))))),
% 10.86/1.88 inference(miniscoping,[status(thm)],[f70])).
% 10.86/1.88 fof(f72,plain,(
% 10.86/1.88 ![W0]: (~aSet0(W0)|(![W1]: (~aSubsetOf0(W1,W0)|((![W2]: (~aUpperBoundOfIn0(W2,W1,W0)|(aElementOf0(W2,W0)&(![W3]: (~aElementOf0(W3,W1)|sdtlseqdt0(W3,W2))))))&(![W2]: (aUpperBoundOfIn0(W2,W1,W0)|(~aElementOf0(W2,W0)|(aElementOf0(sK3_skl(W2,W1,W0),W1)&~sdtlseqdt0(sK3_skl(W2,W1,W0),W2)))))))))),
% 10.86/1.88 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(W3,sK3_skl(W2,W1,W0))],[f71])).
% 10.86/1.88 fof(f73,plain,(
% 10.86/1.88 ![X0,X1,X2]: (~aSet0(X0)|~aSubsetOf0(X1,X0)|~aUpperBoundOfIn0(X2,X1,X0)|aElementOf0(X2,X0))),
% 10.86/1.89 inference(cnf_transformation,[status(thm)],[f72])).
% 10.86/1.89 fof(f136,plain,(
% 10.86/1.89 (((((((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)),
% 10.86/1.89 inference(pre_NNF_transformation,[status(thm)],[f24])).
% 10.86/1.89 fof(f137,definition,(
% 10.86/1.89 ![W0]: (sP0_prd(W0)<=>((~aSet0(W0)|(?[W1]: (aElementOf0(W1,W0)&~aElementOf0(W1,xU))))&~aSubsetOf0(W0,xU)))),
% 10.86/1.89 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 10.86/1.89 fof(f138,plain,(
% 10.86/1.89 (((((((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)),
% 10.86/1.89 inference(formula_renaming,[status(thm)],[f136,f137])).
% 10.86/1.89 fof(f139,plain,(
% 10.86/1.89 (((((((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)),
% 10.86/1.89 inference(miniscoping,[status(thm)],[f138])).
% 10.86/1.89 fof(f140,plain,(
% 10.86/1.89 (((((((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)),
% 10.86/1.89 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))],[f139])).
% 10.86/1.89 fof(f141,plain,(
% 10.86/1.89 aSet0(xU)),
% 10.86/1.89 inference(cnf_transformation,[status(thm)],[f140])).
% 10.86/1.89 fof(f160,plain,(
% 10.86/1.89 ![X0,X1]: (~aElementOf0(X0,szDzozmdt0(xf))|~aElementOf0(X1,szDzozmdt0(xf))|~sdtlseqdt0(X0,X1)|sdtlseqdt0(sdtlpdtrp0(xf,X0),sdtlpdtrp0(xf,X1)))),
% 10.86/1.89 inference(cnf_transformation,[status(thm)],[f140])).
% 10.86/1.89 fof(f162,plain,(
% 10.86/1.89 szDzozmdt0(xf)=szRzazndt0(xf)),
% 10.86/1.89 inference(cnf_transformation,[status(thm)],[f140])).
% 10.86/1.89 fof(f163,plain,(
% 10.86/1.89 szRzazndt0(xf)=xU),
% 10.86/1.89 inference(cnf_transformation,[status(thm)],[f140])).
% 10.86/1.89 fof(f165,plain,(
% 10.86/1.89 (aSet0(xS)&(![W0]: ((~aElementOf0(W0,xS)|((aElementOf0(W0,szDzozmdt0(xf))&sdtlpdtrp0(xf,W0)=W0)&aFixedPointOf0(W0,xf)))&(((~aElementOf0(W0,szDzozmdt0(xf))|~sdtlpdtrp0(xf,W0)=W0)&~aFixedPointOf0(W0,xf))|aElementOf0(W0,xS)))))&xS=cS1142(xf)),
% 10.86/1.89 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 10.86/1.89 fof(f166,plain,(
% 10.86/1.89 (aSet0(xS)&((![W0]: (~aElementOf0(W0,xS)|((aElementOf0(W0,szDzozmdt0(xf))&sdtlpdtrp0(xf,W0)=W0)&aFixedPointOf0(W0,xf))))&(![W0]: (((~aElementOf0(W0,szDzozmdt0(xf))|~sdtlpdtrp0(xf,W0)=W0)&~aFixedPointOf0(W0,xf))|aElementOf0(W0,xS)))))&xS=cS1142(xf)),
% 10.86/1.89 inference(miniscoping,[status(thm)],[f165])).
% 10.86/1.89 fof(f167,plain,(
% 10.86/1.89 aSet0(xS)),
% 10.86/1.89 inference(cnf_transformation,[status(thm)],[f166])).
% 10.86/1.89 fof(f168,plain,(
% 10.86/1.89 ![X0]: (~aElementOf0(X0,xS)|aElementOf0(X0,szDzozmdt0(xf)))),
% 10.86/1.89 inference(cnf_transformation,[status(thm)],[f166])).
% 10.86/1.89 fof(f169,plain,(
% 10.86/1.89 ![X0]: (~aElementOf0(X0,xS)|sdtlpdtrp0(xf,X0)=X0)),
% 10.86/1.89 inference(cnf_transformation,[status(thm)],[f166])).
% 10.86/1.89 fof(f174,plain,(
% 10.86/1.89 (aSet0(xT)&(![W0]: (~aElementOf0(W0,xT)|aElementOf0(W0,xS))))&aSubsetOf0(xT,xS)),
% 10.86/1.89 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 10.86/1.89 fof(f175,plain,(
% 10.86/1.89 aSet0(xT)),
% 10.86/1.89 inference(cnf_transformation,[status(thm)],[f174])).
% 10.86/1.89 fof(f176,plain,(
% 10.86/1.89 ![X0]: (~aElementOf0(X0,xT)|aElementOf0(X0,xS))),
% 10.86/1.89 inference(cnf_transformation,[status(thm)],[f174])).
% 10.86/1.89 fof(f178,plain,(
% 10.86/1.89 (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)),
% 10.86/1.89 inference(pre_NNF_transformation,[status(thm)],[f27])).
% 10.86/1.89 fof(f179,plain,(
% 10.86/1.89 (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)),
% 10.86/1.89 inference(miniscoping,[status(thm)],[f178])).
% 10.86/1.89 fof(f180,plain,(
% 10.86/1.89 (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)),
% 10.86/1.89 inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl]),skolemize(W1,sK15_skl(W0))],[f179])).
% 10.86/1.89 fof(f184,plain,(
% 10.86/1.89 ![X0,X1]: (~aElementOf0(X0,xP)|~aElementOf0(X1,xT)|sdtlseqdt0(X1,X0))),
% 10.86/1.89 inference(cnf_transformation,[status(thm)],[f180])).
% 10.86/1.89 fof(f186,plain,(
% 10.86/1.89 ![X0]: (~aElementOf0(X0,xU)|~sdtlseqdt0(sdtlpdtrp0(xf,X0),X0)|aElementOf0(sK15_skl(X0),xT)|aElementOf0(X0,xP))),
% 10.86/1.89 inference(cnf_transformation,[status(thm)],[f180])).
% 10.86/1.89 fof(f187,plain,(
% 10.86/1.89 ![X0]: (~aElementOf0(X0,xU)|~sdtlseqdt0(sdtlpdtrp0(xf,X0),X0)|~sdtlseqdt0(sK15_skl(X0),X0)|aElementOf0(X0,xP))),
% 10.86/1.89 inference(cnf_transformation,[status(thm)],[f180])).
% 10.86/1.89 fof(f188,plain,(
% 10.86/1.89 ![X0]: (~aElementOf0(X0,xU)|~sdtlseqdt0(sdtlpdtrp0(xf,X0),X0)|~aUpperBoundOfIn0(X0,xT,xU)|aElementOf0(X0,xP))),
% 10.86/1.89 inference(cnf_transformation,[status(thm)],[f180])).
% 10.86/1.89 fof(f190,plain,(
% 10.86/1.89 ((((aElementOf0(xp,xU)&aElementOf0(xp,xU))&(![W0]: (~aElementOf0(W0,xP)|sdtlseqdt0(xp,W0))))&aLowerBoundOfIn0(xp,xP,xU))&(![W0]: (((~aElementOf0(W0,xU)|(?[W1]: (aElementOf0(W1,xP)&~sdtlseqdt0(W0,W1))))&~aLowerBoundOfIn0(W0,xP,xU))|sdtlseqdt0(W0,xp))))&aInfimumOfIn0(xp,xP,xU)),
% 10.86/1.89 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 10.86/1.89 fof(f191,plain,(
% 10.86/1.89 ((((aElementOf0(xp,xU)&aElementOf0(xp,xU))&(![W0]: (~aElementOf0(W0,xP)|sdtlseqdt0(xp,W0))))&aLowerBoundOfIn0(xp,xP,xU))&(![W0]: (((~aElementOf0(W0,xU)|(aElementOf0(sK16_skl(W0),xP)&~sdtlseqdt0(W0,sK16_skl(W0))))&~aLowerBoundOfIn0(W0,xP,xU))|sdtlseqdt0(W0,xp))))&aInfimumOfIn0(xp,xP,xU)),
% 10.86/1.89 inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl]),skolemize(W1,sK16_skl(W0))],[f190])).
% 10.86/1.89 fof(f192,plain,(
% 10.86/1.89 aElementOf0(xp,xU)),
% 10.86/1.89 inference(cnf_transformation,[status(thm)],[f191])).
% 10.86/1.89 fof(f194,plain,(
% 10.86/1.89 ![X0]: (~aElementOf0(X0,xP)|sdtlseqdt0(xp,X0))),
% 10.86/1.89 inference(cnf_transformation,[status(thm)],[f191])).
% 10.86/1.89 fof(f196,plain,(
% 10.86/1.89 ![X0]: (~aElementOf0(X0,xU)|aElementOf0(sK16_skl(X0),xP)|sdtlseqdt0(X0,xp))),
% 10.86/1.89 inference(cnf_transformation,[status(thm)],[f191])).
% 10.86/1.89 fof(f197,plain,(
% 10.86/1.89 ![X0]: (~aElementOf0(X0,xU)|~sdtlseqdt0(X0,sK16_skl(X0))|sdtlseqdt0(X0,xp))),
% 10.86/1.89 inference(cnf_transformation,[status(thm)],[f191])).
% 10.86/1.89 fof(f198,plain,(
% 10.86/1.89 ![X0]: (~aLowerBoundOfIn0(X0,xP,xU)|sdtlseqdt0(X0,xp))),
% 10.86/1.89 inference(cnf_transformation,[status(thm)],[f191])).
% 10.86/1.89 fof(f200,plain,(
% 10.86/1.89 (((![W0]: (~aElementOf0(W0,xP)|sdtlseqdt0(sdtlpdtrp0(xf,xp),W0)))&aLowerBoundOfIn0(sdtlpdtrp0(xf,xp),xP,xU))&(![W0]: (~aElementOf0(W0,xT)|sdtlseqdt0(W0,sdtlpdtrp0(xf,xp)))))&aUpperBoundOfIn0(sdtlpdtrp0(xf,xp),xT,xU)),
% 10.86/1.89 inference(pre_NNF_transformation,[status(thm)],[f29])).
% 10.86/1.89 fof(f201,plain,(
% 10.86/1.89 ![X0]: (~aElementOf0(X0,xP)|sdtlseqdt0(sdtlpdtrp0(xf,xp),X0))),
% 10.86/1.89 inference(cnf_transformation,[status(thm)],[f200])).
% 10.86/1.89 fof(f202,plain,(
% 10.86/1.89 aLowerBoundOfIn0(sdtlpdtrp0(xf,xp),xP,xU)),
% 10.86/1.89 inference(cnf_transformation,[status(thm)],[f200])).
% 10.86/1.89 fof(f204,plain,(
% 10.86/1.89 aUpperBoundOfIn0(sdtlpdtrp0(xf,xp),xT,xU)),
% 10.86/1.89 inference(cnf_transformation,[status(thm)],[f200])).
% 10.86/1.89 fof(f205,plain,(
% 10.86/1.89 (((~aElementOf0(xp,szDzozmdt0(xf))|~sdtlpdtrp0(xf,xp)=xp)&~aFixedPointOf0(xp,xf))|((((?[W0]: (aElementOf0(W0,xT)&~sdtlseqdt0(W0,xp)))&~aUpperBoundOfIn0(xp,xT,xS))|(?[W0]: (((aElementOf0(W0,xS)&(![W1]: (~aElementOf0(W1,xT)|sdtlseqdt0(W1,W0))))&aUpperBoundOfIn0(W0,xT,xS))&~sdtlseqdt0(xp,W0))))&~aSupremumOfIn0(xp,xT,xS)))),
% 10.86/1.89 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 10.86/1.89 fof(f206,definition,(
% 10.86/1.89 sP1_prd<=>((~aElementOf0(xp,szDzozmdt0(xf))|~sdtlpdtrp0(xf,xp)=xp)&~aFixedPointOf0(xp,xf))),
% 10.86/1.89 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 10.86/1.89 fof(f207,plain,(
% 10.86/1.89 sP1_prd|((((?[W0]: (aElementOf0(W0,xT)&~sdtlseqdt0(W0,xp)))&~aUpperBoundOfIn0(xp,xT,xS))|(?[W0]: (((aElementOf0(W0,xS)&(![W1]: (~aElementOf0(W1,xT)|sdtlseqdt0(W1,W0))))&aUpperBoundOfIn0(W0,xT,xS))&~sdtlseqdt0(xp,W0))))&~aSupremumOfIn0(xp,xT,xS))),
% 10.86/1.89 inference(formula_renaming,[status(thm)],[f205,f206])).
% 10.86/1.89 fof(f208,definition,(
% 10.86/1.89 sP2_prd<=>((?[W0]: (aElementOf0(W0,xT)&~sdtlseqdt0(W0,xp)))&~aUpperBoundOfIn0(xp,xT,xS))),
% 10.86/1.89 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 10.86/1.89 fof(f209,plain,(
% 10.86/1.89 sP1_prd|((sP2_prd|(?[W0]: (((aElementOf0(W0,xS)&(![W1]: (~aElementOf0(W1,xT)|sdtlseqdt0(W1,W0))))&aUpperBoundOfIn0(W0,xT,xS))&~sdtlseqdt0(xp,W0))))&~aSupremumOfIn0(xp,xT,xS))),
% 10.86/1.89 inference(formula_renaming,[status(thm)],[f207,f208])).
% 10.86/1.89 fof(f210,plain,(
% 10.86/1.89 sP1_prd|((sP2_prd|(((aElementOf0(sK17_skl,xS)&(![W1]: (~aElementOf0(W1,xT)|sdtlseqdt0(W1,sK17_skl))))&aUpperBoundOfIn0(sK17_skl,xT,xS))&~sdtlseqdt0(xp,sK17_skl)))&~aSupremumOfIn0(xp,xT,xS))),
% 10.86/1.89 inference(skolemize,[status(esa),new_symbols(skolem,[sK17_skl]),skolemize(W0,sK17_skl)],[f209])).
% 10.86/1.89 fof(f211,plain,(
% 10.86/1.89 sP1_prd|sP2_prd|aElementOf0(sK17_skl,xS)),
% 10.86/1.89 inference(cnf_transformation,[status(thm)],[f210])).
% 10.86/1.89 fof(f212,plain,(
% 10.86/1.89 ![X0]: (sP1_prd|sP2_prd|~aElementOf0(X0,xT)|sdtlseqdt0(X0,sK17_skl))),
% 10.86/1.89 inference(cnf_transformation,[status(thm)],[f210])).
% 10.86/1.89 fof(f214,plain,(
% 10.86/1.89 sP1_prd|sP2_prd|~sdtlseqdt0(xp,sK17_skl)),
% 10.86/1.89 inference(cnf_transformation,[status(thm)],[f210])).
% 10.86/1.89 fof(f224,plain,(
% 10.86/1.89 (~sP1_prd|((~aElementOf0(xp,szDzozmdt0(xf))|~sdtlpdtrp0(xf,xp)=xp)&~aFixedPointOf0(xp,xf)))&(sP1_prd|((aElementOf0(xp,szDzozmdt0(xf))&sdtlpdtrp0(xf,xp)=xp)|aFixedPointOf0(xp,xf)))),
% 10.86/1.89 inference(NNF_transformation,[status(thm)],[f206])).
% 10.86/1.89 fof(f225,plain,(
% 10.86/1.89 ~sP1_prd|~aElementOf0(xp,szDzozmdt0(xf))|~sdtlpdtrp0(xf,xp)=xp),
% 10.86/1.89 inference(cnf_transformation,[status(thm)],[f224])).
% 10.86/1.89 fof(f229,plain,(
% 10.86/1.89 (~sP2_prd|((?[W0]: (aElementOf0(W0,xT)&~sdtlseqdt0(W0,xp)))&~aUpperBoundOfIn0(xp,xT,xS)))&(sP2_prd|((![W0]: (~aElementOf0(W0,xT)|sdtlseqdt0(W0,xp)))|aUpperBoundOfIn0(xp,xT,xS)))),
% 10.86/1.89 inference(NNF_transformation,[status(thm)],[f208])).
% 10.86/1.89 fof(f230,plain,(
% 10.86/1.89 (~sP2_prd|((aElementOf0(sK19_skl,xT)&~sdtlseqdt0(sK19_skl,xp))&~aUpperBoundOfIn0(xp,xT,xS)))&(sP2_prd|((![W0]: (~aElementOf0(W0,xT)|sdtlseqdt0(W0,xp)))|aUpperBoundOfIn0(xp,xT,xS)))),
% 10.86/1.89 inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl]),skolemize(W0,sK19_skl)],[f229])).
% 10.86/1.89 fof(f231,plain,(
% 10.86/1.89 ~sP2_prd|aElementOf0(sK19_skl,xT)),
% 10.86/1.89 inference(cnf_transformation,[status(thm)],[f230])).
% 10.86/1.89 fof(f232,plain,(
% 10.86/1.89 ~sP2_prd|~sdtlseqdt0(sK19_skl,xp)),
% 10.86/1.89 inference(cnf_transformation,[status(thm)],[f230])).
% 10.86/1.89 fof(f236,plain,(
% 10.86/1.89 ~aSet0(xS)|aElement0(sK17_skl)|sP1_prd|sP2_prd),
% 10.86/1.89 inference(resolution,[status(thm)],[f39,f211])).
% 10.86/1.89 fof(f237,plain,(
% 10.86/1.89 aElement0(sK17_skl)|sP1_prd|sP2_prd),
% 10.86/1.89 inference(forward_subsumption_resolution,[status(thm)],[f236,f167])).
% 10.86/1.89 fof(f254,plain,(
% 10.86/1.89 ~aSet0(xU)|aElement0(xp)),
% 10.86/1.89 inference(resolution,[status(thm)],[f192,f39])).
% 10.86/1.89 fof(f255,plain,(
% 10.86/1.89 aElement0(xp)),
% 10.86/1.89 inference(forward_subsumption_resolution,[status(thm)],[f254,f141])).
% 10.86/1.89 fof(f258,plain,(
% 10.86/1.89 ![X0]: (~aElement0(X0)|~sdtlseqdt0(X0,xp)|~sdtlseqdt0(xp,X0)|X0=xp)),
% 10.86/1.89 inference(resolution,[status(thm)],[f58,f255])).
% 10.86/1.89 fof(f263,plain,(
% 10.86/1.89 ![X0,X1]: (sP1_prd|sP2_prd|~aElement0(X0)|~aElement0(X1)|~sdtlseqdt0(X0,X1)|~sdtlseqdt0(X1,sK17_skl)|sdtlseqdt0(X0,sK17_skl))),
% 10.86/1.89 inference(resolution,[status(thm)],[f237,f60])).
% 10.86/1.89 fof(f268,plain,(
% 10.86/1.89 ![X0]: (~aElementOf0(sK1_skl(X0,szDzozmdt0(xf)),xS)|~aSet0(szDzozmdt0(xf))|aSubsetOf0(X0,szDzozmdt0(xf))|~aSet0(X0))),
% 10.86/1.89 inference(resolution,[status(thm)],[f168,f52])).
% 10.86/1.89 fof(f272,plain,(
% 10.86/1.89 sdtlpdtrp0(xf,sK17_skl)=sK17_skl|sP1_prd|sP2_prd),
% 10.86/1.89 inference(resolution,[status(thm)],[f169,f211])).
% 10.86/1.89 fof(f299,plain,(
% 10.86/1.89 ![X0]: (aElementOf0(sK1_skl(xT,X0),xS)|~aSet0(X0)|aSubsetOf0(xT,X0)|~aSet0(xT))),
% 10.86/1.89 inference(resolution,[status(thm)],[f176,f51])).
% 10.86/1.89 fof(f301,plain,(
% 10.86/1.89 ![X0]: (aElementOf0(sK1_skl(xT,X0),xS)|~aSet0(X0)|aSubsetOf0(xT,X0))),
% 10.86/1.89 inference(forward_subsumption_resolution,[status(thm)],[f299,f175])).
% 10.86/1.89 fof(f394,plain,(
% 10.86/1.89 sdtlpdtrp0(xf,sK17_skl)=sK17_skl|sP1_prd|~sdtlseqdt0(sK19_skl,xp)),
% 10.86/1.89 inference(resolution,[status(thm)],[f272,f232])).
% 10.86/1.89 fof(f395,plain,(
% 10.86/1.89 sdtlpdtrp0(xf,sK17_skl)=sK17_skl|sP1_prd|aElementOf0(sK19_skl,xT)),
% 10.86/1.89 inference(resolution,[status(thm)],[f272,f231])).
% 10.86/1.89 fof(f415,plain,(
% 10.86/1.89 ![X0]: (~aElementOf0(sK1_skl(X0,szDzozmdt0(xf)),xS)|~aSet0(szDzozmdt0(xf))|aSubsetOf0(X0,xU)|~aSet0(X0))),
% 10.86/1.89 inference(backward_demodulation,[status(thm)],[f422,f268])).
% 10.86/1.89 fof(f419,plain,(
% 10.86/1.89 ![X0]: (~aElementOf0(X0,xS)|aElementOf0(X0,xU))),
% 10.86/1.89 inference(backward_demodulation,[status(thm)],[f422,f168])).
% 10.86/1.89 fof(f420,plain,(
% 10.86/1.89 ![X0,X1]: (~aElementOf0(X0,szDzozmdt0(xf))|~aElementOf0(X1,xU)|~sdtlseqdt0(X0,X1)|sdtlseqdt0(sdtlpdtrp0(xf,X0),sdtlpdtrp0(xf,X1)))),
% 10.86/1.89 inference(backward_demodulation,[status(thm)],[f422,f160])).
% 10.86/1.89 fof(f421,plain,(
% 10.86/1.89 ~sP1_prd|~aElementOf0(xp,xU)|~sdtlpdtrp0(xf,xp)=xp),
% 10.86/1.89 inference(backward_demodulation,[status(thm)],[f422,f225])).
% 10.86/1.89 fof(f422,plain,(
% 10.86/1.89 szDzozmdt0(xf)=xU),
% 10.86/1.89 inference(forward_demodulation,[status(thm)],[f163,f162])).
% 10.86/1.89 fof(f425,plain,(
% 10.86/1.89 ![X0]: (~aElementOf0(sK1_skl(X0,xU),xS)|~aSet0(szDzozmdt0(xf))|aSubsetOf0(X0,xU)|~aSet0(X0))),
% 10.86/1.89 inference(forward_demodulation,[status(thm)],[f422,f415])).
% 10.86/1.89 fof(f426,plain,(
% 10.86/1.89 ![X0]: (~aElementOf0(sK1_skl(X0,xU),xS)|~aSet0(xU)|aSubsetOf0(X0,xU)|~aSet0(X0))),
% 10.86/1.89 inference(forward_demodulation,[status(thm)],[f422,f425])).
% 10.86/1.89 fof(f427,plain,(
% 10.86/1.89 ![X0]: (~aElementOf0(sK1_skl(X0,xU),xS)|aSubsetOf0(X0,xU)|~aSet0(X0))),
% 10.86/1.89 inference(forward_subsumption_resolution,[status(thm)],[f426,f141])).
% 10.86/1.89 fof(f428,plain,(
% 10.86/1.89 ![X0,X1]: (~aElementOf0(X0,xU)|~aElementOf0(X1,xU)|~sdtlseqdt0(X0,X1)|sdtlseqdt0(sdtlpdtrp0(xf,X0),sdtlpdtrp0(xf,X1)))),
% 10.86/1.89 inference(forward_demodulation,[status(thm)],[f422,f420])).
% 10.86/1.89 fof(f429,plain,(
% 10.86/1.89 ~sP1_prd|~sdtlpdtrp0(xf,xp)=xp),
% 10.86/1.89 inference(forward_subsumption_resolution,[status(thm)],[f421,f192])).
% 10.86/1.89 fof(f475,plain,(
% 10.86/1.89 aElementOf0(sK17_skl,xU)|sP1_prd|sP2_prd),
% 10.86/1.89 inference(resolution,[status(thm)],[f419,f211])).
% 10.86/1.89 fof(f557,plain,(
% 10.86/1.89 ![X0]: (sP1_prd|sP2_prd|~aElement0(xp)|~aElement0(X0)|~sdtlseqdt0(xp,X0)|~sdtlseqdt0(X0,sK17_skl)|sP1_prd|sP2_prd)),
% 10.86/1.89 inference(resolution,[status(thm)],[f263,f214])).
% 10.86/1.89 fof(f558,plain,(
% 10.86/1.89 ![X0]: (sP1_prd|sP2_prd|~aElement0(xp)|~aElement0(X0)|~sdtlseqdt0(xp,X0)|~sdtlseqdt0(X0,sK17_skl))),
% 10.86/1.89 inference(duplicate_literals_removal,[status(thm)],[f557])).
% 10.86/1.89 fof(f559,plain,(
% 10.86/1.89 ![X0]: (sP1_prd|sP2_prd|~aElement0(X0)|~sdtlseqdt0(xp,X0)|~sdtlseqdt0(X0,sK17_skl))),
% 10.86/1.89 inference(forward_subsumption_resolution,[status(thm)],[f558,f255])).
% 10.86/1.89 fof(f678,plain,(
% 10.86/1.89 aSubsetOf0(xT,xU)|~aSet0(xT)|~aSet0(xU)|aSubsetOf0(xT,xU)),
% 10.86/1.89 inference(resolution,[status(thm)],[f427,f301])).
% 10.86/1.89 fof(f681,plain,(
% 10.86/1.89 aSubsetOf0(xT,xU)|~aSet0(xT)|~aSet0(xU)),
% 10.86/1.89 inference(duplicate_literals_removal,[status(thm)],[f678])).
% 10.86/1.89 fof(f682,plain,(
% 10.86/1.89 aSubsetOf0(xT,xU)|~aSet0(xU)),
% 10.86/1.89 inference(forward_subsumption_resolution,[status(thm)],[f681,f175])).
% 10.86/1.89 fof(f696,plain,(
% 10.86/1.89 aSubsetOf0(xT,xU)),
% 10.86/1.89 inference(forward_subsumption_resolution,[status(thm)],[f682,f141])).
% 10.86/1.89 fof(f700,plain,(
% 10.86/1.89 ![X0]: (~aSet0(xU)|~aElementOf0(X0,xT)|aElementOf0(X0,xU))),
% 10.86/1.89 inference(resolution,[status(thm)],[f696,f50])).
% 10.86/1.89 fof(f704,plain,(
% 10.86/1.89 ![X0]: (~aSet0(xU)|~aUpperBoundOfIn0(X0,xT,xU)|aElementOf0(X0,xU))),
% 10.86/1.89 inference(resolution,[status(thm)],[f696,f73])).
% 10.86/1.89 fof(f708,plain,(
% 10.86/1.89 ![X0]: (~aElementOf0(X0,xT)|aElementOf0(X0,xU))),
% 10.86/1.89 inference(forward_subsumption_resolution,[status(thm)],[f700,f141])).
% 10.86/1.89 fof(f711,plain,(
% 10.86/1.89 ![X0]: (~aUpperBoundOfIn0(X0,xT,xU)|aElementOf0(X0,xU))),
% 10.86/1.89 inference(forward_subsumption_resolution,[status(thm)],[f704,f141])).
% 10.86/1.89 fof(f717,plain,(
% 10.86/1.89 ~sdtlseqdt0(sdtlpdtrp0(xf,sK17_skl),sK17_skl)|aElementOf0(sK15_skl(sK17_skl),xT)|aElementOf0(sK17_skl,xP)|sP1_prd|sP2_prd),
% 10.86/1.89 inference(resolution,[status(thm)],[f186,f475])).
% 10.86/1.89 fof(f724,plain,(
% 10.86/1.89 ~aElementOf0(sK17_skl,xU)|~sdtlseqdt0(sdtlpdtrp0(xf,sK17_skl),sK17_skl)|aElementOf0(sK17_skl,xP)|sP1_prd|sP2_prd|~aElementOf0(sK15_skl(sK17_skl),xT)),
% 10.86/1.89 inference(resolution,[status(thm)],[f187,f212])).
% 10.86/1.89 fof(f730,plain,(
% 10.86/1.89 ~sdtlseqdt0(sdtlpdtrp0(xf,sK17_skl),sK17_skl)|aElementOf0(sK17_skl,xP)|sP1_prd|sP2_prd|~aElementOf0(sK15_skl(sK17_skl),xT)),
% 10.86/1.89 inference(forward_subsumption_resolution,[status(thm)],[f724,f475])).
% 10.86/1.89 fof(f733,plain,(
% 10.86/1.89 ~aElementOf0(sdtlpdtrp0(xf,xp),xU)|~sdtlseqdt0(sdtlpdtrp0(xf,sdtlpdtrp0(xf,xp)),sdtlpdtrp0(xf,xp))|aElementOf0(sdtlpdtrp0(xf,xp),xP)),
% 10.86/1.89 inference(resolution,[status(thm)],[f188,f204])).
% 10.86/1.89 fof(f737,plain,(
% 10.86/1.89 ![X0,X1]: (~aElementOf0(X0,xU)|sdtlseqdt0(X0,xp)|~aElementOf0(X1,xT)|sdtlseqdt0(X1,sK16_skl(X0)))),
% 10.86/1.89 inference(resolution,[status(thm)],[f196,f184])).
% 10.86/1.89 fof(f829,plain,(
% 10.86/1.89 sdtlseqdt0(sdtlpdtrp0(xf,xp),xp)),
% 10.86/1.89 inference(resolution,[status(thm)],[f202,f198])).
% 10.86/1.89 fof(f1031,plain,(
% 10.86/1.89 ~sdtlseqdt0(sdtlpdtrp0(xf,sK17_skl),sK17_skl)|aElementOf0(sK17_skl,xP)|sP1_prd|sP2_prd),
% 10.86/1.89 inference(forward_subsumption_resolution,[status(thm)],[f717,f730])).
% 10.86/1.89 fof(f1139,plain,(
% 10.86/1.89 aElementOf0(sdtlpdtrp0(xf,xp),xU)),
% 10.86/1.89 inference(resolution,[status(thm)],[f711,f204])).
% 10.86/1.89 fof(f1148,plain,(
% 10.86/1.89 ~aSet0(xU)|aElement0(sdtlpdtrp0(xf,xp))),
% 10.86/1.89 inference(resolution,[status(thm)],[f1139,f39])).
% 10.86/1.89 fof(f1149,plain,(
% 10.86/1.89 aElement0(sdtlpdtrp0(xf,xp))),
% 10.86/1.89 inference(forward_subsumption_resolution,[status(thm)],[f1148,f141])).
% 10.86/1.89 fof(f1158,plain,(
% 10.86/1.89 ~sdtlseqdt0(sdtlpdtrp0(xf,sdtlpdtrp0(xf,xp)),sdtlpdtrp0(xf,xp))|aElementOf0(sdtlpdtrp0(xf,xp),xP)),
% 10.86/1.89 inference(forward_subsumption_resolution,[status(thm)],[f733,f1139])).
% 10.86/1.89 fof(f1159,plain,(
% 10.86/1.89 aElementOf0(sdtlpdtrp0(xf,xp),xP)|~aElementOf0(sdtlpdtrp0(xf,xp),xU)|~aElementOf0(xp,xU)|~sdtlseqdt0(sdtlpdtrp0(xf,xp),xp)),
% 10.86/1.89 inference(resolution,[status(thm)],[f1158,f428])).
% 10.86/1.89 fof(f1164,plain,(
% 10.86/1.89 aElementOf0(sdtlpdtrp0(xf,xp),xP)|~aElementOf0(xp,xU)|~sdtlseqdt0(sdtlpdtrp0(xf,xp),xp)),
% 10.86/1.89 inference(forward_subsumption_resolution,[status(thm)],[f1159,f1139])).
% 10.86/1.89 fof(f1364,plain,(
% 10.86/1.89 sP1_prd|sP2_prd|~aElement0(sdtlpdtrp0(xf,xp))|~sdtlseqdt0(xp,sdtlpdtrp0(xf,xp))|~aElementOf0(sK17_skl,xP)),
% 10.86/1.89 inference(resolution,[status(thm)],[f559,f201])).
% 10.86/1.89 fof(f1372,plain,(
% 10.86/1.89 sP1_prd|sP2_prd|~sdtlseqdt0(xp,sdtlpdtrp0(xf,xp))|~aElementOf0(sK17_skl,xP)),
% 10.86/1.89 inference(forward_subsumption_resolution,[status(thm)],[f1364,f1149])).
% 10.86/1.89 fof(f1387,plain,(
% 10.86/1.89 ~sdtlseqdt0(sdtlpdtrp0(xf,xp),xp)|~sdtlseqdt0(xp,sdtlpdtrp0(xf,xp))|sdtlpdtrp0(xf,xp)=xp),
% 10.86/1.89 inference(resolution,[status(thm)],[f258,f1149])).
% 10.86/1.89 fof(f1398,plain,(
% 10.86/1.89 ~sdtlseqdt0(xp,sdtlpdtrp0(xf,xp))|sdtlpdtrp0(xf,xp)=xp),
% 10.86/1.89 inference(forward_subsumption_resolution,[status(thm)],[f1387,f829])).
% 10.86/1.89 fof(f1594,plain,(
% 10.86/1.89 ![X0]: (~aElementOf0(X0,xU)|sdtlseqdt0(X0,xp)|~aElementOf0(X0,xT)|~aElementOf0(X0,xU)|sdtlseqdt0(X0,xp))),
% 10.86/1.89 inference(resolution,[status(thm)],[f737,f197])).
% 10.86/1.89 fof(f1596,plain,(
% 10.86/1.89 ![X0]: (~aElementOf0(X0,xU)|sdtlseqdt0(X0,xp)|~aElementOf0(X0,xT))),
% 10.86/1.89 inference(duplicate_literals_removal,[status(thm)],[f1594])).
% 10.86/1.89 fof(f1597,plain,(
% 10.86/1.89 ![X0]: (sdtlseqdt0(X0,xp)|~aElementOf0(X0,xT))),
% 10.86/1.89 inference(forward_subsumption_resolution,[status(thm)],[f1596,f708])).
% 10.86/1.89 fof(f1656,plain,(
% 10.86/1.89 ~aElementOf0(sK19_skl,xT)|sdtlpdtrp0(xf,sK17_skl)=sK17_skl|sP1_prd),
% 10.86/1.89 inference(resolution,[status(thm)],[f1597,f394])).
% 10.86/1.89 fof(f1659,plain,(
% 10.86/1.89 sdtlpdtrp0(xf,sK17_skl)=sK17_skl|sP1_prd),
% 10.86/1.89 inference(forward_subsumption_resolution,[status(thm)],[f1656,f395])).
% 10.86/1.89 fof(f1692,plain,(
% 10.86/1.89 sdtlpdtrp0(xf,sK17_skl)=sK17_skl|~sdtlpdtrp0(xf,xp)=xp),
% 10.86/1.89 inference(resolution,[status(thm)],[f1659,f429])).
% 10.86/1.89 fof(f3718,plain,(
% 10.86/1.89 aElementOf0(sdtlpdtrp0(xf,xp),xP)|~sdtlseqdt0(sdtlpdtrp0(xf,xp),xp)),
% 10.86/1.89 inference(forward_subsumption_resolution,[status(thm)],[f1164,f192])).
% 10.86/1.89 fof(f3719,plain,(
% 10.86/1.89 aElementOf0(sdtlpdtrp0(xf,xp),xP)),
% 10.86/1.89 inference(resolution,[status(thm)],[f3718,f829])).
% 10.86/1.89 fof(f3728,plain,(
% 10.86/1.89 sdtlseqdt0(xp,sdtlpdtrp0(xf,xp))),
% 10.86/1.89 inference(resolution,[status(thm)],[f3719,f194])).
% 10.86/1.89 fof(f4757,plain,(
% 10.86/1.89 ~sdtlseqdt0(sdtlpdtrp0(xf,sK17_skl),sK17_skl)|sP1_prd|sP2_prd),
% 10.86/1.89 inference(backward_subsumption_resolution,[status(thm)],[f1031,f4758])).
% 10.86/1.89 fof(f4758,plain,(
% 10.86/1.89 sP1_prd|sP2_prd|~aElementOf0(sK17_skl,xP)),
% 10.86/1.89 inference(forward_subsumption_resolution,[status(thm)],[f1372,f3728])).
% 10.86/1.89 fof(f4872,plain,(
% 10.86/1.89 sdtlpdtrp0(xf,sK17_skl)=sK17_skl|~xp=xp),
% 10.86/1.89 inference(backward_demodulation,[status(thm)],[f4890,f1692])).
% 10.86/1.89 fof(f4886,plain,(
% 10.86/1.89 ~sP1_prd|~xp=xp),
% 10.86/1.89 inference(backward_demodulation,[status(thm)],[f4890,f429])).
% 10.86/1.89 fof(f4890,plain,(
% 10.86/1.89 sdtlpdtrp0(xf,xp)=xp),
% 10.86/1.89 inference(forward_subsumption_resolution,[status(thm)],[f1398,f3728])).
% 10.86/1.89 fof(f4906,plain,(
% 10.86/1.89 sdtlpdtrp0(xf,sK17_skl)=sK17_skl),
% 10.86/1.92 inference(trivial_equality_resolution,[status(thm)],[f4872])).
% 10.86/1.92 fof(f4917,plain,(
% 10.86/1.92 ~sP1_prd),
% 10.86/1.92 inference(trivial_equality_resolution,[status(thm)],[f4886])).
% 10.86/1.92 fof(f4950,plain,(
% 10.86/1.92 ~sdtlseqdt0(sdtlpdtrp0(xf,sK17_skl),sK17_skl)|sP2_prd),
% 10.86/1.92 inference(backward_subsumption_resolution,[status(thm)],[f4757,f4917])).
% 10.86/1.92 fof(f5018,plain,(
% 10.86/1.92 aElement0(sK17_skl)|sP2_prd),
% 10.86/1.92 inference(backward_subsumption_resolution,[status(thm)],[f237,f4917])).
% 10.86/1.92 fof(f5149,plain,(
% 10.86/1.92 ~sdtlseqdt0(sK17_skl,sK17_skl)|sP2_prd),
% 10.86/1.92 inference(forward_demodulation,[status(thm)],[f4906,f4950])).
% 10.86/1.92 fof(f5151,plain,(
% 10.86/1.92 sP2_prd|~aElement0(sK17_skl)),
% 10.86/1.92 inference(resolution,[status(thm)],[f5149,f56])).
% 10.86/1.92 fof(f5154,plain,(
% 10.86/1.92 sP2_prd),
% 10.86/1.92 inference(forward_subsumption_resolution,[status(thm)],[f5151,f5018])).
% 10.86/1.92 fof(f5156,plain,(
% 10.86/1.92 ~sdtlseqdt0(sK19_skl,xp)),
% 10.86/1.92 inference(backward_subsumption_resolution,[status(thm)],[f232,f5154])).
% 10.86/1.92 fof(f5157,plain,(
% 10.86/1.92 aElementOf0(sK19_skl,xT)),
% 10.86/1.92 inference(backward_subsumption_resolution,[status(thm)],[f231,f5154])).
% 10.86/1.92 fof(f5158,plain,(
% 10.86/1.92 ~aElementOf0(sK19_skl,xT)),
% 10.86/1.92 inference(resolution,[status(thm)],[f5156,f1597])).
% 10.86/1.92 fof(f5203,plain,(
% 10.86/1.92 $false),
% 10.86/1.92 inference(forward_subsumption_resolution,[status(thm)],[f5158,f5157])).
% 10.86/1.92 % SZS output end CNFRefutation for theBenchmark.p
% 10.86/1.94 % Elapsed time: 1.546846 seconds
% 10.86/1.94 % CPU time: 11.630335 seconds
% 10.86/1.94 % Total memory used: 187.058 MB
% 10.86/1.94 % Net memory used: 181.128 MB
%------------------------------------------------------------------------------