%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM489+1 : 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 : 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:01 PM UTC 2026
% Result : Theorem 0.13s 0.66s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM489+1 : 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.08/0.57 % Computer : n016.cluster.edu
% 0.08/0.57 % Model : x86_64 x86_64
% 0.08/0.57 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.57 % Memory : 8046.5625MB
% 0.08/0.57 % OS : Linux 6.8.0-71-generic
% 0.08/0.57 % CPULimit : 300
% 0.08/0.57 % WCLimit : 300
% 0.08/0.57 % DateTime : Mon Sep 21 02:39:23 UTC 2026
% 0.08/0.57 % CPUTime :
% 0.08/0.58 % Drodi V4.1.1
% 0.13/0.66 % Refutation found
% 0.13/0.66 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.66 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.66 fof(f19,definition,(
% 0.13/0.66 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> ( sdtlseqdt0(W0,W1)=> (! [W2] :( W2 = sdtmndt0(W1,W0)<=> ( aNaturalNumber0(W2)& sdtpldt0(W0,W2) = W1 ) ) )) ) )),
% 0.13/0.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.66 fof(f39,hypothesis,(
% 0.13/0.66 ( aNaturalNumber0(xn)& aNaturalNumber0(xm)& aNaturalNumber0(xp) ) ),
% 0.13/0.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.66 fof(f42,hypothesis,(
% 0.13/0.66 sdtlseqdt0(xp,xn) ),
% 0.13/0.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.66 fof(f43,hypothesis,(
% 0.13/0.66 xr = sdtmndt0(xn,xp) ),
% 0.13/0.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.66 fof(f45,conjecture,(
% 0.13/0.66 xn = sdtpldt0(xp,xr) ),
% 0.13/0.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.66 fof(f46,negated_conjecture,(
% 0.13/0.66 ~(xn = sdtpldt0(xp,xr) )),
% 0.13/0.66 inference(negated_conjecture,[status(cth)],[f45])).
% 0.13/0.66 fof(f94,plain,(
% 0.13/0.66 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|(~sdtlseqdt0(W0,W1)|(![W2]: (W2=sdtmndt0(W1,W0)<=>(aNaturalNumber0(W2)&sdtpldt0(W0,W2)=W1)))))),
% 0.13/0.66 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 0.13/0.66 fof(f95,plain,(
% 0.13/0.66 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|(~sdtlseqdt0(W0,W1)|(![W2]: ((~W2=sdtmndt0(W1,W0)|(aNaturalNumber0(W2)&sdtpldt0(W0,W2)=W1))&(W2=sdtmndt0(W1,W0)|(~aNaturalNumber0(W2)|~sdtpldt0(W0,W2)=W1))))))),
% 0.13/0.66 inference(NNF_transformation,[status(thm)],[f94])).
% 0.13/0.66 fof(f96,plain,(
% 0.13/0.66 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|(~sdtlseqdt0(W0,W1)|((![W2]: (~W2=sdtmndt0(W1,W0)|(aNaturalNumber0(W2)&sdtpldt0(W0,W2)=W1)))&(![W2]: (W2=sdtmndt0(W1,W0)|(~aNaturalNumber0(W2)|~sdtpldt0(W0,W2)=W1))))))),
% 0.13/0.66 inference(miniscoping,[status(thm)],[f95])).
% 0.13/0.66 fof(f98,plain,(
% 0.13/0.66 ![X0,X1,X2]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|~sdtlseqdt0(X0,X1)|~X2=sdtmndt0(X1,X0)|sdtpldt0(X0,X2)=X1)),
% 0.13/0.66 inference(cnf_transformation,[status(thm)],[f96])).
% 0.13/0.66 fof(f165,plain,(
% 0.13/0.66 aNaturalNumber0(xn)),
% 0.13/0.66 inference(cnf_transformation,[status(thm)],[f39])).
% 0.13/0.66 fof(f167,plain,(
% 0.13/0.66 aNaturalNumber0(xp)),
% 0.13/0.66 inference(cnf_transformation,[status(thm)],[f39])).
% 0.13/0.66 fof(f172,plain,(
% 0.13/0.66 sdtlseqdt0(xp,xn)),
% 0.13/0.66 inference(cnf_transformation,[status(thm)],[f42])).
% 0.13/0.66 fof(f173,plain,(
% 0.13/0.66 xr=sdtmndt0(xn,xp)),
% 0.13/0.66 inference(cnf_transformation,[status(thm)],[f43])).
% 0.13/0.66 fof(f176,plain,(
% 0.13/0.66 ~xn=sdtpldt0(xp,xr)),
% 0.13/0.66 inference(cnf_transformation,[status(thm)],[f46])).
% 0.13/0.66 fof(f179,plain,(
% 0.13/0.66 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|~sdtlseqdt0(X0,X1)|sdtpldt0(X0,sdtmndt0(X1,X0))=X1)),
% 0.13/0.66 inference(destructive_equality_resolution,[status(thm)],[f98])).
% 0.13/0.66 fof(f612,definition,(
% 0.13/0.66 sQ1_spl <=> (aNaturalNumber0(xn))),
% 0.13/0.66 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.13/0.66 fof(f614,plain,(
% 0.13/0.66 ~aNaturalNumber0(xn)|sQ1_spl),
% 0.13/0.66 inference(component_clause,[status(thm)],[f612])).
% 0.13/0.66 fof(f619,definition,(
% 0.13/0.66 sQ3_spl <=> (aNaturalNumber0(xp))),
% 0.13/0.66 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.13/0.66 fof(f621,plain,(
% 0.13/0.66 ~aNaturalNumber0(xp)|sQ3_spl),
% 0.13/0.66 inference(component_clause,[status(thm)],[f619])).
% 0.13/0.66 fof(f647,plain,(
% 0.13/0.66 $false|sQ1_spl),
% 0.13/0.66 inference(forward_subsumption_resolution,[status(thm)],[f614,f165])).
% 0.13/0.66 fof(f648,plain,(
% 0.13/0.66 sQ1_spl),
% 0.13/0.66 inference(contradiction_clause,[status(thm)],[f647])).
% 0.13/0.66 fof(f649,plain,(
% 0.13/0.66 $false|sQ3_spl),
% 0.13/0.66 inference(forward_subsumption_resolution,[status(thm)],[f621,f167])).
% 0.13/0.66 fof(f650,plain,(
% 0.13/0.66 sQ3_spl),
% 0.13/0.66 inference(contradiction_clause,[status(thm)],[f649])).
% 0.13/0.66 fof(f2407,plain,(
% 0.13/0.66 ~aNaturalNumber0(xp)|~aNaturalNumber0(xn)|sdtpldt0(xp,sdtmndt0(xn,xp))=xn),
% 0.13/0.66 inference(resolution,[status(thm)],[f179,f172])).
% 0.13/0.66 fof(f2425,definition,(
% 0.13/0.66 sQ95_spl <=> (sdtpldt0(xp,sdtmndt0(xn,xp))=xn)),
% 0.13/0.66 introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition])).
% 0.13/0.66 fof(f2426,plain,(
% 0.13/0.66 sdtpldt0(xp,sdtmndt0(xn,xp))=xn|~sQ95_spl),
% 0.13/0.66 inference(component_clause,[status(thm)],[f2425])).
% 0.13/0.66 fof(f2428,plain,(
% 0.13/0.66 ~sQ3_spl|~sQ1_spl|sQ95_spl),
% 0.13/0.66 inference(split_clause,[status(thm)],[f2407,f619,f612,f2425])).
% 0.13/0.66 fof(f2433,plain,(
% 0.13/0.66 sdtpldt0(xp,xr)=xn|~sQ95_spl),
% 0.13/0.67 inference(forward_demodulation,[status(thm)],[f173,f2426])).
% 0.13/0.67 fof(f2434,plain,(
% 0.13/0.67 $false|~sQ95_spl),
% 0.13/0.67 inference(forward_subsumption_resolution,[status(thm)],[f2433,f176])).
% 0.13/0.67 fof(f2435,plain,(
% 0.13/0.67 ~sQ95_spl),
% 0.13/0.67 inference(contradiction_clause,[status(thm)],[f2434])).
% 0.13/0.67 fof(f2436,plain,(
% 0.13/0.67 $false),
% 0.13/0.67 inference(sat_refutation,[status(thm)],[f648,f650,f2428,f2435])).
% 0.13/0.67 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.68 % Elapsed time: 0.096386 seconds
% 0.13/0.68 % CPU time: 0.482104 seconds
% 0.13/0.68 % Total memory used: 110.896 MB
% 0.13/0.68 % Net memory used: 110.167 MB
%------------------------------------------------------------------------------