%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM469+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 : n003.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 28.53s 4.04s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM469+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.34 % Computer : n003.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Mon Sep 21 02:34:15 UTC 2026
% 0.07/0.34 % CPUTime :
% 0.07/0.35 % Drodi V4.1.1
% 28.53/4.04 % Refutation found
% 28.53/4.04 % SZS status Theorem for theBenchmark: Theorem is valid
% 28.53/4.04 % SZS output start CNFRefutation for theBenchmark
% 28.53/4.04 fof(f2,axiom,(
% 28.53/4.04 aNaturalNumber0(sz00) ),
% 28.53/4.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.53/4.04 fof(f4,axiom,(
% 28.53/4.04 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> aNaturalNumber0(sdtpldt0(W0,W1)) ) )),
% 28.53/4.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.53/4.04 fof(f8,axiom,(
% 28.53/4.04 (! [W0] :( aNaturalNumber0(W0)=> ( sdtpldt0(W0,sz00) = W0& W0 = sdtpldt0(sz00,W0) ) ) )),
% 28.53/4.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.53/4.04 fof(f12,axiom,(
% 28.53/4.04 (! [W0] :( aNaturalNumber0(W0)=> ( sdtasdt0(W0,sz00) = sz00& sz00 = sdtasdt0(sz00,W0) ) ) )),
% 28.53/4.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.53/4.04 fof(f34,hypothesis,(
% 28.53/4.04 ( (? [W0] :( aNaturalNumber0(W0)& xm = sdtasdt0(xl,W0) ))& doDivides0(xl,xm)& (? [W0] :( aNaturalNumber0(W0)& xn = sdtasdt0(xl,W0) ))& doDivides0(xl,xn) ) ),
% 28.53/4.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.53/4.04 fof(f35,hypothesis,(
% 28.53/4.04 ( xl != sz00=> ( aNaturalNumber0(sdtsldt0(xm,xl))& xm = sdtasdt0(xl,sdtsldt0(xm,xl))& aNaturalNumber0(sdtsldt0(xn,xl))& xn = sdtasdt0(xl,sdtsldt0(xn,xl))& sdtpldt0(xm,xn) = sdtasdt0(xl,sdtpldt0(sdtsldt0(xm,xl),sdtsldt0(xn,xl))) ) ) ),
% 28.53/4.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.53/4.04 fof(f36,conjecture,(
% 28.53/4.04 ( (? [W0] :( aNaturalNumber0(W0)& sdtpldt0(xm,xn) = sdtasdt0(xl,W0) ))| doDivides0(xl,sdtpldt0(xm,xn)) ) ),
% 28.53/4.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.53/4.04 fof(f37,negated_conjecture,(
% 28.53/4.04 ~(( (? [W0] :( aNaturalNumber0(W0)& sdtpldt0(xm,xn) = sdtasdt0(xl,W0) ))| doDivides0(xl,sdtpldt0(xm,xn)) ) )),
% 28.53/4.04 inference(negated_conjecture,[status(cth)],[f36])).
% 28.53/4.04 fof(f41,plain,(
% 28.53/4.04 aNaturalNumber0(sz00)),
% 28.53/4.04 inference(cnf_transformation,[status(thm)],[f2])).
% 28.53/4.04 fof(f44,plain,(
% 28.53/4.04 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|aNaturalNumber0(sdtpldt0(W0,W1)))),
% 28.53/4.04 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 28.53/4.04 fof(f45,plain,(
% 28.53/4.04 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|aNaturalNumber0(sdtpldt0(X0,X1)))),
% 28.53/4.04 inference(cnf_transformation,[status(thm)],[f44])).
% 28.53/4.04 fof(f52,plain,(
% 28.53/4.04 ![W0]: (~aNaturalNumber0(W0)|(sdtpldt0(W0,sz00)=W0&W0=sdtpldt0(sz00,W0)))),
% 28.53/4.04 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 28.53/4.04 fof(f53,plain,(
% 28.53/4.04 ![X0]: (~aNaturalNumber0(X0)|sdtpldt0(X0,sz00)=X0)),
% 28.53/4.04 inference(cnf_transformation,[status(thm)],[f52])).
% 28.53/4.04 fof(f62,plain,(
% 28.53/4.04 ![W0]: (~aNaturalNumber0(W0)|(sdtasdt0(W0,sz00)=sz00&sz00=sdtasdt0(sz00,W0)))),
% 28.53/4.04 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 28.53/4.04 fof(f64,plain,(
% 28.53/4.04 ![X0]: (~aNaturalNumber0(X0)|sz00=sdtasdt0(sz00,X0))),
% 28.53/4.04 inference(cnf_transformation,[status(thm)],[f62])).
% 28.53/4.04 fof(f136,plain,(
% 28.53/4.04 (((aNaturalNumber0(sK2_skl)&xm=sdtasdt0(xl,sK2_skl))&doDivides0(xl,xm))&(aNaturalNumber0(sK3_skl)&xn=sdtasdt0(xl,sK3_skl)))&doDivides0(xl,xn)),
% 28.53/4.04 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl]),skolemize(W0,sK2_skl),skolemize(W0,sK3_skl)],[f34])).
% 28.53/4.04 fof(f137,plain,(
% 28.53/4.04 aNaturalNumber0(sK2_skl)),
% 28.53/4.04 inference(cnf_transformation,[status(thm)],[f136])).
% 28.53/4.04 fof(f138,plain,(
% 28.53/4.04 xm=sdtasdt0(xl,sK2_skl)),
% 28.53/4.04 inference(cnf_transformation,[status(thm)],[f136])).
% 28.53/4.04 fof(f140,plain,(
% 28.53/4.04 aNaturalNumber0(sK3_skl)),
% 28.53/4.04 inference(cnf_transformation,[status(thm)],[f136])).
% 28.53/4.04 fof(f141,plain,(
% 28.53/4.04 xn=sdtasdt0(xl,sK3_skl)),
% 28.53/4.04 inference(cnf_transformation,[status(thm)],[f136])).
% 28.53/4.04 fof(f142,plain,(
% 28.53/4.04 doDivides0(xl,xn)),
% 28.53/4.04 inference(cnf_transformation,[status(thm)],[f136])).
% 28.53/4.04 fof(f143,plain,(
% 28.53/4.04 xl=sz00|((((aNaturalNumber0(sdtsldt0(xm,xl))&xm=sdtasdt0(xl,sdtsldt0(xm,xl)))&aNaturalNumber0(sdtsldt0(xn,xl)))&xn=sdtasdt0(xl,sdtsldt0(xn,xl)))&sdtpldt0(xm,xn)=sdtasdt0(xl,sdtpldt0(sdtsldt0(xm,xl),sdtsldt0(xn,xl))))),
% 28.53/4.04 inference(pre_NNF_transformation,[status(thm)],[f35])).
% 28.53/4.04 fof(f144,plain,(
% 28.53/4.04 xl=sz00|aNaturalNumber0(sdtsldt0(xm,xl))),
% 28.53/4.04 inference(cnf_transformation,[status(thm)],[f143])).
% 28.53/4.04 fof(f146,plain,(
% 28.53/4.04 xl=sz00|aNaturalNumber0(sdtsldt0(xn,xl))),
% 28.53/4.04 inference(cnf_transformation,[status(thm)],[f143])).
% 28.53/4.04 fof(f148,plain,(
% 28.53/4.04 xl=sz00|sdtpldt0(xm,xn)=sdtasdt0(xl,sdtpldt0(sdtsldt0(xm,xl),sdtsldt0(xn,xl)))),
% 28.53/4.08 inference(cnf_transformation,[status(thm)],[f143])).
% 28.53/4.08 fof(f149,plain,(
% 28.53/4.08 ((![W0]: (~aNaturalNumber0(W0)|~sdtpldt0(xm,xn)=sdtasdt0(xl,W0)))&~doDivides0(xl,sdtpldt0(xm,xn)))),
% 28.53/4.08 inference(pre_NNF_transformation,[status(thm)],[f37])).
% 28.53/4.08 fof(f150,plain,(
% 28.53/4.08 ![X0]: (~aNaturalNumber0(X0)|~sdtpldt0(xm,xn)=sdtasdt0(xl,X0))),
% 28.53/4.08 inference(cnf_transformation,[status(thm)],[f149])).
% 28.53/4.08 fof(f151,plain,(
% 28.53/4.08 ~doDivides0(xl,sdtpldt0(xm,xn))),
% 28.53/4.08 inference(cnf_transformation,[status(thm)],[f149])).
% 28.53/4.08 fof(f256,plain,(
% 28.53/4.08 sdtpldt0(sz00,sz00)=sz00),
% 28.53/4.08 inference(resolution,[status(thm)],[f53,f41])).
% 28.53/4.08 fof(f284,plain,(
% 28.53/4.08 ![X0]: (xl=sz00|~aNaturalNumber0(X0)|aNaturalNumber0(sdtpldt0(sdtsldt0(xm,xl),X0)))),
% 28.53/4.08 inference(resolution,[status(thm)],[f144,f45])).
% 28.53/4.08 fof(f1440,plain,(
% 28.53/4.08 xl=sz00|xl=sz00|aNaturalNumber0(sdtpldt0(sdtsldt0(xm,xl),sdtsldt0(xn,xl)))),
% 28.53/4.08 inference(resolution,[status(thm)],[f146,f284])).
% 28.53/4.08 fof(f1458,plain,(
% 28.53/4.08 xl=sz00|aNaturalNumber0(sdtpldt0(sdtsldt0(xm,xl),sdtsldt0(xn,xl)))),
% 28.53/4.08 inference(duplicate_literals_removal,[status(thm)],[f1440])).
% 28.53/4.08 fof(f7830,plain,(
% 28.53/4.08 xl=sz00|~aNaturalNumber0(sdtpldt0(sdtsldt0(xm,xl),sdtsldt0(xn,xl)))),
% 28.53/4.08 inference(resolution,[status(thm)],[f148,f150])).
% 28.53/4.08 fof(f7838,plain,(
% 28.53/4.08 xl=sz00),
% 28.53/4.08 inference(forward_subsumption_resolution,[status(thm)],[f7830,f1458])).
% 28.53/4.08 fof(f9390,plain,(
% 28.53/4.08 xn=sdtasdt0(sz00,sK3_skl)),
% 28.53/4.08 inference(backward_demodulation,[status(thm)],[f7838,f141])).
% 28.53/4.08 fof(f9391,plain,(
% 28.53/4.08 xm=sdtasdt0(sz00,sK2_skl)),
% 28.53/4.08 inference(backward_demodulation,[status(thm)],[f7838,f138])).
% 28.53/4.08 fof(f9469,plain,(
% 28.53/4.08 doDivides0(sz00,xn)),
% 28.53/4.08 inference(backward_demodulation,[status(thm)],[f7838,f142])).
% 28.53/4.08 fof(f9473,plain,(
% 28.53/4.08 ~doDivides0(sz00,sdtpldt0(xm,xn))),
% 28.53/4.08 inference(backward_demodulation,[status(thm)],[f7838,f151])).
% 28.53/4.08 fof(f9745,plain,(
% 28.53/4.08 sz00=sdtasdt0(sz00,sK3_skl)),
% 28.53/4.08 inference(resolution,[status(thm)],[f64,f140])).
% 28.53/4.08 fof(f9746,plain,(
% 28.53/4.08 sz00=sdtasdt0(sz00,sK2_skl)),
% 28.53/4.08 inference(resolution,[status(thm)],[f64,f137])).
% 28.53/4.08 fof(f11315,plain,(
% 28.53/4.08 xn=sz00),
% 28.53/4.08 inference(backward_demodulation,[status(thm)],[f9745,f9390])).
% 28.53/4.08 fof(f11343,plain,(
% 28.53/4.08 doDivides0(sz00,sz00)),
% 28.53/4.08 inference(backward_demodulation,[status(thm)],[f11315,f9469])).
% 28.53/4.08 fof(f11427,plain,(
% 28.53/4.08 xm=sz00),
% 28.53/4.08 inference(backward_demodulation,[status(thm)],[f9746,f9391])).
% 28.53/4.08 fof(f13516,plain,(
% 28.53/4.08 ~doDivides0(sz00,sdtpldt0(sz00,xn))),
% 28.53/4.08 inference(forward_demodulation,[status(thm)],[f11427,f9473])).
% 28.53/4.08 fof(f13517,plain,(
% 28.53/4.08 ~doDivides0(sz00,sdtpldt0(sz00,sz00))),
% 28.53/4.08 inference(forward_demodulation,[status(thm)],[f11315,f13516])).
% 28.53/4.08 fof(f13518,plain,(
% 28.53/4.08 ~doDivides0(sz00,sz00)),
% 28.53/4.08 inference(forward_demodulation,[status(thm)],[f256,f13517])).
% 28.53/4.08 fof(f13519,plain,(
% 28.53/4.08 $false),
% 28.53/4.08 inference(forward_subsumption_resolution,[status(thm)],[f13518,f11343])).
% 28.53/4.08 % SZS output end CNFRefutation for theBenchmark.p
% 9.89/4.11 % Elapsed time: 3.752225 seconds
% 9.89/4.11 % CPU time: 29.203612 seconds
% 9.89/4.11 % Total memory used: 245.242 MB
% 9.89/4.11 % Net memory used: 235.057 MB
%------------------------------------------------------------------------------