%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : RNG060+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 : n007.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 93.05s 12.15s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : RNG060+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.34 % Computer : n007.cluster.edu
% 0.09/0.34 % Model : x86_64 x86_64
% 0.09/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.34 % Memory : 8046.5625MB
% 0.09/0.34 % OS : Linux 6.8.0-71-generic
% 0.09/0.34 % CPULimit : 300
% 0.09/0.34 % WCLimit : 300
% 0.09/0.34 % DateTime : Mon Sep 21 04:14:35 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.36 % Drodi V4.1.1
% 93.05/12.15 % Refutation found
% 93.05/12.15 % SZS status Theorem for theBenchmark: Theorem is valid
% 93.05/12.15 % SZS output start CNFRefutation for theBenchmark
% 93.05/12.15 fof(f12,axiom,(
% 93.05/12.15 (! [W0] :( aScalar0(W0)=> aScalar0(smndt0(W0)) ) )),
% 93.05/12.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 93.05/12.15 fof(f16,axiom,(
% 93.05/12.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))) ) )),
% 93.05/12.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 93.05/12.15 fof(f52,hypothesis,(
% 93.05/12.15 ( aScalar0(xR)& xR = sdtasdt0(xC,xG) ) ),
% 93.05/12.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 93.05/12.15 fof(f54,hypothesis,(
% 93.05/12.15 ( aScalar0(xS)& xS = sdtasdt0(xF,xD) ) ),
% 93.05/12.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 93.05/12.15 fof(f58,hypothesis,(
% 93.05/12.15 ( sdtasdt0(xR,smndt0(xS)) = smndt0(xN)& sdtasdt0(smndt0(xS),xR) = smndt0(xN)& sdtasdt0(smndt0(xS),smndt0(xS)) = sdtasdt0(xS,xS) ) ),
% 93.05/12.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 93.05/12.15 fof(f59,conjecture,(
% 93.05/12.15 sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))) = sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),smndt0(xN)),sdtpldt0(smndt0(xN),sdtasdt0(xS,xS))) ),
% 93.05/12.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 93.05/12.15 fof(f60,negated_conjecture,(
% 93.05/12.15 ~(sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))) = sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),smndt0(xN)),sdtpldt0(smndt0(xN),sdtasdt0(xS,xS))) )),
% 93.05/12.15 inference(negated_conjecture,[status(cth)],[f59])).
% 93.05/12.15 fof(f86,plain,(
% 93.05/12.15 ![W0]: (~aScalar0(W0)|aScalar0(smndt0(W0)))),
% 93.05/12.15 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 93.05/12.15 fof(f87,plain,(
% 93.05/12.15 ![X0]: (~aScalar0(X0)|aScalar0(smndt0(X0)))),
% 93.05/12.15 inference(cnf_transformation,[status(thm)],[f86])).
% 93.05/12.15 fof(f105,plain,(
% 93.05/12.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))))),
% 93.05/12.15 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 93.05/12.15 fof(f106,plain,(
% 93.05/12.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))))),
% 93.05/12.15 inference(cnf_transformation,[status(thm)],[f105])).
% 93.05/12.15 fof(f185,plain,(
% 93.05/12.15 aScalar0(xR)),
% 93.05/12.15 inference(cnf_transformation,[status(thm)],[f52])).
% 93.05/12.15 fof(f189,plain,(
% 93.05/12.15 aScalar0(xS)),
% 93.05/12.15 inference(cnf_transformation,[status(thm)],[f54])).
% 93.05/12.15 fof(f195,plain,(
% 93.05/12.15 sdtasdt0(xR,smndt0(xS))=smndt0(xN)),
% 93.05/12.15 inference(cnf_transformation,[status(thm)],[f58])).
% 93.05/12.15 fof(f196,plain,(
% 93.05/12.15 sdtasdt0(smndt0(xS),xR)=smndt0(xN)),
% 93.05/12.15 inference(cnf_transformation,[status(thm)],[f58])).
% 93.05/12.15 fof(f197,plain,(
% 93.05/12.15 sdtasdt0(smndt0(xS),smndt0(xS))=sdtasdt0(xS,xS)),
% 93.05/12.15 inference(cnf_transformation,[status(thm)],[f58])).
% 93.05/12.15 fof(f198,plain,(
% 93.05/12.15 ~sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS)))=sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),smndt0(xN)),sdtpldt0(smndt0(xN),sdtasdt0(xS,xS)))),
% 93.05/12.15 inference(cnf_transformation,[status(thm)],[f60])).
% 93.05/12.15 fof(f217,plain,(
% 93.05/12.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))))),
% 93.05/12.15 inference(resolution,[status(thm)],[f185,f106])).
% 93.05/12.15 fof(f631,plain,(
% 93.05/12.15 aScalar0(smndt0(xS))),
% 93.05/12.15 inference(resolution,[status(thm)],[f189,f87])).
% 93.05/12.15 fof(f1923,plain,(
% 93.05/12.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)))))),
% 93.05/12.15 inference(resolution,[status(thm)],[f631,f217])).
% 93.05/12.15 fof(f2044,plain,(
% 93.05/12.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)))))),
% 93.05/12.15 inference(forward_demodulation,[status(thm)],[f196,f1923])).
% 93.05/12.15 fof(f2045,plain,(
% 93.05/12.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))))),
% 93.05/12.22 inference(forward_demodulation,[status(thm)],[f197,f2044])).
% 93.05/12.22 fof(f26480,plain,(
% 93.05/12.22 sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS)))=sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xR,smndt0(xS))),sdtpldt0(smndt0(xN),sdtasdt0(xS,xS)))),
% 93.05/12.22 inference(resolution,[status(thm)],[f2045,f185])).
% 93.05/12.22 fof(f26494,plain,(
% 93.05/12.22 sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS)))=sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),smndt0(xN)),sdtpldt0(smndt0(xN),sdtasdt0(xS,xS)))),
% 93.05/12.22 inference(forward_demodulation,[status(thm)],[f195,f26480])).
% 93.05/12.22 fof(f26495,plain,(
% 93.05/12.22 $false),
% 93.05/12.22 inference(forward_subsumption_resolution,[status(thm)],[f26494,f198])).
% 93.05/12.22 % SZS output end CNFRefutation for theBenchmark.p
% 8.94/12.27 % Elapsed time: 11.900150 seconds
% 8.94/12.27 % CPU time: 94.141089 seconds
% 8.94/12.27 % Total memory used: 873.929 MB
% 8.94/12.27 % Net memory used: 807.017 MB
%------------------------------------------------------------------------------