%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM523+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:07 PM UTC 2026
% Result : Theorem 16.92s 2.61s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM523+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.10/0.36 % Computer : n004.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 02:37:19 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 % Drodi V4.1.1
% 16.92/2.61 % Refutation found
% 16.92/2.61 % SZS status Theorem for theBenchmark: Theorem is valid
% 16.92/2.61 % SZS output start CNFRefutation for theBenchmark
% 16.92/2.61 fof(f5,axiom,(
% 16.92/2.61 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> aNaturalNumber0(sdtasdt0(W0,W1)) ) )),
% 16.92/2.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.92/2.61 fof(f30,definition,(
% 16.92/2.61 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> ( doDivides0(W0,W1)<=> (? [W2] :( aNaturalNumber0(W2)& W1 = sdtasdt0(W0,W2) ) )) ) )),
% 16.92/2.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.92/2.61 fof(f39,axiom,(
% 16.92/2.61 (! [W0,W1,W2] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1)& aNaturalNumber0(W2) )=> ( ( isPrime0(W2)& doDivides0(W2,sdtasdt0(W0,W1)) )=> ( doDivides0(W2,W0)| doDivides0(W2,W1) ) ) ) )),
% 16.92/2.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.92/2.61 fof(f40,hypothesis,(
% 16.92/2.61 ( aNaturalNumber0(xn)& aNaturalNumber0(xm)& aNaturalNumber0(xp)& xn != sz00& xm != sz00& xp != sz00 ) ),
% 16.92/2.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.92/2.61 fof(f42,hypothesis,(
% 16.92/2.61 sdtasdt0(xp,sdtasdt0(xm,xm)) = sdtasdt0(xn,xn) ),
% 16.92/2.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.92/2.62 fof(f43,hypothesis,(
% 16.92/2.62 ( xp != sz10& (! [W0] :( ( aNaturalNumber0(W0)& ( (? [W1] :( aNaturalNumber0(W1)& xp = sdtasdt0(W0,W1) ))| doDivides0(W0,xp) ) )=> ( W0 = sz10| W0 = xp ) ))& isPrime0(xp) ) ),
% 16.92/2.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.92/2.62 fof(f44,conjecture,(
% 16.92/2.62 ( ( (? [W0] :( aNaturalNumber0(W0)& sdtasdt0(xn,xn) = sdtasdt0(xp,W0) ))| doDivides0(xp,sdtasdt0(xn,xn)) )& ( (? [W0] :( aNaturalNumber0(W0)& xn = sdtasdt0(xp,W0) ))| doDivides0(xp,xn) ) ) ),
% 16.92/2.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.92/2.62 fof(f45,negated_conjecture,(
% 16.92/2.62 ~(( ( (? [W0] :( aNaturalNumber0(W0)& sdtasdt0(xn,xn) = sdtasdt0(xp,W0) ))| doDivides0(xp,sdtasdt0(xn,xn)) )& ( (? [W0] :( aNaturalNumber0(W0)& xn = sdtasdt0(xp,W0) ))| doDivides0(xp,xn) ) ) )),
% 16.92/2.62 inference(negated_conjecture,[status(cth)],[f44])).
% 16.92/2.62 fof(f54,plain,(
% 16.92/2.62 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|aNaturalNumber0(sdtasdt0(W0,W1)))),
% 16.92/2.62 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 16.92/2.62 fof(f55,plain,(
% 16.92/2.62 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|aNaturalNumber0(sdtasdt0(X0,X1)))),
% 16.92/2.62 inference(cnf_transformation,[status(thm)],[f54])).
% 16.92/2.62 fof(f127,plain,(
% 16.92/2.62 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|(doDivides0(W0,W1)<=>(?[W2]: (aNaturalNumber0(W2)&W1=sdtasdt0(W0,W2)))))),
% 16.92/2.62 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 16.92/2.62 fof(f128,plain,(
% 16.92/2.62 ![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))))))),
% 16.92/2.62 inference(NNF_transformation,[status(thm)],[f127])).
% 16.92/2.62 fof(f129,plain,(
% 16.92/2.62 ![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))))))),
% 16.92/2.62 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W2,sK1_skl(W1,W0))],[f128])).
% 16.92/2.62 fof(f132,plain,(
% 16.92/2.62 ![X0,X1,X2]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|doDivides0(X0,X1)|~aNaturalNumber0(X2)|~X1=sdtasdt0(X0,X2))),
% 16.92/2.62 inference(cnf_transformation,[status(thm)],[f129])).
% 16.92/2.62 fof(f164,plain,(
% 16.92/2.62 ![W0,W1,W2]: (((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|~aNaturalNumber0(W2))|((~isPrime0(W2)|~doDivides0(W2,sdtasdt0(W0,W1)))|(doDivides0(W2,W0)|doDivides0(W2,W1))))),
% 16.92/2.62 inference(pre_NNF_transformation,[status(thm)],[f39])).
% 16.92/2.62 fof(f165,plain,(
% 16.92/2.62 ![X0,X1,X2]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~isPrime0(X2)|~doDivides0(X2,sdtasdt0(X0,X1))|doDivides0(X2,X0)|doDivides0(X2,X1))),
% 16.92/2.62 inference(cnf_transformation,[status(thm)],[f164])).
% 16.92/2.62 fof(f166,plain,(
% 16.92/2.62 aNaturalNumber0(xn)),
% 16.92/2.62 inference(cnf_transformation,[status(thm)],[f40])).
% 16.92/2.62 fof(f167,plain,(
% 16.92/2.62 aNaturalNumber0(xm)),
% 16.92/2.62 inference(cnf_transformation,[status(thm)],[f40])).
% 16.92/2.62 fof(f168,plain,(
% 16.92/2.62 aNaturalNumber0(xp)),
% 16.92/2.62 inference(cnf_transformation,[status(thm)],[f40])).
% 16.92/2.62 fof(f181,plain,(
% 16.92/2.62 sdtasdt0(xp,sdtasdt0(xm,xm))=sdtasdt0(xn,xn)),
% 16.92/2.62 inference(cnf_transformation,[status(thm)],[f42])).
% 16.92/2.62 fof(f182,plain,(
% 16.92/2.62 (~xp=sz10&(![W0]: ((~aNaturalNumber0(W0)|((![W1]: (~aNaturalNumber0(W1)|~xp=sdtasdt0(W0,W1)))&~doDivides0(W0,xp)))|(W0=sz10|W0=xp))))&isPrime0(xp)),
% 16.92/2.62 inference(pre_NNF_transformation,[status(thm)],[f43])).
% 16.92/2.62 fof(f186,plain,(
% 16.92/2.62 isPrime0(xp)),
% 16.92/2.62 inference(cnf_transformation,[status(thm)],[f182])).
% 16.92/2.62 fof(f187,plain,(
% 16.92/2.62 (((![W0]: (~aNaturalNumber0(W0)|~sdtasdt0(xn,xn)=sdtasdt0(xp,W0)))&~doDivides0(xp,sdtasdt0(xn,xn)))|((![W0]: (~aNaturalNumber0(W0)|~xn=sdtasdt0(xp,W0)))&~doDivides0(xp,xn)))),
% 16.92/2.62 inference(pre_NNF_transformation,[status(thm)],[f45])).
% 16.92/2.62 fof(f188,definition,(
% 16.92/2.62 sP0_prd<=>((![W0]: (~aNaturalNumber0(W0)|~sdtasdt0(xn,xn)=sdtasdt0(xp,W0)))&~doDivides0(xp,sdtasdt0(xn,xn)))),
% 16.92/2.62 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 16.92/2.62 fof(f189,plain,(
% 16.92/2.62 sP0_prd|((![W0]: (~aNaturalNumber0(W0)|~xn=sdtasdt0(xp,W0)))&~doDivides0(xp,xn))),
% 16.92/2.62 inference(formula_renaming,[status(thm)],[f187,f188])).
% 16.92/2.62 fof(f191,plain,(
% 16.92/2.62 sP0_prd|~doDivides0(xp,xn)),
% 16.92/2.62 inference(cnf_transformation,[status(thm)],[f189])).
% 16.92/2.62 fof(f192,plain,(
% 16.92/2.62 (~sP0_prd|((![W0]: (~aNaturalNumber0(W0)|~sdtasdt0(xn,xn)=sdtasdt0(xp,W0)))&~doDivides0(xp,sdtasdt0(xn,xn))))&(sP0_prd|((?[W0]: (aNaturalNumber0(W0)&sdtasdt0(xn,xn)=sdtasdt0(xp,W0)))|doDivides0(xp,sdtasdt0(xn,xn))))),
% 16.92/2.62 inference(NNF_transformation,[status(thm)],[f188])).
% 16.92/2.62 fof(f193,plain,(
% 16.92/2.62 (~sP0_prd|((![W0]: (~aNaturalNumber0(W0)|~sdtasdt0(xn,xn)=sdtasdt0(xp,W0)))&~doDivides0(xp,sdtasdt0(xn,xn))))&(sP0_prd|((aNaturalNumber0(sK6_skl)&sdtasdt0(xn,xn)=sdtasdt0(xp,sK6_skl))|doDivides0(xp,sdtasdt0(xn,xn))))),
% 16.92/2.62 inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(W0,sK6_skl)],[f192])).
% 16.92/2.62 fof(f194,plain,(
% 16.92/2.62 ![X0]: (~sP0_prd|~aNaturalNumber0(X0)|~sdtasdt0(xn,xn)=sdtasdt0(xp,X0))),
% 16.92/2.62 inference(cnf_transformation,[status(thm)],[f193])).
% 16.92/2.62 fof(f196,plain,(
% 16.92/2.62 sP0_prd|aNaturalNumber0(sK6_skl)|doDivides0(xp,sdtasdt0(xn,xn))),
% 16.92/2.62 inference(cnf_transformation,[status(thm)],[f193])).
% 16.92/2.62 fof(f197,plain,(
% 16.92/2.62 sP0_prd|sdtasdt0(xn,xn)=sdtasdt0(xp,sK6_skl)|doDivides0(xp,sdtasdt0(xn,xn))),
% 16.92/2.62 inference(cnf_transformation,[status(thm)],[f193])).
% 16.92/2.62 fof(f198,definition,(
% 16.92/2.62 sQ0_spl <=> (sP0_prd)),
% 16.92/2.62 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 16.92/2.62 fof(f205,definition,(
% 16.92/2.62 sQ2_spl <=> (doDivides0(xp,xn))),
% 16.92/2.62 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 16.92/2.62 fof(f208,plain,(
% 16.92/2.62 sQ0_spl|~sQ2_spl),
% 16.92/2.62 inference(split_clause,[status(thm)],[f191,f198,f205])).
% 16.92/2.62 fof(f209,definition,(
% 16.92/2.62 ![X0]: (sQ3_spl <=> (~aNaturalNumber0(X0)|~sdtasdt0(xn,xn)=sdtasdt0(xp,X0)))),
% 16.92/2.62 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 16.92/2.62 fof(f210,plain,(
% 16.92/2.62 ![X0]: (~aNaturalNumber0(X0)|~sdtasdt0(xn,xn)=sdtasdt0(xp,X0)|~sQ3_spl)),
% 16.92/2.62 inference(component_clause,[status(thm)],[f209])).
% 16.92/2.62 fof(f212,plain,(
% 16.92/2.62 ~sQ0_spl|sQ3_spl),
% 16.92/2.62 inference(split_clause,[status(thm)],[f194,f198,f209])).
% 16.92/2.62 fof(f213,definition,(
% 16.92/2.62 sQ4_spl <=> (doDivides0(xp,sdtasdt0(xn,xn)))),
% 16.92/2.62 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 16.92/2.62 fof(f214,plain,(
% 16.92/2.62 doDivides0(xp,sdtasdt0(xn,xn))|~sQ4_spl),
% 16.92/2.62 inference(component_clause,[status(thm)],[f213])).
% 16.92/2.62 fof(f215,plain,(
% 16.92/2.62 ~doDivides0(xp,sdtasdt0(xn,xn))|sQ4_spl),
% 16.92/2.62 inference(component_clause,[status(thm)],[f213])).
% 16.92/2.62 fof(f217,definition,(
% 16.92/2.62 sQ5_spl <=> (aNaturalNumber0(sK6_skl))),
% 16.92/2.62 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 16.92/2.62 fof(f218,plain,(
% 16.92/2.62 aNaturalNumber0(sK6_skl)|~sQ5_spl),
% 16.92/2.62 inference(component_clause,[status(thm)],[f217])).
% 16.92/2.62 fof(f220,plain,(
% 16.92/2.62 sQ0_spl|sQ5_spl|sQ4_spl),
% 16.92/2.62 inference(split_clause,[status(thm)],[f196,f198,f217,f213])).
% 16.92/2.62 fof(f221,definition,(
% 16.92/2.62 sQ6_spl <=> (sdtasdt0(xn,xn)=sdtasdt0(xp,sK6_skl))),
% 16.92/2.62 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 16.92/2.62 fof(f222,plain,(
% 16.92/2.62 sdtasdt0(xn,xn)=sdtasdt0(xp,sK6_skl)|~sQ6_spl),
% 16.92/2.62 inference(component_clause,[status(thm)],[f221])).
% 16.92/2.62 fof(f224,plain,(
% 16.92/2.62 sQ0_spl|sQ6_spl|sQ4_spl),
% 16.92/2.62 inference(split_clause,[status(thm)],[f197,f198,f221,f213])).
% 16.92/2.62 fof(f231,plain,(
% 16.92/2.62 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(sdtasdt0(X0,X1))|doDivides0(X0,sdtasdt0(X0,X1))|~aNaturalNumber0(X1))),
% 16.92/2.62 inference(destructive_equality_resolution,[status(thm)],[f132])).
% 16.92/2.62 fof(f242,plain,(
% 16.92/2.62 ![X0,X1]: (~aNaturalNumber0(X0)|doDivides0(X0,sdtasdt0(X0,X1))|~aNaturalNumber0(X1))),
% 16.92/2.62 inference(forward_subsumption_resolution,[status(thm)],[f231,f55])).
% 16.92/2.62 fof(f359,plain,(
% 16.92/2.62 ![X0]: (doDivides0(xp,sdtasdt0(xp,X0))|~aNaturalNumber0(X0))),
% 16.92/2.62 inference(resolution,[status(thm)],[f168,f242])).
% 16.92/2.62 fof(f387,definition,(
% 16.92/2.62 sQ11_spl <=> (aNaturalNumber0(xn))),
% 16.92/2.62 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 16.92/2.62 fof(f389,plain,(
% 16.92/2.62 ~aNaturalNumber0(xn)|sQ11_spl),
% 16.92/2.62 inference(component_clause,[status(thm)],[f387])).
% 16.92/2.62 fof(f422,definition,(
% 16.92/2.62 sQ17_spl <=> (aNaturalNumber0(xp))),
% 16.92/2.62 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 16.92/2.62 fof(f424,plain,(
% 16.92/2.62 ~aNaturalNumber0(xp)|sQ17_spl),
% 16.92/2.62 inference(component_clause,[status(thm)],[f422])).
% 16.92/2.62 fof(f583,definition,(
% 16.92/2.62 sQ43_spl <=> (sdtasdt0(xn,xn)=sdtasdt0(xn,xn))),
% 16.92/2.62 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 16.92/2.62 fof(f585,plain,(
% 16.92/2.62 ~sdtasdt0(xn,xn)=sdtasdt0(xn,xn)|sQ43_spl),
% 16.92/2.62 inference(component_clause,[status(thm)],[f583])).
% 16.92/2.62 fof(f1937,definition,(
% 16.92/2.62 sQ217_spl <=> (isPrime0(xp))),
% 16.92/2.62 introduced(definition,[new_symbols(definition,[sQ217_spl])],[split_symbol_definition])).
% 16.92/2.62 fof(f1939,plain,(
% 16.92/2.62 ~isPrime0(xp)|sQ217_spl),
% 16.92/2.62 inference(component_clause,[status(thm)],[f1937])).
% 16.92/2.62 fof(f2499,plain,(
% 16.92/2.62 ![X0]: (~aNaturalNumber0(X0)|aNaturalNumber0(sdtasdt0(xm,X0)))),
% 16.92/2.62 inference(resolution,[status(thm)],[f167,f55])).
% 16.92/2.62 fof(f2943,definition,(
% 16.92/2.62 sQ334_spl <=> (aNaturalNumber0(sdtasdt0(xm,xm)))),
% 16.92/2.62 introduced(definition,[new_symbols(definition,[sQ334_spl])],[split_symbol_definition])).
% 16.92/2.62 fof(f2945,plain,(
% 16.92/2.62 ~aNaturalNumber0(sdtasdt0(xm,xm))|sQ334_spl),
% 16.92/2.62 inference(component_clause,[status(thm)],[f2943])).
% 16.92/2.62 fof(f3532,plain,(
% 16.92/2.62 $false|sQ217_spl),
% 16.92/2.62 inference(forward_subsumption_resolution,[status(thm)],[f1939,f186])).
% 16.92/2.62 fof(f3533,plain,(
% 16.92/2.62 sQ217_spl),
% 16.92/2.62 inference(contradiction_clause,[status(thm)],[f3532])).
% 16.92/2.62 fof(f6064,plain,(
% 16.92/2.62 $false|sQ11_spl),
% 16.92/2.62 inference(forward_subsumption_resolution,[status(thm)],[f389,f166])).
% 16.92/2.62 fof(f6065,plain,(
% 16.92/2.62 sQ11_spl),
% 16.92/2.62 inference(contradiction_clause,[status(thm)],[f6064])).
% 16.92/2.62 fof(f6101,plain,(
% 16.92/2.62 ~aNaturalNumber0(xn)|~aNaturalNumber0(xn)|~aNaturalNumber0(xp)|~isPrime0(xp)|doDivides0(xp,xn)|doDivides0(xp,xn)|~sQ4_spl),
% 16.92/2.62 inference(resolution,[status(thm)],[f214,f165])).
% 16.92/2.62 fof(f6111,plain,(
% 16.92/2.62 ~sQ11_spl|~sQ17_spl|~sQ217_spl|sQ2_spl|~sQ4_spl),
% 16.92/2.62 inference(split_clause,[status(thm)],[f6101,f387,f422,f1937,f205,f213])).
% 16.92/2.62 fof(f6900,plain,(
% 16.92/2.62 $false|sQ17_spl),
% 16.92/2.62 inference(forward_subsumption_resolution,[status(thm)],[f424,f168])).
% 16.92/2.62 fof(f6901,plain,(
% 16.92/2.62 sQ17_spl),
% 16.92/2.62 inference(contradiction_clause,[status(thm)],[f6900])).
% 16.92/2.62 fof(f7045,plain,(
% 16.92/2.62 doDivides0(xp,sdtasdt0(xp,sK6_skl))|~sQ5_spl),
% 16.92/2.62 inference(resolution,[status(thm)],[f218,f359])).
% 16.92/2.62 fof(f7555,plain,(
% 16.92/2.62 doDivides0(xp,sdtasdt0(xn,xn))|~sQ6_spl|~sQ5_spl),
% 16.92/2.62 inference(forward_demodulation,[status(thm)],[f222,f7045])).
% 16.92/2.62 fof(f7556,plain,(
% 16.92/2.62 $false|sQ4_spl|~sQ6_spl|~sQ5_spl),
% 16.92/2.62 inference(forward_subsumption_resolution,[status(thm)],[f7555,f215])).
% 16.92/2.62 fof(f7557,plain,(
% 16.92/2.62 sQ4_spl|~sQ6_spl|~sQ5_spl),
% 16.92/2.62 inference(contradiction_clause,[status(thm)],[f7556])).
% 16.92/2.62 fof(f8336,plain,(
% 16.92/2.62 ~aNaturalNumber0(sdtasdt0(xm,xm))|~sQ3_spl),
% 16.92/2.62 inference(resolution,[status(thm)],[f181,f210])).
% 16.92/2.62 fof(f10638,plain,(
% 16.92/2.62 aNaturalNumber0(sdtasdt0(xm,xm))),
% 16.92/2.62 inference(resolution,[status(thm)],[f2499,f167])).
% 16.92/2.62 fof(f10640,plain,(
% 16.92/2.62 $false|sQ334_spl),
% 16.92/2.62 inference(forward_subsumption_resolution,[status(thm)],[f10638,f2945])).
% 16.92/2.62 fof(f10641,plain,(
% 16.92/2.62 sQ334_spl),
% 16.92/2.62 inference(contradiction_clause,[status(thm)],[f10640])).
% 16.92/2.62 fof(f10642,plain,(
% 16.92/2.62 ~sQ334_spl|~sQ3_spl),
% 16.92/2.62 inference(split_clause,[status(thm)],[f8336,f2943,f209])).
% 16.92/2.62 fof(f10645,plain,(
% 16.92/2.62 $false|sQ43_spl),
% 16.92/2.62 inference(trivial_equality_resolution,[status(thm)],[f585])).
% 16.92/2.63 fof(f10646,plain,(
% 16.92/2.63 sQ43_spl),
% 16.92/2.63 inference(contradiction_clause,[status(thm)],[f10645])).
% 16.92/2.63 fof(f10647,plain,(
% 16.92/2.63 $false),
% 16.92/2.63 inference(sat_refutation,[status(thm)],[f208,f212,f220,f224,f3533,f6065,f6111,f6901,f7557,f10641,f10642,f10646])).
% 16.92/2.63 % SZS output end CNFRefutation for theBenchmark.p
% 16.92/2.65 % Elapsed time: 2.272817 seconds
% 16.92/2.65 % CPU time: 17.711186 seconds
% 16.92/2.65 % Total memory used: 238.785 MB
% 16.92/2.65 % Net memory used: 226.379 MB
%------------------------------------------------------------------------------