%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : RNG065+2 : 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 : n017.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:16 PM UTC 2026
% Result : Theorem 9.78s 1.77s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : RNG065+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.43 % Computer : n017.cluster.edu
% 0.18/0.43 % Model : x86_64 x86_64
% 0.18/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.43 % Memory : 8046.5625MB
% 0.18/0.43 % OS : Linux 6.8.0-71-generic
% 0.18/0.43 % CPULimit : 300
% 0.18/0.43 % WCLimit : 300
% 0.18/0.43 % DateTime : Mon Sep 21 04:12:28 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.18/0.46 % Drodi V4.1.1
% 9.78/1.77 % Refutation found
% 9.78/1.77 % SZS status Theorem for theBenchmark: Theorem is valid
% 9.78/1.77 % SZS output start CNFRefutation for theBenchmark
% 9.78/1.77 fof(f10,axiom,(
% 9.78/1.77 (! [W0,W1] :( ( aScalar0(W0)& aScalar0(W1) )=> aScalar0(sdtpldt0(W0,W1)) ) )),
% 9.78/1.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.78/1.77 fof(f11,axiom,(
% 9.78/1.77 (! [W0,W1] :( ( aScalar0(W0)& aScalar0(W1) )=> aScalar0(sdtasdt0(W0,W1)) ) )),
% 9.78/1.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.78/1.77 fof(f22,axiom,(
% 9.78/1.77 (! [W0,W1,W2] :( ( aScalar0(W0)& aScalar0(W1)& aScalar0(W2) )=> ( ( sdtlseqdt0(W0,W1)& sdtlseqdt0(W1,W2) )=> sdtlseqdt0(W0,W2) ) ) )),
% 9.78/1.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.78/1.77 fof(f23,axiom,(
% 9.78/1.77 (! [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)) ) ) )),
% 9.78/1.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.78/1.77 fof(f52,hypothesis,(
% 9.78/1.77 ( aScalar0(xR)& xR = sdtasdt0(xC,xG) ) ),
% 9.78/1.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.78/1.78 fof(f53,hypothesis,(
% 9.78/1.78 ( aScalar0(xP)& xP = sdtasdt0(xE,xH) ) ),
% 9.78/1.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.78/1.78 fof(f54,hypothesis,(
% 9.78/1.78 ( aScalar0(xS)& xS = sdtasdt0(xF,xD) ) ),
% 9.78/1.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.78/1.78 fof(f55,hypothesis,(
% 9.78/1.78 ( aScalar0(xN)& xN = sdtasdt0(xR,xS) ) ),
% 9.78/1.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.78/1.78 fof(f57,hypothesis,(
% 9.78/1.78 sdtlseqdt0(sdtasdt0(xP,xP),xN) ),
% 9.78/1.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.78/1.78 fof(f64,hypothesis,(
% 9.78/1.78 sdtlseqdt0(sdtpldt0(xN,xN),sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS))) ),
% 9.78/1.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.78/1.78 fof(f65,conjecture,(
% 9.78/1.78 sdtlseqdt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS))) ),
% 9.78/1.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.78/1.78 fof(f66,negated_conjecture,(
% 9.78/1.78 ~(sdtlseqdt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS))) )),
% 9.78/1.78 inference(negated_conjecture,[status(cth)],[f65])).
% 9.78/1.78 fof(f88,plain,(
% 9.78/1.78 ![W0,W1]: ((~aScalar0(W0)|~aScalar0(W1))|aScalar0(sdtpldt0(W0,W1)))),
% 9.78/1.78 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 9.78/1.78 fof(f89,plain,(
% 9.78/1.78 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|aScalar0(sdtpldt0(X0,X1)))),
% 9.78/1.78 inference(cnf_transformation,[status(thm)],[f88])).
% 9.78/1.78 fof(f90,plain,(
% 9.78/1.78 ![W0,W1]: ((~aScalar0(W0)|~aScalar0(W1))|aScalar0(sdtasdt0(W0,W1)))),
% 9.78/1.78 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 9.78/1.78 fof(f91,plain,(
% 9.78/1.78 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|aScalar0(sdtasdt0(X0,X1)))),
% 9.78/1.78 inference(cnf_transformation,[status(thm)],[f90])).
% 9.78/1.78 fof(f124,plain,(
% 9.78/1.78 ![W0,W1,W2]: (((~aScalar0(W0)|~aScalar0(W1))|~aScalar0(W2))|((~sdtlseqdt0(W0,W1)|~sdtlseqdt0(W1,W2))|sdtlseqdt0(W0,W2)))),
% 9.78/1.78 inference(pre_NNF_transformation,[status(thm)],[f22])).
% 9.78/1.78 fof(f125,plain,(
% 9.78/1.78 ![X0,X1,X2]: (~aScalar0(X0)|~aScalar0(X1)|~aScalar0(X2)|~sdtlseqdt0(X0,X1)|~sdtlseqdt0(X1,X2)|sdtlseqdt0(X0,X2))),
% 9.78/1.78 inference(cnf_transformation,[status(thm)],[f124])).
% 9.78/1.78 fof(f126,plain,(
% 9.78/1.78 ![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))))),
% 9.78/1.78 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 9.78/1.78 fof(f127,plain,(
% 9.78/1.78 ![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)))),
% 9.78/1.78 inference(cnf_transformation,[status(thm)],[f126])).
% 9.78/1.78 fof(f197,plain,(
% 9.78/1.78 aScalar0(xR)),
% 9.78/1.78 inference(cnf_transformation,[status(thm)],[f52])).
% 9.78/1.78 fof(f199,plain,(
% 9.78/1.78 aScalar0(xP)),
% 9.78/1.78 inference(cnf_transformation,[status(thm)],[f53])).
% 9.78/1.78 fof(f201,plain,(
% 9.78/1.78 aScalar0(xS)),
% 9.78/1.78 inference(cnf_transformation,[status(thm)],[f54])).
% 9.78/1.78 fof(f203,plain,(
% 9.78/1.78 aScalar0(xN)),
% 9.78/1.78 inference(cnf_transformation,[status(thm)],[f55])).
% 9.78/1.78 fof(f206,plain,(
% 9.78/1.78 sdtlseqdt0(sdtasdt0(xP,xP),xN)),
% 9.78/1.78 inference(cnf_transformation,[status(thm)],[f57])).
% 9.78/1.78 fof(f215,plain,(
% 9.78/1.78 sdtlseqdt0(sdtpldt0(xN,xN),sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))),
% 9.78/1.78 inference(cnf_transformation,[status(thm)],[f64])).
% 9.78/1.78 fof(f216,plain,(
% 9.78/1.78 ~sdtlseqdt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))),
% 9.78/1.78 inference(cnf_transformation,[status(thm)],[f66])).
% 9.78/1.78 fof(f378,plain,(
% 9.78/1.78 ![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))))),
% 9.78/1.78 inference(resolution,[status(thm)],[f125,f216])).
% 9.78/1.78 fof(f429,plain,(
% 9.78/1.78 ![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)))),
% 9.78/1.78 inference(resolution,[status(thm)],[f378,f89])).
% 9.78/1.78 fof(f430,plain,(
% 9.78/1.78 ![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)))),
% 9.78/1.78 inference(duplicate_literals_removal,[status(thm)],[f429])).
% 9.78/1.78 fof(f719,plain,(
% 9.78/1.78 ![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))),
% 9.78/1.78 inference(resolution,[status(thm)],[f430,f91])).
% 9.78/1.78 fof(f720,plain,(
% 9.78/1.78 ![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))),
% 9.78/1.78 inference(duplicate_literals_removal,[status(thm)],[f719])).
% 9.78/1.78 fof(f721,plain,(
% 9.78/1.78 ![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))))),
% 9.78/1.78 inference(forward_subsumption_resolution,[status(thm)],[f720,f199])).
% 9.78/1.78 fof(f722,plain,(
% 9.78/1.78 ![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)))),
% 9.78/1.78 inference(resolution,[status(thm)],[f721,f89])).
% 9.78/1.78 fof(f1102,plain,(
% 9.78/1.78 ![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))),
% 9.78/1.78 inference(resolution,[status(thm)],[f722,f91])).
% 9.78/1.78 fof(f1103,plain,(
% 9.78/1.78 ![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))),
% 9.78/1.78 inference(duplicate_literals_removal,[status(thm)],[f1102])).
% 9.78/1.78 fof(f1104,plain,(
% 9.78/1.78 ![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)))),
% 9.78/1.78 inference(forward_subsumption_resolution,[status(thm)],[f1103,f201])).
% 9.78/1.78 fof(f1487,plain,(
% 9.78/1.78 ![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))),
% 9.78/1.78 inference(resolution,[status(thm)],[f1104,f91])).
% 9.78/1.78 fof(f1488,plain,(
% 9.78/1.78 ![X0]: (~aScalar0(X0)|~sdtlseqdt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),X0)|~sdtlseqdt0(X0,sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~aScalar0(xR))),
% 9.78/1.78 inference(duplicate_literals_removal,[status(thm)],[f1487])).
% 9.78/1.78 fof(f1489,plain,(
% 9.78/1.78 ![X0]: (~aScalar0(X0)|~sdtlseqdt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),X0)|~sdtlseqdt0(X0,sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS))))),
% 9.78/1.78 inference(forward_subsumption_resolution,[status(thm)],[f1488,f197])).
% 9.78/1.78 fof(f1717,plain,(
% 9.78/1.78 ![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))),
% 9.78/1.78 inference(resolution,[status(thm)],[f1489,f127])).
% 9.78/1.80 fof(f1720,plain,(
% 9.78/1.80 ![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))),
% 9.78/1.80 inference(duplicate_literals_removal,[status(thm)],[f1717])).
% 9.78/1.80 fof(f1721,plain,(
% 9.78/1.80 ![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))),
% 9.78/1.80 inference(forward_subsumption_resolution,[status(thm)],[f1720,f89])).
% 9.78/1.80 fof(f2016,plain,(
% 9.78/1.80 ![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))),
% 9.78/1.80 inference(resolution,[status(thm)],[f1721,f91])).
% 9.78/1.80 fof(f2017,plain,(
% 9.78/1.80 ![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))),
% 9.78/1.80 inference(duplicate_literals_removal,[status(thm)],[f2016])).
% 9.78/1.80 fof(f2018,plain,(
% 9.78/1.80 ![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))),
% 9.78/1.80 inference(forward_subsumption_resolution,[status(thm)],[f2017,f199])).
% 9.78/1.80 fof(f2210,plain,(
% 9.78/1.80 ![X0]: (~sdtlseqdt0(sdtpldt0(X0,xN),sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~aScalar0(X0)|~aScalar0(xN)|~sdtlseqdt0(sdtasdt0(xP,xP),X0))),
% 9.78/1.80 inference(resolution,[status(thm)],[f2018,f206])).
% 9.78/1.80 fof(f2213,plain,(
% 9.78/1.80 ![X0]: (~sdtlseqdt0(sdtpldt0(X0,xN),sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~aScalar0(X0)|~sdtlseqdt0(sdtasdt0(xP,xP),X0))),
% 9.78/1.80 inference(forward_subsumption_resolution,[status(thm)],[f2210,f203])).
% 9.78/1.80 fof(f3756,plain,(
% 9.78/1.80 ~aScalar0(xN)|~sdtlseqdt0(sdtasdt0(xP,xP),xN)),
% 9.78/1.80 inference(resolution,[status(thm)],[f215,f2213])).
% 9.78/1.80 fof(f3759,plain,(
% 9.78/1.80 ~sdtlseqdt0(sdtasdt0(xP,xP),xN)),
% 9.78/1.80 inference(forward_subsumption_resolution,[status(thm)],[f3756,f203])).
% 9.78/1.80 fof(f3818,plain,(
% 9.78/1.80 $false),
% 9.78/1.80 inference(forward_subsumption_resolution,[status(thm)],[f3759,f206])).
% 9.78/1.80 % SZS output end CNFRefutation for theBenchmark.p
% 9.78/1.81 % Elapsed time: 1.357778 seconds
% 9.78/1.81 % CPU time: 10.362032 seconds
% 9.78/1.81 % Total memory used: 196.254 MB
% 9.78/1.81 % Net memory used: 190.021 MB
%------------------------------------------------------------------------------