YES

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

(rule (sum1 n_0) (u n_0 1 0) :vars ((n_0 Int)))
(rule (u n_1 i_2 k_3) (u n_1 (+ i_2 1) (+ k_3 i_2)) :guard (<= i_2 n_1) :vars ((n_1 Int) (i_2 Int) (k_3 Int)))
(rule (u n_4 i_5 k_6) (return k_6) :guard (not (<= i_5 n_4)) :vars ((n_4 Int) (i_5 Int) (k_6 Int)))

Confluent by Orthogonality with proof:
no critical pairs

Elapsed Time:  39.35 ms