%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : RNG119+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 : 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 02:05:24 PM UTC 2026
% Result : Theorem 92.82s 12.35s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG119+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.11/0.38 % Computer : n013.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Mon Sep 21 04:21:06 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.40 % Drodi V4.1.1
% 92.82/12.35 % Refutation found
% 92.82/12.35 % SZS status Theorem for theBenchmark: Theorem is valid
% 92.82/12.35 % SZS output start CNFRefutation for theBenchmark
% 92.82/12.35 fof(f6,axiom,(
% 92.82/12.35 (! [W0,W1] :( ( aElement0(W0)& aElement0(W1) )=> aElement0(sdtasdt0(W0,W1)) ) )),
% 92.82/12.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 92.82/12.35 fof(f9,axiom,(
% 92.82/12.35 (! [W0] :( aElement0(W0)=> ( sdtpldt0(W0,sz00) = W0& W0 = sdtpldt0(sz00,W0) ) ) )),
% 92.82/12.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 92.82/12.35 fof(f11,axiom,(
% 92.82/12.35 (! [W0,W1] :( ( aElement0(W0)& aElement0(W1) )=> sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) )),
% 92.82/12.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 92.82/12.35 fof(f20,axiom,(
% 92.82/12.35 (! [W0] :( aSet0(W0)=> (! [W1] :( aElementOf0(W1,W0)=> aElement0(W1) ) )) )),
% 92.82/12.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 92.82/12.35 fof(f42,hypothesis,(
% 92.82/12.35 ( 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)) ) ),
% 92.82/12.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 92.82/12.35 fof(f45,hypothesis,(
% 92.82/12.35 ( (? [W0,W1] :( aElementOf0(W0,slsdtgt0(xa))& aElementOf0(W1,slsdtgt0(xb))& sdtpldt0(W0,W1) = xu ))& aElementOf0(xu,xI)& xu != sz00& (! [W0] :( ( ( (? [W1,W2] :( aElementOf0(W1,slsdtgt0(xa))& aElementOf0(W2,slsdtgt0(xb))& sdtpldt0(W1,W2) = W0 ))| aElementOf0(W0,xI) )& W0 != sz00 )=> ~ iLess0(sbrdtbr0(W0),sbrdtbr0(xu)) ) )) ),
% 92.82/12.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 92.82/12.35 fof(f49,hypothesis,(
% 92.82/12.35 ~ ( (? [W0] :( aElement0(W0)& sdtasdt0(xu,W0) = xb ))| doDivides0(xu,xb) ) ),
% 92.82/12.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 92.82/12.35 fof(f50,hypothesis,(
% 92.82/12.35 ( aElement0(xq)& aElement0(xr)& xb = sdtpldt0(sdtasdt0(xq,xu),xr)& ( xr = sz00| iLess0(sbrdtbr0(xr),sbrdtbr0(xu)) ) ) ),
% 92.82/12.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 92.82/12.35 fof(f51,conjecture,(
% 92.82/12.35 xr != sz00 ),
% 92.82/12.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 92.82/12.35 fof(f52,negated_conjecture,(
% 92.82/12.35 ~(xr != sz00 )),
% 92.82/12.35 inference(negated_conjecture,[status(cth)],[f51])).
% 92.82/12.35 fof(f62,plain,(
% 92.82/12.35 ![W0,W1]: ((~aElement0(W0)|~aElement0(W1))|aElement0(sdtasdt0(W0,W1)))),
% 92.82/12.35 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 92.82/12.35 fof(f63,plain,(
% 92.82/12.35 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|aElement0(sdtasdt0(X0,X1)))),
% 92.82/12.35 inference(cnf_transformation,[status(thm)],[f62])).
% 92.82/12.35 fof(f68,plain,(
% 92.82/12.35 ![W0]: (~aElement0(W0)|(sdtpldt0(W0,sz00)=W0&W0=sdtpldt0(sz00,W0)))),
% 92.82/12.35 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 92.82/12.35 fof(f69,plain,(
% 92.82/12.35 ![X0]: (~aElement0(X0)|sdtpldt0(X0,sz00)=X0)),
% 92.82/12.35 inference(cnf_transformation,[status(thm)],[f68])).
% 92.82/12.35 fof(f74,plain,(
% 92.82/12.35 ![W0,W1]: ((~aElement0(W0)|~aElement0(W1))|sdtasdt0(W0,W1)=sdtasdt0(W1,W0))),
% 92.82/12.35 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 92.82/12.35 fof(f75,plain,(
% 92.82/12.35 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|sdtasdt0(X0,X1)=sdtasdt0(X1,X0))),
% 92.82/12.35 inference(cnf_transformation,[status(thm)],[f74])).
% 92.82/12.35 fof(f96,plain,(
% 92.82/12.35 ![W0]: (~aSet0(W0)|(![W1]: (~aElementOf0(W1,W0)|aElement0(W1))))),
% 92.82/12.35 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 92.82/12.35 fof(f97,plain,(
% 92.82/12.35 ![X0,X1]: (~aSet0(X0)|~aElementOf0(X1,X0)|aElement0(X1))),
% 92.82/12.35 inference(cnf_transformation,[status(thm)],[f96])).
% 92.82/12.35 fof(f226,plain,(
% 92.82/12.35 (((((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))),
% 92.82/12.35 inference(pre_NNF_transformation,[status(thm)],[f42])).
% 92.82/12.35 fof(f227,plain,(
% 92.82/12.35 (((((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))),
% 92.82/12.35 inference(NNF_transformation,[status(thm)],[f226])).
% 92.82/12.35 fof(f228,plain,(
% 92.82/12.35 (((((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))),
% 92.82/12.35 inference(miniscoping,[status(thm)],[f227])).
% 92.82/12.35 fof(f229,plain,(
% 92.82/12.35 (((((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))),
% 92.82/12.35 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))],[f228])).
% 92.82/12.35 fof(f230,plain,(
% 92.82/12.35 aSet0(xI)),
% 92.82/12.35 inference(cnf_transformation,[status(thm)],[f229])).
% 92.82/12.35 fof(f272,plain,(
% 92.82/12.35 (((?[W0,W1]: ((aElementOf0(W0,slsdtgt0(xa))&aElementOf0(W1,slsdtgt0(xb)))&sdtpldt0(W0,W1)=xu))&aElementOf0(xu,xI))&~xu=sz00)&(![W0]: ((((![W1,W2]: ((~aElementOf0(W1,slsdtgt0(xa))|~aElementOf0(W2,slsdtgt0(xb)))|~sdtpldt0(W1,W2)=W0))&~aElementOf0(W0,xI))|W0=sz00)|~iLess0(sbrdtbr0(W0),sbrdtbr0(xu))))),
% 92.82/12.35 inference(pre_NNF_transformation,[status(thm)],[f45])).
% 92.82/12.35 fof(f273,plain,(
% 92.82/12.35 ((((aElementOf0(sK36_skl,slsdtgt0(xa))&aElementOf0(sK37_skl,slsdtgt0(xb)))&sdtpldt0(sK36_skl,sK37_skl)=xu)&aElementOf0(xu,xI))&~xu=sz00)&(![W0]: ((((![W1,W2]: ((~aElementOf0(W1,slsdtgt0(xa))|~aElementOf0(W2,slsdtgt0(xb)))|~sdtpldt0(W1,W2)=W0))&~aElementOf0(W0,xI))|W0=sz00)|~iLess0(sbrdtbr0(W0),sbrdtbr0(xu))))),
% 92.82/12.35 inference(skolemize,[status(esa),new_symbols(skolem,[sK36_skl,sK37_skl]),skolemize(W0,sK36_skl),skolemize(W1,sK37_skl)],[f272])).
% 92.82/12.35 fof(f277,plain,(
% 92.82/12.35 aElementOf0(xu,xI)),
% 92.82/12.35 inference(cnf_transformation,[status(thm)],[f273])).
% 92.82/12.35 fof(f295,plain,(
% 92.82/12.35 ((![W0]: (~aElement0(W0)|~sdtasdt0(xu,W0)=xb))&~doDivides0(xu,xb))),
% 92.82/12.35 inference(pre_NNF_transformation,[status(thm)],[f49])).
% 91.84/12.41 fof(f296,plain,(
% 91.84/12.41 ![X0]: (~aElement0(X0)|~sdtasdt0(xu,X0)=xb)),
% 91.84/12.41 inference(cnf_transformation,[status(thm)],[f295])).
% 91.84/12.41 fof(f298,plain,(
% 91.84/12.41 aElement0(xq)),
% 91.84/12.41 inference(cnf_transformation,[status(thm)],[f50])).
% 91.84/12.41 fof(f300,plain,(
% 91.84/12.41 xb=sdtpldt0(sdtasdt0(xq,xu),xr)),
% 91.84/12.41 inference(cnf_transformation,[status(thm)],[f50])).
% 91.84/12.41 fof(f302,plain,(
% 91.84/12.41 xr=sz00),
% 91.84/12.41 inference(cnf_transformation,[status(thm)],[f52])).
% 91.84/12.41 fof(f541,plain,(
% 91.84/12.41 ![X0]: (~aElement0(X0)|aElement0(sdtasdt0(xq,X0)))),
% 91.84/12.41 inference(resolution,[status(thm)],[f298,f63])).
% 91.84/12.41 fof(f945,plain,(
% 91.84/12.41 ![X0]: (~aElement0(X0)|sdtasdt0(xq,X0)=sdtasdt0(X0,xq))),
% 91.84/12.41 inference(resolution,[status(thm)],[f75,f298])).
% 91.84/12.41 fof(f1550,plain,(
% 91.84/12.41 ~aSet0(xI)|aElement0(xu)),
% 91.84/12.41 inference(resolution,[status(thm)],[f97,f277])).
% 91.84/12.41 fof(f1557,plain,(
% 91.84/12.41 aElement0(xu)),
% 91.84/12.41 inference(forward_subsumption_resolution,[status(thm)],[f1550,f230])).
% 91.84/12.41 fof(f5804,plain,(
% 91.84/12.41 ~sdtasdt0(xu,xq)=xb),
% 91.84/12.41 inference(resolution,[status(thm)],[f296,f298])).
% 91.84/12.41 fof(f26322,plain,(
% 91.84/12.41 xb=sdtpldt0(sdtasdt0(xq,xu),sz00)),
% 91.84/12.41 inference(forward_demodulation,[status(thm)],[f302,f300])).
% 91.84/12.41 fof(f88063,plain,(
% 91.84/12.41 aElement0(sdtasdt0(xq,xu))),
% 91.84/12.41 inference(resolution,[status(thm)],[f541,f1557])).
% 91.84/12.41 fof(f103781,plain,(
% 91.84/12.41 sdtpldt0(sdtasdt0(xq,xu),sz00)=sdtasdt0(xq,xu)),
% 91.84/12.41 inference(resolution,[status(thm)],[f88063,f69])).
% 91.84/12.41 fof(f103784,plain,(
% 91.84/12.41 xb=sdtasdt0(xq,xu)),
% 91.84/12.41 inference(forward_demodulation,[status(thm)],[f26322,f103781])).
% 91.84/12.41 fof(f122022,plain,(
% 91.84/12.41 sdtasdt0(xq,xu)=sdtasdt0(xu,xq)),
% 91.84/12.41 inference(resolution,[status(thm)],[f945,f1557])).
% 91.84/12.41 fof(f122136,plain,(
% 91.84/12.41 xb=sdtasdt0(xu,xq)),
% 91.84/12.41 inference(forward_demodulation,[status(thm)],[f103784,f122022])).
% 91.84/12.41 fof(f122137,plain,(
% 91.84/12.41 $false),
% 91.84/12.41 inference(forward_subsumption_resolution,[status(thm)],[f122136,f5804])).
% 91.84/12.41 % SZS output end CNFRefutation for theBenchmark.p
% 91.84/12.44 % Elapsed time: 12.040671 seconds
% 91.84/12.44 % CPU time: 95.263429 seconds
% 91.84/12.44 % Total memory used: 816.532 MB
% 91.84/12.44 % Net memory used: 757.513 MB
%------------------------------------------------------------------------------