%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : RNG061+1 : 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 : n009.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:15 PM UTC 2026
% Result : Theorem 72.07s 9.65s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : RNG061+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n009.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Mon Sep 21 04:16:42 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.18/0.47 % Drodi V4.1.1
% 72.07/9.65 % Refutation found
% 72.07/9.65 % SZS status Theorem for theBenchmark: Theorem is valid
% 72.07/9.65 % SZS output start CNFRefutation for theBenchmark
% 72.07/9.65 fof(f12,axiom,(
% 72.07/9.65 (! [W0] :( aScalar0(W0)=> aScalar0(smndt0(W0)) ) )),
% 72.07/9.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.07/9.65 fof(f13,axiom,(
% 72.07/9.65 (! [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 ) ) )),
% 72.07/9.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.07/9.65 fof(f14,axiom,(
% 72.07/9.65 (! [W0,W1,W2] :( ( aScalar0(W0)& aScalar0(W1)& aScalar0(W2) )=> ( sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2))& sdtpldt0(W0,W1) = sdtpldt0(W1,W0)& sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2))& sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) ) )),
% 72.07/9.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.07/9.65 fof(f15,axiom,(
% 72.07/9.65 (! [W0,W1,W2] :( ( aScalar0(W0)& aScalar0(W1)& aScalar0(W2) )=> ( sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2))& sdtasdt0(sdtpldt0(W0,W1),W2) = sdtpldt0(sdtasdt0(W0,W2),sdtasdt0(W1,W2)) ) ) )),
% 72.07/9.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.07/9.65 fof(f18,axiom,(
% 72.07/9.65 (! [W0,W1] :( ( aScalar0(W0)& aScalar0(W1) )=> sdtasdt0(smndt0(W0),smndt0(W1)) = sdtasdt0(W0,W1) ) )),
% 72.07/9.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.07/9.65 fof(f52,hypothesis,(
% 72.07/9.65 ( aScalar0(xR)& xR = sdtasdt0(xC,xG) ) ),
% 72.07/9.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.07/9.65 fof(f54,hypothesis,(
% 72.07/9.65 ( aScalar0(xS)& xS = sdtasdt0(xF,xD) ) ),
% 72.07/9.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.07/9.65 fof(f58,hypothesis,(
% 72.07/9.65 ( sdtasdt0(xR,smndt0(xS)) = smndt0(xN)& sdtasdt0(smndt0(xS),xR) = smndt0(xN)& sdtasdt0(smndt0(xS),smndt0(xS)) = sdtasdt0(xS,xS) ) ),
% 72.07/9.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.07/9.65 fof(f59,hypothesis,(
% 72.07/9.65 sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))) = sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),smndt0(xN)),sdtpldt0(smndt0(xN),sdtasdt0(xS,xS))) ),
% 72.07/9.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.07/9.65 fof(f60,conjecture,(
% 72.07/9.65 sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))) = sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),smndt0(xN)),sdtpldt0(sdtasdt0(xS,xS),smndt0(xN))) ),
% 72.07/9.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.07/9.65 fof(f61,negated_conjecture,(
% 72.07/9.65 ~(sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))) = sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),smndt0(xN)),sdtpldt0(sdtasdt0(xS,xS),smndt0(xN))) )),
% 72.07/9.65 inference(negated_conjecture,[status(cth)],[f60])).
% 72.07/9.65 fof(f87,plain,(
% 72.07/9.65 ![W0]: (~aScalar0(W0)|aScalar0(smndt0(W0)))),
% 72.07/9.65 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 72.07/9.65 fof(f88,plain,(
% 72.07/9.65 ![X0]: (~aScalar0(X0)|aScalar0(smndt0(X0)))),
% 72.07/9.65 inference(cnf_transformation,[status(thm)],[f87])).
% 72.07/9.65 fof(f89,plain,(
% 72.07/9.65 ![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))),
% 72.07/9.65 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 72.07/9.65 fof(f96,plain,(
% 72.07/9.65 ![X0]: (~aScalar0(X0)|smndt0(smndt0(X0))=X0)),
% 72.07/9.65 inference(cnf_transformation,[status(thm)],[f89])).
% 72.07/9.65 fof(f98,plain,(
% 72.07/9.65 ![W0,W1,W2]: (((~aScalar0(W0)|~aScalar0(W1))|~aScalar0(W2))|(((sdtpldt0(sdtpldt0(W0,W1),W2)=sdtpldt0(W0,sdtpldt0(W1,W2))&sdtpldt0(W0,W1)=sdtpldt0(W1,W0))&sdtasdt0(sdtasdt0(W0,W1),W2)=sdtasdt0(W0,sdtasdt0(W1,W2)))&sdtasdt0(W0,W1)=sdtasdt0(W1,W0)))),
% 72.07/9.65 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 72.07/9.65 fof(f100,plain,(
% 72.07/9.65 ![X0,X1,X2]: (~aScalar0(X0)|~aScalar0(X1)|~aScalar0(X2)|sdtpldt0(X0,X1)=sdtpldt0(X1,X0))),
% 72.07/9.65 inference(cnf_transformation,[status(thm)],[f98])).
% 72.07/9.65 fof(f103,plain,(
% 72.07/9.65 ![W0,W1,W2]: (((~aScalar0(W0)|~aScalar0(W1))|~aScalar0(W2))|(sdtasdt0(W0,sdtpldt0(W1,W2))=sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2))&sdtasdt0(sdtpldt0(W0,W1),W2)=sdtpldt0(sdtasdt0(W0,W2),sdtasdt0(W1,W2))))),
% 72.07/9.65 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 72.07/9.65 fof(f105,plain,(
% 72.07/9.65 ![X0,X1,X2]: (~aScalar0(X0)|~aScalar0(X1)|~aScalar0(X2)|sdtasdt0(sdtpldt0(X0,X1),X2)=sdtpldt0(sdtasdt0(X0,X2),sdtasdt0(X1,X2)))),
% 72.07/9.65 inference(cnf_transformation,[status(thm)],[f103])).
% 72.07/9.65 fof(f111,plain,(
% 72.07/9.65 ![W0,W1]: ((~aScalar0(W0)|~aScalar0(W1))|sdtasdt0(smndt0(W0),smndt0(W1))=sdtasdt0(W0,W1))),
% 72.07/9.65 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 72.07/9.65 fof(f112,plain,(
% 72.07/9.65 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|sdtasdt0(smndt0(X0),smndt0(X1))=sdtasdt0(X0,X1))),
% 72.07/9.65 inference(cnf_transformation,[status(thm)],[f111])).
% 72.07/9.65 fof(f186,plain,(
% 72.07/9.65 aScalar0(xR)),
% 72.07/9.65 inference(cnf_transformation,[status(thm)],[f52])).
% 72.07/9.65 fof(f190,plain,(
% 72.07/9.65 aScalar0(xS)),
% 72.07/9.65 inference(cnf_transformation,[status(thm)],[f54])).
% 72.07/9.65 fof(f196,plain,(
% 72.07/9.65 sdtasdt0(xR,smndt0(xS))=smndt0(xN)),
% 72.07/9.65 inference(cnf_transformation,[status(thm)],[f58])).
% 72.07/9.65 fof(f197,plain,(
% 72.07/9.65 sdtasdt0(smndt0(xS),xR)=smndt0(xN)),
% 72.07/9.65 inference(cnf_transformation,[status(thm)],[f58])).
% 72.07/9.65 fof(f199,plain,(
% 72.07/9.65 sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS)))=sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),smndt0(xN)),sdtpldt0(smndt0(xN),sdtasdt0(xS,xS)))),
% 72.07/9.65 inference(cnf_transformation,[status(thm)],[f59])).
% 72.07/9.65 fof(f200,plain,(
% 72.07/9.65 ~sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS)))=sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),smndt0(xN)),sdtpldt0(sdtasdt0(xS,xS),smndt0(xN)))),
% 72.07/9.65 inference(cnf_transformation,[status(thm)],[f61])).
% 72.07/9.65 fof(f208,plain,(
% 72.07/9.65 ![X0]: (~aScalar0(X0)|sdtasdt0(sdtpldt0(X0,xR),xR)=sdtpldt0(sdtasdt0(X0,xR),sdtasdt0(xR,xR)))),
% 72.07/9.65 inference(resolution,[status(thm)],[f186,f105])).
% 72.07/9.65 fof(f209,plain,(
% 72.07/9.65 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|sdtasdt0(sdtpldt0(X0,X1),xR)=sdtpldt0(sdtasdt0(X0,xR),sdtasdt0(X1,xR)))),
% 72.07/9.65 inference(resolution,[status(thm)],[f186,f105])).
% 72.07/9.65 fof(f221,plain,(
% 72.07/9.65 ![X0]: (~aScalar0(X0)|sdtpldt0(X0,xR)=sdtpldt0(xR,X0))),
% 72.07/9.65 inference(resolution,[status(thm)],[f186,f100])).
% 72.07/9.65 fof(f222,plain,(
% 72.07/9.65 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|sdtpldt0(X0,X1)=sdtpldt0(X1,X0))),
% 72.07/9.65 inference(resolution,[status(thm)],[f186,f100])).
% 72.07/9.65 fof(f226,plain,(
% 72.07/9.65 ![X0]: (~aScalar0(X0)|sdtasdt0(sdtpldt0(X0,xS),xS)=sdtpldt0(sdtasdt0(X0,xS),sdtasdt0(xS,xS)))),
% 72.07/9.65 inference(resolution,[status(thm)],[f190,f105])).
% 72.07/9.65 fof(f227,plain,(
% 72.07/9.65 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|sdtasdt0(sdtpldt0(X0,X1),xS)=sdtpldt0(sdtasdt0(X0,xS),sdtasdt0(X1,xS)))),
% 72.07/9.65 inference(resolution,[status(thm)],[f190,f105])).
% 72.07/9.65 fof(f249,plain,(
% 72.07/9.65 aScalar0(smndt0(xS))),
% 72.07/9.65 inference(resolution,[status(thm)],[f88,f190])).
% 72.07/9.65 fof(f250,plain,(
% 72.07/9.65 aScalar0(smndt0(xR))),
% 72.07/9.65 inference(resolution,[status(thm)],[f88,f186])).
% 72.07/9.65 fof(f294,plain,(
% 72.07/9.65 smndt0(smndt0(xR))=xR),
% 72.07/9.65 inference(resolution,[status(thm)],[f96,f186])).
% 72.07/9.65 fof(f431,plain,(
% 72.07/9.65 ![X0]: (~aScalar0(X0)|sdtasdt0(smndt0(X0),smndt0(xS))=sdtasdt0(X0,xS))),
% 72.07/9.65 inference(resolution,[status(thm)],[f112,f190])).
% 72.07/9.65 fof(f1505,plain,(
% 72.07/9.65 sdtpldt0(smndt0(xS),xR)=sdtpldt0(xR,smndt0(xS))),
% 72.07/9.65 inference(resolution,[status(thm)],[f249,f221])).
% 72.07/9.65 fof(f1517,plain,(
% 72.07/9.65 ![X0]: (~aScalar0(X0)|sdtasdt0(sdtpldt0(X0,smndt0(xS)),xR)=sdtpldt0(sdtasdt0(X0,xR),sdtasdt0(smndt0(xS),xR)))),
% 72.07/9.65 inference(resolution,[status(thm)],[f249,f209])).
% 72.07/9.65 fof(f1518,plain,(
% 72.07/9.65 sdtasdt0(sdtpldt0(smndt0(xS),xR),xR)=sdtpldt0(sdtasdt0(smndt0(xS),xR),sdtasdt0(xR,xR))),
% 72.07/9.65 inference(resolution,[status(thm)],[f249,f208])).
% 72.07/9.65 fof(f1597,plain,(
% 72.07/9.65 ![X0]: (~aScalar0(X0)|sdtasdt0(sdtpldt0(X0,smndt0(xS)),xR)=sdtpldt0(sdtasdt0(X0,xR),smndt0(xN)))),
% 72.07/9.65 inference(forward_demodulation,[status(thm)],[f197,f1517])).
% 72.07/9.65 fof(f1598,plain,(
% 72.07/9.65 sdtasdt0(sdtpldt0(xR,smndt0(xS)),xR)=sdtpldt0(sdtasdt0(smndt0(xS),xR),sdtasdt0(xR,xR))),
% 72.07/9.65 inference(forward_demodulation,[status(thm)],[f1505,f1518])).
% 72.07/9.65 fof(f1599,plain,(
% 72.07/9.65 sdtasdt0(sdtpldt0(xR,smndt0(xS)),xR)=sdtpldt0(smndt0(xN),sdtasdt0(xR,xR))),
% 72.07/9.65 inference(forward_demodulation,[status(thm)],[f197,f1598])).
% 72.07/9.65 fof(f1823,plain,(
% 72.07/9.65 ![X0]: (~aScalar0(X0)|sdtasdt0(sdtpldt0(X0,smndt0(xR)),xS)=sdtpldt0(sdtasdt0(X0,xS),sdtasdt0(smndt0(xR),xS)))),
% 72.07/9.65 inference(resolution,[status(thm)],[f250,f227])).
% 72.07/9.65 fof(f1824,plain,(
% 72.07/9.65 sdtasdt0(sdtpldt0(smndt0(xR),xS),xS)=sdtpldt0(sdtasdt0(smndt0(xR),xS),sdtasdt0(xS,xS))),
% 72.07/9.65 inference(resolution,[status(thm)],[f250,f226])).
% 72.07/9.65 fof(f1840,plain,(
% 72.07/9.65 sdtasdt0(smndt0(smndt0(xR)),smndt0(xS))=sdtasdt0(smndt0(xR),xS)),
% 72.07/9.65 inference(resolution,[status(thm)],[f250,f431])).
% 72.07/9.65 fof(f1874,plain,(
% 72.07/9.65 ![X0]: (~aScalar0(X0)|sdtpldt0(X0,smndt0(xR))=sdtpldt0(smndt0(xR),X0))),
% 72.07/9.65 inference(resolution,[status(thm)],[f250,f222])).
% 72.07/9.65 fof(f1926,plain,(
% 72.07/9.65 sdtasdt0(xR,smndt0(xS))=sdtasdt0(smndt0(xR),xS)),
% 72.07/9.65 inference(forward_demodulation,[status(thm)],[f294,f1840])).
% 72.07/9.65 fof(f1929,plain,(
% 72.07/9.65 sdtasdt0(sdtpldt0(smndt0(xR),xS),xS)=sdtpldt0(smndt0(xN),sdtasdt0(xS,xS))),
% 72.07/9.65 inference(backward_demodulation,[status(thm)],[f1933,f1824])).
% 72.07/9.65 fof(f1930,plain,(
% 72.07/9.65 ![X0]: (~aScalar0(X0)|sdtasdt0(sdtpldt0(X0,smndt0(xR)),xS)=sdtpldt0(sdtasdt0(X0,xS),smndt0(xN)))),
% 72.07/9.65 inference(backward_demodulation,[status(thm)],[f1933,f1823])).
% 72.07/9.65 fof(f1933,plain,(
% 72.07/9.65 smndt0(xN)=sdtasdt0(smndt0(xR),xS)),
% 72.07/9.65 inference(forward_demodulation,[status(thm)],[f196,f1926])).
% 72.07/9.65 fof(f2033,plain,(
% 72.07/9.65 sdtasdt0(sdtpldt0(xR,smndt0(xS)),xR)=sdtpldt0(sdtasdt0(xR,xR),smndt0(xN))),
% 72.07/9.65 inference(resolution,[status(thm)],[f1597,f186])).
% 72.07/9.65 fof(f2043,plain,(
% 72.07/9.65 sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS)))=sdtpldt0(sdtpldt0(smndt0(xN),sdtasdt0(xR,xR)),sdtpldt0(smndt0(xN),sdtasdt0(xS,xS)))),
% 72.07/9.65 inference(backward_demodulation,[status(thm)],[f2045,f199])).
% 72.07/9.65 fof(f2044,plain,(
% 72.07/9.65 ~sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS)))=sdtpldt0(sdtpldt0(smndt0(xN),sdtasdt0(xR,xR)),sdtpldt0(sdtasdt0(xS,xS),smndt0(xN)))),
% 72.07/9.65 inference(backward_demodulation,[status(thm)],[f2045,f200])).
% 72.07/9.65 fof(f2045,plain,(
% 72.07/9.65 sdtpldt0(smndt0(xN),sdtasdt0(xR,xR))=sdtpldt0(sdtasdt0(xR,xR),smndt0(xN))),
% 72.07/9.65 inference(forward_demodulation,[status(thm)],[f1599,f2033])).
% 72.07/9.65 fof(f2774,plain,(
% 72.07/9.65 sdtpldt0(xS,smndt0(xR))=sdtpldt0(smndt0(xR),xS)),
% 72.07/9.65 inference(resolution,[status(thm)],[f1874,f190])).
% 72.07/9.65 fof(f2782,plain,(
% 72.07/9.65 sdtasdt0(sdtpldt0(xS,smndt0(xR)),xS)=sdtpldt0(smndt0(xN),sdtasdt0(xS,xS))),
% 72.07/9.65 inference(backward_demodulation,[status(thm)],[f2774,f1929])).
% 72.07/9.65 fof(f2885,plain,(
% 72.07/9.65 sdtasdt0(sdtpldt0(xS,smndt0(xR)),xS)=sdtpldt0(sdtasdt0(xS,xS),smndt0(xN))),
% 72.07/9.65 inference(resolution,[status(thm)],[f1930,f190])).
% 72.07/9.65 fof(f2896,plain,(
% 72.07/9.65 ~sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS)))=sdtpldt0(sdtpldt0(smndt0(xN),sdtasdt0(xR,xR)),sdtpldt0(smndt0(xN),sdtasdt0(xS,xS)))),
% 72.07/9.65 inference(backward_demodulation,[status(thm)],[f2898,f2044])).
% 72.07/9.65 fof(f2898,plain,(
% 72.07/9.65 sdtpldt0(smndt0(xN),sdtasdt0(xS,xS))=sdtpldt0(sdtasdt0(xS,xS),smndt0(xN))),
% 72.07/9.65 inference(forward_demodulation,[status(thm)],[f2782,f2885])).
% 72.07/9.65 fof(f2902,plain,(
% 72.07/9.65 ~sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS)))=sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS)))),
% 72.07/9.65 inference(forward_demodulation,[status(thm)],[f2043,f2896])).
% 72.07/9.65 fof(f2903,plain,(
% 72.07/9.65 $false),
% 72.07/9.65 inference(trivial_equality_resolution,[status(thm)],[f2902])).
% 72.07/9.65 % SZS output end CNFRefutation for theBenchmark.p
% 1.52/9.72 % Elapsed time: 9.244941 seconds
% 1.52/9.72 % CPU time: 72.634581 seconds
% 1.52/9.72 % Total memory used: 510.673 MB
% 1.52/9.72 % Net memory used: 471.009 MB
%------------------------------------------------------------------------------