%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM841+2 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n018.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:55 PM UTC 2026
% Result : Theorem 3.27s 0.90s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM841+2 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n018.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 03:14:43 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 3.27/0.90 % Refutation found
% 3.27/0.90 % SZS status Theorem for theBenchmark: Theorem is valid
% 3.27/0.90 % SZS output start CNFRefutation for theBenchmark
% 3.27/0.90 fof(f1,conjecture,(
% 3.27/0.90 greater(vplus(vd344,vd347),vplus(vd345,vd348)) ),
% 3.27/0.90 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.27/0.90 fof(f2,negated_conjecture,(
% 3.27/0.90 ~(greater(vplus(vd344,vd347),vplus(vd345,vd348)) )),
% 3.27/0.90 inference(negated_conjecture,[status(cth)],[f1])).
% 3.27/0.90 fof(f7,axiom,(
% 3.27/0.90 greater(vd347,vd348) ),
% 3.27/0.90 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.27/0.90 fof(f8,axiom,(
% 3.27/0.90 greater(vd344,vd345) ),
% 3.27/0.90 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.27/0.90 fof(f20,axiom,(
% 3.27/0.90 (! [Vd193,Vd194] :( greater(Vd194,Vd193)<=> (? [Vd196] : Vd194 = vplus(Vd193,Vd196) )) )),
% 3.27/0.90 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.27/0.90 fof(f22,axiom,(
% 3.27/0.90 (! [Vd78,Vd79] : vplus(Vd79,Vd78) = vplus(Vd78,Vd79) )),
% 3.27/0.90 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.27/0.90 fof(f25,axiom,(
% 3.27/0.90 (! [Vd46,Vd47,Vd48] : vplus(vplus(Vd46,Vd47),Vd48) = vplus(Vd46,vplus(Vd47,Vd48)) )),
% 3.27/0.90 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.27/0.90 fof(f28,plain,(
% 3.27/0.90 ~greater(vplus(vd344,vd347),vplus(vd345,vd348))),
% 3.27/0.90 inference(cnf_transformation,[status(thm)],[f2])).
% 3.27/0.90 fof(f33,plain,(
% 3.27/0.90 greater(vd347,vd348)),
% 3.27/0.90 inference(cnf_transformation,[status(thm)],[f7])).
% 3.27/0.90 fof(f34,plain,(
% 3.27/0.90 greater(vd344,vd345)),
% 3.27/0.90 inference(cnf_transformation,[status(thm)],[f8])).
% 3.27/0.90 fof(f60,plain,(
% 3.27/0.90 ![Vd193,Vd194]: ((~greater(Vd194,Vd193)|(?[Vd196]: Vd194=vplus(Vd193,Vd196)))&(greater(Vd194,Vd193)|(![Vd196]: ~Vd194=vplus(Vd193,Vd196))))),
% 3.27/0.90 inference(NNF_transformation,[status(thm)],[f20])).
% 3.27/0.90 fof(f61,plain,(
% 3.27/0.90 (![Vd193,Vd194]: (~greater(Vd194,Vd193)|(?[Vd196]: Vd194=vplus(Vd193,Vd196))))&(![Vd193,Vd194]: (greater(Vd194,Vd193)|(![Vd196]: ~Vd194=vplus(Vd193,Vd196))))),
% 3.27/0.90 inference(miniscoping,[status(thm)],[f60])).
% 3.27/0.90 fof(f62,plain,(
% 3.27/0.90 (![Vd193,Vd194]: (~greater(Vd194,Vd193)|Vd194=vplus(Vd193,sK0_skl(Vd194,Vd193))))&(![Vd193,Vd194]: (greater(Vd194,Vd193)|(![Vd196]: ~Vd194=vplus(Vd193,Vd196))))),
% 3.27/0.90 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(Vd196,sK0_skl(Vd194,Vd193))],[f61])).
% 3.27/0.90 fof(f63,plain,(
% 3.27/0.90 ![X0,X1]: (~greater(X0,X1)|X0=vplus(X1,sK0_skl(X0,X1)))),
% 3.27/0.90 inference(cnf_transformation,[status(thm)],[f62])).
% 3.27/0.90 fof(f64,plain,(
% 3.27/0.90 ![X0,X1,X2]: (greater(X0,X1)|~X0=vplus(X1,X2))),
% 3.27/0.90 inference(cnf_transformation,[status(thm)],[f62])).
% 3.27/0.90 fof(f67,plain,(
% 3.27/0.90 ![X0,X1]: (vplus(X0,X1)=vplus(X1,X0))),
% 3.27/0.90 inference(cnf_transformation,[status(thm)],[f22])).
% 3.27/0.90 fof(f70,plain,(
% 3.27/0.90 ![X0,X1,X2]: (vplus(vplus(X0,X1),X2)=vplus(X0,vplus(X1,X2)))),
% 3.27/0.90 inference(cnf_transformation,[status(thm)],[f25])).
% 3.27/0.90 fof(f77,plain,(
% 3.27/0.90 ~greater(vplus(vd344,vd347),vplus(vd348,vd345))),
% 3.27/0.90 inference(backward_demodulation,[status(thm)],[f67,f28])).
% 3.27/0.90 fof(f86,plain,(
% 3.27/0.90 ![X0]: (~vplus(vd344,vd347)=vplus(vplus(vd348,vd345),X0))),
% 3.27/0.90 inference(resolution,[status(thm)],[f64,f77])).
% 3.27/0.90 fof(f92,plain,(
% 3.27/0.90 ![X0,X1,X2]: (vplus(X0,vplus(X1,X2))=vplus(X1,vplus(X2,X0)))),
% 3.27/0.90 inference(paramodulation,[status(thm)],[f67,f70])).
% 3.27/0.90 fof(f224,plain,(
% 3.27/0.90 ![X0]: (~vplus(vd344,vd347)=vplus(vd348,vplus(vd345,X0)))),
% 3.27/0.90 inference(forward_demodulation,[status(thm)],[f70,f86])).
% 3.27/0.90 fof(f225,plain,(
% 3.27/0.90 ![X0]: (~vplus(vd344,vd347)=vplus(vd348,vplus(X0,vd345)))),
% 3.27/0.90 inference(paramodulation,[status(thm)],[f67,f224])).
% 3.27/0.90 fof(f227,plain,(
% 3.27/0.90 ![X0,X1]: (~vplus(vd344,vd347)=vplus(vd348,vplus(X0,vplus(X1,vd345))))),
% 3.27/0.90 inference(paramodulation,[status(thm)],[f70,f225])).
% 3.27/0.90 fof(f231,plain,(
% 3.27/0.90 ![X0,X1]: (~vplus(vd344,vd347)=vplus(vd348,vplus(vplus(X0,vd345),X1)))),
% 3.27/0.90 inference(paramodulation,[status(thm)],[f67,f227])).
% 3.27/0.90 fof(f236,plain,(
% 3.27/0.90 ![X0,X1]: (~vplus(vd344,vd347)=vplus(vd348,vplus(X0,vplus(vd345,X1))))),
% 3.27/0.90 inference(forward_demodulation,[status(thm)],[f70,f231])).
% 3.27/0.90 fof(f579,plain,(
% 3.27/0.90 vd344=vplus(vd345,sK0_skl(vd344,vd345))),
% 3.27/0.90 inference(resolution,[status(thm)],[f63,f34])).
% 3.27/0.90 fof(f580,plain,(
% 3.27/0.90 vd347=vplus(vd348,sK0_skl(vd347,vd348))),
% 3.27/0.90 inference(resolution,[status(thm)],[f63,f33])).
% 3.27/0.90 fof(f866,plain,(
% 3.27/0.90 ![X0]: (~vplus(vd344,vd347)=vplus(vd348,vplus(X0,vd344)))),
% 3.27/0.90 inference(paramodulation,[status(thm)],[f579,f236])).
% 3.27/0.90 fof(f907,plain,(
% 0.47/0.91 ![X0]: (~vplus(vd344,vd347)=vplus(vd344,vplus(vd348,X0)))),
% 0.47/0.91 inference(forward_demodulation,[status(thm)],[f92,f866])).
% 0.47/0.91 fof(f1723,plain,(
% 0.47/0.91 ~vplus(vd344,vd347)=vplus(vd344,vd347)),
% 0.47/0.91 inference(paramodulation,[status(thm)],[f580,f907])).
% 0.47/0.91 fof(f1773,plain,(
% 0.47/0.91 $false),
% 0.47/0.91 inference(trivial_equality_resolution,[status(thm)],[f1723])).
% 0.47/0.91 % SZS output end CNFRefutation for theBenchmark.p
% 0.47/0.91 % Elapsed time: 0.546474 seconds
% 0.47/0.91 % CPU time: 4.080320 seconds
% 0.47/0.91 % Total memory used: 151.988 MB
% 0.47/0.91 % Net memory used: 147.866 MB
%------------------------------------------------------------------------------