YES

(format LCTRS :logic QF_LIA)
(fun sum 2 :sort (Int Int Int))

(rule (sum x_0 y_1) 0 :guard (> x_0 y_1) :vars ((x_0 Int) (y_1 Int)))
(rule (sum x_2 y_3) (+ x_2 (sum (+ x_2 1) y_3)) :guard (<= x_2 y_3) :vars ((x_2 Int) (y_3 Int)))

Confluent by Parallel Closedness with proof:
no critical pairs

Elapsed Time:   8.64 ms