%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM475+2 : 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 : n011.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:42:59 PM UTC 2026
% Result : Theorem 8.21s 16.74s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM475+2 : 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.08/0.34 % Computer : n011.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.10/15.64 % CPULimit : 300
% 0.10/15.64 % WCLimit : 300
% 0.10/15.64 % DateTime : Mon Sep 21 02:33:07 UTC 2026
% 0.10/15.64 % CPUTime :
% 0.10/15.66 % Drodi V4.1.1
% 8.21/16.74 % Refutation found
% 8.21/16.74 % SZS status Theorem for theBenchmark: Theorem is valid
% 8.21/16.74 % SZS output start CNFRefutation for theBenchmark
% 8.21/16.74 fof(f3,axiom,(
% 8.21/16.74 ( aNaturalNumber0(sz10)& sz10 != sz00 ) ),
% 8.21/16.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.21/16.74 fof(f5,axiom,(
% 8.21/16.74 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> aNaturalNumber0(sdtasdt0(W0,W1)) ) )),
% 8.21/16.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.21/16.74 fof(f9,axiom,(
% 8.21/16.74 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) )),
% 8.21/16.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.21/16.74 fof(f11,axiom,(
% 8.21/16.74 (! [W0] :( aNaturalNumber0(W0)=> ( sdtasdt0(W0,sz10) = W0& W0 = sdtasdt0(sz10,W0) ) ) )),
% 8.21/16.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.21/16.74 fof(f14,axiom,(
% 8.21/16.74 (! [W0,W1,W2] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1)& aNaturalNumber0(W2) )=> ( ( sdtpldt0(W0,W1) = sdtpldt0(W0,W2)| sdtpldt0(W1,W0) = sdtpldt0(W2,W0) )=> W1 = W2 ) ) )),
% 8.21/16.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.21/16.74 fof(f34,hypothesis,(
% 8.21/16.74 ( aNaturalNumber0(xl)& aNaturalNumber0(xm)& aNaturalNumber0(xn) ) ),
% 8.21/16.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.21/16.74 fof(f35,hypothesis,(
% 8.21/16.74 ( (? [W0] :( aNaturalNumber0(W0)& xm = sdtasdt0(xl,W0) ))& doDivides0(xl,xm)& (? [W0] :( aNaturalNumber0(W0)& sdtpldt0(xm,xn) = sdtasdt0(xl,W0) ))& doDivides0(xl,sdtpldt0(xm,xn)) ) ),
% 8.21/16.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.21/16.74 fof(f37,hypothesis,(
% 8.21/16.74 ( aNaturalNumber0(xp)& xm = sdtasdt0(xl,xp)& xp = sdtsldt0(xm,xl) ) ),
% 8.21/16.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.21/16.74 fof(f40,hypothesis,(
% 8.21/16.74 ( aNaturalNumber0(xr)& sdtpldt0(xp,xr) = xq& xr = sdtmndt0(xq,xp) ) ),
% 8.21/16.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.21/16.74 fof(f41,hypothesis,(
% 8.21/16.74 sdtpldt0(sdtasdt0(xl,xp),sdtasdt0(xl,xr)) = sdtpldt0(sdtasdt0(xl,xp),xn) ),
% 8.21/16.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.21/16.74 fof(f42,conjecture,(
% 8.21/16.74 xn = sdtasdt0(xl,xr) ),
% 8.21/16.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.21/16.74 fof(f43,negated_conjecture,(
% 8.21/16.74 ~(xn = sdtasdt0(xl,xr) )),
% 8.21/16.74 inference(negated_conjecture,[status(cth)],[f42])).
% 8.21/16.74 fof(f48,plain,(
% 8.21/16.74 aNaturalNumber0(sz10)),
% 8.21/16.74 inference(cnf_transformation,[status(thm)],[f3])).
% 8.21/16.74 fof(f52,plain,(
% 8.21/16.74 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|aNaturalNumber0(sdtasdt0(W0,W1)))),
% 8.21/16.74 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 8.21/16.74 fof(f53,plain,(
% 8.21/16.74 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|aNaturalNumber0(sdtasdt0(X0,X1)))),
% 8.21/16.74 inference(cnf_transformation,[status(thm)],[f52])).
% 8.21/16.74 fof(f61,plain,(
% 8.21/16.74 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|sdtasdt0(W0,W1)=sdtasdt0(W1,W0))),
% 8.21/16.74 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 8.21/16.74 fof(f62,plain,(
% 8.21/16.74 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|sdtasdt0(X0,X1)=sdtasdt0(X1,X0))),
% 8.21/16.74 inference(cnf_transformation,[status(thm)],[f61])).
% 8.21/16.74 fof(f65,plain,(
% 8.21/16.74 ![W0]: (~aNaturalNumber0(W0)|(sdtasdt0(W0,sz10)=W0&W0=sdtasdt0(sz10,W0)))),
% 8.21/16.74 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 8.21/16.74 fof(f67,plain,(
% 8.21/16.74 ![X0]: (~aNaturalNumber0(X0)|X0=sdtasdt0(sz10,X0))),
% 8.21/16.74 inference(cnf_transformation,[status(thm)],[f65])).
% 8.21/16.74 fof(f74,plain,(
% 8.21/16.74 ![W0,W1,W2]: (((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|~aNaturalNumber0(W2))|((~sdtpldt0(W0,W1)=sdtpldt0(W0,W2)&~sdtpldt0(W1,W0)=sdtpldt0(W2,W0))|W1=W2))),
% 8.21/16.74 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 8.21/16.74 fof(f75,plain,(
% 8.21/16.74 ![X0,X1,X2]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~sdtpldt0(X0,X1)=sdtpldt0(X0,X2)|X1=X2)),
% 8.21/16.74 inference(cnf_transformation,[status(thm)],[f74])).
% 8.21/16.74 fof(f141,plain,(
% 8.21/16.74 aNaturalNumber0(xl)),
% 8.21/16.74 inference(cnf_transformation,[status(thm)],[f34])).
% 8.21/16.74 fof(f143,plain,(
% 8.21/16.74 aNaturalNumber0(xn)),
% 8.21/16.74 inference(cnf_transformation,[status(thm)],[f34])).
% 8.21/16.74 fof(f144,plain,(
% 8.21/16.74 (((aNaturalNumber0(sK2_skl)&xm=sdtasdt0(xl,sK2_skl))&doDivides0(xl,xm))&(aNaturalNumber0(sK3_skl)&sdtpldt0(xm,xn)=sdtasdt0(xl,sK3_skl)))&doDivides0(xl,sdtpldt0(xm,xn))),
% 8.21/16.74 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl]),skolemize(W0,sK2_skl),skolemize(W0,sK3_skl)],[f35])).
% 8.21/16.74 fof(f145,plain,(
% 8.21/16.74 aNaturalNumber0(sK2_skl)),
% 8.21/16.74 inference(cnf_transformation,[status(thm)],[f144])).
% 8.21/16.74 fof(f146,plain,(
% 8.21/16.74 xm=sdtasdt0(xl,sK2_skl)),
% 8.21/16.74 inference(cnf_transformation,[status(thm)],[f144])).
% 8.21/16.74 fof(f153,plain,(
% 8.21/16.74 xm=sdtasdt0(xl,xp)),
% 8.21/16.74 inference(cnf_transformation,[status(thm)],[f37])).
% 8.21/16.74 fof(f162,plain,(
% 8.21/16.74 aNaturalNumber0(xr)),
% 8.21/16.74 inference(cnf_transformation,[status(thm)],[f40])).
% 8.21/16.74 fof(f165,plain,(
% 8.21/16.74 sdtpldt0(sdtasdt0(xl,xp),sdtasdt0(xl,xr))=sdtpldt0(sdtasdt0(xl,xp),xn)),
% 8.21/16.74 inference(cnf_transformation,[status(thm)],[f41])).
% 8.21/16.74 fof(f166,plain,(
% 8.21/16.74 ~xn=sdtasdt0(xl,xr)),
% 8.21/16.74 inference(cnf_transformation,[status(thm)],[f43])).
% 8.21/16.74 fof(f178,definition,(
% 8.21/16.74 sQ0_spl <=> (aNaturalNumber0(xl))),
% 8.21/16.74 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 8.21/16.74 fof(f180,plain,(
% 8.21/16.74 ~aNaturalNumber0(xl)|sQ0_spl),
% 8.21/16.74 inference(component_clause,[status(thm)],[f178])).
% 8.21/16.74 fof(f189,plain,(
% 8.21/16.74 ![X0]: (~aNaturalNumber0(X0)|sdtasdt0(X0,xr)=sdtasdt0(xr,X0))),
% 8.21/16.74 inference(resolution,[status(thm)],[f62,f162])).
% 8.21/16.74 fof(f265,plain,(
% 8.21/16.74 $false|sQ0_spl),
% 8.21/16.74 inference(forward_subsumption_resolution,[status(thm)],[f180,f141])).
% 8.21/16.74 fof(f266,plain,(
% 8.21/16.74 sQ0_spl),
% 8.21/16.74 inference(contradiction_clause,[status(thm)],[f265])).
% 8.21/16.74 fof(f342,plain,(
% 8.21/16.74 sdtasdt0(xl,xr)=sdtasdt0(xr,xl)),
% 8.21/16.74 inference(resolution,[status(thm)],[f189,f141])).
% 8.21/16.74 fof(f489,definition,(
% 8.21/16.74 sQ15_spl <=> (aNaturalNumber0(xm))),
% 8.21/16.74 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 8.21/16.74 fof(f495,plain,(
% 8.21/16.74 sdtpldt0(sdtasdt0(xl,xp),sdtasdt0(xl,xr))=sdtpldt0(xm,xn)),
% 8.21/16.74 inference(backward_demodulation,[status(thm)],[f153,f165])).
% 8.21/16.74 fof(f497,plain,(
% 8.21/16.74 sdtpldt0(xm,sdtasdt0(xl,xr))=sdtpldt0(xm,xn)),
% 8.21/16.74 inference(forward_demodulation,[status(thm)],[f153,f495])).
% 8.21/16.74 fof(f577,definition,(
% 8.21/16.74 sQ17_spl <=> (aNaturalNumber0(xn))),
% 8.21/16.74 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 8.21/16.74 fof(f592,definition,(
% 8.21/16.74 sQ18_spl <=> (aNaturalNumber0(sz10))),
% 8.21/16.74 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 8.21/16.74 fof(f594,plain,(
% 8.21/16.74 ~aNaturalNumber0(sz10)|sQ18_spl),
% 8.21/16.74 inference(component_clause,[status(thm)],[f592])).
% 8.21/16.74 fof(f675,plain,(
% 8.21/16.74 xn=sdtasdt0(sz10,xn)),
% 8.21/16.74 inference(resolution,[status(thm)],[f67,f143])).
% 8.21/16.74 fof(f1251,plain,(
% 8.21/16.74 ![X0]: (~aNaturalNumber0(X0)|aNaturalNumber0(sdtasdt0(X0,xr)))),
% 8.21/16.74 inference(resolution,[status(thm)],[f53,f162])).
% 8.21/16.74 fof(f1253,plain,(
% 8.21/16.74 ![X0]: (~aNaturalNumber0(X0)|aNaturalNumber0(sdtasdt0(X0,xn)))),
% 8.21/16.74 inference(resolution,[status(thm)],[f53,f143])).
% 8.21/16.74 fof(f1349,plain,(
% 8.21/16.74 ![X0]: (~aNaturalNumber0(X0)|aNaturalNumber0(sdtasdt0(X0,sK2_skl)))),
% 8.21/16.74 inference(resolution,[status(thm)],[f53,f145])).
% 8.21/16.74 fof(f1517,plain,(
% 8.21/16.74 ~aNaturalNumber0(sz10)|aNaturalNumber0(xn)),
% 8.21/16.74 inference(paramodulation,[status(thm)],[f675,f1253])).
% 8.21/16.74 fof(f1519,plain,(
% 8.21/16.74 ~sQ18_spl|sQ17_spl),
% 8.21/16.74 inference(split_clause,[status(thm)],[f1517,f592,f577])).
% 8.21/16.74 fof(f1520,plain,(
% 8.21/16.74 $false|sQ18_spl),
% 8.21/16.74 inference(forward_subsumption_resolution,[status(thm)],[f594,f48])).
% 8.21/16.74 fof(f1521,plain,(
% 8.21/16.74 sQ18_spl),
% 8.21/16.74 inference(contradiction_clause,[status(thm)],[f1520])).
% 8.21/16.74 fof(f1643,plain,(
% 8.21/16.74 ~aNaturalNumber0(xl)|aNaturalNumber0(xm)),
% 8.21/16.74 inference(paramodulation,[status(thm)],[f146,f1349])).
% 8.21/16.74 fof(f1644,plain,(
% 8.21/16.74 ~sQ0_spl|sQ15_spl),
% 8.21/16.74 inference(split_clause,[status(thm)],[f1643,f178,f489])).
% 8.21/16.74 fof(f2081,plain,(
% 8.21/16.74 sdtpldt0(xm,sdtasdt0(xr,xl))=sdtpldt0(xm,xn)),
% 8.21/16.74 inference(backward_demodulation,[status(thm)],[f342,f497])).
% 8.21/16.74 fof(f2082,plain,(
% 8.21/16.74 ~xn=sdtasdt0(xr,xl)),
% 8.21/16.74 inference(backward_demodulation,[status(thm)],[f342,f166])).
% 8.21/16.74 fof(f2083,plain,(
% 8.21/16.74 ~aNaturalNumber0(xl)|aNaturalNumber0(sdtasdt0(xr,xl))),
% 8.21/16.74 inference(paramodulation,[status(thm)],[f342,f1251])).
% 8.21/16.74 fof(f2084,definition,(
% 8.21/16.74 sQ77_spl <=> (aNaturalNumber0(sdtasdt0(xr,xl)))),
% 8.21/16.74 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 8.21/16.74 fof(f2087,plain,(
% 8.21/16.74 ~sQ0_spl|sQ77_spl),
% 8.21/16.74 inference(split_clause,[status(thm)],[f2083,f178,f2084])).
% 8.21/16.74 fof(f3848,plain,(
% 8.21/16.74 ~aNaturalNumber0(xm)|~aNaturalNumber0(sdtasdt0(xr,xl))|~aNaturalNumber0(xn)|sdtasdt0(xr,xl)=xn),
% 8.21/16.74 inference(resolution,[status(thm)],[f75,f2081])).
% 8.21/16.76 fof(f3853,definition,(
% 8.21/16.76 sQ160_spl <=> (sdtasdt0(xr,xl)=xn)),
% 8.21/16.76 introduced(definition,[new_symbols(definition,[sQ160_spl])],[split_symbol_definition])).
% 8.21/16.76 fof(f3854,plain,(
% 8.21/16.76 sdtasdt0(xr,xl)=xn|~sQ160_spl),
% 8.21/16.76 inference(component_clause,[status(thm)],[f3853])).
% 8.21/16.76 fof(f3856,plain,(
% 8.21/16.76 ~sQ15_spl|~sQ77_spl|~sQ17_spl|sQ160_spl),
% 8.21/16.76 inference(split_clause,[status(thm)],[f3848,f489,f2084,f577,f3853])).
% 8.21/16.76 fof(f3870,plain,(
% 8.21/16.76 $false|~sQ160_spl),
% 8.21/16.76 inference(forward_subsumption_resolution,[status(thm)],[f3854,f2082])).
% 8.21/16.76 fof(f3871,plain,(
% 8.21/16.76 ~sQ160_spl),
% 8.21/16.76 inference(contradiction_clause,[status(thm)],[f3870])).
% 8.21/16.76 fof(f3872,plain,(
% 8.21/16.76 $false),
% 8.21/16.76 inference(sat_refutation,[status(thm)],[f266,f1519,f1521,f1644,f2087,f3856,f3871])).
% 8.21/16.76 % SZS output end CNFRefutation for theBenchmark.p
% 8.21/16.77 % Elapsed time: 1.111534 seconds
% 8.21/16.77 % CPU time: 8.180703 seconds
% 8.21/16.77 % Total memory used: 166.214 MB
% 8.21/16.77 % Net memory used: 161.711 MB
%------------------------------------------------------------------------------