%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : RNG060+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 : n012.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 77.39s 10.15s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : RNG060+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n012.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Mon Sep 21 04:16:21 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 77.39/10.15 % Refutation found
% 77.39/10.15 % SZS status Theorem for theBenchmark: Theorem is valid
% 77.39/10.15 % SZS output start CNFRefutation for theBenchmark
% 77.39/10.15 fof(f12,axiom,(
% 77.39/10.15 (! [W0] :( aScalar0(W0)=> aScalar0(smndt0(W0)) ) )),
% 77.39/10.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 77.39/10.15 fof(f16,axiom,(
% 77.39/10.15 (! [W0,W1,W2,W3] :( ( aScalar0(W0)& aScalar0(W1)& aScalar0(W2)& aScalar0(W3) )=> sdtasdt0(sdtpldt0(W0,W1),sdtpldt0(W2,W3)) = sdtpldt0(sdtpldt0(sdtasdt0(W0,W2),sdtasdt0(W0,W3)),sdtpldt0(sdtasdt0(W1,W2),sdtasdt0(W1,W3))) ) )),
% 77.39/10.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 77.39/10.15 fof(f52,hypothesis,(
% 77.39/10.15 ( aScalar0(xR)& xR = sdtasdt0(xC,xG) ) ),
% 77.39/10.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 77.39/10.15 fof(f54,hypothesis,(
% 77.39/10.15 ( aScalar0(xS)& xS = sdtasdt0(xF,xD) ) ),
% 77.39/10.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 77.39/10.15 fof(f58,hypothesis,(
% 77.39/10.15 ( sdtasdt0(xR,smndt0(xS)) = smndt0(xN)& sdtasdt0(smndt0(xS),xR) = smndt0(xN)& sdtasdt0(smndt0(xS),smndt0(xS)) = sdtasdt0(xS,xS) ) ),
% 77.39/10.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 77.39/10.15 fof(f59,conjecture,(
% 77.39/10.15 sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))) = sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),smndt0(xN)),sdtpldt0(smndt0(xN),sdtasdt0(xS,xS))) ),
% 77.39/10.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 77.39/10.15 fof(f60,negated_conjecture,(
% 77.39/10.15 ~(sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))) = sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),smndt0(xN)),sdtpldt0(smndt0(xN),sdtasdt0(xS,xS))) )),
% 77.39/10.15 inference(negated_conjecture,[status(cth)],[f59])).
% 77.39/10.15 fof(f86,plain,(
% 77.39/10.15 ![W0]: (~aScalar0(W0)|aScalar0(smndt0(W0)))),
% 77.39/10.15 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 77.39/10.15 fof(f87,plain,(
% 77.39/10.15 ![X0]: (~aScalar0(X0)|aScalar0(smndt0(X0)))),
% 77.39/10.15 inference(cnf_transformation,[status(thm)],[f86])).
% 77.39/10.15 fof(f105,plain,(
% 77.39/10.15 ![W0,W1,W2,W3]: ((((~aScalar0(W0)|~aScalar0(W1))|~aScalar0(W2))|~aScalar0(W3))|sdtasdt0(sdtpldt0(W0,W1),sdtpldt0(W2,W3))=sdtpldt0(sdtpldt0(sdtasdt0(W0,W2),sdtasdt0(W0,W3)),sdtpldt0(sdtasdt0(W1,W2),sdtasdt0(W1,W3))))),
% 77.39/10.15 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 77.39/10.15 fof(f106,plain,(
% 77.39/10.15 ![X0,X1,X2,X3]: (~aScalar0(X0)|~aScalar0(X1)|~aScalar0(X2)|~aScalar0(X3)|sdtasdt0(sdtpldt0(X0,X1),sdtpldt0(X2,X3))=sdtpldt0(sdtpldt0(sdtasdt0(X0,X2),sdtasdt0(X0,X3)),sdtpldt0(sdtasdt0(X1,X2),sdtasdt0(X1,X3))))),
% 77.39/10.15 inference(cnf_transformation,[status(thm)],[f105])).
% 77.39/10.15 fof(f191,plain,(
% 77.39/10.15 aScalar0(xR)),
% 77.39/10.15 inference(cnf_transformation,[status(thm)],[f52])).
% 77.39/10.15 fof(f195,plain,(
% 77.39/10.15 aScalar0(xS)),
% 77.39/10.15 inference(cnf_transformation,[status(thm)],[f54])).
% 77.39/10.15 fof(f201,plain,(
% 77.39/10.15 sdtasdt0(xR,smndt0(xS))=smndt0(xN)),
% 77.39/10.15 inference(cnf_transformation,[status(thm)],[f58])).
% 77.39/10.15 fof(f202,plain,(
% 77.39/10.15 sdtasdt0(smndt0(xS),xR)=smndt0(xN)),
% 77.39/10.15 inference(cnf_transformation,[status(thm)],[f58])).
% 77.39/10.15 fof(f203,plain,(
% 77.39/10.15 sdtasdt0(smndt0(xS),smndt0(xS))=sdtasdt0(xS,xS)),
% 77.39/10.15 inference(cnf_transformation,[status(thm)],[f58])).
% 77.39/10.15 fof(f204,plain,(
% 77.39/10.15 ~sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS)))=sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),smndt0(xN)),sdtpldt0(smndt0(xN),sdtasdt0(xS,xS)))),
% 77.39/10.15 inference(cnf_transformation,[status(thm)],[f60])).
% 77.39/10.15 fof(f223,plain,(
% 77.39/10.15 ![X0,X1,X2]: (~aScalar0(X0)|~aScalar0(X1)|~aScalar0(X2)|sdtasdt0(sdtpldt0(X0,X1),sdtpldt0(xR,X2))=sdtpldt0(sdtpldt0(sdtasdt0(X0,xR),sdtasdt0(X0,X2)),sdtpldt0(sdtasdt0(X1,xR),sdtasdt0(X1,X2))))),
% 77.39/10.15 inference(resolution,[status(thm)],[f191,f106])).
% 77.39/10.15 fof(f637,plain,(
% 77.39/10.15 aScalar0(smndt0(xS))),
% 77.39/10.15 inference(resolution,[status(thm)],[f195,f87])).
% 77.39/10.15 fof(f1929,plain,(
% 77.39/10.15 ![X0]: (~aScalar0(X0)|sdtasdt0(sdtpldt0(X0,smndt0(xS)),sdtpldt0(xR,smndt0(xS)))=sdtpldt0(sdtpldt0(sdtasdt0(X0,xR),sdtasdt0(X0,smndt0(xS))),sdtpldt0(sdtasdt0(smndt0(xS),xR),sdtasdt0(smndt0(xS),smndt0(xS)))))),
% 77.39/10.15 inference(resolution,[status(thm)],[f637,f223])).
% 77.39/10.15 fof(f2050,plain,(
% 77.39/10.15 ![X0]: (~aScalar0(X0)|sdtasdt0(sdtpldt0(X0,smndt0(xS)),sdtpldt0(xR,smndt0(xS)))=sdtpldt0(sdtpldt0(sdtasdt0(X0,xR),sdtasdt0(X0,smndt0(xS))),sdtpldt0(smndt0(xN),sdtasdt0(smndt0(xS),smndt0(xS)))))),
% 77.39/10.15 inference(forward_demodulation,[status(thm)],[f202,f1929])).
% 77.39/10.15 fof(f2051,plain,(
% 77.39/10.15 ![X0]: (~aScalar0(X0)|sdtasdt0(sdtpldt0(X0,smndt0(xS)),sdtpldt0(xR,smndt0(xS)))=sdtpldt0(sdtpldt0(sdtasdt0(X0,xR),sdtasdt0(X0,smndt0(xS))),sdtpldt0(smndt0(xN),sdtasdt0(xS,xS))))),
% 77.39/10.21 inference(forward_demodulation,[status(thm)],[f203,f2050])).
% 77.39/10.21 fof(f26026,plain,(
% 77.39/10.21 sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS)))=sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xR,smndt0(xS))),sdtpldt0(smndt0(xN),sdtasdt0(xS,xS)))),
% 77.39/10.21 inference(resolution,[status(thm)],[f2051,f191])).
% 77.39/10.21 fof(f26040,plain,(
% 77.39/10.21 sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS)))=sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),smndt0(xN)),sdtpldt0(smndt0(xN),sdtasdt0(xS,xS)))),
% 77.39/10.21 inference(forward_demodulation,[status(thm)],[f201,f26026])).
% 77.39/10.21 fof(f26041,plain,(
% 77.39/10.21 $false),
% 77.39/10.21 inference(forward_subsumption_resolution,[status(thm)],[f26040,f204])).
% 77.39/10.21 % SZS output end CNFRefutation for theBenchmark.p
% 17.84/10.26 % Elapsed time: 9.888391 seconds
% 17.84/10.26 % CPU time: 78.101499 seconds
% 17.84/10.26 % Total memory used: 729.983 MB
% 17.84/10.26 % Net memory used: 676.793 MB
%------------------------------------------------------------------------------