%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : RNG123+4 : 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 : n026.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 02:05:24 PM UTC 2026
% Result : Theorem 14.23s 2.31s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG123+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n026.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 04:24:39 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 14.23/2.31 % Refutation found
% 14.23/2.31 % SZS status Theorem for theBenchmark: Theorem is valid
% 14.23/2.31 % SZS output start CNFRefutation for theBenchmark
% 14.23/2.31 fof(f9,axiom,(
% 14.23/2.31 (! [W0] :( aElement0(W0)=> ( sdtpldt0(W0,sz00) = W0& W0 = sdtpldt0(sz00,W0) ) ) )),
% 14.23/2.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 14.23/2.31 fof(f39,hypothesis,(
% 14.23/2.31 ( aElement0(xa)& aElement0(xb) ) ),
% 14.23/2.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 14.23/2.31 fof(f42,hypothesis,(
% 14.23/2.31 ( aSet0(xI)& (! [W0] :( aElementOf0(W0,xI)=> ( (! [W1] :( aElementOf0(W1,xI)=> aElementOf0(sdtpldt0(W0,W1),xI) ))& (! [W1] :( aElement0(W1)=> aElementOf0(sdtasdt0(W1,W0),xI) ) )) ))& aIdeal0(xI)& (! [W0] :( aElementOf0(W0,slsdtgt0(xa))<=> (? [W1] :( aElement0(W1)& sdtasdt0(xa,W1) = W0 ) )))& (! [W0] :( aElementOf0(W0,slsdtgt0(xb))<=> (? [W1] :( aElement0(W1)& sdtasdt0(xb,W1) = W0 ) )))& (! [W0] :( aElementOf0(W0,xI)<=> (? [W1,W2] :( aElementOf0(W1,slsdtgt0(xa))& aElementOf0(W2,slsdtgt0(xb))& sdtpldt0(W1,W2) = W0 ) )))& xI = sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)) ) ),
% 14.23/2.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 14.23/2.31 fof(f43,hypothesis,(
% 14.23/2.31 ( (? [W0] :( aElement0(W0)& sdtasdt0(xa,W0) = sz00 ))& aElementOf0(sz00,slsdtgt0(xa))& (? [W0] :( aElement0(W0)& sdtasdt0(xa,W0) = xa ))& aElementOf0(xa,slsdtgt0(xa))& (? [W0] :( aElement0(W0)& sdtasdt0(xb,W0) = sz00 ))& aElementOf0(sz00,slsdtgt0(xb))& (? [W0] :( aElement0(W0)& sdtasdt0(xb,W0) = xb ))& aElementOf0(xb,slsdtgt0(xb)) ) ),
% 14.23/2.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 14.23/2.31 fof(f52,hypothesis,(
% 14.23/2.31 ( (? [W0,W1] :( aElementOf0(W0,slsdtgt0(xa))& aElementOf0(W1,slsdtgt0(xb))& sdtpldt0(W0,W1) = smndt0(sdtasdt0(xq,xu)) ))& aElementOf0(smndt0(sdtasdt0(xq,xu)),xI) ) ),
% 14.23/2.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 14.23/2.31 fof(f54,hypothesis,(
% 14.23/2.31 xr = sdtpldt0(smndt0(sdtasdt0(xq,xu)),xb) ),
% 14.23/2.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 14.23/2.31 fof(f55,conjecture,(
% 14.23/2.31 ( (? [W0,W1] :( aElementOf0(W0,slsdtgt0(xa))& aElementOf0(W1,slsdtgt0(xb))& sdtpldt0(W0,W1) = xr ))| aElementOf0(xr,xI) ) ),
% 14.23/2.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 14.23/2.31 fof(f56,negated_conjecture,(
% 14.23/2.31 ~(( (? [W0,W1] :( aElementOf0(W0,slsdtgt0(xa))& aElementOf0(W1,slsdtgt0(xb))& sdtpldt0(W0,W1) = xr ))| aElementOf0(xr,xI) ) )),
% 14.23/2.31 inference(negated_conjecture,[status(cth)],[f55])).
% 14.23/2.31 fof(f72,plain,(
% 14.23/2.31 ![W0]: (~aElement0(W0)|(sdtpldt0(W0,sz00)=W0&W0=sdtpldt0(sz00,W0)))),
% 14.23/2.31 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 14.23/2.31 fof(f74,plain,(
% 14.23/2.31 ![X0]: (~aElement0(X0)|X0=sdtpldt0(sz00,X0))),
% 14.23/2.31 inference(cnf_transformation,[status(thm)],[f72])).
% 14.23/2.31 fof(f210,plain,(
% 14.23/2.31 aElement0(xb)),
% 14.23/2.31 inference(cnf_transformation,[status(thm)],[f39])).
% 14.23/2.31 fof(f230,plain,(
% 14.23/2.31 (((((aSet0(xI)&(![W0]: (~aElementOf0(W0,xI)|((![W1]: (~aElementOf0(W1,xI)|aElementOf0(sdtpldt0(W0,W1),xI)))&(![W1]: (~aElement0(W1)|aElementOf0(sdtasdt0(W1,W0),xI)))))))&aIdeal0(xI))&(![W0]: (aElementOf0(W0,slsdtgt0(xa))<=>(?[W1]: (aElement0(W1)&sdtasdt0(xa,W1)=W0)))))&(![W0]: (aElementOf0(W0,slsdtgt0(xb))<=>(?[W1]: (aElement0(W1)&sdtasdt0(xb,W1)=W0)))))&(![W0]: (aElementOf0(W0,xI)<=>(?[W1,W2]: ((aElementOf0(W1,slsdtgt0(xa))&aElementOf0(W2,slsdtgt0(xb)))&sdtpldt0(W1,W2)=W0)))))&xI=sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))),
% 14.23/2.31 inference(pre_NNF_transformation,[status(thm)],[f42])).
% 14.23/2.31 fof(f231,plain,(
% 14.23/2.31 (((((aSet0(xI)&(![W0]: (~aElementOf0(W0,xI)|((![W1]: (~aElementOf0(W1,xI)|aElementOf0(sdtpldt0(W0,W1),xI)))&(![W1]: (~aElement0(W1)|aElementOf0(sdtasdt0(W1,W0),xI)))))))&aIdeal0(xI))&(![W0]: ((~aElementOf0(W0,slsdtgt0(xa))|(?[W1]: (aElement0(W1)&sdtasdt0(xa,W1)=W0)))&(aElementOf0(W0,slsdtgt0(xa))|(![W1]: (~aElement0(W1)|~sdtasdt0(xa,W1)=W0))))))&(![W0]: ((~aElementOf0(W0,slsdtgt0(xb))|(?[W1]: (aElement0(W1)&sdtasdt0(xb,W1)=W0)))&(aElementOf0(W0,slsdtgt0(xb))|(![W1]: (~aElement0(W1)|~sdtasdt0(xb,W1)=W0))))))&(![W0]: ((~aElementOf0(W0,xI)|(?[W1,W2]: ((aElementOf0(W1,slsdtgt0(xa))&aElementOf0(W2,slsdtgt0(xb)))&sdtpldt0(W1,W2)=W0)))&(aElementOf0(W0,xI)|(![W1,W2]: ((~aElementOf0(W1,slsdtgt0(xa))|~aElementOf0(W2,slsdtgt0(xb)))|~sdtpldt0(W1,W2)=W0))))))&xI=sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))),
% 14.23/2.31 inference(NNF_transformation,[status(thm)],[f230])).
% 14.23/2.31 fof(f232,plain,(
% 14.23/2.31 (((((aSet0(xI)&(![W0]: (~aElementOf0(W0,xI)|((![W1]: (~aElementOf0(W1,xI)|aElementOf0(sdtpldt0(W0,W1),xI)))&(![W1]: (~aElement0(W1)|aElementOf0(sdtasdt0(W1,W0),xI)))))))&aIdeal0(xI))&((![W0]: (~aElementOf0(W0,slsdtgt0(xa))|(?[W1]: (aElement0(W1)&sdtasdt0(xa,W1)=W0))))&(![W0]: (aElementOf0(W0,slsdtgt0(xa))|(![W1]: (~aElement0(W1)|~sdtasdt0(xa,W1)=W0))))))&((![W0]: (~aElementOf0(W0,slsdtgt0(xb))|(?[W1]: (aElement0(W1)&sdtasdt0(xb,W1)=W0))))&(![W0]: (aElementOf0(W0,slsdtgt0(xb))|(![W1]: (~aElement0(W1)|~sdtasdt0(xb,W1)=W0))))))&((![W0]: (~aElementOf0(W0,xI)|(?[W1,W2]: ((aElementOf0(W1,slsdtgt0(xa))&aElementOf0(W2,slsdtgt0(xb)))&sdtpldt0(W1,W2)=W0))))&(![W0]: (aElementOf0(W0,xI)|(![W1,W2]: ((~aElementOf0(W1,slsdtgt0(xa))|~aElementOf0(W2,slsdtgt0(xb)))|~sdtpldt0(W1,W2)=W0))))))&xI=sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))),
% 14.23/2.31 inference(miniscoping,[status(thm)],[f231])).
% 14.23/2.31 fof(f233,plain,(
% 14.23/2.31 (((((aSet0(xI)&(![W0]: (~aElementOf0(W0,xI)|((![W1]: (~aElementOf0(W1,xI)|aElementOf0(sdtpldt0(W0,W1),xI)))&(![W1]: (~aElement0(W1)|aElementOf0(sdtasdt0(W1,W0),xI)))))))&aIdeal0(xI))&((![W0]: (~aElementOf0(W0,slsdtgt0(xa))|(aElement0(sK23_skl(W0))&sdtasdt0(xa,sK23_skl(W0))=W0)))&(![W0]: (aElementOf0(W0,slsdtgt0(xa))|(![W1]: (~aElement0(W1)|~sdtasdt0(xa,W1)=W0))))))&((![W0]: (~aElementOf0(W0,slsdtgt0(xb))|(aElement0(sK24_skl(W0))&sdtasdt0(xb,sK24_skl(W0))=W0)))&(![W0]: (aElementOf0(W0,slsdtgt0(xb))|(![W1]: (~aElement0(W1)|~sdtasdt0(xb,W1)=W0))))))&((![W0]: (~aElementOf0(W0,xI)|((aElementOf0(sK25_skl(W0),slsdtgt0(xa))&aElementOf0(sK26_skl(W0),slsdtgt0(xb)))&sdtpldt0(sK25_skl(W0),sK26_skl(W0))=W0)))&(![W0]: (aElementOf0(W0,xI)|(![W1,W2]: ((~aElementOf0(W1,slsdtgt0(xa))|~aElementOf0(W2,slsdtgt0(xb)))|~sdtpldt0(W1,W2)=W0))))))&xI=sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))),
% 14.23/2.31 inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl,sK24_skl,sK25_skl,sK26_skl]),skolemize(W1,sK23_skl(W0)),skolemize(W1,sK24_skl(W0)),skolemize(W1,sK25_skl(W0)),skolemize(W2,sK26_skl(W0))],[f232])).
% 14.23/2.31 fof(f235,plain,(
% 14.23/2.31 ![X0,X1]: (~aElementOf0(X0,xI)|~aElementOf0(X1,xI)|aElementOf0(sdtpldt0(X0,X1),xI))),
% 14.23/2.31 inference(cnf_transformation,[status(thm)],[f233])).
% 14.23/2.31 fof(f247,plain,(
% 14.23/2.31 ![X0,X1,X2]: (aElementOf0(X0,xI)|~aElementOf0(X1,slsdtgt0(xa))|~aElementOf0(X2,slsdtgt0(xb))|~sdtpldt0(X1,X2)=X0)),
% 14.23/2.31 inference(cnf_transformation,[status(thm)],[f233])).
% 14.23/2.31 fof(f249,plain,(
% 14.23/2.31 (((((((aElement0(sK27_skl)&sdtasdt0(xa,sK27_skl)=sz00)&aElementOf0(sz00,slsdtgt0(xa)))&(aElement0(sK28_skl)&sdtasdt0(xa,sK28_skl)=xa))&aElementOf0(xa,slsdtgt0(xa)))&(aElement0(sK29_skl)&sdtasdt0(xb,sK29_skl)=sz00))&aElementOf0(sz00,slsdtgt0(xb)))&(aElement0(sK30_skl)&sdtasdt0(xb,sK30_skl)=xb))&aElementOf0(xb,slsdtgt0(xb))),
% 14.23/2.31 inference(skolemize,[status(esa),new_symbols(skolem,[sK27_skl,sK28_skl,sK29_skl,sK30_skl]),skolemize(W0,sK27_skl),skolemize(W0,sK28_skl),skolemize(W0,sK29_skl),skolemize(W0,sK30_skl)],[f43])).
% 14.23/2.31 fof(f252,plain,(
% 14.23/2.31 aElementOf0(sz00,slsdtgt0(xa))),
% 14.23/2.31 inference(cnf_transformation,[status(thm)],[f249])).
% 14.23/2.31 fof(f261,plain,(
% 14.23/2.31 aElementOf0(xb,slsdtgt0(xb))),
% 14.23/2.31 inference(cnf_transformation,[status(thm)],[f249])).
% 14.23/2.31 fof(f307,plain,(
% 14.23/2.31 ((aElementOf0(sK41_skl,slsdtgt0(xa))&aElementOf0(sK42_skl,slsdtgt0(xb)))&sdtpldt0(sK41_skl,sK42_skl)=smndt0(sdtasdt0(xq,xu)))&aElementOf0(smndt0(sdtasdt0(xq,xu)),xI)),
% 14.23/2.31 inference(skolemize,[status(esa),new_symbols(skolem,[sK41_skl,sK42_skl]),skolemize(W0,sK41_skl),skolemize(W1,sK42_skl)],[f52])).
% 14.23/2.31 fof(f310,plain,(
% 14.23/2.31 sdtpldt0(sK41_skl,sK42_skl)=smndt0(sdtasdt0(xq,xu))),
% 14.23/2.31 inference(cnf_transformation,[status(thm)],[f307])).
% 14.23/2.31 fof(f311,plain,(
% 14.23/2.31 aElementOf0(smndt0(sdtasdt0(xq,xu)),xI)),
% 14.23/2.31 inference(cnf_transformation,[status(thm)],[f307])).
% 14.23/2.31 fof(f320,plain,(
% 14.23/2.31 xr=sdtpldt0(smndt0(sdtasdt0(xq,xu)),xb)),
% 14.23/2.31 inference(cnf_transformation,[status(thm)],[f54])).
% 14.23/2.31 fof(f321,plain,(
% 14.23/2.31 ((![W0,W1]: ((~aElementOf0(W0,slsdtgt0(xa))|~aElementOf0(W1,slsdtgt0(xb)))|~sdtpldt0(W0,W1)=xr))&~aElementOf0(xr,xI))),
% 14.23/2.31 inference(pre_NNF_transformation,[status(thm)],[f56])).
% 14.23/2.31 fof(f323,plain,(
% 14.23/2.31 ~aElementOf0(xr,xI)),
% 14.23/2.31 inference(cnf_transformation,[status(thm)],[f321])).
% 14.23/2.33 fof(f431,plain,(
% 14.23/2.33 ![X0,X1]: (aElementOf0(sdtpldt0(X0,X1),xI)|~aElementOf0(X0,slsdtgt0(xa))|~aElementOf0(X1,slsdtgt0(xb)))),
% 14.23/2.33 inference(destructive_equality_resolution,[status(thm)],[f247])).
% 14.23/2.33 fof(f478,plain,(
% 14.23/2.33 xb=sdtpldt0(sz00,xb)),
% 14.23/2.33 inference(resolution,[status(thm)],[f210,f74])).
% 14.23/2.33 fof(f913,definition,(
% 14.23/2.33 sQ30_spl <=> (aElementOf0(sz00,slsdtgt0(xa)))),
% 14.23/2.33 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 14.23/2.33 fof(f915,plain,(
% 14.23/2.33 ~aElementOf0(sz00,slsdtgt0(xa))|sQ30_spl),
% 14.23/2.33 inference(component_clause,[status(thm)],[f913])).
% 14.23/2.33 fof(f1017,plain,(
% 14.23/2.33 aElementOf0(xb,xI)|~aElementOf0(sz00,slsdtgt0(xa))|~aElementOf0(xb,slsdtgt0(xb))),
% 14.23/2.33 inference(paramodulation,[status(thm)],[f478,f431])).
% 14.23/2.33 fof(f1019,definition,(
% 14.23/2.33 sQ37_spl <=> (aElementOf0(xb,slsdtgt0(xb)))),
% 14.23/2.33 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 14.23/2.33 fof(f1021,plain,(
% 14.23/2.33 ~aElementOf0(xb,slsdtgt0(xb))|sQ37_spl),
% 14.23/2.33 inference(component_clause,[status(thm)],[f1019])).
% 14.23/2.33 fof(f1026,definition,(
% 14.23/2.33 sQ39_spl <=> (aElementOf0(xb,xI))),
% 14.23/2.33 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 14.23/2.33 fof(f1029,plain,(
% 14.23/2.33 sQ39_spl|~sQ30_spl|~sQ37_spl),
% 14.23/2.33 inference(split_clause,[status(thm)],[f1017,f1026,f913,f1019])).
% 14.23/2.33 fof(f1031,plain,(
% 14.23/2.33 $false|sQ37_spl),
% 14.23/2.33 inference(forward_subsumption_resolution,[status(thm)],[f1021,f261])).
% 14.23/2.33 fof(f1032,plain,(
% 14.23/2.33 sQ37_spl),
% 14.23/2.33 inference(contradiction_clause,[status(thm)],[f1031])).
% 14.23/2.33 fof(f1033,plain,(
% 14.23/2.33 $false|sQ30_spl),
% 14.23/2.33 inference(forward_subsumption_resolution,[status(thm)],[f915,f252])).
% 14.23/2.33 fof(f1034,plain,(
% 14.23/2.33 sQ30_spl),
% 14.23/2.33 inference(contradiction_clause,[status(thm)],[f1033])).
% 14.23/2.33 fof(f2495,definition,(
% 14.23/2.33 sQ159_spl <=> (aElementOf0(xr,xI))),
% 14.23/2.33 introduced(definition,[new_symbols(definition,[sQ159_spl])],[split_symbol_definition])).
% 14.23/2.33 fof(f2496,plain,(
% 14.23/2.33 aElementOf0(xr,xI)|~sQ159_spl),
% 14.23/2.33 inference(component_clause,[status(thm)],[f2495])).
% 14.23/2.33 fof(f6464,plain,(
% 14.23/2.33 aElementOf0(sdtpldt0(sK41_skl,sK42_skl),xI)),
% 14.23/2.33 inference(forward_demodulation,[status(thm)],[f310,f311])).
% 14.23/2.33 fof(f6467,plain,(
% 14.23/2.33 xr=sdtpldt0(sdtpldt0(sK41_skl,sK42_skl),xb)),
% 14.23/2.33 inference(forward_demodulation,[status(thm)],[f310,f320])).
% 14.23/2.33 fof(f6469,plain,(
% 14.23/2.33 ~aElementOf0(sdtpldt0(sK41_skl,sK42_skl),xI)|~aElementOf0(xb,xI)|aElementOf0(xr,xI)),
% 14.23/2.33 inference(paramodulation,[status(thm)],[f6467,f235])).
% 14.23/2.33 fof(f6474,definition,(
% 14.23/2.33 sQ383_spl <=> (aElementOf0(sdtpldt0(sK41_skl,sK42_skl),xI))),
% 14.23/2.33 introduced(definition,[new_symbols(definition,[sQ383_spl])],[split_symbol_definition])).
% 14.23/2.33 fof(f6476,plain,(
% 14.23/2.33 ~aElementOf0(sdtpldt0(sK41_skl,sK42_skl),xI)|sQ383_spl),
% 14.23/2.33 inference(component_clause,[status(thm)],[f6474])).
% 14.23/2.33 fof(f6477,plain,(
% 14.23/2.33 ~sQ383_spl|~sQ39_spl|sQ159_spl),
% 14.23/2.33 inference(split_clause,[status(thm)],[f6469,f6474,f1026,f2495])).
% 14.23/2.33 fof(f6478,plain,(
% 14.23/2.33 $false|sQ383_spl),
% 14.23/2.33 inference(forward_subsumption_resolution,[status(thm)],[f6476,f6464])).
% 14.23/2.33 fof(f6479,plain,(
% 14.23/2.33 sQ383_spl),
% 14.23/2.33 inference(contradiction_clause,[status(thm)],[f6478])).
% 14.23/2.33 fof(f6480,plain,(
% 14.23/2.33 $false|~sQ159_spl),
% 14.23/2.33 inference(forward_subsumption_resolution,[status(thm)],[f2496,f323])).
% 14.23/2.33 fof(f6481,plain,(
% 14.23/2.33 ~sQ159_spl),
% 14.23/2.33 inference(contradiction_clause,[status(thm)],[f6480])).
% 14.23/2.33 fof(f6482,plain,(
% 14.23/2.33 $false),
% 14.23/2.33 inference(sat_refutation,[status(thm)],[f1029,f1032,f1034,f6477,f6479,f6481])).
% 14.23/2.33 % SZS output end CNFRefutation for theBenchmark.p
% 14.23/2.36 % Elapsed time: 1.975270 seconds
% 14.23/2.36 % CPU time: 15.403814 seconds
% 14.23/2.36 % Total memory used: 291.984 MB
% 14.23/2.36 % Net memory used: 274.760 MB
%------------------------------------------------------------------------------