%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : RNG125+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 : n010.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:25 PM UTC 2026
% Result : Theorem 0.10s 0.48s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG125+1 : 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 : n010.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:22:12 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.39 % Drodi V4.1.1
% 0.10/0.48 % Refutation found
% 0.10/0.48 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.10/0.48 % SZS output start CNFRefutation for theBenchmark
% 0.10/0.48 fof(f3,axiom,(
% 0.10/0.48 aElement0(sz10) ),
% 0.10/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.48 fof(f18,axiom,(
% 0.10/0.48 sz10 != sz00 ),
% 0.10/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.48 fof(f20,axiom,(
% 0.10/0.48 (! [W0] :( aSet0(W0)=> (! [W1] :( aElementOf0(W1,W0)=> aElement0(W1) ) )) )),
% 0.10/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.48 fof(f24,definition,(
% 0.10/0.48 (! [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) ) )) ) )) ) )),
% 0.10/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.48 fof(f34,definition,(
% 0.10/0.48 (! [W0] :( aElement0(W0)=> (! [W1] :( aDivisorOf0(W1,W0)<=> ( aElement0(W1)& doDivides0(W1,W0) ) ) )) )),
% 0.10/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.48 fof(f38,axiom,(
% 0.10/0.48 (! [W0] :( aElement0(W0)=> aIdeal0(slsdtgt0(W0)) ) )),
% 0.10/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.48 fof(f39,hypothesis,(
% 0.10/0.48 ( aElement0(xa)& aElement0(xb) ) ),
% 0.10/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.48 fof(f42,hypothesis,(
% 0.10/0.48 ( aIdeal0(xI)& xI = sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)) ) ),
% 0.10/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.48 fof(f43,hypothesis,(
% 0.10/0.48 ( aElementOf0(sz00,slsdtgt0(xa))& aElementOf0(xa,slsdtgt0(xa))& aElementOf0(sz00,slsdtgt0(xb))& aElementOf0(xb,slsdtgt0(xb)) ) ),
% 0.10/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.48 fof(f45,hypothesis,(
% 0.10/0.48 ( aElementOf0(xu,xI)& xu != sz00& (! [W0] :( ( aElementOf0(W0,xI)& W0 != sz00 )=> ~ iLess0(sbrdtbr0(W0),sbrdtbr0(xu)) ) )) ),
% 0.10/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.48 fof(f46,hypothesis,(
% 0.10/0.48 ~ ( aDivisorOf0(xu,xa)& aDivisorOf0(xu,xb) ) ),
% 0.10/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.48 fof(f48,hypothesis,(
% 0.10/0.48 ~ ~ doDivides0(xu,xa) ),
% 0.10/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.48 fof(f49,hypothesis,(
% 0.10/0.48 ~ ~ doDivides0(xu,xb) ),
% 0.10/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.48 fof(f56,plain,(
% 0.10/0.48 aElement0(sz10)),
% 0.10/0.48 inference(cnf_transformation,[status(thm)],[f3])).
% 0.10/0.48 fof(f91,plain,(
% 0.10/0.48 ~sz10=sz00),
% 0.10/0.48 inference(cnf_transformation,[status(thm)],[f18])).
% 0.10/0.48 fof(f95,plain,(
% 0.10/0.48 ![W0]: (~aSet0(W0)|(![W1]: (~aElementOf0(W1,W0)|aElement0(W1))))),
% 0.10/0.48 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 0.10/0.48 fof(f96,plain,(
% 0.10/0.48 ![X0,X1]: (~aSet0(X0)|~aElementOf0(X1,X0)|aElement0(X1))),
% 0.10/0.48 inference(cnf_transformation,[status(thm)],[f95])).
% 0.10/0.48 fof(f125,plain,(
% 0.10/0.48 ![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))))))))),
% 0.10/0.48 inference(pre_NNF_transformation,[status(thm)],[f24])).
% 0.10/0.48 fof(f126,plain,(
% 0.10/0.48 ![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)))))))))),
% 0.10/0.48 inference(NNF_transformation,[status(thm)],[f125])).
% 0.10/0.48 fof(f127,plain,(
% 0.10/0.48 (![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)))))))))),
% 0.10/0.48 inference(miniscoping,[status(thm)],[f126])).
% 0.10/0.48 fof(f128,plain,(
% 0.10/0.48 (![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)))))))),
% 0.10/0.48 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))],[f127])).
% 0.10/0.48 fof(f129,plain,(
% 0.10/0.48 ![X0]: (~aIdeal0(X0)|aSet0(X0))),
% 0.10/0.48 inference(cnf_transformation,[status(thm)],[f128])).
% 0.10/0.48 fof(f171,plain,(
% 0.10/0.48 ![W0]: (~aElement0(W0)|(![W1]: (aDivisorOf0(W1,W0)<=>(aElement0(W1)&doDivides0(W1,W0)))))),
% 0.10/0.48 inference(pre_NNF_transformation,[status(thm)],[f34])).
% 0.10/0.48 fof(f172,plain,(
% 0.10/0.48 ![W0]: (~aElement0(W0)|(![W1]: ((~aDivisorOf0(W1,W0)|(aElement0(W1)&doDivides0(W1,W0)))&(aDivisorOf0(W1,W0)|(~aElement0(W1)|~doDivides0(W1,W0))))))),
% 0.10/0.48 inference(NNF_transformation,[status(thm)],[f171])).
% 0.10/0.48 fof(f173,plain,(
% 0.10/0.48 ![W0]: (~aElement0(W0)|((![W1]: (~aDivisorOf0(W1,W0)|(aElement0(W1)&doDivides0(W1,W0))))&(![W1]: (aDivisorOf0(W1,W0)|(~aElement0(W1)|~doDivides0(W1,W0))))))),
% 0.10/0.48 inference(miniscoping,[status(thm)],[f172])).
% 0.10/0.48 fof(f176,plain,(
% 0.10/0.48 ![X0,X1]: (~aElement0(X0)|aDivisorOf0(X1,X0)|~aElement0(X1)|~doDivides0(X1,X0))),
% 0.10/0.48 inference(cnf_transformation,[status(thm)],[f173])).
% 0.10/0.48 fof(f202,plain,(
% 0.10/0.48 ![W0]: (~aElement0(W0)|aIdeal0(slsdtgt0(W0)))),
% 0.10/0.48 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 0.10/0.48 fof(f203,plain,(
% 0.10/0.48 ![X0]: (~aElement0(X0)|aIdeal0(slsdtgt0(X0)))),
% 0.10/0.48 inference(cnf_transformation,[status(thm)],[f202])).
% 0.10/0.48 fof(f204,plain,(
% 0.10/0.48 aElement0(xa)),
% 0.10/0.48 inference(cnf_transformation,[status(thm)],[f39])).
% 0.10/0.48 fof(f205,plain,(
% 0.10/0.48 aElement0(xb)),
% 0.10/0.48 inference(cnf_transformation,[status(thm)],[f39])).
% 0.10/0.48 fof(f208,plain,(
% 0.10/0.48 aIdeal0(xI)),
% 0.10/0.48 inference(cnf_transformation,[status(thm)],[f42])).
% 0.10/0.48 fof(f211,plain,(
% 0.10/0.48 aElementOf0(xa,slsdtgt0(xa))),
% 0.10/0.48 inference(cnf_transformation,[status(thm)],[f43])).
% 0.10/0.48 fof(f213,plain,(
% 0.10/0.48 aElementOf0(xb,slsdtgt0(xb))),
% 0.10/0.48 inference(cnf_transformation,[status(thm)],[f43])).
% 0.10/0.48 fof(f217,plain,(
% 0.10/0.48 (aElementOf0(xu,xI)&~xu=sz00)&(![W0]: ((~aElementOf0(W0,xI)|W0=sz00)|~iLess0(sbrdtbr0(W0),sbrdtbr0(xu))))),
% 0.10/0.48 inference(pre_NNF_transformation,[status(thm)],[f45])).
% 0.10/0.48 fof(f218,plain,(
% 0.10/0.48 aElementOf0(xu,xI)),
% 0.10/0.48 inference(cnf_transformation,[status(thm)],[f217])).
% 0.10/0.48 fof(f219,plain,(
% 0.10/0.48 ~xu=sz00),
% 0.10/0.48 inference(cnf_transformation,[status(thm)],[f217])).
% 0.10/0.48 fof(f221,plain,(
% 0.10/0.48 (~aDivisorOf0(xu,xa)|~aDivisorOf0(xu,xb))),
% 0.10/0.48 inference(pre_NNF_transformation,[status(thm)],[f46])).
% 0.10/0.48 fof(f222,plain,(
% 0.10/0.48 ~aDivisorOf0(xu,xa)|~aDivisorOf0(xu,xb)),
% 0.10/0.48 inference(cnf_transformation,[status(thm)],[f221])).
% 0.10/0.48 fof(f227,plain,(
% 0.10/0.48 doDivides0(xu,xa)),
% 0.10/0.48 inference(cnf_transformation,[status(thm)],[f48])).
% 0.10/0.48 fof(f228,plain,(
% 0.10/0.48 doDivides0(xu,xb)),
% 0.10/0.48 inference(cnf_transformation,[status(thm)],[f49])).
% 0.10/0.48 fof(f253,definition,(
% 0.10/0.48 sQ2_spl <=> (aDivisorOf0(xu,xa))),
% 0.10/0.48 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.10/0.48 fof(f256,definition,(
% 0.10/0.48 sQ3_spl <=> (aDivisorOf0(xu,xb))),
% 0.10/0.48 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.10/0.48 fof(f259,plain,(
% 0.10/0.48 ~sQ2_spl|~sQ3_spl),
% 0.10/0.48 inference(split_clause,[status(thm)],[f222,f253,f256])).
% 0.10/0.48 fof(f308,plain,(
% 0.10/0.48 aSet0(xI)),
% 0.10/0.48 inference(resolution,[status(thm)],[f129,f208])).
% 0.10/0.48 fof(f541,definition,(
% 0.10/0.48 sQ21_spl <=> (sz10=sz00)),
% 0.10/0.48 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.10/0.48 fof(f542,plain,(
% 0.10/0.48 sz10=sz00|~sQ21_spl),
% 0.10/0.48 inference(component_clause,[status(thm)],[f541])).
% 0.10/0.48 fof(f598,plain,(
% 0.10/0.48 ~aSet0(xI)|aElement0(xu)),
% 0.10/0.48 inference(resolution,[status(thm)],[f96,f218])).
% 0.10/0.48 fof(f599,definition,(
% 0.10/0.48 sQ26_spl <=> (aSet0(xI))),
% 0.10/0.48 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.10/0.48 fof(f601,plain,(
% 0.10/0.48 ~aSet0(xI)|sQ26_spl),
% 0.10/0.48 inference(component_clause,[status(thm)],[f599])).
% 0.10/0.48 fof(f602,definition,(
% 0.10/0.48 sQ27_spl <=> (aElement0(xu))),
% 0.10/0.48 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.10/0.48 fof(f605,plain,(
% 0.10/0.48 ~sQ26_spl|sQ27_spl),
% 0.10/0.48 inference(split_clause,[status(thm)],[f598,f599,f602])).
% 0.10/0.48 fof(f606,plain,(
% 0.10/0.48 $false|sQ26_spl),
% 0.10/0.48 inference(forward_subsumption_resolution,[status(thm)],[f601,f308])).
% 0.10/0.48 fof(f607,plain,(
% 0.10/0.48 sQ26_spl),
% 0.10/0.48 inference(contradiction_clause,[status(thm)],[f606])).
% 0.10/0.48 fof(f691,plain,(
% 0.10/0.48 aIdeal0(slsdtgt0(xa))),
% 0.10/0.48 inference(resolution,[status(thm)],[f203,f204])).
% 0.10/0.48 fof(f701,plain,(
% 0.10/0.48 aIdeal0(slsdtgt0(xb))),
% 0.10/0.48 inference(resolution,[status(thm)],[f203,f205])).
% 0.10/0.48 fof(f711,plain,(
% 0.10/0.48 aSet0(slsdtgt0(xa))),
% 0.10/0.48 inference(resolution,[status(thm)],[f691,f129])).
% 0.10/0.48 fof(f726,plain,(
% 0.10/0.48 aSet0(slsdtgt0(xb))),
% 0.10/0.48 inference(resolution,[status(thm)],[f701,f129])).
% 0.10/0.48 fof(f958,definition,(
% 0.10/0.48 sQ65_spl <=> (aSet0(slsdtgt0(xa)))),
% 0.10/0.48 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 0.10/0.48 fof(f960,plain,(
% 0.10/0.48 ~aSet0(slsdtgt0(xa))|sQ65_spl),
% 0.10/0.48 inference(component_clause,[status(thm)],[f958])).
% 0.10/0.48 fof(f969,plain,(
% 0.10/0.48 $false|sQ65_spl),
% 0.10/0.48 inference(forward_subsumption_resolution,[status(thm)],[f960,f711])).
% 0.10/0.48 fof(f970,plain,(
% 0.10/0.48 sQ65_spl),
% 0.10/0.48 inference(contradiction_clause,[status(thm)],[f969])).
% 0.10/0.48 fof(f974,plain,(
% 0.10/0.48 ~aSet0(slsdtgt0(xa))|aElement0(xa)),
% 0.10/0.48 inference(resolution,[status(thm)],[f211,f96])).
% 0.10/0.48 fof(f987,definition,(
% 0.10/0.48 sQ71_spl <=> (aElement0(xa))),
% 0.10/0.48 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 0.10/0.48 fof(f990,plain,(
% 0.10/0.48 ~sQ65_spl|sQ71_spl),
% 0.10/0.48 inference(split_clause,[status(thm)],[f974,f958,f987])).
% 0.10/0.48 fof(f1005,definition,(
% 0.10/0.48 sQ74_spl <=> (aSet0(slsdtgt0(xb)))),
% 0.10/0.48 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 0.10/0.48 fof(f1007,plain,(
% 0.10/0.48 ~aSet0(slsdtgt0(xb))|sQ74_spl),
% 0.10/0.48 inference(component_clause,[status(thm)],[f1005])).
% 0.10/0.48 fof(f1013,plain,(
% 0.10/0.48 $false|sQ74_spl),
% 0.10/0.48 inference(forward_subsumption_resolution,[status(thm)],[f1007,f726])).
% 0.10/0.48 fof(f1014,plain,(
% 0.10/0.48 sQ74_spl),
% 0.10/0.48 inference(contradiction_clause,[status(thm)],[f1013])).
% 0.10/0.48 fof(f1029,definition,(
% 0.10/0.48 sQ76_spl <=> (xu=sz00)),
% 0.10/0.48 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 0.10/0.48 fof(f1030,plain,(
% 0.10/0.48 xu=sz00|~sQ76_spl),
% 0.10/0.48 inference(component_clause,[status(thm)],[f1029])).
% 0.10/0.48 fof(f1091,plain,(
% 0.10/0.48 $false|~sQ21_spl),
% 0.10/0.48 inference(forward_subsumption_resolution,[status(thm)],[f542,f91])).
% 0.10/0.48 fof(f1092,plain,(
% 0.10/0.48 ~sQ21_spl),
% 0.10/0.48 inference(contradiction_clause,[status(thm)],[f1091])).
% 0.10/0.48 fof(f1093,plain,(
% 0.10/0.48 $false|~sQ76_spl),
% 0.10/0.48 inference(forward_subsumption_resolution,[status(thm)],[f1030,f219])).
% 0.10/0.48 fof(f1094,plain,(
% 0.10/0.48 ~sQ76_spl),
% 0.10/0.48 inference(contradiction_clause,[status(thm)],[f1093])).
% 0.10/0.48 fof(f1155,definition,(
% 0.10/0.48 sQ93_spl <=> (aElement0(sz10))),
% 0.10/0.48 introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition])).
% 0.10/0.48 fof(f1157,plain,(
% 0.10/0.48 ~aElement0(sz10)|sQ93_spl),
% 0.10/0.48 inference(component_clause,[status(thm)],[f1155])).
% 0.10/0.48 fof(f1159,plain,(
% 0.10/0.48 $false|sQ93_spl),
% 0.10/0.48 inference(forward_subsumption_resolution,[status(thm)],[f1157,f56])).
% 0.10/0.48 fof(f1160,plain,(
% 0.10/0.48 sQ93_spl),
% 0.10/0.48 inference(contradiction_clause,[status(thm)],[f1159])).
% 0.10/0.48 fof(f1192,plain,(
% 0.10/0.48 ~aElement0(xa)|aDivisorOf0(xu,xa)|~aElement0(xu)),
% 0.10/0.48 inference(resolution,[status(thm)],[f176,f227])).
% 0.10/0.48 fof(f1193,plain,(
% 0.10/0.48 ~sQ71_spl|sQ2_spl|~sQ27_spl),
% 0.10/0.48 inference(split_clause,[status(thm)],[f1192,f987,f253,f602])).
% 0.10/0.48 fof(f1379,plain,(
% 0.10/0.48 ~aSet0(slsdtgt0(xb))|aElement0(xb)),
% 0.10/0.48 inference(resolution,[status(thm)],[f213,f96])).
% 0.10/0.48 fof(f1392,definition,(
% 0.10/0.48 sQ110_spl <=> (aElement0(xb))),
% 0.10/0.48 introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition])).
% 0.10/0.48 fof(f1395,plain,(
% 0.10/0.48 ~sQ74_spl|sQ110_spl),
% 0.10/0.48 inference(split_clause,[status(thm)],[f1379,f1005,f1392])).
% 0.10/0.48 fof(f1483,plain,(
% 0.10/0.48 ~aElement0(xb)|aDivisorOf0(xu,xb)|~aElement0(xu)),
% 0.10/0.48 inference(resolution,[status(thm)],[f228,f176])).
% 0.10/0.48 fof(f1486,plain,(
% 0.10/0.48 ~sQ110_spl|sQ3_spl|~sQ27_spl),
% 0.10/0.48 inference(split_clause,[status(thm)],[f1483,f1392,f256,f602])).
% 0.10/0.48 fof(f1495,plain,(
% 0.10/0.48 $false),
% 0.10/0.48 inference(sat_refutation,[status(thm)],[f259,f605,f607,f970,f990,f1014,f1092,f1094,f1160,f1193,f1395,f1486])).
% 0.10/0.48 % SZS output end CNFRefutation for theBenchmark.p
% 0.10/0.51 % Elapsed time: 0.116608 seconds
% 0.10/0.51 % CPU time: 0.576643 seconds
% 0.10/0.51 % Total memory used: 114.904 MB
% 0.10/0.51 % Net memory used: 114.175 MB
%------------------------------------------------------------------------------