%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : RNG077+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 : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:05:17 PM UTC 2026
% Result : Theorem 50.22s 6.77s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG077+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.09/0.36 % Computer : n015.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 04:21:06 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 50.22/6.77 % Refutation found
% 50.22/6.77 % SZS status Theorem for theBenchmark: Theorem is valid
% 50.22/6.77 % SZS output start CNFRefutation for theBenchmark
% 50.22/6.77 fof(f9,axiom,(
% 50.22/6.77 aScalar0(sz0z00) ),
% 50.22/6.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.22/6.77 fof(f10,axiom,(
% 50.22/6.77 (! [W0,W1] :( ( aScalar0(W0)& aScalar0(W1) )=> aScalar0(sdtpldt0(W0,W1)) ) )),
% 50.22/6.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.22/6.77 fof(f11,axiom,(
% 50.22/6.77 (! [W0,W1] :( ( aScalar0(W0)& aScalar0(W1) )=> aScalar0(sdtasdt0(W0,W1)) ) )),
% 50.22/6.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.22/6.77 fof(f14,axiom,(
% 50.22/6.77 (! [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) ) ) )),
% 50.22/6.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.22/6.77 fof(f15,axiom,(
% 50.22/6.77 (! [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)) ) ) )),
% 50.22/6.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.22/6.77 fof(f20,axiom,(
% 50.22/6.77 (! [W0] :( aScalar0(W0)=> sdtlseqdt0(W0,W0) ) )),
% 50.22/6.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.22/6.77 fof(f25,axiom,(
% 50.22/6.77 (! [W0,W1] :( ( aScalar0(W0)& aScalar0(W1) )=> ( sdtlseqdt0(W0,W1)| sdtlseqdt0(W1,W0) ) ) )),
% 50.22/6.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.22/6.77 fof(f38,hypothesis,(
% 50.22/6.77 ( aVector0(xs)& aVector0(xt) ) ),
% 50.22/6.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.22/6.77 fof(f40,hypothesis,(
% 50.22/6.77 aDimensionOf0(xs) = aDimensionOf0(xt) ),
% 50.22/6.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.22/6.77 fof(f44,hypothesis,(
% 50.22/6.77 ( aScalar0(xA)& xA = sdtlbdtrb0(xs,aDimensionOf0(xs)) ) ),
% 50.22/6.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.22/6.77 fof(f45,hypothesis,(
% 50.22/6.77 ( aScalar0(xB)& xB = sdtlbdtrb0(xt,aDimensionOf0(xt)) ) ),
% 50.22/6.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.22/6.77 fof(f46,hypothesis,(
% 50.22/6.77 ( aScalar0(xC)& xC = sdtasasdt0(xp,xp) ) ),
% 50.22/6.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.22/6.77 fof(f47,hypothesis,(
% 50.22/6.77 ( aScalar0(xD)& xD = sdtasasdt0(xq,xq) ) ),
% 50.22/6.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.22/6.77 fof(f48,hypothesis,(
% 50.22/6.77 ( aScalar0(xE)& xE = sdtasasdt0(xp,xq) ) ),
% 50.22/6.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.22/6.77 fof(f49,hypothesis,(
% 50.22/6.77 ( aScalar0(xF)& xF = sdtasdt0(xA,xA) ) ),
% 50.22/6.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.22/6.77 fof(f50,hypothesis,(
% 50.22/6.77 ( aScalar0(xG)& xG = sdtasdt0(xB,xB) ) ),
% 50.22/6.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.22/6.77 fof(f51,hypothesis,(
% 50.22/6.77 ( aScalar0(xH)& xH = sdtasdt0(xA,xB) ) ),
% 50.22/6.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.22/6.77 fof(f53,hypothesis,(
% 50.22/6.77 ( aScalar0(xP)& xP = sdtasdt0(xE,xH) ) ),
% 50.22/6.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.22/6.77 fof(f59,conjecture,(
% 50.22/6.77 sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)) = sdtpldt0(sdtasdt0(xE,xH),sdtpldt0(sdtasdt0(xH,xE),sdtasdt0(xH,xH))) ),
% 50.22/6.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.22/6.77 fof(f60,negated_conjecture,(
% 50.22/6.77 ~(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)) = sdtpldt0(sdtasdt0(xE,xH),sdtpldt0(sdtasdt0(xH,xE),sdtasdt0(xH,xH))) )),
% 50.22/6.77 inference(negated_conjecture,[status(cth)],[f59])).
% 50.22/6.77 fof(f81,plain,(
% 50.22/6.77 aScalar0(sz0z00)),
% 50.22/6.77 inference(cnf_transformation,[status(thm)],[f9])).
% 50.22/6.77 fof(f82,plain,(
% 50.22/6.77 ![W0,W1]: ((~aScalar0(W0)|~aScalar0(W1))|aScalar0(sdtpldt0(W0,W1)))),
% 50.22/6.77 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 50.22/6.77 fof(f83,plain,(
% 50.22/6.77 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|aScalar0(sdtpldt0(X0,X1)))),
% 50.22/6.77 inference(cnf_transformation,[status(thm)],[f82])).
% 50.22/6.77 fof(f84,plain,(
% 50.22/6.77 ![W0,W1]: ((~aScalar0(W0)|~aScalar0(W1))|aScalar0(sdtasdt0(W0,W1)))),
% 50.22/6.77 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 50.22/6.77 fof(f85,plain,(
% 50.22/6.77 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|aScalar0(sdtasdt0(X0,X1)))),
% 50.22/6.77 inference(cnf_transformation,[status(thm)],[f84])).
% 50.22/6.77 fof(f97,plain,(
% 50.22/6.77 ![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)))),
% 50.22/6.77 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 50.22/6.77 fof(f98,plain,(
% 50.22/6.77 ![X0,X1,X2]: (~aScalar0(X0)|~aScalar0(X1)|~aScalar0(X2)|sdtpldt0(sdtpldt0(X0,X1),X2)=sdtpldt0(X0,sdtpldt0(X1,X2)))),
% 50.22/6.77 inference(cnf_transformation,[status(thm)],[f97])).
% 50.22/6.77 fof(f99,plain,(
% 50.22/6.77 ![X0,X1,X2]: (~aScalar0(X0)|~aScalar0(X1)|~aScalar0(X2)|sdtpldt0(X0,X1)=sdtpldt0(X1,X0))),
% 50.22/6.77 inference(cnf_transformation,[status(thm)],[f97])).
% 50.22/6.77 fof(f101,plain,(
% 50.22/6.77 ![X0,X1,X2]: (~aScalar0(X0)|~aScalar0(X1)|~aScalar0(X2)|sdtasdt0(X0,X1)=sdtasdt0(X1,X0))),
% 50.22/6.77 inference(cnf_transformation,[status(thm)],[f97])).
% 50.22/6.77 fof(f102,plain,(
% 50.22/6.77 ![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))))),
% 50.22/6.77 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 50.22/6.77 fof(f103,plain,(
% 50.22/6.77 ![X0,X1,X2]: (~aScalar0(X0)|~aScalar0(X1)|~aScalar0(X2)|sdtasdt0(X0,sdtpldt0(X1,X2))=sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2)))),
% 50.22/6.77 inference(cnf_transformation,[status(thm)],[f102])).
% 50.22/6.77 fof(f104,plain,(
% 50.22/6.77 ![X0,X1,X2]: (~aScalar0(X0)|~aScalar0(X1)|~aScalar0(X2)|sdtasdt0(sdtpldt0(X0,X1),X2)=sdtpldt0(sdtasdt0(X0,X2),sdtasdt0(X1,X2)))),
% 50.22/6.77 inference(cnf_transformation,[status(thm)],[f102])).
% 50.22/6.77 fof(f114,plain,(
% 50.22/6.77 ![W0]: (~aScalar0(W0)|sdtlseqdt0(W0,W0))),
% 50.22/6.77 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 50.22/6.77 fof(f115,plain,(
% 50.22/6.77 ![X0]: (~aScalar0(X0)|sdtlseqdt0(X0,X0))),
% 50.22/6.77 inference(cnf_transformation,[status(thm)],[f114])).
% 50.22/6.77 fof(f124,plain,(
% 50.22/6.77 ![W0,W1]: ((~aScalar0(W0)|~aScalar0(W1))|(sdtlseqdt0(W0,W1)|sdtlseqdt0(W1,W0)))),
% 50.22/6.77 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 50.22/6.77 fof(f125,plain,(
% 50.22/6.77 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|sdtlseqdt0(X0,X1)|sdtlseqdt0(X1,X0))),
% 50.22/6.77 inference(cnf_transformation,[status(thm)],[f124])).
% 50.22/6.77 fof(f159,plain,(
% 50.22/6.77 aVector0(xs)),
% 50.22/6.77 inference(cnf_transformation,[status(thm)],[f38])).
% 50.22/6.77 fof(f160,plain,(
% 50.22/6.77 aVector0(xt)),
% 50.22/6.77 inference(cnf_transformation,[status(thm)],[f38])).
% 50.22/6.77 fof(f163,plain,(
% 50.22/6.77 aDimensionOf0(xs)=aDimensionOf0(xt)),
% 50.22/6.77 inference(cnf_transformation,[status(thm)],[f40])).
% 50.22/6.77 fof(f169,plain,(
% 50.22/6.77 aScalar0(xA)),
% 50.22/6.77 inference(cnf_transformation,[status(thm)],[f44])).
% 50.22/6.77 fof(f171,plain,(
% 50.22/6.77 aScalar0(xB)),
% 50.22/6.77 inference(cnf_transformation,[status(thm)],[f45])).
% 50.22/6.77 fof(f173,plain,(
% 50.22/6.77 aScalar0(xC)),
% 50.22/6.77 inference(cnf_transformation,[status(thm)],[f46])).
% 50.22/6.77 fof(f175,plain,(
% 50.22/6.77 aScalar0(xD)),
% 50.22/6.77 inference(cnf_transformation,[status(thm)],[f47])).
% 50.22/6.77 fof(f177,plain,(
% 50.22/6.77 aScalar0(xE)),
% 50.22/6.77 inference(cnf_transformation,[status(thm)],[f48])).
% 50.22/6.77 fof(f179,plain,(
% 50.22/6.77 aScalar0(xF)),
% 50.22/6.77 inference(cnf_transformation,[status(thm)],[f49])).
% 50.22/6.77 fof(f181,plain,(
% 50.22/6.77 aScalar0(xG)),
% 50.22/6.77 inference(cnf_transformation,[status(thm)],[f50])).
% 50.22/6.77 fof(f183,plain,(
% 50.22/6.77 aScalar0(xH)),
% 50.22/6.77 inference(cnf_transformation,[status(thm)],[f51])).
% 50.22/6.77 fof(f187,plain,(
% 50.22/6.77 aScalar0(xP)),
% 50.22/6.77 inference(cnf_transformation,[status(thm)],[f53])).
% 50.22/6.77 fof(f188,plain,(
% 50.22/6.77 xP=sdtasdt0(xE,xH)),
% 50.22/6.77 inference(cnf_transformation,[status(thm)],[f53])).
% 50.22/6.77 fof(f196,plain,(
% 50.22/6.77 ~sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH))=sdtpldt0(sdtasdt0(xE,xH),sdtpldt0(sdtasdt0(xH,xE),sdtasdt0(xH,xH)))),
% 50.22/6.77 inference(cnf_transformation,[status(thm)],[f60])).
% 50.22/6.77 fof(f197,definition,(
% 50.22/6.77 ![X0]: (sQ0_spl <=> (~aScalar0(X0)))),
% 50.22/6.77 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 50.22/6.77 fof(f198,plain,(
% 50.22/6.77 ![X0]: (~aScalar0(X0)|~sQ0_spl)),
% 50.22/6.77 inference(component_clause,[status(thm)],[f197])).
% 50.22/6.77 fof(f204,definition,(
% 50.22/6.77 ![X0,X1]: (sQ2_spl <=> (~aScalar0(X0)|~aScalar0(X1)|sdtpldt0(X0,X1)=sdtpldt0(X1,X0)))),
% 50.22/6.77 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 50.22/6.77 fof(f205,plain,(
% 50.22/6.77 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|sdtpldt0(X0,X1)=sdtpldt0(X1,X0)|~sQ2_spl)),
% 50.22/6.77 inference(component_clause,[status(thm)],[f204])).
% 50.22/6.77 fof(f207,plain,(
% 50.22/6.77 sQ2_spl|sQ0_spl),
% 50.22/6.77 inference(split_clause,[status(thm)],[f99,f204,f197])).
% 50.22/6.77 fof(f208,definition,(
% 50.22/6.77 ![X0,X1]: (sQ3_spl <=> (~aScalar0(X0)|~aScalar0(X1)|sdtasdt0(X0,X1)=sdtasdt0(X1,X0)))),
% 50.22/6.77 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 50.22/6.77 fof(f209,plain,(
% 50.22/6.77 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|sdtasdt0(X0,X1)=sdtasdt0(X1,X0)|~sQ3_spl)),
% 50.22/6.77 inference(component_clause,[status(thm)],[f208])).
% 50.22/6.77 fof(f211,plain,(
% 50.22/6.77 sQ3_spl|sQ0_spl),
% 50.22/6.77 inference(split_clause,[status(thm)],[f101,f208,f197])).
% 50.22/6.77 fof(f218,plain,(
% 50.22/6.77 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|sdtasdt0(sdtpldt0(X0,xE),X1)=sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(xE,X1)))),
% 50.22/6.77 inference(resolution,[status(thm)],[f177,f104])).
% 50.22/6.77 fof(f220,plain,(
% 50.22/6.77 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|sdtasdt0(X0,sdtpldt0(X1,xE))=sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,xE)))),
% 50.22/6.77 inference(resolution,[status(thm)],[f177,f103])).
% 50.22/6.77 fof(f222,plain,(
% 50.22/6.77 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|sdtasdt0(X0,sdtpldt0(xE,X1))=sdtpldt0(sdtasdt0(X0,xE),sdtasdt0(X0,X1)))),
% 50.22/6.77 inference(resolution,[status(thm)],[f177,f103])).
% 50.22/6.77 fof(f230,plain,(
% 50.22/6.77 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|sdtpldt0(sdtpldt0(X0,xE),X1)=sdtpldt0(X0,sdtpldt0(xE,X1)))),
% 50.22/6.77 inference(resolution,[status(thm)],[f177,f98])).
% 50.22/6.77 fof(f231,plain,(
% 50.22/6.77 ![X0]: (~aScalar0(X0)|aScalar0(sdtasdt0(xE,X0)))),
% 50.22/6.77 inference(resolution,[status(thm)],[f177,f85])).
% 50.22/6.77 fof(f232,plain,(
% 50.22/6.77 ![X0]: (~aScalar0(X0)|aScalar0(sdtpldt0(xE,X0)))),
% 50.22/6.77 inference(resolution,[status(thm)],[f177,f83])).
% 50.22/6.77 fof(f233,plain,(
% 50.22/6.77 ![X0]: (~aScalar0(X0)|sdtasdt0(sdtpldt0(X0,xH),xH)=sdtpldt0(sdtasdt0(X0,xH),sdtasdt0(xH,xH)))),
% 50.22/6.77 inference(resolution,[status(thm)],[f183,f104])).
% 50.22/6.77 fof(f234,plain,(
% 50.22/6.77 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|sdtasdt0(sdtpldt0(X0,X1),xH)=sdtpldt0(sdtasdt0(X0,xH),sdtasdt0(X1,xH)))),
% 50.22/6.77 inference(resolution,[status(thm)],[f183,f104])).
% 50.22/6.77 fof(f269,plain,(
% 50.22/6.77 ~sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH))=sdtpldt0(xP,sdtpldt0(sdtasdt0(xH,xE),sdtasdt0(xH,xH)))),
% 50.22/6.77 inference(backward_demodulation,[status(thm)],[f188,f196])).
% 50.22/6.77 fof(f309,plain,(
% 50.22/6.77 sdtlseqdt0(xP,xP)),
% 50.22/6.77 inference(resolution,[status(thm)],[f115,f187])).
% 50.22/6.77 fof(f310,plain,(
% 50.22/6.77 sdtlseqdt0(xH,xH)),
% 50.22/6.77 inference(resolution,[status(thm)],[f115,f183])).
% 50.22/6.77 fof(f311,plain,(
% 50.22/6.77 sdtlseqdt0(xE,xE)),
% 50.22/6.77 inference(resolution,[status(thm)],[f115,f177])).
% 50.22/6.77 fof(f314,plain,(
% 50.22/6.77 ![X0]: (~aScalar0(X0)|sdtasdt0(sdtpldt0(X0,xE),xH)=sdtpldt0(sdtasdt0(X0,xH),sdtasdt0(xE,xH)))),
% 50.22/6.77 inference(resolution,[status(thm)],[f218,f183])).
% 50.22/6.77 fof(f316,plain,(
% 50.22/6.77 ![X0]: (~aScalar0(X0)|sdtasdt0(sdtpldt0(X0,xE),xH)=sdtpldt0(sdtasdt0(X0,xH),xP))),
% 50.22/6.77 inference(forward_demodulation,[status(thm)],[f188,f314])).
% 50.22/6.77 fof(f321,plain,(
% 50.22/6.77 ![X0]: (~aScalar0(X0)|sdtasdt0(X0,sdtpldt0(xH,xE))=sdtpldt0(sdtasdt0(X0,xH),sdtasdt0(X0,xE)))),
% 50.22/6.77 inference(resolution,[status(thm)],[f220,f183])).
% 50.22/6.77 fof(f324,plain,(
% 50.22/6.77 ![X0]: (~aScalar0(X0)|sdtasdt0(X0,sdtpldt0(xE,xH))=sdtpldt0(sdtasdt0(X0,xE),sdtasdt0(X0,xH)))),
% 50.22/6.77 inference(resolution,[status(thm)],[f222,f183])).
% 50.22/6.77 fof(f343,plain,(
% 50.22/6.77 ![X0]: (~aScalar0(X0)|sdtpldt0(sdtpldt0(X0,xE),xH)=sdtpldt0(X0,sdtpldt0(xE,xH)))),
% 50.22/6.77 inference(resolution,[status(thm)],[f230,f183])).
% 50.22/6.77 fof(f345,plain,(
% 50.22/6.77 aScalar0(sdtasdt0(xE,xP))),
% 50.22/6.77 inference(resolution,[status(thm)],[f231,f187])).
% 50.22/6.77 fof(f349,plain,(
% 50.22/6.77 $false|~sQ0_spl),
% 50.22/6.77 inference(backward_subsumption_resolution,[status(thm)],[f187,f198])).
% 50.22/6.77 fof(f352,plain,(
% 50.22/6.77 ~sQ0_spl),
% 50.22/6.77 inference(contradiction_clause,[status(thm)],[f349])).
% 50.22/6.77 fof(f602,plain,(
% 50.22/6.77 sdtasdt0(xH,sdtpldt0(xE,xH))=sdtpldt0(sdtasdt0(xH,xE),sdtasdt0(xH,xH))),
% 50.22/6.77 inference(resolution,[status(thm)],[f183,f324])).
% 50.22/6.77 fof(f604,plain,(
% 50.22/6.77 sdtasdt0(xH,sdtpldt0(xH,xE))=sdtpldt0(sdtasdt0(xH,xH),sdtasdt0(xH,xE))),
% 50.22/6.77 inference(resolution,[status(thm)],[f183,f321])).
% 50.22/6.77 fof(f606,plain,(
% 50.22/6.77 sdtasdt0(sdtpldt0(xH,xE),xH)=sdtpldt0(sdtasdt0(xH,xH),xP)),
% 50.22/6.77 inference(resolution,[status(thm)],[f183,f316])).
% 50.22/6.77 fof(f636,plain,(
% 50.22/6.77 ![X0]: (~aScalar0(X0)|sdtasdt0(X0,xH)=sdtasdt0(xH,X0)|~sQ3_spl)),
% 50.22/6.77 inference(resolution,[status(thm)],[f183,f209])).
% 50.22/6.77 fof(f643,plain,(
% 50.22/6.77 ![X0]: (~aScalar0(X0)|sdtpldt0(X0,xH)=sdtpldt0(xH,X0)|~sQ2_spl)),
% 50.22/6.77 inference(resolution,[status(thm)],[f183,f205])).
% 50.22/6.77 fof(f671,plain,(
% 50.22/6.77 sdtpldt0(sdtpldt0(xE,xE),xH)=sdtpldt0(xE,sdtpldt0(xE,xH))),
% 50.22/6.77 inference(resolution,[status(thm)],[f177,f343])).
% 50.22/6.77 fof(f692,plain,(
% 50.22/6.77 sdtasdt0(sdtpldt0(xE,xE),xH)=sdtpldt0(sdtasdt0(xE,xH),xP)),
% 50.22/6.77 inference(resolution,[status(thm)],[f177,f316])).
% 50.22/6.77 fof(f740,plain,(
% 50.22/6.77 sdtasdt0(sdtpldt0(xE,xH),xH)=sdtpldt0(sdtasdt0(xE,xH),sdtasdt0(xH,xH))),
% 50.22/6.77 inference(resolution,[status(thm)],[f177,f233])).
% 50.22/6.77 fof(f745,plain,(
% 50.22/6.77 sdtasdt0(sdtpldt0(xE,xE),xH)=sdtpldt0(xP,xP)),
% 50.22/6.77 inference(forward_demodulation,[status(thm)],[f188,f692])).
% 50.22/6.77 fof(f754,plain,(
% 50.22/6.77 sdtasdt0(sdtpldt0(xE,xH),xH)=sdtpldt0(xP,sdtasdt0(xH,xH))),
% 50.22/6.77 inference(forward_demodulation,[status(thm)],[f188,f740])).
% 50.22/6.77 fof(f755,plain,(
% 50.22/6.77 aScalar0(sdtpldt0(xE,xE))),
% 50.22/6.77 inference(resolution,[status(thm)],[f232,f177])).
% 50.22/6.77 fof(f756,plain,(
% 50.22/6.77 aScalar0(sdtpldt0(xE,xH))),
% 50.22/6.77 inference(resolution,[status(thm)],[f232,f183])).
% 50.22/6.77 fof(f802,plain,(
% 50.22/6.77 ![X0]: (~aScalar0(X0)|sdtlseqdt0(sz0z00,X0)|sdtlseqdt0(X0,sz0z00))),
% 50.22/6.77 inference(resolution,[status(thm)],[f125,f81])).
% 50.22/6.77 fof(f922,plain,(
% 50.22/6.77 ~sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH))=sdtpldt0(xP,sdtasdt0(xH,sdtpldt0(xE,xH)))),
% 50.22/6.77 inference(backward_demodulation,[status(thm)],[f602,f269])).
% 50.22/6.77 fof(f928,definition,(
% 50.22/6.77 sQ7_spl <=> (aScalar0(xB))),
% 50.22/6.77 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 50.22/6.77 fof(f930,plain,(
% 50.22/6.77 ~aScalar0(xB)|sQ7_spl),
% 50.22/6.77 inference(component_clause,[status(thm)],[f928])).
% 50.22/6.77 fof(f938,definition,(
% 50.22/6.77 sQ10_spl <=> (aScalar0(xA))),
% 50.22/6.77 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 50.22/6.77 fof(f940,plain,(
% 50.22/6.77 ~aScalar0(xA)|sQ10_spl),
% 50.22/6.77 inference(component_clause,[status(thm)],[f938])).
% 50.22/6.77 fof(f967,plain,(
% 50.22/6.77 sdtasdt0(xE,xH)=sdtasdt0(xH,xE)|~sQ3_spl),
% 50.22/6.77 inference(resolution,[status(thm)],[f636,f177])).
% 50.22/6.77 fof(f971,plain,(
% 50.22/6.77 xP=sdtasdt0(xH,xE)|~sQ3_spl),
% 50.22/6.77 inference(forward_demodulation,[status(thm)],[f188,f967])).
% 50.22/6.77 fof(f1005,plain,(
% 50.22/6.77 sdtpldt0(xE,xH)=sdtpldt0(xH,xE)|~sQ2_spl),
% 50.22/6.77 inference(resolution,[status(thm)],[f643,f177])).
% 50.22/6.77 fof(f1175,definition,(
% 50.22/6.77 sQ14_spl <=> (aScalar0(sz0z00))),
% 50.22/6.77 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 50.22/6.77 fof(f1177,plain,(
% 50.22/6.77 ~aScalar0(sz0z00)|sQ14_spl),
% 50.22/6.77 inference(component_clause,[status(thm)],[f1175])).
% 50.22/6.77 fof(f1178,definition,(
% 50.22/6.77 sQ15_spl <=> (sdtlseqdt0(sz0z00,sz0z00))),
% 50.22/6.77 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 50.22/6.77 fof(f1183,plain,(
% 50.22/6.77 $false|sQ14_spl),
% 50.22/6.77 inference(forward_subsumption_resolution,[status(thm)],[f1177,f81])).
% 50.22/6.77 fof(f1184,plain,(
% 50.22/6.77 sQ14_spl),
% 50.22/6.77 inference(contradiction_clause,[status(thm)],[f1183])).
% 50.22/6.77 fof(f1286,plain,(
% 50.22/6.77 sdtasdt0(xH,sdtpldt0(xH,xE))=sdtpldt0(sdtasdt0(xH,xH),xP)|~sQ3_spl),
% 50.22/6.77 inference(backward_demodulation,[status(thm)],[f971,f604])).
% 50.22/6.77 fof(f1394,plain,(
% 50.22/6.77 sdtasdt0(sdtpldt0(xE,xH),xH)=sdtpldt0(sdtasdt0(xH,xH),xP)|~sQ2_spl),
% 50.22/6.77 inference(backward_demodulation,[status(thm)],[f1005,f606])).
% 50.22/6.77 fof(f1403,plain,(
% 50.22/6.77 sdtpldt0(xP,sdtasdt0(xH,xH))=sdtpldt0(sdtasdt0(xH,xH),xP)|~sQ2_spl),
% 50.22/6.77 inference(forward_demodulation,[status(thm)],[f754,f1394])).
% 50.22/6.77 fof(f1437,definition,(
% 50.22/6.77 sQ30_spl <=> (aVector0(xs))),
% 50.22/6.77 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 50.22/6.77 fof(f1439,plain,(
% 50.22/6.77 ~aVector0(xs)|sQ30_spl),
% 50.22/6.77 inference(component_clause,[status(thm)],[f1437])).
% 50.22/6.77 fof(f1440,definition,(
% 50.22/6.77 sQ31_spl <=> (aVector0(xt))),
% 50.22/6.77 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 50.22/6.77 fof(f1442,plain,(
% 50.22/6.77 ~aVector0(xt)|sQ31_spl),
% 50.22/6.77 inference(component_clause,[status(thm)],[f1440])).
% 50.22/6.77 fof(f1485,plain,(
% 50.22/6.77 $false|sQ31_spl),
% 50.22/6.77 inference(forward_subsumption_resolution,[status(thm)],[f1442,f160])).
% 50.22/6.77 fof(f1486,plain,(
% 50.22/6.77 sQ31_spl),
% 50.22/6.77 inference(contradiction_clause,[status(thm)],[f1485])).
% 50.22/6.77 fof(f1487,plain,(
% 50.22/6.77 $false|sQ30_spl),
% 50.22/6.77 inference(forward_subsumption_resolution,[status(thm)],[f1439,f159])).
% 50.22/6.77 fof(f1488,plain,(
% 50.22/6.77 sQ30_spl),
% 50.22/6.77 inference(contradiction_clause,[status(thm)],[f1487])).
% 50.22/6.77 fof(f1656,definition,(
% 50.22/6.77 sQ57_spl <=> (aScalar0(xP))),
% 50.22/6.77 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 50.22/6.77 fof(f1658,plain,(
% 50.22/6.77 ~aScalar0(xP)|sQ57_spl),
% 50.22/6.77 inference(component_clause,[status(thm)],[f1656])).
% 50.22/6.77 fof(f1671,definition,(
% 50.22/6.77 sQ61_spl <=> (sdtlseqdt0(xP,xP))),
% 50.22/6.77 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 50.22/6.77 fof(f1673,plain,(
% 50.22/6.77 ~sdtlseqdt0(xP,xP)|sQ61_spl),
% 50.22/6.77 inference(component_clause,[status(thm)],[f1671])).
% 50.22/6.77 fof(f1678,plain,(
% 50.22/6.77 $false|sQ57_spl),
% 50.22/6.77 inference(forward_subsumption_resolution,[status(thm)],[f1658,f187])).
% 50.22/6.77 fof(f1679,plain,(
% 50.22/6.77 sQ57_spl),
% 50.22/6.77 inference(contradiction_clause,[status(thm)],[f1678])).
% 50.22/6.77 fof(f1680,plain,(
% 50.22/6.77 $false|sQ61_spl),
% 50.22/6.77 inference(forward_subsumption_resolution,[status(thm)],[f1673,f309])).
% 50.22/6.77 fof(f1681,plain,(
% 50.22/6.77 sQ61_spl),
% 50.22/6.77 inference(contradiction_clause,[status(thm)],[f1680])).
% 50.22/6.77 fof(f1711,plain,(
% 50.22/6.77 ~sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH))=sdtpldt0(xP,sdtpldt0(sdtasdt0(xH,xH),xP))|~sQ2_spl|~sQ3_spl),
% 50.22/6.77 inference(backward_demodulation,[status(thm)],[f1712,f922])).
% 50.22/6.77 fof(f1712,plain,(
% 50.22/6.77 sdtasdt0(xH,sdtpldt0(xE,xH))=sdtpldt0(sdtasdt0(xH,xH),xP)|~sQ2_spl|~sQ3_spl),
% 50.22/6.77 inference(forward_demodulation,[status(thm)],[f1005,f1286])).
% 50.22/6.77 fof(f1718,definition,(
% 50.22/6.77 sQ63_spl <=> (aScalar0(xH))),
% 50.22/6.77 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 50.22/6.77 fof(f1720,plain,(
% 50.22/6.77 ~aScalar0(xH)|sQ63_spl),
% 50.22/6.77 inference(component_clause,[status(thm)],[f1718])).
% 50.22/6.77 fof(f1733,definition,(
% 50.22/6.77 sQ67_spl <=> (sdtlseqdt0(xH,xH))),
% 50.22/6.77 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 50.22/6.77 fof(f1735,plain,(
% 50.22/6.77 ~sdtlseqdt0(xH,xH)|sQ67_spl),
% 50.22/6.77 inference(component_clause,[status(thm)],[f1733])).
% 50.22/6.77 fof(f1740,plain,(
% 50.22/6.77 $false|sQ63_spl),
% 50.22/6.77 inference(forward_subsumption_resolution,[status(thm)],[f1720,f183])).
% 50.22/6.77 fof(f1741,plain,(
% 50.22/6.77 sQ63_spl),
% 50.22/6.77 inference(contradiction_clause,[status(thm)],[f1740])).
% 50.22/6.77 fof(f1742,plain,(
% 50.22/6.77 $false|sQ67_spl),
% 50.22/6.77 inference(forward_subsumption_resolution,[status(thm)],[f1735,f310])).
% 50.22/6.77 fof(f1743,plain,(
% 50.22/6.77 sQ67_spl),
% 50.22/6.77 inference(contradiction_clause,[status(thm)],[f1742])).
% 50.22/6.77 fof(f1836,plain,(
% 50.22/6.77 ![X0]: (~aScalar0(X0)|sdtlseqdt0(xA,X0)|sdtlseqdt0(X0,xA))),
% 50.22/6.77 inference(resolution,[status(thm)],[f169,f125])).
% 50.22/6.77 fof(f1947,plain,(
% 50.22/6.77 ~sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH))=sdtpldt0(xP,sdtpldt0(xP,sdtasdt0(xH,xH)))|~sQ2_spl|~sQ3_spl),
% 50.22/6.77 inference(backward_demodulation,[status(thm)],[f1403,f1711])).
% 50.22/6.77 fof(f1977,definition,(
% 50.22/6.77 sQ69_spl <=> (aScalar0(xE))),
% 50.22/6.77 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 50.22/6.77 fof(f1979,plain,(
% 50.22/6.77 ~aScalar0(xE)|sQ69_spl),
% 50.22/6.77 inference(component_clause,[status(thm)],[f1977])).
% 50.22/6.77 fof(f1992,definition,(
% 50.22/6.77 sQ73_spl <=> (sdtlseqdt0(xE,xE))),
% 50.22/6.77 introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 50.22/6.77 fof(f1994,plain,(
% 50.22/6.77 ~sdtlseqdt0(xE,xE)|sQ73_spl),
% 50.22/6.77 inference(component_clause,[status(thm)],[f1992])).
% 50.22/6.77 fof(f1999,plain,(
% 50.22/6.77 $false|sQ69_spl),
% 50.22/6.77 inference(forward_subsumption_resolution,[status(thm)],[f1979,f177])).
% 50.22/6.77 fof(f2000,plain,(
% 50.22/6.77 sQ69_spl),
% 50.22/6.77 inference(contradiction_clause,[status(thm)],[f1999])).
% 50.22/6.77 fof(f2001,plain,(
% 50.22/6.77 $false|sQ73_spl),
% 50.22/6.77 inference(forward_subsumption_resolution,[status(thm)],[f1994,f311])).
% 50.22/6.77 fof(f2002,plain,(
% 50.22/6.77 sQ73_spl),
% 50.22/6.77 inference(contradiction_clause,[status(thm)],[f2001])).
% 50.22/6.77 fof(f2081,plain,(
% 50.22/6.77 ![X0]: (~aScalar0(X0)|sdtlseqdt0(xB,X0)|sdtlseqdt0(X0,xB))),
% 50.22/6.77 inference(resolution,[status(thm)],[f171,f125])).
% 50.22/6.77 fof(f2262,plain,(
% 50.22/6.77 ![X0]: (~aScalar0(X0)|sdtlseqdt0(xC,X0)|sdtlseqdt0(X0,xC))),
% 50.22/6.77 inference(resolution,[status(thm)],[f173,f125])).
% 50.22/6.77 fof(f4654,definition,(
% 50.22/6.77 sQ100_spl <=> (aScalar0(sdtasdt0(xE,xP)))),
% 50.22/6.77 introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition])).
% 50.22/6.77 fof(f4656,plain,(
% 50.22/6.77 ~aScalar0(sdtasdt0(xE,xP))|sQ100_spl),
% 50.22/6.77 inference(component_clause,[status(thm)],[f4654])).
% 50.22/6.77 fof(f4662,plain,(
% 50.22/6.77 $false|sQ100_spl),
% 50.22/6.77 inference(forward_subsumption_resolution,[status(thm)],[f4656,f345])).
% 50.22/6.77 fof(f4663,plain,(
% 50.22/6.77 sQ100_spl),
% 50.22/6.77 inference(contradiction_clause,[status(thm)],[f4662])).
% 50.22/6.77 fof(f8207,plain,(
% 50.22/6.77 sdtlseqdt0(sz0z00,sz0z00)|sdtlseqdt0(sz0z00,sz0z00)),
% 50.22/6.77 inference(resolution,[status(thm)],[f802,f81])).
% 50.22/6.77 fof(f8293,plain,(
% 50.22/6.77 sQ15_spl),
% 50.22/6.77 inference(split_clause,[status(thm)],[f8207,f1178])).
% 50.22/6.77 fof(f8321,plain,(
% 50.22/6.77 $false|sQ7_spl),
% 50.22/6.77 inference(forward_subsumption_resolution,[status(thm)],[f930,f171])).
% 50.22/6.77 fof(f8322,plain,(
% 50.22/6.77 sQ7_spl),
% 50.22/6.77 inference(contradiction_clause,[status(thm)],[f8321])).
% 50.22/6.77 fof(f8361,plain,(
% 50.22/6.77 $false|sQ10_spl),
% 50.22/6.77 inference(forward_subsumption_resolution,[status(thm)],[f940,f169])).
% 50.22/6.77 fof(f8362,plain,(
% 50.22/6.77 sQ10_spl),
% 50.22/6.77 inference(contradiction_clause,[status(thm)],[f8361])).
% 50.22/6.77 fof(f8834,definition,(
% 50.22/6.77 sQ277_spl <=> (aDimensionOf0(xt)=aDimensionOf0(xs))),
% 50.22/6.77 introduced(definition,[new_symbols(definition,[sQ277_spl])],[split_symbol_definition])).
% 50.22/6.77 fof(f8836,plain,(
% 50.22/6.77 ~aDimensionOf0(xt)=aDimensionOf0(xs)|sQ277_spl),
% 50.22/6.77 inference(component_clause,[status(thm)],[f8834])).
% 50.22/6.77 fof(f8841,definition,(
% 50.22/6.77 sQ279_spl <=> (aDimensionOf0(xs)=aDimensionOf0(xs))),
% 50.22/6.77 introduced(definition,[new_symbols(definition,[sQ279_spl])],[split_symbol_definition])).
% 50.22/6.77 fof(f8843,plain,(
% 50.22/6.77 ~aDimensionOf0(xs)=aDimensionOf0(xs)|sQ279_spl),
% 50.22/6.77 inference(component_clause,[status(thm)],[f8841])).
% 50.22/6.77 fof(f8845,plain,(
% 50.22/6.77 ~aDimensionOf0(xs)=aDimensionOf0(xs)|sQ277_spl),
% 50.22/6.77 inference(forward_demodulation,[status(thm)],[f163,f8836])).
% 50.22/6.77 fof(f8846,plain,(
% 50.22/6.77 $false|sQ277_spl),
% 50.22/6.77 inference(trivial_equality_resolution,[status(thm)],[f8845])).
% 50.22/6.77 fof(f8847,plain,(
% 50.22/6.77 sQ277_spl),
% 50.22/6.77 inference(contradiction_clause,[status(thm)],[f8846])).
% 50.22/6.77 fof(f8848,plain,(
% 50.22/6.77 $false|sQ279_spl),
% 50.22/6.77 inference(trivial_equality_resolution,[status(thm)],[f8843])).
% 50.22/6.77 fof(f8849,plain,(
% 50.22/6.77 sQ279_spl),
% 50.22/6.77 inference(contradiction_clause,[status(thm)],[f8848])).
% 50.22/6.77 fof(f10133,definition,(
% 50.22/6.77 sQ308_spl <=> (aScalar0(xC))),
% 50.22/6.77 introduced(definition,[new_symbols(definition,[sQ308_spl])],[split_symbol_definition])).
% 50.22/6.77 fof(f10135,plain,(
% 50.22/6.77 ~aScalar0(xC)|sQ308_spl),
% 50.22/6.77 inference(component_clause,[status(thm)],[f10133])).
% 50.22/6.77 fof(f10160,plain,(
% 50.22/6.77 $false|sQ308_spl),
% 50.22/6.77 inference(forward_subsumption_resolution,[status(thm)],[f10135,f173])).
% 50.22/6.77 fof(f10161,plain,(
% 50.22/6.77 sQ308_spl),
% 50.22/6.77 inference(contradiction_clause,[status(thm)],[f10160])).
% 50.22/6.77 fof(f10381,definition,(
% 50.22/6.77 sQ319_spl <=> (aDimensionOf0(xp)=aDimensionOf0(xp))),
% 50.22/6.77 introduced(definition,[new_symbols(definition,[sQ319_spl])],[split_symbol_definition])).
% 50.22/6.77 fof(f10383,plain,(
% 50.22/6.77 ~aDimensionOf0(xp)=aDimensionOf0(xp)|sQ319_spl),
% 50.22/6.77 inference(component_clause,[status(thm)],[f10381])).
% 50.22/6.77 fof(f10399,plain,(
% 50.22/6.77 $false|sQ319_spl),
% 50.22/6.77 inference(trivial_equality_resolution,[status(thm)],[f10383])).
% 50.22/6.77 fof(f10400,plain,(
% 50.22/6.77 sQ319_spl),
% 50.22/6.77 inference(contradiction_clause,[status(thm)],[f10399])).
% 50.22/6.77 fof(f10487,definition,(
% 50.22/6.77 sQ324_spl <=> (aScalar0(xD))),
% 50.22/6.77 introduced(definition,[new_symbols(definition,[sQ324_spl])],[split_symbol_definition])).
% 50.22/6.77 fof(f10489,plain,(
% 50.22/6.77 ~aScalar0(xD)|sQ324_spl),
% 50.22/6.77 inference(component_clause,[status(thm)],[f10487])).
% 50.22/6.77 fof(f10514,plain,(
% 50.22/6.77 $false|sQ324_spl),
% 50.22/6.77 inference(forward_subsumption_resolution,[status(thm)],[f10489,f175])).
% 50.22/6.77 fof(f10515,plain,(
% 50.22/6.77 sQ324_spl),
% 50.22/6.77 inference(contradiction_clause,[status(thm)],[f10514])).
% 50.22/6.77 fof(f10593,definition,(
% 50.22/6.77 sQ333_spl <=> (aDimensionOf0(xq)=aDimensionOf0(xq))),
% 50.22/6.77 introduced(definition,[new_symbols(definition,[sQ333_spl])],[split_symbol_definition])).
% 50.22/6.77 fof(f10595,plain,(
% 50.22/6.77 ~aDimensionOf0(xq)=aDimensionOf0(xq)|sQ333_spl),
% 50.22/6.77 inference(component_clause,[status(thm)],[f10593])).
% 50.22/6.77 fof(f10615,plain,(
% 50.22/6.77 $false|sQ333_spl),
% 50.22/6.77 inference(trivial_equality_resolution,[status(thm)],[f10595])).
% 50.22/6.77 fof(f10616,plain,(
% 50.22/6.77 sQ333_spl),
% 50.22/6.77 inference(contradiction_clause,[status(thm)],[f10615])).
% 50.22/6.77 fof(f10624,definition,(
% 50.22/6.77 sQ339_spl <=> (aScalar0(xF))),
% 50.22/6.77 introduced(definition,[new_symbols(definition,[sQ339_spl])],[split_symbol_definition])).
% 50.22/6.77 fof(f10626,plain,(
% 50.22/6.77 ~aScalar0(xF)|sQ339_spl),
% 50.22/6.77 inference(component_clause,[status(thm)],[f10624])).
% 50.22/6.77 fof(f10648,plain,(
% 50.22/6.77 $false|sQ339_spl),
% 50.22/6.77 inference(forward_subsumption_resolution,[status(thm)],[f10626,f179])).
% 50.22/6.77 fof(f10649,plain,(
% 50.22/6.77 sQ339_spl),
% 50.22/6.77 inference(contradiction_clause,[status(thm)],[f10648])).
% 50.22/6.77 fof(f10664,plain,(
% 50.22/6.77 sdtlseqdt0(xA,xA)|sdtlseqdt0(xA,xA)),
% 50.22/6.77 inference(resolution,[status(thm)],[f1836,f169])).
% 50.22/6.77 fof(f10767,definition,(
% 50.22/6.77 sQ373_spl <=> (sdtlseqdt0(xA,xA))),
% 50.22/6.77 introduced(definition,[new_symbols(definition,[sQ373_spl])],[split_symbol_definition])).
% 50.22/6.77 fof(f10770,plain,(
% 50.22/6.80 sQ373_spl),
% 50.22/6.80 inference(split_clause,[status(thm)],[f10664,f10767])).
% 50.22/6.80 fof(f11966,plain,(
% 50.22/6.80 sdtasdt0(sdtpldt0(sdtpldt0(xE,xE),xH),xH)=sdtpldt0(sdtasdt0(sdtpldt0(xE,xE),xH),sdtasdt0(xH,xH))),
% 50.22/6.80 inference(resolution,[status(thm)],[f755,f233])).
% 50.22/6.80 fof(f12284,plain,(
% 50.22/6.80 sdtasdt0(sdtpldt0(xE,sdtpldt0(xE,xH)),xH)=sdtpldt0(sdtasdt0(sdtpldt0(xE,xE),xH),sdtasdt0(xH,xH))),
% 50.22/6.80 inference(forward_demodulation,[status(thm)],[f671,f11966])).
% 50.22/6.80 fof(f12285,plain,(
% 50.22/6.80 sdtasdt0(sdtpldt0(xE,sdtpldt0(xE,xH)),xH)=sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH))),
% 50.22/6.80 inference(forward_demodulation,[status(thm)],[f745,f12284])).
% 50.22/6.80 fof(f12947,definition,(
% 50.22/6.80 sQ397_spl <=> (aScalar0(xG))),
% 50.22/6.80 introduced(definition,[new_symbols(definition,[sQ397_spl])],[split_symbol_definition])).
% 50.22/6.80 fof(f12949,plain,(
% 50.22/6.80 ~aScalar0(xG)|sQ397_spl),
% 50.22/6.80 inference(component_clause,[status(thm)],[f12947])).
% 50.22/6.80 fof(f12974,plain,(
% 50.22/6.80 $false|sQ397_spl),
% 50.22/6.80 inference(forward_subsumption_resolution,[status(thm)],[f12949,f181])).
% 50.22/6.80 fof(f12975,plain,(
% 50.22/6.80 sQ397_spl),
% 50.22/6.80 inference(contradiction_clause,[status(thm)],[f12974])).
% 50.22/6.80 fof(f13045,plain,(
% 50.22/6.80 sdtlseqdt0(xB,xB)|sdtlseqdt0(xB,xB)),
% 50.22/6.80 inference(resolution,[status(thm)],[f2081,f171])).
% 50.22/6.80 fof(f13156,definition,(
% 50.22/6.80 sQ434_spl <=> (sdtlseqdt0(xB,xB))),
% 50.22/6.80 introduced(definition,[new_symbols(definition,[sQ434_spl])],[split_symbol_definition])).
% 50.22/6.80 fof(f13159,plain,(
% 50.22/6.80 sQ434_spl),
% 50.22/6.80 inference(split_clause,[status(thm)],[f13045,f13156])).
% 50.22/6.80 fof(f14590,plain,(
% 50.22/6.80 sdtlseqdt0(xC,xC)|sdtlseqdt0(xC,xC)),
% 50.22/6.80 inference(resolution,[status(thm)],[f2262,f173])).
% 50.22/6.80 fof(f14702,definition,(
% 50.22/6.80 sQ489_spl <=> (sdtlseqdt0(xC,xC))),
% 50.22/6.80 introduced(definition,[new_symbols(definition,[sQ489_spl])],[split_symbol_definition])).
% 50.22/6.80 fof(f14705,plain,(
% 50.22/6.80 sQ489_spl),
% 50.22/6.80 inference(split_clause,[status(thm)],[f14590,f14702])).
% 50.22/6.80 fof(f15345,plain,(
% 50.22/6.80 ![X0]: (~aScalar0(X0)|sdtasdt0(sdtpldt0(X0,sdtpldt0(xE,xH)),xH)=sdtpldt0(sdtasdt0(X0,xH),sdtasdt0(sdtpldt0(xE,xH),xH)))),
% 50.22/6.80 inference(resolution,[status(thm)],[f756,f234])).
% 50.22/6.80 fof(f15730,plain,(
% 50.22/6.80 ![X0]: (~aScalar0(X0)|sdtasdt0(sdtpldt0(X0,sdtpldt0(xE,xH)),xH)=sdtpldt0(sdtasdt0(X0,xH),sdtpldt0(xP,sdtasdt0(xH,xH))))),
% 50.22/6.80 inference(forward_demodulation,[status(thm)],[f754,f15345])).
% 50.22/6.80 fof(f17275,plain,(
% 50.22/6.80 sdtasdt0(sdtpldt0(xE,sdtpldt0(xE,xH)),xH)=sdtpldt0(sdtasdt0(xE,xH),sdtpldt0(xP,sdtasdt0(xH,xH)))),
% 50.22/6.80 inference(resolution,[status(thm)],[f15730,f177])).
% 50.22/6.80 fof(f17289,plain,(
% 50.22/6.80 sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH))=sdtpldt0(sdtasdt0(xE,xH),sdtpldt0(xP,sdtasdt0(xH,xH)))),
% 50.22/6.80 inference(forward_demodulation,[status(thm)],[f12285,f17275])).
% 50.22/6.80 fof(f17290,plain,(
% 50.22/6.80 sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH))=sdtpldt0(xP,sdtpldt0(xP,sdtasdt0(xH,xH)))),
% 50.22/6.80 inference(forward_demodulation,[status(thm)],[f188,f17289])).
% 50.22/6.80 fof(f17291,plain,(
% 50.22/6.80 $false|~sQ2_spl|~sQ3_spl),
% 50.22/6.80 inference(forward_subsumption_resolution,[status(thm)],[f17290,f1947])).
% 50.22/6.80 fof(f17292,plain,(
% 50.22/6.80 ~sQ2_spl|~sQ3_spl),
% 50.22/6.80 inference(contradiction_clause,[status(thm)],[f17291])).
% 50.22/6.80 fof(f17293,plain,(
% 50.22/6.80 $false),
% 50.22/6.80 inference(sat_refutation,[status(thm)],[f207,f211,f352,f1184,f1486,f1488,f1679,f1681,f1741,f1743,f2000,f2002,f4663,f8293,f8322,f8362,f8847,f8849,f10161,f10400,f10515,f10616,f10649,f10770,f12975,f13159,f14705,f17292])).
% 50.22/6.80 % SZS output end CNFRefutation for theBenchmark.p
% 17.58/6.83 % Elapsed time: 6.453074 seconds
% 17.58/6.83 % CPU time: 50.812660 seconds
% 17.58/6.83 % Total memory used: 613.376 MB
% 17.58/6.83 % Net memory used: 566.645 MB
%------------------------------------------------------------------------------