%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : RNG090+2 : 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 : n017.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 18.12s 2.75s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG090+2 : 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/0.37 % Computer : n017.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 04:14:26 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.39 % Drodi V4.1.1
% 18.12/2.75 % Refutation found
% 18.12/2.75 % SZS status Theorem for theBenchmark: Theorem is valid
% 18.12/2.75 % SZS output start CNFRefutation for theBenchmark
% 18.12/2.75 fof(f2,axiom,(
% 18.12/2.75 aElement0(sz00) ),
% 18.12/2.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.12/2.75 fof(f5,axiom,(
% 18.12/2.75 (! [W0,W1] :( ( aElement0(W0)& aElement0(W1) )=> aElement0(sdtpldt0(W0,W1)) ) )),
% 18.12/2.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.12/2.75 fof(f7,axiom,(
% 18.12/2.75 (! [W0,W1] :( ( aElement0(W0)& aElement0(W1) )=> sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) )),
% 18.12/2.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.12/2.75 fof(f8,axiom,(
% 18.12/2.75 (! [W0,W1,W2] :( ( aElement0(W0)& aElement0(W1)& aElement0(W2) )=> sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2)) ) )),
% 18.12/2.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.12/2.75 fof(f20,axiom,(
% 18.12/2.75 (! [W0] :( aSet0(W0)=> (! [W1] :( aElementOf0(W1,W0)=> aElement0(W1) ) )) )),
% 18.12/2.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.12/2.75 fof(f25,hypothesis,(
% 18.12/2.75 ( aSet0(xI)& (! [W0] :( aElementOf0(W0,xI)=> ( (! [W1] :( aElementOf0(W1,xI)=> aElementOf0(sdtpldt0(W0,W1),xI) ))& (! [W1] :( aElement0(W1)=> aElementOf0(sdtasdt0(W1,W0),xI) ) )) ))& aIdeal0(xI)& aSet0(xJ)& (! [W0] :( aElementOf0(W0,xJ)=> ( (! [W1] :( aElementOf0(W1,xJ)=> aElementOf0(sdtpldt0(W0,W1),xJ) ))& (! [W1] :( aElement0(W1)=> aElementOf0(sdtasdt0(W1,W0),xJ) ) )) ))& aIdeal0(xJ) ) ),
% 18.12/2.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.12/2.75 fof(f27,hypothesis,(
% 18.12/2.75 ( aElementOf0(xk,xI)& aElementOf0(xl,xJ)& xx = sdtpldt0(xk,xl) ) ),
% 18.12/2.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.12/2.75 fof(f28,hypothesis,(
% 18.12/2.75 ( aElementOf0(xm,xI)& aElementOf0(xn,xJ)& xy = sdtpldt0(xm,xn) ) ),
% 18.12/2.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.12/2.75 fof(f29,hypothesis,(
% 18.12/2.75 ( aElementOf0(sdtpldt0(xk,xm),xI)& aElementOf0(sdtpldt0(xl,xn),xJ) ) ),
% 18.12/2.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.12/2.75 fof(f31,conjecture,(
% 18.12/2.75 sdtpldt0(xx,xy) = sdtpldt0(sdtpldt0(xk,xm),sdtpldt0(xl,xn)) ),
% 18.12/2.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.12/2.75 fof(f32,negated_conjecture,(
% 18.12/2.75 ~(sdtpldt0(xx,xy) = sdtpldt0(sdtpldt0(xk,xm),sdtpldt0(xl,xn)) )),
% 18.12/2.75 inference(negated_conjecture,[status(cth)],[f31])).
% 18.12/2.75 fof(f36,plain,(
% 18.12/2.75 aElement0(sz00)),
% 18.12/2.75 inference(cnf_transformation,[status(thm)],[f2])).
% 18.12/2.75 fof(f40,plain,(
% 18.12/2.75 ![W0,W1]: ((~aElement0(W0)|~aElement0(W1))|aElement0(sdtpldt0(W0,W1)))),
% 18.12/2.75 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 18.12/2.75 fof(f41,plain,(
% 18.12/2.75 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|aElement0(sdtpldt0(X0,X1)))),
% 18.12/2.75 inference(cnf_transformation,[status(thm)],[f40])).
% 18.12/2.75 fof(f44,plain,(
% 18.12/2.75 ![W0,W1]: ((~aElement0(W0)|~aElement0(W1))|sdtpldt0(W0,W1)=sdtpldt0(W1,W0))),
% 18.12/2.75 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 18.12/2.75 fof(f45,plain,(
% 18.12/2.75 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|sdtpldt0(X0,X1)=sdtpldt0(X1,X0))),
% 18.12/2.75 inference(cnf_transformation,[status(thm)],[f44])).
% 18.12/2.75 fof(f46,plain,(
% 18.12/2.75 ![W0,W1,W2]: (((~aElement0(W0)|~aElement0(W1))|~aElement0(W2))|sdtpldt0(sdtpldt0(W0,W1),W2)=sdtpldt0(W0,sdtpldt0(W1,W2)))),
% 18.12/2.75 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 18.12/2.75 fof(f47,plain,(
% 18.12/2.75 ![X0,X1,X2]: (~aElement0(X0)|~aElement0(X1)|~aElement0(X2)|sdtpldt0(sdtpldt0(X0,X1),X2)=sdtpldt0(X0,sdtpldt0(X1,X2)))),
% 18.12/2.75 inference(cnf_transformation,[status(thm)],[f46])).
% 18.12/2.75 fof(f76,plain,(
% 18.12/2.75 ![W0]: (~aSet0(W0)|(![W1]: (~aElementOf0(W1,W0)|aElement0(W1))))),
% 18.12/2.75 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 18.12/2.75 fof(f77,plain,(
% 18.12/2.75 ![X0,X1]: (~aSet0(X0)|~aElementOf0(X1,X0)|aElement0(X1))),
% 18.12/2.75 inference(cnf_transformation,[status(thm)],[f76])).
% 18.12/2.75 fof(f118,plain,(
% 18.12/2.75 ((((aSet0(xI)&(![W0]: (~aElementOf0(W0,xI)|((![W1]: (~aElementOf0(W1,xI)|aElementOf0(sdtpldt0(W0,W1),xI)))&(![W1]: (~aElement0(W1)|aElementOf0(sdtasdt0(W1,W0),xI)))))))&aIdeal0(xI))&aSet0(xJ))&(![W0]: (~aElementOf0(W0,xJ)|((![W1]: (~aElementOf0(W1,xJ)|aElementOf0(sdtpldt0(W0,W1),xJ)))&(![W1]: (~aElement0(W1)|aElementOf0(sdtasdt0(W1,W0),xJ)))))))&aIdeal0(xJ)),
% 18.12/2.75 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 18.12/2.75 fof(f119,plain,(
% 18.12/2.75 aSet0(xI)),
% 18.12/2.75 inference(cnf_transformation,[status(thm)],[f118])).
% 18.12/2.75 fof(f123,plain,(
% 18.12/2.75 aSet0(xJ)),
% 18.12/2.75 inference(cnf_transformation,[status(thm)],[f118])).
% 18.12/2.75 fof(f126,plain,(
% 18.12/2.75 aIdeal0(xJ)),
% 18.12/2.75 inference(cnf_transformation,[status(thm)],[f118])).
% 18.12/2.75 fof(f137,plain,(
% 18.12/2.75 aElementOf0(xk,xI)),
% 18.12/2.75 inference(cnf_transformation,[status(thm)],[f27])).
% 18.12/2.75 fof(f138,plain,(
% 18.12/2.75 aElementOf0(xl,xJ)),
% 18.12/2.75 inference(cnf_transformation,[status(thm)],[f27])).
% 18.12/2.75 fof(f139,plain,(
% 18.12/2.75 xx=sdtpldt0(xk,xl)),
% 18.12/2.75 inference(cnf_transformation,[status(thm)],[f27])).
% 18.12/2.75 fof(f140,plain,(
% 18.12/2.75 aElementOf0(xm,xI)),
% 18.12/2.75 inference(cnf_transformation,[status(thm)],[f28])).
% 18.12/2.75 fof(f141,plain,(
% 18.12/2.75 aElementOf0(xn,xJ)),
% 18.12/2.75 inference(cnf_transformation,[status(thm)],[f28])).
% 18.12/2.75 fof(f142,plain,(
% 18.12/2.75 xy=sdtpldt0(xm,xn)),
% 18.12/2.75 inference(cnf_transformation,[status(thm)],[f28])).
% 18.12/2.75 fof(f143,plain,(
% 18.12/2.75 aElementOf0(sdtpldt0(xk,xm),xI)),
% 18.12/2.75 inference(cnf_transformation,[status(thm)],[f29])).
% 18.12/2.75 fof(f144,plain,(
% 18.12/2.75 aElementOf0(sdtpldt0(xl,xn),xJ)),
% 18.12/2.75 inference(cnf_transformation,[status(thm)],[f29])).
% 18.12/2.75 fof(f147,plain,(
% 18.12/2.75 ~sdtpldt0(xx,xy)=sdtpldt0(sdtpldt0(xk,xm),sdtpldt0(xl,xn))),
% 18.12/2.75 inference(cnf_transformation,[status(thm)],[f32])).
% 18.12/2.75 fof(f265,plain,(
% 18.12/2.75 ~aSet0(xJ)|aElement0(sdtpldt0(xl,xn))),
% 18.12/2.75 inference(resolution,[status(thm)],[f77,f144])).
% 18.12/2.75 fof(f266,plain,(
% 18.12/2.75 ~aSet0(xI)|aElement0(sdtpldt0(xk,xm))),
% 18.12/2.75 inference(resolution,[status(thm)],[f77,f143])).
% 18.12/2.75 fof(f267,plain,(
% 18.12/2.75 ~aSet0(xJ)|aElement0(xn)),
% 18.12/2.75 inference(resolution,[status(thm)],[f77,f141])).
% 18.12/2.75 fof(f268,plain,(
% 18.12/2.75 ~aSet0(xI)|aElement0(xm)),
% 18.12/2.75 inference(resolution,[status(thm)],[f77,f140])).
% 18.12/2.75 fof(f269,plain,(
% 18.12/2.75 ~aSet0(xJ)|aElement0(xl)),
% 18.12/2.75 inference(resolution,[status(thm)],[f77,f138])).
% 18.12/2.75 fof(f270,plain,(
% 18.12/2.75 ~aSet0(xI)|aElement0(xk)),
% 18.12/2.75 inference(resolution,[status(thm)],[f77,f137])).
% 18.12/2.75 fof(f273,definition,(
% 18.12/2.75 sQ0_spl <=> (aSet0(xJ))),
% 18.12/2.75 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 18.12/2.75 fof(f275,plain,(
% 18.12/2.75 ~aSet0(xJ)|sQ0_spl),
% 18.12/2.75 inference(component_clause,[status(thm)],[f273])).
% 18.12/2.75 fof(f276,definition,(
% 18.12/2.75 sQ1_spl <=> (aElement0(sdtpldt0(xl,xn)))),
% 18.12/2.75 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 18.12/2.75 fof(f277,plain,(
% 18.12/2.75 aElement0(sdtpldt0(xl,xn))|~sQ1_spl),
% 18.12/2.75 inference(component_clause,[status(thm)],[f276])).
% 18.12/2.75 fof(f279,plain,(
% 18.12/2.75 ~sQ0_spl|sQ1_spl),
% 18.12/2.75 inference(split_clause,[status(thm)],[f265,f273,f276])).
% 18.12/2.75 fof(f280,definition,(
% 18.12/2.75 sQ2_spl <=> (aSet0(xI))),
% 18.12/2.75 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 18.12/2.75 fof(f282,plain,(
% 18.12/2.75 ~aSet0(xI)|sQ2_spl),
% 18.12/2.75 inference(component_clause,[status(thm)],[f280])).
% 18.12/2.75 fof(f283,definition,(
% 18.12/2.75 sQ3_spl <=> (aElement0(sdtpldt0(xk,xm)))),
% 18.12/2.75 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 18.12/2.75 fof(f284,plain,(
% 18.12/2.75 aElement0(sdtpldt0(xk,xm))|~sQ3_spl),
% 18.12/2.75 inference(component_clause,[status(thm)],[f283])).
% 18.12/2.75 fof(f286,plain,(
% 18.12/2.75 ~sQ2_spl|sQ3_spl),
% 18.12/2.75 inference(split_clause,[status(thm)],[f266,f280,f283])).
% 18.12/2.75 fof(f287,definition,(
% 18.12/2.75 sQ4_spl <=> (aElement0(xn))),
% 18.12/2.75 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 18.12/2.75 fof(f288,plain,(
% 18.12/2.75 aElement0(xn)|~sQ4_spl),
% 18.12/2.75 inference(component_clause,[status(thm)],[f287])).
% 18.12/2.75 fof(f290,plain,(
% 18.12/2.75 ~sQ0_spl|sQ4_spl),
% 18.12/2.75 inference(split_clause,[status(thm)],[f267,f273,f287])).
% 18.12/2.75 fof(f291,definition,(
% 18.12/2.75 sQ5_spl <=> (aElement0(xm))),
% 18.12/2.75 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 18.12/2.75 fof(f292,plain,(
% 18.12/2.75 aElement0(xm)|~sQ5_spl),
% 18.12/2.75 inference(component_clause,[status(thm)],[f291])).
% 18.12/2.75 fof(f294,plain,(
% 18.12/2.75 ~sQ2_spl|sQ5_spl),
% 18.12/2.75 inference(split_clause,[status(thm)],[f268,f280,f291])).
% 18.12/2.75 fof(f295,definition,(
% 18.12/2.75 sQ6_spl <=> (aElement0(xl))),
% 18.12/2.75 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 18.12/2.75 fof(f296,plain,(
% 18.12/2.75 aElement0(xl)|~sQ6_spl),
% 18.12/2.75 inference(component_clause,[status(thm)],[f295])).
% 18.12/2.75 fof(f298,plain,(
% 18.12/2.75 ~sQ0_spl|sQ6_spl),
% 18.12/2.75 inference(split_clause,[status(thm)],[f269,f273,f295])).
% 18.12/2.75 fof(f299,definition,(
% 18.12/2.75 sQ7_spl <=> (aElement0(xk))),
% 18.12/2.75 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 18.12/2.75 fof(f300,plain,(
% 18.12/2.75 aElement0(xk)|~sQ7_spl),
% 18.12/2.75 inference(component_clause,[status(thm)],[f299])).
% 18.12/2.75 fof(f302,plain,(
% 18.12/2.75 ~sQ2_spl|sQ7_spl),
% 18.12/2.75 inference(split_clause,[status(thm)],[f270,f280,f299])).
% 18.12/2.75 fof(f367,definition,(
% 18.12/2.75 sQ11_spl <=> (aElement0(sz00))),
% 18.12/2.75 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 18.12/2.75 fof(f369,plain,(
% 18.12/2.75 ~aElement0(sz00)|sQ11_spl),
% 18.12/2.75 inference(component_clause,[status(thm)],[f367])).
% 18.12/2.75 fof(f511,definition,(
% 18.12/2.75 sQ28_spl <=> (aIdeal0(xJ))),
% 18.12/2.75 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 18.12/2.75 fof(f513,plain,(
% 18.12/2.75 ~aIdeal0(xJ)|sQ28_spl),
% 18.12/2.75 inference(component_clause,[status(thm)],[f511])).
% 18.12/2.75 fof(f626,plain,(
% 18.12/2.75 $false|sQ2_spl),
% 18.12/2.75 inference(forward_subsumption_resolution,[status(thm)],[f119,f282])).
% 18.12/2.75 fof(f627,plain,(
% 18.12/2.75 sQ2_spl),
% 18.12/2.75 inference(contradiction_clause,[status(thm)],[f626])).
% 18.12/2.75 fof(f672,plain,(
% 18.12/2.75 ![X0]: (~aElement0(X0)|sdtpldt0(X0,xm)=sdtpldt0(xm,X0)|~sQ5_spl)),
% 18.12/2.75 inference(resolution,[status(thm)],[f292,f45])).
% 18.12/2.75 fof(f674,plain,(
% 18.12/2.75 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|sdtpldt0(sdtpldt0(X0,X1),xm)=sdtpldt0(X0,sdtpldt0(X1,xm))|~sQ5_spl)),
% 18.12/2.75 inference(resolution,[status(thm)],[f292,f47])).
% 18.12/2.75 fof(f676,plain,(
% 18.12/2.75 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|sdtpldt0(sdtpldt0(X0,xm),X1)=sdtpldt0(X0,sdtpldt0(xm,X1))|~sQ5_spl)),
% 18.12/2.75 inference(resolution,[status(thm)],[f292,f47])).
% 18.12/2.75 fof(f677,plain,(
% 18.12/2.75 ![X0]: (~aElement0(X0)|aElement0(sdtpldt0(xm,X0))|~sQ5_spl)),
% 18.12/2.75 inference(resolution,[status(thm)],[f292,f41])).
% 18.12/2.75 fof(f722,plain,(
% 18.12/2.75 ![X0]: (~aElement0(X0)|sdtpldt0(X0,xk)=sdtpldt0(xk,X0)|~sQ7_spl)),
% 18.12/2.75 inference(resolution,[status(thm)],[f300,f45])).
% 18.12/2.75 fof(f724,plain,(
% 18.12/2.75 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|sdtpldt0(sdtpldt0(X0,X1),xk)=sdtpldt0(X0,sdtpldt0(X1,xk))|~sQ7_spl)),
% 18.12/2.75 inference(resolution,[status(thm)],[f300,f47])).
% 18.12/2.75 fof(f726,plain,(
% 18.12/2.75 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|sdtpldt0(sdtpldt0(X0,xk),X1)=sdtpldt0(X0,sdtpldt0(xk,X1))|~sQ7_spl)),
% 18.12/2.75 inference(resolution,[status(thm)],[f300,f47])).
% 18.12/2.75 fof(f728,plain,(
% 18.12/2.75 sdtpldt0(xk,xm)=sdtpldt0(xm,xk)|~sQ5_spl|~sQ7_spl),
% 18.12/2.75 inference(resolution,[status(thm)],[f672,f300])).
% 18.12/2.75 fof(f740,plain,(
% 18.12/2.75 ![X0]: (~aElement0(X0)|sdtpldt0(sdtpldt0(X0,xk),xm)=sdtpldt0(X0,sdtpldt0(xk,xm))|~sQ5_spl|~sQ7_spl)),
% 18.12/2.75 inference(resolution,[status(thm)],[f674,f300])).
% 18.12/2.75 fof(f754,plain,(
% 18.12/2.75 ![X0]: (~aElement0(X0)|sdtpldt0(sdtpldt0(X0,xm),xk)=sdtpldt0(X0,sdtpldt0(xm,xk))|~sQ5_spl|~sQ7_spl)),
% 18.12/2.75 inference(resolution,[status(thm)],[f676,f300])).
% 18.12/2.75 fof(f815,plain,(
% 18.12/2.75 ![X0]: (~aElement0(X0)|sdtpldt0(X0,sdtpldt0(xk,xm))=sdtpldt0(sdtpldt0(xk,xm),X0)|~sQ3_spl)),
% 18.12/2.75 inference(resolution,[status(thm)],[f284,f45])).
% 18.12/2.75 fof(f861,plain,(
% 18.12/2.75 ![X0]: (~aElement0(X0)|sdtpldt0(sdtpldt0(X0,xm),xk)=sdtpldt0(X0,sdtpldt0(xk,xm))|~sQ5_spl|~sQ7_spl)),
% 18.12/2.75 inference(forward_demodulation,[status(thm)],[f728,f754])).
% 18.12/2.75 fof(f899,plain,(
% 18.12/2.75 $false|sQ0_spl),
% 18.12/2.75 inference(forward_subsumption_resolution,[status(thm)],[f123,f275])).
% 18.12/2.75 fof(f900,plain,(
% 18.12/2.75 sQ0_spl),
% 18.12/2.75 inference(contradiction_clause,[status(thm)],[f899])).
% 18.12/2.75 fof(f995,plain,(
% 18.12/2.75 $false|sQ28_spl),
% 18.12/2.75 inference(forward_subsumption_resolution,[status(thm)],[f126,f513])).
% 18.12/2.75 fof(f996,plain,(
% 18.12/2.75 sQ28_spl),
% 18.12/2.75 inference(contradiction_clause,[status(thm)],[f995])).
% 18.12/2.75 fof(f1063,plain,(
% 18.12/2.75 ![X0]: (~aElement0(X0)|sdtpldt0(sdtpldt0(X0,xk),xn)=sdtpldt0(X0,sdtpldt0(xk,xn))|~sQ4_spl|~sQ7_spl)),
% 18.12/2.75 inference(resolution,[status(thm)],[f288,f726])).
% 18.12/2.75 fof(f1064,plain,(
% 18.12/2.75 ![X0]: (~aElement0(X0)|sdtpldt0(sdtpldt0(X0,xn),xk)=sdtpldt0(X0,sdtpldt0(xn,xk))|~sQ4_spl|~sQ7_spl)),
% 18.12/2.75 inference(resolution,[status(thm)],[f288,f724])).
% 18.12/2.75 fof(f1066,plain,(
% 18.12/2.75 sdtpldt0(xn,xk)=sdtpldt0(xk,xn)|~sQ4_spl|~sQ7_spl),
% 18.12/2.75 inference(resolution,[status(thm)],[f288,f722])).
% 18.12/2.75 fof(f1067,plain,(
% 18.12/2.75 ![X0]: (~aElement0(X0)|sdtpldt0(sdtpldt0(X0,xm),xn)=sdtpldt0(X0,sdtpldt0(xm,xn))|~sQ4_spl|~sQ5_spl)),
% 18.12/2.75 inference(resolution,[status(thm)],[f288,f676])).
% 18.12/2.75 fof(f1068,plain,(
% 18.12/2.75 ![X0]: (~aElement0(X0)|sdtpldt0(sdtpldt0(X0,xn),xm)=sdtpldt0(X0,sdtpldt0(xn,xm))|~sQ4_spl|~sQ5_spl)),
% 18.12/2.75 inference(resolution,[status(thm)],[f288,f674])).
% 18.12/2.75 fof(f1070,plain,(
% 18.12/2.75 sdtpldt0(xn,xm)=sdtpldt0(xm,xn)|~sQ4_spl|~sQ5_spl),
% 18.12/2.75 inference(resolution,[status(thm)],[f288,f672])).
% 18.12/2.75 fof(f1115,plain,(
% 18.12/2.75 ![X0]: (~aElement0(X0)|sdtpldt0(X0,xn)=sdtpldt0(xn,X0)|~sQ4_spl)),
% 18.12/2.75 inference(resolution,[status(thm)],[f288,f45])).
% 18.12/2.75 fof(f1117,plain,(
% 18.12/2.75 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|sdtpldt0(sdtpldt0(X0,X1),xn)=sdtpldt0(X0,sdtpldt0(X1,xn))|~sQ4_spl)),
% 18.12/2.75 inference(resolution,[status(thm)],[f288,f47])).
% 18.12/2.75 fof(f1121,plain,(
% 18.12/2.75 ![X0]: (~aElement0(X0)|sdtpldt0(sdtpldt0(X0,xm),xn)=sdtpldt0(X0,xy)|~sQ4_spl|~sQ5_spl)),
% 18.12/2.75 inference(forward_demodulation,[status(thm)],[f142,f1067])).
% 18.12/2.75 fof(f1122,plain,(
% 18.12/2.75 sdtpldt0(xn,xm)=xy|~sQ4_spl|~sQ5_spl),
% 18.12/2.75 inference(forward_demodulation,[status(thm)],[f142,f1070])).
% 18.12/2.75 fof(f1134,plain,(
% 18.12/2.75 sdtpldt0(xl,sdtpldt0(xk,xm))=sdtpldt0(sdtpldt0(xk,xm),xl)|~sQ6_spl|~sQ3_spl),
% 18.12/2.75 inference(resolution,[status(thm)],[f296,f815])).
% 18.12/2.75 fof(f1138,plain,(
% 18.12/2.75 sdtpldt0(sdtpldt0(xl,xk),xm)=sdtpldt0(xl,sdtpldt0(xk,xm))|~sQ6_spl|~sQ5_spl|~sQ7_spl),
% 18.12/2.75 inference(resolution,[status(thm)],[f296,f740])).
% 18.12/2.75 fof(f1142,plain,(
% 18.12/2.75 sdtpldt0(xl,xk)=sdtpldt0(xk,xl)|~sQ6_spl|~sQ7_spl),
% 18.12/2.75 inference(resolution,[status(thm)],[f296,f722])).
% 18.12/2.75 fof(f1143,plain,(
% 18.12/2.75 ![X0]: (~aElement0(X0)|sdtpldt0(sdtpldt0(X0,xm),xl)=sdtpldt0(X0,sdtpldt0(xm,xl))|~sQ6_spl|~sQ5_spl)),
% 18.12/2.75 inference(resolution,[status(thm)],[f296,f676])).
% 18.12/2.75 fof(f1144,plain,(
% 18.12/2.75 ![X0]: (~aElement0(X0)|sdtpldt0(sdtpldt0(X0,xl),xm)=sdtpldt0(X0,sdtpldt0(xl,xm))|~sQ6_spl|~sQ5_spl)),
% 18.12/2.75 inference(resolution,[status(thm)],[f296,f674])).
% 18.12/2.75 fof(f1146,plain,(
% 18.12/2.75 sdtpldt0(xl,xm)=sdtpldt0(xm,xl)|~sQ6_spl|~sQ5_spl),
% 18.12/2.75 inference(resolution,[status(thm)],[f296,f672])).
% 18.12/2.75 fof(f1195,plain,(
% 18.12/2.75 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|sdtpldt0(sdtpldt0(X0,xl),X1)=sdtpldt0(X0,sdtpldt0(xl,X1))|~sQ6_spl)),
% 18.12/2.75 inference(resolution,[status(thm)],[f296,f47])).
% 18.12/2.75 fof(f1198,plain,(
% 18.12/2.75 sdtpldt0(xl,xk)=xx|~sQ6_spl|~sQ7_spl),
% 18.12/2.75 inference(forward_demodulation,[status(thm)],[f139,f1142])).
% 18.12/2.75 fof(f1352,plain,(
% 18.12/2.75 sdtpldt0(sdtpldt0(xl,xk),xn)=sdtpldt0(xl,sdtpldt0(xk,xn))|~sQ4_spl|~sQ7_spl|~sQ6_spl),
% 18.12/2.75 inference(resolution,[status(thm)],[f1063,f296])).
% 18.12/2.75 fof(f1365,plain,(
% 18.12/2.75 sdtpldt0(sdtpldt0(xl,xn),xk)=sdtpldt0(xl,sdtpldt0(xn,xk))|~sQ4_spl|~sQ7_spl|~sQ6_spl),
% 18.12/2.75 inference(resolution,[status(thm)],[f1064,f296])).
% 18.12/2.75 fof(f1383,plain,(
% 18.12/2.75 sdtpldt0(sdtpldt0(xl,xm),xn)=sdtpldt0(xl,xy)|~sQ4_spl|~sQ5_spl|~sQ6_spl),
% 18.12/2.75 inference(resolution,[status(thm)],[f1121,f296])).
% 18.12/2.75 fof(f1515,plain,(
% 18.12/2.75 sdtpldt0(sdtpldt0(xl,xn),xm)=sdtpldt0(xl,sdtpldt0(xn,xm))|~sQ4_spl|~sQ5_spl|~sQ6_spl),
% 18.12/2.75 inference(resolution,[status(thm)],[f1068,f296])).
% 18.12/2.75 fof(f1545,plain,(
% 18.12/2.75 sdtpldt0(xl,xn)=sdtpldt0(xn,xl)|~sQ4_spl|~sQ6_spl),
% 18.12/2.75 inference(resolution,[status(thm)],[f1115,f296])).
% 18.12/2.75 fof(f1572,plain,(
% 18.12/2.75 ![X0]: (~aElement0(X0)|sdtpldt0(sdtpldt0(X0,xl),xn)=sdtpldt0(X0,sdtpldt0(xl,xn))|~sQ4_spl|~sQ6_spl)),
% 18.12/2.75 inference(resolution,[status(thm)],[f1117,f296])).
% 18.12/2.75 fof(f1639,plain,(
% 18.12/2.75 sdtpldt0(xx,xm)=sdtpldt0(xl,sdtpldt0(xk,xm))|~sQ6_spl|~sQ5_spl|~sQ7_spl),
% 18.12/2.75 inference(backward_demodulation,[status(thm)],[f1198,f1138])).
% 18.12/2.75 fof(f1647,plain,(
% 18.12/2.75 sdtpldt0(sdtpldt0(xn,xm),xl)=sdtpldt0(xn,sdtpldt0(xm,xl))|~sQ6_spl|~sQ5_spl|~sQ4_spl),
% 18.12/2.75 inference(resolution,[status(thm)],[f1143,f288])).
% 18.12/2.75 fof(f1654,plain,(
% 18.12/2.75 sdtpldt0(xy,xl)=sdtpldt0(xn,sdtpldt0(xm,xl))|~sQ6_spl|~sQ5_spl|~sQ4_spl),
% 18.12/2.75 inference(forward_demodulation,[status(thm)],[f1122,f1647])).
% 18.12/2.75 fof(f1661,plain,(
% 18.12/2.75 sdtpldt0(sdtpldt0(xn,xl),xm)=sdtpldt0(xn,sdtpldt0(xl,xm))|~sQ6_spl|~sQ5_spl|~sQ4_spl),
% 18.12/2.75 inference(resolution,[status(thm)],[f1144,f288])).
% 18.12/2.75 fof(f1890,plain,(
% 18.12/2.75 sdtpldt0(xx,xn)=sdtpldt0(xl,sdtpldt0(xk,xn))|~sQ4_spl|~sQ7_spl|~sQ6_spl),
% 18.12/2.75 inference(forward_demodulation,[status(thm)],[f1198,f1352])).
% 18.12/2.75 fof(f1895,plain,(
% 18.12/2.75 sdtpldt0(sdtpldt0(xl,xn),xk)=sdtpldt0(xl,sdtpldt0(xk,xn))|~sQ4_spl|~sQ7_spl|~sQ6_spl),
% 18.12/2.75 inference(forward_demodulation,[status(thm)],[f1066,f1365])).
% 18.12/2.75 fof(f1896,plain,(
% 18.12/2.75 sdtpldt0(sdtpldt0(xl,xn),xk)=sdtpldt0(xx,xn)|~sQ4_spl|~sQ7_spl|~sQ6_spl),
% 18.12/2.75 inference(forward_demodulation,[status(thm)],[f1890,f1895])).
% 18.12/2.75 fof(f1978,plain,(
% 18.12/2.75 sdtpldt0(sdtpldt0(xl,xn),sdtpldt0(xk,xm))=sdtpldt0(sdtpldt0(xk,xm),sdtpldt0(xl,xn))|~sQ1_spl|~sQ3_spl),
% 18.12/2.75 inference(resolution,[status(thm)],[f277,f815])).
% 18.12/2.75 fof(f1981,plain,(
% 18.12/2.75 sdtpldt0(sdtpldt0(sdtpldt0(xl,xn),xm),xk)=sdtpldt0(sdtpldt0(xl,xn),sdtpldt0(xk,xm))|~sQ1_spl|~sQ5_spl|~sQ7_spl),
% 18.12/2.75 inference(resolution,[status(thm)],[f277,f861])).
% 18.12/2.75 fof(f1983,plain,(
% 18.12/2.75 ![X0]: (~aElement0(X0)|sdtpldt0(sdtpldt0(X0,xk),sdtpldt0(xl,xn))=sdtpldt0(X0,sdtpldt0(xk,sdtpldt0(xl,xn)))|~sQ1_spl|~sQ7_spl)),
% 18.12/2.75 inference(resolution,[status(thm)],[f277,f726])).
% 18.12/2.75 fof(f1984,plain,(
% 18.12/2.75 ![X0]: (~aElement0(X0)|sdtpldt0(sdtpldt0(X0,sdtpldt0(xl,xn)),xk)=sdtpldt0(X0,sdtpldt0(sdtpldt0(xl,xn),xk))|~sQ1_spl|~sQ7_spl)),
% 18.12/2.75 inference(resolution,[status(thm)],[f277,f724])).
% 18.12/2.75 fof(f1986,plain,(
% 18.12/2.75 sdtpldt0(sdtpldt0(xl,xn),xk)=sdtpldt0(xk,sdtpldt0(xl,xn))|~sQ1_spl|~sQ7_spl),
% 18.12/2.75 inference(resolution,[status(thm)],[f277,f722])).
% 18.12/2.75 fof(f1987,plain,(
% 18.12/2.75 ![X0]: (~aElement0(X0)|sdtpldt0(sdtpldt0(X0,xm),sdtpldt0(xl,xn))=sdtpldt0(X0,sdtpldt0(xm,sdtpldt0(xl,xn)))|~sQ1_spl|~sQ5_spl)),
% 18.12/2.75 inference(resolution,[status(thm)],[f277,f676])).
% 18.12/2.75 fof(f1990,plain,(
% 18.12/2.75 sdtpldt0(sdtpldt0(xl,xn),xm)=sdtpldt0(xm,sdtpldt0(xl,xn))|~sQ1_spl|~sQ5_spl),
% 18.12/2.75 inference(resolution,[status(thm)],[f277,f672])).
% 18.12/2.75 fof(f2049,plain,(
% 18.12/2.75 ![X0]: (~aElement0(X0)|sdtpldt0(sdtpldt0(X0,sdtpldt0(xl,xn)),xk)=sdtpldt0(X0,sdtpldt0(xx,xn))|~sQ4_spl|~sQ6_spl|~sQ1_spl|~sQ7_spl)),
% 18.12/2.75 inference(forward_demodulation,[status(thm)],[f1896,f1984])).
% 18.12/2.75 fof(f2051,plain,(
% 18.12/2.75 sdtpldt0(xx,xn)=sdtpldt0(xk,sdtpldt0(xl,xn))|~sQ4_spl|~sQ6_spl|~sQ1_spl|~sQ7_spl),
% 18.12/2.75 inference(forward_demodulation,[status(thm)],[f1896,f1986])).
% 18.12/2.75 fof(f2234,plain,(
% 18.12/2.75 sdtpldt0(sdtpldt0(xl,xn),xm)=sdtpldt0(xl,xy)|~sQ4_spl|~sQ5_spl|~sQ6_spl),
% 18.12/2.75 inference(forward_demodulation,[status(thm)],[f1122,f1515])).
% 18.12/2.75 fof(f2313,plain,(
% 18.12/2.75 sdtpldt0(sdtpldt0(xm,xl),xn)=sdtpldt0(xm,sdtpldt0(xl,xn))|~sQ4_spl|~sQ6_spl|~sQ5_spl),
% 18.12/2.75 inference(resolution,[status(thm)],[f1572,f292])).
% 18.12/2.75 fof(f2315,plain,(
% 18.12/2.75 sdtpldt0(sdtpldt0(sdtpldt0(xk,xm),xl),xn)=sdtpldt0(sdtpldt0(xk,xm),sdtpldt0(xl,xn))|~sQ4_spl|~sQ6_spl|~sQ3_spl),
% 18.12/2.75 inference(resolution,[status(thm)],[f1572,f284])).
% 18.12/2.75 fof(f2322,plain,(
% 18.12/2.75 sdtpldt0(sdtpldt0(xl,xm),xn)=sdtpldt0(xm,sdtpldt0(xl,xn))|~sQ4_spl|~sQ6_spl|~sQ5_spl),
% 18.12/2.75 inference(forward_demodulation,[status(thm)],[f1146,f2313])).
% 18.12/2.75 fof(f2323,plain,(
% 18.12/2.75 sdtpldt0(xl,xy)=sdtpldt0(xm,sdtpldt0(xl,xn))|~sQ4_spl|~sQ6_spl|~sQ5_spl),
% 18.12/2.75 inference(forward_demodulation,[status(thm)],[f1383,f2322])).
% 18.12/2.75 fof(f2324,plain,(
% 18.12/2.75 sdtpldt0(sdtpldt0(xl,sdtpldt0(xk,xm)),xn)=sdtpldt0(sdtpldt0(xk,xm),sdtpldt0(xl,xn))|~sQ4_spl|~sQ6_spl|~sQ3_spl),
% 18.12/2.75 inference(forward_demodulation,[status(thm)],[f1134,f2315])).
% 18.12/2.75 fof(f2611,plain,(
% 18.12/2.75 sdtpldt0(xy,xl)=sdtpldt0(xn,sdtpldt0(xl,xm))|~sQ6_spl|~sQ5_spl|~sQ4_spl),
% 18.12/2.75 inference(forward_demodulation,[status(thm)],[f1146,f1654])).
% 18.12/2.75 fof(f2624,plain,(
% 18.12/2.75 sdtpldt0(sdtpldt0(xl,xn),xm)=sdtpldt0(xn,sdtpldt0(xl,xm))|~sQ6_spl|~sQ5_spl|~sQ4_spl),
% 18.12/2.75 inference(forward_demodulation,[status(thm)],[f1545,f1661])).
% 18.12/2.75 fof(f2625,plain,(
% 18.12/2.75 sdtpldt0(xl,xy)=sdtpldt0(xn,sdtpldt0(xl,xm))|~sQ6_spl|~sQ5_spl|~sQ4_spl),
% 18.12/2.75 inference(forward_demodulation,[status(thm)],[f2234,f2624])).
% 18.12/2.75 fof(f2628,plain,(
% 18.12/2.75 sdtpldt0(xl,xy)=sdtpldt0(xy,xl)|~sQ6_spl|~sQ5_spl|~sQ4_spl),
% 18.12/2.75 inference(forward_demodulation,[status(thm)],[f2611,f2625])).
% 18.12/2.75 fof(f3261,plain,(
% 18.12/2.75 sdtpldt0(sdtpldt0(sdtpldt0(xl,xn),xm),xk)=sdtpldt0(sdtpldt0(xk,xm),sdtpldt0(xl,xn))|~sQ3_spl|~sQ1_spl|~sQ5_spl|~sQ7_spl),
% 18.12/2.75 inference(forward_demodulation,[status(thm)],[f1978,f1981])).
% 18.12/2.75 fof(f3267,plain,(
% 18.12/2.75 $false|sQ11_spl),
% 18.12/2.75 inference(forward_subsumption_resolution,[status(thm)],[f369,f36])).
% 18.12/2.75 fof(f3268,plain,(
% 18.12/2.75 sQ11_spl),
% 18.12/2.75 inference(contradiction_clause,[status(thm)],[f3267])).
% 18.12/2.75 fof(f3283,plain,(
% 18.12/2.75 sdtpldt0(sdtpldt0(xm,xk),sdtpldt0(xl,xn))=sdtpldt0(xm,sdtpldt0(xk,sdtpldt0(xl,xn)))|~sQ1_spl|~sQ7_spl|~sQ5_spl),
% 18.12/2.75 inference(resolution,[status(thm)],[f1983,f292])).
% 18.12/2.75 fof(f3293,plain,(
% 18.12/2.75 sdtpldt0(sdtpldt0(xk,xm),sdtpldt0(xl,xn))=sdtpldt0(xm,sdtpldt0(xk,sdtpldt0(xl,xn)))|~sQ1_spl|~sQ7_spl|~sQ5_spl),
% 18.12/2.75 inference(forward_demodulation,[status(thm)],[f728,f3283])).
% 18.12/2.75 fof(f3307,plain,(
% 18.12/2.75 sdtpldt0(sdtpldt0(xm,sdtpldt0(xl,xn)),xk)=sdtpldt0(xm,sdtpldt0(xx,xn))|~sQ4_spl|~sQ6_spl|~sQ1_spl|~sQ7_spl|~sQ5_spl),
% 18.12/2.75 inference(resolution,[status(thm)],[f2049,f292])).
% 18.12/2.75 fof(f3341,plain,(
% 18.12/2.75 sdtpldt0(sdtpldt0(xk,xm),sdtpldt0(xl,xn))=sdtpldt0(xk,sdtpldt0(xm,sdtpldt0(xl,xn)))|~sQ1_spl|~sQ5_spl|~sQ7_spl),
% 18.12/2.77 inference(resolution,[status(thm)],[f1987,f300])).
% 18.12/2.77 fof(f3373,plain,(
% 18.12/2.77 sdtpldt0(sdtpldt0(xm,sdtpldt0(xl,xn)),xk)=sdtpldt0(sdtpldt0(xk,xm),sdtpldt0(xl,xn))|~sQ3_spl|~sQ1_spl|~sQ5_spl|~sQ7_spl),
% 18.12/2.77 inference(backward_demodulation,[status(thm)],[f1990,f3261])).
% 18.12/2.77 fof(f4016,plain,(
% 18.12/2.77 sdtpldt0(xy,xl)=sdtpldt0(xm,sdtpldt0(xl,xn))|~sQ4_spl|~sQ6_spl|~sQ5_spl),
% 18.12/2.77 inference(forward_demodulation,[status(thm)],[f2628,f2323])).
% 18.12/2.77 fof(f4090,plain,(
% 18.12/2.77 ~sdtpldt0(xx,xy)=sdtpldt0(sdtpldt0(xx,xm),xn)|~sQ5_spl|~sQ7_spl|~sQ4_spl|~sQ6_spl|~sQ3_spl),
% 18.12/2.77 inference(backward_demodulation,[status(thm)],[f4091,f147])).
% 18.12/2.77 fof(f4091,plain,(
% 18.12/2.77 sdtpldt0(sdtpldt0(xx,xm),xn)=sdtpldt0(sdtpldt0(xk,xm),sdtpldt0(xl,xn))|~sQ5_spl|~sQ7_spl|~sQ4_spl|~sQ6_spl|~sQ3_spl),
% 18.12/2.77 inference(forward_demodulation,[status(thm)],[f1639,f2324])).
% 18.12/2.77 fof(f4527,plain,(
% 18.12/2.77 sdtpldt0(sdtpldt0(xx,xm),xn)=sdtpldt0(xm,sdtpldt0(xk,sdtpldt0(xl,xn)))|~sQ4_spl|~sQ6_spl|~sQ3_spl|~sQ1_spl|~sQ7_spl|~sQ5_spl),
% 18.12/2.77 inference(forward_demodulation,[status(thm)],[f4091,f3293])).
% 18.12/2.77 fof(f4530,plain,(
% 18.12/2.77 ~sdtpldt0(xx,xy)=sdtpldt0(xm,sdtpldt0(xx,xn))|~sQ1_spl|~sQ5_spl|~sQ7_spl|~sQ4_spl|~sQ6_spl|~sQ3_spl),
% 18.12/2.77 inference(backward_demodulation,[status(thm)],[f4532,f4090])).
% 18.12/2.77 fof(f4532,plain,(
% 18.12/2.77 sdtpldt0(sdtpldt0(xx,xm),xn)=sdtpldt0(xm,sdtpldt0(xx,xn))|~sQ4_spl|~sQ6_spl|~sQ3_spl|~sQ1_spl|~sQ7_spl|~sQ5_spl),
% 18.12/2.77 inference(forward_demodulation,[status(thm)],[f2051,f4527])).
% 18.12/2.77 fof(f4540,plain,(
% 18.12/2.77 sdtpldt0(sdtpldt0(xy,xl),xk)=sdtpldt0(xm,sdtpldt0(xx,xn))|~sQ4_spl|~sQ6_spl|~sQ1_spl|~sQ7_spl|~sQ5_spl),
% 18.12/2.77 inference(forward_demodulation,[status(thm)],[f4016,f3307])).
% 18.12/2.77 fof(f4604,plain,(
% 18.12/2.77 sdtpldt0(sdtpldt0(xk,xm),sdtpldt0(xl,xn))=sdtpldt0(xk,sdtpldt0(xy,xl))|~sQ4_spl|~sQ6_spl|~sQ1_spl|~sQ5_spl|~sQ7_spl),
% 18.12/2.77 inference(forward_demodulation,[status(thm)],[f4016,f3341])).
% 18.12/2.77 fof(f4657,plain,(
% 18.12/2.77 sdtpldt0(sdtpldt0(xy,xl),xk)=sdtpldt0(sdtpldt0(xk,xm),sdtpldt0(xl,xn))|~sQ4_spl|~sQ6_spl|~sQ3_spl|~sQ1_spl|~sQ5_spl|~sQ7_spl),
% 18.12/2.77 inference(forward_demodulation,[status(thm)],[f4016,f3373])).
% 18.12/2.77 fof(f4658,plain,(
% 18.12/2.77 sdtpldt0(xm,sdtpldt0(xx,xn))=sdtpldt0(sdtpldt0(xk,xm),sdtpldt0(xl,xn))|~sQ4_spl|~sQ6_spl|~sQ3_spl|~sQ1_spl|~sQ5_spl|~sQ7_spl),
% 18.12/2.77 inference(forward_demodulation,[status(thm)],[f4540,f4657])).
% 18.12/2.77 fof(f4659,plain,(
% 18.12/2.77 ~sdtpldt0(xx,xy)=sdtpldt0(xk,sdtpldt0(xy,xl))|~sQ1_spl|~sQ5_spl|~sQ7_spl|~sQ4_spl|~sQ6_spl|~sQ3_spl),
% 18.12/2.77 inference(backward_demodulation,[status(thm)],[f4662,f4530])).
% 18.12/2.77 fof(f4662,plain,(
% 18.12/2.77 sdtpldt0(xm,sdtpldt0(xx,xn))=sdtpldt0(xk,sdtpldt0(xy,xl))|~sQ4_spl|~sQ6_spl|~sQ3_spl|~sQ1_spl|~sQ5_spl|~sQ7_spl),
% 18.12/2.77 inference(forward_demodulation,[status(thm)],[f4604,f4658])).
% 18.12/2.77 fof(f5408,plain,(
% 18.12/2.77 aElement0(sdtpldt0(xm,xn))|~sQ5_spl|~sQ4_spl),
% 18.12/2.77 inference(resolution,[status(thm)],[f677,f288])).
% 18.12/2.77 fof(f5419,plain,(
% 18.12/2.77 aElement0(xy)|~sQ5_spl|~sQ4_spl),
% 18.12/2.77 inference(forward_demodulation,[status(thm)],[f142,f5408])).
% 18.12/2.77 fof(f5942,plain,(
% 18.12/2.77 ![X0]: (~aElement0(X0)|sdtpldt0(sdtpldt0(X0,xl),xy)=sdtpldt0(X0,sdtpldt0(xl,xy))|~sQ5_spl|~sQ4_spl|~sQ6_spl)),
% 18.12/2.77 inference(resolution,[status(thm)],[f5419,f1195])).
% 18.12/2.77 fof(f6033,plain,(
% 18.12/2.77 ![X0]: (~aElement0(X0)|sdtpldt0(sdtpldt0(X0,xl),xy)=sdtpldt0(X0,sdtpldt0(xy,xl))|~sQ5_spl|~sQ4_spl|~sQ6_spl)),
% 18.12/2.77 inference(forward_demodulation,[status(thm)],[f2628,f5942])).
% 18.12/2.77 fof(f6428,plain,(
% 18.12/2.77 sdtpldt0(sdtpldt0(xk,xl),xy)=sdtpldt0(xk,sdtpldt0(xy,xl))|~sQ5_spl|~sQ4_spl|~sQ6_spl|~sQ7_spl),
% 18.12/2.77 inference(resolution,[status(thm)],[f6033,f300])).
% 18.12/2.77 fof(f6442,plain,(
% 18.12/2.77 sdtpldt0(xx,xy)=sdtpldt0(xk,sdtpldt0(xy,xl))|~sQ5_spl|~sQ4_spl|~sQ6_spl|~sQ7_spl),
% 18.12/2.77 inference(forward_demodulation,[status(thm)],[f139,f6428])).
% 18.12/2.77 fof(f6443,plain,(
% 18.12/2.77 $false|~sQ1_spl|~sQ3_spl|~sQ5_spl|~sQ4_spl|~sQ6_spl|~sQ7_spl),
% 18.12/2.77 inference(forward_subsumption_resolution,[status(thm)],[f6442,f4659])).
% 18.12/2.77 fof(f6444,plain,(
% 18.12/2.77 ~sQ1_spl|~sQ3_spl|~sQ5_spl|~sQ4_spl|~sQ6_spl|~sQ7_spl),
% 18.12/2.77 inference(contradiction_clause,[status(thm)],[f6443])).
% 18.12/2.77 fof(f6445,plain,(
% 18.12/2.77 $false),
% 18.12/2.77 inference(sat_refutation,[status(thm)],[f279,f286,f290,f294,f298,f302,f627,f900,f996,f3268,f6444])).
% 18.12/2.77 % SZS output end CNFRefutation for theBenchmark.p
% 18.12/2.79 % Elapsed time: 2.399594 seconds
% 18.12/2.79 % CPU time: 18.652383 seconds
% 18.12/2.79 % Total memory used: 350.790 MB
% 18.12/2.79 % Net memory used: 331.388 MB
%------------------------------------------------------------------------------