%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM594+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 01:43:18 PM UTC 2026
% Result : Theorem 6.26s 6.49s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM594+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/5.61 % Computer : n026.cluster.edu
% 0.14/5.61 % Model : x86_64 x86_64
% 0.14/5.61 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/5.61 % Memory : 8046.5625MB
% 0.14/5.61 % OS : Linux 6.8.0-71-generic
% 0.14/5.61 % CPULimit : 300
% 0.14/5.61 % WCLimit : 300
% 0.14/5.61 % DateTime : Mon Sep 21 02:45:59 UTC 2026
% 0.14/5.61 % CPUTime :
% 0.14/5.63 % Drodi V4.1.1
% 6.26/6.49 % Refutation found
% 6.26/6.49 % SZS status Theorem for theBenchmark: Theorem is valid
% 6.26/6.49 % SZS output start CNFRefutation for theBenchmark
% 6.26/6.49 fof(f5,definition,(
% 6.26/6.49 (! [W0] :( W0 = slcrc0<=> ( aSet0(W0)& ~ (? [W1] : aElementOf0(W1,W0) )) ) )),
% 6.26/6.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.26/6.49 fof(f9,axiom,(
% 6.26/6.49 (! [W0] :( ( aSet0(W0)& isCountable0(W0) )=> W0 != slcrc0 ) )),
% 6.26/6.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.26/6.49 fof(f12,axiom,(
% 6.26/6.49 (! [W0] :( aSet0(W0)=> aSubsetOf0(W0,W0) ) )),
% 6.26/6.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.26/6.49 fof(f16,definition,(
% 6.26/6.49 (! [W0,W1] :( ( aSet0(W0)& aElement0(W1) )=> (! [W2] :( W2 = sdtmndt0(W0,W1)<=> ( aSet0(W2)& (! [W3] :( aElementOf0(W3,W2)<=> ( aElement0(W3)& aElementOf0(W3,W0)& W3 != W1 ) ) )) ) )) )),
% 6.26/6.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.26/6.49 fof(f23,axiom,(
% 6.26/6.49 ( aSet0(szNzAzT0)& isCountable0(szNzAzT0) ) ),
% 6.26/6.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.26/6.49 fof(f24,axiom,(
% 6.26/6.49 aElementOf0(sz00,szNzAzT0) ),
% 6.26/6.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.26/6.49 fof(f25,axiom,(
% 6.26/6.49 (! [W0] :( aElementOf0(W0,szNzAzT0)=> ( aElementOf0(szszuzczcdt0(W0),szNzAzT0)& szszuzczcdt0(W0) != sz00 ) ) )),
% 6.26/6.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.26/6.49 fof(f28,axiom,(
% 6.26/6.49 (! [W0] :( aElementOf0(W0,szNzAzT0)=> W0 != szszuzczcdt0(W0) ) )),
% 6.26/6.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.26/6.49 fof(f42,axiom,(
% 6.26/6.49 (! [W0] :( aSet0(W0)=> ( sbrdtbr0(W0) = sz00<=> W0 = slcrc0 ) ) )),
% 6.26/6.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.26/6.49 fof(f50,definition,(
% 6.26/6.49 (! [W0] :( aElementOf0(W0,szNzAzT0)=> (! [W1] :( W1 = slbdtrb0(W0)<=> ( aSet0(W1)& (! [W2] :( aElementOf0(W2,W1)<=> ( aElementOf0(W2,szNzAzT0)& sdtlseqdt0(szszuzczcdt0(W2),W0) ) ) )) ) )) )),
% 6.26/6.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.26/6.49 fof(f51,axiom,(
% 6.26/6.49 (! [W0] :( aElementOf0(W0,szNzAzT0)=> isFinite0(slbdtrb0(W0)) ) )),
% 6.26/6.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.26/6.49 fof(f68,definition,(
% 6.26/6.49 (! [W0] :( aFunction0(W0)=> (! [W1] :( aSubsetOf0(W1,szDzozmdt0(W0))=> (! [W2] :( W2 = sdtlcdtrc0(W0,W1)<=> ( aSet0(W2)& (! [W3] :( aElementOf0(W3,W2)<=> (? [W4] :( aElementOf0(W4,W1)& sdtlpdtrp0(W0,W4) = W3 ) )) )) ) )) )) )),
% 6.26/6.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.26/6.49 fof(f74,hypothesis,(
% 6.26/6.49 aElementOf0(xK,szNzAzT0) ),
% 6.26/6.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.26/6.49 fof(f75,hypothesis,(
% 6.26/6.49 ( aSubsetOf0(xS,szNzAzT0)& isCountable0(xS) ) ),
% 6.26/6.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.26/6.49 fof(f78,hypothesis,(
% 6.26/6.49 xK != sz00 ),
% 6.26/6.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.26/6.49 fof(f80,hypothesis,(
% 6.26/6.49 ( aElementOf0(xk,szNzAzT0)& szszuzczcdt0(xk) = xK ) ),
% 6.26/6.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.26/6.49 fof(f81,hypothesis,(
% 6.26/6.49 ( aFunction0(xN)& szDzozmdt0(xN) = szNzAzT0& sdtlpdtrp0(xN,sz00) = xS& (! [W0] :( aElementOf0(W0,szNzAzT0)=> ( ( aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0)& isCountable0(sdtlpdtrp0(xN,W0)) )=> ( aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))& isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(W0))) ) ) ) )) ),
% 6.26/6.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.26/6.49 fof(f86,hypothesis,(
% 6.26/6.49 ( aFunction0(xC)& szDzozmdt0(xC) = szNzAzT0& (! [W0] :( aElementOf0(W0,szNzAzT0)=> ( aFunction0(sdtlpdtrp0(xC,W0))& szDzozmdt0(sdtlpdtrp0(xC,W0)) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk)& (! [W1] :( ( aSet0(W1)& aElementOf0(W1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk)) )=> sdtlpdtrp0(sdtlpdtrp0(xC,W0),W1) = sdtlpdtrp0(xc,sdtpldt0(W1,szmzizndt0(sdtlpdtrp0(xN,W0)))) ) )) ) )) ),
% 6.26/6.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.26/6.49 fof(f91,hypothesis,(
% 6.26/6.49 ( aFunction0(xe)& szDzozmdt0(xe) = szNzAzT0& (! [W0] :( aElementOf0(W0,szNzAzT0)=> sdtlpdtrp0(xe,W0) = szmzizndt0(sdtlpdtrp0(xN,W0)) ) )) ),
% 6.26/6.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.26/6.49 fof(f92,hypothesis,(
% 6.26/6.49 ( aFunction0(xd)& szDzozmdt0(xd) = szNzAzT0& (! [W0] :( aElementOf0(W0,szNzAzT0)=> (! [W1] :( ( aSet0(W1)& aElementOf0(W1,slbdtsldtrb0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),xk)) )=> sdtlpdtrp0(xd,W0) = sdtlpdtrp0(sdtlpdtrp0(xC,W0),W1) ) )) )) ),
% 6.26/6.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.26/6.49 fof(f94,hypothesis,(
% 6.26/6.49 aElementOf0(xx,sdtlcdtrc0(xd,szDzozmdt0(xd))) ),
% 6.26/6.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.26/6.49 fof(f95,conjecture,(
% 6.26/6.49 (? [W0] :( aElementOf0(W0,szNzAzT0)& sdtlpdtrp0(xd,W0) = xx ) )),
% 6.26/6.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.26/6.49 fof(f96,negated_conjecture,(
% 6.26/6.49 ~((? [W0] :( aElementOf0(W0,szNzAzT0)& sdtlpdtrp0(xd,W0) = xx ) ))),
% 6.26/6.49 inference(negated_conjecture,[status(cth)],[f95])).
% 6.26/6.49 fof(f107,plain,(
% 6.26/6.49 ![W0]: (W0=slcrc0<=>(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0))))),
% 6.26/6.49 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 6.26/6.49 fof(f108,plain,(
% 6.26/6.49 ![W0]: ((~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0))))&(W0=slcrc0|(~aSet0(W0)|(?[W1]: aElementOf0(W1,W0)))))),
% 6.26/6.49 inference(NNF_transformation,[status(thm)],[f107])).
% 6.26/6.49 fof(f109,plain,(
% 6.26/6.49 (![W0]: (~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0)))))&(![W0]: (W0=slcrc0|(~aSet0(W0)|(?[W1]: aElementOf0(W1,W0)))))),
% 6.26/6.49 inference(miniscoping,[status(thm)],[f108])).
% 6.26/6.49 fof(f110,plain,(
% 6.26/6.49 (![W0]: (~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0)))))&(![W0]: (W0=slcrc0|(~aSet0(W0)|aElementOf0(sK0_skl(W0),W0))))),
% 6.26/6.49 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(W1,sK0_skl(W0))],[f109])).
% 6.26/6.49 fof(f111,plain,(
% 6.26/6.49 ![X0]: (~X0=slcrc0|aSet0(X0))),
% 6.26/6.49 inference(cnf_transformation,[status(thm)],[f110])).
% 6.26/6.49 fof(f112,plain,(
% 6.26/6.49 ![X0,X1]: (~X0=slcrc0|~aElementOf0(X1,X0))),
% 6.26/6.49 inference(cnf_transformation,[status(thm)],[f110])).
% 6.26/6.49 fof(f119,plain,(
% 6.26/6.49 ![W0]: ((~aSet0(W0)|~isCountable0(W0))|~W0=slcrc0)),
% 6.26/6.49 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 6.26/6.49 fof(f120,plain,(
% 6.26/6.49 ![X0]: (~aSet0(X0)|~isCountable0(X0)|~X0=slcrc0)),
% 6.26/6.49 inference(cnf_transformation,[status(thm)],[f119])).
% 6.26/6.49 fof(f131,plain,(
% 6.26/6.49 ![W0]: (~aSet0(W0)|aSubsetOf0(W0,W0))),
% 6.26/6.49 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 6.26/6.49 fof(f132,plain,(
% 6.26/6.49 ![X0]: (~aSet0(X0)|aSubsetOf0(X0,X0))),
% 6.26/6.49 inference(cnf_transformation,[status(thm)],[f131])).
% 6.26/6.49 fof(f150,plain,(
% 6.26/6.49 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|(![W2]: (W2=sdtmndt0(W0,W1)<=>(aSet0(W2)&(![W3]: (aElementOf0(W3,W2)<=>((aElement0(W3)&aElementOf0(W3,W0))&~W3=W1)))))))),
% 6.26/6.49 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 6.26/6.49 fof(f151,definition,(
% 6.26/6.49 ![W0,W1,W3]: (sP0_prd(W3,W1,W0)<=>((aElement0(W3)&aElementOf0(W3,W0))&~W3=W1))),
% 6.26/6.49 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 6.26/6.49 fof(f173,plain,(
% 6.26/6.49 aSet0(szNzAzT0)),
% 6.26/6.49 inference(cnf_transformation,[status(thm)],[f23])).
% 6.26/6.49 fof(f174,plain,(
% 6.26/6.49 isCountable0(szNzAzT0)),
% 6.26/6.49 inference(cnf_transformation,[status(thm)],[f23])).
% 6.26/6.49 fof(f175,plain,(
% 6.26/6.49 aElementOf0(sz00,szNzAzT0)),
% 6.26/6.49 inference(cnf_transformation,[status(thm)],[f24])).
% 6.26/6.49 fof(f176,plain,(
% 6.26/6.49 ![W0]: (~aElementOf0(W0,szNzAzT0)|(aElementOf0(szszuzczcdt0(W0),szNzAzT0)&~szszuzczcdt0(W0)=sz00))),
% 6.26/6.49 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 6.26/6.49 fof(f177,plain,(
% 6.26/6.49 ![X0]: (~aElementOf0(X0,szNzAzT0)|aElementOf0(szszuzczcdt0(X0),szNzAzT0))),
% 6.26/6.49 inference(cnf_transformation,[status(thm)],[f176])).
% 6.26/6.49 fof(f178,plain,(
% 6.26/6.49 ![X0]: (~aElementOf0(X0,szNzAzT0)|~szszuzczcdt0(X0)=sz00)),
% 6.26/6.49 inference(cnf_transformation,[status(thm)],[f176])).
% 6.26/6.49 fof(f185,plain,(
% 6.26/6.49 ![W0]: (~aElementOf0(W0,szNzAzT0)|~W0=szszuzczcdt0(W0))),
% 6.26/6.49 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 6.26/6.49 fof(f186,plain,(
% 6.26/6.49 ![X0]: (~aElementOf0(X0,szNzAzT0)|~X0=szszuzczcdt0(X0))),
% 6.26/6.49 inference(cnf_transformation,[status(thm)],[f185])).
% 6.26/6.49 fof(f217,plain,(
% 6.26/6.49 ![W0]: (~aSet0(W0)|(sbrdtbr0(W0)=sz00<=>W0=slcrc0))),
% 6.26/6.49 inference(pre_NNF_transformation,[status(thm)],[f42])).
% 6.26/6.49 fof(f218,plain,(
% 6.26/6.49 ![W0]: (~aSet0(W0)|((~sbrdtbr0(W0)=sz00|W0=slcrc0)&(sbrdtbr0(W0)=sz00|~W0=slcrc0)))),
% 6.26/6.49 inference(NNF_transformation,[status(thm)],[f217])).
% 6.26/6.49 fof(f220,plain,(
% 6.26/6.49 ![X0]: (~aSet0(X0)|sbrdtbr0(X0)=sz00|~X0=slcrc0)),
% 6.26/6.49 inference(cnf_transformation,[status(thm)],[f218])).
% 6.26/6.49 fof(f249,plain,(
% 6.26/6.49 ![W0]: (~aElementOf0(W0,szNzAzT0)|(![W1]: (W1=slbdtrb0(W0)<=>(aSet0(W1)&(![W2]: (aElementOf0(W2,W1)<=>(aElementOf0(W2,szNzAzT0)&sdtlseqdt0(szszuzczcdt0(W2),W0))))))))),
% 6.26/6.49 inference(pre_NNF_transformation,[status(thm)],[f50])).
% 6.26/6.49 fof(f250,plain,(
% 6.26/6.49 ![W0]: (~aElementOf0(W0,szNzAzT0)|(![W1]: ((~W1=slbdtrb0(W0)|(aSet0(W1)&(![W2]: ((~aElementOf0(W2,W1)|(aElementOf0(W2,szNzAzT0)&sdtlseqdt0(szszuzczcdt0(W2),W0)))&(aElementOf0(W2,W1)|(~aElementOf0(W2,szNzAzT0)|~sdtlseqdt0(szszuzczcdt0(W2),W0)))))))&(W1=slbdtrb0(W0)|(~aSet0(W1)|(?[W2]: ((~aElementOf0(W2,W1)|(~aElementOf0(W2,szNzAzT0)|~sdtlseqdt0(szszuzczcdt0(W2),W0)))&(aElementOf0(W2,W1)|(aElementOf0(W2,szNzAzT0)&sdtlseqdt0(szszuzczcdt0(W2),W0))))))))))),
% 6.26/6.49 inference(NNF_transformation,[status(thm)],[f249])).
% 6.26/6.49 fof(f251,plain,(
% 6.26/6.49 ![W0]: (~aElementOf0(W0,szNzAzT0)|((![W1]: (~W1=slbdtrb0(W0)|(aSet0(W1)&((![W2]: (~aElementOf0(W2,W1)|(aElementOf0(W2,szNzAzT0)&sdtlseqdt0(szszuzczcdt0(W2),W0))))&(![W2]: (aElementOf0(W2,W1)|(~aElementOf0(W2,szNzAzT0)|~sdtlseqdt0(szszuzczcdt0(W2),W0))))))))&(![W1]: (W1=slbdtrb0(W0)|(~aSet0(W1)|(?[W2]: ((~aElementOf0(W2,W1)|(~aElementOf0(W2,szNzAzT0)|~sdtlseqdt0(szszuzczcdt0(W2),W0)))&(aElementOf0(W2,W1)|(aElementOf0(W2,szNzAzT0)&sdtlseqdt0(szszuzczcdt0(W2),W0))))))))))),
% 6.26/6.49 inference(miniscoping,[status(thm)],[f250])).
% 6.26/6.49 fof(f252,plain,(
% 6.26/6.49 ![W0]: (~aElementOf0(W0,szNzAzT0)|((![W1]: (~W1=slbdtrb0(W0)|(aSet0(W1)&((![W2]: (~aElementOf0(W2,W1)|(aElementOf0(W2,szNzAzT0)&sdtlseqdt0(szszuzczcdt0(W2),W0))))&(![W2]: (aElementOf0(W2,W1)|(~aElementOf0(W2,szNzAzT0)|~sdtlseqdt0(szszuzczcdt0(W2),W0))))))))&(![W1]: (W1=slbdtrb0(W0)|(~aSet0(W1)|((~aElementOf0(sK8_skl(W1,W0),W1)|(~aElementOf0(sK8_skl(W1,W0),szNzAzT0)|~sdtlseqdt0(szszuzczcdt0(sK8_skl(W1,W0)),W0)))&(aElementOf0(sK8_skl(W1,W0),W1)|(aElementOf0(sK8_skl(W1,W0),szNzAzT0)&sdtlseqdt0(szszuzczcdt0(sK8_skl(W1,W0)),W0)))))))))),
% 6.26/6.49 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(W2,sK8_skl(W1,W0))],[f251])).
% 6.26/6.49 fof(f253,plain,(
% 6.26/6.49 ![X0,X1]: (~aElementOf0(X0,szNzAzT0)|~X1=slbdtrb0(X0)|aSet0(X1))),
% 6.26/6.49 inference(cnf_transformation,[status(thm)],[f252])).
% 6.26/6.49 fof(f260,plain,(
% 6.26/6.49 ![W0]: (~aElementOf0(W0,szNzAzT0)|isFinite0(slbdtrb0(W0)))),
% 6.26/6.49 inference(pre_NNF_transformation,[status(thm)],[f51])).
% 6.26/6.49 fof(f261,plain,(
% 6.26/6.49 ![X0]: (~aElementOf0(X0,szNzAzT0)|isFinite0(slbdtrb0(X0)))),
% 6.26/6.49 inference(cnf_transformation,[status(thm)],[f260])).
% 6.26/6.49 fof(f322,plain,(
% 6.26/6.49 ![W0]: (~aFunction0(W0)|(![W1]: (~aSubsetOf0(W1,szDzozmdt0(W0))|(![W2]: (W2=sdtlcdtrc0(W0,W1)<=>(aSet0(W2)&(![W3]: (aElementOf0(W3,W2)<=>(?[W4]: (aElementOf0(W4,W1)&sdtlpdtrp0(W0,W4)=W3))))))))))),
% 6.26/6.49 inference(pre_NNF_transformation,[status(thm)],[f68])).
% 6.26/6.49 fof(f323,plain,(
% 6.26/6.49 ![W0]: (~aFunction0(W0)|(![W1]: (~aSubsetOf0(W1,szDzozmdt0(W0))|(![W2]: ((~W2=sdtlcdtrc0(W0,W1)|(aSet0(W2)&(![W3]: ((~aElementOf0(W3,W2)|(?[W4]: (aElementOf0(W4,W1)&sdtlpdtrp0(W0,W4)=W3)))&(aElementOf0(W3,W2)|(![W4]: (~aElementOf0(W4,W1)|~sdtlpdtrp0(W0,W4)=W3)))))))&(W2=sdtlcdtrc0(W0,W1)|(~aSet0(W2)|(?[W3]: ((~aElementOf0(W3,W2)|(![W4]: (~aElementOf0(W4,W1)|~sdtlpdtrp0(W0,W4)=W3)))&(aElementOf0(W3,W2)|(?[W4]: (aElementOf0(W4,W1)&sdtlpdtrp0(W0,W4)=W3))))))))))))),
% 6.26/6.49 inference(NNF_transformation,[status(thm)],[f322])).
% 6.26/6.49 fof(f324,plain,(
% 6.26/6.49 ![W0]: (~aFunction0(W0)|(![W1]: (~aSubsetOf0(W1,szDzozmdt0(W0))|((![W2]: (~W2=sdtlcdtrc0(W0,W1)|(aSet0(W2)&((![W3]: (~aElementOf0(W3,W2)|(?[W4]: (aElementOf0(W4,W1)&sdtlpdtrp0(W0,W4)=W3))))&(![W3]: (aElementOf0(W3,W2)|(![W4]: (~aElementOf0(W4,W1)|~sdtlpdtrp0(W0,W4)=W3))))))))&(![W2]: (W2=sdtlcdtrc0(W0,W1)|(~aSet0(W2)|(?[W3]: ((~aElementOf0(W3,W2)|(![W4]: (~aElementOf0(W4,W1)|~sdtlpdtrp0(W0,W4)=W3)))&(aElementOf0(W3,W2)|(?[W4]: (aElementOf0(W4,W1)&sdtlpdtrp0(W0,W4)=W3))))))))))))),
% 6.26/6.49 inference(miniscoping,[status(thm)],[f323])).
% 6.26/6.49 fof(f325,plain,(
% 6.26/6.49 ![W0]: (~aFunction0(W0)|(![W1]: (~aSubsetOf0(W1,szDzozmdt0(W0))|((![W2]: (~W2=sdtlcdtrc0(W0,W1)|(aSet0(W2)&((![W3]: (~aElementOf0(W3,W2)|(aElementOf0(sK13_skl(W3,W2,W1,W0),W1)&sdtlpdtrp0(W0,sK13_skl(W3,W2,W1,W0))=W3)))&(![W3]: (aElementOf0(W3,W2)|(![W4]: (~aElementOf0(W4,W1)|~sdtlpdtrp0(W0,W4)=W3))))))))&(![W2]: (W2=sdtlcdtrc0(W0,W1)|(~aSet0(W2)|((~aElementOf0(sK14_skl(W2,W1,W0),W2)|(![W4]: (~aElementOf0(W4,W1)|~sdtlpdtrp0(W0,W4)=sK14_skl(W2,W1,W0))))&(aElementOf0(sK14_skl(W2,W1,W0),W2)|(aElementOf0(sK15_skl(W2,W1,W0),W1)&sdtlpdtrp0(W0,sK15_skl(W2,W1,W0))=sK14_skl(W2,W1,W0)))))))))))),
% 6.26/6.49 inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl,sK14_skl,sK15_skl]),skolemize(W4,sK13_skl(W3,W2,W1,W0)),skolemize(W3,sK14_skl(W2,W1,W0)),skolemize(W4,sK15_skl(W2,W1,W0))],[f324])).
% 6.26/6.49 fof(f327,plain,(
% 6.26/6.49 ![X0,X1,X2,X3]: (~aFunction0(X0)|~aSubsetOf0(X1,szDzozmdt0(X0))|~X2=sdtlcdtrc0(X0,X1)|~aElementOf0(X3,X2)|aElementOf0(sK13_skl(X3,X2,X1,X0),X1))),
% 6.26/6.49 inference(cnf_transformation,[status(thm)],[f325])).
% 6.26/6.49 fof(f328,plain,(
% 6.26/6.49 ![X0,X1,X2,X3]: (~aFunction0(X0)|~aSubsetOf0(X1,szDzozmdt0(X0))|~X2=sdtlcdtrc0(X0,X1)|~aElementOf0(X3,X2)|sdtlpdtrp0(X0,sK13_skl(X3,X2,X1,X0))=X3)),
% 6.26/6.49 inference(cnf_transformation,[status(thm)],[f325])).
% 6.26/6.49 fof(f355,plain,(
% 6.26/6.49 aElementOf0(xK,szNzAzT0)),
% 6.26/6.49 inference(cnf_transformation,[status(thm)],[f74])).
% 6.26/6.49 fof(f356,plain,(
% 6.26/6.49 aSubsetOf0(xS,szNzAzT0)),
% 6.26/6.49 inference(cnf_transformation,[status(thm)],[f75])).
% 6.26/6.49 fof(f357,plain,(
% 6.26/6.49 isCountable0(xS)),
% 6.26/6.49 inference(cnf_transformation,[status(thm)],[f75])).
% 6.26/6.49 fof(f367,plain,(
% 6.26/6.49 ~xK=sz00),
% 6.26/6.49 inference(cnf_transformation,[status(thm)],[f78])).
% 6.26/6.49 fof(f369,plain,(
% 6.26/6.49 aElementOf0(xk,szNzAzT0)),
% 6.26/6.49 inference(cnf_transformation,[status(thm)],[f80])).
% 6.26/6.49 fof(f371,plain,(
% 6.26/6.49 ((aFunction0(xN)&szDzozmdt0(xN)=szNzAzT0)&sdtlpdtrp0(xN,sz00)=xS)&(![W0]: (~aElementOf0(W0,szNzAzT0)|((~aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0)|~isCountable0(sdtlpdtrp0(xN,W0)))|(aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))&isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))))))),
% 6.26/6.49 inference(pre_NNF_transformation,[status(thm)],[f81])).
% 6.26/6.49 fof(f372,plain,(
% 6.26/6.49 aFunction0(xN)),
% 6.26/6.49 inference(cnf_transformation,[status(thm)],[f371])).
% 6.26/6.49 fof(f386,plain,(
% 6.26/6.49 (aFunction0(xC)&szDzozmdt0(xC)=szNzAzT0)&(![W0]: (~aElementOf0(W0,szNzAzT0)|((aFunction0(sdtlpdtrp0(xC,W0))&szDzozmdt0(sdtlpdtrp0(xC,W0))=slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk))&(![W1]: ((~aSet0(W1)|~aElementOf0(W1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk)))|sdtlpdtrp0(sdtlpdtrp0(xC,W0),W1)=sdtlpdtrp0(xc,sdtpldt0(W1,szmzizndt0(sdtlpdtrp0(xN,W0)))))))))),
% 6.26/6.50 inference(pre_NNF_transformation,[status(thm)],[f86])).
% 6.26/6.50 fof(f387,plain,(
% 6.26/6.50 aFunction0(xC)),
% 6.26/6.50 inference(cnf_transformation,[status(thm)],[f386])).
% 6.26/6.50 fof(f406,plain,(
% 6.26/6.50 (aFunction0(xe)&szDzozmdt0(xe)=szNzAzT0)&(![W0]: (~aElementOf0(W0,szNzAzT0)|sdtlpdtrp0(xe,W0)=szmzizndt0(sdtlpdtrp0(xN,W0))))),
% 6.26/6.50 inference(pre_NNF_transformation,[status(thm)],[f91])).
% 6.26/6.50 fof(f407,plain,(
% 6.26/6.50 aFunction0(xe)),
% 6.26/6.50 inference(cnf_transformation,[status(thm)],[f406])).
% 6.26/6.50 fof(f410,plain,(
% 6.26/6.50 (aFunction0(xd)&szDzozmdt0(xd)=szNzAzT0)&(![W0]: (~aElementOf0(W0,szNzAzT0)|(![W1]: ((~aSet0(W1)|~aElementOf0(W1,slbdtsldtrb0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),xk)))|sdtlpdtrp0(xd,W0)=sdtlpdtrp0(sdtlpdtrp0(xC,W0),W1)))))),
% 6.26/6.50 inference(pre_NNF_transformation,[status(thm)],[f92])).
% 6.26/6.50 fof(f411,plain,(
% 6.26/6.50 aFunction0(xd)),
% 6.26/6.50 inference(cnf_transformation,[status(thm)],[f410])).
% 6.26/6.50 fof(f412,plain,(
% 6.26/6.50 szDzozmdt0(xd)=szNzAzT0),
% 6.26/6.50 inference(cnf_transformation,[status(thm)],[f410])).
% 6.26/6.50 fof(f415,plain,(
% 6.26/6.50 aElementOf0(xx,sdtlcdtrc0(xd,szDzozmdt0(xd)))),
% 6.26/6.50 inference(cnf_transformation,[status(thm)],[f94])).
% 6.26/6.50 fof(f416,plain,(
% 6.26/6.50 (![W0]: (~aElementOf0(W0,szNzAzT0)|~sdtlpdtrp0(xd,W0)=xx))),
% 6.26/6.50 inference(pre_NNF_transformation,[status(thm)],[f96])).
% 6.26/6.50 fof(f417,plain,(
% 6.26/6.50 ![X0]: (~aElementOf0(X0,szNzAzT0)|~sdtlpdtrp0(xd,X0)=xx)),
% 6.26/6.50 inference(cnf_transformation,[status(thm)],[f416])).
% 6.26/6.50 fof(f418,plain,(
% 6.26/6.50 ![W0,W1,W3]: ((~sP0_prd(W3,W1,W0)|((aElement0(W3)&aElementOf0(W3,W0))&~W3=W1))&(sP0_prd(W3,W1,W0)|((~aElement0(W3)|~aElementOf0(W3,W0))|W3=W1)))),
% 6.26/6.50 inference(NNF_transformation,[status(thm)],[f151])).
% 6.26/6.50 fof(f419,plain,(
% 6.26/6.50 (![W0,W1,W3]: (~sP0_prd(W3,W1,W0)|((aElement0(W3)&aElementOf0(W3,W0))&~W3=W1)))&(![W0,W1,W3]: (sP0_prd(W3,W1,W0)|((~aElement0(W3)|~aElementOf0(W3,W0))|W3=W1)))),
% 6.26/6.50 inference(miniscoping,[status(thm)],[f418])).
% 6.26/6.50 fof(f422,plain,(
% 6.26/6.50 ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|~X0=X1)),
% 6.26/6.50 inference(cnf_transformation,[status(thm)],[f419])).
% 6.26/6.50 fof(f424,plain,(
% 6.26/6.50 aSet0(slcrc0)),
% 6.26/6.50 inference(destructive_equality_resolution,[status(thm)],[f111])).
% 6.26/6.50 fof(f425,plain,(
% 6.26/6.50 ![X0]: (~aElementOf0(X0,slcrc0))),
% 6.26/6.50 inference(destructive_equality_resolution,[status(thm)],[f112])).
% 6.26/6.50 fof(f426,plain,(
% 6.26/6.50 ~aSet0(slcrc0)|~isCountable0(slcrc0)),
% 6.26/6.50 inference(destructive_equality_resolution,[status(thm)],[f120])).
% 6.26/6.50 fof(f436,plain,(
% 6.26/6.50 ~aSet0(slcrc0)|sbrdtbr0(slcrc0)=sz00),
% 6.26/6.50 inference(destructive_equality_resolution,[status(thm)],[f220])).
% 6.26/6.50 fof(f441,plain,(
% 6.26/6.50 ![X0]: (~aElementOf0(X0,szNzAzT0)|aSet0(slbdtrb0(X0)))),
% 6.26/6.50 inference(destructive_equality_resolution,[status(thm)],[f253])).
% 6.26/6.50 fof(f456,plain,(
% 6.26/6.50 ![X0,X1,X2]: (~aFunction0(X0)|~aSubsetOf0(X1,szDzozmdt0(X0))|~aElementOf0(X2,sdtlcdtrc0(X0,X1))|aElementOf0(sK13_skl(X2,sdtlcdtrc0(X0,X1),X1,X0),X1))),
% 6.26/6.50 inference(destructive_equality_resolution,[status(thm)],[f327])).
% 6.26/6.50 fof(f457,plain,(
% 6.26/6.50 ![X0,X1,X2]: (~aFunction0(X0)|~aSubsetOf0(X1,szDzozmdt0(X0))|~aElementOf0(X2,sdtlcdtrc0(X0,X1))|sdtlpdtrp0(X0,sK13_skl(X2,sdtlcdtrc0(X0,X1),X1,X0))=X2)),
% 6.26/6.50 inference(destructive_equality_resolution,[status(thm)],[f328])).
% 6.26/6.50 fof(f464,plain,(
% 6.26/6.50 ![X0,X1]: (~sP0_prd(X0,X0,X1))),
% 6.26/6.50 inference(destructive_equality_resolution,[status(thm)],[f422])).
% 6.26/6.50 fof(f466,plain,(
% 6.26/6.50 aElementOf0(xx,sdtlcdtrc0(xd,szNzAzT0))),
% 6.26/6.50 inference(forward_demodulation,[status(thm)],[f412,f415])).
% 6.26/6.50 fof(f490,definition,(
% 6.26/6.50 sQ5_spl <=> (aSet0(szNzAzT0))),
% 6.26/6.50 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 6.26/6.50 fof(f492,plain,(
% 6.26/6.50 ~aSet0(szNzAzT0)|sQ5_spl),
% 6.26/6.50 inference(component_clause,[status(thm)],[f490])).
% 6.26/6.50 fof(f511,plain,(
% 6.26/6.50 $false|sQ5_spl),
% 6.26/6.50 inference(forward_subsumption_resolution,[status(thm)],[f492,f173])).
% 6.26/6.50 fof(f512,plain,(
% 6.26/6.50 sQ5_spl),
% 6.26/6.50 inference(contradiction_clause,[status(thm)],[f511])).
% 6.26/6.50 fof(f547,plain,(
% 6.26/6.50 ~isCountable0(slcrc0)),
% 6.26/6.50 inference(forward_subsumption_resolution,[status(thm)],[f426,f424])).
% 6.26/6.50 fof(f824,definition,(
% 6.26/6.50 sQ46_spl <=> (aFunction0(xN))),
% 6.26/6.50 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 6.26/6.50 fof(f826,plain,(
% 6.26/6.50 ~aFunction0(xN)|sQ46_spl),
% 6.26/6.50 inference(component_clause,[status(thm)],[f824])).
% 6.26/6.50 fof(f828,definition,(
% 6.26/6.50 sQ47_spl <=> (aFunction0(xC))),
% 6.26/6.50 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 6.26/6.50 fof(f830,plain,(
% 6.26/6.50 ~aFunction0(xC)|sQ47_spl),
% 6.26/6.50 inference(component_clause,[status(thm)],[f828])).
% 6.26/6.50 fof(f832,definition,(
% 6.26/6.50 sQ48_spl <=> (aFunction0(xe))),
% 6.26/6.50 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 6.26/6.50 fof(f834,plain,(
% 6.26/6.50 ~aFunction0(xe)|sQ48_spl),
% 6.26/6.50 inference(component_clause,[status(thm)],[f832])).
% 6.26/6.50 fof(f836,definition,(
% 6.26/6.50 sQ49_spl <=> (aFunction0(xd))),
% 6.26/6.50 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 6.26/6.50 fof(f838,plain,(
% 6.26/6.50 ~aFunction0(xd)|sQ49_spl),
% 6.26/6.50 inference(component_clause,[status(thm)],[f836])).
% 6.26/6.50 fof(f840,plain,(
% 6.26/6.50 $false|sQ49_spl),
% 6.26/6.50 inference(forward_subsumption_resolution,[status(thm)],[f838,f411])).
% 6.26/6.50 fof(f841,plain,(
% 6.26/6.50 sQ49_spl),
% 6.26/6.50 inference(contradiction_clause,[status(thm)],[f840])).
% 6.26/6.50 fof(f842,plain,(
% 6.26/6.50 $false|sQ48_spl),
% 6.26/6.50 inference(forward_subsumption_resolution,[status(thm)],[f834,f407])).
% 6.26/6.50 fof(f843,plain,(
% 6.26/6.50 sQ48_spl),
% 6.26/6.50 inference(contradiction_clause,[status(thm)],[f842])).
% 6.26/6.50 fof(f844,plain,(
% 6.26/6.50 $false|sQ47_spl),
% 6.26/6.50 inference(forward_subsumption_resolution,[status(thm)],[f830,f387])).
% 6.26/6.50 fof(f845,plain,(
% 6.26/6.50 sQ47_spl),
% 6.26/6.50 inference(contradiction_clause,[status(thm)],[f844])).
% 6.26/6.50 fof(f846,plain,(
% 6.26/6.50 $false|sQ46_spl),
% 6.26/6.50 inference(forward_subsumption_resolution,[status(thm)],[f826,f372])).
% 6.26/6.50 fof(f847,plain,(
% 6.26/6.50 sQ46_spl),
% 6.26/6.50 inference(contradiction_clause,[status(thm)],[f846])).
% 6.26/6.50 fof(f883,definition,(
% 6.26/6.50 sQ55_spl <=> (aElementOf0(xk,szNzAzT0))),
% 6.26/6.50 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 6.26/6.50 fof(f885,plain,(
% 6.26/6.50 ~aElementOf0(xk,szNzAzT0)|sQ55_spl),
% 6.26/6.50 inference(component_clause,[status(thm)],[f883])).
% 6.26/6.50 fof(f893,plain,(
% 6.26/6.50 $false|sQ55_spl),
% 6.26/6.50 inference(forward_subsumption_resolution,[status(thm)],[f885,f369])).
% 6.26/6.50 fof(f894,plain,(
% 6.26/6.50 sQ55_spl),
% 6.26/6.50 inference(contradiction_clause,[status(thm)],[f893])).
% 6.26/6.50 fof(f924,plain,(
% 6.26/6.50 ~sz00=szszuzczcdt0(sz00)),
% 6.26/6.50 inference(resolution,[status(thm)],[f186,f175])).
% 6.26/6.50 fof(f970,plain,(
% 6.26/6.50 ~szszuzczcdt0(xK)=sz00),
% 6.26/6.50 inference(resolution,[status(thm)],[f178,f355])).
% 6.26/6.50 fof(f1055,definition,(
% 6.26/6.50 sQ83_spl <=> (aElementOf0(xx,slcrc0))),
% 6.26/6.50 introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 6.26/6.50 fof(f1056,plain,(
% 6.26/6.50 aElementOf0(xx,slcrc0)|~sQ83_spl),
% 6.26/6.50 inference(component_clause,[status(thm)],[f1055])).
% 6.26/6.50 fof(f1090,plain,(
% 6.26/6.50 $false|~sQ83_spl),
% 6.26/6.50 inference(forward_subsumption_resolution,[status(thm)],[f1056,f425])).
% 6.26/6.50 fof(f1091,plain,(
% 6.26/6.50 ~sQ83_spl),
% 6.26/6.50 inference(contradiction_clause,[status(thm)],[f1090])).
% 6.26/6.50 fof(f1154,plain,(
% 6.26/6.50 sbrdtbr0(slcrc0)=sz00),
% 6.26/6.50 inference(forward_subsumption_resolution,[status(thm)],[f436,f424])).
% 6.26/6.50 fof(f1159,plain,(
% 6.26/6.50 aSet0(slbdtrb0(xK))),
% 6.26/6.50 inference(resolution,[status(thm)],[f441,f355])).
% 6.26/6.50 fof(f1160,plain,(
% 6.26/6.50 aSet0(slbdtrb0(xk))),
% 6.26/6.50 inference(resolution,[status(thm)],[f441,f369])).
% 6.26/6.50 fof(f1187,definition,(
% 6.26/6.50 sQ107_spl <=> (aSet0(slbdtrb0(xK)))),
% 6.26/6.50 introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition])).
% 6.26/6.50 fof(f1189,plain,(
% 6.26/6.50 ~aSet0(slbdtrb0(xK))|sQ107_spl),
% 6.26/6.50 inference(component_clause,[status(thm)],[f1187])).
% 6.26/6.50 fof(f1194,plain,(
% 6.26/6.50 $false|sQ107_spl),
% 6.26/6.50 inference(forward_subsumption_resolution,[status(thm)],[f1189,f1159])).
% 6.26/6.50 fof(f1195,plain,(
% 6.26/6.50 sQ107_spl),
% 6.26/6.50 inference(contradiction_clause,[status(thm)],[f1194])).
% 6.26/6.50 fof(f1197,definition,(
% 6.26/6.50 sQ109_spl <=> (aSet0(slbdtrb0(xk)))),
% 6.26/6.50 introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition])).
% 6.26/6.50 fof(f1199,plain,(
% 6.26/6.50 ~aSet0(slbdtrb0(xk))|sQ109_spl),
% 6.26/6.50 inference(component_clause,[status(thm)],[f1197])).
% 6.26/6.50 fof(f1204,plain,(
% 6.26/6.50 $false|sQ109_spl),
% 6.26/6.50 inference(forward_subsumption_resolution,[status(thm)],[f1199,f1160])).
% 6.26/6.50 fof(f1205,plain,(
% 6.26/6.50 sQ109_spl),
% 6.26/6.50 inference(contradiction_clause,[status(thm)],[f1204])).
% 6.26/6.50 fof(f1208,plain,(
% 6.26/6.50 isFinite0(slbdtrb0(xK))),
% 6.26/6.50 inference(resolution,[status(thm)],[f261,f355])).
% 6.26/6.50 fof(f1209,plain,(
% 6.26/6.50 isFinite0(slbdtrb0(xk))),
% 6.26/6.50 inference(resolution,[status(thm)],[f261,f369])).
% 6.26/6.50 fof(f1234,definition,(
% 6.26/6.50 sQ116_spl <=> (isCountable0(xS))),
% 6.26/6.50 introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition])).
% 6.26/6.50 fof(f1236,plain,(
% 6.26/6.50 ~isCountable0(xS)|sQ116_spl),
% 6.26/6.50 inference(component_clause,[status(thm)],[f1234])).
% 6.26/6.50 fof(f1241,definition,(
% 6.26/6.50 sQ118_spl <=> (isCountable0(szNzAzT0))),
% 6.26/6.50 introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition])).
% 6.26/6.50 fof(f1243,plain,(
% 6.26/6.50 ~isCountable0(szNzAzT0)|sQ118_spl),
% 6.26/6.50 inference(component_clause,[status(thm)],[f1241])).
% 6.26/6.50 fof(f1257,plain,(
% 6.26/6.50 $false|sQ118_spl),
% 6.26/6.50 inference(forward_subsumption_resolution,[status(thm)],[f1243,f174])).
% 6.26/6.50 fof(f1258,plain,(
% 6.26/6.50 sQ118_spl),
% 6.26/6.50 inference(contradiction_clause,[status(thm)],[f1257])).
% 6.26/6.50 fof(f1261,plain,(
% 6.26/6.50 $false|sQ116_spl),
% 6.26/6.50 inference(forward_subsumption_resolution,[status(thm)],[f1236,f357])).
% 6.26/6.50 fof(f1262,plain,(
% 6.26/6.50 sQ116_spl),
% 6.26/6.50 inference(contradiction_clause,[status(thm)],[f1261])).
% 6.26/6.50 fof(f1339,plain,(
% 6.26/6.50 aElementOf0(szszuzczcdt0(sz00),szNzAzT0)),
% 6.26/6.50 inference(resolution,[status(thm)],[f177,f175])).
% 6.26/6.50 fof(f1340,plain,(
% 6.26/6.50 aElementOf0(szszuzczcdt0(xK),szNzAzT0)),
% 6.26/6.50 inference(resolution,[status(thm)],[f177,f355])).
% 6.26/6.50 fof(f1373,definition,(
% 6.26/6.50 sQ139_spl <=> (isCountable0(slcrc0))),
% 6.26/6.50 introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition])).
% 6.26/6.50 fof(f1374,plain,(
% 6.26/6.50 isCountable0(slcrc0)|~sQ139_spl),
% 6.26/6.50 inference(component_clause,[status(thm)],[f1373])).
% 6.26/6.50 fof(f1387,plain,(
% 6.26/6.50 $false|~sQ139_spl),
% 6.26/6.50 inference(forward_subsumption_resolution,[status(thm)],[f1374,f547])).
% 6.26/6.50 fof(f1388,plain,(
% 6.26/6.50 ~sQ139_spl),
% 6.26/6.50 inference(contradiction_clause,[status(thm)],[f1387])).
% 6.26/6.50 fof(f1497,plain,(
% 6.26/6.50 isFinite0(slbdtrb0(szszuzczcdt0(sz00)))),
% 6.26/6.50 inference(resolution,[status(thm)],[f1339,f261])).
% 6.26/6.50 fof(f1498,plain,(
% 6.26/6.50 aSet0(slbdtrb0(szszuzczcdt0(sz00)))),
% 6.26/6.50 inference(resolution,[status(thm)],[f1339,f441])).
% 6.26/6.50 fof(f1511,plain,(
% 6.26/6.50 isFinite0(slbdtrb0(szszuzczcdt0(xK)))),
% 6.26/6.50 inference(resolution,[status(thm)],[f1340,f261])).
% 6.26/6.50 fof(f1512,plain,(
% 6.26/6.50 aSet0(slbdtrb0(szszuzczcdt0(xK)))),
% 6.26/6.50 inference(resolution,[status(thm)],[f1340,f441])).
% 6.26/6.50 fof(f1528,definition,(
% 6.26/6.50 sQ163_spl <=> (szszuzczcdt0(xK)=sz00)),
% 6.26/6.50 introduced(definition,[new_symbols(definition,[sQ163_spl])],[split_symbol_definition])).
% 6.26/6.50 fof(f1529,plain,(
% 6.26/6.50 szszuzczcdt0(xK)=sz00|~sQ163_spl),
% 6.26/6.50 inference(component_clause,[status(thm)],[f1528])).
% 6.26/6.50 fof(f1535,definition,(
% 6.26/6.50 sQ165_spl <=> (szszuzczcdt0(sz00)=sz00)),
% 6.26/6.50 introduced(definition,[new_symbols(definition,[sQ165_spl])],[split_symbol_definition])).
% 6.26/6.50 fof(f1536,plain,(
% 6.26/6.50 szszuzczcdt0(sz00)=sz00|~sQ165_spl),
% 6.26/6.50 inference(component_clause,[status(thm)],[f1535])).
% 6.26/6.50 fof(f1553,definition,(
% 6.26/6.50 sQ170_spl <=> (xK=sz00)),
% 6.26/6.50 introduced(definition,[new_symbols(definition,[sQ170_spl])],[split_symbol_definition])).
% 6.26/6.50 fof(f1554,plain,(
% 6.26/6.50 xK=sz00|~sQ170_spl),
% 6.26/6.50 inference(component_clause,[status(thm)],[f1553])).
% 6.26/6.50 fof(f1567,plain,(
% 6.26/6.50 $false|~sQ170_spl),
% 6.26/6.50 inference(forward_subsumption_resolution,[status(thm)],[f1554,f367])).
% 6.26/6.50 fof(f1568,plain,(
% 6.26/6.50 ~sQ170_spl),
% 6.26/6.50 inference(contradiction_clause,[status(thm)],[f1567])).
% 6.26/6.50 fof(f1569,plain,(
% 6.26/6.50 $false|~sQ165_spl),
% 6.26/6.50 inference(forward_subsumption_resolution,[status(thm)],[f1536,f924])).
% 6.26/6.50 fof(f1570,plain,(
% 6.26/6.50 ~sQ165_spl),
% 6.26/6.50 inference(contradiction_clause,[status(thm)],[f1569])).
% 6.26/6.50 fof(f1571,plain,(
% 6.26/6.50 $false|~sQ163_spl),
% 6.26/6.50 inference(forward_subsumption_resolution,[status(thm)],[f1529,f970])).
% 6.26/6.50 fof(f1572,plain,(
% 6.26/6.50 ~sQ163_spl),
% 6.26/6.50 inference(contradiction_clause,[status(thm)],[f1571])).
% 6.26/6.50 fof(f1652,definition,(
% 6.26/6.50 sQ187_spl <=> (sP0_prd(xx,xx,xS))),
% 6.26/6.50 introduced(definition,[new_symbols(definition,[sQ187_spl])],[split_symbol_definition])).
% 6.26/6.50 fof(f1653,plain,(
% 6.26/6.50 sP0_prd(xx,xx,xS)|~sQ187_spl),
% 6.26/6.50 inference(component_clause,[status(thm)],[f1652])).
% 6.26/6.50 fof(f1660,plain,(
% 6.26/6.50 $false|~sQ187_spl),
% 6.26/6.50 inference(forward_subsumption_resolution,[status(thm)],[f1653,f464])).
% 6.26/6.50 fof(f1661,plain,(
% 6.26/6.50 ~sQ187_spl),
% 6.26/6.50 inference(contradiction_clause,[status(thm)],[f1660])).
% 6.26/6.50 fof(f1827,definition,(
% 6.26/6.50 sQ205_spl <=> (sP0_prd(xx,xx,xT))),
% 6.26/6.50 introduced(definition,[new_symbols(definition,[sQ205_spl])],[split_symbol_definition])).
% 6.26/6.50 fof(f1828,plain,(
% 6.26/6.50 sP0_prd(xx,xx,xT)|~sQ205_spl),
% 6.26/6.50 inference(component_clause,[status(thm)],[f1827])).
% 6.26/6.50 fof(f1835,plain,(
% 6.26/6.50 $false|~sQ205_spl),
% 6.26/6.50 inference(forward_subsumption_resolution,[status(thm)],[f1828,f464])).
% 6.26/6.50 fof(f1836,plain,(
% 6.26/6.50 ~sQ205_spl),
% 6.26/6.50 inference(contradiction_clause,[status(thm)],[f1835])).
% 6.26/6.50 fof(f1889,definition,(
% 6.26/6.50 sQ214_spl <=> (aElementOf0(xK,szNzAzT0))),
% 6.26/6.50 introduced(definition,[new_symbols(definition,[sQ214_spl])],[split_symbol_definition])).
% 6.26/6.50 fof(f1891,plain,(
% 6.26/6.50 ~aElementOf0(xK,szNzAzT0)|sQ214_spl),
% 6.26/6.50 inference(component_clause,[status(thm)],[f1889])).
% 6.26/6.50 fof(f1896,plain,(
% 6.26/6.50 $false|sQ214_spl),
% 6.26/6.50 inference(forward_subsumption_resolution,[status(thm)],[f1891,f355])).
% 6.26/6.50 fof(f1897,plain,(
% 6.26/6.50 sQ214_spl),
% 6.26/6.50 inference(contradiction_clause,[status(thm)],[f1896])).
% 6.26/6.50 fof(f1906,definition,(
% 6.26/6.50 sQ217_spl <=> (aSet0(slbdtrb0(szszuzczcdt0(xK))))),
% 6.26/6.50 introduced(definition,[new_symbols(definition,[sQ217_spl])],[split_symbol_definition])).
% 6.26/6.50 fof(f1908,plain,(
% 6.26/6.50 ~aSet0(slbdtrb0(szszuzczcdt0(xK)))|sQ217_spl),
% 6.26/6.50 inference(component_clause,[status(thm)],[f1906])).
% 6.26/6.50 fof(f1913,plain,(
% 6.26/6.50 $false|sQ217_spl),
% 6.26/6.50 inference(forward_subsumption_resolution,[status(thm)],[f1908,f1512])).
% 6.26/6.50 fof(f1914,plain,(
% 6.26/6.50 sQ217_spl),
% 6.26/6.50 inference(contradiction_clause,[status(thm)],[f1913])).
% 6.26/6.50 fof(f1994,definition,(
% 6.26/6.50 sQ228_spl <=> (sP0_prd(xx,xx,szNzAzT0))),
% 6.26/6.50 introduced(definition,[new_symbols(definition,[sQ228_spl])],[split_symbol_definition])).
% 6.26/6.50 fof(f1995,plain,(
% 6.26/6.50 sP0_prd(xx,xx,szNzAzT0)|~sQ228_spl),
% 6.26/6.50 inference(component_clause,[status(thm)],[f1994])).
% 6.26/6.50 fof(f2002,plain,(
% 6.26/6.50 $false|~sQ228_spl),
% 6.26/6.50 inference(forward_subsumption_resolution,[status(thm)],[f1995,f464])).
% 6.26/6.50 fof(f2003,plain,(
% 6.26/6.50 ~sQ228_spl),
% 6.26/6.50 inference(contradiction_clause,[status(thm)],[f2002])).
% 6.26/6.50 fof(f2091,plain,(
% 6.26/6.50 isFinite0(slbdtrb0(sz00))),
% 6.26/6.50 inference(resolution,[status(thm)],[f175,f261])).
% 6.26/6.50 fof(f2092,plain,(
% 6.26/6.50 aSet0(slbdtrb0(sz00))),
% 6.26/6.50 inference(resolution,[status(thm)],[f175,f441])).
% 6.26/6.50 fof(f2170,definition,(
% 6.26/6.50 sQ258_spl <=> (sbrdtbr0(slcrc0)=sz00)),
% 6.26/6.50 introduced(definition,[new_symbols(definition,[sQ258_spl])],[split_symbol_definition])).
% 6.26/6.50 fof(f2172,plain,(
% 6.26/6.50 ~sbrdtbr0(slcrc0)=sz00|sQ258_spl),
% 6.26/6.50 inference(component_clause,[status(thm)],[f2170])).
% 6.26/6.50 fof(f2199,plain,(
% 6.26/6.50 ~sz00=sz00|sQ258_spl),
% 6.26/6.50 inference(forward_demodulation,[status(thm)],[f1154,f2172])).
% 6.26/6.50 fof(f2200,plain,(
% 6.26/6.50 $false|sQ258_spl),
% 6.26/6.50 inference(trivial_equality_resolution,[status(thm)],[f2199])).
% 6.26/6.50 fof(f2201,plain,(
% 6.26/6.50 sQ258_spl),
% 6.26/6.50 inference(contradiction_clause,[status(thm)],[f2200])).
% 6.26/6.50 fof(f2583,definition,(
% 6.26/6.50 sQ309_spl <=> (aSet0(slbdtrb0(sz00)))),
% 6.26/6.50 introduced(definition,[new_symbols(definition,[sQ309_spl])],[split_symbol_definition])).
% 6.26/6.50 fof(f2585,plain,(
% 6.26/6.50 ~aSet0(slbdtrb0(sz00))|sQ309_spl),
% 6.26/6.50 inference(component_clause,[status(thm)],[f2583])).
% 6.26/6.50 fof(f2586,definition,(
% 6.26/6.50 sQ310_spl <=> (isFinite0(slbdtrb0(sz00)))),
% 6.26/6.50 introduced(definition,[new_symbols(definition,[sQ310_spl])],[split_symbol_definition])).
% 6.26/6.50 fof(f2588,plain,(
% 6.26/6.50 ~isFinite0(slbdtrb0(sz00))|sQ310_spl),
% 6.26/6.50 inference(component_clause,[status(thm)],[f2586])).
% 6.26/6.50 fof(f2597,plain,(
% 6.26/6.50 $false|sQ309_spl),
% 6.26/6.50 inference(forward_subsumption_resolution,[status(thm)],[f2585,f2092])).
% 6.26/6.50 fof(f2598,plain,(
% 6.26/6.50 sQ309_spl),
% 6.26/6.50 inference(contradiction_clause,[status(thm)],[f2597])).
% 6.26/6.50 fof(f2599,plain,(
% 6.26/6.50 $false|sQ310_spl),
% 6.26/6.50 inference(forward_subsumption_resolution,[status(thm)],[f2588,f2091])).
% 6.26/6.50 fof(f2600,plain,(
% 6.26/6.50 sQ310_spl),
% 6.26/6.50 inference(contradiction_clause,[status(thm)],[f2599])).
% 6.26/6.50 fof(f2912,definition,(
% 6.26/6.50 sQ339_spl <=> (sP0_prd(xx,xx,sdtlcdtrc0(xd,szNzAzT0)))),
% 6.26/6.50 introduced(definition,[new_symbols(definition,[sQ339_spl])],[split_symbol_definition])).
% 6.26/6.50 fof(f2913,plain,(
% 6.26/6.50 sP0_prd(xx,xx,sdtlcdtrc0(xd,szNzAzT0))|~sQ339_spl),
% 6.26/6.50 inference(component_clause,[status(thm)],[f2912])).
% 6.26/6.50 fof(f2924,plain,(
% 6.26/6.50 $false|~sQ339_spl),
% 6.26/6.50 inference(forward_subsumption_resolution,[status(thm)],[f2913,f464])).
% 6.26/6.50 fof(f2925,plain,(
% 6.26/6.50 ~sQ339_spl),
% 6.26/6.50 inference(contradiction_clause,[status(thm)],[f2924])).
% 6.26/6.50 fof(f3086,definition,(
% 6.26/6.50 sQ366_spl <=> (isFinite0(slbdtrb0(xK)))),
% 6.26/6.50 introduced(definition,[new_symbols(definition,[sQ366_spl])],[split_symbol_definition])).
% 6.26/6.50 fof(f3088,plain,(
% 6.26/6.50 ~isFinite0(slbdtrb0(xK))|sQ366_spl),
% 6.26/6.50 inference(component_clause,[status(thm)],[f3086])).
% 6.26/6.50 fof(f3110,plain,(
% 6.26/6.50 $false|sQ366_spl),
% 6.26/6.50 inference(forward_subsumption_resolution,[status(thm)],[f3088,f1208])).
% 6.26/6.50 fof(f3111,plain,(
% 6.26/6.50 sQ366_spl),
% 6.26/6.50 inference(contradiction_clause,[status(thm)],[f3110])).
% 6.26/6.50 fof(f3508,definition,(
% 6.26/6.50 sQ450_spl <=> (isFinite0(slbdtrb0(xk)))),
% 6.26/6.50 introduced(definition,[new_symbols(definition,[sQ450_spl])],[split_symbol_definition])).
% 6.26/6.50 fof(f3510,plain,(
% 6.26/6.50 ~isFinite0(slbdtrb0(xk))|sQ450_spl),
% 6.26/6.50 inference(component_clause,[status(thm)],[f3508])).
% 6.26/6.50 fof(f3517,plain,(
% 6.26/6.50 $false|sQ450_spl),
% 6.26/6.50 inference(forward_subsumption_resolution,[status(thm)],[f3510,f1209])).
% 6.26/6.50 fof(f3518,plain,(
% 6.26/6.50 sQ450_spl),
% 6.26/6.50 inference(contradiction_clause,[status(thm)],[f3517])).
% 6.26/6.50 fof(f3664,definition,(
% 6.26/6.50 sQ469_spl <=> (aSet0(slbdtrb0(szszuzczcdt0(sz00))))),
% 6.26/6.50 introduced(definition,[new_symbols(definition,[sQ469_spl])],[split_symbol_definition])).
% 6.26/6.50 fof(f3666,plain,(
% 6.26/6.50 ~aSet0(slbdtrb0(szszuzczcdt0(sz00)))|sQ469_spl),
% 6.26/6.50 inference(component_clause,[status(thm)],[f3664])).
% 6.26/6.50 fof(f3671,plain,(
% 6.26/6.50 $false|sQ469_spl),
% 6.26/6.50 inference(forward_subsumption_resolution,[status(thm)],[f3666,f1498])).
% 6.26/6.50 fof(f3672,plain,(
% 6.26/6.50 sQ469_spl),
% 6.26/6.50 inference(contradiction_clause,[status(thm)],[f3671])).
% 6.26/6.50 fof(f3860,definition,(
% 6.26/6.50 sQ493_spl <=> (aElementOf0(szszuzczcdt0(xK),szNzAzT0))),
% 6.26/6.50 introduced(definition,[new_symbols(definition,[sQ493_spl])],[split_symbol_definition])).
% 6.26/6.50 fof(f3862,plain,(
% 6.26/6.50 ~aElementOf0(szszuzczcdt0(xK),szNzAzT0)|sQ493_spl),
% 6.26/6.50 inference(component_clause,[status(thm)],[f3860])).
% 6.26/6.50 fof(f3885,plain,(
% 6.26/6.50 $false|sQ493_spl),
% 6.26/6.50 inference(forward_subsumption_resolution,[status(thm)],[f3862,f1340])).
% 6.26/6.50 fof(f3886,plain,(
% 6.26/6.50 sQ493_spl),
% 6.26/6.50 inference(contradiction_clause,[status(thm)],[f3885])).
% 6.26/6.50 fof(f3912,definition,(
% 6.26/6.50 sQ502_spl <=> (aElementOf0(szmzazxdt0(slcrc0),slcrc0))),
% 6.26/6.50 introduced(definition,[new_symbols(definition,[sQ502_spl])],[split_symbol_definition])).
% 6.26/6.50 fof(f3913,plain,(
% 6.26/6.50 aElementOf0(szmzazxdt0(slcrc0),slcrc0)|~sQ502_spl),
% 6.26/6.50 inference(component_clause,[status(thm)],[f3912])).
% 6.26/6.50 fof(f3924,definition,(
% 6.26/6.50 sQ505_spl <=> (aElementOf0(szmzizndt0(slcrc0),slcrc0))),
% 6.26/6.50 introduced(definition,[new_symbols(definition,[sQ505_spl])],[split_symbol_definition])).
% 6.26/6.50 fof(f3925,plain,(
% 6.26/6.50 aElementOf0(szmzizndt0(slcrc0),slcrc0)|~sQ505_spl),
% 6.26/6.50 inference(component_clause,[status(thm)],[f3924])).
% 6.26/6.50 fof(f3929,plain,(
% 6.26/6.50 $false|~sQ505_spl),
% 6.26/6.50 inference(forward_subsumption_resolution,[status(thm)],[f3925,f425])).
% 6.26/6.50 fof(f3930,plain,(
% 6.26/6.50 ~sQ505_spl),
% 6.26/6.50 inference(contradiction_clause,[status(thm)],[f3929])).
% 6.26/6.50 fof(f3931,plain,(
% 6.26/6.50 $false|~sQ502_spl),
% 6.26/6.50 inference(forward_subsumption_resolution,[status(thm)],[f3913,f425])).
% 6.26/6.50 fof(f3932,plain,(
% 6.26/6.50 ~sQ502_spl),
% 6.26/6.50 inference(contradiction_clause,[status(thm)],[f3931])).
% 6.26/6.50 fof(f3936,definition,(
% 6.26/6.50 sQ506_spl <=> (aSubsetOf0(xS,szNzAzT0))),
% 6.26/6.50 introduced(definition,[new_symbols(definition,[sQ506_spl])],[split_symbol_definition])).
% 6.26/6.50 fof(f3938,plain,(
% 6.26/6.50 ~aSubsetOf0(xS,szNzAzT0)|sQ506_spl),
% 6.26/6.50 inference(component_clause,[status(thm)],[f3936])).
% 6.26/6.50 fof(f3951,plain,(
% 6.26/6.50 $false|sQ506_spl),
% 6.26/6.50 inference(forward_subsumption_resolution,[status(thm)],[f3938,f356])).
% 6.26/6.50 fof(f3952,plain,(
% 6.26/6.50 sQ506_spl),
% 6.26/6.50 inference(contradiction_clause,[status(thm)],[f3951])).
% 6.26/6.50 fof(f3968,definition,(
% 6.26/6.50 sQ510_spl <=> (aSubsetOf0(szNzAzT0,szNzAzT0))),
% 6.26/6.50 introduced(definition,[new_symbols(definition,[sQ510_spl])],[split_symbol_definition])).
% 6.26/6.50 fof(f3969,plain,(
% 6.26/6.50 aSubsetOf0(szNzAzT0,szNzAzT0)|~sQ510_spl),
% 6.26/6.50 inference(component_clause,[status(thm)],[f3968])).
% 6.26/6.50 fof(f3970,plain,(
% 6.26/6.50 ~aSubsetOf0(szNzAzT0,szNzAzT0)|sQ510_spl),
% 6.26/6.50 inference(component_clause,[status(thm)],[f3968])).
% 6.26/6.50 fof(f3983,plain,(
% 6.26/6.50 ~aSet0(szNzAzT0)|sQ510_spl),
% 6.26/6.50 inference(resolution,[status(thm)],[f3970,f132])).
% 6.26/6.50 fof(f3984,plain,(
% 6.26/6.50 ~sQ5_spl|sQ510_spl),
% 6.26/6.50 inference(split_clause,[status(thm)],[f3983,f490,f3968])).
% 6.26/6.50 fof(f4428,definition,(
% 6.26/6.50 sQ576_spl <=> (isFinite0(slbdtrb0(szszuzczcdt0(xK))))),
% 6.26/6.50 introduced(definition,[new_symbols(definition,[sQ576_spl])],[split_symbol_definition])).
% 6.26/6.50 fof(f4430,plain,(
% 6.26/6.50 ~isFinite0(slbdtrb0(szszuzczcdt0(xK)))|sQ576_spl),
% 6.26/6.50 inference(component_clause,[status(thm)],[f4428])).
% 6.26/6.50 fof(f4626,definition,(
% 6.26/6.50 sQ588_spl <=> (aElementOf0(szszuzczcdt0(sz00),szNzAzT0))),
% 6.26/6.50 introduced(definition,[new_symbols(definition,[sQ588_spl])],[split_symbol_definition])).
% 6.26/6.50 fof(f4628,plain,(
% 6.26/6.50 ~aElementOf0(szszuzczcdt0(sz00),szNzAzT0)|sQ588_spl),
% 6.26/6.50 inference(component_clause,[status(thm)],[f4626])).
% 6.26/6.50 fof(f4638,definition,(
% 6.26/6.50 sQ591_spl <=> (isFinite0(slbdtrb0(szszuzczcdt0(sz00))))),
% 6.26/6.50 introduced(definition,[new_symbols(definition,[sQ591_spl])],[split_symbol_definition])).
% 6.26/6.50 fof(f4640,plain,(
% 6.26/6.50 ~isFinite0(slbdtrb0(szszuzczcdt0(sz00)))|sQ591_spl),
% 6.26/6.50 inference(component_clause,[status(thm)],[f4638])).
% 6.26/6.50 fof(f4649,plain,(
% 6.26/6.50 $false|sQ588_spl),
% 6.26/6.50 inference(forward_subsumption_resolution,[status(thm)],[f4628,f1339])).
% 6.26/6.50 fof(f4650,plain,(
% 6.26/6.50 sQ588_spl),
% 6.26/6.50 inference(contradiction_clause,[status(thm)],[f4649])).
% 6.26/6.50 fof(f4651,plain,(
% 6.26/6.50 $false|sQ591_spl),
% 6.26/6.50 inference(forward_subsumption_resolution,[status(thm)],[f4640,f1497])).
% 6.26/6.50 fof(f4652,plain,(
% 6.26/6.50 sQ591_spl),
% 6.26/6.50 inference(contradiction_clause,[status(thm)],[f4651])).
% 6.26/6.50 fof(f5128,plain,(
% 6.26/6.50 $false|sQ576_spl),
% 6.26/6.50 inference(forward_subsumption_resolution,[status(thm)],[f1511,f4430])).
% 6.26/6.50 fof(f5129,plain,(
% 6.26/6.50 sQ576_spl),
% 6.26/6.50 inference(contradiction_clause,[status(thm)],[f5128])).
% 6.26/6.50 fof(f5394,plain,(
% 6.26/6.50 ~aFunction0(xd)|~aSubsetOf0(szNzAzT0,szDzozmdt0(xd))|aElementOf0(sK13_skl(xx,sdtlcdtrc0(xd,szNzAzT0),szNzAzT0,xd),szNzAzT0)),
% 6.26/6.50 inference(resolution,[status(thm)],[f456,f466])).
% 6.26/6.50 fof(f5396,definition,(
% 6.26/6.50 sQ661_spl <=> (aSubsetOf0(szNzAzT0,szDzozmdt0(xd)))),
% 6.26/6.50 introduced(definition,[new_symbols(definition,[sQ661_spl])],[split_symbol_definition])).
% 6.26/6.50 fof(f5398,plain,(
% 6.26/6.50 ~aSubsetOf0(szNzAzT0,szDzozmdt0(xd))|sQ661_spl),
% 6.26/6.50 inference(component_clause,[status(thm)],[f5396])).
% 6.26/6.50 fof(f5403,definition,(
% 6.26/6.50 sQ663_spl <=> (aElementOf0(sK13_skl(xx,sdtlcdtrc0(xd,szNzAzT0),szNzAzT0,xd),szNzAzT0))),
% 6.26/6.50 introduced(definition,[new_symbols(definition,[sQ663_spl])],[split_symbol_definition])).
% 6.26/6.50 fof(f5404,plain,(
% 6.26/6.51 aElementOf0(sK13_skl(xx,sdtlcdtrc0(xd,szNzAzT0),szNzAzT0,xd),szNzAzT0)|~sQ663_spl),
% 6.26/6.51 inference(component_clause,[status(thm)],[f5403])).
% 6.26/6.51 fof(f5406,plain,(
% 6.26/6.51 ~sQ49_spl|~sQ661_spl|sQ663_spl),
% 6.26/6.51 inference(split_clause,[status(thm)],[f5394,f836,f5396,f5403])).
% 6.26/6.51 fof(f5408,plain,(
% 6.26/6.51 ~aSubsetOf0(szNzAzT0,szNzAzT0)|sQ661_spl),
% 6.26/6.51 inference(forward_demodulation,[status(thm)],[f412,f5398])).
% 6.26/6.51 fof(f5409,plain,(
% 6.26/6.51 $false|~sQ510_spl|sQ661_spl),
% 6.26/6.51 inference(forward_subsumption_resolution,[status(thm)],[f5408,f3969])).
% 6.26/6.51 fof(f5410,plain,(
% 6.26/6.51 ~sQ510_spl|sQ661_spl),
% 6.26/6.51 inference(contradiction_clause,[status(thm)],[f5409])).
% 6.26/6.51 fof(f5539,plain,(
% 6.26/6.51 ~aFunction0(xd)|~aSubsetOf0(szNzAzT0,szDzozmdt0(xd))|sdtlpdtrp0(xd,sK13_skl(xx,sdtlcdtrc0(xd,szNzAzT0),szNzAzT0,xd))=xx),
% 6.26/6.51 inference(resolution,[status(thm)],[f457,f466])).
% 6.26/6.51 fof(f5545,definition,(
% 6.26/6.51 sQ681_spl <=> (sdtlpdtrp0(xd,sK13_skl(xx,sdtlcdtrc0(xd,szNzAzT0),szNzAzT0,xd))=xx)),
% 6.26/6.51 introduced(definition,[new_symbols(definition,[sQ681_spl])],[split_symbol_definition])).
% 6.26/6.51 fof(f5546,plain,(
% 6.26/6.51 sdtlpdtrp0(xd,sK13_skl(xx,sdtlcdtrc0(xd,szNzAzT0),szNzAzT0,xd))=xx|~sQ681_spl),
% 6.26/6.51 inference(component_clause,[status(thm)],[f5545])).
% 6.26/6.51 fof(f5548,plain,(
% 6.26/6.51 ~sQ49_spl|~sQ661_spl|sQ681_spl),
% 6.26/6.51 inference(split_clause,[status(thm)],[f5539,f836,f5396,f5545])).
% 6.26/6.51 fof(f5559,plain,(
% 6.26/6.51 ~aElementOf0(sK13_skl(xx,sdtlcdtrc0(xd,szNzAzT0),szNzAzT0,xd),szNzAzT0)|~sQ681_spl),
% 6.26/6.51 inference(resolution,[status(thm)],[f5546,f417])).
% 6.26/6.51 fof(f5563,plain,(
% 6.26/6.51 $false|~sQ663_spl|~sQ681_spl),
% 6.26/6.51 inference(forward_subsumption_resolution,[status(thm)],[f5559,f5404])).
% 6.26/6.51 fof(f5564,plain,(
% 6.26/6.51 ~sQ663_spl|~sQ681_spl),
% 6.26/6.51 inference(contradiction_clause,[status(thm)],[f5563])).
% 6.26/6.51 fof(f5565,plain,(
% 6.26/6.51 $false),
% 6.26/6.51 inference(sat_refutation,[status(thm)],[f512,f841,f843,f845,f847,f894,f1091,f1195,f1205,f1258,f1262,f1388,f1568,f1570,f1572,f1661,f1836,f1897,f1914,f2003,f2201,f2598,f2600,f2925,f3111,f3518,f3672,f3886,f3930,f3932,f3952,f3984,f4650,f4652,f5129,f5406,f5410,f5548,f5564])).
% 6.26/6.51 % SZS output end CNFRefutation for theBenchmark.p
% 1.54/6.53 % Elapsed time: 0.898244 seconds
% 1.54/6.53 % CPU time: 6.757212 seconds
% 1.54/6.53 % Total memory used: 183.184 MB
% 1.54/6.53 % Net memory used: 178.590 MB
%------------------------------------------------------------------------------