%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM565+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 : n016.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:13 PM UTC 2026
% Result : Theorem 0.13s 10.92s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM565+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/10.37 % Computer : n016.cluster.edu
% 0.10/10.37 % Model : x86_64 x86_64
% 0.10/10.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/10.37 % Memory : 8046.5625MB
% 0.10/10.37 % OS : Linux 6.8.0-71-generic
% 0.10/10.37 % CPULimit : 300
% 0.10/10.37 % WCLimit : 300
% 0.10/10.37 % DateTime : Mon Sep 21 02:45:05 UTC 2026
% 0.10/10.38 % CPUTime :
% 0.10/10.39 % Drodi V4.1.1
% 0.13/10.92 % Refutation found
% 0.13/10.92 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/10.92 % SZS output start CNFRefutation for theBenchmark
% 0.13/10.92 fof(f5,definition,(
% 0.13/10.92 (! [W0] :( W0 = slcrc0<=> ( aSet0(W0)& ~ (? [W1] : aElementOf0(W1,W0) )) ) )),
% 0.13/10.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/10.92 fof(f10,definition,(
% 0.13/10.92 (! [W0] :( aSet0(W0)=> (! [W1] :( aSubsetOf0(W1,W0)<=> ( aSet0(W1)& (! [W2] :( aElementOf0(W2,W1)=> aElementOf0(W2,W0) ) )) ) )) )),
% 0.13/10.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/10.92 fof(f12,axiom,(
% 0.13/10.92 (! [W0] :( aSet0(W0)=> aSubsetOf0(W0,W0) ) )),
% 0.13/10.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/10.92 fof(f14,axiom,(
% 0.13/10.92 (! [W0,W1,W2] :( ( aSet0(W0)& aSet0(W1)& aSet0(W2) )=> ( ( aSubsetOf0(W0,W1)& aSubsetOf0(W1,W2) )=> aSubsetOf0(W0,W2) ) ) )),
% 0.13/10.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/10.92 fof(f23,axiom,(
% 0.13/10.92 ( aSet0(szNzAzT0)& isCountable0(szNzAzT0) ) ),
% 0.13/10.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/10.92 fof(f24,axiom,(
% 0.13/10.92 aElementOf0(sz00,szNzAzT0) ),
% 0.13/10.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/10.92 fof(f25,axiom,(
% 0.13/10.92 (! [W0] :( aElementOf0(W0,szNzAzT0)=> ( aElementOf0(szszuzczcdt0(W0),szNzAzT0)& szszuzczcdt0(W0) != sz00 ) ) )),
% 0.13/10.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/10.92 fof(f42,axiom,(
% 0.13/10.92 (! [W0] :( aSet0(W0)=> ( sbrdtbr0(W0) = sz00<=> W0 = slcrc0 ) ) )),
% 0.13/10.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/10.92 fof(f50,definition,(
% 0.13/10.92 (! [W0] :( aElementOf0(W0,szNzAzT0)=> (! [W1] :( W1 = slbdtrb0(W0)<=> ( aSet0(W1)& (! [W2] :( aElementOf0(W2,W1)<=> ( aElementOf0(W2,szNzAzT0)& sdtlseqdt0(szszuzczcdt0(W2),W0) ) ) )) ) )) )),
% 0.13/10.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/10.92 fof(f57,definition,(
% 0.13/10.92 (! [W0,W1] :( ( aSet0(W0)& aElementOf0(W1,szNzAzT0) )=> (! [W2] :( W2 = slbdtsldtrb0(W0,W1)<=> ( aSet0(W2)& (! [W3] :( aElementOf0(W3,W2)<=> ( aSubsetOf0(W3,W0)& sbrdtbr0(W3) = W1 ) ) )) ) )) )),
% 0.13/10.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/10.92 fof(f64,axiom,(
% 0.13/10.92 (! [W0] :( aFunction0(W0)=> aSet0(szDzozmdt0(W0)) ) )),
% 0.13/10.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/10.92 fof(f73,hypothesis,(
% 0.13/10.92 ( aSet0(xT)& isFinite0(xT) ) ),
% 0.13/10.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/10.92 fof(f74,hypothesis,(
% 0.13/10.92 aElementOf0(xK,szNzAzT0) ),
% 0.13/10.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/10.92 fof(f75,hypothesis,(
% 0.13/10.92 ( aSubsetOf0(xS,szNzAzT0)& isCountable0(xS) ) ),
% 0.13/10.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/10.92 fof(f76,hypothesis,(
% 0.13/10.92 ( aFunction0(xc)& szDzozmdt0(xc) = slbdtsldtrb0(xS,xK)& aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT) ) ),
% 0.13/10.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/10.92 fof(f78,hypothesis,(
% 0.13/10.92 xK = sz00 ),
% 0.13/10.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/10.92 fof(f79,hypothesis,(
% 0.13/10.92 aElementOf0(slcrc0,slbdtsldtrb0(xS,sz00)) ),
% 0.13/10.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/10.92 fof(f80,conjecture,(
% 0.13/10.92 (! [W0] :( aElementOf0(W0,slbdtsldtrb0(xS,sz00))=> sdtlpdtrp0(xc,W0) = sdtlpdtrp0(xc,slcrc0) ) )),
% 0.13/10.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/10.92 fof(f81,negated_conjecture,(
% 0.13/10.92 ~((! [W0] :( aElementOf0(W0,slbdtsldtrb0(xS,sz00))=> sdtlpdtrp0(xc,W0) = sdtlpdtrp0(xc,slcrc0) ) ))),
% 0.13/10.92 inference(negated_conjecture,[status(cth)],[f80])).
% 0.13/10.92 fof(f92,plain,(
% 0.13/10.92 ![W0]: (W0=slcrc0<=>(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0))))),
% 0.13/10.92 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.13/10.92 fof(f93,plain,(
% 0.13/10.92 ![W0]: ((~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0))))&(W0=slcrc0|(~aSet0(W0)|(?[W1]: aElementOf0(W1,W0)))))),
% 0.13/10.92 inference(NNF_transformation,[status(thm)],[f92])).
% 0.13/10.92 fof(f94,plain,(
% 0.13/10.92 (![W0]: (~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0)))))&(![W0]: (W0=slcrc0|(~aSet0(W0)|(?[W1]: aElementOf0(W1,W0)))))),
% 0.13/10.92 inference(miniscoping,[status(thm)],[f93])).
% 0.13/10.92 fof(f95,plain,(
% 0.13/10.92 (![W0]: (~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0)))))&(![W0]: (W0=slcrc0|(~aSet0(W0)|aElementOf0(sK0_skl(W0),W0))))),
% 0.13/10.92 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(W1,sK0_skl(W0))],[f94])).
% 0.13/10.92 fof(f96,plain,(
% 0.13/10.92 ![X0]: (~X0=slcrc0|aSet0(X0))),
% 0.13/10.92 inference(cnf_transformation,[status(thm)],[f95])).
% 0.13/10.92 fof(f97,plain,(
% 0.13/10.92 ![X0,X1]: (~X0=slcrc0|~aElementOf0(X1,X0))),
% 0.13/10.92 inference(cnf_transformation,[status(thm)],[f95])).
% 0.13/10.92 fof(f106,plain,(
% 0.13/10.92 ![W0]: (~aSet0(W0)|(![W1]: (aSubsetOf0(W1,W0)<=>(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0)))))))),
% 0.13/10.92 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 0.13/10.92 fof(f107,plain,(
% 0.13/10.92 ![W0]: (~aSet0(W0)|(![W1]: ((~aSubsetOf0(W1,W0)|(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0)))))&(aSubsetOf0(W1,W0)|(~aSet0(W1)|(?[W2]: (aElementOf0(W2,W1)&~aElementOf0(W2,W0))))))))),
% 0.13/10.92 inference(NNF_transformation,[status(thm)],[f106])).
% 0.13/10.92 fof(f108,plain,(
% 0.13/10.92 ![W0]: (~aSet0(W0)|((![W1]: (~aSubsetOf0(W1,W0)|(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0))))))&(![W1]: (aSubsetOf0(W1,W0)|(~aSet0(W1)|(?[W2]: (aElementOf0(W2,W1)&~aElementOf0(W2,W0))))))))),
% 0.13/10.92 inference(miniscoping,[status(thm)],[f107])).
% 0.13/10.92 fof(f109,plain,(
% 0.13/10.92 ![W0]: (~aSet0(W0)|((![W1]: (~aSubsetOf0(W1,W0)|(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0))))))&(![W1]: (aSubsetOf0(W1,W0)|(~aSet0(W1)|(aElementOf0(sK1_skl(W1,W0),W1)&~aElementOf0(sK1_skl(W1,W0),W0)))))))),
% 0.13/10.92 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W2,sK1_skl(W1,W0))],[f108])).
% 0.13/10.92 fof(f110,plain,(
% 0.13/10.92 ![X0,X1]: (~aSet0(X0)|~aSubsetOf0(X1,X0)|aSet0(X1))),
% 0.13/10.92 inference(cnf_transformation,[status(thm)],[f109])).
% 0.13/10.92 fof(f116,plain,(
% 0.13/10.92 ![W0]: (~aSet0(W0)|aSubsetOf0(W0,W0))),
% 0.13/10.92 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 0.13/10.92 fof(f117,plain,(
% 0.13/10.92 ![X0]: (~aSet0(X0)|aSubsetOf0(X0,X0))),
% 0.13/10.92 inference(cnf_transformation,[status(thm)],[f116])).
% 0.13/10.92 fof(f120,plain,(
% 0.13/10.92 ![W0,W1,W2]: (((~aSet0(W0)|~aSet0(W1))|~aSet0(W2))|((~aSubsetOf0(W0,W1)|~aSubsetOf0(W1,W2))|aSubsetOf0(W0,W2)))),
% 0.13/10.92 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 0.13/10.92 fof(f121,plain,(
% 0.13/10.92 ![X0,X1,X2]: (~aSet0(X0)|~aSet0(X1)|~aSet0(X2)|~aSubsetOf0(X0,X1)|~aSubsetOf0(X1,X2)|aSubsetOf0(X0,X2))),
% 0.13/10.92 inference(cnf_transformation,[status(thm)],[f120])).
% 0.13/10.92 fof(f158,plain,(
% 0.13/10.92 aSet0(szNzAzT0)),
% 0.13/10.92 inference(cnf_transformation,[status(thm)],[f23])).
% 0.13/10.92 fof(f159,plain,(
% 0.13/10.92 isCountable0(szNzAzT0)),
% 0.13/10.92 inference(cnf_transformation,[status(thm)],[f23])).
% 0.13/10.92 fof(f160,plain,(
% 0.13/10.92 aElementOf0(sz00,szNzAzT0)),
% 0.13/10.92 inference(cnf_transformation,[status(thm)],[f24])).
% 0.13/10.92 fof(f161,plain,(
% 0.13/10.92 ![W0]: (~aElementOf0(W0,szNzAzT0)|(aElementOf0(szszuzczcdt0(W0),szNzAzT0)&~szszuzczcdt0(W0)=sz00))),
% 0.13/10.92 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 0.13/10.92 fof(f162,plain,(
% 0.13/10.92 ![X0]: (~aElementOf0(X0,szNzAzT0)|aElementOf0(szszuzczcdt0(X0),szNzAzT0))),
% 0.13/10.92 inference(cnf_transformation,[status(thm)],[f161])).
% 0.13/10.92 fof(f163,plain,(
% 0.13/10.92 ![X0]: (~aElementOf0(X0,szNzAzT0)|~szszuzczcdt0(X0)=sz00)),
% 0.13/10.92 inference(cnf_transformation,[status(thm)],[f161])).
% 0.13/10.92 fof(f202,plain,(
% 0.13/10.92 ![W0]: (~aSet0(W0)|(sbrdtbr0(W0)=sz00<=>W0=slcrc0))),
% 0.13/10.92 inference(pre_NNF_transformation,[status(thm)],[f42])).
% 0.13/10.92 fof(f203,plain,(
% 0.13/10.92 ![W0]: (~aSet0(W0)|((~sbrdtbr0(W0)=sz00|W0=slcrc0)&(sbrdtbr0(W0)=sz00|~W0=slcrc0)))),
% 0.13/10.92 inference(NNF_transformation,[status(thm)],[f202])).
% 0.13/10.92 fof(f204,plain,(
% 0.13/10.92 ![X0]: (~aSet0(X0)|~sbrdtbr0(X0)=sz00|X0=slcrc0)),
% 0.13/10.92 inference(cnf_transformation,[status(thm)],[f203])).
% 0.13/10.92 fof(f234,plain,(
% 0.13/10.92 ![W0]: (~aElementOf0(W0,szNzAzT0)|(![W1]: (W1=slbdtrb0(W0)<=>(aSet0(W1)&(![W2]: (aElementOf0(W2,W1)<=>(aElementOf0(W2,szNzAzT0)&sdtlseqdt0(szszuzczcdt0(W2),W0))))))))),
% 0.13/10.92 inference(pre_NNF_transformation,[status(thm)],[f50])).
% 0.13/10.92 fof(f235,plain,(
% 0.13/10.92 ![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))))))))))),
% 0.13/10.92 inference(NNF_transformation,[status(thm)],[f234])).
% 0.13/10.92 fof(f236,plain,(
% 0.13/10.92 ![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))))))))))),
% 0.13/10.92 inference(miniscoping,[status(thm)],[f235])).
% 0.13/10.92 fof(f237,plain,(
% 0.13/10.92 ![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)))))))))),
% 0.13/10.92 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(W2,sK8_skl(W1,W0))],[f236])).
% 0.13/10.92 fof(f238,plain,(
% 0.13/10.92 ![X0,X1]: (~aElementOf0(X0,szNzAzT0)|~X1=slbdtrb0(X0)|aSet0(X1))),
% 0.13/10.92 inference(cnf_transformation,[status(thm)],[f237])).
% 0.13/10.92 fof(f263,plain,(
% 0.13/10.92 ![W0,W1]: ((~aSet0(W0)|~aElementOf0(W1,szNzAzT0))|(![W2]: (W2=slbdtsldtrb0(W0,W1)<=>(aSet0(W2)&(![W3]: (aElementOf0(W3,W2)<=>(aSubsetOf0(W3,W0)&sbrdtbr0(W3)=W1)))))))),
% 0.13/10.92 inference(pre_NNF_transformation,[status(thm)],[f57])).
% 0.13/10.92 fof(f264,plain,(
% 0.13/10.92 ![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)))))))))),
% 0.13/10.92 inference(NNF_transformation,[status(thm)],[f263])).
% 0.13/10.92 fof(f265,plain,(
% 0.13/10.92 ![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)))))))))),
% 0.13/10.92 inference(miniscoping,[status(thm)],[f264])).
% 0.13/10.92 fof(f266,plain,(
% 0.13/10.92 ![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))))))))),
% 0.13/10.92 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(W3,sK10_skl(W2,W1,W0))],[f265])).
% 0.13/10.92 fof(f267,plain,(
% 0.13/10.92 ![X0,X1,X2]: (~aSet0(X0)|~aElementOf0(X1,szNzAzT0)|~X2=slbdtsldtrb0(X0,X1)|aSet0(X2))),
% 0.13/10.92 inference(cnf_transformation,[status(thm)],[f266])).
% 0.13/10.92 fof(f268,plain,(
% 0.13/10.92 ![X0,X1,X2,X3]: (~aSet0(X0)|~aElementOf0(X1,szNzAzT0)|~X2=slbdtsldtrb0(X0,X1)|~aElementOf0(X3,X2)|aSubsetOf0(X3,X0))),
% 0.13/10.92 inference(cnf_transformation,[status(thm)],[f266])).
% 0.13/10.92 fof(f269,plain,(
% 0.13/10.92 ![X0,X1,X2,X3]: (~aSet0(X0)|~aElementOf0(X1,szNzAzT0)|~X2=slbdtsldtrb0(X0,X1)|~aElementOf0(X3,X2)|sbrdtbr0(X3)=X1)),
% 0.13/10.92 inference(cnf_transformation,[status(thm)],[f266])).
% 0.13/10.92 fof(f290,plain,(
% 0.13/10.92 ![W0]: (~aFunction0(W0)|aSet0(szDzozmdt0(W0)))),
% 0.13/10.92 inference(pre_NNF_transformation,[status(thm)],[f64])).
% 0.13/10.92 fof(f291,plain,(
% 0.13/10.92 ![X0]: (~aFunction0(X0)|aSet0(szDzozmdt0(X0)))),
% 0.13/10.92 inference(cnf_transformation,[status(thm)],[f290])).
% 0.13/10.92 fof(f338,plain,(
% 0.13/10.92 aSet0(xT)),
% 0.13/10.92 inference(cnf_transformation,[status(thm)],[f73])).
% 0.13/10.92 fof(f339,plain,(
% 0.13/10.92 isFinite0(xT)),
% 0.13/10.92 inference(cnf_transformation,[status(thm)],[f73])).
% 0.13/10.92 fof(f340,plain,(
% 0.13/10.92 aElementOf0(xK,szNzAzT0)),
% 0.13/10.92 inference(cnf_transformation,[status(thm)],[f74])).
% 0.13/10.92 fof(f341,plain,(
% 0.13/10.92 aSubsetOf0(xS,szNzAzT0)),
% 0.13/10.92 inference(cnf_transformation,[status(thm)],[f75])).
% 0.13/10.92 fof(f342,plain,(
% 0.13/10.92 isCountable0(xS)),
% 0.13/10.92 inference(cnf_transformation,[status(thm)],[f75])).
% 0.13/10.92 fof(f343,plain,(
% 0.13/10.92 aFunction0(xc)),
% 0.13/10.92 inference(cnf_transformation,[status(thm)],[f76])).
% 0.13/10.92 fof(f344,plain,(
% 0.13/10.92 szDzozmdt0(xc)=slbdtsldtrb0(xS,xK)),
% 0.13/10.92 inference(cnf_transformation,[status(thm)],[f76])).
% 0.13/10.92 fof(f352,plain,(
% 0.13/10.92 xK=sz00),
% 0.13/10.92 inference(cnf_transformation,[status(thm)],[f78])).
% 0.13/10.92 fof(f353,plain,(
% 0.13/10.92 aElementOf0(slcrc0,slbdtsldtrb0(xS,sz00))),
% 0.13/10.92 inference(cnf_transformation,[status(thm)],[f79])).
% 0.13/10.92 fof(f354,plain,(
% 0.13/10.92 (?[W0]: (aElementOf0(W0,slbdtsldtrb0(xS,sz00))&~sdtlpdtrp0(xc,W0)=sdtlpdtrp0(xc,slcrc0)))),
% 0.13/10.92 inference(pre_NNF_transformation,[status(thm)],[f81])).
% 0.13/10.92 fof(f355,plain,(
% 0.13/10.92 (aElementOf0(sK21_skl,slbdtsldtrb0(xS,sz00))&~sdtlpdtrp0(xc,sK21_skl)=sdtlpdtrp0(xc,slcrc0))),
% 0.13/10.92 inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl]),skolemize(W0,sK21_skl)],[f354])).
% 0.13/10.92 fof(f356,plain,(
% 0.13/10.92 aElementOf0(sK21_skl,slbdtsldtrb0(xS,sz00))),
% 0.13/10.92 inference(cnf_transformation,[status(thm)],[f355])).
% 0.13/10.92 fof(f357,plain,(
% 0.13/10.92 ~sdtlpdtrp0(xc,sK21_skl)=sdtlpdtrp0(xc,slcrc0)),
% 0.13/10.92 inference(cnf_transformation,[status(thm)],[f355])).
% 0.13/10.92 fof(f364,plain,(
% 0.13/10.92 aSet0(slcrc0)),
% 0.13/10.92 inference(destructive_equality_resolution,[status(thm)],[f96])).
% 0.13/10.92 fof(f365,plain,(
% 0.13/10.92 ![X0]: (~aElementOf0(X0,slcrc0))),
% 0.13/10.92 inference(destructive_equality_resolution,[status(thm)],[f97])).
% 0.13/10.92 fof(f381,plain,(
% 0.13/10.92 ![X0]: (~aElementOf0(X0,szNzAzT0)|aSet0(slbdtrb0(X0)))),
% 0.13/10.92 inference(destructive_equality_resolution,[status(thm)],[f238])).
% 0.13/10.92 fof(f387,plain,(
% 0.13/10.92 ![X0,X1]: (~aSet0(X0)|~aElementOf0(X1,szNzAzT0)|aSet0(slbdtsldtrb0(X0,X1)))),
% 0.13/10.92 inference(destructive_equality_resolution,[status(thm)],[f267])).
% 0.13/10.92 fof(f388,plain,(
% 0.13/10.92 ![X0,X1,X2]: (~aSet0(X0)|~aElementOf0(X1,szNzAzT0)|~aElementOf0(X2,slbdtsldtrb0(X0,X1))|aSubsetOf0(X2,X0))),
% 0.13/10.92 inference(destructive_equality_resolution,[status(thm)],[f268])).
% 0.13/10.92 fof(f389,plain,(
% 0.13/10.92 ![X0,X1,X2]: (~aSet0(X0)|~aElementOf0(X1,szNzAzT0)|~aElementOf0(X2,slbdtsldtrb0(X0,X1))|sbrdtbr0(X2)=X1)),
% 0.13/10.92 inference(destructive_equality_resolution,[status(thm)],[f269])).
% 0.13/10.92 fof(f439,definition,(
% 0.13/10.92 sQ8_spl <=> (aSet0(szNzAzT0))),
% 0.13/10.92 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.13/10.92 fof(f441,plain,(
% 0.13/10.92 ~aSet0(szNzAzT0)|sQ8_spl),
% 0.13/10.92 inference(component_clause,[status(thm)],[f439])).
% 0.13/10.92 fof(f446,plain,(
% 0.13/10.92 $false|sQ8_spl),
% 0.13/10.92 inference(forward_subsumption_resolution,[status(thm)],[f441,f158])).
% 0.13/10.92 fof(f447,plain,(
% 0.13/10.92 sQ8_spl),
% 0.13/10.92 inference(contradiction_clause,[status(thm)],[f446])).
% 0.13/10.92 fof(f454,definition,(
% 0.13/10.92 sQ11_spl <=> (aSet0(xS))),
% 0.13/10.92 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.13/10.92 fof(f461,plain,(
% 0.13/10.92 ~szszuzczcdt0(sz00)=sz00),
% 0.13/10.92 inference(resolution,[status(thm)],[f163,f160])).
% 0.13/10.92 fof(f490,plain,(
% 0.13/10.92 ~aSet0(szNzAzT0)|aSet0(xS)),
% 0.13/10.92 inference(resolution,[status(thm)],[f341,f110])).
% 0.13/10.92 fof(f496,plain,(
% 0.13/10.92 ~sQ8_spl|sQ11_spl),
% 0.13/10.92 inference(split_clause,[status(thm)],[f490,f439,f454])).
% 0.13/10.92 fof(f497,plain,(
% 0.13/10.92 ![X0]: (~aElementOf0(X0,szNzAzT0)|aSet0(slbdtsldtrb0(slcrc0,X0)))),
% 0.13/10.92 inference(resolution,[status(thm)],[f387,f364])).
% 0.13/10.92 fof(f514,plain,(
% 0.13/10.92 ~aSet0(xS)|~aElementOf0(sz00,szNzAzT0)|aSubsetOf0(sK21_skl,xS)),
% 0.13/10.92 inference(resolution,[status(thm)],[f388,f356])).
% 0.13/10.92 fof(f515,definition,(
% 0.13/10.92 sQ19_spl <=> (aElementOf0(sz00,szNzAzT0))),
% 0.13/10.92 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.13/10.92 fof(f517,plain,(
% 0.13/10.92 ~aElementOf0(sz00,szNzAzT0)|sQ19_spl),
% 0.13/10.92 inference(component_clause,[status(thm)],[f515])).
% 0.13/10.92 fof(f518,definition,(
% 0.13/10.92 sQ20_spl <=> (aSubsetOf0(sK21_skl,xS))),
% 0.13/10.92 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.13/10.92 fof(f519,plain,(
% 0.13/10.92 aSubsetOf0(sK21_skl,xS)|~sQ20_spl),
% 0.13/10.92 inference(component_clause,[status(thm)],[f518])).
% 0.13/10.92 fof(f521,plain,(
% 0.13/10.92 ~sQ11_spl|~sQ19_spl|sQ20_spl),
% 0.13/10.92 inference(split_clause,[status(thm)],[f514,f454,f515,f518])).
% 0.13/10.92 fof(f533,plain,(
% 0.13/10.92 aSubsetOf0(szNzAzT0,szNzAzT0)),
% 0.13/10.92 inference(resolution,[status(thm)],[f158,f117])).
% 0.13/10.92 fof(f551,plain,(
% 0.13/10.92 ![X0,X1,X2]: (~aSet0(X0)|~aSet0(X1)|~aSubsetOf0(X2,X0)|~aSubsetOf0(X0,X1)|aSubsetOf0(X2,X1))),
% 0.13/10.92 inference(forward_subsumption_resolution,[status(thm)],[f121,f110])).
% 0.13/10.92 fof(f598,plain,(
% 0.13/10.92 aElementOf0(sz00,szNzAzT0)),
% 0.13/10.92 inference(forward_demodulation,[status(thm)],[f352,f340])).
% 0.13/10.92 fof(f599,plain,(
% 0.13/10.92 $false|sQ19_spl),
% 0.13/10.92 inference(forward_subsumption_resolution,[status(thm)],[f598,f517])).
% 0.13/10.92 fof(f600,plain,(
% 0.13/10.92 sQ19_spl),
% 0.13/10.92 inference(contradiction_clause,[status(thm)],[f599])).
% 0.13/10.92 fof(f627,plain,(
% 0.13/10.92 ![X0]: (~aSet0(xS)|~aSet0(X0)|~aSubsetOf0(xS,X0)|aSubsetOf0(sK21_skl,X0)|~sQ20_spl)),
% 0.13/10.92 inference(resolution,[status(thm)],[f519,f551])).
% 0.13/10.92 fof(f632,definition,(
% 0.13/10.92 ![X0]: (sQ33_spl <=> (~aSet0(X0)|~aSubsetOf0(xS,X0)|aSubsetOf0(sK21_skl,X0)))),
% 0.13/10.92 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.13/10.92 fof(f633,plain,(
% 0.13/10.92 ![X0]: (~aSet0(X0)|~aSubsetOf0(xS,X0)|aSubsetOf0(sK21_skl,X0)|~sQ33_spl)),
% 0.13/10.92 inference(component_clause,[status(thm)],[f632])).
% 0.13/10.92 fof(f635,plain,(
% 0.13/10.92 ~sQ11_spl|sQ33_spl|~sQ20_spl),
% 0.13/10.92 inference(split_clause,[status(thm)],[f627,f454,f632,f518])).
% 0.13/10.92 fof(f651,definition,(
% 0.13/10.92 sQ38_spl <=> (aSet0(sK21_skl))),
% 0.13/10.92 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.13/10.92 fof(f652,plain,(
% 0.13/10.92 aSet0(sK21_skl)|~sQ38_spl),
% 0.13/10.92 inference(component_clause,[status(thm)],[f651])).
% 0.13/10.92 fof(f660,plain,(
% 0.13/10.92 ~sbrdtbr0(sK21_skl)=sz00|sK21_skl=slcrc0|~sQ38_spl),
% 0.13/10.92 inference(resolution,[status(thm)],[f652,f204])).
% 0.13/10.92 fof(f667,definition,(
% 0.13/10.92 sQ40_spl <=> (sbrdtbr0(sK21_skl)=sz00)),
% 0.13/10.92 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.13/10.92 fof(f669,plain,(
% 0.13/10.92 ~sbrdtbr0(sK21_skl)=sz00|sQ40_spl),
% 0.13/10.92 inference(component_clause,[status(thm)],[f667])).
% 0.13/10.92 fof(f670,definition,(
% 0.13/10.92 sQ41_spl <=> (sK21_skl=slcrc0)),
% 0.13/10.92 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.13/10.92 fof(f671,plain,(
% 0.13/10.92 sK21_skl=slcrc0|~sQ41_spl),
% 0.13/10.92 inference(component_clause,[status(thm)],[f670])).
% 0.13/10.92 fof(f673,plain,(
% 0.13/10.92 ~sQ40_spl|sQ41_spl|~sQ38_spl),
% 0.13/10.92 inference(split_clause,[status(thm)],[f660,f667,f670,f651])).
% 0.13/10.92 fof(f692,plain,(
% 0.13/10.92 ~sdtlpdtrp0(xc,sK21_skl)=sdtlpdtrp0(xc,sK21_skl)|~sQ41_spl),
% 0.13/10.92 inference(backward_demodulation,[status(thm)],[f671,f357])).
% 0.13/10.92 fof(f694,plain,(
% 0.13/10.92 $false|~sQ41_spl),
% 0.13/10.92 inference(trivial_equality_resolution,[status(thm)],[f692])).
% 0.13/10.92 fof(f695,plain,(
% 0.13/10.92 ~sQ41_spl),
% 0.13/10.92 inference(contradiction_clause,[status(thm)],[f694])).
% 0.13/10.92 fof(f697,plain,(
% 0.13/10.92 aElementOf0(sK21_skl,szDzozmdt0(xc))),
% 0.13/10.92 inference(backward_demodulation,[status(thm)],[f698,f356])).
% 0.13/10.92 fof(f698,plain,(
% 0.13/10.92 szDzozmdt0(xc)=slbdtsldtrb0(xS,sz00)),
% 0.13/10.92 inference(forward_demodulation,[status(thm)],[f352,f344])).
% 0.13/10.92 fof(f726,definition,(
% 0.13/10.92 sQ45_spl <=> (aSet0(xT))),
% 0.13/10.92 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.13/10.92 fof(f728,plain,(
% 0.13/10.92 ~aSet0(xT)|sQ45_spl),
% 0.13/10.92 inference(component_clause,[status(thm)],[f726])).
% 0.13/10.92 fof(f740,definition,(
% 0.13/10.92 sQ49_spl <=> (isFinite0(xT))),
% 0.13/10.92 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.13/10.92 fof(f742,plain,(
% 0.13/10.92 ~isFinite0(xT)|sQ49_spl),
% 0.13/10.92 inference(component_clause,[status(thm)],[f740])).
% 0.13/10.92 fof(f755,plain,(
% 0.13/10.92 aElementOf0(slcrc0,szDzozmdt0(xc))),
% 0.13/10.92 inference(forward_demodulation,[status(thm)],[f698,f353])).
% 0.13/10.92 fof(f759,definition,(
% 0.13/10.92 sQ53_spl <=> (aFunction0(xc))),
% 0.13/10.92 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.13/10.92 fof(f761,plain,(
% 0.13/10.92 ~aFunction0(xc)|sQ53_spl),
% 0.13/10.92 inference(component_clause,[status(thm)],[f759])).
% 0.13/10.92 fof(f770,definition,(
% 0.13/10.92 sQ56_spl <=> (aSet0(szDzozmdt0(xc)))),
% 0.13/10.92 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 0.13/10.92 fof(f772,plain,(
% 0.13/10.92 ~aSet0(szDzozmdt0(xc))|sQ56_spl),
% 0.13/10.92 inference(component_clause,[status(thm)],[f770])).
% 0.13/10.92 fof(f777,plain,(
% 0.13/10.92 $false|sQ53_spl),
% 0.13/10.92 inference(forward_subsumption_resolution,[status(thm)],[f761,f343])).
% 0.13/10.92 fof(f778,plain,(
% 0.13/10.92 sQ53_spl),
% 0.13/10.92 inference(contradiction_clause,[status(thm)],[f777])).
% 0.13/10.92 fof(f831,plain,(
% 0.13/10.92 aSubsetOf0(xT,xT)),
% 0.13/10.92 inference(resolution,[status(thm)],[f338,f117])).
% 0.13/10.92 fof(f886,plain,(
% 0.13/10.92 $false|sQ45_spl),
% 0.13/10.92 inference(forward_subsumption_resolution,[status(thm)],[f728,f338])).
% 0.13/10.92 fof(f887,plain,(
% 0.13/10.92 sQ45_spl),
% 0.13/10.92 inference(contradiction_clause,[status(thm)],[f886])).
% 0.13/10.92 fof(f956,definition,(
% 0.13/10.92 sQ81_spl <=> (aSubsetOf0(szNzAzT0,szNzAzT0))),
% 0.13/10.92 introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 0.13/10.92 fof(f958,plain,(
% 0.13/10.92 ~aSubsetOf0(szNzAzT0,szNzAzT0)|sQ81_spl),
% 0.13/10.92 inference(component_clause,[status(thm)],[f956])).
% 0.13/10.92 fof(f969,plain,(
% 0.13/10.92 $false|sQ81_spl),
% 0.13/10.92 inference(forward_subsumption_resolution,[status(thm)],[f958,f533])).
% 0.13/10.92 fof(f970,plain,(
% 0.13/10.92 sQ81_spl),
% 0.13/10.92 inference(contradiction_clause,[status(thm)],[f969])).
% 0.13/10.92 fof(f995,plain,(
% 0.13/10.92 $false|sQ49_spl),
% 0.13/10.92 inference(forward_subsumption_resolution,[status(thm)],[f742,f339])).
% 0.13/10.92 fof(f996,plain,(
% 0.13/10.92 sQ49_spl),
% 0.13/10.92 inference(contradiction_clause,[status(thm)],[f995])).
% 0.13/10.92 fof(f1010,plain,(
% 0.13/10.92 aElementOf0(szszuzczcdt0(sz00),szNzAzT0)),
% 0.13/10.92 inference(resolution,[status(thm)],[f162,f160])).
% 0.13/10.92 fof(f1023,plain,(
% 0.13/10.92 ~aSet0(szNzAzT0)|aSubsetOf0(sK21_skl,szNzAzT0)|~sQ33_spl),
% 0.13/10.92 inference(resolution,[status(thm)],[f633,f341])).
% 0.13/10.92 fof(f1025,definition,(
% 0.13/10.92 sQ87_spl <=> (aSubsetOf0(sK21_skl,szNzAzT0))),
% 0.13/10.92 introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 0.13/10.92 fof(f1026,plain,(
% 0.13/10.92 aSubsetOf0(sK21_skl,szNzAzT0)|~sQ87_spl),
% 0.13/10.92 inference(component_clause,[status(thm)],[f1025])).
% 0.13/10.92 fof(f1028,plain,(
% 0.13/10.92 ~sQ8_spl|sQ87_spl|~sQ33_spl),
% 0.13/10.92 inference(split_clause,[status(thm)],[f1023,f439,f1025,f632])).
% 0.13/10.92 fof(f1058,definition,(
% 0.13/10.92 sQ89_spl <=> (aSubsetOf0(xT,xT))),
% 0.13/10.92 introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition])).
% 0.13/10.92 fof(f1060,plain,(
% 0.13/10.92 ~aSubsetOf0(xT,xT)|sQ89_spl),
% 0.13/10.92 inference(component_clause,[status(thm)],[f1058])).
% 0.13/10.92 fof(f1071,plain,(
% 0.13/10.92 $false|sQ89_spl),
% 0.13/10.92 inference(forward_subsumption_resolution,[status(thm)],[f1060,f831])).
% 0.13/10.92 fof(f1072,plain,(
% 0.13/10.92 sQ89_spl),
% 0.13/10.92 inference(contradiction_clause,[status(thm)],[f1071])).
% 0.13/10.92 fof(f1095,plain,(
% 0.13/10.92 ~aSet0(szNzAzT0)|aSet0(sK21_skl)|~sQ87_spl),
% 0.13/10.92 inference(resolution,[status(thm)],[f1026,f110])).
% 0.13/10.92 fof(f1112,plain,(
% 0.13/10.92 ~sQ8_spl|sQ38_spl|~sQ87_spl),
% 0.13/10.92 inference(split_clause,[status(thm)],[f1095,f439,f651,f1025])).
% 0.13/10.92 fof(f1125,definition,(
% 0.13/10.92 sQ100_spl <=> (aElementOf0(sK1_skl(slcrc0,slcrc0),slcrc0))),
% 0.13/10.92 introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition])).
% 0.13/10.92 fof(f1126,plain,(
% 0.13/10.92 aElementOf0(sK1_skl(slcrc0,slcrc0),slcrc0)|~sQ100_spl),
% 0.13/10.92 inference(component_clause,[status(thm)],[f1125])).
% 0.13/10.92 fof(f1150,plain,(
% 0.13/10.92 $false|~sQ100_spl),
% 0.13/10.92 inference(forward_subsumption_resolution,[status(thm)],[f1126,f365])).
% 0.13/10.92 fof(f1151,plain,(
% 0.13/10.92 ~sQ100_spl),
% 0.13/10.92 inference(contradiction_clause,[status(thm)],[f1150])).
% 0.13/10.92 fof(f1223,plain,(
% 0.13/10.92 aSet0(slbdtsldtrb0(slcrc0,sz00))),
% 0.13/10.92 inference(resolution,[status(thm)],[f497,f160])).
% 0.13/10.92 fof(f1457,plain,(
% 0.13/10.92 aSet0(szDzozmdt0(xc))),
% 0.13/10.92 inference(resolution,[status(thm)],[f291,f343])).
% 0.13/10.92 fof(f1458,plain,(
% 0.13/10.92 $false|sQ56_spl),
% 0.13/10.92 inference(forward_subsumption_resolution,[status(thm)],[f1457,f772])).
% 0.13/10.92 fof(f1459,plain,(
% 0.13/10.92 sQ56_spl),
% 0.13/10.92 inference(contradiction_clause,[status(thm)],[f1458])).
% 0.13/10.92 fof(f1621,definition,(
% 0.13/10.92 sQ168_spl <=> (szDzozmdt0(xc)=slcrc0)),
% 0.13/10.92 introduced(definition,[new_symbols(definition,[sQ168_spl])],[split_symbol_definition])).
% 0.13/10.92 fof(f1622,plain,(
% 0.13/10.92 szDzozmdt0(xc)=slcrc0|~sQ168_spl),
% 0.13/10.92 inference(component_clause,[status(thm)],[f1621])).
% 0.13/10.92 fof(f1837,definition,(
% 0.13/10.92 sQ203_spl <=> (aElementOf0(sdtlpdtrp0(xc,sK21_skl),slcrc0))),
% 0.13/10.92 introduced(definition,[new_symbols(definition,[sQ203_spl])],[split_symbol_definition])).
% 0.13/10.92 fof(f1838,plain,(
% 0.13/10.92 aElementOf0(sdtlpdtrp0(xc,sK21_skl),slcrc0)|~sQ203_spl),
% 0.13/10.92 inference(component_clause,[status(thm)],[f1837])).
% 0.13/10.92 fof(f1865,plain,(
% 0.13/10.92 $false|~sQ203_spl),
% 0.13/10.92 inference(forward_subsumption_resolution,[status(thm)],[f1838,f365])).
% 0.13/10.92 fof(f1866,plain,(
% 0.13/10.92 ~sQ203_spl),
% 0.13/10.92 inference(contradiction_clause,[status(thm)],[f1865])).
% 0.13/10.92 fof(f1887,definition,(
% 0.13/10.92 sQ211_spl <=> (szszuzczcdt0(sz00)=sz00)),
% 0.13/10.92 introduced(definition,[new_symbols(definition,[sQ211_spl])],[split_symbol_definition])).
% 0.13/10.92 fof(f1888,plain,(
% 0.13/10.92 szszuzczcdt0(sz00)=sz00|~sQ211_spl),
% 0.13/10.92 inference(component_clause,[status(thm)],[f1887])).
% 0.13/10.92 fof(f1918,plain,(
% 0.13/10.92 $false|~sQ211_spl),
% 0.13/10.92 inference(forward_subsumption_resolution,[status(thm)],[f1888,f461])).
% 0.13/10.92 fof(f1919,plain,(
% 0.13/10.92 ~sQ211_spl),
% 0.13/10.92 inference(contradiction_clause,[status(thm)],[f1918])).
% 0.13/10.92 fof(f1958,definition,(
% 0.13/10.92 sQ219_spl <=> (aElementOf0(szszuzczcdt0(sz00),szNzAzT0))),
% 0.13/10.92 introduced(definition,[new_symbols(definition,[sQ219_spl])],[split_symbol_definition])).
% 0.13/10.92 fof(f1960,plain,(
% 0.13/10.92 ~aElementOf0(szszuzczcdt0(sz00),szNzAzT0)|sQ219_spl),
% 0.13/10.92 inference(component_clause,[status(thm)],[f1958])).
% 0.13/10.92 fof(f1973,plain,(
% 0.13/10.92 $false|sQ219_spl),
% 0.13/10.92 inference(forward_subsumption_resolution,[status(thm)],[f1960,f1010])).
% 0.13/10.92 fof(f1974,plain,(
% 0.13/10.92 sQ219_spl),
% 0.13/10.92 inference(contradiction_clause,[status(thm)],[f1973])).
% 0.13/10.92 fof(f2181,definition,(
% 0.13/10.92 sQ257_spl <=> (aSet0(slbdtsldtrb0(slcrc0,sz00)))),
% 0.13/10.92 introduced(definition,[new_symbols(definition,[sQ257_spl])],[split_symbol_definition])).
% 0.13/10.92 fof(f2183,plain,(
% 0.13/10.92 ~aSet0(slbdtsldtrb0(slcrc0,sz00))|sQ257_spl),
% 0.13/10.92 inference(component_clause,[status(thm)],[f2181])).
% 0.13/10.92 fof(f2200,plain,(
% 0.13/10.92 $false|sQ257_spl),
% 0.13/10.92 inference(forward_subsumption_resolution,[status(thm)],[f2183,f1223])).
% 0.13/10.92 fof(f2201,plain,(
% 0.13/10.92 sQ257_spl),
% 0.13/10.92 inference(contradiction_clause,[status(thm)],[f2200])).
% 0.13/10.92 fof(f2223,plain,(
% 0.13/10.92 aSet0(slbdtrb0(szszuzczcdt0(sz00)))),
% 0.13/10.92 inference(resolution,[status(thm)],[f381,f1010])).
% 0.13/10.92 fof(f2780,definition,(
% 0.13/10.92 sQ357_spl <=> (aElementOf0(sK21_skl,slcrc0))),
% 0.13/10.92 introduced(definition,[new_symbols(definition,[sQ357_spl])],[split_symbol_definition])).
% 0.13/10.92 fof(f2781,plain,(
% 0.13/10.92 aElementOf0(sK21_skl,slcrc0)|~sQ357_spl),
% 0.13/10.92 inference(component_clause,[status(thm)],[f2780])).
% 0.13/10.92 fof(f2808,plain,(
% 0.13/10.92 $false|~sQ357_spl),
% 0.13/10.92 inference(forward_subsumption_resolution,[status(thm)],[f2781,f365])).
% 0.13/10.92 fof(f2809,plain,(
% 0.13/10.92 ~sQ357_spl),
% 0.13/10.92 inference(contradiction_clause,[status(thm)],[f2808])).
% 0.13/10.92 fof(f3363,plain,(
% 0.13/10.92 aElementOf0(slcrc0,slcrc0)|~sQ168_spl),
% 0.13/10.92 inference(backward_demodulation,[status(thm)],[f1622,f755])).
% 0.13/10.92 fof(f3502,plain,(
% 0.13/10.92 $false|~sQ168_spl),
% 0.13/10.92 inference(forward_subsumption_resolution,[status(thm)],[f3363,f365])).
% 0.13/10.92 fof(f3503,plain,(
% 0.13/10.92 ~sQ168_spl),
% 0.13/10.92 inference(contradiction_clause,[status(thm)],[f3502])).
% 0.13/10.92 fof(f3529,definition,(
% 0.13/10.92 sQ445_spl <=> (aSubsetOf0(xS,szNzAzT0))),
% 0.13/10.92 introduced(definition,[new_symbols(definition,[sQ445_spl])],[split_symbol_definition])).
% 0.13/10.92 fof(f3531,plain,(
% 0.13/10.92 ~aSubsetOf0(xS,szNzAzT0)|sQ445_spl),
% 0.13/10.92 inference(component_clause,[status(thm)],[f3529])).
% 0.13/10.92 fof(f3552,plain,(
% 0.13/10.92 $false|sQ445_spl),
% 0.13/10.92 inference(forward_subsumption_resolution,[status(thm)],[f3531,f341])).
% 0.13/10.92 fof(f3553,plain,(
% 0.13/10.92 sQ445_spl),
% 0.13/10.92 inference(contradiction_clause,[status(thm)],[f3552])).
% 0.13/10.92 fof(f4123,definition,(
% 0.13/10.92 sQ514_spl <=> (isCountable0(szNzAzT0))),
% 0.13/10.92 introduced(definition,[new_symbols(definition,[sQ514_spl])],[split_symbol_definition])).
% 0.13/10.92 fof(f4125,plain,(
% 0.13/10.92 ~isCountable0(szNzAzT0)|sQ514_spl),
% 0.13/10.92 inference(component_clause,[status(thm)],[f4123])).
% 0.13/10.92 fof(f4130,definition,(
% 0.13/10.92 sQ516_spl <=> (isCountable0(xS))),
% 0.13/10.92 introduced(definition,[new_symbols(definition,[sQ516_spl])],[split_symbol_definition])).
% 0.13/10.92 fof(f4132,plain,(
% 0.13/10.92 ~isCountable0(xS)|sQ516_spl),
% 0.13/10.92 inference(component_clause,[status(thm)],[f4130])).
% 0.13/10.92 fof(f4176,plain,(
% 0.13/10.92 ![X0]: (~aSet0(xS)|~aElementOf0(sz00,szNzAzT0)|~aElementOf0(X0,szDzozmdt0(xc))|sbrdtbr0(X0)=sz00)),
% 0.13/10.92 inference(paramodulation,[status(thm)],[f698,f389])).
% 0.13/10.92 fof(f4192,definition,(
% 0.13/10.92 ![X0]: (sQ528_spl <=> (~aElementOf0(X0,szDzozmdt0(xc))|sbrdtbr0(X0)=sz00))),
% 0.13/10.92 introduced(definition,[new_symbols(definition,[sQ528_spl])],[split_symbol_definition])).
% 0.13/10.92 fof(f4193,plain,(
% 0.13/10.92 ![X0]: (~aElementOf0(X0,szDzozmdt0(xc))|sbrdtbr0(X0)=sz00|~sQ528_spl)),
% 0.13/10.92 inference(component_clause,[status(thm)],[f4192])).
% 0.13/10.92 fof(f4195,plain,(
% 0.13/10.92 ~sQ11_spl|~sQ19_spl|sQ528_spl),
% 0.13/10.92 inference(split_clause,[status(thm)],[f4176,f454,f515,f4192])).
% 0.13/10.92 fof(f4265,plain,(
% 0.13/10.92 $false|sQ516_spl),
% 0.13/10.92 inference(forward_subsumption_resolution,[status(thm)],[f4132,f342])).
% 0.13/10.92 fof(f4266,plain,(
% 0.13/10.92 sQ516_spl),
% 0.13/10.92 inference(contradiction_clause,[status(thm)],[f4265])).
% 0.13/10.92 fof(f4267,plain,(
% 0.13/10.92 $false|sQ514_spl),
% 0.13/10.92 inference(forward_subsumption_resolution,[status(thm)],[f4125,f159])).
% 0.13/10.92 fof(f4268,plain,(
% 0.13/10.92 sQ514_spl),
% 0.13/10.92 inference(contradiction_clause,[status(thm)],[f4267])).
% 0.13/10.93 fof(f4592,definition,(
% 0.13/10.93 sQ585_spl <=> (aElementOf0(sK1_skl(slcrc0,xT),slcrc0))),
% 0.13/10.93 introduced(definition,[new_symbols(definition,[sQ585_spl])],[split_symbol_definition])).
% 0.13/10.93 fof(f4593,plain,(
% 0.13/10.93 aElementOf0(sK1_skl(slcrc0,xT),slcrc0)|~sQ585_spl),
% 0.13/10.93 inference(component_clause,[status(thm)],[f4592])).
% 0.13/10.93 fof(f4617,plain,(
% 0.13/10.93 $false|~sQ585_spl),
% 0.13/10.93 inference(forward_subsumption_resolution,[status(thm)],[f4593,f365])).
% 0.13/10.93 fof(f4618,plain,(
% 0.13/10.93 ~sQ585_spl),
% 0.13/10.93 inference(contradiction_clause,[status(thm)],[f4617])).
% 0.13/10.93 fof(f4776,definition,(
% 0.13/10.93 sQ613_spl <=> (aElementOf0(sK1_skl(slcrc0,szNzAzT0),slcrc0))),
% 0.13/10.93 introduced(definition,[new_symbols(definition,[sQ613_spl])],[split_symbol_definition])).
% 0.13/10.93 fof(f4777,plain,(
% 0.13/10.93 aElementOf0(sK1_skl(slcrc0,szNzAzT0),slcrc0)|~sQ613_spl),
% 0.13/10.93 inference(component_clause,[status(thm)],[f4776])).
% 0.13/10.93 fof(f4792,plain,(
% 0.13/10.93 $false|~sQ613_spl),
% 0.13/10.93 inference(forward_subsumption_resolution,[status(thm)],[f4777,f365])).
% 0.13/10.93 fof(f4793,plain,(
% 0.13/10.93 ~sQ613_spl),
% 0.13/10.93 inference(contradiction_clause,[status(thm)],[f4792])).
% 0.13/10.93 fof(f5577,definition,(
% 0.13/10.93 sQ726_spl <=> (aSet0(slbdtrb0(szszuzczcdt0(sz00))))),
% 0.13/10.93 introduced(definition,[new_symbols(definition,[sQ726_spl])],[split_symbol_definition])).
% 0.13/10.93 fof(f5579,plain,(
% 0.13/10.93 ~aSet0(slbdtrb0(szszuzczcdt0(sz00)))|sQ726_spl),
% 0.13/10.93 inference(component_clause,[status(thm)],[f5577])).
% 0.13/10.93 fof(f5608,plain,(
% 0.13/10.93 $false|sQ726_spl),
% 0.13/10.93 inference(forward_subsumption_resolution,[status(thm)],[f5579,f2223])).
% 0.13/10.93 fof(f5609,plain,(
% 0.13/10.93 sQ726_spl),
% 0.13/10.93 inference(contradiction_clause,[status(thm)],[f5608])).
% 0.13/10.93 fof(f5752,definition,(
% 0.13/10.93 sQ766_spl <=> (aElementOf0(sK8_skl(slcrc0,sz00),slcrc0))),
% 0.13/10.93 introduced(definition,[new_symbols(definition,[sQ766_spl])],[split_symbol_definition])).
% 0.13/10.93 fof(f5753,plain,(
% 0.13/10.93 aElementOf0(sK8_skl(slcrc0,sz00),slcrc0)|~sQ766_spl),
% 0.13/10.93 inference(component_clause,[status(thm)],[f5752])).
% 0.13/10.93 fof(f8338,definition,(
% 0.13/10.93 sQ1103_spl <=> (aElementOf0(sK2_skl(slcrc0,sK21_skl,slcrc0),slcrc0))),
% 0.13/10.93 introduced(definition,[new_symbols(definition,[sQ1103_spl])],[split_symbol_definition])).
% 0.13/10.93 fof(f8339,plain,(
% 0.13/10.93 aElementOf0(sK2_skl(slcrc0,sK21_skl,slcrc0),slcrc0)|~sQ1103_spl),
% 0.13/10.93 inference(component_clause,[status(thm)],[f8338])).
% 0.13/10.93 fof(f8378,plain,(
% 0.13/10.93 $false|~sQ766_spl),
% 0.13/10.93 inference(forward_subsumption_resolution,[status(thm)],[f5753,f365])).
% 0.13/10.93 fof(f8379,plain,(
% 0.13/10.93 ~sQ766_spl),
% 0.13/10.93 inference(contradiction_clause,[status(thm)],[f8378])).
% 0.13/10.93 fof(f8388,plain,(
% 0.13/10.93 $false|~sQ1103_spl),
% 0.13/10.93 inference(forward_subsumption_resolution,[status(thm)],[f8339,f365])).
% 0.13/10.93 fof(f8389,plain,(
% 0.13/10.93 ~sQ1103_spl),
% 0.13/10.93 inference(contradiction_clause,[status(thm)],[f8388])).
% 0.13/10.93 fof(f8547,plain,(
% 0.13/10.93 sbrdtbr0(sK21_skl)=sz00|~sQ528_spl),
% 0.13/10.93 inference(resolution,[status(thm)],[f4193,f697])).
% 0.13/10.93 fof(f8548,plain,(
% 0.13/10.93 $false|sQ40_spl|~sQ528_spl),
% 0.13/10.93 inference(forward_subsumption_resolution,[status(thm)],[f8547,f669])).
% 0.13/10.93 fof(f8549,plain,(
% 0.13/10.93 sQ40_spl|~sQ528_spl),
% 0.13/10.93 inference(contradiction_clause,[status(thm)],[f8548])).
% 0.13/10.93 fof(f8550,plain,(
% 0.13/10.93 $false),
% 0.13/10.93 inference(sat_refutation,[status(thm)],[f447,f496,f521,f600,f635,f673,f695,f778,f887,f970,f996,f1028,f1072,f1112,f1151,f1459,f1866,f1919,f1974,f2201,f2809,f3503,f3553,f4195,f4266,f4268,f4618,f4793,f5609,f8379,f8389,f8549])).
% 0.13/10.93 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/10.94 % Elapsed time: 0.551527 seconds
% 0.13/10.94 % CPU time: 4.146584 seconds
% 0.13/10.94 % Total memory used: 170.932 MB
% 0.13/10.94 % Net memory used: 167.107 MB
%------------------------------------------------------------------------------