%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : RNG067+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 : n016.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 46.81s 6.32s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG067+2 : 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.35 % Computer : n016.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 04:21:37 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 46.81/6.32 % Refutation found
% 46.81/6.32 % SZS status Theorem for theBenchmark: Theorem is valid
% 46.81/6.32 % SZS output start CNFRefutation for theBenchmark
% 46.81/6.32 fof(f10,axiom,(
% 46.81/6.32 (! [W0,W1] :( ( aScalar0(W0)& aScalar0(W1) )=> aScalar0(sdtpldt0(W0,W1)) ) )),
% 46.81/6.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 46.81/6.32 fof(f11,axiom,(
% 46.81/6.32 (! [W0,W1] :( ( aScalar0(W0)& aScalar0(W1) )=> aScalar0(sdtasdt0(W0,W1)) ) )),
% 46.81/6.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 46.81/6.32 fof(f23,axiom,(
% 46.81/6.32 (! [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)) ) ) )),
% 46.81/6.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 46.81/6.32 fof(f52,hypothesis,(
% 46.81/6.32 ( aScalar0(xR)& xR = sdtasdt0(xC,xG) ) ),
% 46.81/6.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 46.81/6.32 fof(f53,hypothesis,(
% 46.81/6.32 ( aScalar0(xP)& xP = sdtasdt0(xE,xH) ) ),
% 46.81/6.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 46.81/6.32 fof(f54,hypothesis,(
% 46.81/6.32 ( aScalar0(xS)& xS = sdtasdt0(xF,xD) ) ),
% 46.81/6.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 46.81/6.32 fof(f55,hypothesis,(
% 46.81/6.32 ( aScalar0(xN)& xN = sdtasdt0(xR,xS) ) ),
% 46.81/6.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 46.81/6.32 fof(f57,hypothesis,(
% 46.81/6.32 sdtlseqdt0(sdtasdt0(xP,xP),xN) ),
% 46.81/6.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 46.81/6.32 fof(f58,hypothesis,(
% 46.81/6.32 sdtlseqdt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS))) ),
% 46.81/6.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 46.81/6.32 fof(f59,conjecture,(
% 46.81/6.32 sdtlseqdt0(sdtpldt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtpldt0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN),xN)) ),
% 46.81/6.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 46.81/6.32 fof(f60,negated_conjecture,(
% 46.81/6.32 ~(sdtlseqdt0(sdtpldt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtpldt0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN),xN)) )),
% 46.81/6.32 inference(negated_conjecture,[status(cth)],[f59])).
% 46.81/6.32 fof(f82,plain,(
% 46.81/6.32 ![W0,W1]: ((~aScalar0(W0)|~aScalar0(W1))|aScalar0(sdtpldt0(W0,W1)))),
% 46.81/6.32 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 46.81/6.32 fof(f83,plain,(
% 46.81/6.32 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|aScalar0(sdtpldt0(X0,X1)))),
% 46.81/6.32 inference(cnf_transformation,[status(thm)],[f82])).
% 46.81/6.32 fof(f84,plain,(
% 46.81/6.32 ![W0,W1]: ((~aScalar0(W0)|~aScalar0(W1))|aScalar0(sdtasdt0(W0,W1)))),
% 46.81/6.32 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 46.81/6.32 fof(f85,plain,(
% 46.81/6.32 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|aScalar0(sdtasdt0(X0,X1)))),
% 46.81/6.32 inference(cnf_transformation,[status(thm)],[f84])).
% 46.81/6.32 fof(f120,plain,(
% 46.81/6.32 ![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))))),
% 46.81/6.32 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 46.81/6.32 fof(f121,plain,(
% 46.81/6.32 ![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)))),
% 46.81/6.32 inference(cnf_transformation,[status(thm)],[f120])).
% 46.81/6.32 fof(f191,plain,(
% 46.81/6.32 aScalar0(xR)),
% 46.81/6.32 inference(cnf_transformation,[status(thm)],[f52])).
% 46.81/6.32 fof(f193,plain,(
% 46.81/6.32 aScalar0(xP)),
% 46.81/6.32 inference(cnf_transformation,[status(thm)],[f53])).
% 46.81/6.32 fof(f195,plain,(
% 46.81/6.32 aScalar0(xS)),
% 46.81/6.32 inference(cnf_transformation,[status(thm)],[f54])).
% 46.81/6.32 fof(f197,plain,(
% 46.81/6.32 aScalar0(xN)),
% 46.81/6.32 inference(cnf_transformation,[status(thm)],[f55])).
% 46.81/6.32 fof(f200,plain,(
% 46.81/6.32 sdtlseqdt0(sdtasdt0(xP,xP),xN)),
% 46.81/6.32 inference(cnf_transformation,[status(thm)],[f57])).
% 46.81/6.32 fof(f201,plain,(
% 46.81/6.32 sdtlseqdt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))),
% 46.81/6.32 inference(cnf_transformation,[status(thm)],[f58])).
% 46.81/6.32 fof(f202,plain,(
% 46.81/6.32 ~sdtlseqdt0(sdtpldt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtpldt0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN),xN))),
% 46.81/6.32 inference(cnf_transformation,[status(thm)],[f60])).
% 46.81/6.32 fof(f1517,plain,(
% 46.81/6.32 ~aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)))|~aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))|~aScalar0(sdtasdt0(xP,xP))|~aScalar0(xN)|~sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))|~sdtlseqdt0(sdtasdt0(xP,xP),xN)),
% 46.81/6.33 inference(resolution,[status(thm)],[f121,f202])).
% 46.81/6.33 fof(f1518,plain,(
% 46.81/6.33 ~aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)))|~aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))|~aScalar0(sdtasdt0(xP,xP))|~sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))|~sdtlseqdt0(sdtasdt0(xP,xP),xN)),
% 46.81/6.33 inference(forward_subsumption_resolution,[status(thm)],[f1517,f197])).
% 46.81/6.33 fof(f1920,plain,(
% 46.81/6.33 ~aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)))|~aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))|~sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))|~sdtlseqdt0(sdtasdt0(xP,xP),xN)|~aScalar0(xP)|~aScalar0(xP)),
% 46.81/6.33 inference(resolution,[status(thm)],[f1518,f85])).
% 46.81/6.33 fof(f1921,plain,(
% 46.81/6.33 ~aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)))|~aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))|~sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))|~sdtlseqdt0(sdtasdt0(xP,xP),xN)|~aScalar0(xP)),
% 46.81/6.33 inference(duplicate_literals_removal,[status(thm)],[f1920])).
% 46.81/6.33 fof(f1922,plain,(
% 46.81/6.33 ~aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)))|~aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))|~sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))|~aScalar0(xP)),
% 46.81/6.33 inference(forward_subsumption_resolution,[status(thm)],[f1921,f200])).
% 46.81/6.33 fof(f1923,plain,(
% 46.81/6.33 ~aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)))|~aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))|~sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))),
% 46.81/6.33 inference(resolution,[status(thm)],[f1922,f193])).
% 46.81/6.33 fof(f1924,plain,(
% 46.81/6.33 ~aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))|~sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))|~aScalar0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)))|~aScalar0(sdtasdt0(xP,xP))),
% 46.81/6.33 inference(resolution,[status(thm)],[f1923,f83])).
% 46.81/6.33 fof(f1925,plain,(
% 46.81/6.33 ~aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))|~sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))|~aScalar0(sdtasdt0(xP,xP))|~aScalar0(sdtasdt0(xP,xP))|~aScalar0(sdtasdt0(xP,xP))),
% 46.81/6.33 inference(resolution,[status(thm)],[f1924,f83])).
% 46.81/6.33 fof(f1927,plain,(
% 46.81/6.33 ~aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))|~sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))|~aScalar0(sdtasdt0(xP,xP))),
% 46.81/6.33 inference(duplicate_literals_removal,[status(thm)],[f1925])).
% 46.81/6.33 fof(f1930,plain,(
% 46.81/6.33 ~aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))|~sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))|~aScalar0(xP)|~aScalar0(xP)),
% 46.81/6.33 inference(resolution,[status(thm)],[f1927,f85])).
% 46.81/6.33 fof(f1931,plain,(
% 46.81/6.33 ~aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))|~sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))|~aScalar0(xP)),
% 46.81/6.33 inference(duplicate_literals_removal,[status(thm)],[f1930])).
% 46.81/6.33 fof(f1932,plain,(
% 46.81/6.33 ~aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))|~sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))),
% 46.81/6.33 inference(forward_subsumption_resolution,[status(thm)],[f1931,f193])).
% 46.81/6.33 fof(f1933,plain,(
% 46.81/6.33 ~sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))|~aScalar0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~aScalar0(xN)),
% 46.81/6.33 inference(resolution,[status(thm)],[f1932,f83])).
% 46.81/6.33 fof(f1934,plain,(
% 46.81/6.33 ~sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))|~aScalar0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))),
% 46.81/6.33 inference(forward_subsumption_resolution,[status(thm)],[f1933,f197])).
% 46.81/6.33 fof(f2527,plain,(
% 46.81/6.33 ~sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))|~aScalar0(sdtasdt0(xR,xR))|~aScalar0(sdtasdt0(xS,xS))),
% 46.81/6.33 inference(resolution,[status(thm)],[f1934,f83])).
% 46.81/6.33 fof(f2528,plain,(
% 46.81/6.33 ~sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))|~aScalar0(sdtasdt0(xR,xR))|~aScalar0(xS)|~aScalar0(xS)),
% 46.81/6.33 inference(resolution,[status(thm)],[f2527,f85])).
% 46.81/6.33 fof(f2529,plain,(
% 46.81/6.33 ~sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))|~aScalar0(sdtasdt0(xR,xR))|~aScalar0(xS)),
% 46.81/6.33 inference(duplicate_literals_removal,[status(thm)],[f2528])).
% 46.81/6.33 fof(f2530,plain,(
% 46.81/6.33 ~sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))|~aScalar0(sdtasdt0(xR,xR))),
% 46.81/6.33 inference(forward_subsumption_resolution,[status(thm)],[f2529,f195])).
% 46.81/6.33 fof(f2531,plain,(
% 46.81/6.33 ~sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))|~aScalar0(xR)|~aScalar0(xR)),
% 46.81/6.33 inference(resolution,[status(thm)],[f2530,f85])).
% 46.81/6.33 fof(f2532,plain,(
% 46.81/6.33 ~sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))|~aScalar0(xR)),
% 46.81/6.33 inference(duplicate_literals_removal,[status(thm)],[f2531])).
% 46.81/6.33 fof(f2533,plain,(
% 46.81/6.33 ~sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))),
% 46.81/6.33 inference(forward_subsumption_resolution,[status(thm)],[f2532,f191])).
% 46.81/6.33 fof(f2534,plain,(
% 46.81/6.33 ~aScalar0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)))|~aScalar0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~aScalar0(sdtasdt0(xP,xP))|~aScalar0(xN)|~sdtlseqdt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~sdtlseqdt0(sdtasdt0(xP,xP),xN)),
% 46.81/6.33 inference(resolution,[status(thm)],[f2533,f121])).
% 46.81/6.33 fof(f2536,plain,(
% 46.81/6.33 ~aScalar0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)))|~aScalar0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~aScalar0(sdtasdt0(xP,xP))|~sdtlseqdt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~sdtlseqdt0(sdtasdt0(xP,xP),xN)),
% 46.81/6.33 inference(forward_subsumption_resolution,[status(thm)],[f2534,f197])).
% 46.81/6.33 fof(f2537,plain,(
% 46.81/6.33 ~aScalar0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)))|~aScalar0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~sdtlseqdt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~sdtlseqdt0(sdtasdt0(xP,xP),xN)|~aScalar0(xP)|~aScalar0(xP)),
% 46.81/6.33 inference(resolution,[status(thm)],[f2536,f85])).
% 46.81/6.33 fof(f2538,plain,(
% 46.81/6.33 ~aScalar0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)))|~aScalar0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~sdtlseqdt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~sdtlseqdt0(sdtasdt0(xP,xP),xN)|~aScalar0(xP)),
% 46.81/6.33 inference(duplicate_literals_removal,[status(thm)],[f2537])).
% 46.81/6.33 fof(f2539,plain,(
% 46.81/6.33 ~aScalar0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)))|~aScalar0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~sdtlseqdt0(sdtasdt0(xP,xP),xN)|~aScalar0(xP)),
% 46.81/6.33 inference(forward_subsumption_resolution,[status(thm)],[f2538,f201])).
% 46.81/6.36 fof(f2540,plain,(
% 46.81/6.36 ~aScalar0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)))|~aScalar0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~sdtlseqdt0(sdtasdt0(xP,xP),xN)),
% 46.81/6.36 inference(resolution,[status(thm)],[f2539,f193])).
% 46.81/6.36 fof(f2541,plain,(
% 46.81/6.36 ~aScalar0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)))|~aScalar0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))),
% 46.81/6.36 inference(forward_subsumption_resolution,[status(thm)],[f2540,f200])).
% 46.81/6.36 fof(f3205,plain,(
% 46.81/6.36 ~aScalar0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~aScalar0(sdtasdt0(xP,xP))|~aScalar0(sdtasdt0(xP,xP))),
% 46.81/6.36 inference(resolution,[status(thm)],[f2541,f83])).
% 46.81/6.36 fof(f3206,plain,(
% 46.81/6.36 ~aScalar0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~aScalar0(sdtasdt0(xP,xP))),
% 46.81/6.36 inference(duplicate_literals_removal,[status(thm)],[f3205])).
% 46.81/6.36 fof(f3207,plain,(
% 46.81/6.36 ~aScalar0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~aScalar0(xP)|~aScalar0(xP)),
% 46.81/6.36 inference(resolution,[status(thm)],[f3206,f85])).
% 46.81/6.36 fof(f3208,plain,(
% 46.81/6.36 ~aScalar0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~aScalar0(xP)),
% 46.81/6.36 inference(duplicate_literals_removal,[status(thm)],[f3207])).
% 46.81/6.36 fof(f3209,plain,(
% 46.81/6.36 ~aScalar0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))),
% 46.81/6.36 inference(forward_subsumption_resolution,[status(thm)],[f3208,f193])).
% 46.81/6.36 fof(f3210,plain,(
% 46.81/6.36 ~aScalar0(sdtasdt0(xR,xR))|~aScalar0(sdtasdt0(xS,xS))),
% 46.81/6.36 inference(resolution,[status(thm)],[f3209,f83])).
% 46.81/6.36 fof(f3211,plain,(
% 46.81/6.36 ~aScalar0(sdtasdt0(xR,xR))|~aScalar0(xS)|~aScalar0(xS)),
% 46.81/6.36 inference(resolution,[status(thm)],[f3210,f85])).
% 46.81/6.36 fof(f3212,plain,(
% 46.81/6.36 ~aScalar0(sdtasdt0(xR,xR))|~aScalar0(xS)),
% 46.81/6.36 inference(duplicate_literals_removal,[status(thm)],[f3211])).
% 46.81/6.36 fof(f3213,plain,(
% 46.81/6.36 ~aScalar0(sdtasdt0(xR,xR))),
% 46.81/6.36 inference(forward_subsumption_resolution,[status(thm)],[f3212,f195])).
% 46.81/6.36 fof(f3214,plain,(
% 46.81/6.36 ~aScalar0(xR)|~aScalar0(xR)),
% 46.81/6.36 inference(resolution,[status(thm)],[f3213,f85])).
% 46.81/6.36 fof(f3215,plain,(
% 46.81/6.36 ~aScalar0(xR)),
% 46.81/6.36 inference(duplicate_literals_removal,[status(thm)],[f3214])).
% 46.81/6.36 fof(f3216,plain,(
% 46.81/6.36 $false),
% 46.81/6.36 inference(forward_subsumption_resolution,[status(thm)],[f3215,f191])).
% 46.81/6.36 % SZS output end CNFRefutation for theBenchmark.p
% 46.81/6.38 % Elapsed time: 6.005638 seconds
% 46.81/6.38 % CPU time: 47.320796 seconds
% 46.81/6.38 % Total memory used: 461.810 MB
% 46.81/6.38 % Net memory used: 430.915 MB
%------------------------------------------------------------------------------