%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : RNG046+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 : 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 02:05:13 PM UTC 2026
% Result : Theorem 0.16s 0.52s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : RNG046+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.44 % Computer : n003.cluster.edu
% 0.16/0.44 % Model : x86_64 x86_64
% 0.16/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.44 % Memory : 8046.5625MB
% 0.16/0.44 % OS : Linux 6.8.0-71-generic
% 0.16/0.44 % CPULimit : 300
% 0.16/0.44 % WCLimit : 300
% 0.16/0.44 % DateTime : Mon Sep 21 04:17:01 UTC 2026
% 0.16/0.44 % CPUTime :
% 0.16/0.45 % Drodi V4.1.1
% 0.16/0.52 % Refutation found
% 0.16/0.52 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.16/0.52 % SZS output start CNFRefutation for theBenchmark
% 0.16/0.52 fof(f12,axiom,(
% 0.16/0.52 (! [W0] :( aScalar0(W0)=> aScalar0(smndt0(W0)) ) )),
% 0.16/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.52 fof(f13,axiom,(
% 0.16/0.52 (! [W0] :( aScalar0(W0)=> ( sdtpldt0(W0,sz0z00) = W0& sdtpldt0(sz0z00,W0) = W0& sdtasdt0(W0,sz0z00) = sz0z00& sdtasdt0(sz0z00,W0) = sz0z00& sdtpldt0(W0,smndt0(W0)) = sz0z00& sdtpldt0(smndt0(W0),W0) = sz0z00& smndt0(smndt0(W0)) = W0& smndt0(sz0z00) = sz0z00 ) ) )),
% 0.16/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.52 fof(f17,axiom,(
% 0.16/0.52 (! [W0,W1] :( ( aScalar0(W0)& aScalar0(W1) )=> ( sdtasdt0(W0,smndt0(W1)) = smndt0(sdtasdt0(W0,W1))& sdtasdt0(smndt0(W0),W1) = smndt0(sdtasdt0(W0,W1)) ) ) )),
% 0.16/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.52 fof(f18,hypothesis,(
% 0.16/0.52 ( aScalar0(xx)& aScalar0(xy) ) ),
% 0.16/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.52 fof(f19,conjecture,(
% 0.16/0.52 sdtasdt0(smndt0(xx),smndt0(xy)) = sdtasdt0(xx,xy) ),
% 0.16/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.52 fof(f20,negated_conjecture,(
% 0.16/0.52 ~(sdtasdt0(smndt0(xx),smndt0(xy)) = sdtasdt0(xx,xy) )),
% 0.16/0.52 inference(negated_conjecture,[status(cth)],[f19])).
% 0.16/0.52 fof(f46,plain,(
% 0.16/0.52 ![W0]: (~aScalar0(W0)|aScalar0(smndt0(W0)))),
% 0.16/0.52 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 0.16/0.52 fof(f47,plain,(
% 0.16/0.52 ![X0]: (~aScalar0(X0)|aScalar0(smndt0(X0)))),
% 0.16/0.52 inference(cnf_transformation,[status(thm)],[f46])).
% 0.16/0.52 fof(f48,plain,(
% 0.16/0.52 ![W0]: (~aScalar0(W0)|(((((((sdtpldt0(W0,sz0z00)=W0&sdtpldt0(sz0z00,W0)=W0)&sdtasdt0(W0,sz0z00)=sz0z00)&sdtasdt0(sz0z00,W0)=sz0z00)&sdtpldt0(W0,smndt0(W0))=sz0z00)&sdtpldt0(smndt0(W0),W0)=sz0z00)&smndt0(smndt0(W0))=W0)&smndt0(sz0z00)=sz0z00))),
% 0.16/0.52 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 0.16/0.52 fof(f55,plain,(
% 0.16/0.52 ![X0]: (~aScalar0(X0)|smndt0(smndt0(X0))=X0)),
% 0.16/0.52 inference(cnf_transformation,[status(thm)],[f48])).
% 0.16/0.52 fof(f67,plain,(
% 0.16/0.52 ![W0,W1]: ((~aScalar0(W0)|~aScalar0(W1))|(sdtasdt0(W0,smndt0(W1))=smndt0(sdtasdt0(W0,W1))&sdtasdt0(smndt0(W0),W1)=smndt0(sdtasdt0(W0,W1))))),
% 0.16/0.52 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 0.16/0.52 fof(f68,plain,(
% 0.16/0.52 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|sdtasdt0(X0,smndt0(X1))=smndt0(sdtasdt0(X0,X1)))),
% 0.16/0.52 inference(cnf_transformation,[status(thm)],[f67])).
% 0.16/0.52 fof(f69,plain,(
% 0.16/0.52 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|sdtasdt0(smndt0(X0),X1)=smndt0(sdtasdt0(X0,X1)))),
% 0.16/0.52 inference(cnf_transformation,[status(thm)],[f67])).
% 0.16/0.52 fof(f70,plain,(
% 0.16/0.52 aScalar0(xx)),
% 0.16/0.52 inference(cnf_transformation,[status(thm)],[f18])).
% 0.16/0.52 fof(f71,plain,(
% 0.16/0.52 aScalar0(xy)),
% 0.16/0.52 inference(cnf_transformation,[status(thm)],[f18])).
% 0.16/0.52 fof(f72,plain,(
% 0.16/0.52 ~sdtasdt0(smndt0(xx),smndt0(xy))=sdtasdt0(xx,xy)),
% 0.16/0.52 inference(cnf_transformation,[status(thm)],[f20])).
% 0.16/0.52 fof(f94,plain,(
% 0.16/0.52 ![X0]: (~aScalar0(X0)|sdtasdt0(smndt0(xx),X0)=smndt0(sdtasdt0(xx,X0)))),
% 0.16/0.52 inference(resolution,[status(thm)],[f70,f69])).
% 0.16/0.52 fof(f96,plain,(
% 0.16/0.52 ![X0]: (~aScalar0(X0)|sdtasdt0(xx,smndt0(X0))=smndt0(sdtasdt0(xx,X0)))),
% 0.16/0.52 inference(resolution,[status(thm)],[f68,f70])).
% 0.16/0.52 fof(f101,plain,(
% 0.16/0.52 smndt0(smndt0(xy))=xy),
% 0.16/0.52 inference(resolution,[status(thm)],[f55,f71])).
% 0.16/0.52 fof(f103,plain,(
% 0.16/0.52 aScalar0(smndt0(xy))),
% 0.16/0.52 inference(resolution,[status(thm)],[f47,f71])).
% 0.16/0.52 fof(f174,plain,(
% 0.16/0.52 sdtasdt0(smndt0(xx),smndt0(xy))=smndt0(sdtasdt0(xx,smndt0(xy)))),
% 0.16/0.52 inference(resolution,[status(thm)],[f94,f103])).
% 0.16/0.52 fof(f193,plain,(
% 0.16/0.52 sdtasdt0(xx,smndt0(smndt0(xy)))=smndt0(sdtasdt0(xx,smndt0(xy)))),
% 0.16/0.52 inference(resolution,[status(thm)],[f96,f103])).
% 0.16/0.52 fof(f198,plain,(
% 0.16/0.52 sdtasdt0(smndt0(xx),smndt0(xy))=sdtasdt0(xx,xy)),
% 0.16/0.52 inference(backward_demodulation,[status(thm)],[f199,f174])).
% 0.16/0.52 fof(f199,plain,(
% 0.16/0.52 sdtasdt0(xx,xy)=smndt0(sdtasdt0(xx,smndt0(xy)))),
% 0.16/0.52 inference(forward_demodulation,[status(thm)],[f101,f193])).
% 0.16/0.52 fof(f206,plain,(
% 0.16/0.52 $false),
% 0.16/0.52 inference(forward_subsumption_resolution,[status(thm)],[f198,f72])).
% 0.16/0.52 % SZS output end CNFRefutation for theBenchmark.p
% 0.16/0.54 % Elapsed time: 0.084351 seconds
% 0.16/0.54 % CPU time: 0.440606 seconds
% 0.16/0.54 % Total memory used: 85.948 MB
% 0.16/0.54 % Net memory used: 85.511 MB
%------------------------------------------------------------------------------