%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : RNG067+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 : n011.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 77.18s 10.27s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : RNG067+1 : 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.16/0.44 % Computer : n011.cluster.edu
% 0.16/0.44 % Model : x86_64 x86_64
% 0.16/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.44 % Memory : 8046.5625MB
% 0.16/0.44 % OS : Linux 6.8.0-71-generic
% 0.16/0.44 % CPULimit : 300
% 0.16/0.44 % WCLimit : 300
% 0.16/0.44 % DateTime : Mon Sep 21 04:17:10 UTC 2026
% 0.16/0.44 % CPUTime :
% 0.16/0.47 % Drodi V4.1.1
% 77.18/10.27 % Refutation found
% 77.18/10.27 % SZS status Theorem for theBenchmark: Theorem is valid
% 77.18/10.27 % SZS output start CNFRefutation for theBenchmark
% 77.18/10.27 fof(f10,axiom,(
% 77.18/10.27 (! [W0,W1] :( ( aScalar0(W0)& aScalar0(W1) )=> aScalar0(sdtpldt0(W0,W1)) ) )),
% 77.18/10.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 77.18/10.27 fof(f11,axiom,(
% 77.18/10.27 (! [W0,W1] :( ( aScalar0(W0)& aScalar0(W1) )=> aScalar0(sdtasdt0(W0,W1)) ) )),
% 77.18/10.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 77.18/10.27 fof(f23,axiom,(
% 77.18/10.27 (! [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)) ) ) )),
% 77.18/10.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 77.18/10.27 fof(f52,hypothesis,(
% 77.18/10.27 ( aScalar0(xR)& xR = sdtasdt0(xC,xG) ) ),
% 77.18/10.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 77.18/10.27 fof(f53,hypothesis,(
% 77.18/10.27 ( aScalar0(xP)& xP = sdtasdt0(xE,xH) ) ),
% 77.18/10.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 77.18/10.27 fof(f54,hypothesis,(
% 77.18/10.27 ( aScalar0(xS)& xS = sdtasdt0(xF,xD) ) ),
% 77.18/10.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 77.18/10.27 fof(f55,hypothesis,(
% 77.18/10.27 ( aScalar0(xN)& xN = sdtasdt0(xR,xS) ) ),
% 77.18/10.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 77.18/10.27 fof(f57,hypothesis,(
% 77.18/10.27 sdtlseqdt0(sdtasdt0(xP,xP),xN) ),
% 77.18/10.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 77.18/10.27 fof(f58,hypothesis,(
% 77.18/10.27 sdtlseqdt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS))) ),
% 77.18/10.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 77.18/10.27 fof(f59,conjecture,(
% 77.18/10.27 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)) ),
% 77.18/10.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 77.18/10.27 fof(f60,negated_conjecture,(
% 77.18/10.27 ~(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)) )),
% 77.18/10.27 inference(negated_conjecture,[status(cth)],[f59])).
% 77.18/10.27 fof(f82,plain,(
% 77.18/10.27 ![W0,W1]: ((~aScalar0(W0)|~aScalar0(W1))|aScalar0(sdtpldt0(W0,W1)))),
% 77.18/10.27 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 77.18/10.27 fof(f83,plain,(
% 77.18/10.27 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|aScalar0(sdtpldt0(X0,X1)))),
% 77.18/10.27 inference(cnf_transformation,[status(thm)],[f82])).
% 77.18/10.27 fof(f84,plain,(
% 77.18/10.27 ![W0,W1]: ((~aScalar0(W0)|~aScalar0(W1))|aScalar0(sdtasdt0(W0,W1)))),
% 77.18/10.27 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 77.18/10.27 fof(f85,plain,(
% 77.18/10.27 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|aScalar0(sdtasdt0(X0,X1)))),
% 77.18/10.27 inference(cnf_transformation,[status(thm)],[f84])).
% 77.18/10.27 fof(f120,plain,(
% 77.18/10.27 ![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))))),
% 77.18/10.27 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 77.18/10.27 fof(f121,plain,(
% 77.18/10.27 ![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)))),
% 77.18/10.27 inference(cnf_transformation,[status(thm)],[f120])).
% 77.18/10.27 fof(f185,plain,(
% 77.18/10.27 aScalar0(xR)),
% 77.18/10.27 inference(cnf_transformation,[status(thm)],[f52])).
% 77.18/10.27 fof(f187,plain,(
% 77.18/10.27 aScalar0(xP)),
% 77.18/10.27 inference(cnf_transformation,[status(thm)],[f53])).
% 77.18/10.27 fof(f189,plain,(
% 77.18/10.27 aScalar0(xS)),
% 77.18/10.27 inference(cnf_transformation,[status(thm)],[f54])).
% 77.18/10.27 fof(f191,plain,(
% 77.18/10.27 aScalar0(xN)),
% 77.18/10.27 inference(cnf_transformation,[status(thm)],[f55])).
% 77.18/10.27 fof(f194,plain,(
% 77.18/10.27 sdtlseqdt0(sdtasdt0(xP,xP),xN)),
% 77.18/10.27 inference(cnf_transformation,[status(thm)],[f57])).
% 77.18/10.27 fof(f195,plain,(
% 77.18/10.27 sdtlseqdt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))),
% 77.18/10.27 inference(cnf_transformation,[status(thm)],[f58])).
% 77.18/10.27 fof(f196,plain,(
% 77.18/10.27 ~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))),
% 77.18/10.27 inference(cnf_transformation,[status(thm)],[f60])).
% 77.18/10.27 fof(f1510,plain,(
% 77.18/10.27 ~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)),
% 77.18/10.27 inference(resolution,[status(thm)],[f121,f196])).
% 77.18/10.27 fof(f1511,plain,(
% 77.18/10.27 ~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)),
% 77.18/10.27 inference(forward_subsumption_resolution,[status(thm)],[f1510,f191])).
% 77.18/10.27 fof(f1913,plain,(
% 77.18/10.27 ~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)),
% 77.18/10.27 inference(resolution,[status(thm)],[f1511,f85])).
% 77.18/10.27 fof(f1914,plain,(
% 77.18/10.27 ~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)),
% 77.18/10.27 inference(duplicate_literals_removal,[status(thm)],[f1913])).
% 77.18/10.27 fof(f1915,plain,(
% 77.18/10.27 ~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)),
% 77.18/10.27 inference(forward_subsumption_resolution,[status(thm)],[f1914,f194])).
% 77.18/10.27 fof(f1916,plain,(
% 77.18/10.27 ~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))),
% 77.18/10.27 inference(resolution,[status(thm)],[f1915,f187])).
% 77.18/10.27 fof(f1917,plain,(
% 77.18/10.27 ~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))),
% 77.18/10.27 inference(resolution,[status(thm)],[f1916,f83])).
% 77.18/10.27 fof(f1918,plain,(
% 77.18/10.27 ~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))),
% 77.18/10.27 inference(resolution,[status(thm)],[f1917,f83])).
% 77.18/10.27 fof(f1920,plain,(
% 77.18/10.27 ~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))),
% 77.18/10.27 inference(duplicate_literals_removal,[status(thm)],[f1918])).
% 77.18/10.27 fof(f1923,plain,(
% 77.18/10.27 ~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)),
% 77.18/10.27 inference(resolution,[status(thm)],[f1920,f85])).
% 77.18/10.27 fof(f1924,plain,(
% 77.18/10.27 ~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)),
% 77.18/10.27 inference(duplicate_literals_removal,[status(thm)],[f1923])).
% 77.18/10.27 fof(f1925,plain,(
% 77.18/10.27 ~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))),
% 77.18/10.27 inference(forward_subsumption_resolution,[status(thm)],[f1924,f187])).
% 77.18/10.27 fof(f1926,plain,(
% 77.18/10.27 ~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)),
% 77.18/10.27 inference(resolution,[status(thm)],[f1925,f83])).
% 77.18/10.27 fof(f1927,plain,(
% 77.18/10.27 ~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)))),
% 77.18/10.27 inference(forward_subsumption_resolution,[status(thm)],[f1926,f191])).
% 77.18/10.27 fof(f2520,plain,(
% 77.18/10.27 ~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))),
% 77.18/10.27 inference(resolution,[status(thm)],[f1927,f83])).
% 77.18/10.27 fof(f2521,plain,(
% 77.18/10.27 ~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)),
% 77.18/10.27 inference(resolution,[status(thm)],[f2520,f85])).
% 77.18/10.27 fof(f2522,plain,(
% 77.18/10.27 ~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)),
% 77.18/10.27 inference(duplicate_literals_removal,[status(thm)],[f2521])).
% 77.18/10.27 fof(f2523,plain,(
% 77.18/10.27 ~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))),
% 77.18/10.27 inference(forward_subsumption_resolution,[status(thm)],[f2522,f189])).
% 77.18/10.27 fof(f2524,plain,(
% 77.18/10.27 ~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)),
% 77.18/10.27 inference(resolution,[status(thm)],[f2523,f85])).
% 77.18/10.27 fof(f2525,plain,(
% 77.18/10.27 ~sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))|~aScalar0(xR)),
% 77.18/10.27 inference(duplicate_literals_removal,[status(thm)],[f2524])).
% 77.18/10.27 fof(f2526,plain,(
% 77.18/10.27 ~sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))),
% 77.18/10.27 inference(forward_subsumption_resolution,[status(thm)],[f2525,f185])).
% 77.18/10.27 fof(f2527,plain,(
% 77.18/10.27 ~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)),
% 77.18/10.27 inference(resolution,[status(thm)],[f2526,f121])).
% 77.18/10.27 fof(f2529,plain,(
% 77.18/10.27 ~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)),
% 77.18/10.27 inference(forward_subsumption_resolution,[status(thm)],[f2527,f191])).
% 77.18/10.27 fof(f2530,plain,(
% 77.18/10.27 ~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)),
% 77.18/10.27 inference(resolution,[status(thm)],[f2529,f85])).
% 77.18/10.27 fof(f2531,plain,(
% 77.18/10.27 ~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)),
% 77.18/10.27 inference(duplicate_literals_removal,[status(thm)],[f2530])).
% 77.18/10.27 fof(f2532,plain,(
% 77.18/10.27 ~aScalar0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)))|~aScalar0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~sdtlseqdt0(sdtasdt0(xP,xP),xN)|~aScalar0(xP)),
% 77.18/10.27 inference(forward_subsumption_resolution,[status(thm)],[f2531,f195])).
% 63.20/10.37 fof(f2533,plain,(
% 63.20/10.37 ~aScalar0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)))|~aScalar0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~sdtlseqdt0(sdtasdt0(xP,xP),xN)),
% 63.20/10.37 inference(resolution,[status(thm)],[f2532,f187])).
% 63.20/10.37 fof(f2534,plain,(
% 63.20/10.37 ~aScalar0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)))|~aScalar0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))),
% 63.20/10.37 inference(forward_subsumption_resolution,[status(thm)],[f2533,f194])).
% 63.20/10.37 fof(f3198,plain,(
% 63.20/10.37 ~aScalar0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~aScalar0(sdtasdt0(xP,xP))|~aScalar0(sdtasdt0(xP,xP))),
% 63.20/10.37 inference(resolution,[status(thm)],[f2534,f83])).
% 63.20/10.37 fof(f3199,plain,(
% 63.20/10.37 ~aScalar0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~aScalar0(sdtasdt0(xP,xP))),
% 63.20/10.37 inference(duplicate_literals_removal,[status(thm)],[f3198])).
% 63.20/10.37 fof(f3200,plain,(
% 63.20/10.37 ~aScalar0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~aScalar0(xP)|~aScalar0(xP)),
% 63.20/10.37 inference(resolution,[status(thm)],[f3199,f85])).
% 63.20/10.37 fof(f3201,plain,(
% 63.20/10.37 ~aScalar0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))|~aScalar0(xP)),
% 63.20/10.37 inference(duplicate_literals_removal,[status(thm)],[f3200])).
% 63.20/10.37 fof(f3202,plain,(
% 63.20/10.37 ~aScalar0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))),
% 63.20/10.37 inference(forward_subsumption_resolution,[status(thm)],[f3201,f187])).
% 63.20/10.37 fof(f3203,plain,(
% 63.20/10.37 ~aScalar0(sdtasdt0(xR,xR))|~aScalar0(sdtasdt0(xS,xS))),
% 63.20/10.37 inference(resolution,[status(thm)],[f3202,f83])).
% 63.20/10.37 fof(f3204,plain,(
% 63.20/10.37 ~aScalar0(sdtasdt0(xR,xR))|~aScalar0(xS)|~aScalar0(xS)),
% 63.20/10.37 inference(resolution,[status(thm)],[f3203,f85])).
% 63.20/10.37 fof(f3205,plain,(
% 63.20/10.37 ~aScalar0(sdtasdt0(xR,xR))|~aScalar0(xS)),
% 63.20/10.37 inference(duplicate_literals_removal,[status(thm)],[f3204])).
% 63.20/10.37 fof(f3206,plain,(
% 63.20/10.37 ~aScalar0(sdtasdt0(xR,xR))),
% 63.20/10.37 inference(forward_subsumption_resolution,[status(thm)],[f3205,f189])).
% 63.20/10.37 fof(f3207,plain,(
% 63.20/10.37 ~aScalar0(xR)|~aScalar0(xR)),
% 63.20/10.37 inference(resolution,[status(thm)],[f3206,f85])).
% 63.20/10.37 fof(f3208,plain,(
% 63.20/10.37 ~aScalar0(xR)),
% 63.20/10.37 inference(duplicate_literals_removal,[status(thm)],[f3207])).
% 63.20/10.37 fof(f3209,plain,(
% 63.20/10.37 $false),
% 63.20/10.37 inference(forward_subsumption_resolution,[status(thm)],[f3208,f185])).
% 63.20/10.37 % SZS output end CNFRefutation for theBenchmark.p
% 63.20/10.37 % Elapsed time: 9.897807 seconds
% 63.20/10.37 % CPU time: 77.819349 seconds
% 63.20/10.37 % Total memory used: 562.570 MB
% 63.20/10.37 % Net memory used: 522.618 MB
%------------------------------------------------------------------------------