YES

(format LCTRS :logic QF_LIA)
(fun f 1 :sort (Int Int))

(rule (f x_0) (f (- 0 x_0)) :guard (> x_0 0) :vars ((x_0 Int)))

Confluent by Newmans Lemma with proof:
terminating and no critical pairs

Elapsed Time:   9.90 ms