%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM479+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 : n010.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:00 PM UTC 2026
% Result : Theorem 75.88s 10.11s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM479+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n010.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:34:09 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 75.88/10.11 % Refutation found
% 75.88/10.11 % SZS status Theorem for theBenchmark: Theorem is valid
% 75.88/10.11 % SZS output start CNFRefutation for theBenchmark
% 75.88/10.11 fof(f9,axiom,(
% 75.88/10.11 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) )),
% 75.88/10.11 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 75.88/10.11 fof(f10,axiom,(
% 75.88/10.11 (! [W0,W1,W2] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1)& aNaturalNumber0(W2) )=> sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2)) ) )),
% 75.88/10.11 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 75.88/10.11 fof(f36,hypothesis,(
% 75.88/10.11 ( aNaturalNumber0(xl)& aNaturalNumber0(xm) ) ),
% 75.88/10.11 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 75.88/10.11 fof(f38,hypothesis,(
% 75.88/10.11 aNaturalNumber0(xn) ),
% 75.88/10.11 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 75.88/10.11 fof(f39,conjecture,(
% 75.88/10.11 ( ( aNaturalNumber0(sdtsldt0(xm,xl))& xm = sdtasdt0(xl,sdtsldt0(xm,xl)) )=> ( ( aNaturalNumber0(sdtsldt0(sdtasdt0(xn,xm),xl))& sdtasdt0(xn,xm) = sdtasdt0(xl,sdtsldt0(sdtasdt0(xn,xm),xl)) )=> sdtasdt0(sdtasdt0(xl,xn),sdtsldt0(xm,xl)) = sdtasdt0(xl,sdtsldt0(sdtasdt0(xn,xm),xl)) ) ) ),
% 75.88/10.11 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 75.88/10.11 fof(f40,negated_conjecture,(
% 75.88/10.11 ~(( ( aNaturalNumber0(sdtsldt0(xm,xl))& xm = sdtasdt0(xl,sdtsldt0(xm,xl)) )=> ( ( aNaturalNumber0(sdtsldt0(sdtasdt0(xn,xm),xl))& sdtasdt0(xn,xm) = sdtasdt0(xl,sdtsldt0(sdtasdt0(xn,xm),xl)) )=> sdtasdt0(sdtasdt0(xl,xn),sdtsldt0(xm,xl)) = sdtasdt0(xl,sdtsldt0(sdtasdt0(xn,xm),xl)) ) ) )),
% 75.88/10.11 inference(negated_conjecture,[status(cth)],[f39])).
% 75.88/10.11 fof(f58,plain,(
% 75.88/10.11 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|sdtasdt0(W0,W1)=sdtasdt0(W1,W0))),
% 75.88/10.11 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 75.88/10.11 fof(f59,plain,(
% 75.88/10.11 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|sdtasdt0(X0,X1)=sdtasdt0(X1,X0))),
% 75.88/10.11 inference(cnf_transformation,[status(thm)],[f58])).
% 75.88/10.11 fof(f60,plain,(
% 75.88/10.11 ![W0,W1,W2]: (((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|~aNaturalNumber0(W2))|sdtasdt0(sdtasdt0(W0,W1),W2)=sdtasdt0(W0,sdtasdt0(W1,W2)))),
% 75.88/10.11 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 75.88/10.11 fof(f61,plain,(
% 75.88/10.11 ![X0,X1,X2]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|sdtasdt0(sdtasdt0(X0,X1),X2)=sdtasdt0(X0,sdtasdt0(X1,X2)))),
% 75.88/10.11 inference(cnf_transformation,[status(thm)],[f60])).
% 75.88/10.11 fof(f142,plain,(
% 75.88/10.11 aNaturalNumber0(xl)),
% 75.88/10.11 inference(cnf_transformation,[status(thm)],[f36])).
% 75.88/10.11 fof(f143,plain,(
% 75.88/10.11 aNaturalNumber0(xm)),
% 75.88/10.11 inference(cnf_transformation,[status(thm)],[f36])).
% 75.88/10.11 fof(f149,plain,(
% 75.88/10.11 aNaturalNumber0(xn)),
% 75.88/10.11 inference(cnf_transformation,[status(thm)],[f38])).
% 75.88/10.11 fof(f150,plain,(
% 75.88/10.11 ((aNaturalNumber0(sdtsldt0(xm,xl))&xm=sdtasdt0(xl,sdtsldt0(xm,xl)))&((aNaturalNumber0(sdtsldt0(sdtasdt0(xn,xm),xl))&sdtasdt0(xn,xm)=sdtasdt0(xl,sdtsldt0(sdtasdt0(xn,xm),xl)))&~sdtasdt0(sdtasdt0(xl,xn),sdtsldt0(xm,xl))=sdtasdt0(xl,sdtsldt0(sdtasdt0(xn,xm),xl))))),
% 75.88/10.11 inference(pre_NNF_transformation,[status(thm)],[f40])).
% 75.88/10.11 fof(f151,plain,(
% 75.88/10.11 aNaturalNumber0(sdtsldt0(xm,xl))),
% 75.88/10.11 inference(cnf_transformation,[status(thm)],[f150])).
% 75.88/10.11 fof(f152,plain,(
% 75.88/10.11 xm=sdtasdt0(xl,sdtsldt0(xm,xl))),
% 75.88/10.11 inference(cnf_transformation,[status(thm)],[f150])).
% 75.88/10.11 fof(f154,plain,(
% 75.88/10.11 sdtasdt0(xn,xm)=sdtasdt0(xl,sdtsldt0(sdtasdt0(xn,xm),xl))),
% 75.88/10.11 inference(cnf_transformation,[status(thm)],[f150])).
% 75.88/10.11 fof(f155,plain,(
% 75.88/10.11 ~sdtasdt0(sdtasdt0(xl,xn),sdtsldt0(xm,xl))=sdtasdt0(xl,sdtsldt0(sdtasdt0(xn,xm),xl))),
% 75.88/10.11 inference(cnf_transformation,[status(thm)],[f150])).
% 75.88/10.11 fof(f170,plain,(
% 75.88/10.11 ~sdtasdt0(sdtasdt0(xl,xn),sdtsldt0(xm,xl))=sdtasdt0(xn,xm)),
% 75.88/10.11 inference(forward_demodulation,[status(thm)],[f154,f155])).
% 75.88/10.11 fof(f177,plain,(
% 75.88/10.11 ![X0]: (~aNaturalNumber0(X0)|sdtasdt0(X0,xn)=sdtasdt0(xn,X0))),
% 75.88/10.11 inference(resolution,[status(thm)],[f59,f149])).
% 75.88/10.11 fof(f184,plain,(
% 75.88/10.11 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|sdtasdt0(sdtasdt0(X0,xn),X1)=sdtasdt0(X0,sdtasdt0(xn,X1)))),
% 75.88/10.11 inference(resolution,[status(thm)],[f61,f149])).
% 75.88/10.11 fof(f195,plain,(
% 75.88/10.11 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|sdtasdt0(sdtasdt0(X0,X1),xn)=sdtasdt0(X0,sdtasdt0(X1,xn)))),
% 75.88/10.11 inference(resolution,[status(thm)],[f61,f149])).
% 75.88/10.11 fof(f231,plain,(
% 75.88/10.11 ![X0]: (~aNaturalNumber0(X0)|sdtasdt0(sdtasdt0(X0,sdtsldt0(xm,xl)),xn)=sdtasdt0(X0,sdtasdt0(sdtsldt0(xm,xl),xn)))),
% 76.65/10.19 inference(resolution,[status(thm)],[f195,f151])).
% 76.65/10.19 fof(f353,plain,(
% 76.65/10.19 sdtasdt0(sdtasdt0(xl,sdtsldt0(xm,xl)),xn)=sdtasdt0(xl,sdtasdt0(sdtsldt0(xm,xl),xn))),
% 76.65/10.19 inference(resolution,[status(thm)],[f231,f142])).
% 76.65/10.19 fof(f356,plain,(
% 76.65/10.19 sdtasdt0(xm,xn)=sdtasdt0(xl,sdtasdt0(sdtsldt0(xm,xl),xn))),
% 76.65/10.19 inference(forward_demodulation,[status(thm)],[f152,f353])).
% 76.65/10.19 fof(f1060,plain,(
% 76.65/10.19 sdtasdt0(xm,xn)=sdtasdt0(xn,xm)),
% 76.65/10.19 inference(resolution,[status(thm)],[f177,f143])).
% 76.65/10.19 fof(f1065,plain,(
% 76.65/10.19 sdtasdt0(sdtsldt0(xm,xl),xn)=sdtasdt0(xn,sdtsldt0(xm,xl))),
% 76.65/10.19 inference(resolution,[status(thm)],[f177,f151])).
% 76.65/10.19 fof(f1080,plain,(
% 76.65/10.19 ~sdtasdt0(sdtasdt0(xl,xn),sdtsldt0(xm,xl))=sdtasdt0(xm,xn)),
% 76.65/10.19 inference(backward_demodulation,[status(thm)],[f1060,f170])).
% 76.65/10.19 fof(f1207,plain,(
% 76.65/10.19 sdtasdt0(xm,xn)=sdtasdt0(xl,sdtasdt0(xn,sdtsldt0(xm,xl)))),
% 76.65/10.19 inference(backward_demodulation,[status(thm)],[f1065,f356])).
% 76.65/10.19 fof(f3078,plain,(
% 76.65/10.19 ![X0]: (~aNaturalNumber0(X0)|sdtasdt0(sdtasdt0(X0,xn),sdtsldt0(xm,xl))=sdtasdt0(X0,sdtasdt0(xn,sdtsldt0(xm,xl))))),
% 76.65/10.19 inference(resolution,[status(thm)],[f184,f151])).
% 76.65/10.19 fof(f3841,plain,(
% 76.65/10.19 sdtasdt0(sdtasdt0(xl,xn),sdtsldt0(xm,xl))=sdtasdt0(xl,sdtasdt0(xn,sdtsldt0(xm,xl)))),
% 76.65/10.19 inference(resolution,[status(thm)],[f3078,f142])).
% 76.65/10.19 fof(f3854,plain,(
% 76.65/10.19 sdtasdt0(sdtasdt0(xl,xn),sdtsldt0(xm,xl))=sdtasdt0(xm,xn)),
% 76.65/10.19 inference(forward_demodulation,[status(thm)],[f1207,f3841])).
% 76.65/10.19 fof(f3855,plain,(
% 76.65/10.19 $false),
% 76.65/10.19 inference(forward_subsumption_resolution,[status(thm)],[f3854,f1080])).
% 76.65/10.19 % SZS output end CNFRefutation for theBenchmark.p
% 76.65/10.21 % Elapsed time: 9.834004 seconds
% 76.65/10.21 % CPU time: 77.222574 seconds
% 76.65/10.21 % Total memory used: 441.822 MB
% 76.65/10.21 % Net memory used: 415.674 MB
%------------------------------------------------------------------------------