%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : RNG116+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 : 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:23 PM UTC 2026
% Result : Theorem 37.02s 5.82s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : RNG116+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/1.01 % Computer : n017.cluster.edu
% 0.18/1.01 % Model : x86_64 x86_64
% 0.18/1.01 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/1.01 % Memory : 8046.5625MB
% 0.18/1.01 % OS : Linux 6.8.0-71-generic
% 0.18/1.01 % CPULimit : 300
% 0.18/1.01 % WCLimit : 300
% 0.18/1.01 % DateTime : Mon Sep 21 04:16:27 UTC 2026
% 0.18/1.02 % CPUTime :
% 0.18/1.04 % Drodi V4.1.1
% 37.02/5.82 % Refutation found
% 37.02/5.82 % SZS status Theorem for theBenchmark: Theorem is valid
% 37.02/5.82 % SZS output start CNFRefutation for theBenchmark
% 37.02/5.82 fof(f2,axiom,(
% 37.02/5.82 aElement0(sz00) ),
% 37.02/5.82 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.02/5.82 fof(f4,axiom,(
% 37.02/5.82 (! [W0] :( aElement0(W0)=> aElement0(smndt0(W0)) ) )),
% 37.02/5.82 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.02/5.82 fof(f16,axiom,(
% 37.02/5.82 (! [W0] :( aElement0(W0)=> ( sdtasdt0(W0,sz00) = sz00& sz00 = sdtasdt0(sz00,W0) ) ) )),
% 37.02/5.82 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.02/5.82 fof(f20,axiom,(
% 37.02/5.82 (! [W0] :( aSet0(W0)=> (! [W1] :( aElementOf0(W1,W0)=> aElement0(W1) ) )) )),
% 37.02/5.82 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.02/5.82 fof(f37,definition,(
% 37.02/5.82 (! [W0] :( aElement0(W0)=> (! [W1] :( W1 = slsdtgt0(W0)<=> ( aSet0(W1)& (! [W2] :( aElementOf0(W2,W1)<=> (? [W3] :( aElement0(W3)& sdtasdt0(W0,W3) = W2 ) )) )) ) )) )),
% 37.02/5.82 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.02/5.82 fof(f38,axiom,(
% 37.02/5.82 (! [W0] :( aElement0(W0)=> aIdeal0(slsdtgt0(W0)) ) )),
% 37.02/5.82 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.02/5.82 fof(f39,hypothesis,(
% 37.02/5.82 ( aElement0(xa)& aElement0(xb) ) ),
% 37.02/5.82 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.02/5.82 fof(f43,hypothesis,(
% 37.02/5.82 ( aElementOf0(sz00,slsdtgt0(xa))& aElementOf0(xa,slsdtgt0(xa))& aElementOf0(sz00,slsdtgt0(xb))& aElementOf0(xb,slsdtgt0(xb)) ) ),
% 37.02/5.82 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.02/5.82 fof(f45,hypothesis,(
% 37.02/5.82 ( aElementOf0(xu,xI)& xu != sz00& (! [W0] :( ( aElementOf0(W0,xI)& W0 != sz00 )=> ~ iLess0(sbrdtbr0(W0),sbrdtbr0(xu)) ) )) ),
% 37.02/5.82 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.02/5.82 fof(f47,hypothesis,(
% 37.02/5.82 ( aElementOf0(xk,slsdtgt0(xa))& aElementOf0(xl,slsdtgt0(xb))& xu = sdtpldt0(xk,xl) ) ),
% 37.02/5.82 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.02/5.82 fof(f48,conjecture,(
% 37.02/5.82 (? [W0,W1] :( aElement0(W0)& aElement0(W1)& xu = sdtpldt0(sdtasdt0(xa,W0),sdtasdt0(xb,W1)) ) )),
% 37.02/5.82 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.02/5.82 fof(f49,negated_conjecture,(
% 37.02/5.82 ~((? [W0,W1] :( aElement0(W0)& aElement0(W1)& xu = sdtpldt0(sdtasdt0(xa,W0),sdtasdt0(xb,W1)) ) ))),
% 37.02/5.82 inference(negated_conjecture,[status(cth)],[f48])).
% 37.02/5.82 fof(f53,plain,(
% 37.02/5.82 aElement0(sz00)),
% 37.02/5.82 inference(cnf_transformation,[status(thm)],[f2])).
% 37.02/5.82 fof(f55,plain,(
% 37.02/5.82 ![W0]: (~aElement0(W0)|aElement0(smndt0(W0)))),
% 37.02/5.82 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 37.02/5.82 fof(f56,plain,(
% 37.02/5.82 ![X0]: (~aElement0(X0)|aElement0(smndt0(X0)))),
% 37.02/5.82 inference(cnf_transformation,[status(thm)],[f55])).
% 37.02/5.82 fof(f84,plain,(
% 37.02/5.82 ![W0]: (~aElement0(W0)|(sdtasdt0(W0,sz00)=sz00&sz00=sdtasdt0(sz00,W0)))),
% 37.02/5.82 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 37.02/5.82 fof(f85,plain,(
% 37.02/5.82 ![X0]: (~aElement0(X0)|sdtasdt0(X0,sz00)=sz00)),
% 37.02/5.82 inference(cnf_transformation,[status(thm)],[f84])).
% 37.02/5.82 fof(f86,plain,(
% 37.02/5.82 ![X0]: (~aElement0(X0)|sz00=sdtasdt0(sz00,X0))),
% 37.02/5.82 inference(cnf_transformation,[status(thm)],[f84])).
% 37.02/5.82 fof(f93,plain,(
% 37.02/5.82 ![W0]: (~aSet0(W0)|(![W1]: (~aElementOf0(W1,W0)|aElement0(W1))))),
% 37.02/5.82 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 37.02/5.82 fof(f94,plain,(
% 37.02/5.82 ![X0,X1]: (~aSet0(X0)|~aElementOf0(X1,X0)|aElement0(X1))),
% 37.02/5.82 inference(cnf_transformation,[status(thm)],[f93])).
% 37.02/5.82 fof(f189,plain,(
% 37.02/5.82 ![W0]: (~aElement0(W0)|(![W1]: (W1=slsdtgt0(W0)<=>(aSet0(W1)&(![W2]: (aElementOf0(W2,W1)<=>(?[W3]: (aElement0(W3)&sdtasdt0(W0,W3)=W2))))))))),
% 37.02/5.82 inference(pre_NNF_transformation,[status(thm)],[f37])).
% 37.02/5.82 fof(f190,plain,(
% 37.02/5.82 ![W0]: (~aElement0(W0)|(![W1]: ((~W1=slsdtgt0(W0)|(aSet0(W1)&(![W2]: ((~aElementOf0(W2,W1)|(?[W3]: (aElement0(W3)&sdtasdt0(W0,W3)=W2)))&(aElementOf0(W2,W1)|(![W3]: (~aElement0(W3)|~sdtasdt0(W0,W3)=W2)))))))&(W1=slsdtgt0(W0)|(~aSet0(W1)|(?[W2]: ((~aElementOf0(W2,W1)|(![W3]: (~aElement0(W3)|~sdtasdt0(W0,W3)=W2)))&(aElementOf0(W2,W1)|(?[W3]: (aElement0(W3)&sdtasdt0(W0,W3)=W2))))))))))),
% 37.02/5.82 inference(NNF_transformation,[status(thm)],[f189])).
% 37.02/5.82 fof(f191,plain,(
% 37.02/5.82 ![W0]: (~aElement0(W0)|((![W1]: (~W1=slsdtgt0(W0)|(aSet0(W1)&((![W2]: (~aElementOf0(W2,W1)|(?[W3]: (aElement0(W3)&sdtasdt0(W0,W3)=W2))))&(![W2]: (aElementOf0(W2,W1)|(![W3]: (~aElement0(W3)|~sdtasdt0(W0,W3)=W2))))))))&(![W1]: (W1=slsdtgt0(W0)|(~aSet0(W1)|(?[W2]: ((~aElementOf0(W2,W1)|(![W3]: (~aElement0(W3)|~sdtasdt0(W0,W3)=W2)))&(aElementOf0(W2,W1)|(?[W3]: (aElement0(W3)&sdtasdt0(W0,W3)=W2))))))))))),
% 37.02/5.82 inference(miniscoping,[status(thm)],[f190])).
% 37.02/5.82 fof(f192,plain,(
% 37.02/5.82 ![W0]: (~aElement0(W0)|((![W1]: (~W1=slsdtgt0(W0)|(aSet0(W1)&((![W2]: (~aElementOf0(W2,W1)|(aElement0(sK17_skl(W2,W1,W0))&sdtasdt0(W0,sK17_skl(W2,W1,W0))=W2)))&(![W2]: (aElementOf0(W2,W1)|(![W3]: (~aElement0(W3)|~sdtasdt0(W0,W3)=W2))))))))&(![W1]: (W1=slsdtgt0(W0)|(~aSet0(W1)|((~aElementOf0(sK18_skl(W1,W0),W1)|(![W3]: (~aElement0(W3)|~sdtasdt0(W0,W3)=sK18_skl(W1,W0))))&(aElementOf0(sK18_skl(W1,W0),W1)|(aElement0(sK19_skl(W1,W0))&sdtasdt0(W0,sK19_skl(W1,W0))=sK18_skl(W1,W0)))))))))),
% 37.02/5.82 inference(skolemize,[status(esa),new_symbols(skolem,[sK17_skl,sK18_skl,sK19_skl]),skolemize(W3,sK17_skl(W2,W1,W0)),skolemize(W2,sK18_skl(W1,W0)),skolemize(W3,sK19_skl(W1,W0))],[f191])).
% 37.02/5.82 fof(f193,plain,(
% 37.02/5.82 ![X0,X1]: (~aElement0(X0)|~X1=slsdtgt0(X0)|aSet0(X1))),
% 37.02/5.82 inference(cnf_transformation,[status(thm)],[f192])).
% 37.02/5.82 fof(f194,plain,(
% 37.02/5.82 ![X0,X1,X2]: (~aElement0(X0)|~X1=slsdtgt0(X0)|~aElementOf0(X2,X1)|aElement0(sK17_skl(X2,X1,X0)))),
% 37.02/5.82 inference(cnf_transformation,[status(thm)],[f192])).
% 37.02/5.82 fof(f195,plain,(
% 37.02/5.82 ![X0,X1,X2]: (~aElement0(X0)|~X1=slsdtgt0(X0)|~aElementOf0(X2,X1)|sdtasdt0(X0,sK17_skl(X2,X1,X0))=X2)),
% 37.02/5.82 inference(cnf_transformation,[status(thm)],[f192])).
% 37.02/5.82 fof(f200,plain,(
% 37.02/5.82 ![W0]: (~aElement0(W0)|aIdeal0(slsdtgt0(W0)))),
% 37.02/5.82 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 37.02/5.82 fof(f201,plain,(
% 37.02/5.82 ![X0]: (~aElement0(X0)|aIdeal0(slsdtgt0(X0)))),
% 37.02/5.82 inference(cnf_transformation,[status(thm)],[f200])).
% 37.02/5.82 fof(f202,plain,(
% 37.02/5.82 aElement0(xa)),
% 37.02/5.82 inference(cnf_transformation,[status(thm)],[f39])).
% 37.02/5.82 fof(f203,plain,(
% 37.02/5.82 aElement0(xb)),
% 37.02/5.82 inference(cnf_transformation,[status(thm)],[f39])).
% 37.02/5.82 fof(f209,plain,(
% 37.02/5.82 aElementOf0(xa,slsdtgt0(xa))),
% 37.02/5.82 inference(cnf_transformation,[status(thm)],[f43])).
% 37.02/5.82 fof(f211,plain,(
% 37.02/5.82 aElementOf0(xb,slsdtgt0(xb))),
% 37.02/5.82 inference(cnf_transformation,[status(thm)],[f43])).
% 37.02/5.82 fof(f215,plain,(
% 37.02/5.82 (aElementOf0(xu,xI)&~xu=sz00)&(![W0]: ((~aElementOf0(W0,xI)|W0=sz00)|~iLess0(sbrdtbr0(W0),sbrdtbr0(xu))))),
% 37.02/5.82 inference(pre_NNF_transformation,[status(thm)],[f45])).
% 37.02/5.82 fof(f217,plain,(
% 37.02/5.82 ~xu=sz00),
% 37.02/5.82 inference(cnf_transformation,[status(thm)],[f215])).
% 37.02/5.82 fof(f221,plain,(
% 37.02/5.82 aElementOf0(xk,slsdtgt0(xa))),
% 37.02/5.82 inference(cnf_transformation,[status(thm)],[f47])).
% 37.02/5.82 fof(f222,plain,(
% 37.02/5.82 aElementOf0(xl,slsdtgt0(xb))),
% 37.02/5.82 inference(cnf_transformation,[status(thm)],[f47])).
% 37.02/5.82 fof(f223,plain,(
% 37.02/5.82 xu=sdtpldt0(xk,xl)),
% 37.02/5.82 inference(cnf_transformation,[status(thm)],[f47])).
% 37.02/5.82 fof(f224,plain,(
% 37.02/5.82 (![W0,W1]: ((~aElement0(W0)|~aElement0(W1))|~xu=sdtpldt0(sdtasdt0(xa,W0),sdtasdt0(xb,W1))))),
% 37.02/5.82 inference(pre_NNF_transformation,[status(thm)],[f49])).
% 37.02/5.82 fof(f225,plain,(
% 37.02/5.82 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|~xu=sdtpldt0(sdtasdt0(xa,X0),sdtasdt0(xb,X1)))),
% 37.02/5.82 inference(cnf_transformation,[status(thm)],[f224])).
% 37.02/5.82 fof(f265,plain,(
% 37.02/5.82 ![X0]: (~aElement0(X0)|aSet0(slsdtgt0(X0)))),
% 37.02/5.82 inference(destructive_equality_resolution,[status(thm)],[f193])).
% 37.02/5.82 fof(f266,plain,(
% 37.02/5.82 ![X0,X1]: (~aElement0(X0)|~aElementOf0(X1,slsdtgt0(X0))|aElement0(sK17_skl(X1,slsdtgt0(X0),X0)))),
% 37.02/5.82 inference(destructive_equality_resolution,[status(thm)],[f194])).
% 37.02/5.82 fof(f267,plain,(
% 37.02/5.82 ![X0,X1]: (~aElement0(X0)|~aElementOf0(X1,slsdtgt0(X0))|sdtasdt0(X0,sK17_skl(X1,slsdtgt0(X0),X0))=X1)),
% 37.02/5.82 inference(destructive_equality_resolution,[status(thm)],[f195])).
% 37.02/5.82 fof(f321,definition,(
% 37.02/5.82 sQ4_spl <=> (aSet0(slsdtgt0(xa)))),
% 37.02/5.82 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 37.02/5.82 fof(f323,plain,(
% 37.02/5.82 ~aSet0(slsdtgt0(xa))|sQ4_spl),
% 37.02/5.82 inference(component_clause,[status(thm)],[f321])).
% 37.02/5.82 fof(f328,plain,(
% 37.02/5.82 aSet0(slsdtgt0(xb))),
% 37.02/5.82 inference(resolution,[status(thm)],[f265,f203])).
% 37.02/5.82 fof(f329,plain,(
% 37.02/5.82 aSet0(slsdtgt0(xa))),
% 37.02/5.82 inference(resolution,[status(thm)],[f265,f202])).
% 37.02/5.82 fof(f330,plain,(
% 37.02/5.82 aIdeal0(slsdtgt0(xb))),
% 37.02/5.82 inference(resolution,[status(thm)],[f201,f203])).
% 37.02/5.82 fof(f387,plain,(
% 37.02/5.82 aElement0(smndt0(sz00))),
% 37.02/5.82 inference(resolution,[status(thm)],[f56,f53])).
% 37.02/5.82 fof(f398,plain,(
% 37.02/5.82 ~aSet0(slsdtgt0(xa))|aElement0(xa)),
% 37.02/5.82 inference(resolution,[status(thm)],[f209,f94])).
% 37.02/5.82 fof(f399,definition,(
% 37.02/5.82 sQ6_spl <=> (aElement0(xa))),
% 37.02/5.82 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 37.02/5.82 fof(f402,plain,(
% 37.02/5.82 ~sQ4_spl|sQ6_spl),
% 37.02/5.82 inference(split_clause,[status(thm)],[f398,f321,f399])).
% 37.02/5.82 fof(f420,definition,(
% 37.02/5.82 sQ7_spl <=> (aSet0(slsdtgt0(xb)))),
% 37.02/5.82 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 37.02/5.82 fof(f422,plain,(
% 37.02/5.82 ~aSet0(slsdtgt0(xb))|sQ7_spl),
% 37.02/5.82 inference(component_clause,[status(thm)],[f420])).
% 37.02/5.82 fof(f424,plain,(
% 37.02/5.82 ~aSet0(slsdtgt0(xb))|aElement0(xb)),
% 37.02/5.82 inference(resolution,[status(thm)],[f211,f94])).
% 37.02/5.82 fof(f425,definition,(
% 37.02/5.82 sQ8_spl <=> (aElement0(xb))),
% 37.02/5.82 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 37.02/5.82 fof(f428,plain,(
% 37.02/5.82 ~sQ7_spl|sQ8_spl),
% 37.02/5.82 inference(split_clause,[status(thm)],[f424,f420,f425])).
% 37.02/5.82 fof(f493,plain,(
% 37.02/5.82 $false|sQ4_spl),
% 37.02/5.82 inference(forward_subsumption_resolution,[status(thm)],[f329,f323])).
% 37.02/5.82 fof(f494,plain,(
% 37.02/5.82 sQ4_spl),
% 37.02/5.82 inference(contradiction_clause,[status(thm)],[f493])).
% 37.02/5.82 fof(f517,plain,(
% 37.02/5.82 $false|sQ7_spl),
% 37.02/5.82 inference(forward_subsumption_resolution,[status(thm)],[f422,f328])).
% 37.02/5.82 fof(f518,plain,(
% 37.02/5.82 sQ7_spl),
% 37.02/5.82 inference(contradiction_clause,[status(thm)],[f517])).
% 37.02/5.82 fof(f526,plain,(
% 37.02/5.82 sdtasdt0(xa,sz00)=sz00),
% 37.02/5.82 inference(resolution,[status(thm)],[f85,f202])).
% 37.02/5.82 fof(f530,plain,(
% 37.02/5.82 sz00=sdtasdt0(sz00,xa)),
% 37.02/5.82 inference(resolution,[status(thm)],[f86,f202])).
% 37.02/5.82 fof(f973,definition,(
% 37.02/5.82 sQ56_spl <=> (aElement0(sdtasdt0(xa,sz00)))),
% 37.02/5.82 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 37.02/5.82 fof(f975,plain,(
% 37.02/5.82 ~aElement0(sdtasdt0(xa,sz00))|sQ56_spl),
% 37.02/5.82 inference(component_clause,[status(thm)],[f973])).
% 37.02/5.82 fof(f1408,plain,(
% 37.02/5.82 ~aElement0(xa)|sdtasdt0(xa,sK17_skl(xk,slsdtgt0(xa),xa))=xk),
% 37.02/5.82 inference(resolution,[status(thm)],[f221,f267])).
% 37.02/5.82 fof(f1409,plain,(
% 37.02/5.82 ~aElement0(xa)|aElement0(sK17_skl(xk,slsdtgt0(xa),xa))),
% 37.02/5.82 inference(resolution,[status(thm)],[f221,f266])).
% 37.02/5.82 fof(f1414,definition,(
% 37.02/5.82 sQ105_spl <=> (sdtasdt0(xa,sK17_skl(xk,slsdtgt0(xa),xa))=xk)),
% 37.02/5.82 introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition])).
% 37.02/5.82 fof(f1415,plain,(
% 37.02/5.82 sdtasdt0(xa,sK17_skl(xk,slsdtgt0(xa),xa))=xk|~sQ105_spl),
% 37.02/5.82 inference(component_clause,[status(thm)],[f1414])).
% 37.02/5.82 fof(f1417,plain,(
% 37.02/5.82 ~sQ6_spl|sQ105_spl),
% 37.02/5.82 inference(split_clause,[status(thm)],[f1408,f399,f1414])).
% 37.02/5.82 fof(f1418,definition,(
% 37.02/5.82 sQ106_spl <=> (aElement0(sK17_skl(xk,slsdtgt0(xa),xa)))),
% 37.02/5.82 introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition])).
% 37.02/5.82 fof(f1421,plain,(
% 37.02/5.82 ~sQ6_spl|sQ106_spl),
% 37.02/5.82 inference(split_clause,[status(thm)],[f1409,f399,f1418])).
% 37.02/5.82 fof(f2008,definition,(
% 37.02/5.82 sQ136_spl <=> (aElement0(sdtasdt0(sz00,xa)))),
% 37.02/5.82 introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition])).
% 37.02/5.82 fof(f2010,plain,(
% 37.02/5.82 ~aElement0(sdtasdt0(sz00,xa))|sQ136_spl),
% 37.02/5.82 inference(component_clause,[status(thm)],[f2008])).
% 37.02/5.82 fof(f5534,definition,(
% 37.02/5.82 sQ469_spl <=> (xu=sdtpldt0(xk,xl))),
% 37.02/5.82 introduced(definition,[new_symbols(definition,[sQ469_spl])],[split_symbol_definition])).
% 37.02/5.82 fof(f5536,plain,(
% 37.02/5.82 ~xu=sdtpldt0(xk,xl)|sQ469_spl),
% 37.02/5.82 inference(component_clause,[status(thm)],[f5534])).
% 37.02/5.82 fof(f5541,plain,(
% 37.02/5.82 ~xu=xu|sQ469_spl),
% 37.02/5.82 inference(forward_demodulation,[status(thm)],[f223,f5536])).
% 37.02/5.82 fof(f5542,plain,(
% 37.02/5.82 $false|sQ469_spl),
% 37.02/5.82 inference(trivial_equality_resolution,[status(thm)],[f5541])).
% 37.02/5.82 fof(f5543,plain,(
% 37.02/5.82 sQ469_spl),
% 37.02/5.82 inference(contradiction_clause,[status(thm)],[f5542])).
% 37.02/5.82 fof(f5544,plain,(
% 37.02/5.82 ~aElement0(sz00)|sQ136_spl),
% 37.02/5.82 inference(forward_demodulation,[status(thm)],[f530,f2010])).
% 37.02/5.82 fof(f5545,plain,(
% 37.02/5.82 $false|sQ136_spl),
% 37.02/5.82 inference(forward_subsumption_resolution,[status(thm)],[f5544,f53])).
% 37.02/5.82 fof(f5546,plain,(
% 37.02/5.82 sQ136_spl),
% 37.02/5.82 inference(contradiction_clause,[status(thm)],[f5545])).
% 37.02/5.82 fof(f5547,plain,(
% 37.02/5.82 ~aElement0(sz00)|sQ56_spl),
% 37.02/5.82 inference(forward_demodulation,[status(thm)],[f526,f975])).
% 37.02/5.82 fof(f5548,plain,(
% 37.02/5.82 $false|sQ56_spl),
% 37.02/5.82 inference(forward_subsumption_resolution,[status(thm)],[f5547,f53])).
% 37.02/5.82 fof(f5549,plain,(
% 35.79/5.86 sQ56_spl),
% 35.79/5.86 inference(contradiction_clause,[status(thm)],[f5548])).
% 35.79/5.86 fof(f5588,plain,(
% 35.79/5.86 ![X0]: (~aElement0(sK17_skl(xk,slsdtgt0(xa),xa))|~aElement0(X0)|~xu=sdtpldt0(xk,sdtasdt0(xb,X0))|~sQ105_spl)),
% 35.79/5.86 inference(paramodulation,[status(thm)],[f1415,f225])).
% 35.79/5.86 fof(f5600,definition,(
% 35.79/5.86 ![X0]: (sQ475_spl <=> (~aElement0(X0)|~xu=sdtpldt0(xk,sdtasdt0(xb,X0))))),
% 35.79/5.86 introduced(definition,[new_symbols(definition,[sQ475_spl])],[split_symbol_definition])).
% 35.79/5.86 fof(f5601,plain,(
% 35.79/5.86 ![X0]: (~aElement0(X0)|~xu=sdtpldt0(xk,sdtasdt0(xb,X0))|~sQ475_spl)),
% 35.79/5.86 inference(component_clause,[status(thm)],[f5600])).
% 35.79/5.86 fof(f5603,plain,(
% 35.79/5.86 ~sQ106_spl|sQ475_spl|~sQ105_spl),
% 35.79/5.86 inference(split_clause,[status(thm)],[f5588,f1418,f5600,f1414])).
% 35.79/5.86 fof(f5649,definition,(
% 35.79/5.86 sQ479_spl <=> (aIdeal0(slsdtgt0(xb)))),
% 35.79/5.86 introduced(definition,[new_symbols(definition,[sQ479_spl])],[split_symbol_definition])).
% 35.79/5.86 fof(f5651,plain,(
% 35.79/5.86 ~aIdeal0(slsdtgt0(xb))|sQ479_spl),
% 35.79/5.86 inference(component_clause,[status(thm)],[f5649])).
% 35.79/5.86 fof(f5750,plain,(
% 35.79/5.86 ~aElement0(xb)|sdtasdt0(xb,sK17_skl(xl,slsdtgt0(xb),xb))=xl),
% 35.79/5.86 inference(resolution,[status(thm)],[f222,f267])).
% 35.79/5.86 fof(f5751,plain,(
% 35.79/5.86 ~aElement0(xb)|aElement0(sK17_skl(xl,slsdtgt0(xb),xb))),
% 35.79/5.86 inference(resolution,[status(thm)],[f222,f266])).
% 35.79/5.86 fof(f5758,definition,(
% 35.79/5.86 sQ490_spl <=> (sdtasdt0(xb,sK17_skl(xl,slsdtgt0(xb),xb))=xl)),
% 35.79/5.86 introduced(definition,[new_symbols(definition,[sQ490_spl])],[split_symbol_definition])).
% 35.79/5.86 fof(f5759,plain,(
% 35.79/5.86 sdtasdt0(xb,sK17_skl(xl,slsdtgt0(xb),xb))=xl|~sQ490_spl),
% 35.79/5.86 inference(component_clause,[status(thm)],[f5758])).
% 35.79/5.86 fof(f5761,plain,(
% 35.79/5.86 ~sQ8_spl|sQ490_spl),
% 35.79/5.86 inference(split_clause,[status(thm)],[f5750,f425,f5758])).
% 35.79/5.86 fof(f5762,definition,(
% 35.79/5.86 sQ491_spl <=> (aElement0(sK17_skl(xl,slsdtgt0(xb),xb)))),
% 35.79/5.86 introduced(definition,[new_symbols(definition,[sQ491_spl])],[split_symbol_definition])).
% 35.79/5.86 fof(f5765,plain,(
% 35.79/5.86 ~sQ8_spl|sQ491_spl),
% 35.79/5.86 inference(split_clause,[status(thm)],[f5751,f425,f5762])).
% 35.79/5.86 fof(f6781,plain,(
% 35.79/5.86 $false|sQ479_spl),
% 35.79/5.86 inference(forward_subsumption_resolution,[status(thm)],[f5651,f330])).
% 35.79/5.86 fof(f6782,plain,(
% 35.79/5.86 sQ479_spl),
% 35.79/5.86 inference(contradiction_clause,[status(thm)],[f6781])).
% 35.79/5.86 fof(f8500,definition,(
% 35.79/5.86 sQ653_spl <=> (xu=sz00)),
% 35.79/5.86 introduced(definition,[new_symbols(definition,[sQ653_spl])],[split_symbol_definition])).
% 35.79/5.86 fof(f8501,plain,(
% 35.79/5.86 xu=sz00|~sQ653_spl),
% 35.79/5.86 inference(component_clause,[status(thm)],[f8500])).
% 35.79/5.86 fof(f8541,plain,(
% 35.79/5.86 $false|~sQ653_spl),
% 35.79/5.86 inference(forward_subsumption_resolution,[status(thm)],[f8501,f217])).
% 35.79/5.86 fof(f8542,plain,(
% 35.79/5.86 ~sQ653_spl),
% 35.79/5.86 inference(contradiction_clause,[status(thm)],[f8541])).
% 35.79/5.86 fof(f9828,definition,(
% 35.79/5.86 sQ741_spl <=> (aElement0(smndt0(sz00)))),
% 35.79/5.86 introduced(definition,[new_symbols(definition,[sQ741_spl])],[split_symbol_definition])).
% 35.79/5.86 fof(f9830,plain,(
% 35.79/5.86 ~aElement0(smndt0(sz00))|sQ741_spl),
% 35.79/5.86 inference(component_clause,[status(thm)],[f9828])).
% 35.79/5.86 fof(f9835,plain,(
% 35.79/5.86 $false|sQ741_spl),
% 35.79/5.86 inference(forward_subsumption_resolution,[status(thm)],[f9830,f387])).
% 35.79/5.86 fof(f9836,plain,(
% 35.79/5.86 sQ741_spl),
% 35.79/5.86 inference(contradiction_clause,[status(thm)],[f9835])).
% 35.79/5.86 fof(f12163,plain,(
% 35.79/5.86 ~aElement0(sK17_skl(xl,slsdtgt0(xb),xb))|~xu=sdtpldt0(xk,xl)|~sQ475_spl|~sQ490_spl),
% 35.79/5.86 inference(paramodulation,[status(thm)],[f5759,f5601])).
% 35.79/5.86 fof(f12172,plain,(
% 35.79/5.86 ~sQ491_spl|~sQ469_spl|~sQ475_spl|~sQ490_spl),
% 35.79/5.86 inference(split_clause,[status(thm)],[f12163,f5762,f5534,f5600,f5758])).
% 35.79/5.86 fof(f12186,plain,(
% 35.79/5.86 $false),
% 35.79/5.86 inference(sat_refutation,[status(thm)],[f402,f428,f494,f518,f1417,f1421,f5543,f5546,f5549,f5603,f5761,f5765,f6782,f8542,f9836,f12172])).
% 35.79/5.86 % SZS output end CNFRefutation for theBenchmark.p
% 35.79/5.88 % Elapsed time: 4.842010 seconds
% 35.79/5.88 % CPU time: 38.040787 seconds
% 35.79/5.88 % Total memory used: 338.443 MB
% 35.79/5.88 % Net memory used: 319.295 MB
%------------------------------------------------------------------------------