%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM558+3 : 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 : 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:12 PM UTC 2026
% Result : Theorem 0.18s 0.55s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM558+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.43 % Computer : n013.cluster.edu
% 0.18/0.43 % Model : x86_64 x86_64
% 0.18/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.43 % Memory : 8046.5625MB
% 0.18/0.43 % OS : Linux 6.8.0-71-generic
% 0.18/0.43 % CPULimit : 300
% 0.18/0.43 % WCLimit : 300
% 0.18/0.43 % DateTime : Mon Sep 21 02:39:20 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.18/0.46 % Drodi V4.1.1
% 0.18/0.55 % Refutation found
% 0.18/0.55 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.18/0.55 % SZS output start CNFRefutation for theBenchmark
% 0.18/0.55 fof(f3,axiom,(
% 0.18/0.55 (! [W0] :( aSet0(W0)=> (! [W1] :( aElementOf0(W1,W0)=> aElement0(W1) ) )) )),
% 0.18/0.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.55 fof(f10,definition,(
% 0.18/0.55 (! [W0] :( aSet0(W0)=> (! [W1] :( aSubsetOf0(W1,W0)<=> ( aSet0(W1)& (! [W2] :( aElementOf0(W2,W1)=> aElementOf0(W2,W0) ) )) ) )) )),
% 0.18/0.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.55 fof(f12,axiom,(
% 0.18/0.55 (! [W0] :( aSet0(W0)=> aSubsetOf0(W0,W0) ) )),
% 0.18/0.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.55 fof(f14,axiom,(
% 0.18/0.55 (! [W0,W1,W2] :( ( aSet0(W0)& aSet0(W1)& aSet0(W2) )=> ( ( aSubsetOf0(W0,W1)& aSubsetOf0(W1,W2) )=> aSubsetOf0(W0,W2) ) ) )),
% 0.18/0.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.55 fof(f62,hypothesis,(
% 0.18/0.55 ( aSet0(xS)& aSet0(xT)& xk != sz00 ) ),
% 0.18/0.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.55 fof(f63,hypothesis,(
% 0.18/0.55 ( aSet0(slbdtsldtrb0(xS,xk))& (! [W0] :( ( aElementOf0(W0,slbdtsldtrb0(xS,xk))=> ( 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,slbdtsldtrb0(xS,xk)) ) ))& aSet0(slbdtsldtrb0(xT,xk))& (! [W0] :( ( aElementOf0(W0,slbdtsldtrb0(xT,xk))=> ( aSet0(W0)& (! [W1] :( aElementOf0(W1,W0)=> aElementOf0(W1,xT) ))& aSubsetOf0(W0,xT)& sbrdtbr0(W0) = xk ) )& ( ( ( ( aSet0(W0)& (! [W1] :( aElementOf0(W1,W0)=> aElementOf0(W1,xT) ) ))| aSubsetOf0(W0,xT) )& sbrdtbr0(W0) = xk )=> aElementOf0(W0,slbdtsldtrb0(xT,xk)) ) ))& (! [W0] :( aElementOf0(W0,slbdtsldtrb0(xS,xk))=> aElementOf0(W0,slbdtsldtrb0(xT,xk)) ))& aSubsetOf0(slbdtsldtrb0(xS,xk),slbdtsldtrb0(xT,xk))& ~ ( (! [W0] :( ( aElementOf0(W0,slbdtsldtrb0(xS,xk))=> ( 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,slbdtsldtrb0(xS,xk)) ) ))=> ( ~ (? [W0] : aElementOf0(W0,slbdtsldtrb0(xS,xk)))| slbdtsldtrb0(xS,xk) = slcrc0 ) ) ) ),
% 0.18/0.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.55 fof(f64,hypothesis,(
% 0.18/0.55 aElementOf0(xx,xS) ),
% 0.18/0.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.55 fof(f70,hypothesis,(
% 0.18/0.55 ( aSet0(sdtmndt0(xQ,xy))& (! [W0] :( aElementOf0(W0,sdtmndt0(xQ,xy))<=> ( aElement0(W0)& aElementOf0(W0,xQ)& W0 != xy ) ))& aSet0(xP)& (! [W0] :( aElementOf0(W0,xP)<=> ( aElement0(W0)& ( aElementOf0(W0,sdtmndt0(xQ,xy))| W0 = xx ) ) ))& xP = sdtpldt0(sdtmndt0(xQ,xy),xx) ) ),
% 0.18/0.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.55 fof(f71,hypothesis,(
% 0.18/0.55 ( (! [W0] :( aElementOf0(W0,xP)=> aElementOf0(W0,xS) ))& aSubsetOf0(xP,xS)& sbrdtbr0(xP) = xk& aElementOf0(xP,slbdtsldtrb0(xS,xk)) ) ),
% 0.18/0.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.55 fof(f72,conjecture,(
% 0.18/0.55 aElementOf0(xx,xT) ),
% 0.18/0.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.55 fof(f73,negated_conjecture,(
% 0.18/0.55 ~(aElementOf0(xx,xT) )),
% 0.18/0.55 inference(negated_conjecture,[status(cth)],[f72])).
% 0.18/0.55 fof(f80,plain,(
% 0.18/0.55 ![W0]: (~aSet0(W0)|(![W1]: (~aElementOf0(W1,W0)|aElement0(W1))))),
% 0.18/0.55 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.18/0.55 fof(f81,plain,(
% 0.18/0.55 ![X0,X1]: (~aSet0(X0)|~aElementOf0(X1,X0)|aElement0(X1))),
% 0.18/0.55 inference(cnf_transformation,[status(thm)],[f80])).
% 0.18/0.55 fof(f98,plain,(
% 0.18/0.55 ![W0]: (~aSet0(W0)|(![W1]: (aSubsetOf0(W1,W0)<=>(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0)))))))),
% 0.18/0.55 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 0.18/0.55 fof(f99,plain,(
% 0.18/0.55 ![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.18/0.55 inference(NNF_transformation,[status(thm)],[f98])).
% 0.18/0.55 fof(f100,plain,(
% 0.18/0.55 ![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.18/0.55 inference(miniscoping,[status(thm)],[f99])).
% 0.18/0.55 fof(f101,plain,(
% 0.18/0.55 ![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.18/0.55 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W2,sK1_skl(W1,W0))],[f100])).
% 0.18/0.55 fof(f102,plain,(
% 0.18/0.55 ![X0,X1]: (~aSet0(X0)|~aSubsetOf0(X1,X0)|aSet0(X1))),
% 0.18/0.55 inference(cnf_transformation,[status(thm)],[f101])).
% 0.18/0.55 fof(f108,plain,(
% 0.18/0.55 ![W0]: (~aSet0(W0)|aSubsetOf0(W0,W0))),
% 0.18/0.55 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 0.18/0.55 fof(f109,plain,(
% 0.18/0.55 ![X0]: (~aSet0(X0)|aSubsetOf0(X0,X0))),
% 0.18/0.55 inference(cnf_transformation,[status(thm)],[f108])).
% 0.18/0.55 fof(f112,plain,(
% 0.18/0.55 ![W0,W1,W2]: (((~aSet0(W0)|~aSet0(W1))|~aSet0(W2))|((~aSubsetOf0(W0,W1)|~aSubsetOf0(W1,W2))|aSubsetOf0(W0,W2)))),
% 0.18/0.55 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 0.18/0.55 fof(f113,plain,(
% 0.18/0.55 ![X0,X1,X2]: (~aSet0(X0)|~aSet0(X1)|~aSet0(X2)|~aSubsetOf0(X0,X1)|~aSubsetOf0(X1,X2)|aSubsetOf0(X0,X2))),
% 0.18/0.55 inference(cnf_transformation,[status(thm)],[f112])).
% 0.18/0.55 fof(f273,plain,(
% 0.18/0.55 aSet0(xS)),
% 0.18/0.55 inference(cnf_transformation,[status(thm)],[f62])).
% 0.18/0.55 fof(f274,plain,(
% 0.18/0.55 aSet0(xT)),
% 0.18/0.55 inference(cnf_transformation,[status(thm)],[f62])).
% 0.18/0.55 fof(f276,plain,(
% 0.18/0.55 (((((aSet0(slbdtsldtrb0(xS,xk))&(![W0]: ((~aElementOf0(W0,slbdtsldtrb0(xS,xk))|(((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,slbdtsldtrb0(xS,xk))))))&aSet0(slbdtsldtrb0(xT,xk)))&(![W0]: ((~aElementOf0(W0,slbdtsldtrb0(xT,xk))|(((aSet0(W0)&(![W1]: (~aElementOf0(W1,W0)|aElementOf0(W1,xT))))&aSubsetOf0(W0,xT))&sbrdtbr0(W0)=xk))&((((~aSet0(W0)|(?[W1]: (aElementOf0(W1,W0)&~aElementOf0(W1,xT))))&~aSubsetOf0(W0,xT))|~sbrdtbr0(W0)=xk)|aElementOf0(W0,slbdtsldtrb0(xT,xk))))))&(![W0]: (~aElementOf0(W0,slbdtsldtrb0(xS,xk))|aElementOf0(W0,slbdtsldtrb0(xT,xk)))))&aSubsetOf0(slbdtsldtrb0(xS,xk),slbdtsldtrb0(xT,xk)))&((![W0]: ((~aElementOf0(W0,slbdtsldtrb0(xS,xk))|(((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,slbdtsldtrb0(xS,xk)))))&((?[W0]: aElementOf0(W0,slbdtsldtrb0(xS,xk)))&~slbdtsldtrb0(xS,xk)=slcrc0))),
% 0.18/0.55 inference(pre_NNF_transformation,[status(thm)],[f63])).
% 0.18/0.55 fof(f277,plain,(
% 0.18/0.55 (((((aSet0(slbdtsldtrb0(xS,xk))&((![W0]: (~aElementOf0(W0,slbdtsldtrb0(xS,xk))|(((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,slbdtsldtrb0(xS,xk))))))&aSet0(slbdtsldtrb0(xT,xk)))&((![W0]: (~aElementOf0(W0,slbdtsldtrb0(xT,xk))|(((aSet0(W0)&(![W1]: (~aElementOf0(W1,W0)|aElementOf0(W1,xT))))&aSubsetOf0(W0,xT))&sbrdtbr0(W0)=xk)))&(![W0]: ((((~aSet0(W0)|(?[W1]: (aElementOf0(W1,W0)&~aElementOf0(W1,xT))))&~aSubsetOf0(W0,xT))|~sbrdtbr0(W0)=xk)|aElementOf0(W0,slbdtsldtrb0(xT,xk))))))&(![W0]: (~aElementOf0(W0,slbdtsldtrb0(xS,xk))|aElementOf0(W0,slbdtsldtrb0(xT,xk)))))&aSubsetOf0(slbdtsldtrb0(xS,xk),slbdtsldtrb0(xT,xk)))&(((![W0]: (~aElementOf0(W0,slbdtsldtrb0(xS,xk))|(((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,slbdtsldtrb0(xS,xk)))))&((?[W0]: aElementOf0(W0,slbdtsldtrb0(xS,xk)))&~slbdtsldtrb0(xS,xk)=slcrc0))),
% 0.18/0.55 inference(miniscoping,[status(thm)],[f276])).
% 0.18/0.55 fof(f278,plain,(
% 0.18/0.55 (((((aSet0(slbdtsldtrb0(xS,xk))&((![W0]: (~aElementOf0(W0,slbdtsldtrb0(xS,xk))|(((aSet0(W0)&(![W1]: (~aElementOf0(W1,W0)|aElementOf0(W1,xS))))&aSubsetOf0(W0,xS))&sbrdtbr0(W0)=xk)))&(![W0]: ((((~aSet0(W0)|(aElementOf0(sK11_skl(W0),W0)&~aElementOf0(sK11_skl(W0),xS)))&~aSubsetOf0(W0,xS))|~sbrdtbr0(W0)=xk)|aElementOf0(W0,slbdtsldtrb0(xS,xk))))))&aSet0(slbdtsldtrb0(xT,xk)))&((![W0]: (~aElementOf0(W0,slbdtsldtrb0(xT,xk))|(((aSet0(W0)&(![W1]: (~aElementOf0(W1,W0)|aElementOf0(W1,xT))))&aSubsetOf0(W0,xT))&sbrdtbr0(W0)=xk)))&(![W0]: ((((~aSet0(W0)|(aElementOf0(sK12_skl(W0),W0)&~aElementOf0(sK12_skl(W0),xT)))&~aSubsetOf0(W0,xT))|~sbrdtbr0(W0)=xk)|aElementOf0(W0,slbdtsldtrb0(xT,xk))))))&(![W0]: (~aElementOf0(W0,slbdtsldtrb0(xS,xk))|aElementOf0(W0,slbdtsldtrb0(xT,xk)))))&aSubsetOf0(slbdtsldtrb0(xS,xk),slbdtsldtrb0(xT,xk)))&(((![W0]: (~aElementOf0(W0,slbdtsldtrb0(xS,xk))|(((aSet0(W0)&(![W1]: (~aElementOf0(W1,W0)|aElementOf0(W1,xS))))&aSubsetOf0(W0,xS))&sbrdtbr0(W0)=xk)))&(![W0]: ((((~aSet0(W0)|(aElementOf0(sK13_skl(W0),W0)&~aElementOf0(sK13_skl(W0),xS)))&~aSubsetOf0(W0,xS))|~sbrdtbr0(W0)=xk)|aElementOf0(W0,slbdtsldtrb0(xS,xk)))))&(aElementOf0(sK14_skl,slbdtsldtrb0(xS,xk))&~slbdtsldtrb0(xS,xk)=slcrc0))),
% 0.18/0.55 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl,sK12_skl,sK13_skl,sK14_skl]),skolemize(W1,sK11_skl(W0)),skolemize(W1,sK12_skl(W0)),skolemize(W1,sK13_skl(W0)),skolemize(W0,sK14_skl)],[f277])).
% 0.18/0.55 fof(f289,plain,(
% 0.18/0.55 ![X0,X1]: (~aElementOf0(X0,slbdtsldtrb0(xT,xk))|~aElementOf0(X1,X0)|aElementOf0(X1,xT))),
% 0.18/0.55 inference(cnf_transformation,[status(thm)],[f278])).
% 0.18/0.55 fof(f290,plain,(
% 0.18/0.55 ![X0]: (~aElementOf0(X0,slbdtsldtrb0(xT,xk))|aSubsetOf0(X0,xT))),
% 0.18/0.55 inference(cnf_transformation,[status(thm)],[f278])).
% 0.18/0.55 fof(f294,plain,(
% 0.18/0.55 ![X0]: (~aSubsetOf0(X0,xT)|~sbrdtbr0(X0)=xk|aElementOf0(X0,slbdtsldtrb0(xT,xk)))),
% 0.18/0.55 inference(cnf_transformation,[status(thm)],[f278])).
% 0.18/0.55 fof(f295,plain,(
% 0.18/0.55 ![X0]: (~aElementOf0(X0,slbdtsldtrb0(xS,xk))|aElementOf0(X0,slbdtsldtrb0(xT,xk)))),
% 0.18/0.55 inference(cnf_transformation,[status(thm)],[f278])).
% 0.18/0.55 fof(f306,plain,(
% 0.18/0.55 aElementOf0(xx,xS)),
% 0.18/0.55 inference(cnf_transformation,[status(thm)],[f64])).
% 0.18/0.55 fof(f320,plain,(
% 0.18/0.55 (((aSet0(sdtmndt0(xQ,xy))&(![W0]: ((~aElementOf0(W0,sdtmndt0(xQ,xy))|((aElement0(W0)&aElementOf0(W0,xQ))&~W0=xy))&(aElementOf0(W0,sdtmndt0(xQ,xy))|((~aElement0(W0)|~aElementOf0(W0,xQ))|W0=xy)))))&aSet0(xP))&(![W0]: ((~aElementOf0(W0,xP)|(aElement0(W0)&(aElementOf0(W0,sdtmndt0(xQ,xy))|W0=xx)))&(aElementOf0(W0,xP)|(~aElement0(W0)|(~aElementOf0(W0,sdtmndt0(xQ,xy))&~W0=xx))))))&xP=sdtpldt0(sdtmndt0(xQ,xy),xx)),
% 0.18/0.55 inference(NNF_transformation,[status(thm)],[f70])).
% 0.18/0.55 fof(f321,plain,(
% 0.18/0.55 (((aSet0(sdtmndt0(xQ,xy))&((![W0]: (~aElementOf0(W0,sdtmndt0(xQ,xy))|((aElement0(W0)&aElementOf0(W0,xQ))&~W0=xy)))&(![W0]: (aElementOf0(W0,sdtmndt0(xQ,xy))|((~aElement0(W0)|~aElementOf0(W0,xQ))|W0=xy)))))&aSet0(xP))&((![W0]: (~aElementOf0(W0,xP)|(aElement0(W0)&(aElementOf0(W0,sdtmndt0(xQ,xy))|W0=xx))))&(![W0]: (aElementOf0(W0,xP)|(~aElement0(W0)|(~aElementOf0(W0,sdtmndt0(xQ,xy))&~W0=xx))))))&xP=sdtpldt0(sdtmndt0(xQ,xy),xx)),
% 0.18/0.55 inference(miniscoping,[status(thm)],[f320])).
% 0.18/0.55 fof(f327,plain,(
% 0.18/0.55 aSet0(xP)),
% 0.18/0.55 inference(cnf_transformation,[status(thm)],[f321])).
% 0.18/0.55 fof(f331,plain,(
% 0.18/0.55 ![X0]: (aElementOf0(X0,xP)|~aElement0(X0)|~X0=xx)),
% 0.18/0.55 inference(cnf_transformation,[status(thm)],[f321])).
% 0.18/0.55 fof(f333,plain,(
% 0.18/0.55 (((![W0]: (~aElementOf0(W0,xP)|aElementOf0(W0,xS)))&aSubsetOf0(xP,xS))&sbrdtbr0(xP)=xk)&aElementOf0(xP,slbdtsldtrb0(xS,xk))),
% 0.18/0.55 inference(pre_NNF_transformation,[status(thm)],[f71])).
% 0.18/0.55 fof(f336,plain,(
% 0.18/0.55 sbrdtbr0(xP)=xk),
% 0.18/0.55 inference(cnf_transformation,[status(thm)],[f333])).
% 0.18/0.55 fof(f337,plain,(
% 0.18/0.55 aElementOf0(xP,slbdtsldtrb0(xS,xk))),
% 0.18/0.55 inference(cnf_transformation,[status(thm)],[f333])).
% 0.18/0.55 fof(f338,plain,(
% 0.18/0.55 ~aElementOf0(xx,xT)),
% 0.18/0.55 inference(cnf_transformation,[status(thm)],[f73])).
% 0.18/0.55 fof(f350,plain,(
% 0.18/0.55 ![X0,X1,X2]: (~aSet0(X0)|~aSet0(X1)|~aSubsetOf0(X2,X0)|~aSubsetOf0(X0,X1)|aSubsetOf0(X2,X1))),
% 0.18/0.55 inference(forward_subsumption_resolution,[status(thm)],[f113,f102])).
% 0.18/0.55 fof(f383,plain,(
% 0.18/0.55 aElementOf0(xx,xP)|~aElement0(xx)),
% 0.18/0.55 inference(destructive_equality_resolution,[status(thm)],[f331])).
% 0.18/0.55 fof(f385,plain,(
% 0.18/0.55 ~aSet0(xS)|aElement0(xx)),
% 0.18/0.55 inference(resolution,[status(thm)],[f81,f306])).
% 0.18/0.55 fof(f387,plain,(
% 0.18/0.55 aElementOf0(xx,xP)),
% 0.18/0.55 inference(backward_subsumption_resolution,[status(thm)],[f383,f388])).
% 0.18/0.56 fof(f388,plain,(
% 0.18/0.56 aElement0(xx)),
% 0.18/0.56 inference(forward_subsumption_resolution,[status(thm)],[f385,f273])).
% 0.18/0.56 fof(f542,plain,(
% 0.18/0.56 ![X0,X1]: (~aSet0(X0)|~aSet0(xT)|~aSubsetOf0(X1,X0)|~aSubsetOf0(X0,xT)|~sbrdtbr0(X1)=xk|aElementOf0(X1,slbdtsldtrb0(xT,xk)))),
% 0.18/0.56 inference(resolution,[status(thm)],[f350,f294])).
% 0.18/0.56 fof(f548,plain,(
% 0.18/0.56 ![X0,X1]: (~aSet0(xT)|~aSubsetOf0(X0,X1)|~aSubsetOf0(X1,xT)|~sbrdtbr0(X0)=xk|aElementOf0(X0,slbdtsldtrb0(xT,xk)))),
% 0.18/0.56 inference(forward_subsumption_resolution,[status(thm)],[f542,f102])).
% 0.18/0.56 fof(f604,plain,(
% 0.18/0.56 ![X0,X1]: (~aSubsetOf0(X0,X1)|~aSubsetOf0(X1,xT)|~sbrdtbr0(X0)=xk|aElementOf0(X0,slbdtsldtrb0(xT,xk)))),
% 0.18/0.56 inference(resolution,[status(thm)],[f548,f274])).
% 0.18/0.56 fof(f608,plain,(
% 0.18/0.56 ![X0,X1,X2]: (~aSubsetOf0(X0,X1)|~aSubsetOf0(X1,xT)|~sbrdtbr0(X0)=xk|~aElementOf0(X2,X0)|aElementOf0(X2,xT))),
% 0.18/0.56 inference(resolution,[status(thm)],[f604,f289])).
% 0.18/0.56 fof(f719,plain,(
% 0.18/0.56 ![X0,X1]: (~aSubsetOf0(X0,X1)|~aSubsetOf0(X1,xT)|~sbrdtbr0(X0)=xk|~aElementOf0(xx,X0))),
% 0.18/0.56 inference(resolution,[status(thm)],[f608,f338])).
% 0.18/0.56 fof(f723,plain,(
% 0.18/0.56 ![X0]: (~aSubsetOf0(xP,X0)|~aSubsetOf0(X0,xT)|~sbrdtbr0(xP)=xk)),
% 0.18/0.56 inference(resolution,[status(thm)],[f719,f387])).
% 0.18/0.56 fof(f729,plain,(
% 0.18/0.56 ![X0]: (~aSubsetOf0(xP,X0)|~aSubsetOf0(X0,xT)|~xk=xk)),
% 0.18/0.56 inference(forward_demodulation,[status(thm)],[f336,f723])).
% 0.18/0.56 fof(f730,plain,(
% 0.18/0.56 ![X0]: (~aSubsetOf0(xP,X0)|~aSubsetOf0(X0,xT))),
% 0.18/0.56 inference(trivial_equality_resolution,[status(thm)],[f729])).
% 0.18/0.56 fof(f752,plain,(
% 0.18/0.56 aElementOf0(xP,slbdtsldtrb0(xT,xk))),
% 0.18/0.56 inference(resolution,[status(thm)],[f337,f295])).
% 0.18/0.56 fof(f781,plain,(
% 0.18/0.56 ~aSubsetOf0(xP,xT)|~aSet0(xP)),
% 0.18/0.56 inference(resolution,[status(thm)],[f730,f109])).
% 0.18/0.56 fof(f783,plain,(
% 0.18/0.56 ~aSubsetOf0(xP,xT)),
% 0.18/0.56 inference(forward_subsumption_resolution,[status(thm)],[f781,f327])).
% 0.18/0.56 fof(f847,plain,(
% 0.18/0.56 aSubsetOf0(xP,xT)),
% 0.18/0.56 inference(resolution,[status(thm)],[f752,f290])).
% 0.18/0.56 fof(f850,plain,(
% 0.18/0.56 $false),
% 0.18/0.56 inference(forward_subsumption_resolution,[status(thm)],[f847,f783])).
% 0.18/0.56 % SZS output end CNFRefutation for theBenchmark.p
% 0.75/0.58 % Elapsed time: 0.124360 seconds
% 0.75/0.58 % CPU time: 0.676272 seconds
% 0.75/0.58 % Total memory used: 112.026 MB
% 0.75/0.58 % Net memory used: 111.359 MB
%------------------------------------------------------------------------------