%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM537+2 : 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 : n003.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:09 PM UTC 2026
% Result : Theorem 0.14s 0.48s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM537+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n003.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 02:40:00 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 0.14/0.48 % Refutation found
% 0.14/0.48 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.48 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.48 fof(f3,axiom,(
% 0.14/0.48 (! [W0] :( aSet0(W0)=> (! [W1] :( aElementOf0(W1,W0)=> aElement0(W1) ) )) )),
% 0.14/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.48 fof(f18,hypothesis,(
% 0.14/0.48 ( aElement0(xx)& aSet0(xS) ) ),
% 0.14/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.48 fof(f19,hypothesis,(
% 0.14/0.48 ~ aElementOf0(xx,xS) ),
% 0.14/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.48 fof(f20,conjecture,(
% 0.14/0.48 ( ( ( aSet0(sdtpldt0(xS,xx))& (! [W0] :( aElementOf0(W0,sdtpldt0(xS,xx))<=> ( aElement0(W0)& ( aElementOf0(W0,xS)| W0 = xx ) ) ) ))=> ( ( aSet0(sdtmndt0(sdtpldt0(xS,xx),xx))& (! [W0] :( aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx))<=> ( aElement0(W0)& aElementOf0(W0,sdtpldt0(xS,xx))& W0 != xx ) ) ))=> ( (! [W0] :( aElementOf0(W0,xS)=> aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx)) ))| aSubsetOf0(xS,sdtmndt0(sdtpldt0(xS,xx),xx)) ) ) )& ( ( aSet0(sdtpldt0(xS,xx))& (! [W0] :( aElementOf0(W0,sdtpldt0(xS,xx))<=> ( aElement0(W0)& ( aElementOf0(W0,xS)| W0 = xx ) ) ) ))=> ( ( aSet0(sdtmndt0(sdtpldt0(xS,xx),xx))& (! [W0] :( aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx))<=> ( aElement0(W0)& aElementOf0(W0,sdtpldt0(xS,xx))& W0 != xx ) ) ))=> ( (! [W0] :( aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx))=> aElementOf0(W0,xS) ))| aSubsetOf0(sdtmndt0(sdtpldt0(xS,xx),xx),xS) ) ) ) ) ),
% 0.14/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.48 fof(f21,negated_conjecture,(
% 0.14/0.48 ~(( ( ( aSet0(sdtpldt0(xS,xx))& (! [W0] :( aElementOf0(W0,sdtpldt0(xS,xx))<=> ( aElement0(W0)& ( aElementOf0(W0,xS)| W0 = xx ) ) ) ))=> ( ( aSet0(sdtmndt0(sdtpldt0(xS,xx),xx))& (! [W0] :( aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx))<=> ( aElement0(W0)& aElementOf0(W0,sdtpldt0(xS,xx))& W0 != xx ) ) ))=> ( (! [W0] :( aElementOf0(W0,xS)=> aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx)) ))| aSubsetOf0(xS,sdtmndt0(sdtpldt0(xS,xx),xx)) ) ) )& ( ( aSet0(sdtpldt0(xS,xx))& (! [W0] :( aElementOf0(W0,sdtpldt0(xS,xx))<=> ( aElement0(W0)& ( aElementOf0(W0,xS)| W0 = xx ) ) ) ))=> ( ( aSet0(sdtmndt0(sdtpldt0(xS,xx),xx))& (! [W0] :( aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx))<=> ( aElement0(W0)& aElementOf0(W0,sdtpldt0(xS,xx))& W0 != xx ) ) ))=> ( (! [W0] :( aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx))=> aElementOf0(W0,xS) ))| aSubsetOf0(sdtmndt0(sdtpldt0(xS,xx),xx),xS) ) ) ) ) )),
% 0.14/0.48 inference(negated_conjecture,[status(cth)],[f20])).
% 0.14/0.48 fof(f28,plain,(
% 0.14/0.48 ![W0]: (~aSet0(W0)|(![W1]: (~aElementOf0(W1,W0)|aElement0(W1))))),
% 0.14/0.48 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.14/0.48 fof(f29,plain,(
% 0.14/0.48 ![X0,X1]: (~aSet0(X0)|~aElementOf0(X1,X0)|aElement0(X1))),
% 0.14/0.48 inference(cnf_transformation,[status(thm)],[f28])).
% 0.14/0.48 fof(f89,plain,(
% 0.14/0.48 aSet0(xS)),
% 0.14/0.48 inference(cnf_transformation,[status(thm)],[f18])).
% 0.14/0.48 fof(f90,plain,(
% 0.14/0.48 ~aElementOf0(xx,xS)),
% 0.14/0.48 inference(cnf_transformation,[status(thm)],[f19])).
% 0.14/0.48 fof(f91,plain,(
% 0.14/0.48 (((aSet0(sdtpldt0(xS,xx))&(![W0]: (aElementOf0(W0,sdtpldt0(xS,xx))<=>(aElement0(W0)&(aElementOf0(W0,xS)|W0=xx)))))&((aSet0(sdtmndt0(sdtpldt0(xS,xx),xx))&(![W0]: (aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx))<=>((aElement0(W0)&aElementOf0(W0,sdtpldt0(xS,xx)))&~W0=xx))))&((?[W0]: (aElementOf0(W0,xS)&~aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx))))&~aSubsetOf0(xS,sdtmndt0(sdtpldt0(xS,xx),xx)))))|((aSet0(sdtpldt0(xS,xx))&(![W0]: (aElementOf0(W0,sdtpldt0(xS,xx))<=>(aElement0(W0)&(aElementOf0(W0,xS)|W0=xx)))))&((aSet0(sdtmndt0(sdtpldt0(xS,xx),xx))&(![W0]: (aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx))<=>((aElement0(W0)&aElementOf0(W0,sdtpldt0(xS,xx)))&~W0=xx))))&((?[W0]: (aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx))&~aElementOf0(W0,xS)))&~aSubsetOf0(sdtmndt0(sdtpldt0(xS,xx),xx),xS)))))),
% 0.14/0.48 inference(pre_NNF_transformation,[status(thm)],[f21])).
% 0.14/0.48 fof(f92,definition,(
% 0.14/0.48 sP1_prd<=>((aSet0(sdtpldt0(xS,xx))&(![W0]: (aElementOf0(W0,sdtpldt0(xS,xx))<=>(aElement0(W0)&(aElementOf0(W0,xS)|W0=xx)))))&((aSet0(sdtmndt0(sdtpldt0(xS,xx),xx))&(![W0]: (aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx))<=>((aElement0(W0)&aElementOf0(W0,sdtpldt0(xS,xx)))&~W0=xx))))&((?[W0]: (aElementOf0(W0,xS)&~aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx))))&~aSubsetOf0(xS,sdtmndt0(sdtpldt0(xS,xx),xx)))))),
% 0.14/0.48 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 0.14/0.48 fof(f93,plain,(
% 0.14/0.48 sP1_prd|((aSet0(sdtpldt0(xS,xx))&(![W0]: (aElementOf0(W0,sdtpldt0(xS,xx))<=>(aElement0(W0)&(aElementOf0(W0,xS)|W0=xx)))))&((aSet0(sdtmndt0(sdtpldt0(xS,xx),xx))&(![W0]: (aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx))<=>((aElement0(W0)&aElementOf0(W0,sdtpldt0(xS,xx)))&~W0=xx))))&((?[W0]: (aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx))&~aElementOf0(W0,xS)))&~aSubsetOf0(sdtmndt0(sdtpldt0(xS,xx),xx),xS))))),
% 0.14/0.48 inference(formula_renaming,[status(thm)],[f91,f92])).
% 0.14/0.48 fof(f94,plain,(
% 0.14/0.48 sP1_prd|((aSet0(sdtpldt0(xS,xx))&(![W0]: ((~aElementOf0(W0,sdtpldt0(xS,xx))|(aElement0(W0)&(aElementOf0(W0,xS)|W0=xx)))&(aElementOf0(W0,sdtpldt0(xS,xx))|(~aElement0(W0)|(~aElementOf0(W0,xS)&~W0=xx))))))&((aSet0(sdtmndt0(sdtpldt0(xS,xx),xx))&(![W0]: ((~aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx))|((aElement0(W0)&aElementOf0(W0,sdtpldt0(xS,xx)))&~W0=xx))&(aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx))|((~aElement0(W0)|~aElementOf0(W0,sdtpldt0(xS,xx)))|W0=xx)))))&((?[W0]: (aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx))&~aElementOf0(W0,xS)))&~aSubsetOf0(sdtmndt0(sdtpldt0(xS,xx),xx),xS))))),
% 0.14/0.48 inference(NNF_transformation,[status(thm)],[f93])).
% 0.14/0.48 fof(f95,plain,(
% 0.14/0.48 sP1_prd|((aSet0(sdtpldt0(xS,xx))&((![W0]: (~aElementOf0(W0,sdtpldt0(xS,xx))|(aElement0(W0)&(aElementOf0(W0,xS)|W0=xx))))&(![W0]: (aElementOf0(W0,sdtpldt0(xS,xx))|(~aElement0(W0)|(~aElementOf0(W0,xS)&~W0=xx))))))&((aSet0(sdtmndt0(sdtpldt0(xS,xx),xx))&((![W0]: (~aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx))|((aElement0(W0)&aElementOf0(W0,sdtpldt0(xS,xx)))&~W0=xx)))&(![W0]: (aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx))|((~aElement0(W0)|~aElementOf0(W0,sdtpldt0(xS,xx)))|W0=xx)))))&((?[W0]: (aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx))&~aElementOf0(W0,xS)))&~aSubsetOf0(sdtmndt0(sdtpldt0(xS,xx),xx),xS))))),
% 0.14/0.48 inference(miniscoping,[status(thm)],[f94])).
% 0.14/0.48 fof(f96,plain,(
% 0.14/0.48 sP1_prd|((aSet0(sdtpldt0(xS,xx))&((![W0]: (~aElementOf0(W0,sdtpldt0(xS,xx))|(aElement0(W0)&(aElementOf0(W0,xS)|W0=xx))))&(![W0]: (aElementOf0(W0,sdtpldt0(xS,xx))|(~aElement0(W0)|(~aElementOf0(W0,xS)&~W0=xx))))))&((aSet0(sdtmndt0(sdtpldt0(xS,xx),xx))&((![W0]: (~aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx))|((aElement0(W0)&aElementOf0(W0,sdtpldt0(xS,xx)))&~W0=xx)))&(![W0]: (aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx))|((~aElement0(W0)|~aElementOf0(W0,sdtpldt0(xS,xx)))|W0=xx)))))&((aElementOf0(sK4_skl,sdtmndt0(sdtpldt0(xS,xx),xx))&~aElementOf0(sK4_skl,xS))&~aSubsetOf0(sdtmndt0(sdtpldt0(xS,xx),xx),xS))))),
% 0.14/0.48 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(W0,sK4_skl)],[f95])).
% 0.14/0.48 fof(f98,plain,(
% 0.14/0.48 ![X0]: (sP1_prd|~aElementOf0(X0,sdtpldt0(xS,xx))|aElement0(X0))),
% 0.14/0.48 inference(cnf_transformation,[status(thm)],[f96])).
% 0.14/0.48 fof(f99,plain,(
% 0.14/0.48 ![X0]: (sP1_prd|~aElementOf0(X0,sdtpldt0(xS,xx))|aElementOf0(X0,xS)|X0=xx)),
% 0.14/0.48 inference(cnf_transformation,[status(thm)],[f96])).
% 0.14/0.48 fof(f104,plain,(
% 0.14/0.48 ![X0]: (sP1_prd|~aElementOf0(X0,sdtmndt0(sdtpldt0(xS,xx),xx))|aElementOf0(X0,sdtpldt0(xS,xx)))),
% 0.14/0.48 inference(cnf_transformation,[status(thm)],[f96])).
% 0.14/0.48 fof(f105,plain,(
% 0.14/0.48 ![X0]: (sP1_prd|~aElementOf0(X0,sdtmndt0(sdtpldt0(xS,xx),xx))|~X0=xx)),
% 0.14/0.48 inference(cnf_transformation,[status(thm)],[f96])).
% 0.14/0.48 fof(f107,plain,(
% 0.14/0.48 sP1_prd|aElementOf0(sK4_skl,sdtmndt0(sdtpldt0(xS,xx),xx))),
% 0.14/0.48 inference(cnf_transformation,[status(thm)],[f96])).
% 0.14/0.48 fof(f108,plain,(
% 0.14/0.48 sP1_prd|~aElementOf0(sK4_skl,xS)),
% 0.14/0.48 inference(cnf_transformation,[status(thm)],[f96])).
% 0.14/0.48 fof(f116,definition,(
% 0.14/0.48 ![W0]: (sP2_prd(W0)<=>((aElement0(W0)&aElementOf0(W0,sdtpldt0(xS,xx)))&~W0=xx))),
% 0.14/0.48 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 0.14/0.48 fof(f117,plain,(
% 0.14/0.48 sP1_prd<=>((aSet0(sdtpldt0(xS,xx))&(![W0]: (aElementOf0(W0,sdtpldt0(xS,xx))<=>(aElement0(W0)&(aElementOf0(W0,xS)|W0=xx)))))&((aSet0(sdtmndt0(sdtpldt0(xS,xx),xx))&(![W0]: (aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx))<=>sP2_prd(W0))))&((?[W0]: (aElementOf0(W0,xS)&~aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx))))&~aSubsetOf0(xS,sdtmndt0(sdtpldt0(xS,xx),xx)))))),
% 0.14/0.48 inference(formula_renaming,[status(thm)],[f92,f116])).
% 0.14/0.48 fof(f118,plain,(
% 0.14/0.48 (~sP1_prd|((aSet0(sdtpldt0(xS,xx))&(![W0]: ((~aElementOf0(W0,sdtpldt0(xS,xx))|(aElement0(W0)&(aElementOf0(W0,xS)|W0=xx)))&(aElementOf0(W0,sdtpldt0(xS,xx))|(~aElement0(W0)|(~aElementOf0(W0,xS)&~W0=xx))))))&((aSet0(sdtmndt0(sdtpldt0(xS,xx),xx))&(![W0]: ((~aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx))|sP2_prd(W0))&(aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx))|~sP2_prd(W0)))))&((?[W0]: (aElementOf0(W0,xS)&~aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx))))&~aSubsetOf0(xS,sdtmndt0(sdtpldt0(xS,xx),xx))))))&(sP1_prd|((~aSet0(sdtpldt0(xS,xx))|(?[W0]: ((~aElementOf0(W0,sdtpldt0(xS,xx))|(~aElement0(W0)|(~aElementOf0(W0,xS)&~W0=xx)))&(aElementOf0(W0,sdtpldt0(xS,xx))|(aElement0(W0)&(aElementOf0(W0,xS)|W0=xx))))))|((~aSet0(sdtmndt0(sdtpldt0(xS,xx),xx))|(?[W0]: ((~aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx))|~sP2_prd(W0))&(aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx))|sP2_prd(W0)))))|((![W0]: (~aElementOf0(W0,xS)|aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx))))|aSubsetOf0(xS,sdtmndt0(sdtpldt0(xS,xx),xx))))))),
% 0.14/0.48 inference(NNF_transformation,[status(thm)],[f117])).
% 0.14/0.48 fof(f119,plain,(
% 0.14/0.48 (~sP1_prd|((aSet0(sdtpldt0(xS,xx))&((![W0]: (~aElementOf0(W0,sdtpldt0(xS,xx))|(aElement0(W0)&(aElementOf0(W0,xS)|W0=xx))))&(![W0]: (aElementOf0(W0,sdtpldt0(xS,xx))|(~aElement0(W0)|(~aElementOf0(W0,xS)&~W0=xx))))))&((aSet0(sdtmndt0(sdtpldt0(xS,xx),xx))&((![W0]: (~aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx))|sP2_prd(W0)))&(![W0]: (aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx))|~sP2_prd(W0)))))&((?[W0]: (aElementOf0(W0,xS)&~aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx))))&~aSubsetOf0(xS,sdtmndt0(sdtpldt0(xS,xx),xx))))))&(sP1_prd|((~aSet0(sdtpldt0(xS,xx))|(?[W0]: ((~aElementOf0(W0,sdtpldt0(xS,xx))|(~aElement0(W0)|(~aElementOf0(W0,xS)&~W0=xx)))&(aElementOf0(W0,sdtpldt0(xS,xx))|(aElement0(W0)&(aElementOf0(W0,xS)|W0=xx))))))|((~aSet0(sdtmndt0(sdtpldt0(xS,xx),xx))|(?[W0]: ((~aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx))|~sP2_prd(W0))&(aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx))|sP2_prd(W0)))))|((![W0]: (~aElementOf0(W0,xS)|aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx))))|aSubsetOf0(xS,sdtmndt0(sdtpldt0(xS,xx),xx))))))),
% 0.14/0.48 inference(miniscoping,[status(thm)],[f118])).
% 0.14/0.48 fof(f120,plain,(
% 0.14/0.48 (~sP1_prd|((aSet0(sdtpldt0(xS,xx))&((![W0]: (~aElementOf0(W0,sdtpldt0(xS,xx))|(aElement0(W0)&(aElementOf0(W0,xS)|W0=xx))))&(![W0]: (aElementOf0(W0,sdtpldt0(xS,xx))|(~aElement0(W0)|(~aElementOf0(W0,xS)&~W0=xx))))))&((aSet0(sdtmndt0(sdtpldt0(xS,xx),xx))&((![W0]: (~aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx))|sP2_prd(W0)))&(![W0]: (aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx))|~sP2_prd(W0)))))&((aElementOf0(sK5_skl,xS)&~aElementOf0(sK5_skl,sdtmndt0(sdtpldt0(xS,xx),xx)))&~aSubsetOf0(xS,sdtmndt0(sdtpldt0(xS,xx),xx))))))&(sP1_prd|((~aSet0(sdtpldt0(xS,xx))|((~aElementOf0(sK6_skl,sdtpldt0(xS,xx))|(~aElement0(sK6_skl)|(~aElementOf0(sK6_skl,xS)&~sK6_skl=xx)))&(aElementOf0(sK6_skl,sdtpldt0(xS,xx))|(aElement0(sK6_skl)&(aElementOf0(sK6_skl,xS)|sK6_skl=xx)))))|((~aSet0(sdtmndt0(sdtpldt0(xS,xx),xx))|((~aElementOf0(sK7_skl,sdtmndt0(sdtpldt0(xS,xx),xx))|~sP2_prd(sK7_skl))&(aElementOf0(sK7_skl,sdtmndt0(sdtpldt0(xS,xx),xx))|sP2_prd(sK7_skl))))|((![W0]: (~aElementOf0(W0,xS)|aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx))))|aSubsetOf0(xS,sdtmndt0(sdtpldt0(xS,xx),xx))))))),
% 0.14/0.48 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl,sK6_skl,sK7_skl]),skolemize(W0,sK5_skl),skolemize(W0,sK6_skl),skolemize(W0,sK7_skl)],[f119])).
% 0.14/0.48 fof(f122,plain,(
% 0.14/0.48 ![X0]: (~sP1_prd|~aElementOf0(X0,sdtpldt0(xS,xx))|aElement0(X0))),
% 0.14/0.48 inference(cnf_transformation,[status(thm)],[f120])).
% 0.14/0.48 fof(f124,plain,(
% 0.14/0.48 ![X0]: (~sP1_prd|aElementOf0(X0,sdtpldt0(xS,xx))|~aElement0(X0)|~aElementOf0(X0,xS))),
% 0.14/0.48 inference(cnf_transformation,[status(thm)],[f120])).
% 0.14/0.48 fof(f128,plain,(
% 0.14/0.48 ![X0]: (~sP1_prd|aElementOf0(X0,sdtmndt0(sdtpldt0(xS,xx),xx))|~sP2_prd(X0))),
% 0.14/0.48 inference(cnf_transformation,[status(thm)],[f120])).
% 0.14/0.48 fof(f129,plain,(
% 0.14/0.48 ~sP1_prd|aElementOf0(sK5_skl,xS)),
% 0.14/0.48 inference(cnf_transformation,[status(thm)],[f120])).
% 0.14/0.48 fof(f130,plain,(
% 0.14/0.48 ~sP1_prd|~aElementOf0(sK5_skl,sdtmndt0(sdtpldt0(xS,xx),xx))),
% 0.14/0.48 inference(cnf_transformation,[status(thm)],[f120])).
% 0.14/0.49 fof(f140,plain,(
% 0.14/0.49 ![W0]: ((~sP2_prd(W0)|((aElement0(W0)&aElementOf0(W0,sdtpldt0(xS,xx)))&~W0=xx))&(sP2_prd(W0)|((~aElement0(W0)|~aElementOf0(W0,sdtpldt0(xS,xx)))|W0=xx)))),
% 0.14/0.49 inference(NNF_transformation,[status(thm)],[f116])).
% 0.14/0.49 fof(f141,plain,(
% 0.14/0.49 (![W0]: (~sP2_prd(W0)|((aElement0(W0)&aElementOf0(W0,sdtpldt0(xS,xx)))&~W0=xx)))&(![W0]: (sP2_prd(W0)|((~aElement0(W0)|~aElementOf0(W0,sdtpldt0(xS,xx)))|W0=xx)))),
% 0.14/0.49 inference(miniscoping,[status(thm)],[f140])).
% 0.14/0.49 fof(f145,plain,(
% 0.14/0.49 ![X0]: (sP2_prd(X0)|~aElement0(X0)|~aElementOf0(X0,sdtpldt0(xS,xx))|X0=xx)),
% 0.14/0.49 inference(cnf_transformation,[status(thm)],[f141])).
% 0.14/0.49 fof(f207,plain,(
% 0.14/0.49 ![X0]: (~aElementOf0(X0,sdtpldt0(xS,xx))|aElement0(X0))),
% 0.14/0.49 inference(forward_subsumption_resolution,[status(thm)],[f122,f98])).
% 0.14/0.49 fof(f527,plain,(
% 0.14/0.49 sP1_prd|sP1_prd|~sK4_skl=xx),
% 0.14/0.49 inference(resolution,[status(thm)],[f107,f105])).
% 0.14/0.49 fof(f528,plain,(
% 0.14/0.49 sP1_prd|sP1_prd|aElementOf0(sK4_skl,sdtpldt0(xS,xx))),
% 0.14/0.49 inference(resolution,[status(thm)],[f107,f104])).
% 0.14/0.49 fof(f539,plain,(
% 0.14/0.49 sP1_prd|~sK4_skl=xx),
% 0.14/0.49 inference(duplicate_literals_removal,[status(thm)],[f527])).
% 0.14/0.49 fof(f540,plain,(
% 0.14/0.49 sP1_prd|aElementOf0(sK4_skl,sdtpldt0(xS,xx))),
% 0.14/0.49 inference(duplicate_literals_removal,[status(thm)],[f528])).
% 0.14/0.49 fof(f565,plain,(
% 0.14/0.49 sP1_prd|sP1_prd|aElementOf0(sK4_skl,xS)|sK4_skl=xx),
% 0.14/0.49 inference(resolution,[status(thm)],[f540,f99])).
% 0.14/0.49 fof(f577,plain,(
% 0.14/0.49 sP1_prd|aElementOf0(sK4_skl,xS)|sK4_skl=xx),
% 0.14/0.49 inference(duplicate_literals_removal,[status(thm)],[f565])).
% 0.14/0.49 fof(f578,plain,(
% 0.14/0.49 sP1_prd|sK4_skl=xx),
% 0.14/0.49 inference(forward_subsumption_resolution,[status(thm)],[f577,f108])).
% 0.14/0.49 fof(f586,plain,(
% 0.14/0.49 aElementOf0(sK5_skl,xS)),
% 0.14/0.49 inference(backward_subsumption_resolution,[status(thm)],[f129,f587])).
% 0.14/0.49 fof(f587,plain,(
% 0.14/0.49 sP1_prd),
% 0.14/0.49 inference(forward_subsumption_resolution,[status(thm)],[f578,f539])).
% 0.14/0.49 fof(f596,plain,(
% 0.14/0.49 ~aSet0(xS)|aElement0(sK5_skl)),
% 0.14/0.49 inference(resolution,[status(thm)],[f586,f29])).
% 0.14/0.49 fof(f599,plain,(
% 0.14/0.49 aElement0(sK5_skl)),
% 0.14/0.49 inference(forward_subsumption_resolution,[status(thm)],[f596,f89])).
% 0.14/0.49 fof(f671,plain,(
% 0.14/0.49 ![X0]: (aElementOf0(X0,sdtpldt0(xS,xx))|~aElement0(X0)|~aElementOf0(X0,xS))),
% 0.14/0.49 inference(forward_subsumption_resolution,[status(thm)],[f124,f587])).
% 0.14/0.49 fof(f672,plain,(
% 0.14/0.49 aElementOf0(sK5_skl,sdtpldt0(xS,xx))|~aElement0(sK5_skl)),
% 0.14/0.49 inference(resolution,[status(thm)],[f671,f586])).
% 0.14/0.49 fof(f673,plain,(
% 0.14/0.49 aElementOf0(sK5_skl,sdtpldt0(xS,xx))),
% 0.14/0.49 inference(forward_subsumption_resolution,[status(thm)],[f672,f599])).
% 0.14/0.49 fof(f761,plain,(
% 0.14/0.49 ![X0]: (aElementOf0(X0,sdtmndt0(sdtpldt0(xS,xx),xx))|~sP2_prd(X0))),
% 0.14/0.49 inference(forward_subsumption_resolution,[status(thm)],[f128,f587])).
% 0.14/0.49 fof(f762,plain,(
% 0.14/0.49 ~aElementOf0(sK5_skl,sdtmndt0(sdtpldt0(xS,xx),xx))),
% 0.14/0.49 inference(forward_subsumption_resolution,[status(thm)],[f130,f587])).
% 0.14/0.49 fof(f934,plain,(
% 0.14/0.49 ![X0]: (sP2_prd(X0)|~aElementOf0(X0,sdtpldt0(xS,xx))|X0=xx)),
% 0.14/0.49 inference(forward_subsumption_resolution,[status(thm)],[f145,f207])).
% 0.14/0.49 fof(f935,plain,(
% 0.14/0.49 sP2_prd(sK5_skl)|sK5_skl=xx),
% 0.14/0.49 inference(resolution,[status(thm)],[f934,f673])).
% 0.14/0.49 fof(f937,plain,(
% 0.14/0.49 sK5_skl=xx|aElementOf0(sK5_skl,sdtmndt0(sdtpldt0(xS,xx),xx))),
% 0.14/0.49 inference(resolution,[status(thm)],[f935,f761])).
% 0.14/0.49 fof(f941,plain,(
% 0.14/0.49 sK5_skl=xx),
% 0.14/0.49 inference(forward_subsumption_resolution,[status(thm)],[f937,f762])).
% 0.14/0.49 fof(f963,plain,(
% 0.14/0.49 aElementOf0(xx,xS)),
% 0.14/0.49 inference(backward_demodulation,[status(thm)],[f941,f586])).
% 0.14/0.49 fof(f969,plain,(
% 0.14/0.49 $false),
% 0.14/0.49 inference(forward_subsumption_resolution,[status(thm)],[f963,f90])).
% 0.14/0.49 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.50 % Elapsed time: 0.140632 seconds
% 0.14/0.50 % CPU time: 0.809292 seconds
% 0.14/0.50 % Total memory used: 96.467 MB
% 0.14/0.50 % Net memory used: 95.330 MB
%------------------------------------------------------------------------------