%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : RNG069+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n003.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 45.12s 11.23s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG069+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/5.37 % Computer : n003.cluster.edu
% 0.10/5.37 % Model : x86_64 x86_64
% 0.10/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.37 % Memory : 8046.5625MB
% 0.10/5.37 % OS : Linux 6.8.0-71-generic
% 0.10/5.37 % CPULimit : 300
% 0.10/5.37 % WCLimit : 300
% 0.10/5.37 % DateTime : Mon Sep 21 04:19:07 UTC 2026
% 0.10/5.38 % CPUTime :
% 0.10/5.40 % Drodi V4.1.1
% 45.12/11.23 % Refutation found
% 45.12/11.23 % SZS status Theorem for theBenchmark: Theorem is valid
% 45.12/11.23 % SZS output start CNFRefutation for theBenchmark
% 45.12/11.23 fof(f9,axiom,(
% 45.12/11.23 aScalar0(sz0z00) ),
% 45.12/11.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 45.12/11.23 fof(f10,axiom,(
% 45.12/11.23 (! [W0,W1] :( ( aScalar0(W0)& aScalar0(W1) )=> aScalar0(sdtpldt0(W0,W1)) ) )),
% 45.12/11.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 45.12/11.23 fof(f11,axiom,(
% 45.12/11.23 (! [W0,W1] :( ( aScalar0(W0)& aScalar0(W1) )=> aScalar0(sdtasdt0(W0,W1)) ) )),
% 45.12/11.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 45.12/11.23 fof(f12,axiom,(
% 45.12/11.23 (! [W0] :( aScalar0(W0)=> aScalar0(smndt0(W0)) ) )),
% 45.12/11.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 45.12/11.23 fof(f13,axiom,(
% 45.12/11.23 (! [W0] :( aScalar0(W0)=> ( sdtpldt0(W0,sz0z00) = W0& sdtpldt0(sz0z00,W0) = W0& sdtasdt0(W0,sz0z00) = sz0z00& sdtasdt0(sz0z00,W0) = sz0z00& sdtpldt0(W0,smndt0(W0)) = sz0z00& sdtpldt0(smndt0(W0),W0) = sz0z00& smndt0(smndt0(W0)) = W0& smndt0(sz0z00) = sz0z00 ) ) )),
% 45.12/11.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 45.12/11.23 fof(f14,axiom,(
% 45.12/11.23 (! [W0,W1,W2] :( ( aScalar0(W0)& aScalar0(W1)& aScalar0(W2) )=> ( sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2))& sdtpldt0(W0,W1) = sdtpldt0(W1,W0)& sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2))& sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) ) )),
% 45.12/11.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 45.12/11.23 fof(f15,axiom,(
% 45.12/11.23 (! [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)) ) ) )),
% 45.12/11.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 45.12/11.23 fof(f16,axiom,(
% 45.12/11.23 (! [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))) ) )),
% 45.12/11.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 45.12/11.23 fof(f20,axiom,(
% 45.12/11.23 (! [W0] :( aScalar0(W0)=> sdtlseqdt0(W0,W0) ) )),
% 45.12/11.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 45.12/11.23 fof(f25,axiom,(
% 45.12/11.23 (! [W0,W1] :( ( aScalar0(W0)& aScalar0(W1) )=> ( sdtlseqdt0(W0,W1)| sdtlseqdt0(W1,W0) ) ) )),
% 45.12/11.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 45.12/11.23 fof(f38,hypothesis,(
% 45.12/11.23 ( aVector0(xs)& aVector0(xt) ) ),
% 45.12/11.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 45.12/11.23 fof(f52,hypothesis,(
% 45.12/11.23 ( aScalar0(xR)& xR = sdtasdt0(xC,xG) ) ),
% 45.12/11.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 45.12/11.23 fof(f53,hypothesis,(
% 45.12/11.23 ( aScalar0(xP)& xP = sdtasdt0(xE,xH) ) ),
% 45.12/11.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 45.12/11.23 fof(f54,hypothesis,(
% 45.12/11.23 ( aScalar0(xS)& xS = sdtasdt0(xF,xD) ) ),
% 45.12/11.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 45.12/11.23 fof(f55,hypothesis,(
% 45.12/11.23 ( aScalar0(xN)& xN = sdtasdt0(xR,xS) ) ),
% 45.12/11.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 45.12/11.23 fof(f61,hypothesis,(
% 45.12/11.23 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)))) ),
% 45.12/11.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 45.12/11.23 fof(f62,conjecture,(
% 45.12/11.23 sdtlseqdt0(sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)),sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS))) ),
% 45.12/11.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 45.12/11.23 fof(f63,negated_conjecture,(
% 45.12/11.23 ~(sdtlseqdt0(sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)),sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS))) )),
% 45.12/11.23 inference(negated_conjecture,[status(cth)],[f62])).
% 45.12/11.23 fof(f84,plain,(
% 45.12/11.23 aScalar0(sz0z00)),
% 45.12/11.23 inference(cnf_transformation,[status(thm)],[f9])).
% 45.12/11.23 fof(f85,plain,(
% 45.12/11.23 ![W0,W1]: ((~aScalar0(W0)|~aScalar0(W1))|aScalar0(sdtpldt0(W0,W1)))),
% 45.12/11.23 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 45.12/11.23 fof(f86,plain,(
% 45.12/11.23 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|aScalar0(sdtpldt0(X0,X1)))),
% 45.12/11.23 inference(cnf_transformation,[status(thm)],[f85])).
% 45.12/11.23 fof(f87,plain,(
% 45.12/11.23 ![W0,W1]: ((~aScalar0(W0)|~aScalar0(W1))|aScalar0(sdtasdt0(W0,W1)))),
% 45.12/11.23 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 45.12/11.23 fof(f88,plain,(
% 45.12/11.23 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|aScalar0(sdtasdt0(X0,X1)))),
% 45.12/11.23 inference(cnf_transformation,[status(thm)],[f87])).
% 45.12/11.23 fof(f89,plain,(
% 45.12/11.23 ![W0]: (~aScalar0(W0)|aScalar0(smndt0(W0)))),
% 45.12/11.23 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 45.12/11.23 fof(f90,plain,(
% 45.12/11.23 ![X0]: (~aScalar0(X0)|aScalar0(smndt0(X0)))),
% 45.12/11.23 inference(cnf_transformation,[status(thm)],[f89])).
% 45.12/11.23 fof(f91,plain,(
% 45.12/11.23 ![W0]: (~aScalar0(W0)|(((((((sdtpldt0(W0,sz0z00)=W0&sdtpldt0(sz0z00,W0)=W0)&sdtasdt0(W0,sz0z00)=sz0z00)&sdtasdt0(sz0z00,W0)=sz0z00)&sdtpldt0(W0,smndt0(W0))=sz0z00)&sdtpldt0(smndt0(W0),W0)=sz0z00)&smndt0(smndt0(W0))=W0)&smndt0(sz0z00)=sz0z00))),
% 45.12/11.23 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 45.12/11.23 fof(f95,plain,(
% 45.12/11.23 ![X0]: (~aScalar0(X0)|sdtasdt0(sz0z00,X0)=sz0z00)),
% 45.12/11.23 inference(cnf_transformation,[status(thm)],[f91])).
% 45.12/11.23 fof(f100,plain,(
% 45.12/11.23 ![W0,W1,W2]: (((~aScalar0(W0)|~aScalar0(W1))|~aScalar0(W2))|(((sdtpldt0(sdtpldt0(W0,W1),W2)=sdtpldt0(W0,sdtpldt0(W1,W2))&sdtpldt0(W0,W1)=sdtpldt0(W1,W0))&sdtasdt0(sdtasdt0(W0,W1),W2)=sdtasdt0(W0,sdtasdt0(W1,W2)))&sdtasdt0(W0,W1)=sdtasdt0(W1,W0)))),
% 45.12/11.23 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 45.12/11.23 fof(f102,plain,(
% 45.12/11.23 ![X0,X1,X2]: (~aScalar0(X0)|~aScalar0(X1)|~aScalar0(X2)|sdtpldt0(X0,X1)=sdtpldt0(X1,X0))),
% 45.12/11.23 inference(cnf_transformation,[status(thm)],[f100])).
% 45.12/11.23 fof(f104,plain,(
% 45.12/11.23 ![X0,X1,X2]: (~aScalar0(X0)|~aScalar0(X1)|~aScalar0(X2)|sdtasdt0(X0,X1)=sdtasdt0(X1,X0))),
% 45.12/11.23 inference(cnf_transformation,[status(thm)],[f100])).
% 45.12/11.23 fof(f105,plain,(
% 45.12/11.23 ![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))))),
% 45.12/11.23 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 45.12/11.23 fof(f106,plain,(
% 45.12/11.23 ![X0,X1,X2]: (~aScalar0(X0)|~aScalar0(X1)|~aScalar0(X2)|sdtasdt0(X0,sdtpldt0(X1,X2))=sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2)))),
% 45.12/11.23 inference(cnf_transformation,[status(thm)],[f105])).
% 45.12/11.23 fof(f107,plain,(
% 45.12/11.23 ![X0,X1,X2]: (~aScalar0(X0)|~aScalar0(X1)|~aScalar0(X2)|sdtasdt0(sdtpldt0(X0,X1),X2)=sdtpldt0(sdtasdt0(X0,X2),sdtasdt0(X1,X2)))),
% 45.12/11.23 inference(cnf_transformation,[status(thm)],[f105])).
% 45.12/11.23 fof(f108,plain,(
% 45.12/11.23 ![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))))),
% 45.12/11.23 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 45.12/11.23 fof(f109,plain,(
% 45.12/11.23 ![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))))),
% 45.12/11.23 inference(cnf_transformation,[status(thm)],[f108])).
% 45.12/11.23 fof(f117,plain,(
% 45.12/11.23 ![W0]: (~aScalar0(W0)|sdtlseqdt0(W0,W0))),
% 45.12/11.23 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 45.12/11.23 fof(f118,plain,(
% 45.12/11.23 ![X0]: (~aScalar0(X0)|sdtlseqdt0(X0,X0))),
% 45.12/11.23 inference(cnf_transformation,[status(thm)],[f117])).
% 45.12/11.23 fof(f127,plain,(
% 45.12/11.23 ![W0,W1]: ((~aScalar0(W0)|~aScalar0(W1))|(sdtlseqdt0(W0,W1)|sdtlseqdt0(W1,W0)))),
% 45.12/11.23 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 45.12/11.23 fof(f128,plain,(
% 45.12/11.23 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|sdtlseqdt0(X0,X1)|sdtlseqdt0(X1,X0))),
% 45.12/11.23 inference(cnf_transformation,[status(thm)],[f127])).
% 45.12/11.23 fof(f162,plain,(
% 45.12/11.23 aVector0(xs)),
% 45.12/11.23 inference(cnf_transformation,[status(thm)],[f38])).
% 45.12/11.23 fof(f163,plain,(
% 45.12/11.23 aVector0(xt)),
% 45.12/11.23 inference(cnf_transformation,[status(thm)],[f38])).
% 45.12/11.23 fof(f188,plain,(
% 45.12/11.23 aScalar0(xR)),
% 45.12/11.23 inference(cnf_transformation,[status(thm)],[f52])).
% 45.12/11.23 fof(f190,plain,(
% 45.12/11.23 aScalar0(xP)),
% 45.12/11.23 inference(cnf_transformation,[status(thm)],[f53])).
% 45.12/11.23 fof(f192,plain,(
% 45.12/11.23 aScalar0(xS)),
% 45.12/11.23 inference(cnf_transformation,[status(thm)],[f54])).
% 45.12/11.23 fof(f195,plain,(
% 45.12/11.23 xN=sdtasdt0(xR,xS)),
% 45.12/11.23 inference(cnf_transformation,[status(thm)],[f55])).
% 45.12/11.23 fof(f201,plain,(
% 45.12/11.23 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))))),
% 45.12/11.23 inference(cnf_transformation,[status(thm)],[f61])).
% 45.12/11.23 fof(f202,plain,(
% 45.12/11.23 ~sdtlseqdt0(sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)),sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS)))),
% 45.12/11.23 inference(cnf_transformation,[status(thm)],[f63])).
% 45.12/11.23 fof(f203,definition,(
% 45.12/11.23 ![X0]: (sQ0_spl <=> (~aScalar0(X0)))),
% 45.12/11.23 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 45.12/11.23 fof(f204,plain,(
% 45.12/11.23 ![X0]: (~aScalar0(X0)|~sQ0_spl)),
% 45.12/11.23 inference(component_clause,[status(thm)],[f203])).
% 45.12/11.23 fof(f210,definition,(
% 45.12/11.23 ![X0,X1]: (sQ2_spl <=> (~aScalar0(X0)|~aScalar0(X1)|sdtpldt0(X0,X1)=sdtpldt0(X1,X0)))),
% 45.12/11.23 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 45.12/11.23 fof(f211,plain,(
% 45.12/11.23 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|sdtpldt0(X0,X1)=sdtpldt0(X1,X0)|~sQ2_spl)),
% 45.12/11.23 inference(component_clause,[status(thm)],[f210])).
% 45.12/11.23 fof(f213,plain,(
% 45.12/11.23 sQ2_spl|sQ0_spl),
% 45.12/11.23 inference(split_clause,[status(thm)],[f102,f210,f203])).
% 45.12/11.23 fof(f214,definition,(
% 45.12/11.23 ![X0,X1]: (sQ3_spl <=> (~aScalar0(X0)|~aScalar0(X1)|sdtasdt0(X0,X1)=sdtasdt0(X1,X0)))),
% 45.12/11.23 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 45.12/11.23 fof(f215,plain,(
% 45.12/11.23 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|sdtasdt0(X0,X1)=sdtasdt0(X1,X0)|~sQ3_spl)),
% 45.12/11.23 inference(component_clause,[status(thm)],[f214])).
% 45.12/11.23 fof(f217,plain,(
% 45.12/11.23 sQ3_spl|sQ0_spl),
% 45.12/11.23 inference(split_clause,[status(thm)],[f104,f214,f203])).
% 45.12/11.23 fof(f218,plain,(
% 45.12/11.23 sdtlseqdt0(xR,xR)),
% 45.12/11.23 inference(resolution,[status(thm)],[f188,f118])).
% 45.12/11.23 fof(f222,plain,(
% 45.12/11.23 ![X0,X1,X2]: (~aScalar0(X0)|~aScalar0(X1)|~aScalar0(X2)|sdtasdt0(sdtpldt0(X0,X1),sdtpldt0(xR,X2))=sdtpldt0(sdtpldt0(sdtasdt0(X0,xR),sdtasdt0(X0,X2)),sdtpldt0(sdtasdt0(X1,xR),sdtasdt0(X1,X2))))),
% 45.12/11.23 inference(resolution,[status(thm)],[f188,f109])).
% 45.12/11.23 fof(f225,plain,(
% 45.12/11.23 ![X0]: (~aScalar0(X0)|aScalar0(sdtpldt0(X0,xR)))),
% 45.12/11.23 inference(resolution,[status(thm)],[f188,f86])).
% 45.12/11.23 fof(f229,plain,(
% 45.12/11.23 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|sdtasdt0(sdtpldt0(X0,xR),X1)=sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(xR,X1)))),
% 45.12/11.23 inference(resolution,[status(thm)],[f188,f107])).
% 45.12/11.23 fof(f231,plain,(
% 45.12/11.23 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|sdtasdt0(X0,sdtpldt0(X1,xR))=sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,xR)))),
% 45.12/11.23 inference(resolution,[status(thm)],[f188,f106])).
% 45.12/11.23 fof(f233,plain,(
% 45.12/11.23 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|sdtasdt0(X0,sdtpldt0(xR,X1))=sdtpldt0(sdtasdt0(X0,xR),sdtasdt0(X0,X1)))),
% 45.12/11.23 inference(resolution,[status(thm)],[f188,f106])).
% 45.12/11.23 fof(f242,plain,(
% 45.12/11.23 sdtlseqdt0(xP,xP)),
% 45.12/11.23 inference(resolution,[status(thm)],[f190,f118])).
% 45.12/11.23 fof(f243,plain,(
% 45.12/11.23 ![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))))),
% 45.12/11.23 inference(resolution,[status(thm)],[f190,f109])).
% 45.12/11.23 fof(f249,plain,(
% 45.12/11.23 ![X0]: (~aScalar0(X0)|aScalar0(sdtpldt0(X0,xP)))),
% 45.12/11.23 inference(resolution,[status(thm)],[f190,f86])).
% 45.12/11.23 fof(f254,plain,(
% 45.12/11.23 ![X0]: (~aScalar0(X0)|sdtasdt0(X0,sdtpldt0(xP,xP))=sdtpldt0(sdtasdt0(X0,xP),sdtasdt0(X0,xP)))),
% 45.12/11.23 inference(resolution,[status(thm)],[f190,f106])).
% 45.12/11.23 fof(f266,plain,(
% 45.12/11.23 sdtlseqdt0(xS,xS)),
% 45.12/11.23 inference(resolution,[status(thm)],[f192,f118])).
% 45.12/11.23 fof(f273,plain,(
% 45.12/11.23 ![X0]: (~aScalar0(X0)|aScalar0(sdtpldt0(X0,xS)))),
% 45.12/11.23 inference(resolution,[status(thm)],[f192,f86])).
% 45.12/11.23 fof(f274,plain,(
% 45.12/11.23 ![X0]: (~aScalar0(X0)|sdtasdt0(sdtpldt0(X0,xS),xS)=sdtpldt0(sdtasdt0(X0,xS),sdtasdt0(xS,xS)))),
% 45.12/11.23 inference(resolution,[status(thm)],[f192,f107])).
% 45.12/11.23 fof(f302,plain,(
% 45.12/11.23 ![X0]: (~aScalar0(X0)|aScalar0(sdtasdt0(X0,xS)))),
% 45.12/11.23 inference(resolution,[status(thm)],[f88,f192])).
% 45.12/11.23 fof(f303,plain,(
% 45.12/11.23 ![X0]: (~aScalar0(X0)|aScalar0(sdtasdt0(X0,xP)))),
% 45.12/11.23 inference(resolution,[status(thm)],[f88,f190])).
% 45.12/11.23 fof(f304,plain,(
% 45.12/11.23 ![X0]: (~aScalar0(X0)|aScalar0(sdtasdt0(X0,xR)))),
% 45.12/11.23 inference(resolution,[status(thm)],[f88,f188])).
% 45.12/11.23 fof(f317,plain,(
% 45.12/11.23 sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP))),sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),xN),sdtpldt0(sdtasdt0(xS,xR),sdtasdt0(xS,xS))))),
% 45.12/11.23 inference(backward_demodulation,[status(thm)],[f195,f201])).
% 45.12/11.23 fof(f318,plain,(
% 45.12/11.23 $false|~sQ0_spl),
% 45.12/11.23 inference(backward_subsumption_resolution,[status(thm)],[f192,f204])).
% 45.12/11.23 fof(f321,plain,(
% 45.12/11.23 ~sQ0_spl),
% 45.12/11.23 inference(contradiction_clause,[status(thm)],[f318])).
% 45.12/11.23 fof(f419,plain,(
% 45.12/11.23 ![X0]: (~aScalar0(X0)|sdtlseqdt0(X0,sz0z00)|sdtlseqdt0(sz0z00,X0))),
% 45.12/11.23 inference(resolution,[status(thm)],[f84,f128])).
% 45.12/11.23 fof(f457,definition,(
% 45.12/11.23 sQ16_spl <=> (sdtlseqdt0(sz0z00,sz0z00))),
% 45.12/11.23 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 45.12/11.23 fof(f476,definition,(
% 45.12/11.23 sQ18_spl <=> (aScalar0(sz0z00))),
% 45.12/11.23 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 45.12/11.23 fof(f478,plain,(
% 45.12/11.23 ~aScalar0(sz0z00)|sQ18_spl),
% 45.12/11.23 inference(component_clause,[status(thm)],[f476])).
% 45.12/11.23 fof(f479,definition,(
% 45.12/11.23 sQ19_spl <=> (aScalar0(xS))),
% 45.12/11.23 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 45.12/11.23 fof(f481,plain,(
% 45.12/11.23 ~aScalar0(xS)|sQ19_spl),
% 45.12/11.23 inference(component_clause,[status(thm)],[f479])).
% 45.12/11.23 fof(f492,definition,(
% 45.12/11.23 sQ22_spl <=> (aScalar0(xP))),
% 45.12/11.23 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 45.12/11.23 fof(f494,plain,(
% 45.59/11.23 ~aScalar0(xP)|sQ22_spl),
% 45.59/11.23 inference(component_clause,[status(thm)],[f492])).
% 45.59/11.23 fof(f500,plain,(
% 45.59/11.23 $false|sQ18_spl),
% 45.59/11.23 inference(forward_subsumption_resolution,[status(thm)],[f478,f84])).
% 45.59/11.23 fof(f501,plain,(
% 45.59/11.23 sQ18_spl),
% 45.59/11.23 inference(contradiction_clause,[status(thm)],[f500])).
% 45.59/11.23 fof(f507,definition,(
% 45.59/11.23 sQ25_spl <=> (aScalar0(xR))),
% 45.59/11.23 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 45.59/11.23 fof(f509,plain,(
% 45.59/11.23 ~aScalar0(xR)|sQ25_spl),
% 45.59/11.23 inference(component_clause,[status(thm)],[f507])).
% 45.59/11.23 fof(f648,plain,(
% 45.59/11.23 aScalar0(smndt0(xS))),
% 45.59/11.23 inference(resolution,[status(thm)],[f192,f90])).
% 45.59/11.23 fof(f658,plain,(
% 45.59/11.23 ![X0]: (~aScalar0(X0)|sdtasdt0(X0,xS)=sdtasdt0(xS,X0)|~sQ3_spl)),
% 45.59/11.23 inference(resolution,[status(thm)],[f192,f215])).
% 45.59/11.23 fof(f659,plain,(
% 45.59/11.23 ![X0]: (~aScalar0(X0)|sdtpldt0(X0,xS)=sdtpldt0(xS,X0)|~sQ2_spl)),
% 45.59/11.23 inference(resolution,[status(thm)],[f192,f211])).
% 45.59/11.23 fof(f713,plain,(
% 45.59/11.23 ![X0]: (~aScalar0(X0)|sdtasdt0(X0,sdtpldt0(xR,xS))=sdtpldt0(sdtasdt0(X0,xR),sdtasdt0(X0,xS)))),
% 45.59/11.23 inference(resolution,[status(thm)],[f192,f233])).
% 45.59/11.23 fof(f714,plain,(
% 45.59/11.23 ![X0]: (~aScalar0(X0)|sdtasdt0(X0,sdtpldt0(xS,xR))=sdtpldt0(sdtasdt0(X0,xS),sdtasdt0(X0,xR)))),
% 45.59/11.23 inference(resolution,[status(thm)],[f192,f231])).
% 45.59/11.23 fof(f716,plain,(
% 45.59/11.23 ![X0]: (~aScalar0(X0)|sdtasdt0(sdtpldt0(X0,xR),xS)=sdtpldt0(sdtasdt0(X0,xS),sdtasdt0(xR,xS)))),
% 45.59/11.23 inference(resolution,[status(thm)],[f192,f229])).
% 45.59/11.23 fof(f723,plain,(
% 45.59/11.23 ![X0]: (~aScalar0(X0)|sdtasdt0(sdtpldt0(X0,xS),sdtpldt0(xR,xS))=sdtpldt0(sdtpldt0(sdtasdt0(X0,xR),sdtasdt0(X0,xS)),sdtpldt0(sdtasdt0(xS,xR),sdtasdt0(xS,xS))))),
% 45.59/11.23 inference(resolution,[status(thm)],[f192,f222])).
% 45.59/11.23 fof(f733,definition,(
% 45.59/11.23 sQ43_spl <=> (sdtlseqdt0(xS,xS))),
% 45.59/11.23 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 45.59/11.23 fof(f735,plain,(
% 45.59/11.23 ~sdtlseqdt0(xS,xS)|sQ43_spl),
% 45.59/11.23 inference(component_clause,[status(thm)],[f733])).
% 45.59/11.23 fof(f738,plain,(
% 45.59/11.23 ![X0]: (~aScalar0(X0)|sdtasdt0(sdtpldt0(X0,xR),xS)=sdtpldt0(sdtasdt0(X0,xS),xN))),
% 45.59/11.23 inference(forward_demodulation,[status(thm)],[f195,f716])).
% 45.59/11.23 fof(f820,plain,(
% 45.59/11.23 sdtasdt0(xP,sdtpldt0(xP,xP))=sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP))),
% 45.59/11.23 inference(resolution,[status(thm)],[f190,f254])).
% 45.59/11.23 fof(f837,plain,(
% 45.59/11.23 sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP))=sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)))),
% 45.59/11.23 inference(resolution,[status(thm)],[f190,f243])).
% 45.59/11.23 fof(f866,definition,(
% 45.59/11.23 sQ45_spl <=> (sdtlseqdt0(xP,xP))),
% 45.59/11.23 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 45.59/11.23 fof(f868,plain,(
% 45.59/11.23 ~sdtlseqdt0(xP,xP)|sQ45_spl),
% 45.59/11.23 inference(component_clause,[status(thm)],[f866])).
% 45.59/11.23 fof(f924,plain,(
% 45.59/11.23 sdtasdt0(sdtpldt0(xR,xS),xS)=sdtpldt0(sdtasdt0(xR,xS),sdtasdt0(xS,xS))),
% 45.59/11.23 inference(resolution,[status(thm)],[f188,f274])).
% 45.59/11.23 fof(f996,plain,(
% 45.59/11.23 sdtasdt0(sdtpldt0(xR,xS),xS)=sdtpldt0(xN,sdtasdt0(xS,xS))),
% 45.59/11.23 inference(forward_demodulation,[status(thm)],[f195,f924])).
% 45.59/11.23 fof(f1008,definition,(
% 45.59/11.23 sQ47_spl <=> (sdtlseqdt0(xR,xR))),
% 45.59/11.23 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 45.59/11.23 fof(f1010,plain,(
% 45.59/11.23 ~sdtlseqdt0(xR,xR)|sQ47_spl),
% 45.59/11.23 inference(component_clause,[status(thm)],[f1008])).
% 45.59/11.23 fof(f1021,plain,(
% 45.59/11.23 sdtasdt0(sz0z00,xR)=sz0z00),
% 45.59/11.23 inference(resolution,[status(thm)],[f95,f188])).
% 45.59/11.23 fof(f1022,plain,(
% 45.59/11.23 sdtasdt0(sz0z00,xP)=sz0z00),
% 45.59/11.23 inference(resolution,[status(thm)],[f95,f190])).
% 45.59/11.23 fof(f1023,plain,(
% 45.59/11.23 sdtasdt0(sz0z00,xS)=sz0z00),
% 45.59/11.23 inference(resolution,[status(thm)],[f95,f192])).
% 45.59/11.23 fof(f1031,definition,(
% 45.59/11.23 sQ49_spl <=> (aScalar0(sdtpldt0(xS,xS)))),
% 45.59/11.23 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 45.59/11.23 fof(f1033,plain,(
% 45.59/11.23 ~aScalar0(sdtpldt0(xS,xS))|sQ49_spl),
% 45.59/11.23 inference(component_clause,[status(thm)],[f1031])).
% 45.59/11.23 fof(f1045,definition,(
% 45.59/11.23 sQ52_spl <=> (aScalar0(sdtasdt0(sz0z00,xS)))),
% 45.59/11.23 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 45.59/11.23 fof(f1047,plain,(
% 45.59/11.23 ~aScalar0(sdtasdt0(sz0z00,xS))|sQ52_spl),
% 45.59/11.23 inference(component_clause,[status(thm)],[f1045])).
% 45.59/11.23 fof(f1048,definition,(
% 45.59/11.23 sQ53_spl <=> (aScalar0(sdtasdt0(xS,xS)))),
% 45.59/11.23 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 45.59/11.23 fof(f1050,plain,(
% 45.59/11.23 ~aScalar0(sdtasdt0(xS,xS))|sQ53_spl),
% 45.59/11.23 inference(component_clause,[status(thm)],[f1048])).
% 45.59/11.23 fof(f1062,definition,(
% 45.59/11.23 sQ56_spl <=> (aScalar0(sdtpldt0(xP,xP)))),
% 45.59/11.23 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 45.59/11.23 fof(f1064,plain,(
% 45.59/11.23 ~aScalar0(sdtpldt0(xP,xP))|sQ56_spl),
% 45.59/11.23 inference(component_clause,[status(thm)],[f1062])).
% 45.59/11.23 fof(f1080,definition,(
% 45.59/11.23 sQ59_spl <=> (aScalar0(sdtasdt0(sz0z00,xP)))),
% 45.59/11.23 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 45.59/11.23 fof(f1082,plain,(
% 45.59/11.23 ~aScalar0(sdtasdt0(sz0z00,xP))|sQ59_spl),
% 45.59/11.23 inference(component_clause,[status(thm)],[f1080])).
% 45.59/11.23 fof(f1083,definition,(
% 45.59/11.23 sQ60_spl <=> (aScalar0(sdtasdt0(xP,xP)))),
% 45.59/11.23 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 45.59/11.23 fof(f1085,plain,(
% 45.59/11.23 ~aScalar0(sdtasdt0(xP,xP))|sQ60_spl),
% 45.59/11.23 inference(component_clause,[status(thm)],[f1083])).
% 45.59/11.23 fof(f1097,definition,(
% 45.59/11.23 sQ63_spl <=> (aScalar0(sdtpldt0(xR,xR)))),
% 45.59/11.23 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 45.59/11.23 fof(f1099,plain,(
% 45.59/11.23 ~aScalar0(sdtpldt0(xR,xR))|sQ63_spl),
% 45.59/11.23 inference(component_clause,[status(thm)],[f1097])).
% 45.59/11.23 fof(f1111,definition,(
% 45.59/11.23 sQ66_spl <=> (aScalar0(sdtasdt0(sz0z00,xR)))),
% 45.59/11.23 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 45.59/11.23 fof(f1113,plain,(
% 45.59/11.23 ~aScalar0(sdtasdt0(sz0z00,xR))|sQ66_spl),
% 45.59/11.23 inference(component_clause,[status(thm)],[f1111])).
% 45.59/11.23 fof(f1114,definition,(
% 45.59/11.23 sQ67_spl <=> (aScalar0(sdtasdt0(xR,xR)))),
% 45.59/11.23 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 45.59/11.23 fof(f1116,plain,(
% 45.59/11.23 ~aScalar0(sdtasdt0(xR,xR))|sQ67_spl),
% 45.59/11.23 inference(component_clause,[status(thm)],[f1114])).
% 45.59/11.23 fof(f1122,plain,(
% 45.59/11.23 $false|sQ19_spl),
% 45.59/11.23 inference(forward_subsumption_resolution,[status(thm)],[f481,f192])).
% 45.59/11.23 fof(f1123,plain,(
% 45.59/11.23 sQ19_spl),
% 45.59/11.23 inference(contradiction_clause,[status(thm)],[f1122])).
% 45.59/11.23 fof(f1124,plain,(
% 45.59/11.23 $false|sQ22_spl),
% 45.59/11.23 inference(forward_subsumption_resolution,[status(thm)],[f494,f190])).
% 45.59/11.23 fof(f1125,plain,(
% 45.59/11.23 sQ22_spl),
% 45.59/11.23 inference(contradiction_clause,[status(thm)],[f1124])).
% 45.59/11.23 fof(f1126,plain,(
% 45.59/11.23 $false|sQ25_spl),
% 45.59/11.23 inference(forward_subsumption_resolution,[status(thm)],[f509,f188])).
% 45.59/11.23 fof(f1127,plain,(
% 45.59/11.23 sQ25_spl),
% 45.59/11.23 inference(contradiction_clause,[status(thm)],[f1126])).
% 45.59/11.23 fof(f1144,plain,(
% 45.59/11.23 aScalar0(sdtpldt0(xR,xR))),
% 45.59/11.23 inference(resolution,[status(thm)],[f225,f188])).
% 45.59/11.23 fof(f1146,plain,(
% 45.59/11.23 aScalar0(sdtpldt0(xS,xR))),
% 45.59/11.23 inference(resolution,[status(thm)],[f225,f192])).
% 45.59/11.23 fof(f1150,plain,(
% 45.59/11.23 aScalar0(sdtpldt0(xP,xP))),
% 45.59/11.23 inference(resolution,[status(thm)],[f249,f190])).
% 45.59/11.23 fof(f1151,plain,(
% 45.59/11.23 aScalar0(sdtpldt0(xS,xP))),
% 45.59/11.23 inference(resolution,[status(thm)],[f249,f192])).
% 45.59/11.23 fof(f1177,plain,(
% 45.59/11.23 aScalar0(sdtpldt0(smndt0(xS),xP))),
% 45.59/11.23 inference(resolution,[status(thm)],[f648,f249])).
% 45.59/11.23 fof(f1178,plain,(
% 45.59/11.23 aScalar0(sdtpldt0(smndt0(xS),xR))),
% 45.59/11.23 inference(resolution,[status(thm)],[f648,f225])).
% 45.59/11.23 fof(f1353,plain,(
% 45.59/11.23 sdtasdt0(xR,xS)=sdtasdt0(xS,xR)|~sQ3_spl),
% 45.59/11.23 inference(resolution,[status(thm)],[f658,f188])).
% 45.59/11.23 fof(f1357,plain,(
% 45.59/11.23 xN=sdtasdt0(xS,xR)|~sQ3_spl),
% 45.59/11.23 inference(forward_demodulation,[status(thm)],[f195,f1353])).
% 45.59/11.23 fof(f1359,plain,(
% 45.59/11.23 sdtpldt0(xR,xS)=sdtpldt0(xS,xR)|~sQ2_spl),
% 45.59/11.23 inference(resolution,[status(thm)],[f659,f188])).
% 45.59/11.23 fof(f1449,definition,(
% 45.59/11.23 sQ86_spl <=> (aScalar0(sdtpldt0(xS,xP)))),
% 45.59/11.23 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 45.59/11.23 fof(f1451,plain,(
% 45.59/11.23 ~aScalar0(sdtpldt0(xS,xP))|sQ86_spl),
% 45.59/11.23 inference(component_clause,[status(thm)],[f1449])).
% 45.59/11.23 fof(f1460,plain,(
% 45.59/11.23 aScalar0(sdtpldt0(xS,xS))),
% 45.59/11.23 inference(resolution,[status(thm)],[f273,f192])).
% 45.59/11.23 fof(f1537,plain,(
% 45.59/11.23 aScalar0(sdtasdt0(xS,xS))),
% 45.59/11.23 inference(resolution,[status(thm)],[f302,f192])).
% 45.59/11.23 fof(f1542,plain,(
% 45.59/11.23 aScalar0(sdtasdt0(xP,xP))),
% 45.59/11.23 inference(resolution,[status(thm)],[f303,f190])).
% 45.59/11.23 fof(f1635,definition,(
% 45.59/11.23 sQ98_spl <=> (aScalar0(sdtpldt0(xS,xR)))),
% 45.59/11.23 introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition])).
% 45.59/11.23 fof(f1637,plain,(
% 45.59/11.23 ~aScalar0(sdtpldt0(xS,xR))|sQ98_spl),
% 45.59/11.23 inference(component_clause,[status(thm)],[f1635])).
% 45.59/11.23 fof(f1670,plain,(
% 45.59/11.23 sdtasdt0(xR,sdtpldt0(xR,xS))=sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xR,xS))),
% 45.59/11.23 inference(resolution,[status(thm)],[f713,f188])).
% 45.59/11.23 fof(f1672,plain,(
% 45.59/11.23 sdtasdt0(xS,sdtpldt0(xR,xS))=sdtpldt0(sdtasdt0(xS,xR),sdtasdt0(xS,xS))),
% 45.59/11.23 inference(resolution,[status(thm)],[f713,f192])).
% 45.59/11.23 fof(f1674,plain,(
% 45.59/11.23 sdtasdt0(xR,sdtpldt0(xR,xS))=sdtpldt0(sdtasdt0(xR,xR),xN)),
% 45.59/11.23 inference(forward_demodulation,[status(thm)],[f195,f1670])).
% 45.59/11.23 fof(f1678,plain,(
% 45.59/11.23 sdtasdt0(xS,sdtpldt0(xS,xR))=sdtpldt0(sdtasdt0(xS,xS),sdtasdt0(xS,xR))),
% 45.59/11.23 inference(resolution,[status(thm)],[f714,f192])).
% 45.59/11.23 fof(f1681,plain,(
% 45.59/11.23 aScalar0(sdtasdt0(smndt0(xS),xR))),
% 45.59/11.23 inference(resolution,[status(thm)],[f304,f648])).
% 45.59/11.23 fof(f1682,plain,(
% 45.59/11.23 aScalar0(sdtasdt0(xR,xR))),
% 45.59/11.23 inference(resolution,[status(thm)],[f304,f188])).
% 45.59/11.23 fof(f1704,plain,(
% 45.59/11.23 sdtasdt0(sdtpldt0(xS,xR),xS)=sdtpldt0(sdtasdt0(xS,xS),xN)),
% 45.59/11.23 inference(resolution,[status(thm)],[f738,f192])).
% 45.59/11.23 fof(f1752,plain,(
% 45.59/11.23 sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS))=sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xR,xS)),sdtpldt0(sdtasdt0(xS,xR),sdtasdt0(xS,xS)))),
% 45.59/11.23 inference(resolution,[status(thm)],[f723,f188])).
% 45.59/11.23 fof(f1757,plain,(
% 45.59/11.23 sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS))=sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),xN),sdtpldt0(sdtasdt0(xS,xR),sdtasdt0(xS,xS)))),
% 45.59/11.23 inference(forward_demodulation,[status(thm)],[f195,f1752])).
% 45.59/11.23 fof(f1772,plain,(
% 45.59/11.23 $false|sQ43_spl),
% 45.59/11.23 inference(forward_subsumption_resolution,[status(thm)],[f735,f266])).
% 45.59/11.23 fof(f1773,plain,(
% 45.59/11.23 sQ43_spl),
% 45.59/11.23 inference(contradiction_clause,[status(thm)],[f1772])).
% 45.59/11.23 fof(f1781,plain,(
% 45.59/11.23 $false|sQ45_spl),
% 45.59/11.23 inference(forward_subsumption_resolution,[status(thm)],[f868,f242])).
% 45.59/11.23 fof(f1782,plain,(
% 45.59/11.23 sQ45_spl),
% 45.59/11.23 inference(contradiction_clause,[status(thm)],[f1781])).
% 45.59/11.23 fof(f2091,plain,(
% 45.59/11.23 $false|sQ47_spl),
% 45.59/11.23 inference(forward_subsumption_resolution,[status(thm)],[f1010,f218])).
% 45.59/11.23 fof(f2092,plain,(
% 45.59/11.23 sQ47_spl),
% 45.59/11.23 inference(contradiction_clause,[status(thm)],[f2091])).
% 45.59/11.23 fof(f2173,plain,(
% 45.59/11.23 sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,sdtpldt0(xP,xP))),sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),xN),sdtpldt0(sdtasdt0(xS,xR),sdtasdt0(xS,xS))))),
% 45.59/11.23 inference(backward_demodulation,[status(thm)],[f820,f317])).
% 45.59/11.23 fof(f2178,plain,(
% 45.59/11.23 sdtlseqdt0(sdtpldt0(sdtasdt0(xP,sdtpldt0(xP,xP)),sdtasdt0(xP,sdtpldt0(xP,xP))),sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),xN),sdtpldt0(sdtasdt0(xS,xR),sdtasdt0(xS,xS))))),
% 45.59/11.23 inference(forward_demodulation,[status(thm)],[f820,f2173])).
% 45.59/11.23 fof(f2213,plain,(
% 45.59/11.23 sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP))=sdtpldt0(sdtasdt0(xP,sdtpldt0(xP,xP)),sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)))),
% 45.59/11.23 inference(forward_demodulation,[status(thm)],[f820,f837])).
% 45.59/11.23 fof(f2214,plain,(
% 45.59/11.23 sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP))=sdtpldt0(sdtasdt0(xP,sdtpldt0(xP,xP)),sdtasdt0(xP,sdtpldt0(xP,xP)))),
% 45.59/11.23 inference(forward_demodulation,[status(thm)],[f820,f2213])).
% 45.59/11.23 fof(f2257,plain,(
% 45.59/11.23 sdtlseqdt0(sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)),sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),xN),sdtpldt0(sdtasdt0(xS,xR),sdtasdt0(xS,xS))))),
% 45.59/11.24 inference(forward_demodulation,[status(thm)],[f2214,f2178])).
% 45.59/11.24 fof(f2337,plain,(
% 45.59/11.24 sdtlseqdt0(sz0z00,sz0z00)|sdtlseqdt0(sz0z00,sz0z00)),
% 45.59/11.24 inference(resolution,[status(thm)],[f419,f84])).
% 45.59/11.24 fof(f2373,plain,(
% 45.59/11.24 sQ16_spl),
% 45.59/11.24 inference(split_clause,[status(thm)],[f2337,f457])).
% 45.59/11.24 fof(f3169,plain,(
% 45.59/11.24 $false|sQ63_spl),
% 45.59/11.24 inference(forward_subsumption_resolution,[status(thm)],[f1144,f1099])).
% 45.59/11.24 fof(f3170,plain,(
% 45.59/11.24 sQ63_spl),
% 45.59/11.24 inference(contradiction_clause,[status(thm)],[f3169])).
% 45.59/11.24 fof(f3921,plain,(
% 45.59/11.24 $false|sQ56_spl),
% 45.59/11.24 inference(forward_subsumption_resolution,[status(thm)],[f1150,f1064])).
% 45.59/11.24 fof(f3922,plain,(
% 45.59/11.24 sQ56_spl),
% 45.59/11.24 inference(contradiction_clause,[status(thm)],[f3921])).
% 45.59/11.24 fof(f5252,definition,(
% 45.59/11.24 sQ286_spl <=> (aVector0(xs))),
% 45.59/11.24 introduced(definition,[new_symbols(definition,[sQ286_spl])],[split_symbol_definition])).
% 45.59/11.24 fof(f5254,plain,(
% 45.59/11.24 ~aVector0(xs)|sQ286_spl),
% 45.59/11.24 inference(component_clause,[status(thm)],[f5252])).
% 45.59/11.24 fof(f5255,definition,(
% 45.59/11.24 sQ287_spl <=> (aVector0(xt))),
% 45.59/11.24 introduced(definition,[new_symbols(definition,[sQ287_spl])],[split_symbol_definition])).
% 45.59/11.24 fof(f5257,plain,(
% 45.59/11.24 ~aVector0(xt)|sQ287_spl),
% 45.59/11.24 inference(component_clause,[status(thm)],[f5255])).
% 45.59/11.24 fof(f5271,plain,(
% 45.59/11.24 $false|sQ286_spl),
% 45.59/11.24 inference(forward_subsumption_resolution,[status(thm)],[f5254,f162])).
% 45.59/11.24 fof(f5272,plain,(
% 45.59/11.24 sQ286_spl),
% 45.59/11.24 inference(contradiction_clause,[status(thm)],[f5271])).
% 45.59/11.24 fof(f5273,plain,(
% 45.59/11.24 $false|sQ287_spl),
% 45.59/11.24 inference(forward_subsumption_resolution,[status(thm)],[f5257,f163])).
% 45.59/11.24 fof(f5274,plain,(
% 45.59/11.24 sQ287_spl),
% 45.59/11.24 inference(contradiction_clause,[status(thm)],[f5273])).
% 45.59/11.24 fof(f5377,definition,(
% 45.59/11.24 sQ301_spl <=> (aScalar0(sdtpldt0(smndt0(xS),xP)))),
% 45.59/11.24 introduced(definition,[new_symbols(definition,[sQ301_spl])],[split_symbol_definition])).
% 45.59/11.24 fof(f5379,plain,(
% 45.59/11.24 ~aScalar0(sdtpldt0(smndt0(xS),xP))|sQ301_spl),
% 45.59/11.24 inference(component_clause,[status(thm)],[f5377])).
% 45.59/11.24 fof(f5385,plain,(
% 45.59/11.24 $false|sQ301_spl),
% 45.59/11.24 inference(forward_subsumption_resolution,[status(thm)],[f5379,f1177])).
% 45.59/11.24 fof(f5386,plain,(
% 45.59/11.24 sQ301_spl),
% 45.59/11.24 inference(contradiction_clause,[status(thm)],[f5385])).
% 45.59/11.24 fof(f5504,definition,(
% 45.59/11.24 sQ307_spl <=> (aScalar0(sdtpldt0(smndt0(xS),xR)))),
% 45.59/11.24 introduced(definition,[new_symbols(definition,[sQ307_spl])],[split_symbol_definition])).
% 45.59/11.24 fof(f5506,plain,(
% 45.59/11.24 ~aScalar0(sdtpldt0(smndt0(xS),xR))|sQ307_spl),
% 45.59/11.24 inference(component_clause,[status(thm)],[f5504])).
% 45.59/11.24 fof(f5512,plain,(
% 45.59/11.24 $false|sQ307_spl),
% 45.59/11.24 inference(forward_subsumption_resolution,[status(thm)],[f5506,f1178])).
% 45.59/11.24 fof(f5513,plain,(
% 45.59/11.24 sQ307_spl),
% 45.59/11.24 inference(contradiction_clause,[status(thm)],[f5512])).
% 45.59/11.24 fof(f5612,definition,(
% 45.59/11.24 sQ310_spl <=> (aScalar0(sdtasdt0(smndt0(xS),xR)))),
% 45.59/11.24 introduced(definition,[new_symbols(definition,[sQ310_spl])],[split_symbol_definition])).
% 45.59/11.24 fof(f5614,plain,(
% 45.59/11.24 ~aScalar0(sdtasdt0(smndt0(xS),xR))|sQ310_spl),
% 45.59/11.24 inference(component_clause,[status(thm)],[f5612])).
% 45.59/11.24 fof(f5635,plain,(
% 45.59/11.24 sdtlseqdt0(sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)),sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),xN),sdtpldt0(xN,sdtasdt0(xS,xS))))|~sQ3_spl),
% 45.59/11.24 inference(backward_demodulation,[status(thm)],[f1357,f2257])).
% 45.59/11.24 fof(f5650,plain,(
% 45.59/11.24 sdtlseqdt0(sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)),sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),xN),sdtasdt0(sdtpldt0(xR,xS),xS)))|~sQ3_spl),
% 45.59/11.24 inference(forward_demodulation,[status(thm)],[f996,f5635])).
% 45.59/11.24 fof(f5681,plain,(
% 45.59/11.24 ~sdtlseqdt0(sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)),sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xS,xR)))|~sQ2_spl),
% 45.59/11.24 inference(backward_demodulation,[status(thm)],[f1359,f202])).
% 45.59/11.24 fof(f5684,plain,(
% 45.59/11.24 ~sdtlseqdt0(sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)),sdtasdt0(sdtpldt0(xS,xR),sdtpldt0(xS,xR)))|~sQ2_spl),
% 45.59/11.24 inference(forward_demodulation,[status(thm)],[f1359,f5681])).
% 45.59/11.24 fof(f5818,plain,(
% 45.59/11.24 sdtlseqdt0(sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)),sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),xN),sdtasdt0(sdtpldt0(xS,xR),xS)))|~sQ2_spl|~sQ3_spl),
% 45.59/11.24 inference(forward_demodulation,[status(thm)],[f1359,f5650])).
% 45.59/11.24 fof(f5985,plain,(
% 45.59/11.24 $false|sQ86_spl),
% 45.59/11.24 inference(forward_subsumption_resolution,[status(thm)],[f1451,f1151])).
% 45.59/11.24 fof(f5986,plain,(
% 45.59/11.24 sQ86_spl),
% 45.59/11.24 inference(contradiction_clause,[status(thm)],[f5985])).
% 45.59/11.24 fof(f5989,plain,(
% 45.59/11.24 $false|sQ49_spl),
% 45.59/11.24 inference(forward_subsumption_resolution,[status(thm)],[f1460,f1033])).
% 45.59/11.24 fof(f5990,plain,(
% 45.59/11.24 sQ49_spl),
% 45.59/11.24 inference(contradiction_clause,[status(thm)],[f5989])).
% 45.59/11.24 fof(f7071,plain,(
% 45.59/11.24 $false|sQ53_spl),
% 45.59/11.24 inference(forward_subsumption_resolution,[status(thm)],[f1537,f1050])).
% 45.59/11.24 fof(f7072,plain,(
% 45.59/11.24 sQ53_spl),
% 45.59/11.24 inference(contradiction_clause,[status(thm)],[f7071])).
% 45.59/11.24 fof(f7073,plain,(
% 45.59/11.24 ~aScalar0(sz0z00)|sQ52_spl),
% 45.59/11.24 inference(forward_demodulation,[status(thm)],[f1023,f1047])).
% 45.59/11.24 fof(f7074,plain,(
% 45.59/11.24 $false|sQ52_spl),
% 45.59/11.24 inference(forward_subsumption_resolution,[status(thm)],[f7073,f84])).
% 45.59/11.24 fof(f7075,plain,(
% 45.59/11.24 sQ52_spl),
% 45.59/11.24 inference(contradiction_clause,[status(thm)],[f7074])).
% 45.59/11.24 fof(f7720,plain,(
% 45.59/11.24 $false|sQ60_spl),
% 45.59/11.24 inference(forward_subsumption_resolution,[status(thm)],[f1542,f1085])).
% 45.59/11.24 fof(f7721,plain,(
% 45.59/11.24 sQ60_spl),
% 45.59/11.24 inference(contradiction_clause,[status(thm)],[f7720])).
% 45.59/11.24 fof(f7722,plain,(
% 45.59/11.24 ~aScalar0(sz0z00)|sQ59_spl),
% 45.59/11.24 inference(forward_demodulation,[status(thm)],[f1022,f1082])).
% 45.59/11.24 fof(f7723,plain,(
% 45.59/11.24 $false|sQ59_spl),
% 45.59/11.24 inference(forward_subsumption_resolution,[status(thm)],[f7722,f84])).
% 45.59/11.24 fof(f7724,plain,(
% 45.59/11.24 sQ59_spl),
% 45.59/11.24 inference(contradiction_clause,[status(thm)],[f7723])).
% 45.59/11.24 fof(f9390,plain,(
% 45.59/11.24 $false|sQ98_spl),
% 45.59/11.24 inference(forward_subsumption_resolution,[status(thm)],[f1637,f1146])).
% 45.59/11.24 fof(f9391,plain,(
% 45.59/11.24 sQ98_spl),
% 45.59/11.24 inference(contradiction_clause,[status(thm)],[f9390])).
% 45.59/11.24 fof(f9649,plain,(
% 45.59/11.24 sdtlseqdt0(sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)),sdtpldt0(sdtasdt0(xR,sdtpldt0(xS,xR)),sdtasdt0(sdtpldt0(xS,xR),xS)))|~sQ2_spl|~sQ3_spl),
% 45.59/11.24 inference(backward_demodulation,[status(thm)],[f9650,f5818])).
% 45.59/11.24 fof(f9650,plain,(
% 45.59/11.24 sdtasdt0(xR,sdtpldt0(xS,xR))=sdtpldt0(sdtasdt0(xR,xR),xN)|~sQ2_spl),
% 45.59/11.24 inference(forward_demodulation,[status(thm)],[f1359,f1674])).
% 45.59/11.24 fof(f9678,plain,(
% 45.59/11.24 sdtasdt0(xS,sdtpldt0(xS,xR))=sdtpldt0(sdtasdt0(xS,xR),sdtasdt0(xS,xS))|~sQ2_spl),
% 45.59/11.24 inference(forward_demodulation,[status(thm)],[f1359,f1672])).
% 45.59/11.24 fof(f9680,plain,(
% 45.59/11.24 sdtasdt0(xS,sdtpldt0(xS,xR))=sdtpldt0(xN,sdtasdt0(xS,xS))|~sQ3_spl|~sQ2_spl),
% 45.59/11.24 inference(forward_demodulation,[status(thm)],[f1357,f9678])).
% 45.59/11.24 fof(f9715,plain,(
% 45.59/11.24 sdtasdt0(xS,sdtpldt0(xS,xR))=sdtpldt0(sdtasdt0(xS,xS),xN)|~sQ3_spl),
% 45.59/11.24 inference(forward_demodulation,[status(thm)],[f1357,f1678])).
% 45.59/11.24 fof(f10075,plain,(
% 45.59/11.24 $false|sQ67_spl),
% 45.59/11.24 inference(forward_subsumption_resolution,[status(thm)],[f1682,f1116])).
% 45.59/11.24 fof(f10076,plain,(
% 45.59/11.24 sQ67_spl),
% 45.59/11.24 inference(contradiction_clause,[status(thm)],[f10075])).
% 45.59/11.24 fof(f10077,plain,(
% 45.59/11.24 ~aScalar0(sz0z00)|sQ66_spl),
% 45.59/11.24 inference(forward_demodulation,[status(thm)],[f1021,f1113])).
% 45.59/11.24 fof(f10078,plain,(
% 45.59/11.24 $false|sQ66_spl),
% 45.59/11.24 inference(forward_subsumption_resolution,[status(thm)],[f10077,f84])).
% 45.59/11.24 fof(f10079,plain,(
% 45.59/11.24 sQ66_spl),
% 45.59/11.24 inference(contradiction_clause,[status(thm)],[f10078])).
% 45.59/11.24 fof(f10080,plain,(
% 45.59/11.24 $false|sQ310_spl),
% 45.59/11.24 inference(forward_subsumption_resolution,[status(thm)],[f5614,f1681])).
% 45.59/11.24 fof(f10081,plain,(
% 45.59/11.24 sQ310_spl),
% 45.59/11.24 inference(contradiction_clause,[status(thm)],[f10080])).
% 45.59/11.24 fof(f10793,plain,(
% 45.59/11.24 sdtlseqdt0(sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)),sdtpldt0(sdtasdt0(xR,sdtpldt0(xS,xR)),sdtasdt0(xS,sdtpldt0(xS,xR))))|~sQ2_spl|~sQ3_spl),
% 45.59/11.24 inference(backward_demodulation,[status(thm)],[f10794,f9649])).
% 45.59/11.24 fof(f10794,plain,(
% 45.59/11.24 sdtasdt0(sdtpldt0(xS,xR),xS)=sdtasdt0(xS,sdtpldt0(xS,xR))|~sQ3_spl),
% 45.59/11.24 inference(forward_demodulation,[status(thm)],[f9715,f1704])).
% 45.59/11.24 fof(f11214,plain,(
% 45.59/11.24 sdtasdt0(sdtpldt0(xS,xR),sdtpldt0(xR,xS))=sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),xN),sdtpldt0(sdtasdt0(xS,xR),sdtasdt0(xS,xS)))|~sQ2_spl),
% 45.59/11.24 inference(forward_demodulation,[status(thm)],[f1359,f1757])).
% 45.59/11.24 fof(f11215,plain,(
% 45.59/11.24 sdtasdt0(sdtpldt0(xS,xR),sdtpldt0(xS,xR))=sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),xN),sdtpldt0(sdtasdt0(xS,xR),sdtasdt0(xS,xS)))|~sQ2_spl),
% 45.59/11.24 inference(forward_demodulation,[status(thm)],[f1359,f11214])).
% 45.59/11.24 fof(f11216,plain,(
% 45.59/11.24 sdtasdt0(sdtpldt0(xS,xR),sdtpldt0(xS,xR))=sdtpldt0(sdtasdt0(xR,sdtpldt0(xS,xR)),sdtpldt0(sdtasdt0(xS,xR),sdtasdt0(xS,xS)))|~sQ2_spl),
% 45.59/11.24 inference(forward_demodulation,[status(thm)],[f9650,f11215])).
% 45.59/11.27 fof(f11217,plain,(
% 45.59/11.27 sdtasdt0(sdtpldt0(xS,xR),sdtpldt0(xS,xR))=sdtpldt0(sdtasdt0(xR,sdtpldt0(xS,xR)),sdtpldt0(xN,sdtasdt0(xS,xS)))|~sQ3_spl|~sQ2_spl),
% 45.59/11.27 inference(forward_demodulation,[status(thm)],[f1357,f11216])).
% 45.59/11.27 fof(f11218,plain,(
% 45.59/11.27 sdtlseqdt0(sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)),sdtasdt0(sdtpldt0(xS,xR),sdtpldt0(xS,xR)))|~sQ2_spl|~sQ3_spl),
% 45.59/11.27 inference(backward_demodulation,[status(thm)],[f11219,f10793])).
% 45.59/11.27 fof(f11219,plain,(
% 45.59/11.27 sdtasdt0(sdtpldt0(xS,xR),sdtpldt0(xS,xR))=sdtpldt0(sdtasdt0(xR,sdtpldt0(xS,xR)),sdtasdt0(xS,sdtpldt0(xS,xR)))|~sQ3_spl|~sQ2_spl),
% 45.59/11.27 inference(forward_demodulation,[status(thm)],[f9680,f11217])).
% 45.59/11.27 fof(f11222,plain,(
% 45.59/11.27 $false|~sQ2_spl|~sQ3_spl),
% 45.59/11.27 inference(forward_subsumption_resolution,[status(thm)],[f11218,f5684])).
% 45.59/11.27 fof(f11223,plain,(
% 45.59/11.27 ~sQ2_spl|~sQ3_spl),
% 45.59/11.27 inference(contradiction_clause,[status(thm)],[f11222])).
% 45.59/11.27 fof(f11224,plain,(
% 45.59/11.27 $false),
% 45.59/11.27 inference(sat_refutation,[status(thm)],[f213,f217,f321,f501,f1123,f1125,f1127,f1773,f1782,f2092,f2373,f3170,f3922,f5272,f5274,f5386,f5513,f5986,f5990,f7072,f7075,f7721,f7724,f9391,f10076,f10079,f10081,f11223])).
% 45.59/11.27 % SZS output end CNFRefutation for theBenchmark.p
% 45.59/11.31 % Elapsed time: 5.914365 seconds
% 45.59/11.31 % CPU time: 46.130711 seconds
% 45.59/11.31 % Total memory used: 362.716 MB
% 45.59/11.31 % Net memory used: 343.814 MB
%------------------------------------------------------------------------------