%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM514+1 : 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 : n016.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:05 PM UTC 2026
% Result : Theorem 0.15s 10.86s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM514+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/10.37 % Computer : n016.cluster.edu
% 0.10/10.37 % Model : x86_64 x86_64
% 0.10/10.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/10.37 % Memory : 8046.5625MB
% 0.10/10.37 % OS : Linux 6.8.0-71-generic
% 0.10/10.38 % CPULimit : 300
% 0.10/10.38 % WCLimit : 300
% 0.10/10.38 % DateTime : Mon Sep 21 02:42:03 UTC 2026
% 0.10/10.38 % CPUTime :
% 0.15/10.40 % Drodi V4.1.1
% 0.15/10.86 % Refutation found
% 0.15/10.86 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.15/10.86 % SZS output start CNFRefutation for theBenchmark
% 0.15/10.86 fof(f2,axiom,(
% 0.15/10.86 aNaturalNumber0(sz00) ),
% 0.15/10.86 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/10.86 fof(f5,axiom,(
% 0.15/10.86 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> aNaturalNumber0(sdtasdt0(W0,W1)) ) )),
% 0.15/10.86 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/10.86 fof(f30,definition,(
% 0.15/10.86 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> ( doDivides0(W0,W1)<=> (? [W2] :( aNaturalNumber0(W2)& W1 = sdtasdt0(W0,W2) ) )) ) )),
% 0.15/10.86 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/10.86 fof(f31,definition,(
% 0.15/10.86 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> ( ( W0 != sz00& doDivides0(W0,W1) )=> (! [W2] :( W2 = sdtsldt0(W1,W0)<=> ( aNaturalNumber0(W2)& W1 = sdtasdt0(W0,W2) ) ) )) ) )),
% 0.15/10.86 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/10.86 fof(f37,definition,(
% 0.15/10.86 (! [W0] :( aNaturalNumber0(W0)=> ( isPrime0(W0)<=> ( W0 != sz00& W0 != sz10& (! [W1] :( ( aNaturalNumber0(W1)& doDivides0(W1,W0) )=> ( W1 = sz10| W1 = W0 ) ) )) ) ) )),
% 0.15/10.86 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/10.86 fof(f39,hypothesis,(
% 0.15/10.86 ( aNaturalNumber0(xn)& aNaturalNumber0(xm)& aNaturalNumber0(xp) ) ),
% 0.15/10.86 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/10.86 fof(f41,hypothesis,(
% 0.15/10.86 ( isPrime0(xp)& doDivides0(xp,sdtasdt0(xn,xm)) ) ),
% 0.15/10.86 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/10.86 fof(f45,hypothesis,(
% 0.15/10.86 xk = sdtsldt0(sdtasdt0(xn,xm),xp) ),
% 0.15/10.86 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/10.86 fof(f48,hypothesis,(
% 0.15/10.86 ( aNaturalNumber0(xr)& doDivides0(xr,xk)& isPrime0(xr) ) ),
% 0.15/10.86 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/10.86 fof(f55,hypothesis,(
% 0.15/10.86 sdtasdt0(xp,sdtsldt0(xk,xr)) = sdtasdt0(sdtsldt0(xn,xr),xm) ),
% 0.15/10.86 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/10.86 fof(f56,conjecture,(
% 0.15/10.86 doDivides0(xp,sdtasdt0(sdtsldt0(xn,xr),xm)) ),
% 0.15/10.86 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/10.86 fof(f57,negated_conjecture,(
% 0.15/10.86 ~(doDivides0(xp,sdtasdt0(sdtsldt0(xn,xr),xm)) )),
% 0.15/10.86 inference(negated_conjecture,[status(cth)],[f56])).
% 0.15/10.86 fof(f61,plain,(
% 0.15/10.86 aNaturalNumber0(sz00)),
% 0.15/10.86 inference(cnf_transformation,[status(thm)],[f2])).
% 0.15/10.86 fof(f66,plain,(
% 0.15/10.86 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|aNaturalNumber0(sdtasdt0(W0,W1)))),
% 0.15/10.86 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.15/10.86 fof(f67,plain,(
% 0.15/10.86 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|aNaturalNumber0(sdtasdt0(X0,X1)))),
% 0.15/10.86 inference(cnf_transformation,[status(thm)],[f66])).
% 0.15/10.86 fof(f139,plain,(
% 0.15/10.86 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|(doDivides0(W0,W1)<=>(?[W2]: (aNaturalNumber0(W2)&W1=sdtasdt0(W0,W2)))))),
% 0.15/10.86 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 0.15/10.86 fof(f140,plain,(
% 0.15/10.86 ![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))))))),
% 0.15/10.86 inference(NNF_transformation,[status(thm)],[f139])).
% 0.15/10.86 fof(f141,plain,(
% 0.15/10.86 ![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))))))),
% 0.15/10.86 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W2,sK1_skl(W1,W0))],[f140])).
% 0.15/10.86 fof(f144,plain,(
% 0.15/10.86 ![X0,X1,X2]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|doDivides0(X0,X1)|~aNaturalNumber0(X2)|~X1=sdtasdt0(X0,X2))),
% 0.15/10.86 inference(cnf_transformation,[status(thm)],[f141])).
% 0.15/10.86 fof(f145,plain,(
% 0.15/10.86 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|((W0=sz00|~doDivides0(W0,W1))|(![W2]: (W2=sdtsldt0(W1,W0)<=>(aNaturalNumber0(W2)&W1=sdtasdt0(W0,W2))))))),
% 0.15/10.86 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 0.15/10.86 fof(f146,plain,(
% 0.15/10.86 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|((W0=sz00|~doDivides0(W0,W1))|(![W2]: ((~W2=sdtsldt0(W1,W0)|(aNaturalNumber0(W2)&W1=sdtasdt0(W0,W2)))&(W2=sdtsldt0(W1,W0)|(~aNaturalNumber0(W2)|~W1=sdtasdt0(W0,W2)))))))),
% 0.15/10.86 inference(NNF_transformation,[status(thm)],[f145])).
% 0.15/10.86 fof(f147,plain,(
% 0.15/10.86 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|((W0=sz00|~doDivides0(W0,W1))|((![W2]: (~W2=sdtsldt0(W1,W0)|(aNaturalNumber0(W2)&W1=sdtasdt0(W0,W2))))&(![W2]: (W2=sdtsldt0(W1,W0)|(~aNaturalNumber0(W2)|~W1=sdtasdt0(W0,W2)))))))),
% 0.15/10.86 inference(miniscoping,[status(thm)],[f146])).
% 0.15/10.86 fof(f148,plain,(
% 0.15/10.86 ![X0,X1,X2]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|X0=sz00|~doDivides0(X0,X1)|~X2=sdtsldt0(X1,X0)|aNaturalNumber0(X2))),
% 0.15/10.86 inference(cnf_transformation,[status(thm)],[f147])).
% 0.15/10.86 fof(f161,plain,(
% 0.15/10.86 ![W0]: (~aNaturalNumber0(W0)|(isPrime0(W0)<=>((~W0=sz00&~W0=sz10)&(![W1]: ((~aNaturalNumber0(W1)|~doDivides0(W1,W0))|(W1=sz10|W1=W0))))))),
% 0.15/10.86 inference(pre_NNF_transformation,[status(thm)],[f37])).
% 0.15/10.86 fof(f162,plain,(
% 0.15/10.86 ![W0]: (~aNaturalNumber0(W0)|((~isPrime0(W0)|((~W0=sz00&~W0=sz10)&(![W1]: ((~aNaturalNumber0(W1)|~doDivides0(W1,W0))|(W1=sz10|W1=W0)))))&(isPrime0(W0)|((W0=sz00|W0=sz10)|(?[W1]: ((aNaturalNumber0(W1)&doDivides0(W1,W0))&(~W1=sz10&~W1=W0)))))))),
% 0.15/10.86 inference(NNF_transformation,[status(thm)],[f161])).
% 0.15/10.86 fof(f163,plain,(
% 0.15/10.86 ![W0]: (~aNaturalNumber0(W0)|((~isPrime0(W0)|((~W0=sz00&~W0=sz10)&(![W1]: ((~aNaturalNumber0(W1)|~doDivides0(W1,W0))|(W1=sz10|W1=W0)))))&(isPrime0(W0)|((W0=sz00|W0=sz10)|((aNaturalNumber0(sK2_skl(W0))&doDivides0(sK2_skl(W0),W0))&(~sK2_skl(W0)=sz10&~sK2_skl(W0)=W0))))))),
% 0.15/10.86 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(W1,sK2_skl(W0))],[f162])).
% 0.15/10.86 fof(f164,plain,(
% 0.15/10.86 ![X0]: (~aNaturalNumber0(X0)|~isPrime0(X0)|~X0=sz00)),
% 0.15/10.86 inference(cnf_transformation,[status(thm)],[f163])).
% 0.15/10.86 fof(f176,plain,(
% 0.15/10.86 aNaturalNumber0(xn)),
% 0.15/10.86 inference(cnf_transformation,[status(thm)],[f39])).
% 0.15/10.86 fof(f177,plain,(
% 0.15/10.86 aNaturalNumber0(xm)),
% 0.15/10.86 inference(cnf_transformation,[status(thm)],[f39])).
% 0.15/10.86 fof(f178,plain,(
% 0.15/10.86 aNaturalNumber0(xp)),
% 0.15/10.86 inference(cnf_transformation,[status(thm)],[f39])).
% 0.15/10.86 fof(f181,plain,(
% 0.15/10.86 isPrime0(xp)),
% 0.15/10.86 inference(cnf_transformation,[status(thm)],[f41])).
% 0.15/10.86 fof(f182,plain,(
% 0.15/10.86 doDivides0(xp,sdtasdt0(xn,xm))),
% 0.15/10.86 inference(cnf_transformation,[status(thm)],[f41])).
% 0.15/10.86 fof(f189,plain,(
% 0.15/10.86 xk=sdtsldt0(sdtasdt0(xn,xm),xp)),
% 0.15/10.86 inference(cnf_transformation,[status(thm)],[f45])).
% 0.15/10.86 fof(f195,plain,(
% 0.15/10.86 aNaturalNumber0(xr)),
% 0.15/10.86 inference(cnf_transformation,[status(thm)],[f48])).
% 0.15/10.86 fof(f196,plain,(
% 0.15/10.86 doDivides0(xr,xk)),
% 0.15/10.86 inference(cnf_transformation,[status(thm)],[f48])).
% 0.15/10.86 fof(f197,plain,(
% 0.15/10.86 isPrime0(xr)),
% 0.15/10.86 inference(cnf_transformation,[status(thm)],[f48])).
% 0.15/10.86 fof(f208,plain,(
% 0.15/10.86 sdtasdt0(xp,sdtsldt0(xk,xr))=sdtasdt0(sdtsldt0(xn,xr),xm)),
% 0.15/10.86 inference(cnf_transformation,[status(thm)],[f55])).
% 0.15/10.86 fof(f209,plain,(
% 0.15/10.86 ~doDivides0(xp,sdtasdt0(sdtsldt0(xn,xr),xm))),
% 0.15/10.86 inference(cnf_transformation,[status(thm)],[f57])).
% 0.15/10.86 fof(f225,plain,(
% 0.15/10.86 ![X0,X2]: (~aNaturalNumber0(X0)|~aNaturalNumber0(sdtasdt0(X0,X2))|doDivides0(X0,sdtasdt0(X0,X2))|~aNaturalNumber0(X2))),
% 0.15/10.86 inference(destructive_equality_resolution,[status(thm)],[f144])).
% 0.15/10.86 fof(f226,plain,(
% 0.15/10.86 ![X0,X1]: (~aNaturalNumber0(X0)|doDivides0(X0,sdtasdt0(X0,X1))|~aNaturalNumber0(X1))),
% 0.15/10.86 inference(forward_subsumption_resolution,[status(thm)],[f225,f67])).
% 0.15/10.86 fof(f227,plain,(
% 0.15/10.86 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|X0=sz00|~doDivides0(X0,X1)|aNaturalNumber0(sdtsldt0(X1,X0)))),
% 0.15/10.86 inference(destructive_equality_resolution,[status(thm)],[f148])).
% 0.15/10.86 fof(f231,plain,(
% 0.15/10.86 ~aNaturalNumber0(sz00)|~isPrime0(sz00)),
% 0.15/10.86 inference(destructive_equality_resolution,[status(thm)],[f164])).
% 0.15/10.86 fof(f232,plain,(
% 0.15/10.86 ~isPrime0(sz00)),
% 0.15/10.86 inference(forward_subsumption_resolution,[status(thm)],[f231,f61])).
% 0.15/10.86 fof(f236,plain,(
% 0.15/10.86 ~doDivides0(xp,sdtasdt0(xp,sdtsldt0(xk,xr)))),
% 0.15/10.86 inference(forward_demodulation,[status(thm)],[f208,f209])).
% 0.15/10.86 fof(f306,plain,(
% 0.15/10.86 ~aNaturalNumber0(xp)|~aNaturalNumber0(sdtsldt0(xk,xr))),
% 0.15/10.86 inference(resolution,[status(thm)],[f226,f236])).
% 0.15/10.86 fof(f307,definition,(
% 0.15/10.86 sQ2_spl <=> (aNaturalNumber0(xp))),
% 0.15/10.86 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.15/10.86 fof(f309,plain,(
% 0.15/10.86 ~aNaturalNumber0(xp)|sQ2_spl),
% 0.15/10.86 inference(component_clause,[status(thm)],[f307])).
% 0.15/10.86 fof(f310,definition,(
% 0.15/10.86 sQ3_spl <=> (aNaturalNumber0(sdtsldt0(xk,xr)))),
% 0.15/10.86 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.15/10.86 fof(f313,plain,(
% 0.15/10.86 ~sQ2_spl|~sQ3_spl),
% 0.15/10.86 inference(split_clause,[status(thm)],[f306,f307,f310])).
% 0.15/10.86 fof(f314,plain,(
% 0.15/10.86 $false|sQ2_spl),
% 0.15/10.86 inference(forward_subsumption_resolution,[status(thm)],[f309,f178])).
% 0.15/10.86 fof(f315,plain,(
% 0.15/10.86 sQ2_spl),
% 0.15/10.86 inference(contradiction_clause,[status(thm)],[f314])).
% 0.15/10.86 fof(f332,definition,(
% 0.15/10.86 sQ6_spl <=> (aNaturalNumber0(xr))),
% 0.15/10.86 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.15/10.86 fof(f334,plain,(
% 0.15/10.86 ~aNaturalNumber0(xr)|sQ6_spl),
% 0.15/10.86 inference(component_clause,[status(thm)],[f332])).
% 0.15/10.86 fof(f340,plain,(
% 0.15/10.86 $false|sQ6_spl),
% 0.15/10.86 inference(forward_subsumption_resolution,[status(thm)],[f334,f195])).
% 0.15/10.86 fof(f341,plain,(
% 0.15/10.86 sQ6_spl),
% 0.15/10.86 inference(contradiction_clause,[status(thm)],[f340])).
% 0.15/10.86 fof(f383,plain,(
% 0.15/10.86 ~aNaturalNumber0(xp)|~aNaturalNumber0(sdtasdt0(xn,xm))|xp=sz00|aNaturalNumber0(sdtsldt0(sdtasdt0(xn,xm),xp))),
% 0.15/10.86 inference(resolution,[status(thm)],[f227,f182])).
% 0.15/10.86 fof(f385,plain,(
% 0.15/10.86 ~aNaturalNumber0(xr)|~aNaturalNumber0(xk)|xr=sz00|aNaturalNumber0(sdtsldt0(xk,xr))),
% 0.15/10.86 inference(resolution,[status(thm)],[f227,f196])).
% 0.15/10.86 fof(f402,definition,(
% 0.15/10.86 sQ15_spl <=> (aNaturalNumber0(sdtasdt0(xn,xm)))),
% 0.15/10.86 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.15/10.86 fof(f404,plain,(
% 0.15/10.86 ~aNaturalNumber0(sdtasdt0(xn,xm))|sQ15_spl),
% 0.15/10.86 inference(component_clause,[status(thm)],[f402])).
% 0.15/10.86 fof(f405,definition,(
% 0.15/10.86 sQ16_spl <=> (xp=sz00)),
% 0.15/10.86 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.15/10.86 fof(f406,plain,(
% 0.15/10.86 xp=sz00|~sQ16_spl),
% 0.15/10.86 inference(component_clause,[status(thm)],[f405])).
% 0.15/10.86 fof(f408,definition,(
% 0.15/10.86 sQ17_spl <=> (aNaturalNumber0(sdtsldt0(sdtasdt0(xn,xm),xp)))),
% 0.15/10.86 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.15/10.86 fof(f409,plain,(
% 0.15/10.86 aNaturalNumber0(sdtsldt0(sdtasdt0(xn,xm),xp))|~sQ17_spl),
% 0.15/10.86 inference(component_clause,[status(thm)],[f408])).
% 0.15/10.86 fof(f411,plain,(
% 0.15/10.86 ~sQ2_spl|~sQ15_spl|sQ16_spl|sQ17_spl),
% 0.15/10.86 inference(split_clause,[status(thm)],[f383,f307,f402,f405,f408])).
% 0.15/10.86 fof(f412,definition,(
% 0.15/10.86 sQ18_spl <=> (xr=sz00)),
% 0.15/10.86 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.15/10.86 fof(f413,plain,(
% 0.15/10.86 xr=sz00|~sQ18_spl),
% 0.15/10.86 inference(component_clause,[status(thm)],[f412])).
% 0.15/10.86 fof(f419,definition,(
% 0.15/10.86 sQ20_spl <=> (aNaturalNumber0(xk))),
% 0.15/10.86 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.15/10.86 fof(f421,plain,(
% 0.15/10.86 ~aNaturalNumber0(xk)|sQ20_spl),
% 0.15/10.86 inference(component_clause,[status(thm)],[f419])).
% 0.15/10.86 fof(f422,plain,(
% 0.15/10.86 ~sQ6_spl|~sQ20_spl|sQ18_spl|sQ3_spl),
% 0.15/10.86 inference(split_clause,[status(thm)],[f385,f332,f419,f412,f310])).
% 0.15/10.86 fof(f423,definition,(
% 0.15/10.86 sQ21_spl <=> (aNaturalNumber0(xn))),
% 0.15/10.86 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.15/10.86 fof(f425,plain,(
% 0.15/10.86 ~aNaturalNumber0(xn)|sQ21_spl),
% 0.15/10.86 inference(component_clause,[status(thm)],[f423])).
% 0.15/10.86 fof(f437,plain,(
% 0.15/10.86 ~isPrime0(xr)|~sQ18_spl),
% 0.15/10.86 inference(backward_demodulation,[status(thm)],[f413,f232])).
% 0.15/10.86 fof(f510,plain,(
% 0.15/10.86 $false|~sQ18_spl),
% 0.15/10.86 inference(forward_subsumption_resolution,[status(thm)],[f437,f197])).
% 0.15/10.86 fof(f511,plain,(
% 0.15/10.86 ~sQ18_spl),
% 0.15/10.86 inference(contradiction_clause,[status(thm)],[f510])).
% 0.15/10.86 fof(f512,plain,(
% 0.15/10.86 $false|sQ21_spl),
% 0.15/10.86 inference(forward_subsumption_resolution,[status(thm)],[f425,f176])).
% 0.15/10.86 fof(f513,plain,(
% 0.15/10.86 sQ21_spl),
% 0.15/10.86 inference(contradiction_clause,[status(thm)],[f512])).
% 0.15/10.86 fof(f547,plain,(
% 0.15/10.86 ~aNaturalNumber0(xn)|~aNaturalNumber0(xm)|sQ15_spl),
% 0.15/10.86 inference(resolution,[status(thm)],[f404,f67])).
% 0.15/10.86 fof(f548,definition,(
% 0.15/10.86 sQ25_spl <=> (aNaturalNumber0(xm))),
% 0.15/10.86 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.15/10.86 fof(f550,plain,(
% 0.15/10.86 ~aNaturalNumber0(xm)|sQ25_spl),
% 0.15/10.86 inference(component_clause,[status(thm)],[f548])).
% 0.15/10.86 fof(f551,plain,(
% 0.15/10.86 ~sQ21_spl|~sQ25_spl|sQ15_spl),
% 0.15/10.86 inference(split_clause,[status(thm)],[f547,f423,f548,f402])).
% 0.15/10.86 fof(f552,plain,(
% 0.15/10.86 $false|sQ25_spl),
% 0.15/10.86 inference(forward_subsumption_resolution,[status(thm)],[f550,f177])).
% 0.15/10.87 fof(f553,plain,(
% 0.15/10.87 sQ25_spl),
% 0.15/10.87 inference(contradiction_clause,[status(thm)],[f552])).
% 0.15/10.87 fof(f557,plain,(
% 0.15/10.87 ~isPrime0(xp)|~sQ16_spl),
% 0.15/10.87 inference(backward_demodulation,[status(thm)],[f406,f232])).
% 0.15/10.87 fof(f605,plain,(
% 0.15/10.87 $false|~sQ16_spl),
% 0.15/10.87 inference(forward_subsumption_resolution,[status(thm)],[f557,f181])).
% 0.15/10.87 fof(f606,plain,(
% 0.15/10.87 ~sQ16_spl),
% 0.15/10.87 inference(contradiction_clause,[status(thm)],[f605])).
% 0.15/10.87 fof(f607,plain,(
% 0.15/10.87 aNaturalNumber0(xk)|~sQ17_spl),
% 0.15/10.87 inference(forward_demodulation,[status(thm)],[f189,f409])).
% 0.15/10.87 fof(f608,plain,(
% 0.15/10.87 $false|sQ20_spl|~sQ17_spl),
% 0.15/10.87 inference(forward_subsumption_resolution,[status(thm)],[f607,f421])).
% 0.15/10.87 fof(f609,plain,(
% 0.15/10.87 sQ20_spl|~sQ17_spl),
% 0.15/10.87 inference(contradiction_clause,[status(thm)],[f608])).
% 0.15/10.87 fof(f610,plain,(
% 0.15/10.87 $false),
% 0.15/10.87 inference(sat_refutation,[status(thm)],[f313,f315,f341,f411,f422,f511,f513,f551,f553,f606,f609])).
% 0.15/10.87 % SZS output end CNFRefutation for theBenchmark.p
% 0.15/10.87 % Elapsed time: 0.485430 seconds
% 0.15/10.87 % CPU time: 3.553913 seconds
% 0.15/10.87 % Total memory used: 146.904 MB
% 0.15/10.87 % Net memory used: 142.977 MB
%------------------------------------------------------------------------------