%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : RNG080+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 : n001.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 53.57s 12.23s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG080+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/5.38 % Computer : n001.cluster.edu
% 0.11/5.38 % Model : x86_64 x86_64
% 0.11/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.38 % Memory : 8046.5625MB
% 0.11/5.38 % OS : Linux 6.8.0-71-generic
% 0.11/5.38 % CPULimit : 300
% 0.11/5.38 % WCLimit : 300
% 0.11/5.38 % DateTime : Mon Sep 21 04:24:04 UTC 2026
% 0.11/5.39 % CPUTime :
% 0.16/5.41 % Drodi V4.1.1
% 53.57/12.23 % Refutation found
% 53.57/12.23 % SZS status Theorem for theBenchmark: Theorem is valid
% 53.57/12.23 % SZS output start CNFRefutation for theBenchmark
% 53.57/12.23 fof(f9,axiom,(
% 53.57/12.23 aScalar0(sz0z00) ),
% 53.57/12.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.57/12.23 fof(f14,axiom,(
% 53.57/12.23 (! [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) ) ) )),
% 53.57/12.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.57/12.23 fof(f34,axiom,(
% 53.57/12.23 (! [W0,W1] :( ( aVector0(W0)& aVector0(W1) )=> ( aDimensionOf0(W0) = aDimensionOf0(W1)=> aScalar0(sdtasasdt0(W0,W1)) ) ) )),
% 53.57/12.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.57/12.23 fof(f36,axiom,(
% 53.57/12.23 (! [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)))) ) ) )),
% 53.57/12.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.57/12.23 fof(f38,hypothesis,(
% 53.57/12.23 ( aVector0(xs)& aVector0(xt) ) ),
% 53.57/12.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.57/12.23 fof(f40,hypothesis,(
% 53.57/12.23 aDimensionOf0(xs) = aDimensionOf0(xt) ),
% 53.57/12.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.57/12.23 fof(f41,hypothesis,(
% 53.57/12.23 aDimensionOf0(xs) != sz00 ),
% 53.57/12.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.57/12.23 fof(f42,hypothesis,(
% 53.57/12.23 ( aVector0(xp)& szszuzczcdt0(aDimensionOf0(xp)) = aDimensionOf0(xs)& (! [W0] :( aNaturalNumber0(W0)=> sdtlbdtrb0(xp,W0) = sdtlbdtrb0(xs,W0) ))& xp = sziznziztdt0(xs) ) ),
% 53.57/12.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.57/12.23 fof(f43,hypothesis,(
% 53.57/12.23 ( aVector0(xq)& szszuzczcdt0(aDimensionOf0(xq)) = aDimensionOf0(xt)& (! [W0] :( aNaturalNumber0(W0)=> sdtlbdtrb0(xq,W0) = sdtlbdtrb0(xt,W0) ))& xq = sziznziztdt0(xt) ) ),
% 53.57/12.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.57/12.23 fof(f44,hypothesis,(
% 53.57/12.23 ( aScalar0(xA)& xA = sdtlbdtrb0(xs,aDimensionOf0(xs)) ) ),
% 53.57/12.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.57/12.23 fof(f45,hypothesis,(
% 53.57/12.23 ( aScalar0(xB)& xB = sdtlbdtrb0(xt,aDimensionOf0(xt)) ) ),
% 53.57/12.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.57/12.23 fof(f46,hypothesis,(
% 53.57/12.23 ( aScalar0(xC)& xC = sdtasasdt0(xp,xp) ) ),
% 53.57/12.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.57/12.23 fof(f47,hypothesis,(
% 53.57/12.23 ( aScalar0(xD)& xD = sdtasasdt0(xq,xq) ) ),
% 53.57/12.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.57/12.23 fof(f48,hypothesis,(
% 53.57/12.23 ( aScalar0(xE)& xE = sdtasasdt0(xp,xq) ) ),
% 53.57/12.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.57/12.23 fof(f49,hypothesis,(
% 53.57/12.23 ( aScalar0(xF)& xF = sdtasdt0(xA,xA) ) ),
% 53.57/12.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.57/12.23 fof(f50,hypothesis,(
% 53.57/12.23 ( aScalar0(xG)& xG = sdtasdt0(xB,xB) ) ),
% 53.57/12.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.57/12.23 fof(f51,hypothesis,(
% 53.57/12.23 ( aScalar0(xH)& xH = sdtasdt0(xA,xB) ) ),
% 53.57/12.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.57/12.23 fof(f58,hypothesis,(
% 53.57/12.23 sdtlseqdt0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)),sdtasdt0(sdtpldt0(xC,xF),sdtpldt0(xD,xG))) ),
% 53.57/12.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.57/12.23 fof(f59,conjecture,(
% 53.57/12.23 sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt))) ),
% 53.57/12.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.57/12.23 fof(f60,negated_conjecture,(
% 53.57/12.23 ~(sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt))) )),
% 53.57/12.23 inference(negated_conjecture,[status(cth)],[f59])).
% 53.57/12.23 fof(f81,plain,(
% 53.57/12.23 aScalar0(sz0z00)),
% 53.57/12.23 inference(cnf_transformation,[status(thm)],[f9])).
% 53.57/12.23 fof(f97,plain,(
% 53.57/12.23 ![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)))),
% 53.57/12.23 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 53.57/12.23 fof(f101,plain,(
% 53.57/12.23 ![X0,X1,X2]: (~aScalar0(X0)|~aScalar0(X1)|~aScalar0(X2)|sdtasdt0(X0,X1)=sdtasdt0(X1,X0))),
% 53.57/12.23 inference(cnf_transformation,[status(thm)],[f97])).
% 53.57/12.23 fof(f151,plain,(
% 53.57/12.23 ![W0,W1]: ((~aVector0(W0)|~aVector0(W1))|(~aDimensionOf0(W0)=aDimensionOf0(W1)|aScalar0(sdtasasdt0(W0,W1))))),
% 53.57/12.23 inference(pre_NNF_transformation,[status(thm)],[f34])).
% 53.57/12.23 fof(f152,plain,(
% 53.57/12.23 ![X0,X1]: (~aVector0(X0)|~aVector0(X1)|~aDimensionOf0(X0)=aDimensionOf0(X1)|aScalar0(sdtasasdt0(X0,X1)))),
% 53.57/12.23 inference(cnf_transformation,[status(thm)],[f151])).
% 53.57/12.23 fof(f155,plain,(
% 53.57/12.23 ![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))))))),
% 53.57/12.23 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 53.57/12.23 fof(f156,plain,(
% 53.57/12.23 ![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)))))),
% 53.57/12.23 inference(cnf_transformation,[status(thm)],[f155])).
% 53.57/12.23 fof(f159,plain,(
% 53.57/12.23 aVector0(xs)),
% 53.57/12.23 inference(cnf_transformation,[status(thm)],[f38])).
% 53.57/12.23 fof(f160,plain,(
% 53.57/12.23 aVector0(xt)),
% 53.57/12.23 inference(cnf_transformation,[status(thm)],[f38])).
% 53.57/12.23 fof(f163,plain,(
% 53.57/12.23 aDimensionOf0(xs)=aDimensionOf0(xt)),
% 53.57/12.23 inference(cnf_transformation,[status(thm)],[f40])).
% 53.57/12.23 fof(f164,plain,(
% 53.57/12.23 ~aDimensionOf0(xs)=sz00),
% 53.57/12.23 inference(cnf_transformation,[status(thm)],[f41])).
% 53.57/12.23 fof(f165,plain,(
% 53.57/12.23 ((aVector0(xp)&szszuzczcdt0(aDimensionOf0(xp))=aDimensionOf0(xs))&(![W0]: (~aNaturalNumber0(W0)|sdtlbdtrb0(xp,W0)=sdtlbdtrb0(xs,W0))))&xp=sziznziztdt0(xs)),
% 53.57/12.23 inference(pre_NNF_transformation,[status(thm)],[f42])).
% 53.57/12.23 fof(f169,plain,(
% 53.57/12.23 xp=sziznziztdt0(xs)),
% 53.57/12.23 inference(cnf_transformation,[status(thm)],[f165])).
% 53.57/12.23 fof(f170,plain,(
% 53.57/12.23 ((aVector0(xq)&szszuzczcdt0(aDimensionOf0(xq))=aDimensionOf0(xt))&(![W0]: (~aNaturalNumber0(W0)|sdtlbdtrb0(xq,W0)=sdtlbdtrb0(xt,W0))))&xq=sziznziztdt0(xt)),
% 53.57/12.23 inference(pre_NNF_transformation,[status(thm)],[f43])).
% 53.57/12.23 fof(f174,plain,(
% 53.57/12.23 xq=sziznziztdt0(xt)),
% 53.57/12.23 inference(cnf_transformation,[status(thm)],[f170])).
% 53.57/12.23 fof(f176,plain,(
% 53.57/12.23 xA=sdtlbdtrb0(xs,aDimensionOf0(xs))),
% 53.57/12.23 inference(cnf_transformation,[status(thm)],[f44])).
% 53.57/12.23 fof(f178,plain,(
% 53.57/12.23 xB=sdtlbdtrb0(xt,aDimensionOf0(xt))),
% 53.57/12.23 inference(cnf_transformation,[status(thm)],[f45])).
% 53.57/12.23 fof(f180,plain,(
% 53.57/12.23 xC=sdtasasdt0(xp,xp)),
% 53.57/12.23 inference(cnf_transformation,[status(thm)],[f46])).
% 53.57/12.23 fof(f182,plain,(
% 53.57/12.23 xD=sdtasasdt0(xq,xq)),
% 53.57/12.23 inference(cnf_transformation,[status(thm)],[f47])).
% 53.57/12.23 fof(f184,plain,(
% 53.57/12.23 xE=sdtasasdt0(xp,xq)),
% 53.57/12.23 inference(cnf_transformation,[status(thm)],[f48])).
% 53.57/12.23 fof(f186,plain,(
% 53.57/12.23 xF=sdtasdt0(xA,xA)),
% 53.57/12.23 inference(cnf_transformation,[status(thm)],[f49])).
% 53.57/12.23 fof(f188,plain,(
% 53.57/12.23 xG=sdtasdt0(xB,xB)),
% 53.57/12.23 inference(cnf_transformation,[status(thm)],[f50])).
% 53.57/12.23 fof(f190,plain,(
% 53.57/12.23 xH=sdtasdt0(xA,xB)),
% 53.57/12.23 inference(cnf_transformation,[status(thm)],[f51])).
% 53.57/12.23 fof(f201,plain,(
% 53.57/12.23 sdtlseqdt0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)),sdtasdt0(sdtpldt0(xC,xF),sdtpldt0(xD,xG)))),
% 53.57/12.23 inference(cnf_transformation,[status(thm)],[f58])).
% 53.57/12.23 fof(f202,plain,(
% 53.57/12.23 ~sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt)))),
% 53.57/12.23 inference(cnf_transformation,[status(thm)],[f60])).
% 53.57/12.23 fof(f207,plain,(
% 53.57/12.23 ~aDimensionOf0(xt)=sz00),
% 53.57/12.23 inference(forward_demodulation,[status(thm)],[f163,f164])).
% 53.57/12.23 fof(f209,plain,(
% 53.57/12.23 xA=sdtlbdtrb0(xs,aDimensionOf0(xt))),
% 53.57/12.23 inference(forward_demodulation,[status(thm)],[f163,f176])).
% 53.57/12.23 fof(f210,plain,(
% 53.57/12.23 ![X0]: (~aVector0(X0)|~aDimensionOf0(X0)=aDimensionOf0(xt)|aScalar0(sdtasasdt0(X0,xt)))),
% 53.57/12.23 inference(resolution,[status(thm)],[f152,f160])).
% 53.57/12.23 fof(f211,plain,(
% 53.57/12.23 ![X0]: (~aVector0(X0)|~aDimensionOf0(X0)=aDimensionOf0(xs)|aScalar0(sdtasasdt0(X0,xs)))),
% 53.57/12.23 inference(resolution,[status(thm)],[f152,f159])).
% 53.57/12.23 fof(f212,plain,(
% 53.57/12.23 ![X0]: (~aVector0(X0)|~aDimensionOf0(X0)=aDimensionOf0(xt)|aScalar0(sdtasasdt0(X0,xs)))),
% 53.57/12.23 inference(forward_demodulation,[status(thm)],[f163,f211])).
% 53.57/12.23 fof(f233,plain,(
% 53.57/12.23 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|sdtasdt0(X0,X1)=sdtasdt0(X1,X0))),
% 53.57/12.23 inference(resolution,[status(thm)],[f81,f101])).
% 53.57/12.23 fof(f249,plain,(
% 53.57/12.23 ~aDimensionOf0(xt)=aDimensionOf0(xt)|aScalar0(sdtasasdt0(xt,xt))),
% 53.57/12.23 inference(resolution,[status(thm)],[f210,f160])).
% 53.57/12.23 fof(f251,plain,(
% 53.57/12.23 aScalar0(sdtasasdt0(xt,xt))),
% 53.57/12.23 inference(trivial_equality_resolution,[status(thm)],[f249])).
% 53.57/12.23 fof(f255,plain,(
% 53.57/12.23 ~aDimensionOf0(xs)=aDimensionOf0(xt)|aScalar0(sdtasasdt0(xs,xs))),
% 53.57/12.23 inference(resolution,[status(thm)],[f212,f159])).
% 53.57/12.23 fof(f257,plain,(
% 53.57/12.23 ~aDimensionOf0(xt)=aDimensionOf0(xt)|aScalar0(sdtasasdt0(xs,xs))),
% 53.57/12.23 inference(forward_demodulation,[status(thm)],[f163,f255])).
% 53.57/12.23 fof(f258,plain,(
% 53.57/12.23 aScalar0(sdtasasdt0(xs,xs))),
% 53.57/12.23 inference(trivial_equality_resolution,[status(thm)],[f257])).
% 53.57/12.23 fof(f343,plain,(
% 53.57/12.23 ![X0]: (~aScalar0(X0)|sdtasdt0(X0,sdtasasdt0(xt,xt))=sdtasdt0(sdtasasdt0(xt,xt),X0))),
% 53.57/12.23 inference(resolution,[status(thm)],[f251,f233])).
% 53.57/12.23 fof(f780,plain,(
% 53.57/12.23 ![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)))))),
% 53.57/12.23 inference(resolution,[status(thm)],[f156,f160])).
% 53.57/12.23 fof(f781,plain,(
% 53.57/12.23 ![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)))))),
% 53.57/12.23 inference(resolution,[status(thm)],[f156,f159])).
% 53.57/12.23 fof(f782,plain,(
% 53.57/12.23 ![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)))))),
% 53.57/12.23 inference(forward_demodulation,[status(thm)],[f174,f780])).
% 53.57/12.23 fof(f783,plain,(
% 53.57/12.23 ![X0]: (~aVector0(X0)|~aDimensionOf0(X0)=aDimensionOf0(xt)|aDimensionOf0(xt)=sz00|sdtasasdt0(X0,xt)=sdtpldt0(sdtasasdt0(sziznziztdt0(X0),xq),sdtasdt0(sdtlbdtrb0(X0,aDimensionOf0(X0)),xB)))),
% 53.57/12.23 inference(forward_demodulation,[status(thm)],[f178,f782])).
% 53.57/12.23 fof(f784,plain,(
% 53.57/12.23 ![X0]: (~aVector0(X0)|~aDimensionOf0(X0)=aDimensionOf0(xt)|sdtasasdt0(X0,xt)=sdtpldt0(sdtasasdt0(sziznziztdt0(X0),xq),sdtasdt0(sdtlbdtrb0(X0,aDimensionOf0(X0)),xB)))),
% 53.57/12.23 inference(forward_subsumption_resolution,[status(thm)],[f783,f207])).
% 53.57/12.23 fof(f785,plain,(
% 53.57/12.23 ![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)))))),
% 53.57/12.23 inference(forward_demodulation,[status(thm)],[f163,f781])).
% 53.57/12.23 fof(f786,plain,(
% 53.57/12.23 ![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)))))),
% 53.57/12.23 inference(forward_demodulation,[status(thm)],[f163,f785])).
% 53.57/12.23 fof(f787,plain,(
% 53.57/12.23 ![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)))))),
% 53.57/12.23 inference(forward_demodulation,[status(thm)],[f169,f786])).
% 53.57/12.23 fof(f788,plain,(
% 53.57/12.23 ![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)))))),
% 53.57/12.23 inference(forward_demodulation,[status(thm)],[f163,f787])).
% 53.57/12.23 fof(f789,plain,(
% 53.57/12.23 ![X0]: (~aVector0(X0)|~aDimensionOf0(X0)=aDimensionOf0(xt)|aDimensionOf0(xt)=sz00|sdtasasdt0(X0,xs)=sdtpldt0(sdtasasdt0(sziznziztdt0(X0),xp),sdtasdt0(sdtlbdtrb0(X0,aDimensionOf0(X0)),xA)))),
% 53.57/12.23 inference(forward_demodulation,[status(thm)],[f209,f788])).
% 53.57/12.23 fof(f790,plain,(
% 53.57/12.23 ![X0]: (~aVector0(X0)|~aDimensionOf0(X0)=aDimensionOf0(xt)|sdtasasdt0(X0,xs)=sdtpldt0(sdtasasdt0(sziznziztdt0(X0),xp),sdtasdt0(sdtlbdtrb0(X0,aDimensionOf0(X0)),xA)))),
% 53.57/12.23 inference(forward_subsumption_resolution,[status(thm)],[f789,f207])).
% 53.57/12.23 fof(f1651,plain,(
% 53.57/12.23 ~aDimensionOf0(xt)=aDimensionOf0(xt)|sdtasasdt0(xt,xt)=sdtpldt0(sdtasasdt0(sziznziztdt0(xt),xq),sdtasdt0(sdtlbdtrb0(xt,aDimensionOf0(xt)),xB))),
% 53.57/12.23 inference(resolution,[status(thm)],[f784,f160])).
% 53.57/12.23 fof(f1652,plain,(
% 53.57/12.23 ~aDimensionOf0(xs)=aDimensionOf0(xt)|sdtasasdt0(xs,xt)=sdtpldt0(sdtasasdt0(sziznziztdt0(xs),xq),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),xB))),
% 53.57/12.23 inference(resolution,[status(thm)],[f784,f159])).
% 53.57/12.23 fof(f1655,plain,(
% 53.57/12.23 ~aDimensionOf0(xt)=aDimensionOf0(xt)|sdtasasdt0(xt,xt)=sdtpldt0(sdtasasdt0(xq,xq),sdtasdt0(sdtlbdtrb0(xt,aDimensionOf0(xt)),xB))),
% 53.57/12.23 inference(forward_demodulation,[status(thm)],[f174,f1651])).
% 53.57/12.23 fof(f1656,plain,(
% 53.57/12.23 ~aDimensionOf0(xt)=aDimensionOf0(xt)|sdtasasdt0(xt,xt)=sdtpldt0(xD,sdtasdt0(sdtlbdtrb0(xt,aDimensionOf0(xt)),xB))),
% 53.57/12.23 inference(forward_demodulation,[status(thm)],[f182,f1655])).
% 53.57/12.23 fof(f1657,plain,(
% 53.57/12.23 ~aDimensionOf0(xt)=aDimensionOf0(xt)|sdtasasdt0(xt,xt)=sdtpldt0(xD,sdtasdt0(xB,xB))),
% 53.57/12.23 inference(forward_demodulation,[status(thm)],[f178,f1656])).
% 53.57/12.23 fof(f1658,plain,(
% 53.57/12.23 ~aDimensionOf0(xt)=aDimensionOf0(xt)|sdtasasdt0(xt,xt)=sdtpldt0(xD,xG)),
% 53.57/12.23 inference(forward_demodulation,[status(thm)],[f188,f1657])).
% 53.57/12.23 fof(f1659,plain,(
% 53.57/12.23 sdtlseqdt0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)),sdtasdt0(sdtpldt0(xC,xF),sdtasasdt0(xt,xt)))),
% 53.57/12.23 inference(backward_demodulation,[status(thm)],[f1660,f201])).
% 53.57/12.23 fof(f1660,plain,(
% 53.57/12.23 sdtasasdt0(xt,xt)=sdtpldt0(xD,xG)),
% 53.57/12.23 inference(trivial_equality_resolution,[status(thm)],[f1658])).
% 53.57/12.23 fof(f1661,plain,(
% 53.57/12.23 ~aDimensionOf0(xt)=aDimensionOf0(xt)|sdtasasdt0(xs,xt)=sdtpldt0(sdtasasdt0(sziznziztdt0(xs),xq),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),xB))),
% 53.57/12.23 inference(forward_demodulation,[status(thm)],[f163,f1652])).
% 53.57/12.23 fof(f1662,plain,(
% 53.57/12.23 ~aDimensionOf0(xt)=aDimensionOf0(xt)|sdtasasdt0(xs,xt)=sdtpldt0(sdtasasdt0(xp,xq),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),xB))),
% 53.57/12.23 inference(forward_demodulation,[status(thm)],[f169,f1661])).
% 53.57/12.23 fof(f1663,plain,(
% 53.57/12.23 ~aDimensionOf0(xt)=aDimensionOf0(xt)|sdtasasdt0(xs,xt)=sdtpldt0(xE,sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),xB))),
% 53.57/12.24 inference(forward_demodulation,[status(thm)],[f184,f1662])).
% 53.57/12.24 fof(f1664,plain,(
% 53.57/12.24 ~aDimensionOf0(xt)=aDimensionOf0(xt)|sdtasasdt0(xs,xt)=sdtpldt0(xE,sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xt)),xB))),
% 53.57/12.24 inference(forward_demodulation,[status(thm)],[f163,f1663])).
% 53.57/12.24 fof(f1665,plain,(
% 53.57/12.24 ~aDimensionOf0(xt)=aDimensionOf0(xt)|sdtasasdt0(xs,xt)=sdtpldt0(xE,sdtasdt0(xA,xB))),
% 53.57/12.24 inference(forward_demodulation,[status(thm)],[f209,f1664])).
% 53.57/12.24 fof(f1666,plain,(
% 53.57/12.24 ~aDimensionOf0(xt)=aDimensionOf0(xt)|sdtasasdt0(xs,xt)=sdtpldt0(xE,xH)),
% 53.57/12.24 inference(forward_demodulation,[status(thm)],[f190,f1665])).
% 53.57/12.24 fof(f1667,plain,(
% 53.57/12.24 sdtasasdt0(xs,xt)=sdtpldt0(xE,xH)),
% 53.57/12.24 inference(trivial_equality_resolution,[status(thm)],[f1666])).
% 53.57/12.24 fof(f1668,plain,(
% 53.57/12.24 sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtpldt0(xE,xH)),sdtasdt0(sdtpldt0(xC,xF),sdtasasdt0(xt,xt)))),
% 53.57/12.24 inference(forward_demodulation,[status(thm)],[f1667,f1659])).
% 53.57/12.24 fof(f1669,plain,(
% 53.57/12.24 sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtpldt0(xC,xF),sdtasasdt0(xt,xt)))),
% 53.57/12.24 inference(forward_demodulation,[status(thm)],[f1667,f1668])).
% 53.57/12.24 fof(f1702,plain,(
% 53.57/12.24 sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt))=sdtasdt0(sdtasasdt0(xt,xt),sdtasasdt0(xs,xs))),
% 53.57/12.24 inference(resolution,[status(thm)],[f343,f258])).
% 53.57/12.24 fof(f1735,plain,(
% 53.57/12.24 ~sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xt,xt),sdtasasdt0(xs,xs)))),
% 53.57/12.24 inference(backward_demodulation,[status(thm)],[f1702,f202])).
% 53.57/12.24 fof(f2522,plain,(
% 53.57/12.24 ~aDimensionOf0(xs)=aDimensionOf0(xt)|sdtasasdt0(xs,xs)=sdtpldt0(sdtasasdt0(sziznziztdt0(xs),xp),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),xA))),
% 53.57/12.24 inference(resolution,[status(thm)],[f790,f159])).
% 53.57/12.24 fof(f2528,plain,(
% 53.57/12.24 ~aDimensionOf0(xt)=aDimensionOf0(xt)|sdtasasdt0(xs,xs)=sdtpldt0(sdtasasdt0(sziznziztdt0(xs),xp),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),xA))),
% 53.57/12.24 inference(forward_demodulation,[status(thm)],[f163,f2522])).
% 53.57/12.24 fof(f2529,plain,(
% 53.57/12.24 ~aDimensionOf0(xt)=aDimensionOf0(xt)|sdtasasdt0(xs,xs)=sdtpldt0(sdtasasdt0(xp,xp),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),xA))),
% 53.57/12.27 inference(forward_demodulation,[status(thm)],[f169,f2528])).
% 53.57/12.27 fof(f2530,plain,(
% 53.57/12.27 ~aDimensionOf0(xt)=aDimensionOf0(xt)|sdtasasdt0(xs,xs)=sdtpldt0(xC,sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),xA))),
% 53.57/12.27 inference(forward_demodulation,[status(thm)],[f180,f2529])).
% 53.57/12.27 fof(f2531,plain,(
% 53.57/12.27 ~aDimensionOf0(xt)=aDimensionOf0(xt)|sdtasasdt0(xs,xs)=sdtpldt0(xC,sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xt)),xA))),
% 53.57/12.27 inference(forward_demodulation,[status(thm)],[f163,f2530])).
% 53.57/12.27 fof(f2532,plain,(
% 53.57/12.27 ~aDimensionOf0(xt)=aDimensionOf0(xt)|sdtasasdt0(xs,xs)=sdtpldt0(xC,sdtasdt0(xA,xA))),
% 53.57/12.27 inference(forward_demodulation,[status(thm)],[f209,f2531])).
% 53.57/12.27 fof(f2533,plain,(
% 53.57/12.27 ~aDimensionOf0(xt)=aDimensionOf0(xt)|sdtasasdt0(xs,xs)=sdtpldt0(xC,xF)),
% 53.57/12.27 inference(forward_demodulation,[status(thm)],[f186,f2532])).
% 53.57/12.27 fof(f2534,plain,(
% 53.57/12.27 sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt)))),
% 53.57/12.27 inference(backward_demodulation,[status(thm)],[f2535,f1669])).
% 53.57/12.27 fof(f2535,plain,(
% 53.57/12.27 sdtasasdt0(xs,xs)=sdtpldt0(xC,xF)),
% 53.57/12.27 inference(trivial_equality_resolution,[status(thm)],[f2533])).
% 53.57/12.27 fof(f2536,plain,(
% 53.57/12.27 sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xt,xt),sdtasasdt0(xs,xs)))),
% 53.57/12.27 inference(forward_demodulation,[status(thm)],[f1702,f2534])).
% 53.57/12.27 fof(f2537,plain,(
% 53.57/12.27 $false),
% 53.57/12.27 inference(forward_subsumption_resolution,[status(thm)],[f2536,f1735])).
% 53.57/12.27 % SZS output end CNFRefutation for theBenchmark.p
% 32.77/12.30 % Elapsed time: 6.897635 seconds
% 32.77/12.30 % CPU time: 54.171801 seconds
% 32.77/12.30 % Total memory used: 501.806 MB
% 32.77/12.30 % Net memory used: 477.595 MB
%------------------------------------------------------------------------------