YES

(format LCTRS :logic QF_LIA)
(fun return 1 :sort (Int Int))
(fun sum2 2 :sort (Int Int Int))
(fun u 4 :sort (Int Int Int Int Int))

(rule (sum2 m_0 n_1) (u m_0 n_1 m_0 0) :vars ((m_0 Int) (n_1 Int)))
(rule (u m_2 n_3 i_4 total_5) (u m_2 n_3 (+ i_4 1) (+ total_5 i_4)) :guard (<= i_4 n_3) :vars ((m_2 Int) (n_3 Int) (i_4 Int) (total_5 Int)))
(rule (u m_6 n_7 i_8 total_9) (return total_9) :guard (not (<= i_8 n_7)) :vars ((m_6 Int) (n_7 Int) (i_8 Int) (total_9 Int)))

Confluent by Orthogonality with proof:
no critical pairs

Elapsed Time:  11.52 ms