%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM627+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n017.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:23 PM UTC 2026
% Result : Theorem 8.71s 1.64s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM627+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n017.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 02:40:56 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.40 % Drodi V4.1.1
% 8.71/1.64 % Refutation found
% 8.71/1.64 % SZS status Theorem for theBenchmark: Theorem is valid
% 8.71/1.64 % SZS output start CNFRefutation for theBenchmark
% 8.71/1.64 fof(f3,axiom,(
% 8.71/1.64 (! [W0] :( aSet0(W0)=> (! [W1] :( aElementOf0(W1,W0)=> aElement0(W1) ) )) )),
% 8.71/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.71/1.64 fof(f5,definition,(
% 8.71/1.64 (! [W0] :( W0 = slcrc0<=> ( aSet0(W0)& ~ (? [W1] : aElementOf0(W1,W0) )) ) )),
% 8.71/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.71/1.64 fof(f23,axiom,(
% 8.71/1.64 ( aSet0(szNzAzT0)& isCountable0(szNzAzT0) ) ),
% 8.71/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.71/1.64 fof(f24,axiom,(
% 8.71/1.64 aElementOf0(sz00,szNzAzT0) ),
% 8.71/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.71/1.64 fof(f25,axiom,(
% 8.71/1.64 (! [W0] :( aElementOf0(W0,szNzAzT0)=> ( aElementOf0(szszuzczcdt0(W0),szNzAzT0)& szszuzczcdt0(W0) != sz00 ) ) )),
% 8.71/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.71/1.64 fof(f28,axiom,(
% 8.71/1.64 (! [W0] :( aElementOf0(W0,szNzAzT0)=> W0 != szszuzczcdt0(W0) ) )),
% 8.71/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.71/1.64 fof(f30,axiom,(
% 8.71/1.64 (! [W0] :( aElementOf0(W0,szNzAzT0)=> sdtlseqdt0(sz00,W0) ) )),
% 8.71/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.71/1.64 fof(f33,axiom,(
% 8.71/1.64 (! [W0] :( aElementOf0(W0,szNzAzT0)=> sdtlseqdt0(W0,szszuzczcdt0(W0)) ) )),
% 8.71/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.71/1.64 fof(f34,axiom,(
% 8.71/1.64 (! [W0] :( aElementOf0(W0,szNzAzT0)=> sdtlseqdt0(W0,W0) ) )),
% 8.71/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.71/1.64 fof(f37,axiom,(
% 8.71/1.64 (! [W0,W1] :( ( aElementOf0(W0,szNzAzT0)& aElementOf0(W1,szNzAzT0) )=> ( sdtlseqdt0(W0,W1)| sdtlseqdt0(szszuzczcdt0(W1),W0) ) ) )),
% 8.71/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.71/1.64 fof(f42,axiom,(
% 8.71/1.64 (! [W0] :( aSet0(W0)=> ( sbrdtbr0(W0) = sz00<=> W0 = slcrc0 ) ) )),
% 8.71/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.71/1.64 fof(f50,definition,(
% 8.71/1.64 (! [W0] :( aElementOf0(W0,szNzAzT0)=> (! [W1] :( W1 = slbdtrb0(W0)<=> ( aSet0(W1)& (! [W2] :( aElementOf0(W2,W1)<=> ( aElementOf0(W2,szNzAzT0)& sdtlseqdt0(szszuzczcdt0(W2),W0) ) ) )) ) )) )),
% 8.71/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.71/1.64 fof(f51,axiom,(
% 8.71/1.64 (! [W0] :( aElementOf0(W0,szNzAzT0)=> isFinite0(slbdtrb0(W0)) ) )),
% 8.71/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.71/1.64 fof(f64,axiom,(
% 8.71/1.64 (! [W0] :( aFunction0(W0)=> aSet0(szDzozmdt0(W0)) ) )),
% 8.71/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.71/1.64 fof(f73,hypothesis,(
% 8.71/1.64 ( aSet0(xT)& isFinite0(xT) ) ),
% 8.71/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.71/1.64 fof(f74,hypothesis,(
% 8.71/1.64 aElementOf0(xK,szNzAzT0) ),
% 8.71/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.71/1.64 fof(f75,hypothesis,(
% 8.71/1.64 ( aSubsetOf0(xS,szNzAzT0)& isCountable0(xS) ) ),
% 8.71/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.71/1.64 fof(f76,hypothesis,(
% 8.71/1.64 ( aFunction0(xc)& szDzozmdt0(xc) = slbdtsldtrb0(xS,xK)& aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT) ) ),
% 8.71/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.71/1.64 fof(f80,hypothesis,(
% 8.71/1.64 ( aElementOf0(xk,szNzAzT0)& szszuzczcdt0(xk) = xK ) ),
% 8.71/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.71/1.64 fof(f81,hypothesis,(
% 8.71/1.64 ( 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))) ) ) ) )) ),
% 8.71/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.71/1.64 fof(f83,hypothesis,(
% 8.71/1.64 (! [W0,W1] :( ( aElementOf0(W0,szNzAzT0)& aElementOf0(W1,szNzAzT0) )=> ( sdtlseqdt0(W1,W0)=> aSubsetOf0(sdtlpdtrp0(xN,W0),sdtlpdtrp0(xN,W1)) ) ) )),
% 8.71/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.71/1.64 fof(f86,hypothesis,(
% 8.71/1.64 ( 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)))) ) )) ) )) ),
% 8.71/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.71/1.64 fof(f91,hypothesis,(
% 8.71/1.64 ( aFunction0(xe)& szDzozmdt0(xe) = szNzAzT0& (! [W0] :( aElementOf0(W0,szNzAzT0)=> sdtlpdtrp0(xe,W0) = szmzizndt0(sdtlpdtrp0(xN,W0)) ) )) ),
% 8.71/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.71/1.64 fof(f92,hypothesis,(
% 8.71/1.64 ( 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) ) )) )) ),
% 8.71/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.71/1.64 fof(f94,hypothesis,(
% 8.71/1.64 ( aElementOf0(szDzizrdt0(xd),xT)& isCountable0(sdtlbdtrb0(xd,szDzizrdt0(xd))) ) ),
% 8.71/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.71/1.64 fof(f96,hypothesis,(
% 8.71/1.64 ( aSet0(xO)& isCountable0(xO) ) ),
% 8.71/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.71/1.64 fof(f104,hypothesis,(
% 8.71/1.64 ( aSet0(xP)& xP = sdtmndt0(xQ,szmzizndt0(xQ)) ) ),
% 8.71/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.71/1.64 fof(f106,hypothesis,(
% 8.71/1.64 aElementOf0(xp,xO) ),
% 8.71/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.71/1.64 fof(f111,hypothesis,(
% 8.71/1.64 ( aElementOf0(xn,sdtlbdtrb0(xd,szDzizrdt0(xd)))& aElementOf0(xn,szNzAzT0)& sdtlpdtrp0(xe,xn) = xp ) ),
% 8.71/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.71/1.64 fof(f113,hypothesis,(
% 8.71/1.64 aElementOf0(xx,xP) ),
% 8.71/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.71/1.64 fof(f114,hypothesis,(
% 8.71/1.64 ( aElementOf0(xx,szNzAzT0)& aElementOf0(xx,xO) ) ),
% 8.71/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.71/1.64 fof(f115,hypothesis,(
% 8.71/1.64 ( aElementOf0(xm,szNzAzT0)& xx = sdtlpdtrp0(xe,xm) ) ),
% 8.71/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.71/1.64 fof(f117,hypothesis,(
% 8.71/1.64 ~ aSubsetOf0(sdtlpdtrp0(xN,xm),sdtlpdtrp0(xN,szszuzczcdt0(xn))) ),
% 8.71/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.71/1.64 fof(f118,hypothesis,(
% 8.71/1.64 ~ aSubsetOf0(sdtlpdtrp0(xN,xn),sdtlpdtrp0(xN,xm)) ),
% 8.71/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.71/1.64 fof(f127,plain,(
% 8.71/1.64 ![W0]: (~aSet0(W0)|(![W1]: (~aElementOf0(W1,W0)|aElement0(W1))))),
% 8.71/1.64 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 8.71/1.64 fof(f128,plain,(
% 8.71/1.64 ![X0,X1]: (~aSet0(X0)|~aElementOf0(X1,X0)|aElement0(X1))),
% 8.71/1.64 inference(cnf_transformation,[status(thm)],[f127])).
% 8.71/1.64 fof(f131,plain,(
% 8.71/1.64 ![W0]: (W0=slcrc0<=>(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0))))),
% 8.71/1.64 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 8.71/1.64 fof(f132,plain,(
% 8.71/1.64 ![W0]: ((~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0))))&(W0=slcrc0|(~aSet0(W0)|(?[W1]: aElementOf0(W1,W0)))))),
% 8.71/1.64 inference(NNF_transformation,[status(thm)],[f131])).
% 8.71/1.64 fof(f133,plain,(
% 8.71/1.64 (![W0]: (~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0)))))&(![W0]: (W0=slcrc0|(~aSet0(W0)|(?[W1]: aElementOf0(W1,W0)))))),
% 8.71/1.64 inference(miniscoping,[status(thm)],[f132])).
% 8.71/1.64 fof(f134,plain,(
% 8.71/1.64 (![W0]: (~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0)))))&(![W0]: (W0=slcrc0|(~aSet0(W0)|aElementOf0(sK0_skl(W0),W0))))),
% 8.71/1.64 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(W1,sK0_skl(W0))],[f133])).
% 8.71/1.64 fof(f135,plain,(
% 8.71/1.64 ![X0]: (~X0=slcrc0|aSet0(X0))),
% 8.71/1.64 inference(cnf_transformation,[status(thm)],[f134])).
% 8.71/1.64 fof(f136,plain,(
% 8.71/1.64 ![X0,X1]: (~X0=slcrc0|~aElementOf0(X1,X0))),
% 8.71/1.64 inference(cnf_transformation,[status(thm)],[f134])).
% 8.71/1.64 fof(f197,plain,(
% 8.71/1.64 aSet0(szNzAzT0)),
% 8.71/1.64 inference(cnf_transformation,[status(thm)],[f23])).
% 8.71/1.64 fof(f198,plain,(
% 8.71/1.64 isCountable0(szNzAzT0)),
% 8.71/1.64 inference(cnf_transformation,[status(thm)],[f23])).
% 8.71/1.64 fof(f199,plain,(
% 8.71/1.64 aElementOf0(sz00,szNzAzT0)),
% 8.71/1.64 inference(cnf_transformation,[status(thm)],[f24])).
% 8.71/1.64 fof(f200,plain,(
% 8.71/1.64 ![W0]: (~aElementOf0(W0,szNzAzT0)|(aElementOf0(szszuzczcdt0(W0),szNzAzT0)&~szszuzczcdt0(W0)=sz00))),
% 8.71/1.64 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 8.71/1.64 fof(f201,plain,(
% 8.71/1.64 ![X0]: (~aElementOf0(X0,szNzAzT0)|aElementOf0(szszuzczcdt0(X0),szNzAzT0))),
% 8.71/1.64 inference(cnf_transformation,[status(thm)],[f200])).
% 8.71/1.64 fof(f202,plain,(
% 8.71/1.64 ![X0]: (~aElementOf0(X0,szNzAzT0)|~szszuzczcdt0(X0)=sz00)),
% 8.71/1.65 inference(cnf_transformation,[status(thm)],[f200])).
% 8.71/1.65 fof(f209,plain,(
% 8.71/1.65 ![W0]: (~aElementOf0(W0,szNzAzT0)|~W0=szszuzczcdt0(W0))),
% 8.71/1.65 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 8.71/1.65 fof(f210,plain,(
% 8.71/1.65 ![X0]: (~aElementOf0(X0,szNzAzT0)|~X0=szszuzczcdt0(X0))),
% 8.71/1.65 inference(cnf_transformation,[status(thm)],[f209])).
% 8.71/1.65 fof(f213,plain,(
% 8.71/1.65 ![W0]: (~aElementOf0(W0,szNzAzT0)|sdtlseqdt0(sz00,W0))),
% 8.71/1.65 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 8.71/1.65 fof(f214,plain,(
% 8.71/1.65 ![X0]: (~aElementOf0(X0,szNzAzT0)|sdtlseqdt0(sz00,X0))),
% 8.71/1.65 inference(cnf_transformation,[status(thm)],[f213])).
% 8.71/1.65 fof(f221,plain,(
% 8.71/1.65 ![W0]: (~aElementOf0(W0,szNzAzT0)|sdtlseqdt0(W0,szszuzczcdt0(W0)))),
% 8.71/1.65 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 8.71/1.65 fof(f222,plain,(
% 8.71/1.65 ![X0]: (~aElementOf0(X0,szNzAzT0)|sdtlseqdt0(X0,szszuzczcdt0(X0)))),
% 8.71/1.65 inference(cnf_transformation,[status(thm)],[f221])).
% 8.71/1.65 fof(f223,plain,(
% 8.71/1.65 ![W0]: (~aElementOf0(W0,szNzAzT0)|sdtlseqdt0(W0,W0))),
% 8.71/1.65 inference(pre_NNF_transformation,[status(thm)],[f34])).
% 8.71/1.65 fof(f224,plain,(
% 8.71/1.65 ![X0]: (~aElementOf0(X0,szNzAzT0)|sdtlseqdt0(X0,X0))),
% 8.71/1.65 inference(cnf_transformation,[status(thm)],[f223])).
% 8.71/1.65 fof(f229,plain,(
% 8.71/1.65 ![W0,W1]: ((~aElementOf0(W0,szNzAzT0)|~aElementOf0(W1,szNzAzT0))|(sdtlseqdt0(W0,W1)|sdtlseqdt0(szszuzczcdt0(W1),W0)))),
% 8.71/1.65 inference(pre_NNF_transformation,[status(thm)],[f37])).
% 8.71/1.65 fof(f230,plain,(
% 8.71/1.65 ![X0,X1]: (~aElementOf0(X0,szNzAzT0)|~aElementOf0(X1,szNzAzT0)|sdtlseqdt0(X0,X1)|sdtlseqdt0(szszuzczcdt0(X1),X0))),
% 8.71/1.65 inference(cnf_transformation,[status(thm)],[f229])).
% 8.71/1.65 fof(f241,plain,(
% 8.71/1.65 ![W0]: (~aSet0(W0)|(sbrdtbr0(W0)=sz00<=>W0=slcrc0))),
% 8.71/1.65 inference(pre_NNF_transformation,[status(thm)],[f42])).
% 8.71/1.65 fof(f242,plain,(
% 8.71/1.65 ![W0]: (~aSet0(W0)|((~sbrdtbr0(W0)=sz00|W0=slcrc0)&(sbrdtbr0(W0)=sz00|~W0=slcrc0)))),
% 8.71/1.65 inference(NNF_transformation,[status(thm)],[f241])).
% 8.71/1.65 fof(f244,plain,(
% 8.71/1.65 ![X0]: (~aSet0(X0)|sbrdtbr0(X0)=sz00|~X0=slcrc0)),
% 8.71/1.65 inference(cnf_transformation,[status(thm)],[f242])).
% 8.71/1.65 fof(f273,plain,(
% 8.71/1.65 ![W0]: (~aElementOf0(W0,szNzAzT0)|(![W1]: (W1=slbdtrb0(W0)<=>(aSet0(W1)&(![W2]: (aElementOf0(W2,W1)<=>(aElementOf0(W2,szNzAzT0)&sdtlseqdt0(szszuzczcdt0(W2),W0))))))))),
% 8.71/1.65 inference(pre_NNF_transformation,[status(thm)],[f50])).
% 8.71/1.65 fof(f274,plain,(
% 8.71/1.65 ![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))))))))))),
% 8.71/1.65 inference(NNF_transformation,[status(thm)],[f273])).
% 8.71/1.65 fof(f275,plain,(
% 8.71/1.65 ![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))))))))))),
% 8.71/1.65 inference(miniscoping,[status(thm)],[f274])).
% 8.71/1.65 fof(f276,plain,(
% 8.71/1.65 ![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)))))))))),
% 8.71/1.65 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(W2,sK8_skl(W1,W0))],[f275])).
% 8.71/1.65 fof(f277,plain,(
% 8.71/1.65 ![X0,X1]: (~aElementOf0(X0,szNzAzT0)|~X1=slbdtrb0(X0)|aSet0(X1))),
% 8.71/1.65 inference(cnf_transformation,[status(thm)],[f276])).
% 8.71/1.65 fof(f284,plain,(
% 8.71/1.65 ![W0]: (~aElementOf0(W0,szNzAzT0)|isFinite0(slbdtrb0(W0)))),
% 8.71/1.65 inference(pre_NNF_transformation,[status(thm)],[f51])).
% 8.71/1.65 fof(f285,plain,(
% 8.71/1.65 ![X0]: (~aElementOf0(X0,szNzAzT0)|isFinite0(slbdtrb0(X0)))),
% 8.71/1.65 inference(cnf_transformation,[status(thm)],[f284])).
% 8.71/1.65 fof(f329,plain,(
% 8.71/1.65 ![W0]: (~aFunction0(W0)|aSet0(szDzozmdt0(W0)))),
% 8.71/1.65 inference(pre_NNF_transformation,[status(thm)],[f64])).
% 8.71/1.65 fof(f330,plain,(
% 8.71/1.65 ![X0]: (~aFunction0(X0)|aSet0(szDzozmdt0(X0)))),
% 8.71/1.65 inference(cnf_transformation,[status(thm)],[f329])).
% 8.71/1.65 fof(f377,plain,(
% 8.71/1.65 aSet0(xT)),
% 8.71/1.65 inference(cnf_transformation,[status(thm)],[f73])).
% 8.71/1.65 fof(f379,plain,(
% 8.71/1.65 aElementOf0(xK,szNzAzT0)),
% 8.71/1.65 inference(cnf_transformation,[status(thm)],[f74])).
% 8.71/1.65 fof(f381,plain,(
% 8.71/1.65 isCountable0(xS)),
% 8.71/1.65 inference(cnf_transformation,[status(thm)],[f75])).
% 8.71/1.65 fof(f382,plain,(
% 8.71/1.65 aFunction0(xc)),
% 8.71/1.65 inference(cnf_transformation,[status(thm)],[f76])).
% 8.71/1.65 fof(f393,plain,(
% 8.71/1.65 aElementOf0(xk,szNzAzT0)),
% 8.71/1.65 inference(cnf_transformation,[status(thm)],[f80])).
% 8.71/1.65 fof(f394,plain,(
% 8.71/1.65 szszuzczcdt0(xk)=xK),
% 8.71/1.65 inference(cnf_transformation,[status(thm)],[f80])).
% 8.71/1.65 fof(f395,plain,(
% 8.71/1.65 ((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)))))))),
% 8.71/1.65 inference(pre_NNF_transformation,[status(thm)],[f81])).
% 8.71/1.65 fof(f396,plain,(
% 8.71/1.65 aFunction0(xN)),
% 8.71/1.65 inference(cnf_transformation,[status(thm)],[f395])).
% 8.71/1.65 fof(f398,plain,(
% 8.71/1.65 sdtlpdtrp0(xN,sz00)=xS),
% 8.71/1.65 inference(cnf_transformation,[status(thm)],[f395])).
% 8.71/1.65 fof(f404,plain,(
% 8.71/1.65 ![W0,W1]: ((~aElementOf0(W0,szNzAzT0)|~aElementOf0(W1,szNzAzT0))|(~sdtlseqdt0(W1,W0)|aSubsetOf0(sdtlpdtrp0(xN,W0),sdtlpdtrp0(xN,W1))))),
% 8.71/1.65 inference(pre_NNF_transformation,[status(thm)],[f83])).
% 8.71/1.65 fof(f405,plain,(
% 8.71/1.65 ![X0,X1]: (~aElementOf0(X0,szNzAzT0)|~aElementOf0(X1,szNzAzT0)|~sdtlseqdt0(X1,X0)|aSubsetOf0(sdtlpdtrp0(xN,X0),sdtlpdtrp0(xN,X1)))),
% 8.71/1.65 inference(cnf_transformation,[status(thm)],[f404])).
% 8.71/1.65 fof(f410,plain,(
% 8.71/1.65 (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)))))))))),
% 8.71/1.65 inference(pre_NNF_transformation,[status(thm)],[f86])).
% 8.71/1.65 fof(f411,plain,(
% 8.71/1.65 aFunction0(xC)),
% 8.71/1.65 inference(cnf_transformation,[status(thm)],[f410])).
% 8.71/1.65 fof(f430,plain,(
% 8.71/1.65 (aFunction0(xe)&szDzozmdt0(xe)=szNzAzT0)&(![W0]: (~aElementOf0(W0,szNzAzT0)|sdtlpdtrp0(xe,W0)=szmzizndt0(sdtlpdtrp0(xN,W0))))),
% 8.71/1.65 inference(pre_NNF_transformation,[status(thm)],[f91])).
% 8.71/1.65 fof(f431,plain,(
% 8.71/1.65 aFunction0(xe)),
% 8.71/1.65 inference(cnf_transformation,[status(thm)],[f430])).
% 8.71/1.65 fof(f434,plain,(
% 8.71/1.65 (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)))))),
% 8.71/1.65 inference(pre_NNF_transformation,[status(thm)],[f92])).
% 8.71/1.65 fof(f435,plain,(
% 8.71/1.65 aFunction0(xd)),
% 8.71/1.65 inference(cnf_transformation,[status(thm)],[f434])).
% 8.71/1.65 fof(f439,plain,(
% 8.71/1.65 aElementOf0(szDzizrdt0(xd),xT)),
% 8.71/1.65 inference(cnf_transformation,[status(thm)],[f94])).
% 8.71/1.65 fof(f444,plain,(
% 8.71/1.65 isCountable0(xO)),
% 8.71/1.65 inference(cnf_transformation,[status(thm)],[f96])).
% 8.71/1.65 fof(f457,plain,(
% 8.71/1.65 aSet0(xP)),
% 8.71/1.65 inference(cnf_transformation,[status(thm)],[f104])).
% 8.71/1.65 fof(f460,plain,(
% 8.71/1.65 aElementOf0(xp,xO)),
% 8.71/1.65 inference(cnf_transformation,[status(thm)],[f106])).
% 8.71/1.65 fof(f466,plain,(
% 8.71/1.65 aElementOf0(xn,szNzAzT0)),
% 8.71/1.65 inference(cnf_transformation,[status(thm)],[f111])).
% 8.71/1.65 fof(f469,plain,(
% 8.71/1.65 aElementOf0(xx,xP)),
% 8.71/1.65 inference(cnf_transformation,[status(thm)],[f113])).
% 8.71/1.65 fof(f470,plain,(
% 8.71/1.65 aElementOf0(xx,szNzAzT0)),
% 8.71/1.65 inference(cnf_transformation,[status(thm)],[f114])).
% 8.71/1.65 fof(f471,plain,(
% 8.71/1.65 aElementOf0(xx,xO)),
% 8.71/1.65 inference(cnf_transformation,[status(thm)],[f114])).
% 8.71/1.65 fof(f472,plain,(
% 8.71/1.65 aElementOf0(xm,szNzAzT0)),
% 8.71/1.65 inference(cnf_transformation,[status(thm)],[f115])).
% 8.71/1.65 fof(f475,plain,(
% 8.71/1.65 ~aSubsetOf0(sdtlpdtrp0(xN,xm),sdtlpdtrp0(xN,szszuzczcdt0(xn)))),
% 8.71/1.65 inference(cnf_transformation,[status(thm)],[f117])).
% 8.71/1.65 fof(f476,plain,(
% 8.71/1.65 ~aSubsetOf0(sdtlpdtrp0(xN,xn),sdtlpdtrp0(xN,xm))),
% 8.71/1.65 inference(cnf_transformation,[status(thm)],[f118])).
% 8.71/1.65 fof(f484,plain,(
% 8.71/1.65 aSet0(slcrc0)),
% 8.71/1.65 inference(destructive_equality_resolution,[status(thm)],[f135])).
% 8.71/1.65 fof(f485,plain,(
% 8.71/1.65 ![X0]: (~aElementOf0(X0,slcrc0))),
% 8.71/1.65 inference(destructive_equality_resolution,[status(thm)],[f136])).
% 8.71/1.65 fof(f496,plain,(
% 8.71/1.65 ~aSet0(slcrc0)|sbrdtbr0(slcrc0)=sz00),
% 8.71/1.65 inference(destructive_equality_resolution,[status(thm)],[f244])).
% 8.71/1.65 fof(f501,plain,(
% 8.71/1.65 ![X0]: (~aElementOf0(X0,szNzAzT0)|aSet0(slbdtrb0(X0)))),
% 8.71/1.65 inference(destructive_equality_resolution,[status(thm)],[f277])).
% 8.71/1.65 fof(f531,plain,(
% 8.71/1.65 ![X0]: (~aElementOf0(X0,xT)|aElement0(X0))),
% 8.71/1.65 inference(resolution,[status(thm)],[f128,f377])).
% 8.71/1.65 fof(f532,plain,(
% 8.71/1.65 ![X0]: (~aElementOf0(X0,szNzAzT0)|aElement0(X0))),
% 8.71/1.65 inference(resolution,[status(thm)],[f128,f197])).
% 8.71/1.65 fof(f579,plain,(
% 8.71/1.65 ![X0]: (~aElementOf0(X0,xP)|aElement0(X0))),
% 8.71/1.65 inference(resolution,[status(thm)],[f457,f128])).
% 8.71/1.65 fof(f680,plain,(
% 8.71/1.65 ~sz00=szszuzczcdt0(sz00)),
% 8.71/1.65 inference(resolution,[status(thm)],[f199,f210])).
% 8.71/1.65 fof(f1005,plain,(
% 8.71/1.65 ~xm=szszuzczcdt0(xm)),
% 8.71/1.65 inference(resolution,[status(thm)],[f472,f210])).
% 8.71/1.65 fof(f1396,plain,(
% 8.71/1.65 ~szszuzczcdt0(xx)=sz00),
% 8.71/1.65 inference(resolution,[status(thm)],[f202,f470])).
% 8.71/1.65 fof(f1540,plain,(
% 8.71/1.65 sdtlseqdt0(xK,xK)),
% 8.71/1.65 inference(resolution,[status(thm)],[f379,f224])).
% 8.71/1.65 fof(f1543,plain,(
% 8.71/1.65 aElementOf0(szszuzczcdt0(xK),szNzAzT0)),
% 8.71/1.65 inference(resolution,[status(thm)],[f379,f201])).
% 8.71/1.65 fof(f1555,plain,(
% 8.71/1.65 aElementOf0(szszuzczcdt0(xm),szNzAzT0)),
% 8.71/1.65 inference(resolution,[status(thm)],[f472,f201])).
% 8.71/1.65 fof(f1622,plain,(
% 8.71/1.65 sdtlseqdt0(xx,szszuzczcdt0(xx))),
% 8.71/1.65 inference(resolution,[status(thm)],[f470,f222])).
% 8.71/1.65 fof(f1624,plain,(
% 8.71/1.65 aElementOf0(szszuzczcdt0(xx),szNzAzT0)),
% 8.71/1.65 inference(resolution,[status(thm)],[f470,f201])).
% 8.71/1.65 fof(f1641,definition,(
% 8.71/1.65 sQ126_spl <=> (aElementOf0(xm,szNzAzT0))),
% 8.71/1.65 introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition])).
% 8.71/1.65 fof(f1643,plain,(
% 8.71/1.65 ~aElementOf0(xm,szNzAzT0)|sQ126_spl),
% 8.71/1.65 inference(component_clause,[status(thm)],[f1641])).
% 8.71/1.65 fof(f1652,plain,(
% 8.71/1.65 $false|sQ126_spl),
% 8.71/1.65 inference(forward_subsumption_resolution,[status(thm)],[f1643,f472])).
% 8.71/1.65 fof(f1653,plain,(
% 8.71/1.65 sQ126_spl),
% 8.71/1.65 inference(contradiction_clause,[status(thm)],[f1652])).
% 8.71/1.65 fof(f1668,plain,(
% 8.71/1.65 sbrdtbr0(slcrc0)=sz00),
% 8.71/1.65 inference(forward_subsumption_resolution,[status(thm)],[f496,f484])).
% 8.71/1.65 fof(f1674,definition,(
% 8.71/1.65 sQ131_spl <=> (aElementOf0(sz00,szNzAzT0))),
% 8.71/1.65 introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition])).
% 8.71/1.65 fof(f1676,plain,(
% 8.71/1.65 ~aElementOf0(sz00,szNzAzT0)|sQ131_spl),
% 8.71/1.65 inference(component_clause,[status(thm)],[f1674])).
% 8.71/1.65 fof(f1687,plain,(
% 8.71/1.65 sdtlseqdt0(xn,szszuzczcdt0(xn))),
% 8.71/1.65 inference(resolution,[status(thm)],[f466,f222])).
% 8.71/1.65 fof(f1689,plain,(
% 8.71/1.65 aElementOf0(szszuzczcdt0(xn),szNzAzT0)),
% 8.71/1.65 inference(resolution,[status(thm)],[f466,f201])).
% 8.71/1.65 fof(f1707,definition,(
% 8.71/1.65 sQ135_spl <=> (aElementOf0(xn,szNzAzT0))),
% 8.71/1.65 introduced(definition,[new_symbols(definition,[sQ135_spl])],[split_symbol_definition])).
% 8.71/1.65 fof(f1709,plain,(
% 8.71/1.65 ~aElementOf0(xn,szNzAzT0)|sQ135_spl),
% 8.71/1.65 inference(component_clause,[status(thm)],[f1707])).
% 8.71/1.65 fof(f1785,plain,(
% 8.71/1.65 $false|sQ135_spl),
% 8.71/1.65 inference(forward_subsumption_resolution,[status(thm)],[f1709,f466])).
% 8.71/1.65 fof(f1786,plain,(
% 8.71/1.65 sQ135_spl),
% 8.71/1.65 inference(contradiction_clause,[status(thm)],[f1785])).
% 8.71/1.65 fof(f1812,definition,(
% 8.71/1.65 sQ153_spl <=> (szszuzczcdt0(xm)=szszuzczcdt0(xm))),
% 8.71/1.65 introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition])).
% 8.71/1.65 fof(f1814,plain,(
% 8.71/1.65 ~szszuzczcdt0(xm)=szszuzczcdt0(xm)|sQ153_spl),
% 8.71/1.65 inference(component_clause,[status(thm)],[f1812])).
% 8.71/1.65 fof(f1913,plain,(
% 8.71/1.65 sdtlseqdt0(sz00,szszuzczcdt0(sz00))),
% 8.71/1.65 inference(resolution,[status(thm)],[f199,f222])).
% 8.71/1.65 fof(f1963,definition,(
% 8.71/1.65 sQ167_spl <=> (sdtlseqdt0(xK,xK))),
% 8.71/1.65 introduced(definition,[new_symbols(definition,[sQ167_spl])],[split_symbol_definition])).
% 8.71/1.65 fof(f1965,plain,(
% 8.71/1.65 ~sdtlseqdt0(xK,xK)|sQ167_spl),
% 8.71/1.65 inference(component_clause,[status(thm)],[f1963])).
% 8.71/1.65 fof(f2072,definition,(
% 8.71/1.65 sQ184_spl <=> (aElementOf0(szszuzczcdt0(xn),szNzAzT0))),
% 8.71/1.65 introduced(definition,[new_symbols(definition,[sQ184_spl])],[split_symbol_definition])).
% 8.71/1.65 fof(f2074,plain,(
% 8.71/1.65 ~aElementOf0(szszuzczcdt0(xn),szNzAzT0)|sQ184_spl),
% 8.71/1.65 inference(component_clause,[status(thm)],[f2072])).
% 8.71/1.65 fof(f2161,plain,(
% 8.71/1.65 sdtlseqdt0(xk,xk)),
% 8.71/1.65 inference(resolution,[status(thm)],[f393,f224])).
% 8.71/1.65 fof(f2162,plain,(
% 8.71/1.65 sdtlseqdt0(xk,szszuzczcdt0(xk))),
% 8.71/1.65 inference(resolution,[status(thm)],[f393,f222])).
% 8.71/1.65 fof(f2186,definition,(
% 8.71/1.65 sQ199_spl <=> (aElementOf0(szmzazxdt0(slcrc0),slcrc0))),
% 8.71/1.65 introduced(definition,[new_symbols(definition,[sQ199_spl])],[split_symbol_definition])).
% 8.71/1.65 fof(f2187,plain,(
% 8.71/1.65 aElementOf0(szmzazxdt0(slcrc0),slcrc0)|~sQ199_spl),
% 8.71/1.65 inference(component_clause,[status(thm)],[f2186])).
% 8.71/1.65 fof(f2429,plain,(
% 8.71/1.65 aSet0(slbdtrb0(xn))),
% 8.71/1.65 inference(resolution,[status(thm)],[f501,f466])).
% 8.71/1.65 fof(f2430,plain,(
% 8.71/1.65 aSet0(slbdtrb0(xk))),
% 8.71/1.65 inference(resolution,[status(thm)],[f501,f393])).
% 8.71/1.65 fof(f2431,plain,(
% 8.71/1.65 aSet0(slbdtrb0(xx))),
% 8.71/1.65 inference(resolution,[status(thm)],[f501,f470])).
% 8.71/1.65 fof(f2432,plain,(
% 8.71/1.65 aSet0(slbdtrb0(xm))),
% 8.71/1.65 inference(resolution,[status(thm)],[f501,f472])).
% 8.71/1.65 fof(f2433,plain,(
% 8.71/1.65 aSet0(slbdtrb0(xK))),
% 8.71/1.65 inference(resolution,[status(thm)],[f501,f379])).
% 8.71/1.65 fof(f2569,plain,(
% 8.71/1.65 aSet0(slbdtrb0(szszuzczcdt0(xK)))),
% 8.71/1.65 inference(resolution,[status(thm)],[f1543,f501])).
% 8.71/1.65 fof(f2621,plain,(
% 8.71/1.65 aSet0(slbdtrb0(szszuzczcdt0(xm)))),
% 8.71/1.65 inference(resolution,[status(thm)],[f1555,f501])).
% 8.71/1.65 fof(f2662,definition,(
% 8.71/1.65 sQ247_spl <=> (szszuzczcdt0(xm)=xm)),
% 8.71/1.65 introduced(definition,[new_symbols(definition,[sQ247_spl])],[split_symbol_definition])).
% 8.71/1.65 fof(f2663,plain,(
% 8.71/1.65 szszuzczcdt0(xm)=xm|~sQ247_spl),
% 8.71/1.65 inference(component_clause,[status(thm)],[f2662])).
% 8.71/1.65 fof(f2724,definition,(
% 8.71/1.65 sQ255_spl <=> (sdtlseqdt0(xk,xk))),
% 8.71/1.65 introduced(definition,[new_symbols(definition,[sQ255_spl])],[split_symbol_definition])).
% 8.71/1.65 fof(f2726,plain,(
% 8.71/1.65 ~sdtlseqdt0(xk,xk)|sQ255_spl),
% 8.71/1.65 inference(component_clause,[status(thm)],[f2724])).
% 8.71/1.65 fof(f2779,plain,(
% 8.71/1.65 aSet0(slbdtrb0(szszuzczcdt0(xx)))),
% 8.71/1.65 inference(resolution,[status(thm)],[f1624,f501])).
% 8.71/1.65 fof(f2836,plain,(
% 8.71/1.65 aSet0(slbdtrb0(szszuzczcdt0(xn)))),
% 8.71/1.65 inference(resolution,[status(thm)],[f1689,f501])).
% 8.71/1.65 fof(f2866,plain,(
% 8.71/1.65 $false|sQ184_spl),
% 8.71/1.65 inference(forward_subsumption_resolution,[status(thm)],[f2074,f1689])).
% 8.71/1.65 fof(f2867,plain,(
% 8.71/1.65 sQ184_spl),
% 8.71/1.65 inference(contradiction_clause,[status(thm)],[f2866])).
% 8.71/1.65 fof(f2869,definition,(
% 8.71/1.65 sQ268_spl <=> (aElement0(xm))),
% 8.71/1.65 introduced(definition,[new_symbols(definition,[sQ268_spl])],[split_symbol_definition])).
% 8.71/1.65 fof(f2871,plain,(
% 8.71/1.65 ~aElement0(xm)|sQ268_spl),
% 8.71/1.65 inference(component_clause,[status(thm)],[f2869])).
% 8.71/1.65 fof(f2878,definition,(
% 8.71/1.65 sQ271_spl <=> (isCountable0(szNzAzT0))),
% 8.71/1.65 introduced(definition,[new_symbols(definition,[sQ271_spl])],[split_symbol_definition])).
% 8.71/1.65 fof(f2880,plain,(
% 8.71/1.65 ~isCountable0(szNzAzT0)|sQ271_spl),
% 8.71/1.65 inference(component_clause,[status(thm)],[f2878])).
% 8.71/1.65 fof(f2913,plain,(
% 8.71/1.65 aSet0(szDzozmdt0(xc))),
% 8.71/1.65 inference(resolution,[status(thm)],[f330,f382])).
% 8.71/1.65 fof(f2926,plain,(
% 8.71/1.65 isFinite0(slbdtrb0(xn))),
% 8.71/1.65 inference(resolution,[status(thm)],[f285,f466])).
% 8.71/1.65 fof(f2927,plain,(
% 8.71/1.65 isFinite0(slbdtrb0(xk))),
% 8.71/1.65 inference(resolution,[status(thm)],[f285,f393])).
% 8.71/1.65 fof(f2928,plain,(
% 8.71/1.65 isFinite0(slbdtrb0(xx))),
% 8.71/1.65 inference(resolution,[status(thm)],[f285,f470])).
% 8.71/1.65 fof(f2929,plain,(
% 8.71/1.65 isFinite0(slbdtrb0(xm))),
% 8.71/1.65 inference(resolution,[status(thm)],[f285,f472])).
% 8.71/1.65 fof(f2930,plain,(
% 8.71/1.65 isFinite0(slbdtrb0(xK))),
% 8.71/1.65 inference(resolution,[status(thm)],[f285,f379])).
% 8.71/1.65 fof(f2949,definition,(
% 8.71/1.65 sQ277_spl <=> (aSet0(slbdtrb0(xn)))),
% 8.71/1.65 introduced(definition,[new_symbols(definition,[sQ277_spl])],[split_symbol_definition])).
% 8.71/1.65 fof(f2951,plain,(
% 8.71/1.65 ~aSet0(slbdtrb0(xn))|sQ277_spl),
% 8.71/1.65 inference(component_clause,[status(thm)],[f2949])).
% 8.71/1.65 fof(f2976,plain,(
% 8.71/1.65 $false|sQ277_spl),
% 8.71/1.65 inference(forward_subsumption_resolution,[status(thm)],[f2951,f2429])).
% 8.71/1.65 fof(f2977,plain,(
% 8.71/1.65 sQ277_spl),
% 8.71/1.65 inference(contradiction_clause,[status(thm)],[f2976])).
% 8.71/1.65 fof(f2999,definition,(
% 8.71/1.65 sQ288_spl <=> (aElement0(xx))),
% 8.71/1.65 introduced(definition,[new_symbols(definition,[sQ288_spl])],[split_symbol_definition])).
% 8.71/1.65 fof(f3001,plain,(
% 8.71/1.65 ~aElement0(xx)|sQ288_spl),
% 8.71/1.65 inference(component_clause,[status(thm)],[f2999])).
% 8.71/1.65 fof(f3025,definition,(
% 8.71/1.65 sQ293_spl <=> (aSet0(slbdtrb0(xk)))),
% 8.71/1.65 introduced(definition,[new_symbols(definition,[sQ293_spl])],[split_symbol_definition])).
% 8.71/1.65 fof(f3027,plain,(
% 8.71/1.65 ~aSet0(slbdtrb0(xk))|sQ293_spl),
% 8.71/1.65 inference(component_clause,[status(thm)],[f3025])).
% 8.71/1.65 fof(f3052,plain,(
% 8.71/1.65 $false|sQ293_spl),
% 8.71/1.65 inference(forward_subsumption_resolution,[status(thm)],[f3027,f2430])).
% 8.71/1.65 fof(f3053,plain,(
% 8.71/1.65 sQ293_spl),
% 8.71/1.65 inference(contradiction_clause,[status(thm)],[f3052])).
% 8.71/1.65 fof(f3060,definition,(
% 8.71/1.65 sQ300_spl <=> (aSet0(slbdtrb0(xm)))),
% 8.71/1.65 introduced(definition,[new_symbols(definition,[sQ300_spl])],[split_symbol_definition])).
% 8.71/1.65 fof(f3062,plain,(
% 8.71/1.65 ~aSet0(slbdtrb0(xm))|sQ300_spl),
% 8.71/1.65 inference(component_clause,[status(thm)],[f3060])).
% 8.71/1.65 fof(f3087,plain,(
% 8.71/1.65 $false|sQ300_spl),
% 8.71/1.65 inference(forward_subsumption_resolution,[status(thm)],[f3062,f2432])).
% 8.71/1.65 fof(f3088,plain,(
% 8.71/1.65 sQ300_spl),
% 8.71/1.65 inference(contradiction_clause,[status(thm)],[f3087])).
% 8.71/1.65 fof(f3095,definition,(
% 8.71/1.65 sQ307_spl <=> (aSet0(slbdtrb0(xK)))),
% 8.71/1.65 introduced(definition,[new_symbols(definition,[sQ307_spl])],[split_symbol_definition])).
% 8.71/1.65 fof(f3097,plain,(
% 8.71/1.65 ~aSet0(slbdtrb0(xK))|sQ307_spl),
% 8.71/1.65 inference(component_clause,[status(thm)],[f3095])).
% 8.71/1.65 fof(f3122,plain,(
% 8.71/1.65 $false|sQ307_spl),
% 8.71/1.65 inference(forward_subsumption_resolution,[status(thm)],[f3097,f2433])).
% 8.71/1.65 fof(f3123,plain,(
% 8.71/1.65 sQ307_spl),
% 8.71/1.65 inference(contradiction_clause,[status(thm)],[f3122])).
% 8.71/1.65 fof(f3393,definition,(
% 8.71/1.65 sQ320_spl <=> (aSet0(slbdtrb0(szszuzczcdt0(xn))))),
% 8.71/1.65 introduced(definition,[new_symbols(definition,[sQ320_spl])],[split_symbol_definition])).
% 8.71/1.65 fof(f3395,plain,(
% 8.71/1.65 ~aSet0(slbdtrb0(szszuzczcdt0(xn)))|sQ320_spl),
% 8.71/1.65 inference(component_clause,[status(thm)],[f3393])).
% 8.71/1.65 fof(f3408,plain,(
% 8.71/1.65 $false|sQ320_spl),
% 8.71/1.65 inference(forward_subsumption_resolution,[status(thm)],[f3395,f2836])).
% 8.71/1.65 fof(f3409,plain,(
% 8.71/1.65 sQ320_spl),
% 8.71/1.65 inference(contradiction_clause,[status(thm)],[f3408])).
% 8.71/1.65 fof(f3413,definition,(
% 8.71/1.65 sQ324_spl <=> (aSet0(slbdtrb0(szszuzczcdt0(xx))))),
% 8.71/1.65 introduced(definition,[new_symbols(definition,[sQ324_spl])],[split_symbol_definition])).
% 8.71/1.65 fof(f3415,plain,(
% 8.71/1.65 ~aSet0(slbdtrb0(szszuzczcdt0(xx)))|sQ324_spl),
% 8.71/1.65 inference(component_clause,[status(thm)],[f3413])).
% 8.71/1.65 fof(f3428,plain,(
% 8.71/1.65 $false|sQ324_spl),
% 8.71/1.65 inference(forward_subsumption_resolution,[status(thm)],[f3415,f2779])).
% 8.71/1.65 fof(f3429,plain,(
% 8.71/1.65 sQ324_spl),
% 8.71/1.65 inference(contradiction_clause,[status(thm)],[f3428])).
% 8.71/1.65 fof(f3447,definition,(
% 8.71/1.65 sQ328_spl <=> (aSet0(slbdtrb0(szszuzczcdt0(xm))))),
% 8.71/1.65 introduced(definition,[new_symbols(definition,[sQ328_spl])],[split_symbol_definition])).
% 8.71/1.65 fof(f3449,plain,(
% 8.71/1.65 ~aSet0(slbdtrb0(szszuzczcdt0(xm)))|sQ328_spl),
% 8.71/1.65 inference(component_clause,[status(thm)],[f3447])).
% 8.71/1.65 fof(f3462,plain,(
% 8.71/1.65 $false|sQ328_spl),
% 8.71/1.65 inference(forward_subsumption_resolution,[status(thm)],[f3449,f2621])).
% 8.71/1.65 fof(f3463,plain,(
% 8.71/1.65 sQ328_spl),
% 8.71/1.65 inference(contradiction_clause,[status(thm)],[f3462])).
% 8.71/1.65 fof(f3467,definition,(
% 8.71/1.65 sQ332_spl <=> (aSet0(slbdtrb0(szszuzczcdt0(xK))))),
% 8.71/1.65 introduced(definition,[new_symbols(definition,[sQ332_spl])],[split_symbol_definition])).
% 8.71/1.65 fof(f3469,plain,(
% 8.71/1.65 ~aSet0(slbdtrb0(szszuzczcdt0(xK)))|sQ332_spl),
% 8.71/1.65 inference(component_clause,[status(thm)],[f3467])).
% 8.71/1.65 fof(f3482,plain,(
% 8.71/1.65 $false|sQ332_spl),
% 8.71/1.65 inference(forward_subsumption_resolution,[status(thm)],[f3469,f2569])).
% 8.71/1.65 fof(f3483,plain,(
% 8.71/1.65 sQ332_spl),
% 8.71/1.65 inference(contradiction_clause,[status(thm)],[f3482])).
% 8.71/1.65 fof(f3512,definition,(
% 8.71/1.65 sQ342_spl <=> (aSet0(szDzozmdt0(xc)))),
% 8.71/1.65 introduced(definition,[new_symbols(definition,[sQ342_spl])],[split_symbol_definition])).
% 8.71/1.65 fof(f3514,plain,(
% 8.71/1.65 ~aSet0(szDzozmdt0(xc))|sQ342_spl),
% 8.71/1.65 inference(component_clause,[status(thm)],[f3512])).
% 8.71/1.65 fof(f3519,plain,(
% 8.71/1.65 $false|sQ342_spl),
% 8.71/1.65 inference(forward_subsumption_resolution,[status(thm)],[f3514,f2913])).
% 8.71/1.65 fof(f3520,plain,(
% 8.71/1.65 sQ342_spl),
% 8.71/1.65 inference(contradiction_clause,[status(thm)],[f3519])).
% 8.71/1.65 fof(f3521,plain,(
% 8.71/1.65 aElement0(szDzizrdt0(xd))),
% 8.71/1.65 inference(resolution,[status(thm)],[f531,f439])).
% 8.71/1.65 fof(f3541,plain,(
% 8.71/1.65 aElement0(xm)),
% 8.71/1.65 inference(resolution,[status(thm)],[f532,f472])).
% 8.71/1.65 fof(f3546,plain,(
% 8.71/1.65 aElement0(xn)),
% 8.71/1.65 inference(resolution,[status(thm)],[f532,f466])).
% 8.71/1.65 fof(f3623,definition,(
% 8.71/1.65 sQ346_spl <=> (aElement0(xn))),
% 8.71/1.65 introduced(definition,[new_symbols(definition,[sQ346_spl])],[split_symbol_definition])).
% 8.71/1.65 fof(f3625,plain,(
% 8.71/1.65 ~aElement0(xn)|sQ346_spl),
% 8.71/1.65 inference(component_clause,[status(thm)],[f3623])).
% 8.71/1.65 fof(f3808,plain,(
% 8.71/1.65 aElement0(xx)),
% 8.71/1.65 inference(resolution,[status(thm)],[f579,f469])).
% 8.71/1.65 fof(f3814,definition,(
% 8.71/1.65 ![X0]: (sQ359_spl <=> (~aSet0(X0)|~aSet0(X0)))),
% 8.71/1.65 introduced(definition,[new_symbols(definition,[sQ359_spl])],[split_symbol_definition])).
% 8.71/1.65 fof(f3815,plain,(
% 8.71/1.65 ![X0]: (~aSet0(X0)|~aSet0(X0)|~sQ359_spl)),
% 8.71/1.65 inference(component_clause,[status(thm)],[f3814])).
% 8.71/1.65 fof(f3855,definition,(
% 8.71/1.66 sQ361_spl <=> (isFinite0(slbdtrb0(xn)))),
% 8.71/1.66 introduced(definition,[new_symbols(definition,[sQ361_spl])],[split_symbol_definition])).
% 8.71/1.66 fof(f3857,plain,(
% 8.71/1.66 ~isFinite0(slbdtrb0(xn))|sQ361_spl),
% 8.71/1.66 inference(component_clause,[status(thm)],[f3855])).
% 8.71/1.66 fof(f3863,plain,(
% 8.71/1.66 $false|sQ361_spl),
% 8.71/1.66 inference(forward_subsumption_resolution,[status(thm)],[f3857,f2926])).
% 8.71/1.66 fof(f3864,plain,(
% 8.71/1.66 sQ361_spl),
% 8.71/1.66 inference(contradiction_clause,[status(thm)],[f3863])).
% 8.71/1.66 fof(f3968,definition,(
% 8.71/1.66 sQ371_spl <=> (aSet0(slbdtrb0(xx)))),
% 8.71/1.66 introduced(definition,[new_symbols(definition,[sQ371_spl])],[split_symbol_definition])).
% 8.71/1.66 fof(f3970,plain,(
% 8.71/1.66 ~aSet0(slbdtrb0(xx))|sQ371_spl),
% 8.71/1.66 inference(component_clause,[status(thm)],[f3968])).
% 8.71/1.66 fof(f4001,plain,(
% 8.71/1.66 $false|sQ371_spl),
% 8.71/1.66 inference(forward_subsumption_resolution,[status(thm)],[f3970,f2431])).
% 8.71/1.66 fof(f4002,plain,(
% 8.71/1.66 sQ371_spl),
% 8.71/1.66 inference(contradiction_clause,[status(thm)],[f4001])).
% 8.71/1.66 fof(f4098,plain,(
% 8.71/1.66 $false|sQ131_spl),
% 8.71/1.66 inference(forward_subsumption_resolution,[status(thm)],[f1676,f199])).
% 8.71/1.66 fof(f4099,plain,(
% 8.71/1.66 sQ131_spl),
% 8.71/1.66 inference(contradiction_clause,[status(thm)],[f4098])).
% 8.71/1.66 fof(f4183,definition,(
% 8.71/1.66 sQ394_spl <=> (isCountable0(xO))),
% 8.71/1.66 introduced(definition,[new_symbols(definition,[sQ394_spl])],[split_symbol_definition])).
% 8.71/1.66 fof(f4185,plain,(
% 8.71/1.66 ~isCountable0(xO)|sQ394_spl),
% 8.71/1.66 inference(component_clause,[status(thm)],[f4183])).
% 8.71/1.66 fof(f4194,definition,(
% 8.71/1.66 sQ396_spl <=> (isFinite0(slbdtrb0(xx)))),
% 8.71/1.66 introduced(definition,[new_symbols(definition,[sQ396_spl])],[split_symbol_definition])).
% 8.71/1.66 fof(f4196,plain,(
% 8.71/1.66 ~isFinite0(slbdtrb0(xx))|sQ396_spl),
% 8.71/1.66 inference(component_clause,[status(thm)],[f4194])).
% 8.71/1.66 fof(f4202,plain,(
% 8.71/1.66 $false|sQ396_spl),
% 8.71/1.66 inference(forward_subsumption_resolution,[status(thm)],[f4196,f2928])).
% 8.71/1.66 fof(f4203,plain,(
% 8.71/1.66 sQ396_spl),
% 8.71/1.66 inference(contradiction_clause,[status(thm)],[f4202])).
% 8.71/1.66 fof(f4288,definition,(
% 8.71/1.66 sQ409_spl <=> (sdtlseqdt0(sz00,xn))),
% 8.71/1.66 introduced(definition,[new_symbols(definition,[sQ409_spl])],[split_symbol_definition])).
% 8.71/1.66 fof(f4290,plain,(
% 8.71/1.66 ~sdtlseqdt0(sz00,xn)|sQ409_spl),
% 8.71/1.66 inference(component_clause,[status(thm)],[f4288])).
% 8.71/1.66 fof(f4291,definition,(
% 8.71/1.66 sQ410_spl <=> (sdtlseqdt0(xn,szszuzczcdt0(xn)))),
% 8.71/1.66 introduced(definition,[new_symbols(definition,[sQ410_spl])],[split_symbol_definition])).
% 8.71/1.66 fof(f4293,plain,(
% 8.71/1.66 ~sdtlseqdt0(xn,szszuzczcdt0(xn))|sQ410_spl),
% 8.71/1.66 inference(component_clause,[status(thm)],[f4291])).
% 8.71/1.66 fof(f4295,definition,(
% 8.71/1.66 sQ411_spl <=> (isCountable0(sdtlpdtrp0(xN,sz00)))),
% 8.71/1.66 introduced(definition,[new_symbols(definition,[sQ411_spl])],[split_symbol_definition])).
% 8.71/1.66 fof(f4297,plain,(
% 8.71/1.66 ~isCountable0(sdtlpdtrp0(xN,sz00))|sQ411_spl),
% 8.71/1.66 inference(component_clause,[status(thm)],[f4295])).
% 8.71/1.66 fof(f4303,plain,(
% 8.71/1.66 $false|sQ410_spl),
% 8.71/1.66 inference(forward_subsumption_resolution,[status(thm)],[f4293,f1687])).
% 8.71/1.66 fof(f4304,plain,(
% 8.71/1.66 sQ410_spl),
% 8.71/1.66 inference(contradiction_clause,[status(thm)],[f4303])).
% 8.71/1.66 fof(f4374,definition,(
% 8.71/1.66 sQ422_spl <=> (sdtlseqdt0(xx,szszuzczcdt0(xx)))),
% 8.71/1.66 introduced(definition,[new_symbols(definition,[sQ422_spl])],[split_symbol_definition])).
% 8.71/1.66 fof(f4376,plain,(
% 8.71/1.66 ~sdtlseqdt0(xx,szszuzczcdt0(xx))|sQ422_spl),
% 8.71/1.66 inference(component_clause,[status(thm)],[f4374])).
% 8.71/1.66 fof(f4386,plain,(
% 8.71/1.66 $false|sQ422_spl),
% 8.71/1.66 inference(forward_subsumption_resolution,[status(thm)],[f4376,f1622])).
% 8.71/1.66 fof(f4387,plain,(
% 8.71/1.66 sQ422_spl),
% 8.71/1.66 inference(contradiction_clause,[status(thm)],[f4386])).
% 8.71/1.66 fof(f4422,definition,(
% 8.71/1.66 sQ427_spl <=> (aFunction0(xd))),
% 8.71/1.66 introduced(definition,[new_symbols(definition,[sQ427_spl])],[split_symbol_definition])).
% 8.71/1.66 fof(f4424,plain,(
% 8.71/1.66 ~aFunction0(xd)|sQ427_spl),
% 8.71/1.66 inference(component_clause,[status(thm)],[f4422])).
% 8.71/1.66 fof(f4425,definition,(
% 8.71/1.66 sQ428_spl <=> (aElement0(szDzizrdt0(xd)))),
% 8.71/1.66 introduced(definition,[new_symbols(definition,[sQ428_spl])],[split_symbol_definition])).
% 8.71/1.66 fof(f4427,plain,(
% 8.71/1.66 ~aElement0(szDzizrdt0(xd))|sQ428_spl),
% 8.71/1.66 inference(component_clause,[status(thm)],[f4425])).
% 8.71/1.66 fof(f4429,plain,(
% 8.71/1.66 $false|sQ427_spl),
% 8.71/1.66 inference(forward_subsumption_resolution,[status(thm)],[f4424,f435])).
% 8.71/1.66 fof(f4430,plain,(
% 8.71/1.66 sQ427_spl),
% 8.71/1.66 inference(contradiction_clause,[status(thm)],[f4429])).
% 8.71/1.66 fof(f4431,plain,(
% 8.71/1.66 $false|sQ428_spl),
% 8.71/1.66 inference(forward_subsumption_resolution,[status(thm)],[f4427,f3521])).
% 8.71/1.66 fof(f4432,plain,(
% 8.71/1.66 sQ428_spl),
% 8.71/1.66 inference(contradiction_clause,[status(thm)],[f4431])).
% 8.71/1.66 fof(f4614,plain,(
% 8.71/1.66 ![X0]: (~aSet0(X0)|~sQ359_spl)),
% 8.71/1.66 inference(duplicate_literals_removal,[status(thm)],[f3815])).
% 8.71/1.66 fof(f4615,plain,(
% 8.71/1.66 $false|sQ346_spl),
% 8.71/1.66 inference(forward_subsumption_resolution,[status(thm)],[f3625,f3546])).
% 8.71/1.66 fof(f4616,plain,(
% 8.71/1.66 sQ346_spl),
% 8.71/1.66 inference(contradiction_clause,[status(thm)],[f4615])).
% 8.71/1.66 fof(f4618,plain,(
% 8.71/1.66 $false|sQ268_spl),
% 8.71/1.66 inference(forward_subsumption_resolution,[status(thm)],[f2871,f3541])).
% 8.71/1.66 fof(f4619,plain,(
% 8.71/1.66 sQ268_spl),
% 8.71/1.66 inference(contradiction_clause,[status(thm)],[f4618])).
% 8.71/1.66 fof(f4623,plain,(
% 8.71/1.66 $false|sQ255_spl),
% 8.71/1.66 inference(forward_subsumption_resolution,[status(thm)],[f2726,f2161])).
% 8.71/1.66 fof(f4624,plain,(
% 8.71/1.66 sQ255_spl),
% 8.71/1.66 inference(contradiction_clause,[status(thm)],[f4623])).
% 8.71/1.66 fof(f4625,plain,(
% 8.71/1.66 $false|~sQ247_spl),
% 8.71/1.66 inference(forward_subsumption_resolution,[status(thm)],[f2663,f1005])).
% 8.71/1.66 fof(f4626,plain,(
% 8.71/1.66 ~sQ247_spl),
% 8.71/1.66 inference(contradiction_clause,[status(thm)],[f4625])).
% 8.71/1.66 fof(f4630,plain,(
% 8.71/1.66 $false|~sQ199_spl),
% 8.71/1.66 inference(forward_subsumption_resolution,[status(thm)],[f2187,f485])).
% 8.71/1.66 fof(f4631,plain,(
% 8.71/1.66 ~sQ199_spl),
% 8.71/1.66 inference(contradiction_clause,[status(thm)],[f4630])).
% 8.71/1.66 fof(f4634,plain,(
% 8.71/1.66 $false|sQ167_spl),
% 8.71/1.66 inference(forward_subsumption_resolution,[status(thm)],[f1965,f1540])).
% 8.71/1.66 fof(f4635,plain,(
% 8.71/1.66 sQ167_spl),
% 8.71/1.66 inference(contradiction_clause,[status(thm)],[f4634])).
% 8.71/1.66 fof(f4636,plain,(
% 8.71/1.66 $false|sQ153_spl),
% 8.71/1.66 inference(trivial_equality_resolution,[status(thm)],[f1814])).
% 8.71/1.66 fof(f4637,plain,(
% 8.71/1.66 sQ153_spl),
% 8.71/1.66 inference(contradiction_clause,[status(thm)],[f4636])).
% 8.71/1.66 fof(f4642,plain,(
% 8.71/1.66 $false|sQ288_spl),
% 8.71/1.66 inference(forward_subsumption_resolution,[status(thm)],[f3001,f3808])).
% 8.71/1.66 fof(f4643,plain,(
% 8.71/1.66 sQ288_spl),
% 8.71/1.66 inference(contradiction_clause,[status(thm)],[f4642])).
% 8.71/1.66 fof(f4644,plain,(
% 8.71/1.66 $false|sQ394_spl),
% 8.71/1.66 inference(forward_subsumption_resolution,[status(thm)],[f4185,f444])).
% 8.71/1.66 fof(f4645,plain,(
% 8.71/1.66 sQ394_spl),
% 8.71/1.66 inference(contradiction_clause,[status(thm)],[f4644])).
% 8.71/1.66 fof(f4686,definition,(
% 8.71/1.66 sQ444_spl <=> (szszuzczcdt0(sz00)=sz00)),
% 8.71/1.66 introduced(definition,[new_symbols(definition,[sQ444_spl])],[split_symbol_definition])).
% 8.71/1.66 fof(f4687,plain,(
% 8.71/1.66 szszuzczcdt0(sz00)=sz00|~sQ444_spl),
% 8.71/1.66 inference(component_clause,[status(thm)],[f4686])).
% 8.71/1.66 fof(f4700,definition,(
% 8.71/1.66 sQ448_spl <=> (szszuzczcdt0(xx)=sz00)),
% 8.71/1.66 introduced(definition,[new_symbols(definition,[sQ448_spl])],[split_symbol_definition])).
% 8.71/1.66 fof(f4701,plain,(
% 8.71/1.66 szszuzczcdt0(xx)=sz00|~sQ448_spl),
% 8.71/1.66 inference(component_clause,[status(thm)],[f4700])).
% 8.71/1.66 fof(f4998,plain,(
% 8.71/1.66 $false|~sQ444_spl),
% 8.71/1.66 inference(forward_subsumption_resolution,[status(thm)],[f4687,f680])).
% 8.71/1.66 fof(f4999,plain,(
% 8.71/1.66 ~sQ444_spl),
% 8.71/1.66 inference(contradiction_clause,[status(thm)],[f4998])).
% 8.71/1.66 fof(f5000,plain,(
% 8.71/1.66 sdtlseqdt0(xk,xK)),
% 8.71/1.66 inference(forward_demodulation,[status(thm)],[f394,f2162])).
% 8.71/1.66 fof(f5148,definition,(
% 8.71/1.66 sQ493_spl <=> (isFinite0(slbdtrb0(xk)))),
% 8.71/1.66 introduced(definition,[new_symbols(definition,[sQ493_spl])],[split_symbol_definition])).
% 8.71/1.66 fof(f5150,plain,(
% 8.71/1.66 ~isFinite0(slbdtrb0(xk))|sQ493_spl),
% 8.71/1.66 inference(component_clause,[status(thm)],[f5148])).
% 8.71/1.66 fof(f5156,plain,(
% 8.71/1.66 $false|sQ493_spl),
% 8.71/1.66 inference(forward_subsumption_resolution,[status(thm)],[f5150,f2927])).
% 8.71/1.66 fof(f5157,plain,(
% 8.71/1.66 sQ493_spl),
% 8.71/1.66 inference(contradiction_clause,[status(thm)],[f5156])).
% 8.71/1.66 fof(f5166,definition,(
% 8.71/1.66 sQ496_spl <=> (isFinite0(slbdtrb0(xm)))),
% 8.71/1.66 introduced(definition,[new_symbols(definition,[sQ496_spl])],[split_symbol_definition])).
% 8.71/1.66 fof(f5168,plain,(
% 8.71/1.66 ~isFinite0(slbdtrb0(xm))|sQ496_spl),
% 8.71/1.66 inference(component_clause,[status(thm)],[f5166])).
% 8.71/1.66 fof(f5174,plain,(
% 8.71/1.66 $false|sQ496_spl),
% 8.71/1.66 inference(forward_subsumption_resolution,[status(thm)],[f5168,f2929])).
% 8.71/1.66 fof(f5175,plain,(
% 8.71/1.66 sQ496_spl),
% 8.71/1.66 inference(contradiction_clause,[status(thm)],[f5174])).
% 8.71/1.66 fof(f5184,definition,(
% 8.71/1.66 sQ499_spl <=> (isFinite0(slbdtrb0(xK)))),
% 8.71/1.66 introduced(definition,[new_symbols(definition,[sQ499_spl])],[split_symbol_definition])).
% 8.71/1.66 fof(f5186,plain,(
% 8.71/1.66 ~isFinite0(slbdtrb0(xK))|sQ499_spl),
% 8.71/1.66 inference(component_clause,[status(thm)],[f5184])).
% 8.71/1.66 fof(f5192,plain,(
% 8.71/1.66 $false|sQ499_spl),
% 8.71/1.66 inference(forward_subsumption_resolution,[status(thm)],[f5186,f2930])).
% 8.71/1.66 fof(f5193,plain,(
% 8.71/1.66 sQ499_spl),
% 8.71/1.66 inference(contradiction_clause,[status(thm)],[f5192])).
% 8.71/1.66 fof(f5439,definition,(
% 8.71/1.66 sQ556_spl <=> (aElementOf0(sK8_skl(slcrc0,xn),slcrc0))),
% 8.71/1.66 introduced(definition,[new_symbols(definition,[sQ556_spl])],[split_symbol_definition])).
% 8.71/1.66 fof(f5440,plain,(
% 8.71/1.66 aElementOf0(sK8_skl(slcrc0,xn),slcrc0)|~sQ556_spl),
% 8.71/1.66 inference(component_clause,[status(thm)],[f5439])).
% 8.71/1.66 fof(f5486,plain,(
% 8.71/1.66 ~isCountable0(xS)|sQ411_spl),
% 8.71/1.66 inference(forward_demodulation,[status(thm)],[f398,f4297])).
% 8.71/1.66 fof(f5487,plain,(
% 8.71/1.66 $false|sQ411_spl),
% 8.71/1.66 inference(forward_subsumption_resolution,[status(thm)],[f5486,f381])).
% 8.71/1.66 fof(f5488,plain,(
% 8.71/1.66 sQ411_spl),
% 8.71/1.66 inference(contradiction_clause,[status(thm)],[f5487])).
% 8.71/1.66 fof(f5489,plain,(
% 8.71/1.66 $false|~sQ556_spl),
% 8.71/1.66 inference(forward_subsumption_resolution,[status(thm)],[f5440,f485])).
% 8.71/1.66 fof(f5490,plain,(
% 8.71/1.66 ~sQ556_spl),
% 8.71/1.66 inference(contradiction_clause,[status(thm)],[f5489])).
% 8.71/1.66 fof(f5934,definition,(
% 8.71/1.66 sQ608_spl <=> (aFunction0(xc))),
% 8.71/1.66 introduced(definition,[new_symbols(definition,[sQ608_spl])],[split_symbol_definition])).
% 8.71/1.66 fof(f5936,plain,(
% 8.71/1.66 ~aFunction0(xc)|sQ608_spl),
% 8.71/1.66 inference(component_clause,[status(thm)],[f5934])).
% 8.71/1.66 fof(f5965,plain,(
% 8.71/1.66 $false|sQ608_spl),
% 8.71/1.66 inference(forward_subsumption_resolution,[status(thm)],[f5936,f382])).
% 8.71/1.66 fof(f5966,plain,(
% 8.71/1.66 sQ608_spl),
% 8.71/1.66 inference(contradiction_clause,[status(thm)],[f5965])).
% 8.71/1.66 fof(f6053,definition,(
% 8.71/1.66 sQ620_spl <=> (aFunction0(xN))),
% 8.71/1.66 introduced(definition,[new_symbols(definition,[sQ620_spl])],[split_symbol_definition])).
% 8.71/1.66 fof(f6055,plain,(
% 8.71/1.66 ~aFunction0(xN)|sQ620_spl),
% 8.71/1.66 inference(component_clause,[status(thm)],[f6053])).
% 8.71/1.66 fof(f6099,plain,(
% 8.71/1.66 $false|sQ620_spl),
% 8.71/1.66 inference(forward_subsumption_resolution,[status(thm)],[f6055,f396])).
% 8.71/1.66 fof(f6100,plain,(
% 8.71/1.66 sQ620_spl),
% 8.71/1.66 inference(contradiction_clause,[status(thm)],[f6099])).
% 8.71/1.66 fof(f6133,plain,(
% 8.71/1.66 $false|~sQ448_spl),
% 8.71/1.66 inference(forward_subsumption_resolution,[status(thm)],[f4701,f1396])).
% 8.71/1.66 fof(f6134,plain,(
% 8.71/1.66 ~sQ448_spl),
% 8.71/1.66 inference(contradiction_clause,[status(thm)],[f6133])).
% 8.71/1.66 fof(f6179,plain,(
% 8.71/1.66 $false|~sQ359_spl),
% 8.71/1.66 inference(backward_subsumption_resolution,[status(thm)],[f377,f4614])).
% 8.71/1.66 fof(f6196,plain,(
% 8.71/1.66 ~sQ359_spl),
% 8.71/1.66 inference(contradiction_clause,[status(thm)],[f6179])).
% 8.71/1.66 fof(f6352,definition,(
% 8.71/1.66 sQ643_spl <=> (aFunction0(xe))),
% 8.71/1.66 introduced(definition,[new_symbols(definition,[sQ643_spl])],[split_symbol_definition])).
% 8.71/1.66 fof(f6354,plain,(
% 8.71/1.66 ~aFunction0(xe)|sQ643_spl),
% 8.71/1.66 inference(component_clause,[status(thm)],[f6352])).
% 8.71/1.66 fof(f6398,plain,(
% 8.71/1.66 $false|sQ643_spl),
% 8.71/1.66 inference(forward_subsumption_resolution,[status(thm)],[f6354,f431])).
% 8.71/1.66 fof(f6399,plain,(
% 8.71/1.66 sQ643_spl),
% 8.71/1.66 inference(contradiction_clause,[status(thm)],[f6398])).
% 8.71/1.66 fof(f6425,definition,(
% 8.71/1.66 sQ655_spl <=> (aFunction0(xC))),
% 8.71/1.66 introduced(definition,[new_symbols(definition,[sQ655_spl])],[split_symbol_definition])).
% 8.71/1.66 fof(f6427,plain,(
% 8.71/1.66 ~aFunction0(xC)|sQ655_spl),
% 8.71/1.66 inference(component_clause,[status(thm)],[f6425])).
% 8.71/1.66 fof(f6471,plain,(
% 8.71/1.66 $false|sQ655_spl),
% 8.71/1.66 inference(forward_subsumption_resolution,[status(thm)],[f6427,f411])).
% 8.71/1.66 fof(f6472,plain,(
% 8.71/1.66 sQ655_spl),
% 8.71/1.66 inference(contradiction_clause,[status(thm)],[f6471])).
% 8.71/1.66 fof(f6493,definition,(
% 8.71/1.66 sQ668_spl <=> (isCountable0(xS))),
% 8.71/1.66 introduced(definition,[new_symbols(definition,[sQ668_spl])],[split_symbol_definition])).
% 8.71/1.66 fof(f6495,plain,(
% 8.71/1.66 ~isCountable0(xS)|sQ668_spl),
% 8.71/1.66 inference(component_clause,[status(thm)],[f6493])).
% 8.71/1.66 fof(f6501,plain,(
% 8.71/1.66 $false|sQ668_spl),
% 8.71/1.66 inference(forward_subsumption_resolution,[status(thm)],[f6495,f381])).
% 8.71/1.66 fof(f6502,plain,(
% 8.71/1.66 sQ668_spl),
% 8.71/1.66 inference(contradiction_clause,[status(thm)],[f6501])).
% 8.71/1.66 fof(f6997,plain,(
% 8.71/1.66 $false|sQ271_spl),
% 8.71/1.66 inference(forward_subsumption_resolution,[status(thm)],[f2880,f198])).
% 8.71/1.66 fof(f6998,plain,(
% 8.71/1.66 sQ271_spl),
% 8.71/1.66 inference(contradiction_clause,[status(thm)],[f6997])).
% 8.71/1.66 fof(f7082,plain,(
% 8.71/1.66 ~aElementOf0(xm,szNzAzT0)|~aElementOf0(szszuzczcdt0(xn),szNzAzT0)|~sdtlseqdt0(szszuzczcdt0(xn),xm)),
% 8.71/1.66 inference(resolution,[status(thm)],[f475,f405])).
% 8.71/1.66 fof(f7083,definition,(
% 8.71/1.66 sQ719_spl <=> (sdtlseqdt0(szszuzczcdt0(xn),xm))),
% 8.71/1.66 introduced(definition,[new_symbols(definition,[sQ719_spl])],[split_symbol_definition])).
% 8.71/1.66 fof(f7085,plain,(
% 8.71/1.66 ~sdtlseqdt0(szszuzczcdt0(xn),xm)|sQ719_spl),
% 8.71/1.66 inference(component_clause,[status(thm)],[f7083])).
% 8.71/1.66 fof(f7086,plain,(
% 8.71/1.66 ~sQ126_spl|~sQ184_spl|~sQ719_spl),
% 8.71/1.66 inference(split_clause,[status(thm)],[f7082,f1641,f2072,f7083])).
% 8.71/1.66 fof(f7087,plain,(
% 8.71/1.66 ~aElementOf0(xn,szNzAzT0)|~aElementOf0(xm,szNzAzT0)|~sdtlseqdt0(xm,xn)),
% 8.71/1.66 inference(resolution,[status(thm)],[f476,f405])).
% 8.71/1.66 fof(f7088,definition,(
% 8.71/1.66 sQ720_spl <=> (sdtlseqdt0(xm,xn))),
% 8.71/1.66 introduced(definition,[new_symbols(definition,[sQ720_spl])],[split_symbol_definition])).
% 8.71/1.66 fof(f7091,plain,(
% 8.71/1.66 ~sQ135_spl|~sQ126_spl|~sQ720_spl),
% 8.71/1.66 inference(split_clause,[status(thm)],[f7087,f1707,f1641,f7088])).
% 8.71/1.66 fof(f7561,definition,(
% 8.71/1.66 sQ787_spl <=> (aElementOf0(sK0_skl(slcrc0),slcrc0))),
% 8.71/1.66 introduced(definition,[new_symbols(definition,[sQ787_spl])],[split_symbol_definition])).
% 8.71/1.66 fof(f7562,plain,(
% 8.71/1.66 aElementOf0(sK0_skl(slcrc0),slcrc0)|~sQ787_spl),
% 8.71/1.66 inference(component_clause,[status(thm)],[f7561])).
% 8.71/1.66 fof(f7621,plain,(
% 8.71/1.66 $false|~sQ787_spl),
% 8.71/1.66 inference(forward_subsumption_resolution,[status(thm)],[f7562,f485])).
% 8.71/1.66 fof(f7622,plain,(
% 8.71/1.66 ~sQ787_spl),
% 8.71/1.66 inference(contradiction_clause,[status(thm)],[f7621])).
% 8.71/1.66 fof(f7687,plain,(
% 8.71/1.66 sdtlseqdt0(sz00,xn)),
% 8.71/1.66 inference(resolution,[status(thm)],[f214,f466])).
% 8.71/1.66 fof(f7830,definition,(
% 8.71/1.66 sQ814_spl <=> (sbrdtbr0(slcrc0)=sz00)),
% 8.71/1.66 introduced(definition,[new_symbols(definition,[sQ814_spl])],[split_symbol_definition])).
% 8.71/1.66 fof(f7832,plain,(
% 8.71/1.66 ~sbrdtbr0(slcrc0)=sz00|sQ814_spl),
% 8.71/1.66 inference(component_clause,[status(thm)],[f7830])).
% 8.71/1.66 fof(f7881,plain,(
% 8.71/1.66 $false|sQ409_spl),
% 8.71/1.66 inference(forward_subsumption_resolution,[status(thm)],[f7687,f4290])).
% 8.71/1.66 fof(f7882,plain,(
% 8.71/1.66 sQ409_spl),
% 8.71/1.66 inference(contradiction_clause,[status(thm)],[f7881])).
% 8.71/1.66 fof(f8324,definition,(
% 8.71/1.66 sQ883_spl <=> (aElementOf0(sK8_skl(slcrc0,xx),slcrc0))),
% 8.71/1.66 introduced(definition,[new_symbols(definition,[sQ883_spl])],[split_symbol_definition])).
% 8.71/1.66 fof(f8325,plain,(
% 8.71/1.66 aElementOf0(sK8_skl(slcrc0,xx),slcrc0)|~sQ883_spl),
% 8.71/1.66 inference(component_clause,[status(thm)],[f8324])).
% 8.71/1.66 fof(f8373,plain,(
% 8.71/1.66 $false|~sQ883_spl),
% 8.71/1.66 inference(forward_subsumption_resolution,[status(thm)],[f8325,f485])).
% 8.71/1.66 fof(f8374,plain,(
% 8.71/1.66 ~sQ883_spl),
% 8.71/1.66 inference(contradiction_clause,[status(thm)],[f8373])).
% 8.71/1.66 fof(f8434,plain,(
% 8.71/1.66 $false|sQ814_spl),
% 8.71/1.66 inference(forward_subsumption_resolution,[status(thm)],[f1668,f7832])).
% 8.71/1.66 fof(f8435,plain,(
% 8.71/1.66 sQ814_spl),
% 8.71/1.66 inference(contradiction_clause,[status(thm)],[f8434])).
% 8.71/1.66 fof(f9623,definition,(
% 8.71/1.66 sQ1034_spl <=> (aElementOf0(szmzizndt0(slcrc0),slcrc0))),
% 8.71/1.66 introduced(definition,[new_symbols(definition,[sQ1034_spl])],[split_symbol_definition])).
% 8.71/1.66 fof(f9624,plain,(
% 8.71/1.66 aElementOf0(szmzizndt0(slcrc0),slcrc0)|~sQ1034_spl),
% 8.71/1.66 inference(component_clause,[status(thm)],[f9623])).
% 8.71/1.66 fof(f9641,plain,(
% 8.71/1.66 $false|~sQ1034_spl),
% 8.71/1.66 inference(forward_subsumption_resolution,[status(thm)],[f9624,f485])).
% 8.71/1.66 fof(f9642,plain,(
% 8.71/1.66 ~sQ1034_spl),
% 8.71/1.66 inference(contradiction_clause,[status(thm)],[f9641])).
% 8.71/1.66 fof(f10452,definition,(
% 8.71/1.66 sQ1140_spl <=> (sdtlseqdt0(sz00,szszuzczcdt0(sz00)))),
% 8.71/1.66 introduced(definition,[new_symbols(definition,[sQ1140_spl])],[split_symbol_definition])).
% 8.71/1.66 fof(f10454,plain,(
% 8.71/1.66 ~sdtlseqdt0(sz00,szszuzczcdt0(sz00))|sQ1140_spl),
% 8.71/1.66 inference(component_clause,[status(thm)],[f10452])).
% 8.71/1.66 fof(f10459,definition,(
% 8.71/1.66 sQ1142_spl <=> (sdtlseqdt0(xk,szszuzczcdt0(xk)))),
% 8.71/1.66 introduced(definition,[new_symbols(definition,[sQ1142_spl])],[split_symbol_definition])).
% 8.71/1.66 fof(f10461,plain,(
% 8.71/1.66 ~sdtlseqdt0(xk,szszuzczcdt0(xk))|sQ1142_spl),
% 8.71/1.66 inference(component_clause,[status(thm)],[f10459])).
% 8.71/1.66 fof(f10481,plain,(
% 8.71/1.66 ~sdtlseqdt0(xk,xK)|sQ1142_spl),
% 8.71/1.66 inference(forward_demodulation,[status(thm)],[f394,f10461])).
% 8.71/1.66 fof(f10482,plain,(
% 8.71/1.66 $false|sQ1142_spl),
% 8.71/1.66 inference(forward_subsumption_resolution,[status(thm)],[f10481,f5000])).
% 8.71/1.66 fof(f10483,plain,(
% 8.71/1.66 sQ1142_spl),
% 8.71/1.66 inference(contradiction_clause,[status(thm)],[f10482])).
% 8.71/1.66 fof(f10484,plain,(
% 8.71/1.66 $false|sQ1140_spl),
% 8.71/1.66 inference(forward_subsumption_resolution,[status(thm)],[f10454,f1913])).
% 8.71/1.66 fof(f10485,plain,(
% 8.71/1.66 sQ1140_spl),
% 8.71/1.66 inference(contradiction_clause,[status(thm)],[f10484])).
% 8.71/1.66 fof(f11120,definition,(
% 8.71/1.66 sQ1223_spl <=> (aElementOf0(xx,xO))),
% 8.71/1.66 introduced(definition,[new_symbols(definition,[sQ1223_spl])],[split_symbol_definition])).
% 8.71/1.66 fof(f11122,plain,(
% 8.71/1.66 ~aElementOf0(xx,xO)|sQ1223_spl),
% 8.71/1.66 inference(component_clause,[status(thm)],[f11120])).
% 8.71/1.66 fof(f11127,plain,(
% 8.71/1.66 $false|sQ1223_spl),
% 8.71/1.66 inference(forward_subsumption_resolution,[status(thm)],[f11122,f471])).
% 8.71/1.66 fof(f11128,plain,(
% 8.71/1.66 sQ1223_spl),
% 8.71/1.66 inference(contradiction_clause,[status(thm)],[f11127])).
% 8.71/1.66 fof(f11353,definition,(
% 8.71/1.66 sQ1255_spl <=> (aElementOf0(xp,xO))),
% 8.71/1.66 introduced(definition,[new_symbols(definition,[sQ1255_spl])],[split_symbol_definition])).
% 8.71/1.66 fof(f11355,plain,(
% 8.71/1.66 ~aElementOf0(xp,xO)|sQ1255_spl),
% 8.71/1.66 inference(component_clause,[status(thm)],[f11353])).
% 8.71/1.66 fof(f11357,plain,(
% 8.71/1.66 $false|sQ1255_spl),
% 8.71/1.66 inference(forward_subsumption_resolution,[status(thm)],[f11355,f460])).
% 8.71/1.67 fof(f11358,plain,(
% 8.71/1.67 sQ1255_spl),
% 8.71/1.67 inference(contradiction_clause,[status(thm)],[f11357])).
% 8.71/1.67 fof(f11710,plain,(
% 8.71/1.67 ~aElementOf0(xm,szNzAzT0)|~aElementOf0(xn,szNzAzT0)|sdtlseqdt0(xm,xn)|sQ719_spl),
% 8.71/1.67 inference(resolution,[status(thm)],[f7085,f230])).
% 8.71/1.67 fof(f11712,plain,(
% 8.71/1.67 ~sQ126_spl|~sQ135_spl|sQ720_spl|sQ719_spl),
% 8.71/1.67 inference(split_clause,[status(thm)],[f11710,f1641,f1707,f7088,f7083])).
% 8.71/1.67 fof(f11717,plain,(
% 8.71/1.67 $false),
% 8.71/1.67 inference(sat_refutation,[status(thm)],[f1653,f1786,f2867,f2977,f3053,f3088,f3123,f3409,f3429,f3463,f3483,f3520,f3864,f4002,f4099,f4203,f4304,f4387,f4430,f4432,f4616,f4619,f4624,f4626,f4631,f4635,f4637,f4643,f4645,f4999,f5157,f5175,f5193,f5488,f5490,f5966,f6100,f6134,f6196,f6399,f6472,f6502,f6998,f7086,f7091,f7622,f7882,f8374,f8435,f9642,f10483,f10485,f11128,f11358,f11712])).
% 8.71/1.67 % SZS output end CNFRefutation for theBenchmark.p
% 8.71/1.70 % Elapsed time: 1.313201 seconds
% 8.71/1.70 % CPU time: 9.985708 seconds
% 8.71/1.70 % Total memory used: 203.878 MB
% 8.71/1.70 % Net memory used: 197.899 MB
%------------------------------------------------------------------------------