%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM466+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 : n011.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 273.14s 50.02s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM466+2 : 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.34 % Computer : n011.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/15.41 % CPULimit : 300
% 0.08/15.41 % WCLimit : 300
% 0.08/15.41 % DateTime : Mon Sep 21 02:33:13 UTC 2026
% 0.08/15.41 % CPUTime :
% 0.08/15.43 % Drodi V4.1.1
% 273.14/50.02 % Refutation found
% 273.14/50.02 % SZS status Theorem for theBenchmark: Theorem is valid
% 273.14/50.02 % SZS output start CNFRefutation for theBenchmark
% 273.14/50.02 fof(f5,axiom,(
% 273.14/50.02 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> aNaturalNumber0(sdtasdt0(W0,W1)) ) )),
% 273.14/50.02 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 273.14/50.02 fof(f9,axiom,(
% 273.14/50.02 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) )),
% 273.14/50.02 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 273.14/50.02 fof(f10,axiom,(
% 273.14/50.02 (! [W0,W1,W2] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1)& aNaturalNumber0(W2) )=> sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2)) ) )),
% 273.14/50.02 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 273.14/50.02 fof(f30,definition,(
% 273.14/50.02 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> ( doDivides0(W0,W1)<=> (? [W2] :( aNaturalNumber0(W2)& W1 = sdtasdt0(W0,W2) ) )) ) )),
% 273.14/50.02 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 273.14/50.02 fof(f32,hypothesis,(
% 273.14/50.02 ( aNaturalNumber0(xl)& aNaturalNumber0(xm)& aNaturalNumber0(xn) ) ),
% 273.14/50.02 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 273.14/50.02 fof(f33,conjecture,(
% 273.14/50.02 ( ( (? [W0] :( aNaturalNumber0(W0)& xm = sdtasdt0(xl,W0) ))& doDivides0(xl,xm)& (? [W0] :( aNaturalNumber0(W0)& xn = sdtasdt0(xm,W0) ))& doDivides0(xm,xn) )=> ( (? [W0] :( aNaturalNumber0(W0)& xn = sdtasdt0(xl,W0) ))| doDivides0(xl,xn) ) ) ),
% 273.14/50.02 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 273.14/50.02 fof(f34,negated_conjecture,(
% 273.14/50.02 ~(( ( (? [W0] :( aNaturalNumber0(W0)& xm = sdtasdt0(xl,W0) ))& doDivides0(xl,xm)& (? [W0] :( aNaturalNumber0(W0)& xn = sdtasdt0(xm,W0) ))& doDivides0(xm,xn) )=> ( (? [W0] :( aNaturalNumber0(W0)& xn = sdtasdt0(xl,W0) ))| doDivides0(xl,xn) ) ) )),
% 273.14/50.02 inference(negated_conjecture,[status(cth)],[f33])).
% 273.14/50.02 fof(f43,plain,(
% 273.14/50.02 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|aNaturalNumber0(sdtasdt0(W0,W1)))),
% 273.14/50.02 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 273.14/50.02 fof(f44,plain,(
% 273.14/50.02 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|aNaturalNumber0(sdtasdt0(X0,X1)))),
% 273.14/50.02 inference(cnf_transformation,[status(thm)],[f43])).
% 273.14/50.02 fof(f52,plain,(
% 273.14/50.02 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|sdtasdt0(W0,W1)=sdtasdt0(W1,W0))),
% 273.14/50.02 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 273.14/50.02 fof(f53,plain,(
% 273.14/50.02 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|sdtasdt0(X0,X1)=sdtasdt0(X1,X0))),
% 273.14/50.02 inference(cnf_transformation,[status(thm)],[f52])).
% 273.14/50.02 fof(f54,plain,(
% 273.14/50.02 ![W0,W1,W2]: (((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|~aNaturalNumber0(W2))|sdtasdt0(sdtasdt0(W0,W1),W2)=sdtasdt0(W0,sdtasdt0(W1,W2)))),
% 273.14/50.02 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 273.14/50.02 fof(f55,plain,(
% 273.14/50.02 ![X0,X1,X2]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|sdtasdt0(sdtasdt0(X0,X1),X2)=sdtasdt0(X0,sdtasdt0(X1,X2)))),
% 273.14/50.02 inference(cnf_transformation,[status(thm)],[f54])).
% 273.14/50.02 fof(f116,plain,(
% 273.14/50.02 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|(doDivides0(W0,W1)<=>(?[W2]: (aNaturalNumber0(W2)&W1=sdtasdt0(W0,W2)))))),
% 273.14/50.02 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 273.14/50.02 fof(f117,plain,(
% 273.14/50.02 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|((~doDivides0(W0,W1)|(?[W2]: (aNaturalNumber0(W2)&W1=sdtasdt0(W0,W2))))&(doDivides0(W0,W1)|(![W2]: (~aNaturalNumber0(W2)|~W1=sdtasdt0(W0,W2))))))),
% 273.14/50.02 inference(NNF_transformation,[status(thm)],[f116])).
% 273.14/50.02 fof(f118,plain,(
% 273.14/50.02 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|((~doDivides0(W0,W1)|(aNaturalNumber0(sK1_skl(W1,W0))&W1=sdtasdt0(W0,sK1_skl(W1,W0))))&(doDivides0(W0,W1)|(![W2]: (~aNaturalNumber0(W2)|~W1=sdtasdt0(W0,W2))))))),
% 273.14/50.02 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W2,sK1_skl(W1,W0))],[f117])).
% 273.14/50.02 fof(f121,plain,(
% 273.14/50.02 ![X0,X1,X2]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|doDivides0(X0,X1)|~aNaturalNumber0(X2)|~X1=sdtasdt0(X0,X2))),
% 273.14/50.02 inference(cnf_transformation,[status(thm)],[f118])).
% 273.14/50.02 fof(f128,plain,(
% 273.14/50.02 aNaturalNumber0(xl)),
% 273.14/50.02 inference(cnf_transformation,[status(thm)],[f32])).
% 273.14/50.02 fof(f131,plain,(
% 273.14/50.02 (((((?[W0]: (aNaturalNumber0(W0)&xm=sdtasdt0(xl,W0)))&doDivides0(xl,xm))&(?[W0]: (aNaturalNumber0(W0)&xn=sdtasdt0(xm,W0))))&doDivides0(xm,xn))&((![W0]: (~aNaturalNumber0(W0)|~xn=sdtasdt0(xl,W0)))&~doDivides0(xl,xn)))),
% 273.92/50.12 inference(pre_NNF_transformation,[status(thm)],[f34])).
% 273.92/50.12 fof(f132,plain,(
% 273.92/50.12 ((((aNaturalNumber0(sK2_skl)&xm=sdtasdt0(xl,sK2_skl))&doDivides0(xl,xm))&(aNaturalNumber0(sK3_skl)&xn=sdtasdt0(xm,sK3_skl)))&doDivides0(xm,xn))&((![W0]: (~aNaturalNumber0(W0)|~xn=sdtasdt0(xl,W0)))&~doDivides0(xl,xn))),
% 273.92/50.12 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl]),skolemize(W0,sK2_skl),skolemize(W0,sK3_skl)],[f131])).
% 273.92/50.12 fof(f133,plain,(
% 273.92/50.12 aNaturalNumber0(sK2_skl)),
% 273.92/50.12 inference(cnf_transformation,[status(thm)],[f132])).
% 273.92/50.12 fof(f134,plain,(
% 273.92/50.12 xm=sdtasdt0(xl,sK2_skl)),
% 273.92/50.12 inference(cnf_transformation,[status(thm)],[f132])).
% 273.92/50.12 fof(f136,plain,(
% 273.92/50.12 aNaturalNumber0(sK3_skl)),
% 273.92/50.12 inference(cnf_transformation,[status(thm)],[f132])).
% 273.92/50.12 fof(f137,plain,(
% 273.92/50.12 xn=sdtasdt0(xm,sK3_skl)),
% 273.92/50.12 inference(cnf_transformation,[status(thm)],[f132])).
% 273.92/50.12 fof(f140,plain,(
% 273.92/50.12 ~doDivides0(xl,xn)),
% 273.92/50.12 inference(cnf_transformation,[status(thm)],[f132])).
% 273.92/50.12 fof(f143,plain,(
% 273.92/50.12 ![X0]: (~aNaturalNumber0(X0)|aNaturalNumber0(sdtasdt0(sK3_skl,X0)))),
% 273.92/50.12 inference(resolution,[status(thm)],[f44,f136])).
% 273.92/50.12 fof(f145,plain,(
% 273.92/50.12 ![X0]: (~aNaturalNumber0(X0)|sdtasdt0(X0,sK3_skl)=sdtasdt0(sK3_skl,X0))),
% 273.92/50.12 inference(resolution,[status(thm)],[f53,f136])).
% 273.92/50.12 fof(f151,plain,(
% 273.92/50.12 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|sdtasdt0(sdtasdt0(X0,X1),sK3_skl)=sdtasdt0(X0,sdtasdt0(X1,sK3_skl)))),
% 273.92/50.12 inference(resolution,[status(thm)],[f55,f136])).
% 273.92/50.12 fof(f1147,plain,(
% 273.92/50.12 ![X0]: (~aNaturalNumber0(X0)|sdtasdt0(sdtasdt0(X0,sK2_skl),sK3_skl)=sdtasdt0(X0,sdtasdt0(sK2_skl,sK3_skl)))),
% 273.92/50.12 inference(resolution,[status(thm)],[f133,f151])).
% 273.92/50.12 fof(f1276,plain,(
% 273.92/50.12 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(sdtasdt0(X0,X1))|doDivides0(X0,sdtasdt0(X0,X1))|~aNaturalNumber0(X1))),
% 273.92/50.12 inference(equality_resolution,[status(thm)],[f121])).
% 273.92/50.12 fof(f1304,plain,(
% 273.92/50.12 ![X0,X1]: (~aNaturalNumber0(X0)|doDivides0(X0,sdtasdt0(X0,X1))|~aNaturalNumber0(X1))),
% 273.92/50.12 inference(forward_subsumption_resolution,[status(thm)],[f1276,f44])).
% 273.92/50.12 fof(f1969,plain,(
% 273.92/50.12 sdtasdt0(sK2_skl,sK3_skl)=sdtasdt0(sK3_skl,sK2_skl)),
% 273.92/50.12 inference(resolution,[status(thm)],[f145,f133])).
% 273.92/50.12 fof(f1975,plain,(
% 273.92/50.12 aNaturalNumber0(sdtasdt0(sK3_skl,sK2_skl))),
% 273.92/50.12 inference(resolution,[status(thm)],[f143,f133])).
% 273.92/50.12 fof(f14052,plain,(
% 273.92/50.12 ![X0]: (doDivides0(xl,sdtasdt0(xl,X0))|~aNaturalNumber0(X0))),
% 273.92/50.12 inference(resolution,[status(thm)],[f1304,f128])).
% 273.92/50.12 fof(f48960,plain,(
% 273.92/50.12 ![X0]: (~aNaturalNumber0(X0)|sdtasdt0(sdtasdt0(X0,sK2_skl),sK3_skl)=sdtasdt0(X0,sdtasdt0(sK3_skl,sK2_skl)))),
% 273.92/50.12 inference(forward_demodulation,[status(thm)],[f1969,f1147])).
% 273.92/50.12 fof(f48964,plain,(
% 273.92/50.12 sdtasdt0(sdtasdt0(xl,sK2_skl),sK3_skl)=sdtasdt0(xl,sdtasdt0(sK3_skl,sK2_skl))),
% 273.92/50.12 inference(resolution,[status(thm)],[f48960,f128])).
% 273.92/50.12 fof(f48970,plain,(
% 273.92/50.12 sdtasdt0(xm,sK3_skl)=sdtasdt0(xl,sdtasdt0(sK3_skl,sK2_skl))),
% 273.92/50.12 inference(forward_demodulation,[status(thm)],[f134,f48964])).
% 273.92/50.12 fof(f48971,plain,(
% 273.92/50.12 xn=sdtasdt0(xl,sdtasdt0(sK3_skl,sK2_skl))),
% 273.92/50.12 inference(forward_demodulation,[status(thm)],[f137,f48970])).
% 273.92/50.12 fof(f50720,plain,(
% 273.92/50.12 doDivides0(xl,sdtasdt0(xl,sdtasdt0(sK3_skl,sK2_skl)))),
% 273.92/50.12 inference(resolution,[status(thm)],[f1975,f14052])).
% 273.92/50.12 fof(f50896,plain,(
% 273.92/50.12 doDivides0(xl,xn)),
% 273.92/50.12 inference(forward_demodulation,[status(thm)],[f48971,f50720])).
% 273.92/50.12 fof(f50897,plain,(
% 273.92/50.12 $false),
% 273.92/50.12 inference(forward_subsumption_resolution,[status(thm)],[f50896,f140])).
% 273.92/50.12 % SZS output end CNFRefutation for theBenchmark.p
% 110.89/50.20 % Elapsed time: 34.763464 seconds
% 110.89/50.20 % CPU time: 274.702061 seconds
% 110.89/50.20 % Total memory used: 940.066 MB
% 110.89/50.20 % Net memory used: 877.455 MB
%------------------------------------------------------------------------------