%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : RNG109+4 : 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 : n015.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.17s 5.56s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG109+4 : 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.11/5.39 % Computer : n015.cluster.edu
% 0.11/5.39 % Model : x86_64 x86_64
% 0.11/5.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.39 % Memory : 8046.5625MB
% 0.11/5.39 % OS : Linux 6.8.0-71-generic
% 0.11/5.39 % CPULimit : 300
% 0.11/5.39 % WCLimit : 300
% 0.11/5.39 % DateTime : Mon Sep 21 04:23:40 UTC 2026
% 0.11/5.39 % CPUTime :
% 0.17/5.41 % Drodi V4.1.1
% 0.17/5.56 % Refutation found
% 0.17/5.56 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.17/5.56 % SZS output start CNFRefutation for theBenchmark
% 0.17/5.56 fof(f9,axiom,(
% 0.17/5.56 (! [W0] :( aElement0(W0)=> ( sdtpldt0(W0,sz00) = W0& W0 = sdtpldt0(sz00,W0) ) ) )),
% 0.17/5.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/5.56 fof(f39,hypothesis,(
% 0.17/5.56 ( aElement0(xa)& aElement0(xb) ) ),
% 0.17/5.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/5.56 fof(f40,hypothesis,(
% 0.17/5.56 ( xa != sz00| xb != sz00 ) ),
% 0.17/5.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/5.56 fof(f43,hypothesis,(
% 0.17/5.56 ( (? [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)) ) ),
% 0.17/5.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/5.56 fof(f44,conjecture,(
% 0.17/5.56 (? [W0] :( ( (! [W1] :( aElementOf0(W1,slsdtgt0(xa))<=> (? [W2] :( aElement0(W2)& sdtasdt0(xa,W2) = W1 ) )))=> ( (! [W1] :( aElementOf0(W1,slsdtgt0(xb))<=> (? [W2] :( aElement0(W2)& sdtasdt0(xb,W2) = W1 ) )))=> ( (? [W1,W2] :( aElementOf0(W1,slsdtgt0(xa))& aElementOf0(W2,slsdtgt0(xb))& sdtpldt0(W1,W2) = W0 ))| aElementOf0(W0,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))) ) ) )& W0 != sz00 ) )),
% 0.17/5.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/5.56 fof(f45,negated_conjecture,(
% 0.17/5.56 ~((? [W0] :( ( (! [W1] :( aElementOf0(W1,slsdtgt0(xa))<=> (? [W2] :( aElement0(W2)& sdtasdt0(xa,W2) = W1 ) )))=> ( (! [W1] :( aElementOf0(W1,slsdtgt0(xb))<=> (? [W2] :( aElement0(W2)& sdtasdt0(xb,W2) = W1 ) )))=> ( (? [W1,W2] :( aElementOf0(W1,slsdtgt0(xa))& aElementOf0(W2,slsdtgt0(xb))& sdtpldt0(W1,W2) = W0 ))| aElementOf0(W0,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))) ) ) )& W0 != sz00 ) ))),
% 0.17/5.56 inference(negated_conjecture,[status(cth)],[f44])).
% 0.17/5.56 fof(f61,plain,(
% 0.17/5.56 ![W0]: (~aElement0(W0)|(sdtpldt0(W0,sz00)=W0&W0=sdtpldt0(sz00,W0)))),
% 0.17/5.56 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 0.17/5.56 fof(f62,plain,(
% 0.17/5.56 ![X0]: (~aElement0(X0)|sdtpldt0(X0,sz00)=X0)),
% 0.17/5.56 inference(cnf_transformation,[status(thm)],[f61])).
% 0.17/5.56 fof(f63,plain,(
% 0.17/5.56 ![X0]: (~aElement0(X0)|X0=sdtpldt0(sz00,X0))),
% 0.17/5.56 inference(cnf_transformation,[status(thm)],[f61])).
% 0.17/5.56 fof(f198,plain,(
% 0.17/5.56 aElement0(xa)),
% 0.17/5.56 inference(cnf_transformation,[status(thm)],[f39])).
% 0.17/5.56 fof(f199,plain,(
% 0.17/5.56 aElement0(xb)),
% 0.17/5.56 inference(cnf_transformation,[status(thm)],[f39])).
% 0.17/5.56 fof(f200,plain,(
% 0.17/5.56 ~xa=sz00|~xb=sz00),
% 0.17/5.56 inference(cnf_transformation,[status(thm)],[f40])).
% 0.17/5.56 fof(f238,plain,(
% 0.17/5.56 (((((((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))),
% 0.17/5.56 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])).
% 0.17/5.56 fof(f241,plain,(
% 0.17/5.56 aElementOf0(sz00,slsdtgt0(xa))),
% 0.17/5.56 inference(cnf_transformation,[status(thm)],[f238])).
% 0.17/5.56 fof(f244,plain,(
% 0.17/5.56 aElementOf0(xa,slsdtgt0(xa))),
% 0.17/5.56 inference(cnf_transformation,[status(thm)],[f238])).
% 0.17/5.56 fof(f247,plain,(
% 0.17/5.56 aElementOf0(sz00,slsdtgt0(xb))),
% 0.17/5.56 inference(cnf_transformation,[status(thm)],[f238])).
% 0.17/5.56 fof(f250,plain,(
% 0.17/5.56 aElementOf0(xb,slsdtgt0(xb))),
% 0.17/5.56 inference(cnf_transformation,[status(thm)],[f238])).
% 0.17/5.56 fof(f251,plain,(
% 0.17/5.56 (![W0]: (((![W1]: (aElementOf0(W1,slsdtgt0(xa))<=>(?[W2]: (aElement0(W2)&sdtasdt0(xa,W2)=W1))))&((![W1]: (aElementOf0(W1,slsdtgt0(xb))<=>(?[W2]: (aElement0(W2)&sdtasdt0(xb,W2)=W1))))&((![W1,W2]: ((~aElementOf0(W1,slsdtgt0(xa))|~aElementOf0(W2,slsdtgt0(xb)))|~sdtpldt0(W1,W2)=W0))&~aElementOf0(W0,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))))))|W0=sz00))),
% 0.17/5.56 inference(pre_NNF_transformation,[status(thm)],[f45])).
% 0.17/5.56 fof(f252,plain,(
% 0.17/5.56 ![W0]: (((![W1]: ((~aElementOf0(W1,slsdtgt0(xa))|(?[W2]: (aElement0(W2)&sdtasdt0(xa,W2)=W1)))&(aElementOf0(W1,slsdtgt0(xa))|(![W2]: (~aElement0(W2)|~sdtasdt0(xa,W2)=W1)))))&((![W1]: ((~aElementOf0(W1,slsdtgt0(xb))|(?[W2]: (aElement0(W2)&sdtasdt0(xb,W2)=W1)))&(aElementOf0(W1,slsdtgt0(xb))|(![W2]: (~aElement0(W2)|~sdtasdt0(xb,W2)=W1)))))&((![W1,W2]: ((~aElementOf0(W1,slsdtgt0(xa))|~aElementOf0(W2,slsdtgt0(xb)))|~sdtpldt0(W1,W2)=W0))&~aElementOf0(W0,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))))))|W0=sz00)),
% 0.17/5.57 inference(NNF_transformation,[status(thm)],[f251])).
% 0.17/5.57 fof(f253,plain,(
% 0.17/5.57 ![W0]: ((((![W1]: (~aElementOf0(W1,slsdtgt0(xa))|(?[W2]: (aElement0(W2)&sdtasdt0(xa,W2)=W1))))&(![W1]: (aElementOf0(W1,slsdtgt0(xa))|(![W2]: (~aElement0(W2)|~sdtasdt0(xa,W2)=W1)))))&(((![W1]: (~aElementOf0(W1,slsdtgt0(xb))|(?[W2]: (aElement0(W2)&sdtasdt0(xb,W2)=W1))))&(![W1]: (aElementOf0(W1,slsdtgt0(xb))|(![W2]: (~aElement0(W2)|~sdtasdt0(xb,W2)=W1)))))&((![W1,W2]: ((~aElementOf0(W1,slsdtgt0(xa))|~aElementOf0(W2,slsdtgt0(xb)))|~sdtpldt0(W1,W2)=W0))&~aElementOf0(W0,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))))))|W0=sz00)),
% 0.17/5.57 inference(miniscoping,[status(thm)],[f252])).
% 0.17/5.57 fof(f254,plain,(
% 0.17/5.57 ![W0]: ((((![W1]: (~aElementOf0(W1,slsdtgt0(xa))|(aElement0(sK31_skl(W1,W0))&sdtasdt0(xa,sK31_skl(W1,W0))=W1)))&(![W1]: (aElementOf0(W1,slsdtgt0(xa))|(![W2]: (~aElement0(W2)|~sdtasdt0(xa,W2)=W1)))))&(((![W1]: (~aElementOf0(W1,slsdtgt0(xb))|(aElement0(sK32_skl(W1,W0))&sdtasdt0(xb,sK32_skl(W1,W0))=W1)))&(![W1]: (aElementOf0(W1,slsdtgt0(xb))|(![W2]: (~aElement0(W2)|~sdtasdt0(xb,W2)=W1)))))&((![W1,W2]: ((~aElementOf0(W1,slsdtgt0(xa))|~aElementOf0(W2,slsdtgt0(xb)))|~sdtpldt0(W1,W2)=W0))&~aElementOf0(W0,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))))))|W0=sz00)),
% 0.17/5.57 inference(skolemize,[status(esa),new_symbols(skolem,[sK31_skl,sK32_skl]),skolemize(W2,sK31_skl(W1,W0)),skolemize(W2,sK32_skl(W1,W0))],[f253])).
% 0.17/5.57 fof(f261,plain,(
% 0.17/5.57 ![X0,X1,X2]: (~aElementOf0(X0,slsdtgt0(xa))|~aElementOf0(X1,slsdtgt0(xb))|~sdtpldt0(X0,X1)=X2|X2=sz00)),
% 0.17/5.57 inference(cnf_transformation,[status(thm)],[f254])).
% 0.17/5.57 fof(f300,definition,(
% 0.17/5.57 sQ0_spl <=> (xa=sz00)),
% 0.17/5.57 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.17/5.57 fof(f302,plain,(
% 0.17/5.57 ~xa=sz00|sQ0_spl),
% 0.17/5.57 inference(component_clause,[status(thm)],[f300])).
% 0.17/5.57 fof(f303,definition,(
% 0.17/5.57 sQ1_spl <=> (xb=sz00)),
% 0.17/5.57 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.17/5.57 fof(f305,plain,(
% 0.17/5.57 ~xb=sz00|sQ1_spl),
% 0.17/5.57 inference(component_clause,[status(thm)],[f303])).
% 0.17/5.57 fof(f306,plain,(
% 0.17/5.57 ~sQ0_spl|~sQ1_spl),
% 0.17/5.57 inference(split_clause,[status(thm)],[f200,f300,f303])).
% 0.17/5.57 fof(f334,plain,(
% 0.17/5.57 ![X0,X1]: (~aElementOf0(X0,slsdtgt0(xa))|~aElementOf0(X1,slsdtgt0(xb))|sdtpldt0(X0,X1)=sz00)),
% 0.17/5.57 inference(destructive_equality_resolution,[status(thm)],[f261])).
% 0.17/5.57 fof(f342,plain,(
% 0.17/5.57 ![X0]: (~aElementOf0(X0,slsdtgt0(xb))|sdtpldt0(sz00,X0)=sz00)),
% 0.17/5.57 inference(resolution,[status(thm)],[f241,f334])).
% 0.17/5.57 fof(f343,plain,(
% 0.17/5.57 ![X0]: (~aElementOf0(X0,slsdtgt0(xb))|sdtpldt0(xa,X0)=sz00)),
% 0.17/5.57 inference(resolution,[status(thm)],[f244,f334])).
% 0.17/5.57 fof(f417,plain,(
% 0.17/5.57 sdtpldt0(xa,sz00)=sz00),
% 0.17/5.57 inference(resolution,[status(thm)],[f343,f247])).
% 0.17/5.57 fof(f426,plain,(
% 0.17/5.57 sdtpldt0(sz00,xb)=sz00),
% 0.17/5.57 inference(resolution,[status(thm)],[f250,f342])).
% 0.17/5.57 fof(f447,plain,(
% 0.17/5.57 sdtpldt0(xa,sz00)=xa),
% 0.17/5.57 inference(resolution,[status(thm)],[f62,f198])).
% 0.17/5.57 fof(f488,plain,(
% 0.17/5.57 sz00=xa),
% 0.17/5.57 inference(forward_demodulation,[status(thm)],[f417,f447])).
% 0.17/5.57 fof(f522,plain,(
% 0.17/5.57 xb=sdtpldt0(sz00,xb)),
% 0.17/5.57 inference(resolution,[status(thm)],[f63,f199])).
% 0.17/5.57 fof(f525,plain,(
% 0.17/5.57 xb=sz00),
% 0.17/5.57 inference(forward_demodulation,[status(thm)],[f426,f522])).
% 0.17/5.57 fof(f526,plain,(
% 0.17/5.57 $false|sQ1_spl),
% 0.17/5.57 inference(forward_subsumption_resolution,[status(thm)],[f525,f305])).
% 0.17/5.57 fof(f527,plain,(
% 0.17/5.57 sQ1_spl),
% 0.17/5.57 inference(contradiction_clause,[status(thm)],[f526])).
% 0.17/5.57 fof(f566,plain,(
% 0.17/5.57 ~sz00=sz00|sQ0_spl),
% 0.17/5.57 inference(forward_demodulation,[status(thm)],[f488,f302])).
% 0.17/5.57 fof(f567,plain,(
% 0.17/5.57 $false|sQ0_spl),
% 0.17/5.57 inference(trivial_equality_resolution,[status(thm)],[f566])).
% 0.17/5.57 fof(f568,plain,(
% 0.17/5.57 sQ0_spl),
% 0.17/5.57 inference(contradiction_clause,[status(thm)],[f567])).
% 0.17/5.57 fof(f569,plain,(
% 0.17/5.57 $false),
% 0.17/5.57 inference(sat_refutation,[status(thm)],[f306,f527,f568])).
% 0.17/5.57 % SZS output end CNFRefutation for theBenchmark.p
% 0.17/5.60 % Elapsed time: 0.187084 seconds
% 0.17/5.60 % CPU time: 1.185974 seconds
% 0.17/5.60 % Total memory used: 121.989 MB
% 0.17/5.60 % Net memory used: 120.787 MB
%------------------------------------------------------------------------------