%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM586+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 : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 01:43:17 PM UTC 2026
% Result : Theorem 204.31s 26.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM586+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.45 % Computer : n003.cluster.edu
% 0.18/0.45 % Model : x86_64 x86_64
% 0.18/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.45 % Memory : 8046.5625MB
% 0.18/0.45 % OS : Linux 6.8.0-71-generic
% 0.18/0.45 % CPULimit : 300
% 0.18/0.45 % WCLimit : 300
% 0.18/0.45 % DateTime : Mon Sep 21 02:44:00 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.50 % Drodi V4.1.1
% 204.31/26.40 % Refutation found
% 204.31/26.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 204.31/26.40 % SZS output start CNFRefutation for theBenchmark
% 204.31/26.40 fof(f5,definition,(
% 204.31/26.40 (! [W0] :( W0 = slcrc0<=> ( aSet0(W0)& ~ (? [W1] : aElementOf0(W1,W0) )) ) )),
% 204.31/26.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 204.31/26.40 fof(f9,axiom,(
% 204.31/26.40 (! [W0] :( ( aSet0(W0)& isCountable0(W0) )=> W0 != slcrc0 ) )),
% 204.31/26.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 204.31/26.40 fof(f12,axiom,(
% 204.31/26.40 (! [W0] :( aSet0(W0)=> aSubsetOf0(W0,W0) ) )),
% 204.31/26.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 204.31/26.40 fof(f15,definition,(
% 204.31/26.40 (! [W0,W1] :( ( aSet0(W0)& aElement0(W1) )=> (! [W2] :( W2 = sdtpldt0(W0,W1)<=> ( aSet0(W2)& (! [W3] :( aElementOf0(W3,W2)<=> ( aElement0(W3)& ( aElementOf0(W3,W0)| W3 = W1 ) ) ) )) ) )) )),
% 204.31/26.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 204.31/26.40 fof(f16,definition,(
% 204.31/26.40 (! [W0,W1] :( ( aSet0(W0)& aElement0(W1) )=> (! [W2] :( W2 = sdtmndt0(W0,W1)<=> ( aSet0(W2)& (! [W3] :( aElementOf0(W3,W2)<=> ( aElement0(W3)& aElementOf0(W3,W0)& W3 != W1 ) ) )) ) )) )),
% 204.31/26.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 204.31/26.40 fof(f23,axiom,(
% 204.31/26.40 ( aSet0(szNzAzT0)& isCountable0(szNzAzT0) ) ),
% 204.31/26.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 204.31/26.40 fof(f25,axiom,(
% 204.31/26.40 (! [W0] :( aElementOf0(W0,szNzAzT0)=> ( aElementOf0(szszuzczcdt0(W0),szNzAzT0)& szszuzczcdt0(W0) != sz00 ) ) )),
% 204.31/26.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 204.31/26.40 fof(f40,axiom,(
% 204.31/26.40 (! [W0] :( aSet0(W0)=> aElement0(sbrdtbr0(W0)) ) )),
% 204.31/26.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 204.31/26.40 fof(f42,axiom,(
% 204.31/26.40 (! [W0] :( aSet0(W0)=> ( sbrdtbr0(W0) = sz00<=> W0 = slcrc0 ) ) )),
% 204.31/26.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 204.31/26.40 fof(f56,axiom,(
% 204.31/26.40 (! [W0] :( aElementOf0(W0,szNzAzT0)=> sbrdtbr0(slbdtrb0(W0)) = W0 ) )),
% 204.31/26.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 204.31/26.40 fof(f57,definition,(
% 204.31/26.40 (! [W0,W1] :( ( aSet0(W0)& aElementOf0(W1,szNzAzT0) )=> (! [W2] :( W2 = slbdtsldtrb0(W0,W1)<=> ( aSet0(W2)& (! [W3] :( aElementOf0(W3,W2)<=> ( aSubsetOf0(W3,W0)& sbrdtbr0(W3) = W1 ) ) )) ) )) )),
% 204.31/26.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 204.31/26.40 fof(f64,axiom,(
% 204.31/26.40 (! [W0] :( aFunction0(W0)=> aSet0(szDzozmdt0(W0)) ) )),
% 204.31/26.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 204.31/26.40 fof(f68,definition,(
% 204.31/26.40 (! [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 ) )) )) ) )) )) )),
% 204.31/26.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 204.31/26.40 fof(f73,hypothesis,(
% 204.31/26.40 ( aSet0(xT)& isFinite0(xT) ) ),
% 204.31/26.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 204.31/26.40 fof(f74,hypothesis,(
% 204.31/26.40 aElementOf0(xK,szNzAzT0) ),
% 204.31/26.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 204.31/26.40 fof(f75,hypothesis,(
% 204.31/26.40 ( aSubsetOf0(xS,szNzAzT0)& isCountable0(xS) ) ),
% 204.31/26.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 204.31/26.40 fof(f78,hypothesis,(
% 204.31/26.40 xK != sz00 ),
% 204.31/26.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 204.31/26.40 fof(f80,hypothesis,(
% 204.31/26.40 ( aElementOf0(xk,szNzAzT0)& szszuzczcdt0(xk) = xK ) ),
% 204.31/26.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 204.31/26.40 fof(f81,hypothesis,(
% 204.31/26.40 ( 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))) ) ) ) )) ),
% 204.31/26.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 204.31/26.40 fof(f82,hypothesis,(
% 204.31/26.40 (! [W0] :( aElementOf0(W0,szNzAzT0)=> ( aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0)& isCountable0(sdtlpdtrp0(xN,W0)) ) ) )),
% 204.31/26.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 204.31/26.40 fof(f86,hypothesis,(
% 204.31/26.40 ( 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)))) ) )) ) )) ),
% 204.31/26.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 204.31/26.40 fof(f87,hypothesis,(
% 204.31/26.40 aElementOf0(xi,szNzAzT0) ),
% 204.31/26.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 204.31/26.40 fof(f88,hypothesis,(
% 204.31/26.40 aElementOf0(xx,sdtlcdtrc0(sdtlpdtrp0(xC,xi),szDzozmdt0(sdtlpdtrp0(xC,xi)))) ),
% 204.31/26.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 204.31/26.40 fof(f89,conjecture,(
% 204.31/26.40 (? [W0] :( aElementOf0(W0,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))),xk))& sdtlpdtrp0(sdtlpdtrp0(xC,xi),W0) = xx ) )),
% 204.31/26.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 204.31/26.40 fof(f90,negated_conjecture,(
% 204.31/26.40 ~((? [W0] :( aElementOf0(W0,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))),xk))& sdtlpdtrp0(sdtlpdtrp0(xC,xi),W0) = xx ) ))),
% 204.31/26.40 inference(negated_conjecture,[status(cth)],[f89])).
% 204.31/26.40 fof(f101,plain,(
% 204.31/26.40 ![W0]: (W0=slcrc0<=>(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0))))),
% 204.31/26.40 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 204.31/26.40 fof(f102,plain,(
% 204.31/26.40 ![W0]: ((~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0))))&(W0=slcrc0|(~aSet0(W0)|(?[W1]: aElementOf0(W1,W0)))))),
% 204.31/26.40 inference(NNF_transformation,[status(thm)],[f101])).
% 204.31/26.40 fof(f103,plain,(
% 204.31/26.40 (![W0]: (~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0)))))&(![W0]: (W0=slcrc0|(~aSet0(W0)|(?[W1]: aElementOf0(W1,W0)))))),
% 204.31/26.40 inference(miniscoping,[status(thm)],[f102])).
% 204.31/26.40 fof(f104,plain,(
% 204.31/26.40 (![W0]: (~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0)))))&(![W0]: (W0=slcrc0|(~aSet0(W0)|aElementOf0(sK0_skl(W0),W0))))),
% 204.31/26.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(W1,sK0_skl(W0))],[f103])).
% 204.31/26.40 fof(f105,plain,(
% 204.31/26.40 ![X0]: (~X0=slcrc0|aSet0(X0))),
% 204.31/26.40 inference(cnf_transformation,[status(thm)],[f104])).
% 204.31/26.40 fof(f106,plain,(
% 204.31/26.40 ![X0,X1]: (~X0=slcrc0|~aElementOf0(X1,X0))),
% 204.31/26.40 inference(cnf_transformation,[status(thm)],[f104])).
% 204.31/26.40 fof(f113,plain,(
% 204.31/26.40 ![W0]: ((~aSet0(W0)|~isCountable0(W0))|~W0=slcrc0)),
% 204.31/26.40 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 204.31/26.40 fof(f114,plain,(
% 204.31/26.40 ![X0]: (~aSet0(X0)|~isCountable0(X0)|~X0=slcrc0)),
% 204.31/26.40 inference(cnf_transformation,[status(thm)],[f113])).
% 204.31/26.40 fof(f125,plain,(
% 204.31/26.40 ![W0]: (~aSet0(W0)|aSubsetOf0(W0,W0))),
% 204.31/26.40 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 204.31/26.40 fof(f126,plain,(
% 204.31/26.40 ![X0]: (~aSet0(X0)|aSubsetOf0(X0,X0))),
% 204.31/26.40 inference(cnf_transformation,[status(thm)],[f125])).
% 204.31/26.40 fof(f131,plain,(
% 204.31/26.40 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|(![W2]: (W2=sdtpldt0(W0,W1)<=>(aSet0(W2)&(![W3]: (aElementOf0(W3,W2)<=>(aElement0(W3)&(aElementOf0(W3,W0)|W3=W1))))))))),
% 204.31/26.40 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 204.31/26.40 fof(f132,plain,(
% 204.31/26.40 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|(![W2]: ((~W2=sdtpldt0(W0,W1)|(aSet0(W2)&(![W3]: ((~aElementOf0(W3,W2)|(aElement0(W3)&(aElementOf0(W3,W0)|W3=W1)))&(aElementOf0(W3,W2)|(~aElement0(W3)|(~aElementOf0(W3,W0)&~W3=W1)))))))&(W2=sdtpldt0(W0,W1)|(~aSet0(W2)|(?[W3]: ((~aElementOf0(W3,W2)|(~aElement0(W3)|(~aElementOf0(W3,W0)&~W3=W1)))&(aElementOf0(W3,W2)|(aElement0(W3)&(aElementOf0(W3,W0)|W3=W1))))))))))),
% 204.31/26.40 inference(NNF_transformation,[status(thm)],[f131])).
% 204.31/26.40 fof(f133,plain,(
% 204.31/26.40 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|((![W2]: (~W2=sdtpldt0(W0,W1)|(aSet0(W2)&((![W3]: (~aElementOf0(W3,W2)|(aElement0(W3)&(aElementOf0(W3,W0)|W3=W1))))&(![W3]: (aElementOf0(W3,W2)|(~aElement0(W3)|(~aElementOf0(W3,W0)&~W3=W1))))))))&(![W2]: (W2=sdtpldt0(W0,W1)|(~aSet0(W2)|(?[W3]: ((~aElementOf0(W3,W2)|(~aElement0(W3)|(~aElementOf0(W3,W0)&~W3=W1)))&(aElementOf0(W3,W2)|(aElement0(W3)&(aElementOf0(W3,W0)|W3=W1))))))))))),
% 204.31/26.40 inference(miniscoping,[status(thm)],[f132])).
% 204.31/26.40 fof(f134,plain,(
% 204.31/26.40 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|((![W2]: (~W2=sdtpldt0(W0,W1)|(aSet0(W2)&((![W3]: (~aElementOf0(W3,W2)|(aElement0(W3)&(aElementOf0(W3,W0)|W3=W1))))&(![W3]: (aElementOf0(W3,W2)|(~aElement0(W3)|(~aElementOf0(W3,W0)&~W3=W1))))))))&(![W2]: (W2=sdtpldt0(W0,W1)|(~aSet0(W2)|((~aElementOf0(sK2_skl(W2,W1,W0),W2)|(~aElement0(sK2_skl(W2,W1,W0))|(~aElementOf0(sK2_skl(W2,W1,W0),W0)&~sK2_skl(W2,W1,W0)=W1)))&(aElementOf0(sK2_skl(W2,W1,W0),W2)|(aElement0(sK2_skl(W2,W1,W0))&(aElementOf0(sK2_skl(W2,W1,W0),W0)|sK2_skl(W2,W1,W0)=W1)))))))))),
% 204.31/26.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(W3,sK2_skl(W2,W1,W0))],[f133])).
% 204.31/26.40 fof(f135,plain,(
% 204.31/26.40 ![X0,X1,X2]: (~aSet0(X0)|~aElement0(X1)|~X2=sdtpldt0(X0,X1)|aSet0(X2))),
% 204.31/26.40 inference(cnf_transformation,[status(thm)],[f134])).
% 204.31/26.40 fof(f144,plain,(
% 204.31/26.40 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|(![W2]: (W2=sdtmndt0(W0,W1)<=>(aSet0(W2)&(![W3]: (aElementOf0(W3,W2)<=>((aElement0(W3)&aElementOf0(W3,W0))&~W3=W1)))))))),
% 204.31/26.40 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 204.31/26.40 fof(f145,definition,(
% 204.31/26.40 ![W0,W1,W3]: (sP0_prd(W3,W1,W0)<=>((aElement0(W3)&aElementOf0(W3,W0))&~W3=W1))),
% 204.31/26.40 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 204.31/26.40 fof(f167,plain,(
% 204.31/26.40 aSet0(szNzAzT0)),
% 204.31/26.40 inference(cnf_transformation,[status(thm)],[f23])).
% 204.31/26.40 fof(f168,plain,(
% 204.31/26.40 isCountable0(szNzAzT0)),
% 204.31/26.40 inference(cnf_transformation,[status(thm)],[f23])).
% 204.31/26.40 fof(f170,plain,(
% 204.31/26.40 ![W0]: (~aElementOf0(W0,szNzAzT0)|(aElementOf0(szszuzczcdt0(W0),szNzAzT0)&~szszuzczcdt0(W0)=sz00))),
% 204.31/26.40 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 204.31/26.40 fof(f171,plain,(
% 204.31/26.40 ![X0]: (~aElementOf0(X0,szNzAzT0)|aElementOf0(szszuzczcdt0(X0),szNzAzT0))),
% 204.31/26.40 inference(cnf_transformation,[status(thm)],[f170])).
% 204.31/26.40 fof(f205,plain,(
% 204.31/26.40 ![W0]: (~aSet0(W0)|aElement0(sbrdtbr0(W0)))),
% 204.31/26.40 inference(pre_NNF_transformation,[status(thm)],[f40])).
% 204.31/26.40 fof(f206,plain,(
% 204.31/26.40 ![X0]: (~aSet0(X0)|aElement0(sbrdtbr0(X0)))),
% 204.31/26.40 inference(cnf_transformation,[status(thm)],[f205])).
% 204.31/26.40 fof(f211,plain,(
% 204.31/26.40 ![W0]: (~aSet0(W0)|(sbrdtbr0(W0)=sz00<=>W0=slcrc0))),
% 204.31/26.40 inference(pre_NNF_transformation,[status(thm)],[f42])).
% 204.31/26.40 fof(f212,plain,(
% 204.31/26.40 ![W0]: (~aSet0(W0)|((~sbrdtbr0(W0)=sz00|W0=slcrc0)&(sbrdtbr0(W0)=sz00|~W0=slcrc0)))),
% 204.31/26.40 inference(NNF_transformation,[status(thm)],[f211])).
% 204.31/26.40 fof(f214,plain,(
% 204.31/26.40 ![X0]: (~aSet0(X0)|sbrdtbr0(X0)=sz00|~X0=slcrc0)),
% 204.31/26.40 inference(cnf_transformation,[status(thm)],[f212])).
% 204.31/26.40 fof(f270,plain,(
% 204.31/26.40 ![W0]: (~aElementOf0(W0,szNzAzT0)|sbrdtbr0(slbdtrb0(W0))=W0)),
% 204.31/26.40 inference(pre_NNF_transformation,[status(thm)],[f56])).
% 204.31/26.40 fof(f271,plain,(
% 204.31/26.40 ![X0]: (~aElementOf0(X0,szNzAzT0)|sbrdtbr0(slbdtrb0(X0))=X0)),
% 204.31/26.40 inference(cnf_transformation,[status(thm)],[f270])).
% 204.31/26.40 fof(f272,plain,(
% 204.31/26.40 ![W0,W1]: ((~aSet0(W0)|~aElementOf0(W1,szNzAzT0))|(![W2]: (W2=slbdtsldtrb0(W0,W1)<=>(aSet0(W2)&(![W3]: (aElementOf0(W3,W2)<=>(aSubsetOf0(W3,W0)&sbrdtbr0(W3)=W1)))))))),
% 204.31/26.40 inference(pre_NNF_transformation,[status(thm)],[f57])).
% 204.31/26.40 fof(f273,plain,(
% 204.31/26.40 ![W0,W1]: ((~aSet0(W0)|~aElementOf0(W1,szNzAzT0))|(![W2]: ((~W2=slbdtsldtrb0(W0,W1)|(aSet0(W2)&(![W3]: ((~aElementOf0(W3,W2)|(aSubsetOf0(W3,W0)&sbrdtbr0(W3)=W1))&(aElementOf0(W3,W2)|(~aSubsetOf0(W3,W0)|~sbrdtbr0(W3)=W1))))))&(W2=slbdtsldtrb0(W0,W1)|(~aSet0(W2)|(?[W3]: ((~aElementOf0(W3,W2)|(~aSubsetOf0(W3,W0)|~sbrdtbr0(W3)=W1))&(aElementOf0(W3,W2)|(aSubsetOf0(W3,W0)&sbrdtbr0(W3)=W1)))))))))),
% 204.31/26.40 inference(NNF_transformation,[status(thm)],[f272])).
% 204.31/26.40 fof(f274,plain,(
% 204.31/26.40 ![W0,W1]: ((~aSet0(W0)|~aElementOf0(W1,szNzAzT0))|((![W2]: (~W2=slbdtsldtrb0(W0,W1)|(aSet0(W2)&((![W3]: (~aElementOf0(W3,W2)|(aSubsetOf0(W3,W0)&sbrdtbr0(W3)=W1)))&(![W3]: (aElementOf0(W3,W2)|(~aSubsetOf0(W3,W0)|~sbrdtbr0(W3)=W1)))))))&(![W2]: (W2=slbdtsldtrb0(W0,W1)|(~aSet0(W2)|(?[W3]: ((~aElementOf0(W3,W2)|(~aSubsetOf0(W3,W0)|~sbrdtbr0(W3)=W1))&(aElementOf0(W3,W2)|(aSubsetOf0(W3,W0)&sbrdtbr0(W3)=W1)))))))))),
% 204.31/26.40 inference(miniscoping,[status(thm)],[f273])).
% 204.31/26.40 fof(f275,plain,(
% 204.31/26.40 ![W0,W1]: ((~aSet0(W0)|~aElementOf0(W1,szNzAzT0))|((![W2]: (~W2=slbdtsldtrb0(W0,W1)|(aSet0(W2)&((![W3]: (~aElementOf0(W3,W2)|(aSubsetOf0(W3,W0)&sbrdtbr0(W3)=W1)))&(![W3]: (aElementOf0(W3,W2)|(~aSubsetOf0(W3,W0)|~sbrdtbr0(W3)=W1)))))))&(![W2]: (W2=slbdtsldtrb0(W0,W1)|(~aSet0(W2)|((~aElementOf0(sK10_skl(W2,W1,W0),W2)|(~aSubsetOf0(sK10_skl(W2,W1,W0),W0)|~sbrdtbr0(sK10_skl(W2,W1,W0))=W1))&(aElementOf0(sK10_skl(W2,W1,W0),W2)|(aSubsetOf0(sK10_skl(W2,W1,W0),W0)&sbrdtbr0(sK10_skl(W2,W1,W0))=W1))))))))),
% 204.31/26.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(W3,sK10_skl(W2,W1,W0))],[f274])).
% 204.31/26.40 fof(f276,plain,(
% 204.31/26.40 ![X0,X1,X2]: (~aSet0(X0)|~aElementOf0(X1,szNzAzT0)|~X2=slbdtsldtrb0(X0,X1)|aSet0(X2))),
% 204.31/26.40 inference(cnf_transformation,[status(thm)],[f275])).
% 204.31/26.40 fof(f299,plain,(
% 204.31/26.40 ![W0]: (~aFunction0(W0)|aSet0(szDzozmdt0(W0)))),
% 204.31/26.40 inference(pre_NNF_transformation,[status(thm)],[f64])).
% 204.31/26.40 fof(f300,plain,(
% 204.31/26.40 ![X0]: (~aFunction0(X0)|aSet0(szDzozmdt0(X0)))),
% 204.31/26.40 inference(cnf_transformation,[status(thm)],[f299])).
% 204.31/26.40 fof(f316,plain,(
% 204.31/26.40 ![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))))))))))),
% 204.31/26.40 inference(pre_NNF_transformation,[status(thm)],[f68])).
% 204.31/26.40 fof(f317,plain,(
% 204.31/26.40 ![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))))))))))))),
% 204.31/26.40 inference(NNF_transformation,[status(thm)],[f316])).
% 204.31/26.40 fof(f318,plain,(
% 204.31/26.40 ![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))))))))))))),
% 204.31/26.40 inference(miniscoping,[status(thm)],[f317])).
% 204.31/26.40 fof(f319,plain,(
% 204.31/26.40 ![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)))))))))))),
% 204.31/26.40 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))],[f318])).
% 204.31/26.40 fof(f321,plain,(
% 204.31/26.40 ![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))),
% 204.31/26.40 inference(cnf_transformation,[status(thm)],[f319])).
% 204.31/26.40 fof(f322,plain,(
% 204.31/26.40 ![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)),
% 204.31/26.40 inference(cnf_transformation,[status(thm)],[f319])).
% 204.31/26.40 fof(f347,plain,(
% 204.31/26.40 aSet0(xT)),
% 204.31/26.40 inference(cnf_transformation,[status(thm)],[f73])).
% 204.31/26.40 fof(f349,plain,(
% 204.31/26.40 aElementOf0(xK,szNzAzT0)),
% 204.31/26.40 inference(cnf_transformation,[status(thm)],[f74])).
% 204.31/26.40 fof(f351,plain,(
% 204.31/26.40 isCountable0(xS)),
% 204.31/26.40 inference(cnf_transformation,[status(thm)],[f75])).
% 204.31/26.40 fof(f361,plain,(
% 204.31/26.40 ~xK=sz00),
% 204.31/26.40 inference(cnf_transformation,[status(thm)],[f78])).
% 204.31/26.40 fof(f363,plain,(
% 204.31/26.40 aElementOf0(xk,szNzAzT0)),
% 204.31/26.40 inference(cnf_transformation,[status(thm)],[f80])).
% 204.31/26.40 fof(f365,plain,(
% 204.31/26.40 ((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)))))))),
% 204.31/26.40 inference(pre_NNF_transformation,[status(thm)],[f81])).
% 204.31/26.40 fof(f367,plain,(
% 204.31/26.40 szDzozmdt0(xN)=szNzAzT0),
% 204.31/26.40 inference(cnf_transformation,[status(thm)],[f365])).
% 204.31/26.40 fof(f371,plain,(
% 204.31/26.40 ![W0]: (~aElementOf0(W0,szNzAzT0)|(aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0)&isCountable0(sdtlpdtrp0(xN,W0))))),
% 204.31/26.40 inference(pre_NNF_transformation,[status(thm)],[f82])).
% 204.31/26.40 fof(f373,plain,(
% 204.31/26.40 ![X0]: (~aElementOf0(X0,szNzAzT0)|isCountable0(sdtlpdtrp0(xN,X0)))),
% 204.31/26.40 inference(cnf_transformation,[status(thm)],[f371])).
% 204.31/26.40 fof(f380,plain,(
% 204.31/26.40 (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)))))))))),
% 204.31/26.40 inference(pre_NNF_transformation,[status(thm)],[f86])).
% 204.31/26.40 fof(f381,plain,(
% 204.31/26.40 aFunction0(xC)),
% 204.31/26.40 inference(cnf_transformation,[status(thm)],[f380])).
% 204.31/26.40 fof(f382,plain,(
% 204.31/26.40 szDzozmdt0(xC)=szNzAzT0),
% 204.31/26.40 inference(cnf_transformation,[status(thm)],[f380])).
% 204.31/26.40 fof(f383,plain,(
% 204.31/26.40 ![X0]: (~aElementOf0(X0,szNzAzT0)|aFunction0(sdtlpdtrp0(xC,X0)))),
% 204.31/26.40 inference(cnf_transformation,[status(thm)],[f380])).
% 204.31/26.40 fof(f384,plain,(
% 204.31/26.40 ![X0]: (~aElementOf0(X0,szNzAzT0)|szDzozmdt0(sdtlpdtrp0(xC,X0))=slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk))),
% 204.31/26.40 inference(cnf_transformation,[status(thm)],[f380])).
% 204.31/26.40 fof(f386,plain,(
% 204.31/26.40 aElementOf0(xi,szNzAzT0)),
% 204.31/26.40 inference(cnf_transformation,[status(thm)],[f87])).
% 204.31/26.40 fof(f387,plain,(
% 204.31/26.40 aElementOf0(xx,sdtlcdtrc0(sdtlpdtrp0(xC,xi),szDzozmdt0(sdtlpdtrp0(xC,xi))))),
% 204.31/26.40 inference(cnf_transformation,[status(thm)],[f88])).
% 204.31/26.40 fof(f388,plain,(
% 204.31/26.40 (![W0]: (~aElementOf0(W0,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))),xk))|~sdtlpdtrp0(sdtlpdtrp0(xC,xi),W0)=xx))),
% 204.31/26.40 inference(pre_NNF_transformation,[status(thm)],[f90])).
% 204.31/26.40 fof(f389,plain,(
% 204.31/26.40 ![X0]: (~aElementOf0(X0,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))),xk))|~sdtlpdtrp0(sdtlpdtrp0(xC,xi),X0)=xx)),
% 204.31/26.40 inference(cnf_transformation,[status(thm)],[f388])).
% 204.31/26.40 fof(f390,plain,(
% 204.31/26.40 ![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)))),
% 204.31/26.40 inference(NNF_transformation,[status(thm)],[f145])).
% 204.31/26.40 fof(f391,plain,(
% 204.31/26.40 (![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)))),
% 204.31/26.40 inference(miniscoping,[status(thm)],[f390])).
% 204.31/26.40 fof(f394,plain,(
% 204.31/26.40 ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|~X0=X1)),
% 204.31/26.40 inference(cnf_transformation,[status(thm)],[f391])).
% 204.31/26.40 fof(f396,plain,(
% 204.31/26.40 aSet0(slcrc0)),
% 204.31/26.40 inference(destructive_equality_resolution,[status(thm)],[f105])).
% 204.31/26.40 fof(f397,plain,(
% 204.31/26.40 ![X0]: (~aElementOf0(X0,slcrc0))),
% 204.31/26.40 inference(destructive_equality_resolution,[status(thm)],[f106])).
% 204.31/26.40 fof(f398,plain,(
% 204.31/26.40 ~aSet0(slcrc0)|~isCountable0(slcrc0)),
% 204.31/26.40 inference(destructive_equality_resolution,[status(thm)],[f114])).
% 204.31/26.40 fof(f399,plain,(
% 204.31/26.40 ![X0,X1]: (~aSet0(X0)|~aElement0(X1)|aSet0(sdtpldt0(X0,X1)))),
% 204.31/26.40 inference(destructive_equality_resolution,[status(thm)],[f135])).
% 204.31/26.40 fof(f408,plain,(
% 204.31/26.40 ~aSet0(slcrc0)|sbrdtbr0(slcrc0)=sz00),
% 204.31/26.40 inference(destructive_equality_resolution,[status(thm)],[f214])).
% 204.31/26.40 fof(f419,plain,(
% 204.31/26.40 ![X0,X1]: (~aSet0(X0)|~aElementOf0(X1,szNzAzT0)|aSet0(slbdtsldtrb0(X0,X1)))),
% 204.31/26.40 inference(destructive_equality_resolution,[status(thm)],[f276])).
% 204.31/26.40 fof(f428,plain,(
% 204.31/26.40 ![X0,X1,X2]: (~aFunction0(X0)|~aSubsetOf0(X1,szDzozmdt0(X0))|~aElementOf0(X2,sdtlcdtrc0(X0,X1))|aElementOf0(sK13_skl(X2,sdtlcdtrc0(X0,X1),X1,X0),X1))),
% 204.31/26.40 inference(destructive_equality_resolution,[status(thm)],[f321])).
% 204.31/26.40 fof(f429,plain,(
% 204.31/26.40 ![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)),
% 204.31/26.40 inference(destructive_equality_resolution,[status(thm)],[f322])).
% 204.31/26.40 fof(f436,plain,(
% 204.31/26.40 ![X0,X1]: (~sP0_prd(X0,X0,X1))),
% 204.31/26.40 inference(destructive_equality_resolution,[status(thm)],[f394])).
% 204.31/26.40 fof(f437,plain,(
% 204.31/26.40 aSet0(szDzozmdt0(xC))),
% 204.31/26.40 inference(resolution,[status(thm)],[f300,f381])).
% 204.31/26.40 fof(f439,plain,(
% 204.31/26.40 aElement0(sbrdtbr0(slcrc0))),
% 204.31/26.40 inference(resolution,[status(thm)],[f396,f206])).
% 204.31/26.40 fof(f440,plain,(
% 204.31/26.40 ![X0]: (~aElement0(X0)|aSet0(sdtpldt0(slcrc0,X0)))),
% 204.31/26.40 inference(resolution,[status(thm)],[f396,f399])).
% 204.31/26.40 fof(f441,plain,(
% 204.31/26.40 ![X0]: (~aElementOf0(X0,szNzAzT0)|aSet0(slbdtsldtrb0(slcrc0,X0)))),
% 204.31/26.40 inference(resolution,[status(thm)],[f396,f419])).
% 204.31/26.40 fof(f453,plain,(
% 204.31/26.40 ![X0]: (~aElement0(X0)|aSet0(sdtpldt0(szDzozmdt0(xC),X0)))),
% 204.31/26.40 inference(resolution,[status(thm)],[f437,f399])).
% 204.31/26.40 fof(f454,plain,(
% 204.31/26.40 ![X0]: (~aElementOf0(X0,szNzAzT0)|aSet0(slbdtsldtrb0(szDzozmdt0(xC),X0)))),
% 204.31/26.40 inference(resolution,[status(thm)],[f437,f419])).
% 204.31/26.40 fof(f564,plain,(
% 204.31/26.40 ~isCountable0(slcrc0)),
% 204.31/26.40 inference(forward_subsumption_resolution,[status(thm)],[f398,f396])).
% 204.31/26.40 fof(f568,plain,(
% 204.31/26.40 szDzozmdt0(sdtlpdtrp0(xC,xi))=slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))),xk)),
% 204.31/26.40 inference(resolution,[status(thm)],[f386,f384])).
% 204.31/26.40 fof(f569,plain,(
% 204.31/26.40 aFunction0(sdtlpdtrp0(xC,xi))),
% 204.31/26.40 inference(resolution,[status(thm)],[f386,f383])).
% 204.31/26.40 fof(f570,plain,(
% 204.31/26.40 isCountable0(sdtlpdtrp0(xN,xi))),
% 204.31/26.40 inference(resolution,[status(thm)],[f386,f373])).
% 204.31/26.40 fof(f621,plain,(
% 204.31/26.40 ![X0]: (~aElement0(X0)|aSet0(sdtpldt0(szNzAzT0,X0)))),
% 204.31/26.40 inference(forward_demodulation,[status(thm)],[f382,f453])).
% 204.31/26.40 fof(f623,plain,(
% 204.31/26.40 ![X0]: (~aElementOf0(X0,szNzAzT0)|aSet0(slbdtsldtrb0(szNzAzT0,X0)))),
% 204.31/26.40 inference(forward_demodulation,[status(thm)],[f382,f454])).
% 204.31/26.40 fof(f625,plain,(
% 204.31/26.40 aSet0(slbdtsldtrb0(szNzAzT0,xk))),
% 204.31/26.40 inference(resolution,[status(thm)],[f623,f363])).
% 204.31/26.40 fof(f688,plain,(
% 204.31/26.40 aSubsetOf0(szNzAzT0,szNzAzT0)),
% 204.31/26.40 inference(resolution,[status(thm)],[f167,f126])).
% 204.31/26.40 fof(f959,plain,(
% 204.31/26.40 aElementOf0(szszuzczcdt0(xi),szNzAzT0)),
% 204.31/26.40 inference(resolution,[status(thm)],[f386,f171])).
% 204.31/26.40 fof(f1076,plain,(
% 204.31/26.40 sbrdtbr0(slcrc0)=sz00),
% 204.31/26.40 inference(forward_subsumption_resolution,[status(thm)],[f408,f396])).
% 204.31/26.40 fof(f1133,plain,(
% 204.31/26.40 ![X0]: (~aElementOf0(X0,szDzozmdt0(sdtlpdtrp0(xC,xi)))|~sdtlpdtrp0(sdtlpdtrp0(xC,xi),X0)=xx)),
% 204.31/26.40 inference(backward_demodulation,[status(thm)],[f568,f389])).
% 204.31/26.40 fof(f1134,plain,(
% 204.31/26.40 aSet0(szDzozmdt0(sdtlpdtrp0(xC,xi)))),
% 204.31/26.40 inference(resolution,[status(thm)],[f569,f300])).
% 204.31/26.40 fof(f1142,plain,(
% 204.31/26.40 aSubsetOf0(szDzozmdt0(sdtlpdtrp0(xC,xi)),szDzozmdt0(sdtlpdtrp0(xC,xi)))),
% 204.31/26.40 inference(resolution,[status(thm)],[f1134,f126])).
% 204.31/26.40 fof(f1642,plain,(
% 204.31/26.40 aSubsetOf0(slbdtsldtrb0(szNzAzT0,xk),slbdtsldtrb0(szNzAzT0,xk))),
% 204.31/26.40 inference(resolution,[status(thm)],[f625,f126])).
% 204.31/26.40 fof(f1934,plain,(
% 204.31/26.40 ~aFunction0(sdtlpdtrp0(xC,xi))|~aSubsetOf0(szDzozmdt0(sdtlpdtrp0(xC,xi)),szDzozmdt0(sdtlpdtrp0(xC,xi)))|aElementOf0(sK13_skl(xx,sdtlcdtrc0(sdtlpdtrp0(xC,xi),szDzozmdt0(sdtlpdtrp0(xC,xi))),szDzozmdt0(sdtlpdtrp0(xC,xi)),sdtlpdtrp0(xC,xi)),szDzozmdt0(sdtlpdtrp0(xC,xi)))),
% 204.31/26.40 inference(resolution,[status(thm)],[f428,f387])).
% 204.31/26.40 fof(f1935,definition,(
% 204.31/26.40 sQ226_spl <=> (aFunction0(sdtlpdtrp0(xC,xi)))),
% 204.31/26.40 introduced(definition,[new_symbols(definition,[sQ226_spl])],[split_symbol_definition])).
% 204.31/26.40 fof(f1937,plain,(
% 204.31/26.40 ~aFunction0(sdtlpdtrp0(xC,xi))|sQ226_spl),
% 204.31/26.40 inference(component_clause,[status(thm)],[f1935])).
% 204.31/26.40 fof(f1938,definition,(
% 204.31/26.40 sQ227_spl <=> (aSubsetOf0(szDzozmdt0(sdtlpdtrp0(xC,xi)),szDzozmdt0(sdtlpdtrp0(xC,xi))))),
% 204.31/26.40 introduced(definition,[new_symbols(definition,[sQ227_spl])],[split_symbol_definition])).
% 204.31/26.40 fof(f1940,plain,(
% 204.31/26.40 ~aSubsetOf0(szDzozmdt0(sdtlpdtrp0(xC,xi)),szDzozmdt0(sdtlpdtrp0(xC,xi)))|sQ227_spl),
% 204.31/26.40 inference(component_clause,[status(thm)],[f1938])).
% 204.31/26.40 fof(f1941,definition,(
% 204.31/26.40 sQ228_spl <=> (aElementOf0(sK13_skl(xx,sdtlcdtrc0(sdtlpdtrp0(xC,xi),szDzozmdt0(sdtlpdtrp0(xC,xi))),szDzozmdt0(sdtlpdtrp0(xC,xi)),sdtlpdtrp0(xC,xi)),szDzozmdt0(sdtlpdtrp0(xC,xi))))),
% 204.31/26.40 introduced(definition,[new_symbols(definition,[sQ228_spl])],[split_symbol_definition])).
% 204.31/26.40 fof(f1942,plain,(
% 204.31/26.40 aElementOf0(sK13_skl(xx,sdtlcdtrc0(sdtlpdtrp0(xC,xi),szDzozmdt0(sdtlpdtrp0(xC,xi))),szDzozmdt0(sdtlpdtrp0(xC,xi)),sdtlpdtrp0(xC,xi)),szDzozmdt0(sdtlpdtrp0(xC,xi)))|~sQ228_spl),
% 204.31/26.40 inference(component_clause,[status(thm)],[f1941])).
% 204.31/26.40 fof(f1944,plain,(
% 204.31/26.40 ~sQ226_spl|~sQ227_spl|sQ228_spl),
% 204.31/26.40 inference(split_clause,[status(thm)],[f1934,f1935,f1938,f1941])).
% 204.31/26.40 fof(f1945,plain,(
% 204.31/26.40 ~aFunction0(sdtlpdtrp0(xC,xi))|~aSubsetOf0(szDzozmdt0(sdtlpdtrp0(xC,xi)),szDzozmdt0(sdtlpdtrp0(xC,xi)))|sdtlpdtrp0(sdtlpdtrp0(xC,xi),sK13_skl(xx,sdtlcdtrc0(sdtlpdtrp0(xC,xi),szDzozmdt0(sdtlpdtrp0(xC,xi))),szDzozmdt0(sdtlpdtrp0(xC,xi)),sdtlpdtrp0(xC,xi)))=xx),
% 204.31/26.40 inference(resolution,[status(thm)],[f429,f387])).
% 204.31/26.40 fof(f1946,definition,(
% 204.31/26.40 sQ229_spl <=> (sdtlpdtrp0(sdtlpdtrp0(xC,xi),sK13_skl(xx,sdtlcdtrc0(sdtlpdtrp0(xC,xi),szDzozmdt0(sdtlpdtrp0(xC,xi))),szDzozmdt0(sdtlpdtrp0(xC,xi)),sdtlpdtrp0(xC,xi)))=xx)),
% 204.31/26.40 introduced(definition,[new_symbols(definition,[sQ229_spl])],[split_symbol_definition])).
% 204.31/26.40 fof(f1947,plain,(
% 204.31/26.40 sdtlpdtrp0(sdtlpdtrp0(xC,xi),sK13_skl(xx,sdtlcdtrc0(sdtlpdtrp0(xC,xi),szDzozmdt0(sdtlpdtrp0(xC,xi))),szDzozmdt0(sdtlpdtrp0(xC,xi)),sdtlpdtrp0(xC,xi)))=xx|~sQ229_spl),
% 204.31/26.40 inference(component_clause,[status(thm)],[f1946])).
% 204.31/26.40 fof(f1949,plain,(
% 204.31/26.40 ~sQ226_spl|~sQ227_spl|sQ229_spl),
% 204.31/26.40 inference(split_clause,[status(thm)],[f1945,f1935,f1938,f1946])).
% 204.31/26.40 fof(f2412,plain,(
% 204.31/26.40 $false|sQ226_spl),
% 204.31/26.40 inference(forward_subsumption_resolution,[status(thm)],[f1937,f569])).
% 204.31/26.40 fof(f2413,plain,(
% 204.31/26.40 sQ226_spl),
% 204.31/26.40 inference(contradiction_clause,[status(thm)],[f2412])).
% 204.31/26.40 fof(f2438,plain,(
% 204.31/26.40 aSubsetOf0(xT,xT)),
% 204.31/26.40 inference(resolution,[status(thm)],[f347,f126])).
% 204.31/26.40 fof(f2523,plain,(
% 204.31/26.40 aSet0(slbdtsldtrb0(slcrc0,xK))),
% 204.31/26.40 inference(resolution,[status(thm)],[f349,f441])).
% 204.31/26.40 fof(f2525,plain,(
% 204.31/26.40 sbrdtbr0(slbdtrb0(xK))=xK),
% 204.31/26.40 inference(resolution,[status(thm)],[f349,f271])).
% 204.31/26.40 fof(f2538,plain,(
% 204.31/26.40 aFunction0(sdtlpdtrp0(xC,xK))),
% 204.31/26.40 inference(resolution,[status(thm)],[f349,f383])).
% 204.31/26.40 fof(f2623,definition,(
% 204.31/26.40 sQ350_spl <=> (xS=slcrc0)),
% 204.31/26.40 introduced(definition,[new_symbols(definition,[sQ350_spl])],[split_symbol_definition])).
% 204.31/26.40 fof(f2624,plain,(
% 204.31/26.40 xS=slcrc0|~sQ350_spl),
% 204.31/26.40 inference(component_clause,[status(thm)],[f2623])).
% 204.31/26.40 fof(f3338,plain,(
% 204.31/26.40 aElement0(sz00)),
% 204.31/26.40 inference(forward_demodulation,[status(thm)],[f1076,f439])).
% 204.31/26.40 fof(f3339,plain,(
% 204.31/26.40 aSet0(sdtpldt0(szNzAzT0,sz00))),
% 204.31/26.40 inference(resolution,[status(thm)],[f3338,f621])).
% 204.31/26.40 fof(f3417,definition,(
% 204.31/26.40 sQ491_spl <=> (aElementOf0(szszuzczcdt0(xi),szNzAzT0))),
% 204.31/26.40 introduced(definition,[new_symbols(definition,[sQ491_spl])],[split_symbol_definition])).
% 204.31/26.40 fof(f3419,plain,(
% 204.31/26.40 ~aElementOf0(szszuzczcdt0(xi),szNzAzT0)|sQ491_spl),
% 204.31/26.40 inference(component_clause,[status(thm)],[f3417])).
% 204.31/26.40 fof(f3626,plain,(
% 204.31/26.40 aSet0(sdtpldt0(slcrc0,sz00))),
% 204.31/26.40 inference(resolution,[status(thm)],[f440,f3338])).
% 204.31/26.40 fof(f4014,definition,(
% 204.31/26.40 sQ607_spl <=> (aElementOf0(sK1_skl(slcrc0,szNzAzT0),slcrc0))),
% 204.31/26.40 introduced(definition,[new_symbols(definition,[sQ607_spl])],[split_symbol_definition])).
% 204.31/26.40 fof(f4015,plain,(
% 204.31/26.40 aElementOf0(sK1_skl(slcrc0,szNzAzT0),slcrc0)|~sQ607_spl),
% 204.31/26.40 inference(component_clause,[status(thm)],[f4014])).
% 204.31/26.40 fof(f5981,definition,(
% 204.31/26.40 sQ876_spl <=> (aElementOf0(sK1_skl(slcrc0,szDzozmdt0(sdtlpdtrp0(xC,xk))),slcrc0))),
% 204.31/26.40 introduced(definition,[new_symbols(definition,[sQ876_spl])],[split_symbol_definition])).
% 204.31/26.40 fof(f5982,plain,(
% 204.31/26.40 aElementOf0(sK1_skl(slcrc0,szDzozmdt0(sdtlpdtrp0(xC,xk))),slcrc0)|~sQ876_spl),
% 204.31/26.40 inference(component_clause,[status(thm)],[f5981])).
% 204.31/26.40 fof(f15595,plain,(
% 204.31/26.40 $false|sQ227_spl),
% 204.31/26.40 inference(forward_subsumption_resolution,[status(thm)],[f1940,f1142])).
% 204.31/26.40 fof(f15596,plain,(
% 204.31/26.40 sQ227_spl),
% 204.31/26.40 inference(contradiction_clause,[status(thm)],[f15595])).
% 204.31/26.40 fof(f15635,definition,(
% 204.31/26.40 sQ2300_spl <=> (isCountable0(szNzAzT0))),
% 204.31/26.40 introduced(definition,[new_symbols(definition,[sQ2300_spl])],[split_symbol_definition])).
% 204.31/26.40 fof(f15637,plain,(
% 204.31/26.40 ~isCountable0(szNzAzT0)|sQ2300_spl),
% 204.31/26.40 inference(component_clause,[status(thm)],[f15635])).
% 204.31/26.40 fof(f15676,plain,(
% 204.31/26.40 $false|sQ2300_spl),
% 204.31/26.40 inference(forward_subsumption_resolution,[status(thm)],[f15637,f168])).
% 204.31/26.40 fof(f15677,plain,(
% 204.31/26.40 sQ2300_spl),
% 204.31/26.40 inference(contradiction_clause,[status(thm)],[f15676])).
% 204.31/26.40 fof(f15826,definition,(
% 204.31/26.40 sQ2327_spl <=> (aSubsetOf0(slbdtsldtrb0(szNzAzT0,xk),slbdtsldtrb0(szNzAzT0,xk)))),
% 204.31/26.40 introduced(definition,[new_symbols(definition,[sQ2327_spl])],[split_symbol_definition])).
% 204.31/26.40 fof(f15828,plain,(
% 204.31/26.40 ~aSubsetOf0(slbdtsldtrb0(szNzAzT0,xk),slbdtsldtrb0(szNzAzT0,xk))|sQ2327_spl),
% 204.31/26.40 inference(component_clause,[status(thm)],[f15826])).
% 204.31/26.40 fof(f15839,plain,(
% 204.31/26.40 $false|sQ2327_spl),
% 204.31/26.40 inference(forward_subsumption_resolution,[status(thm)],[f15828,f1642])).
% 204.31/26.40 fof(f15840,plain,(
% 204.31/26.40 sQ2327_spl),
% 204.31/26.40 inference(contradiction_clause,[status(thm)],[f15839])).
% 204.31/26.40 fof(f15915,definition,(
% 204.31/26.40 sQ2347_spl <=> (aElementOf0(sK1_skl(slcrc0,slbdtsldtrb0(szNzAzT0,xk)),slcrc0))),
% 204.31/26.40 introduced(definition,[new_symbols(definition,[sQ2347_spl])],[split_symbol_definition])).
% 204.31/26.40 fof(f15916,plain,(
% 204.31/26.40 aElementOf0(sK1_skl(slcrc0,slbdtsldtrb0(szNzAzT0,xk)),slcrc0)|~sQ2347_spl),
% 204.31/26.40 inference(component_clause,[status(thm)],[f15915])).
% 204.31/26.40 fof(f15919,plain,(
% 204.31/26.40 $false|~sQ2347_spl),
% 204.31/26.40 inference(forward_subsumption_resolution,[status(thm)],[f15916,f397])).
% 204.31/26.40 fof(f15920,plain,(
% 204.31/26.40 ~sQ2347_spl),
% 204.31/26.40 inference(contradiction_clause,[status(thm)],[f15919])).
% 204.31/26.40 fof(f18541,definition,(
% 204.31/26.40 sQ2818_spl <=> (aElementOf0(sK8_skl(slcrc0,sK0_skl(szNzAzT0)),slcrc0))),
% 204.31/26.40 introduced(definition,[new_symbols(definition,[sQ2818_spl])],[split_symbol_definition])).
% 204.31/26.40 fof(f18542,plain,(
% 204.31/26.40 aElementOf0(sK8_skl(slcrc0,sK0_skl(szNzAzT0)),slcrc0)|~sQ2818_spl),
% 204.31/26.40 inference(component_clause,[status(thm)],[f18541])).
% 204.31/26.40 fof(f18548,plain,(
% 204.31/26.40 $false|~sQ2818_spl),
% 204.31/26.40 inference(forward_subsumption_resolution,[status(thm)],[f18542,f397])).
% 204.31/26.40 fof(f18549,plain,(
% 204.31/26.40 ~sQ2818_spl),
% 204.31/26.40 inference(contradiction_clause,[status(thm)],[f18548])).
% 204.31/26.40 fof(f19001,definition,(
% 204.31/26.40 sQ2910_spl <=> (aSubsetOf0(szDzozmdt0(xC),szNzAzT0))),
% 204.31/26.40 introduced(definition,[new_symbols(definition,[sQ2910_spl])],[split_symbol_definition])).
% 204.31/26.40 fof(f19003,plain,(
% 204.31/26.40 ~aSubsetOf0(szDzozmdt0(xC),szNzAzT0)|sQ2910_spl),
% 204.31/26.40 inference(component_clause,[status(thm)],[f19001])).
% 204.31/26.40 fof(f19005,definition,(
% 204.31/26.40 sQ2911_spl <=> (aSubsetOf0(szDzozmdt0(xN),szNzAzT0))),
% 204.31/26.40 introduced(definition,[new_symbols(definition,[sQ2911_spl])],[split_symbol_definition])).
% 204.31/26.40 fof(f19007,plain,(
% 204.31/26.40 ~aSubsetOf0(szDzozmdt0(xN),szNzAzT0)|sQ2911_spl),
% 204.31/26.40 inference(component_clause,[status(thm)],[f19005])).
% 204.31/26.40 fof(f19009,plain,(
% 204.31/26.40 ~aSubsetOf0(szNzAzT0,szNzAzT0)|sQ2911_spl),
% 204.31/26.40 inference(forward_demodulation,[status(thm)],[f367,f19007])).
% 204.31/26.40 fof(f19010,plain,(
% 204.31/26.40 $false|sQ2911_spl),
% 204.31/26.40 inference(forward_subsumption_resolution,[status(thm)],[f19009,f688])).
% 204.31/26.40 fof(f19011,plain,(
% 204.31/26.40 sQ2911_spl),
% 204.31/26.40 inference(contradiction_clause,[status(thm)],[f19010])).
% 204.31/26.40 fof(f19012,plain,(
% 204.31/26.40 ~aSubsetOf0(szNzAzT0,szNzAzT0)|sQ2910_spl),
% 204.31/26.40 inference(forward_demodulation,[status(thm)],[f382,f19003])).
% 204.31/26.40 fof(f19013,plain,(
% 204.31/26.40 $false|sQ2910_spl),
% 204.31/26.40 inference(forward_subsumption_resolution,[status(thm)],[f19012,f688])).
% 204.31/26.40 fof(f19014,plain,(
% 204.31/26.40 sQ2910_spl),
% 204.31/26.40 inference(contradiction_clause,[status(thm)],[f19013])).
% 204.31/26.40 fof(f19897,definition,(
% 204.31/26.40 sQ3025_spl <=> (isCountable0(sdtlpdtrp0(xN,xi)))),
% 204.31/26.40 introduced(definition,[new_symbols(definition,[sQ3025_spl])],[split_symbol_definition])).
% 204.31/26.40 fof(f19899,plain,(
% 204.31/26.40 ~isCountable0(sdtlpdtrp0(xN,xi))|sQ3025_spl),
% 204.31/26.40 inference(component_clause,[status(thm)],[f19897])).
% 204.31/26.40 fof(f19907,plain,(
% 204.31/26.40 $false|sQ3025_spl),
% 204.31/26.40 inference(forward_subsumption_resolution,[status(thm)],[f19899,f570])).
% 204.31/26.40 fof(f19908,plain,(
% 204.31/26.40 sQ3025_spl),
% 204.31/26.40 inference(contradiction_clause,[status(thm)],[f19907])).
% 204.31/26.40 fof(f20266,definition,(
% 204.31/26.40 sQ3080_spl <=> (aElementOf0(sK1_skl(slcrc0,sdtmndt0(szNzAzT0,xk)),slcrc0))),
% 204.31/26.40 introduced(definition,[new_symbols(definition,[sQ3080_spl])],[split_symbol_definition])).
% 204.31/26.40 fof(f20267,plain,(
% 204.31/26.40 aElementOf0(sK1_skl(slcrc0,sdtmndt0(szNzAzT0,xk)),slcrc0)|~sQ3080_spl),
% 204.31/26.40 inference(component_clause,[status(thm)],[f20266])).
% 204.31/26.40 fof(f20270,plain,(
% 204.31/26.40 $false|~sQ3080_spl),
% 204.31/26.40 inference(forward_subsumption_resolution,[status(thm)],[f20267,f397])).
% 204.31/26.40 fof(f20271,plain,(
% 204.31/26.40 ~sQ3080_spl),
% 204.31/26.40 inference(contradiction_clause,[status(thm)],[f20270])).
% 204.31/26.40 fof(f20494,definition,(
% 204.31/26.40 sQ3105_spl <=> (sP0_prd(xk,xk,szNzAzT0))),
% 204.31/26.40 introduced(definition,[new_symbols(definition,[sQ3105_spl])],[split_symbol_definition])).
% 204.31/26.40 fof(f20495,plain,(
% 204.31/26.40 sP0_prd(xk,xk,szNzAzT0)|~sQ3105_spl),
% 204.31/26.40 inference(component_clause,[status(thm)],[f20494])).
% 204.31/26.40 fof(f20543,plain,(
% 204.31/26.40 $false|~sQ3105_spl),
% 204.31/26.40 inference(forward_subsumption_resolution,[status(thm)],[f20495,f436])).
% 204.31/26.40 fof(f20544,plain,(
% 204.31/26.40 ~sQ3105_spl),
% 204.31/26.40 inference(contradiction_clause,[status(thm)],[f20543])).
% 204.31/26.40 fof(f20831,definition,(
% 204.31/26.40 sQ3158_spl <=> (aElementOf0(sK1_skl(slcrc0,sdtmndt0(slcrc0,xk)),slcrc0))),
% 204.31/26.40 introduced(definition,[new_symbols(definition,[sQ3158_spl])],[split_symbol_definition])).
% 204.31/26.40 fof(f20832,plain,(
% 204.31/26.40 aElementOf0(sK1_skl(slcrc0,sdtmndt0(slcrc0,xk)),slcrc0)|~sQ3158_spl),
% 204.31/26.40 inference(component_clause,[status(thm)],[f20831])).
% 204.31/26.40 fof(f20835,plain,(
% 204.31/26.40 $false|~sQ3158_spl),
% 204.31/26.40 inference(forward_subsumption_resolution,[status(thm)],[f20832,f397])).
% 204.31/26.40 fof(f20836,plain,(
% 204.31/26.40 ~sQ3158_spl),
% 204.31/26.40 inference(contradiction_clause,[status(thm)],[f20835])).
% 204.31/26.40 fof(f21079,definition,(
% 204.31/26.40 sQ3183_spl <=> (sP0_prd(xk,xk,slcrc0))),
% 204.31/26.40 introduced(definition,[new_symbols(definition,[sQ3183_spl])],[split_symbol_definition])).
% 204.31/26.40 fof(f21080,plain,(
% 204.31/26.40 sP0_prd(xk,xk,slcrc0)|~sQ3183_spl),
% 204.31/26.40 inference(component_clause,[status(thm)],[f21079])).
% 204.31/26.40 fof(f21128,plain,(
% 204.31/26.40 $false|~sQ3183_spl),
% 204.31/26.40 inference(forward_subsumption_resolution,[status(thm)],[f21080,f436])).
% 204.31/26.40 fof(f21129,plain,(
% 204.31/26.40 ~sQ3183_spl),
% 204.31/26.40 inference(contradiction_clause,[status(thm)],[f21128])).
% 204.31/26.40 fof(f21545,definition,(
% 204.31/26.40 sQ3258_spl <=> (aElementOf0(sK1_skl(slcrc0,sdtmndt0(szNzAzT0,xi)),slcrc0))),
% 204.31/26.40 introduced(definition,[new_symbols(definition,[sQ3258_spl])],[split_symbol_definition])).
% 204.31/26.40 fof(f21546,plain,(
% 204.31/26.40 aElementOf0(sK1_skl(slcrc0,sdtmndt0(szNzAzT0,xi)),slcrc0)|~sQ3258_spl),
% 204.31/26.40 inference(component_clause,[status(thm)],[f21545])).
% 204.31/26.40 fof(f21549,plain,(
% 204.31/26.40 $false|~sQ3258_spl),
% 204.31/26.40 inference(forward_subsumption_resolution,[status(thm)],[f21546,f397])).
% 204.31/26.40 fof(f21550,plain,(
% 204.31/26.40 ~sQ3258_spl),
% 204.31/26.40 inference(contradiction_clause,[status(thm)],[f21549])).
% 204.31/26.40 fof(f21836,definition,(
% 204.31/26.40 sQ3294_spl <=> (sP0_prd(xi,xi,szNzAzT0))),
% 204.31/26.40 introduced(definition,[new_symbols(definition,[sQ3294_spl])],[split_symbol_definition])).
% 204.31/26.40 fof(f21837,plain,(
% 204.31/26.40 sP0_prd(xi,xi,szNzAzT0)|~sQ3294_spl),
% 204.31/26.40 inference(component_clause,[status(thm)],[f21836])).
% 204.31/26.40 fof(f21885,plain,(
% 204.31/26.40 $false|~sQ3294_spl),
% 204.31/26.40 inference(forward_subsumption_resolution,[status(thm)],[f21837,f436])).
% 204.31/26.40 fof(f21886,plain,(
% 204.31/26.40 ~sQ3294_spl),
% 204.31/26.40 inference(contradiction_clause,[status(thm)],[f21885])).
% 204.31/26.40 fof(f22283,definition,(
% 204.31/26.40 sQ3368_spl <=> (aElementOf0(sK1_skl(slcrc0,sdtmndt0(slcrc0,xi)),slcrc0))),
% 204.31/26.40 introduced(definition,[new_symbols(definition,[sQ3368_spl])],[split_symbol_definition])).
% 204.31/26.40 fof(f22284,plain,(
% 204.31/26.40 aElementOf0(sK1_skl(slcrc0,sdtmndt0(slcrc0,xi)),slcrc0)|~sQ3368_spl),
% 204.31/26.40 inference(component_clause,[status(thm)],[f22283])).
% 204.31/26.40 fof(f22287,plain,(
% 204.31/26.40 $false|~sQ3368_spl),
% 204.31/26.40 inference(forward_subsumption_resolution,[status(thm)],[f22284,f397])).
% 204.31/26.40 fof(f22288,plain,(
% 204.31/26.40 ~sQ3368_spl),
% 204.31/26.40 inference(contradiction_clause,[status(thm)],[f22287])).
% 204.31/26.40 fof(f22451,definition,(
% 204.31/26.40 sQ3381_spl <=> (sP0_prd(xi,xi,slcrc0))),
% 204.31/26.40 introduced(definition,[new_symbols(definition,[sQ3381_spl])],[split_symbol_definition])).
% 204.31/26.40 fof(f22452,plain,(
% 204.31/26.40 sP0_prd(xi,xi,slcrc0)|~sQ3381_spl),
% 204.31/26.40 inference(component_clause,[status(thm)],[f22451])).
% 204.31/26.40 fof(f22500,plain,(
% 204.31/26.40 $false|~sQ3381_spl),
% 204.31/26.40 inference(forward_subsumption_resolution,[status(thm)],[f22452,f436])).
% 204.31/26.40 fof(f22501,plain,(
% 204.31/26.40 ~sQ3381_spl),
% 204.31/26.40 inference(contradiction_clause,[status(thm)],[f22500])).
% 204.31/26.40 fof(f22676,definition,(
% 204.31/26.40 sQ3408_spl <=> (aFunction0(sdtlpdtrp0(xC,xK)))),
% 204.31/26.40 introduced(definition,[new_symbols(definition,[sQ3408_spl])],[split_symbol_definition])).
% 204.31/26.40 fof(f22678,plain,(
% 204.31/26.40 ~aFunction0(sdtlpdtrp0(xC,xK))|sQ3408_spl),
% 204.31/26.40 inference(component_clause,[status(thm)],[f22676])).
% 204.31/26.40 fof(f22755,plain,(
% 204.31/26.40 $false|sQ3408_spl),
% 204.31/26.40 inference(forward_subsumption_resolution,[status(thm)],[f22678,f2538])).
% 204.31/26.40 fof(f22756,plain,(
% 204.31/26.40 sQ3408_spl),
% 204.31/26.40 inference(contradiction_clause,[status(thm)],[f22755])).
% 204.31/26.40 fof(f23277,definition,(
% 204.31/26.40 sQ3533_spl <=> (aSubsetOf0(xT,xT))),
% 204.31/26.40 introduced(definition,[new_symbols(definition,[sQ3533_spl])],[split_symbol_definition])).
% 204.31/26.40 fof(f23279,plain,(
% 204.31/26.40 ~aSubsetOf0(xT,xT)|sQ3533_spl),
% 204.31/26.40 inference(component_clause,[status(thm)],[f23277])).
% 204.31/26.40 fof(f23290,plain,(
% 204.31/26.40 $false|sQ3533_spl),
% 204.31/26.40 inference(forward_subsumption_resolution,[status(thm)],[f23279,f2438])).
% 204.31/26.40 fof(f23291,plain,(
% 204.31/26.40 sQ3533_spl),
% 204.31/26.40 inference(contradiction_clause,[status(thm)],[f23290])).
% 204.31/26.40 fof(f23413,definition,(
% 204.31/26.40 sQ3566_spl <=> (aElementOf0(sK1_skl(slcrc0,xT),slcrc0))),
% 204.31/26.40 introduced(definition,[new_symbols(definition,[sQ3566_spl])],[split_symbol_definition])).
% 204.31/26.40 fof(f23414,plain,(
% 204.31/26.40 aElementOf0(sK1_skl(slcrc0,xT),slcrc0)|~sQ3566_spl),
% 204.31/26.40 inference(component_clause,[status(thm)],[f23413])).
% 204.31/26.40 fof(f23417,plain,(
% 204.31/26.40 $false|~sQ3566_spl),
% 204.31/26.40 inference(forward_subsumption_resolution,[status(thm)],[f23414,f397])).
% 204.31/26.40 fof(f23418,plain,(
% 204.31/26.40 ~sQ3566_spl),
% 204.31/26.40 inference(contradiction_clause,[status(thm)],[f23417])).
% 204.31/26.40 fof(f23751,definition,(
% 204.31/26.40 sQ3608_spl <=> (slbdtrb0(xK)=slcrc0)),
% 204.31/26.40 introduced(definition,[new_symbols(definition,[sQ3608_spl])],[split_symbol_definition])).
% 204.31/26.40 fof(f23752,plain,(
% 204.31/26.40 slbdtrb0(xK)=slcrc0|~sQ3608_spl),
% 204.31/26.40 inference(component_clause,[status(thm)],[f23751])).
% 204.31/26.40 fof(f23805,definition,(
% 204.31/26.40 sQ3615_spl <=> (aSet0(slbdtsldtrb0(slcrc0,xK)))),
% 204.31/26.40 introduced(definition,[new_symbols(definition,[sQ3615_spl])],[split_symbol_definition])).
% 204.31/26.40 fof(f23807,plain,(
% 204.31/26.40 ~aSet0(slbdtsldtrb0(slcrc0,xK))|sQ3615_spl),
% 204.31/26.40 inference(component_clause,[status(thm)],[f23805])).
% 204.31/26.40 fof(f23864,plain,(
% 204.31/26.40 $false|sQ3615_spl),
% 204.31/26.40 inference(forward_subsumption_resolution,[status(thm)],[f23807,f2523])).
% 204.31/26.40 fof(f23865,plain,(
% 204.31/26.40 sQ3615_spl),
% 204.31/26.40 inference(contradiction_clause,[status(thm)],[f23864])).
% 204.31/26.40 fof(f24085,plain,(
% 204.31/26.40 isCountable0(slcrc0)|~sQ350_spl),
% 204.31/26.40 inference(backward_demodulation,[status(thm)],[f2624,f351])).
% 204.31/26.40 fof(f24088,plain,(
% 204.31/26.40 $false|~sQ350_spl),
% 204.31/26.40 inference(forward_subsumption_resolution,[status(thm)],[f24085,f564])).
% 204.31/26.40 fof(f24089,plain,(
% 204.31/26.40 ~sQ350_spl),
% 204.31/26.40 inference(contradiction_clause,[status(thm)],[f24088])).
% 204.31/26.40 fof(f24527,plain,(
% 204.31/26.40 sbrdtbr0(slcrc0)=xK|~sQ3608_spl),
% 204.31/26.40 inference(backward_demodulation,[status(thm)],[f23752,f2525])).
% 204.31/26.40 fof(f24534,plain,(
% 204.31/26.40 sz00=xK|~sQ3608_spl),
% 204.31/26.40 inference(forward_demodulation,[status(thm)],[f1076,f24527])).
% 204.31/26.40 fof(f24535,plain,(
% 204.31/26.40 $false|~sQ3608_spl),
% 204.31/26.40 inference(forward_subsumption_resolution,[status(thm)],[f24534,f361])).
% 204.31/26.40 fof(f24536,plain,(
% 204.31/26.40 ~sQ3608_spl),
% 204.31/26.40 inference(contradiction_clause,[status(thm)],[f24535])).
% 205.14/26.42 fof(f24867,definition,(
% 205.14/26.42 sQ3816_spl <=> (aElementOf0(sK8_skl(slcrc0,xK),slcrc0))),
% 205.14/26.42 introduced(definition,[new_symbols(definition,[sQ3816_spl])],[split_symbol_definition])).
% 205.14/26.42 fof(f24868,plain,(
% 205.14/26.42 aElementOf0(sK8_skl(slcrc0,xK),slcrc0)|~sQ3816_spl),
% 205.14/26.42 inference(component_clause,[status(thm)],[f24867])).
% 205.14/26.42 fof(f24874,plain,(
% 205.14/26.42 $false|~sQ3816_spl),
% 205.14/26.42 inference(forward_subsumption_resolution,[status(thm)],[f24868,f397])).
% 205.14/26.42 fof(f24875,plain,(
% 205.14/26.42 ~sQ3816_spl),
% 205.14/26.42 inference(contradiction_clause,[status(thm)],[f24874])).
% 205.14/26.42 fof(f25597,definition,(
% 205.14/26.42 sQ3952_spl <=> (szmzizndt0(xS)=szmzizndt0(xS))),
% 205.14/26.42 introduced(definition,[new_symbols(definition,[sQ3952_spl])],[split_symbol_definition])).
% 205.14/26.42 fof(f25599,plain,(
% 205.14/26.42 ~szmzizndt0(xS)=szmzizndt0(xS)|sQ3952_spl),
% 205.14/26.42 inference(component_clause,[status(thm)],[f25597])).
% 205.14/26.42 fof(f27904,definition,(
% 205.14/26.42 sQ4346_spl <=> (aElementOf0(xS,slcrc0))),
% 205.14/26.42 introduced(definition,[new_symbols(definition,[sQ4346_spl])],[split_symbol_definition])).
% 205.14/26.42 fof(f27905,plain,(
% 205.14/26.42 aElementOf0(xS,slcrc0)|~sQ4346_spl),
% 205.14/26.42 inference(component_clause,[status(thm)],[f27904])).
% 205.14/26.42 fof(f27911,plain,(
% 205.14/26.42 $false|~sQ4346_spl),
% 205.14/26.42 inference(forward_subsumption_resolution,[status(thm)],[f27905,f397])).
% 205.14/26.42 fof(f27912,plain,(
% 205.14/26.42 ~sQ4346_spl),
% 205.14/26.42 inference(contradiction_clause,[status(thm)],[f27911])).
% 205.14/26.42 fof(f29601,definition,(
% 205.14/26.42 sQ4673_spl <=> (aElementOf0(sz00,slcrc0))),
% 205.14/26.42 introduced(definition,[new_symbols(definition,[sQ4673_spl])],[split_symbol_definition])).
% 205.14/26.42 fof(f29602,plain,(
% 205.14/26.42 aElementOf0(sz00,slcrc0)|~sQ4673_spl),
% 205.14/26.42 inference(component_clause,[status(thm)],[f29601])).
% 205.14/26.42 fof(f29608,plain,(
% 205.14/26.42 $false|~sQ4673_spl),
% 205.14/26.42 inference(forward_subsumption_resolution,[status(thm)],[f29602,f397])).
% 205.14/26.42 fof(f29609,plain,(
% 205.14/26.42 ~sQ4673_spl),
% 205.14/26.42 inference(contradiction_clause,[status(thm)],[f29608])).
% 205.14/26.42 fof(f30848,definition,(
% 205.14/26.42 sQ4862_spl <=> (aElementOf0(sK1_skl(slcrc0,sdtlpdtrp0(xN,xk)),slcrc0))),
% 205.14/26.42 introduced(definition,[new_symbols(definition,[sQ4862_spl])],[split_symbol_definition])).
% 205.14/26.42 fof(f30849,plain,(
% 205.14/26.42 aElementOf0(sK1_skl(slcrc0,sdtlpdtrp0(xN,xk)),slcrc0)|~sQ4862_spl),
% 205.14/26.42 inference(component_clause,[status(thm)],[f30848])).
% 205.14/26.42 fof(f30852,plain,(
% 205.14/26.42 $false|~sQ4862_spl),
% 205.14/26.42 inference(forward_subsumption_resolution,[status(thm)],[f30849,f397])).
% 205.14/26.42 fof(f30853,plain,(
% 205.14/26.42 ~sQ4862_spl),
% 205.14/26.42 inference(contradiction_clause,[status(thm)],[f30852])).
% 205.14/26.42 fof(f33360,definition,(
% 205.14/26.42 sQ5275_spl <=> (aElementOf0(sbrdtbr0(sdtlpdtrp0(xN,xk)),slcrc0))),
% 205.14/26.42 introduced(definition,[new_symbols(definition,[sQ5275_spl])],[split_symbol_definition])).
% 205.14/26.42 fof(f33361,plain,(
% 205.14/26.42 aElementOf0(sbrdtbr0(sdtlpdtrp0(xN,xk)),slcrc0)|~sQ5275_spl),
% 205.14/26.42 inference(component_clause,[status(thm)],[f33360])).
% 205.14/26.42 fof(f33367,plain,(
% 205.14/26.42 $false|~sQ5275_spl),
% 205.14/26.42 inference(forward_subsumption_resolution,[status(thm)],[f33361,f397])).
% 205.14/26.42 fof(f33368,plain,(
% 205.14/26.42 ~sQ5275_spl),
% 205.14/26.42 inference(contradiction_clause,[status(thm)],[f33367])).
% 205.14/26.42 fof(f34543,plain,(
% 205.14/26.42 $false|sQ491_spl),
% 205.14/26.42 inference(forward_subsumption_resolution,[status(thm)],[f3419,f959])).
% 205.14/26.42 fof(f34544,plain,(
% 205.14/26.42 sQ491_spl),
% 205.14/26.42 inference(contradiction_clause,[status(thm)],[f34543])).
% 205.14/26.42 fof(f39323,plain,(
% 205.14/26.42 $false|sQ3952_spl),
% 205.14/26.42 inference(trivial_equality_resolution,[status(thm)],[f25599])).
% 205.14/26.42 fof(f39324,plain,(
% 205.14/26.42 sQ3952_spl),
% 205.14/26.42 inference(contradiction_clause,[status(thm)],[f39323])).
% 205.14/26.42 fof(f40113,plain,(
% 205.14/26.42 $false|~sQ876_spl),
% 205.14/26.42 inference(forward_subsumption_resolution,[status(thm)],[f5982,f397])).
% 205.14/26.42 fof(f40114,plain,(
% 205.14/26.42 ~sQ876_spl),
% 205.14/26.42 inference(contradiction_clause,[status(thm)],[f40113])).
% 205.14/26.42 fof(f40991,definition,(
% 205.14/26.42 sQ6204_spl <=> (aSet0(sdtpldt0(slcrc0,sz00)))),
% 205.14/26.42 introduced(definition,[new_symbols(definition,[sQ6204_spl])],[split_symbol_definition])).
% 205.14/26.42 fof(f40993,plain,(
% 205.14/26.42 ~aSet0(sdtpldt0(slcrc0,sz00))|sQ6204_spl),
% 205.14/26.42 inference(component_clause,[status(thm)],[f40991])).
% 205.14/26.42 fof(f41051,plain,(
% 205.14/26.42 $false|sQ6204_spl),
% 205.14/26.42 inference(forward_subsumption_resolution,[status(thm)],[f40993,f3626])).
% 205.14/26.42 fof(f41052,plain,(
% 205.14/26.42 sQ6204_spl),
% 205.14/26.42 inference(contradiction_clause,[status(thm)],[f41051])).
% 205.14/26.42 fof(f43317,definition,(
% 205.14/26.42 sQ6754_spl <=> (aElementOf0(sK2_skl(slcrc0,sbrdtbr0(sdtlpdtrp0(xN,xk)),slcrc0),slcrc0))),
% 205.14/26.42 introduced(definition,[new_symbols(definition,[sQ6754_spl])],[split_symbol_definition])).
% 205.14/26.42 fof(f43318,plain,(
% 205.14/26.42 aElementOf0(sK2_skl(slcrc0,sbrdtbr0(sdtlpdtrp0(xN,xk)),slcrc0),slcrc0)|~sQ6754_spl),
% 205.14/26.42 inference(component_clause,[status(thm)],[f43317])).
% 205.14/26.42 fof(f43324,plain,(
% 205.14/26.42 $false|~sQ6754_spl),
% 205.14/26.42 inference(forward_subsumption_resolution,[status(thm)],[f43318,f397])).
% 205.14/26.42 fof(f43325,plain,(
% 205.14/26.42 ~sQ6754_spl),
% 205.14/26.42 inference(contradiction_clause,[status(thm)],[f43324])).
% 205.14/26.42 fof(f43643,definition,(
% 205.14/26.42 sQ6834_spl <=> (aElementOf0(sK2_skl(slcrc0,sbrdtbr0(szNzAzT0),slcrc0),slcrc0))),
% 205.14/26.42 introduced(definition,[new_symbols(definition,[sQ6834_spl])],[split_symbol_definition])).
% 205.14/26.42 fof(f43644,plain,(
% 205.14/26.42 aElementOf0(sK2_skl(slcrc0,sbrdtbr0(szNzAzT0),slcrc0),slcrc0)|~sQ6834_spl),
% 205.14/26.42 inference(component_clause,[status(thm)],[f43643])).
% 205.14/26.42 fof(f43650,plain,(
% 205.14/26.42 $false|~sQ6834_spl),
% 205.14/26.42 inference(forward_subsumption_resolution,[status(thm)],[f43644,f397])).
% 205.14/26.42 fof(f43651,plain,(
% 205.14/26.42 ~sQ6834_spl),
% 205.14/26.42 inference(contradiction_clause,[status(thm)],[f43650])).
% 205.14/26.42 fof(f43965,definition,(
% 205.14/26.42 sQ6914_spl <=> (aElementOf0(sK2_skl(slcrc0,xi,slcrc0),slcrc0))),
% 205.14/26.42 introduced(definition,[new_symbols(definition,[sQ6914_spl])],[split_symbol_definition])).
% 205.14/26.42 fof(f43966,plain,(
% 205.14/26.42 aElementOf0(sK2_skl(slcrc0,xi,slcrc0),slcrc0)|~sQ6914_spl),
% 205.14/26.42 inference(component_clause,[status(thm)],[f43965])).
% 205.14/26.42 fof(f43972,plain,(
% 205.14/26.42 $false|~sQ6914_spl),
% 205.14/26.42 inference(forward_subsumption_resolution,[status(thm)],[f43966,f397])).
% 205.14/26.42 fof(f43973,plain,(
% 205.14/26.42 ~sQ6914_spl),
% 205.14/26.42 inference(contradiction_clause,[status(thm)],[f43972])).
% 205.14/26.42 fof(f44287,definition,(
% 205.14/26.42 sQ6994_spl <=> (aElementOf0(sK2_skl(slcrc0,xk,slcrc0),slcrc0))),
% 205.14/26.42 introduced(definition,[new_symbols(definition,[sQ6994_spl])],[split_symbol_definition])).
% 205.14/26.42 fof(f44288,plain,(
% 205.14/26.42 aElementOf0(sK2_skl(slcrc0,xk,slcrc0),slcrc0)|~sQ6994_spl),
% 205.14/26.42 inference(component_clause,[status(thm)],[f44287])).
% 205.14/26.42 fof(f44294,plain,(
% 205.14/26.42 $false|~sQ6994_spl),
% 205.14/26.42 inference(forward_subsumption_resolution,[status(thm)],[f44288,f397])).
% 205.14/26.42 fof(f44295,plain,(
% 205.14/26.42 ~sQ6994_spl),
% 205.14/26.42 inference(contradiction_clause,[status(thm)],[f44294])).
% 205.14/26.42 fof(f44717,definition,(
% 205.14/26.42 sQ7110_spl <=> (aElementOf0(sK3_skl(slcrc0,sbrdtbr0(sdtlpdtrp0(xN,xk)),slcrc0),slcrc0))),
% 205.14/26.42 introduced(definition,[new_symbols(definition,[sQ7110_spl])],[split_symbol_definition])).
% 205.14/26.42 fof(f44718,plain,(
% 205.14/26.42 aElementOf0(sK3_skl(slcrc0,sbrdtbr0(sdtlpdtrp0(xN,xk)),slcrc0),slcrc0)|~sQ7110_spl),
% 205.14/26.42 inference(component_clause,[status(thm)],[f44717])).
% 205.14/26.42 fof(f44724,plain,(
% 205.14/26.42 $false|~sQ7110_spl),
% 205.14/26.42 inference(forward_subsumption_resolution,[status(thm)],[f44718,f397])).
% 205.14/26.42 fof(f44725,plain,(
% 205.14/26.42 ~sQ7110_spl),
% 205.14/26.42 inference(contradiction_clause,[status(thm)],[f44724])).
% 205.14/26.42 fof(f45156,definition,(
% 205.14/26.42 sQ7229_spl <=> (aElementOf0(sK3_skl(slcrc0,sbrdtbr0(szNzAzT0),slcrc0),slcrc0))),
% 205.14/26.42 introduced(definition,[new_symbols(definition,[sQ7229_spl])],[split_symbol_definition])).
% 205.14/26.42 fof(f45157,plain,(
% 205.14/26.42 aElementOf0(sK3_skl(slcrc0,sbrdtbr0(szNzAzT0),slcrc0),slcrc0)|~sQ7229_spl),
% 205.14/26.42 inference(component_clause,[status(thm)],[f45156])).
% 205.14/26.42 fof(f45163,plain,(
% 205.14/26.42 $false|~sQ7229_spl),
% 205.14/26.42 inference(forward_subsumption_resolution,[status(thm)],[f45157,f397])).
% 205.14/26.42 fof(f45164,plain,(
% 205.14/26.42 ~sQ7229_spl),
% 205.14/26.42 inference(contradiction_clause,[status(thm)],[f45163])).
% 205.14/26.42 fof(f45595,definition,(
% 205.14/26.42 sQ7348_spl <=> (aElementOf0(sK3_skl(slcrc0,xi,slcrc0),slcrc0))),
% 205.14/26.42 introduced(definition,[new_symbols(definition,[sQ7348_spl])],[split_symbol_definition])).
% 205.14/26.42 fof(f45596,plain,(
% 205.14/26.42 aElementOf0(sK3_skl(slcrc0,xi,slcrc0),slcrc0)|~sQ7348_spl),
% 205.14/26.42 inference(component_clause,[status(thm)],[f45595])).
% 205.14/26.42 fof(f45602,plain,(
% 205.14/26.42 $false|~sQ7348_spl),
% 205.14/26.42 inference(forward_subsumption_resolution,[status(thm)],[f45596,f397])).
% 205.14/26.42 fof(f45603,plain,(
% 205.14/26.42 ~sQ7348_spl),
% 205.14/26.42 inference(contradiction_clause,[status(thm)],[f45602])).
% 205.14/26.42 fof(f46034,definition,(
% 205.14/26.42 sQ7467_spl <=> (aElementOf0(sK3_skl(slcrc0,xk,slcrc0),slcrc0))),
% 205.14/26.42 introduced(definition,[new_symbols(definition,[sQ7467_spl])],[split_symbol_definition])).
% 205.14/26.42 fof(f46035,plain,(
% 205.14/26.42 aElementOf0(sK3_skl(slcrc0,xk,slcrc0),slcrc0)|~sQ7467_spl),
% 205.14/26.42 inference(component_clause,[status(thm)],[f46034])).
% 205.14/26.42 fof(f46041,plain,(
% 205.14/26.42 $false|~sQ7467_spl),
% 205.14/26.42 inference(forward_subsumption_resolution,[status(thm)],[f46035,f397])).
% 205.14/26.42 fof(f46042,plain,(
% 205.14/26.42 ~sQ7467_spl),
% 205.14/26.42 inference(contradiction_clause,[status(thm)],[f46041])).
% 205.14/26.42 fof(f46461,definition,(
% 205.14/26.42 sQ7582_spl <=> (aElementOf0(sK3_skl(slcrc0,sbrdtbr0(sdtlpdtrp0(xN,xk)),szNzAzT0),slcrc0))),
% 205.14/26.42 introduced(definition,[new_symbols(definition,[sQ7582_spl])],[split_symbol_definition])).
% 205.14/26.42 fof(f46462,plain,(
% 205.14/26.42 aElementOf0(sK3_skl(slcrc0,sbrdtbr0(sdtlpdtrp0(xN,xk)),szNzAzT0),slcrc0)|~sQ7582_spl),
% 205.14/26.42 inference(component_clause,[status(thm)],[f46461])).
% 205.14/26.42 fof(f46468,plain,(
% 205.14/26.42 $false|~sQ7582_spl),
% 205.14/26.42 inference(forward_subsumption_resolution,[status(thm)],[f46462,f397])).
% 205.14/26.42 fof(f46469,plain,(
% 205.14/26.42 ~sQ7582_spl),
% 205.14/26.42 inference(contradiction_clause,[status(thm)],[f46468])).
% 205.14/26.42 fof(f46885,definition,(
% 205.14/26.42 sQ7696_spl <=> (aElementOf0(sK3_skl(slcrc0,sbrdtbr0(szNzAzT0),szNzAzT0),slcrc0))),
% 205.14/26.42 introduced(definition,[new_symbols(definition,[sQ7696_spl])],[split_symbol_definition])).
% 205.14/26.42 fof(f46886,plain,(
% 205.14/26.42 aElementOf0(sK3_skl(slcrc0,sbrdtbr0(szNzAzT0),szNzAzT0),slcrc0)|~sQ7696_spl),
% 205.14/26.42 inference(component_clause,[status(thm)],[f46885])).
% 205.14/26.42 fof(f46892,plain,(
% 205.14/26.42 $false|~sQ7696_spl),
% 205.14/26.42 inference(forward_subsumption_resolution,[status(thm)],[f46886,f397])).
% 205.14/26.42 fof(f46893,plain,(
% 205.14/26.42 ~sQ7696_spl),
% 205.14/26.42 inference(contradiction_clause,[status(thm)],[f46892])).
% 205.14/26.42 fof(f47258,definition,(
% 205.14/26.42 sQ7781_spl <=> (aElementOf0(sK2_skl(slcrc0,sz00,slcrc0),slcrc0))),
% 205.14/26.42 introduced(definition,[new_symbols(definition,[sQ7781_spl])],[split_symbol_definition])).
% 205.14/26.42 fof(f47259,plain,(
% 205.14/26.42 aElementOf0(sK2_skl(slcrc0,sz00,slcrc0),slcrc0)|~sQ7781_spl),
% 205.14/26.42 inference(component_clause,[status(thm)],[f47258])).
% 205.14/26.42 fof(f47265,plain,(
% 205.14/26.42 $false|~sQ7781_spl),
% 205.14/26.42 inference(forward_subsumption_resolution,[status(thm)],[f47259,f397])).
% 205.14/26.42 fof(f47266,plain,(
% 205.14/26.42 ~sQ7781_spl),
% 205.14/26.42 inference(contradiction_clause,[status(thm)],[f47265])).
% 205.14/26.42 fof(f47679,definition,(
% 205.14/26.42 sQ7894_spl <=> (aElementOf0(sK3_skl(slcrc0,sz00,slcrc0),slcrc0))),
% 205.14/26.42 introduced(definition,[new_symbols(definition,[sQ7894_spl])],[split_symbol_definition])).
% 205.14/26.42 fof(f47680,plain,(
% 205.14/26.42 aElementOf0(sK3_skl(slcrc0,sz00,slcrc0),slcrc0)|~sQ7894_spl),
% 205.14/26.42 inference(component_clause,[status(thm)],[f47679])).
% 205.14/26.42 fof(f47686,plain,(
% 205.14/26.42 $false|~sQ7894_spl),
% 205.14/26.42 inference(forward_subsumption_resolution,[status(thm)],[f47680,f397])).
% 205.14/26.42 fof(f47687,plain,(
% 205.14/26.42 ~sQ7894_spl),
% 205.14/26.42 inference(contradiction_clause,[status(thm)],[f47686])).
% 205.14/26.42 fof(f48097,definition,(
% 205.14/26.42 sQ8006_spl <=> (aElementOf0(sK3_skl(slcrc0,sz00,szNzAzT0),slcrc0))),
% 205.14/26.42 introduced(definition,[new_symbols(definition,[sQ8006_spl])],[split_symbol_definition])).
% 205.14/26.42 fof(f48098,plain,(
% 205.14/26.42 aElementOf0(sK3_skl(slcrc0,sz00,szNzAzT0),slcrc0)|~sQ8006_spl),
% 205.14/26.42 inference(component_clause,[status(thm)],[f48097])).
% 205.14/26.42 fof(f48104,plain,(
% 205.14/26.42 $false|~sQ8006_spl),
% 205.14/26.42 inference(forward_subsumption_resolution,[status(thm)],[f48098,f397])).
% 205.14/26.42 fof(f48105,plain,(
% 205.14/26.42 ~sQ8006_spl),
% 205.14/26.42 inference(contradiction_clause,[status(thm)],[f48104])).
% 205.14/26.42 fof(f48536,definition,(
% 205.14/26.42 sQ8125_spl <=> (aElementOf0(sK3_skl(slcrc0,xi,szNzAzT0),slcrc0))),
% 205.14/26.42 introduced(definition,[new_symbols(definition,[sQ8125_spl])],[split_symbol_definition])).
% 205.14/26.42 fof(f48537,plain,(
% 205.14/26.42 aElementOf0(sK3_skl(slcrc0,xi,szNzAzT0),slcrc0)|~sQ8125_spl),
% 205.14/26.42 inference(component_clause,[status(thm)],[f48536])).
% 205.14/26.42 fof(f48543,plain,(
% 205.14/26.42 $false|~sQ8125_spl),
% 205.14/26.42 inference(forward_subsumption_resolution,[status(thm)],[f48537,f397])).
% 205.14/26.42 fof(f48544,plain,(
% 205.14/26.42 ~sQ8125_spl),
% 205.14/26.42 inference(contradiction_clause,[status(thm)],[f48543])).
% 205.14/26.42 fof(f48975,definition,(
% 205.14/26.42 sQ8244_spl <=> (aElementOf0(sK3_skl(slcrc0,xk,szNzAzT0),slcrc0))),
% 205.14/26.42 introduced(definition,[new_symbols(definition,[sQ8244_spl])],[split_symbol_definition])).
% 205.14/26.42 fof(f48976,plain,(
% 205.14/26.42 aElementOf0(sK3_skl(slcrc0,xk,szNzAzT0),slcrc0)|~sQ8244_spl),
% 205.14/26.42 inference(component_clause,[status(thm)],[f48975])).
% 205.14/26.42 fof(f48982,plain,(
% 205.14/26.42 $false|~sQ8244_spl),
% 205.14/26.42 inference(forward_subsumption_resolution,[status(thm)],[f48976,f397])).
% 205.14/26.42 fof(f48983,plain,(
% 205.14/26.42 ~sQ8244_spl),
% 205.14/26.42 inference(contradiction_clause,[status(thm)],[f48982])).
% 205.14/26.42 fof(f49504,definition,(
% 205.14/26.42 sQ8393_spl <=> (aElementOf0(sK2_skl(slcrc0,sz00,szNzAzT0),slcrc0))),
% 205.14/26.42 introduced(definition,[new_symbols(definition,[sQ8393_spl])],[split_symbol_definition])).
% 205.14/26.42 fof(f49505,plain,(
% 205.14/26.42 aElementOf0(sK2_skl(slcrc0,sz00,szNzAzT0),slcrc0)|~sQ8393_spl),
% 205.14/26.42 inference(component_clause,[status(thm)],[f49504])).
% 205.14/26.42 fof(f49514,plain,(
% 205.14/26.42 $false|~sQ8393_spl),
% 205.14/26.42 inference(forward_subsumption_resolution,[status(thm)],[f49505,f397])).
% 205.14/26.42 fof(f49515,plain,(
% 205.14/26.42 ~sQ8393_spl),
% 205.14/26.42 inference(contradiction_clause,[status(thm)],[f49514])).
% 205.14/26.42 fof(f50033,definition,(
% 205.14/26.42 sQ8542_spl <=> (aElementOf0(sK2_skl(slcrc0,sbrdtbr0(sdtlpdtrp0(xN,xk)),szNzAzT0),slcrc0))),
% 205.14/26.42 introduced(definition,[new_symbols(definition,[sQ8542_spl])],[split_symbol_definition])).
% 205.14/26.42 fof(f50034,plain,(
% 205.14/26.42 aElementOf0(sK2_skl(slcrc0,sbrdtbr0(sdtlpdtrp0(xN,xk)),szNzAzT0),slcrc0)|~sQ8542_spl),
% 205.14/26.42 inference(component_clause,[status(thm)],[f50033])).
% 205.14/26.42 fof(f50043,plain,(
% 205.14/26.42 $false|~sQ8542_spl),
% 205.14/26.42 inference(forward_subsumption_resolution,[status(thm)],[f50034,f397])).
% 205.14/26.42 fof(f50044,plain,(
% 205.14/26.42 ~sQ8542_spl),
% 205.14/26.42 inference(contradiction_clause,[status(thm)],[f50043])).
% 205.14/26.42 fof(f50589,definition,(
% 205.14/26.42 sQ8700_spl <=> (aElementOf0(sK2_skl(slcrc0,sbrdtbr0(szNzAzT0),szNzAzT0),slcrc0))),
% 205.14/26.42 introduced(definition,[new_symbols(definition,[sQ8700_spl])],[split_symbol_definition])).
% 205.14/26.42 fof(f50590,plain,(
% 205.14/26.42 aElementOf0(sK2_skl(slcrc0,sbrdtbr0(szNzAzT0),szNzAzT0),slcrc0)|~sQ8700_spl),
% 205.14/26.42 inference(component_clause,[status(thm)],[f50589])).
% 205.14/26.42 fof(f50599,plain,(
% 205.14/26.42 $false|~sQ8700_spl),
% 205.14/26.42 inference(forward_subsumption_resolution,[status(thm)],[f50590,f397])).
% 205.14/26.42 fof(f50600,plain,(
% 205.14/26.42 ~sQ8700_spl),
% 205.14/26.42 inference(contradiction_clause,[status(thm)],[f50599])).
% 205.14/26.42 fof(f51115,definition,(
% 205.14/26.42 sQ8848_spl <=> (aElementOf0(sK2_skl(slcrc0,xi,szNzAzT0),slcrc0))),
% 205.14/26.42 introduced(definition,[new_symbols(definition,[sQ8848_spl])],[split_symbol_definition])).
% 205.14/26.42 fof(f51116,plain,(
% 205.14/26.42 aElementOf0(sK2_skl(slcrc0,xi,szNzAzT0),slcrc0)|~sQ8848_spl),
% 205.14/26.42 inference(component_clause,[status(thm)],[f51115])).
% 205.14/26.42 fof(f51125,plain,(
% 205.14/26.42 $false|~sQ8848_spl),
% 205.14/26.42 inference(forward_subsumption_resolution,[status(thm)],[f51116,f397])).
% 205.14/26.42 fof(f51126,plain,(
% 205.14/26.42 ~sQ8848_spl),
% 205.14/26.48 inference(contradiction_clause,[status(thm)],[f51125])).
% 205.14/26.48 fof(f51638,definition,(
% 205.14/26.48 sQ8995_spl <=> (aElementOf0(sK2_skl(slcrc0,xk,szNzAzT0),slcrc0))),
% 205.14/26.48 introduced(definition,[new_symbols(definition,[sQ8995_spl])],[split_symbol_definition])).
% 205.14/26.48 fof(f51639,plain,(
% 205.14/26.48 aElementOf0(sK2_skl(slcrc0,xk,szNzAzT0),slcrc0)|~sQ8995_spl),
% 205.14/26.48 inference(component_clause,[status(thm)],[f51638])).
% 205.14/26.48 fof(f51648,plain,(
% 205.14/26.48 $false|~sQ8995_spl),
% 205.14/26.48 inference(forward_subsumption_resolution,[status(thm)],[f51639,f397])).
% 205.14/26.48 fof(f51649,plain,(
% 205.14/26.48 ~sQ8995_spl),
% 205.14/26.48 inference(contradiction_clause,[status(thm)],[f51648])).
% 205.14/26.48 fof(f53648,definition,(
% 205.14/26.48 sQ9299_spl <=> (aSet0(sdtpldt0(szNzAzT0,sz00)))),
% 205.14/26.48 introduced(definition,[new_symbols(definition,[sQ9299_spl])],[split_symbol_definition])).
% 205.14/26.48 fof(f53650,plain,(
% 205.14/26.48 ~aSet0(sdtpldt0(szNzAzT0,sz00))|sQ9299_spl),
% 205.14/26.48 inference(component_clause,[status(thm)],[f53648])).
% 205.14/26.48 fof(f53695,plain,(
% 205.14/26.48 $false|sQ9299_spl),
% 205.14/26.48 inference(forward_subsumption_resolution,[status(thm)],[f53650,f3339])).
% 205.14/26.48 fof(f53696,plain,(
% 205.14/26.48 sQ9299_spl),
% 205.14/26.48 inference(contradiction_clause,[status(thm)],[f53695])).
% 205.14/26.48 fof(f54063,definition,(
% 205.14/26.48 sQ9375_spl <=> (aElementOf0(szmzizndt0(slcrc0),slcrc0))),
% 205.14/26.48 introduced(definition,[new_symbols(definition,[sQ9375_spl])],[split_symbol_definition])).
% 205.14/26.48 fof(f54064,plain,(
% 205.14/26.48 aElementOf0(szmzizndt0(slcrc0),slcrc0)|~sQ9375_spl),
% 205.14/26.48 inference(component_clause,[status(thm)],[f54063])).
% 205.14/26.48 fof(f54087,definition,(
% 205.14/26.48 sQ9381_spl <=> (aElementOf0(szmzazxdt0(slcrc0),slcrc0))),
% 205.14/26.48 introduced(definition,[new_symbols(definition,[sQ9381_spl])],[split_symbol_definition])).
% 205.14/26.48 fof(f54088,plain,(
% 205.14/26.48 aElementOf0(szmzazxdt0(slcrc0),slcrc0)|~sQ9381_spl),
% 205.14/26.48 inference(component_clause,[status(thm)],[f54087])).
% 205.14/26.48 fof(f54107,plain,(
% 205.14/26.48 $false|~sQ607_spl),
% 205.14/26.48 inference(forward_subsumption_resolution,[status(thm)],[f4015,f397])).
% 205.14/26.48 fof(f54108,plain,(
% 205.14/26.48 ~sQ607_spl),
% 205.14/26.48 inference(contradiction_clause,[status(thm)],[f54107])).
% 205.14/26.48 fof(f54109,plain,(
% 205.14/26.48 $false|~sQ9381_spl),
% 205.14/26.48 inference(forward_subsumption_resolution,[status(thm)],[f54088,f397])).
% 205.14/26.48 fof(f54110,plain,(
% 205.14/26.48 ~sQ9381_spl),
% 205.14/26.48 inference(contradiction_clause,[status(thm)],[f54109])).
% 205.14/26.48 fof(f54111,plain,(
% 205.14/26.48 $false|~sQ9375_spl),
% 205.14/26.48 inference(forward_subsumption_resolution,[status(thm)],[f54064,f397])).
% 205.14/26.48 fof(f54112,plain,(
% 205.14/26.48 ~sQ9375_spl),
% 205.14/26.48 inference(contradiction_clause,[status(thm)],[f54111])).
% 205.14/26.48 fof(f62249,plain,(
% 205.14/26.48 ~aElementOf0(sK13_skl(xx,sdtlcdtrc0(sdtlpdtrp0(xC,xi),szDzozmdt0(sdtlpdtrp0(xC,xi))),szDzozmdt0(sdtlpdtrp0(xC,xi)),sdtlpdtrp0(xC,xi)),szDzozmdt0(sdtlpdtrp0(xC,xi)))|~sQ229_spl),
% 205.14/26.48 inference(resolution,[status(thm)],[f1947,f1133])).
% 205.14/26.48 fof(f62252,plain,(
% 205.14/26.48 $false|~sQ228_spl|~sQ229_spl),
% 205.14/26.48 inference(forward_subsumption_resolution,[status(thm)],[f62249,f1942])).
% 205.14/26.48 fof(f62253,plain,(
% 205.14/26.48 ~sQ228_spl|~sQ229_spl),
% 205.14/26.48 inference(contradiction_clause,[status(thm)],[f62252])).
% 205.14/26.48 fof(f62254,plain,(
% 205.14/26.48 $false),
% 205.14/26.48 inference(sat_refutation,[status(thm)],[f1944,f1949,f2413,f15596,f15677,f15840,f15920,f18549,f19011,f19014,f19908,f20271,f20544,f20836,f21129,f21550,f21886,f22288,f22501,f22756,f23291,f23418,f23865,f24089,f24536,f24875,f27912,f29609,f30853,f33368,f34544,f39324,f40114,f41052,f43325,f43651,f43973,f44295,f44725,f45164,f45603,f46042,f46469,f46893,f47266,f47687,f48105,f48544,f48983,f49515,f50044,f50600,f51126,f51649,f53696,f54108,f54110,f54112,f62253])).
% 205.14/26.48 % SZS output end CNFRefutation for theBenchmark.p
% 26.23/26.53 % Elapsed time: 26.053943 seconds
% 26.23/26.53 % CPU time: 205.713354 seconds
% 26.23/26.53 % Total memory used: 818.038 MB
% 26.23/26.53 % Net memory used: 766.429 MB
%------------------------------------------------------------------------------