%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : RNG080+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:18 PM UTC 2026
% Result : Theorem 38.13s 10.28s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG080+1 : 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.10/5.37 % Computer : n011.cluster.edu
% 0.10/5.37 % Model : x86_64 x86_64
% 0.10/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.37 % Memory : 8046.5625MB
% 0.10/5.37 % OS : Linux 6.8.0-71-generic
% 0.10/5.37 % CPULimit : 300
% 0.10/5.37 % WCLimit : 300
% 0.10/5.37 % DateTime : Mon Sep 21 04:18:46 UTC 2026
% 0.10/5.38 % CPUTime :
% 0.10/5.38 % Drodi V4.1.1
% 38.13/10.28 % Refutation found
% 38.13/10.28 % SZS status Theorem for theBenchmark: Theorem is valid
% 38.13/10.28 % SZS output start CNFRefutation for theBenchmark
% 38.13/10.28 fof(f9,axiom,(
% 38.13/10.28 aScalar0(sz0z00) ),
% 38.13/10.28 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 38.13/10.28 fof(f14,axiom,(
% 38.13/10.28 (! [W0,W1,W2] :( ( aScalar0(W0)& aScalar0(W1)& aScalar0(W2) )=> ( sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2))& sdtpldt0(W0,W1) = sdtpldt0(W1,W0)& sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2))& sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) ) )),
% 38.13/10.28 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 38.13/10.28 fof(f34,axiom,(
% 38.13/10.28 (! [W0,W1] :( ( aVector0(W0)& aVector0(W1) )=> ( aDimensionOf0(W0) = aDimensionOf0(W1)=> aScalar0(sdtasasdt0(W0,W1)) ) ) )),
% 38.13/10.28 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 38.13/10.28 fof(f36,axiom,(
% 38.13/10.28 (! [W0,W1] :( ( aVector0(W0)& aVector0(W1) )=> ( ( aDimensionOf0(W0) = aDimensionOf0(W1)& aDimensionOf0(W1) != sz00 )=> sdtasasdt0(W0,W1) = sdtpldt0(sdtasasdt0(sziznziztdt0(W0),sziznziztdt0(W1)),sdtasdt0(sdtlbdtrb0(W0,aDimensionOf0(W0)),sdtlbdtrb0(W1,aDimensionOf0(W1)))) ) ) )),
% 38.13/10.28 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 38.13/10.28 fof(f38,hypothesis,(
% 38.13/10.28 ( aVector0(xs)& aVector0(xt) ) ),
% 38.13/10.28 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 38.13/10.28 fof(f40,hypothesis,(
% 38.13/10.28 aDimensionOf0(xs) = aDimensionOf0(xt) ),
% 38.13/10.28 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 38.13/10.28 fof(f41,hypothesis,(
% 38.13/10.28 aDimensionOf0(xs) != sz00 ),
% 38.13/10.28 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 38.13/10.28 fof(f42,hypothesis,(
% 38.13/10.28 ( aVector0(xp)& xp = sziznziztdt0(xs) ) ),
% 38.13/10.28 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 38.13/10.28 fof(f43,hypothesis,(
% 38.13/10.28 ( aVector0(xq)& xq = sziznziztdt0(xt) ) ),
% 38.13/10.28 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 38.13/10.28 fof(f44,hypothesis,(
% 38.13/10.28 ( aScalar0(xA)& xA = sdtlbdtrb0(xs,aDimensionOf0(xs)) ) ),
% 38.13/10.28 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 38.13/10.28 fof(f45,hypothesis,(
% 38.13/10.28 ( aScalar0(xB)& xB = sdtlbdtrb0(xt,aDimensionOf0(xt)) ) ),
% 38.13/10.28 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 38.13/10.28 fof(f46,hypothesis,(
% 38.13/10.28 ( aScalar0(xC)& xC = sdtasasdt0(xp,xp) ) ),
% 38.13/10.28 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 38.13/10.28 fof(f47,hypothesis,(
% 38.13/10.28 ( aScalar0(xD)& xD = sdtasasdt0(xq,xq) ) ),
% 38.13/10.28 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 38.13/10.28 fof(f48,hypothesis,(
% 38.13/10.28 ( aScalar0(xE)& xE = sdtasasdt0(xp,xq) ) ),
% 38.13/10.28 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 38.13/10.28 fof(f49,hypothesis,(
% 38.13/10.28 ( aScalar0(xF)& xF = sdtasdt0(xA,xA) ) ),
% 38.13/10.28 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 38.13/10.28 fof(f50,hypothesis,(
% 38.13/10.28 ( aScalar0(xG)& xG = sdtasdt0(xB,xB) ) ),
% 38.13/10.28 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 38.13/10.28 fof(f51,hypothesis,(
% 38.13/10.28 ( aScalar0(xH)& xH = sdtasdt0(xA,xB) ) ),
% 38.13/10.28 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 38.13/10.28 fof(f58,hypothesis,(
% 38.13/10.28 sdtlseqdt0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)),sdtasdt0(sdtpldt0(xC,xF),sdtpldt0(xD,xG))) ),
% 38.13/10.28 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 38.13/10.28 fof(f59,conjecture,(
% 38.13/10.28 sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt))) ),
% 38.13/10.28 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 38.13/10.28 fof(f60,negated_conjecture,(
% 38.13/10.28 ~(sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt))) )),
% 38.13/10.28 inference(negated_conjecture,[status(cth)],[f59])).
% 38.13/10.28 fof(f81,plain,(
% 38.13/10.28 aScalar0(sz0z00)),
% 38.13/10.28 inference(cnf_transformation,[status(thm)],[f9])).
% 38.13/10.28 fof(f97,plain,(
% 38.13/10.28 ![W0,W1,W2]: (((~aScalar0(W0)|~aScalar0(W1))|~aScalar0(W2))|(((sdtpldt0(sdtpldt0(W0,W1),W2)=sdtpldt0(W0,sdtpldt0(W1,W2))&sdtpldt0(W0,W1)=sdtpldt0(W1,W0))&sdtasdt0(sdtasdt0(W0,W1),W2)=sdtasdt0(W0,sdtasdt0(W1,W2)))&sdtasdt0(W0,W1)=sdtasdt0(W1,W0)))),
% 38.13/10.28 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 38.13/10.28 fof(f101,plain,(
% 38.13/10.28 ![X0,X1,X2]: (~aScalar0(X0)|~aScalar0(X1)|~aScalar0(X2)|sdtasdt0(X0,X1)=sdtasdt0(X1,X0))),
% 38.13/10.28 inference(cnf_transformation,[status(thm)],[f97])).
% 38.13/10.28 fof(f151,plain,(
% 38.13/10.28 ![W0,W1]: ((~aVector0(W0)|~aVector0(W1))|(~aDimensionOf0(W0)=aDimensionOf0(W1)|aScalar0(sdtasasdt0(W0,W1))))),
% 38.13/10.28 inference(pre_NNF_transformation,[status(thm)],[f34])).
% 38.13/10.28 fof(f152,plain,(
% 38.13/10.28 ![X0,X1]: (~aVector0(X0)|~aVector0(X1)|~aDimensionOf0(X0)=aDimensionOf0(X1)|aScalar0(sdtasasdt0(X0,X1)))),
% 38.13/10.28 inference(cnf_transformation,[status(thm)],[f151])).
% 38.13/10.28 fof(f155,plain,(
% 38.13/10.28 ![W0,W1]: ((~aVector0(W0)|~aVector0(W1))|((~aDimensionOf0(W0)=aDimensionOf0(W1)|aDimensionOf0(W1)=sz00)|sdtasasdt0(W0,W1)=sdtpldt0(sdtasasdt0(sziznziztdt0(W0),sziznziztdt0(W1)),sdtasdt0(sdtlbdtrb0(W0,aDimensionOf0(W0)),sdtlbdtrb0(W1,aDimensionOf0(W1))))))),
% 38.13/10.28 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 38.13/10.28 fof(f156,plain,(
% 38.13/10.28 ![X0,X1]: (~aVector0(X0)|~aVector0(X1)|~aDimensionOf0(X0)=aDimensionOf0(X1)|aDimensionOf0(X1)=sz00|sdtasasdt0(X0,X1)=sdtpldt0(sdtasasdt0(sziznziztdt0(X0),sziznziztdt0(X1)),sdtasdt0(sdtlbdtrb0(X0,aDimensionOf0(X0)),sdtlbdtrb0(X1,aDimensionOf0(X1)))))),
% 38.13/10.28 inference(cnf_transformation,[status(thm)],[f155])).
% 38.13/10.28 fof(f159,plain,(
% 38.13/10.28 aVector0(xs)),
% 38.13/10.28 inference(cnf_transformation,[status(thm)],[f38])).
% 38.13/10.28 fof(f160,plain,(
% 38.13/10.28 aVector0(xt)),
% 38.13/10.28 inference(cnf_transformation,[status(thm)],[f38])).
% 38.13/10.28 fof(f163,plain,(
% 38.13/10.28 aDimensionOf0(xs)=aDimensionOf0(xt)),
% 38.13/10.28 inference(cnf_transformation,[status(thm)],[f40])).
% 38.13/10.28 fof(f164,plain,(
% 38.13/10.28 ~aDimensionOf0(xs)=sz00),
% 38.13/10.28 inference(cnf_transformation,[status(thm)],[f41])).
% 38.13/10.28 fof(f166,plain,(
% 38.13/10.28 xp=sziznziztdt0(xs)),
% 38.13/10.28 inference(cnf_transformation,[status(thm)],[f42])).
% 38.13/10.28 fof(f168,plain,(
% 38.13/10.28 xq=sziznziztdt0(xt)),
% 38.13/10.28 inference(cnf_transformation,[status(thm)],[f43])).
% 38.13/10.28 fof(f170,plain,(
% 38.13/10.28 xA=sdtlbdtrb0(xs,aDimensionOf0(xs))),
% 38.13/10.28 inference(cnf_transformation,[status(thm)],[f44])).
% 38.13/10.28 fof(f172,plain,(
% 38.13/10.28 xB=sdtlbdtrb0(xt,aDimensionOf0(xt))),
% 38.13/10.28 inference(cnf_transformation,[status(thm)],[f45])).
% 38.13/10.28 fof(f174,plain,(
% 38.13/10.28 xC=sdtasasdt0(xp,xp)),
% 38.13/10.28 inference(cnf_transformation,[status(thm)],[f46])).
% 38.13/10.28 fof(f176,plain,(
% 38.13/10.28 xD=sdtasasdt0(xq,xq)),
% 38.13/10.28 inference(cnf_transformation,[status(thm)],[f47])).
% 38.13/10.28 fof(f178,plain,(
% 38.13/10.28 xE=sdtasasdt0(xp,xq)),
% 38.13/10.28 inference(cnf_transformation,[status(thm)],[f48])).
% 38.13/10.28 fof(f180,plain,(
% 38.13/10.28 xF=sdtasdt0(xA,xA)),
% 38.13/10.28 inference(cnf_transformation,[status(thm)],[f49])).
% 38.13/10.28 fof(f182,plain,(
% 38.13/10.28 xG=sdtasdt0(xB,xB)),
% 38.13/10.28 inference(cnf_transformation,[status(thm)],[f50])).
% 38.13/10.28 fof(f184,plain,(
% 38.13/10.28 xH=sdtasdt0(xA,xB)),
% 38.13/10.28 inference(cnf_transformation,[status(thm)],[f51])).
% 38.13/10.28 fof(f195,plain,(
% 38.13/10.28 sdtlseqdt0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)),sdtasdt0(sdtpldt0(xC,xF),sdtpldt0(xD,xG)))),
% 38.13/10.28 inference(cnf_transformation,[status(thm)],[f58])).
% 38.13/10.28 fof(f196,plain,(
% 38.13/10.28 ~sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt)))),
% 38.13/10.28 inference(cnf_transformation,[status(thm)],[f60])).
% 38.13/10.28 fof(f201,plain,(
% 38.13/10.28 ~aDimensionOf0(xt)=sz00),
% 38.13/10.28 inference(forward_demodulation,[status(thm)],[f163,f164])).
% 38.13/10.28 fof(f202,plain,(
% 38.13/10.28 xA=sdtlbdtrb0(xs,aDimensionOf0(xt))),
% 38.13/10.28 inference(forward_demodulation,[status(thm)],[f163,f170])).
% 38.13/10.28 fof(f203,plain,(
% 38.13/10.28 ![X0]: (~aVector0(X0)|~aDimensionOf0(X0)=aDimensionOf0(xt)|aScalar0(sdtasasdt0(X0,xt)))),
% 38.13/10.28 inference(resolution,[status(thm)],[f152,f160])).
% 38.13/10.28 fof(f204,plain,(
% 38.13/10.28 ![X0]: (~aVector0(X0)|~aDimensionOf0(X0)=aDimensionOf0(xs)|aScalar0(sdtasasdt0(X0,xs)))),
% 38.13/10.28 inference(resolution,[status(thm)],[f152,f159])).
% 38.13/10.28 fof(f205,plain,(
% 38.13/10.28 ![X0]: (~aVector0(X0)|~aDimensionOf0(X0)=aDimensionOf0(xt)|aScalar0(sdtasasdt0(X0,xs)))),
% 38.13/10.28 inference(forward_demodulation,[status(thm)],[f163,f204])).
% 38.13/10.28 fof(f226,plain,(
% 38.13/10.28 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|sdtasdt0(X0,X1)=sdtasdt0(X1,X0))),
% 38.13/10.28 inference(resolution,[status(thm)],[f81,f101])).
% 38.13/10.28 fof(f239,plain,(
% 38.13/10.28 ~aDimensionOf0(xt)=aDimensionOf0(xt)|aScalar0(sdtasasdt0(xt,xt))),
% 38.13/10.28 inference(resolution,[status(thm)],[f203,f160])).
% 38.13/10.28 fof(f241,plain,(
% 38.13/10.28 aScalar0(sdtasasdt0(xt,xt))),
% 38.13/10.28 inference(trivial_equality_resolution,[status(thm)],[f239])).
% 38.13/10.28 fof(f245,plain,(
% 38.13/10.28 ~aDimensionOf0(xs)=aDimensionOf0(xt)|aScalar0(sdtasasdt0(xs,xs))),
% 38.13/10.28 inference(resolution,[status(thm)],[f205,f159])).
% 38.13/10.28 fof(f247,plain,(
% 38.13/10.28 ~aDimensionOf0(xt)=aDimensionOf0(xt)|aScalar0(sdtasasdt0(xs,xs))),
% 38.13/10.28 inference(forward_demodulation,[status(thm)],[f163,f245])).
% 38.13/10.28 fof(f248,plain,(
% 38.13/10.28 aScalar0(sdtasasdt0(xs,xs))),
% 38.13/10.28 inference(trivial_equality_resolution,[status(thm)],[f247])).
% 38.13/10.28 fof(f261,plain,(
% 38.13/10.28 ![X0]: (~aScalar0(X0)|sdtasdt0(X0,sdtasasdt0(xt,xt))=sdtasdt0(sdtasasdt0(xt,xt),X0))),
% 38.13/10.28 inference(resolution,[status(thm)],[f241,f226])).
% 38.13/10.28 fof(f488,plain,(
% 38.13/10.28 sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt))=sdtasdt0(sdtasasdt0(xt,xt),sdtasasdt0(xs,xs))),
% 38.13/10.28 inference(resolution,[status(thm)],[f261,f248])).
% 38.13/10.28 fof(f493,plain,(
% 38.13/10.28 ~sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xt,xt),sdtasasdt0(xs,xs)))),
% 38.13/10.28 inference(backward_demodulation,[status(thm)],[f488,f196])).
% 38.13/10.28 fof(f781,plain,(
% 38.13/10.28 ![X0]: (~aVector0(X0)|~aDimensionOf0(X0)=aDimensionOf0(xt)|aDimensionOf0(xt)=sz00|sdtasasdt0(X0,xt)=sdtpldt0(sdtasasdt0(sziznziztdt0(X0),sziznziztdt0(xt)),sdtasdt0(sdtlbdtrb0(X0,aDimensionOf0(X0)),sdtlbdtrb0(xt,aDimensionOf0(xt)))))),
% 38.13/10.28 inference(resolution,[status(thm)],[f156,f160])).
% 38.13/10.28 fof(f782,plain,(
% 38.13/10.28 ![X0]: (~aVector0(X0)|~aDimensionOf0(X0)=aDimensionOf0(xs)|aDimensionOf0(xs)=sz00|sdtasasdt0(X0,xs)=sdtpldt0(sdtasasdt0(sziznziztdt0(X0),sziznziztdt0(xs)),sdtasdt0(sdtlbdtrb0(X0,aDimensionOf0(X0)),sdtlbdtrb0(xs,aDimensionOf0(xs)))))),
% 38.13/10.28 inference(resolution,[status(thm)],[f156,f159])).
% 38.13/10.28 fof(f783,plain,(
% 38.13/10.28 ![X0]: (~aVector0(X0)|~aDimensionOf0(X0)=aDimensionOf0(xt)|aDimensionOf0(xt)=sz00|sdtasasdt0(X0,xt)=sdtpldt0(sdtasasdt0(sziznziztdt0(X0),xq),sdtasdt0(sdtlbdtrb0(X0,aDimensionOf0(X0)),sdtlbdtrb0(xt,aDimensionOf0(xt)))))),
% 38.13/10.28 inference(forward_demodulation,[status(thm)],[f168,f781])).
% 38.13/10.28 fof(f784,plain,(
% 38.13/10.28 ![X0]: (~aVector0(X0)|~aDimensionOf0(X0)=aDimensionOf0(xt)|aDimensionOf0(xt)=sz00|sdtasasdt0(X0,xt)=sdtpldt0(sdtasasdt0(sziznziztdt0(X0),xq),sdtasdt0(sdtlbdtrb0(X0,aDimensionOf0(X0)),xB)))),
% 38.13/10.28 inference(forward_demodulation,[status(thm)],[f172,f783])).
% 38.13/10.28 fof(f785,plain,(
% 38.13/10.28 ![X0]: (~aVector0(X0)|~aDimensionOf0(X0)=aDimensionOf0(xt)|sdtasasdt0(X0,xt)=sdtpldt0(sdtasasdt0(sziznziztdt0(X0),xq),sdtasdt0(sdtlbdtrb0(X0,aDimensionOf0(X0)),xB)))),
% 38.13/10.28 inference(forward_subsumption_resolution,[status(thm)],[f784,f201])).
% 38.13/10.28 fof(f786,plain,(
% 38.13/10.28 ![X0]: (~aVector0(X0)|~aDimensionOf0(X0)=aDimensionOf0(xt)|aDimensionOf0(xs)=sz00|sdtasasdt0(X0,xs)=sdtpldt0(sdtasasdt0(sziznziztdt0(X0),sziznziztdt0(xs)),sdtasdt0(sdtlbdtrb0(X0,aDimensionOf0(X0)),sdtlbdtrb0(xs,aDimensionOf0(xs)))))),
% 38.13/10.28 inference(forward_demodulation,[status(thm)],[f163,f782])).
% 38.13/10.28 fof(f787,plain,(
% 38.13/10.28 ![X0]: (~aVector0(X0)|~aDimensionOf0(X0)=aDimensionOf0(xt)|aDimensionOf0(xt)=sz00|sdtasasdt0(X0,xs)=sdtpldt0(sdtasasdt0(sziznziztdt0(X0),sziznziztdt0(xs)),sdtasdt0(sdtlbdtrb0(X0,aDimensionOf0(X0)),sdtlbdtrb0(xs,aDimensionOf0(xs)))))),
% 38.13/10.28 inference(forward_demodulation,[status(thm)],[f163,f786])).
% 38.13/10.28 fof(f788,plain,(
% 38.13/10.28 ![X0]: (~aVector0(X0)|~aDimensionOf0(X0)=aDimensionOf0(xt)|aDimensionOf0(xt)=sz00|sdtasasdt0(X0,xs)=sdtpldt0(sdtasasdt0(sziznziztdt0(X0),xp),sdtasdt0(sdtlbdtrb0(X0,aDimensionOf0(X0)),sdtlbdtrb0(xs,aDimensionOf0(xs)))))),
% 38.13/10.28 inference(forward_demodulation,[status(thm)],[f166,f787])).
% 38.13/10.28 fof(f789,plain,(
% 38.13/10.28 ![X0]: (~aVector0(X0)|~aDimensionOf0(X0)=aDimensionOf0(xt)|aDimensionOf0(xt)=sz00|sdtasasdt0(X0,xs)=sdtpldt0(sdtasasdt0(sziznziztdt0(X0),xp),sdtasdt0(sdtlbdtrb0(X0,aDimensionOf0(X0)),sdtlbdtrb0(xs,aDimensionOf0(xt)))))),
% 38.13/10.28 inference(forward_demodulation,[status(thm)],[f163,f788])).
% 38.13/10.28 fof(f790,plain,(
% 38.13/10.28 ![X0]: (~aVector0(X0)|~aDimensionOf0(X0)=aDimensionOf0(xt)|aDimensionOf0(xt)=sz00|sdtasasdt0(X0,xs)=sdtpldt0(sdtasasdt0(sziznziztdt0(X0),xp),sdtasdt0(sdtlbdtrb0(X0,aDimensionOf0(X0)),xA)))),
% 38.13/10.28 inference(forward_demodulation,[status(thm)],[f202,f789])).
% 38.13/10.28 fof(f791,plain,(
% 38.13/10.28 ![X0]: (~aVector0(X0)|~aDimensionOf0(X0)=aDimensionOf0(xt)|sdtasasdt0(X0,xs)=sdtpldt0(sdtasasdt0(sziznziztdt0(X0),xp),sdtasdt0(sdtlbdtrb0(X0,aDimensionOf0(X0)),xA)))),
% 38.13/10.28 inference(forward_subsumption_resolution,[status(thm)],[f790,f201])).
% 38.13/10.28 fof(f2548,plain,(
% 38.13/10.28 ~aDimensionOf0(xt)=aDimensionOf0(xt)|sdtasasdt0(xt,xt)=sdtpldt0(sdtasasdt0(sziznziztdt0(xt),xq),sdtasdt0(sdtlbdtrb0(xt,aDimensionOf0(xt)),xB))),
% 38.13/10.28 inference(resolution,[status(thm)],[f785,f160])).
% 38.13/10.28 fof(f2549,plain,(
% 38.13/10.28 ~aDimensionOf0(xs)=aDimensionOf0(xt)|sdtasasdt0(xs,xt)=sdtpldt0(sdtasasdt0(sziznziztdt0(xs),xq),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),xB))),
% 38.13/10.28 inference(resolution,[status(thm)],[f785,f159])).
% 38.13/10.28 fof(f2552,plain,(
% 38.13/10.28 ~aDimensionOf0(xt)=aDimensionOf0(xt)|sdtasasdt0(xt,xt)=sdtpldt0(sdtasasdt0(xq,xq),sdtasdt0(sdtlbdtrb0(xt,aDimensionOf0(xt)),xB))),
% 38.13/10.28 inference(forward_demodulation,[status(thm)],[f168,f2548])).
% 38.13/10.28 fof(f2553,plain,(
% 38.13/10.28 ~aDimensionOf0(xt)=aDimensionOf0(xt)|sdtasasdt0(xt,xt)=sdtpldt0(xD,sdtasdt0(sdtlbdtrb0(xt,aDimensionOf0(xt)),xB))),
% 38.13/10.28 inference(forward_demodulation,[status(thm)],[f176,f2552])).
% 38.13/10.28 fof(f2554,plain,(
% 38.13/10.28 ~aDimensionOf0(xt)=aDimensionOf0(xt)|sdtasasdt0(xt,xt)=sdtpldt0(xD,sdtasdt0(xB,xB))),
% 38.13/10.28 inference(forward_demodulation,[status(thm)],[f172,f2553])).
% 38.13/10.28 fof(f2555,plain,(
% 38.13/10.28 ~aDimensionOf0(xt)=aDimensionOf0(xt)|sdtasasdt0(xt,xt)=sdtpldt0(xD,xG)),
% 38.13/10.28 inference(forward_demodulation,[status(thm)],[f182,f2554])).
% 38.13/10.28 fof(f2556,plain,(
% 38.13/10.28 sdtlseqdt0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)),sdtasdt0(sdtpldt0(xC,xF),sdtasasdt0(xt,xt)))),
% 38.13/10.28 inference(backward_demodulation,[status(thm)],[f2557,f195])).
% 38.13/10.28 fof(f2557,plain,(
% 38.13/10.28 sdtasasdt0(xt,xt)=sdtpldt0(xD,xG)),
% 38.13/10.28 inference(trivial_equality_resolution,[status(thm)],[f2555])).
% 38.13/10.28 fof(f2558,plain,(
% 38.13/10.28 ~aDimensionOf0(xt)=aDimensionOf0(xt)|sdtasasdt0(xs,xt)=sdtpldt0(sdtasasdt0(sziznziztdt0(xs),xq),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),xB))),
% 38.13/10.28 inference(forward_demodulation,[status(thm)],[f163,f2549])).
% 38.13/10.28 fof(f2559,plain,(
% 38.13/10.28 ~aDimensionOf0(xt)=aDimensionOf0(xt)|sdtasasdt0(xs,xt)=sdtpldt0(sdtasasdt0(xp,xq),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),xB))),
% 38.13/10.28 inference(forward_demodulation,[status(thm)],[f166,f2558])).
% 38.13/10.28 fof(f2560,plain,(
% 38.13/10.28 ~aDimensionOf0(xt)=aDimensionOf0(xt)|sdtasasdt0(xs,xt)=sdtpldt0(xE,sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),xB))),
% 38.13/10.28 inference(forward_demodulation,[status(thm)],[f178,f2559])).
% 38.13/10.28 fof(f2561,plain,(
% 38.13/10.28 ~aDimensionOf0(xt)=aDimensionOf0(xt)|sdtasasdt0(xs,xt)=sdtpldt0(xE,sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xt)),xB))),
% 38.13/10.28 inference(forward_demodulation,[status(thm)],[f163,f2560])).
% 38.13/10.28 fof(f2562,plain,(
% 38.13/10.28 ~aDimensionOf0(xt)=aDimensionOf0(xt)|sdtasasdt0(xs,xt)=sdtpldt0(xE,sdtasdt0(xA,xB))),
% 38.13/10.28 inference(forward_demodulation,[status(thm)],[f202,f2561])).
% 38.13/10.28 fof(f2563,plain,(
% 38.13/10.28 ~aDimensionOf0(xt)=aDimensionOf0(xt)|sdtasasdt0(xs,xt)=sdtpldt0(xE,xH)),
% 38.13/10.28 inference(forward_demodulation,[status(thm)],[f184,f2562])).
% 38.13/10.28 fof(f2564,plain,(
% 38.13/10.28 sdtasasdt0(xs,xt)=sdtpldt0(xE,xH)),
% 38.13/10.28 inference(trivial_equality_resolution,[status(thm)],[f2563])).
% 38.13/10.28 fof(f2565,plain,(
% 38.13/10.28 sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtpldt0(xE,xH)),sdtasdt0(sdtpldt0(xC,xF),sdtasasdt0(xt,xt)))),
% 38.13/10.28 inference(forward_demodulation,[status(thm)],[f2564,f2556])).
% 38.13/10.28 fof(f2566,plain,(
% 38.13/10.28 sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtpldt0(xC,xF),sdtasasdt0(xt,xt)))),
% 38.13/10.28 inference(forward_demodulation,[status(thm)],[f2564,f2565])).
% 38.13/10.28 fof(f3142,plain,(
% 38.13/10.28 ~aDimensionOf0(xs)=aDimensionOf0(xt)|sdtasasdt0(xs,xs)=sdtpldt0(sdtasasdt0(sziznziztdt0(xs),xp),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),xA))),
% 38.13/10.28 inference(resolution,[status(thm)],[f791,f159])).
% 38.13/10.28 fof(f3148,plain,(
% 38.13/10.28 ~aDimensionOf0(xt)=aDimensionOf0(xt)|sdtasasdt0(xs,xs)=sdtpldt0(sdtasasdt0(sziznziztdt0(xs),xp),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),xA))),
% 38.13/10.28 inference(forward_demodulation,[status(thm)],[f163,f3142])).
% 38.13/10.28 fof(f3149,plain,(
% 38.13/10.28 ~aDimensionOf0(xt)=aDimensionOf0(xt)|sdtasasdt0(xs,xs)=sdtpldt0(sdtasasdt0(xp,xp),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),xA))),
% 38.13/10.28 inference(forward_demodulation,[status(thm)],[f166,f3148])).
% 38.13/10.28 fof(f3150,plain,(
% 38.13/10.28 ~aDimensionOf0(xt)=aDimensionOf0(xt)|sdtasasdt0(xs,xs)=sdtpldt0(xC,sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),xA))),
% 38.13/10.28 inference(forward_demodulation,[status(thm)],[f174,f3149])).
% 38.13/10.28 fof(f3151,plain,(
% 38.13/10.28 ~aDimensionOf0(xt)=aDimensionOf0(xt)|sdtasasdt0(xs,xs)=sdtpldt0(xC,sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xt)),xA))),
% 38.13/10.28 inference(forward_demodulation,[status(thm)],[f163,f3150])).
% 38.13/10.28 fof(f3152,plain,(
% 38.13/10.28 ~aDimensionOf0(xt)=aDimensionOf0(xt)|sdtasasdt0(xs,xs)=sdtpldt0(xC,sdtasdt0(xA,xA))),
% 38.13/10.28 inference(forward_demodulation,[status(thm)],[f202,f3151])).
% 38.13/10.28 fof(f3153,plain,(
% 38.13/10.28 ~aDimensionOf0(xt)=aDimensionOf0(xt)|sdtasasdt0(xs,xs)=sdtpldt0(xC,xF)),
% 22.04/10.32 inference(forward_demodulation,[status(thm)],[f180,f3152])).
% 22.04/10.32 fof(f3154,plain,(
% 22.04/10.32 sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt)))),
% 22.04/10.32 inference(backward_demodulation,[status(thm)],[f3155,f2566])).
% 22.04/10.32 fof(f3155,plain,(
% 22.04/10.32 sdtasasdt0(xs,xs)=sdtpldt0(xC,xF)),
% 22.04/10.32 inference(trivial_equality_resolution,[status(thm)],[f3153])).
% 22.04/10.32 fof(f3156,plain,(
% 22.04/10.32 sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xt,xt),sdtasasdt0(xs,xs)))),
% 22.04/10.32 inference(forward_demodulation,[status(thm)],[f488,f3154])).
% 22.04/10.32 fof(f3157,plain,(
% 22.04/10.32 $false),
% 22.04/10.32 inference(forward_subsumption_resolution,[status(thm)],[f3156,f493])).
% 22.04/10.32 % SZS output end CNFRefutation for theBenchmark.p
% 22.04/10.34 % Elapsed time: 4.944495 seconds
% 22.04/10.34 % CPU time: 39.077066 seconds
% 22.04/10.34 % Total memory used: 477.009 MB
% 22.04/10.34 % Net memory used: 452.548 MB
%------------------------------------------------------------------------------