%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM563+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 : n008.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 13.73s 7.53s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : NUM563+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/5.43 % Computer : n008.cluster.edu
% 0.16/5.43 % Model : x86_64 x86_64
% 0.16/5.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/5.43 % Memory : 8046.5625MB
% 0.16/5.43 % OS : Linux 6.8.0-71-generic
% 0.16/5.43 % CPULimit : 300
% 0.16/5.43 % WCLimit : 300
% 0.16/5.43 % DateTime : Mon Sep 21 02:40:59 UTC 2026
% 0.16/5.43 % CPUTime :
% 0.16/5.46 % Drodi V4.1.1
% 13.73/7.53 % Refutation found
% 13.73/7.53 % SZS status Theorem for theBenchmark: Theorem is valid
% 13.73/7.53 % SZS output start CNFRefutation for theBenchmark
% 13.73/7.53 fof(f5,definition,(
% 13.73/7.53 (! [W0] :( W0 = slcrc0<=> ( aSet0(W0)& ~ (? [W1] : aElementOf0(W1,W0) )) ) )),
% 13.73/7.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.73/7.53 fof(f10,definition,(
% 13.73/7.53 (! [W0] :( aSet0(W0)=> (! [W1] :( aSubsetOf0(W1,W0)<=> ( aSet0(W1)& (! [W2] :( aElementOf0(W2,W1)=> aElementOf0(W2,W0) ) )) ) )) )),
% 13.73/7.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.73/7.53 fof(f12,axiom,(
% 13.73/7.53 (! [W0] :( aSet0(W0)=> aSubsetOf0(W0,W0) ) )),
% 13.73/7.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.73/7.53 fof(f42,axiom,(
% 13.73/7.53 (! [W0] :( aSet0(W0)=> ( sbrdtbr0(W0) = sz00<=> W0 = slcrc0 ) ) )),
% 13.73/7.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.73/7.53 fof(f75,hypothesis,(
% 13.73/7.53 ( aSet0(xS)& (! [W0] :( aElementOf0(W0,xS)=> aElementOf0(W0,szNzAzT0) ))& aSubsetOf0(xS,szNzAzT0)& isCountable0(xS) ) ),
% 13.73/7.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.73/7.53 fof(f76,hypothesis,(
% 13.73/7.53 ( 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) ) ),
% 13.73/7.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.73/7.53 fof(f78,conjecture,(
% 13.73/7.53 ( xK = sz00=> (? [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 ) )) )) )) ),
% 13.73/7.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.73/7.53 fof(f79,negated_conjecture,(
% 13.73/7.53 ~(( xK = sz00=> (? [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 ) )) )) )) )),
% 13.73/7.53 inference(negated_conjecture,[status(cth)],[f78])).
% 13.73/7.53 fof(f90,plain,(
% 13.73/7.53 ![W0]: (W0=slcrc0<=>(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0))))),
% 13.73/7.53 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 13.73/7.53 fof(f91,plain,(
% 13.73/7.53 ![W0]: ((~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0))))&(W0=slcrc0|(~aSet0(W0)|(?[W1]: aElementOf0(W1,W0)))))),
% 13.73/7.53 inference(NNF_transformation,[status(thm)],[f90])).
% 13.73/7.53 fof(f92,plain,(
% 13.73/7.53 (![W0]: (~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0)))))&(![W0]: (W0=slcrc0|(~aSet0(W0)|(?[W1]: aElementOf0(W1,W0)))))),
% 13.73/7.53 inference(miniscoping,[status(thm)],[f91])).
% 13.73/7.53 fof(f93,plain,(
% 13.73/7.53 (![W0]: (~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0)))))&(![W0]: (W0=slcrc0|(~aSet0(W0)|aElementOf0(sK0_skl(W0),W0))))),
% 13.73/7.53 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(W1,sK0_skl(W0))],[f92])).
% 13.73/7.53 fof(f94,plain,(
% 13.73/7.53 ![X0]: (~X0=slcrc0|aSet0(X0))),
% 13.73/7.53 inference(cnf_transformation,[status(thm)],[f93])).
% 13.73/7.53 fof(f95,plain,(
% 13.73/7.53 ![X0,X1]: (~X0=slcrc0|~aElementOf0(X1,X0))),
% 13.73/7.53 inference(cnf_transformation,[status(thm)],[f93])).
% 13.73/7.53 fof(f104,plain,(
% 13.73/7.53 ![W0]: (~aSet0(W0)|(![W1]: (aSubsetOf0(W1,W0)<=>(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0)))))))),
% 13.73/7.53 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 13.73/7.53 fof(f105,plain,(
% 13.73/7.53 ![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))))))))),
% 13.73/7.53 inference(NNF_transformation,[status(thm)],[f104])).
% 13.73/7.53 fof(f106,plain,(
% 13.73/7.53 ![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))))))))),
% 13.73/7.53 inference(miniscoping,[status(thm)],[f105])).
% 13.73/7.53 fof(f107,plain,(
% 13.73/7.53 ![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)))))))),
% 13.73/7.53 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W2,sK1_skl(W1,W0))],[f106])).
% 13.73/7.53 fof(f110,plain,(
% 13.73/7.53 ![X0,X1]: (~aSet0(X0)|aSubsetOf0(X1,X0)|~aSet0(X1)|aElementOf0(sK1_skl(X1,X0),X1))),
% 13.73/7.53 inference(cnf_transformation,[status(thm)],[f107])).
% 13.73/7.53 fof(f114,plain,(
% 13.73/7.53 ![W0]: (~aSet0(W0)|aSubsetOf0(W0,W0))),
% 13.73/7.53 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 13.73/7.53 fof(f115,plain,(
% 13.73/7.53 ![X0]: (~aSet0(X0)|aSubsetOf0(X0,X0))),
% 13.73/7.53 inference(cnf_transformation,[status(thm)],[f114])).
% 13.73/7.53 fof(f200,plain,(
% 13.73/7.53 ![W0]: (~aSet0(W0)|(sbrdtbr0(W0)=sz00<=>W0=slcrc0))),
% 13.73/7.53 inference(pre_NNF_transformation,[status(thm)],[f42])).
% 13.73/7.53 fof(f201,plain,(
% 13.73/7.53 ![W0]: (~aSet0(W0)|((~sbrdtbr0(W0)=sz00|W0=slcrc0)&(sbrdtbr0(W0)=sz00|~W0=slcrc0)))),
% 13.73/7.53 inference(NNF_transformation,[status(thm)],[f200])).
% 13.73/7.53 fof(f202,plain,(
% 13.73/7.53 ![X0]: (~aSet0(X0)|~sbrdtbr0(X0)=sz00|X0=slcrc0)),
% 13.73/7.53 inference(cnf_transformation,[status(thm)],[f201])).
% 13.73/7.53 fof(f203,plain,(
% 13.73/7.53 ![X0]: (~aSet0(X0)|sbrdtbr0(X0)=sz00|~X0=slcrc0)),
% 13.73/7.53 inference(cnf_transformation,[status(thm)],[f201])).
% 13.73/7.53 fof(f339,plain,(
% 13.73/7.53 ((aSet0(xS)&(![W0]: (~aElementOf0(W0,xS)|aElementOf0(W0,szNzAzT0))))&aSubsetOf0(xS,szNzAzT0))&isCountable0(xS)),
% 13.73/7.53 inference(pre_NNF_transformation,[status(thm)],[f75])).
% 13.73/7.53 fof(f340,plain,(
% 13.73/7.53 aSet0(xS)),
% 13.73/7.53 inference(cnf_transformation,[status(thm)],[f339])).
% 13.73/7.53 fof(f343,plain,(
% 13.73/7.53 isCountable0(xS)),
% 13.73/7.53 inference(cnf_transformation,[status(thm)],[f339])).
% 13.73/7.53 fof(f344,plain,(
% 13.73/7.53 (((((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)),
% 13.73/7.53 inference(pre_NNF_transformation,[status(thm)],[f76])).
% 13.73/7.53 fof(f345,plain,(
% 13.73/7.53 (((((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)),
% 13.73/7.53 inference(NNF_transformation,[status(thm)],[f344])).
% 13.73/7.53 fof(f346,plain,(
% 13.73/7.53 (((((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)),
% 13.73/7.53 inference(miniscoping,[status(thm)],[f345])).
% 13.73/7.53 fof(f347,plain,(
% 13.73/7.53 (((((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)),
% 13.73/7.53 inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl,sK20_skl]),skolemize(W1,sK19_skl(W0)),skolemize(W1,sK20_skl(W0))],[f346])).
% 13.73/7.53 fof(f355,plain,(
% 13.73/7.53 ![X0]: (~aSubsetOf0(X0,xS)|~sbrdtbr0(X0)=xK|aElementOf0(X0,szDzozmdt0(xc)))),
% 13.73/7.53 inference(cnf_transformation,[status(thm)],[f347])).
% 13.73/7.53 fof(f360,plain,(
% 13.73/7.53 ![X0,X1]: (aElementOf0(X0,sdtlcdtrc0(xc,szDzozmdt0(xc)))|~aElementOf0(X1,szDzozmdt0(xc))|~sdtlpdtrp0(xc,X1)=X0)),
% 13.73/7.53 inference(cnf_transformation,[status(thm)],[f347])).
% 13.73/7.53 fof(f361,plain,(
% 13.73/7.53 ![X0]: (~aElementOf0(X0,sdtlcdtrc0(xc,szDzozmdt0(xc)))|aElementOf0(X0,xT))),
% 13.73/7.53 inference(cnf_transformation,[status(thm)],[f347])).
% 13.73/7.53 fof(f372,plain,(
% 13.73/7.53 (xK=sz00&(![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)))))))),
% 13.73/7.53 inference(pre_NNF_transformation,[status(thm)],[f79])).
% 13.73/7.53 fof(f373,definition,(
% 13.73/7.53 ![W1]: (sP4_prd(W1)<=>(((~aSet0(W1)|(?[W2]: (aElementOf0(W2,W1)&~aElementOf0(W2,xS))))&~aSubsetOf0(W1,xS))|~isCountable0(W1)))),
% 13.73/7.53 introduced(definition,[new_symbols(definition,[sP4_prd])],[])).
% 13.73/7.53 fof(f374,plain,(
% 13.73/7.53 xK=sz00&(![W0]: (~aElementOf0(W0,xT)|(![W1]: (sP4_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))))))),
% 13.73/7.53 inference(formula_renaming,[status(thm)],[f372,f373])).
% 13.73/7.53 fof(f375,plain,(
% 13.73/7.53 xK=sz00&(![W0]: (~aElementOf0(W0,xT)|(![W1]: (sP4_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)))))),
% 13.73/7.53 inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl]),skolemize(W2,sK23_skl(W1,W0))],[f374])).
% 13.73/7.53 fof(f376,plain,(
% 13.73/7.53 xK=sz00),
% 13.73/7.53 inference(cnf_transformation,[status(thm)],[f375])).
% 13.73/7.53 fof(f377,plain,(
% 13.73/7.53 ![X0,X1]: (~aElementOf0(X0,xT)|sP4_prd(X1)|aSet0(sK23_skl(X1,X0)))),
% 13.73/7.53 inference(cnf_transformation,[status(thm)],[f375])).
% 13.73/7.53 fof(f380,plain,(
% 13.73/7.53 ![X0,X1]: (~aElementOf0(X0,xT)|sP4_prd(X1)|sbrdtbr0(sK23_skl(X1,X0))=xK)),
% 13.73/7.53 inference(cnf_transformation,[status(thm)],[f375])).
% 13.73/7.53 fof(f382,plain,(
% 13.73/7.53 ![X0,X1]: (~aElementOf0(X0,xT)|sP4_prd(X1)|~sdtlpdtrp0(xc,sK23_skl(X1,X0))=X0)),
% 13.73/7.53 inference(cnf_transformation,[status(thm)],[f375])).
% 13.73/7.53 fof(f434,plain,(
% 13.73/7.53 ![W1]: ((~sP4_prd(W1)|(((~aSet0(W1)|(?[W2]: (aElementOf0(W2,W1)&~aElementOf0(W2,xS))))&~aSubsetOf0(W1,xS))|~isCountable0(W1)))&(sP4_prd(W1)|(((aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,xS))))|aSubsetOf0(W1,xS))&isCountable0(W1))))),
% 13.73/7.53 inference(NNF_transformation,[status(thm)],[f373])).
% 13.73/7.53 fof(f435,plain,(
% 13.73/7.53 (![W1]: (~sP4_prd(W1)|(((~aSet0(W1)|(?[W2]: (aElementOf0(W2,W1)&~aElementOf0(W2,xS))))&~aSubsetOf0(W1,xS))|~isCountable0(W1))))&(![W1]: (sP4_prd(W1)|(((aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,xS))))|aSubsetOf0(W1,xS))&isCountable0(W1))))),
% 13.73/7.53 inference(miniscoping,[status(thm)],[f434])).
% 13.73/7.53 fof(f436,plain,(
% 13.73/7.53 (![W1]: (~sP4_prd(W1)|(((~aSet0(W1)|(aElementOf0(sK35_skl(W1),W1)&~aElementOf0(sK35_skl(W1),xS)))&~aSubsetOf0(W1,xS))|~isCountable0(W1))))&(![W1]: (sP4_prd(W1)|(((aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,xS))))|aSubsetOf0(W1,xS))&isCountable0(W1))))),
% 13.73/7.53 inference(skolemize,[status(esa),new_symbols(skolem,[sK35_skl]),skolemize(W2,sK35_skl(W1))],[f435])).
% 13.73/7.53 fof(f439,plain,(
% 13.73/7.53 ![X0]: (~sP4_prd(X0)|~aSubsetOf0(X0,xS)|~isCountable0(X0))),
% 13.73/7.53 inference(cnf_transformation,[status(thm)],[f436])).
% 13.73/7.53 fof(f458,plain,(
% 13.73/7.53 aSet0(slcrc0)),
% 13.73/7.53 inference(destructive_equality_resolution,[status(thm)],[f94])).
% 13.73/7.53 fof(f459,plain,(
% 13.73/7.53 ![X0]: (~aElementOf0(X0,slcrc0))),
% 13.73/7.53 inference(destructive_equality_resolution,[status(thm)],[f95])).
% 13.73/7.53 fof(f477,plain,(
% 13.73/7.53 ~aSet0(slcrc0)|sbrdtbr0(slcrc0)=sz00),
% 13.73/7.53 inference(destructive_equality_resolution,[status(thm)],[f203])).
% 13.73/7.53 fof(f478,plain,(
% 13.73/7.53 sbrdtbr0(slcrc0)=sz00),
% 13.73/7.53 inference(forward_subsumption_resolution,[status(thm)],[f477,f458])).
% 13.73/7.53 fof(f508,plain,(
% 13.73/7.53 ![X0]: (aElementOf0(sdtlpdtrp0(xc,X0),sdtlcdtrc0(xc,szDzozmdt0(xc)))|~aElementOf0(X0,szDzozmdt0(xc)))),
% 13.73/7.53 inference(destructive_equality_resolution,[status(thm)],[f360])).
% 13.73/7.53 fof(f512,plain,(
% 13.73/7.53 sbrdtbr0(slcrc0)=xK),
% 13.73/7.53 inference(backward_demodulation,[status(thm)],[f376,f478])).
% 13.73/7.53 fof(f513,plain,(
% 13.73/7.53 ![X0]: (~aSet0(X0)|~sbrdtbr0(X0)=xK|X0=slcrc0)),
% 13.73/7.53 inference(backward_demodulation,[status(thm)],[f376,f202])).
% 13.73/7.53 fof(f570,plain,(
% 13.73/7.53 ~sP4_prd(xS)|~isCountable0(xS)|~aSet0(xS)),
% 13.73/7.53 inference(resolution,[status(thm)],[f439,f115])).
% 13.73/7.53 fof(f571,plain,(
% 13.73/7.53 ~sP4_prd(xS)|~aSet0(xS)),
% 13.73/7.53 inference(forward_subsumption_resolution,[status(thm)],[f570,f343])).
% 13.73/7.53 fof(f594,plain,(
% 13.73/7.53 ![X0]: (~aSet0(X0)|aSubsetOf0(slcrc0,X0)|aElementOf0(sK1_skl(slcrc0,X0),slcrc0))),
% 13.73/7.53 inference(resolution,[status(thm)],[f110,f458])).
% 13.73/7.53 fof(f598,plain,(
% 13.73/7.53 ![X0]: (~aSet0(X0)|aSubsetOf0(slcrc0,X0))),
% 13.73/7.53 inference(forward_subsumption_resolution,[status(thm)],[f594,f459])).
% 13.73/7.53 fof(f622,plain,(
% 13.73/7.53 ![X0,X1]: (~sbrdtbr0(sK23_skl(X0,X1))=xK|sK23_skl(X0,X1)=slcrc0|~aElementOf0(X1,xT)|sP4_prd(X0))),
% 13.73/7.53 inference(resolution,[status(thm)],[f513,f377])).
% 13.73/7.53 fof(f624,plain,(
% 13.73/7.53 ![X0,X1]: (sK23_skl(X0,X1)=slcrc0|~aElementOf0(X1,xT)|sP4_prd(X0))),
% 13.73/7.53 inference(forward_subsumption_resolution,[status(thm)],[f622,f380])).
% 13.73/7.53 fof(f880,plain,(
% 13.73/7.53 ![X0]: (~aElementOf0(X0,xT)|~sdtlpdtrp0(xc,sK23_skl(xS,X0))=X0|~aSet0(xS))),
% 13.73/7.53 inference(resolution,[status(thm)],[f382,f571])).
% 13.73/7.53 fof(f881,plain,(
% 13.73/7.53 ![X0]: (~aElementOf0(X0,xT)|~sdtlpdtrp0(xc,sK23_skl(xS,X0))=X0)),
% 13.73/7.53 inference(forward_subsumption_resolution,[status(thm)],[f880,f340])).
% 13.73/7.53 fof(f963,plain,(
% 13.73/7.53 ![X0]: (sK23_skl(xS,X0)=slcrc0|~aElementOf0(X0,xT)|~aSet0(xS))),
% 13.73/7.53 inference(resolution,[status(thm)],[f624,f571])).
% 13.73/7.53 fof(f964,plain,(
% 13.73/7.53 ![X0]: (sK23_skl(xS,X0)=slcrc0|~aElementOf0(X0,xT))),
% 13.73/7.53 inference(forward_subsumption_resolution,[status(thm)],[f963,f340])).
% 13.73/7.53 fof(f1132,plain,(
% 13.73/7.53 ~sbrdtbr0(slcrc0)=xK|aElementOf0(slcrc0,szDzozmdt0(xc))|~aSet0(xS)),
% 13.73/7.53 inference(resolution,[status(thm)],[f355,f598])).
% 13.73/7.53 fof(f1134,plain,(
% 13.73/7.53 ~xK=xK|aElementOf0(slcrc0,szDzozmdt0(xc))|~aSet0(xS)),
% 13.73/7.53 inference(forward_demodulation,[status(thm)],[f512,f1132])).
% 13.73/7.53 fof(f1135,plain,(
% 13.73/7.53 aElementOf0(slcrc0,szDzozmdt0(xc))|~aSet0(xS)),
% 13.73/7.53 inference(trivial_equality_resolution,[status(thm)],[f1134])).
% 13.73/7.53 fof(f1136,plain,(
% 13.73/7.53 aElementOf0(slcrc0,szDzozmdt0(xc))),
% 13.73/7.53 inference(forward_subsumption_resolution,[status(thm)],[f1135,f340])).
% 13.73/7.53 fof(f1408,plain,(
% 13.73/7.53 ![X0]: (aElementOf0(sdtlpdtrp0(xc,X0),xT)|~aElementOf0(X0,szDzozmdt0(xc)))),
% 13.73/7.53 inference(resolution,[status(thm)],[f361,f508])).
% 13.73/7.53 fof(f3860,plain,(
% 13.73/7.53 aElementOf0(sdtlpdtrp0(xc,slcrc0),xT)),
% 13.73/7.53 inference(resolution,[status(thm)],[f1408,f1136])).
% 13.73/7.53 fof(f3866,plain,(
% 13.73/7.53 ~sdtlpdtrp0(xc,sK23_skl(xS,sdtlpdtrp0(xc,slcrc0)))=sdtlpdtrp0(xc,slcrc0)),
% 13.73/7.53 inference(resolution,[status(thm)],[f3860,f881])).
% 13.73/7.53 fof(f3870,plain,(
% 13.73/7.53 sK23_skl(xS,sdtlpdtrp0(xc,slcrc0))=slcrc0),
% 13.73/7.53 inference(resolution,[status(thm)],[f3860,f964])).
% 13.73/7.53 fof(f3886,plain,(
% 13.73/7.53 ~sdtlpdtrp0(xc,slcrc0)=sdtlpdtrp0(xc,slcrc0)),
% 13.73/7.53 inference(backward_demodulation,[status(thm)],[f3870,f3866])).
% 13.73/7.53 fof(f3888,plain,(
% 13.73/7.56 $false),
% 13.73/7.56 inference(trivial_equality_resolution,[status(thm)],[f3886])).
% 13.73/7.56 % SZS output end CNFRefutation for theBenchmark.p
% 13.73/7.58 % Elapsed time: 2.129616 seconds
% 13.73/7.58 % CPU time: 16.320423 seconds
% 13.73/7.58 % Total memory used: 234.869 MB
% 13.73/7.58 % Net memory used: 225.232 MB
%------------------------------------------------------------------------------