%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : RNG108+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 : n019.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:22 PM UTC 2026
% Result : Theorem 0.12s 0.46s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG108+1 : 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.08/0.35 % Computer : n019.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 04:20:34 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.36 % Drodi V4.1.1
% 0.12/0.46 % Refutation found
% 0.12/0.46 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.46 % SZS output start CNFRefutation for theBenchmark
% 0.12/0.46 fof(f2,axiom,(
% 0.12/0.46 aElement0(sz00) ),
% 0.12/0.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.46 fof(f3,axiom,(
% 0.12/0.46 aElement0(sz10) ),
% 0.12/0.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.46 fof(f13,axiom,(
% 0.12/0.46 (! [W0] :( aElement0(W0)=> ( sdtasdt0(W0,sz10) = W0& W0 = sdtasdt0(sz10,W0) ) ) )),
% 0.12/0.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.46 fof(f16,axiom,(
% 0.12/0.46 (! [W0] :( aElement0(W0)=> ( sdtasdt0(W0,sz00) = sz00& sz00 = sdtasdt0(sz00,W0) ) ) )),
% 0.12/0.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.46 fof(f37,definition,(
% 0.12/0.46 (! [W0] :( aElement0(W0)=> (! [W1] :( W1 = slsdtgt0(W0)<=> ( aSet0(W1)& (! [W2] :( aElementOf0(W2,W1)<=> (? [W3] :( aElement0(W3)& sdtasdt0(W0,W3) = W2 ) )) )) ) )) )),
% 0.12/0.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.46 fof(f39,hypothesis,(
% 0.12/0.46 ( aElement0(xa)& aElement0(xb) ) ),
% 0.12/0.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.47 fof(f43,conjecture,(
% 0.12/0.47 ( aElementOf0(sz00,slsdtgt0(xa))& aElementOf0(xa,slsdtgt0(xa))& aElementOf0(sz00,slsdtgt0(xb))& aElementOf0(xb,slsdtgt0(xb)) ) ),
% 0.12/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.47 fof(f44,negated_conjecture,(
% 0.12/0.47 ~(( aElementOf0(sz00,slsdtgt0(xa))& aElementOf0(xa,slsdtgt0(xa))& aElementOf0(sz00,slsdtgt0(xb))& aElementOf0(xb,slsdtgt0(xb)) ) )),
% 0.12/0.47 inference(negated_conjecture,[status(cth)],[f43])).
% 0.12/0.47 fof(f48,plain,(
% 0.12/0.47 aElement0(sz00)),
% 0.12/0.47 inference(cnf_transformation,[status(thm)],[f2])).
% 0.12/0.47 fof(f49,plain,(
% 0.12/0.47 aElement0(sz10)),
% 0.12/0.47 inference(cnf_transformation,[status(thm)],[f3])).
% 0.12/0.47 fof(f70,plain,(
% 0.12/0.47 ![W0]: (~aElement0(W0)|(sdtasdt0(W0,sz10)=W0&W0=sdtasdt0(sz10,W0)))),
% 0.12/0.47 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 0.12/0.47 fof(f71,plain,(
% 0.12/0.47 ![X0]: (~aElement0(X0)|sdtasdt0(X0,sz10)=X0)),
% 0.12/0.47 inference(cnf_transformation,[status(thm)],[f70])).
% 0.12/0.47 fof(f79,plain,(
% 0.12/0.47 ![W0]: (~aElement0(W0)|(sdtasdt0(W0,sz00)=sz00&sz00=sdtasdt0(sz00,W0)))),
% 0.12/0.47 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 0.12/0.47 fof(f80,plain,(
% 0.12/0.47 ![X0]: (~aElement0(X0)|sdtasdt0(X0,sz00)=sz00)),
% 0.12/0.47 inference(cnf_transformation,[status(thm)],[f79])).
% 0.12/0.47 fof(f184,plain,(
% 0.12/0.47 ![W0]: (~aElement0(W0)|(![W1]: (W1=slsdtgt0(W0)<=>(aSet0(W1)&(![W2]: (aElementOf0(W2,W1)<=>(?[W3]: (aElement0(W3)&sdtasdt0(W0,W3)=W2))))))))),
% 0.12/0.47 inference(pre_NNF_transformation,[status(thm)],[f37])).
% 0.12/0.47 fof(f185,plain,(
% 0.12/0.47 ![W0]: (~aElement0(W0)|(![W1]: ((~W1=slsdtgt0(W0)|(aSet0(W1)&(![W2]: ((~aElementOf0(W2,W1)|(?[W3]: (aElement0(W3)&sdtasdt0(W0,W3)=W2)))&(aElementOf0(W2,W1)|(![W3]: (~aElement0(W3)|~sdtasdt0(W0,W3)=W2)))))))&(W1=slsdtgt0(W0)|(~aSet0(W1)|(?[W2]: ((~aElementOf0(W2,W1)|(![W3]: (~aElement0(W3)|~sdtasdt0(W0,W3)=W2)))&(aElementOf0(W2,W1)|(?[W3]: (aElement0(W3)&sdtasdt0(W0,W3)=W2))))))))))),
% 0.12/0.47 inference(NNF_transformation,[status(thm)],[f184])).
% 0.12/0.47 fof(f186,plain,(
% 0.12/0.47 ![W0]: (~aElement0(W0)|((![W1]: (~W1=slsdtgt0(W0)|(aSet0(W1)&((![W2]: (~aElementOf0(W2,W1)|(?[W3]: (aElement0(W3)&sdtasdt0(W0,W3)=W2))))&(![W2]: (aElementOf0(W2,W1)|(![W3]: (~aElement0(W3)|~sdtasdt0(W0,W3)=W2))))))))&(![W1]: (W1=slsdtgt0(W0)|(~aSet0(W1)|(?[W2]: ((~aElementOf0(W2,W1)|(![W3]: (~aElement0(W3)|~sdtasdt0(W0,W3)=W2)))&(aElementOf0(W2,W1)|(?[W3]: (aElement0(W3)&sdtasdt0(W0,W3)=W2))))))))))),
% 0.12/0.47 inference(miniscoping,[status(thm)],[f185])).
% 0.12/0.47 fof(f187,plain,(
% 0.12/0.47 ![W0]: (~aElement0(W0)|((![W1]: (~W1=slsdtgt0(W0)|(aSet0(W1)&((![W2]: (~aElementOf0(W2,W1)|(aElement0(sK17_skl(W2,W1,W0))&sdtasdt0(W0,sK17_skl(W2,W1,W0))=W2)))&(![W2]: (aElementOf0(W2,W1)|(![W3]: (~aElement0(W3)|~sdtasdt0(W0,W3)=W2))))))))&(![W1]: (W1=slsdtgt0(W0)|(~aSet0(W1)|((~aElementOf0(sK18_skl(W1,W0),W1)|(![W3]: (~aElement0(W3)|~sdtasdt0(W0,W3)=sK18_skl(W1,W0))))&(aElementOf0(sK18_skl(W1,W0),W1)|(aElement0(sK19_skl(W1,W0))&sdtasdt0(W0,sK19_skl(W1,W0))=sK18_skl(W1,W0)))))))))),
% 0.12/0.47 inference(skolemize,[status(esa),new_symbols(skolem,[sK17_skl,sK18_skl,sK19_skl]),skolemize(W3,sK17_skl(W2,W1,W0)),skolemize(W2,sK18_skl(W1,W0)),skolemize(W3,sK19_skl(W1,W0))],[f186])).
% 0.12/0.47 fof(f191,plain,(
% 0.12/0.47 ![X0,X1,X2,X3]: (~aElement0(X0)|~X1=slsdtgt0(X0)|aElementOf0(X2,X1)|~aElement0(X3)|~sdtasdt0(X0,X3)=X2)),
% 0.12/0.48 inference(cnf_transformation,[status(thm)],[f187])).
% 0.12/0.48 fof(f197,plain,(
% 0.12/0.48 aElement0(xa)),
% 0.12/0.48 inference(cnf_transformation,[status(thm)],[f39])).
% 0.12/0.48 fof(f198,plain,(
% 0.12/0.48 aElement0(xb)),
% 0.12/0.48 inference(cnf_transformation,[status(thm)],[f39])).
% 0.12/0.48 fof(f203,plain,(
% 0.12/0.48 (((~aElementOf0(sz00,slsdtgt0(xa))|~aElementOf0(xa,slsdtgt0(xa)))|~aElementOf0(sz00,slsdtgt0(xb)))|~aElementOf0(xb,slsdtgt0(xb)))),
% 0.12/0.48 inference(pre_NNF_transformation,[status(thm)],[f44])).
% 0.12/0.48 fof(f204,plain,(
% 0.12/0.48 ~aElementOf0(sz00,slsdtgt0(xa))|~aElementOf0(xa,slsdtgt0(xa))|~aElementOf0(sz00,slsdtgt0(xb))|~aElementOf0(xb,slsdtgt0(xb))),
% 0.12/0.48 inference(cnf_transformation,[status(thm)],[f203])).
% 0.12/0.48 fof(f234,plain,(
% 0.12/0.48 ![X0,X1]: (~aElement0(X0)|aElementOf0(sdtasdt0(X0,X1),slsdtgt0(X0))|~aElement0(X1))),
% 0.12/0.48 inference(destructive_equality_resolution,[status(thm)],[f191])).
% 0.12/0.48 fof(f242,plain,(
% 0.12/0.48 sdtasdt0(xb,sz00)=sz00),
% 0.12/0.48 inference(resolution,[status(thm)],[f80,f198])).
% 0.12/0.48 fof(f243,plain,(
% 0.12/0.48 sdtasdt0(xa,sz00)=sz00),
% 0.12/0.48 inference(resolution,[status(thm)],[f80,f197])).
% 0.12/0.48 fof(f286,plain,(
% 0.12/0.48 ~aElement0(xb)|aElementOf0(sz00,slsdtgt0(xb))|~aElement0(sz00)),
% 0.12/0.48 inference(paramodulation,[status(thm)],[f242,f234])).
% 0.12/0.48 fof(f288,plain,(
% 0.12/0.48 aElementOf0(sz00,slsdtgt0(xb))|~aElement0(sz00)),
% 0.12/0.48 inference(forward_subsumption_resolution,[status(thm)],[f286,f198])).
% 0.12/0.48 fof(f289,plain,(
% 0.12/0.48 ~aElement0(xa)|aElementOf0(sz00,slsdtgt0(xa))|~aElement0(sz00)),
% 0.12/0.48 inference(paramodulation,[status(thm)],[f243,f234])).
% 0.12/0.48 fof(f291,plain,(
% 0.12/0.48 aElementOf0(sz00,slsdtgt0(xa))|~aElement0(sz00)),
% 0.12/0.48 inference(forward_subsumption_resolution,[status(thm)],[f289,f197])).
% 0.12/0.48 fof(f377,plain,(
% 0.12/0.48 sdtasdt0(xb,sz10)=xb),
% 0.12/0.48 inference(resolution,[status(thm)],[f71,f198])).
% 0.12/0.48 fof(f378,plain,(
% 0.12/0.48 sdtasdt0(xa,sz10)=xa),
% 0.12/0.48 inference(resolution,[status(thm)],[f71,f197])).
% 0.12/0.48 fof(f384,plain,(
% 0.12/0.48 ~aElement0(xb)|aElementOf0(xb,slsdtgt0(xb))|~aElement0(sz10)),
% 0.12/0.48 inference(paramodulation,[status(thm)],[f377,f234])).
% 0.12/0.48 fof(f386,plain,(
% 0.12/0.48 aElementOf0(xb,slsdtgt0(xb))|~aElement0(sz10)),
% 0.12/0.48 inference(forward_subsumption_resolution,[status(thm)],[f384,f198])).
% 0.12/0.48 fof(f387,plain,(
% 0.12/0.48 ~aElement0(xa)|aElementOf0(xa,slsdtgt0(xa))|~aElement0(sz10)),
% 0.12/0.48 inference(paramodulation,[status(thm)],[f378,f234])).
% 0.12/0.48 fof(f389,plain,(
% 0.12/0.48 aElementOf0(xa,slsdtgt0(xa))|~aElement0(sz10)),
% 0.12/0.48 inference(forward_subsumption_resolution,[status(thm)],[f387,f197])).
% 0.12/0.48 fof(f570,plain,(
% 0.12/0.48 ~aElement0(sz00)|~aElementOf0(sz00,slsdtgt0(xa))|~aElementOf0(xa,slsdtgt0(xa))|~aElementOf0(xb,slsdtgt0(xb))),
% 0.12/0.48 inference(resolution,[status(thm)],[f288,f204])).
% 0.12/0.48 fof(f571,plain,(
% 0.12/0.48 ~aElementOf0(sz00,slsdtgt0(xa))|~aElementOf0(xa,slsdtgt0(xa))|~aElementOf0(xb,slsdtgt0(xb))),
% 0.12/0.48 inference(forward_subsumption_resolution,[status(thm)],[f570,f48])).
% 0.12/0.48 fof(f625,plain,(
% 0.12/0.48 ~aElement0(sz10)|~aElementOf0(sz00,slsdtgt0(xa))|~aElementOf0(xa,slsdtgt0(xa))),
% 0.12/0.48 inference(resolution,[status(thm)],[f386,f571])).
% 0.12/0.48 fof(f626,plain,(
% 0.12/0.48 ~aElementOf0(sz00,slsdtgt0(xa))|~aElementOf0(xa,slsdtgt0(xa))),
% 0.12/0.48 inference(forward_subsumption_resolution,[status(thm)],[f625,f49])).
% 0.12/0.48 fof(f683,plain,(
% 0.12/0.48 ~aElementOf0(sz00,slsdtgt0(xa))|~aElement0(sz10)),
% 0.12/0.48 inference(resolution,[status(thm)],[f626,f389])).
% 0.12/0.48 fof(f684,plain,(
% 0.12/0.48 ~aElement0(sz00)),
% 0.12/0.48 inference(backward_subsumption_resolution,[status(thm)],[f291,f685])).
% 0.12/0.48 fof(f685,plain,(
% 0.12/0.48 ~aElementOf0(sz00,slsdtgt0(xa))),
% 0.12/0.48 inference(forward_subsumption_resolution,[status(thm)],[f683,f49])).
% 0.12/0.48 fof(f686,plain,(
% 0.12/0.48 $false),
% 0.12/0.48 inference(forward_subsumption_resolution,[status(thm)],[f684,f48])).
% 0.12/0.48 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/0.50 % Elapsed time: 0.137183 seconds
% 0.12/0.50 % CPU time: 0.854356 seconds
% 0.12/0.50 % Total memory used: 115.735 MB
% 0.12/0.50 % Net memory used: 114.531 MB
%------------------------------------------------------------------------------