%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : RNG076+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/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:17 PM UTC 2026
% Result : Theorem 43.36s 6.08s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : RNG076+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.41 % Computer : n011.cluster.edu
% 0.16/0.41 % Model : x86_64 x86_64
% 0.16/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.41 % Memory : 8046.5625MB
% 0.16/0.41 % OS : Linux 6.8.0-71-generic
% 0.16/0.41 % CPULimit : 300
% 0.16/0.41 % WCLimit : 300
% 0.16/0.41 % DateTime : Mon Sep 21 04:17:55 UTC 2026
% 0.16/0.41 % CPUTime :
% 0.16/0.43 % Drodi V4.1.1
% 43.36/6.08 % Refutation found
% 43.36/6.08 % SZS status Theorem for theBenchmark: Theorem is valid
% 43.36/6.08 % SZS output start CNFRefutation for theBenchmark
% 43.36/6.08 fof(f10,axiom,(
% 43.36/6.08 (! [W0,W1] :( ( aScalar0(W0)& aScalar0(W1) )=> aScalar0(sdtpldt0(W0,W1)) ) )),
% 43.36/6.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 43.36/6.08 fof(f11,axiom,(
% 43.36/6.08 (! [W0,W1] :( ( aScalar0(W0)& aScalar0(W1) )=> aScalar0(sdtasdt0(W0,W1)) ) )),
% 43.36/6.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 43.36/6.08 fof(f20,axiom,(
% 43.36/6.08 (! [W0] :( aScalar0(W0)=> sdtlseqdt0(W0,W0) ) )),
% 43.36/6.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 43.36/6.08 fof(f23,axiom,(
% 43.36/6.08 (! [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)) ) ) )),
% 43.36/6.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 43.36/6.08 fof(f46,hypothesis,(
% 43.36/6.08 ( aScalar0(xC)& xC = sdtasasdt0(xp,xp) ) ),
% 43.36/6.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 43.36/6.08 fof(f47,hypothesis,(
% 43.36/6.08 ( aScalar0(xD)& xD = sdtasasdt0(xq,xq) ) ),
% 43.36/6.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 43.36/6.08 fof(f48,hypothesis,(
% 43.36/6.08 ( aScalar0(xE)& xE = sdtasasdt0(xp,xq) ) ),
% 43.36/6.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 43.36/6.08 fof(f51,hypothesis,(
% 43.36/6.08 ( aScalar0(xH)& xH = sdtasdt0(xA,xB) ) ),
% 43.36/6.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 43.36/6.08 fof(f52,hypothesis,(
% 43.36/6.08 ( aScalar0(xR)& xR = sdtasdt0(xC,xG) ) ),
% 43.36/6.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 43.36/6.08 fof(f53,hypothesis,(
% 43.36/6.08 ( aScalar0(xP)& xP = sdtasdt0(xE,xH) ) ),
% 43.36/6.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 43.36/6.08 fof(f54,hypothesis,(
% 43.36/6.08 ( aScalar0(xS)& xS = sdtasdt0(xF,xD) ) ),
% 43.36/6.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 43.36/6.08 fof(f56,hypothesis,(
% 43.36/6.08 sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(xC,xD)) ),
% 43.36/6.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 43.36/6.08 fof(f57,hypothesis,(
% 43.36/6.08 sdtlseqdt0(sdtpldt0(xP,xP),sdtpldt0(xR,xS)) ),
% 43.36/6.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 43.36/6.08 fof(f58,conjecture,(
% 43.36/6.08 sdtlseqdt0(sdtpldt0(sdtasdt0(xE,xE),sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH))),sdtpldt0(sdtasdt0(xC,xD),sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))) ),
% 43.36/6.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 43.36/6.08 fof(f59,negated_conjecture,(
% 43.36/6.08 ~(sdtlseqdt0(sdtpldt0(sdtasdt0(xE,xE),sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH))),sdtpldt0(sdtasdt0(xC,xD),sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))) )),
% 43.36/6.08 inference(negated_conjecture,[status(cth)],[f58])).
% 43.36/6.08 fof(f81,plain,(
% 43.36/6.08 ![W0,W1]: ((~aScalar0(W0)|~aScalar0(W1))|aScalar0(sdtpldt0(W0,W1)))),
% 43.36/6.08 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 43.36/6.08 fof(f82,plain,(
% 43.36/6.08 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|aScalar0(sdtpldt0(X0,X1)))),
% 43.36/6.08 inference(cnf_transformation,[status(thm)],[f81])).
% 43.36/6.08 fof(f83,plain,(
% 43.36/6.08 ![W0,W1]: ((~aScalar0(W0)|~aScalar0(W1))|aScalar0(sdtasdt0(W0,W1)))),
% 43.36/6.08 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 43.36/6.08 fof(f84,plain,(
% 43.36/6.08 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|aScalar0(sdtasdt0(X0,X1)))),
% 43.36/6.08 inference(cnf_transformation,[status(thm)],[f83])).
% 43.36/6.08 fof(f113,plain,(
% 43.36/6.08 ![W0]: (~aScalar0(W0)|sdtlseqdt0(W0,W0))),
% 43.36/6.08 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 43.36/6.08 fof(f114,plain,(
% 43.36/6.08 ![X0]: (~aScalar0(X0)|sdtlseqdt0(X0,X0))),
% 43.36/6.08 inference(cnf_transformation,[status(thm)],[f113])).
% 43.36/6.08 fof(f119,plain,(
% 43.36/6.08 ![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))))),
% 43.36/6.08 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 43.36/6.08 fof(f120,plain,(
% 43.36/6.08 ![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)))),
% 43.36/6.08 inference(cnf_transformation,[status(thm)],[f119])).
% 43.36/6.08 fof(f178,plain,(
% 43.36/6.08 aScalar0(xC)),
% 43.36/6.08 inference(cnf_transformation,[status(thm)],[f46])).
% 43.36/6.08 fof(f180,plain,(
% 43.36/6.08 aScalar0(xD)),
% 43.36/6.08 inference(cnf_transformation,[status(thm)],[f47])).
% 43.36/6.08 fof(f182,plain,(
% 43.36/6.08 aScalar0(xE)),
% 43.36/6.08 inference(cnf_transformation,[status(thm)],[f48])).
% 43.36/6.08 fof(f188,plain,(
% 43.36/6.08 aScalar0(xH)),
% 43.36/6.08 inference(cnf_transformation,[status(thm)],[f51])).
% 43.36/6.08 fof(f190,plain,(
% 43.36/6.08 aScalar0(xR)),
% 43.36/6.08 inference(cnf_transformation,[status(thm)],[f52])).
% 43.36/6.08 fof(f192,plain,(
% 43.36/6.08 aScalar0(xP)),
% 43.36/6.08 inference(cnf_transformation,[status(thm)],[f53])).
% 43.36/6.08 fof(f194,plain,(
% 43.36/6.08 aScalar0(xS)),
% 43.36/6.08 inference(cnf_transformation,[status(thm)],[f54])).
% 43.36/6.08 fof(f198,plain,(
% 43.36/6.08 sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(xC,xD))),
% 43.36/6.08 inference(cnf_transformation,[status(thm)],[f56])).
% 43.36/6.08 fof(f199,plain,(
% 43.36/6.08 sdtlseqdt0(sdtpldt0(xP,xP),sdtpldt0(xR,xS))),
% 43.36/6.08 inference(cnf_transformation,[status(thm)],[f57])).
% 43.36/6.08 fof(f200,plain,(
% 43.36/6.08 ~sdtlseqdt0(sdtpldt0(sdtasdt0(xE,xE),sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH))),sdtpldt0(sdtasdt0(xC,xD),sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH))))),
% 43.36/6.08 inference(cnf_transformation,[status(thm)],[f59])).
% 43.36/6.08 fof(f1794,plain,(
% 43.36/6.08 ~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)))),
% 43.36/6.09 inference(resolution,[status(thm)],[f120,f200])).
% 43.36/6.09 fof(f1795,plain,(
% 43.36/6.09 ~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)))),
% 43.36/6.09 inference(forward_subsumption_resolution,[status(thm)],[f1794,f198])).
% 43.36/6.09 fof(f2178,plain,(
% 43.36/6.09 ~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)),
% 43.36/6.09 inference(resolution,[status(thm)],[f1795,f84])).
% 43.36/6.09 fof(f2179,plain,(
% 43.36/6.09 ~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)),
% 43.36/6.09 inference(duplicate_literals_removal,[status(thm)],[f2178])).
% 43.36/6.09 fof(f2180,plain,(
% 43.36/6.09 ~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)))),
% 43.36/6.09 inference(forward_subsumption_resolution,[status(thm)],[f2179,f182])).
% 43.36/6.09 fof(f2181,plain,(
% 43.36/6.09 ~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)),
% 43.36/6.09 inference(resolution,[status(thm)],[f2180,f84])).
% 43.36/6.09 fof(f2182,plain,(
% 43.36/6.09 ~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)),
% 43.36/6.09 inference(forward_subsumption_resolution,[status(thm)],[f2181,f178])).
% 43.36/6.09 fof(f2831,plain,(
% 43.36/6.09 ~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)))),
% 43.36/6.09 inference(forward_subsumption_resolution,[status(thm)],[f2182,f180])).
% 43.36/6.09 fof(f2832,plain,(
% 43.36/6.09 ~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))),
% 43.36/6.09 inference(resolution,[status(thm)],[f2831,f82])).
% 43.36/6.09 fof(f2833,plain,(
% 43.36/6.09 ~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)),
% 43.36/6.09 inference(resolution,[status(thm)],[f2832,f84])).
% 43.36/6.09 fof(f2834,plain,(
% 43.36/6.09 ~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)),
% 43.36/6.09 inference(duplicate_literals_removal,[status(thm)],[f2833])).
% 43.36/6.09 fof(f2835,plain,(
% 43.36/6.09 ~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))),
% 43.36/6.09 inference(forward_subsumption_resolution,[status(thm)],[f2834,f188])).
% 43.36/6.09 fof(f3291,plain,(
% 43.36/6.09 ~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))),
% 43.36/6.09 inference(resolution,[status(thm)],[f2835,f82])).
% 43.36/6.09 fof(f3292,plain,(
% 43.36/6.09 ~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)),
% 43.36/6.09 inference(resolution,[status(thm)],[f3291,f84])).
% 43.36/6.09 fof(f3293,plain,(
% 43.36/6.09 ~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)),
% 43.36/6.09 inference(duplicate_literals_removal,[status(thm)],[f3292])).
% 43.36/6.09 fof(f3294,plain,(
% 43.36/6.09 ~sdtlseqdt0(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)),sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))|~aScalar0(sdtpldt0(xP,xP))|~aScalar0(sdtpldt0(xR,xS))),
% 43.36/6.09 inference(forward_subsumption_resolution,[status(thm)],[f3293,f188])).
% 43.36/6.09 fof(f5510,plain,(
% 43.36/6.09 ~sdtlseqdt0(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)),sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))|~aScalar0(sdtpldt0(xR,xS))|~aScalar0(xP)|~aScalar0(xP)),
% 43.36/6.09 inference(resolution,[status(thm)],[f3294,f82])).
% 43.36/6.09 fof(f5511,plain,(
% 43.36/6.09 ~sdtlseqdt0(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)),sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))|~aScalar0(sdtpldt0(xR,xS))|~aScalar0(xP)),
% 43.36/6.09 inference(duplicate_literals_removal,[status(thm)],[f5510])).
% 43.36/6.09 fof(f5512,plain,(
% 43.36/6.09 ~sdtlseqdt0(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)),sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))|~aScalar0(sdtpldt0(xR,xS))),
% 43.36/6.09 inference(forward_subsumption_resolution,[status(thm)],[f5511,f192])).
% 43.36/6.09 fof(f5513,plain,(
% 43.36/6.09 ~sdtlseqdt0(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)),sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))|~aScalar0(xR)|~aScalar0(xS)),
% 43.36/6.09 inference(resolution,[status(thm)],[f5512,f82])).
% 43.36/6.09 fof(f5514,plain,(
% 43.36/6.09 ~sdtlseqdt0(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)),sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))|~aScalar0(xS)),
% 43.36/6.09 inference(forward_subsumption_resolution,[status(thm)],[f5513,f190])).
% 43.36/6.09 fof(f6779,plain,(
% 43.36/6.09 ~sdtlseqdt0(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)),sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))),
% 43.36/6.09 inference(forward_subsumption_resolution,[status(thm)],[f5514,f194])).
% 43.36/6.09 fof(f6780,plain,(
% 43.36/6.09 ~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))),
% 43.36/6.09 inference(resolution,[status(thm)],[f6779,f120])).
% 43.36/6.09 fof(f6782,plain,(
% 43.36/6.09 ~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))),
% 43.36/6.09 inference(duplicate_literals_removal,[status(thm)],[f6780])).
% 43.36/6.09 fof(f6783,plain,(
% 43.36/6.09 ~aScalar0(sdtpldt0(xP,xP))|~aScalar0(sdtpldt0(xR,xS))|~aScalar0(sdtasdt0(xH,xH))|~sdtlseqdt0(sdtasdt0(xH,xH),sdtasdt0(xH,xH))),
% 43.36/6.09 inference(forward_subsumption_resolution,[status(thm)],[f6782,f199])).
% 43.36/6.09 fof(f6784,plain,(
% 43.36/6.09 ~aScalar0(sdtpldt0(xP,xP))|~aScalar0(sdtpldt0(xR,xS))|~aScalar0(sdtasdt0(xH,xH))),
% 43.36/6.09 inference(forward_subsumption_resolution,[status(thm)],[f6783,f114])).
% 43.36/6.09 fof(f6785,plain,(
% 43.36/6.09 ~aScalar0(sdtpldt0(xP,xP))|~aScalar0(sdtpldt0(xR,xS))|~aScalar0(xH)|~aScalar0(xH)),
% 43.36/6.09 inference(resolution,[status(thm)],[f6784,f84])).
% 43.36/6.09 fof(f6786,plain,(
% 43.36/6.09 ~aScalar0(sdtpldt0(xP,xP))|~aScalar0(sdtpldt0(xR,xS))|~aScalar0(xH)),
% 43.36/6.09 inference(duplicate_literals_removal,[status(thm)],[f6785])).
% 43.36/6.09 fof(f6787,plain,(
% 43.36/6.09 ~aScalar0(sdtpldt0(xP,xP))|~aScalar0(sdtpldt0(xR,xS))),
% 43.36/6.09 inference(forward_subsumption_resolution,[status(thm)],[f6786,f188])).
% 43.36/6.09 fof(f6790,plain,(
% 43.36/6.09 ~aScalar0(sdtpldt0(xR,xS))|~aScalar0(xP)|~aScalar0(xP)),
% 43.36/6.12 inference(resolution,[status(thm)],[f6787,f82])).
% 43.36/6.12 fof(f6791,plain,(
% 43.36/6.12 ~aScalar0(sdtpldt0(xR,xS))|~aScalar0(xP)),
% 43.36/6.12 inference(duplicate_literals_removal,[status(thm)],[f6790])).
% 43.36/6.12 fof(f6792,plain,(
% 43.36/6.12 ~aScalar0(sdtpldt0(xR,xS))),
% 43.36/6.12 inference(forward_subsumption_resolution,[status(thm)],[f6791,f192])).
% 43.36/6.12 fof(f6793,plain,(
% 43.36/6.12 ~aScalar0(xR)|~aScalar0(xS)),
% 43.36/6.12 inference(resolution,[status(thm)],[f6792,f82])).
% 43.36/6.12 fof(f6794,plain,(
% 43.36/6.12 ~aScalar0(xS)),
% 43.36/6.12 inference(forward_subsumption_resolution,[status(thm)],[f6793,f190])).
% 43.36/6.12 fof(f6795,plain,(
% 43.36/6.12 $false),
% 43.36/6.12 inference(forward_subsumption_resolution,[status(thm)],[f6794,f194])).
% 43.36/6.12 % SZS output end CNFRefutation for theBenchmark.p
% 43.36/6.16 % Elapsed time: 5.726503 seconds
% 43.36/6.16 % CPU time: 44.841664 seconds
% 43.36/6.16 % Total memory used: 335.207 MB
% 43.36/6.16 % Net memory used: 317.775 MB
%------------------------------------------------------------------------------