%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : RNG061+2 : 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 : 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:15 PM UTC 2026
% Result : Theorem 11.01s 1.89s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG061+2 : 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/0.36 % Computer : n013.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Mon Sep 21 04:16:20 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.38 % Drodi V4.1.1
% 11.01/1.89 % Refutation found
% 11.01/1.89 % SZS status Theorem for theBenchmark: Theorem is valid
% 11.01/1.89 % SZS output start CNFRefutation for theBenchmark
% 11.01/1.89 fof(f12,axiom,(
% 11.01/1.89 (! [W0] :( aScalar0(W0)=> aScalar0(smndt0(W0)) ) )),
% 11.01/1.89 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.01/1.89 fof(f13,axiom,(
% 11.01/1.89 (! [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 ) ) )),
% 11.01/1.89 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.01/1.89 fof(f14,axiom,(
% 11.01/1.89 (! [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) ) ) )),
% 11.01/1.89 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.01/1.89 fof(f15,axiom,(
% 11.01/1.89 (! [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)) ) ) )),
% 11.01/1.89 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.01/1.89 fof(f18,axiom,(
% 11.01/1.89 (! [W0,W1] :( ( aScalar0(W0)& aScalar0(W1) )=> sdtasdt0(smndt0(W0),smndt0(W1)) = sdtasdt0(W0,W1) ) )),
% 11.01/1.89 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.01/1.89 fof(f52,hypothesis,(
% 11.01/1.89 ( aScalar0(xR)& xR = sdtasdt0(xC,xG) ) ),
% 11.01/1.89 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.01/1.89 fof(f54,hypothesis,(
% 11.01/1.89 ( aScalar0(xS)& xS = sdtasdt0(xF,xD) ) ),
% 11.01/1.89 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.01/1.89 fof(f58,hypothesis,(
% 11.01/1.89 ( sdtasdt0(xR,smndt0(xS)) = smndt0(xN)& sdtasdt0(smndt0(xS),xR) = smndt0(xN)& sdtasdt0(smndt0(xS),smndt0(xS)) = sdtasdt0(xS,xS) ) ),
% 11.01/1.89 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.01/1.89 fof(f59,hypothesis,(
% 11.01/1.89 sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))) = sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),smndt0(xN)),sdtpldt0(smndt0(xN),sdtasdt0(xS,xS))) ),
% 11.01/1.89 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.01/1.89 fof(f60,conjecture,(
% 11.01/1.89 sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))) = sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),smndt0(xN)),sdtpldt0(sdtasdt0(xS,xS),smndt0(xN))) ),
% 11.01/1.89 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.01/1.89 fof(f61,negated_conjecture,(
% 11.01/1.89 ~(sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))) = sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),smndt0(xN)),sdtpldt0(sdtasdt0(xS,xS),smndt0(xN))) )),
% 11.01/1.89 inference(negated_conjecture,[status(cth)],[f60])).
% 11.01/1.89 fof(f87,plain,(
% 11.01/1.89 ![W0]: (~aScalar0(W0)|aScalar0(smndt0(W0)))),
% 11.01/1.89 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 11.01/1.89 fof(f88,plain,(
% 11.01/1.89 ![X0]: (~aScalar0(X0)|aScalar0(smndt0(X0)))),
% 11.01/1.89 inference(cnf_transformation,[status(thm)],[f87])).
% 11.01/1.89 fof(f89,plain,(
% 11.01/1.89 ![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))),
% 11.01/1.89 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 11.01/1.89 fof(f96,plain,(
% 11.01/1.89 ![X0]: (~aScalar0(X0)|smndt0(smndt0(X0))=X0)),
% 11.01/1.89 inference(cnf_transformation,[status(thm)],[f89])).
% 11.01/1.89 fof(f98,plain,(
% 11.01/1.89 ![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)))),
% 11.01/1.89 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 11.01/1.89 fof(f100,plain,(
% 11.01/1.89 ![X0,X1,X2]: (~aScalar0(X0)|~aScalar0(X1)|~aScalar0(X2)|sdtpldt0(X0,X1)=sdtpldt0(X1,X0))),
% 11.01/1.89 inference(cnf_transformation,[status(thm)],[f98])).
% 11.01/1.89 fof(f103,plain,(
% 11.01/1.89 ![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))))),
% 11.01/1.89 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 11.01/1.89 fof(f105,plain,(
% 11.01/1.89 ![X0,X1,X2]: (~aScalar0(X0)|~aScalar0(X1)|~aScalar0(X2)|sdtasdt0(sdtpldt0(X0,X1),X2)=sdtpldt0(sdtasdt0(X0,X2),sdtasdt0(X1,X2)))),
% 11.01/1.89 inference(cnf_transformation,[status(thm)],[f103])).
% 11.01/1.89 fof(f111,plain,(
% 11.01/1.89 ![W0,W1]: ((~aScalar0(W0)|~aScalar0(W1))|sdtasdt0(smndt0(W0),smndt0(W1))=sdtasdt0(W0,W1))),
% 11.01/1.89 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 11.01/1.89 fof(f112,plain,(
% 11.01/1.89 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|sdtasdt0(smndt0(X0),smndt0(X1))=sdtasdt0(X0,X1))),
% 11.01/1.89 inference(cnf_transformation,[status(thm)],[f111])).
% 11.01/1.89 fof(f192,plain,(
% 11.01/1.89 aScalar0(xR)),
% 11.01/1.89 inference(cnf_transformation,[status(thm)],[f52])).
% 11.01/1.89 fof(f196,plain,(
% 11.01/1.89 aScalar0(xS)),
% 11.01/1.89 inference(cnf_transformation,[status(thm)],[f54])).
% 11.01/1.89 fof(f202,plain,(
% 11.01/1.89 sdtasdt0(xR,smndt0(xS))=smndt0(xN)),
% 11.01/1.89 inference(cnf_transformation,[status(thm)],[f58])).
% 11.01/1.89 fof(f203,plain,(
% 11.01/1.89 sdtasdt0(smndt0(xS),xR)=smndt0(xN)),
% 11.01/1.89 inference(cnf_transformation,[status(thm)],[f58])).
% 11.01/1.89 fof(f205,plain,(
% 11.01/1.89 sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS)))=sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),smndt0(xN)),sdtpldt0(smndt0(xN),sdtasdt0(xS,xS)))),
% 11.01/1.89 inference(cnf_transformation,[status(thm)],[f59])).
% 11.01/1.89 fof(f206,plain,(
% 11.01/1.89 ~sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS)))=sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),smndt0(xN)),sdtpldt0(sdtasdt0(xS,xS),smndt0(xN)))),
% 11.01/1.89 inference(cnf_transformation,[status(thm)],[f61])).
% 11.01/1.89 fof(f215,plain,(
% 11.01/1.89 ![X0]: (~aScalar0(X0)|sdtasdt0(sdtpldt0(X0,xR),xR)=sdtpldt0(sdtasdt0(X0,xR),sdtasdt0(xR,xR)))),
% 11.01/1.89 inference(resolution,[status(thm)],[f192,f105])).
% 11.01/1.89 fof(f216,plain,(
% 11.01/1.89 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|sdtasdt0(sdtpldt0(X0,X1),xR)=sdtpldt0(sdtasdt0(X0,xR),sdtasdt0(X1,xR)))),
% 11.01/1.89 inference(resolution,[status(thm)],[f192,f105])).
% 11.01/1.89 fof(f228,plain,(
% 11.01/1.89 ![X0]: (~aScalar0(X0)|sdtpldt0(X0,xR)=sdtpldt0(xR,X0))),
% 11.01/1.89 inference(resolution,[status(thm)],[f192,f100])).
% 11.01/1.89 fof(f229,plain,(
% 11.01/1.89 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|sdtpldt0(X0,X1)=sdtpldt0(X1,X0))),
% 11.01/1.89 inference(resolution,[status(thm)],[f192,f100])).
% 11.01/1.89 fof(f233,plain,(
% 11.01/1.89 ![X0]: (~aScalar0(X0)|sdtasdt0(sdtpldt0(X0,xS),xS)=sdtpldt0(sdtasdt0(X0,xS),sdtasdt0(xS,xS)))),
% 11.01/1.89 inference(resolution,[status(thm)],[f196,f105])).
% 11.01/1.89 fof(f234,plain,(
% 11.01/1.89 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|sdtasdt0(sdtpldt0(X0,X1),xS)=sdtpldt0(sdtasdt0(X0,xS),sdtasdt0(X1,xS)))),
% 11.01/1.89 inference(resolution,[status(thm)],[f196,f105])).
% 11.01/1.89 fof(f256,plain,(
% 11.01/1.89 aScalar0(smndt0(xS))),
% 11.01/1.89 inference(resolution,[status(thm)],[f88,f196])).
% 11.01/1.89 fof(f257,plain,(
% 11.01/1.89 aScalar0(smndt0(xR))),
% 11.01/1.89 inference(resolution,[status(thm)],[f88,f192])).
% 11.01/1.89 fof(f301,plain,(
% 11.01/1.89 smndt0(smndt0(xR))=xR),
% 11.01/1.89 inference(resolution,[status(thm)],[f96,f192])).
% 11.01/1.89 fof(f438,plain,(
% 11.01/1.89 ![X0]: (~aScalar0(X0)|sdtasdt0(smndt0(X0),smndt0(xS))=sdtasdt0(X0,xS))),
% 11.01/1.89 inference(resolution,[status(thm)],[f112,f196])).
% 11.01/1.89 fof(f1352,plain,(
% 11.01/1.89 sdtpldt0(smndt0(xS),xR)=sdtpldt0(xR,smndt0(xS))),
% 11.01/1.89 inference(resolution,[status(thm)],[f256,f228])).
% 11.01/1.89 fof(f1364,plain,(
% 11.01/1.89 ![X0]: (~aScalar0(X0)|sdtasdt0(sdtpldt0(X0,smndt0(xS)),xR)=sdtpldt0(sdtasdt0(X0,xR),sdtasdt0(smndt0(xS),xR)))),
% 11.01/1.89 inference(resolution,[status(thm)],[f256,f216])).
% 11.01/1.89 fof(f1365,plain,(
% 11.01/1.89 sdtasdt0(sdtpldt0(smndt0(xS),xR),xR)=sdtpldt0(sdtasdt0(smndt0(xS),xR),sdtasdt0(xR,xR))),
% 11.01/1.89 inference(resolution,[status(thm)],[f256,f215])).
% 11.01/1.89 fof(f1444,plain,(
% 11.01/1.89 ![X0]: (~aScalar0(X0)|sdtasdt0(sdtpldt0(X0,smndt0(xS)),xR)=sdtpldt0(sdtasdt0(X0,xR),smndt0(xN)))),
% 11.01/1.89 inference(forward_demodulation,[status(thm)],[f203,f1364])).
% 11.01/1.89 fof(f1445,plain,(
% 11.01/1.89 sdtasdt0(sdtpldt0(xR,smndt0(xS)),xR)=sdtpldt0(sdtasdt0(smndt0(xS),xR),sdtasdt0(xR,xR))),
% 11.01/1.89 inference(forward_demodulation,[status(thm)],[f1352,f1365])).
% 11.01/1.89 fof(f1446,plain,(
% 11.01/1.89 sdtasdt0(sdtpldt0(xR,smndt0(xS)),xR)=sdtpldt0(smndt0(xN),sdtasdt0(xR,xR))),
% 11.01/1.89 inference(forward_demodulation,[status(thm)],[f203,f1445])).
% 11.01/1.89 fof(f1644,plain,(
% 11.01/1.89 ![X0]: (~aScalar0(X0)|sdtasdt0(sdtpldt0(X0,smndt0(xR)),xS)=sdtpldt0(sdtasdt0(X0,xS),sdtasdt0(smndt0(xR),xS)))),
% 11.01/1.89 inference(resolution,[status(thm)],[f257,f234])).
% 11.01/1.89 fof(f1645,plain,(
% 11.01/1.89 sdtasdt0(sdtpldt0(smndt0(xR),xS),xS)=sdtpldt0(sdtasdt0(smndt0(xR),xS),sdtasdt0(xS,xS))),
% 11.01/1.89 inference(resolution,[status(thm)],[f257,f233])).
% 11.01/1.89 fof(f1661,plain,(
% 11.01/1.89 sdtasdt0(smndt0(smndt0(xR)),smndt0(xS))=sdtasdt0(smndt0(xR),xS)),
% 6.62/1.92 inference(resolution,[status(thm)],[f257,f438])).
% 6.62/1.92 fof(f1695,plain,(
% 6.62/1.92 ![X0]: (~aScalar0(X0)|sdtpldt0(X0,smndt0(xR))=sdtpldt0(smndt0(xR),X0))),
% 6.62/1.92 inference(resolution,[status(thm)],[f257,f229])).
% 6.62/1.92 fof(f1747,plain,(
% 6.62/1.92 sdtasdt0(xR,smndt0(xS))=sdtasdt0(smndt0(xR),xS)),
% 6.62/1.92 inference(forward_demodulation,[status(thm)],[f301,f1661])).
% 6.62/1.92 fof(f1750,plain,(
% 6.62/1.92 sdtasdt0(sdtpldt0(smndt0(xR),xS),xS)=sdtpldt0(smndt0(xN),sdtasdt0(xS,xS))),
% 6.62/1.92 inference(backward_demodulation,[status(thm)],[f1754,f1645])).
% 6.62/1.92 fof(f1751,plain,(
% 6.62/1.92 ![X0]: (~aScalar0(X0)|sdtasdt0(sdtpldt0(X0,smndt0(xR)),xS)=sdtpldt0(sdtasdt0(X0,xS),smndt0(xN)))),
% 6.62/1.92 inference(backward_demodulation,[status(thm)],[f1754,f1644])).
% 6.62/1.92 fof(f1754,plain,(
% 6.62/1.92 smndt0(xN)=sdtasdt0(smndt0(xR),xS)),
% 6.62/1.92 inference(forward_demodulation,[status(thm)],[f202,f1747])).
% 6.62/1.92 fof(f1844,plain,(
% 6.62/1.92 sdtasdt0(sdtpldt0(xR,smndt0(xS)),xR)=sdtpldt0(sdtasdt0(xR,xR),smndt0(xN))),
% 6.62/1.92 inference(resolution,[status(thm)],[f1444,f192])).
% 6.62/1.92 fof(f1854,plain,(
% 6.62/1.92 sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS)))=sdtpldt0(sdtpldt0(smndt0(xN),sdtasdt0(xR,xR)),sdtpldt0(smndt0(xN),sdtasdt0(xS,xS)))),
% 6.62/1.92 inference(backward_demodulation,[status(thm)],[f1856,f205])).
% 6.62/1.92 fof(f1855,plain,(
% 6.62/1.92 ~sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS)))=sdtpldt0(sdtpldt0(smndt0(xN),sdtasdt0(xR,xR)),sdtpldt0(sdtasdt0(xS,xS),smndt0(xN)))),
% 6.62/1.92 inference(backward_demodulation,[status(thm)],[f1856,f206])).
% 6.62/1.92 fof(f1856,plain,(
% 6.62/1.92 sdtpldt0(smndt0(xN),sdtasdt0(xR,xR))=sdtpldt0(sdtasdt0(xR,xR),smndt0(xN))),
% 6.62/1.92 inference(forward_demodulation,[status(thm)],[f1446,f1844])).
% 6.62/1.92 fof(f2513,plain,(
% 6.62/1.92 sdtpldt0(xS,smndt0(xR))=sdtpldt0(smndt0(xR),xS)),
% 6.62/1.92 inference(resolution,[status(thm)],[f1695,f196])).
% 6.62/1.92 fof(f2521,plain,(
% 6.62/1.92 sdtasdt0(sdtpldt0(xS,smndt0(xR)),xS)=sdtpldt0(smndt0(xN),sdtasdt0(xS,xS))),
% 6.62/1.92 inference(backward_demodulation,[status(thm)],[f2513,f1750])).
% 6.62/1.92 fof(f2610,plain,(
% 6.62/1.92 sdtasdt0(sdtpldt0(xS,smndt0(xR)),xS)=sdtpldt0(sdtasdt0(xS,xS),smndt0(xN))),
% 6.62/1.92 inference(resolution,[status(thm)],[f1751,f196])).
% 6.62/1.92 fof(f2621,plain,(
% 6.62/1.92 ~sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS)))=sdtpldt0(sdtpldt0(smndt0(xN),sdtasdt0(xR,xR)),sdtpldt0(smndt0(xN),sdtasdt0(xS,xS)))),
% 6.62/1.92 inference(backward_demodulation,[status(thm)],[f2623,f1855])).
% 6.62/1.92 fof(f2623,plain,(
% 6.62/1.92 sdtpldt0(smndt0(xN),sdtasdt0(xS,xS))=sdtpldt0(sdtasdt0(xS,xS),smndt0(xN))),
% 6.62/1.92 inference(forward_demodulation,[status(thm)],[f2521,f2610])).
% 6.62/1.92 fof(f2627,plain,(
% 6.62/1.92 ~sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS)))=sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS)))),
% 6.62/1.92 inference(forward_demodulation,[status(thm)],[f1854,f2621])).
% 6.62/1.92 fof(f2628,plain,(
% 6.62/1.92 $false),
% 6.62/1.92 inference(trivial_equality_resolution,[status(thm)],[f2627])).
% 6.62/1.92 % SZS output end CNFRefutation for theBenchmark.p
% 6.62/1.93 % Elapsed time: 1.555015 seconds
% 6.62/1.93 % CPU time: 11.988212 seconds
% 6.62/1.93 % Total memory used: 264.235 MB
% 6.62/1.93 % Net memory used: 251.747 MB
%------------------------------------------------------------------------------