YES

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

(rule (sum1 n_0 m_1) (u n_0 m_1 0) :vars ((n_0 Int) (m_1 Int)))
(rule (u x_2 i_3 z_4) (u x_2 (+ i_3 1) (+ z_4 i_3)) :guard (<= i_3 x_2) :vars ((x_2 Int) (i_3 Int) (z_4 Int)))
(rule (u x_5 i_6 z_7) z_7 :guard (not (<= i_6 x_5)) :vars ((x_5 Int) (i_6 Int) (z_7 Int)))

Confluent by Weak Orthogonality with proof:
no critical pairs

Elapsed Time:  10.56 ms