%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM492+3 : 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 01:43:02 PM UTC 2026
% Result : Theorem 102.46s 13.53s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM492+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n010.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Mon Sep 21 02:35:09 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 % Drodi V4.1.1
% 102.46/13.53 % Refutation found
% 102.46/13.53 % SZS status Theorem for theBenchmark: Theorem is valid
% 102.46/13.53 % SZS output start CNFRefutation for theBenchmark
% 102.46/13.53 fof(f5,axiom,(
% 102.46/13.53 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> aNaturalNumber0(sdtasdt0(W0,W1)) ) )),
% 102.46/13.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 102.46/13.53 fof(f30,definition,(
% 102.46/13.53 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> ( doDivides0(W0,W1)<=> (? [W2] :( aNaturalNumber0(W2)& W1 = sdtasdt0(W0,W2) ) )) ) )),
% 102.46/13.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 102.46/13.53 fof(f34,axiom,(
% 102.46/13.53 (! [W0,W1,W2] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1)& aNaturalNumber0(W2) )=> ( ( doDivides0(W0,W1)& doDivides0(W0,sdtpldt0(W1,W2)) )=> doDivides0(W0,W2) ) ) )),
% 102.46/13.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 102.46/13.53 fof(f39,hypothesis,(
% 102.46/13.53 ( aNaturalNumber0(xn)& aNaturalNumber0(xm)& aNaturalNumber0(xp) ) ),
% 102.46/13.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 102.46/13.53 fof(f41,hypothesis,(
% 102.46/13.53 ( xp != sz00& xp != sz10& (! [W0] :( ( aNaturalNumber0(W0)& ( (? [W1] :( aNaturalNumber0(W1)& xp = sdtasdt0(W0,W1) ))| doDivides0(W0,xp) ) )=> ( W0 = sz10| W0 = xp ) ))& isPrime0(xp)& (? [W0] :( aNaturalNumber0(W0)& sdtasdt0(xn,xm) = sdtasdt0(xp,W0) ))& doDivides0(xp,sdtasdt0(xn,xm)) ) ),
% 102.46/13.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 102.46/13.53 fof(f43,hypothesis,(
% 102.46/13.53 ( aNaturalNumber0(xr)& sdtpldt0(xp,xr) = xn& xr = sdtmndt0(xn,xp) ) ),
% 102.46/13.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 102.46/13.53 fof(f46,hypothesis,(
% 102.46/13.53 sdtasdt0(xn,xm) = sdtpldt0(sdtasdt0(xp,xm),sdtasdt0(xr,xm)) ),
% 102.46/13.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 102.46/13.53 fof(f48,hypothesis,(
% 102.46/13.53 ( (? [W0] :( aNaturalNumber0(W0)& sdtasdt0(xn,xm) = sdtasdt0(xp,W0) ))& (? [W0] :( aNaturalNumber0(W0)& sdtasdt0(xp,xm) = sdtasdt0(xp,W0) ))& doDivides0(xp,sdtasdt0(xp,xm)) ) ),
% 102.46/13.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 102.46/13.53 fof(f49,conjecture,(
% 102.46/13.53 ( (? [W0] :( aNaturalNumber0(W0)& sdtasdt0(xr,xm) = sdtasdt0(xp,W0) ))| doDivides0(xp,sdtasdt0(xr,xm)) ) ),
% 102.46/13.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 102.46/13.53 fof(f50,negated_conjecture,(
% 102.46/13.53 ~(( (? [W0] :( aNaturalNumber0(W0)& sdtasdt0(xr,xm) = sdtasdt0(xp,W0) ))| doDivides0(xp,sdtasdt0(xr,xm)) ) )),
% 102.46/13.53 inference(negated_conjecture,[status(cth)],[f49])).
% 102.46/13.53 fof(f59,plain,(
% 102.46/13.53 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|aNaturalNumber0(sdtasdt0(W0,W1)))),
% 102.46/13.53 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 102.46/13.53 fof(f60,plain,(
% 102.46/13.53 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|aNaturalNumber0(sdtasdt0(X0,X1)))),
% 102.46/13.53 inference(cnf_transformation,[status(thm)],[f59])).
% 102.46/13.53 fof(f132,plain,(
% 102.46/13.53 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|(doDivides0(W0,W1)<=>(?[W2]: (aNaturalNumber0(W2)&W1=sdtasdt0(W0,W2)))))),
% 102.46/13.53 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 102.46/13.53 fof(f133,plain,(
% 102.46/13.53 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|((~doDivides0(W0,W1)|(?[W2]: (aNaturalNumber0(W2)&W1=sdtasdt0(W0,W2))))&(doDivides0(W0,W1)|(![W2]: (~aNaturalNumber0(W2)|~W1=sdtasdt0(W0,W2))))))),
% 102.46/13.53 inference(NNF_transformation,[status(thm)],[f132])).
% 102.46/13.53 fof(f134,plain,(
% 102.46/13.53 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|((~doDivides0(W0,W1)|(aNaturalNumber0(sK1_skl(W1,W0))&W1=sdtasdt0(W0,sK1_skl(W1,W0))))&(doDivides0(W0,W1)|(![W2]: (~aNaturalNumber0(W2)|~W1=sdtasdt0(W0,W2))))))),
% 102.46/13.53 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W2,sK1_skl(W1,W0))],[f133])).
% 102.46/13.53 fof(f137,plain,(
% 102.46/13.53 ![X0,X1,X2]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|doDivides0(X0,X1)|~aNaturalNumber0(X2)|~X1=sdtasdt0(X0,X2))),
% 102.46/13.53 inference(cnf_transformation,[status(thm)],[f134])).
% 102.46/13.53 fof(f148,plain,(
% 102.46/13.53 ![W0,W1,W2]: (((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|~aNaturalNumber0(W2))|((~doDivides0(W0,W1)|~doDivides0(W0,sdtpldt0(W1,W2)))|doDivides0(W0,W2)))),
% 102.46/13.53 inference(pre_NNF_transformation,[status(thm)],[f34])).
% 102.46/13.53 fof(f149,plain,(
% 102.46/13.53 ![X0,X1,X2]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~doDivides0(X0,X1)|~doDivides0(X0,sdtpldt0(X1,X2))|doDivides0(X0,X2))),
% 102.46/13.53 inference(cnf_transformation,[status(thm)],[f148])).
% 102.46/13.53 fof(f170,plain,(
% 102.46/13.53 aNaturalNumber0(xm)),
% 102.46/13.53 inference(cnf_transformation,[status(thm)],[f39])).
% 102.46/13.53 fof(f171,plain,(
% 102.46/13.53 aNaturalNumber0(xp)),
% 102.46/13.53 inference(cnf_transformation,[status(thm)],[f39])).
% 102.46/13.53 fof(f183,plain,(
% 102.46/13.53 ((((~xp=sz00&~xp=sz10)&(![W0]: ((~aNaturalNumber0(W0)|((![W1]: (~aNaturalNumber0(W1)|~xp=sdtasdt0(W0,W1)))&~doDivides0(W0,xp)))|(W0=sz10|W0=xp))))&isPrime0(xp))&(?[W0]: (aNaturalNumber0(W0)&sdtasdt0(xn,xm)=sdtasdt0(xp,W0))))&doDivides0(xp,sdtasdt0(xn,xm))),
% 102.46/13.53 inference(pre_NNF_transformation,[status(thm)],[f41])).
% 102.46/13.53 fof(f184,plain,(
% 102.46/13.53 ((((~xp=sz00&~xp=sz10)&(![W0]: ((~aNaturalNumber0(W0)|((![W1]: (~aNaturalNumber0(W1)|~xp=sdtasdt0(W0,W1)))&~doDivides0(W0,xp)))|(W0=sz10|W0=xp))))&isPrime0(xp))&(aNaturalNumber0(sK5_skl)&sdtasdt0(xn,xm)=sdtasdt0(xp,sK5_skl)))&doDivides0(xp,sdtasdt0(xn,xm))),
% 102.46/13.53 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(W0,sK5_skl)],[f183])).
% 102.46/13.53 fof(f190,plain,(
% 102.46/13.53 aNaturalNumber0(sK5_skl)),
% 102.46/13.53 inference(cnf_transformation,[status(thm)],[f184])).
% 102.46/13.53 fof(f191,plain,(
% 102.46/13.53 sdtasdt0(xn,xm)=sdtasdt0(xp,sK5_skl)),
% 102.46/13.53 inference(cnf_transformation,[status(thm)],[f184])).
% 102.46/13.53 fof(f197,plain,(
% 102.46/13.53 aNaturalNumber0(xr)),
% 102.46/13.53 inference(cnf_transformation,[status(thm)],[f43])).
% 102.46/13.53 fof(f206,plain,(
% 102.46/13.53 sdtasdt0(xn,xm)=sdtpldt0(sdtasdt0(xp,xm),sdtasdt0(xr,xm))),
% 102.46/13.53 inference(cnf_transformation,[status(thm)],[f46])).
% 102.46/13.53 fof(f209,plain,(
% 102.46/13.53 ((aNaturalNumber0(sK8_skl)&sdtasdt0(xn,xm)=sdtasdt0(xp,sK8_skl))&(aNaturalNumber0(sK9_skl)&sdtasdt0(xp,xm)=sdtasdt0(xp,sK9_skl)))&doDivides0(xp,sdtasdt0(xp,xm))),
% 102.46/13.53 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl,sK9_skl]),skolemize(W0,sK8_skl),skolemize(W0,sK9_skl)],[f48])).
% 102.46/13.53 fof(f211,plain,(
% 102.46/13.53 sdtasdt0(xn,xm)=sdtasdt0(xp,sK8_skl)),
% 102.46/13.53 inference(cnf_transformation,[status(thm)],[f209])).
% 102.46/13.53 fof(f212,plain,(
% 102.46/13.53 aNaturalNumber0(sK9_skl)),
% 102.46/13.53 inference(cnf_transformation,[status(thm)],[f209])).
% 102.46/13.53 fof(f213,plain,(
% 102.46/13.53 sdtasdt0(xp,xm)=sdtasdt0(xp,sK9_skl)),
% 102.46/13.53 inference(cnf_transformation,[status(thm)],[f209])).
% 102.46/13.53 fof(f214,plain,(
% 102.46/13.53 doDivides0(xp,sdtasdt0(xp,xm))),
% 102.46/13.53 inference(cnf_transformation,[status(thm)],[f209])).
% 102.46/13.53 fof(f215,plain,(
% 102.46/13.53 ((![W0]: (~aNaturalNumber0(W0)|~sdtasdt0(xr,xm)=sdtasdt0(xp,W0)))&~doDivides0(xp,sdtasdt0(xr,xm)))),
% 102.46/13.53 inference(pre_NNF_transformation,[status(thm)],[f50])).
% 102.46/13.53 fof(f217,plain,(
% 102.46/13.53 ~doDivides0(xp,sdtasdt0(xr,xm))),
% 102.46/13.53 inference(cnf_transformation,[status(thm)],[f215])).
% 102.46/13.53 fof(f244,plain,(
% 102.46/13.53 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(sdtasdt0(X0,X1))|doDivides0(X0,sdtasdt0(X0,X1))|~aNaturalNumber0(X1))),
% 102.46/13.53 inference(destructive_equality_resolution,[status(thm)],[f137])).
% 102.46/13.53 fof(f259,plain,(
% 102.46/13.53 ![X0,X1]: (~aNaturalNumber0(X0)|doDivides0(X0,sdtasdt0(X0,X1))|~aNaturalNumber0(X1))),
% 102.46/13.53 inference(forward_subsumption_resolution,[status(thm)],[f244,f60])).
% 102.46/13.53 fof(f293,definition,(
% 102.46/13.53 sQ0_spl <=> (aNaturalNumber0(xp))),
% 102.46/13.53 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 102.46/13.53 fof(f295,plain,(
% 102.46/13.53 ~aNaturalNumber0(xp)|sQ0_spl),
% 102.46/13.53 inference(component_clause,[status(thm)],[f293])).
% 102.46/13.53 fof(f299,definition,(
% 102.46/13.53 sQ2_spl <=> (aNaturalNumber0(sdtasdt0(xr,xm)))),
% 102.46/13.53 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 102.46/13.53 fof(f301,plain,(
% 102.46/13.53 ~aNaturalNumber0(sdtasdt0(xr,xm))|sQ2_spl),
% 102.46/13.53 inference(component_clause,[status(thm)],[f299])).
% 102.46/13.53 fof(f304,plain,(
% 102.46/13.53 ~aNaturalNumber0(xr)|~aNaturalNumber0(xm)|sQ2_spl),
% 102.46/13.53 inference(resolution,[status(thm)],[f301,f60])).
% 102.46/13.53 fof(f305,definition,(
% 102.46/13.53 sQ3_spl <=> (aNaturalNumber0(xr))),
% 102.46/13.53 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 102.46/13.53 fof(f307,plain,(
% 102.46/13.53 ~aNaturalNumber0(xr)|sQ3_spl),
% 102.46/13.53 inference(component_clause,[status(thm)],[f305])).
% 102.46/13.53 fof(f308,definition,(
% 102.46/13.53 sQ4_spl <=> (aNaturalNumber0(xm))),
% 102.46/13.53 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 102.46/13.53 fof(f310,plain,(
% 102.46/13.53 ~aNaturalNumber0(xm)|sQ4_spl),
% 102.46/13.53 inference(component_clause,[status(thm)],[f308])).
% 102.46/13.53 fof(f311,plain,(
% 102.46/13.53 ~sQ3_spl|~sQ4_spl|sQ2_spl),
% 102.46/13.53 inference(split_clause,[status(thm)],[f304,f305,f308,f299])).
% 102.46/13.53 fof(f354,plain,(
% 102.46/13.53 $false|sQ4_spl),
% 102.46/13.53 inference(forward_subsumption_resolution,[status(thm)],[f310,f170])).
% 102.46/13.53 fof(f355,plain,(
% 102.46/13.53 sQ4_spl),
% 102.46/13.53 inference(contradiction_clause,[status(thm)],[f354])).
% 102.46/13.53 fof(f604,plain,(
% 102.46/13.53 $false|sQ3_spl),
% 102.46/13.53 inference(forward_subsumption_resolution,[status(thm)],[f307,f197])).
% 102.46/13.53 fof(f605,plain,(
% 102.46/13.53 sQ3_spl),
% 102.46/13.53 inference(contradiction_clause,[status(thm)],[f604])).
% 102.46/13.53 fof(f606,plain,(
% 102.46/13.53 $false|sQ0_spl),
% 102.46/13.53 inference(forward_subsumption_resolution,[status(thm)],[f295,f171])).
% 102.46/13.53 fof(f607,plain,(
% 102.46/13.53 sQ0_spl),
% 102.46/13.53 inference(contradiction_clause,[status(thm)],[f606])).
% 102.46/13.53 fof(f608,plain,(
% 102.46/13.53 ![X0]: (~aNaturalNumber0(X0)|~aNaturalNumber0(sdtasdt0(xp,xm))|~aNaturalNumber0(sdtasdt0(xr,xm))|~doDivides0(X0,sdtasdt0(xp,xm))|~doDivides0(X0,sdtasdt0(xn,xm))|doDivides0(X0,sdtasdt0(xr,xm)))),
% 102.46/13.53 inference(paramodulation,[status(thm)],[f206,f149])).
% 102.46/13.53 fof(f610,definition,(
% 102.46/13.53 ![X0]: (sQ29_spl <=> (~aNaturalNumber0(X0)|~doDivides0(X0,sdtasdt0(xp,xm))|~doDivides0(X0,sdtasdt0(xn,xm))|doDivides0(X0,sdtasdt0(xr,xm))))),
% 102.46/13.53 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 102.46/13.53 fof(f611,plain,(
% 102.46/13.54 ![X0]: (~aNaturalNumber0(X0)|~doDivides0(X0,sdtasdt0(xp,xm))|~doDivides0(X0,sdtasdt0(xn,xm))|doDivides0(X0,sdtasdt0(xr,xm))|~sQ29_spl)),
% 102.46/13.54 inference(component_clause,[status(thm)],[f610])).
% 102.46/13.54 fof(f613,definition,(
% 102.46/13.54 sQ30_spl <=> (aNaturalNumber0(sdtasdt0(xp,xm)))),
% 102.46/13.54 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 102.46/13.54 fof(f616,plain,(
% 102.46/13.54 sQ29_spl|~sQ30_spl|~sQ2_spl),
% 102.46/13.54 inference(split_clause,[status(thm)],[f608,f610,f613,f299])).
% 102.46/13.54 fof(f1497,plain,(
% 102.46/13.54 sdtasdt0(xp,sK8_skl)=sdtasdt0(xp,sK5_skl)),
% 102.46/13.54 inference(backward_demodulation,[status(thm)],[f211,f191])).
% 102.46/13.54 fof(f1695,plain,(
% 102.46/13.54 ~aNaturalNumber0(xp)|~aNaturalNumber0(sK9_skl)|aNaturalNumber0(sdtasdt0(xp,xm))),
% 102.46/13.54 inference(paramodulation,[status(thm)],[f213,f60])).
% 102.46/13.54 fof(f1696,definition,(
% 102.46/13.54 sQ135_spl <=> (aNaturalNumber0(sK9_skl))),
% 102.46/13.54 introduced(definition,[new_symbols(definition,[sQ135_spl])],[split_symbol_definition])).
% 102.46/13.54 fof(f1698,plain,(
% 102.46/13.54 ~aNaturalNumber0(sK9_skl)|sQ135_spl),
% 102.46/13.54 inference(component_clause,[status(thm)],[f1696])).
% 102.46/13.54 fof(f1707,plain,(
% 102.46/13.54 ~sQ0_spl|~sQ135_spl|sQ30_spl),
% 102.46/13.54 inference(split_clause,[status(thm)],[f1695,f293,f1696,f613])).
% 102.46/13.54 fof(f1708,plain,(
% 102.46/13.54 $false|sQ135_spl),
% 102.46/13.54 inference(forward_subsumption_resolution,[status(thm)],[f1698,f212])).
% 102.46/13.54 fof(f1709,plain,(
% 102.46/13.54 sQ135_spl),
% 102.46/13.54 inference(contradiction_clause,[status(thm)],[f1708])).
% 102.46/13.54 fof(f1710,plain,(
% 102.46/13.54 ![X0]: (~aNaturalNumber0(X0)|~doDivides0(X0,sdtasdt0(xp,xm))|~doDivides0(X0,sdtasdt0(xp,sK8_skl))|doDivides0(X0,sdtasdt0(xr,xm))|~sQ29_spl)),
% 102.46/13.54 inference(forward_demodulation,[status(thm)],[f211,f611])).
% 102.46/13.54 fof(f7073,plain,(
% 102.46/13.54 ~aNaturalNumber0(xp)|doDivides0(xp,sdtasdt0(xp,sK8_skl))|~aNaturalNumber0(sK5_skl)),
% 102.46/13.54 inference(paramodulation,[status(thm)],[f1497,f259])).
% 102.46/13.54 fof(f7075,definition,(
% 102.46/13.54 sQ656_spl <=> (aNaturalNumber0(sK5_skl))),
% 102.46/13.54 introduced(definition,[new_symbols(definition,[sQ656_spl])],[split_symbol_definition])).
% 102.46/13.54 fof(f7077,plain,(
% 102.46/13.54 ~aNaturalNumber0(sK5_skl)|sQ656_spl),
% 102.46/13.54 inference(component_clause,[status(thm)],[f7075])).
% 102.46/13.54 fof(f7082,definition,(
% 102.46/13.54 sQ658_spl <=> (doDivides0(xp,sdtasdt0(xp,sK8_skl)))),
% 102.46/13.54 introduced(definition,[new_symbols(definition,[sQ658_spl])],[split_symbol_definition])).
% 102.46/13.54 fof(f7089,plain,(
% 102.46/13.54 ~sQ0_spl|sQ658_spl|~sQ656_spl),
% 102.46/13.54 inference(split_clause,[status(thm)],[f7073,f293,f7082,f7075])).
% 102.46/13.54 fof(f7091,plain,(
% 102.46/13.54 $false|sQ656_spl),
% 102.46/13.54 inference(forward_subsumption_resolution,[status(thm)],[f7077,f190])).
% 102.46/13.54 fof(f7092,plain,(
% 102.46/13.54 sQ656_spl),
% 102.46/13.54 inference(contradiction_clause,[status(thm)],[f7091])).
% 102.46/13.54 fof(f20733,plain,(
% 102.46/13.54 ~aNaturalNumber0(xp)|~doDivides0(xp,sdtasdt0(xp,sK8_skl))|doDivides0(xp,sdtasdt0(xr,xm))|~sQ29_spl),
% 102.46/13.54 inference(resolution,[status(thm)],[f1710,f214])).
% 102.46/13.54 fof(f20736,definition,(
% 102.46/13.54 sQ1226_spl <=> (doDivides0(xp,sdtasdt0(xr,xm)))),
% 102.46/13.54 introduced(definition,[new_symbols(definition,[sQ1226_spl])],[split_symbol_definition])).
% 102.46/13.54 fof(f20737,plain,(
% 102.46/13.54 doDivides0(xp,sdtasdt0(xr,xm))|~sQ1226_spl),
% 102.46/13.54 inference(component_clause,[status(thm)],[f20736])).
% 102.46/13.54 fof(f20739,plain,(
% 102.46/13.54 ~sQ0_spl|~sQ658_spl|sQ1226_spl|~sQ29_spl),
% 102.46/13.54 inference(split_clause,[status(thm)],[f20733,f293,f7082,f20736,f610])).
% 94.63/13.58 fof(f20746,plain,(
% 94.63/13.58 $false|~sQ1226_spl),
% 94.63/13.58 inference(forward_subsumption_resolution,[status(thm)],[f20737,f217])).
% 94.63/13.58 fof(f20747,plain,(
% 94.63/13.58 ~sQ1226_spl),
% 94.63/13.58 inference(contradiction_clause,[status(thm)],[f20746])).
% 94.63/13.58 fof(f20748,plain,(
% 94.63/13.58 $false),
% 94.63/13.58 inference(sat_refutation,[status(thm)],[f311,f355,f605,f607,f616,f1707,f1709,f7089,f7092,f20739,f20747])).
% 94.63/13.58 % SZS output end CNFRefutation for theBenchmark.p
% 94.63/13.60 % Elapsed time: 13.231410 seconds
% 94.63/13.60 % CPU time: 104.673062 seconds
% 94.63/13.60 % Total memory used: 595.251 MB
% 94.63/13.60 % Net memory used: 549.362 MB
%------------------------------------------------------------------------------