%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : RNG076+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 : n020.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:17 PM UTC 2026
% Result : Theorem 44.28s 6.18s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : RNG076+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.18/0.44 % Computer : n020.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Mon Sep 21 04:18:48 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.46 % Drodi V4.1.1
% 44.28/6.18 % Refutation found
% 44.28/6.18 % SZS status Theorem for theBenchmark: Theorem is valid
% 44.28/6.18 % SZS output start CNFRefutation for theBenchmark
% 44.28/6.18 fof(f10,axiom,(
% 44.28/6.18 (! [W0,W1] :( ( aScalar0(W0)& aScalar0(W1) )=> aScalar0(sdtpldt0(W0,W1)) ) )),
% 44.28/6.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.28/6.18 fof(f11,axiom,(
% 44.28/6.18 (! [W0,W1] :( ( aScalar0(W0)& aScalar0(W1) )=> aScalar0(sdtasdt0(W0,W1)) ) )),
% 44.28/6.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.28/6.18 fof(f20,axiom,(
% 44.28/6.18 (! [W0] :( aScalar0(W0)=> sdtlseqdt0(W0,W0) ) )),
% 44.28/6.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.28/6.18 fof(f23,axiom,(
% 44.28/6.18 (! [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)) ) ) )),
% 44.28/6.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.28/6.18 fof(f46,hypothesis,(
% 44.28/6.18 ( aScalar0(xC)& xC = sdtasasdt0(xp,xp) ) ),
% 44.28/6.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.28/6.18 fof(f47,hypothesis,(
% 44.28/6.18 ( aScalar0(xD)& xD = sdtasasdt0(xq,xq) ) ),
% 44.28/6.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.28/6.18 fof(f48,hypothesis,(
% 44.28/6.18 ( aScalar0(xE)& xE = sdtasasdt0(xp,xq) ) ),
% 44.28/6.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.28/6.18 fof(f51,hypothesis,(
% 44.28/6.18 ( aScalar0(xH)& xH = sdtasdt0(xA,xB) ) ),
% 44.28/6.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.28/6.18 fof(f52,hypothesis,(
% 44.28/6.18 ( aScalar0(xR)& xR = sdtasdt0(xC,xG) ) ),
% 44.28/6.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.28/6.18 fof(f53,hypothesis,(
% 44.28/6.18 ( aScalar0(xP)& xP = sdtasdt0(xE,xH) ) ),
% 44.28/6.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.28/6.18 fof(f54,hypothesis,(
% 44.28/6.18 ( aScalar0(xS)& xS = sdtasdt0(xF,xD) ) ),
% 44.28/6.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.28/6.18 fof(f56,hypothesis,(
% 44.28/6.18 sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(xC,xD)) ),
% 44.28/6.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.28/6.18 fof(f57,hypothesis,(
% 44.28/6.18 sdtlseqdt0(sdtpldt0(xP,xP),sdtpldt0(xR,xS)) ),
% 44.28/6.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.28/6.18 fof(f58,conjecture,(
% 44.28/6.18 sdtlseqdt0(sdtpldt0(sdtasdt0(xE,xE),sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH))),sdtpldt0(sdtasdt0(xC,xD),sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))) ),
% 44.28/6.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.28/6.18 fof(f59,negated_conjecture,(
% 44.28/6.18 ~(sdtlseqdt0(sdtpldt0(sdtasdt0(xE,xE),sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH))),sdtpldt0(sdtasdt0(xC,xD),sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))) )),
% 44.28/6.18 inference(negated_conjecture,[status(cth)],[f58])).
% 44.28/6.18 fof(f81,plain,(
% 44.28/6.18 ![W0,W1]: ((~aScalar0(W0)|~aScalar0(W1))|aScalar0(sdtpldt0(W0,W1)))),
% 44.28/6.18 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 44.28/6.18 fof(f82,plain,(
% 44.28/6.18 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|aScalar0(sdtpldt0(X0,X1)))),
% 44.28/6.18 inference(cnf_transformation,[status(thm)],[f81])).
% 44.28/6.18 fof(f83,plain,(
% 44.28/6.18 ![W0,W1]: ((~aScalar0(W0)|~aScalar0(W1))|aScalar0(sdtasdt0(W0,W1)))),
% 44.28/6.18 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 44.28/6.18 fof(f84,plain,(
% 44.28/6.18 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|aScalar0(sdtasdt0(X0,X1)))),
% 44.28/6.18 inference(cnf_transformation,[status(thm)],[f83])).
% 44.28/6.18 fof(f113,plain,(
% 44.28/6.18 ![W0]: (~aScalar0(W0)|sdtlseqdt0(W0,W0))),
% 44.28/6.18 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 44.28/6.18 fof(f114,plain,(
% 44.28/6.18 ![X0]: (~aScalar0(X0)|sdtlseqdt0(X0,X0))),
% 44.28/6.18 inference(cnf_transformation,[status(thm)],[f113])).
% 44.28/6.18 fof(f119,plain,(
% 44.28/6.18 ![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))))),
% 44.28/6.18 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 44.28/6.18 fof(f120,plain,(
% 44.28/6.18 ![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)))),
% 44.28/6.18 inference(cnf_transformation,[status(thm)],[f119])).
% 44.28/6.18 fof(f172,plain,(
% 44.28/6.18 aScalar0(xC)),
% 44.28/6.18 inference(cnf_transformation,[status(thm)],[f46])).
% 44.28/6.18 fof(f174,plain,(
% 44.28/6.18 aScalar0(xD)),
% 44.28/6.18 inference(cnf_transformation,[status(thm)],[f47])).
% 44.28/6.18 fof(f176,plain,(
% 44.28/6.18 aScalar0(xE)),
% 44.28/6.18 inference(cnf_transformation,[status(thm)],[f48])).
% 44.28/6.18 fof(f182,plain,(
% 44.28/6.18 aScalar0(xH)),
% 44.28/6.18 inference(cnf_transformation,[status(thm)],[f51])).
% 44.28/6.19 fof(f184,plain,(
% 44.28/6.19 aScalar0(xR)),
% 44.28/6.19 inference(cnf_transformation,[status(thm)],[f52])).
% 44.28/6.19 fof(f186,plain,(
% 44.28/6.19 aScalar0(xP)),
% 44.28/6.19 inference(cnf_transformation,[status(thm)],[f53])).
% 44.28/6.19 fof(f188,plain,(
% 44.28/6.19 aScalar0(xS)),
% 44.28/6.19 inference(cnf_transformation,[status(thm)],[f54])).
% 44.28/6.19 fof(f192,plain,(
% 44.28/6.19 sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(xC,xD))),
% 44.28/6.19 inference(cnf_transformation,[status(thm)],[f56])).
% 44.28/6.19 fof(f193,plain,(
% 44.28/6.19 sdtlseqdt0(sdtpldt0(xP,xP),sdtpldt0(xR,xS))),
% 44.28/6.19 inference(cnf_transformation,[status(thm)],[f57])).
% 44.28/6.19 fof(f194,plain,(
% 44.28/6.19 ~sdtlseqdt0(sdtpldt0(sdtasdt0(xE,xE),sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH))),sdtpldt0(sdtasdt0(xC,xD),sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH))))),
% 44.28/6.19 inference(cnf_transformation,[status(thm)],[f59])).
% 44.28/6.19 fof(f1788,plain,(
% 44.28/6.19 ~aScalar0(sdtasdt0(xE,xE))|~aScalar0(sdtasdt0(xC,xD))|~aScalar0(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)))|~aScalar0(sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))|~sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(xC,xD))|~sdtlseqdt0(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)),sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))),
% 44.28/6.19 inference(resolution,[status(thm)],[f120,f194])).
% 44.28/6.19 fof(f1789,plain,(
% 44.28/6.19 ~aScalar0(sdtasdt0(xE,xE))|~aScalar0(sdtasdt0(xC,xD))|~aScalar0(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)))|~aScalar0(sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))|~sdtlseqdt0(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)),sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))),
% 44.28/6.19 inference(forward_subsumption_resolution,[status(thm)],[f1788,f192])).
% 44.28/6.19 fof(f2172,plain,(
% 44.28/6.19 ~aScalar0(sdtasdt0(xC,xD))|~aScalar0(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)))|~aScalar0(sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))|~sdtlseqdt0(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)),sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))|~aScalar0(xE)|~aScalar0(xE)),
% 44.28/6.19 inference(resolution,[status(thm)],[f1789,f84])).
% 44.28/6.19 fof(f2173,plain,(
% 44.28/6.19 ~aScalar0(sdtasdt0(xC,xD))|~aScalar0(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)))|~aScalar0(sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))|~sdtlseqdt0(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)),sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))|~aScalar0(xE)),
% 44.28/6.19 inference(duplicate_literals_removal,[status(thm)],[f2172])).
% 44.28/6.19 fof(f2174,plain,(
% 44.28/6.19 ~aScalar0(sdtasdt0(xC,xD))|~aScalar0(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)))|~aScalar0(sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))|~sdtlseqdt0(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)),sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))),
% 44.28/6.19 inference(forward_subsumption_resolution,[status(thm)],[f2173,f176])).
% 44.28/6.19 fof(f2175,plain,(
% 44.28/6.19 ~aScalar0(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)))|~aScalar0(sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))|~sdtlseqdt0(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)),sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))|~aScalar0(xC)|~aScalar0(xD)),
% 44.28/6.19 inference(resolution,[status(thm)],[f2174,f84])).
% 44.28/6.19 fof(f2176,plain,(
% 44.28/6.19 ~aScalar0(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)))|~aScalar0(sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))|~sdtlseqdt0(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)),sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))|~aScalar0(xD)),
% 44.28/6.19 inference(forward_subsumption_resolution,[status(thm)],[f2175,f172])).
% 44.28/6.19 fof(f2825,plain,(
% 44.28/6.19 ~aScalar0(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)))|~aScalar0(sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))|~sdtlseqdt0(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)),sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))),
% 44.28/6.19 inference(forward_subsumption_resolution,[status(thm)],[f2176,f174])).
% 44.28/6.19 fof(f2826,plain,(
% 44.28/6.19 ~aScalar0(sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))|~sdtlseqdt0(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)),sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))|~aScalar0(sdtpldt0(xP,xP))|~aScalar0(sdtasdt0(xH,xH))),
% 44.28/6.19 inference(resolution,[status(thm)],[f2825,f82])).
% 44.28/6.19 fof(f2827,plain,(
% 44.28/6.19 ~aScalar0(sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))|~sdtlseqdt0(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)),sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))|~aScalar0(sdtpldt0(xP,xP))|~aScalar0(xH)|~aScalar0(xH)),
% 44.28/6.19 inference(resolution,[status(thm)],[f2826,f84])).
% 44.28/6.19 fof(f2828,plain,(
% 44.28/6.19 ~aScalar0(sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))|~sdtlseqdt0(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)),sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))|~aScalar0(sdtpldt0(xP,xP))|~aScalar0(xH)),
% 44.28/6.19 inference(duplicate_literals_removal,[status(thm)],[f2827])).
% 44.28/6.19 fof(f2829,plain,(
% 44.28/6.19 ~aScalar0(sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))|~sdtlseqdt0(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)),sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))|~aScalar0(sdtpldt0(xP,xP))),
% 44.28/6.19 inference(forward_subsumption_resolution,[status(thm)],[f2828,f182])).
% 44.28/6.19 fof(f3285,plain,(
% 44.28/6.19 ~sdtlseqdt0(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)),sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))|~aScalar0(sdtpldt0(xP,xP))|~aScalar0(sdtpldt0(xR,xS))|~aScalar0(sdtasdt0(xH,xH))),
% 44.28/6.19 inference(resolution,[status(thm)],[f2829,f82])).
% 44.28/6.19 fof(f3286,plain,(
% 44.28/6.19 ~sdtlseqdt0(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)),sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))|~aScalar0(sdtpldt0(xP,xP))|~aScalar0(sdtpldt0(xR,xS))|~aScalar0(xH)|~aScalar0(xH)),
% 44.28/6.19 inference(resolution,[status(thm)],[f3285,f84])).
% 44.28/6.19 fof(f3287,plain,(
% 44.28/6.19 ~sdtlseqdt0(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)),sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))|~aScalar0(sdtpldt0(xP,xP))|~aScalar0(sdtpldt0(xR,xS))|~aScalar0(xH)),
% 44.28/6.19 inference(duplicate_literals_removal,[status(thm)],[f3286])).
% 44.28/6.19 fof(f3288,plain,(
% 44.28/6.19 ~sdtlseqdt0(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)),sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))|~aScalar0(sdtpldt0(xP,xP))|~aScalar0(sdtpldt0(xR,xS))),
% 44.28/6.19 inference(forward_subsumption_resolution,[status(thm)],[f3287,f182])).
% 44.28/6.19 fof(f5504,plain,(
% 44.28/6.19 ~sdtlseqdt0(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)),sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))|~aScalar0(sdtpldt0(xR,xS))|~aScalar0(xP)|~aScalar0(xP)),
% 44.28/6.19 inference(resolution,[status(thm)],[f3288,f82])).
% 44.28/6.19 fof(f5505,plain,(
% 44.28/6.19 ~sdtlseqdt0(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)),sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))|~aScalar0(sdtpldt0(xR,xS))|~aScalar0(xP)),
% 44.28/6.19 inference(duplicate_literals_removal,[status(thm)],[f5504])).
% 44.28/6.19 fof(f5506,plain,(
% 44.28/6.19 ~sdtlseqdt0(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)),sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))|~aScalar0(sdtpldt0(xR,xS))),
% 44.28/6.19 inference(forward_subsumption_resolution,[status(thm)],[f5505,f186])).
% 44.28/6.19 fof(f5507,plain,(
% 44.28/6.19 ~sdtlseqdt0(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)),sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))|~aScalar0(xR)|~aScalar0(xS)),
% 44.28/6.19 inference(resolution,[status(thm)],[f5506,f82])).
% 44.28/6.19 fof(f5508,plain,(
% 44.28/6.19 ~sdtlseqdt0(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)),sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))|~aScalar0(xS)),
% 44.28/6.19 inference(forward_subsumption_resolution,[status(thm)],[f5507,f184])).
% 44.28/6.19 fof(f6828,plain,(
% 44.28/6.19 ~sdtlseqdt0(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)),sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))),
% 44.28/6.19 inference(forward_subsumption_resolution,[status(thm)],[f5508,f188])).
% 44.28/6.19 fof(f6829,plain,(
% 44.28/6.19 ~aScalar0(sdtpldt0(xP,xP))|~aScalar0(sdtpldt0(xR,xS))|~aScalar0(sdtasdt0(xH,xH))|~aScalar0(sdtasdt0(xH,xH))|~sdtlseqdt0(sdtpldt0(xP,xP),sdtpldt0(xR,xS))|~sdtlseqdt0(sdtasdt0(xH,xH),sdtasdt0(xH,xH))),
% 44.28/6.19 inference(resolution,[status(thm)],[f6828,f120])).
% 44.28/6.19 fof(f6831,plain,(
% 44.28/6.19 ~aScalar0(sdtpldt0(xP,xP))|~aScalar0(sdtpldt0(xR,xS))|~aScalar0(sdtasdt0(xH,xH))|~sdtlseqdt0(sdtpldt0(xP,xP),sdtpldt0(xR,xS))|~sdtlseqdt0(sdtasdt0(xH,xH),sdtasdt0(xH,xH))),
% 44.28/6.19 inference(duplicate_literals_removal,[status(thm)],[f6829])).
% 44.28/6.19 fof(f6832,plain,(
% 44.28/6.19 ~aScalar0(sdtpldt0(xP,xP))|~aScalar0(sdtpldt0(xR,xS))|~aScalar0(sdtasdt0(xH,xH))|~sdtlseqdt0(sdtasdt0(xH,xH),sdtasdt0(xH,xH))),
% 44.28/6.19 inference(forward_subsumption_resolution,[status(thm)],[f6831,f193])).
% 44.28/6.19 fof(f6833,plain,(
% 44.28/6.19 ~aScalar0(sdtpldt0(xP,xP))|~aScalar0(sdtpldt0(xR,xS))|~aScalar0(sdtasdt0(xH,xH))),
% 44.28/6.19 inference(forward_subsumption_resolution,[status(thm)],[f6832,f114])).
% 44.28/6.19 fof(f6834,plain,(
% 44.28/6.19 ~aScalar0(sdtpldt0(xP,xP))|~aScalar0(sdtpldt0(xR,xS))|~aScalar0(xH)|~aScalar0(xH)),
% 44.28/6.19 inference(resolution,[status(thm)],[f6833,f84])).
% 44.28/6.19 fof(f6835,plain,(
% 44.28/6.19 ~aScalar0(sdtpldt0(xP,xP))|~aScalar0(sdtpldt0(xR,xS))|~aScalar0(xH)),
% 44.28/6.19 inference(duplicate_literals_removal,[status(thm)],[f6834])).
% 44.28/6.19 fof(f6836,plain,(
% 44.28/6.19 ~aScalar0(sdtpldt0(xP,xP))|~aScalar0(sdtpldt0(xR,xS))),
% 44.28/6.19 inference(forward_subsumption_resolution,[status(thm)],[f6835,f182])).
% 44.28/6.19 fof(f6839,plain,(
% 44.28/6.19 ~aScalar0(sdtpldt0(xR,xS))|~aScalar0(xP)|~aScalar0(xP)),
% 44.28/6.22 inference(resolution,[status(thm)],[f6836,f82])).
% 44.28/6.22 fof(f6840,plain,(
% 44.28/6.22 ~aScalar0(sdtpldt0(xR,xS))|~aScalar0(xP)),
% 44.28/6.22 inference(duplicate_literals_removal,[status(thm)],[f6839])).
% 44.28/6.22 fof(f6841,plain,(
% 44.28/6.22 ~aScalar0(sdtpldt0(xR,xS))),
% 44.28/6.22 inference(forward_subsumption_resolution,[status(thm)],[f6840,f186])).
% 44.28/6.22 fof(f6842,plain,(
% 44.28/6.22 ~aScalar0(xR)|~aScalar0(xS)),
% 44.28/6.22 inference(resolution,[status(thm)],[f6841,f82])).
% 44.28/6.22 fof(f6843,plain,(
% 44.28/6.22 ~aScalar0(xS)),
% 44.28/6.22 inference(forward_subsumption_resolution,[status(thm)],[f6842,f184])).
% 44.28/6.22 fof(f6844,plain,(
% 44.28/6.22 $false),
% 44.28/6.22 inference(forward_subsumption_resolution,[status(thm)],[f6843,f188])).
% 44.28/6.22 % SZS output end CNFRefutation for theBenchmark.p
% 25.11/6.26 % Elapsed time: 5.790054 seconds
% 25.11/6.26 % CPU time: 45.208631 seconds
% 25.11/6.26 % Total memory used: 377.738 MB
% 25.11/6.26 % Net memory used: 358.174 MB
%------------------------------------------------------------------------------