%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM525+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 : n002.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 54.93s 7.79s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : NUM525+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n002.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Mon Sep 21 02:40:17 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.18/0.46 % Drodi V4.1.1
% 54.93/7.79 % Refutation found
% 54.93/7.79 % SZS status Theorem for theBenchmark: Theorem is valid
% 54.93/7.79 % SZS output start CNFRefutation for theBenchmark
% 54.93/7.79 fof(f2,axiom,(
% 54.93/7.79 aNaturalNumber0(sz00) ),
% 54.93/7.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 54.93/7.79 fof(f4,axiom,(
% 54.93/7.79 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> aNaturalNumber0(sdtpldt0(W0,W1)) ) )),
% 54.93/7.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 54.93/7.79 fof(f5,axiom,(
% 54.93/7.79 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> aNaturalNumber0(sdtasdt0(W0,W1)) ) )),
% 54.93/7.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 54.93/7.79 fof(f8,axiom,(
% 54.93/7.79 (! [W0] :( aNaturalNumber0(W0)=> ( sdtpldt0(W0,sz00) = W0& W0 = sdtpldt0(sz00,W0) ) ) )),
% 54.93/7.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 54.93/7.79 fof(f9,axiom,(
% 54.93/7.79 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) )),
% 54.93/7.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 54.93/7.79 fof(f10,axiom,(
% 54.93/7.79 (! [W0,W1,W2] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1)& aNaturalNumber0(W2) )=> sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2)) ) )),
% 54.93/7.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 54.93/7.79 fof(f40,hypothesis,(
% 54.93/7.79 ( aNaturalNumber0(xn)& aNaturalNumber0(xm)& aNaturalNumber0(xp)& xn != sz00& xm != sz00& xp != sz00 ) ),
% 54.93/7.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 54.93/7.79 fof(f42,hypothesis,(
% 54.93/7.79 sdtasdt0(xp,sdtasdt0(xm,xm)) = sdtasdt0(xn,xn) ),
% 54.93/7.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 54.93/7.79 fof(f44,hypothesis,(
% 54.93/7.79 ( (? [W0] :( aNaturalNumber0(W0)& sdtasdt0(xn,xn) = sdtasdt0(xp,W0) ))& doDivides0(xp,sdtasdt0(xn,xn))& (? [W0] :( aNaturalNumber0(W0)& xn = sdtasdt0(xp,W0) ))& doDivides0(xp,xn) ) ),
% 54.93/7.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 54.93/7.79 fof(f45,hypothesis,(
% 54.93/7.79 ( aNaturalNumber0(xq)& xn = sdtasdt0(xp,xq)& xq = sdtsldt0(xn,xp) ) ),
% 54.93/7.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 54.93/7.79 fof(f46,conjecture,(
% 54.93/7.79 sdtasdt0(xp,sdtasdt0(xm,xm)) = sdtasdt0(xp,sdtasdt0(xp,sdtasdt0(xq,xq))) ),
% 54.93/7.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 54.93/7.79 fof(f47,negated_conjecture,(
% 54.93/7.79 ~(sdtasdt0(xp,sdtasdt0(xm,xm)) = sdtasdt0(xp,sdtasdt0(xp,sdtasdt0(xq,xq))) )),
% 54.93/7.79 inference(negated_conjecture,[status(cth)],[f46])).
% 54.93/7.79 fof(f51,plain,(
% 54.93/7.79 aNaturalNumber0(sz00)),
% 54.93/7.79 inference(cnf_transformation,[status(thm)],[f2])).
% 54.93/7.79 fof(f54,plain,(
% 54.93/7.79 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|aNaturalNumber0(sdtpldt0(W0,W1)))),
% 54.93/7.79 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 54.93/7.79 fof(f55,plain,(
% 54.93/7.79 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|aNaturalNumber0(sdtpldt0(X0,X1)))),
% 54.93/7.79 inference(cnf_transformation,[status(thm)],[f54])).
% 54.93/7.79 fof(f56,plain,(
% 54.93/7.79 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|aNaturalNumber0(sdtasdt0(W0,W1)))),
% 54.93/7.79 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 54.93/7.79 fof(f57,plain,(
% 54.93/7.79 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|aNaturalNumber0(sdtasdt0(X0,X1)))),
% 54.93/7.79 inference(cnf_transformation,[status(thm)],[f56])).
% 54.93/7.79 fof(f62,plain,(
% 54.93/7.79 ![W0]: (~aNaturalNumber0(W0)|(sdtpldt0(W0,sz00)=W0&W0=sdtpldt0(sz00,W0)))),
% 54.93/7.79 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 54.93/7.79 fof(f64,plain,(
% 54.93/7.79 ![X0]: (~aNaturalNumber0(X0)|X0=sdtpldt0(sz00,X0))),
% 54.93/7.79 inference(cnf_transformation,[status(thm)],[f62])).
% 54.93/7.79 fof(f65,plain,(
% 54.93/7.79 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|sdtasdt0(W0,W1)=sdtasdt0(W1,W0))),
% 54.93/7.79 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 54.93/7.79 fof(f66,plain,(
% 54.93/7.79 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|sdtasdt0(X0,X1)=sdtasdt0(X1,X0))),
% 54.93/7.79 inference(cnf_transformation,[status(thm)],[f65])).
% 54.93/7.79 fof(f67,plain,(
% 54.93/7.79 ![W0,W1,W2]: (((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|~aNaturalNumber0(W2))|sdtasdt0(sdtasdt0(W0,W1),W2)=sdtasdt0(W0,sdtasdt0(W1,W2)))),
% 54.93/7.79 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 54.93/7.79 fof(f68,plain,(
% 54.93/7.79 ![X0,X1,X2]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|sdtasdt0(sdtasdt0(X0,X1),X2)=sdtasdt0(X0,sdtasdt0(X1,X2)))),
% 54.93/7.79 inference(cnf_transformation,[status(thm)],[f67])).
% 54.93/7.79 fof(f170,plain,(
% 54.93/7.79 aNaturalNumber0(xp)),
% 54.93/7.79 inference(cnf_transformation,[status(thm)],[f40])).
% 54.93/7.79 fof(f183,plain,(
% 54.93/7.79 sdtasdt0(xp,sdtasdt0(xm,xm))=sdtasdt0(xn,xn)),
% 54.93/7.79 inference(cnf_transformation,[status(thm)],[f42])).
% 54.93/7.79 fof(f189,plain,(
% 54.93/7.79 (((aNaturalNumber0(sK6_skl)&sdtasdt0(xn,xn)=sdtasdt0(xp,sK6_skl))&doDivides0(xp,sdtasdt0(xn,xn)))&(aNaturalNumber0(sK7_skl)&xn=sdtasdt0(xp,sK7_skl)))&doDivides0(xp,xn)),
% 54.93/7.79 inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl,sK7_skl]),skolemize(W0,sK6_skl),skolemize(W0,sK7_skl)],[f44])).
% 54.93/7.79 fof(f191,plain,(
% 54.93/7.79 sdtasdt0(xn,xn)=sdtasdt0(xp,sK6_skl)),
% 54.93/7.79 inference(cnf_transformation,[status(thm)],[f189])).
% 54.93/7.79 fof(f193,plain,(
% 54.93/7.79 aNaturalNumber0(sK7_skl)),
% 54.93/7.79 inference(cnf_transformation,[status(thm)],[f189])).
% 54.93/7.79 fof(f194,plain,(
% 54.93/7.79 xn=sdtasdt0(xp,sK7_skl)),
% 54.93/7.79 inference(cnf_transformation,[status(thm)],[f189])).
% 54.93/7.79 fof(f196,plain,(
% 54.93/7.79 aNaturalNumber0(xq)),
% 54.93/7.79 inference(cnf_transformation,[status(thm)],[f45])).
% 54.93/7.79 fof(f197,plain,(
% 54.93/7.79 xn=sdtasdt0(xp,xq)),
% 54.93/7.79 inference(cnf_transformation,[status(thm)],[f45])).
% 54.93/7.79 fof(f199,plain,(
% 54.93/7.79 ~sdtasdt0(xp,sdtasdt0(xm,xm))=sdtasdt0(xp,sdtasdt0(xp,sdtasdt0(xq,xq)))),
% 54.93/7.79 inference(cnf_transformation,[status(thm)],[f47])).
% 54.93/7.79 fof(f208,plain,(
% 54.93/7.79 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|sdtasdt0(sdtasdt0(X0,X1),xp)=sdtasdt0(X0,sdtasdt0(X1,xp)))),
% 54.93/7.79 inference(resolution,[status(thm)],[f170,f68])).
% 54.93/7.79 fof(f210,plain,(
% 54.93/7.79 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|sdtasdt0(sdtasdt0(X0,xp),X1)=sdtasdt0(X0,sdtasdt0(xp,X1)))),
% 54.93/7.79 inference(resolution,[status(thm)],[f170,f68])).
% 54.93/7.79 fof(f211,plain,(
% 54.93/7.79 ![X0]: (~aNaturalNumber0(X0)|sdtasdt0(X0,xp)=sdtasdt0(xp,X0))),
% 54.93/7.79 inference(resolution,[status(thm)],[f170,f66])).
% 54.93/7.79 fof(f212,plain,(
% 54.93/7.79 ![X0]: (~aNaturalNumber0(X0)|aNaturalNumber0(sdtasdt0(X0,xp)))),
% 54.93/7.79 inference(resolution,[status(thm)],[f57,f170])).
% 54.93/7.79 fof(f214,plain,(
% 54.93/7.79 ~sdtasdt0(xn,xn)=sdtasdt0(xp,sdtasdt0(xp,sdtasdt0(xq,xq)))),
% 54.93/7.79 inference(backward_demodulation,[status(thm)],[f183,f199])).
% 54.93/7.79 fof(f216,plain,(
% 54.93/7.79 ![X0]: (~aNaturalNumber0(X0)|sdtasdt0(sdtasdt0(X0,xq),xq)=sdtasdt0(X0,sdtasdt0(xq,xq)))),
% 54.93/7.79 inference(resolution,[status(thm)],[f196,f68])).
% 54.93/7.79 fof(f219,plain,(
% 54.93/7.79 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|sdtasdt0(sdtasdt0(X0,xq),X1)=sdtasdt0(X0,sdtasdt0(xq,X1)))),
% 54.93/7.79 inference(resolution,[status(thm)],[f196,f68])).
% 54.93/7.79 fof(f220,plain,(
% 54.93/7.79 ![X0]: (~aNaturalNumber0(X0)|sdtasdt0(X0,xq)=sdtasdt0(xq,X0))),
% 54.93/7.79 inference(resolution,[status(thm)],[f196,f66])).
% 54.93/7.79 fof(f270,plain,(
% 54.93/7.79 ![X0]: (~aNaturalNumber0(X0)|sdtasdt0(sdtasdt0(X0,sK7_skl),xp)=sdtasdt0(X0,sdtasdt0(sK7_skl,xp)))),
% 54.93/7.79 inference(resolution,[status(thm)],[f208,f193])).
% 54.93/7.79 fof(f272,plain,(
% 54.93/7.79 ![X0]: (~aNaturalNumber0(X0)|sdtasdt0(sdtasdt0(X0,xq),xp)=sdtasdt0(X0,sdtasdt0(xq,xp)))),
% 54.93/7.79 inference(resolution,[status(thm)],[f208,f196])).
% 54.93/7.79 fof(f277,plain,(
% 54.93/7.79 ![X0]: (~aNaturalNumber0(X0)|sdtasdt0(sdtasdt0(X0,xp),xq)=sdtasdt0(X0,sdtasdt0(xp,xq)))),
% 54.93/7.79 inference(resolution,[status(thm)],[f210,f196])).
% 54.93/7.79 fof(f281,plain,(
% 54.93/7.79 ![X0]: (~aNaturalNumber0(X0)|sdtasdt0(sdtasdt0(X0,xp),xq)=sdtasdt0(X0,xn))),
% 54.93/7.79 inference(forward_demodulation,[status(thm)],[f197,f277])).
% 54.93/7.79 fof(f282,plain,(
% 54.93/7.79 sdtasdt0(sK7_skl,xp)=sdtasdt0(xp,sK7_skl)),
% 54.93/7.79 inference(resolution,[status(thm)],[f211,f193])).
% 54.93/7.79 fof(f284,plain,(
% 54.93/7.79 sdtasdt0(xq,xp)=sdtasdt0(xp,xq)),
% 54.93/7.79 inference(resolution,[status(thm)],[f211,f196])).
% 54.93/7.79 fof(f287,plain,(
% 54.93/7.79 sdtasdt0(sK7_skl,xp)=xn),
% 54.93/7.79 inference(forward_demodulation,[status(thm)],[f194,f282])).
% 54.93/7.79 fof(f288,plain,(
% 54.93/7.79 sdtasdt0(xq,xp)=xn),
% 54.93/7.79 inference(forward_demodulation,[status(thm)],[f197,f284])).
% 54.93/7.79 fof(f289,plain,(
% 54.93/7.79 ~sdtasdt0(xp,sK6_skl)=sdtasdt0(xp,sdtasdt0(xp,sdtasdt0(xq,xq)))),
% 54.93/7.79 inference(forward_demodulation,[status(thm)],[f191,f214])).
% 54.93/7.79 fof(f293,plain,(
% 54.93/7.79 sdtasdt0(sdtasdt0(xp,xq),xq)=sdtasdt0(xp,sdtasdt0(xq,xq))),
% 54.93/7.79 inference(resolution,[status(thm)],[f216,f170])).
% 54.93/7.79 fof(f295,plain,(
% 54.93/7.79 sdtasdt0(xn,xq)=sdtasdt0(xp,sdtasdt0(xq,xq))),
% 54.93/7.79 inference(forward_demodulation,[status(thm)],[f197,f293])).
% 54.93/7.79 fof(f347,plain,(
% 54.93/7.79 sdtasdt0(sK7_skl,xq)=sdtasdt0(xq,sK7_skl)),
% 54.93/7.79 inference(resolution,[status(thm)],[f220,f193])).
% 54.93/7.79 fof(f426,plain,(
% 54.93/7.79 ![X0]: (~aNaturalNumber0(X0)|aNaturalNumber0(sdtpldt0(X0,xp)))),
% 54.93/7.79 inference(resolution,[status(thm)],[f55,f170])).
% 54.93/7.83 fof(f489,plain,(
% 54.93/7.83 sdtasdt0(sdtasdt0(xq,sK7_skl),xp)=sdtasdt0(xq,sdtasdt0(sK7_skl,xp))),
% 54.93/7.83 inference(resolution,[status(thm)],[f270,f196])).
% 54.93/7.83 fof(f503,plain,(
% 54.93/7.83 sdtasdt0(sdtasdt0(sK7_skl,xq),xp)=sdtasdt0(sK7_skl,sdtasdt0(xq,xp))),
% 54.93/7.83 inference(resolution,[status(thm)],[f272,f193])).
% 54.93/7.83 fof(f544,plain,(
% 54.93/7.83 sdtasdt0(sdtasdt0(sK7_skl,xp),xq)=sdtasdt0(sK7_skl,xn)),
% 54.93/7.83 inference(resolution,[status(thm)],[f281,f193])).
% 54.93/7.83 fof(f558,plain,(
% 54.93/7.83 aNaturalNumber0(sdtasdt0(xq,xp))),
% 54.93/7.83 inference(resolution,[status(thm)],[f212,f196])).
% 54.93/7.83 fof(f568,plain,(
% 54.93/7.83 ~sdtasdt0(xp,sK6_skl)=sdtasdt0(xp,sdtasdt0(xn,xq))),
% 54.93/7.83 inference(backward_demodulation,[status(thm)],[f295,f289])).
% 54.93/7.83 fof(f618,plain,(
% 54.93/7.83 xp=sdtpldt0(sz00,xp)),
% 54.93/7.83 inference(resolution,[status(thm)],[f64,f170])).
% 54.93/7.83 fof(f1067,plain,(
% 54.93/7.83 aNaturalNumber0(sdtpldt0(sz00,xp))),
% 54.93/7.83 inference(resolution,[status(thm)],[f426,f51])).
% 54.93/7.83 fof(f1211,plain,(
% 54.93/7.83 sdtasdt0(sdtasdt0(xq,sK7_skl),xp)=sdtasdt0(xq,xn)),
% 54.93/7.83 inference(forward_demodulation,[status(thm)],[f287,f489])).
% 54.93/7.83 fof(f1247,plain,(
% 54.93/7.83 sdtasdt0(sdtasdt0(xq,sK7_skl),xp)=sdtasdt0(sK7_skl,sdtasdt0(xq,xp))),
% 54.93/7.83 inference(forward_demodulation,[status(thm)],[f347,f503])).
% 54.93/7.83 fof(f1248,plain,(
% 54.93/7.83 sdtasdt0(xq,xn)=sdtasdt0(sK7_skl,sdtasdt0(xq,xp))),
% 54.93/7.83 inference(forward_demodulation,[status(thm)],[f1211,f1247])).
% 54.93/7.83 fof(f1250,plain,(
% 54.93/7.83 sdtasdt0(xq,xn)=sdtasdt0(sK7_skl,xn)),
% 54.93/7.83 inference(forward_demodulation,[status(thm)],[f288,f1248])).
% 54.93/7.83 fof(f1347,plain,(
% 54.93/7.83 sdtasdt0(xn,xq)=sdtasdt0(sK7_skl,xn)),
% 54.93/7.83 inference(forward_demodulation,[status(thm)],[f287,f544])).
% 54.93/7.83 fof(f1348,plain,(
% 54.93/7.83 ~sdtasdt0(xp,sK6_skl)=sdtasdt0(xp,sdtasdt0(xq,xn))),
% 54.93/7.83 inference(backward_demodulation,[status(thm)],[f1350,f568])).
% 54.93/7.83 fof(f1350,plain,(
% 54.93/7.83 sdtasdt0(xn,xq)=sdtasdt0(xq,xn)),
% 54.93/7.83 inference(forward_demodulation,[status(thm)],[f1250,f1347])).
% 54.93/7.83 fof(f1354,plain,(
% 54.93/7.83 aNaturalNumber0(xn)),
% 54.93/7.83 inference(forward_demodulation,[status(thm)],[f288,f558])).
% 54.93/7.83 fof(f1430,plain,(
% 54.93/7.83 ![X0]: (~aNaturalNumber0(X0)|sdtasdt0(sdtasdt0(X0,xq),xn)=sdtasdt0(X0,sdtasdt0(xq,xn)))),
% 54.93/7.83 inference(resolution,[status(thm)],[f1354,f219])).
% 54.93/7.83 fof(f3553,plain,(
% 54.93/7.83 aNaturalNumber0(xp)),
% 54.93/7.83 inference(forward_demodulation,[status(thm)],[f618,f1067])).
% 54.93/7.83 fof(f4226,plain,(
% 54.93/7.83 sdtasdt0(sdtasdt0(xp,xq),xn)=sdtasdt0(xp,sdtasdt0(xq,xn))),
% 54.93/7.83 inference(resolution,[status(thm)],[f1430,f3553])).
% 54.93/7.83 fof(f4243,plain,(
% 54.93/7.83 sdtasdt0(xn,xn)=sdtasdt0(xp,sdtasdt0(xq,xn))),
% 54.93/7.83 inference(forward_demodulation,[status(thm)],[f197,f4226])).
% 54.93/7.83 fof(f14924,plain,(
% 54.93/7.83 ~sdtasdt0(xp,sK6_skl)=sdtasdt0(xn,xn)),
% 54.93/7.83 inference(forward_demodulation,[status(thm)],[f4243,f1348])).
% 54.93/7.83 fof(f15991,plain,(
% 54.93/7.83 $false),
% 54.93/7.83 inference(forward_subsumption_resolution,[status(thm)],[f191,f14924])).
% 54.93/7.83 % SZS output end CNFRefutation for theBenchmark.p
% 23.53/7.86 % Elapsed time: 7.409633 seconds
% 23.53/7.86 % CPU time: 58.016293 seconds
% 23.53/7.86 % Total memory used: 336.257 MB
% 23.53/7.86 % Net memory used: 317.541 MB
%------------------------------------------------------------------------------