%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : RNG090+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 : n018.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:19 PM UTC 2026
% Result : Theorem 35.16s 4.93s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : RNG090+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n018.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Mon Sep 21 04:21:13 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.18/0.47 % Drodi V4.1.1
% 35.16/4.93 % Refutation found
% 35.16/4.93 % SZS status Theorem for theBenchmark: Theorem is valid
% 35.16/4.93 % SZS output start CNFRefutation for theBenchmark
% 35.16/4.93 fof(f2,axiom,(
% 35.16/4.93 aElement0(sz00) ),
% 35.16/4.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.16/4.93 fof(f3,axiom,(
% 35.16/4.93 aElement0(sz10) ),
% 35.16/4.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.16/4.93 fof(f4,axiom,(
% 35.16/4.93 (! [W0] :( aElement0(W0)=> aElement0(smndt0(W0)) ) )),
% 35.16/4.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.16/4.93 fof(f5,axiom,(
% 35.16/4.93 (! [W0,W1] :( ( aElement0(W0)& aElement0(W1) )=> aElement0(sdtpldt0(W0,W1)) ) )),
% 35.16/4.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.16/4.93 fof(f7,axiom,(
% 35.16/4.93 (! [W0,W1] :( ( aElement0(W0)& aElement0(W1) )=> sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) )),
% 35.16/4.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.16/4.93 fof(f8,axiom,(
% 35.16/4.93 (! [W0,W1,W2] :( ( aElement0(W0)& aElement0(W1)& aElement0(W2) )=> sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2)) ) )),
% 35.16/4.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.16/4.93 fof(f18,axiom,(
% 35.16/4.93 sz10 != sz00 ),
% 35.16/4.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.16/4.93 fof(f20,axiom,(
% 35.16/4.93 (! [W0] :( aSet0(W0)=> (! [W1] :( aElementOf0(W1,W0)=> aElement0(W1) ) )) )),
% 35.16/4.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.16/4.93 fof(f24,definition,(
% 35.16/4.93 (! [W0] :( aIdeal0(W0)<=> ( aSet0(W0)& (! [W1] :( aElementOf0(W1,W0)=> ( (! [W2] :( aElementOf0(W2,W0)=> aElementOf0(sdtpldt0(W1,W2),W0) ))& (! [W2] :( aElement0(W2)=> aElementOf0(sdtasdt0(W2,W1),W0) ) )) ) )) ) )),
% 35.16/4.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.16/4.93 fof(f25,hypothesis,(
% 35.16/4.93 ( aIdeal0(xI)& aIdeal0(xJ) ) ),
% 35.16/4.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.16/4.93 fof(f26,hypothesis,(
% 35.16/4.93 ( aElementOf0(xx,sdtpldt1(xI,xJ))& aElementOf0(xy,sdtpldt1(xI,xJ))& aElement0(xz) ) ),
% 35.16/4.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.16/4.93 fof(f27,hypothesis,(
% 35.16/4.93 ( aElementOf0(xk,xI)& aElementOf0(xl,xJ)& xx = sdtpldt0(xk,xl) ) ),
% 35.16/4.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.16/4.93 fof(f28,hypothesis,(
% 35.16/4.93 ( aElementOf0(xm,xI)& aElementOf0(xn,xJ)& xy = sdtpldt0(xm,xn) ) ),
% 35.16/4.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.16/4.93 fof(f29,hypothesis,(
% 35.16/4.93 ( aElementOf0(sdtpldt0(xk,xm),xI)& aElementOf0(sdtpldt0(xl,xn),xJ) ) ),
% 35.16/4.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.16/4.93 fof(f31,conjecture,(
% 35.16/4.93 sdtpldt0(xx,xy) = sdtpldt0(sdtpldt0(xk,xm),sdtpldt0(xl,xn)) ),
% 35.16/4.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.16/4.93 fof(f32,negated_conjecture,(
% 35.16/4.93 ~(sdtpldt0(xx,xy) = sdtpldt0(sdtpldt0(xk,xm),sdtpldt0(xl,xn)) )),
% 35.16/4.93 inference(negated_conjecture,[status(cth)],[f31])).
% 35.16/4.93 fof(f36,plain,(
% 35.16/4.93 aElement0(sz00)),
% 35.16/4.93 inference(cnf_transformation,[status(thm)],[f2])).
% 35.16/4.93 fof(f37,plain,(
% 35.16/4.93 aElement0(sz10)),
% 35.16/4.93 inference(cnf_transformation,[status(thm)],[f3])).
% 35.16/4.93 fof(f38,plain,(
% 35.16/4.93 ![W0]: (~aElement0(W0)|aElement0(smndt0(W0)))),
% 35.16/4.93 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 35.16/4.93 fof(f39,plain,(
% 35.16/4.93 ![X0]: (~aElement0(X0)|aElement0(smndt0(X0)))),
% 35.16/4.93 inference(cnf_transformation,[status(thm)],[f38])).
% 35.16/4.93 fof(f40,plain,(
% 35.16/4.93 ![W0,W1]: ((~aElement0(W0)|~aElement0(W1))|aElement0(sdtpldt0(W0,W1)))),
% 35.16/4.93 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 35.16/4.93 fof(f41,plain,(
% 35.16/4.93 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|aElement0(sdtpldt0(X0,X1)))),
% 35.16/4.93 inference(cnf_transformation,[status(thm)],[f40])).
% 35.16/4.93 fof(f44,plain,(
% 35.16/4.93 ![W0,W1]: ((~aElement0(W0)|~aElement0(W1))|sdtpldt0(W0,W1)=sdtpldt0(W1,W0))),
% 35.16/4.93 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 35.16/4.93 fof(f45,plain,(
% 35.16/4.93 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|sdtpldt0(X0,X1)=sdtpldt0(X1,X0))),
% 35.16/4.93 inference(cnf_transformation,[status(thm)],[f44])).
% 35.16/4.93 fof(f46,plain,(
% 35.16/4.93 ![W0,W1,W2]: (((~aElement0(W0)|~aElement0(W1))|~aElement0(W2))|sdtpldt0(sdtpldt0(W0,W1),W2)=sdtpldt0(W0,sdtpldt0(W1,W2)))),
% 35.16/4.93 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 35.16/4.93 fof(f47,plain,(
% 35.16/4.93 ![X0,X1,X2]: (~aElement0(X0)|~aElement0(X1)|~aElement0(X2)|sdtpldt0(sdtpldt0(X0,X1),X2)=sdtpldt0(X0,sdtpldt0(X1,X2)))),
% 35.16/4.93 inference(cnf_transformation,[status(thm)],[f46])).
% 35.16/4.93 fof(f72,plain,(
% 35.16/4.93 ~sz10=sz00),
% 35.16/4.93 inference(cnf_transformation,[status(thm)],[f18])).
% 35.16/4.93 fof(f76,plain,(
% 35.16/4.93 ![W0]: (~aSet0(W0)|(![W1]: (~aElementOf0(W1,W0)|aElement0(W1))))),
% 35.16/4.93 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 35.16/4.93 fof(f77,plain,(
% 35.16/4.93 ![X0,X1]: (~aSet0(X0)|~aElementOf0(X1,X0)|aElement0(X1))),
% 35.16/4.93 inference(cnf_transformation,[status(thm)],[f76])).
% 35.16/4.93 fof(f106,plain,(
% 35.16/4.93 ![W0]: (aIdeal0(W0)<=>(aSet0(W0)&(![W1]: (~aElementOf0(W1,W0)|((![W2]: (~aElementOf0(W2,W0)|aElementOf0(sdtpldt0(W1,W2),W0)))&(![W2]: (~aElement0(W2)|aElementOf0(sdtasdt0(W2,W1),W0))))))))),
% 35.16/4.93 inference(pre_NNF_transformation,[status(thm)],[f24])).
% 35.16/4.93 fof(f107,plain,(
% 35.16/4.93 ![W0]: ((~aIdeal0(W0)|(aSet0(W0)&(![W1]: (~aElementOf0(W1,W0)|((![W2]: (~aElementOf0(W2,W0)|aElementOf0(sdtpldt0(W1,W2),W0)))&(![W2]: (~aElement0(W2)|aElementOf0(sdtasdt0(W2,W1),W0))))))))&(aIdeal0(W0)|(~aSet0(W0)|(?[W1]: (aElementOf0(W1,W0)&((?[W2]: (aElementOf0(W2,W0)&~aElementOf0(sdtpldt0(W1,W2),W0)))|(?[W2]: (aElement0(W2)&~aElementOf0(sdtasdt0(W2,W1),W0)))))))))),
% 35.16/4.93 inference(NNF_transformation,[status(thm)],[f106])).
% 35.16/4.93 fof(f108,plain,(
% 35.16/4.93 (![W0]: (~aIdeal0(W0)|(aSet0(W0)&(![W1]: (~aElementOf0(W1,W0)|((![W2]: (~aElementOf0(W2,W0)|aElementOf0(sdtpldt0(W1,W2),W0)))&(![W2]: (~aElement0(W2)|aElementOf0(sdtasdt0(W2,W1),W0)))))))))&(![W0]: (aIdeal0(W0)|(~aSet0(W0)|(?[W1]: (aElementOf0(W1,W0)&((?[W2]: (aElementOf0(W2,W0)&~aElementOf0(sdtpldt0(W1,W2),W0)))|(?[W2]: (aElement0(W2)&~aElementOf0(sdtasdt0(W2,W1),W0)))))))))),
% 35.16/4.93 inference(miniscoping,[status(thm)],[f107])).
% 35.16/4.93 fof(f109,plain,(
% 35.16/4.93 (![W0]: (~aIdeal0(W0)|(aSet0(W0)&(![W1]: (~aElementOf0(W1,W0)|((![W2]: (~aElementOf0(W2,W0)|aElementOf0(sdtpldt0(W1,W2),W0)))&(![W2]: (~aElement0(W2)|aElementOf0(sdtasdt0(W2,W1),W0)))))))))&(![W0]: (aIdeal0(W0)|(~aSet0(W0)|(aElementOf0(sK8_skl(W0),W0)&((aElementOf0(sK9_skl(W0),W0)&~aElementOf0(sdtpldt0(sK8_skl(W0),sK9_skl(W0)),W0))|(aElement0(sK10_skl(W0))&~aElementOf0(sdtasdt0(sK10_skl(W0),sK8_skl(W0)),W0)))))))),
% 35.16/4.93 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl,sK9_skl,sK10_skl]),skolemize(W1,sK8_skl(W0)),skolemize(W2,sK9_skl(W0)),skolemize(W2,sK10_skl(W0))],[f108])).
% 35.16/4.93 fof(f110,plain,(
% 35.16/4.93 ![X0]: (~aIdeal0(X0)|aSet0(X0))),
% 35.16/4.93 inference(cnf_transformation,[status(thm)],[f109])).
% 35.16/4.93 fof(f118,plain,(
% 35.16/4.93 aIdeal0(xI)),
% 35.16/4.93 inference(cnf_transformation,[status(thm)],[f25])).
% 35.16/4.93 fof(f119,plain,(
% 35.16/4.93 aIdeal0(xJ)),
% 35.16/4.93 inference(cnf_transformation,[status(thm)],[f25])).
% 35.16/4.93 fof(f122,plain,(
% 35.16/4.93 aElement0(xz)),
% 35.16/4.93 inference(cnf_transformation,[status(thm)],[f26])).
% 35.16/4.93 fof(f123,plain,(
% 35.16/4.93 aElementOf0(xk,xI)),
% 35.16/4.93 inference(cnf_transformation,[status(thm)],[f27])).
% 35.16/4.93 fof(f124,plain,(
% 35.16/4.93 aElementOf0(xl,xJ)),
% 35.16/4.93 inference(cnf_transformation,[status(thm)],[f27])).
% 35.16/4.93 fof(f125,plain,(
% 35.16/4.93 xx=sdtpldt0(xk,xl)),
% 35.16/4.93 inference(cnf_transformation,[status(thm)],[f27])).
% 35.16/4.93 fof(f126,plain,(
% 35.16/4.93 aElementOf0(xm,xI)),
% 35.16/4.93 inference(cnf_transformation,[status(thm)],[f28])).
% 35.16/4.93 fof(f127,plain,(
% 35.16/4.93 aElementOf0(xn,xJ)),
% 35.16/4.93 inference(cnf_transformation,[status(thm)],[f28])).
% 35.16/4.93 fof(f128,plain,(
% 35.16/4.93 xy=sdtpldt0(xm,xn)),
% 35.16/4.93 inference(cnf_transformation,[status(thm)],[f28])).
% 35.16/4.93 fof(f129,plain,(
% 35.16/4.93 aElementOf0(sdtpldt0(xk,xm),xI)),
% 35.16/4.93 inference(cnf_transformation,[status(thm)],[f29])).
% 35.16/4.93 fof(f130,plain,(
% 35.16/4.93 aElementOf0(sdtpldt0(xl,xn),xJ)),
% 35.16/4.93 inference(cnf_transformation,[status(thm)],[f29])).
% 35.16/4.93 fof(f133,plain,(
% 35.16/4.93 ~sdtpldt0(xx,xy)=sdtpldt0(sdtpldt0(xk,xm),sdtpldt0(xl,xn))),
% 35.16/4.93 inference(cnf_transformation,[status(thm)],[f32])).
% 35.16/4.93 fof(f172,plain,(
% 35.16/4.93 ![X0]: (~aElement0(X0)|aElement0(sdtpldt0(sz10,X0)))),
% 35.16/4.93 inference(resolution,[status(thm)],[f37,f41])).
% 35.16/4.93 fof(f173,plain,(
% 35.16/4.93 aElement0(smndt0(sz10))),
% 35.16/4.93 inference(resolution,[status(thm)],[f39,f37])).
% 35.16/4.93 fof(f216,plain,(
% 35.16/4.93 aElement0(sdtpldt0(sz10,sz10))),
% 35.16/4.93 inference(resolution,[status(thm)],[f172,f37])).
% 35.16/4.93 fof(f251,plain,(
% 35.16/4.93 ~aSet0(xJ)|aElement0(sdtpldt0(xl,xn))),
% 35.16/4.93 inference(resolution,[status(thm)],[f77,f130])).
% 35.16/4.93 fof(f252,plain,(
% 35.16/4.93 ~aSet0(xI)|aElement0(sdtpldt0(xk,xm))),
% 35.16/4.93 inference(resolution,[status(thm)],[f77,f129])).
% 35.16/4.93 fof(f253,plain,(
% 35.16/4.93 ~aSet0(xJ)|aElement0(xn)),
% 35.16/4.93 inference(resolution,[status(thm)],[f77,f127])).
% 35.16/4.93 fof(f254,plain,(
% 35.16/4.93 ~aSet0(xI)|aElement0(xm)),
% 35.16/4.93 inference(resolution,[status(thm)],[f77,f126])).
% 35.16/4.93 fof(f255,plain,(
% 35.16/4.93 ~aSet0(xJ)|aElement0(xl)),
% 35.16/4.93 inference(resolution,[status(thm)],[f77,f124])).
% 35.16/4.93 fof(f256,plain,(
% 35.16/4.93 ~aSet0(xI)|aElement0(xk)),
% 35.16/4.93 inference(resolution,[status(thm)],[f77,f123])).
% 35.16/4.93 fof(f259,definition,(
% 35.16/4.93 sQ0_spl <=> (aSet0(xJ))),
% 35.16/4.93 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 35.16/4.93 fof(f261,plain,(
% 35.16/4.93 ~aSet0(xJ)|sQ0_spl),
% 35.16/4.93 inference(component_clause,[status(thm)],[f259])).
% 35.16/4.93 fof(f262,definition,(
% 35.16/4.93 sQ1_spl <=> (aElement0(sdtpldt0(xl,xn)))),
% 35.16/4.93 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 35.16/4.93 fof(f263,plain,(
% 35.16/4.93 aElement0(sdtpldt0(xl,xn))|~sQ1_spl),
% 35.16/4.93 inference(component_clause,[status(thm)],[f262])).
% 35.16/4.93 fof(f265,plain,(
% 35.16/4.93 ~sQ0_spl|sQ1_spl),
% 35.16/4.93 inference(split_clause,[status(thm)],[f251,f259,f262])).
% 35.16/4.93 fof(f266,definition,(
% 35.16/4.93 sQ2_spl <=> (aSet0(xI))),
% 35.16/4.93 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 35.16/4.93 fof(f268,plain,(
% 35.16/4.93 ~aSet0(xI)|sQ2_spl),
% 35.16/4.93 inference(component_clause,[status(thm)],[f266])).
% 35.16/4.93 fof(f269,definition,(
% 35.16/4.93 sQ3_spl <=> (aElement0(sdtpldt0(xk,xm)))),
% 35.16/4.93 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 35.16/4.93 fof(f270,plain,(
% 35.16/4.93 aElement0(sdtpldt0(xk,xm))|~sQ3_spl),
% 35.16/4.93 inference(component_clause,[status(thm)],[f269])).
% 35.16/4.93 fof(f272,plain,(
% 35.16/4.93 ~sQ2_spl|sQ3_spl),
% 35.16/4.93 inference(split_clause,[status(thm)],[f252,f266,f269])).
% 35.16/4.93 fof(f273,definition,(
% 35.16/4.93 sQ4_spl <=> (aElement0(xn))),
% 35.16/4.93 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 35.16/4.93 fof(f274,plain,(
% 35.16/4.93 aElement0(xn)|~sQ4_spl),
% 35.16/4.93 inference(component_clause,[status(thm)],[f273])).
% 35.16/4.93 fof(f276,plain,(
% 35.16/4.93 ~sQ0_spl|sQ4_spl),
% 35.16/4.93 inference(split_clause,[status(thm)],[f253,f259,f273])).
% 35.16/4.93 fof(f277,definition,(
% 35.16/4.93 sQ5_spl <=> (aElement0(xm))),
% 35.16/4.93 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 35.16/4.93 fof(f278,plain,(
% 35.16/4.93 aElement0(xm)|~sQ5_spl),
% 35.16/4.93 inference(component_clause,[status(thm)],[f277])).
% 35.16/4.93 fof(f280,plain,(
% 35.16/4.93 ~sQ2_spl|sQ5_spl),
% 35.16/4.93 inference(split_clause,[status(thm)],[f254,f266,f277])).
% 35.16/4.93 fof(f281,definition,(
% 35.16/4.93 sQ6_spl <=> (aElement0(xl))),
% 35.16/4.93 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 35.16/4.93 fof(f282,plain,(
% 35.16/4.93 aElement0(xl)|~sQ6_spl),
% 35.16/4.93 inference(component_clause,[status(thm)],[f281])).
% 35.16/4.93 fof(f284,plain,(
% 35.16/4.93 ~sQ0_spl|sQ6_spl),
% 35.16/4.93 inference(split_clause,[status(thm)],[f255,f259,f281])).
% 35.16/4.93 fof(f285,definition,(
% 35.16/4.93 sQ7_spl <=> (aElement0(xk))),
% 35.16/4.93 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 35.16/4.93 fof(f286,plain,(
% 35.16/4.93 aElement0(xk)|~sQ7_spl),
% 35.16/4.93 inference(component_clause,[status(thm)],[f285])).
% 35.16/4.93 fof(f288,plain,(
% 35.16/4.93 ~sQ2_spl|sQ7_spl),
% 35.16/4.93 inference(split_clause,[status(thm)],[f256,f266,f285])).
% 35.16/4.93 fof(f326,plain,(
% 35.16/4.93 aElement0(sdtpldt0(sz10,sdtpldt0(sz10,sz10)))),
% 35.16/4.93 inference(resolution,[status(thm)],[f216,f172])).
% 35.16/4.93 fof(f363,definition,(
% 35.16/4.93 sQ13_spl <=> (aElement0(sz00))),
% 35.16/4.93 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 35.16/4.93 fof(f365,plain,(
% 35.16/4.93 ~aElement0(sz00)|sQ13_spl),
% 35.16/4.93 inference(component_clause,[status(thm)],[f363])).
% 35.16/4.93 fof(f366,definition,(
% 35.16/4.94 sQ14_spl <=> (aElement0(sdtpldt0(sz10,sz10)))),
% 35.16/4.94 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 35.16/4.94 fof(f368,plain,(
% 35.16/4.94 ~aElement0(sdtpldt0(sz10,sz10))|sQ14_spl),
% 35.16/4.94 inference(component_clause,[status(thm)],[f366])).
% 35.16/4.94 fof(f393,definition,(
% 35.16/4.94 sQ17_spl <=> (aElement0(smndt0(sz10)))),
% 35.16/4.94 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 35.16/4.94 fof(f395,plain,(
% 35.16/4.94 ~aElement0(smndt0(sz10))|sQ17_spl),
% 35.16/4.94 inference(component_clause,[status(thm)],[f393])).
% 35.16/4.94 fof(f599,definition,(
% 35.16/4.94 sQ47_spl <=> (aElement0(sz10))),
% 35.16/4.94 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 35.16/4.94 fof(f601,plain,(
% 35.16/4.94 ~aElement0(sz10)|sQ47_spl),
% 35.16/4.94 inference(component_clause,[status(thm)],[f599])).
% 35.16/4.94 fof(f602,definition,(
% 35.16/4.94 sQ48_spl <=> (sz10=sz00)),
% 35.16/4.94 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 35.16/4.94 fof(f603,plain,(
% 35.16/4.94 sz10=sz00|~sQ48_spl),
% 35.16/4.94 inference(component_clause,[status(thm)],[f602])).
% 35.16/4.94 fof(f744,plain,(
% 35.16/4.94 aElement0(sdtpldt0(sz10,sdtpldt0(sz10,sdtpldt0(sz10,sz10))))),
% 35.16/4.94 inference(resolution,[status(thm)],[f326,f172])).
% 35.16/4.94 fof(f1013,plain,(
% 35.16/4.94 aSet0(xI)),
% 35.16/4.94 inference(resolution,[status(thm)],[f118,f110])).
% 35.16/4.94 fof(f1014,plain,(
% 35.16/4.94 $false|sQ2_spl),
% 35.16/4.94 inference(forward_subsumption_resolution,[status(thm)],[f1013,f268])).
% 35.16/4.94 fof(f1015,plain,(
% 35.16/4.94 sQ2_spl),
% 35.16/4.94 inference(contradiction_clause,[status(thm)],[f1014])).
% 35.16/4.94 fof(f1016,plain,(
% 35.16/4.94 aSet0(xJ)),
% 35.16/4.94 inference(resolution,[status(thm)],[f119,f110])).
% 35.16/4.94 fof(f1017,plain,(
% 35.16/4.94 $false|sQ0_spl),
% 35.16/4.94 inference(forward_subsumption_resolution,[status(thm)],[f1016,f261])).
% 35.16/4.94 fof(f1018,plain,(
% 35.16/4.94 sQ0_spl),
% 35.16/4.94 inference(contradiction_clause,[status(thm)],[f1017])).
% 35.16/4.94 fof(f1082,plain,(
% 35.16/4.94 ![X0]: (~aElement0(X0)|sdtpldt0(X0,xm)=sdtpldt0(xm,X0)|~sQ5_spl)),
% 35.16/4.94 inference(resolution,[status(thm)],[f278,f45])).
% 35.16/4.94 fof(f1084,plain,(
% 35.16/4.94 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|sdtpldt0(sdtpldt0(X0,X1),xm)=sdtpldt0(X0,sdtpldt0(X1,xm))|~sQ5_spl)),
% 35.16/4.94 inference(resolution,[status(thm)],[f278,f47])).
% 35.16/4.94 fof(f1086,plain,(
% 35.16/4.94 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|sdtpldt0(sdtpldt0(X0,xm),X1)=sdtpldt0(X0,sdtpldt0(xm,X1))|~sQ5_spl)),
% 35.16/4.94 inference(resolution,[status(thm)],[f278,f47])).
% 35.16/4.94 fof(f1087,plain,(
% 35.16/4.94 ![X0]: (~aElement0(X0)|aElement0(sdtpldt0(xm,X0))|~sQ5_spl)),
% 35.16/4.94 inference(resolution,[status(thm)],[f278,f41])).
% 35.16/4.94 fof(f1144,plain,(
% 35.16/4.94 ![X0]: (~aElement0(X0)|sdtpldt0(X0,xk)=sdtpldt0(xk,X0)|~sQ7_spl)),
% 35.16/4.94 inference(resolution,[status(thm)],[f286,f45])).
% 35.16/4.94 fof(f1146,plain,(
% 35.16/4.94 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|sdtpldt0(sdtpldt0(X0,X1),xk)=sdtpldt0(X0,sdtpldt0(X1,xk))|~sQ7_spl)),
% 35.16/4.94 inference(resolution,[status(thm)],[f286,f47])).
% 35.16/4.94 fof(f1148,plain,(
% 35.16/4.94 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|sdtpldt0(sdtpldt0(X0,xk),X1)=sdtpldt0(X0,sdtpldt0(xk,X1))|~sQ7_spl)),
% 35.16/4.94 inference(resolution,[status(thm)],[f286,f47])).
% 35.16/4.94 fof(f1206,plain,(
% 35.16/4.94 ![X0]: (~aElement0(X0)|sdtpldt0(X0,xn)=sdtpldt0(xn,X0)|~sQ4_spl)),
% 35.16/4.94 inference(resolution,[status(thm)],[f274,f45])).
% 35.16/4.94 fof(f1208,plain,(
% 35.16/4.94 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|sdtpldt0(sdtpldt0(X0,X1),xn)=sdtpldt0(X0,sdtpldt0(X1,xn))|~sQ4_spl)),
% 35.16/4.94 inference(resolution,[status(thm)],[f274,f47])).
% 35.16/4.94 fof(f1210,plain,(
% 35.16/4.94 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|sdtpldt0(sdtpldt0(X0,xn),X1)=sdtpldt0(X0,sdtpldt0(xn,X1))|~sQ4_spl)),
% 35.16/4.94 inference(resolution,[status(thm)],[f274,f47])).
% 35.16/4.94 fof(f1272,plain,(
% 35.16/4.94 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|sdtpldt0(sdtpldt0(X0,xl),X1)=sdtpldt0(X0,sdtpldt0(xl,X1))|~sQ6_spl)),
% 35.16/4.94 inference(resolution,[status(thm)],[f282,f47])).
% 35.16/4.94 fof(f1285,plain,(
% 35.16/4.94 sdtpldt0(xl,xm)=sdtpldt0(xm,xl)|~sQ5_spl|~sQ6_spl),
% 35.16/4.94 inference(resolution,[status(thm)],[f1082,f282])).
% 35.16/4.94 fof(f1286,plain,(
% 35.16/4.94 sdtpldt0(xn,xm)=sdtpldt0(xm,xn)|~sQ5_spl|~sQ4_spl),
% 35.16/4.94 inference(resolution,[status(thm)],[f1082,f274])).
% 35.16/4.94 fof(f1287,plain,(
% 35.16/4.94 sdtpldt0(xk,xm)=sdtpldt0(xm,xk)|~sQ5_spl|~sQ7_spl),
% 35.16/4.94 inference(resolution,[status(thm)],[f1082,f286])).
% 35.16/4.94 fof(f1296,plain,(
% 35.16/4.94 sdtpldt0(xn,xm)=xy|~sQ5_spl|~sQ4_spl),
% 35.16/4.94 inference(forward_demodulation,[status(thm)],[f128,f1286])).
% 35.16/4.94 fof(f1310,plain,(
% 35.16/4.94 ![X0]: (~aElement0(X0)|sdtpldt0(sdtpldt0(X0,xl),xm)=sdtpldt0(X0,sdtpldt0(xl,xm))|~sQ5_spl|~sQ6_spl)),
% 35.16/4.94 inference(resolution,[status(thm)],[f1084,f282])).
% 35.16/4.94 fof(f1311,plain,(
% 35.16/4.94 ![X0]: (~aElement0(X0)|sdtpldt0(sdtpldt0(X0,xn),xm)=sdtpldt0(X0,sdtpldt0(xn,xm))|~sQ5_spl|~sQ4_spl)),
% 35.16/4.94 inference(resolution,[status(thm)],[f1084,f274])).
% 35.16/4.94 fof(f1312,plain,(
% 35.16/4.94 ![X0]: (~aElement0(X0)|sdtpldt0(sdtpldt0(X0,xk),xm)=sdtpldt0(X0,sdtpldt0(xk,xm))|~sQ5_spl|~sQ7_spl)),
% 35.16/4.94 inference(resolution,[status(thm)],[f1084,f286])).
% 35.16/4.94 fof(f1322,plain,(
% 35.16/4.94 ![X0]: (~aElement0(X0)|sdtpldt0(sdtpldt0(X0,xm),xl)=sdtpldt0(X0,sdtpldt0(xm,xl))|~sQ5_spl|~sQ6_spl)),
% 35.16/4.94 inference(resolution,[status(thm)],[f1086,f282])).
% 35.16/4.94 fof(f1323,plain,(
% 35.16/4.94 ![X0]: (~aElement0(X0)|sdtpldt0(sdtpldt0(X0,xm),xn)=sdtpldt0(X0,sdtpldt0(xm,xn))|~sQ5_spl|~sQ4_spl)),
% 35.16/4.94 inference(resolution,[status(thm)],[f1086,f274])).
% 35.16/4.94 fof(f1333,plain,(
% 35.16/4.94 ![X0]: (~aElement0(X0)|sdtpldt0(sdtpldt0(X0,xm),xn)=sdtpldt0(X0,xy)|~sQ5_spl|~sQ4_spl)),
% 35.16/4.94 inference(forward_demodulation,[status(thm)],[f128,f1323])).
% 35.16/4.94 fof(f1357,plain,(
% 35.16/4.94 sdtpldt0(xl,xk)=sdtpldt0(xk,xl)|~sQ7_spl|~sQ6_spl),
% 35.16/4.94 inference(resolution,[status(thm)],[f1144,f282])).
% 35.16/4.94 fof(f1358,plain,(
% 35.16/4.94 sdtpldt0(xn,xk)=sdtpldt0(xk,xn)|~sQ7_spl|~sQ4_spl),
% 35.16/4.94 inference(resolution,[status(thm)],[f1144,f274])).
% 35.16/4.94 fof(f1368,plain,(
% 35.16/4.94 sdtpldt0(xl,xk)=xx|~sQ7_spl|~sQ6_spl),
% 35.16/4.94 inference(forward_demodulation,[status(thm)],[f125,f1357])).
% 35.16/4.94 fof(f1383,plain,(
% 35.16/4.94 ![X0]: (~aElement0(X0)|sdtpldt0(sdtpldt0(X0,xn),xk)=sdtpldt0(X0,sdtpldt0(xn,xk))|~sQ7_spl|~sQ4_spl)),
% 35.16/4.94 inference(resolution,[status(thm)],[f1146,f274])).
% 35.16/4.94 fof(f1395,plain,(
% 35.16/4.94 ![X0]: (~aElement0(X0)|sdtpldt0(sdtpldt0(X0,xk),xn)=sdtpldt0(X0,sdtpldt0(xk,xn))|~sQ7_spl|~sQ4_spl)),
% 35.16/4.94 inference(resolution,[status(thm)],[f1148,f274])).
% 35.16/4.94 fof(f1407,plain,(
% 35.16/4.94 sdtpldt0(xl,xn)=sdtpldt0(xn,xl)|~sQ4_spl|~sQ6_spl),
% 35.16/4.94 inference(resolution,[status(thm)],[f1206,f282])).
% 35.16/4.94 fof(f1433,plain,(
% 35.16/4.94 ![X0]: (~aElement0(X0)|sdtpldt0(sdtpldt0(X0,xl),xn)=sdtpldt0(X0,sdtpldt0(xl,xn))|~sQ4_spl|~sQ6_spl)),
% 35.16/4.94 inference(resolution,[status(thm)],[f1208,f282])).
% 35.16/4.94 fof(f1480,plain,(
% 35.16/4.94 ![X0]: (~aElement0(X0)|sdtpldt0(sdtpldt0(X0,xn),xl)=sdtpldt0(X0,sdtpldt0(xn,xl))|~sQ4_spl|~sQ6_spl)),
% 35.16/4.94 inference(resolution,[status(thm)],[f1210,f282])).
% 35.16/4.94 fof(f1553,plain,(
% 35.16/4.94 sdtpldt0(sdtpldt0(xn,xl),xm)=sdtpldt0(xn,sdtpldt0(xl,xm))|~sQ5_spl|~sQ6_spl|~sQ4_spl),
% 35.16/4.94 inference(resolution,[status(thm)],[f1310,f274])).
% 35.16/4.94 fof(f1554,plain,(
% 35.16/4.94 sdtpldt0(sdtpldt0(xk,xl),xm)=sdtpldt0(xk,sdtpldt0(xl,xm))|~sQ5_spl|~sQ6_spl|~sQ7_spl),
% 35.16/4.94 inference(resolution,[status(thm)],[f1310,f286])).
% 35.16/4.94 fof(f1563,plain,(
% 35.16/4.94 sdtpldt0(xx,xm)=sdtpldt0(xk,sdtpldt0(xl,xm))|~sQ5_spl|~sQ6_spl|~sQ7_spl),
% 35.16/4.94 inference(forward_demodulation,[status(thm)],[f125,f1554])).
% 35.16/4.94 fof(f1567,plain,(
% 35.16/4.94 ![X0]: (~aElement0(X0)|sdtpldt0(sdtpldt0(X0,xn),xm)=sdtpldt0(X0,xy)|~sQ5_spl|~sQ4_spl)),
% 35.16/4.94 inference(forward_demodulation,[status(thm)],[f1296,f1311])).
% 35.16/4.94 fof(f1568,plain,(
% 35.16/4.94 sdtpldt0(sdtpldt0(xl,xn),xm)=sdtpldt0(xl,xy)|~sQ5_spl|~sQ4_spl|~sQ6_spl),
% 35.16/4.94 inference(resolution,[status(thm)],[f1567,f282])).
% 35.16/4.94 fof(f1582,plain,(
% 35.16/4.94 sdtpldt0(sdtpldt0(xl,xk),xm)=sdtpldt0(xl,sdtpldt0(xk,xm))|~sQ5_spl|~sQ7_spl|~sQ6_spl),
% 35.16/4.94 inference(resolution,[status(thm)],[f1312,f282])).
% 35.16/4.94 fof(f1596,plain,(
% 35.16/4.94 ![X0]: (~aElement0(X0)|sdtpldt0(sdtpldt0(X0,xm),xl)=sdtpldt0(X0,sdtpldt0(xl,xm))|~sQ5_spl|~sQ6_spl)),
% 35.16/4.94 inference(forward_demodulation,[status(thm)],[f1285,f1322])).
% 35.16/4.94 fof(f1598,plain,(
% 35.16/4.94 sdtpldt0(sdtpldt0(xn,xm),xl)=sdtpldt0(xn,sdtpldt0(xl,xm))|~sQ5_spl|~sQ6_spl|~sQ4_spl),
% 35.16/4.94 inference(resolution,[status(thm)],[f1596,f274])).
% 35.16/4.94 fof(f1599,plain,(
% 35.16/4.94 sdtpldt0(sdtpldt0(xk,xm),xl)=sdtpldt0(xk,sdtpldt0(xl,xm))|~sQ5_spl|~sQ6_spl|~sQ7_spl),
% 35.16/4.94 inference(resolution,[status(thm)],[f1596,f286])).
% 35.16/4.94 fof(f1608,plain,(
% 35.16/4.94 sdtpldt0(xy,xl)=sdtpldt0(xn,sdtpldt0(xl,xm))|~sQ5_spl|~sQ6_spl|~sQ4_spl),
% 35.16/4.94 inference(forward_demodulation,[status(thm)],[f1296,f1598])).
% 35.16/4.94 fof(f1613,plain,(
% 35.16/4.94 sdtpldt0(sdtpldt0(xk,xm),xn)=sdtpldt0(xk,xy)|~sQ5_spl|~sQ4_spl|~sQ7_spl),
% 35.16/4.94 inference(resolution,[status(thm)],[f1333,f286])).
% 35.16/4.94 fof(f1662,plain,(
% 35.16/4.94 $false|sQ13_spl),
% 35.16/4.94 inference(forward_subsumption_resolution,[status(thm)],[f365,f36])).
% 35.16/4.94 fof(f1663,plain,(
% 35.16/4.94 sQ13_spl),
% 35.16/4.94 inference(contradiction_clause,[status(thm)],[f1662])).
% 35.16/4.94 fof(f1687,plain,(
% 35.16/4.94 ![X0]: (~aElement0(X0)|sdtpldt0(sdtpldt0(X0,xn),xk)=sdtpldt0(X0,sdtpldt0(xk,xn))|~sQ7_spl|~sQ4_spl)),
% 35.16/4.94 inference(forward_demodulation,[status(thm)],[f1358,f1383])).
% 35.16/4.94 fof(f1691,plain,(
% 35.16/4.94 sdtpldt0(sdtpldt0(xm,xn),xk)=sdtpldt0(xm,sdtpldt0(xk,xn))|~sQ7_spl|~sQ4_spl|~sQ5_spl),
% 35.16/4.94 inference(resolution,[status(thm)],[f1687,f278])).
% 35.16/4.94 fof(f1699,plain,(
% 35.16/4.94 sdtpldt0(xy,xk)=sdtpldt0(xm,sdtpldt0(xk,xn))|~sQ7_spl|~sQ4_spl|~sQ5_spl),
% 35.16/4.94 inference(forward_demodulation,[status(thm)],[f128,f1691])).
% 35.16/4.94 fof(f1722,plain,(
% 35.16/4.94 sdtpldt0(sdtpldt0(xm,xk),xn)=sdtpldt0(xm,sdtpldt0(xk,xn))|~sQ7_spl|~sQ4_spl|~sQ5_spl),
% 35.16/4.94 inference(resolution,[status(thm)],[f1395,f278])).
% 35.16/4.94 fof(f1732,plain,(
% 35.16/4.94 sdtpldt0(sdtpldt0(xk,xm),xn)=sdtpldt0(xm,sdtpldt0(xk,xn))|~sQ7_spl|~sQ4_spl|~sQ5_spl),
% 35.16/4.94 inference(forward_demodulation,[status(thm)],[f1287,f1722])).
% 35.16/4.94 fof(f1827,plain,(
% 35.16/4.94 ![X0]: (~aElement0(X0)|sdtpldt0(sdtpldt0(X0,xn),xl)=sdtpldt0(X0,sdtpldt0(xl,xn))|~sQ4_spl|~sQ6_spl)),
% 35.16/4.94 inference(forward_demodulation,[status(thm)],[f1407,f1480])).
% 35.16/4.94 fof(f1831,plain,(
% 35.16/4.94 sdtpldt0(sdtpldt0(xm,xn),xl)=sdtpldt0(xm,sdtpldt0(xl,xn))|~sQ4_spl|~sQ6_spl|~sQ5_spl),
% 35.16/4.94 inference(resolution,[status(thm)],[f1827,f278])).
% 35.16/4.94 fof(f1839,plain,(
% 35.16/4.94 sdtpldt0(xy,xl)=sdtpldt0(xm,sdtpldt0(xl,xn))|~sQ4_spl|~sQ6_spl|~sQ5_spl),
% 35.16/4.94 inference(forward_demodulation,[status(thm)],[f128,f1831])).
% 35.16/4.94 fof(f1906,plain,(
% 35.16/4.94 sdtpldt0(sdtpldt0(xl,xn),xm)=sdtpldt0(xn,sdtpldt0(xl,xm))|~sQ5_spl|~sQ6_spl|~sQ4_spl),
% 35.16/4.94 inference(forward_demodulation,[status(thm)],[f1407,f1553])).
% 35.16/4.94 fof(f1954,plain,(
% 35.16/4.94 sdtpldt0(xl,xy)=sdtpldt0(xn,sdtpldt0(xl,xm))|~sQ5_spl|~sQ6_spl|~sQ4_spl),
% 35.16/4.94 inference(backward_demodulation,[status(thm)],[f1568,f1906])).
% 35.16/4.94 fof(f1967,plain,(
% 35.16/4.94 sdtpldt0(xx,xm)=sdtpldt0(xl,sdtpldt0(xk,xm))|~sQ5_spl|~sQ7_spl|~sQ6_spl),
% 35.16/4.94 inference(forward_demodulation,[status(thm)],[f1368,f1582])).
% 35.16/4.94 fof(f1983,plain,(
% 35.16/4.94 sdtpldt0(sdtpldt0(xk,xm),xl)=sdtpldt0(xx,xm)|~sQ5_spl|~sQ6_spl|~sQ7_spl),
% 35.16/4.94 inference(forward_demodulation,[status(thm)],[f1563,f1599])).
% 35.16/4.94 fof(f2134,plain,(
% 35.16/4.94 sdtpldt0(xk,xy)=sdtpldt0(xm,sdtpldt0(xk,xn))|~sQ7_spl|~sQ4_spl|~sQ5_spl),
% 35.16/4.94 inference(forward_demodulation,[status(thm)],[f1613,f1732])).
% 35.16/4.94 fof(f2135,plain,(
% 35.16/4.94 sdtpldt0(sdtpldt0(xk,xm),xn)=sdtpldt0(xy,xk)|~sQ5_spl|~sQ4_spl|~sQ7_spl),
% 35.16/4.94 inference(backward_demodulation,[status(thm)],[f2137,f1613])).
% 35.16/4.94 fof(f2137,plain,(
% 35.16/4.94 sdtpldt0(xk,xy)=sdtpldt0(xy,xk)|~sQ7_spl|~sQ4_spl|~sQ5_spl),
% 35.16/4.94 inference(forward_demodulation,[status(thm)],[f1699,f2134])).
% 35.16/4.94 fof(f2203,plain,(
% 35.16/4.94 sdtpldt0(xl,xy)=sdtpldt0(xy,xl)|~sQ5_spl|~sQ6_spl|~sQ4_spl),
% 35.16/4.94 inference(forward_demodulation,[status(thm)],[f1608,f1954])).
% 35.16/4.94 fof(f2255,definition,(
% 35.16/4.94 sQ72_spl <=> (aElement0(xz))),
% 35.16/4.94 introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 35.16/4.94 fof(f2257,plain,(
% 35.16/4.94 ~aElement0(xz)|sQ72_spl),
% 35.16/4.94 inference(component_clause,[status(thm)],[f2255])).
% 35.16/4.94 fof(f2486,plain,(
% 35.16/4.94 $false|sQ14_spl),
% 35.16/4.94 inference(forward_subsumption_resolution,[status(thm)],[f368,f216])).
% 35.16/4.94 fof(f2487,plain,(
% 35.16/4.94 sQ14_spl),
% 35.16/4.94 inference(contradiction_clause,[status(thm)],[f2486])).
% 35.16/4.94 fof(f3001,plain,(
% 35.16/4.94 sdtpldt0(sdtpldt0(sdtpldt0(xk,xm),xn),xl)=sdtpldt0(sdtpldt0(xk,xm),sdtpldt0(xl,xn))|~sQ3_spl|~sQ4_spl|~sQ6_spl),
% 35.16/4.94 inference(resolution,[status(thm)],[f270,f1827])).
% 35.16/4.94 fof(f3004,plain,(
% 35.16/4.94 sdtpldt0(sdtpldt0(sdtpldt0(xk,xm),xl),xn)=sdtpldt0(sdtpldt0(xk,xm),sdtpldt0(xl,xn))|~sQ3_spl|~sQ4_spl|~sQ6_spl),
% 35.16/4.94 inference(resolution,[status(thm)],[f270,f1433])).
% 35.16/4.94 fof(f3027,plain,(
% 35.16/4.94 ![X0]: (~aElement0(X0)|sdtpldt0(sdtpldt0(X0,sdtpldt0(xk,xm)),xn)=sdtpldt0(X0,sdtpldt0(sdtpldt0(xk,xm),xn))|~sQ3_spl|~sQ4_spl)),
% 35.16/4.94 inference(resolution,[status(thm)],[f270,f1208])).
% 35.16/4.94 fof(f3109,plain,(
% 35.16/4.94 sdtpldt0(sdtpldt0(xy,xk),xl)=sdtpldt0(sdtpldt0(xk,xm),sdtpldt0(xl,xn))|~sQ5_spl|~sQ7_spl|~sQ3_spl|~sQ4_spl|~sQ6_spl),
% 35.16/4.94 inference(forward_demodulation,[status(thm)],[f2135,f3001])).
% 35.16/4.94 fof(f3110,plain,(
% 35.16/4.94 sdtpldt0(sdtpldt0(xx,xm),xn)=sdtpldt0(sdtpldt0(xk,xm),sdtpldt0(xl,xn))|~sQ5_spl|~sQ7_spl|~sQ3_spl|~sQ4_spl|~sQ6_spl),
% 35.16/4.94 inference(forward_demodulation,[status(thm)],[f1983,f3004])).
% 35.16/4.94 fof(f3130,plain,(
% 35.16/4.94 ![X0]: (~aElement0(X0)|sdtpldt0(sdtpldt0(X0,sdtpldt0(xk,xm)),xn)=sdtpldt0(X0,sdtpldt0(xy,xk))|~sQ5_spl|~sQ7_spl|~sQ3_spl|~sQ4_spl)),
% 35.16/4.94 inference(forward_demodulation,[status(thm)],[f2135,f3027])).
% 35.16/4.94 fof(f3143,plain,(
% 35.16/4.94 ~sdtpldt0(xx,xy)=sdtpldt0(sdtpldt0(xy,xk),xl)|~sQ5_spl|~sQ7_spl|~sQ3_spl|~sQ4_spl|~sQ6_spl),
% 35.16/4.94 inference(backward_demodulation,[status(thm)],[f3109,f133])).
% 35.16/4.94 fof(f3144,plain,(
% 35.16/4.94 sdtpldt0(sdtpldt0(xy,xk),xl)=sdtpldt0(sdtpldt0(xx,xm),xn)|~sQ5_spl|~sQ7_spl|~sQ3_spl|~sQ4_spl|~sQ6_spl),
% 35.16/4.94 inference(backward_demodulation,[status(thm)],[f3110,f3109])).
% 35.16/4.94 fof(f3208,plain,(
% 35.16/4.94 sdtpldt0(sdtpldt0(xl,sdtpldt0(xk,xm)),xn)=sdtpldt0(xl,sdtpldt0(xy,xk))|~sQ5_spl|~sQ7_spl|~sQ3_spl|~sQ4_spl|~sQ6_spl),
% 35.16/4.94 inference(resolution,[status(thm)],[f3130,f282])).
% 35.16/4.94 fof(f3221,plain,(
% 35.16/4.94 sdtpldt0(sdtpldt0(xx,xm),xn)=sdtpldt0(xl,sdtpldt0(xy,xk))|~sQ5_spl|~sQ7_spl|~sQ3_spl|~sQ4_spl|~sQ6_spl),
% 35.16/4.94 inference(forward_demodulation,[status(thm)],[f1967,f3208])).
% 35.16/4.94 fof(f3324,plain,(
% 35.16/4.94 ~sdtpldt0(xx,xy)=sdtpldt0(sdtpldt0(xx,xm),xn)|~sQ5_spl|~sQ7_spl|~sQ3_spl|~sQ4_spl|~sQ6_spl),
% 35.16/4.95 inference(backward_demodulation,[status(thm)],[f3144,f3143])).
% 35.16/4.95 fof(f3388,plain,(
% 35.16/4.95 ~sdtpldt0(xx,xy)=sdtpldt0(xl,sdtpldt0(xy,xk))|~sQ5_spl|~sQ7_spl|~sQ3_spl|~sQ4_spl|~sQ6_spl),
% 35.16/4.95 inference(backward_demodulation,[status(thm)],[f3221,f3324])).
% 35.16/4.95 fof(f3389,plain,(
% 35.16/4.95 sdtpldt0(xl,sdtpldt0(xy,xk))=sdtpldt0(sdtpldt0(xk,xm),sdtpldt0(xl,xn))|~sQ5_spl|~sQ7_spl|~sQ3_spl|~sQ4_spl|~sQ6_spl),
% 35.16/4.95 inference(backward_demodulation,[status(thm)],[f3221,f3110])).
% 35.16/4.95 fof(f3695,plain,(
% 35.16/4.95 ![X0]: (~aElement0(X0)|sdtpldt0(sdtpldt0(X0,xm),sdtpldt0(xl,xn))=sdtpldt0(X0,sdtpldt0(xm,sdtpldt0(xl,xn)))|~sQ1_spl|~sQ5_spl)),
% 35.16/4.95 inference(resolution,[status(thm)],[f263,f1086])).
% 35.16/4.95 fof(f3804,plain,(
% 35.16/4.95 ![X0]: (~aElement0(X0)|sdtpldt0(sdtpldt0(X0,xm),sdtpldt0(xl,xn))=sdtpldt0(X0,sdtpldt0(xy,xl))|~sQ4_spl|~sQ6_spl|~sQ1_spl|~sQ5_spl)),
% 35.16/4.95 inference(forward_demodulation,[status(thm)],[f1839,f3695])).
% 35.16/4.95 fof(f3953,plain,(
% 35.16/4.95 sdtpldt0(sdtpldt0(xk,xm),sdtpldt0(xl,xn))=sdtpldt0(xk,sdtpldt0(xy,xl))|~sQ4_spl|~sQ6_spl|~sQ1_spl|~sQ5_spl|~sQ7_spl),
% 35.16/4.95 inference(resolution,[status(thm)],[f3804,f286])).
% 35.16/4.95 fof(f4306,plain,(
% 35.16/4.95 sdtpldt0(xl,sdtpldt0(xy,xk))=sdtpldt0(xk,sdtpldt0(xy,xl))|~sQ1_spl|~sQ5_spl|~sQ7_spl|~sQ3_spl|~sQ4_spl|~sQ6_spl),
% 35.16/4.95 inference(backward_demodulation,[status(thm)],[f3953,f3389])).
% 35.16/4.95 fof(f4508,plain,(
% 35.16/4.95 ~sdtpldt0(xx,xy)=sdtpldt0(xk,sdtpldt0(xy,xl))|~sQ1_spl|~sQ5_spl|~sQ7_spl|~sQ3_spl|~sQ4_spl|~sQ6_spl),
% 35.16/4.95 inference(backward_demodulation,[status(thm)],[f4306,f3388])).
% 35.16/4.95 fof(f4909,definition,(
% 35.16/4.95 sQ101_spl <=> (aElement0(sdtpldt0(sz10,sdtpldt0(sz10,sz10))))),
% 35.16/4.95 introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition])).
% 35.16/4.95 fof(f4911,plain,(
% 35.16/4.95 ~aElement0(sdtpldt0(sz10,sdtpldt0(sz10,sz10)))|sQ101_spl),
% 35.16/4.95 inference(component_clause,[status(thm)],[f4909])).
% 35.16/4.95 fof(f6304,plain,(
% 35.16/4.95 $false|sQ17_spl),
% 35.16/4.95 inference(forward_subsumption_resolution,[status(thm)],[f395,f173])).
% 35.16/4.95 fof(f6305,plain,(
% 35.16/4.95 sQ17_spl),
% 35.16/4.95 inference(contradiction_clause,[status(thm)],[f6304])).
% 35.16/4.95 fof(f6306,plain,(
% 35.16/4.95 $false|sQ101_spl),
% 35.16/4.95 inference(forward_subsumption_resolution,[status(thm)],[f4911,f326])).
% 35.16/4.95 fof(f6307,plain,(
% 35.16/4.95 sQ101_spl),
% 35.16/4.95 inference(contradiction_clause,[status(thm)],[f6306])).
% 35.16/4.95 fof(f6308,plain,(
% 35.16/4.95 $false|sQ72_spl),
% 35.16/4.95 inference(forward_subsumption_resolution,[status(thm)],[f2257,f122])).
% 35.16/4.95 fof(f6309,plain,(
% 35.16/4.95 sQ72_spl),
% 35.16/4.95 inference(contradiction_clause,[status(thm)],[f6308])).
% 35.16/4.95 fof(f6947,definition,(
% 35.16/4.95 sQ142_spl <=> (aElement0(sdtpldt0(sz10,sdtpldt0(sz10,sdtpldt0(sz10,sz10)))))),
% 35.16/4.95 introduced(definition,[new_symbols(definition,[sQ142_spl])],[split_symbol_definition])).
% 35.16/4.95 fof(f6949,plain,(
% 35.16/4.95 ~aElement0(sdtpldt0(sz10,sdtpldt0(sz10,sdtpldt0(sz10,sz10))))|sQ142_spl),
% 35.16/4.95 inference(component_clause,[status(thm)],[f6947])).
% 35.16/4.95 fof(f6957,plain,(
% 35.16/4.95 $false|sQ142_spl),
% 35.16/4.95 inference(forward_subsumption_resolution,[status(thm)],[f6949,f744])).
% 35.16/4.95 fof(f6958,plain,(
% 35.16/4.95 sQ142_spl),
% 35.16/4.95 inference(contradiction_clause,[status(thm)],[f6957])).
% 35.16/4.95 fof(f7988,plain,(
% 35.16/4.95 $false|~sQ48_spl),
% 35.16/4.95 inference(forward_subsumption_resolution,[status(thm)],[f603,f72])).
% 35.16/4.95 fof(f7989,plain,(
% 35.16/4.95 ~sQ48_spl),
% 35.16/4.95 inference(contradiction_clause,[status(thm)],[f7988])).
% 35.16/4.95 fof(f7990,plain,(
% 35.16/4.95 $false|sQ47_spl),
% 35.16/4.95 inference(forward_subsumption_resolution,[status(thm)],[f601,f37])).
% 35.16/4.95 fof(f7991,plain,(
% 35.16/4.95 sQ47_spl),
% 35.16/4.95 inference(contradiction_clause,[status(thm)],[f7990])).
% 35.16/4.95 fof(f9607,plain,(
% 35.16/4.95 aElement0(sdtpldt0(xm,xn))|~sQ5_spl|~sQ4_spl),
% 35.16/4.95 inference(resolution,[status(thm)],[f1087,f274])).
% 35.16/4.95 fof(f9627,plain,(
% 35.16/4.95 aElement0(xy)|~sQ5_spl|~sQ4_spl),
% 35.16/4.95 inference(forward_demodulation,[status(thm)],[f128,f9607])).
% 35.16/4.95 fof(f9838,plain,(
% 35.16/4.95 ![X0]: (~aElement0(X0)|sdtpldt0(sdtpldt0(X0,xl),xy)=sdtpldt0(X0,sdtpldt0(xl,xy))|~sQ5_spl|~sQ4_spl|~sQ6_spl)),
% 35.16/4.95 inference(resolution,[status(thm)],[f9627,f1272])).
% 35.16/4.95 fof(f9929,plain,(
% 35.16/4.95 ![X0]: (~aElement0(X0)|sdtpldt0(sdtpldt0(X0,xl),xy)=sdtpldt0(X0,sdtpldt0(xy,xl))|~sQ5_spl|~sQ4_spl|~sQ6_spl)),
% 35.16/4.95 inference(forward_demodulation,[status(thm)],[f2203,f9838])).
% 35.16/4.95 fof(f10472,plain,(
% 35.16/4.95 sdtpldt0(sdtpldt0(xk,xl),xy)=sdtpldt0(xk,sdtpldt0(xy,xl))|~sQ5_spl|~sQ4_spl|~sQ6_spl|~sQ7_spl),
% 35.16/4.95 inference(resolution,[status(thm)],[f9929,f286])).
% 35.16/4.97 fof(f10492,plain,(
% 35.16/4.97 sdtpldt0(xx,xy)=sdtpldt0(xk,sdtpldt0(xy,xl))|~sQ5_spl|~sQ4_spl|~sQ6_spl|~sQ7_spl),
% 35.16/4.97 inference(forward_demodulation,[status(thm)],[f125,f10472])).
% 35.16/4.97 fof(f10493,plain,(
% 35.16/4.97 $false|~sQ1_spl|~sQ3_spl|~sQ5_spl|~sQ4_spl|~sQ6_spl|~sQ7_spl),
% 35.16/4.97 inference(forward_subsumption_resolution,[status(thm)],[f10492,f4508])).
% 35.16/4.97 fof(f10494,plain,(
% 35.16/4.97 ~sQ1_spl|~sQ3_spl|~sQ5_spl|~sQ4_spl|~sQ6_spl|~sQ7_spl),
% 35.16/4.97 inference(contradiction_clause,[status(thm)],[f10493])).
% 35.16/4.97 fof(f10495,plain,(
% 35.16/4.97 $false),
% 35.16/4.97 inference(sat_refutation,[status(thm)],[f265,f272,f276,f280,f284,f288,f1015,f1018,f1663,f2487,f6305,f6307,f6309,f6958,f7989,f7991,f10494])).
% 35.16/4.97 % SZS output end CNFRefutation for theBenchmark.p
% 0.77/5.00 % Elapsed time: 4.536893 seconds
% 0.77/5.00 % CPU time: 35.605656 seconds
% 0.77/5.00 % Total memory used: 407.683 MB
% 0.77/5.00 % Net memory used: 381.124 MB
%------------------------------------------------------------------------------