%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : RNG105+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 : n004.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 51.89s 7.04s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : RNG105+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.15/0.41 % Computer : n004.cluster.edu
% 0.15/0.41 % Model : x86_64 x86_64
% 0.15/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.41 % Memory : 8046.5625MB
% 0.15/0.41 % OS : Linux 6.8.0-71-generic
% 0.15/0.41 % CPULimit : 300
% 0.15/0.41 % WCLimit : 300
% 0.15/0.41 % DateTime : Mon Sep 21 04:20:04 UTC 2026
% 0.15/0.41 % CPUTime :
% 0.15/0.42 % Drodi V4.1.1
% 51.89/7.04 % Refutation found
% 51.89/7.04 % SZS status Theorem for theBenchmark: Theorem is valid
% 51.89/7.04 % SZS output start CNFRefutation for theBenchmark
% 51.89/7.04 fof(f2,axiom,(
% 51.89/7.04 aElement0(sz00) ),
% 51.89/7.04 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 51.89/7.04 fof(f3,axiom,(
% 51.89/7.04 aElement0(sz10) ),
% 51.89/7.04 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 51.89/7.04 fof(f5,axiom,(
% 51.89/7.04 (! [W0,W1] :( ( aElement0(W0)& aElement0(W1) )=> aElement0(sdtpldt0(W0,W1)) ) )),
% 51.89/7.04 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 51.89/7.04 fof(f6,axiom,(
% 51.89/7.04 (! [W0,W1] :( ( aElement0(W0)& aElement0(W1) )=> aElement0(sdtasdt0(W0,W1)) ) )),
% 51.89/7.04 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 51.89/7.04 fof(f16,axiom,(
% 51.89/7.04 (! [W0] :( aElement0(W0)=> ( sdtasdt0(W0,sz00) = sz00& sz00 = sdtasdt0(sz00,W0) ) ) )),
% 51.89/7.04 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 51.89/7.04 fof(f18,axiom,(
% 51.89/7.04 sz10 != sz00 ),
% 51.89/7.04 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 51.89/7.04 fof(f37,definition,(
% 51.89/7.04 (! [W0] :( aElement0(W0)=> (! [W1] :( W1 = slsdtgt0(W0)<=> ( aSet0(W1)& (! [W2] :( aElementOf0(W2,W1)<=> (? [W3] :( aElement0(W3)& sdtasdt0(W0,W3) = W2 ) )) )) ) )) )),
% 51.89/7.04 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 51.89/7.04 fof(f38,hypothesis,(
% 51.89/7.04 aElement0(xc) ),
% 51.89/7.04 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 51.89/7.04 fof(f39,hypothesis,(
% 51.89/7.04 ( aElementOf0(xx,slsdtgt0(xc))& aElementOf0(xy,slsdtgt0(xc))& aElement0(xz) ) ),
% 51.89/7.04 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 51.89/7.04 fof(f40,hypothesis,(
% 51.89/7.04 ( aElement0(xu)& sdtasdt0(xc,xu) = xx ) ),
% 51.89/7.04 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 51.89/7.04 fof(f41,hypothesis,(
% 51.89/7.04 ( aElement0(xv)& sdtasdt0(xc,xv) = xy ) ),
% 51.89/7.04 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 51.89/7.04 fof(f42,hypothesis,(
% 51.89/7.04 sdtpldt0(xx,xy) = sdtasdt0(xc,sdtpldt0(xu,xv)) ),
% 51.89/7.04 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 51.89/7.04 fof(f43,hypothesis,(
% 51.89/7.04 sdtasdt0(xz,xx) = sdtasdt0(xc,sdtasdt0(xu,xz)) ),
% 51.89/7.04 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 51.89/7.04 fof(f44,conjecture,(
% 51.89/7.04 ( aElementOf0(sdtpldt0(xx,xy),slsdtgt0(xc))& aElementOf0(sdtasdt0(xz,xx),slsdtgt0(xc)) ) ),
% 51.89/7.04 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 51.89/7.04 fof(f45,negated_conjecture,(
% 51.89/7.04 ~(( aElementOf0(sdtpldt0(xx,xy),slsdtgt0(xc))& aElementOf0(sdtasdt0(xz,xx),slsdtgt0(xc)) ) )),
% 51.89/7.04 inference(negated_conjecture,[status(cth)],[f44])).
% 51.89/7.04 fof(f49,plain,(
% 51.89/7.04 aElement0(sz00)),
% 51.89/7.04 inference(cnf_transformation,[status(thm)],[f2])).
% 51.89/7.04 fof(f50,plain,(
% 51.89/7.04 aElement0(sz10)),
% 51.89/7.04 inference(cnf_transformation,[status(thm)],[f3])).
% 51.89/7.04 fof(f53,plain,(
% 51.89/7.04 ![W0,W1]: ((~aElement0(W0)|~aElement0(W1))|aElement0(sdtpldt0(W0,W1)))),
% 51.89/7.04 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 51.89/7.04 fof(f54,plain,(
% 51.89/7.04 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|aElement0(sdtpldt0(X0,X1)))),
% 51.89/7.04 inference(cnf_transformation,[status(thm)],[f53])).
% 51.89/7.04 fof(f55,plain,(
% 51.89/7.04 ![W0,W1]: ((~aElement0(W0)|~aElement0(W1))|aElement0(sdtasdt0(W0,W1)))),
% 51.89/7.04 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 51.89/7.04 fof(f56,plain,(
% 51.89/7.04 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|aElement0(sdtasdt0(X0,X1)))),
% 51.89/7.04 inference(cnf_transformation,[status(thm)],[f55])).
% 51.89/7.04 fof(f80,plain,(
% 51.89/7.04 ![W0]: (~aElement0(W0)|(sdtasdt0(W0,sz00)=sz00&sz00=sdtasdt0(sz00,W0)))),
% 51.89/7.04 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 51.89/7.04 fof(f81,plain,(
% 51.89/7.04 ![X0]: (~aElement0(X0)|sdtasdt0(X0,sz00)=sz00)),
% 51.89/7.04 inference(cnf_transformation,[status(thm)],[f80])).
% 51.89/7.04 fof(f85,plain,(
% 51.89/7.04 ~sz10=sz00),
% 51.89/7.04 inference(cnf_transformation,[status(thm)],[f18])).
% 51.89/7.04 fof(f185,plain,(
% 51.89/7.04 ![W0]: (~aElement0(W0)|(![W1]: (W1=slsdtgt0(W0)<=>(aSet0(W1)&(![W2]: (aElementOf0(W2,W1)<=>(?[W3]: (aElement0(W3)&sdtasdt0(W0,W3)=W2))))))))),
% 51.89/7.04 inference(pre_NNF_transformation,[status(thm)],[f37])).
% 51.89/7.04 fof(f186,plain,(
% 51.89/7.04 ![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))))))))))),
% 51.89/7.04 inference(NNF_transformation,[status(thm)],[f185])).
% 51.89/7.04 fof(f187,plain,(
% 51.89/7.04 ![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))))))))))),
% 51.89/7.04 inference(miniscoping,[status(thm)],[f186])).
% 51.89/7.04 fof(f188,plain,(
% 51.89/7.04 ![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)))))))))),
% 51.89/7.04 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])).
% 51.89/7.04 fof(f189,plain,(
% 51.89/7.04 ![X0,X1]: (~aElement0(X0)|~X1=slsdtgt0(X0)|aSet0(X1))),
% 51.89/7.04 inference(cnf_transformation,[status(thm)],[f188])).
% 51.89/7.04 fof(f192,plain,(
% 51.89/7.04 ![X0,X1,X2,X3]: (~aElement0(X0)|~X1=slsdtgt0(X0)|aElementOf0(X2,X1)|~aElement0(X3)|~sdtasdt0(X0,X3)=X2)),
% 51.89/7.04 inference(cnf_transformation,[status(thm)],[f188])).
% 51.89/7.04 fof(f196,plain,(
% 51.89/7.04 aElement0(xc)),
% 51.89/7.04 inference(cnf_transformation,[status(thm)],[f38])).
% 51.89/7.04 fof(f199,plain,(
% 51.89/7.04 aElement0(xz)),
% 51.89/7.04 inference(cnf_transformation,[status(thm)],[f39])).
% 51.89/7.04 fof(f200,plain,(
% 51.89/7.04 aElement0(xu)),
% 51.89/7.04 inference(cnf_transformation,[status(thm)],[f40])).
% 51.89/7.04 fof(f202,plain,(
% 51.89/7.04 aElement0(xv)),
% 51.89/7.04 inference(cnf_transformation,[status(thm)],[f41])).
% 51.89/7.04 fof(f204,plain,(
% 51.89/7.04 sdtpldt0(xx,xy)=sdtasdt0(xc,sdtpldt0(xu,xv))),
% 51.89/7.04 inference(cnf_transformation,[status(thm)],[f42])).
% 51.89/7.04 fof(f205,plain,(
% 51.89/7.04 sdtasdt0(xz,xx)=sdtasdt0(xc,sdtasdt0(xu,xz))),
% 51.89/7.04 inference(cnf_transformation,[status(thm)],[f43])).
% 51.89/7.04 fof(f206,plain,(
% 51.89/7.04 (~aElementOf0(sdtpldt0(xx,xy),slsdtgt0(xc))|~aElementOf0(sdtasdt0(xz,xx),slsdtgt0(xc)))),
% 51.89/7.04 inference(pre_NNF_transformation,[status(thm)],[f45])).
% 51.89/7.04 fof(f207,plain,(
% 51.89/7.04 ~aElementOf0(sdtpldt0(xx,xy),slsdtgt0(xc))|~aElementOf0(sdtasdt0(xz,xx),slsdtgt0(xc))),
% 51.89/7.04 inference(cnf_transformation,[status(thm)],[f206])).
% 51.89/7.04 fof(f225,definition,(
% 51.89/7.04 sQ0_spl <=> (aElementOf0(sdtpldt0(xx,xy),slsdtgt0(xc)))),
% 51.89/7.04 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 51.89/7.04 fof(f228,definition,(
% 51.89/7.04 sQ1_spl <=> (aElementOf0(sdtasdt0(xz,xx),slsdtgt0(xc)))),
% 51.89/7.04 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 51.89/7.04 fof(f231,plain,(
% 51.89/7.04 ~sQ0_spl|~sQ1_spl),
% 51.89/7.04 inference(split_clause,[status(thm)],[f207,f225,f228])).
% 51.89/7.04 fof(f240,plain,(
% 51.89/7.04 ![X0]: (~aElement0(X0)|aSet0(slsdtgt0(X0)))),
% 51.89/7.04 inference(destructive_equality_resolution,[status(thm)],[f189])).
% 51.89/7.04 fof(f243,plain,(
% 51.89/7.04 ![X0,X1]: (~aElement0(X0)|aElementOf0(sdtasdt0(X0,X1),slsdtgt0(X0))|~aElement0(X1))),
% 51.89/7.04 inference(destructive_equality_resolution,[status(thm)],[f192])).
% 51.89/7.04 fof(f305,definition,(
% 51.89/7.04 sQ2_spl <=> (aElement0(xc))),
% 51.89/7.04 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 51.89/7.04 fof(f307,plain,(
% 51.89/7.04 ~aElement0(xc)|sQ2_spl),
% 51.89/7.04 inference(component_clause,[status(thm)],[f305])).
% 51.89/7.04 fof(f308,definition,(
% 51.89/7.04 sQ3_spl <=> (aElement0(xu))),
% 51.89/7.04 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 51.89/7.04 fof(f310,plain,(
% 51.89/7.04 ~aElement0(xu)|sQ3_spl),
% 51.89/7.04 inference(component_clause,[status(thm)],[f308])).
% 51.89/7.04 fof(f358,definition,(
% 51.89/7.04 sQ6_spl <=> (aElement0(xz))),
% 51.89/7.04 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 51.89/7.04 fof(f360,plain,(
% 51.89/7.04 ~aElement0(xz)|sQ6_spl),
% 51.89/7.04 inference(component_clause,[status(thm)],[f358])).
% 51.89/7.04 fof(f405,plain,(
% 51.89/7.04 $false|sQ3_spl),
% 51.89/7.04 inference(forward_subsumption_resolution,[status(thm)],[f310,f200])).
% 51.89/7.04 fof(f406,plain,(
% 51.89/7.04 sQ3_spl),
% 51.89/7.04 inference(contradiction_clause,[status(thm)],[f405])).
% 51.89/7.04 fof(f407,plain,(
% 51.89/7.04 $false|sQ2_spl),
% 51.89/7.04 inference(forward_subsumption_resolution,[status(thm)],[f307,f196])).
% 51.89/7.04 fof(f408,plain,(
% 51.89/7.04 sQ2_spl),
% 51.89/7.04 inference(contradiction_clause,[status(thm)],[f407])).
% 51.89/7.04 fof(f509,definition,(
% 51.89/7.04 sQ8_spl <=> (aElement0(xv))),
% 51.89/7.04 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 51.89/7.04 fof(f511,plain,(
% 51.89/7.04 ~aElement0(xv)|sQ8_spl),
% 51.89/7.04 inference(component_clause,[status(thm)],[f509])).
% 51.89/7.04 fof(f516,plain,(
% 51.89/7.04 $false|sQ8_spl),
% 51.89/7.04 inference(forward_subsumption_resolution,[status(thm)],[f511,f202])).
% 51.89/7.04 fof(f517,plain,(
% 51.89/7.04 sQ8_spl),
% 51.89/7.04 inference(contradiction_clause,[status(thm)],[f516])).
% 51.89/7.04 fof(f632,plain,(
% 51.89/7.04 $false|sQ6_spl),
% 51.89/7.04 inference(forward_subsumption_resolution,[status(thm)],[f360,f199])).
% 51.89/7.04 fof(f633,plain,(
% 51.89/7.04 sQ6_spl),
% 51.89/7.04 inference(contradiction_clause,[status(thm)],[f632])).
% 51.89/7.04 fof(f634,plain,(
% 51.89/7.04 ~aElement0(xc)|aElementOf0(sdtasdt0(xz,xx),slsdtgt0(xc))|~aElement0(sdtasdt0(xu,xz))),
% 51.89/7.04 inference(paramodulation,[status(thm)],[f205,f243])).
% 51.89/7.04 fof(f636,definition,(
% 51.89/7.04 sQ16_spl <=> (aElement0(sdtasdt0(xu,xz)))),
% 51.89/7.04 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 51.89/7.04 fof(f638,plain,(
% 51.89/7.04 ~aElement0(sdtasdt0(xu,xz))|sQ16_spl),
% 51.89/7.04 inference(component_clause,[status(thm)],[f636])).
% 51.89/7.04 fof(f639,plain,(
% 51.89/7.04 ~sQ2_spl|sQ1_spl|~sQ16_spl),
% 51.89/7.04 inference(split_clause,[status(thm)],[f634,f305,f228,f636])).
% 51.89/7.04 fof(f819,plain,(
% 51.89/7.04 ~aElement0(xu)|~aElement0(xz)|sQ16_spl),
% 51.89/7.04 inference(resolution,[status(thm)],[f638,f56])).
% 51.89/7.04 fof(f820,plain,(
% 51.89/7.04 ~sQ3_spl|~sQ6_spl|sQ16_spl),
% 51.89/7.04 inference(split_clause,[status(thm)],[f819,f308,f358,f636])).
% 51.89/7.04 fof(f924,definition,(
% 51.89/7.04 sQ42_spl <=> (sz10=sz00)),
% 51.89/7.04 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 51.89/7.04 fof(f925,plain,(
% 51.89/7.04 sz10=sz00|~sQ42_spl),
% 51.89/7.04 inference(component_clause,[status(thm)],[f924])).
% 51.89/7.04 fof(f928,definition,(
% 51.89/7.04 ![X0]: (sQ43_spl <=> (~aElement0(X0)|~sdtasdt0(X0,sz00)=sz00|X0=sz00))),
% 51.89/7.04 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 51.89/7.04 fof(f929,plain,(
% 51.89/7.04 ![X0]: (~aElement0(X0)|~sdtasdt0(X0,sz00)=sz00|X0=sz00|~sQ43_spl)),
% 51.89/7.04 inference(component_clause,[status(thm)],[f928])).
% 51.89/7.04 fof(f949,plain,(
% 51.89/7.04 ![X0]: (~aElement0(X0)|X0=sz00|~sQ43_spl)),
% 51.89/7.04 inference(forward_subsumption_resolution,[status(thm)],[f929,f81])).
% 51.89/7.04 fof(f1240,plain,(
% 51.89/7.04 sz10=sz00|~sQ43_spl),
% 51.89/7.04 inference(resolution,[status(thm)],[f949,f50])).
% 51.89/7.04 fof(f1248,plain,(
% 51.89/7.04 $false|~sQ43_spl),
% 51.89/7.04 inference(forward_subsumption_resolution,[status(thm)],[f1240,f85])).
% 51.89/7.04 fof(f1249,plain,(
% 51.89/7.04 ~sQ43_spl),
% 51.89/7.04 inference(contradiction_clause,[status(thm)],[f1248])).
% 51.89/7.04 fof(f4360,plain,(
% 51.89/7.04 $false|~sQ42_spl),
% 51.89/7.04 inference(forward_subsumption_resolution,[status(thm)],[f925,f85])).
% 51.89/7.04 fof(f4361,plain,(
% 51.89/7.04 ~sQ42_spl),
% 51.89/7.04 inference(contradiction_clause,[status(thm)],[f4360])).
% 51.89/7.04 fof(f6631,definition,(
% 51.89/7.04 sQ270_spl <=> (aElement0(sdtpldt0(xu,xv)))),
% 51.89/7.04 introduced(definition,[new_symbols(definition,[sQ270_spl])],[split_symbol_definition])).
% 51.89/7.04 fof(f6633,plain,(
% 51.89/7.04 ~aElement0(sdtpldt0(xu,xv))|sQ270_spl),
% 51.89/7.04 inference(component_clause,[status(thm)],[f6631])).
% 51.89/7.04 fof(f10204,definition,(
% 51.89/7.04 sQ361_spl <=> (aSet0(slsdtgt0(sz00)))),
% 51.89/7.04 introduced(definition,[new_symbols(definition,[sQ361_spl])],[split_symbol_definition])).
% 51.89/7.04 fof(f10206,plain,(
% 51.89/7.04 ~aSet0(slsdtgt0(sz00))|sQ361_spl),
% 51.89/7.04 inference(component_clause,[status(thm)],[f10204])).
% 51.89/7.04 fof(f10219,plain,(
% 51.89/7.04 ~aElement0(sz00)|sQ361_spl),
% 51.89/7.04 inference(resolution,[status(thm)],[f10206,f240])).
% 51.89/7.04 fof(f10221,plain,(
% 51.89/7.04 $false|sQ361_spl),
% 51.89/7.04 inference(forward_subsumption_resolution,[status(thm)],[f10219,f49])).
% 51.89/7.04 fof(f10222,plain,(
% 51.89/7.04 sQ361_spl),
% 51.89/7.04 inference(contradiction_clause,[status(thm)],[f10221])).
% 51.89/7.04 fof(f11170,plain,(
% 51.89/7.04 ~aElement0(xc)|aElementOf0(sdtpldt0(xx,xy),slsdtgt0(xc))|~aElement0(sdtpldt0(xu,xv))),
% 51.89/7.04 inference(paramodulation,[status(thm)],[f204,f243])).
% 51.89/7.04 fof(f11176,plain,(
% 51.89/7.04 ~sQ2_spl|sQ0_spl|~sQ270_spl),
% 51.89/7.04 inference(split_clause,[status(thm)],[f11170,f305,f225,f6631])).
% 51.89/7.04 fof(f20382,plain,(
% 51.89/7.04 ~aElement0(xu)|~aElement0(xv)|sQ270_spl),
% 51.89/7.04 inference(resolution,[status(thm)],[f6633,f54])).
% 51.89/7.04 fof(f20383,plain,(
% 51.89/7.04 ~sQ3_spl|~sQ8_spl|sQ270_spl),
% 51.89/7.04 inference(split_clause,[status(thm)],[f20382,f308,f509,f6631])).
% 51.89/7.09 fof(f20384,plain,(
% 51.89/7.09 $false),
% 51.89/7.09 inference(sat_refutation,[status(thm)],[f231,f406,f408,f517,f633,f639,f820,f1249,f4361,f10222,f11176,f20383])).
% 51.89/7.09 % SZS output end CNFRefutation for theBenchmark.p
% 51.89/7.10 % Elapsed time: 6.675909 seconds
% 51.89/7.10 % CPU time: 52.424481 seconds
% 51.89/7.10 % Total memory used: 389.143 MB
% 51.89/7.10 % Net memory used: 365.114 MB
%------------------------------------------------------------------------------