%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM583+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 : n014.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:16 PM UTC 2026
% Result : Theorem 9.40s 1.70s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM583+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.16/0.41 % Computer : n014.cluster.edu
% 0.16/0.41 % Model : x86_64 x86_64
% 0.16/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.41 % Memory : 8046.5625MB
% 0.16/0.41 % OS : Linux 6.8.0-71-generic
% 0.16/0.41 % CPULimit : 300
% 0.16/0.41 % WCLimit : 300
% 0.16/0.41 % DateTime : Mon Sep 21 02:41:51 UTC 2026
% 0.16/0.41 % CPUTime :
% 0.21/0.45 % Drodi V4.1.1
% 9.40/1.70 % Refutation found
% 9.40/1.70 % SZS status Theorem for theBenchmark: Theorem is valid
% 9.40/1.70 % SZS output start CNFRefutation for theBenchmark
% 9.40/1.70 fof(f3,axiom,(
% 9.40/1.70 (! [W0] :( aSet0(W0)=> (! [W1] :( aElementOf0(W1,W0)=> aElement0(W1) ) )) )),
% 9.40/1.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.40/1.70 fof(f10,definition,(
% 9.40/1.70 (! [W0] :( aSet0(W0)=> (! [W1] :( aSubsetOf0(W1,W0)<=> ( aSet0(W1)& (! [W2] :( aElementOf0(W2,W1)=> aElementOf0(W2,W0) ) )) ) )) )),
% 9.40/1.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.40/1.70 fof(f15,definition,(
% 9.40/1.70 (! [W0,W1] :( ( aSet0(W0)& aElement0(W1) )=> (! [W2] :( W2 = sdtpldt0(W0,W1)<=> ( aSet0(W2)& (! [W3] :( aElementOf0(W3,W2)<=> ( aElement0(W3)& ( aElementOf0(W3,W0)| W3 = W1 ) ) ) )) ) )) )),
% 9.40/1.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.40/1.70 fof(f16,definition,(
% 9.40/1.70 (! [W0,W1] :( ( aSet0(W0)& aElement0(W1) )=> (! [W2] :( W2 = sdtmndt0(W0,W1)<=> ( aSet0(W2)& (! [W3] :( aElementOf0(W3,W2)<=> ( aElement0(W3)& aElementOf0(W3,W0)& W3 != W1 ) ) )) ) )) )),
% 9.40/1.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.40/1.70 fof(f17,axiom,(
% 9.40/1.70 (! [W0] :( aSet0(W0)=> (! [W1] :( aElementOf0(W1,W0)=> sdtpldt0(sdtmndt0(W0,W1),W1) = W0 ) )) )),
% 9.40/1.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.40/1.70 fof(f75,hypothesis,(
% 9.40/1.70 ( aSet0(xS)& (! [W0] :( aElementOf0(W0,xS)=> aElementOf0(W0,szNzAzT0) ))& aSubsetOf0(xS,szNzAzT0)& isCountable0(xS) ) ),
% 9.40/1.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.40/1.70 fof(f86,hypothesis,(
% 9.40/1.70 ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))& (! [W0] :( aElementOf0(W0,sdtlpdtrp0(xN,xi))=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0) ))& aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))& (! [W0] :( aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))<=> ( aElement0(W0)& aElementOf0(W0,sdtlpdtrp0(xN,xi))& W0 != szmzizndt0(sdtlpdtrp0(xN,xi)) ) ))& aSet0(xQ)& (! [W0] :( aElementOf0(W0,xQ)=> aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) ))& aSubsetOf0(xQ,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))& sbrdtbr0(xQ) = xk& aElementOf0(xQ,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))),xk)) ) ),
% 9.40/1.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.40/1.70 fof(f88,hypothesis,(
% 9.40/1.70 ( (! [W0] :( aElementOf0(W0,sdtlpdtrp0(xN,xi))=> aElementOf0(W0,xS) ))& aSubsetOf0(sdtlpdtrp0(xN,xi),xS) ) ),
% 9.40/1.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.40/1.70 fof(f89,conjecture,(
% 9.40/1.70 ( ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))& (! [W0] :( aElementOf0(W0,sdtlpdtrp0(xN,xi))=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0) ) ))=> ( ( aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))& (! [W0] :( aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))<=> ( aElement0(W0)& ( aElementOf0(W0,xQ)| W0 = szmzizndt0(sdtlpdtrp0(xN,xi)) ) ) ) ))=> ( (! [W0] :( aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))=> aElementOf0(W0,xS) ))| aSubsetOf0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))),xS) ) ) ) ),
% 9.40/1.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.40/1.70 fof(f90,negated_conjecture,(
% 9.40/1.70 ~(( ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))& (! [W0] :( aElementOf0(W0,sdtlpdtrp0(xN,xi))=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0) ) ))=> ( ( aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))& (! [W0] :( aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))<=> ( aElement0(W0)& ( aElementOf0(W0,xQ)| W0 = szmzizndt0(sdtlpdtrp0(xN,xi)) ) ) ) ))=> ( (! [W0] :( aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))=> aElementOf0(W0,xS) ))| aSubsetOf0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))),xS) ) ) ) )),
% 9.40/1.70 inference(negated_conjecture,[status(cth)],[f89])).
% 9.40/1.70 fof(f97,plain,(
% 9.40/1.70 ![W0]: (~aSet0(W0)|(![W1]: (~aElementOf0(W1,W0)|aElement0(W1))))),
% 9.40/1.70 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 9.40/1.70 fof(f98,plain,(
% 9.40/1.70 ![X0,X1]: (~aSet0(X0)|~aElementOf0(X1,X0)|aElement0(X1))),
% 9.40/1.70 inference(cnf_transformation,[status(thm)],[f97])).
% 9.40/1.70 fof(f115,plain,(
% 9.40/1.70 ![W0]: (~aSet0(W0)|(![W1]: (aSubsetOf0(W1,W0)<=>(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0)))))))),
% 9.40/1.70 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 9.40/1.70 fof(f116,plain,(
% 9.40/1.70 ![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))))))))),
% 9.40/1.70 inference(NNF_transformation,[status(thm)],[f115])).
% 9.40/1.70 fof(f117,plain,(
% 9.40/1.70 ![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))))))))),
% 9.40/1.70 inference(miniscoping,[status(thm)],[f116])).
% 9.40/1.70 fof(f118,plain,(
% 9.40/1.70 ![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)))))))),
% 9.40/1.70 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W2,sK1_skl(W1,W0))],[f117])).
% 9.40/1.70 fof(f119,plain,(
% 9.40/1.70 ![X0,X1]: (~aSet0(X0)|~aSubsetOf0(X1,X0)|aSet0(X1))),
% 9.40/1.70 inference(cnf_transformation,[status(thm)],[f118])).
% 9.40/1.70 fof(f131,plain,(
% 9.40/1.70 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|(![W2]: (W2=sdtpldt0(W0,W1)<=>(aSet0(W2)&(![W3]: (aElementOf0(W3,W2)<=>(aElement0(W3)&(aElementOf0(W3,W0)|W3=W1))))))))),
% 9.40/1.70 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 9.40/1.70 fof(f132,plain,(
% 9.40/1.70 ![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))))))))))),
% 9.40/1.70 inference(NNF_transformation,[status(thm)],[f131])).
% 9.40/1.70 fof(f133,plain,(
% 9.40/1.70 ![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))))))))))),
% 9.40/1.70 inference(miniscoping,[status(thm)],[f132])).
% 9.40/1.70 fof(f134,plain,(
% 9.40/1.70 ![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)))))))))),
% 9.40/1.70 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(W3,sK2_skl(W2,W1,W0))],[f133])).
% 9.40/1.70 fof(f139,plain,(
% 9.40/1.70 ![X0,X1,X2,X3]: (~aSet0(X0)|~aElement0(X1)|~X2=sdtpldt0(X0,X1)|aElementOf0(X3,X2)|~aElement0(X3)|~X3=X1)),
% 9.40/1.70 inference(cnf_transformation,[status(thm)],[f134])).
% 9.40/1.70 fof(f144,plain,(
% 9.40/1.70 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|(![W2]: (W2=sdtmndt0(W0,W1)<=>(aSet0(W2)&(![W3]: (aElementOf0(W3,W2)<=>((aElement0(W3)&aElementOf0(W3,W0))&~W3=W1)))))))),
% 9.40/1.70 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 9.40/1.70 fof(f145,definition,(
% 9.40/1.70 ![W0,W1,W3]: (sP0_prd(W3,W1,W0)<=>((aElement0(W3)&aElementOf0(W3,W0))&~W3=W1))),
% 9.40/1.70 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 9.40/1.70 fof(f146,plain,(
% 9.40/1.70 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|(![W2]: (W2=sdtmndt0(W0,W1)<=>(aSet0(W2)&(![W3]: (aElementOf0(W3,W2)<=>sP0_prd(W3,W1,W0)))))))),
% 9.40/1.70 inference(formula_renaming,[status(thm)],[f144,f145])).
% 9.40/1.70 fof(f147,plain,(
% 9.40/1.70 ![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)))))))))),
% 9.40/1.70 inference(NNF_transformation,[status(thm)],[f146])).
% 9.40/1.70 fof(f148,plain,(
% 9.40/1.70 ![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)))))))))),
% 9.40/1.70 inference(miniscoping,[status(thm)],[f147])).
% 9.40/1.70 fof(f149,plain,(
% 9.40/1.70 ![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))))))))),
% 9.40/1.70 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(W3,sK3_skl(W2,W1,W0))],[f148])).
% 9.40/1.70 fof(f150,plain,(
% 9.40/1.70 ![X0,X1,X2]: (~aSet0(X0)|~aElement0(X1)|~X2=sdtmndt0(X0,X1)|aSet0(X2))),
% 9.40/1.70 inference(cnf_transformation,[status(thm)],[f149])).
% 9.40/1.70 fof(f155,plain,(
% 9.40/1.70 ![W0]: (~aSet0(W0)|(![W1]: (~aElementOf0(W1,W0)|sdtpldt0(sdtmndt0(W0,W1),W1)=W0)))),
% 9.40/1.70 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 9.40/1.70 fof(f156,plain,(
% 9.40/1.70 ![X0,X1]: (~aSet0(X0)|~aElementOf0(X1,X0)|sdtpldt0(sdtmndt0(X0,X1),X1)=X0)),
% 9.40/1.70 inference(cnf_transformation,[status(thm)],[f155])).
% 9.40/1.70 fof(f350,plain,(
% 9.40/1.70 ((aSet0(xS)&(![W0]: (~aElementOf0(W0,xS)|aElementOf0(W0,szNzAzT0))))&aSubsetOf0(xS,szNzAzT0))&isCountable0(xS)),
% 9.40/1.70 inference(pre_NNF_transformation,[status(thm)],[f75])).
% 9.40/1.70 fof(f351,plain,(
% 9.40/1.70 aSet0(xS)),
% 9.40/1.70 inference(cnf_transformation,[status(thm)],[f350])).
% 9.40/1.70 fof(f422,plain,(
% 9.40/1.70 (((((((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))&(![W0]: (~aElementOf0(W0,sdtlpdtrp0(xN,xi))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0))))&aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))&(![W0]: (aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))<=>((aElement0(W0)&aElementOf0(W0,sdtlpdtrp0(xN,xi)))&~W0=szmzizndt0(sdtlpdtrp0(xN,xi))))))&aSet0(xQ))&(![W0]: (~aElementOf0(W0,xQ)|aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))))&aSubsetOf0(xQ,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))&sbrdtbr0(xQ)=xk)&aElementOf0(xQ,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))),xk))),
% 9.40/1.70 inference(pre_NNF_transformation,[status(thm)],[f86])).
% 9.40/1.70 fof(f423,plain,(
% 9.40/1.70 (((((((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))&(![W0]: (~aElementOf0(W0,sdtlpdtrp0(xN,xi))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0))))&aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))&(![W0]: ((~aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))|((aElement0(W0)&aElementOf0(W0,sdtlpdtrp0(xN,xi)))&~W0=szmzizndt0(sdtlpdtrp0(xN,xi))))&(aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))|((~aElement0(W0)|~aElementOf0(W0,sdtlpdtrp0(xN,xi)))|W0=szmzizndt0(sdtlpdtrp0(xN,xi)))))))&aSet0(xQ))&(![W0]: (~aElementOf0(W0,xQ)|aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))))&aSubsetOf0(xQ,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))&sbrdtbr0(xQ)=xk)&aElementOf0(xQ,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))),xk))),
% 9.40/1.70 inference(NNF_transformation,[status(thm)],[f422])).
% 9.40/1.70 fof(f424,plain,(
% 9.40/1.70 (((((((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))&(![W0]: (~aElementOf0(W0,sdtlpdtrp0(xN,xi))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0))))&aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))&((![W0]: (~aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))|((aElement0(W0)&aElementOf0(W0,sdtlpdtrp0(xN,xi)))&~W0=szmzizndt0(sdtlpdtrp0(xN,xi)))))&(![W0]: (aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))|((~aElement0(W0)|~aElementOf0(W0,sdtlpdtrp0(xN,xi)))|W0=szmzizndt0(sdtlpdtrp0(xN,xi)))))))&aSet0(xQ))&(![W0]: (~aElementOf0(W0,xQ)|aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))))&aSubsetOf0(xQ,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))&sbrdtbr0(xQ)=xk)&aElementOf0(xQ,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))),xk))),
% 9.40/1.70 inference(miniscoping,[status(thm)],[f423])).
% 9.40/1.70 fof(f429,plain,(
% 9.40/1.70 ![X0]: (~aElementOf0(X0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))|aElementOf0(X0,sdtlpdtrp0(xN,xi)))),
% 9.40/1.70 inference(cnf_transformation,[status(thm)],[f424])).
% 9.40/1.70 fof(f433,plain,(
% 9.40/1.70 ![X0]: (~aElementOf0(X0,xQ)|aElementOf0(X0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))),
% 9.40/1.70 inference(cnf_transformation,[status(thm)],[f424])).
% 9.40/1.70 fof(f448,plain,(
% 9.40/1.70 (![W0]: (~aElementOf0(W0,sdtlpdtrp0(xN,xi))|aElementOf0(W0,xS)))&aSubsetOf0(sdtlpdtrp0(xN,xi),xS)),
% 9.40/1.70 inference(pre_NNF_transformation,[status(thm)],[f88])).
% 9.40/1.70 fof(f449,plain,(
% 9.40/1.70 ![X0]: (~aElementOf0(X0,sdtlpdtrp0(xN,xi))|aElementOf0(X0,xS))),
% 9.40/1.70 inference(cnf_transformation,[status(thm)],[f448])).
% 9.40/1.70 fof(f450,plain,(
% 9.40/1.70 aSubsetOf0(sdtlpdtrp0(xN,xi),xS)),
% 9.40/1.70 inference(cnf_transformation,[status(thm)],[f448])).
% 9.40/1.70 fof(f451,plain,(
% 9.40/1.70 ((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))&(![W0]: (~aElementOf0(W0,sdtlpdtrp0(xN,xi))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0))))&((aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))&(![W0]: (aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))<=>(aElement0(W0)&(aElementOf0(W0,xQ)|W0=szmzizndt0(sdtlpdtrp0(xN,xi)))))))&((?[W0]: (aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))&~aElementOf0(W0,xS)))&~aSubsetOf0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))),xS))))),
% 9.40/1.70 inference(pre_NNF_transformation,[status(thm)],[f90])).
% 9.40/1.70 fof(f452,plain,(
% 9.40/1.70 (aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))&(![W0]: (~aElementOf0(W0,sdtlpdtrp0(xN,xi))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0))))&((aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))&(![W0]: ((~aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))|(aElement0(W0)&(aElementOf0(W0,xQ)|W0=szmzizndt0(sdtlpdtrp0(xN,xi)))))&(aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))|(~aElement0(W0)|(~aElementOf0(W0,xQ)&~W0=szmzizndt0(sdtlpdtrp0(xN,xi))))))))&((?[W0]: (aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))&~aElementOf0(W0,xS)))&~aSubsetOf0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))),xS)))),
% 9.40/1.70 inference(NNF_transformation,[status(thm)],[f451])).
% 9.40/1.70 fof(f453,plain,(
% 9.40/1.70 (aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))&(![W0]: (~aElementOf0(W0,sdtlpdtrp0(xN,xi))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0))))&((aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))&((![W0]: (~aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))|(aElement0(W0)&(aElementOf0(W0,xQ)|W0=szmzizndt0(sdtlpdtrp0(xN,xi))))))&(![W0]: (aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))|(~aElement0(W0)|(~aElementOf0(W0,xQ)&~W0=szmzizndt0(sdtlpdtrp0(xN,xi))))))))&((?[W0]: (aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))&~aElementOf0(W0,xS)))&~aSubsetOf0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))),xS)))),
% 9.40/1.70 inference(miniscoping,[status(thm)],[f452])).
% 9.40/1.70 fof(f454,plain,(
% 9.40/1.70 (aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))&(![W0]: (~aElementOf0(W0,sdtlpdtrp0(xN,xi))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0))))&((aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))&((![W0]: (~aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))|(aElement0(W0)&(aElementOf0(W0,xQ)|W0=szmzizndt0(sdtlpdtrp0(xN,xi))))))&(![W0]: (aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))|(~aElement0(W0)|(~aElementOf0(W0,xQ)&~W0=szmzizndt0(sdtlpdtrp0(xN,xi))))))))&((aElementOf0(sK24_skl,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))&~aElementOf0(sK24_skl,xS))&~aSubsetOf0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))),xS)))),
% 9.40/1.70 inference(skolemize,[status(esa),new_symbols(skolem,[sK24_skl]),skolemize(W0,sK24_skl)],[f453])).
% 9.40/1.70 fof(f455,plain,(
% 9.40/1.70 aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))),
% 9.40/1.70 inference(cnf_transformation,[status(thm)],[f454])).
% 9.40/1.70 fof(f457,plain,(
% 9.40/1.70 aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))),
% 9.40/1.70 inference(cnf_transformation,[status(thm)],[f454])).
% 9.40/1.70 fof(f459,plain,(
% 9.40/1.70 ![X0]: (~aElementOf0(X0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))|aElementOf0(X0,xQ)|X0=szmzizndt0(sdtlpdtrp0(xN,xi)))),
% 9.40/1.70 inference(cnf_transformation,[status(thm)],[f454])).
% 9.40/1.70 fof(f462,plain,(
% 9.40/1.70 aElementOf0(sK24_skl,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))),
% 9.40/1.70 inference(cnf_transformation,[status(thm)],[f454])).
% 9.40/1.70 fof(f463,plain,(
% 9.40/1.70 ~aElementOf0(sK24_skl,xS)),
% 9.40/1.70 inference(cnf_transformation,[status(thm)],[f454])).
% 9.40/1.70 fof(f547,plain,(
% 9.40/1.70 ![X0,X1]: (~aSet0(X0)|~aElement0(X1)|aElementOf0(X1,sdtpldt0(X0,X1))|~aElement0(X1))),
% 9.40/1.70 inference(destructive_equality_resolution,[status(thm)],[f139])).
% 9.40/1.70 fof(f548,plain,(
% 9.40/1.70 ![X0,X1]: (~aSet0(X0)|~aElement0(X1)|aElementOf0(X1,sdtpldt0(X0,X1)))),
% 9.40/1.70 inference(duplicate_literals_removal,[status(thm)],[f547])).
% 9.40/1.70 fof(f549,plain,(
% 9.40/1.70 ![X0,X1]: (~aSet0(X0)|~aElement0(X1)|aSet0(sdtmndt0(X0,X1)))),
% 9.40/1.70 inference(destructive_equality_resolution,[status(thm)],[f150])).
% 9.40/1.70 fof(f596,plain,(
% 9.40/1.70 ~aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))|aElement0(sK24_skl)),
% 9.40/1.70 inference(resolution,[status(thm)],[f98,f462])).
% 9.40/1.70 fof(f598,definition,(
% 9.40/1.70 sQ0_spl <=> (aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))))),
% 9.40/1.70 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 9.40/1.70 fof(f600,plain,(
% 9.40/1.70 ~aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))|sQ0_spl),
% 9.40/1.70 inference(component_clause,[status(thm)],[f598])).
% 9.40/1.70 fof(f601,definition,(
% 9.40/1.70 sQ1_spl <=> (aElement0(sK24_skl))),
% 9.40/1.70 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 9.40/1.70 fof(f604,plain,(
% 9.40/1.70 ~sQ0_spl|sQ1_spl),
% 9.40/1.70 inference(split_clause,[status(thm)],[f596,f598,f601])).
% 9.40/1.70 fof(f605,definition,(
% 9.40/1.70 sQ2_spl <=> (aSet0(sdtlpdtrp0(xN,xi)))),
% 9.40/1.70 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 9.40/1.70 fof(f612,plain,(
% 9.40/1.70 $false|sQ0_spl),
% 9.40/1.70 inference(forward_subsumption_resolution,[status(thm)],[f600,f457])).
% 9.40/1.70 fof(f613,plain,(
% 9.40/1.70 sQ0_spl),
% 9.40/1.70 inference(contradiction_clause,[status(thm)],[f612])).
% 9.40/1.70 fof(f615,plain,(
% 9.40/1.70 ~aSet0(xS)|aSet0(sdtlpdtrp0(xN,xi))),
% 9.40/1.70 inference(resolution,[status(thm)],[f450,f119])).
% 9.40/1.70 fof(f616,definition,(
% 9.40/1.70 sQ4_spl <=> (aSet0(xS))),
% 9.40/1.70 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 9.40/1.70 fof(f618,plain,(
% 9.40/1.70 ~aSet0(xS)|sQ4_spl),
% 9.40/1.70 inference(component_clause,[status(thm)],[f616])).
% 9.40/1.70 fof(f619,plain,(
% 9.40/1.70 ~sQ4_spl|sQ2_spl),
% 9.40/1.70 inference(split_clause,[status(thm)],[f615,f616,f605])).
% 9.40/1.70 fof(f620,plain,(
% 9.40/1.70 $false|sQ4_spl),
% 9.40/1.70 inference(forward_subsumption_resolution,[status(thm)],[f618,f351])).
% 9.40/1.70 fof(f621,plain,(
% 9.40/1.70 sQ4_spl),
% 9.40/1.70 inference(contradiction_clause,[status(thm)],[f620])).
% 9.40/1.70 fof(f708,plain,(
% 9.40/1.70 aElementOf0(sK24_skl,xQ)|sK24_skl=szmzizndt0(sdtlpdtrp0(xN,xi))),
% 9.40/1.70 inference(resolution,[status(thm)],[f459,f462])).
% 9.40/1.70 fof(f712,definition,(
% 9.40/1.70 sQ20_spl <=> (aElementOf0(sK24_skl,xQ))),
% 9.40/1.70 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 9.40/1.70 fof(f713,plain,(
% 9.40/1.70 aElementOf0(sK24_skl,xQ)|~sQ20_spl),
% 9.40/1.70 inference(component_clause,[status(thm)],[f712])).
% 9.40/1.70 fof(f715,definition,(
% 9.40/1.70 sQ21_spl <=> (sK24_skl=szmzizndt0(sdtlpdtrp0(xN,xi)))),
% 9.40/1.70 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 9.40/1.70 fof(f716,plain,(
% 9.40/1.70 sK24_skl=szmzizndt0(sdtlpdtrp0(xN,xi))|~sQ21_spl),
% 9.40/1.70 inference(component_clause,[status(thm)],[f715])).
% 9.40/1.70 fof(f718,plain,(
% 9.40/1.70 sQ20_spl|sQ21_spl),
% 9.40/1.70 inference(split_clause,[status(thm)],[f708,f712,f715])).
% 9.40/1.70 fof(f749,plain,(
% 9.40/1.70 aElementOf0(sK24_skl,sdtlpdtrp0(xN,xi))|~sQ21_spl),
% 9.40/1.70 inference(backward_demodulation,[status(thm)],[f716,f455])).
% 9.40/1.70 fof(f946,plain,(
% 9.40/1.70 ~aSet0(sdtlpdtrp0(xN,xi))|sdtpldt0(sdtmndt0(sdtlpdtrp0(xN,xi),sK24_skl),sK24_skl)=sdtlpdtrp0(xN,xi)|~sQ21_spl),
% 9.40/1.70 inference(resolution,[status(thm)],[f749,f156])).
% 9.40/1.70 fof(f948,definition,(
% 9.40/1.70 sQ50_spl <=> (sdtpldt0(sdtmndt0(sdtlpdtrp0(xN,xi),sK24_skl),sK24_skl)=sdtlpdtrp0(xN,xi))),
% 9.40/1.70 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 9.40/1.70 fof(f949,plain,(
% 9.40/1.70 sdtpldt0(sdtmndt0(sdtlpdtrp0(xN,xi),sK24_skl),sK24_skl)=sdtlpdtrp0(xN,xi)|~sQ50_spl),
% 9.40/1.70 inference(component_clause,[status(thm)],[f948])).
% 9.40/1.70 fof(f951,plain,(
% 9.40/1.70 ~sQ2_spl|sQ50_spl|~sQ21_spl),
% 9.40/1.71 inference(split_clause,[status(thm)],[f946,f605,f948,f715])).
% 9.40/1.71 fof(f1615,plain,(
% 9.40/1.71 ~aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),sK24_skl))|~aElement0(sK24_skl)|aElementOf0(sK24_skl,sdtlpdtrp0(xN,xi))|~sQ50_spl),
% 9.40/1.71 inference(paramodulation,[status(thm)],[f949,f548])).
% 9.40/1.71 fof(f1617,definition,(
% 9.40/1.71 sQ117_spl <=> (aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),sK24_skl)))),
% 9.40/1.71 introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition])).
% 9.40/1.71 fof(f1619,plain,(
% 9.40/1.71 ~aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),sK24_skl))|sQ117_spl),
% 9.40/1.71 inference(component_clause,[status(thm)],[f1617])).
% 9.40/1.71 fof(f1625,definition,(
% 9.40/1.71 sQ119_spl <=> (aElementOf0(sK24_skl,sdtlpdtrp0(xN,xi)))),
% 9.40/1.71 introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition])).
% 9.40/1.71 fof(f1626,plain,(
% 9.40/1.71 aElementOf0(sK24_skl,sdtlpdtrp0(xN,xi))|~sQ119_spl),
% 9.40/1.71 inference(component_clause,[status(thm)],[f1625])).
% 9.40/1.71 fof(f1628,plain,(
% 9.40/1.71 ~sQ117_spl|~sQ1_spl|sQ119_spl|~sQ50_spl),
% 9.40/1.71 inference(split_clause,[status(thm)],[f1615,f1617,f601,f1625,f948])).
% 9.40/1.71 fof(f1792,plain,(
% 9.40/1.71 ~aSet0(sdtlpdtrp0(xN,xi))|~aElement0(sK24_skl)|sQ117_spl),
% 9.40/1.71 inference(resolution,[status(thm)],[f1619,f549])).
% 9.40/1.71 fof(f1793,plain,(
% 9.40/1.71 ~sQ2_spl|~sQ1_spl|sQ117_spl),
% 9.40/1.71 inference(split_clause,[status(thm)],[f1792,f605,f601,f1617])).
% 9.40/1.71 fof(f6946,plain,(
% 9.40/1.71 aElementOf0(sK24_skl,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))|~sQ20_spl),
% 9.40/1.71 inference(resolution,[status(thm)],[f433,f713])).
% 9.40/1.71 fof(f11755,plain,(
% 9.40/1.71 aElementOf0(sK24_skl,sdtlpdtrp0(xN,xi))|~sQ20_spl),
% 9.40/1.71 inference(resolution,[status(thm)],[f429,f6946])).
% 9.40/1.71 fof(f11756,plain,(
% 9.40/1.71 sQ119_spl|~sQ20_spl),
% 9.40/1.71 inference(split_clause,[status(thm)],[f11755,f1625,f712])).
% 9.40/1.71 fof(f11761,plain,(
% 9.40/1.71 aElementOf0(sK24_skl,xS)|~sQ119_spl),
% 9.40/1.71 inference(resolution,[status(thm)],[f1626,f449])).
% 9.40/1.71 fof(f11771,plain,(
% 9.40/1.71 $false|~sQ119_spl),
% 9.40/1.71 inference(forward_subsumption_resolution,[status(thm)],[f11761,f463])).
% 9.40/1.71 fof(f11772,plain,(
% 9.40/1.71 ~sQ119_spl),
% 9.40/1.71 inference(contradiction_clause,[status(thm)],[f11771])).
% 9.40/1.71 fof(f11773,plain,(
% 9.40/1.71 $false),
% 9.40/1.71 inference(sat_refutation,[status(thm)],[f604,f613,f619,f621,f718,f951,f1628,f1793,f11756,f11772])).
% 9.40/1.71 % SZS output end CNFRefutation for theBenchmark.p
% 1.71/1.76 % Elapsed time: 1.326682 seconds
% 1.71/1.76 % CPU time: 10.000259 seconds
% 1.71/1.76 % Total memory used: 190.828 MB
% 1.71/1.76 % Net memory used: 185.195 MB
%------------------------------------------------------------------------------