%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : RNG065+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 : n026.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 6.26s 1.24s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG065+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.11/0.36 % Computer : n026.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.12/0.36 % CPULimit : 300
% 0.12/0.36 % WCLimit : 300
% 0.12/0.36 % DateTime : Mon Sep 21 04:19:51 UTC 2026
% 0.12/0.36 % CPUTime :
% 0.12/0.38 % Drodi V4.1.1
% 6.26/1.24 % Refutation found
% 6.26/1.24 % SZS status Theorem for theBenchmark: Theorem is valid
% 6.26/1.24 % SZS output start CNFRefutation for theBenchmark
% 6.26/1.24 fof(f10,axiom,(
% 6.26/1.24 (! [W0,W1] :( ( aScalar0(W0)& aScalar0(W1) )=> aScalar0(sdtpldt0(W0,W1)) ) )),
% 6.26/1.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.26/1.24 fof(f11,axiom,(
% 6.26/1.24 (! [W0,W1] :( ( aScalar0(W0)& aScalar0(W1) )=> aScalar0(sdtasdt0(W0,W1)) ) )),
% 6.26/1.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.26/1.24 fof(f22,axiom,(
% 6.26/1.24 (! [W0,W1,W2] :( ( aScalar0(W0)& aScalar0(W1)& aScalar0(W2) )=> ( ( sdtlseqdt0(W0,W1)& sdtlseqdt0(W1,W2) )=> sdtlseqdt0(W0,W2) ) ) )),
% 6.26/1.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.26/1.24 fof(f23,axiom,(
% 6.26/1.24 (! [W0,W1,W2,W3] :( ( aScalar0(W0)& aScalar0(W1)& aScalar0(W2)& aScalar0(W3) )=> ( ( sdtlseqdt0(W0,W1)& sdtlseqdt0(W2,W3) )=> sdtlseqdt0(sdtpldt0(W0,W2),sdtpldt0(W1,W3)) ) ) )),
% 6.26/1.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.26/1.24 fof(f52,hypothesis,(
% 6.26/1.24 ( aScalar0(xR)& xR = sdtasdt0(xC,xG) ) ),
% 6.26/1.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.26/1.24 fof(f53,hypothesis,(
% 6.26/1.24 ( aScalar0(xP)& xP = sdtasdt0(xE,xH) ) ),
% 6.26/1.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.26/1.24 fof(f54,hypothesis,(
% 6.26/1.24 ( aScalar0(xS)& xS = sdtasdt0(xF,xD) ) ),
% 6.26/1.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.26/1.24 fof(f55,hypothesis,(
% 6.26/1.24 ( aScalar0(xN)& xN = sdtasdt0(xR,xS) ) ),
% 6.26/1.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.26/1.24 fof(f57,hypothesis,(
% 6.26/1.24 sdtlseqdt0(sdtasdt0(xP,xP),xN) ),
% 6.26/1.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.26/1.24 fof(f64,hypothesis,(
% 6.26/1.24 sdtlseqdt0(sdtpldt0(xN,xN),sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS))) ),
% 6.26/1.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.26/1.24 fof(f65,conjecture,(
% 6.26/1.24 sdtlseqdt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS))) ),
% 6.26/1.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.26/1.24 fof(f66,negated_conjecture,(
% 6.26/1.24 ~(sdtlseqdt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS))) )),
% 6.26/1.24 inference(negated_conjecture,[status(cth)],[f65])).
% 6.26/1.24 fof(f88,plain,(
% 6.26/1.24 ![W0,W1]: ((~aScalar0(W0)|~aScalar0(W1))|aScalar0(sdtpldt0(W0,W1)))),
% 6.26/1.24 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 6.26/1.24 fof(f89,plain,(
% 6.26/1.24 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|aScalar0(sdtpldt0(X0,X1)))),
% 6.26/1.24 inference(cnf_transformation,[status(thm)],[f88])).
% 6.26/1.24 fof(f90,plain,(
% 6.26/1.24 ![W0,W1]: ((~aScalar0(W0)|~aScalar0(W1))|aScalar0(sdtasdt0(W0,W1)))),
% 6.26/1.24 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 6.26/1.24 fof(f91,plain,(
% 6.26/1.24 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|aScalar0(sdtasdt0(X0,X1)))),
% 6.26/1.24 inference(cnf_transformation,[status(thm)],[f90])).
% 6.26/1.24 fof(f124,plain,(
% 6.26/1.24 ![W0,W1,W2]: (((~aScalar0(W0)|~aScalar0(W1))|~aScalar0(W2))|((~sdtlseqdt0(W0,W1)|~sdtlseqdt0(W1,W2))|sdtlseqdt0(W0,W2)))),
% 6.26/1.24 inference(pre_NNF_transformation,[status(thm)],[f22])).
% 6.26/1.24 fof(f125,plain,(
% 6.26/1.24 ![X0,X1,X2]: (~aScalar0(X0)|~aScalar0(X1)|~aScalar0(X2)|~sdtlseqdt0(X0,X1)|~sdtlseqdt0(X1,X2)|sdtlseqdt0(X0,X2))),
% 6.26/1.24 inference(cnf_transformation,[status(thm)],[f124])).
% 6.26/1.24 fof(f126,plain,(
% 6.26/1.24 ![W0,W1,W2,W3]: ((((~aScalar0(W0)|~aScalar0(W1))|~aScalar0(W2))|~aScalar0(W3))|((~sdtlseqdt0(W0,W1)|~sdtlseqdt0(W2,W3))|sdtlseqdt0(sdtpldt0(W0,W2),sdtpldt0(W1,W3))))),
% 6.26/1.24 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 6.26/1.24 fof(f127,plain,(
% 6.26/1.24 ![X0,X1,X2,X3]: (~aScalar0(X0)|~aScalar0(X1)|~aScalar0(X2)|~aScalar0(X3)|~sdtlseqdt0(X0,X1)|~sdtlseqdt0(X2,X3)|sdtlseqdt0(sdtpldt0(X0,X2),sdtpldt0(X1,X3)))),
% 6.26/1.24 inference(cnf_transformation,[status(thm)],[f126])).
% 6.26/1.24 fof(f191,plain,(
% 6.26/1.24 aScalar0(xR)),
% 6.26/1.24 inference(cnf_transformation,[status(thm)],[f52])).
% 6.26/1.24 fof(f193,plain,(
% 6.26/1.24 aScalar0(xP)),
% 6.26/1.24 inference(cnf_transformation,[status(thm)],[f53])).
% 6.26/1.24 fof(f195,plain,(
% 6.26/1.24 aScalar0(xS)),
% 6.26/1.24 inference(cnf_transformation,[status(thm)],[f54])).
% 6.26/1.24 fof(f197,plain,(
% 6.26/1.24 aScalar0(xN)),
% 6.26/1.24 inference(cnf_transformation,[status(thm)],[f55])).
% 6.26/1.24 fof(f200,plain,(
% 6.26/1.24 sdtlseqdt0(sdtasdt0(xP,xP),xN)),
% 6.26/1.24 inference(cnf_transformation,[status(thm)],[f57])).
% 6.26/1.24 fof(f209,plain,(
% 6.26/1.24 sdtlseqdt0(sdtpldt0(xN,xN),sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))),
% 6.26/1.24 inference(cnf_transformation,[status(thm)],[f64])).
% 6.26/1.24 fof(f210,plain,(
% 6.26/1.24 ~sdtlseqdt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))),
% 6.26/1.24 inference(cnf_transformation,[status(thm)],[f66])).
% 6.26/1.24 fof(f372,plain,(
% 6.26/1.24 ![X0]: (~aScalar0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)))|~aScalar0(X0)|~aScalar0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~sdtlseqdt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),X0)|~sdtlseqdt0(X0,sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS))))),
% 6.26/1.24 inference(resolution,[status(thm)],[f125,f210])).
% 6.26/1.24 fof(f423,plain,(
% 6.26/1.24 ![X0]: (~aScalar0(X0)|~aScalar0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~sdtlseqdt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),X0)|~sdtlseqdt0(X0,sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~aScalar0(sdtasdt0(xP,xP))|~aScalar0(sdtasdt0(xP,xP)))),
% 6.26/1.24 inference(resolution,[status(thm)],[f372,f89])).
% 6.26/1.24 fof(f424,plain,(
% 6.26/1.24 ![X0]: (~aScalar0(X0)|~aScalar0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~sdtlseqdt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),X0)|~sdtlseqdt0(X0,sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~aScalar0(sdtasdt0(xP,xP)))),
% 6.26/1.24 inference(duplicate_literals_removal,[status(thm)],[f423])).
% 6.26/1.24 fof(f713,plain,(
% 6.26/1.24 ![X0]: (~aScalar0(X0)|~aScalar0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~sdtlseqdt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),X0)|~sdtlseqdt0(X0,sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~aScalar0(xP)|~aScalar0(xP))),
% 6.26/1.24 inference(resolution,[status(thm)],[f424,f91])).
% 6.26/1.24 fof(f714,plain,(
% 6.26/1.24 ![X0]: (~aScalar0(X0)|~aScalar0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~sdtlseqdt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),X0)|~sdtlseqdt0(X0,sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~aScalar0(xP))),
% 6.26/1.24 inference(duplicate_literals_removal,[status(thm)],[f713])).
% 6.26/1.24 fof(f715,plain,(
% 6.26/1.24 ![X0]: (~aScalar0(X0)|~aScalar0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~sdtlseqdt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),X0)|~sdtlseqdt0(X0,sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS))))),
% 6.26/1.24 inference(forward_subsumption_resolution,[status(thm)],[f714,f193])).
% 6.26/1.24 fof(f716,plain,(
% 6.26/1.24 ![X0]: (~aScalar0(X0)|~sdtlseqdt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),X0)|~sdtlseqdt0(X0,sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~aScalar0(sdtasdt0(xR,xR))|~aScalar0(sdtasdt0(xS,xS)))),
% 6.26/1.24 inference(resolution,[status(thm)],[f715,f89])).
% 6.26/1.24 fof(f1096,plain,(
% 6.26/1.24 ![X0]: (~aScalar0(X0)|~sdtlseqdt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),X0)|~sdtlseqdt0(X0,sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~aScalar0(sdtasdt0(xR,xR))|~aScalar0(xS)|~aScalar0(xS))),
% 6.26/1.24 inference(resolution,[status(thm)],[f716,f91])).
% 6.26/1.24 fof(f1097,plain,(
% 6.26/1.24 ![X0]: (~aScalar0(X0)|~sdtlseqdt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),X0)|~sdtlseqdt0(X0,sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~aScalar0(sdtasdt0(xR,xR))|~aScalar0(xS))),
% 6.26/1.24 inference(duplicate_literals_removal,[status(thm)],[f1096])).
% 6.26/1.24 fof(f1098,plain,(
% 6.26/1.24 ![X0]: (~aScalar0(X0)|~sdtlseqdt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),X0)|~sdtlseqdt0(X0,sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~aScalar0(sdtasdt0(xR,xR)))),
% 6.26/1.24 inference(forward_subsumption_resolution,[status(thm)],[f1097,f195])).
% 6.26/1.24 fof(f1481,plain,(
% 6.26/1.24 ![X0]: (~aScalar0(X0)|~sdtlseqdt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),X0)|~sdtlseqdt0(X0,sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~aScalar0(xR)|~aScalar0(xR))),
% 6.26/1.24 inference(resolution,[status(thm)],[f1098,f91])).
% 6.26/1.24 fof(f1482,plain,(
% 6.26/1.24 ![X0]: (~aScalar0(X0)|~sdtlseqdt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),X0)|~sdtlseqdt0(X0,sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~aScalar0(xR))),
% 6.26/1.24 inference(duplicate_literals_removal,[status(thm)],[f1481])).
% 6.26/1.24 fof(f1483,plain,(
% 6.26/1.24 ![X0]: (~aScalar0(X0)|~sdtlseqdt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),X0)|~sdtlseqdt0(X0,sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS))))),
% 6.26/1.24 inference(forward_subsumption_resolution,[status(thm)],[f1482,f191])).
% 6.26/1.24 fof(f1711,plain,(
% 6.26/1.24 ![X0,X1]: (~aScalar0(sdtpldt0(X0,X1))|~sdtlseqdt0(sdtpldt0(X0,X1),sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~aScalar0(sdtasdt0(xP,xP))|~aScalar0(X0)|~aScalar0(sdtasdt0(xP,xP))|~aScalar0(X1)|~sdtlseqdt0(sdtasdt0(xP,xP),X0)|~sdtlseqdt0(sdtasdt0(xP,xP),X1))),
% 6.26/1.24 inference(resolution,[status(thm)],[f1483,f127])).
% 6.26/1.25 fof(f1714,plain,(
% 6.26/1.25 ![X0,X1]: (~aScalar0(sdtpldt0(X0,X1))|~sdtlseqdt0(sdtpldt0(X0,X1),sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~aScalar0(sdtasdt0(xP,xP))|~aScalar0(X0)|~aScalar0(X1)|~sdtlseqdt0(sdtasdt0(xP,xP),X0)|~sdtlseqdt0(sdtasdt0(xP,xP),X1))),
% 6.26/1.25 inference(duplicate_literals_removal,[status(thm)],[f1711])).
% 6.26/1.25 fof(f1715,plain,(
% 6.26/1.25 ![X0,X1]: (~sdtlseqdt0(sdtpldt0(X0,X1),sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~aScalar0(sdtasdt0(xP,xP))|~aScalar0(X0)|~aScalar0(X1)|~sdtlseqdt0(sdtasdt0(xP,xP),X0)|~sdtlseqdt0(sdtasdt0(xP,xP),X1))),
% 6.26/1.25 inference(forward_subsumption_resolution,[status(thm)],[f1714,f89])).
% 6.26/1.25 fof(f1994,plain,(
% 6.26/1.25 ![X0,X1]: (~sdtlseqdt0(sdtpldt0(X0,X1),sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~aScalar0(X0)|~aScalar0(X1)|~sdtlseqdt0(sdtasdt0(xP,xP),X0)|~sdtlseqdt0(sdtasdt0(xP,xP),X1)|~aScalar0(xP)|~aScalar0(xP))),
% 6.26/1.25 inference(resolution,[status(thm)],[f1715,f91])).
% 6.26/1.25 fof(f1995,plain,(
% 6.26/1.25 ![X0,X1]: (~sdtlseqdt0(sdtpldt0(X0,X1),sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~aScalar0(X0)|~aScalar0(X1)|~sdtlseqdt0(sdtasdt0(xP,xP),X0)|~sdtlseqdt0(sdtasdt0(xP,xP),X1)|~aScalar0(xP))),
% 6.26/1.25 inference(duplicate_literals_removal,[status(thm)],[f1994])).
% 6.26/1.25 fof(f1996,plain,(
% 6.26/1.25 ![X0,X1]: (~sdtlseqdt0(sdtpldt0(X0,X1),sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~aScalar0(X0)|~aScalar0(X1)|~sdtlseqdt0(sdtasdt0(xP,xP),X0)|~sdtlseqdt0(sdtasdt0(xP,xP),X1))),
% 6.26/1.25 inference(forward_subsumption_resolution,[status(thm)],[f1995,f193])).
% 6.26/1.25 fof(f2191,plain,(
% 6.26/1.25 ![X0]: (~sdtlseqdt0(sdtpldt0(X0,xN),sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~aScalar0(X0)|~aScalar0(xN)|~sdtlseqdt0(sdtasdt0(xP,xP),X0))),
% 6.26/1.25 inference(resolution,[status(thm)],[f1996,f200])).
% 6.26/1.25 fof(f2194,plain,(
% 6.26/1.25 ![X0]: (~sdtlseqdt0(sdtpldt0(X0,xN),sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~aScalar0(X0)|~sdtlseqdt0(sdtasdt0(xP,xP),X0))),
% 6.26/1.25 inference(forward_subsumption_resolution,[status(thm)],[f2191,f197])).
% 6.26/1.25 fof(f3144,plain,(
% 6.26/1.25 ~aScalar0(xN)|~sdtlseqdt0(sdtasdt0(xP,xP),xN)),
% 6.26/1.25 inference(resolution,[status(thm)],[f209,f2194])).
% 6.26/1.25 fof(f3147,plain,(
% 6.26/1.25 ~sdtlseqdt0(sdtasdt0(xP,xP),xN)),
% 6.26/1.25 inference(forward_subsumption_resolution,[status(thm)],[f3144,f197])).
% 6.26/1.25 fof(f3199,plain,(
% 6.26/1.25 $false),
% 6.26/1.25 inference(forward_subsumption_resolution,[status(thm)],[f3147,f200])).
% 6.26/1.25 % SZS output end CNFRefutation for theBenchmark.p
% 6.26/1.26 % Elapsed time: 0.893277 seconds
% 6.26/1.26 % CPU time: 6.688792 seconds
% 6.26/1.26 % Total memory used: 175.845 MB
% 6.26/1.26 % Net memory used: 171.206 MB
%------------------------------------------------------------------------------