YES

(format LCTRS :logic QF_LIA)
(fun sum 1 :sort (Int Int))
(fun test 1 :sort (Int Unit))

(rule (test x_0) (test y_1) :guard (and (> x_0 0) (= x_0 (+ y_1 1))) :vars ((x_0 Int) (y_1 Int)))
(rule (sum x_2) (+ x_2 (sum (- x_2 1))) :guard (< 0 x_2) :vars ((x_2 Int)))
(rule (sum 0) 0)
(rule (sum x_3) 0 :guard (< x_3 0) :vars ((x_3 Int)))

Confluent by Parallel Closedness with proof:
* CriticalPair
  Left rule: (test x_0_L) -> (test y_1_L) [(and (> x_0_L 0) (= x_0_L (+ y_1_L 1)))]
  Right rule: (test x_0_R) -> (test y_1_R) [(and (> x_0_R 0) (= x_0_R (+ y_1_R 1)))]
  Critical pair: (test y_1_L) ≈ (test y_1_R) [(and (and (> x_0_R 0) (= x_0_R (+ y_1_L 1))) (and (> x_0_R 0) (= x_0_R (+ y_1_R 1))))]
 which reaches the trivial constrained equation
  (≈ (test y_1_L) (test y_1_R)) [(and (and (> x_0_R 0) (= x_0_R (+ y_1_L 1))) (and (> x_0_R 0) (= x_0_R (+ y_1_R 1))))]


Elapsed Time:  19.59 ms