%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM463+2 : 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 : n015.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:58 PM UTC 2026
% Result : Theorem 0.14s 10.43s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM463+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/10.37 % Computer : n015.cluster.edu
% 0.09/10.37 % Model : x86_64 x86_64
% 0.09/10.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/10.37 % Memory : 8046.5625MB
% 0.09/10.37 % OS : Linux 6.8.0-71-generic
% 0.09/10.37 % CPULimit : 300
% 0.09/10.37 % WCLimit : 300
% 0.09/10.37 % DateTime : Mon Sep 21 02:35:16 UTC 2026
% 0.09/10.37 % CPUTime :
% 0.09/10.39 % Drodi V4.1.1
% 0.14/10.43 % Refutation found
% 0.14/10.43 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/10.43 % SZS output start CNFRefutation for theBenchmark
% 0.14/10.43 fof(f2,axiom,(
% 0.14/10.43 aNaturalNumber0(sz00) ),
% 0.14/10.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/10.43 fof(f3,axiom,(
% 0.14/10.43 ( aNaturalNumber0(sz10)& sz10 != sz00 ) ),
% 0.14/10.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/10.43 fof(f8,axiom,(
% 0.14/10.43 (! [W0] :( aNaturalNumber0(W0)=> ( sdtpldt0(W0,sz00) = W0& W0 = sdtpldt0(sz00,W0) ) ) )),
% 0.14/10.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/10.43 fof(f11,axiom,(
% 0.14/10.43 (! [W0] :( aNaturalNumber0(W0)=> ( sdtasdt0(W0,sz10) = W0& W0 = sdtasdt0(sz10,W0) ) ) )),
% 0.14/10.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/10.43 fof(f12,axiom,(
% 0.14/10.43 (! [W0] :( aNaturalNumber0(W0)=> ( sdtasdt0(W0,sz00) = sz00& sz00 = sdtasdt0(sz00,W0) ) ) )),
% 0.14/10.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/10.43 fof(f25,axiom,(
% 0.14/10.43 (! [W0,W1,W2] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1)& aNaturalNumber0(W2) )=> ( ( W0 != sz00& W1 != W2& sdtlseqdt0(W1,W2) )=> ( sdtasdt0(W0,W1) != sdtasdt0(W0,W2)& sdtlseqdt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2))& sdtasdt0(W1,W0) != sdtasdt0(W2,W0)& sdtlseqdt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0)) ) ) ) )),
% 0.14/10.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/10.43 fof(f26,axiom,(
% 0.14/10.43 (! [W0] :( aNaturalNumber0(W0)=> ( W0 = sz00| W0 = sz10| ( sz10 != W0& sdtlseqdt0(sz10,W0) ) ) ) )),
% 0.14/10.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/10.43 fof(f27,hypothesis,(
% 0.14/10.43 ( aNaturalNumber0(xm)& aNaturalNumber0(xn) ) ),
% 0.14/10.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/10.43 fof(f28,conjecture,(
% 0.14/10.43 ( xm != sz00=> ( (? [W0] :( aNaturalNumber0(W0)& sdtpldt0(xn,W0) = sdtasdt0(xn,xm) ))| sdtlseqdt0(xn,sdtasdt0(xn,xm)) ) ) ),
% 0.14/10.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/10.43 fof(f29,negated_conjecture,(
% 0.14/10.43 ~(( xm != sz00=> ( (? [W0] :( aNaturalNumber0(W0)& sdtpldt0(xn,W0) = sdtasdt0(xn,xm) ))| sdtlseqdt0(xn,sdtasdt0(xn,xm)) ) ) )),
% 0.14/10.43 inference(negated_conjecture,[status(cth)],[f28])).
% 0.14/10.43 fof(f33,plain,(
% 0.14/10.43 aNaturalNumber0(sz00)),
% 0.14/10.43 inference(cnf_transformation,[status(thm)],[f2])).
% 0.14/10.43 fof(f34,plain,(
% 0.14/10.43 aNaturalNumber0(sz10)),
% 0.14/10.43 inference(cnf_transformation,[status(thm)],[f3])).
% 0.14/10.43 fof(f44,plain,(
% 0.14/10.43 ![W0]: (~aNaturalNumber0(W0)|(sdtpldt0(W0,sz00)=W0&W0=sdtpldt0(sz00,W0)))),
% 0.14/10.43 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 0.14/10.43 fof(f45,plain,(
% 0.14/10.43 ![X0]: (~aNaturalNumber0(X0)|sdtpldt0(X0,sz00)=X0)),
% 0.14/10.43 inference(cnf_transformation,[status(thm)],[f44])).
% 0.14/10.43 fof(f51,plain,(
% 0.14/10.43 ![W0]: (~aNaturalNumber0(W0)|(sdtasdt0(W0,sz10)=W0&W0=sdtasdt0(sz10,W0)))),
% 0.14/10.43 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 0.14/10.43 fof(f52,plain,(
% 0.14/10.43 ![X0]: (~aNaturalNumber0(X0)|sdtasdt0(X0,sz10)=X0)),
% 0.14/10.43 inference(cnf_transformation,[status(thm)],[f51])).
% 0.14/10.43 fof(f54,plain,(
% 0.14/10.43 ![W0]: (~aNaturalNumber0(W0)|(sdtasdt0(W0,sz00)=sz00&sz00=sdtasdt0(sz00,W0)))),
% 0.14/10.43 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 0.14/10.43 fof(f56,plain,(
% 0.14/10.43 ![X0]: (~aNaturalNumber0(X0)|sz00=sdtasdt0(sz00,X0))),
% 0.14/10.43 inference(cnf_transformation,[status(thm)],[f54])).
% 0.14/10.43 fof(f97,plain,(
% 0.14/10.43 ![W0,W1,W2]: (((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|~aNaturalNumber0(W2))|(((W0=sz00|W1=W2)|~sdtlseqdt0(W1,W2))|(((~sdtasdt0(W0,W1)=sdtasdt0(W0,W2)&sdtlseqdt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)))&~sdtasdt0(W1,W0)=sdtasdt0(W2,W0))&sdtlseqdt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0)))))),
% 0.14/10.43 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 0.14/10.43 fof(f99,plain,(
% 0.14/10.43 ![X0,X1,X2]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|X0=sz00|X1=X2|~sdtlseqdt0(X1,X2)|sdtlseqdt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2)))),
% 0.14/10.43 inference(cnf_transformation,[status(thm)],[f97])).
% 0.14/10.43 fof(f102,plain,(
% 0.14/10.43 ![W0]: (~aNaturalNumber0(W0)|((W0=sz00|W0=sz10)|(~sz10=W0&sdtlseqdt0(sz10,W0))))),
% 0.14/10.43 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 0.14/10.43 fof(f104,plain,(
% 0.14/10.43 ![X0]: (~aNaturalNumber0(X0)|X0=sz00|X0=sz10|sdtlseqdt0(sz10,X0))),
% 0.14/10.43 inference(cnf_transformation,[status(thm)],[f102])).
% 0.14/10.43 fof(f105,plain,(
% 0.14/10.43 aNaturalNumber0(xm)),
% 0.14/10.43 inference(cnf_transformation,[status(thm)],[f27])).
% 0.14/10.43 fof(f106,plain,(
% 0.14/10.43 aNaturalNumber0(xn)),
% 0.14/10.43 inference(cnf_transformation,[status(thm)],[f27])).
% 0.14/10.43 fof(f107,plain,(
% 0.14/10.43 (~xm=sz00&((![W0]: (~aNaturalNumber0(W0)|~sdtpldt0(xn,W0)=sdtasdt0(xn,xm)))&~sdtlseqdt0(xn,sdtasdt0(xn,xm))))),
% 0.14/10.43 inference(pre_NNF_transformation,[status(thm)],[f29])).
% 0.14/10.43 fof(f108,plain,(
% 0.14/10.43 ~xm=sz00),
% 0.14/10.43 inference(cnf_transformation,[status(thm)],[f107])).
% 0.14/10.43 fof(f109,plain,(
% 0.14/10.43 ![X0]: (~aNaturalNumber0(X0)|~sdtpldt0(xn,X0)=sdtasdt0(xn,xm))),
% 0.14/10.43 inference(cnf_transformation,[status(thm)],[f107])).
% 0.14/10.43 fof(f110,plain,(
% 0.14/10.43 ~sdtlseqdt0(xn,sdtasdt0(xn,xm))),
% 0.14/10.43 inference(cnf_transformation,[status(thm)],[f107])).
% 0.14/10.43 fof(f119,plain,(
% 0.14/10.43 ~sdtpldt0(xn,sz00)=sdtasdt0(xn,xm)),
% 0.14/10.43 inference(resolution,[status(thm)],[f33,f109])).
% 0.14/10.43 fof(f139,plain,(
% 0.14/10.43 sdtpldt0(xn,sz00)=xn),
% 0.14/10.43 inference(resolution,[status(thm)],[f45,f106])).
% 0.14/10.43 fof(f143,plain,(
% 0.14/10.43 ~xn=sdtasdt0(xn,xm)),
% 0.14/10.43 inference(backward_demodulation,[status(thm)],[f139,f119])).
% 0.14/10.43 fof(f156,plain,(
% 0.14/10.43 sdtasdt0(xn,sz10)=xn),
% 0.14/10.43 inference(resolution,[status(thm)],[f52,f106])).
% 0.14/10.43 fof(f206,definition,(
% 0.14/10.43 sQ8_spl <=> (sdtlseqdt0(sz10,xm))),
% 0.14/10.43 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.14/10.43 fof(f207,plain,(
% 0.14/10.43 sdtlseqdt0(sz10,xm)|~sQ8_spl),
% 0.14/10.43 inference(component_clause,[status(thm)],[f206])).
% 0.14/10.43 fof(f241,definition,(
% 0.14/10.43 sQ15_spl <=> (xn=sz00)),
% 0.14/10.43 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.14/10.43 fof(f242,plain,(
% 0.14/10.43 xn=sz00|~sQ15_spl),
% 0.14/10.43 inference(component_clause,[status(thm)],[f241])).
% 0.14/10.43 fof(f255,definition,(
% 0.14/10.43 sQ19_spl <=> (xm=sz00)),
% 0.14/10.43 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.14/10.43 fof(f256,plain,(
% 0.14/10.43 xm=sz00|~sQ19_spl),
% 0.14/10.43 inference(component_clause,[status(thm)],[f255])).
% 0.14/10.43 fof(f269,plain,(
% 0.14/10.43 $false|~sQ19_spl),
% 0.14/10.43 inference(forward_subsumption_resolution,[status(thm)],[f256,f108])).
% 0.14/10.43 fof(f270,plain,(
% 0.14/10.43 ~sQ19_spl),
% 0.14/10.43 inference(contradiction_clause,[status(thm)],[f269])).
% 0.14/10.43 fof(f286,plain,(
% 0.14/10.43 ~xn=sdtasdt0(sz00,xm)|~sQ15_spl),
% 0.14/10.43 inference(backward_demodulation,[status(thm)],[f242,f143])).
% 0.14/10.43 fof(f304,plain,(
% 0.14/10.43 ~sz00=sdtasdt0(sz00,xm)|~sQ15_spl),
% 0.14/10.43 inference(forward_demodulation,[status(thm)],[f242,f286])).
% 0.14/10.43 fof(f385,plain,(
% 0.14/10.43 xm=sz00|xm=sz10|sdtlseqdt0(sz10,xm)),
% 0.14/10.43 inference(resolution,[status(thm)],[f104,f105])).
% 0.14/10.43 fof(f391,definition,(
% 0.14/10.43 sQ37_spl <=> (xm=sz10)),
% 0.14/10.43 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.14/10.43 fof(f392,plain,(
% 0.14/10.43 xm=sz10|~sQ37_spl),
% 0.14/10.43 inference(component_clause,[status(thm)],[f391])).
% 0.14/10.43 fof(f394,plain,(
% 0.14/10.43 sQ19_spl|sQ37_spl|sQ8_spl),
% 0.14/10.43 inference(split_clause,[status(thm)],[f385,f255,f391,f206])).
% 0.14/10.43 fof(f406,plain,(
% 0.14/10.43 sz00=sdtasdt0(sz00,xm)),
% 0.14/10.43 inference(resolution,[status(thm)],[f56,f105])).
% 0.14/10.43 fof(f408,plain,(
% 0.14/10.43 $false|~sQ15_spl),
% 0.14/10.43 inference(forward_subsumption_resolution,[status(thm)],[f406,f304])).
% 0.14/10.43 fof(f409,plain,(
% 0.14/10.43 ~sQ15_spl),
% 0.14/10.43 inference(contradiction_clause,[status(thm)],[f408])).
% 0.14/10.43 fof(f459,plain,(
% 0.14/10.43 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|xn=sz00|X0=X1|~sdtlseqdt0(X0,X1)|sdtlseqdt0(sdtasdt0(xn,X0),sdtasdt0(xn,X1)))),
% 0.14/10.43 inference(resolution,[status(thm)],[f106,f99])).
% 0.14/10.43 fof(f490,definition,(
% 0.14/10.43 ![X0,X1]: (sQ44_spl <=> (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|X0=X1|~sdtlseqdt0(X0,X1)|sdtlseqdt0(sdtasdt0(xn,X0),sdtasdt0(xn,X1))))),
% 0.14/10.43 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.14/10.43 fof(f491,plain,(
% 0.14/10.43 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|X0=X1|~sdtlseqdt0(X0,X1)|sdtlseqdt0(sdtasdt0(xn,X0),sdtasdt0(xn,X1))|~sQ44_spl)),
% 0.14/10.43 inference(component_clause,[status(thm)],[f490])).
% 0.14/10.43 fof(f493,plain,(
% 0.14/10.43 sQ44_spl|sQ15_spl),
% 0.14/10.43 inference(split_clause,[status(thm)],[f459,f490,f241])).
% 0.14/10.43 fof(f513,definition,(
% 0.14/10.43 sQ47_spl <=> (aNaturalNumber0(sz10))),
% 0.14/10.43 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.14/10.43 fof(f515,plain,(
% 0.14/10.43 ~aNaturalNumber0(sz10)|sQ47_spl),
% 0.14/10.43 inference(component_clause,[status(thm)],[f513])).
% 0.14/10.43 fof(f588,plain,(
% 0.14/10.43 $false|sQ47_spl),
% 0.14/10.43 inference(forward_subsumption_resolution,[status(thm)],[f515,f34])).
% 0.14/10.43 fof(f589,plain,(
% 0.14/10.43 sQ47_spl),
% 0.14/10.43 inference(contradiction_clause,[status(thm)],[f588])).
% 0.14/10.43 fof(f592,plain,(
% 0.14/10.43 ~aNaturalNumber0(sz10)|~aNaturalNumber0(xm)|sz10=xm|sdtlseqdt0(sdtasdt0(xn,sz10),sdtasdt0(xn,xm))|~sQ8_spl|~sQ44_spl),
% 0.14/10.43 inference(resolution,[status(thm)],[f207,f491])).
% 0.14/10.43 fof(f600,definition,(
% 0.14/10.43 sQ64_spl <=> (aNaturalNumber0(xm))),
% 0.14/10.43 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 0.14/10.43 fof(f602,plain,(
% 0.14/10.43 ~aNaturalNumber0(xm)|sQ64_spl),
% 0.14/10.43 inference(component_clause,[status(thm)],[f600])).
% 0.14/10.43 fof(f603,definition,(
% 0.14/10.43 sQ65_spl <=> (sdtlseqdt0(sdtasdt0(xn,sz10),sdtasdt0(xn,xm)))),
% 0.14/10.43 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 0.14/10.43 fof(f604,plain,(
% 0.14/10.43 sdtlseqdt0(sdtasdt0(xn,sz10),sdtasdt0(xn,xm))|~sQ65_spl),
% 0.14/10.43 inference(component_clause,[status(thm)],[f603])).
% 0.14/10.43 fof(f606,plain,(
% 0.14/10.43 ~sQ47_spl|~sQ64_spl|sQ37_spl|sQ65_spl|~sQ8_spl|~sQ44_spl),
% 0.14/10.43 inference(split_clause,[status(thm)],[f592,f513,f600,f391,f603,f206,f490])).
% 0.14/10.43 fof(f639,plain,(
% 0.14/10.43 ~xn=sdtasdt0(xn,sz10)|~sQ37_spl),
% 0.14/10.43 inference(backward_demodulation,[status(thm)],[f392,f143])).
% 0.14/10.43 fof(f674,plain,(
% 0.14/10.43 ~xn=xn|~sQ37_spl),
% 0.14/10.43 inference(forward_demodulation,[status(thm)],[f156,f639])).
% 0.14/10.43 fof(f675,plain,(
% 0.14/10.43 $false|~sQ37_spl),
% 0.14/10.43 inference(trivial_equality_resolution,[status(thm)],[f674])).
% 0.14/10.43 fof(f676,plain,(
% 0.14/10.43 ~sQ37_spl),
% 0.14/10.43 inference(contradiction_clause,[status(thm)],[f675])).
% 0.14/10.43 fof(f677,plain,(
% 0.14/10.43 $false|sQ64_spl),
% 0.14/10.43 inference(forward_subsumption_resolution,[status(thm)],[f105,f602])).
% 0.14/10.43 fof(f678,plain,(
% 0.14/10.43 sQ64_spl),
% 0.14/10.43 inference(contradiction_clause,[status(thm)],[f677])).
% 0.14/10.43 fof(f686,plain,(
% 0.14/10.43 sdtlseqdt0(xn,sdtasdt0(xn,xm))|~sQ65_spl),
% 0.14/10.43 inference(forward_demodulation,[status(thm)],[f156,f604])).
% 0.14/10.43 fof(f687,plain,(
% 0.14/10.43 $false|~sQ65_spl),
% 0.14/10.43 inference(forward_subsumption_resolution,[status(thm)],[f686,f110])).
% 0.14/10.43 fof(f688,plain,(
% 0.14/10.43 ~sQ65_spl),
% 0.14/10.43 inference(contradiction_clause,[status(thm)],[f687])).
% 0.14/10.43 fof(f689,plain,(
% 0.14/10.43 $false),
% 0.14/10.43 inference(sat_refutation,[status(thm)],[f270,f394,f409,f493,f589,f606,f676,f678,f688])).
% 0.14/10.43 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/10.45 % Elapsed time: 0.066546 seconds
% 0.14/10.45 % CPU time: 0.299614 seconds
% 0.14/10.45 % Total memory used: 59.290 MB
% 0.14/10.45 % Net memory used: 58.978 MB
%------------------------------------------------------------------------------