%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM420-1.000 : 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 : n020.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:50 PM UTC 2026
% Result : Unsatisfiable 4.79s 1.22s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM420-1.000 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.55 % Computer : n020.cluster.edu
% 0.09/0.55 % Model : x86_64 x86_64
% 0.09/0.55 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.55 % Memory : 8046.5625MB
% 0.09/0.55 % OS : Linux 6.8.0-71-generic
% 0.09/0.55 % CPULimit : 300
% 0.09/0.55 % WCLimit : 300
% 0.09/0.55 % DateTime : Mon Sep 21 02:28:32 UTC 2026
% 0.09/0.55 % CPUTime :
% 0.09/0.57 % Drodi V4.1.1
% 4.79/1.22 % Refutation found
% 4.79/1.22 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 4.79/1.22 % SZS output start CNFRefutation for theBenchmark
% 4.79/1.22 fof(f6,axiom,(
% 4.79/1.22 (![X1,X2]: (plus(X1,X2) = plus(X2,X1) ))),
% 4.79/1.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.79/1.22 fof(f8,axiom,(
% 4.79/1.22 (![X1]: (plus(n0,X1) = X1 ))),
% 4.79/1.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.79/1.22 fof(f9,axiom,(
% 4.79/1.22 (![X1,X2]: (( X1 != plus(X2,X1)| X2 = n0 ) ))),
% 4.79/1.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.79/1.22 fof(f14,axiom,(
% 4.79/1.22 (![X1]: (plus(n1,plus(X1,n1)) != n1 ))),
% 4.79/1.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.79/1.22 fof(f15,axiom,(
% 4.79/1.22 (![X1,X2]: (times(X1,X2) = times(X2,X1) ))),
% 4.79/1.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.79/1.22 fof(f16,axiom,(
% 4.79/1.22 (![X1]: (plus(X1,n1) != n0 ))),
% 4.79/1.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.79/1.22 fof(f30,axiom,(
% 4.79/1.22 (![X1]: (less(n0,plus(X1,n1)) ))),
% 4.79/1.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.79/1.22 fof(f58,negated_conjecture,(
% 4.79/1.22 (![X8,X9,X22]: (( ~ less(n0,X8)| ~ less(n0,p__0)| ~ less(X8,p__0)| plus(X8,times(X9,p__0)) != plus(n0,times(X22,p__0)) ) ))),
% 4.79/1.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.79/1.22 fof(f68,negated_conjecture,(
% 4.79/1.22 ( ~ less(plus(n0,n1),p__0)| less(n0,p__0) ) ),
% 4.79/1.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.79/1.22 fof(f78,negated_conjecture,(
% 4.79/1.22 (![X7]: (( X7 != p__0| less(n1,X7) ) ))),
% 4.79/1.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.79/1.22 fof(f82,negated_conjecture,(
% 4.79/1.22 (![X10]: (( X10 = n1| times(s_1(X10),s_4(X10)) = X10 ) ))),
% 4.79/1.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.79/1.22 fof(f87,negated_conjecture,(
% 4.79/1.22 (![X10]: (( X10 = n1| s_1(X10) = p__0 ) ))),
% 4.79/1.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.79/1.22 fof(f99,plain,(
% 4.79/1.22 ![X0,X1]: (plus(X0,X1)=plus(X1,X0))),
% 4.79/1.22 inference(cnf_transformation,[status(thm)],[f6])).
% 4.79/1.22 fof(f102,plain,(
% 4.79/1.22 ![X0]: (plus(n0,X0)=X0)),
% 4.79/1.22 inference(cnf_transformation,[status(thm)],[f8])).
% 4.79/1.22 fof(f103,plain,(
% 4.79/1.22 ![X2]: ((![X1]: ~X1=plus(X2,X1))|X2=n0)),
% 4.79/1.22 inference(miniscoping,[status(thm)],[f9])).
% 4.79/1.22 fof(f104,plain,(
% 4.79/1.22 ![X0,X1]: (~X0=plus(X1,X0)|X1=n0)),
% 4.79/1.22 inference(cnf_transformation,[status(thm)],[f103])).
% 4.79/1.22 fof(f113,plain,(
% 4.79/1.22 ![X0]: (~plus(n1,plus(X0,n1))=n1)),
% 4.79/1.22 inference(cnf_transformation,[status(thm)],[f14])).
% 4.79/1.22 fof(f114,plain,(
% 4.79/1.22 ![X0,X1]: (times(X0,X1)=times(X1,X0))),
% 4.79/1.22 inference(cnf_transformation,[status(thm)],[f15])).
% 4.79/1.22 fof(f115,plain,(
% 4.79/1.22 ![X0]: (~plus(X0,n1)=n0)),
% 4.79/1.22 inference(cnf_transformation,[status(thm)],[f16])).
% 4.79/1.22 fof(f132,plain,(
% 4.79/1.22 ![X0]: (less(n0,plus(X0,n1)))),
% 4.79/1.22 inference(cnf_transformation,[status(thm)],[f30])).
% 4.79/1.22 fof(f164,plain,(
% 4.79/1.22 ![X8]: (((~less(n0,X8)|~less(n0,p__0))|~less(X8,p__0))|(![X9,X22]: ~plus(X8,times(X9,p__0))=plus(n0,times(X22,p__0))))),
% 4.79/1.22 inference(miniscoping,[status(thm)],[f58])).
% 4.79/1.22 fof(f165,plain,(
% 4.79/1.22 ![X0,X1,X2]: (~less(n0,X0)|~less(n0,p__0)|~less(X0,p__0)|~plus(X0,times(X1,p__0))=plus(n0,times(X2,p__0)))),
% 4.79/1.22 inference(cnf_transformation,[status(thm)],[f164])).
% 4.79/1.22 fof(f177,plain,(
% 4.79/1.22 ~less(plus(n0,n1),p__0)|less(n0,p__0)),
% 4.79/1.22 inference(cnf_transformation,[status(thm)],[f68])).
% 4.79/1.22 fof(f188,plain,(
% 4.79/1.22 ![X0]: (~X0=p__0|less(n1,X0))),
% 4.79/1.22 inference(cnf_transformation,[status(thm)],[f78])).
% 4.79/1.22 fof(f193,plain,(
% 4.79/1.22 ![X0]: (X0=n1|times(s_1(X0),s_4(X0))=X0)),
% 4.79/1.22 inference(cnf_transformation,[status(thm)],[f82])).
% 4.79/1.22 fof(f198,plain,(
% 4.79/1.22 ![X0]: (X0=n1|s_1(X0)=p__0)),
% 4.79/1.22 inference(cnf_transformation,[status(thm)],[f87])).
% 4.79/1.22 fof(f210,plain,(
% 4.79/1.22 ![X0,X1,X2]: (~less(n0,X0)|~less(n0,p__0)|~less(X0,p__0)|~plus(X0,times(X1,p__0))=times(X2,p__0))),
% 4.79/1.22 inference(forward_demodulation,[status(thm)],[f102,f165])).
% 4.79/1.22 fof(f211,plain,(
% 4.79/1.22 ~less(n1,p__0)|less(n0,p__0)),
% 4.79/1.22 inference(forward_demodulation,[status(thm)],[f102,f177])).
% 4.79/1.22 fof(f213,plain,(
% 4.79/1.22 less(n0,p__0)),
% 4.79/1.22 inference(backward_subsumption_resolution,[status(thm)],[f211,f214])).
% 4.79/1.22 fof(f214,plain,(
% 4.79/1.22 less(n1,p__0)),
% 4.79/1.22 inference(destructive_equality_resolution,[status(thm)],[f188])).
% 4.79/1.22 fof(f217,plain,(
% 4.79/1.22 ![X0,X1,X2]: (~less(n0,X0)|~less(X0,p__0)|~plus(X0,times(X1,p__0))=times(X2,p__0))),
% 4.79/1.22 inference(backward_subsumption_resolution,[status(thm)],[f210,f213])).
% 4.79/1.22 fof(f270,plain,(
% 4.79/1.22 ![X0]: (~plus(n1,X0)=n0)),
% 4.79/1.22 inference(paramodulation,[status(thm)],[f99,f115])).
% 4.79/1.22 fof(f382,plain,(
% 4.79/1.22 less(n0,n1)),
% 4.79/1.22 inference(paramodulation,[status(thm)],[f102,f132])).
% 4.79/1.22 fof(f495,plain,(
% 4.79/1.22 ~plus(n1,n1)=n1),
% 4.79/1.22 inference(paramodulation,[status(thm)],[f102,f113])).
% 4.79/1.22 fof(f649,plain,(
% 4.79/1.22 ![X0]: (X0=n1|times(p__0,s_4(X0))=X0|X0=n1)),
% 4.79/1.22 inference(paramodulation,[status(thm)],[f198,f193])).
% 4.79/1.22 fof(f656,plain,(
% 4.79/1.22 ![X0]: (X0=n1|times(p__0,s_4(X0))=X0)),
% 4.79/1.22 inference(duplicate_literals_removal,[status(thm)],[f649])).
% 4.79/1.22 fof(f684,plain,(
% 4.79/1.22 ![X0,X1]: (~less(n1,p__0)|~plus(n1,times(X0,p__0))=times(X1,p__0))),
% 4.79/1.22 inference(resolution,[status(thm)],[f217,f382])).
% 4.79/1.22 fof(f692,plain,(
% 4.79/1.22 ![X0,X1]: (~plus(n1,times(X0,p__0))=times(X1,p__0))),
% 4.79/1.22 inference(forward_subsumption_resolution,[status(thm)],[f684,f214])).
% 4.79/1.22 fof(f1551,plain,(
% 4.79/1.22 ![X0,X1]: (~plus(n1,times(p__0,X0))=times(X1,p__0))),
% 4.79/1.22 inference(paramodulation,[status(thm)],[f114,f692])).
% 4.79/1.22 fof(f2073,plain,(
% 4.79/1.22 ![X0,X1]: (~plus(n1,X0)=times(X1,p__0)|X0=n1)),
% 4.79/1.22 inference(paramodulation,[status(thm)],[f656,f1551])).
% 4.79/1.22 fof(f2091,plain,(
% 4.79/1.22 ![X0,X1]: (~plus(X0,n1)=times(X1,p__0)|X0=n1)),
% 4.79/1.22 inference(paramodulation,[status(thm)],[f99,f2073])).
% 4.79/1.22 fof(f2107,plain,(
% 4.79/1.22 ![X0,X1]: (~plus(X0,n1)=times(p__0,X1)|X0=n1)),
% 4.79/1.22 inference(paramodulation,[status(thm)],[f114,f2091])).
% 4.79/1.22 fof(f2111,plain,(
% 4.79/1.22 ![X0]: (X0=n1|plus(X0,n1)=n1)),
% 4.79/1.22 inference(resolution,[status(thm)],[f2107,f656])).
% 4.79/1.22 fof(f2131,plain,(
% 4.79/1.22 ![X0]: (X0=n1|X0=n0)),
% 4.79/1.22 inference(resolution,[status(thm)],[f2111,f104])).
% 4.79/1.22 fof(f2198,plain,(
% 4.79/1.22 plus(n1,n1)=n0),
% 4.79/1.22 inference(resolution,[status(thm)],[f2131,f495])).
% 4.79/1.22 fof(f2269,plain,(
% 4.79/1.22 $false),
% 4.79/1.22 inference(forward_subsumption_resolution,[status(thm)],[f2198,f270])).
% 4.79/1.22 % SZS output end CNFRefutation for theBenchmark.p
% 4.79/1.25 % Elapsed time: 0.680260 seconds
% 4.79/1.25 % CPU time: 5.138580 seconds
% 4.79/1.25 % Total memory used: 161.999 MB
% 4.79/1.25 % Net memory used: 157.334 MB
%------------------------------------------------------------------------------