%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM558+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 : n009.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.17s 0.65s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : NUM558+1 : 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.13/0.38 % Computer : n009.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Mon Sep 21 02:39:57 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.41 % Drodi V4.1.1
% 0.17/0.65 % Refutation found
% 0.17/0.65 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.17/0.65 % SZS output start CNFRefutation for theBenchmark
% 0.17/0.65 fof(f3,axiom,(
% 0.17/0.65 (! [W0] :( aSet0(W0)=> (! [W1] :( aElementOf0(W1,W0)=> aElement0(W1) ) )) )),
% 0.17/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.65 fof(f10,definition,(
% 0.17/0.65 (! [W0] :( aSet0(W0)=> (! [W1] :( aSubsetOf0(W1,W0)<=> ( aSet0(W1)& (! [W2] :( aElementOf0(W2,W1)=> aElementOf0(W2,W0) ) )) ) )) )),
% 0.17/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.65 fof(f15,definition,(
% 0.17/0.65 (! [W0,W1] :( ( aSet0(W0)& aElement0(W1) )=> (! [W2] :( W2 = sdtpldt0(W0,W1)<=> ( aSet0(W2)& (! [W3] :( aElementOf0(W3,W2)<=> ( aElement0(W3)& ( aElementOf0(W3,W0)| W3 = W1 ) ) ) )) ) )) )),
% 0.17/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.65 fof(f16,definition,(
% 0.17/0.65 (! [W0,W1] :( ( aSet0(W0)& aElement0(W1) )=> (! [W2] :( W2 = sdtmndt0(W0,W1)<=> ( aSet0(W2)& (! [W3] :( aElementOf0(W3,W2)<=> ( aElement0(W3)& aElementOf0(W3,W0)& W3 != W1 ) ) )) ) )) )),
% 0.17/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.65 fof(f24,axiom,(
% 0.17/0.65 aElementOf0(sz00,szNzAzT0) ),
% 0.17/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.65 fof(f57,definition,(
% 0.17/0.65 (! [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.17/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.65 fof(f61,hypothesis,(
% 0.17/0.65 aElementOf0(xk,szNzAzT0) ),
% 0.17/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.65 fof(f62,hypothesis,(
% 0.17/0.65 ( aSet0(xS)& aSet0(xT)& xk != sz00 ) ),
% 0.17/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.65 fof(f63,hypothesis,(
% 0.17/0.65 ( aSubsetOf0(slbdtsldtrb0(xS,xk),slbdtsldtrb0(xT,xk))& slbdtsldtrb0(xS,xk) != slcrc0 ) ),
% 0.17/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.65 fof(f64,hypothesis,(
% 0.17/0.65 aElementOf0(xx,xS) ),
% 0.17/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.65 fof(f66,hypothesis,(
% 0.17/0.65 ( aSet0(xQ)& isFinite0(xQ)& sbrdtbr0(xQ) = xk ) ),
% 0.17/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.65 fof(f67,hypothesis,(
% 0.17/0.65 ( aElement0(xy)& aElementOf0(xy,xQ) ) ),
% 0.17/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.65 fof(f70,hypothesis,(
% 0.17/0.65 xP = sdtpldt0(sdtmndt0(xQ,xy),xx) ),
% 0.17/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.65 fof(f71,hypothesis,(
% 0.17/0.65 aElementOf0(xP,slbdtsldtrb0(xS,xk)) ),
% 0.17/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.65 fof(f72,conjecture,(
% 0.17/0.65 aElementOf0(xx,xT) ),
% 0.17/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.65 fof(f73,negated_conjecture,(
% 0.17/0.65 ~(aElementOf0(xx,xT) )),
% 0.17/0.65 inference(negated_conjecture,[status(cth)],[f72])).
% 0.17/0.65 fof(f80,plain,(
% 0.17/0.65 ![W0]: (~aSet0(W0)|(![W1]: (~aElementOf0(W1,W0)|aElement0(W1))))),
% 0.17/0.65 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.17/0.65 fof(f81,plain,(
% 0.17/0.65 ![X0,X1]: (~aSet0(X0)|~aElementOf0(X1,X0)|aElement0(X1))),
% 0.17/0.65 inference(cnf_transformation,[status(thm)],[f80])).
% 0.17/0.65 fof(f98,plain,(
% 0.17/0.65 ![W0]: (~aSet0(W0)|(![W1]: (aSubsetOf0(W1,W0)<=>(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0)))))))),
% 0.17/0.65 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 0.17/0.65 fof(f99,plain,(
% 0.17/0.65 ![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.17/0.65 inference(NNF_transformation,[status(thm)],[f98])).
% 0.17/0.65 fof(f100,plain,(
% 0.17/0.65 ![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.17/0.65 inference(miniscoping,[status(thm)],[f99])).
% 0.17/0.65 fof(f101,plain,(
% 0.17/0.65 ![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.17/0.65 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W2,sK1_skl(W1,W0))],[f100])).
% 0.17/0.65 fof(f103,plain,(
% 0.17/0.65 ![X0,X1,X2]: (~aSet0(X0)|~aSubsetOf0(X1,X0)|~aElementOf0(X2,X1)|aElementOf0(X2,X0))),
% 0.17/0.65 inference(cnf_transformation,[status(thm)],[f101])).
% 0.17/0.65 fof(f114,plain,(
% 0.17/0.65 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|(![W2]: (W2=sdtpldt0(W0,W1)<=>(aSet0(W2)&(![W3]: (aElementOf0(W3,W2)<=>(aElement0(W3)&(aElementOf0(W3,W0)|W3=W1))))))))),
% 0.17/0.65 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 0.17/0.65 fof(f115,plain,(
% 0.17/0.65 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|(![W2]: ((~W2=sdtpldt0(W0,W1)|(aSet0(W2)&(![W3]: ((~aElementOf0(W3,W2)|(aElement0(W3)&(aElementOf0(W3,W0)|W3=W1)))&(aElementOf0(W3,W2)|(~aElement0(W3)|(~aElementOf0(W3,W0)&~W3=W1)))))))&(W2=sdtpldt0(W0,W1)|(~aSet0(W2)|(?[W3]: ((~aElementOf0(W3,W2)|(~aElement0(W3)|(~aElementOf0(W3,W0)&~W3=W1)))&(aElementOf0(W3,W2)|(aElement0(W3)&(aElementOf0(W3,W0)|W3=W1))))))))))),
% 0.17/0.65 inference(NNF_transformation,[status(thm)],[f114])).
% 0.17/0.65 fof(f116,plain,(
% 0.17/0.65 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|((![W2]: (~W2=sdtpldt0(W0,W1)|(aSet0(W2)&((![W3]: (~aElementOf0(W3,W2)|(aElement0(W3)&(aElementOf0(W3,W0)|W3=W1))))&(![W3]: (aElementOf0(W3,W2)|(~aElement0(W3)|(~aElementOf0(W3,W0)&~W3=W1))))))))&(![W2]: (W2=sdtpldt0(W0,W1)|(~aSet0(W2)|(?[W3]: ((~aElementOf0(W3,W2)|(~aElement0(W3)|(~aElementOf0(W3,W0)&~W3=W1)))&(aElementOf0(W3,W2)|(aElement0(W3)&(aElementOf0(W3,W0)|W3=W1))))))))))),
% 0.17/0.65 inference(miniscoping,[status(thm)],[f115])).
% 0.17/0.65 fof(f117,plain,(
% 0.17/0.65 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|((![W2]: (~W2=sdtpldt0(W0,W1)|(aSet0(W2)&((![W3]: (~aElementOf0(W3,W2)|(aElement0(W3)&(aElementOf0(W3,W0)|W3=W1))))&(![W3]: (aElementOf0(W3,W2)|(~aElement0(W3)|(~aElementOf0(W3,W0)&~W3=W1))))))))&(![W2]: (W2=sdtpldt0(W0,W1)|(~aSet0(W2)|((~aElementOf0(sK2_skl(W2,W1,W0),W2)|(~aElement0(sK2_skl(W2,W1,W0))|(~aElementOf0(sK2_skl(W2,W1,W0),W0)&~sK2_skl(W2,W1,W0)=W1)))&(aElementOf0(sK2_skl(W2,W1,W0),W2)|(aElement0(sK2_skl(W2,W1,W0))&(aElementOf0(sK2_skl(W2,W1,W0),W0)|sK2_skl(W2,W1,W0)=W1)))))))))),
% 0.17/0.65 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(W3,sK2_skl(W2,W1,W0))],[f116])).
% 0.17/0.65 fof(f122,plain,(
% 0.17/0.65 ![X0,X1,X2,X3]: (~aSet0(X0)|~aElement0(X1)|~X2=sdtpldt0(X0,X1)|aElementOf0(X3,X2)|~aElement0(X3)|~X3=X1)),
% 0.17/0.65 inference(cnf_transformation,[status(thm)],[f117])).
% 0.17/0.65 fof(f127,plain,(
% 0.17/0.65 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|(![W2]: (W2=sdtmndt0(W0,W1)<=>(aSet0(W2)&(![W3]: (aElementOf0(W3,W2)<=>((aElement0(W3)&aElementOf0(W3,W0))&~W3=W1)))))))),
% 0.17/0.65 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 0.17/0.65 fof(f128,definition,(
% 0.17/0.65 ![W0,W1,W3]: (sP0_prd(W3,W1,W0)<=>((aElement0(W3)&aElementOf0(W3,W0))&~W3=W1))),
% 0.17/0.65 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.17/0.65 fof(f129,plain,(
% 0.17/0.65 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|(![W2]: (W2=sdtmndt0(W0,W1)<=>(aSet0(W2)&(![W3]: (aElementOf0(W3,W2)<=>sP0_prd(W3,W1,W0)))))))),
% 0.17/0.65 inference(formula_renaming,[status(thm)],[f127,f128])).
% 0.17/0.65 fof(f130,plain,(
% 0.17/0.65 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|(![W2]: ((~W2=sdtmndt0(W0,W1)|(aSet0(W2)&(![W3]: ((~aElementOf0(W3,W2)|sP0_prd(W3,W1,W0))&(aElementOf0(W3,W2)|~sP0_prd(W3,W1,W0))))))&(W2=sdtmndt0(W0,W1)|(~aSet0(W2)|(?[W3]: ((~aElementOf0(W3,W2)|~sP0_prd(W3,W1,W0))&(aElementOf0(W3,W2)|sP0_prd(W3,W1,W0)))))))))),
% 0.17/0.65 inference(NNF_transformation,[status(thm)],[f129])).
% 0.17/0.65 fof(f131,plain,(
% 0.17/0.65 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|((![W2]: (~W2=sdtmndt0(W0,W1)|(aSet0(W2)&((![W3]: (~aElementOf0(W3,W2)|sP0_prd(W3,W1,W0)))&(![W3]: (aElementOf0(W3,W2)|~sP0_prd(W3,W1,W0)))))))&(![W2]: (W2=sdtmndt0(W0,W1)|(~aSet0(W2)|(?[W3]: ((~aElementOf0(W3,W2)|~sP0_prd(W3,W1,W0))&(aElementOf0(W3,W2)|sP0_prd(W3,W1,W0)))))))))),
% 0.17/0.65 inference(miniscoping,[status(thm)],[f130])).
% 0.17/0.65 fof(f132,plain,(
% 0.17/0.65 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|((![W2]: (~W2=sdtmndt0(W0,W1)|(aSet0(W2)&((![W3]: (~aElementOf0(W3,W2)|sP0_prd(W3,W1,W0)))&(![W3]: (aElementOf0(W3,W2)|~sP0_prd(W3,W1,W0)))))))&(![W2]: (W2=sdtmndt0(W0,W1)|(~aSet0(W2)|((~aElementOf0(sK3_skl(W2,W1,W0),W2)|~sP0_prd(sK3_skl(W2,W1,W0),W1,W0))&(aElementOf0(sK3_skl(W2,W1,W0),W2)|sP0_prd(sK3_skl(W2,W1,W0),W1,W0))))))))),
% 0.17/0.65 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(W3,sK3_skl(W2,W1,W0))],[f131])).
% 0.17/0.65 fof(f133,plain,(
% 0.17/0.65 ![X0,X1,X2]: (~aSet0(X0)|~aElement0(X1)|~X2=sdtmndt0(X0,X1)|aSet0(X2))),
% 0.17/0.65 inference(cnf_transformation,[status(thm)],[f132])).
% 0.17/0.65 fof(f152,plain,(
% 0.17/0.65 aElementOf0(sz00,szNzAzT0)),
% 0.17/0.65 inference(cnf_transformation,[status(thm)],[f24])).
% 0.17/0.65 fof(f255,plain,(
% 0.17/0.65 ![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.17/0.65 inference(pre_NNF_transformation,[status(thm)],[f57])).
% 0.17/0.65 fof(f256,plain,(
% 0.17/0.65 ![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.17/0.65 inference(NNF_transformation,[status(thm)],[f255])).
% 0.17/0.65 fof(f257,plain,(
% 0.17/0.65 ![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.17/0.65 inference(miniscoping,[status(thm)],[f256])).
% 0.17/0.65 fof(f258,plain,(
% 0.17/0.65 ![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.17/0.65 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(W3,sK10_skl(W2,W1,W0))],[f257])).
% 0.17/0.65 fof(f259,plain,(
% 0.17/0.65 ![X0,X1,X2]: (~aSet0(X0)|~aElementOf0(X1,szNzAzT0)|~X2=slbdtsldtrb0(X0,X1)|aSet0(X2))),
% 0.17/0.65 inference(cnf_transformation,[status(thm)],[f258])).
% 0.17/0.65 fof(f260,plain,(
% 0.17/0.65 ![X0,X1,X2,X3]: (~aSet0(X0)|~aElementOf0(X1,szNzAzT0)|~X2=slbdtsldtrb0(X0,X1)|~aElementOf0(X3,X2)|aSubsetOf0(X3,X0))),
% 0.17/0.65 inference(cnf_transformation,[status(thm)],[f258])).
% 0.17/0.65 fof(f272,plain,(
% 0.17/0.65 aElementOf0(xk,szNzAzT0)),
% 0.17/0.65 inference(cnf_transformation,[status(thm)],[f61])).
% 0.17/0.65 fof(f273,plain,(
% 0.17/0.65 aSet0(xS)),
% 0.17/0.65 inference(cnf_transformation,[status(thm)],[f62])).
% 0.17/0.65 fof(f274,plain,(
% 0.17/0.65 aSet0(xT)),
% 0.17/0.65 inference(cnf_transformation,[status(thm)],[f62])).
% 0.17/0.65 fof(f276,plain,(
% 0.17/0.65 aSubsetOf0(slbdtsldtrb0(xS,xk),slbdtsldtrb0(xT,xk))),
% 0.17/0.65 inference(cnf_transformation,[status(thm)],[f63])).
% 0.17/0.65 fof(f278,plain,(
% 0.17/0.65 aElementOf0(xx,xS)),
% 0.17/0.65 inference(cnf_transformation,[status(thm)],[f64])).
% 0.17/0.65 fof(f280,plain,(
% 0.17/0.65 aSet0(xQ)),
% 0.17/0.65 inference(cnf_transformation,[status(thm)],[f66])).
% 0.17/0.65 fof(f284,plain,(
% 0.17/0.65 aElementOf0(xy,xQ)),
% 0.17/0.65 inference(cnf_transformation,[status(thm)],[f67])).
% 0.17/0.65 fof(f287,plain,(
% 0.17/0.65 xP=sdtpldt0(sdtmndt0(xQ,xy),xx)),
% 0.17/0.65 inference(cnf_transformation,[status(thm)],[f70])).
% 0.17/0.65 fof(f288,plain,(
% 0.17/0.65 aElementOf0(xP,slbdtsldtrb0(xS,xk))),
% 0.17/0.65 inference(cnf_transformation,[status(thm)],[f71])).
% 0.17/0.65 fof(f289,plain,(
% 0.17/0.65 ~aElementOf0(xx,xT)),
% 0.17/0.65 inference(cnf_transformation,[status(thm)],[f73])).
% 0.17/0.65 fof(f307,plain,(
% 0.17/0.65 ![X0,X1]: (~aSet0(X0)|~aElement0(X1)|aElementOf0(X1,sdtpldt0(X0,X1))|~aElement0(X1))),
% 0.17/0.65 inference(destructive_equality_resolution,[status(thm)],[f122])).
% 0.17/0.65 fof(f308,plain,(
% 0.17/0.65 ![X0,X1]: (~aSet0(X0)|~aElement0(X1)|aElementOf0(X1,sdtpldt0(X0,X1)))),
% 0.17/0.65 inference(duplicate_literals_removal,[status(thm)],[f307])).
% 0.17/0.65 fof(f312,plain,(
% 0.17/0.65 ![X0,X1]: (~aSet0(X0)|~aElement0(X1)|aSet0(sdtmndt0(X0,X1)))),
% 0.17/0.65 inference(destructive_equality_resolution,[status(thm)],[f133])).
% 0.17/0.65 fof(f328,plain,(
% 0.17/0.65 ![X0,X1]: (~aSet0(X0)|~aElementOf0(X1,szNzAzT0)|aSet0(slbdtsldtrb0(X0,X1)))),
% 0.17/0.65 inference(destructive_equality_resolution,[status(thm)],[f259])).
% 0.17/0.65 fof(f329,plain,(
% 0.17/0.65 ![X0,X1,X2]: (~aSet0(X0)|~aElementOf0(X1,szNzAzT0)|~aElementOf0(X2,slbdtsldtrb0(X0,X1))|aSubsetOf0(X2,X0))),
% 0.17/0.65 inference(destructive_equality_resolution,[status(thm)],[f260])).
% 0.17/0.65 fof(f333,plain,(
% 0.17/0.65 ~aSet0(xS)|aElement0(xx)),
% 0.17/0.65 inference(resolution,[status(thm)],[f81,f278])).
% 0.17/0.65 fof(f334,definition,(
% 0.17/0.65 sQ0_spl <=> (aSet0(xS))),
% 0.17/0.65 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.17/0.65 fof(f336,plain,(
% 0.17/0.65 ~aSet0(xS)|sQ0_spl),
% 0.17/0.65 inference(component_clause,[status(thm)],[f334])).
% 0.17/0.65 fof(f337,definition,(
% 0.17/0.65 sQ1_spl <=> (aElement0(xx))),
% 0.17/0.65 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.17/0.65 fof(f340,plain,(
% 0.17/0.65 ~sQ0_spl|sQ1_spl),
% 0.17/0.65 inference(split_clause,[status(thm)],[f333,f334,f337])).
% 0.17/0.65 fof(f341,plain,(
% 0.17/0.65 $false|sQ0_spl),
% 0.17/0.65 inference(forward_subsumption_resolution,[status(thm)],[f336,f273])).
% 0.17/0.65 fof(f342,plain,(
% 0.17/0.65 sQ0_spl),
% 0.17/0.65 inference(contradiction_clause,[status(thm)],[f341])).
% 0.17/0.65 fof(f358,plain,(
% 0.17/0.65 ~aSet0(xQ)|aElement0(xy)),
% 0.17/0.65 inference(resolution,[status(thm)],[f284,f81])).
% 0.17/0.65 fof(f359,definition,(
% 0.17/0.65 sQ5_spl <=> (aSet0(xQ))),
% 0.17/0.65 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.17/0.65 fof(f361,plain,(
% 0.17/0.65 ~aSet0(xQ)|sQ5_spl),
% 0.17/0.65 inference(component_clause,[status(thm)],[f359])).
% 0.17/0.65 fof(f362,definition,(
% 0.17/0.65 sQ6_spl <=> (aElement0(xy))),
% 0.17/0.65 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.17/0.65 fof(f365,plain,(
% 0.17/0.65 ~sQ5_spl|sQ6_spl),
% 0.17/0.65 inference(split_clause,[status(thm)],[f358,f359,f362])).
% 0.17/0.65 fof(f366,plain,(
% 0.17/0.65 $false|sQ5_spl),
% 0.17/0.65 inference(forward_subsumption_resolution,[status(thm)],[f361,f280])).
% 0.17/0.65 fof(f367,plain,(
% 0.17/0.65 sQ5_spl),
% 0.17/0.65 inference(contradiction_clause,[status(thm)],[f366])).
% 0.17/0.65 fof(f384,definition,(
% 0.17/0.65 sQ10_spl <=> (aSet0(slbdtsldtrb0(xT,xk)))),
% 0.17/0.65 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.17/0.65 fof(f386,plain,(
% 0.17/0.65 ~aSet0(slbdtsldtrb0(xT,xk))|sQ10_spl),
% 0.17/0.65 inference(component_clause,[status(thm)],[f384])).
% 0.17/0.65 fof(f398,plain,(
% 0.17/0.65 ![X0]: (~aSet0(slbdtsldtrb0(xT,xk))|~aElementOf0(X0,slbdtsldtrb0(xS,xk))|aElementOf0(X0,slbdtsldtrb0(xT,xk)))),
% 0.17/0.65 inference(resolution,[status(thm)],[f103,f276])).
% 0.17/0.65 fof(f400,definition,(
% 0.17/0.65 ![X0]: (sQ12_spl <=> (~aElementOf0(X0,slbdtsldtrb0(xS,xk))|aElementOf0(X0,slbdtsldtrb0(xT,xk))))),
% 0.17/0.65 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.17/0.65 fof(f401,plain,(
% 0.17/0.65 ![X0]: (~aElementOf0(X0,slbdtsldtrb0(xS,xk))|aElementOf0(X0,slbdtsldtrb0(xT,xk))|~sQ12_spl)),
% 0.17/0.65 inference(component_clause,[status(thm)],[f400])).
% 0.17/0.65 fof(f403,plain,(
% 0.17/0.65 ~sQ10_spl|sQ12_spl),
% 0.17/0.65 inference(split_clause,[status(thm)],[f398,f384,f400])).
% 0.17/0.65 fof(f835,definition,(
% 0.17/0.65 sQ58_spl <=> (aSet0(sdtmndt0(xQ,xy)))),
% 0.17/0.65 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 0.17/0.65 fof(f837,plain,(
% 0.17/0.65 ~aSet0(sdtmndt0(xQ,xy))|sQ58_spl),
% 0.17/0.65 inference(component_clause,[status(thm)],[f835])).
% 0.17/0.65 fof(f872,plain,(
% 0.17/0.65 ~aSet0(xQ)|~aElement0(xy)|sQ58_spl),
% 0.17/0.65 inference(resolution,[status(thm)],[f312,f837])).
% 0.17/0.65 fof(f874,plain,(
% 0.17/0.65 ~sQ5_spl|~sQ6_spl|sQ58_spl),
% 0.17/0.65 inference(split_clause,[status(thm)],[f872,f359,f362,f835])).
% 0.17/0.65 fof(f954,plain,(
% 0.17/0.65 ~aSet0(sdtmndt0(xQ,xy))|~aElement0(xx)|aElementOf0(xx,xP)),
% 0.17/0.65 inference(paramodulation,[status(thm)],[f287,f308])).
% 0.17/0.65 fof(f955,definition,(
% 0.17/0.65 sQ76_spl <=> (aElementOf0(xx,xP))),
% 0.17/0.65 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 0.17/0.65 fof(f956,plain,(
% 0.17/0.65 aElementOf0(xx,xP)|~sQ76_spl),
% 0.17/0.65 inference(component_clause,[status(thm)],[f955])).
% 0.17/0.65 fof(f958,plain,(
% 0.17/0.65 ~sQ58_spl|~sQ1_spl|sQ76_spl),
% 0.17/0.65 inference(split_clause,[status(thm)],[f954,f835,f337,f955])).
% 0.17/0.65 fof(f1228,definition,(
% 0.17/0.65 sQ100_spl <=> (aElementOf0(sz00,szNzAzT0))),
% 0.17/0.65 introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition])).
% 0.17/0.65 fof(f1230,plain,(
% 0.17/0.65 ~aElementOf0(sz00,szNzAzT0)|sQ100_spl),
% 0.17/0.65 inference(component_clause,[status(thm)],[f1228])).
% 0.17/0.65 fof(f1232,definition,(
% 0.17/0.65 sQ101_spl <=> (aElementOf0(xk,szNzAzT0))),
% 0.17/0.65 introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition])).
% 0.17/0.65 fof(f1234,plain,(
% 0.17/0.65 ~aElementOf0(xk,szNzAzT0)|sQ101_spl),
% 0.17/0.65 inference(component_clause,[status(thm)],[f1232])).
% 0.17/0.67 fof(f1590,plain,(
% 0.17/0.67 ~aSet0(xT)|~aElementOf0(xk,szNzAzT0)|sQ10_spl),
% 0.17/0.67 inference(resolution,[status(thm)],[f328,f386])).
% 0.17/0.67 fof(f1593,definition,(
% 0.17/0.67 sQ153_spl <=> (aSet0(xT))),
% 0.17/0.67 introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition])).
% 0.17/0.67 fof(f1595,plain,(
% 0.17/0.67 ~aSet0(xT)|sQ153_spl),
% 0.17/0.67 inference(component_clause,[status(thm)],[f1593])).
% 0.17/0.67 fof(f1596,plain,(
% 0.17/0.67 ~sQ153_spl|~sQ101_spl|sQ10_spl),
% 0.17/0.67 inference(split_clause,[status(thm)],[f1590,f1593,f1232,f384])).
% 0.17/0.67 fof(f1598,plain,(
% 0.17/0.67 $false|sQ101_spl),
% 0.17/0.67 inference(forward_subsumption_resolution,[status(thm)],[f1234,f272])).
% 0.17/0.67 fof(f1599,plain,(
% 0.17/0.67 sQ101_spl),
% 0.17/0.67 inference(contradiction_clause,[status(thm)],[f1598])).
% 0.17/0.67 fof(f1629,plain,(
% 0.17/0.67 aElementOf0(xP,slbdtsldtrb0(xT,xk))|~sQ12_spl),
% 0.17/0.67 inference(resolution,[status(thm)],[f401,f288])).
% 0.17/0.67 fof(f1635,plain,(
% 0.17/0.67 ~aSet0(xT)|~aElementOf0(xk,szNzAzT0)|aSubsetOf0(xP,xT)|~sQ12_spl),
% 0.17/0.67 inference(resolution,[status(thm)],[f1629,f329])).
% 0.17/0.67 fof(f1637,definition,(
% 0.17/0.67 sQ161_spl <=> (aSubsetOf0(xP,xT))),
% 0.17/0.67 introduced(definition,[new_symbols(definition,[sQ161_spl])],[split_symbol_definition])).
% 0.17/0.67 fof(f1638,plain,(
% 0.17/0.67 aSubsetOf0(xP,xT)|~sQ161_spl),
% 0.17/0.67 inference(component_clause,[status(thm)],[f1637])).
% 0.17/0.67 fof(f1640,plain,(
% 0.17/0.67 ~sQ153_spl|~sQ101_spl|sQ161_spl|~sQ12_spl),
% 0.17/0.67 inference(split_clause,[status(thm)],[f1635,f1593,f1232,f1637,f400])).
% 0.17/0.67 fof(f1642,plain,(
% 0.17/0.67 $false|sQ153_spl),
% 0.17/0.67 inference(forward_subsumption_resolution,[status(thm)],[f1595,f274])).
% 0.17/0.67 fof(f1643,plain,(
% 0.17/0.67 sQ153_spl),
% 0.17/0.67 inference(contradiction_clause,[status(thm)],[f1642])).
% 0.17/0.67 fof(f1644,plain,(
% 0.17/0.67 ![X0]: (~aSet0(xT)|~aElementOf0(X0,xP)|aElementOf0(X0,xT)|~sQ161_spl)),
% 0.17/0.67 inference(resolution,[status(thm)],[f1638,f103])).
% 0.17/0.67 fof(f1648,definition,(
% 0.17/0.67 ![X0]: (sQ162_spl <=> (~aElementOf0(X0,xP)|aElementOf0(X0,xT)))),
% 0.17/0.67 introduced(definition,[new_symbols(definition,[sQ162_spl])],[split_symbol_definition])).
% 0.17/0.67 fof(f1649,plain,(
% 0.17/0.67 ![X0]: (~aElementOf0(X0,xP)|aElementOf0(X0,xT)|~sQ162_spl)),
% 0.17/0.67 inference(component_clause,[status(thm)],[f1648])).
% 0.17/0.67 fof(f1651,plain,(
% 0.17/0.67 ~sQ153_spl|sQ162_spl|~sQ161_spl),
% 0.17/0.67 inference(split_clause,[status(thm)],[f1644,f1593,f1648,f1637])).
% 0.17/0.67 fof(f1801,plain,(
% 0.17/0.67 $false|sQ100_spl),
% 0.17/0.67 inference(forward_subsumption_resolution,[status(thm)],[f1230,f152])).
% 0.17/0.67 fof(f1802,plain,(
% 0.17/0.67 sQ100_spl),
% 0.17/0.67 inference(contradiction_clause,[status(thm)],[f1801])).
% 0.17/0.67 fof(f1869,plain,(
% 0.17/0.67 aElementOf0(xx,xT)|~sQ162_spl|~sQ76_spl),
% 0.17/0.67 inference(resolution,[status(thm)],[f1649,f956])).
% 0.17/0.67 fof(f1874,plain,(
% 0.17/0.67 $false|~sQ162_spl|~sQ76_spl),
% 0.17/0.67 inference(forward_subsumption_resolution,[status(thm)],[f1869,f289])).
% 0.17/0.67 fof(f1875,plain,(
% 0.17/0.67 ~sQ162_spl|~sQ76_spl),
% 0.17/0.67 inference(contradiction_clause,[status(thm)],[f1874])).
% 0.17/0.67 fof(f1876,plain,(
% 0.17/0.67 $false),
% 0.17/0.67 inference(sat_refutation,[status(thm)],[f340,f342,f365,f367,f403,f874,f958,f1596,f1599,f1640,f1643,f1651,f1802,f1875])).
% 0.17/0.67 % SZS output end CNFRefutation for theBenchmark.p
% 0.17/0.70 % Elapsed time: 0.293921 seconds
% 0.17/0.70 % CPU time: 1.665753 seconds
% 0.17/0.70 % Total memory used: 127.074 MB
% 0.17/0.70 % Net memory used: 125.734 MB
%------------------------------------------------------------------------------