%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : RNG105+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/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:22 PM UTC 2026
% Result : Theorem 11.16s 1.87s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : RNG105+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n018.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 04:22:28 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.12/0.36 % Drodi V4.1.1
% 11.16/1.87 % Refutation found
% 11.16/1.87 % SZS status Theorem for theBenchmark: Theorem is valid
% 11.16/1.87 % SZS output start CNFRefutation for theBenchmark
% 11.16/1.87 fof(f2,axiom,(
% 11.16/1.87 aElement0(sz00) ),
% 11.16/1.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.16/1.87 fof(f3,axiom,(
% 11.16/1.87 aElement0(sz10) ),
% 11.16/1.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.16/1.87 fof(f5,axiom,(
% 11.16/1.87 (! [W0,W1] :( ( aElement0(W0)& aElement0(W1) )=> aElement0(sdtpldt0(W0,W1)) ) )),
% 11.16/1.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.16/1.87 fof(f6,axiom,(
% 11.16/1.87 (! [W0,W1] :( ( aElement0(W0)& aElement0(W1) )=> aElement0(sdtasdt0(W0,W1)) ) )),
% 11.16/1.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.16/1.87 fof(f18,axiom,(
% 11.16/1.87 sz10 != sz00 ),
% 11.16/1.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.16/1.87 fof(f37,definition,(
% 11.16/1.87 (! [W0] :( aElement0(W0)=> (! [W1] :( W1 = slsdtgt0(W0)<=> ( aSet0(W1)& (! [W2] :( aElementOf0(W2,W1)<=> (? [W3] :( aElement0(W3)& sdtasdt0(W0,W3) = W2 ) )) )) ) )) )),
% 11.16/1.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.16/1.87 fof(f38,hypothesis,(
% 11.16/1.87 aElement0(xc) ),
% 11.16/1.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.16/1.87 fof(f39,hypothesis,(
% 11.16/1.87 ( (? [W0] :( aElement0(W0)& sdtasdt0(xc,W0) = xx ))& aElementOf0(xx,slsdtgt0(xc))& (? [W0] :( aElement0(W0)& sdtasdt0(xc,W0) = xy ))& aElementOf0(xy,slsdtgt0(xc))& aElement0(xz) ) ),
% 11.16/1.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.16/1.87 fof(f40,hypothesis,(
% 11.16/1.87 ( aElement0(xu)& sdtasdt0(xc,xu) = xx ) ),
% 11.16/1.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.16/1.87 fof(f41,hypothesis,(
% 11.16/1.87 ( aElement0(xv)& sdtasdt0(xc,xv) = xy ) ),
% 11.16/1.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.16/1.87 fof(f42,hypothesis,(
% 11.16/1.87 sdtpldt0(xx,xy) = sdtasdt0(xc,sdtpldt0(xu,xv)) ),
% 11.16/1.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.16/1.87 fof(f43,hypothesis,(
% 11.16/1.87 sdtasdt0(xz,xx) = sdtasdt0(xc,sdtasdt0(xu,xz)) ),
% 11.16/1.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.16/1.87 fof(f44,conjecture,(
% 11.16/1.87 ( ( (? [W0] :( aElement0(W0)& sdtasdt0(xc,W0) = sdtpldt0(xx,xy) ))| aElementOf0(sdtpldt0(xx,xy),slsdtgt0(xc)) )& ( (? [W0] :( aElement0(W0)& sdtasdt0(xc,W0) = sdtasdt0(xz,xx) ))| aElementOf0(sdtasdt0(xz,xx),slsdtgt0(xc)) ) ) ),
% 11.16/1.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.16/1.87 fof(f45,negated_conjecture,(
% 11.16/1.87 ~(( ( (? [W0] :( aElement0(W0)& sdtasdt0(xc,W0) = sdtpldt0(xx,xy) ))| aElementOf0(sdtpldt0(xx,xy),slsdtgt0(xc)) )& ( (? [W0] :( aElement0(W0)& sdtasdt0(xc,W0) = sdtasdt0(xz,xx) ))| aElementOf0(sdtasdt0(xz,xx),slsdtgt0(xc)) ) ) )),
% 11.16/1.87 inference(negated_conjecture,[status(cth)],[f44])).
% 11.16/1.87 fof(f49,plain,(
% 11.16/1.87 aElement0(sz00)),
% 11.16/1.87 inference(cnf_transformation,[status(thm)],[f2])).
% 11.16/1.87 fof(f50,plain,(
% 11.16/1.87 aElement0(sz10)),
% 11.16/1.87 inference(cnf_transformation,[status(thm)],[f3])).
% 11.16/1.87 fof(f53,plain,(
% 11.16/1.87 ![W0,W1]: ((~aElement0(W0)|~aElement0(W1))|aElement0(sdtpldt0(W0,W1)))),
% 11.16/1.87 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 11.16/1.87 fof(f54,plain,(
% 11.16/1.87 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|aElement0(sdtpldt0(X0,X1)))),
% 11.16/1.87 inference(cnf_transformation,[status(thm)],[f53])).
% 11.16/1.87 fof(f55,plain,(
% 11.16/1.87 ![W0,W1]: ((~aElement0(W0)|~aElement0(W1))|aElement0(sdtasdt0(W0,W1)))),
% 11.16/1.87 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 11.16/1.87 fof(f56,plain,(
% 11.16/1.87 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|aElement0(sdtasdt0(X0,X1)))),
% 11.16/1.87 inference(cnf_transformation,[status(thm)],[f55])).
% 11.16/1.87 fof(f85,plain,(
% 11.16/1.87 ~sz10=sz00),
% 11.16/1.87 inference(cnf_transformation,[status(thm)],[f18])).
% 11.16/1.87 fof(f185,plain,(
% 11.16/1.87 ![W0]: (~aElement0(W0)|(![W1]: (W1=slsdtgt0(W0)<=>(aSet0(W1)&(![W2]: (aElementOf0(W2,W1)<=>(?[W3]: (aElement0(W3)&sdtasdt0(W0,W3)=W2))))))))),
% 11.16/1.87 inference(pre_NNF_transformation,[status(thm)],[f37])).
% 11.16/1.87 fof(f186,plain,(
% 11.16/1.87 ![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))))))))))),
% 11.16/1.87 inference(NNF_transformation,[status(thm)],[f185])).
% 11.16/1.87 fof(f187,plain,(
% 11.16/1.87 ![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))))))))))),
% 11.16/1.87 inference(miniscoping,[status(thm)],[f186])).
% 11.16/1.87 fof(f188,plain,(
% 11.16/1.87 ![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)))))))))),
% 11.16/1.87 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))],[f187])).
% 11.16/1.87 fof(f192,plain,(
% 11.16/1.87 ![X0,X1,X2,X3]: (~aElement0(X0)|~X1=slsdtgt0(X0)|aElementOf0(X2,X1)|~aElement0(X3)|~sdtasdt0(X0,X3)=X2)),
% 11.16/1.87 inference(cnf_transformation,[status(thm)],[f188])).
% 11.16/1.87 fof(f196,plain,(
% 11.16/1.87 aElement0(xc)),
% 11.16/1.87 inference(cnf_transformation,[status(thm)],[f38])).
% 11.16/1.87 fof(f197,plain,(
% 11.16/1.87 ((((aElement0(sK20_skl)&sdtasdt0(xc,sK20_skl)=xx)&aElementOf0(xx,slsdtgt0(xc)))&(aElement0(sK21_skl)&sdtasdt0(xc,sK21_skl)=xy))&aElementOf0(xy,slsdtgt0(xc)))&aElement0(xz)),
% 11.16/1.87 inference(skolemize,[status(esa),new_symbols(skolem,[sK20_skl,sK21_skl]),skolemize(W0,sK20_skl),skolemize(W0,sK21_skl)],[f39])).
% 11.16/1.87 fof(f200,plain,(
% 11.16/1.87 aElementOf0(xx,slsdtgt0(xc))),
% 11.16/1.87 inference(cnf_transformation,[status(thm)],[f197])).
% 11.16/1.87 fof(f204,plain,(
% 11.16/1.87 aElement0(xz)),
% 11.16/1.87 inference(cnf_transformation,[status(thm)],[f197])).
% 11.16/1.87 fof(f205,plain,(
% 11.16/1.87 aElement0(xu)),
% 11.16/1.87 inference(cnf_transformation,[status(thm)],[f40])).
% 11.16/1.87 fof(f207,plain,(
% 11.16/1.87 aElement0(xv)),
% 11.16/1.87 inference(cnf_transformation,[status(thm)],[f41])).
% 11.16/1.87 fof(f209,plain,(
% 11.16/1.87 sdtpldt0(xx,xy)=sdtasdt0(xc,sdtpldt0(xu,xv))),
% 11.16/1.87 inference(cnf_transformation,[status(thm)],[f42])).
% 11.16/1.87 fof(f210,plain,(
% 11.16/1.87 sdtasdt0(xz,xx)=sdtasdt0(xc,sdtasdt0(xu,xz))),
% 11.16/1.87 inference(cnf_transformation,[status(thm)],[f43])).
% 11.16/1.87 fof(f211,plain,(
% 11.16/1.87 (((![W0]: (~aElement0(W0)|~sdtasdt0(xc,W0)=sdtpldt0(xx,xy)))&~aElementOf0(sdtpldt0(xx,xy),slsdtgt0(xc)))|((![W0]: (~aElement0(W0)|~sdtasdt0(xc,W0)=sdtasdt0(xz,xx)))&~aElementOf0(sdtasdt0(xz,xx),slsdtgt0(xc))))),
% 11.16/1.87 inference(pre_NNF_transformation,[status(thm)],[f45])).
% 11.16/1.87 fof(f212,definition,(
% 11.16/1.87 sP3_prd<=>((![W0]: (~aElement0(W0)|~sdtasdt0(xc,W0)=sdtpldt0(xx,xy)))&~aElementOf0(sdtpldt0(xx,xy),slsdtgt0(xc)))),
% 11.16/1.87 introduced(definition,[new_symbols(definition,[sP3_prd])],[])).
% 11.16/1.87 fof(f213,plain,(
% 11.16/1.87 sP3_prd|((![W0]: (~aElement0(W0)|~sdtasdt0(xc,W0)=sdtasdt0(xz,xx)))&~aElementOf0(sdtasdt0(xz,xx),slsdtgt0(xc)))),
% 11.16/1.87 inference(formula_renaming,[status(thm)],[f211,f212])).
% 11.16/1.87 fof(f215,plain,(
% 11.16/1.87 sP3_prd|~aElementOf0(sdtasdt0(xz,xx),slsdtgt0(xc))),
% 11.16/1.87 inference(cnf_transformation,[status(thm)],[f213])).
% 11.16/1.87 fof(f233,plain,(
% 11.16/1.87 (~sP3_prd|((![W0]: (~aElement0(W0)|~sdtasdt0(xc,W0)=sdtpldt0(xx,xy)))&~aElementOf0(sdtpldt0(xx,xy),slsdtgt0(xc))))&(sP3_prd|((?[W0]: (aElement0(W0)&sdtasdt0(xc,W0)=sdtpldt0(xx,xy)))|aElementOf0(sdtpldt0(xx,xy),slsdtgt0(xc))))),
% 11.16/1.87 inference(NNF_transformation,[status(thm)],[f212])).
% 11.16/1.87 fof(f234,plain,(
% 11.16/1.87 (~sP3_prd|((![W0]: (~aElement0(W0)|~sdtasdt0(xc,W0)=sdtpldt0(xx,xy)))&~aElementOf0(sdtpldt0(xx,xy),slsdtgt0(xc))))&(sP3_prd|((aElement0(sK22_skl)&sdtasdt0(xc,sK22_skl)=sdtpldt0(xx,xy))|aElementOf0(sdtpldt0(xx,xy),slsdtgt0(xc))))),
% 11.16/1.87 inference(skolemize,[status(esa),new_symbols(skolem,[sK22_skl]),skolemize(W0,sK22_skl)],[f233])).
% 11.16/1.87 fof(f235,plain,(
% 11.16/1.87 ![X0]: (~sP3_prd|~aElement0(X0)|~sdtasdt0(xc,X0)=sdtpldt0(xx,xy))),
% 11.16/1.87 inference(cnf_transformation,[status(thm)],[f234])).
% 11.16/1.87 fof(f239,definition,(
% 11.16/1.87 sQ0_spl <=> (sP3_prd)),
% 11.16/1.87 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 11.16/1.87 fof(f246,definition,(
% 11.16/1.87 sQ2_spl <=> (aElementOf0(sdtasdt0(xz,xx),slsdtgt0(xc)))),
% 11.16/1.87 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 11.16/1.87 fof(f249,plain,(
% 11.16/1.87 sQ0_spl|~sQ2_spl),
% 11.16/1.87 inference(split_clause,[status(thm)],[f215,f239,f246])).
% 11.16/1.87 fof(f250,definition,(
% 11.16/1.87 ![X0]: (sQ3_spl <=> (~aElement0(X0)|~sdtasdt0(xc,X0)=sdtpldt0(xx,xy)))),
% 11.16/1.87 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 11.16/1.87 fof(f251,plain,(
% 11.16/1.87 ![X0]: (~aElement0(X0)|~sdtasdt0(xc,X0)=sdtpldt0(xx,xy)|~sQ3_spl)),
% 11.16/1.87 inference(component_clause,[status(thm)],[f250])).
% 11.16/1.87 fof(f253,plain,(
% 11.16/1.87 ~sQ0_spl|sQ3_spl),
% 11.16/1.87 inference(split_clause,[status(thm)],[f235,f239,f250])).
% 11.16/1.87 fof(f277,plain,(
% 11.16/1.87 ![X0,X1]: (~aElement0(X0)|aElementOf0(sdtasdt0(X0,X1),slsdtgt0(X0))|~aElement0(X1))),
% 11.16/1.87 inference(destructive_equality_resolution,[status(thm)],[f192])).
% 11.16/1.87 fof(f352,definition,(
% 11.16/1.87 sQ7_spl <=> (aElement0(sz00))),
% 11.16/1.87 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 11.16/1.87 fof(f354,plain,(
% 11.16/1.87 ~aElement0(sz00)|sQ7_spl),
% 11.16/1.87 inference(component_clause,[status(thm)],[f352])).
% 11.16/1.87 fof(f357,definition,(
% 11.16/1.87 sQ8_spl <=> (aElement0(xz))),
% 11.16/1.87 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 11.16/1.87 fof(f359,plain,(
% 11.16/1.87 ~aElement0(xz)|sQ8_spl),
% 11.16/1.87 inference(component_clause,[status(thm)],[f357])).
% 11.16/1.87 fof(f362,definition,(
% 11.16/1.87 sQ9_spl <=> (aElement0(xc))),
% 11.16/1.87 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 11.16/1.87 fof(f364,plain,(
% 11.16/1.87 ~aElement0(xc)|sQ9_spl),
% 11.16/1.87 inference(component_clause,[status(thm)],[f362])).
% 11.16/1.87 fof(f383,definition,(
% 11.16/1.87 sQ10_spl <=> (aElement0(xv))),
% 11.16/1.87 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 11.16/1.87 fof(f385,plain,(
% 11.16/1.87 ~aElement0(xv)|sQ10_spl),
% 11.16/1.87 inference(component_clause,[status(thm)],[f383])).
% 11.16/1.87 fof(f449,plain,(
% 11.16/1.87 $false|sQ9_spl),
% 11.16/1.87 inference(forward_subsumption_resolution,[status(thm)],[f364,f196])).
% 11.16/1.87 fof(f450,plain,(
% 11.16/1.87 sQ9_spl),
% 11.16/1.87 inference(contradiction_clause,[status(thm)],[f449])).
% 11.16/1.87 fof(f494,definition,(
% 11.16/1.87 sQ18_spl <=> (aElement0(xu))),
% 11.16/1.87 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 11.16/1.87 fof(f496,plain,(
% 11.16/1.87 ~aElement0(xu)|sQ18_spl),
% 11.16/1.87 inference(component_clause,[status(thm)],[f494])).
% 11.16/1.87 fof(f499,plain,(
% 11.16/1.87 $false|sQ18_spl),
% 11.16/1.87 inference(forward_subsumption_resolution,[status(thm)],[f496,f205])).
% 11.16/1.87 fof(f500,plain,(
% 11.16/1.87 sQ18_spl),
% 11.16/1.87 inference(contradiction_clause,[status(thm)],[f499])).
% 11.16/1.87 fof(f516,plain,(
% 11.16/1.87 $false|sQ10_spl),
% 11.16/1.87 inference(forward_subsumption_resolution,[status(thm)],[f385,f207])).
% 11.16/1.87 fof(f517,plain,(
% 11.16/1.87 sQ10_spl),
% 11.16/1.87 inference(contradiction_clause,[status(thm)],[f516])).
% 11.16/1.87 fof(f518,plain,(
% 11.16/1.87 $false|sQ8_spl),
% 11.16/1.87 inference(forward_subsumption_resolution,[status(thm)],[f359,f204])).
% 11.16/1.87 fof(f519,plain,(
% 11.16/1.87 sQ8_spl),
% 11.16/1.87 inference(contradiction_clause,[status(thm)],[f518])).
% 11.16/1.87 fof(f697,definition,(
% 11.16/1.87 sQ21_spl <=> (aElement0(sz10))),
% 11.16/1.87 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 11.16/1.87 fof(f699,plain,(
% 11.16/1.87 ~aElement0(sz10)|sQ21_spl),
% 11.16/1.87 inference(component_clause,[status(thm)],[f697])).
% 11.16/1.87 fof(f830,plain,(
% 11.16/1.87 $false|sQ21_spl),
% 11.16/1.87 inference(forward_subsumption_resolution,[status(thm)],[f699,f50])).
% 11.16/1.87 fof(f831,plain,(
% 11.16/1.87 sQ21_spl),
% 11.16/1.87 inference(contradiction_clause,[status(thm)],[f830])).
% 11.16/1.87 fof(f883,plain,(
% 11.16/1.87 $false|sQ7_spl),
% 11.16/1.87 inference(forward_subsumption_resolution,[status(thm)],[f354,f49])).
% 11.16/1.87 fof(f884,plain,(
% 11.16/1.87 sQ7_spl),
% 11.16/1.87 inference(contradiction_clause,[status(thm)],[f883])).
% 11.16/1.87 fof(f979,definition,(
% 11.16/1.87 sQ49_spl <=> (sz10=sz00)),
% 11.16/1.87 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 11.16/1.87 fof(f980,plain,(
% 11.16/1.87 sz10=sz00|~sQ49_spl),
% 11.16/1.87 inference(component_clause,[status(thm)],[f979])).
% 11.16/1.87 fof(f1012,plain,(
% 11.16/1.87 $false|~sQ49_spl),
% 11.16/1.87 inference(forward_subsumption_resolution,[status(thm)],[f980,f85])).
% 11.16/1.87 fof(f1013,plain,(
% 11.16/1.87 ~sQ49_spl),
% 11.16/1.87 inference(contradiction_clause,[status(thm)],[f1012])).
% 11.16/1.87 fof(f3973,plain,(
% 11.16/1.87 ~aElement0(xc)|aElementOf0(sdtasdt0(xz,xx),slsdtgt0(xc))|~aElement0(sdtasdt0(xu,xz))),
% 11.16/1.87 inference(paramodulation,[status(thm)],[f210,f277])).
% 11.16/1.87 fof(f3978,definition,(
% 11.16/1.87 sQ177_spl <=> (aElement0(sdtasdt0(xu,xz)))),
% 11.16/1.88 introduced(definition,[new_symbols(definition,[sQ177_spl])],[split_symbol_definition])).
% 11.16/1.88 fof(f3980,plain,(
% 11.16/1.88 ~aElement0(sdtasdt0(xu,xz))|sQ177_spl),
% 11.16/1.88 inference(component_clause,[status(thm)],[f3978])).
% 11.16/1.88 fof(f3982,plain,(
% 11.16/1.88 ~sQ9_spl|sQ2_spl|~sQ177_spl),
% 11.16/1.88 inference(split_clause,[status(thm)],[f3973,f362,f246,f3978])).
% 11.16/1.88 fof(f4385,definition,(
% 11.16/1.88 ![X0,X1]: (sQ198_spl <=> (~aElementOf0(X0,X1)))),
% 11.16/1.88 introduced(definition,[new_symbols(definition,[sQ198_spl])],[split_symbol_definition])).
% 11.16/1.88 fof(f4386,plain,(
% 11.16/1.88 ![X0,X1]: (~aElementOf0(X0,X1)|~sQ198_spl)),
% 11.16/1.88 inference(component_clause,[status(thm)],[f4385])).
% 11.16/1.88 fof(f4454,plain,(
% 11.16/1.88 $false|~sQ198_spl),
% 11.16/1.88 inference(backward_subsumption_resolution,[status(thm)],[f200,f4386])).
% 11.16/1.88 fof(f4463,plain,(
% 11.16/1.88 ~sQ198_spl),
% 11.16/1.88 inference(contradiction_clause,[status(thm)],[f4454])).
% 11.16/1.88 fof(f6459,plain,(
% 11.16/1.88 ~aElement0(sdtpldt0(xu,xv))|~sQ3_spl),
% 11.16/1.88 inference(resolution,[status(thm)],[f251,f209])).
% 11.16/1.88 fof(f6463,definition,(
% 11.16/1.88 sQ294_spl <=> (sdtpldt0(xx,xy)=sdtpldt0(xx,xy))),
% 11.16/1.88 introduced(definition,[new_symbols(definition,[sQ294_spl])],[split_symbol_definition])).
% 11.16/1.88 fof(f6465,plain,(
% 11.16/1.88 ~sdtpldt0(xx,xy)=sdtpldt0(xx,xy)|sQ294_spl),
% 11.16/1.88 inference(component_clause,[status(thm)],[f6463])).
% 11.16/1.88 fof(f6469,plain,(
% 11.16/1.88 $false|sQ294_spl),
% 11.16/1.88 inference(trivial_equality_resolution,[status(thm)],[f6465])).
% 11.16/1.88 fof(f6470,plain,(
% 11.16/1.88 sQ294_spl),
% 11.16/1.88 inference(contradiction_clause,[status(thm)],[f6469])).
% 11.16/1.88 fof(f9183,plain,(
% 11.16/1.88 ~aElement0(xu)|~aElement0(xv)|~sQ3_spl),
% 11.16/1.88 inference(resolution,[status(thm)],[f6459,f54])).
% 11.16/1.88 fof(f9184,plain,(
% 11.16/1.88 ~sQ18_spl|~sQ10_spl|~sQ3_spl),
% 11.16/1.88 inference(split_clause,[status(thm)],[f9183,f494,f383,f250])).
% 11.16/1.88 fof(f10680,plain,(
% 11.16/1.88 ~aElement0(xu)|~aElement0(xz)|sQ177_spl),
% 11.16/1.88 inference(resolution,[status(thm)],[f3980,f56])).
% 11.16/1.88 fof(f10681,plain,(
% 11.16/1.88 ~sQ18_spl|~sQ8_spl|sQ177_spl),
% 11.16/1.88 inference(split_clause,[status(thm)],[f10680,f494,f357,f3978])).
% 11.16/1.88 fof(f10682,plain,(
% 11.16/1.88 $false),
% 11.16/1.88 inference(sat_refutation,[status(thm)],[f249,f253,f450,f500,f517,f519,f831,f884,f1013,f3982,f4463,f6470,f9184,f10681])).
% 11.16/1.88 % SZS output end CNFRefutation for theBenchmark.p
% 11.16/1.90 % Elapsed time: 1.529743 seconds
% 11.16/1.90 % CPU time: 11.833788 seconds
% 11.16/1.90 % Total memory used: 248.811 MB
% 11.16/1.90 % Net memory used: 237.822 MB
%------------------------------------------------------------------------------