%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM498+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 : 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 01:43:03 PM UTC 2026
% Result : Theorem 7.47s 1.46s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM498+3 : 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.09/0.36 % Computer : n004.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 02:34:49 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 7.47/1.46 % Refutation found
% 7.47/1.46 % SZS status Theorem for theBenchmark: Theorem is valid
% 7.47/1.46 % SZS output start CNFRefutation for theBenchmark
% 7.47/1.46 fof(f11,axiom,(
% 7.47/1.46 (! [W0] :( aNaturalNumber0(W0)=> ( sdtasdt0(W0,sz10) = W0& W0 = sdtasdt0(sz10,W0) ) ) )),
% 7.47/1.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.47/1.46 fof(f12,axiom,(
% 7.47/1.46 (! [W0] :( aNaturalNumber0(W0)=> ( sdtasdt0(W0,sz00) = sz00& sz00 = sdtasdt0(sz00,W0) ) ) )),
% 7.47/1.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.47/1.46 fof(f17,axiom,(
% 7.47/1.46 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> ( sdtasdt0(W0,W1) = sz00=> ( W0 = sz00| W1 = sz00 ) ) ) )),
% 7.47/1.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.47/1.46 fof(f39,hypothesis,(
% 7.47/1.46 ( aNaturalNumber0(xn)& aNaturalNumber0(xm)& aNaturalNumber0(xp) ) ),
% 7.47/1.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.47/1.46 fof(f41,hypothesis,(
% 7.47/1.46 ( 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)) ) ),
% 7.47/1.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.47/1.46 fof(f44,hypothesis,(
% 7.47/1.46 ( xn != xp& (? [W0] :( aNaturalNumber0(W0)& sdtpldt0(xn,W0) = xp ))& sdtlseqdt0(xn,xp)& xm != xp& (? [W0] :( aNaturalNumber0(W0)& sdtpldt0(xm,W0) = xp ))& sdtlseqdt0(xm,xp) ) ),
% 7.47/1.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.47/1.46 fof(f45,hypothesis,(
% 7.47/1.46 ( aNaturalNumber0(xk)& sdtasdt0(xn,xm) = sdtasdt0(xp,xk)& xk = sdtsldt0(sdtasdt0(xn,xm),xp) ) ),
% 7.47/1.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.47/1.46 fof(f46,conjecture,(
% 7.47/1.46 ( ( xk = sz00| xk = sz10 )=> ( (? [W0] :( aNaturalNumber0(W0)& xn = sdtasdt0(xp,W0) ))| doDivides0(xp,xn)| (? [W0] :( aNaturalNumber0(W0)& xm = sdtasdt0(xp,W0) ))| doDivides0(xp,xm) ) ) ),
% 7.47/1.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.47/1.46 fof(f47,negated_conjecture,(
% 7.47/1.46 ~(( ( xk = sz00| xk = sz10 )=> ( (? [W0] :( aNaturalNumber0(W0)& xn = sdtasdt0(xp,W0) ))| doDivides0(xp,xn)| (? [W0] :( aNaturalNumber0(W0)& xm = sdtasdt0(xp,W0) ))| doDivides0(xp,xm) ) ) )),
% 7.47/1.46 inference(negated_conjecture,[status(cth)],[f46])).
% 7.47/1.46 fof(f69,plain,(
% 7.47/1.46 ![W0]: (~aNaturalNumber0(W0)|(sdtasdt0(W0,sz10)=W0&W0=sdtasdt0(sz10,W0)))),
% 7.47/1.46 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 7.47/1.46 fof(f70,plain,(
% 7.47/1.46 ![X0]: (~aNaturalNumber0(X0)|sdtasdt0(X0,sz10)=X0)),
% 7.47/1.46 inference(cnf_transformation,[status(thm)],[f69])).
% 7.47/1.46 fof(f71,plain,(
% 7.47/1.46 ![X0]: (~aNaturalNumber0(X0)|X0=sdtasdt0(sz10,X0))),
% 7.47/1.46 inference(cnf_transformation,[status(thm)],[f69])).
% 7.47/1.46 fof(f72,plain,(
% 7.47/1.46 ![W0]: (~aNaturalNumber0(W0)|(sdtasdt0(W0,sz00)=sz00&sz00=sdtasdt0(sz00,W0)))),
% 7.47/1.46 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 7.47/1.46 fof(f73,plain,(
% 7.47/1.46 ![X0]: (~aNaturalNumber0(X0)|sdtasdt0(X0,sz00)=sz00)),
% 7.47/1.46 inference(cnf_transformation,[status(thm)],[f72])).
% 7.47/1.46 fof(f87,plain,(
% 7.47/1.46 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|(~sdtasdt0(W0,W1)=sz00|(W0=sz00|W1=sz00)))),
% 7.47/1.46 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 7.47/1.46 fof(f88,plain,(
% 7.47/1.46 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|~sdtasdt0(X0,X1)=sz00|X0=sz00|X1=sz00)),
% 7.47/1.46 inference(cnf_transformation,[status(thm)],[f87])).
% 7.47/1.46 fof(f166,plain,(
% 7.47/1.46 aNaturalNumber0(xn)),
% 7.47/1.46 inference(cnf_transformation,[status(thm)],[f39])).
% 7.47/1.46 fof(f167,plain,(
% 7.47/1.46 aNaturalNumber0(xm)),
% 7.47/1.46 inference(cnf_transformation,[status(thm)],[f39])).
% 7.47/1.46 fof(f168,plain,(
% 7.47/1.46 aNaturalNumber0(xp)),
% 7.47/1.46 inference(cnf_transformation,[status(thm)],[f39])).
% 7.47/1.46 fof(f180,plain,(
% 7.47/1.46 ((((~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))),
% 7.47/1.46 inference(pre_NNF_transformation,[status(thm)],[f41])).
% 7.47/1.46 fof(f181,plain,(
% 7.47/1.46 ((((~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))),
% 7.47/1.46 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(W0,sK5_skl)],[f180])).
% 7.47/1.46 fof(f184,plain,(
% 7.47/1.46 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|~xp=sdtasdt0(X0,X1)|X0=sz10|X0=xp)),
% 7.47/1.46 inference(cnf_transformation,[status(thm)],[f181])).
% 7.47/1.46 fof(f187,plain,(
% 7.47/1.46 aNaturalNumber0(sK5_skl)),
% 7.47/1.46 inference(cnf_transformation,[status(thm)],[f181])).
% 7.47/1.46 fof(f188,plain,(
% 7.47/1.46 sdtasdt0(xn,xm)=sdtasdt0(xp,sK5_skl)),
% 7.47/1.46 inference(cnf_transformation,[status(thm)],[f181])).
% 7.47/1.46 fof(f189,plain,(
% 7.47/1.46 doDivides0(xp,sdtasdt0(xn,xm))),
% 7.47/1.46 inference(cnf_transformation,[status(thm)],[f181])).
% 7.47/1.46 fof(f196,plain,(
% 7.47/1.46 ((((~xn=xp&(aNaturalNumber0(sK6_skl)&sdtpldt0(xn,sK6_skl)=xp))&sdtlseqdt0(xn,xp))&~xm=xp)&(aNaturalNumber0(sK7_skl)&sdtpldt0(xm,sK7_skl)=xp))&sdtlseqdt0(xm,xp)),
% 7.47/1.46 inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl,sK7_skl]),skolemize(W0,sK6_skl),skolemize(W0,sK7_skl)],[f44])).
% 7.47/1.46 fof(f197,plain,(
% 7.47/1.46 ~xn=xp),
% 7.47/1.46 inference(cnf_transformation,[status(thm)],[f196])).
% 7.47/1.46 fof(f206,plain,(
% 7.47/1.46 sdtasdt0(xn,xm)=sdtasdt0(xp,xk)),
% 7.47/1.46 inference(cnf_transformation,[status(thm)],[f45])).
% 7.47/1.46 fof(f208,plain,(
% 7.47/1.46 ((xk=sz00|xk=sz10)&((((![W0]: (~aNaturalNumber0(W0)|~xn=sdtasdt0(xp,W0)))&~doDivides0(xp,xn))&(![W0]: (~aNaturalNumber0(W0)|~xm=sdtasdt0(xp,W0))))&~doDivides0(xp,xm)))),
% 7.47/1.46 inference(pre_NNF_transformation,[status(thm)],[f47])).
% 7.47/1.46 fof(f209,plain,(
% 7.47/1.46 xk=sz00|xk=sz10),
% 7.47/1.46 inference(cnf_transformation,[status(thm)],[f208])).
% 7.47/1.46 fof(f210,plain,(
% 7.47/1.46 ![X0]: (~aNaturalNumber0(X0)|~xn=sdtasdt0(xp,X0))),
% 7.47/1.46 inference(cnf_transformation,[status(thm)],[f208])).
% 7.47/1.46 fof(f212,plain,(
% 7.47/1.46 ![X0]: (~aNaturalNumber0(X0)|~xm=sdtasdt0(xp,X0))),
% 7.47/1.46 inference(cnf_transformation,[status(thm)],[f208])).
% 7.47/1.46 fof(f213,plain,(
% 7.47/1.46 ~doDivides0(xp,xm)),
% 7.47/1.46 inference(cnf_transformation,[status(thm)],[f208])).
% 7.47/1.46 fof(f234,definition,(
% 7.47/1.46 sQ0_spl <=> (xk=sz00)),
% 7.47/1.46 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 7.47/1.46 fof(f235,plain,(
% 7.47/1.46 xk=sz00|~sQ0_spl),
% 7.47/1.46 inference(component_clause,[status(thm)],[f234])).
% 7.47/1.46 fof(f237,definition,(
% 7.47/1.46 sQ1_spl <=> (xk=sz10)),
% 7.47/1.46 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 7.47/1.46 fof(f238,plain,(
% 7.47/1.46 xk=sz10|~sQ1_spl),
% 7.47/1.46 inference(component_clause,[status(thm)],[f237])).
% 7.47/1.46 fof(f240,plain,(
% 7.47/1.46 sQ0_spl|sQ1_spl),
% 7.47/1.46 inference(split_clause,[status(thm)],[f209,f234,f237])).
% 7.47/1.46 fof(f246,plain,(
% 7.47/1.46 sdtasdt0(xn,xm)=sdtasdt0(xp,sz00)|~sQ0_spl),
% 7.47/1.46 inference(backward_demodulation,[status(thm)],[f235,f206])).
% 7.47/1.46 fof(f294,definition,(
% 7.47/1.46 sQ5_spl <=> (xm=sz00)),
% 7.47/1.46 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 7.47/1.46 fof(f304,definition,(
% 7.47/1.46 sQ8_spl <=> (xn=sz00)),
% 7.47/1.46 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 7.47/1.46 fof(f307,definition,(
% 7.47/1.46 sQ9_spl <=> (xn=sz10)),
% 7.47/1.46 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 7.47/1.46 fof(f308,plain,(
% 7.47/1.46 xn=sz10|~sQ9_spl),
% 7.47/1.46 inference(component_clause,[status(thm)],[f307])).
% 7.47/1.46 fof(f350,plain,(
% 7.47/1.46 doDivides0(xp,sdtasdt0(sz10,xm))|~sQ9_spl),
% 7.47/1.46 inference(backward_demodulation,[status(thm)],[f308,f189])).
% 7.47/1.46 fof(f465,plain,(
% 7.47/1.46 sdtasdt0(xn,xm)=sdtasdt0(xp,sz10)|~sQ1_spl),
% 7.47/1.46 inference(forward_demodulation,[status(thm)],[f238,f206])).
% 7.47/1.46 fof(f513,definition,(
% 7.47/1.46 sQ37_spl <=> (aNaturalNumber0(xn))),
% 7.47/1.46 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 7.47/1.46 fof(f515,plain,(
% 7.47/1.46 ~aNaturalNumber0(xn)|sQ37_spl),
% 7.47/1.46 inference(component_clause,[status(thm)],[f513])).
% 7.47/1.46 fof(f516,definition,(
% 7.47/1.46 sQ38_spl <=> (aNaturalNumber0(xm))),
% 7.47/1.46 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 7.47/1.46 fof(f518,plain,(
% 7.47/1.46 ~aNaturalNumber0(xm)|sQ38_spl),
% 7.47/1.46 inference(component_clause,[status(thm)],[f516])).
% 7.47/1.46 fof(f591,definition,(
% 7.47/1.46 sQ54_spl <=> (xp=sdtasdt0(xp,sz10))),
% 7.47/1.46 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 7.47/1.46 fof(f592,plain,(
% 7.47/1.46 xp=sdtasdt0(xp,sz10)|~sQ54_spl),
% 7.47/1.46 inference(component_clause,[status(thm)],[f591])).
% 7.47/1.46 fof(f593,plain,(
% 7.47/1.46 ~xp=sdtasdt0(xp,sz10)|sQ54_spl),
% 7.47/1.46 inference(component_clause,[status(thm)],[f591])).
% 7.47/1.46 fof(f607,plain,(
% 7.47/1.46 $false|sQ38_spl),
% 7.47/1.46 inference(forward_subsumption_resolution,[status(thm)],[f518,f167])).
% 7.47/1.46 fof(f608,plain,(
% 7.47/1.46 sQ38_spl),
% 7.47/1.46 inference(contradiction_clause,[status(thm)],[f607])).
% 7.47/1.46 fof(f609,plain,(
% 7.47/1.46 $false|sQ37_spl),
% 7.47/1.46 inference(forward_subsumption_resolution,[status(thm)],[f515,f166])).
% 7.47/1.46 fof(f610,plain,(
% 7.47/1.46 sQ37_spl),
% 7.47/1.46 inference(contradiction_clause,[status(thm)],[f609])).
% 7.47/1.46 fof(f624,definition,(
% 7.47/1.46 sQ56_spl <=> (sdtasdt0(xn,xm)=sz00)),
% 7.47/1.46 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 7.47/1.46 fof(f625,plain,(
% 7.47/1.46 sdtasdt0(xn,xm)=sz00|~sQ56_spl),
% 7.47/1.46 inference(component_clause,[status(thm)],[f624])).
% 7.47/1.46 fof(f667,plain,(
% 7.47/1.46 sdtasdt0(xn,xm)=xp|~sQ54_spl|~sQ1_spl),
% 7.47/1.46 inference(forward_demodulation,[status(thm)],[f592,f465])).
% 7.47/1.46 fof(f674,plain,(
% 7.47/1.46 ~aNaturalNumber0(xn)|~aNaturalNumber0(xm)|xn=sz10|xn=xp|~sQ54_spl|~sQ1_spl),
% 7.47/1.46 inference(resolution,[status(thm)],[f667,f184])).
% 7.47/1.46 fof(f679,definition,(
% 7.47/1.46 sQ62_spl <=> (xn=xp)),
% 7.47/1.46 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 7.47/1.46 fof(f680,plain,(
% 7.47/1.46 xn=xp|~sQ62_spl),
% 7.47/1.46 inference(component_clause,[status(thm)],[f679])).
% 7.47/1.46 fof(f682,plain,(
% 7.47/1.46 ~sQ37_spl|~sQ38_spl|sQ9_spl|sQ62_spl|~sQ54_spl|~sQ1_spl),
% 7.47/1.46 inference(split_clause,[status(thm)],[f674,f513,f516,f307,f679,f591,f237])).
% 7.47/1.46 fof(f699,plain,(
% 7.47/1.46 $false|~sQ62_spl),
% 7.47/1.46 inference(forward_subsumption_resolution,[status(thm)],[f680,f197])).
% 7.47/1.46 fof(f700,plain,(
% 7.47/1.46 ~sQ62_spl),
% 7.47/1.46 inference(contradiction_clause,[status(thm)],[f699])).
% 7.47/1.46 fof(f838,plain,(
% 7.47/1.46 sdtasdt0(xp,sz10)=xp),
% 7.47/1.46 inference(resolution,[status(thm)],[f70,f168])).
% 7.47/1.46 fof(f1436,definition,(
% 7.47/1.46 sQ131_spl <=> (aNaturalNumber0(sK5_skl))),
% 7.47/1.46 introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition])).
% 7.47/1.46 fof(f1438,plain,(
% 7.47/1.46 ~aNaturalNumber0(sK5_skl)|sQ131_spl),
% 7.47/1.46 inference(component_clause,[status(thm)],[f1436])).
% 7.47/1.46 fof(f1716,plain,(
% 7.47/1.46 xm=sdtasdt0(sz10,xm)),
% 7.47/1.46 inference(resolution,[status(thm)],[f71,f167])).
% 7.47/1.46 fof(f1721,plain,(
% 7.47/1.46 sdtasdt0(xp,sz00)=sz00),
% 7.47/1.46 inference(resolution,[status(thm)],[f73,f168])).
% 7.47/1.46 fof(f1724,plain,(
% 7.47/1.46 sdtasdt0(xn,xm)=sz00|~sQ0_spl),
% 7.47/1.46 inference(backward_demodulation,[status(thm)],[f1721,f246])).
% 7.47/1.46 fof(f1726,plain,(
% 7.47/1.46 sQ56_spl|~sQ0_spl),
% 7.47/1.46 inference(split_clause,[status(thm)],[f1724,f624,f234])).
% 7.47/1.46 fof(f1730,plain,(
% 7.47/1.46 sz00=sdtasdt0(xp,sK5_skl)|~sQ56_spl),
% 7.47/1.46 inference(backward_demodulation,[status(thm)],[f625,f188])).
% 7.47/1.46 fof(f2126,plain,(
% 7.47/1.46 ~aNaturalNumber0(sK5_skl)|~xn=sz00|~sQ56_spl),
% 7.47/1.46 inference(paramodulation,[status(thm)],[f1730,f210])).
% 7.47/1.46 fof(f2127,plain,(
% 7.47/1.46 ~aNaturalNumber0(sK5_skl)|~xm=sz00|~sQ56_spl),
% 7.47/1.46 inference(paramodulation,[status(thm)],[f1730,f212])).
% 7.47/1.46 fof(f2142,plain,(
% 7.47/1.46 ~sQ131_spl|~sQ8_spl|~sQ56_spl),
% 7.47/1.46 inference(split_clause,[status(thm)],[f2126,f1436,f304,f624])).
% 7.47/1.46 fof(f2143,plain,(
% 7.47/1.46 ~sQ131_spl|~sQ5_spl|~sQ56_spl),
% 7.47/1.46 inference(split_clause,[status(thm)],[f2127,f1436,f294,f624])).
% 7.47/1.46 fof(f2154,plain,(
% 7.47/1.46 $false|sQ131_spl),
% 7.47/1.46 inference(forward_subsumption_resolution,[status(thm)],[f1438,f187])).
% 7.47/1.46 fof(f2155,plain,(
% 7.47/1.46 sQ131_spl),
% 7.47/1.46 inference(contradiction_clause,[status(thm)],[f2154])).
% 7.47/1.46 fof(f2470,plain,(
% 7.47/1.46 ~xp=xp|sQ54_spl),
% 7.47/1.46 inference(forward_demodulation,[status(thm)],[f838,f593])).
% 7.47/1.46 fof(f2471,plain,(
% 7.47/1.46 $false|sQ54_spl),
% 7.47/1.46 inference(trivial_equality_resolution,[status(thm)],[f2470])).
% 7.47/1.46 fof(f2472,plain,(
% 7.47/1.46 sQ54_spl),
% 7.47/1.46 inference(contradiction_clause,[status(thm)],[f2471])).
% 7.47/1.46 fof(f2536,plain,(
% 7.47/1.46 sdtasdt0(xn,xm)=sdtasdt0(xp,sz00)|~sQ0_spl),
% 7.47/1.46 inference(forward_demodulation,[status(thm)],[f235,f206])).
% 7.47/1.46 fof(f2544,plain,(
% 7.47/1.46 sdtasdt0(xn,xm)=sz00|~sQ0_spl),
% 7.47/1.46 inference(forward_demodulation,[status(thm)],[f1721,f2536])).
% 7.47/1.46 fof(f2985,plain,(
% 7.47/1.46 ~aNaturalNumber0(xn)|~aNaturalNumber0(xm)|xn=sz00|xm=sz00|~sQ0_spl),
% 7.47/1.46 inference(resolution,[status(thm)],[f88,f2544])).
% 7.47/1.46 fof(f2989,plain,(
% 7.47/1.46 ~sQ37_spl|~sQ38_spl|sQ8_spl|sQ5_spl|~sQ0_spl),
% 7.47/1.46 inference(split_clause,[status(thm)],[f2985,f513,f516,f304,f294,f234])).
% 7.47/1.46 fof(f3113,plain,(
% 7.47/1.46 doDivides0(xp,xm)|~sQ9_spl),
% 7.47/1.46 inference(forward_demodulation,[status(thm)],[f1716,f350])).
% 7.47/1.46 fof(f3114,plain,(
% 7.47/1.46 $false|~sQ9_spl),
% 7.47/1.46 inference(forward_subsumption_resolution,[status(thm)],[f3113,f213])).
% 8.30/1.47 fof(f3115,plain,(
% 8.30/1.47 ~sQ9_spl),
% 8.30/1.47 inference(contradiction_clause,[status(thm)],[f3114])).
% 8.30/1.47 fof(f3116,plain,(
% 8.30/1.47 $false),
% 8.30/1.47 inference(sat_refutation,[status(thm)],[f240,f608,f610,f682,f700,f1726,f2142,f2143,f2155,f2472,f2989,f3115])).
% 8.30/1.47 % SZS output end CNFRefutation for theBenchmark.p
% 8.30/1.49 % Elapsed time: 1.110576 seconds
% 8.30/1.49 % CPU time: 8.511465 seconds
% 8.30/1.49 % Total memory used: 179.663 MB
% 8.30/1.49 % Net memory used: 172.605 MB
%------------------------------------------------------------------------------