%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM571+3 : 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 : n012.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:43:14 PM UTC 2026
% Result : Theorem 0.08s 0.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM571+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n012.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.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 02:40:36 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.36 % Drodi V4.1.1
% 0.08/0.41 % Refutation found
% 0.08/0.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.08/0.41 % SZS output start CNFRefutation for theBenchmark
% 0.08/0.41 fof(f3,axiom,(
% 0.08/0.41 (! [W0] :( aSet0(W0)=> (! [W1] :( aElementOf0(W1,W0)=> aElement0(W1) ) )) )),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f5,definition,(
% 0.08/0.41 (! [W0] :( W0 = slcrc0<=> ( aSet0(W0)& ~ (? [W1] : aElementOf0(W1,W0) )) ) )),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f6,axiom,(
% 0.08/0.41 isFinite0(slcrc0) ),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f8,axiom,(
% 0.08/0.41 (! [W0] :( ( aSet0(W0)& isCountable0(W0) )=> ~ isFinite0(W0) ) )),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f10,definition,(
% 0.08/0.41 (! [W0] :( aSet0(W0)=> (! [W1] :( aSubsetOf0(W1,W0)<=> ( aSet0(W1)& (! [W2] :( aElementOf0(W2,W1)=> aElementOf0(W2,W0) ) )) ) )) )),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f11,axiom,(
% 0.08/0.41 (! [W0] :( ( aSet0(W0)& isFinite0(W0) )=> (! [W1] :( aSubsetOf0(W1,W0)=> isFinite0(W1) ) )) )),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f12,axiom,(
% 0.08/0.41 (! [W0] :( aSet0(W0)=> aSubsetOf0(W0,W0) ) )),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f13,axiom,(
% 0.08/0.41 (! [W0,W1] :( ( aSet0(W0)& aSet0(W1) )=> ( ( aSubsetOf0(W0,W1)& aSubsetOf0(W1,W0) )=> W0 = W1 ) ) )),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f14,axiom,(
% 0.08/0.41 (! [W0,W1,W2] :( ( aSet0(W0)& aSet0(W1)& aSet0(W2) )=> ( ( aSubsetOf0(W0,W1)& aSubsetOf0(W1,W2) )=> aSubsetOf0(W0,W2) ) ) )),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f23,axiom,(
% 0.08/0.41 ( aSet0(szNzAzT0)& isCountable0(szNzAzT0) ) ),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f24,axiom,(
% 0.08/0.41 aElementOf0(sz00,szNzAzT0) ),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f64,axiom,(
% 0.08/0.41 (! [W0] :( aFunction0(W0)=> aSet0(szDzozmdt0(W0)) ) )),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f73,hypothesis,(
% 0.08/0.41 ( aSet0(xT)& isFinite0(xT) ) ),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f74,hypothesis,(
% 0.08/0.41 aElementOf0(xK,szNzAzT0) ),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f75,hypothesis,(
% 0.08/0.41 ( aSet0(xS)& (! [W0] :( aElementOf0(W0,xS)=> aElementOf0(W0,szNzAzT0) ))& aSubsetOf0(xS,szNzAzT0)& isCountable0(xS) ) ),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f76,hypothesis,(
% 0.08/0.41 ( aFunction0(xc)& (! [W0] :( ( aElementOf0(W0,szDzozmdt0(xc))=> ( aSet0(W0)& (! [W1] :( aElementOf0(W1,W0)=> aElementOf0(W1,xS) ))& aSubsetOf0(W0,xS)& sbrdtbr0(W0) = xK ) )& ( ( ( ( aSet0(W0)& (! [W1] :( aElementOf0(W1,W0)=> aElementOf0(W1,xS) ) ))| aSubsetOf0(W0,xS) )& sbrdtbr0(W0) = xK )=> aElementOf0(W0,szDzozmdt0(xc)) ) ))& szDzozmdt0(xc) = slbdtsldtrb0(xS,xK)& aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc)))& (! [W0] :( aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc)))<=> (? [W1] :( aElementOf0(W1,szDzozmdt0(xc))& sdtlpdtrp0(xc,W1) = W0 ) )))& (! [W0] :( aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc)))=> aElementOf0(W0,xT) ))& aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT) ) ),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f80,hypothesis,(
% 0.08/0.41 ( aElementOf0(xk,szNzAzT0)& szszuzczcdt0(xk) = xK ) ),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f81,hypothesis,(
% 0.08/0.41 ( aFunction0(xN)& szDzozmdt0(xN) = szNzAzT0& sdtlpdtrp0(xN,sz00) = xS& (! [W0] :( aElementOf0(W0,szNzAzT0)=> ( ( ( ( aSet0(sdtlpdtrp0(xN,W0))& (! [W1] :( aElementOf0(W1,sdtlpdtrp0(xN,W0))=> aElementOf0(W1,szNzAzT0) ) ))| aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0) )& isCountable0(sdtlpdtrp0(xN,W0)) )=> ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0))& (! [W1] :( aElementOf0(W1,sdtlpdtrp0(xN,W0))=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W1) ))& aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))& (! [W1] :( aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))<=> ( aElement0(W1)& aElementOf0(W1,sdtlpdtrp0(xN,W0))& W1 != szmzizndt0(sdtlpdtrp0(xN,W0)) ) ))& aSet0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))& (! [W1] :( aElementOf0(W1,sdtlpdtrp0(xN,szszuzczcdt0(W0)))=> aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) ))& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))& isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(W0))) ) ) ) )) ),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f82,hypothesis,(
% 0.08/0.41 aElementOf0(xi,szNzAzT0) ),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f84,hypothesis,(
% 0.08/0.41 ( xi != sz00=> ( (? [W0] :( aElementOf0(W0,szNzAzT0)& szszuzczcdt0(W0) = xi ))& aSet0(sdtlpdtrp0(xN,xi))& (! [W0] :( aElementOf0(W0,sdtlpdtrp0(xN,xi))=> aElementOf0(W0,szNzAzT0) ))& aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0)& isCountable0(sdtlpdtrp0(xN,xi)) ) ) ),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f85,conjecture,(
% 0.08/0.41 ( ( ( aSet0(sdtlpdtrp0(xN,xi))& (! [W0] :( aElementOf0(W0,sdtlpdtrp0(xN,xi))=> aElementOf0(W0,szNzAzT0) ) ))| aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0) )& isCountable0(sdtlpdtrp0(xN,xi)) ) ),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f86,negated_conjecture,(
% 0.08/0.41 ~(( ( ( aSet0(sdtlpdtrp0(xN,xi))& (! [W0] :( aElementOf0(W0,sdtlpdtrp0(xN,xi))=> aElementOf0(W0,szNzAzT0) ) ))| aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0) )& isCountable0(sdtlpdtrp0(xN,xi)) ) )),
% 0.08/0.41 inference(negated_conjecture,[status(cth)],[f85])).
% 0.08/0.41 fof(f93,plain,(
% 0.08/0.41 ![W0]: (~aSet0(W0)|(![W1]: (~aElementOf0(W1,W0)|aElement0(W1))))),
% 0.08/0.41 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.08/0.41 fof(f94,plain,(
% 0.08/0.41 ![X0,X1]: (~aSet0(X0)|~aElementOf0(X1,X0)|aElement0(X1))),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f93])).
% 0.08/0.41 fof(f97,plain,(
% 0.08/0.41 ![W0]: (W0=slcrc0<=>(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0))))),
% 0.08/0.41 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.08/0.41 fof(f98,plain,(
% 0.08/0.41 ![W0]: ((~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0))))&(W0=slcrc0|(~aSet0(W0)|(?[W1]: aElementOf0(W1,W0)))))),
% 0.08/0.41 inference(NNF_transformation,[status(thm)],[f97])).
% 0.08/0.41 fof(f99,plain,(
% 0.08/0.41 (![W0]: (~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0)))))&(![W0]: (W0=slcrc0|(~aSet0(W0)|(?[W1]: aElementOf0(W1,W0)))))),
% 0.08/0.41 inference(miniscoping,[status(thm)],[f98])).
% 0.08/0.41 fof(f100,plain,(
% 0.08/0.41 (![W0]: (~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0)))))&(![W0]: (W0=slcrc0|(~aSet0(W0)|aElementOf0(sK0_skl(W0),W0))))),
% 0.08/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(W1,sK0_skl(W0))],[f99])).
% 0.08/0.41 fof(f101,plain,(
% 0.08/0.41 ![X0]: (~X0=slcrc0|aSet0(X0))),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f100])).
% 0.08/0.41 fof(f102,plain,(
% 0.08/0.41 ![X0,X1]: (~X0=slcrc0|~aElementOf0(X1,X0))),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f100])).
% 0.08/0.41 fof(f103,plain,(
% 0.08/0.41 ![X0]: (X0=slcrc0|~aSet0(X0)|aElementOf0(sK0_skl(X0),X0))),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f100])).
% 0.08/0.41 fof(f104,plain,(
% 0.08/0.41 isFinite0(slcrc0)),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f6])).
% 0.08/0.41 fof(f107,plain,(
% 0.08/0.41 ![W0]: ((~aSet0(W0)|~isCountable0(W0))|~isFinite0(W0))),
% 0.08/0.41 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 0.08/0.41 fof(f108,plain,(
% 0.08/0.41 ![X0]: (~aSet0(X0)|~isCountable0(X0)|~isFinite0(X0))),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f107])).
% 0.08/0.41 fof(f111,plain,(
% 0.08/0.41 ![W0]: (~aSet0(W0)|(![W1]: (aSubsetOf0(W1,W0)<=>(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0)))))))),
% 0.08/0.41 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 0.08/0.41 fof(f112,plain,(
% 0.08/0.41 ![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.08/0.41 inference(NNF_transformation,[status(thm)],[f111])).
% 0.08/0.41 fof(f113,plain,(
% 0.08/0.41 ![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.08/0.41 inference(miniscoping,[status(thm)],[f112])).
% 0.08/0.41 fof(f114,plain,(
% 0.08/0.41 ![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.08/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W2,sK1_skl(W1,W0))],[f113])).
% 0.08/0.41 fof(f115,plain,(
% 0.08/0.41 ![X0,X1]: (~aSet0(X0)|~aSubsetOf0(X1,X0)|aSet0(X1))),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f114])).
% 0.08/0.41 fof(f116,plain,(
% 0.08/0.41 ![X0,X1,X2]: (~aSet0(X0)|~aSubsetOf0(X1,X0)|~aElementOf0(X2,X1)|aElementOf0(X2,X0))),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f114])).
% 0.08/0.41 fof(f117,plain,(
% 0.08/0.41 ![X0,X1]: (~aSet0(X0)|aSubsetOf0(X1,X0)|~aSet0(X1)|aElementOf0(sK1_skl(X1,X0),X1))),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f114])).
% 0.08/0.41 fof(f119,plain,(
% 0.08/0.41 ![W0]: ((~aSet0(W0)|~isFinite0(W0))|(![W1]: (~aSubsetOf0(W1,W0)|isFinite0(W1))))),
% 0.08/0.41 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 0.08/0.41 fof(f120,plain,(
% 0.08/0.41 ![X0,X1]: (~aSet0(X0)|~isFinite0(X0)|~aSubsetOf0(X1,X0)|isFinite0(X1))),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f119])).
% 0.08/0.41 fof(f121,plain,(
% 0.08/0.41 ![W0]: (~aSet0(W0)|aSubsetOf0(W0,W0))),
% 0.08/0.41 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 0.08/0.41 fof(f122,plain,(
% 0.08/0.41 ![X0]: (~aSet0(X0)|aSubsetOf0(X0,X0))),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f121])).
% 0.08/0.41 fof(f123,plain,(
% 0.08/0.41 ![W0,W1]: ((~aSet0(W0)|~aSet0(W1))|((~aSubsetOf0(W0,W1)|~aSubsetOf0(W1,W0))|W0=W1))),
% 0.08/0.41 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 0.08/0.41 fof(f124,plain,(
% 0.08/0.41 ![X0,X1]: (~aSet0(X0)|~aSet0(X1)|~aSubsetOf0(X0,X1)|~aSubsetOf0(X1,X0)|X0=X1)),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f123])).
% 0.08/0.41 fof(f125,plain,(
% 0.08/0.41 ![W0,W1,W2]: (((~aSet0(W0)|~aSet0(W1))|~aSet0(W2))|((~aSubsetOf0(W0,W1)|~aSubsetOf0(W1,W2))|aSubsetOf0(W0,W2)))),
% 0.08/0.41 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 0.08/0.41 fof(f126,plain,(
% 0.08/0.41 ![X0,X1,X2]: (~aSet0(X0)|~aSet0(X1)|~aSet0(X2)|~aSubsetOf0(X0,X1)|~aSubsetOf0(X1,X2)|aSubsetOf0(X0,X2))),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f125])).
% 0.08/0.41 fof(f163,plain,(
% 0.08/0.41 aSet0(szNzAzT0)),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f23])).
% 0.08/0.41 fof(f164,plain,(
% 0.08/0.41 isCountable0(szNzAzT0)),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f23])).
% 0.08/0.41 fof(f165,plain,(
% 0.08/0.41 aElementOf0(sz00,szNzAzT0)),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f24])).
% 0.08/0.41 fof(f295,plain,(
% 0.08/0.41 ![W0]: (~aFunction0(W0)|aSet0(szDzozmdt0(W0)))),
% 0.08/0.41 inference(pre_NNF_transformation,[status(thm)],[f64])).
% 0.08/0.41 fof(f296,plain,(
% 0.08/0.41 ![X0]: (~aFunction0(X0)|aSet0(szDzozmdt0(X0)))),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f295])).
% 0.08/0.41 fof(f343,plain,(
% 0.08/0.41 aSet0(xT)),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f73])).
% 0.08/0.41 fof(f344,plain,(
% 0.08/0.41 isFinite0(xT)),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f73])).
% 0.08/0.41 fof(f345,plain,(
% 0.08/0.41 aElementOf0(xK,szNzAzT0)),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f74])).
% 0.08/0.41 fof(f346,plain,(
% 0.08/0.41 ((aSet0(xS)&(![W0]: (~aElementOf0(W0,xS)|aElementOf0(W0,szNzAzT0))))&aSubsetOf0(xS,szNzAzT0))&isCountable0(xS)),
% 0.08/0.41 inference(pre_NNF_transformation,[status(thm)],[f75])).
% 0.08/0.41 fof(f347,plain,(
% 0.08/0.41 aSet0(xS)),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f346])).
% 0.08/0.41 fof(f349,plain,(
% 0.08/0.41 aSubsetOf0(xS,szNzAzT0)),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f346])).
% 0.08/0.41 fof(f350,plain,(
% 0.08/0.41 isCountable0(xS)),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f346])).
% 0.08/0.41 fof(f351,plain,(
% 0.08/0.41 (((((aFunction0(xc)&(![W0]: ((~aElementOf0(W0,szDzozmdt0(xc))|(((aSet0(W0)&(![W1]: (~aElementOf0(W1,W0)|aElementOf0(W1,xS))))&aSubsetOf0(W0,xS))&sbrdtbr0(W0)=xK))&((((~aSet0(W0)|(?[W1]: (aElementOf0(W1,W0)&~aElementOf0(W1,xS))))&~aSubsetOf0(W0,xS))|~sbrdtbr0(W0)=xK)|aElementOf0(W0,szDzozmdt0(xc))))))&szDzozmdt0(xc)=slbdtsldtrb0(xS,xK))&aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc))))&(![W0]: (aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc)))<=>(?[W1]: (aElementOf0(W1,szDzozmdt0(xc))&sdtlpdtrp0(xc,W1)=W0)))))&(![W0]: (~aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc)))|aElementOf0(W0,xT))))&aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT)),
% 0.08/0.41 inference(pre_NNF_transformation,[status(thm)],[f76])).
% 0.08/0.41 fof(f352,plain,(
% 0.08/0.41 (((((aFunction0(xc)&(![W0]: ((~aElementOf0(W0,szDzozmdt0(xc))|(((aSet0(W0)&(![W1]: (~aElementOf0(W1,W0)|aElementOf0(W1,xS))))&aSubsetOf0(W0,xS))&sbrdtbr0(W0)=xK))&((((~aSet0(W0)|(?[W1]: (aElementOf0(W1,W0)&~aElementOf0(W1,xS))))&~aSubsetOf0(W0,xS))|~sbrdtbr0(W0)=xK)|aElementOf0(W0,szDzozmdt0(xc))))))&szDzozmdt0(xc)=slbdtsldtrb0(xS,xK))&aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc))))&(![W0]: ((~aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc)))|(?[W1]: (aElementOf0(W1,szDzozmdt0(xc))&sdtlpdtrp0(xc,W1)=W0)))&(aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc)))|(![W1]: (~aElementOf0(W1,szDzozmdt0(xc))|~sdtlpdtrp0(xc,W1)=W0))))))&(![W0]: (~aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc)))|aElementOf0(W0,xT))))&aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT)),
% 0.08/0.41 inference(NNF_transformation,[status(thm)],[f351])).
% 0.08/0.41 fof(f353,plain,(
% 0.08/0.41 (((((aFunction0(xc)&((![W0]: (~aElementOf0(W0,szDzozmdt0(xc))|(((aSet0(W0)&(![W1]: (~aElementOf0(W1,W0)|aElementOf0(W1,xS))))&aSubsetOf0(W0,xS))&sbrdtbr0(W0)=xK)))&(![W0]: ((((~aSet0(W0)|(?[W1]: (aElementOf0(W1,W0)&~aElementOf0(W1,xS))))&~aSubsetOf0(W0,xS))|~sbrdtbr0(W0)=xK)|aElementOf0(W0,szDzozmdt0(xc))))))&szDzozmdt0(xc)=slbdtsldtrb0(xS,xK))&aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc))))&((![W0]: (~aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc)))|(?[W1]: (aElementOf0(W1,szDzozmdt0(xc))&sdtlpdtrp0(xc,W1)=W0))))&(![W0]: (aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc)))|(![W1]: (~aElementOf0(W1,szDzozmdt0(xc))|~sdtlpdtrp0(xc,W1)=W0))))))&(![W0]: (~aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc)))|aElementOf0(W0,xT))))&aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT)),
% 0.08/0.41 inference(miniscoping,[status(thm)],[f352])).
% 0.08/0.41 fof(f354,plain,(
% 0.08/0.41 (((((aFunction0(xc)&((![W0]: (~aElementOf0(W0,szDzozmdt0(xc))|(((aSet0(W0)&(![W1]: (~aElementOf0(W1,W0)|aElementOf0(W1,xS))))&aSubsetOf0(W0,xS))&sbrdtbr0(W0)=xK)))&(![W0]: ((((~aSet0(W0)|(aElementOf0(sK19_skl(W0),W0)&~aElementOf0(sK19_skl(W0),xS)))&~aSubsetOf0(W0,xS))|~sbrdtbr0(W0)=xK)|aElementOf0(W0,szDzozmdt0(xc))))))&szDzozmdt0(xc)=slbdtsldtrb0(xS,xK))&aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc))))&((![W0]: (~aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc)))|(aElementOf0(sK20_skl(W0),szDzozmdt0(xc))&sdtlpdtrp0(xc,sK20_skl(W0))=W0)))&(![W0]: (aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc)))|(![W1]: (~aElementOf0(W1,szDzozmdt0(xc))|~sdtlpdtrp0(xc,W1)=W0))))))&(![W0]: (~aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc)))|aElementOf0(W0,xT))))&aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT)),
% 0.08/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl,sK20_skl]),skolemize(W1,sK19_skl(W0)),skolemize(W1,sK20_skl(W0))],[f353])).
% 0.08/0.41 fof(f355,plain,(
% 0.08/0.41 aFunction0(xc)),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f354])).
% 0.08/0.41 fof(f381,plain,(
% 0.08/0.41 aElementOf0(xk,szNzAzT0)),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f80])).
% 0.08/0.41 fof(f383,plain,(
% 0.08/0.41 ((aFunction0(xN)&szDzozmdt0(xN)=szNzAzT0)&sdtlpdtrp0(xN,sz00)=xS)&(![W0]: (~aElementOf0(W0,szNzAzT0)|((((~aSet0(sdtlpdtrp0(xN,W0))|(?[W1]: (aElementOf0(W1,sdtlpdtrp0(xN,W0))&~aElementOf0(W1,szNzAzT0))))&~aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0))|~isCountable0(sdtlpdtrp0(xN,W0)))|(((((((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0))&(![W1]: (~aElementOf0(W1,sdtlpdtrp0(xN,W0))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W1))))&aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))&(![W1]: (aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))<=>((aElement0(W1)&aElementOf0(W1,sdtlpdtrp0(xN,W0)))&~W1=szmzizndt0(sdtlpdtrp0(xN,W0))))))&aSet0(sdtlpdtrp0(xN,szszuzczcdt0(W0))))&(![W1]: (~aElementOf0(W1,sdtlpdtrp0(xN,szszuzczcdt0(W0)))|aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))))&aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))&isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))))))),
% 0.08/0.41 inference(pre_NNF_transformation,[status(thm)],[f81])).
% 0.08/0.41 fof(f384,definition,(
% 0.08/0.41 ![W0]: (sP4_prd(W0)<=>(((~aSet0(sdtlpdtrp0(xN,W0))|(?[W1]: (aElementOf0(W1,sdtlpdtrp0(xN,W0))&~aElementOf0(W1,szNzAzT0))))&~aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0))|~isCountable0(sdtlpdtrp0(xN,W0))))),
% 0.08/0.41 introduced(definition,[new_symbols(definition,[sP4_prd])],[])).
% 0.08/0.41 fof(f385,plain,(
% 0.08/0.41 ((aFunction0(xN)&szDzozmdt0(xN)=szNzAzT0)&sdtlpdtrp0(xN,sz00)=xS)&(![W0]: (~aElementOf0(W0,szNzAzT0)|(sP4_prd(W0)|(((((((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0))&(![W1]: (~aElementOf0(W1,sdtlpdtrp0(xN,W0))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W1))))&aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))&(![W1]: (aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))<=>((aElement0(W1)&aElementOf0(W1,sdtlpdtrp0(xN,W0)))&~W1=szmzizndt0(sdtlpdtrp0(xN,W0))))))&aSet0(sdtlpdtrp0(xN,szszuzczcdt0(W0))))&(![W1]: (~aElementOf0(W1,sdtlpdtrp0(xN,szszuzczcdt0(W0)))|aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))))&aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))&isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))))))),
% 0.08/0.41 inference(formula_renaming,[status(thm)],[f383,f384])).
% 0.08/0.41 fof(f386,plain,(
% 0.08/0.41 ((aFunction0(xN)&szDzozmdt0(xN)=szNzAzT0)&sdtlpdtrp0(xN,sz00)=xS)&(![W0]: (~aElementOf0(W0,szNzAzT0)|(sP4_prd(W0)|(((((((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0))&(![W1]: (~aElementOf0(W1,sdtlpdtrp0(xN,W0))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W1))))&aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))&(![W1]: ((~aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))|((aElement0(W1)&aElementOf0(W1,sdtlpdtrp0(xN,W0)))&~W1=szmzizndt0(sdtlpdtrp0(xN,W0))))&(aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))|((~aElement0(W1)|~aElementOf0(W1,sdtlpdtrp0(xN,W0)))|W1=szmzizndt0(sdtlpdtrp0(xN,W0)))))))&aSet0(sdtlpdtrp0(xN,szszuzczcdt0(W0))))&(![W1]: (~aElementOf0(W1,sdtlpdtrp0(xN,szszuzczcdt0(W0)))|aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))))&aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))&isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))))))),
% 0.08/0.41 inference(NNF_transformation,[status(thm)],[f385])).
% 0.08/0.41 fof(f387,plain,(
% 0.08/0.41 ((aFunction0(xN)&szDzozmdt0(xN)=szNzAzT0)&sdtlpdtrp0(xN,sz00)=xS)&(![W0]: (~aElementOf0(W0,szNzAzT0)|(sP4_prd(W0)|(((((((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0))&(![W1]: (~aElementOf0(W1,sdtlpdtrp0(xN,W0))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W1))))&aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))&((![W1]: (~aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))|((aElement0(W1)&aElementOf0(W1,sdtlpdtrp0(xN,W0)))&~W1=szmzizndt0(sdtlpdtrp0(xN,W0)))))&(![W1]: (aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))|((~aElement0(W1)|~aElementOf0(W1,sdtlpdtrp0(xN,W0)))|W1=szmzizndt0(sdtlpdtrp0(xN,W0)))))))&aSet0(sdtlpdtrp0(xN,szszuzczcdt0(W0))))&(![W1]: (~aElementOf0(W1,sdtlpdtrp0(xN,szszuzczcdt0(W0)))|aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))))&aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))&isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))))))),
% 0.08/0.41 inference(miniscoping,[status(thm)],[f386])).
% 0.08/0.41 fof(f390,plain,(
% 0.08/0.41 sdtlpdtrp0(xN,sz00)=xS),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f387])).
% 0.08/0.41 fof(f402,plain,(
% 0.08/0.41 aElementOf0(xi,szNzAzT0)),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f82])).
% 0.08/0.41 fof(f408,plain,(
% 0.08/0.41 xi=sz00|(((((?[W0]: (aElementOf0(W0,szNzAzT0)&szszuzczcdt0(W0)=xi))&aSet0(sdtlpdtrp0(xN,xi)))&(![W0]: (~aElementOf0(W0,sdtlpdtrp0(xN,xi))|aElementOf0(W0,szNzAzT0))))&aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0))&isCountable0(sdtlpdtrp0(xN,xi)))),
% 0.08/0.41 inference(pre_NNF_transformation,[status(thm)],[f84])).
% 0.08/0.41 fof(f409,plain,(
% 0.08/0.41 xi=sz00|(((((aElementOf0(sK23_skl,szNzAzT0)&szszuzczcdt0(sK23_skl)=xi)&aSet0(sdtlpdtrp0(xN,xi)))&(![W0]: (~aElementOf0(W0,sdtlpdtrp0(xN,xi))|aElementOf0(W0,szNzAzT0))))&aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0))&isCountable0(sdtlpdtrp0(xN,xi)))),
% 0.08/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl]),skolemize(W0,sK23_skl)],[f408])).
% 0.08/0.41 fof(f414,plain,(
% 0.08/0.41 xi=sz00|aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0)),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f409])).
% 0.08/0.41 fof(f415,plain,(
% 0.08/0.41 xi=sz00|isCountable0(sdtlpdtrp0(xN,xi))),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f409])).
% 0.08/0.41 fof(f416,plain,(
% 0.08/0.41 (((~aSet0(sdtlpdtrp0(xN,xi))|(?[W0]: (aElementOf0(W0,sdtlpdtrp0(xN,xi))&~aElementOf0(W0,szNzAzT0))))&~aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0))|~isCountable0(sdtlpdtrp0(xN,xi)))),
% 0.08/0.41 inference(pre_NNF_transformation,[status(thm)],[f86])).
% 0.08/0.41 fof(f417,plain,(
% 0.08/0.41 ((~aSet0(sdtlpdtrp0(xN,xi))|(aElementOf0(sK24_skl,sdtlpdtrp0(xN,xi))&~aElementOf0(sK24_skl,szNzAzT0)))&~aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0))|~isCountable0(sdtlpdtrp0(xN,xi))),
% 0.08/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK24_skl]),skolemize(W0,sK24_skl)],[f416])).
% 0.08/0.41 fof(f420,plain,(
% 0.08/0.41 ~aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0)|~isCountable0(sdtlpdtrp0(xN,xi))),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f417])).
% 0.08/0.41 fof(f496,definition,(
% 0.08/0.41 sQ0_spl <=> (xi=sz00)),
% 0.08/0.41 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.08/0.41 fof(f497,plain,(
% 0.08/0.41 xi=sz00|~sQ0_spl),
% 0.08/0.41 inference(component_clause,[status(thm)],[f496])).
% 0.08/0.41 fof(f515,definition,(
% 0.08/0.41 sQ5_spl <=> (aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0))),
% 0.08/0.41 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.08/0.41 fof(f517,plain,(
% 0.08/0.41 ~aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0)|sQ5_spl),
% 0.08/0.41 inference(component_clause,[status(thm)],[f515])).
% 0.08/0.41 fof(f518,plain,(
% 0.08/0.41 sQ0_spl|sQ5_spl),
% 0.08/0.41 inference(split_clause,[status(thm)],[f414,f496,f515])).
% 0.08/0.41 fof(f519,definition,(
% 0.08/0.41 sQ6_spl <=> (isCountable0(sdtlpdtrp0(xN,xi)))),
% 0.08/0.41 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.08/0.41 fof(f521,plain,(
% 0.08/0.41 ~isCountable0(sdtlpdtrp0(xN,xi))|sQ6_spl),
% 0.08/0.41 inference(component_clause,[status(thm)],[f519])).
% 0.08/0.41 fof(f522,plain,(
% 0.08/0.41 sQ0_spl|sQ6_spl),
% 0.08/0.41 inference(split_clause,[status(thm)],[f415,f496,f519])).
% 0.08/0.41 fof(f531,plain,(
% 0.08/0.41 ~sQ5_spl|~sQ6_spl),
% 0.08/0.41 inference(split_clause,[status(thm)],[f420,f515,f519])).
% 0.08/0.41 fof(f532,plain,(
% 0.08/0.41 aSet0(slcrc0)),
% 0.08/0.41 inference(destructive_equality_resolution,[status(thm)],[f101])).
% 0.08/0.41 fof(f533,plain,(
% 0.08/0.41 ![X0]: (~aElementOf0(X0,slcrc0))),
% 0.08/0.41 inference(destructive_equality_resolution,[status(thm)],[f102])).
% 0.08/0.41 fof(f584,plain,(
% 0.08/0.41 aSubsetOf0(szNzAzT0,szNzAzT0)),
% 0.08/0.41 inference(resolution,[status(thm)],[f122,f163])).
% 0.08/0.41 fof(f586,definition,(
% 0.08/0.41 sQ9_spl <=> (aSet0(szNzAzT0))),
% 0.08/0.41 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.08/0.41 fof(f588,plain,(
% 0.08/0.41 ~aSet0(szNzAzT0)|sQ9_spl),
% 0.08/0.41 inference(component_clause,[status(thm)],[f586])).
% 0.08/0.41 fof(f590,plain,(
% 0.08/0.41 ![X0,X1]: (~aSet0(X0)|~aSubsetOf0(X1,X0)|~aSubsetOf0(X0,X1)|X1=X0)),
% 0.08/0.41 inference(forward_subsumption_resolution,[status(thm)],[f124,f115])).
% 0.08/0.41 fof(f591,plain,(
% 0.08/0.41 ![X0]: (~aSubsetOf0(X0,szNzAzT0)|~aSubsetOf0(szNzAzT0,X0)|X0=szNzAzT0)),
% 0.08/0.41 inference(resolution,[status(thm)],[f590,f163])).
% 0.08/0.41 fof(f592,plain,(
% 0.08/0.41 ~aSubsetOf0(szNzAzT0,szNzAzT0)|szNzAzT0=szNzAzT0),
% 0.08/0.41 inference(resolution,[status(thm)],[f591,f584])).
% 0.08/0.41 fof(f593,definition,(
% 0.08/0.41 sQ10_spl <=> (aSubsetOf0(szNzAzT0,szNzAzT0))),
% 0.08/0.41 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.08/0.41 fof(f595,plain,(
% 0.08/0.41 ~aSubsetOf0(szNzAzT0,szNzAzT0)|sQ10_spl),
% 0.08/0.41 inference(component_clause,[status(thm)],[f593])).
% 0.08/0.41 fof(f596,definition,(
% 0.08/0.41 sQ11_spl <=> (szNzAzT0=szNzAzT0)),
% 0.08/0.41 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.08/0.41 fof(f599,plain,(
% 0.08/0.41 ~sQ10_spl|sQ11_spl),
% 0.08/0.41 inference(split_clause,[status(thm)],[f592,f593,f596])).
% 0.08/0.41 fof(f600,plain,(
% 0.08/0.41 $false|sQ10_spl),
% 0.08/0.41 inference(forward_subsumption_resolution,[status(thm)],[f595,f584])).
% 0.08/0.41 fof(f601,plain,(
% 0.08/0.41 sQ10_spl),
% 0.08/0.41 inference(contradiction_clause,[status(thm)],[f600])).
% 0.08/0.41 fof(f602,plain,(
% 0.08/0.41 ![X0,X1,X2]: (~aSet0(X0)|~aSet0(X1)|~aSubsetOf0(X2,X0)|~aSubsetOf0(X0,X1)|aSubsetOf0(X2,X1))),
% 0.08/0.41 inference(forward_subsumption_resolution,[status(thm)],[f126,f115])).
% 0.08/0.41 fof(f603,plain,(
% 0.08/0.41 ![X0,X1]: (~aSet0(X0)|~aSubsetOf0(X1,X0)|~aSubsetOf0(X0,szNzAzT0)|aSubsetOf0(X1,szNzAzT0))),
% 0.08/0.41 inference(resolution,[status(thm)],[f602,f163])).
% 0.08/0.41 fof(f604,plain,(
% 0.08/0.41 ![X0]: (~aSubsetOf0(X0,szNzAzT0)|~aSubsetOf0(szNzAzT0,szNzAzT0)|aSubsetOf0(X0,szNzAzT0))),
% 0.08/0.41 inference(resolution,[status(thm)],[f603,f163])).
% 0.08/0.41 fof(f605,definition,(
% 0.08/0.41 ![X0]: (sQ12_spl <=> (~aSubsetOf0(X0,szNzAzT0)|aSubsetOf0(X0,szNzAzT0)))),
% 0.08/0.41 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.08/0.41 fof(f608,plain,(
% 0.08/0.41 sQ12_spl|~sQ10_spl),
% 0.08/0.41 inference(split_clause,[status(thm)],[f604,f605,f593])).
% 0.08/0.42 fof(f610,plain,(
% 0.08/0.42 ![X0,X1]: (~aSet0(X0)|~aSubsetOf0(X1,X0)|~aSubsetOf0(X0,slcrc0)|aSubsetOf0(X1,slcrc0))),
% 0.08/0.42 inference(resolution,[status(thm)],[f532,f602])).
% 0.08/0.42 fof(f612,plain,(
% 0.08/0.42 aSubsetOf0(slcrc0,slcrc0)),
% 0.08/0.42 inference(resolution,[status(thm)],[f532,f122])).
% 0.08/0.42 fof(f621,plain,(
% 0.08/0.42 ![X0,X1]: (~aSet0(X0)|~aSubsetOf0(X1,X0)|~aSubsetOf0(X0,xT)|aSubsetOf0(X1,xT))),
% 0.08/0.42 inference(resolution,[status(thm)],[f343,f602])).
% 0.08/0.42 fof(f622,plain,(
% 0.08/0.42 ![X0]: (~aSubsetOf0(X0,xT)|~aSubsetOf0(xT,X0)|X0=xT)),
% 0.08/0.42 inference(resolution,[status(thm)],[f343,f590])).
% 0.08/0.42 fof(f623,plain,(
% 0.08/0.42 aSubsetOf0(xT,xT)),
% 0.08/0.42 inference(resolution,[status(thm)],[f343,f122])).
% 0.08/0.42 fof(f632,plain,(
% 0.08/0.42 ![X0,X1]: (~aSet0(X0)|~aSubsetOf0(X1,X0)|~aSubsetOf0(X0,xS)|aSubsetOf0(X1,xS))),
% 0.08/0.42 inference(resolution,[status(thm)],[f347,f602])).
% 0.08/0.42 fof(f633,plain,(
% 0.08/0.42 ![X0]: (~aSubsetOf0(X0,xS)|~aSubsetOf0(xS,X0)|X0=xS)),
% 0.08/0.42 inference(resolution,[status(thm)],[f347,f590])).
% 0.08/0.42 fof(f634,plain,(
% 0.08/0.42 aSubsetOf0(xS,xS)),
% 0.08/0.42 inference(resolution,[status(thm)],[f347,f122])).
% 0.08/0.42 fof(f642,plain,(
% 0.08/0.42 ~aSet0(szNzAzT0)|aElement0(xi)),
% 0.08/0.42 inference(resolution,[status(thm)],[f94,f402])).
% 0.08/0.42 fof(f643,plain,(
% 0.08/0.42 ![X0,X1,X2]: (~aSet0(X0)|aElement0(X1)|~aSet0(X0)|~aSubsetOf0(X2,X0)|~aElementOf0(X1,X2))),
% 0.08/0.42 inference(resolution,[status(thm)],[f94,f116])).
% 0.08/0.42 fof(f644,definition,(
% 0.08/0.42 sQ19_spl <=> (aElement0(xi))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f647,plain,(
% 0.08/0.42 ~sQ9_spl|sQ19_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f642,f586,f644])).
% 0.08/0.42 fof(f648,plain,(
% 0.08/0.42 ![X0,X1,X2]: (~aSet0(X0)|aElement0(X1)|~aSubsetOf0(X2,X0)|~aElementOf0(X1,X2))),
% 0.08/0.42 inference(duplicate_literals_removal,[status(thm)],[f643])).
% 0.08/0.42 fof(f649,plain,(
% 0.08/0.42 $false|sQ9_spl),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f588,f163])).
% 0.08/0.42 fof(f650,plain,(
% 0.08/0.42 sQ9_spl),
% 0.08/0.42 inference(contradiction_clause,[status(thm)],[f649])).
% 0.08/0.42 fof(f651,plain,(
% 0.08/0.42 ![X0,X1]: (~aSet0(slcrc0)|~aSubsetOf0(X0,slcrc0)|~aElementOf0(X1,X0))),
% 0.08/0.42 inference(resolution,[status(thm)],[f533,f116])).
% 0.08/0.42 fof(f652,definition,(
% 0.08/0.42 sQ20_spl <=> (aSet0(slcrc0))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f654,plain,(
% 0.08/0.42 ~aSet0(slcrc0)|sQ20_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f652])).
% 0.08/0.42 fof(f655,definition,(
% 0.08/0.42 ![X0,X1]: (sQ21_spl <=> (~aSubsetOf0(X0,slcrc0)|~aElementOf0(X1,X0)))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f658,plain,(
% 0.08/0.42 ~sQ20_spl|sQ21_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f651,f652,f655])).
% 0.08/0.42 fof(f659,plain,(
% 0.08/0.42 $false|sQ20_spl),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f654,f532])).
% 0.08/0.42 fof(f660,plain,(
% 0.08/0.42 sQ20_spl),
% 0.08/0.42 inference(contradiction_clause,[status(thm)],[f659])).
% 0.08/0.42 fof(f661,plain,(
% 0.08/0.42 slcrc0=slcrc0|~aSet0(slcrc0)),
% 0.08/0.42 inference(resolution,[status(thm)],[f103,f533])).
% 0.08/0.42 fof(f663,definition,(
% 0.08/0.42 sQ22_spl <=> (slcrc0=slcrc0)),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f666,plain,(
% 0.08/0.42 sQ22_spl|~sQ20_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f661,f663,f652])).
% 0.08/0.42 fof(f671,definition,(
% 0.08/0.42 sQ23_spl <=> (aSet0(xT))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f673,plain,(
% 0.08/0.42 ~aSet0(xT)|sQ23_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f671])).
% 0.08/0.42 fof(f675,plain,(
% 0.08/0.42 ![X0]: (~aSet0(slcrc0)|~aSubsetOf0(X0,slcrc0)|aSubsetOf0(X0,slcrc0))),
% 0.08/0.42 inference(resolution,[status(thm)],[f610,f612])).
% 0.08/0.42 fof(f676,definition,(
% 0.08/0.42 ![X0]: (sQ24_spl <=> (~aSubsetOf0(X0,slcrc0)|aSubsetOf0(X0,slcrc0)))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f679,plain,(
% 0.08/0.42 ~sQ20_spl|sQ24_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f675,f652,f676])).
% 0.08/0.42 fof(f681,definition,(
% 0.08/0.42 sQ25_spl <=> (aSet0(xS))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f695,plain,(
% 0.08/0.42 ![X0]: (~aSet0(xT)|~aSubsetOf0(X0,xT)|aSubsetOf0(X0,xT))),
% 0.08/0.42 inference(resolution,[status(thm)],[f621,f623])).
% 0.08/0.42 fof(f696,definition,(
% 0.08/0.42 ![X0]: (sQ27_spl <=> (~aSubsetOf0(X0,xT)|aSubsetOf0(X0,xT)))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f699,plain,(
% 0.08/0.42 ~sQ23_spl|sQ27_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f695,f671,f696])).
% 0.08/0.42 fof(f700,plain,(
% 0.08/0.42 $false|sQ23_spl),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f673,f343])).
% 0.08/0.42 fof(f701,plain,(
% 0.08/0.42 sQ23_spl),
% 0.08/0.42 inference(contradiction_clause,[status(thm)],[f700])).
% 0.08/0.42 fof(f704,plain,(
% 0.08/0.42 ~aSet0(szNzAzT0)|aElement0(sz00)),
% 0.08/0.42 inference(resolution,[status(thm)],[f165,f94])).
% 0.08/0.42 fof(f705,definition,(
% 0.08/0.42 sQ28_spl <=> (aElement0(sz00))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f708,plain,(
% 0.08/0.42 ~sQ9_spl|sQ28_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f704,f586,f705])).
% 0.08/0.42 fof(f709,plain,(
% 0.08/0.42 ~aSet0(szNzAzT0)|aElement0(xK)),
% 0.08/0.42 inference(resolution,[status(thm)],[f345,f94])).
% 0.08/0.42 fof(f710,definition,(
% 0.08/0.42 sQ29_spl <=> (aElement0(xK))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f713,plain,(
% 0.08/0.42 ~sQ9_spl|sQ29_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f709,f586,f710])).
% 0.08/0.42 fof(f714,plain,(
% 0.08/0.42 ~aSet0(szNzAzT0)|aSet0(xS)),
% 0.08/0.42 inference(resolution,[status(thm)],[f349,f115])).
% 0.08/0.42 fof(f715,plain,(
% 0.08/0.42 ~sQ9_spl|sQ25_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f714,f586,f681])).
% 0.08/0.42 fof(f716,plain,(
% 0.08/0.42 ~aSet0(xS)|~isFinite0(xS)),
% 0.08/0.42 inference(resolution,[status(thm)],[f108,f350])).
% 0.08/0.42 fof(f717,plain,(
% 0.08/0.42 ~aSet0(szNzAzT0)|~isFinite0(szNzAzT0)),
% 0.08/0.42 inference(resolution,[status(thm)],[f108,f164])).
% 0.08/0.42 fof(f718,definition,(
% 0.08/0.42 sQ30_spl <=> (isFinite0(xS))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f721,plain,(
% 0.08/0.42 ~sQ25_spl|~sQ30_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f716,f681,f718])).
% 0.08/0.42 fof(f722,definition,(
% 0.08/0.42 sQ31_spl <=> (isFinite0(szNzAzT0))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f725,plain,(
% 0.08/0.42 ~sQ9_spl|~sQ31_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f717,f586,f722])).
% 0.08/0.42 fof(f727,plain,(
% 0.08/0.42 ![X0]: (~aSet0(X0)|aSubsetOf0(slcrc0,X0)|~aSet0(slcrc0))),
% 0.08/0.42 inference(resolution,[status(thm)],[f117,f533])).
% 0.08/0.42 fof(f729,definition,(
% 0.08/0.42 ![X0]: (sQ32_spl <=> (~aSet0(X0)|aSubsetOf0(slcrc0,X0)))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f732,plain,(
% 0.08/0.42 sQ32_spl|~sQ20_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f727,f729,f652])).
% 0.08/0.42 fof(f736,plain,(
% 0.08/0.42 ~aSubsetOf0(xT,xT)|xT=xT),
% 0.08/0.42 inference(resolution,[status(thm)],[f622,f623])).
% 0.08/0.42 fof(f737,definition,(
% 0.08/0.42 sQ33_spl <=> (aSubsetOf0(xT,xT))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f739,plain,(
% 0.08/0.42 ~aSubsetOf0(xT,xT)|sQ33_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f737])).
% 0.08/0.42 fof(f740,definition,(
% 0.08/0.42 sQ34_spl <=> (xT=xT)),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f743,plain,(
% 0.08/0.42 ~sQ33_spl|sQ34_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f736,f737,f740])).
% 0.08/0.42 fof(f744,plain,(
% 0.08/0.42 $false|sQ33_spl),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f739,f623])).
% 0.08/0.42 fof(f745,plain,(
% 0.08/0.42 sQ33_spl),
% 0.08/0.42 inference(contradiction_clause,[status(thm)],[f744])).
% 0.08/0.42 fof(f747,plain,(
% 0.08/0.42 ~aSubsetOf0(xS,xS)|xS=xS),
% 0.08/0.42 inference(resolution,[status(thm)],[f633,f634])).
% 0.08/0.42 fof(f748,definition,(
% 0.08/0.42 sQ35_spl <=> (aSubsetOf0(xS,xS))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f750,plain,(
% 0.08/0.42 ~aSubsetOf0(xS,xS)|sQ35_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f748])).
% 0.08/0.42 fof(f751,definition,(
% 0.08/0.42 sQ36_spl <=> (xS=xS)),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f754,plain,(
% 0.08/0.42 ~sQ35_spl|sQ36_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f747,f748,f751])).
% 0.08/0.42 fof(f755,plain,(
% 0.08/0.42 $false|sQ35_spl),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f750,f634])).
% 0.08/0.42 fof(f756,plain,(
% 0.08/0.42 sQ35_spl),
% 0.08/0.42 inference(contradiction_clause,[status(thm)],[f755])).
% 0.08/0.42 fof(f757,plain,(
% 0.08/0.42 ![X0,X1]: (aElement0(X0)|~aSubsetOf0(X1,xS)|~aElementOf0(X0,X1))),
% 0.08/0.42 inference(resolution,[status(thm)],[f648,f347])).
% 0.08/0.42 fof(f758,plain,(
% 0.08/0.42 ![X0,X1]: (aElement0(X0)|~aSubsetOf0(X1,xT)|~aElementOf0(X0,X1))),
% 0.08/0.42 inference(resolution,[status(thm)],[f648,f343])).
% 0.08/0.42 fof(f760,plain,(
% 0.08/0.42 ![X0,X1]: (aElement0(X0)|~aSubsetOf0(X1,szNzAzT0)|~aElementOf0(X0,X1))),
% 0.08/0.42 inference(resolution,[status(thm)],[f648,f163])).
% 0.08/0.42 fof(f761,plain,(
% 0.08/0.42 ![X0]: (aElement0(X0)|~aElementOf0(X0,xS))),
% 0.08/0.42 inference(resolution,[status(thm)],[f757,f634])).
% 0.08/0.42 fof(f762,plain,(
% 0.08/0.42 ![X0]: (aElement0(sK1_skl(xS,X0))|~aSet0(X0)|aSubsetOf0(xS,X0)|~aSet0(xS))),
% 0.08/0.42 inference(resolution,[status(thm)],[f761,f117])).
% 0.08/0.42 fof(f763,plain,(
% 0.08/0.42 aElement0(sK0_skl(xS))|xS=slcrc0|~aSet0(xS)),
% 0.08/0.42 inference(resolution,[status(thm)],[f761,f103])).
% 0.08/0.42 fof(f764,plain,(
% 0.08/0.42 ![X0,X1]: (aElement0(X0)|~aSet0(xS)|~aSubsetOf0(X1,xS)|~aElementOf0(X0,X1))),
% 0.08/0.42 inference(resolution,[status(thm)],[f761,f116])).
% 0.08/0.42 fof(f765,definition,(
% 0.08/0.42 ![X0]: (sQ37_spl <=> (aElement0(sK1_skl(xS,X0))|~aSet0(X0)|aSubsetOf0(xS,X0)))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f768,plain,(
% 0.08/0.42 sQ37_spl|~sQ25_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f762,f765,f681])).
% 0.08/0.42 fof(f769,definition,(
% 0.08/0.42 sQ38_spl <=> (aElement0(sK0_skl(xS)))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f772,definition,(
% 0.08/0.42 sQ39_spl <=> (xS=slcrc0)),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f775,plain,(
% 0.08/0.42 sQ38_spl|sQ39_spl|~sQ25_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f763,f769,f772,f681])).
% 0.08/0.42 fof(f776,definition,(
% 0.08/0.42 ![X0,X1]: (sQ40_spl <=> (aElement0(X0)|~aSubsetOf0(X1,xS)|~aElementOf0(X0,X1)))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f779,plain,(
% 0.08/0.42 sQ40_spl|~sQ25_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f764,f776,f681])).
% 0.08/0.42 fof(f780,plain,(
% 0.08/0.42 ![X0]: (~aSet0(xS)|~aSubsetOf0(X0,xS)|aSubsetOf0(X0,xS))),
% 0.08/0.42 inference(resolution,[status(thm)],[f632,f634])).
% 0.08/0.42 fof(f781,definition,(
% 0.08/0.42 ![X0]: (sQ41_spl <=> (~aSubsetOf0(X0,xS)|aSubsetOf0(X0,xS)))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f784,plain,(
% 0.08/0.42 ~sQ25_spl|sQ41_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f780,f681,f781])).
% 0.08/0.42 fof(f785,plain,(
% 0.08/0.42 ![X0]: (aElement0(X0)|~aElementOf0(X0,xT))),
% 0.08/0.42 inference(resolution,[status(thm)],[f758,f623])).
% 0.08/0.42 fof(f786,plain,(
% 0.08/0.42 ~aSet0(szNzAzT0)|aElement0(xk)),
% 0.08/0.42 inference(resolution,[status(thm)],[f381,f94])).
% 0.08/0.42 fof(f787,definition,(
% 0.08/0.42 sQ42_spl <=> (aElement0(xk))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f790,plain,(
% 0.08/0.42 ~sQ9_spl|sQ42_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f786,f586,f787])).
% 0.08/0.42 fof(f792,plain,(
% 0.08/0.42 aSet0(szDzozmdt0(xc))),
% 0.08/0.42 inference(resolution,[status(thm)],[f296,f355])).
% 0.08/0.42 fof(f795,plain,(
% 0.08/0.42 ![X0]: (~aSubsetOf0(X0,szDzozmdt0(xc))|~aSubsetOf0(szDzozmdt0(xc),szNzAzT0)|aSubsetOf0(X0,szNzAzT0))),
% 0.08/0.42 inference(resolution,[status(thm)],[f792,f603])).
% 0.08/0.42 fof(f798,plain,(
% 0.08/0.42 aSubsetOf0(szDzozmdt0(xc),szDzozmdt0(xc))),
% 0.08/0.42 inference(resolution,[status(thm)],[f792,f122])).
% 0.08/0.42 fof(f799,definition,(
% 0.08/0.42 ![X0]: (sQ43_spl <=> (~aSubsetOf0(X0,szDzozmdt0(xc))|aSubsetOf0(X0,szNzAzT0)))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f800,plain,(
% 0.08/0.42 ![X0]: (~aSubsetOf0(X0,szDzozmdt0(xc))|aSubsetOf0(X0,szNzAzT0)|~sQ43_spl)),
% 0.08/0.42 inference(component_clause,[status(thm)],[f799])).
% 0.08/0.42 fof(f802,definition,(
% 0.08/0.42 sQ44_spl <=> (aSubsetOf0(szDzozmdt0(xc),szNzAzT0))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f805,plain,(
% 0.08/0.42 sQ43_spl|~sQ44_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f795,f799,f802])).
% 0.08/0.42 fof(f810,plain,(
% 0.08/0.42 ![X0]: (~aSet0(xT)|~aSubsetOf0(X0,xT)|isFinite0(X0))),
% 0.08/0.42 inference(resolution,[status(thm)],[f120,f344])).
% 0.08/0.42 fof(f811,plain,(
% 0.08/0.42 ![X0]: (~aSet0(slcrc0)|~aSubsetOf0(X0,slcrc0)|isFinite0(X0))),
% 0.08/0.42 inference(resolution,[status(thm)],[f120,f104])).
% 0.08/0.42 fof(f812,definition,(
% 0.08/0.42 ![X0]: (sQ45_spl <=> (~aSubsetOf0(X0,xT)|isFinite0(X0)))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f815,plain,(
% 0.08/0.42 ~sQ23_spl|sQ45_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f810,f671,f812])).
% 0.08/0.42 fof(f816,definition,(
% 0.08/0.42 ![X0]: (sQ46_spl <=> (~aSubsetOf0(X0,slcrc0)|isFinite0(X0)))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f819,plain,(
% 0.08/0.42 ~sQ20_spl|sQ46_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f811,f652,f816])).
% 0.08/0.42 fof(f825,plain,(
% 0.08/0.42 ![X0]: (aElement0(sK1_skl(xT,X0))|~aSet0(X0)|aSubsetOf0(xT,X0)|~aSet0(xT))),
% 0.08/0.42 inference(resolution,[status(thm)],[f785,f117])).
% 0.08/0.42 fof(f826,plain,(
% 0.08/0.42 aElement0(sK0_skl(xT))|xT=slcrc0|~aSet0(xT)),
% 0.08/0.42 inference(resolution,[status(thm)],[f785,f103])).
% 0.08/0.42 fof(f827,plain,(
% 0.08/0.42 ![X0,X1]: (aElement0(X0)|~aSet0(xT)|~aSubsetOf0(X1,xT)|~aElementOf0(X0,X1))),
% 0.08/0.42 inference(resolution,[status(thm)],[f785,f116])).
% 0.08/0.42 fof(f828,definition,(
% 0.08/0.42 ![X0]: (sQ47_spl <=> (aElement0(sK1_skl(xT,X0))|~aSet0(X0)|aSubsetOf0(xT,X0)))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f831,plain,(
% 0.08/0.42 sQ47_spl|~sQ23_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f825,f828,f671])).
% 0.08/0.42 fof(f832,definition,(
% 0.08/0.42 sQ48_spl <=> (aElement0(sK0_skl(xT)))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f835,definition,(
% 0.08/0.42 sQ49_spl <=> (xT=slcrc0)),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f838,plain,(
% 0.08/0.42 sQ48_spl|sQ49_spl|~sQ23_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f826,f832,f835,f671])).
% 0.08/0.42 fof(f839,definition,(
% 0.08/0.42 ![X0,X1]: (sQ50_spl <=> (aElement0(X0)|~aSubsetOf0(X1,xT)|~aElementOf0(X0,X1)))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f842,plain,(
% 0.08/0.42 sQ50_spl|~sQ23_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f827,f839,f671])).
% 0.08/0.42 fof(f844,definition,(
% 0.08/0.42 sQ51_spl <=> (aSet0(szDzozmdt0(xc)))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f852,plain,(
% 0.08/0.42 ![X0]: (aElement0(X0)|~aElementOf0(X0,szNzAzT0))),
% 0.08/0.42 inference(resolution,[status(thm)],[f760,f584])).
% 0.08/0.42 fof(f854,plain,(
% 0.08/0.42 ![X0]: (aElement0(sK1_skl(szNzAzT0,X0))|~aSet0(X0)|aSubsetOf0(szNzAzT0,X0)|~aSet0(szNzAzT0))),
% 0.08/0.42 inference(resolution,[status(thm)],[f852,f117])).
% 0.08/0.42 fof(f857,plain,(
% 0.08/0.42 aElement0(sK0_skl(szNzAzT0))|szNzAzT0=slcrc0|~aSet0(szNzAzT0)),
% 0.08/0.42 inference(resolution,[status(thm)],[f852,f103])).
% 0.08/0.42 fof(f858,plain,(
% 0.08/0.42 ![X0,X1]: (aElement0(X0)|~aSet0(szNzAzT0)|~aSubsetOf0(X1,szNzAzT0)|~aElementOf0(X0,X1))),
% 0.08/0.42 inference(resolution,[status(thm)],[f852,f116])).
% 0.08/0.42 fof(f859,definition,(
% 0.08/0.42 ![X0]: (sQ52_spl <=> (aElement0(sK1_skl(szNzAzT0,X0))|~aSet0(X0)|aSubsetOf0(szNzAzT0,X0)))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f862,plain,(
% 0.08/0.42 sQ52_spl|~sQ9_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f854,f859,f586])).
% 0.08/0.42 fof(f863,definition,(
% 0.08/0.42 sQ53_spl <=> (aElement0(sK0_skl(szNzAzT0)))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f866,definition,(
% 0.08/0.42 sQ54_spl <=> (szNzAzT0=slcrc0)),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f869,plain,(
% 0.08/0.42 sQ53_spl|sQ54_spl|~sQ9_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f857,f863,f866,f586])).
% 0.08/0.42 fof(f870,definition,(
% 0.08/0.42 ![X0,X1]: (sQ55_spl <=> (aElement0(X0)|~aSubsetOf0(X1,szNzAzT0)|~aElementOf0(X0,X1)))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f873,plain,(
% 0.08/0.42 sQ55_spl|~sQ9_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f858,f870,f586])).
% 0.08/0.42 fof(f874,plain,(
% 0.08/0.42 aSubsetOf0(szDzozmdt0(xc),szNzAzT0)|~sQ43_spl),
% 0.08/0.42 inference(resolution,[status(thm)],[f800,f798])).
% 0.08/0.42 fof(f876,plain,(
% 0.08/0.42 ~aSet0(szNzAzT0)|aSet0(szDzozmdt0(xc))|~sQ43_spl),
% 0.08/0.42 inference(resolution,[status(thm)],[f874,f115])).
% 0.08/0.42 fof(f877,plain,(
% 0.08/0.42 ~sQ9_spl|sQ51_spl|~sQ43_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f876,f586,f844,f799])).
% 0.08/0.42 fof(f878,plain,(
% 0.08/0.42 ~isCountable0(sdtlpdtrp0(xN,sz00))|~sQ0_spl|sQ6_spl),
% 0.08/0.42 inference(forward_demodulation,[status(thm)],[f497,f521])).
% 0.08/0.42 fof(f879,plain,(
% 0.08/0.42 ~isCountable0(xS)|~sQ0_spl|sQ6_spl),
% 0.08/0.42 inference(forward_demodulation,[status(thm)],[f390,f878])).
% 0.08/0.42 fof(f880,plain,(
% 0.08/0.42 $false|~sQ0_spl|sQ6_spl),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f879,f350])).
% 0.08/0.42 fof(f881,plain,(
% 0.08/0.42 ~sQ0_spl|sQ6_spl),
% 0.08/0.42 inference(contradiction_clause,[status(thm)],[f880])).
% 0.08/0.42 fof(f888,plain,(
% 0.08/0.42 ~aSubsetOf0(sdtlpdtrp0(xN,sz00),szNzAzT0)|~sQ0_spl|sQ5_spl),
% 0.08/0.42 inference(forward_demodulation,[status(thm)],[f497,f517])).
% 0.08/0.42 fof(f889,plain,(
% 0.08/0.42 ~aSubsetOf0(xS,szNzAzT0)|~sQ0_spl|sQ5_spl),
% 0.08/0.42 inference(forward_demodulation,[status(thm)],[f390,f888])).
% 0.08/0.42 fof(f890,plain,(
% 0.08/0.42 $false|~sQ0_spl|sQ5_spl),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f889,f349])).
% 0.08/0.42 fof(f891,plain,(
% 0.08/0.42 ~sQ0_spl|sQ5_spl),
% 0.08/0.42 inference(contradiction_clause,[status(thm)],[f890])).
% 0.08/0.42 fof(f892,plain,(
% 0.08/0.42 $false),
% 0.08/0.42 inference(sat_refutation,[status(thm)],[f518,f522,f531,f599,f601,f608,f647,f650,f658,f660,f666,f679,f699,f701,f708,f713,f715,f721,f725,f732,f743,f745,f754,f756,f768,f775,f779,f784,f790,f805,f815,f819,f831,f838,f842,f862,f869,f873,f877,f881,f891])).
% 0.08/0.42 % SZS output end CNFRefutation for theBenchmark.p
% 0.08/0.43 % Elapsed time: 0.074116 seconds
% 0.08/0.43 % CPU time: 0.364958 seconds
% 0.08/0.43 % Total memory used: 79.071 MB
% 0.08/0.43 % Net memory used: 78.624 MB
%------------------------------------------------------------------------------