%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM521+3 : 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 : n006.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:06 PM UTC 2026
% Result : Theorem 3.45s 0.87s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM521+3 : 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.35 % Computer : n006.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 02:37:12 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.13/0.37 % Drodi V4.1.1
% 3.45/0.87 % Refutation found
% 3.45/0.87 % SZS status Theorem for theBenchmark: Theorem is valid
% 3.45/0.87 % SZS output start CNFRefutation for theBenchmark
% 3.45/0.87 fof(f2,axiom,(
% 3.45/0.87 aNaturalNumber0(sz00) ),
% 3.45/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.45/0.87 fof(f8,axiom,(
% 3.45/0.87 (! [W0] :( aNaturalNumber0(W0)=> ( sdtpldt0(W0,sz00) = W0& W0 = sdtpldt0(sz00,W0) ) ) )),
% 3.45/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.45/0.87 fof(f23,axiom,(
% 3.45/0.87 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> ( sdtlseqdt0(W0,W1)| ( W1 != W0& sdtlseqdt0(W1,W0) ) ) ) )),
% 3.45/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.45/0.87 fof(f39,hypothesis,(
% 3.45/0.87 ( aNaturalNumber0(xn)& aNaturalNumber0(xm)& aNaturalNumber0(xp) ) ),
% 3.45/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.45/0.87 fof(f42,hypothesis,(
% 3.45/0.87 ~ ( (? [W0] :( aNaturalNumber0(W0)& sdtpldt0(xp,W0) = xn ))| sdtlseqdt0(xp,xn) ) ),
% 3.45/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.45/0.87 fof(f43,hypothesis,(
% 3.45/0.87 ~ ( (? [W0] :( aNaturalNumber0(W0)& sdtpldt0(xp,W0) = xm ))| sdtlseqdt0(xp,xm) ) ),
% 3.45/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.45/0.87 fof(f44,hypothesis,(
% 3.45/0.87 ~ ( xn != xp& ( (? [W0] :( aNaturalNumber0(W0)& sdtpldt0(xn,W0) = xp ))| sdtlseqdt0(xn,xp) )& xm != xp& ( (? [W0] :( aNaturalNumber0(W0)& sdtpldt0(xm,W0) = xp ))| sdtlseqdt0(xm,xp) ) ) ),
% 3.45/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.45/0.87 fof(f50,plain,(
% 3.45/0.87 aNaturalNumber0(sz00)),
% 3.45/0.87 inference(cnf_transformation,[status(thm)],[f2])).
% 3.45/0.87 fof(f61,plain,(
% 3.45/0.87 ![W0]: (~aNaturalNumber0(W0)|(sdtpldt0(W0,sz00)=W0&W0=sdtpldt0(sz00,W0)))),
% 3.45/0.87 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 3.45/0.87 fof(f62,plain,(
% 3.45/0.87 ![X0]: (~aNaturalNumber0(X0)|sdtpldt0(X0,sz00)=X0)),
% 3.45/0.87 inference(cnf_transformation,[status(thm)],[f61])).
% 3.45/0.87 fof(f106,plain,(
% 3.45/0.87 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|(sdtlseqdt0(W0,W1)|(~W1=W0&sdtlseqdt0(W1,W0))))),
% 3.45/0.87 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 3.45/0.87 fof(f108,plain,(
% 3.45/0.87 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|sdtlseqdt0(X0,X1)|sdtlseqdt0(X1,X0))),
% 3.45/0.87 inference(cnf_transformation,[status(thm)],[f106])).
% 3.45/0.87 fof(f165,plain,(
% 3.45/0.87 aNaturalNumber0(xn)),
% 3.45/0.87 inference(cnf_transformation,[status(thm)],[f39])).
% 3.45/0.87 fof(f166,plain,(
% 3.45/0.87 aNaturalNumber0(xm)),
% 3.45/0.87 inference(cnf_transformation,[status(thm)],[f39])).
% 3.45/0.87 fof(f167,plain,(
% 3.45/0.87 aNaturalNumber0(xp)),
% 3.45/0.87 inference(cnf_transformation,[status(thm)],[f39])).
% 3.45/0.87 fof(f189,plain,(
% 3.45/0.87 ((![W0]: (~aNaturalNumber0(W0)|~sdtpldt0(xp,W0)=xn))&~sdtlseqdt0(xp,xn))),
% 3.45/0.87 inference(pre_NNF_transformation,[status(thm)],[f42])).
% 3.45/0.87 fof(f190,plain,(
% 3.45/0.87 ![X0]: (~aNaturalNumber0(X0)|~sdtpldt0(xp,X0)=xn)),
% 3.45/0.87 inference(cnf_transformation,[status(thm)],[f189])).
% 3.45/0.87 fof(f191,plain,(
% 3.45/0.87 ~sdtlseqdt0(xp,xn)),
% 3.45/0.87 inference(cnf_transformation,[status(thm)],[f189])).
% 3.45/0.87 fof(f192,plain,(
% 3.45/0.87 ((![W0]: (~aNaturalNumber0(W0)|~sdtpldt0(xp,W0)=xm))&~sdtlseqdt0(xp,xm))),
% 3.45/0.87 inference(pre_NNF_transformation,[status(thm)],[f43])).
% 3.45/0.87 fof(f193,plain,(
% 3.45/0.87 ![X0]: (~aNaturalNumber0(X0)|~sdtpldt0(xp,X0)=xm)),
% 3.45/0.87 inference(cnf_transformation,[status(thm)],[f192])).
% 3.45/0.87 fof(f194,plain,(
% 3.45/0.87 ~sdtlseqdt0(xp,xm)),
% 3.45/0.87 inference(cnf_transformation,[status(thm)],[f192])).
% 3.45/0.87 fof(f195,plain,(
% 3.45/0.87 (((xn=xp|((![W0]: (~aNaturalNumber0(W0)|~sdtpldt0(xn,W0)=xp))&~sdtlseqdt0(xn,xp)))|xm=xp)|((![W0]: (~aNaturalNumber0(W0)|~sdtpldt0(xm,W0)=xp))&~sdtlseqdt0(xm,xp)))),
% 3.45/0.87 inference(pre_NNF_transformation,[status(thm)],[f44])).
% 3.45/0.87 fof(f196,definition,(
% 3.45/0.87 sP2_prd<=>((![W0]: (~aNaturalNumber0(W0)|~sdtpldt0(xn,W0)=xp))&~sdtlseqdt0(xn,xp))),
% 3.45/0.87 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 3.45/0.87 fof(f197,plain,(
% 3.45/0.87 ((xn=xp|sP2_prd)|xm=xp)|((![W0]: (~aNaturalNumber0(W0)|~sdtpldt0(xm,W0)=xp))&~sdtlseqdt0(xm,xp))),
% 3.45/0.87 inference(formula_renaming,[status(thm)],[f195,f196])).
% 3.45/0.87 fof(f199,plain,(
% 3.45/0.87 xn=xp|sP2_prd|xm=xp|~sdtlseqdt0(xm,xp)),
% 3.45/0.87 inference(cnf_transformation,[status(thm)],[f197])).
% 3.45/0.87 fof(f225,plain,(
% 3.45/0.87 (~sP2_prd|((![W0]: (~aNaturalNumber0(W0)|~sdtpldt0(xn,W0)=xp))&~sdtlseqdt0(xn,xp)))&(sP2_prd|((?[W0]: (aNaturalNumber0(W0)&sdtpldt0(xn,W0)=xp))|sdtlseqdt0(xn,xp)))),
% 3.45/0.87 inference(NNF_transformation,[status(thm)],[f196])).
% 3.45/0.87 fof(f226,plain,(
% 3.45/0.87 (~sP2_prd|((![W0]: (~aNaturalNumber0(W0)|~sdtpldt0(xn,W0)=xp))&~sdtlseqdt0(xn,xp)))&(sP2_prd|((aNaturalNumber0(sK9_skl)&sdtpldt0(xn,sK9_skl)=xp)|sdtlseqdt0(xn,xp)))),
% 3.45/0.89 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(W0,sK9_skl)],[f225])).
% 3.45/0.89 fof(f228,plain,(
% 3.45/0.89 ~sP2_prd|~sdtlseqdt0(xn,xp)),
% 3.45/0.89 inference(cnf_transformation,[status(thm)],[f226])).
% 3.45/0.89 fof(f311,plain,(
% 3.45/0.89 sdtpldt0(xp,sz00)=xp),
% 3.45/0.89 inference(resolution,[status(thm)],[f62,f167])).
% 3.45/0.89 fof(f330,plain,(
% 3.45/0.89 ~sdtpldt0(xp,sz00)=xm),
% 3.45/0.89 inference(resolution,[status(thm)],[f50,f193])).
% 3.45/0.89 fof(f331,plain,(
% 3.45/0.89 ~sdtpldt0(xp,sz00)=xn),
% 3.45/0.89 inference(resolution,[status(thm)],[f50,f190])).
% 3.45/0.89 fof(f336,plain,(
% 3.45/0.89 xn=xp|sP2_prd|~sdtlseqdt0(xm,xp)),
% 3.45/0.89 inference(backward_subsumption_resolution,[status(thm)],[f199,f338])).
% 3.45/0.89 fof(f338,plain,(
% 3.45/0.89 ~xp=xm),
% 3.45/0.89 inference(forward_demodulation,[status(thm)],[f311,f330])).
% 3.45/0.89 fof(f339,plain,(
% 3.45/0.89 ~xp=xn),
% 3.45/0.89 inference(forward_demodulation,[status(thm)],[f311,f331])).
% 3.45/0.89 fof(f340,plain,(
% 3.45/0.89 sP2_prd|~sdtlseqdt0(xm,xp)),
% 3.45/0.89 inference(forward_subsumption_resolution,[status(thm)],[f336,f339])).
% 3.45/0.89 fof(f641,plain,(
% 3.45/0.89 ![X0]: (~aNaturalNumber0(X0)|sdtlseqdt0(X0,xp)|sdtlseqdt0(xp,X0))),
% 3.45/0.89 inference(resolution,[status(thm)],[f108,f167])).
% 3.45/0.89 fof(f655,plain,(
% 3.45/0.89 sdtlseqdt0(xm,xp)|sdtlseqdt0(xp,xm)),
% 3.45/0.89 inference(resolution,[status(thm)],[f641,f166])).
% 3.45/0.89 fof(f656,plain,(
% 3.45/0.89 sdtlseqdt0(xn,xp)|sdtlseqdt0(xp,xn)),
% 3.45/0.89 inference(resolution,[status(thm)],[f641,f165])).
% 3.45/0.89 fof(f658,plain,(
% 3.45/0.89 sP2_prd),
% 3.45/0.89 inference(backward_subsumption_resolution,[status(thm)],[f340,f659])).
% 3.45/0.89 fof(f659,plain,(
% 3.45/0.89 sdtlseqdt0(xm,xp)),
% 3.45/0.89 inference(forward_subsumption_resolution,[status(thm)],[f655,f194])).
% 3.45/0.89 fof(f660,plain,(
% 3.45/0.89 ~sP2_prd),
% 3.45/0.89 inference(backward_subsumption_resolution,[status(thm)],[f228,f661])).
% 3.45/0.89 fof(f661,plain,(
% 3.45/0.89 sdtlseqdt0(xn,xp)),
% 3.45/0.89 inference(forward_subsumption_resolution,[status(thm)],[f656,f191])).
% 3.45/0.89 fof(f663,plain,(
% 3.45/0.89 $false),
% 3.45/0.89 inference(forward_subsumption_resolution,[status(thm)],[f660,f658])).
% 3.45/0.89 % SZS output end CNFRefutation for theBenchmark.p
% 2.55/0.90 % Elapsed time: 0.529624 seconds
% 2.55/0.90 % CPU time: 3.986971 seconds
% 2.55/0.90 % Total memory used: 149.149 MB
% 2.55/0.90 % Net memory used: 145.047 MB
%------------------------------------------------------------------------------