%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM566+3 : 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 : n018.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:14 PM UTC 2026
% Result : Theorem 15.98s 2.64s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : NUM566+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.37 % Computer : n018.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Mon Sep 21 02:41:58 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.43 % Drodi V4.1.1
% 15.98/2.64 % Refutation found
% 15.98/2.64 % SZS status Theorem for theBenchmark: Theorem is valid
% 15.98/2.64 % SZS output start CNFRefutation for theBenchmark
% 15.98/2.64 fof(f10,definition,(
% 15.98/2.64 (! [W0] :( aSet0(W0)=> (! [W1] :( aSubsetOf0(W1,W0)<=> ( aSet0(W1)& (! [W2] :( aElementOf0(W2,W1)=> aElementOf0(W2,W0) ) )) ) )) )),
% 15.98/2.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.98/2.64 fof(f12,axiom,(
% 15.98/2.64 (! [W0] :( aSet0(W0)=> aSubsetOf0(W0,W0) ) )),
% 15.98/2.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.98/2.64 fof(f42,axiom,(
% 15.98/2.64 (! [W0] :( aSet0(W0)=> ( sbrdtbr0(W0) = sz00<=> W0 = slcrc0 ) ) )),
% 15.98/2.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.98/2.64 fof(f64,axiom,(
% 15.98/2.64 (! [W0] :( aFunction0(W0)=> aSet0(szDzozmdt0(W0)) ) )),
% 15.98/2.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.98/2.64 fof(f68,definition,(
% 15.98/2.64 (! [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 ) )) )) ) )) )) )),
% 15.98/2.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.98/2.64 fof(f75,hypothesis,(
% 15.98/2.64 ( aSet0(xS)& (! [W0] :( aElementOf0(W0,xS)=> aElementOf0(W0,szNzAzT0) ))& aSubsetOf0(xS,szNzAzT0)& isCountable0(xS) ) ),
% 15.98/2.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.98/2.64 fof(f76,hypothesis,(
% 15.98/2.64 ( aFunction0(xc)& (! [W0] :( ( aElementOf0(W0,szDzozmdt0(xc))=> ( aSet0(W0)& (! [W1] :( aElementOf0(W1,W0)=> aElementOf0(W1,xS) ))& aSubsetOf0(W0,xS)& sbrdtbr0(W0) = xK ) )& ( ( ( ( aSet0(W0)& (! [W1] :( aElementOf0(W1,W0)=> aElementOf0(W1,xS) ) ))| aSubsetOf0(W0,xS) )& sbrdtbr0(W0) = xK )=> aElementOf0(W0,szDzozmdt0(xc)) ) ))& szDzozmdt0(xc) = slbdtsldtrb0(xS,xK)& aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc)))& (! [W0] :( aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc)))<=> (? [W1] :( aElementOf0(W1,szDzozmdt0(xc))& sdtlpdtrp0(xc,W1) = W0 ) )))& (! [W0] :( aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc)))=> aElementOf0(W0,xT) ))& aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT) ) ),
% 15.98/2.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.98/2.64 fof(f78,hypothesis,(
% 15.98/2.64 xK = sz00 ),
% 15.98/2.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.98/2.64 fof(f79,hypothesis,(
% 15.98/2.64 ( aSet0(slcrc0)& ~ (? [W0] : aElementOf0(W0,slcrc0))& (! [W0] :( aElementOf0(W0,slcrc0)=> aElementOf0(W0,xS) ))& aSubsetOf0(slcrc0,xS)& aElementOf0(slcrc0,slbdtsldtrb0(xS,sz00)) ) ),
% 15.98/2.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.98/2.64 fof(f81,conjecture,(
% 15.98/2.64 (? [W0] :( aElementOf0(W0,xT)& (? [W1] :( ( ( aSet0(W1)& (! [W2] :( aElementOf0(W2,W1)=> aElementOf0(W2,xS) ) ))| aSubsetOf0(W1,xS) )& isCountable0(W1)& (! [W2] :( ( aSet0(W2)& (! [W3] :( aElementOf0(W3,W2)=> aElementOf0(W3,W1) ))& aSubsetOf0(W2,W1)& sbrdtbr0(W2) = xK& aElementOf0(W2,slbdtsldtrb0(W1,xK)) )=> sdtlpdtrp0(xc,W2) = W0 ) )) )) )),
% 15.98/2.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.98/2.64 fof(f82,negated_conjecture,(
% 15.98/2.64 ~((? [W0] :( aElementOf0(W0,xT)& (? [W1] :( ( ( aSet0(W1)& (! [W2] :( aElementOf0(W2,W1)=> aElementOf0(W2,xS) ) ))| aSubsetOf0(W1,xS) )& isCountable0(W1)& (! [W2] :( ( aSet0(W2)& (! [W3] :( aElementOf0(W3,W2)=> aElementOf0(W3,W1) ))& aSubsetOf0(W2,W1)& sbrdtbr0(W2) = xK& aElementOf0(W2,slbdtsldtrb0(W1,xK)) )=> sdtlpdtrp0(xc,W2) = W0 ) )) )) ))),
% 15.98/2.64 inference(negated_conjecture,[status(cth)],[f81])).
% 15.98/2.64 fof(f107,plain,(
% 15.98/2.64 ![W0]: (~aSet0(W0)|(![W1]: (aSubsetOf0(W1,W0)<=>(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0)))))))),
% 15.98/2.64 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 15.98/2.64 fof(f108,plain,(
% 15.98/2.64 ![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))))))))),
% 15.98/2.64 inference(NNF_transformation,[status(thm)],[f107])).
% 15.98/2.64 fof(f109,plain,(
% 15.98/2.64 ![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))))))))),
% 15.98/2.64 inference(miniscoping,[status(thm)],[f108])).
% 15.98/2.64 fof(f110,plain,(
% 15.98/2.64 ![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)))))))),
% 15.98/2.64 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W2,sK1_skl(W1,W0))],[f109])).
% 15.98/2.64 fof(f111,plain,(
% 15.98/2.64 ![X0,X1]: (~aSet0(X0)|~aSubsetOf0(X1,X0)|aSet0(X1))),
% 15.98/2.64 inference(cnf_transformation,[status(thm)],[f110])).
% 15.98/2.64 fof(f117,plain,(
% 15.98/2.64 ![W0]: (~aSet0(W0)|aSubsetOf0(W0,W0))),
% 15.98/2.64 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 15.98/2.64 fof(f118,plain,(
% 15.98/2.64 ![X0]: (~aSet0(X0)|aSubsetOf0(X0,X0))),
% 15.98/2.64 inference(cnf_transformation,[status(thm)],[f117])).
% 15.98/2.64 fof(f203,plain,(
% 15.98/2.64 ![W0]: (~aSet0(W0)|(sbrdtbr0(W0)=sz00<=>W0=slcrc0))),
% 15.98/2.64 inference(pre_NNF_transformation,[status(thm)],[f42])).
% 15.98/2.64 fof(f204,plain,(
% 15.98/2.64 ![W0]: (~aSet0(W0)|((~sbrdtbr0(W0)=sz00|W0=slcrc0)&(sbrdtbr0(W0)=sz00|~W0=slcrc0)))),
% 15.98/2.64 inference(NNF_transformation,[status(thm)],[f203])).
% 15.98/2.64 fof(f205,plain,(
% 15.98/2.64 ![X0]: (~aSet0(X0)|~sbrdtbr0(X0)=sz00|X0=slcrc0)),
% 15.98/2.64 inference(cnf_transformation,[status(thm)],[f204])).
% 15.98/2.64 fof(f291,plain,(
% 15.98/2.64 ![W0]: (~aFunction0(W0)|aSet0(szDzozmdt0(W0)))),
% 15.98/2.64 inference(pre_NNF_transformation,[status(thm)],[f64])).
% 15.98/2.64 fof(f292,plain,(
% 15.98/2.64 ![X0]: (~aFunction0(X0)|aSet0(szDzozmdt0(X0)))),
% 15.98/2.64 inference(cnf_transformation,[status(thm)],[f291])).
% 15.98/2.64 fof(f308,plain,(
% 15.98/2.64 ![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))))))))))),
% 15.98/2.64 inference(pre_NNF_transformation,[status(thm)],[f68])).
% 15.98/2.64 fof(f309,plain,(
% 15.98/2.64 ![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))))))))))))),
% 15.98/2.64 inference(NNF_transformation,[status(thm)],[f308])).
% 15.98/2.64 fof(f310,plain,(
% 15.98/2.64 ![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))))))))))))),
% 15.98/2.64 inference(miniscoping,[status(thm)],[f309])).
% 15.98/2.64 fof(f311,plain,(
% 15.98/2.64 ![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)))))))))))),
% 15.98/2.64 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))],[f310])).
% 15.98/2.64 fof(f315,plain,(
% 15.98/2.64 ![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)),
% 15.98/2.64 inference(cnf_transformation,[status(thm)],[f311])).
% 15.98/2.64 fof(f342,plain,(
% 15.98/2.64 ((aSet0(xS)&(![W0]: (~aElementOf0(W0,xS)|aElementOf0(W0,szNzAzT0))))&aSubsetOf0(xS,szNzAzT0))&isCountable0(xS)),
% 15.98/2.64 inference(pre_NNF_transformation,[status(thm)],[f75])).
% 15.98/2.64 fof(f343,plain,(
% 15.98/2.64 aSet0(xS)),
% 15.98/2.64 inference(cnf_transformation,[status(thm)],[f342])).
% 15.98/2.64 fof(f346,plain,(
% 15.98/2.64 isCountable0(xS)),
% 15.98/2.64 inference(cnf_transformation,[status(thm)],[f342])).
% 15.98/2.64 fof(f347,plain,(
% 15.98/2.64 (((((aFunction0(xc)&(![W0]: ((~aElementOf0(W0,szDzozmdt0(xc))|(((aSet0(W0)&(![W1]: (~aElementOf0(W1,W0)|aElementOf0(W1,xS))))&aSubsetOf0(W0,xS))&sbrdtbr0(W0)=xK))&((((~aSet0(W0)|(?[W1]: (aElementOf0(W1,W0)&~aElementOf0(W1,xS))))&~aSubsetOf0(W0,xS))|~sbrdtbr0(W0)=xK)|aElementOf0(W0,szDzozmdt0(xc))))))&szDzozmdt0(xc)=slbdtsldtrb0(xS,xK))&aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc))))&(![W0]: (aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc)))<=>(?[W1]: (aElementOf0(W1,szDzozmdt0(xc))&sdtlpdtrp0(xc,W1)=W0)))))&(![W0]: (~aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc)))|aElementOf0(W0,xT))))&aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT)),
% 15.98/2.64 inference(pre_NNF_transformation,[status(thm)],[f76])).
% 15.98/2.64 fof(f348,plain,(
% 15.98/2.64 (((((aFunction0(xc)&(![W0]: ((~aElementOf0(W0,szDzozmdt0(xc))|(((aSet0(W0)&(![W1]: (~aElementOf0(W1,W0)|aElementOf0(W1,xS))))&aSubsetOf0(W0,xS))&sbrdtbr0(W0)=xK))&((((~aSet0(W0)|(?[W1]: (aElementOf0(W1,W0)&~aElementOf0(W1,xS))))&~aSubsetOf0(W0,xS))|~sbrdtbr0(W0)=xK)|aElementOf0(W0,szDzozmdt0(xc))))))&szDzozmdt0(xc)=slbdtsldtrb0(xS,xK))&aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc))))&(![W0]: ((~aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc)))|(?[W1]: (aElementOf0(W1,szDzozmdt0(xc))&sdtlpdtrp0(xc,W1)=W0)))&(aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc)))|(![W1]: (~aElementOf0(W1,szDzozmdt0(xc))|~sdtlpdtrp0(xc,W1)=W0))))))&(![W0]: (~aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc)))|aElementOf0(W0,xT))))&aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT)),
% 15.98/2.64 inference(NNF_transformation,[status(thm)],[f347])).
% 15.98/2.64 fof(f349,plain,(
% 15.98/2.64 (((((aFunction0(xc)&((![W0]: (~aElementOf0(W0,szDzozmdt0(xc))|(((aSet0(W0)&(![W1]: (~aElementOf0(W1,W0)|aElementOf0(W1,xS))))&aSubsetOf0(W0,xS))&sbrdtbr0(W0)=xK)))&(![W0]: ((((~aSet0(W0)|(?[W1]: (aElementOf0(W1,W0)&~aElementOf0(W1,xS))))&~aSubsetOf0(W0,xS))|~sbrdtbr0(W0)=xK)|aElementOf0(W0,szDzozmdt0(xc))))))&szDzozmdt0(xc)=slbdtsldtrb0(xS,xK))&aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc))))&((![W0]: (~aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc)))|(?[W1]: (aElementOf0(W1,szDzozmdt0(xc))&sdtlpdtrp0(xc,W1)=W0))))&(![W0]: (aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc)))|(![W1]: (~aElementOf0(W1,szDzozmdt0(xc))|~sdtlpdtrp0(xc,W1)=W0))))))&(![W0]: (~aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc)))|aElementOf0(W0,xT))))&aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT)),
% 15.98/2.64 inference(miniscoping,[status(thm)],[f348])).
% 15.98/2.64 fof(f350,plain,(
% 15.98/2.64 (((((aFunction0(xc)&((![W0]: (~aElementOf0(W0,szDzozmdt0(xc))|(((aSet0(W0)&(![W1]: (~aElementOf0(W1,W0)|aElementOf0(W1,xS))))&aSubsetOf0(W0,xS))&sbrdtbr0(W0)=xK)))&(![W0]: ((((~aSet0(W0)|(aElementOf0(sK19_skl(W0),W0)&~aElementOf0(sK19_skl(W0),xS)))&~aSubsetOf0(W0,xS))|~sbrdtbr0(W0)=xK)|aElementOf0(W0,szDzozmdt0(xc))))))&szDzozmdt0(xc)=slbdtsldtrb0(xS,xK))&aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc))))&((![W0]: (~aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc)))|(aElementOf0(sK20_skl(W0),szDzozmdt0(xc))&sdtlpdtrp0(xc,sK20_skl(W0))=W0)))&(![W0]: (aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc)))|(![W1]: (~aElementOf0(W1,szDzozmdt0(xc))|~sdtlpdtrp0(xc,W1)=W0))))))&(![W0]: (~aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc)))|aElementOf0(W0,xT))))&aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT)),
% 15.98/2.64 inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl,sK20_skl]),skolemize(W1,sK19_skl(W0)),skolemize(W1,sK20_skl(W0))],[f349])).
% 15.98/2.64 fof(f351,plain,(
% 15.98/2.64 aFunction0(xc)),
% 15.98/2.64 inference(cnf_transformation,[status(thm)],[f350])).
% 15.98/2.64 fof(f359,plain,(
% 15.98/2.64 szDzozmdt0(xc)=slbdtsldtrb0(xS,xK)),
% 15.98/2.64 inference(cnf_transformation,[status(thm)],[f350])).
% 15.98/2.64 fof(f364,plain,(
% 15.98/2.64 ![X0]: (~aElementOf0(X0,sdtlcdtrc0(xc,szDzozmdt0(xc)))|aElementOf0(X0,xT))),
% 15.98/2.64 inference(cnf_transformation,[status(thm)],[f350])).
% 15.98/2.64 fof(f375,plain,(
% 15.98/2.64 xK=sz00),
% 15.98/2.64 inference(cnf_transformation,[status(thm)],[f78])).
% 15.98/2.64 fof(f376,plain,(
% 15.98/2.64 (((aSet0(slcrc0)&(![W0]: ~aElementOf0(W0,slcrc0)))&(![W0]: (~aElementOf0(W0,slcrc0)|aElementOf0(W0,xS))))&aSubsetOf0(slcrc0,xS))&aElementOf0(slcrc0,slbdtsldtrb0(xS,sz00))),
% 15.98/2.64 inference(pre_NNF_transformation,[status(thm)],[f79])).
% 15.98/2.64 fof(f381,plain,(
% 15.98/2.64 aElementOf0(slcrc0,slbdtsldtrb0(xS,sz00))),
% 15.98/2.64 inference(cnf_transformation,[status(thm)],[f376])).
% 15.98/2.64 fof(f388,plain,(
% 15.98/2.64 (![W0]: (~aElementOf0(W0,xT)|(![W1]: ((((~aSet0(W1)|(?[W2]: (aElementOf0(W2,W1)&~aElementOf0(W2,xS))))&~aSubsetOf0(W1,xS))|~isCountable0(W1))|(?[W2]: (((((aSet0(W2)&(![W3]: (~aElementOf0(W3,W2)|aElementOf0(W3,W1))))&aSubsetOf0(W2,W1))&sbrdtbr0(W2)=xK)&aElementOf0(W2,slbdtsldtrb0(W1,xK)))&~sdtlpdtrp0(xc,W2)=W0))))))),
% 16.61/2.66 inference(pre_NNF_transformation,[status(thm)],[f82])).
% 16.61/2.66 fof(f389,definition,(
% 16.61/2.66 ![W1]: (sP5_prd(W1)<=>(((~aSet0(W1)|(?[W2]: (aElementOf0(W2,W1)&~aElementOf0(W2,xS))))&~aSubsetOf0(W1,xS))|~isCountable0(W1)))),
% 16.61/2.66 introduced(definition,[new_symbols(definition,[sP5_prd])],[])).
% 16.61/2.66 fof(f390,plain,(
% 16.61/2.66 ![W0]: (~aElementOf0(W0,xT)|(![W1]: (sP5_prd(W1)|(?[W2]: (((((aSet0(W2)&(![W3]: (~aElementOf0(W3,W2)|aElementOf0(W3,W1))))&aSubsetOf0(W2,W1))&sbrdtbr0(W2)=xK)&aElementOf0(W2,slbdtsldtrb0(W1,xK)))&~sdtlpdtrp0(xc,W2)=W0)))))),
% 16.61/2.66 inference(formula_renaming,[status(thm)],[f388,f389])).
% 16.61/2.66 fof(f391,plain,(
% 16.61/2.66 ![W0]: (~aElementOf0(W0,xT)|(![W1]: (sP5_prd(W1)|(((((aSet0(sK23_skl(W1,W0))&(![W3]: (~aElementOf0(W3,sK23_skl(W1,W0))|aElementOf0(W3,W1))))&aSubsetOf0(sK23_skl(W1,W0),W1))&sbrdtbr0(sK23_skl(W1,W0))=xK)&aElementOf0(sK23_skl(W1,W0),slbdtsldtrb0(W1,xK)))&~sdtlpdtrp0(xc,sK23_skl(W1,W0))=W0))))),
% 16.61/2.66 inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl]),skolemize(W2,sK23_skl(W1,W0))],[f390])).
% 16.61/2.66 fof(f394,plain,(
% 16.61/2.66 ![X0,X1]: (~aElementOf0(X0,xT)|sP5_prd(X1)|aSubsetOf0(sK23_skl(X1,X0),X1))),
% 16.61/2.66 inference(cnf_transformation,[status(thm)],[f391])).
% 16.61/2.66 fof(f395,plain,(
% 16.61/2.66 ![X0,X1]: (~aElementOf0(X0,xT)|sP5_prd(X1)|sbrdtbr0(sK23_skl(X1,X0))=xK)),
% 16.61/2.66 inference(cnf_transformation,[status(thm)],[f391])).
% 16.61/2.66 fof(f397,plain,(
% 16.61/2.66 ![X0,X1]: (~aElementOf0(X0,xT)|sP5_prd(X1)|~sdtlpdtrp0(xc,sK23_skl(X1,X0))=X0)),
% 16.61/2.66 inference(cnf_transformation,[status(thm)],[f391])).
% 16.61/2.66 fof(f459,plain,(
% 16.61/2.66 ![W1]: ((~sP5_prd(W1)|(((~aSet0(W1)|(?[W2]: (aElementOf0(W2,W1)&~aElementOf0(W2,xS))))&~aSubsetOf0(W1,xS))|~isCountable0(W1)))&(sP5_prd(W1)|(((aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,xS))))|aSubsetOf0(W1,xS))&isCountable0(W1))))),
% 16.61/2.66 inference(NNF_transformation,[status(thm)],[f389])).
% 16.61/2.66 fof(f460,plain,(
% 16.61/2.66 (![W1]: (~sP5_prd(W1)|(((~aSet0(W1)|(?[W2]: (aElementOf0(W2,W1)&~aElementOf0(W2,xS))))&~aSubsetOf0(W1,xS))|~isCountable0(W1))))&(![W1]: (sP5_prd(W1)|(((aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,xS))))|aSubsetOf0(W1,xS))&isCountable0(W1))))),
% 16.61/2.66 inference(miniscoping,[status(thm)],[f459])).
% 16.61/2.66 fof(f461,plain,(
% 16.61/2.66 (![W1]: (~sP5_prd(W1)|(((~aSet0(W1)|(aElementOf0(sK36_skl(W1),W1)&~aElementOf0(sK36_skl(W1),xS)))&~aSubsetOf0(W1,xS))|~isCountable0(W1))))&(![W1]: (sP5_prd(W1)|(((aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,xS))))|aSubsetOf0(W1,xS))&isCountable0(W1))))),
% 16.61/2.66 inference(skolemize,[status(esa),new_symbols(skolem,[sK36_skl]),skolemize(W2,sK36_skl(W1))],[f460])).
% 16.61/2.66 fof(f464,plain,(
% 16.61/2.66 ![X0]: (~sP5_prd(X0)|~aSubsetOf0(X0,xS)|~isCountable0(X0))),
% 16.61/2.66 inference(cnf_transformation,[status(thm)],[f461])).
% 16.61/2.66 fof(f527,plain,(
% 16.61/2.66 ![X0,X1,X2]: (~aFunction0(X0)|~aSubsetOf0(X1,szDzozmdt0(X0))|aElementOf0(sdtlpdtrp0(X0,X2),sdtlcdtrc0(X0,X1))|~aElementOf0(X2,X1))),
% 16.61/2.66 inference(destructive_equality_resolution,[status(thm)],[f315])).
% 16.61/2.66 fof(f538,plain,(
% 16.61/2.66 ![X0]: (~aSet0(X0)|~sbrdtbr0(X0)=xK|X0=slcrc0)),
% 16.61/2.66 inference(backward_demodulation,[status(thm)],[f375,f205])).
% 16.61/2.66 fof(f545,plain,(
% 16.61/2.66 aElementOf0(slcrc0,slbdtsldtrb0(xS,xK))),
% 16.61/2.66 inference(forward_demodulation,[status(thm)],[f375,f381])).
% 16.61/2.66 fof(f546,plain,(
% 16.61/2.66 aElementOf0(slcrc0,szDzozmdt0(xc))),
% 16.61/2.66 inference(forward_demodulation,[status(thm)],[f359,f545])).
% 16.61/2.66 fof(f708,plain,(
% 16.61/2.66 ![X0]: (~aSubsetOf0(X0,xS)|aSet0(X0))),
% 16.61/2.66 inference(resolution,[status(thm)],[f343,f111])).
% 16.61/2.66 fof(f709,plain,(
% 16.61/2.66 aSubsetOf0(xS,xS)),
% 16.61/2.66 inference(resolution,[status(thm)],[f343,f118])).
% 16.61/2.66 fof(f716,plain,(
% 16.61/2.66 ~sP5_prd(xS)|~isCountable0(xS)),
% 16.61/2.66 inference(resolution,[status(thm)],[f709,f464])).
% 16.61/2.66 fof(f719,plain,(
% 16.61/2.66 ~sP5_prd(xS)),
% 16.61/2.66 inference(forward_subsumption_resolution,[status(thm)],[f716,f346])).
% 16.61/2.66 fof(f788,plain,(
% 16.61/2.66 ![X0]: (~aElementOf0(X0,xT)|~sdtlpdtrp0(xc,sK23_skl(xS,X0))=X0)),
% 16.61/2.66 inference(resolution,[status(thm)],[f719,f397])).
% 16.61/2.66 fof(f789,plain,(
% 16.61/2.66 ![X0]: (~aElementOf0(X0,xT)|sbrdtbr0(sK23_skl(xS,X0))=xK)),
% 16.61/2.68 inference(resolution,[status(thm)],[f719,f395])).
% 16.61/2.68 fof(f834,plain,(
% 16.61/2.68 aSet0(szDzozmdt0(xc))),
% 16.61/2.68 inference(resolution,[status(thm)],[f292,f351])).
% 16.61/2.68 fof(f848,plain,(
% 16.61/2.68 aSubsetOf0(szDzozmdt0(xc),szDzozmdt0(xc))),
% 16.61/2.68 inference(resolution,[status(thm)],[f834,f118])).
% 16.61/2.68 fof(f935,plain,(
% 16.61/2.68 ![X0,X1]: (~aSubsetOf0(X0,szDzozmdt0(xc))|aElementOf0(sdtlpdtrp0(xc,X1),sdtlcdtrc0(xc,X0))|~aElementOf0(X1,X0))),
% 16.61/2.68 inference(resolution,[status(thm)],[f527,f351])).
% 16.61/2.68 fof(f937,plain,(
% 16.61/2.68 ![X0]: (~aSubsetOf0(szDzozmdt0(xc),szDzozmdt0(xc))|~aElementOf0(X0,szDzozmdt0(xc))|aElementOf0(sdtlpdtrp0(xc,X0),xT))),
% 16.61/2.68 inference(resolution,[status(thm)],[f935,f364])).
% 16.61/2.68 fof(f939,plain,(
% 16.61/2.68 ![X0]: (~aElementOf0(X0,szDzozmdt0(xc))|aElementOf0(sdtlpdtrp0(xc,X0),xT))),
% 16.61/2.68 inference(forward_subsumption_resolution,[status(thm)],[f937,f848])).
% 16.61/2.68 fof(f941,plain,(
% 16.61/2.68 aElementOf0(sdtlpdtrp0(xc,slcrc0),xT)),
% 16.61/2.68 inference(resolution,[status(thm)],[f939,f546])).
% 16.61/2.68 fof(f943,plain,(
% 16.61/2.68 ~sdtlpdtrp0(xc,sK23_skl(xS,sdtlpdtrp0(xc,slcrc0)))=sdtlpdtrp0(xc,slcrc0)),
% 16.61/2.68 inference(resolution,[status(thm)],[f941,f788])).
% 16.61/2.68 fof(f945,plain,(
% 16.61/2.68 sbrdtbr0(sK23_skl(xS,sdtlpdtrp0(xc,slcrc0)))=xK),
% 16.61/2.68 inference(resolution,[status(thm)],[f941,f789])).
% 16.61/2.68 fof(f949,plain,(
% 16.61/2.68 ![X0]: (sP5_prd(X0)|aSubsetOf0(sK23_skl(X0,sdtlpdtrp0(xc,slcrc0)),X0))),
% 16.61/2.68 inference(resolution,[status(thm)],[f941,f394])).
% 16.61/2.68 fof(f2111,plain,(
% 16.61/2.68 sP5_prd(xS)|aSet0(sK23_skl(xS,sdtlpdtrp0(xc,slcrc0)))),
% 16.61/2.68 inference(resolution,[status(thm)],[f949,f708])).
% 16.61/2.68 fof(f2116,plain,(
% 16.61/2.68 aSet0(sK23_skl(xS,sdtlpdtrp0(xc,slcrc0)))),
% 16.61/2.68 inference(forward_subsumption_resolution,[status(thm)],[f2111,f719])).
% 16.61/2.68 fof(f2222,plain,(
% 16.61/2.68 ~sbrdtbr0(sK23_skl(xS,sdtlpdtrp0(xc,slcrc0)))=xK|sK23_skl(xS,sdtlpdtrp0(xc,slcrc0))=slcrc0),
% 16.61/2.68 inference(resolution,[status(thm)],[f538,f2116])).
% 16.61/2.68 fof(f2226,plain,(
% 16.61/2.68 ~xK=xK|sK23_skl(xS,sdtlpdtrp0(xc,slcrc0))=slcrc0),
% 16.61/2.68 inference(forward_demodulation,[status(thm)],[f945,f2222])).
% 16.61/2.68 fof(f2253,plain,(
% 16.61/2.68 ~sdtlpdtrp0(xc,slcrc0)=sdtlpdtrp0(xc,slcrc0)),
% 16.61/2.68 inference(backward_demodulation,[status(thm)],[f2254,f943])).
% 16.61/2.68 fof(f2254,plain,(
% 16.61/2.68 sK23_skl(xS,sdtlpdtrp0(xc,slcrc0))=slcrc0),
% 16.61/2.68 inference(trivial_equality_resolution,[status(thm)],[f2226])).
% 16.61/2.68 fof(f2269,plain,(
% 16.61/2.68 $false),
% 16.61/2.68 inference(trivial_equality_resolution,[status(thm)],[f2253])).
% 16.61/2.68 % SZS output end CNFRefutation for theBenchmark.p
% 16.61/2.70 % Elapsed time: 2.298315 seconds
% 16.61/2.70 % CPU time: 17.535666 seconds
% 16.61/2.70 % Total memory used: 237.217 MB
% 16.61/2.70 % Net memory used: 226.452 MB
%------------------------------------------------------------------------------