%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : RNG077+2 : 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 : n002.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 51.49s 11.98s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG077+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/5.37 % Computer : n002.cluster.edu
% 0.11/5.37 % Model : x86_64 x86_64
% 0.11/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.37 % Memory : 8046.5625MB
% 0.11/5.37 % OS : Linux 6.8.0-71-generic
% 0.11/5.37 % CPULimit : 300
% 0.11/5.37 % WCLimit : 300
% 0.11/5.37 % DateTime : Mon Sep 21 04:20:54 UTC 2026
% 0.11/5.38 % CPUTime :
% 0.11/5.39 % Drodi V4.1.1
% 51.49/11.98 % Refutation found
% 51.49/11.98 % SZS status Theorem for theBenchmark: Theorem is valid
% 51.49/11.98 % SZS output start CNFRefutation for theBenchmark
% 51.49/11.98 fof(f9,axiom,(
% 51.49/11.98 aScalar0(sz0z00) ),
% 51.49/11.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 51.49/11.98 fof(f11,axiom,(
% 51.49/11.98 (! [W0,W1] :( ( aScalar0(W0)& aScalar0(W1) )=> aScalar0(sdtasdt0(W0,W1)) ) )),
% 51.49/11.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 51.49/11.98 fof(f14,axiom,(
% 51.49/11.98 (! [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) ) ) )),
% 51.49/11.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 51.49/11.98 fof(f15,axiom,(
% 51.49/11.98 (! [W0,W1,W2] :( ( aScalar0(W0)& aScalar0(W1)& aScalar0(W2) )=> ( sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2))& sdtasdt0(sdtpldt0(W0,W1),W2) = sdtpldt0(sdtasdt0(W0,W2),sdtasdt0(W1,W2)) ) ) )),
% 51.49/11.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 51.49/11.98 fof(f20,axiom,(
% 51.49/11.98 (! [W0] :( aScalar0(W0)=> sdtlseqdt0(W0,W0) ) )),
% 51.49/11.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 51.49/11.98 fof(f25,axiom,(
% 51.49/11.98 (! [W0,W1] :( ( aScalar0(W0)& aScalar0(W1) )=> ( sdtlseqdt0(W0,W1)| sdtlseqdt0(W1,W0) ) ) )),
% 51.49/11.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 51.49/11.98 fof(f30,axiom,(
% 51.49/11.98 (! [W0] :( aVector0(W0)=> aNaturalNumber0(aDimensionOf0(W0)) ) )),
% 51.49/11.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 51.49/11.98 fof(f38,hypothesis,(
% 51.49/11.98 ( aVector0(xs)& aVector0(xt) ) ),
% 51.49/11.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 51.49/11.98 fof(f40,hypothesis,(
% 51.49/11.98 aDimensionOf0(xs) = aDimensionOf0(xt) ),
% 51.49/11.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 51.49/11.98 fof(f41,hypothesis,(
% 51.49/11.98 aDimensionOf0(xs) != sz00 ),
% 51.49/11.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 51.49/11.98 fof(f42,hypothesis,(
% 51.49/11.98 ( aVector0(xp)& szszuzczcdt0(aDimensionOf0(xp)) = aDimensionOf0(xs)& (! [W0] :( aNaturalNumber0(W0)=> sdtlbdtrb0(xp,W0) = sdtlbdtrb0(xs,W0) ))& xp = sziznziztdt0(xs) ) ),
% 51.49/11.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 51.49/11.98 fof(f43,hypothesis,(
% 51.49/11.98 ( aVector0(xq)& szszuzczcdt0(aDimensionOf0(xq)) = aDimensionOf0(xt)& (! [W0] :( aNaturalNumber0(W0)=> sdtlbdtrb0(xq,W0) = sdtlbdtrb0(xt,W0) ))& xq = sziznziztdt0(xt) ) ),
% 51.49/11.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 51.49/11.98 fof(f44,hypothesis,(
% 51.49/11.98 ( aScalar0(xA)& xA = sdtlbdtrb0(xs,aDimensionOf0(xs)) ) ),
% 51.49/11.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 51.49/11.98 fof(f45,hypothesis,(
% 51.49/11.98 ( aScalar0(xB)& xB = sdtlbdtrb0(xt,aDimensionOf0(xt)) ) ),
% 51.49/11.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 51.49/11.98 fof(f46,hypothesis,(
% 51.49/11.98 ( aScalar0(xC)& xC = sdtasasdt0(xp,xp) ) ),
% 51.49/11.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 51.49/11.98 fof(f47,hypothesis,(
% 51.49/11.98 ( aScalar0(xD)& xD = sdtasasdt0(xq,xq) ) ),
% 51.49/11.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 51.49/11.98 fof(f48,hypothesis,(
% 51.49/11.98 ( aScalar0(xE)& xE = sdtasasdt0(xp,xq) ) ),
% 51.49/11.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 51.49/11.98 fof(f49,hypothesis,(
% 51.49/11.98 ( aScalar0(xF)& xF = sdtasdt0(xA,xA) ) ),
% 51.49/11.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 51.49/11.98 fof(f50,hypothesis,(
% 51.49/11.98 ( aScalar0(xG)& xG = sdtasdt0(xB,xB) ) ),
% 51.49/11.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 51.49/11.98 fof(f51,hypothesis,(
% 51.49/11.98 ( aScalar0(xH)& xH = sdtasdt0(xA,xB) ) ),
% 51.49/11.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 51.49/11.98 fof(f53,hypothesis,(
% 51.49/11.98 ( aScalar0(xP)& xP = sdtasdt0(xE,xH) ) ),
% 51.49/11.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 51.49/11.98 fof(f59,conjecture,(
% 51.49/11.98 sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)) = sdtpldt0(sdtasdt0(xE,xH),sdtpldt0(sdtasdt0(xH,xE),sdtasdt0(xH,xH))) ),
% 51.49/11.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 51.49/11.98 fof(f60,negated_conjecture,(
% 51.49/11.98 ~(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)) = sdtpldt0(sdtasdt0(xE,xH),sdtpldt0(sdtasdt0(xH,xE),sdtasdt0(xH,xH))) )),
% 51.49/11.98 inference(negated_conjecture,[status(cth)],[f59])).
% 51.49/11.98 fof(f81,plain,(
% 51.49/11.98 aScalar0(sz0z00)),
% 51.49/11.98 inference(cnf_transformation,[status(thm)],[f9])).
% 51.49/11.98 fof(f84,plain,(
% 51.49/11.98 ![W0,W1]: ((~aScalar0(W0)|~aScalar0(W1))|aScalar0(sdtasdt0(W0,W1)))),
% 51.49/11.98 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 51.49/11.98 fof(f85,plain,(
% 51.49/11.98 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|aScalar0(sdtasdt0(X0,X1)))),
% 51.49/11.98 inference(cnf_transformation,[status(thm)],[f84])).
% 51.49/11.98 fof(f97,plain,(
% 51.49/11.98 ![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)))),
% 51.49/11.98 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 51.49/11.98 fof(f98,plain,(
% 51.49/11.98 ![X0,X1,X2]: (~aScalar0(X0)|~aScalar0(X1)|~aScalar0(X2)|sdtpldt0(sdtpldt0(X0,X1),X2)=sdtpldt0(X0,sdtpldt0(X1,X2)))),
% 51.49/11.98 inference(cnf_transformation,[status(thm)],[f97])).
% 51.49/11.98 fof(f99,plain,(
% 51.49/11.98 ![X0,X1,X2]: (~aScalar0(X0)|~aScalar0(X1)|~aScalar0(X2)|sdtpldt0(X0,X1)=sdtpldt0(X1,X0))),
% 51.49/11.98 inference(cnf_transformation,[status(thm)],[f97])).
% 51.49/11.98 fof(f101,plain,(
% 51.49/11.98 ![X0,X1,X2]: (~aScalar0(X0)|~aScalar0(X1)|~aScalar0(X2)|sdtasdt0(X0,X1)=sdtasdt0(X1,X0))),
% 51.49/11.98 inference(cnf_transformation,[status(thm)],[f97])).
% 51.49/11.98 fof(f102,plain,(
% 51.49/11.98 ![W0,W1,W2]: (((~aScalar0(W0)|~aScalar0(W1))|~aScalar0(W2))|(sdtasdt0(W0,sdtpldt0(W1,W2))=sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2))&sdtasdt0(sdtpldt0(W0,W1),W2)=sdtpldt0(sdtasdt0(W0,W2),sdtasdt0(W1,W2))))),
% 51.49/11.98 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 51.49/11.98 fof(f103,plain,(
% 51.49/11.98 ![X0,X1,X2]: (~aScalar0(X0)|~aScalar0(X1)|~aScalar0(X2)|sdtasdt0(X0,sdtpldt0(X1,X2))=sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2)))),
% 51.49/11.98 inference(cnf_transformation,[status(thm)],[f102])).
% 51.49/11.98 fof(f104,plain,(
% 51.49/11.98 ![X0,X1,X2]: (~aScalar0(X0)|~aScalar0(X1)|~aScalar0(X2)|sdtasdt0(sdtpldt0(X0,X1),X2)=sdtpldt0(sdtasdt0(X0,X2),sdtasdt0(X1,X2)))),
% 51.49/11.98 inference(cnf_transformation,[status(thm)],[f102])).
% 51.49/11.98 fof(f114,plain,(
% 51.49/11.98 ![W0]: (~aScalar0(W0)|sdtlseqdt0(W0,W0))),
% 51.49/11.98 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 51.49/11.98 fof(f115,plain,(
% 51.49/11.98 ![X0]: (~aScalar0(X0)|sdtlseqdt0(X0,X0))),
% 51.49/11.98 inference(cnf_transformation,[status(thm)],[f114])).
% 51.49/11.98 fof(f124,plain,(
% 51.49/11.98 ![W0,W1]: ((~aScalar0(W0)|~aScalar0(W1))|(sdtlseqdt0(W0,W1)|sdtlseqdt0(W1,W0)))),
% 51.49/11.98 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 51.49/11.98 fof(f125,plain,(
% 51.49/11.98 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|sdtlseqdt0(X0,X1)|sdtlseqdt0(X1,X0))),
% 51.49/11.98 inference(cnf_transformation,[status(thm)],[f124])).
% 51.49/11.98 fof(f136,plain,(
% 51.49/11.98 ![W0]: (~aVector0(W0)|aNaturalNumber0(aDimensionOf0(W0)))),
% 51.49/11.98 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 51.49/11.98 fof(f137,plain,(
% 51.49/11.98 ![X0]: (~aVector0(X0)|aNaturalNumber0(aDimensionOf0(X0)))),
% 51.49/11.98 inference(cnf_transformation,[status(thm)],[f136])).
% 51.49/11.98 fof(f159,plain,(
% 51.49/11.98 aVector0(xs)),
% 51.49/11.98 inference(cnf_transformation,[status(thm)],[f38])).
% 51.49/11.98 fof(f160,plain,(
% 51.49/11.98 aVector0(xt)),
% 51.49/11.98 inference(cnf_transformation,[status(thm)],[f38])).
% 51.49/11.98 fof(f163,plain,(
% 51.49/11.98 aDimensionOf0(xs)=aDimensionOf0(xt)),
% 51.49/11.98 inference(cnf_transformation,[status(thm)],[f40])).
% 51.49/11.98 fof(f164,plain,(
% 51.49/11.98 ~aDimensionOf0(xs)=sz00),
% 51.49/11.98 inference(cnf_transformation,[status(thm)],[f41])).
% 51.49/11.98 fof(f165,plain,(
% 51.49/11.98 ((aVector0(xp)&szszuzczcdt0(aDimensionOf0(xp))=aDimensionOf0(xs))&(![W0]: (~aNaturalNumber0(W0)|sdtlbdtrb0(xp,W0)=sdtlbdtrb0(xs,W0))))&xp=sziznziztdt0(xs)),
% 51.49/11.98 inference(pre_NNF_transformation,[status(thm)],[f42])).
% 51.49/11.98 fof(f166,plain,(
% 51.49/11.98 aVector0(xp)),
% 51.49/11.98 inference(cnf_transformation,[status(thm)],[f165])).
% 51.49/11.98 fof(f170,plain,(
% 51.49/11.98 ((aVector0(xq)&szszuzczcdt0(aDimensionOf0(xq))=aDimensionOf0(xt))&(![W0]: (~aNaturalNumber0(W0)|sdtlbdtrb0(xq,W0)=sdtlbdtrb0(xt,W0))))&xq=sziznziztdt0(xt)),
% 51.49/11.98 inference(pre_NNF_transformation,[status(thm)],[f43])).
% 51.49/11.98 fof(f171,plain,(
% 51.49/11.98 aVector0(xq)),
% 51.49/11.98 inference(cnf_transformation,[status(thm)],[f170])).
% 51.49/11.98 fof(f175,plain,(
% 51.49/11.98 aScalar0(xA)),
% 51.49/11.98 inference(cnf_transformation,[status(thm)],[f44])).
% 51.49/11.98 fof(f177,plain,(
% 51.49/11.98 aScalar0(xB)),
% 51.49/11.98 inference(cnf_transformation,[status(thm)],[f45])).
% 51.49/11.98 fof(f179,plain,(
% 51.49/11.98 aScalar0(xC)),
% 51.49/11.98 inference(cnf_transformation,[status(thm)],[f46])).
% 51.49/11.98 fof(f181,plain,(
% 51.49/11.98 aScalar0(xD)),
% 51.49/11.98 inference(cnf_transformation,[status(thm)],[f47])).
% 51.49/11.98 fof(f183,plain,(
% 51.49/11.98 aScalar0(xE)),
% 51.49/11.98 inference(cnf_transformation,[status(thm)],[f48])).
% 51.49/11.98 fof(f185,plain,(
% 51.49/11.98 aScalar0(xF)),
% 51.49/11.98 inference(cnf_transformation,[status(thm)],[f49])).
% 51.49/11.98 fof(f187,plain,(
% 51.49/11.98 aScalar0(xG)),
% 51.49/11.98 inference(cnf_transformation,[status(thm)],[f50])).
% 51.49/11.98 fof(f189,plain,(
% 51.49/11.98 aScalar0(xH)),
% 51.49/11.98 inference(cnf_transformation,[status(thm)],[f51])).
% 51.49/11.98 fof(f193,plain,(
% 51.49/11.98 aScalar0(xP)),
% 51.49/11.98 inference(cnf_transformation,[status(thm)],[f53])).
% 51.49/11.98 fof(f194,plain,(
% 51.49/11.98 xP=sdtasdt0(xE,xH)),
% 51.49/11.98 inference(cnf_transformation,[status(thm)],[f53])).
% 51.49/11.98 fof(f202,plain,(
% 51.49/11.98 ~sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH))=sdtpldt0(sdtasdt0(xE,xH),sdtpldt0(sdtasdt0(xH,xE),sdtasdt0(xH,xH)))),
% 51.49/11.98 inference(cnf_transformation,[status(thm)],[f60])).
% 51.49/11.98 fof(f203,definition,(
% 51.49/11.98 ![X0]: (sQ0_spl <=> (~aScalar0(X0)))),
% 51.49/11.98 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 51.49/11.98 fof(f204,plain,(
% 51.49/11.98 ![X0]: (~aScalar0(X0)|~sQ0_spl)),
% 51.49/11.98 inference(component_clause,[status(thm)],[f203])).
% 51.49/11.98 fof(f210,definition,(
% 51.49/11.98 ![X0,X1]: (sQ2_spl <=> (~aScalar0(X0)|~aScalar0(X1)|sdtpldt0(X0,X1)=sdtpldt0(X1,X0)))),
% 51.49/11.98 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 51.49/11.98 fof(f211,plain,(
% 51.49/11.98 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|sdtpldt0(X0,X1)=sdtpldt0(X1,X0)|~sQ2_spl)),
% 51.49/11.98 inference(component_clause,[status(thm)],[f210])).
% 51.49/11.98 fof(f213,plain,(
% 51.49/11.98 sQ2_spl|sQ0_spl),
% 51.49/11.98 inference(split_clause,[status(thm)],[f99,f210,f203])).
% 51.49/11.98 fof(f214,definition,(
% 51.49/11.98 ![X0,X1]: (sQ3_spl <=> (~aScalar0(X0)|~aScalar0(X1)|sdtasdt0(X0,X1)=sdtasdt0(X1,X0)))),
% 51.49/11.98 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 51.49/11.98 fof(f215,plain,(
% 51.49/11.98 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|sdtasdt0(X0,X1)=sdtasdt0(X1,X0)|~sQ3_spl)),
% 51.49/11.98 inference(component_clause,[status(thm)],[f214])).
% 51.49/11.98 fof(f217,plain,(
% 51.49/11.98 sQ3_spl|sQ0_spl),
% 51.49/11.98 inference(split_clause,[status(thm)],[f101,f214,f203])).
% 51.49/11.98 fof(f224,plain,(
% 51.49/11.98 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|sdtasdt0(sdtpldt0(X0,xE),X1)=sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(xE,X1)))),
% 51.49/11.98 inference(resolution,[status(thm)],[f183,f104])).
% 51.49/11.98 fof(f226,plain,(
% 51.49/11.98 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|sdtasdt0(X0,sdtpldt0(X1,xE))=sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,xE)))),
% 51.49/11.98 inference(resolution,[status(thm)],[f183,f103])).
% 51.49/11.98 fof(f228,plain,(
% 51.49/11.98 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|sdtasdt0(X0,sdtpldt0(xE,X1))=sdtpldt0(sdtasdt0(X0,xE),sdtasdt0(X0,X1)))),
% 51.49/11.98 inference(resolution,[status(thm)],[f183,f103])).
% 51.49/11.98 fof(f237,plain,(
% 51.49/11.98 ![X0]: (~aScalar0(X0)|aScalar0(sdtasdt0(xE,X0)))),
% 51.49/11.98 inference(resolution,[status(thm)],[f183,f85])).
% 51.49/11.98 fof(f239,plain,(
% 51.49/11.98 ![X0]: (~aScalar0(X0)|sdtasdt0(sdtpldt0(X0,xH),xH)=sdtpldt0(sdtasdt0(X0,xH),sdtasdt0(xH,xH)))),
% 51.49/11.98 inference(resolution,[status(thm)],[f189,f104])).
% 51.49/11.98 fof(f255,plain,(
% 51.49/11.98 ![X0]: (~aScalar0(X0)|aScalar0(sdtasdt0(xH,X0)))),
% 51.49/11.98 inference(resolution,[status(thm)],[f189,f85])).
% 51.49/11.98 fof(f272,plain,(
% 51.49/11.98 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|sdtpldt0(sdtpldt0(X0,xP),X1)=sdtpldt0(X0,sdtpldt0(xP,X1)))),
% 51.49/11.98 inference(resolution,[status(thm)],[f193,f98])).
% 51.49/11.98 fof(f275,plain,(
% 51.49/11.98 ~sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH))=sdtpldt0(xP,sdtpldt0(sdtasdt0(xH,xE),sdtasdt0(xH,xH)))),
% 51.49/11.98 inference(backward_demodulation,[status(thm)],[f194,f202])).
% 51.49/11.98 fof(f315,plain,(
% 51.49/11.98 sdtlseqdt0(xP,xP)),
% 51.49/11.98 inference(resolution,[status(thm)],[f115,f193])).
% 51.49/11.98 fof(f316,plain,(
% 51.49/11.98 sdtlseqdt0(xH,xH)),
% 51.49/11.98 inference(resolution,[status(thm)],[f115,f189])).
% 51.49/11.98 fof(f317,plain,(
% 51.49/11.98 sdtlseqdt0(xE,xE)),
% 51.49/11.98 inference(resolution,[status(thm)],[f115,f183])).
% 51.49/11.98 fof(f320,plain,(
% 51.49/11.98 ![X0]: (~aScalar0(X0)|sdtasdt0(sdtpldt0(X0,xE),xH)=sdtpldt0(sdtasdt0(X0,xH),sdtasdt0(xE,xH)))),
% 51.49/11.98 inference(resolution,[status(thm)],[f224,f189])).
% 51.49/11.98 fof(f322,plain,(
% 51.49/11.98 ![X0]: (~aScalar0(X0)|sdtasdt0(sdtpldt0(X0,xE),xH)=sdtpldt0(sdtasdt0(X0,xH),xP))),
% 51.49/11.98 inference(forward_demodulation,[status(thm)],[f194,f320])).
% 51.49/11.98 fof(f327,plain,(
% 51.49/11.98 ![X0]: (~aScalar0(X0)|sdtasdt0(X0,sdtpldt0(xH,xE))=sdtpldt0(sdtasdt0(X0,xH),sdtasdt0(X0,xE)))),
% 51.49/11.98 inference(resolution,[status(thm)],[f226,f189])).
% 51.49/11.98 fof(f330,plain,(
% 51.49/11.98 ![X0]: (~aScalar0(X0)|sdtasdt0(X0,sdtpldt0(xE,xH))=sdtpldt0(sdtasdt0(X0,xE),sdtasdt0(X0,xH)))),
% 51.49/11.98 inference(resolution,[status(thm)],[f228,f189])).
% 51.49/11.98 fof(f351,plain,(
% 51.49/11.98 aScalar0(sdtasdt0(xE,xP))),
% 51.49/11.98 inference(resolution,[status(thm)],[f237,f193])).
% 51.49/11.98 fof(f355,plain,(
% 51.49/11.98 $false|~sQ0_spl),
% 51.49/11.98 inference(backward_subsumption_resolution,[status(thm)],[f193,f204])).
% 51.49/11.98 fof(f358,plain,(
% 51.49/11.98 ~sQ0_spl),
% 51.49/11.98 inference(contradiction_clause,[status(thm)],[f355])).
% 51.49/11.98 fof(f608,plain,(
% 51.49/11.98 sdtasdt0(xH,sdtpldt0(xE,xH))=sdtpldt0(sdtasdt0(xH,xE),sdtasdt0(xH,xH))),
% 51.49/11.98 inference(resolution,[status(thm)],[f189,f330])).
% 51.49/11.98 fof(f610,plain,(
% 51.49/11.98 sdtasdt0(xH,sdtpldt0(xH,xE))=sdtpldt0(sdtasdt0(xH,xH),sdtasdt0(xH,xE))),
% 51.49/11.98 inference(resolution,[status(thm)],[f189,f327])).
% 51.49/11.98 fof(f612,plain,(
% 51.49/11.98 sdtasdt0(sdtpldt0(xH,xE),xH)=sdtpldt0(sdtasdt0(xH,xH),xP)),
% 51.49/11.98 inference(resolution,[status(thm)],[f189,f322])).
% 51.49/11.98 fof(f642,plain,(
% 51.49/11.98 ![X0]: (~aScalar0(X0)|sdtasdt0(X0,xH)=sdtasdt0(xH,X0)|~sQ3_spl)),
% 51.49/11.98 inference(resolution,[status(thm)],[f189,f215])).
% 51.49/11.98 fof(f649,plain,(
% 51.49/11.98 ![X0]: (~aScalar0(X0)|sdtpldt0(X0,xH)=sdtpldt0(xH,X0)|~sQ2_spl)),
% 51.49/11.98 inference(resolution,[status(thm)],[f189,f211])).
% 51.49/11.98 fof(f746,plain,(
% 51.49/11.98 sdtasdt0(sdtpldt0(xE,xH),xH)=sdtpldt0(sdtasdt0(xE,xH),sdtasdt0(xH,xH))),
% 51.49/11.98 inference(resolution,[status(thm)],[f183,f239])).
% 51.49/11.98 fof(f760,plain,(
% 51.49/11.98 sdtasdt0(sdtpldt0(xE,xH),xH)=sdtpldt0(xP,sdtasdt0(xH,xH))),
% 51.49/11.98 inference(forward_demodulation,[status(thm)],[f194,f746])).
% 51.49/11.98 fof(f767,plain,(
% 51.49/11.98 aScalar0(sdtasdt0(xH,xH))),
% 51.49/11.98 inference(resolution,[status(thm)],[f255,f189])).
% 51.49/11.98 fof(f808,plain,(
% 51.49/11.98 ![X0]: (~aScalar0(X0)|sdtlseqdt0(sz0z00,X0)|sdtlseqdt0(X0,sz0z00))),
% 51.49/11.98 inference(resolution,[status(thm)],[f125,f81])).
% 51.49/11.98 fof(f928,plain,(
% 51.49/11.98 ~sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH))=sdtpldt0(xP,sdtasdt0(xH,sdtpldt0(xE,xH)))),
% 51.49/11.98 inference(backward_demodulation,[status(thm)],[f608,f275])).
% 51.49/11.98 fof(f934,definition,(
% 51.49/11.98 sQ7_spl <=> (aScalar0(xB))),
% 51.49/11.98 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 51.49/11.98 fof(f936,plain,(
% 51.49/11.98 ~aScalar0(xB)|sQ7_spl),
% 51.49/11.98 inference(component_clause,[status(thm)],[f934])).
% 51.49/11.98 fof(f944,definition,(
% 51.49/11.98 sQ10_spl <=> (aScalar0(xA))),
% 51.49/11.98 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 51.49/11.98 fof(f946,plain,(
% 51.49/11.98 ~aScalar0(xA)|sQ10_spl),
% 51.49/11.98 inference(component_clause,[status(thm)],[f944])).
% 51.49/11.98 fof(f973,plain,(
% 51.49/11.98 sdtasdt0(xE,xH)=sdtasdt0(xH,xE)|~sQ3_spl),
% 51.49/11.98 inference(resolution,[status(thm)],[f642,f183])).
% 51.49/11.98 fof(f977,plain,(
% 51.49/11.98 xP=sdtasdt0(xH,xE)|~sQ3_spl),
% 51.49/11.98 inference(forward_demodulation,[status(thm)],[f194,f973])).
% 51.49/11.98 fof(f1011,plain,(
% 51.49/11.98 sdtpldt0(xE,xH)=sdtpldt0(xH,xE)|~sQ2_spl),
% 51.49/11.98 inference(resolution,[status(thm)],[f649,f183])).
% 51.49/11.98 fof(f1181,definition,(
% 51.49/11.98 sQ14_spl <=> (aScalar0(sz0z00))),
% 51.49/11.98 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 51.49/11.98 fof(f1183,plain,(
% 51.49/11.98 ~aScalar0(sz0z00)|sQ14_spl),
% 51.49/11.98 inference(component_clause,[status(thm)],[f1181])).
% 51.49/11.98 fof(f1184,definition,(
% 51.49/11.98 sQ15_spl <=> (sdtlseqdt0(sz0z00,sz0z00))),
% 51.49/11.98 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 51.49/11.98 fof(f1189,plain,(
% 51.49/11.98 $false|sQ14_spl),
% 51.49/11.98 inference(forward_subsumption_resolution,[status(thm)],[f1183,f81])).
% 51.49/11.98 fof(f1190,plain,(
% 51.49/11.98 sQ14_spl),
% 51.49/11.98 inference(contradiction_clause,[status(thm)],[f1189])).
% 51.49/11.98 fof(f1292,plain,(
% 51.49/11.98 sdtasdt0(xH,sdtpldt0(xH,xE))=sdtpldt0(sdtasdt0(xH,xH),xP)|~sQ3_spl),
% 51.49/11.98 inference(backward_demodulation,[status(thm)],[f977,f610])).
% 51.49/11.98 fof(f1319,definition,(
% 51.49/11.98 sQ17_spl <=> (aDimensionOf0(xs)=sz00)),
% 51.49/11.98 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 51.49/11.98 fof(f1320,plain,(
% 51.49/11.98 aDimensionOf0(xs)=sz00|~sQ17_spl),
% 51.49/11.98 inference(component_clause,[status(thm)],[f1319])).
% 51.49/11.98 fof(f1400,plain,(
% 51.49/11.98 sdtasdt0(sdtpldt0(xE,xH),xH)=sdtpldt0(sdtasdt0(xH,xH),xP)|~sQ2_spl),
% 51.49/11.98 inference(backward_demodulation,[status(thm)],[f1011,f612])).
% 51.49/11.98 fof(f1409,plain,(
% 51.49/11.98 sdtpldt0(xP,sdtasdt0(xH,xH))=sdtpldt0(sdtasdt0(xH,xH),xP)|~sQ2_spl),
% 51.49/11.98 inference(forward_demodulation,[status(thm)],[f760,f1400])).
% 51.49/11.98 fof(f1443,definition,(
% 51.49/11.98 sQ30_spl <=> (aVector0(xs))),
% 51.49/11.98 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 51.49/11.98 fof(f1445,plain,(
% 51.49/11.98 ~aVector0(xs)|sQ30_spl),
% 51.49/11.98 inference(component_clause,[status(thm)],[f1443])).
% 51.49/11.98 fof(f1446,definition,(
% 51.49/11.98 sQ31_spl <=> (aVector0(xt))),
% 51.49/11.98 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 51.49/11.98 fof(f1448,plain,(
% 51.49/11.98 ~aVector0(xt)|sQ31_spl),
% 51.49/11.98 inference(component_clause,[status(thm)],[f1446])).
% 51.49/11.98 fof(f1491,plain,(
% 51.49/11.98 $false|sQ31_spl),
% 51.49/11.98 inference(forward_subsumption_resolution,[status(thm)],[f1448,f160])).
% 51.49/11.98 fof(f1492,plain,(
% 51.49/11.98 sQ31_spl),
% 51.49/11.98 inference(contradiction_clause,[status(thm)],[f1491])).
% 51.49/11.98 fof(f1493,plain,(
% 51.49/11.98 $false|sQ30_spl),
% 51.49/11.98 inference(forward_subsumption_resolution,[status(thm)],[f1445,f159])).
% 51.49/11.98 fof(f1494,plain,(
% 51.49/11.98 sQ30_spl),
% 51.49/11.98 inference(contradiction_clause,[status(thm)],[f1493])).
% 51.49/11.98 fof(f1572,plain,(
% 51.49/11.98 aNaturalNumber0(aDimensionOf0(xp))),
% 51.49/11.98 inference(resolution,[status(thm)],[f166,f137])).
% 51.49/11.98 fof(f1608,definition,(
% 51.49/11.98 sQ51_spl <=> (aVector0(xp))),
% 51.49/11.98 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 51.49/11.98 fof(f1610,plain,(
% 51.49/11.98 ~aVector0(xp)|sQ51_spl),
% 51.49/11.98 inference(component_clause,[status(thm)],[f1608])).
% 51.49/11.98 fof(f1622,definition,(
% 51.49/11.98 sQ55_spl <=> (aNaturalNumber0(aDimensionOf0(xp)))),
% 51.49/11.98 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 51.49/11.98 fof(f1624,plain,(
% 51.49/11.98 ~aNaturalNumber0(aDimensionOf0(xp))|sQ55_spl),
% 51.49/11.98 inference(component_clause,[status(thm)],[f1622])).
% 51.49/11.98 fof(f1628,plain,(
% 51.49/11.98 $false|sQ51_spl),
% 51.49/11.98 inference(forward_subsumption_resolution,[status(thm)],[f1610,f166])).
% 51.49/11.98 fof(f1629,plain,(
% 51.49/11.98 sQ51_spl),
% 51.49/11.98 inference(contradiction_clause,[status(thm)],[f1628])).
% 51.49/11.98 fof(f1630,plain,(
% 51.49/11.98 $false|~sQ17_spl),
% 51.49/11.98 inference(forward_subsumption_resolution,[status(thm)],[f1320,f164])).
% 51.49/11.98 fof(f1631,plain,(
% 51.49/11.98 ~sQ17_spl),
% 51.49/11.98 inference(contradiction_clause,[status(thm)],[f1630])).
% 51.49/11.98 fof(f1659,definition,(
% 51.49/11.98 sQ56_spl <=> (aScalar0(xP))),
% 51.49/11.98 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 51.49/11.98 fof(f1661,plain,(
% 51.49/11.98 ~aScalar0(xP)|sQ56_spl),
% 51.49/11.98 inference(component_clause,[status(thm)],[f1659])).
% 51.49/11.98 fof(f1674,definition,(
% 51.49/11.98 sQ60_spl <=> (sdtlseqdt0(xP,xP))),
% 51.49/11.98 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 51.49/11.98 fof(f1676,plain,(
% 51.49/11.98 ~sdtlseqdt0(xP,xP)|sQ60_spl),
% 51.49/11.98 inference(component_clause,[status(thm)],[f1674])).
% 51.49/11.98 fof(f1681,plain,(
% 51.49/11.98 $false|sQ56_spl),
% 51.49/11.98 inference(forward_subsumption_resolution,[status(thm)],[f1661,f193])).
% 51.49/11.98 fof(f1682,plain,(
% 51.49/11.98 sQ56_spl),
% 51.49/11.98 inference(contradiction_clause,[status(thm)],[f1681])).
% 51.49/11.98 fof(f1683,plain,(
% 51.49/11.98 $false|sQ60_spl),
% 51.49/11.98 inference(forward_subsumption_resolution,[status(thm)],[f1676,f315])).
% 51.49/11.98 fof(f1684,plain,(
% 51.49/11.98 sQ60_spl),
% 51.49/11.98 inference(contradiction_clause,[status(thm)],[f1683])).
% 51.49/11.98 fof(f1714,plain,(
% 51.49/11.98 ~sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH))=sdtpldt0(xP,sdtpldt0(sdtasdt0(xH,xH),xP))|~sQ2_spl|~sQ3_spl),
% 51.49/11.98 inference(backward_demodulation,[status(thm)],[f1715,f928])).
% 51.49/11.98 fof(f1715,plain,(
% 51.49/11.98 sdtasdt0(xH,sdtpldt0(xE,xH))=sdtpldt0(sdtasdt0(xH,xH),xP)|~sQ2_spl|~sQ3_spl),
% 51.49/11.98 inference(forward_demodulation,[status(thm)],[f1011,f1292])).
% 51.49/11.98 fof(f1721,definition,(
% 51.49/11.98 sQ62_spl <=> (aScalar0(xH))),
% 51.49/11.98 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 51.49/11.98 fof(f1723,plain,(
% 51.49/11.98 ~aScalar0(xH)|sQ62_spl),
% 51.49/11.98 inference(component_clause,[status(thm)],[f1721])).
% 51.49/11.98 fof(f1736,definition,(
% 51.49/11.98 sQ66_spl <=> (sdtlseqdt0(xH,xH))),
% 51.49/11.98 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 51.49/11.98 fof(f1738,plain,(
% 51.49/11.98 ~sdtlseqdt0(xH,xH)|sQ66_spl),
% 51.49/11.98 inference(component_clause,[status(thm)],[f1736])).
% 51.49/11.98 fof(f1743,plain,(
% 51.49/11.98 $false|sQ62_spl),
% 51.49/11.98 inference(forward_subsumption_resolution,[status(thm)],[f1723,f189])).
% 51.49/11.98 fof(f1744,plain,(
% 51.49/11.98 sQ62_spl),
% 51.49/11.98 inference(contradiction_clause,[status(thm)],[f1743])).
% 51.49/11.98 fof(f1745,plain,(
% 51.49/11.98 $false|sQ66_spl),
% 51.49/11.98 inference(forward_subsumption_resolution,[status(thm)],[f1738,f316])).
% 51.49/11.98 fof(f1746,plain,(
% 51.49/11.98 sQ66_spl),
% 51.49/11.98 inference(contradiction_clause,[status(thm)],[f1745])).
% 51.49/11.98 fof(f1779,plain,(
% 51.49/11.98 aNaturalNumber0(aDimensionOf0(xq))),
% 51.49/11.98 inference(resolution,[status(thm)],[f171,f137])).
% 51.49/11.98 fof(f1816,definition,(
% 51.49/11.98 sQ76_spl <=> (aVector0(xq))),
% 51.49/11.98 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 51.49/11.98 fof(f1818,plain,(
% 51.49/11.98 ~aVector0(xq)|sQ76_spl),
% 51.49/11.98 inference(component_clause,[status(thm)],[f1816])).
% 51.49/11.98 fof(f1830,definition,(
% 51.49/11.98 sQ80_spl <=> (aNaturalNumber0(aDimensionOf0(xq)))),
% 51.49/11.98 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 51.49/11.98 fof(f1832,plain,(
% 51.49/11.98 ~aNaturalNumber0(aDimensionOf0(xq))|sQ80_spl),
% 51.49/11.98 inference(component_clause,[status(thm)],[f1830])).
% 51.49/11.98 fof(f1836,plain,(
% 51.49/11.98 $false|sQ76_spl),
% 51.49/11.98 inference(forward_subsumption_resolution,[status(thm)],[f1818,f171])).
% 51.49/11.98 fof(f1837,plain,(
% 51.49/11.98 sQ76_spl),
% 51.49/11.98 inference(contradiction_clause,[status(thm)],[f1836])).
% 51.49/11.98 fof(f1841,plain,(
% 51.49/11.98 ~sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH))=sdtpldt0(xP,sdtpldt0(xP,sdtasdt0(xH,xH)))|~sQ2_spl|~sQ3_spl),
% 51.49/11.98 inference(backward_demodulation,[status(thm)],[f1409,f1714])).
% 51.49/11.98 fof(f1869,definition,(
% 51.49/11.98 sQ81_spl <=> (aScalar0(xE))),
% 51.49/11.98 introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 51.49/11.98 fof(f1871,plain,(
% 51.49/11.98 ~aScalar0(xE)|sQ81_spl),
% 51.49/11.98 inference(component_clause,[status(thm)],[f1869])).
% 51.49/11.98 fof(f1884,definition,(
% 51.49/11.98 sQ85_spl <=> (sdtlseqdt0(xE,xE))),
% 51.49/11.98 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 51.49/11.98 fof(f1886,plain,(
% 51.49/11.98 ~sdtlseqdt0(xE,xE)|sQ85_spl),
% 51.49/11.98 inference(component_clause,[status(thm)],[f1884])).
% 51.49/11.98 fof(f1891,plain,(
% 51.49/11.98 $false|sQ81_spl),
% 51.49/11.98 inference(forward_subsumption_resolution,[status(thm)],[f1871,f183])).
% 51.49/11.98 fof(f1892,plain,(
% 51.49/11.98 sQ81_spl),
% 51.49/11.98 inference(contradiction_clause,[status(thm)],[f1891])).
% 51.49/11.98 fof(f1893,plain,(
% 51.49/11.98 $false|sQ85_spl),
% 51.49/11.98 inference(forward_subsumption_resolution,[status(thm)],[f1886,f317])).
% 51.49/11.98 fof(f1894,plain,(
% 51.49/11.98 sQ85_spl),
% 51.49/11.98 inference(contradiction_clause,[status(thm)],[f1893])).
% 51.49/11.98 fof(f1973,plain,(
% 51.49/11.98 ![X0]: (~aScalar0(X0)|sdtlseqdt0(xA,X0)|sdtlseqdt0(X0,xA))),
% 51.49/11.98 inference(resolution,[status(thm)],[f175,f125])).
% 51.49/11.98 fof(f2231,plain,(
% 51.49/11.98 ![X0]: (~aScalar0(X0)|sdtlseqdt0(xB,X0)|sdtlseqdt0(X0,xB))),
% 51.49/11.98 inference(resolution,[status(thm)],[f177,f125])).
% 51.49/11.98 fof(f2826,plain,(
% 51.49/11.98 ![X0]: (~aScalar0(X0)|sdtlseqdt0(xC,X0)|sdtlseqdt0(X0,xC))),
% 51.49/11.98 inference(resolution,[status(thm)],[f179,f125])).
% 51.49/11.98 fof(f4379,definition,(
% 51.49/11.98 sQ88_spl <=> (aScalar0(sdtasdt0(xE,xP)))),
% 51.49/11.98 introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition])).
% 51.49/11.98 fof(f4381,plain,(
% 51.49/11.98 ~aScalar0(sdtasdt0(xE,xP))|sQ88_spl),
% 51.49/11.98 inference(component_clause,[status(thm)],[f4379])).
% 51.49/11.98 fof(f4387,plain,(
% 51.49/11.98 $false|sQ88_spl),
% 51.49/11.98 inference(forward_subsumption_resolution,[status(thm)],[f4381,f351])).
% 51.49/11.98 fof(f4388,plain,(
% 51.49/11.98 sQ88_spl),
% 51.49/11.98 inference(contradiction_clause,[status(thm)],[f4387])).
% 51.49/11.98 fof(f7514,plain,(
% 51.49/11.98 sdtlseqdt0(sz0z00,sz0z00)|sdtlseqdt0(sz0z00,sz0z00)),
% 51.49/11.98 inference(resolution,[status(thm)],[f808,f81])).
% 51.49/11.98 fof(f7604,plain,(
% 51.49/11.98 sQ15_spl),
% 51.49/11.98 inference(split_clause,[status(thm)],[f7514,f1184])).
% 51.49/11.98 fof(f8217,plain,(
% 51.49/11.98 $false|sQ7_spl),
% 51.49/11.98 inference(forward_subsumption_resolution,[status(thm)],[f936,f177])).
% 51.49/11.98 fof(f8218,plain,(
% 51.49/11.98 sQ7_spl),
% 51.49/11.98 inference(contradiction_clause,[status(thm)],[f8217])).
% 51.49/11.98 fof(f8219,plain,(
% 51.49/11.98 $false|sQ10_spl),
% 51.49/11.98 inference(forward_subsumption_resolution,[status(thm)],[f946,f175])).
% 51.49/11.98 fof(f8220,plain,(
% 51.49/11.98 sQ10_spl),
% 51.49/11.98 inference(contradiction_clause,[status(thm)],[f8219])).
% 51.49/11.98 fof(f8861,definition,(
% 51.49/11.98 sQ294_spl <=> (aDimensionOf0(xt)=aDimensionOf0(xs))),
% 51.49/11.98 introduced(definition,[new_symbols(definition,[sQ294_spl])],[split_symbol_definition])).
% 51.49/11.98 fof(f8863,plain,(
% 51.49/11.98 ~aDimensionOf0(xt)=aDimensionOf0(xs)|sQ294_spl),
% 51.49/11.98 inference(component_clause,[status(thm)],[f8861])).
% 51.49/11.98 fof(f8868,definition,(
% 51.49/11.98 sQ296_spl <=> (aDimensionOf0(xs)=aDimensionOf0(xs))),
% 51.49/11.98 introduced(definition,[new_symbols(definition,[sQ296_spl])],[split_symbol_definition])).
% 51.49/11.98 fof(f8870,plain,(
% 51.49/11.98 ~aDimensionOf0(xs)=aDimensionOf0(xs)|sQ296_spl),
% 51.49/11.98 inference(component_clause,[status(thm)],[f8868])).
% 51.49/11.98 fof(f8875,plain,(
% 51.49/11.98 ~aDimensionOf0(xs)=aDimensionOf0(xs)|sQ294_spl),
% 51.49/11.98 inference(forward_demodulation,[status(thm)],[f163,f8863])).
% 51.49/11.98 fof(f8876,plain,(
% 51.49/11.98 $false|sQ294_spl),
% 51.49/11.98 inference(trivial_equality_resolution,[status(thm)],[f8875])).
% 51.49/11.98 fof(f8877,plain,(
% 51.49/11.98 sQ294_spl),
% 51.49/11.98 inference(contradiction_clause,[status(thm)],[f8876])).
% 51.49/11.98 fof(f8878,plain,(
% 51.49/11.98 $false|sQ296_spl),
% 51.49/11.98 inference(trivial_equality_resolution,[status(thm)],[f8870])).
% 51.49/11.98 fof(f8879,plain,(
% 51.49/11.98 sQ296_spl),
% 51.49/11.98 inference(contradiction_clause,[status(thm)],[f8878])).
% 51.49/11.98 fof(f10800,definition,(
% 51.49/11.98 sQ335_spl <=> (aScalar0(xC))),
% 51.49/11.98 introduced(definition,[new_symbols(definition,[sQ335_spl])],[split_symbol_definition])).
% 51.49/11.98 fof(f10802,plain,(
% 51.49/11.98 ~aScalar0(xC)|sQ335_spl),
% 51.49/11.98 inference(component_clause,[status(thm)],[f10800])).
% 51.49/11.98 fof(f10827,plain,(
% 51.49/11.98 $false|sQ335_spl),
% 51.49/11.98 inference(forward_subsumption_resolution,[status(thm)],[f10802,f179])).
% 51.49/11.98 fof(f10828,plain,(
% 51.49/11.98 sQ335_spl),
% 51.49/11.98 inference(contradiction_clause,[status(thm)],[f10827])).
% 51.49/11.98 fof(f10979,definition,(
% 51.49/11.98 sQ346_spl <=> (aDimensionOf0(xp)=aDimensionOf0(xp))),
% 51.49/11.98 introduced(definition,[new_symbols(definition,[sQ346_spl])],[split_symbol_definition])).
% 51.49/11.98 fof(f10981,plain,(
% 51.49/11.98 ~aDimensionOf0(xp)=aDimensionOf0(xp)|sQ346_spl),
% 51.49/11.98 inference(component_clause,[status(thm)],[f10979])).
% 51.49/11.98 fof(f10997,plain,(
% 51.49/11.98 $false|sQ346_spl),
% 51.49/11.98 inference(trivial_equality_resolution,[status(thm)],[f10981])).
% 51.49/11.98 fof(f10998,plain,(
% 51.49/11.98 sQ346_spl),
% 51.49/11.98 inference(contradiction_clause,[status(thm)],[f10997])).
% 51.49/11.98 fof(f11000,plain,(
% 51.49/11.98 $false|sQ55_spl),
% 51.49/11.98 inference(forward_subsumption_resolution,[status(thm)],[f1624,f1572])).
% 51.49/11.98 fof(f11001,plain,(
% 51.49/11.98 sQ55_spl),
% 51.49/11.98 inference(contradiction_clause,[status(thm)],[f11000])).
% 51.49/11.98 fof(f11205,definition,(
% 51.49/11.98 sQ353_spl <=> (aScalar0(xD))),
% 51.49/11.98 introduced(definition,[new_symbols(definition,[sQ353_spl])],[split_symbol_definition])).
% 51.49/11.98 fof(f11207,plain,(
% 51.49/11.98 ~aScalar0(xD)|sQ353_spl),
% 51.49/11.98 inference(component_clause,[status(thm)],[f11205])).
% 51.49/11.98 fof(f11232,plain,(
% 51.49/11.98 $false|sQ353_spl),
% 51.49/11.98 inference(forward_subsumption_resolution,[status(thm)],[f11207,f181])).
% 51.49/11.98 fof(f11233,plain,(
% 51.49/11.98 sQ353_spl),
% 51.49/11.98 inference(contradiction_clause,[status(thm)],[f11232])).
% 51.49/11.98 fof(f11306,definition,(
% 51.49/11.98 sQ362_spl <=> (aDimensionOf0(xq)=aDimensionOf0(xq))),
% 51.49/11.98 introduced(definition,[new_symbols(definition,[sQ362_spl])],[split_symbol_definition])).
% 51.49/11.98 fof(f11308,plain,(
% 51.49/11.98 ~aDimensionOf0(xq)=aDimensionOf0(xq)|sQ362_spl),
% 51.49/11.98 inference(component_clause,[status(thm)],[f11306])).
% 51.49/11.98 fof(f11328,plain,(
% 51.49/11.98 $false|sQ362_spl),
% 51.49/11.98 inference(trivial_equality_resolution,[status(thm)],[f11308])).
% 51.49/11.98 fof(f11329,plain,(
% 51.49/11.98 sQ362_spl),
% 51.49/11.98 inference(contradiction_clause,[status(thm)],[f11328])).
% 51.49/11.98 fof(f11394,plain,(
% 51.49/11.98 $false|sQ80_spl),
% 51.49/11.98 inference(forward_subsumption_resolution,[status(thm)],[f1832,f1779])).
% 51.49/11.98 fof(f11395,plain,(
% 51.49/11.98 sQ80_spl),
% 51.49/11.98 inference(contradiction_clause,[status(thm)],[f11394])).
% 51.49/11.98 fof(f13255,definition,(
% 51.49/11.98 sQ383_spl <=> (aScalar0(xF))),
% 51.49/11.98 introduced(definition,[new_symbols(definition,[sQ383_spl])],[split_symbol_definition])).
% 51.49/11.98 fof(f13257,plain,(
% 51.49/11.98 ~aScalar0(xF)|sQ383_spl),
% 51.49/11.98 inference(component_clause,[status(thm)],[f13255])).
% 51.49/11.98 fof(f13279,plain,(
% 51.49/11.98 $false|sQ383_spl),
% 51.49/11.98 inference(forward_subsumption_resolution,[status(thm)],[f13257,f185])).
% 51.49/11.98 fof(f13280,plain,(
% 51.49/11.98 sQ383_spl),
% 51.49/11.98 inference(contradiction_clause,[status(thm)],[f13279])).
% 51.49/11.98 fof(f13558,plain,(
% 51.49/11.98 sdtlseqdt0(xA,xA)|sdtlseqdt0(xA,xA)),
% 51.49/11.98 inference(resolution,[status(thm)],[f1973,f175])).
% 51.49/11.98 fof(f13639,definition,(
% 51.49/11.98 sQ413_spl <=> (sdtlseqdt0(xA,xA))),
% 51.49/11.98 introduced(definition,[new_symbols(definition,[sQ413_spl])],[split_symbol_definition])).
% 51.49/11.98 fof(f13642,plain,(
% 51.49/11.98 sQ413_spl),
% 51.49/11.98 inference(split_clause,[status(thm)],[f13558,f13639])).
% 51.49/11.98 fof(f14415,definition,(
% 51.49/11.98 sQ425_spl <=> (aScalar0(xG))),
% 51.49/11.98 introduced(definition,[new_symbols(definition,[sQ425_spl])],[split_symbol_definition])).
% 51.49/11.98 fof(f14417,plain,(
% 51.49/11.98 ~aScalar0(xG)|sQ425_spl),
% 51.49/11.98 inference(component_clause,[status(thm)],[f14415])).
% 51.49/11.98 fof(f14442,plain,(
% 51.49/11.98 $false|sQ425_spl),
% 51.49/11.98 inference(forward_subsumption_resolution,[status(thm)],[f14417,f187])).
% 51.49/11.98 fof(f14443,plain,(
% 51.49/11.98 sQ425_spl),
% 51.49/11.98 inference(contradiction_clause,[status(thm)],[f14442])).
% 51.49/11.98 fof(f14455,plain,(
% 51.49/11.98 sdtlseqdt0(xB,xB)|sdtlseqdt0(xB,xB)),
% 51.49/11.98 inference(resolution,[status(thm)],[f2231,f177])).
% 51.49/11.98 fof(f14537,definition,(
% 51.49/11.98 sQ454_spl <=> (sdtlseqdt0(xB,xB))),
% 51.49/11.98 introduced(definition,[new_symbols(definition,[sQ454_spl])],[split_symbol_definition])).
% 51.49/11.98 fof(f14540,plain,(
% 51.49/11.98 sQ454_spl),
% 51.49/11.98 inference(split_clause,[status(thm)],[f14455,f14537])).
% 51.49/11.98 fof(f16597,plain,(
% 51.49/11.98 sdtlseqdt0(xC,xC)|sdtlseqdt0(xC,xC)),
% 51.49/11.98 inference(resolution,[status(thm)],[f2826,f179])).
% 51.49/11.98 fof(f16694,definition,(
% 21.29/12.02 sQ525_spl <=> (sdtlseqdt0(xC,xC))),
% 21.29/12.02 introduced(definition,[new_symbols(definition,[sQ525_spl])],[split_symbol_definition])).
% 21.29/12.02 fof(f16697,plain,(
% 21.29/12.02 sQ525_spl),
% 21.29/12.02 inference(split_clause,[status(thm)],[f16597,f16694])).
% 21.29/12.02 fof(f17273,plain,(
% 21.29/12.02 ![X0]: (~aScalar0(X0)|sdtpldt0(sdtpldt0(X0,xP),sdtasdt0(xH,xH))=sdtpldt0(X0,sdtpldt0(xP,sdtasdt0(xH,xH))))),
% 21.29/12.02 inference(resolution,[status(thm)],[f767,f272])).
% 21.29/12.02 fof(f18129,plain,(
% 21.29/12.02 sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH))=sdtpldt0(xP,sdtpldt0(xP,sdtasdt0(xH,xH)))),
% 21.29/12.02 inference(resolution,[status(thm)],[f17273,f193])).
% 21.29/12.02 fof(f18134,plain,(
% 21.29/12.02 $false|~sQ2_spl|~sQ3_spl),
% 21.29/12.02 inference(forward_subsumption_resolution,[status(thm)],[f18129,f1841])).
% 21.29/12.02 fof(f18135,plain,(
% 21.29/12.02 ~sQ2_spl|~sQ3_spl),
% 21.29/12.02 inference(contradiction_clause,[status(thm)],[f18134])).
% 21.29/12.02 fof(f18136,plain,(
% 21.29/12.02 $false),
% 21.29/12.02 inference(sat_refutation,[status(thm)],[f213,f217,f358,f1190,f1492,f1494,f1629,f1631,f1682,f1684,f1744,f1746,f1837,f1892,f1894,f4388,f7604,f8218,f8220,f8877,f8879,f10828,f10998,f11001,f11233,f11329,f11395,f13280,f13642,f14443,f14540,f16697,f18135])).
% 21.29/12.02 % SZS output end CNFRefutation for theBenchmark.p
% 21.29/12.05 % Elapsed time: 6.655637 seconds
% 21.29/12.05 % CPU time: 52.462379 seconds
% 21.29/12.05 % Total memory used: 634.427 MB
% 21.29/12.05 % Net memory used: 589.605 MB
%------------------------------------------------------------------------------