YES

(format LCTRS :logic QF_LIA)
(fun return 1 :sort (Int Unit))
(fun sum1 1 :sort (Int Unit))
(fun u 3 :sort (Int Int Int Unit))

(rule (u n_0 s_1 i_2) (return s_1) :guard (not (<= i_2 n_0)) :vars ((n_0 Int) (s_1 Int) (i_2 Int)))
(rule (u n_3 s_4 i_5) (u n_3 (+ s_4 i_5) (+ i_5 1)) :guard (<= i_5 n_3) :vars ((n_3 Int) (s_4 Int) (i_5 Int)))
(rule (sum1 n_6) (u n_6 0 0) :vars ((n_6 Int)))

Confluent by Weak Orthogonality with proof:
no critical pairs

Elapsed Time:  10.59 ms