%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM563+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n013.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 232.71s 35.34s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM563+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/5.57 % Computer : n013.cluster.edu
% 0.11/5.57 % Model : x86_64 x86_64
% 0.11/5.57 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.57 % Memory : 8046.5625MB
% 0.11/5.57 % OS : Linux 6.8.0-71-generic
% 0.11/5.57 % CPULimit : 300
% 0.11/5.57 % WCLimit : 300
% 0.11/5.57 % DateTime : Mon Sep 21 02:39:57 UTC 2026
% 0.11/5.57 % CPUTime :
% 0.11/5.59 % Drodi V4.1.1
% 232.71/35.34 % Refutation found
% 232.71/35.34 % SZS status Theorem for theBenchmark: Theorem is valid
% 232.71/35.34 % SZS output start CNFRefutation for theBenchmark
% 232.71/35.34 fof(f5,definition,(
% 232.71/35.34 (! [W0] :( W0 = slcrc0<=> ( aSet0(W0)& ~ (? [W1] : aElementOf0(W1,W0) )) ) )),
% 232.71/35.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 232.71/35.34 fof(f10,definition,(
% 232.71/35.34 (! [W0] :( aSet0(W0)=> (! [W1] :( aSubsetOf0(W1,W0)<=> ( aSet0(W1)& (! [W2] :( aElementOf0(W2,W1)=> aElementOf0(W2,W0) ) )) ) )) )),
% 232.71/35.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 232.71/35.34 fof(f12,axiom,(
% 232.71/35.34 (! [W0] :( aSet0(W0)=> aSubsetOf0(W0,W0) ) )),
% 232.71/35.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 232.71/35.34 fof(f23,axiom,(
% 232.71/35.34 ( aSet0(szNzAzT0)& isCountable0(szNzAzT0) ) ),
% 232.71/35.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 232.71/35.34 fof(f24,axiom,(
% 232.71/35.34 aElementOf0(sz00,szNzAzT0) ),
% 232.71/35.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 232.71/35.34 fof(f42,axiom,(
% 232.71/35.34 (! [W0] :( aSet0(W0)=> ( sbrdtbr0(W0) = sz00<=> W0 = slcrc0 ) ) )),
% 232.71/35.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 232.71/35.34 fof(f57,definition,(
% 232.71/35.34 (! [W0,W1] :( ( aSet0(W0)& aElementOf0(W1,szNzAzT0) )=> (! [W2] :( W2 = slbdtsldtrb0(W0,W1)<=> ( aSet0(W2)& (! [W3] :( aElementOf0(W3,W2)<=> ( aSubsetOf0(W3,W0)& sbrdtbr0(W3) = W1 ) ) )) ) )) )),
% 232.71/35.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 232.71/35.34 fof(f64,axiom,(
% 232.71/35.34 (! [W0] :( aFunction0(W0)=> aSet0(szDzozmdt0(W0)) ) )),
% 232.71/35.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 232.71/35.34 fof(f68,definition,(
% 232.71/35.34 (! [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 ) )) )) ) )) )) )),
% 232.71/35.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 232.71/35.34 fof(f73,hypothesis,(
% 232.71/35.34 ( aSet0(xT)& isFinite0(xT) ) ),
% 232.71/35.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 232.71/35.34 fof(f75,hypothesis,(
% 232.71/35.34 ( aSubsetOf0(xS,szNzAzT0)& isCountable0(xS) ) ),
% 232.71/35.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 232.71/35.34 fof(f76,hypothesis,(
% 232.71/35.34 ( aFunction0(xc)& szDzozmdt0(xc) = slbdtsldtrb0(xS,xK)& aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT) ) ),
% 232.71/35.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 232.71/35.34 fof(f78,conjecture,(
% 232.71/35.34 ( xK = sz00=> (? [W0] :( aElementOf0(W0,xT)& (? [W1] :( aSubsetOf0(W1,xS)& isCountable0(W1)& (! [W2] :( aElementOf0(W2,slbdtsldtrb0(W1,xK))=> sdtlpdtrp0(xc,W2) = W0 ) )) )) )) ),
% 232.71/35.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 232.71/35.34 fof(f79,negated_conjecture,(
% 232.71/35.34 ~(( xK = sz00=> (? [W0] :( aElementOf0(W0,xT)& (? [W1] :( aSubsetOf0(W1,xS)& isCountable0(W1)& (! [W2] :( aElementOf0(W2,slbdtsldtrb0(W1,xK))=> sdtlpdtrp0(xc,W2) = W0 ) )) )) )) )),
% 232.71/35.34 inference(negated_conjecture,[status(cth)],[f78])).
% 232.71/35.34 fof(f90,plain,(
% 232.71/35.34 ![W0]: (W0=slcrc0<=>(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0))))),
% 232.71/35.34 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 232.71/35.34 fof(f91,plain,(
% 232.71/35.34 ![W0]: ((~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0))))&(W0=slcrc0|(~aSet0(W0)|(?[W1]: aElementOf0(W1,W0)))))),
% 232.71/35.34 inference(NNF_transformation,[status(thm)],[f90])).
% 232.71/35.34 fof(f92,plain,(
% 232.71/35.34 (![W0]: (~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0)))))&(![W0]: (W0=slcrc0|(~aSet0(W0)|(?[W1]: aElementOf0(W1,W0)))))),
% 232.71/35.34 inference(miniscoping,[status(thm)],[f91])).
% 232.71/35.34 fof(f93,plain,(
% 232.71/35.34 (![W0]: (~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0)))))&(![W0]: (W0=slcrc0|(~aSet0(W0)|aElementOf0(sK0_skl(W0),W0))))),
% 232.71/35.34 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(W1,sK0_skl(W0))],[f92])).
% 232.71/35.34 fof(f94,plain,(
% 232.71/35.34 ![X0]: (~X0=slcrc0|aSet0(X0))),
% 232.71/35.34 inference(cnf_transformation,[status(thm)],[f93])).
% 232.71/35.34 fof(f95,plain,(
% 232.71/35.34 ![X0,X1]: (~X0=slcrc0|~aElementOf0(X1,X0))),
% 232.71/35.34 inference(cnf_transformation,[status(thm)],[f93])).
% 232.71/35.34 fof(f104,plain,(
% 232.71/35.34 ![W0]: (~aSet0(W0)|(![W1]: (aSubsetOf0(W1,W0)<=>(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0)))))))),
% 232.71/35.34 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 232.71/35.34 fof(f105,plain,(
% 232.71/35.34 ![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))))))))),
% 232.71/35.34 inference(NNF_transformation,[status(thm)],[f104])).
% 232.71/35.34 fof(f106,plain,(
% 232.71/35.34 ![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))))))))),
% 232.71/35.34 inference(miniscoping,[status(thm)],[f105])).
% 232.71/35.34 fof(f107,plain,(
% 232.71/35.34 ![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)))))))),
% 232.71/35.34 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W2,sK1_skl(W1,W0))],[f106])).
% 232.71/35.34 fof(f108,plain,(
% 232.71/35.34 ![X0,X1]: (~aSet0(X0)|~aSubsetOf0(X1,X0)|aSet0(X1))),
% 232.71/35.34 inference(cnf_transformation,[status(thm)],[f107])).
% 232.71/35.34 fof(f109,plain,(
% 232.71/35.34 ![X0,X1,X2]: (~aSet0(X0)|~aSubsetOf0(X1,X0)|~aElementOf0(X2,X1)|aElementOf0(X2,X0))),
% 232.71/35.34 inference(cnf_transformation,[status(thm)],[f107])).
% 232.71/35.34 fof(f110,plain,(
% 232.71/35.34 ![X0,X1]: (~aSet0(X0)|aSubsetOf0(X1,X0)|~aSet0(X1)|aElementOf0(sK1_skl(X1,X0),X1))),
% 232.71/35.34 inference(cnf_transformation,[status(thm)],[f107])).
% 232.71/35.34 fof(f114,plain,(
% 232.71/35.34 ![W0]: (~aSet0(W0)|aSubsetOf0(W0,W0))),
% 232.71/35.34 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 232.71/35.34 fof(f115,plain,(
% 232.71/35.34 ![X0]: (~aSet0(X0)|aSubsetOf0(X0,X0))),
% 232.71/35.34 inference(cnf_transformation,[status(thm)],[f114])).
% 232.71/35.34 fof(f156,plain,(
% 232.71/35.34 aSet0(szNzAzT0)),
% 232.71/35.34 inference(cnf_transformation,[status(thm)],[f23])).
% 232.71/35.34 fof(f158,plain,(
% 232.71/35.34 aElementOf0(sz00,szNzAzT0)),
% 232.71/35.34 inference(cnf_transformation,[status(thm)],[f24])).
% 232.71/35.34 fof(f200,plain,(
% 232.71/35.34 ![W0]: (~aSet0(W0)|(sbrdtbr0(W0)=sz00<=>W0=slcrc0))),
% 232.71/35.34 inference(pre_NNF_transformation,[status(thm)],[f42])).
% 232.71/35.34 fof(f201,plain,(
% 232.71/35.34 ![W0]: (~aSet0(W0)|((~sbrdtbr0(W0)=sz00|W0=slcrc0)&(sbrdtbr0(W0)=sz00|~W0=slcrc0)))),
% 232.71/35.34 inference(NNF_transformation,[status(thm)],[f200])).
% 232.71/35.34 fof(f202,plain,(
% 232.71/35.34 ![X0]: (~aSet0(X0)|~sbrdtbr0(X0)=sz00|X0=slcrc0)),
% 232.71/35.34 inference(cnf_transformation,[status(thm)],[f201])).
% 232.71/35.34 fof(f203,plain,(
% 232.71/35.34 ![X0]: (~aSet0(X0)|sbrdtbr0(X0)=sz00|~X0=slcrc0)),
% 232.71/35.34 inference(cnf_transformation,[status(thm)],[f201])).
% 232.71/35.34 fof(f261,plain,(
% 232.71/35.34 ![W0,W1]: ((~aSet0(W0)|~aElementOf0(W1,szNzAzT0))|(![W2]: (W2=slbdtsldtrb0(W0,W1)<=>(aSet0(W2)&(![W3]: (aElementOf0(W3,W2)<=>(aSubsetOf0(W3,W0)&sbrdtbr0(W3)=W1)))))))),
% 232.71/35.34 inference(pre_NNF_transformation,[status(thm)],[f57])).
% 232.71/35.34 fof(f262,plain,(
% 232.71/35.34 ![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)))))))))),
% 232.71/35.34 inference(NNF_transformation,[status(thm)],[f261])).
% 232.71/35.34 fof(f263,plain,(
% 232.71/35.34 ![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)))))))))),
% 232.71/35.34 inference(miniscoping,[status(thm)],[f262])).
% 232.71/35.34 fof(f264,plain,(
% 232.71/35.34 ![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))))))))),
% 232.71/35.34 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(W3,sK10_skl(W2,W1,W0))],[f263])).
% 232.71/35.34 fof(f266,plain,(
% 232.71/35.34 ![X0,X1,X2,X3]: (~aSet0(X0)|~aElementOf0(X1,szNzAzT0)|~X2=slbdtsldtrb0(X0,X1)|~aElementOf0(X3,X2)|aSubsetOf0(X3,X0))),
% 232.71/35.34 inference(cnf_transformation,[status(thm)],[f264])).
% 232.71/35.34 fof(f267,plain,(
% 232.71/35.34 ![X0,X1,X2,X3]: (~aSet0(X0)|~aElementOf0(X1,szNzAzT0)|~X2=slbdtsldtrb0(X0,X1)|~aElementOf0(X3,X2)|sbrdtbr0(X3)=X1)),
% 232.71/35.34 inference(cnf_transformation,[status(thm)],[f264])).
% 232.71/35.34 fof(f268,plain,(
% 232.71/35.34 ![X0,X1,X2,X3]: (~aSet0(X0)|~aElementOf0(X1,szNzAzT0)|~X2=slbdtsldtrb0(X0,X1)|aElementOf0(X3,X2)|~aSubsetOf0(X3,X0)|~sbrdtbr0(X3)=X1)),
% 232.71/35.34 inference(cnf_transformation,[status(thm)],[f264])).
% 232.71/35.34 fof(f288,plain,(
% 232.71/35.34 ![W0]: (~aFunction0(W0)|aSet0(szDzozmdt0(W0)))),
% 232.71/35.34 inference(pre_NNF_transformation,[status(thm)],[f64])).
% 232.71/35.34 fof(f289,plain,(
% 232.71/35.34 ![X0]: (~aFunction0(X0)|aSet0(szDzozmdt0(X0)))),
% 232.71/35.34 inference(cnf_transformation,[status(thm)],[f288])).
% 232.71/35.34 fof(f305,plain,(
% 232.71/35.34 ![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))))))))))),
% 232.71/35.34 inference(pre_NNF_transformation,[status(thm)],[f68])).
% 232.71/35.34 fof(f306,plain,(
% 232.71/35.34 ![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))))))))))))),
% 232.71/35.34 inference(NNF_transformation,[status(thm)],[f305])).
% 232.71/35.34 fof(f307,plain,(
% 232.71/35.34 ![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))))))))))))),
% 232.71/35.34 inference(miniscoping,[status(thm)],[f306])).
% 232.71/35.34 fof(f308,plain,(
% 232.71/35.34 ![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)))))))))))),
% 232.71/35.34 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))],[f307])).
% 232.71/35.34 fof(f312,plain,(
% 232.71/35.34 ![X0,X1,X2,X3,X4]: (~aFunction0(X0)|~aSubsetOf0(X1,szDzozmdt0(X0))|~X2=sdtlcdtrc0(X0,X1)|aElementOf0(X3,X2)|~aElementOf0(X4,X1)|~sdtlpdtrp0(X0,X4)=X3)),
% 232.71/35.34 inference(cnf_transformation,[status(thm)],[f308])).
% 232.71/35.34 fof(f336,plain,(
% 232.71/35.34 aSet0(xT)),
% 232.71/35.34 inference(cnf_transformation,[status(thm)],[f73])).
% 232.71/35.34 fof(f339,plain,(
% 232.71/35.34 aSubsetOf0(xS,szNzAzT0)),
% 232.71/35.34 inference(cnf_transformation,[status(thm)],[f75])).
% 232.71/35.34 fof(f340,plain,(
% 232.71/35.34 isCountable0(xS)),
% 232.71/35.34 inference(cnf_transformation,[status(thm)],[f75])).
% 232.71/35.34 fof(f341,plain,(
% 232.71/35.34 aFunction0(xc)),
% 232.71/35.34 inference(cnf_transformation,[status(thm)],[f76])).
% 232.71/35.34 fof(f342,plain,(
% 232.71/35.34 szDzozmdt0(xc)=slbdtsldtrb0(xS,xK)),
% 232.71/35.34 inference(cnf_transformation,[status(thm)],[f76])).
% 232.71/35.34 fof(f343,plain,(
% 232.71/35.34 aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT)),
% 232.71/35.34 inference(cnf_transformation,[status(thm)],[f76])).
% 232.71/35.34 fof(f350,plain,(
% 232.71/35.34 (xK=sz00&(![W0]: (~aElementOf0(W0,xT)|(![W1]: ((~aSubsetOf0(W1,xS)|~isCountable0(W1))|(?[W2]: (aElementOf0(W2,slbdtsldtrb0(W1,xK))&~sdtlpdtrp0(xc,W2)=W0)))))))),
% 232.71/35.34 inference(pre_NNF_transformation,[status(thm)],[f79])).
% 232.71/35.34 fof(f351,plain,(
% 232.71/35.34 xK=sz00&(![W0]: (~aElementOf0(W0,xT)|(![W1]: ((~aSubsetOf0(W1,xS)|~isCountable0(W1))|(aElementOf0(sK21_skl(W1,W0),slbdtsldtrb0(W1,xK))&~sdtlpdtrp0(xc,sK21_skl(W1,W0))=W0)))))),
% 232.71/35.34 inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl]),skolemize(W2,sK21_skl(W1,W0))],[f350])).
% 232.71/35.34 fof(f352,plain,(
% 232.71/35.34 xK=sz00),
% 232.71/35.34 inference(cnf_transformation,[status(thm)],[f351])).
% 232.71/35.34 fof(f353,plain,(
% 232.71/35.34 ![X0,X1]: (~aElementOf0(X0,xT)|~aSubsetOf0(X1,xS)|~isCountable0(X1)|aElementOf0(sK21_skl(X1,X0),slbdtsldtrb0(X1,xK)))),
% 232.71/35.34 inference(cnf_transformation,[status(thm)],[f351])).
% 232.71/35.34 fof(f354,plain,(
% 232.71/35.34 ![X0,X1]: (~aElementOf0(X0,xT)|~aSubsetOf0(X1,xS)|~isCountable0(X1)|~sdtlpdtrp0(xc,sK21_skl(X1,X0))=X0)),
% 232.71/35.34 inference(cnf_transformation,[status(thm)],[f351])).
% 232.71/35.34 fof(f361,plain,(
% 232.71/35.34 aSet0(slcrc0)),
% 232.71/35.34 inference(destructive_equality_resolution,[status(thm)],[f94])).
% 232.71/35.34 fof(f362,plain,(
% 232.71/35.34 ![X0]: (~aElementOf0(X0,slcrc0))),
% 232.71/35.34 inference(destructive_equality_resolution,[status(thm)],[f95])).
% 232.71/35.34 fof(f380,plain,(
% 232.71/35.34 ~aSet0(slcrc0)|sbrdtbr0(slcrc0)=sz00),
% 232.71/35.34 inference(destructive_equality_resolution,[status(thm)],[f203])).
% 232.71/35.34 fof(f381,plain,(
% 232.71/35.34 sbrdtbr0(slcrc0)=sz00),
% 232.71/35.34 inference(forward_subsumption_resolution,[status(thm)],[f380,f361])).
% 232.71/35.34 fof(f394,plain,(
% 232.71/35.34 ![X0,X1,X2]: (~aSet0(X0)|~aElementOf0(X1,szNzAzT0)|~aElementOf0(X2,slbdtsldtrb0(X0,X1))|aSubsetOf0(X2,X0))),
% 232.71/35.34 inference(destructive_equality_resolution,[status(thm)],[f266])).
% 232.71/35.34 fof(f395,plain,(
% 232.71/35.34 ![X0,X1,X2]: (~aSet0(X0)|~aElementOf0(X1,szNzAzT0)|~aElementOf0(X2,slbdtsldtrb0(X0,X1))|sbrdtbr0(X2)=X1)),
% 232.71/35.34 inference(destructive_equality_resolution,[status(thm)],[f267])).
% 232.71/35.34 fof(f396,plain,(
% 232.71/35.34 ![X0,X1]: (~aSet0(X0)|~aElementOf0(sbrdtbr0(X1),szNzAzT0)|aElementOf0(X1,slbdtsldtrb0(X0,sbrdtbr0(X1)))|~aSubsetOf0(X1,X0))),
% 232.71/35.34 inference(destructive_equality_resolution,[status(thm)],[f268])).
% 232.71/35.34 fof(f405,plain,(
% 232.71/35.34 ![X0,X1,X2]: (~aFunction0(X0)|~aSubsetOf0(X1,szDzozmdt0(X0))|aElementOf0(sdtlpdtrp0(X0,X2),sdtlcdtrc0(X0,X1))|~aElementOf0(X2,X1))),
% 232.71/35.34 inference(destructive_equality_resolution,[status(thm)],[f312])).
% 232.71/35.34 fof(f415,plain,(
% 232.71/35.34 szDzozmdt0(xc)=slbdtsldtrb0(xS,sz00)),
% 232.71/35.34 inference(backward_demodulation,[status(thm)],[f352,f342])).
% 232.71/35.34 fof(f417,plain,(
% 232.71/35.34 ![X0,X1]: (~aElementOf0(X0,xT)|~aSubsetOf0(X1,xS)|~isCountable0(X1)|aElementOf0(sK21_skl(X1,X0),slbdtsldtrb0(X1,sz00)))),
% 232.71/35.34 inference(forward_demodulation,[status(thm)],[f352,f353])).
% 232.71/35.34 fof(f420,plain,(
% 232.71/35.34 ![X0]: (~aElementOf0(X0,xT)|~aSubsetOf0(xS,xS)|aElementOf0(sK21_skl(xS,X0),slbdtsldtrb0(xS,sz00)))),
% 232.71/35.34 inference(resolution,[status(thm)],[f340,f417])).
% 232.71/35.34 fof(f421,plain,(
% 232.71/35.34 ![X0]: (~aElementOf0(X0,xT)|~aSubsetOf0(xS,xS)|aElementOf0(sK21_skl(xS,X0),szDzozmdt0(xc)))),
% 232.71/35.34 inference(forward_demodulation,[status(thm)],[f415,f420])).
% 232.71/35.34 fof(f434,plain,(
% 232.71/35.34 ~aSet0(szNzAzT0)|aSet0(xS)),
% 232.71/35.34 inference(resolution,[status(thm)],[f339,f108])).
% 232.71/35.34 fof(f436,plain,(
% 232.71/35.34 aSet0(xS)),
% 232.71/35.34 inference(forward_subsumption_resolution,[status(thm)],[f434,f156])).
% 232.71/35.34 fof(f437,plain,(
% 232.71/35.34 aSubsetOf0(xS,xS)),
% 232.71/35.34 inference(resolution,[status(thm)],[f436,f115])).
% 232.71/35.34 fof(f438,plain,(
% 232.71/35.34 ![X0]: (~aElementOf0(X0,xT)|aElementOf0(sK21_skl(xS,X0),szDzozmdt0(xc)))),
% 232.71/35.34 inference(backward_subsumption_resolution,[status(thm)],[f421,f437])).
% 232.71/35.34 fof(f445,plain,(
% 232.71/35.34 ![X0]: (~aSet0(X0)|aSubsetOf0(slcrc0,X0)|~aSet0(slcrc0))),
% 232.71/35.34 inference(resolution,[status(thm)],[f110,f362])).
% 232.71/35.34 fof(f447,plain,(
% 232.71/35.34 ![X0]: (~aSet0(X0)|aSubsetOf0(slcrc0,X0))),
% 232.71/35.34 inference(forward_subsumption_resolution,[status(thm)],[f445,f361])).
% 232.71/35.34 fof(f456,plain,(
% 232.71/35.34 ![X0]: (~aElementOf0(X0,xT)|~isCountable0(xS)|~sdtlpdtrp0(xc,sK21_skl(xS,X0))=X0)),
% 232.71/35.34 inference(resolution,[status(thm)],[f437,f354])).
% 232.71/35.34 fof(f460,plain,(
% 232.71/35.34 ![X0]: (~aElementOf0(X0,xT)|~sdtlpdtrp0(xc,sK21_skl(xS,X0))=X0)),
% 232.71/35.34 inference(forward_subsumption_resolution,[status(thm)],[f456,f340])).
% 232.71/35.34 fof(f477,plain,(
% 232.71/35.34 aSet0(szDzozmdt0(xc))),
% 232.71/35.34 inference(resolution,[status(thm)],[f289,f341])).
% 232.71/35.34 fof(f481,plain,(
% 232.71/35.34 aSubsetOf0(szDzozmdt0(xc),szDzozmdt0(xc))),
% 232.71/35.34 inference(resolution,[status(thm)],[f477,f115])).
% 232.71/35.34 fof(f554,plain,(
% 232.71/35.34 ![X0]: (~aSet0(xT)|~aElementOf0(X0,sdtlcdtrc0(xc,szDzozmdt0(xc)))|aElementOf0(X0,xT))),
% 232.71/35.34 inference(resolution,[status(thm)],[f343,f109])).
% 232.71/35.34 fof(f560,plain,(
% 232.71/35.34 ![X0]: (~aElementOf0(X0,sdtlcdtrc0(xc,szDzozmdt0(xc)))|aElementOf0(X0,xT))),
% 232.71/35.34 inference(forward_subsumption_resolution,[status(thm)],[f554,f336])).
% 232.71/35.34 fof(f568,plain,(
% 232.71/35.34 ![X0,X1]: (~aSet0(X0)|~aElementOf0(X1,slbdtsldtrb0(X0,sz00))|aSubsetOf0(X1,X0))),
% 232.71/35.34 inference(resolution,[status(thm)],[f394,f158])).
% 232.71/35.34 fof(f750,plain,(
% 232.71/35.34 ![X0,X1]: (~aSubsetOf0(X0,szDzozmdt0(xc))|aElementOf0(sdtlpdtrp0(xc,X1),sdtlcdtrc0(xc,X0))|~aElementOf0(X1,X0))),
% 232.71/35.34 inference(resolution,[status(thm)],[f405,f341])).
% 232.71/35.34 fof(f1353,plain,(
% 232.71/35.34 ![X0]: (~aSet0(xS)|~aElementOf0(X0,szDzozmdt0(xc))|aSubsetOf0(X0,xS))),
% 232.71/35.34 inference(paramodulation,[status(thm)],[f415,f568])).
% 232.71/35.34 fof(f1357,plain,(
% 232.71/35.34 ![X0]: (~aElementOf0(X0,szDzozmdt0(xc))|aSubsetOf0(X0,xS))),
% 232.71/35.34 inference(forward_subsumption_resolution,[status(thm)],[f1353,f436])).
% 232.71/35.34 fof(f1366,plain,(
% 232.71/35.34 ![X0]: (aSubsetOf0(sK21_skl(xS,X0),xS)|~aElementOf0(X0,xT))),
% 232.71/35.34 inference(resolution,[status(thm)],[f1357,f438])).
% 232.71/35.34 fof(f1812,plain,(
% 232.71/35.34 ![X0]: (~aSubsetOf0(szDzozmdt0(xc),szDzozmdt0(xc))|~aElementOf0(X0,szDzozmdt0(xc))|aElementOf0(sdtlpdtrp0(xc,X0),xT))),
% 232.71/35.34 inference(resolution,[status(thm)],[f750,f560])).
% 232.71/35.34 fof(f1815,plain,(
% 232.71/35.34 ![X0]: (~aElementOf0(X0,szDzozmdt0(xc))|aElementOf0(sdtlpdtrp0(xc,X0),xT))),
% 232.71/35.34 inference(forward_subsumption_resolution,[status(thm)],[f1812,f481])).
% 232.71/35.34 fof(f2133,plain,(
% 232.71/35.34 ![X0]: (~aSet0(xS)|~aElementOf0(sz00,szNzAzT0)|~aElementOf0(X0,szDzozmdt0(xc))|sbrdtbr0(X0)=sz00)),
% 232.71/35.34 inference(paramodulation,[status(thm)],[f415,f395])).
% 232.71/35.34 fof(f2137,plain,(
% 232.71/35.34 ![X0]: (~aElementOf0(sz00,szNzAzT0)|~aElementOf0(X0,szDzozmdt0(xc))|sbrdtbr0(X0)=sz00)),
% 232.71/35.34 inference(forward_subsumption_resolution,[status(thm)],[f2133,f436])).
% 232.71/35.34 fof(f2143,plain,(
% 232.71/35.34 ![X0]: (~aSet0(X0)|~aElementOf0(sz00,szNzAzT0)|aElementOf0(slcrc0,slbdtsldtrb0(X0,sbrdtbr0(slcrc0)))|~aSubsetOf0(slcrc0,X0))),
% 232.71/35.34 inference(paramodulation,[status(thm)],[f381,f396])).
% 232.71/35.34 fof(f2148,plain,(
% 232.71/35.34 ![X0]: (~aSet0(X0)|~aElementOf0(sz00,szNzAzT0)|aElementOf0(slcrc0,slbdtsldtrb0(X0,sz00))|~aSubsetOf0(slcrc0,X0))),
% 232.71/35.34 inference(forward_demodulation,[status(thm)],[f381,f2143])).
% 232.71/35.34 fof(f2149,plain,(
% 232.71/35.34 ![X0]: (~aSet0(X0)|aElementOf0(slcrc0,slbdtsldtrb0(X0,sz00))|~aSubsetOf0(slcrc0,X0))),
% 232.71/35.34 inference(forward_subsumption_resolution,[status(thm)],[f2148,f158])).
% 232.71/35.34 fof(f2150,plain,(
% 232.71/35.34 ![X0]: (~aElementOf0(X0,szDzozmdt0(xc))|sbrdtbr0(X0)=sz00)),
% 232.71/35.34 inference(resolution,[status(thm)],[f2137,f158])).
% 232.71/35.34 fof(f2151,plain,(
% 232.71/35.34 ![X0]: (sbrdtbr0(sK21_skl(xS,X0))=sz00|~aElementOf0(X0,xT))),
% 232.71/35.34 inference(resolution,[status(thm)],[f2150,f438])).
% 232.71/35.34 fof(f4397,plain,(
% 232.71/35.34 ~aSet0(xS)|aElementOf0(slcrc0,szDzozmdt0(xc))|~aSubsetOf0(slcrc0,xS)),
% 232.71/35.34 inference(paramodulation,[status(thm)],[f415,f2149])).
% 232.71/35.34 fof(f4402,plain,(
% 232.71/35.34 aElementOf0(slcrc0,szDzozmdt0(xc))|~aSubsetOf0(slcrc0,xS)),
% 232.71/35.34 inference(forward_subsumption_resolution,[status(thm)],[f4397,f436])).
% 232.71/35.34 fof(f4423,plain,(
% 232.71/35.34 aElementOf0(slcrc0,szDzozmdt0(xc))|~aSet0(xS)),
% 232.71/35.34 inference(resolution,[status(thm)],[f4402,f447])).
% 232.71/35.34 fof(f4424,plain,(
% 232.71/35.34 aElementOf0(slcrc0,szDzozmdt0(xc))),
% 232.71/35.34 inference(forward_subsumption_resolution,[status(thm)],[f4423,f436])).
% 232.71/35.34 fof(f9667,plain,(
% 232.71/35.34 aElementOf0(sdtlpdtrp0(xc,slcrc0),xT)),
% 232.71/35.34 inference(resolution,[status(thm)],[f1815,f4424])).
% 232.71/35.34 fof(f9675,plain,(
% 232.71/35.34 sbrdtbr0(sK21_skl(xS,sdtlpdtrp0(xc,slcrc0)))=sz00),
% 232.71/35.34 inference(resolution,[status(thm)],[f9667,f2151])).
% 232.71/35.34 fof(f9678,plain,(
% 232.71/35.34 aSubsetOf0(sK21_skl(xS,sdtlpdtrp0(xc,slcrc0)),xS)),
% 232.71/35.34 inference(resolution,[status(thm)],[f9667,f1366])).
% 232.71/35.34 fof(f9682,plain,(
% 232.71/35.34 ~sdtlpdtrp0(xc,sK21_skl(xS,sdtlpdtrp0(xc,slcrc0)))=sdtlpdtrp0(xc,slcrc0)),
% 232.71/35.34 inference(resolution,[status(thm)],[f9667,f460])).
% 232.71/35.34 fof(f10107,plain,(
% 232.71/35.34 ~aSet0(xS)|aSet0(sK21_skl(xS,sdtlpdtrp0(xc,slcrc0)))),
% 232.71/35.34 inference(resolution,[status(thm)],[f9678,f108])).
% 232.71/35.34 fof(f10112,plain,(
% 232.71/35.34 aSet0(sK21_skl(xS,sdtlpdtrp0(xc,slcrc0)))),
% 232.71/35.34 inference(forward_subsumption_resolution,[status(thm)],[f10107,f436])).
% 232.71/35.34 fof(f10127,plain,(
% 232.71/35.34 ~sbrdtbr0(sK21_skl(xS,sdtlpdtrp0(xc,slcrc0)))=sz00|sK21_skl(xS,sdtlpdtrp0(xc,slcrc0))=slcrc0),
% 232.71/35.34 inference(resolution,[status(thm)],[f10112,f202])).
% 232.71/35.34 fof(f10161,plain,(
% 232.71/35.34 ~sz00=sz00|sK21_skl(xS,sdtlpdtrp0(xc,slcrc0))=slcrc0),
% 232.71/35.34 inference(forward_demodulation,[status(thm)],[f9675,f10127])).
% 232.71/35.34 fof(f10203,plain,(
% 232.71/35.34 ~sdtlpdtrp0(xc,slcrc0)=sdtlpdtrp0(xc,slcrc0)),
% 232.71/35.34 inference(backward_demodulation,[status(thm)],[f10206,f9682])).
% 235.38/35.49 fof(f10206,plain,(
% 235.38/35.49 sK21_skl(xS,sdtlpdtrp0(xc,slcrc0))=slcrc0),
% 235.38/35.49 inference(trivial_equality_resolution,[status(thm)],[f10161])).
% 235.38/35.49 fof(f10270,plain,(
% 235.38/35.49 $false),
% 235.38/35.49 inference(trivial_equality_resolution,[status(thm)],[f10203])).
% 235.38/35.49 % SZS output end CNFRefutation for theBenchmark.p
% 14.58/35.54 % Elapsed time: 29.942011 seconds
% 14.58/35.54 % CPU time: 236.352283 seconds
% 14.58/35.54 % Total memory used: 875.549 MB
% 14.58/35.54 % Net memory used: 824.607 MB
%------------------------------------------------------------------------------