%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : RNG069+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 : n014.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:16 PM UTC 2026
% Result : Theorem 27.01s 3.87s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG069+2 : 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.08/0.35 % Computer : n014.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 04:17:38 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.13/0.37 % Drodi V4.1.1
% 27.01/3.87 % Refutation found
% 27.01/3.87 % SZS status Theorem for theBenchmark: Theorem is valid
% 27.01/3.87 % SZS output start CNFRefutation for theBenchmark
% 27.01/3.87 fof(f9,axiom,(
% 27.01/3.87 aScalar0(sz0z00) ),
% 27.01/3.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.01/3.87 fof(f10,axiom,(
% 27.01/3.87 (! [W0,W1] :( ( aScalar0(W0)& aScalar0(W1) )=> aScalar0(sdtpldt0(W0,W1)) ) )),
% 27.01/3.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.01/3.87 fof(f11,axiom,(
% 27.01/3.87 (! [W0,W1] :( ( aScalar0(W0)& aScalar0(W1) )=> aScalar0(sdtasdt0(W0,W1)) ) )),
% 27.01/3.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.01/3.87 fof(f12,axiom,(
% 27.01/3.87 (! [W0] :( aScalar0(W0)=> aScalar0(smndt0(W0)) ) )),
% 27.01/3.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.01/3.87 fof(f14,axiom,(
% 27.01/3.87 (! [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) ) ) )),
% 27.01/3.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.01/3.87 fof(f15,axiom,(
% 27.01/3.87 (! [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)) ) ) )),
% 27.01/3.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.01/3.87 fof(f16,axiom,(
% 27.01/3.87 (! [W0,W1,W2,W3] :( ( aScalar0(W0)& aScalar0(W1)& aScalar0(W2)& aScalar0(W3) )=> sdtasdt0(sdtpldt0(W0,W1),sdtpldt0(W2,W3)) = sdtpldt0(sdtpldt0(sdtasdt0(W0,W2),sdtasdt0(W0,W3)),sdtpldt0(sdtasdt0(W1,W2),sdtasdt0(W1,W3))) ) )),
% 27.01/3.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.01/3.87 fof(f25,axiom,(
% 27.01/3.87 (! [W0,W1] :( ( aScalar0(W0)& aScalar0(W1) )=> ( sdtlseqdt0(W0,W1)| sdtlseqdt0(W1,W0) ) ) )),
% 27.01/3.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.01/3.87 fof(f38,hypothesis,(
% 27.01/3.87 ( aVector0(xs)& aVector0(xt) ) ),
% 27.01/3.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.01/3.87 fof(f40,hypothesis,(
% 27.01/3.87 aDimensionOf0(xs) = aDimensionOf0(xt) ),
% 27.01/3.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.01/3.87 fof(f41,hypothesis,(
% 27.01/3.87 aDimensionOf0(xs) != sz00 ),
% 27.01/3.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.01/3.87 fof(f42,hypothesis,(
% 27.01/3.87 ( aVector0(xp)& szszuzczcdt0(aDimensionOf0(xp)) = aDimensionOf0(xs)& (! [W0] :( aNaturalNumber0(W0)=> sdtlbdtrb0(xp,W0) = sdtlbdtrb0(xs,W0) ))& xp = sziznziztdt0(xs) ) ),
% 27.01/3.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.01/3.87 fof(f43,hypothesis,(
% 27.01/3.87 ( aVector0(xq)& szszuzczcdt0(aDimensionOf0(xq)) = aDimensionOf0(xt)& (! [W0] :( aNaturalNumber0(W0)=> sdtlbdtrb0(xq,W0) = sdtlbdtrb0(xt,W0) ))& xq = sziznziztdt0(xt) ) ),
% 27.01/3.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.01/3.87 fof(f44,hypothesis,(
% 27.01/3.87 ( aScalar0(xA)& xA = sdtlbdtrb0(xs,aDimensionOf0(xs)) ) ),
% 27.01/3.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.01/3.87 fof(f45,hypothesis,(
% 27.01/3.87 ( aScalar0(xB)& xB = sdtlbdtrb0(xt,aDimensionOf0(xt)) ) ),
% 27.01/3.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.01/3.87 fof(f46,hypothesis,(
% 27.01/3.87 ( aScalar0(xC)& xC = sdtasasdt0(xp,xp) ) ),
% 27.01/3.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.01/3.87 fof(f47,hypothesis,(
% 27.01/3.87 ( aScalar0(xD)& xD = sdtasasdt0(xq,xq) ) ),
% 27.01/3.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.01/3.87 fof(f48,hypothesis,(
% 27.01/3.87 ( aScalar0(xE)& xE = sdtasasdt0(xp,xq) ) ),
% 27.01/3.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.01/3.87 fof(f49,hypothesis,(
% 27.01/3.87 ( aScalar0(xF)& xF = sdtasdt0(xA,xA) ) ),
% 27.01/3.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.01/3.87 fof(f50,hypothesis,(
% 27.01/3.87 ( aScalar0(xG)& xG = sdtasdt0(xB,xB) ) ),
% 27.01/3.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.01/3.87 fof(f51,hypothesis,(
% 27.01/3.87 ( aScalar0(xH)& xH = sdtasdt0(xA,xB) ) ),
% 27.01/3.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.01/3.87 fof(f52,hypothesis,(
% 27.01/3.87 ( aScalar0(xR)& xR = sdtasdt0(xC,xG) ) ),
% 27.01/3.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.01/3.87 fof(f53,hypothesis,(
% 27.01/3.87 ( aScalar0(xP)& xP = sdtasdt0(xE,xH) ) ),
% 27.01/3.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.01/3.87 fof(f54,hypothesis,(
% 27.01/3.87 ( aScalar0(xS)& xS = sdtasdt0(xF,xD) ) ),
% 27.01/3.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.01/3.88 fof(f55,hypothesis,(
% 27.01/3.88 ( aScalar0(xN)& xN = sdtasdt0(xR,xS) ) ),
% 27.01/3.88 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.01/3.88 fof(f61,hypothesis,(
% 27.01/3.88 sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP))),sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xR,xS)),sdtpldt0(sdtasdt0(xS,xR),sdtasdt0(xS,xS)))) ),
% 27.01/3.88 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.01/3.88 fof(f62,conjecture,(
% 27.01/3.88 sdtlseqdt0(sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)),sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS))) ),
% 27.01/3.88 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.01/3.88 fof(f63,negated_conjecture,(
% 27.01/3.88 ~(sdtlseqdt0(sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)),sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS))) )),
% 27.01/3.88 inference(negated_conjecture,[status(cth)],[f62])).
% 27.01/3.88 fof(f84,plain,(
% 27.01/3.88 aScalar0(sz0z00)),
% 27.01/3.88 inference(cnf_transformation,[status(thm)],[f9])).
% 27.01/3.88 fof(f85,plain,(
% 27.01/3.88 ![W0,W1]: ((~aScalar0(W0)|~aScalar0(W1))|aScalar0(sdtpldt0(W0,W1)))),
% 27.01/3.88 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 27.01/3.88 fof(f86,plain,(
% 27.01/3.88 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|aScalar0(sdtpldt0(X0,X1)))),
% 27.01/3.88 inference(cnf_transformation,[status(thm)],[f85])).
% 27.01/3.88 fof(f87,plain,(
% 27.01/3.88 ![W0,W1]: ((~aScalar0(W0)|~aScalar0(W1))|aScalar0(sdtasdt0(W0,W1)))),
% 27.01/3.88 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 27.01/3.88 fof(f88,plain,(
% 27.01/3.88 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|aScalar0(sdtasdt0(X0,X1)))),
% 27.01/3.88 inference(cnf_transformation,[status(thm)],[f87])).
% 27.01/3.88 fof(f89,plain,(
% 27.01/3.88 ![W0]: (~aScalar0(W0)|aScalar0(smndt0(W0)))),
% 27.01/3.88 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 27.01/3.88 fof(f90,plain,(
% 27.01/3.88 ![X0]: (~aScalar0(X0)|aScalar0(smndt0(X0)))),
% 27.01/3.88 inference(cnf_transformation,[status(thm)],[f89])).
% 27.01/3.88 fof(f100,plain,(
% 27.01/3.88 ![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)))),
% 27.01/3.88 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 27.01/3.88 fof(f102,plain,(
% 27.01/3.88 ![X0,X1,X2]: (~aScalar0(X0)|~aScalar0(X1)|~aScalar0(X2)|sdtpldt0(X0,X1)=sdtpldt0(X1,X0))),
% 27.01/3.88 inference(cnf_transformation,[status(thm)],[f100])).
% 27.01/3.88 fof(f104,plain,(
% 27.01/3.88 ![X0,X1,X2]: (~aScalar0(X0)|~aScalar0(X1)|~aScalar0(X2)|sdtasdt0(X0,X1)=sdtasdt0(X1,X0))),
% 27.01/3.88 inference(cnf_transformation,[status(thm)],[f100])).
% 27.01/3.88 fof(f105,plain,(
% 27.01/3.88 ![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))))),
% 27.01/3.88 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 27.01/3.88 fof(f106,plain,(
% 27.01/3.88 ![X0,X1,X2]: (~aScalar0(X0)|~aScalar0(X1)|~aScalar0(X2)|sdtasdt0(X0,sdtpldt0(X1,X2))=sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2)))),
% 27.01/3.88 inference(cnf_transformation,[status(thm)],[f105])).
% 27.01/3.88 fof(f107,plain,(
% 27.01/3.88 ![X0,X1,X2]: (~aScalar0(X0)|~aScalar0(X1)|~aScalar0(X2)|sdtasdt0(sdtpldt0(X0,X1),X2)=sdtpldt0(sdtasdt0(X0,X2),sdtasdt0(X1,X2)))),
% 27.01/3.88 inference(cnf_transformation,[status(thm)],[f105])).
% 27.01/3.88 fof(f108,plain,(
% 27.01/3.88 ![W0,W1,W2,W3]: ((((~aScalar0(W0)|~aScalar0(W1))|~aScalar0(W2))|~aScalar0(W3))|sdtasdt0(sdtpldt0(W0,W1),sdtpldt0(W2,W3))=sdtpldt0(sdtpldt0(sdtasdt0(W0,W2),sdtasdt0(W0,W3)),sdtpldt0(sdtasdt0(W1,W2),sdtasdt0(W1,W3))))),
% 27.01/3.88 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 27.01/3.88 fof(f109,plain,(
% 27.01/3.88 ![X0,X1,X2,X3]: (~aScalar0(X0)|~aScalar0(X1)|~aScalar0(X2)|~aScalar0(X3)|sdtasdt0(sdtpldt0(X0,X1),sdtpldt0(X2,X3))=sdtpldt0(sdtpldt0(sdtasdt0(X0,X2),sdtasdt0(X0,X3)),sdtpldt0(sdtasdt0(X1,X2),sdtasdt0(X1,X3))))),
% 27.01/3.88 inference(cnf_transformation,[status(thm)],[f108])).
% 27.01/3.88 fof(f127,plain,(
% 27.01/3.88 ![W0,W1]: ((~aScalar0(W0)|~aScalar0(W1))|(sdtlseqdt0(W0,W1)|sdtlseqdt0(W1,W0)))),
% 27.01/3.88 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 27.01/3.88 fof(f128,plain,(
% 27.01/3.88 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|sdtlseqdt0(X0,X1)|sdtlseqdt0(X1,X0))),
% 27.01/3.88 inference(cnf_transformation,[status(thm)],[f127])).
% 27.01/3.88 fof(f162,plain,(
% 27.01/3.88 aVector0(xs)),
% 27.01/3.88 inference(cnf_transformation,[status(thm)],[f38])).
% 27.01/3.88 fof(f163,plain,(
% 27.01/3.88 aVector0(xt)),
% 27.01/3.88 inference(cnf_transformation,[status(thm)],[f38])).
% 27.01/3.88 fof(f166,plain,(
% 27.01/3.88 aDimensionOf0(xs)=aDimensionOf0(xt)),
% 27.01/3.88 inference(cnf_transformation,[status(thm)],[f40])).
% 27.01/3.88 fof(f167,plain,(
% 27.01/3.88 ~aDimensionOf0(xs)=sz00),
% 27.01/3.88 inference(cnf_transformation,[status(thm)],[f41])).
% 27.01/3.88 fof(f168,plain,(
% 27.01/3.88 ((aVector0(xp)&szszuzczcdt0(aDimensionOf0(xp))=aDimensionOf0(xs))&(![W0]: (~aNaturalNumber0(W0)|sdtlbdtrb0(xp,W0)=sdtlbdtrb0(xs,W0))))&xp=sziznziztdt0(xs)),
% 27.01/3.88 inference(pre_NNF_transformation,[status(thm)],[f42])).
% 27.01/3.88 fof(f169,plain,(
% 27.01/3.88 aVector0(xp)),
% 27.01/3.88 inference(cnf_transformation,[status(thm)],[f168])).
% 27.01/3.88 fof(f173,plain,(
% 27.01/3.88 ((aVector0(xq)&szszuzczcdt0(aDimensionOf0(xq))=aDimensionOf0(xt))&(![W0]: (~aNaturalNumber0(W0)|sdtlbdtrb0(xq,W0)=sdtlbdtrb0(xt,W0))))&xq=sziznziztdt0(xt)),
% 27.01/3.88 inference(pre_NNF_transformation,[status(thm)],[f43])).
% 27.01/3.88 fof(f174,plain,(
% 27.01/3.88 aVector0(xq)),
% 27.01/3.88 inference(cnf_transformation,[status(thm)],[f173])).
% 27.01/3.88 fof(f178,plain,(
% 27.01/3.88 aScalar0(xA)),
% 27.01/3.88 inference(cnf_transformation,[status(thm)],[f44])).
% 27.01/3.88 fof(f180,plain,(
% 27.01/3.88 aScalar0(xB)),
% 27.01/3.88 inference(cnf_transformation,[status(thm)],[f45])).
% 27.01/3.88 fof(f182,plain,(
% 27.01/3.88 aScalar0(xC)),
% 27.01/3.88 inference(cnf_transformation,[status(thm)],[f46])).
% 27.01/3.88 fof(f184,plain,(
% 27.01/3.88 aScalar0(xD)),
% 27.01/3.88 inference(cnf_transformation,[status(thm)],[f47])).
% 27.01/3.88 fof(f186,plain,(
% 27.01/3.88 aScalar0(xE)),
% 27.01/3.88 inference(cnf_transformation,[status(thm)],[f48])).
% 27.01/3.88 fof(f188,plain,(
% 27.01/3.88 aScalar0(xF)),
% 27.01/3.88 inference(cnf_transformation,[status(thm)],[f49])).
% 27.01/3.88 fof(f190,plain,(
% 27.01/3.88 aScalar0(xG)),
% 27.01/3.88 inference(cnf_transformation,[status(thm)],[f50])).
% 27.01/3.88 fof(f192,plain,(
% 27.01/3.88 aScalar0(xH)),
% 27.01/3.88 inference(cnf_transformation,[status(thm)],[f51])).
% 27.01/3.88 fof(f194,plain,(
% 27.01/3.88 aScalar0(xR)),
% 27.01/3.88 inference(cnf_transformation,[status(thm)],[f52])).
% 27.01/3.88 fof(f196,plain,(
% 27.01/3.88 aScalar0(xP)),
% 27.01/3.88 inference(cnf_transformation,[status(thm)],[f53])).
% 27.01/3.88 fof(f198,plain,(
% 27.01/3.88 aScalar0(xS)),
% 27.01/3.88 inference(cnf_transformation,[status(thm)],[f54])).
% 27.01/3.88 fof(f200,plain,(
% 27.01/3.88 aScalar0(xN)),
% 27.01/3.88 inference(cnf_transformation,[status(thm)],[f55])).
% 27.01/3.88 fof(f201,plain,(
% 27.01/3.88 xN=sdtasdt0(xR,xS)),
% 27.01/3.88 inference(cnf_transformation,[status(thm)],[f55])).
% 27.01/3.88 fof(f207,plain,(
% 27.01/3.88 sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP))),sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xR,xS)),sdtpldt0(sdtasdt0(xS,xR),sdtasdt0(xS,xS))))),
% 27.01/3.88 inference(cnf_transformation,[status(thm)],[f61])).
% 27.01/3.88 fof(f208,plain,(
% 27.01/3.88 ~sdtlseqdt0(sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)),sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS)))),
% 27.01/3.88 inference(cnf_transformation,[status(thm)],[f63])).
% 27.01/3.88 fof(f209,definition,(
% 27.01/3.88 ![X0]: (sQ0_spl <=> (~aScalar0(X0)))),
% 27.01/3.88 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 27.01/3.88 fof(f210,plain,(
% 27.01/3.88 ![X0]: (~aScalar0(X0)|~sQ0_spl)),
% 27.01/3.88 inference(component_clause,[status(thm)],[f209])).
% 27.01/3.88 fof(f216,definition,(
% 27.01/3.88 ![X0,X1]: (sQ2_spl <=> (~aScalar0(X0)|~aScalar0(X1)|sdtpldt0(X0,X1)=sdtpldt0(X1,X0)))),
% 27.01/3.88 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 27.01/3.88 fof(f217,plain,(
% 27.01/3.88 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|sdtpldt0(X0,X1)=sdtpldt0(X1,X0)|~sQ2_spl)),
% 27.01/3.88 inference(component_clause,[status(thm)],[f216])).
% 27.01/3.88 fof(f219,plain,(
% 27.01/3.88 sQ2_spl|sQ0_spl),
% 27.01/3.88 inference(split_clause,[status(thm)],[f102,f216,f209])).
% 27.01/3.88 fof(f220,definition,(
% 27.01/3.88 ![X0,X1]: (sQ3_spl <=> (~aScalar0(X0)|~aScalar0(X1)|sdtasdt0(X0,X1)=sdtasdt0(X1,X0)))),
% 27.01/3.88 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 27.01/3.88 fof(f221,plain,(
% 27.01/3.88 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|sdtasdt0(X0,X1)=sdtasdt0(X1,X0)|~sQ3_spl)),
% 27.01/3.88 inference(component_clause,[status(thm)],[f220])).
% 27.01/3.88 fof(f223,plain,(
% 27.01/3.88 sQ3_spl|sQ0_spl),
% 27.01/3.88 inference(split_clause,[status(thm)],[f104,f220,f209])).
% 27.01/3.88 fof(f224,plain,(
% 27.01/3.88 ![X0]: (~aScalar0(X0)|aScalar0(sdtpldt0(xR,X0)))),
% 27.01/3.88 inference(resolution,[status(thm)],[f86,f194])).
% 27.01/3.88 fof(f225,plain,(
% 27.01/3.88 ![X0]: (~aScalar0(X0)|aScalar0(sdtpldt0(xP,X0)))),
% 27.01/3.88 inference(resolution,[status(thm)],[f196,f86])).
% 27.01/3.88 fof(f231,plain,(
% 27.01/3.88 ![X0]: (~aScalar0(X0)|aScalar0(sdtasdt0(xP,X0)))),
% 27.01/3.88 inference(resolution,[status(thm)],[f88,f196])).
% 27.01/3.88 fof(f243,plain,(
% 27.01/3.88 $false|~sQ0_spl),
% 27.01/3.88 inference(backward_subsumption_resolution,[status(thm)],[f198,f210])).
% 27.01/3.88 fof(f246,plain,(
% 27.01/3.88 ~sQ0_spl),
% 27.01/3.88 inference(contradiction_clause,[status(thm)],[f243])).
% 27.01/3.88 fof(f248,plain,(
% 27.01/3.88 ![X0]: (~aScalar0(X0)|sdtlseqdt0(xR,X0)|sdtlseqdt0(X0,xR))),
% 27.01/3.88 inference(resolution,[status(thm)],[f128,f194])).
% 27.01/3.88 fof(f249,plain,(
% 27.01/3.88 ![X0]: (~aScalar0(X0)|sdtlseqdt0(xP,X0)|sdtlseqdt0(X0,xP))),
% 27.01/3.88 inference(resolution,[status(thm)],[f128,f196])).
% 27.01/3.88 fof(f250,plain,(
% 27.01/3.88 ![X0]: (~aScalar0(X0)|sdtlseqdt0(xS,X0)|sdtlseqdt0(X0,xS))),
% 27.01/3.88 inference(resolution,[status(thm)],[f128,f198])).
% 27.01/3.88 fof(f251,plain,(
% 27.01/3.88 sdtlseqdt0(xR,xR)|sdtlseqdt0(xR,xR)),
% 27.01/3.88 inference(resolution,[status(thm)],[f248,f194])).
% 27.01/3.88 fof(f254,definition,(
% 27.01/3.88 sQ4_spl <=> (sdtlseqdt0(xR,xR))),
% 27.01/3.88 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 27.01/3.88 fof(f257,plain,(
% 27.01/3.88 sQ4_spl),
% 27.01/3.88 inference(split_clause,[status(thm)],[f251,f254])).
% 27.01/3.88 fof(f273,plain,(
% 27.01/3.88 sdtlseqdt0(xP,xP)|sdtlseqdt0(xP,xP)),
% 27.01/3.88 inference(resolution,[status(thm)],[f249,f196])).
% 27.01/3.88 fof(f276,definition,(
% 27.01/3.88 sQ9_spl <=> (sdtlseqdt0(xP,xP))),
% 27.01/3.88 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 27.01/3.88 fof(f279,plain,(
% 27.01/3.88 sQ9_spl),
% 27.01/3.88 inference(split_clause,[status(thm)],[f273,f276])).
% 27.01/3.88 fof(f289,plain,(
% 27.01/3.88 sdtlseqdt0(xS,xS)|sdtlseqdt0(xS,xS)),
% 27.01/3.88 inference(resolution,[status(thm)],[f250,f198])).
% 27.01/3.88 fof(f292,definition,(
% 27.01/3.88 sQ12_spl <=> (sdtlseqdt0(xS,xS))),
% 27.01/3.88 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 27.01/3.88 fof(f295,plain,(
% 27.01/3.88 sQ12_spl),
% 27.01/3.88 inference(split_clause,[status(thm)],[f289,f292])).
% 27.01/3.88 fof(f327,definition,(
% 27.01/3.88 sQ16_spl <=> (aScalar0(xP))),
% 27.01/3.88 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 27.01/3.88 fof(f329,plain,(
% 27.01/3.88 ~aScalar0(xP)|sQ16_spl),
% 27.01/3.88 inference(component_clause,[status(thm)],[f327])).
% 27.01/3.88 fof(f330,definition,(
% 27.01/3.88 sQ17_spl <=> (aScalar0(xR))),
% 27.01/3.88 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 27.01/3.88 fof(f332,plain,(
% 27.01/3.88 ~aScalar0(xR)|sQ17_spl),
% 27.01/3.88 inference(component_clause,[status(thm)],[f330])).
% 27.01/3.88 fof(f337,definition,(
% 27.01/3.88 sQ19_spl <=> (aScalar0(xS))),
% 27.01/3.88 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 27.01/3.88 fof(f339,plain,(
% 27.01/3.88 ~aScalar0(xS)|sQ19_spl),
% 27.01/3.88 inference(component_clause,[status(thm)],[f337])).
% 27.01/3.88 fof(f360,plain,(
% 27.01/3.88 $false|sQ17_spl),
% 27.01/3.88 inference(forward_subsumption_resolution,[status(thm)],[f332,f194])).
% 27.01/3.88 fof(f361,plain,(
% 27.01/3.88 sQ17_spl),
% 27.01/3.88 inference(contradiction_clause,[status(thm)],[f360])).
% 27.01/3.88 fof(f362,plain,(
% 27.01/3.88 $false|sQ16_spl),
% 27.01/3.88 inference(forward_subsumption_resolution,[status(thm)],[f329,f196])).
% 27.01/3.88 fof(f363,plain,(
% 27.01/3.88 sQ16_spl),
% 27.01/3.88 inference(contradiction_clause,[status(thm)],[f362])).
% 27.01/3.88 fof(f364,plain,(
% 27.01/3.88 $false|sQ19_spl),
% 27.01/3.88 inference(forward_subsumption_resolution,[status(thm)],[f339,f198])).
% 27.01/3.88 fof(f365,plain,(
% 27.01/3.88 sQ19_spl),
% 27.01/3.88 inference(contradiction_clause,[status(thm)],[f364])).
% 27.01/3.88 fof(f413,plain,(
% 27.01/3.88 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|sdtasdt0(X0,sdtpldt0(xR,X1))=sdtpldt0(sdtasdt0(X0,xR),sdtasdt0(X0,X1)))),
% 27.01/3.88 inference(resolution,[status(thm)],[f106,f194])).
% 27.01/3.88 fof(f414,plain,(
% 27.01/3.88 ![X0]: (~aScalar0(X0)|sdtasdt0(X0,sdtpldt0(xP,xP))=sdtpldt0(sdtasdt0(X0,xP),sdtasdt0(X0,xP)))),
% 27.01/3.88 inference(resolution,[status(thm)],[f106,f196])).
% 27.01/3.88 fof(f417,plain,(
% 27.01/3.88 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|sdtasdt0(X0,sdtpldt0(xS,X1))=sdtpldt0(sdtasdt0(X0,xS),sdtasdt0(X0,X1)))),
% 27.01/3.88 inference(resolution,[status(thm)],[f106,f198])).
% 27.01/3.88 fof(f427,plain,(
% 27.01/3.88 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|sdtasdt0(sdtpldt0(X0,xS),X1)=sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(xS,X1)))),
% 27.01/3.88 inference(resolution,[status(thm)],[f107,f198])).
% 27.01/3.88 fof(f430,plain,(
% 27.01/3.88 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|sdtasdt0(sdtpldt0(X0,X1),xS)=sdtpldt0(sdtasdt0(X0,xS),sdtasdt0(X1,xS)))),
% 27.01/3.88 inference(resolution,[status(thm)],[f107,f198])).
% 27.01/3.88 fof(f434,plain,(
% 27.01/3.88 ![X0]: (~aScalar0(X0)|sdtasdt0(sdtpldt0(X0,xP),sdtpldt0(xP,xP))=sdtpldt0(sdtpldt0(sdtasdt0(X0,xP),sdtasdt0(X0,xP)),sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP))))),
% 27.01/3.88 inference(resolution,[status(thm)],[f109,f196])).
% 27.01/3.88 fof(f444,plain,(
% 27.01/3.88 ![X0,X1,X2]: (~aScalar0(X0)|~aScalar0(X1)|~aScalar0(X2)|sdtasdt0(sdtpldt0(X0,X1),sdtpldt0(X2,xR))=sdtpldt0(sdtpldt0(sdtasdt0(X0,X2),sdtasdt0(X0,xR)),sdtpldt0(sdtasdt0(X1,X2),sdtasdt0(X1,xR))))),
% 27.01/3.88 inference(resolution,[status(thm)],[f109,f194])).
% 27.01/3.88 fof(f526,plain,(
% 27.01/3.88 ![X0]: (~aScalar0(X0)|sdtpldt0(X0,xR)=sdtpldt0(xR,X0)|~sQ2_spl)),
% 27.01/3.88 inference(resolution,[status(thm)],[f217,f194])).
% 27.01/3.88 fof(f567,plain,(
% 27.01/3.88 sdtpldt0(xS,xR)=sdtpldt0(xR,xS)|~sQ2_spl),
% 27.01/3.88 inference(resolution,[status(thm)],[f526,f198])).
% 27.01/3.88 fof(f569,plain,(
% 27.01/3.88 ~sdtlseqdt0(sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)),sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xS,xR)))|~sQ2_spl),
% 27.01/3.88 inference(backward_demodulation,[status(thm)],[f567,f208])).
% 27.01/3.88 fof(f570,plain,(
% 27.01/3.88 ~sdtlseqdt0(sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)),sdtasdt0(sdtpldt0(xS,xR),sdtpldt0(xS,xR)))|~sQ2_spl),
% 27.01/3.88 inference(forward_demodulation,[status(thm)],[f567,f569])).
% 27.01/3.88 fof(f588,plain,(
% 27.01/3.88 ![X0]: (~aScalar0(X0)|sdtasdt0(X0,xR)=sdtasdt0(xR,X0)|~sQ3_spl)),
% 27.01/3.88 inference(resolution,[status(thm)],[f221,f194])).
% 27.01/3.88 fof(f601,plain,(
% 27.01/3.88 aScalar0(sdtpldt0(xR,xR))),
% 27.01/3.88 inference(resolution,[status(thm)],[f224,f194])).
% 27.01/3.88 fof(f607,plain,(
% 27.01/3.88 aScalar0(sdtpldt0(xP,xP))),
% 27.01/3.88 inference(resolution,[status(thm)],[f225,f196])).
% 27.01/3.88 fof(f641,plain,(
% 27.01/3.88 sdtasdt0(xS,xR)=sdtasdt0(xR,xS)|~sQ3_spl),
% 27.01/3.88 inference(resolution,[status(thm)],[f588,f198])).
% 27.01/3.88 fof(f646,plain,(
% 27.01/3.88 sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP))),sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xR)),sdtpldt0(sdtasdt0(xS,xR),sdtasdt0(xS,xS))))|~sQ3_spl),
% 27.01/3.88 inference(backward_demodulation,[status(thm)],[f641,f207])).
% 27.01/3.88 fof(f732,plain,(
% 27.01/3.88 ![X0]: (~aScalar0(X0)|sdtlseqdt0(sz0z00,X0)|sdtlseqdt0(X0,sz0z00))),
% 27.01/3.88 inference(resolution,[status(thm)],[f84,f128])).
% 27.01/3.88 fof(f754,plain,(
% 27.01/3.88 sdtlseqdt0(sz0z00,sz0z00)|sdtlseqdt0(sz0z00,sz0z00)),
% 27.01/3.88 inference(resolution,[status(thm)],[f732,f84])).
% 27.01/3.88 fof(f758,definition,(
% 27.01/3.88 sQ66_spl <=> (sdtlseqdt0(sz0z00,sz0z00))),
% 27.01/3.88 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 27.01/3.88 fof(f761,plain,(
% 27.01/3.88 sQ66_spl),
% 27.01/3.88 inference(split_clause,[status(thm)],[f754,f758])).
% 27.01/3.88 fof(f860,plain,(
% 27.01/3.88 ![X0]: (~aScalar0(X0)|sdtasdt0(X0,sdtpldt0(xR,xS))=sdtpldt0(sdtasdt0(X0,xR),sdtasdt0(X0,xS)))),
% 27.01/3.88 inference(resolution,[status(thm)],[f413,f198])).
% 27.01/3.88 fof(f862,plain,(
% 27.01/3.88 ![X0]: (~aScalar0(X0)|sdtasdt0(X0,sdtpldt0(xS,xR))=sdtpldt0(sdtasdt0(X0,xR),sdtasdt0(X0,xS))|~sQ2_spl)),
% 27.01/3.88 inference(forward_demodulation,[status(thm)],[f567,f860])).
% 27.01/3.88 fof(f865,plain,(
% 27.01/3.88 sdtasdt0(xP,sdtpldt0(xP,xP))=sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP))),
% 27.01/3.88 inference(resolution,[status(thm)],[f414,f196])).
% 27.01/3.88 fof(f883,plain,(
% 27.01/3.88 ![X0]: (~aScalar0(X0)|sdtasdt0(X0,sdtpldt0(xS,xR))=sdtpldt0(sdtasdt0(X0,xS),sdtasdt0(X0,xR)))),
% 27.01/3.88 inference(resolution,[status(thm)],[f417,f194])).
% 27.01/3.88 fof(f939,plain,(
% 27.01/3.88 sdtasdt0(xS,xR)=xN|~sQ3_spl),
% 27.01/3.88 inference(backward_demodulation,[status(thm)],[f201,f641])).
% 27.01/3.88 fof(f942,plain,(
% 27.01/3.88 sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP))),sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xR)),sdtpldt0(xN,sdtasdt0(xS,xS))))|~sQ3_spl),
% 27.01/3.88 inference(backward_demodulation,[status(thm)],[f939,f646])).
% 27.01/3.88 fof(f943,plain,(
% 27.01/3.88 sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP))),sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),xN),sdtpldt0(xN,sdtasdt0(xS,xS))))|~sQ3_spl),
% 27.01/3.88 inference(forward_demodulation,[status(thm)],[f939,f942])).
% 27.01/3.88 fof(f949,plain,(
% 27.01/3.88 aScalar0(smndt0(xR))),
% 27.01/3.88 inference(resolution,[status(thm)],[f90,f194])).
% 27.01/3.88 fof(f950,plain,(
% 27.01/3.88 aScalar0(smndt0(xP))),
% 27.01/3.88 inference(resolution,[status(thm)],[f90,f196])).
% 27.01/3.88 fof(f951,plain,(
% 27.01/3.88 aScalar0(smndt0(xS))),
% 27.01/3.88 inference(resolution,[status(thm)],[f90,f198])).
% 27.01/3.88 fof(f982,plain,(
% 27.01/3.88 ![X0]: (~aScalar0(X0)|sdtasdt0(sdtpldt0(X0,xS),xR)=sdtpldt0(sdtasdt0(X0,xR),sdtasdt0(xS,xR)))),
% 27.01/3.88 inference(resolution,[status(thm)],[f427,f194])).
% 27.01/3.88 fof(f986,plain,(
% 27.01/3.88 ![X0]: (~aScalar0(X0)|sdtasdt0(sdtpldt0(X0,xS),xR)=sdtpldt0(sdtasdt0(X0,xR),xN)|~sQ3_spl)),
% 27.01/3.88 inference(forward_demodulation,[status(thm)],[f939,f982])).
% 27.01/3.88 fof(f1020,plain,(
% 27.01/3.88 ![X0]: (~aScalar0(X0)|sdtasdt0(sdtpldt0(X0,xR),xS)=sdtpldt0(sdtasdt0(X0,xS),sdtasdt0(xR,xS)))),
% 27.01/3.88 inference(resolution,[status(thm)],[f430,f194])).
% 27.01/3.88 fof(f1023,plain,(
% 27.01/3.88 ![X0]: (~aScalar0(X0)|sdtasdt0(sdtpldt0(X0,xR),xS)=sdtpldt0(sdtasdt0(X0,xS),xN))),
% 27.01/3.88 inference(forward_demodulation,[status(thm)],[f201,f1020])).
% 27.01/3.88 fof(f1148,plain,(
% 27.01/3.88 sdtasdt0(sdtpldt0(xR,xS),xR)=sdtpldt0(sdtasdt0(xR,xR),xN)|~sQ3_spl),
% 27.01/3.88 inference(resolution,[status(thm)],[f986,f194])).
% 27.01/3.88 fof(f1153,plain,(
% 27.01/3.88 sdtasdt0(sdtpldt0(xS,xR),xR)=sdtpldt0(sdtasdt0(xR,xR),xN)|~sQ2_spl|~sQ3_spl),
% 27.01/3.88 inference(forward_demodulation,[status(thm)],[f567,f1148])).
% 27.01/3.88 fof(f1156,plain,(
% 27.01/3.88 sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP))),sdtpldt0(sdtasdt0(sdtpldt0(xS,xR),xR),sdtpldt0(xN,sdtasdt0(xS,xS))))|~sQ2_spl|~sQ3_spl),
% 27.01/3.88 inference(backward_demodulation,[status(thm)],[f1153,f943])).
% 27.01/3.88 fof(f1160,plain,(
% 27.01/3.88 sdtasdt0(sdtpldt0(xS,xR),xS)=sdtpldt0(sdtasdt0(xS,xS),xN)),
% 27.01/3.88 inference(resolution,[status(thm)],[f1023,f198])).
% 27.01/3.88 fof(f1271,plain,(
% 27.01/3.88 ![X0]: (~aScalar0(X0)|sdtasdt0(sdtpldt0(X0,xS),sdtpldt0(xS,xR))=sdtpldt0(sdtpldt0(sdtasdt0(X0,xS),sdtasdt0(X0,xR)),sdtpldt0(sdtasdt0(xS,xS),sdtasdt0(xS,xR))))),
% 27.01/3.88 inference(resolution,[status(thm)],[f444,f198])).
% 27.01/3.88 fof(f1279,plain,(
% 27.01/3.88 ![X0]: (~aScalar0(X0)|sdtasdt0(sdtpldt0(X0,xS),sdtpldt0(xS,xR))=sdtpldt0(sdtpldt0(sdtasdt0(X0,xS),sdtasdt0(X0,xR)),sdtpldt0(sdtasdt0(xS,xS),xN))|~sQ3_spl)),
% 27.01/3.88 inference(forward_demodulation,[status(thm)],[f939,f1271])).
% 27.01/3.88 fof(f1280,plain,(
% 27.01/3.88 ![X0]: (~aScalar0(X0)|sdtasdt0(sdtpldt0(X0,xS),sdtpldt0(xS,xR))=sdtpldt0(sdtpldt0(sdtasdt0(X0,xS),sdtasdt0(X0,xR)),sdtasdt0(sdtpldt0(xS,xR),xS))|~sQ3_spl)),
% 27.01/3.88 inference(forward_demodulation,[status(thm)],[f1160,f1279])).
% 27.01/3.88 fof(f1370,plain,(
% 27.01/3.88 sdtasdt0(xR,sdtpldt0(xS,xR))=sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xR,xS))|~sQ2_spl),
% 27.01/3.88 inference(resolution,[status(thm)],[f862,f194])).
% 27.01/3.88 fof(f1372,plain,(
% 27.01/3.88 sdtasdt0(xS,sdtpldt0(xS,xR))=sdtpldt0(sdtasdt0(xS,xR),sdtasdt0(xS,xS))|~sQ2_spl),
% 27.01/3.88 inference(resolution,[status(thm)],[f862,f198])).
% 27.01/3.88 fof(f1376,plain,(
% 27.01/3.88 sdtasdt0(xR,sdtpldt0(xS,xR))=sdtpldt0(sdtasdt0(xR,xR),xN)|~sQ2_spl),
% 27.01/3.88 inference(forward_demodulation,[status(thm)],[f201,f1370])).
% 27.01/3.88 fof(f1378,plain,(
% 27.01/3.88 sdtasdt0(xS,sdtpldt0(xS,xR))=sdtpldt0(xN,sdtasdt0(xS,xS))|~sQ3_spl|~sQ2_spl),
% 27.01/3.88 inference(forward_demodulation,[status(thm)],[f939,f1372])).
% 27.01/3.88 fof(f1379,plain,(
% 27.01/3.88 sdtasdt0(sdtpldt0(xS,xR),xR)=sdtasdt0(xR,sdtpldt0(xS,xR))|~sQ2_spl|~sQ3_spl),
% 27.01/3.88 inference(backward_demodulation,[status(thm)],[f1376,f1153])).
% 27.01/3.88 fof(f1381,plain,(
% 27.01/3.88 sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP))),sdtpldt0(sdtasdt0(sdtpldt0(xS,xR),xR),sdtasdt0(xS,sdtpldt0(xS,xR))))|~sQ2_spl|~sQ3_spl),
% 27.01/3.88 inference(backward_demodulation,[status(thm)],[f1378,f1156])).
% 27.01/3.88 fof(f1441,plain,(
% 27.01/3.88 sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP))),sdtpldt0(sdtasdt0(xR,sdtpldt0(xS,xR)),sdtasdt0(xS,sdtpldt0(xS,xR))))|~sQ2_spl|~sQ3_spl),
% 27.01/3.88 inference(backward_demodulation,[status(thm)],[f1379,f1381])).
% 27.01/3.88 fof(f1445,plain,(
% 27.01/3.88 ![X0]: (~aScalar0(X0)|sdtasdt0(sdtpldt0(X0,xP),sdtpldt0(xP,xP))=sdtpldt0(sdtpldt0(sdtasdt0(X0,xP),sdtasdt0(X0,xP)),sdtasdt0(xP,sdtpldt0(xP,xP))))),
% 27.01/3.88 inference(backward_demodulation,[status(thm)],[f865,f434])).
% 27.01/3.88 fof(f1458,plain,(
% 27.01/3.88 sdtlseqdt0(sdtpldt0(sdtasdt0(xP,sdtpldt0(xP,xP)),sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP))),sdtpldt0(sdtasdt0(xR,sdtpldt0(xS,xR)),sdtasdt0(xS,sdtpldt0(xS,xR))))|~sQ2_spl|~sQ3_spl),
% 27.01/3.88 inference(forward_demodulation,[status(thm)],[f865,f1441])).
% 27.01/3.88 fof(f1459,plain,(
% 27.01/3.88 sdtlseqdt0(sdtpldt0(sdtasdt0(xP,sdtpldt0(xP,xP)),sdtasdt0(xP,sdtpldt0(xP,xP))),sdtpldt0(sdtasdt0(xR,sdtpldt0(xS,xR)),sdtasdt0(xS,sdtpldt0(xS,xR))))|~sQ2_spl|~sQ3_spl),
% 27.01/3.88 inference(forward_demodulation,[status(thm)],[f865,f1458])).
% 27.01/3.88 fof(f1487,definition,(
% 27.01/3.88 sQ88_spl <=> (aScalar0(sdtasdt0(xP,sdtpldt0(xP,xP))))),
% 27.01/3.88 introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition])).
% 27.01/3.88 fof(f1489,plain,(
% 27.01/3.88 ~aScalar0(sdtasdt0(xP,sdtpldt0(xP,xP)))|sQ88_spl),
% 27.01/3.88 inference(component_clause,[status(thm)],[f1487])).
% 27.01/3.88 fof(f1606,plain,(
% 27.01/3.88 sdtasdt0(xR,sdtpldt0(xS,xR))=sdtpldt0(sdtasdt0(xR,xS),sdtasdt0(xR,xR))),
% 27.01/3.88 inference(resolution,[status(thm)],[f883,f194])).
% 27.01/3.88 fof(f1608,plain,(
% 27.01/3.88 sdtasdt0(xS,sdtpldt0(xS,xR))=sdtpldt0(sdtasdt0(xS,xS),sdtasdt0(xS,xR))),
% 27.01/3.88 inference(resolution,[status(thm)],[f883,f198])).
% 27.01/3.88 fof(f1612,plain,(
% 27.01/3.88 sdtasdt0(xR,sdtpldt0(xS,xR))=sdtpldt0(xN,sdtasdt0(xR,xR))),
% 27.01/3.88 inference(forward_demodulation,[status(thm)],[f201,f1606])).
% 27.01/3.88 fof(f1614,plain,(
% 27.01/3.88 sdtasdt0(xS,sdtpldt0(xS,xR))=sdtpldt0(sdtasdt0(xS,xS),xN)|~sQ3_spl),
% 27.01/3.88 inference(forward_demodulation,[status(thm)],[f939,f1608])).
% 27.01/3.88 fof(f1615,plain,(
% 27.01/3.88 sdtasdt0(sdtpldt0(xS,xR),xS)=sdtasdt0(xS,sdtpldt0(xS,xR))|~sQ3_spl),
% 27.01/3.88 inference(backward_demodulation,[status(thm)],[f1614,f1160])).
% 27.01/3.88 fof(f1886,definition,(
% 27.01/3.88 sQ101_spl <=> (aScalar0(sz0z00))),
% 27.01/3.88 introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition])).
% 27.01/3.88 fof(f1888,plain,(
% 27.01/3.88 ~aScalar0(sz0z00)|sQ101_spl),
% 27.01/3.88 inference(component_clause,[status(thm)],[f1886])).
% 27.01/3.88 fof(f1905,plain,(
% 27.01/3.88 $false|sQ101_spl),
% 27.01/3.88 inference(forward_subsumption_resolution,[status(thm)],[f1888,f84])).
% 27.01/3.88 fof(f1906,plain,(
% 27.01/3.88 sQ101_spl),
% 27.01/3.88 inference(contradiction_clause,[status(thm)],[f1905])).
% 27.01/3.88 fof(f2095,plain,(
% 27.01/3.88 ![X0]: (~aScalar0(X0)|sdtlseqdt0(smndt0(xR),X0)|sdtlseqdt0(X0,smndt0(xR)))),
% 27.01/3.88 inference(resolution,[status(thm)],[f949,f128])).
% 27.01/3.88 fof(f2124,plain,(
% 27.01/3.88 sdtlseqdt0(smndt0(xR),smndt0(xR))|sdtlseqdt0(smndt0(xR),smndt0(xR))),
% 27.01/3.88 inference(resolution,[status(thm)],[f2095,f949])).
% 27.01/3.88 fof(f2129,definition,(
% 27.01/3.88 sQ114_spl <=> (sdtlseqdt0(smndt0(xR),smndt0(xR)))),
% 27.01/3.88 introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition])).
% 27.01/3.88 fof(f2132,plain,(
% 27.01/3.88 sQ114_spl),
% 27.01/3.88 inference(split_clause,[status(thm)],[f2124,f2129])).
% 27.01/3.88 fof(f2369,plain,(
% 27.01/3.88 ![X0]: (~aScalar0(X0)|sdtlseqdt0(smndt0(xP),X0)|sdtlseqdt0(X0,smndt0(xP)))),
% 27.01/3.88 inference(resolution,[status(thm)],[f950,f128])).
% 27.01/3.88 fof(f2405,plain,(
% 27.01/3.88 sdtlseqdt0(smndt0(xP),smndt0(xP))|sdtlseqdt0(smndt0(xP),smndt0(xP))),
% 27.01/3.88 inference(resolution,[status(thm)],[f2369,f950])).
% 27.01/3.88 fof(f2411,definition,(
% 27.01/3.88 sQ125_spl <=> (sdtlseqdt0(smndt0(xP),smndt0(xP)))),
% 27.01/3.88 introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition])).
% 27.01/3.88 fof(f2414,plain,(
% 27.01/3.88 sQ125_spl),
% 27.01/3.88 inference(split_clause,[status(thm)],[f2405,f2411])).
% 27.01/3.88 fof(f2613,plain,(
% 27.01/3.88 ![X0]: (~aScalar0(X0)|sdtlseqdt0(smndt0(xS),X0)|sdtlseqdt0(X0,smndt0(xS)))),
% 27.01/3.88 inference(resolution,[status(thm)],[f951,f128])).
% 27.01/3.88 fof(f2656,plain,(
% 27.01/3.88 sdtlseqdt0(smndt0(xS),smndt0(xS))|sdtlseqdt0(smndt0(xS),smndt0(xS))),
% 27.01/3.88 inference(resolution,[status(thm)],[f2613,f951])).
% 27.01/3.88 fof(f2663,definition,(
% 27.01/3.88 sQ138_spl <=> (sdtlseqdt0(smndt0(xS),smndt0(xS)))),
% 27.01/3.88 introduced(definition,[new_symbols(definition,[sQ138_spl])],[split_symbol_definition])).
% 27.01/3.88 fof(f2666,plain,(
% 27.01/3.88 sQ138_spl),
% 27.01/3.88 inference(split_clause,[status(thm)],[f2656,f2663])).
% 27.01/3.88 fof(f2688,plain,(
% 27.01/3.88 ![X0]: (~aScalar0(X0)|sdtasdt0(sdtpldt0(X0,xS),sdtpldt0(xS,xR))=sdtpldt0(sdtpldt0(sdtasdt0(X0,xS),sdtasdt0(X0,xR)),sdtasdt0(xS,sdtpldt0(xS,xR)))|~sQ3_spl)),
% 27.01/3.88 inference(forward_demodulation,[status(thm)],[f1615,f1280])).
% 27.01/3.88 fof(f2693,plain,(
% 27.01/3.88 sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xS,xR))=sdtpldt0(sdtpldt0(sdtasdt0(xR,xS),sdtasdt0(xR,xR)),sdtasdt0(xS,sdtpldt0(xS,xR)))|~sQ3_spl),
% 27.01/3.88 inference(resolution,[status(thm)],[f2688,f194])).
% 27.01/3.88 fof(f2700,plain,(
% 27.01/3.88 sdtasdt0(sdtpldt0(xS,xR),sdtpldt0(xS,xR))=sdtpldt0(sdtpldt0(sdtasdt0(xR,xS),sdtasdt0(xR,xR)),sdtasdt0(xS,sdtpldt0(xS,xR)))|~sQ2_spl|~sQ3_spl),
% 27.01/3.88 inference(forward_demodulation,[status(thm)],[f567,f2693])).
% 27.01/3.88 fof(f2701,plain,(
% 27.01/3.88 sdtasdt0(sdtpldt0(xS,xR),sdtpldt0(xS,xR))=sdtpldt0(sdtpldt0(xN,sdtasdt0(xR,xR)),sdtasdt0(xS,sdtpldt0(xS,xR)))|~sQ2_spl|~sQ3_spl),
% 27.01/3.88 inference(forward_demodulation,[status(thm)],[f201,f2700])).
% 27.01/3.88 fof(f2702,plain,(
% 27.01/3.88 sdtasdt0(sdtpldt0(xS,xR),sdtpldt0(xS,xR))=sdtpldt0(sdtasdt0(xR,sdtpldt0(xS,xR)),sdtasdt0(xS,sdtpldt0(xS,xR)))|~sQ2_spl|~sQ3_spl),
% 27.01/3.88 inference(forward_demodulation,[status(thm)],[f1612,f2701])).
% 27.01/3.88 fof(f2708,plain,(
% 27.01/3.88 sdtlseqdt0(sdtpldt0(sdtasdt0(xP,sdtpldt0(xP,xP)),sdtasdt0(xP,sdtpldt0(xP,xP))),sdtasdt0(sdtpldt0(xS,xR),sdtpldt0(xS,xR)))|~sQ2_spl|~sQ3_spl),
% 27.01/3.88 inference(backward_demodulation,[status(thm)],[f2702,f1459])).
% 27.01/3.88 fof(f3035,plain,(
% 27.01/3.88 ![X0]: (~aScalar0(X0)|sdtlseqdt0(sdtpldt0(xR,xR),X0)|sdtlseqdt0(X0,sdtpldt0(xR,xR)))),
% 27.01/3.88 inference(resolution,[status(thm)],[f601,f128])).
% 27.01/3.88 fof(f3222,plain,(
% 27.01/3.88 sdtlseqdt0(sdtpldt0(xR,xR),sdtpldt0(xR,xR))|sdtlseqdt0(sdtpldt0(xR,xR),sdtpldt0(xR,xR))),
% 27.01/3.88 inference(resolution,[status(thm)],[f3035,f601])).
% 27.01/3.88 fof(f3230,definition,(
% 27.01/3.88 sQ174_spl <=> (sdtlseqdt0(sdtpldt0(xR,xR),sdtpldt0(xR,xR)))),
% 27.01/3.88 introduced(definition,[new_symbols(definition,[sQ174_spl])],[split_symbol_definition])).
% 27.01/3.88 fof(f3233,plain,(
% 27.01/3.88 sQ174_spl),
% 27.01/3.88 inference(split_clause,[status(thm)],[f3222,f3230])).
% 27.01/3.88 fof(f3305,definition,(
% 27.01/3.88 sQ181_spl <=> (aScalar0(sdtpldt0(xR,xR)))),
% 27.01/3.88 introduced(definition,[new_symbols(definition,[sQ181_spl])],[split_symbol_definition])).
% 27.01/3.88 fof(f3307,plain,(
% 27.01/3.88 ~aScalar0(sdtpldt0(xR,xR))|sQ181_spl),
% 27.01/3.88 inference(component_clause,[status(thm)],[f3305])).
% 27.01/3.88 fof(f3324,plain,(
% 27.01/3.88 $false|sQ181_spl),
% 27.01/3.88 inference(forward_subsumption_resolution,[status(thm)],[f3307,f601])).
% 27.01/3.88 fof(f3325,plain,(
% 27.01/3.88 sQ181_spl),
% 27.01/3.88 inference(contradiction_clause,[status(thm)],[f3324])).
% 27.01/3.88 fof(f3352,plain,(
% 27.01/3.88 sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP))=sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,sdtpldt0(xP,xP)))),
% 27.01/3.88 inference(resolution,[status(thm)],[f1445,f196])).
% 27.01/3.88 fof(f3366,plain,(
% 27.01/3.88 sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP))=sdtpldt0(sdtasdt0(xP,sdtpldt0(xP,xP)),sdtasdt0(xP,sdtpldt0(xP,xP)))),
% 27.01/3.88 inference(forward_demodulation,[status(thm)],[f865,f3352])).
% 27.01/3.88 fof(f5517,plain,(
% 27.01/3.88 aScalar0(sdtasdt0(xP,sdtpldt0(xP,xP)))),
% 27.01/3.88 inference(resolution,[status(thm)],[f607,f231])).
% 27.01/3.88 fof(f5749,plain,(
% 27.01/3.88 $false|sQ88_spl),
% 27.01/3.88 inference(forward_subsumption_resolution,[status(thm)],[f5517,f1489])).
% 27.01/3.88 fof(f5750,plain,(
% 27.01/3.88 sQ88_spl),
% 27.01/3.88 inference(contradiction_clause,[status(thm)],[f5749])).
% 27.01/3.88 fof(f6060,definition,(
% 27.01/3.88 sQ397_spl <=> (aScalar0(sdtpldt0(xP,xP)))),
% 27.01/3.88 introduced(definition,[new_symbols(definition,[sQ397_spl])],[split_symbol_definition])).
% 27.01/3.88 fof(f6062,plain,(
% 27.01/3.88 ~aScalar0(sdtpldt0(xP,xP))|sQ397_spl),
% 27.01/3.88 inference(component_clause,[status(thm)],[f6060])).
% 27.01/3.88 fof(f6091,plain,(
% 27.01/3.88 $false|sQ397_spl),
% 27.01/3.88 inference(forward_subsumption_resolution,[status(thm)],[f6062,f607])).
% 27.01/3.88 fof(f6092,plain,(
% 27.01/3.88 sQ397_spl),
% 27.01/3.88 inference(contradiction_clause,[status(thm)],[f6091])).
% 27.01/3.88 fof(f7597,plain,(
% 27.01/3.88 sdtasdt0(xP,sdtpldt0(xP,xP))=sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP))),
% 27.01/3.88 inference(resolution,[status(thm)],[f414,f196])).
% 27.01/3.88 fof(f7797,definition,(
% 27.01/3.88 sQ541_spl <=> (aDimensionOf0(xt)=sz00)),
% 27.01/3.88 introduced(definition,[new_symbols(definition,[sQ541_spl])],[split_symbol_definition])).
% 27.01/3.88 fof(f7798,plain,(
% 27.01/3.88 aDimensionOf0(xt)=sz00|~sQ541_spl),
% 27.01/3.88 inference(component_clause,[status(thm)],[f7797])).
% 27.01/3.88 fof(f7830,definition,(
% 27.01/3.88 sQ547_spl <=> (aVector0(xs))),
% 27.01/3.88 introduced(definition,[new_symbols(definition,[sQ547_spl])],[split_symbol_definition])).
% 27.01/3.88 fof(f7832,plain,(
% 27.01/3.88 ~aVector0(xs)|sQ547_spl),
% 27.01/3.88 inference(component_clause,[status(thm)],[f7830])).
% 27.01/3.88 fof(f7833,definition,(
% 27.01/3.88 sQ548_spl <=> (aVector0(xt))),
% 27.01/3.88 introduced(definition,[new_symbols(definition,[sQ548_spl])],[split_symbol_definition])).
% 27.01/3.88 fof(f7835,plain,(
% 27.01/3.88 ~aVector0(xt)|sQ548_spl),
% 27.01/3.88 inference(component_clause,[status(thm)],[f7833])).
% 27.01/3.88 fof(f7863,plain,(
% 27.01/3.88 $false|sQ547_spl),
% 27.01/3.88 inference(forward_subsumption_resolution,[status(thm)],[f7832,f162])).
% 27.01/3.88 fof(f7864,plain,(
% 27.01/3.88 sQ547_spl),
% 27.01/3.88 inference(contradiction_clause,[status(thm)],[f7863])).
% 27.01/3.88 fof(f7865,plain,(
% 27.01/3.88 $false|sQ548_spl),
% 27.01/3.88 inference(forward_subsumption_resolution,[status(thm)],[f7835,f163])).
% 27.01/3.88 fof(f7866,plain,(
% 27.01/3.88 sQ548_spl),
% 27.01/3.88 inference(contradiction_clause,[status(thm)],[f7865])).
% 27.01/3.88 fof(f8814,plain,(
% 27.01/3.88 ~aDimensionOf0(xt)=sz00),
% 27.01/3.88 inference(forward_demodulation,[status(thm)],[f166,f167])).
% 27.01/3.88 fof(f8861,definition,(
% 27.01/3.88 sQ710_spl <=> (aVector0(xp))),
% 27.01/3.88 introduced(definition,[new_symbols(definition,[sQ710_spl])],[split_symbol_definition])).
% 27.01/3.88 fof(f8863,plain,(
% 27.01/3.88 ~aVector0(xp)|sQ710_spl),
% 27.01/3.88 inference(component_clause,[status(thm)],[f8861])).
% 27.01/3.88 fof(f8888,plain,(
% 27.01/3.88 $false|sQ710_spl),
% 27.01/3.88 inference(forward_subsumption_resolution,[status(thm)],[f8863,f169])).
% 27.01/3.88 fof(f8889,plain,(
% 27.01/3.88 sQ710_spl),
% 27.01/3.88 inference(contradiction_clause,[status(thm)],[f8888])).
% 27.01/3.88 fof(f9167,definition,(
% 27.01/3.88 sQ741_spl <=> (sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP))=sdtasdt0(xP,sdtpldt0(xP,xP)))),
% 27.01/3.88 introduced(definition,[new_symbols(definition,[sQ741_spl])],[split_symbol_definition])).
% 27.01/3.88 fof(f9169,plain,(
% 27.01/3.88 ~sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP))=sdtasdt0(xP,sdtpldt0(xP,xP))|sQ741_spl),
% 27.01/3.88 inference(component_clause,[status(thm)],[f9167])).
% 27.01/3.88 fof(f9883,definition,(
% 27.01/3.88 sQ765_spl <=> (aVector0(xq))),
% 27.01/3.88 introduced(definition,[new_symbols(definition,[sQ765_spl])],[split_symbol_definition])).
% 27.01/3.88 fof(f9885,plain,(
% 27.01/3.88 ~aVector0(xq)|sQ765_spl),
% 27.01/3.88 inference(component_clause,[status(thm)],[f9883])).
% 27.01/3.88 fof(f9910,plain,(
% 27.01/3.88 $false|sQ765_spl),
% 27.01/3.88 inference(forward_subsumption_resolution,[status(thm)],[f9885,f174])).
% 27.01/3.88 fof(f9911,plain,(
% 27.01/3.88 sQ765_spl),
% 27.01/3.88 inference(contradiction_clause,[status(thm)],[f9910])).
% 27.01/3.88 fof(f10178,plain,(
% 27.01/3.88 ![X0]: (~aScalar0(X0)|sdtlseqdt0(xA,X0)|sdtlseqdt0(X0,xA))),
% 27.01/3.88 inference(resolution,[status(thm)],[f178,f128])).
% 27.01/3.88 fof(f10478,plain,(
% 27.01/3.88 ![X0]: (~aScalar0(X0)|sdtlseqdt0(xB,X0)|sdtlseqdt0(X0,xB))),
% 27.01/3.88 inference(resolution,[status(thm)],[f180,f128])).
% 27.01/3.88 fof(f10585,plain,(
% 27.01/3.88 sdtlseqdt0(xA,xA)|sdtlseqdt0(xA,xA)),
% 27.01/3.88 inference(resolution,[status(thm)],[f10178,f178])).
% 27.01/3.88 fof(f10601,definition,(
% 27.01/3.88 sQ819_spl <=> (sdtlseqdt0(xA,xA))),
% 27.01/3.88 introduced(definition,[new_symbols(definition,[sQ819_spl])],[split_symbol_definition])).
% 27.01/3.88 fof(f10604,plain,(
% 27.01/3.88 sQ819_spl),
% 27.01/3.88 inference(split_clause,[status(thm)],[f10585,f10601])).
% 27.01/3.88 fof(f10613,plain,(
% 27.01/3.88 sdtlseqdt0(xB,xB)|sdtlseqdt0(xB,xB)),
% 27.01/3.88 inference(resolution,[status(thm)],[f10478,f180])).
% 27.01/3.88 fof(f10623,definition,(
% 27.01/3.88 sQ820_spl <=> (sdtlseqdt0(xB,xB))),
% 27.01/3.88 introduced(definition,[new_symbols(definition,[sQ820_spl])],[split_symbol_definition])).
% 27.01/3.88 fof(f10626,plain,(
% 27.01/3.88 sQ820_spl),
% 27.01/3.88 inference(split_clause,[status(thm)],[f10613,f10623])).
% 27.01/3.88 fof(f11467,plain,(
% 27.01/3.88 ![X0]: (~aScalar0(X0)|sdtlseqdt0(xC,X0)|sdtlseqdt0(X0,xC))),
% 27.01/3.88 inference(resolution,[status(thm)],[f182,f128])).
% 27.01/3.88 fof(f11559,plain,(
% 27.01/3.88 sdtlseqdt0(xC,xC)|sdtlseqdt0(xC,xC)),
% 27.01/3.88 inference(resolution,[status(thm)],[f11467,f182])).
% 27.01/3.88 fof(f11570,definition,(
% 27.01/3.88 sQ906_spl <=> (sdtlseqdt0(xC,xC))),
% 27.01/3.88 introduced(definition,[new_symbols(definition,[sQ906_spl])],[split_symbol_definition])).
% 27.01/3.88 fof(f11573,plain,(
% 27.01/3.88 sQ906_spl),
% 27.01/3.88 inference(split_clause,[status(thm)],[f11559,f11570])).
% 27.01/3.88 fof(f12133,plain,(
% 27.01/3.88 ![X0]: (~aScalar0(X0)|sdtlseqdt0(xD,X0)|sdtlseqdt0(X0,xD))),
% 27.01/3.88 inference(resolution,[status(thm)],[f184,f128])).
% 27.01/3.88 fof(f12461,plain,(
% 27.01/3.88 ![X0]: (~aScalar0(X0)|sdtlseqdt0(xE,X0)|sdtlseqdt0(X0,xE))),
% 27.01/3.88 inference(resolution,[status(thm)],[f186,f128])).
% 27.01/3.88 fof(f12561,plain,(
% 27.01/3.88 sdtlseqdt0(xD,xD)|sdtlseqdt0(xD,xD)),
% 27.01/3.88 inference(resolution,[status(thm)],[f12133,f184])).
% 27.01/3.88 fof(f12580,definition,(
% 27.01/3.88 sQ969_spl <=> (sdtlseqdt0(xD,xD))),
% 27.01/3.88 introduced(definition,[new_symbols(definition,[sQ969_spl])],[split_symbol_definition])).
% 27.01/3.88 fof(f12583,plain,(
% 27.01/3.88 sQ969_spl),
% 27.01/3.88 inference(split_clause,[status(thm)],[f12561,f12580])).
% 27.01/3.88 fof(f12595,plain,(
% 27.01/3.88 sdtlseqdt0(xE,xE)|sdtlseqdt0(xE,xE)),
% 27.01/3.88 inference(resolution,[status(thm)],[f12461,f186])).
% 27.01/3.88 fof(f12608,definition,(
% 27.01/3.88 sQ970_spl <=> (sdtlseqdt0(xE,xE))),
% 27.01/3.88 introduced(definition,[new_symbols(definition,[sQ970_spl])],[split_symbol_definition])).
% 27.01/3.88 fof(f12611,plain,(
% 27.01/3.88 sQ970_spl),
% 27.01/3.88 inference(split_clause,[status(thm)],[f12595,f12608])).
% 27.01/3.88 fof(f12871,plain,(
% 27.01/3.88 ~sdtasdt0(xP,sdtpldt0(xP,xP))=sdtasdt0(xP,sdtpldt0(xP,xP))|sQ741_spl),
% 27.01/3.88 inference(forward_demodulation,[status(thm)],[f7597,f9169])).
% 27.01/3.88 fof(f12872,plain,(
% 27.01/3.88 $false|sQ741_spl),
% 27.01/3.88 inference(trivial_equality_resolution,[status(thm)],[f12871])).
% 27.01/3.88 fof(f12873,plain,(
% 27.01/3.88 sQ741_spl),
% 27.01/3.88 inference(contradiction_clause,[status(thm)],[f12872])).
% 27.01/3.88 fof(f13487,plain,(
% 27.01/3.88 ![X0]: (~aScalar0(X0)|sdtlseqdt0(xF,X0)|sdtlseqdt0(X0,xF))),
% 27.01/3.88 inference(resolution,[status(thm)],[f188,f128])).
% 27.01/3.88 fof(f13885,plain,(
% 27.01/3.88 ![X0]: (~aScalar0(X0)|sdtlseqdt0(xG,X0)|sdtlseqdt0(X0,xG))),
% 27.01/3.88 inference(resolution,[status(thm)],[f190,f128])).
% 27.01/3.88 fof(f13999,plain,(
% 27.01/3.88 sdtlseqdt0(xF,xF)|sdtlseqdt0(xF,xF)),
% 27.01/3.88 inference(resolution,[status(thm)],[f13487,f188])).
% 27.01/3.88 fof(f14020,definition,(
% 27.01/3.88 sQ1043_spl <=> (sdtlseqdt0(xF,xF))),
% 27.01/3.88 introduced(definition,[new_symbols(definition,[sQ1043_spl])],[split_symbol_definition])).
% 27.01/3.88 fof(f14023,plain,(
% 27.01/3.88 sQ1043_spl),
% 27.01/3.88 inference(split_clause,[status(thm)],[f13999,f14020])).
% 27.01/3.88 fof(f14037,plain,(
% 27.01/3.88 sdtlseqdt0(xG,xG)|sdtlseqdt0(xG,xG)),
% 27.01/3.88 inference(resolution,[status(thm)],[f13885,f190])).
% 27.01/3.88 fof(f14052,definition,(
% 27.01/3.88 sQ1044_spl <=> (sdtlseqdt0(xG,xG))),
% 27.01/3.88 introduced(definition,[new_symbols(definition,[sQ1044_spl])],[split_symbol_definition])).
% 27.01/3.88 fof(f14055,plain,(
% 27.01/3.88 sQ1044_spl),
% 27.01/3.88 inference(split_clause,[status(thm)],[f14037,f14052])).
% 27.01/3.88 fof(f14878,plain,(
% 27.01/3.88 ![X0]: (~aScalar0(X0)|sdtlseqdt0(xH,X0)|sdtlseqdt0(X0,xH))),
% 27.01/3.88 inference(resolution,[status(thm)],[f192,f128])).
% 27.01/3.88 fof(f15302,plain,(
% 27.01/3.88 ![X0]: (~aScalar0(X0)|sdtlseqdt0(xN,X0)|sdtlseqdt0(X0,xN))),
% 27.01/3.88 inference(resolution,[status(thm)],[f200,f128])).
% 27.01/3.88 fof(f15497,plain,(
% 27.01/3.88 sdtlseqdt0(xH,xH)|sdtlseqdt0(xH,xH)),
% 27.01/3.88 inference(resolution,[status(thm)],[f14878,f192])).
% 27.01/3.88 fof(f15520,definition,(
% 27.01/3.88 sQ1134_spl <=> (sdtlseqdt0(xH,xH))),
% 27.01/3.88 introduced(definition,[new_symbols(definition,[sQ1134_spl])],[split_symbol_definition])).
% 27.01/3.88 fof(f15523,plain,(
% 27.01/3.88 sQ1134_spl),
% 27.01/3.88 inference(split_clause,[status(thm)],[f15497,f15520])).
% 27.01/3.88 fof(f15539,plain,(
% 27.01/3.88 sdtlseqdt0(xN,xN)|sdtlseqdt0(xN,xN)),
% 27.01/3.88 inference(resolution,[status(thm)],[f15302,f200])).
% 27.01/3.88 fof(f15556,definition,(
% 27.01/3.88 sQ1135_spl <=> (sdtlseqdt0(xN,xN))),
% 27.01/3.88 introduced(definition,[new_symbols(definition,[sQ1135_spl])],[split_symbol_definition])).
% 27.01/3.88 fof(f15559,plain,(
% 27.01/3.88 sQ1135_spl),
% 27.01/3.88 inference(split_clause,[status(thm)],[f15539,f15556])).
% 27.01/3.88 fof(f15993,definition,(
% 27.01/3.88 sQ1136_spl <=> (aScalar0(xC))),
% 27.01/3.88 introduced(definition,[new_symbols(definition,[sQ1136_spl])],[split_symbol_definition])).
% 27.01/3.88 fof(f15995,plain,(
% 27.01/3.88 ~aScalar0(xC)|sQ1136_spl),
% 27.01/3.88 inference(component_clause,[status(thm)],[f15993])).
% 27.01/3.88 fof(f16020,plain,(
% 27.01/3.88 $false|sQ1136_spl),
% 27.01/3.88 inference(forward_subsumption_resolution,[status(thm)],[f15995,f182])).
% 27.01/3.88 fof(f16021,plain,(
% 27.01/3.88 sQ1136_spl),
% 27.01/3.88 inference(contradiction_clause,[status(thm)],[f16020])).
% 27.01/3.88 fof(f16083,definition,(
% 27.01/3.88 sQ1143_spl <=> (aScalar0(xN))),
% 27.01/3.88 introduced(definition,[new_symbols(definition,[sQ1143_spl])],[split_symbol_definition])).
% 27.01/3.88 fof(f16085,plain,(
% 27.01/3.88 ~aScalar0(xN)|sQ1143_spl),
% 27.01/3.88 inference(component_clause,[status(thm)],[f16083])).
% 27.01/3.88 fof(f16113,plain,(
% 27.01/3.88 $false|sQ1143_spl),
% 27.01/3.88 inference(forward_subsumption_resolution,[status(thm)],[f16085,f200])).
% 27.01/3.88 fof(f16114,plain,(
% 27.01/3.88 sQ1143_spl),
% 27.01/3.88 inference(contradiction_clause,[status(thm)],[f16113])).
% 27.01/3.88 fof(f16936,definition,(
% 27.01/3.88 sQ1161_spl <=> (aScalar0(xD))),
% 27.01/3.88 introduced(definition,[new_symbols(definition,[sQ1161_spl])],[split_symbol_definition])).
% 27.01/3.88 fof(f16938,plain,(
% 27.01/3.88 ~aScalar0(xD)|sQ1161_spl),
% 27.01/3.88 inference(component_clause,[status(thm)],[f16936])).
% 27.01/3.88 fof(f16963,plain,(
% 27.01/3.88 $false|sQ1161_spl),
% 27.01/3.88 inference(forward_subsumption_resolution,[status(thm)],[f16938,f184])).
% 27.01/3.88 fof(f16964,plain,(
% 27.01/3.88 sQ1161_spl),
% 27.01/3.88 inference(contradiction_clause,[status(thm)],[f16963])).
% 27.01/3.88 fof(f17940,plain,(
% 27.01/3.88 $false|~sQ541_spl),
% 27.01/3.88 inference(forward_subsumption_resolution,[status(thm)],[f7798,f8814])).
% 27.01/3.88 fof(f17941,plain,(
% 27.01/3.88 ~sQ541_spl),
% 27.01/3.88 inference(contradiction_clause,[status(thm)],[f17940])).
% 27.01/3.88 fof(f17999,definition,(
% 27.01/3.88 sQ1189_spl <=> (aScalar0(xE))),
% 27.01/3.88 introduced(definition,[new_symbols(definition,[sQ1189_spl])],[split_symbol_definition])).
% 27.01/3.88 fof(f18001,plain,(
% 27.01/3.88 ~aScalar0(xE)|sQ1189_spl),
% 27.01/3.88 inference(component_clause,[status(thm)],[f17999])).
% 27.01/3.88 fof(f18026,plain,(
% 27.01/3.88 $false|sQ1189_spl),
% 27.01/3.88 inference(forward_subsumption_resolution,[status(thm)],[f18001,f186])).
% 27.01/3.88 fof(f18027,plain,(
% 27.01/3.88 sQ1189_spl),
% 27.01/3.88 inference(contradiction_clause,[status(thm)],[f18026])).
% 27.01/3.88 fof(f18100,plain,(
% 27.01/3.88 sdtlseqdt0(sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)),sdtasdt0(sdtpldt0(xS,xR),sdtpldt0(xS,xR)))|~sQ2_spl|~sQ3_spl),
% 27.01/3.88 inference(backward_demodulation,[status(thm)],[f3366,f2708])).
% 27.01/3.88 fof(f18103,plain,(
% 27.01/3.88 $false|~sQ2_spl|~sQ3_spl),
% 27.01/3.88 inference(forward_subsumption_resolution,[status(thm)],[f18100,f570])).
% 27.01/3.88 fof(f18104,plain,(
% 27.01/3.88 ~sQ2_spl|~sQ3_spl),
% 27.01/3.88 inference(contradiction_clause,[status(thm)],[f18103])).
% 27.01/3.88 fof(f18105,plain,(
% 27.01/3.88 $false),
% 27.01/3.88 inference(sat_refutation,[status(thm)],[f219,f223,f246,f257,f279,f295,f361,f363,f365,f761,f1906,f2132,f2414,f2666,f3233,f3325,f5750,f6092,f7864,f7866,f8889,f9911,f10604,f10626,f11573,f12583,f12611,f12873,f14023,f14055,f15523,f15559,f16021,f16114,f16964,f17941,f18027,f18104])).
% 20.04/3.91 % SZS output end CNFRefutation for theBenchmark.p
% 20.04/3.93 % Elapsed time: 3.559312 seconds
% 20.04/3.93 % CPU time: 27.917040 seconds
% 20.04/3.93 % Total memory used: 389.069 MB
% 20.04/3.93 % Net memory used: 363.642 MB
%------------------------------------------------------------------------------