YES

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

(rule (v m_0 n_1 s_2 i_3) (return s_2) :guard (not (<= i_3 n_1)) :vars ((m_0 Int) (n_1 Int) (s_2 Int) (i_3 Int)))
(rule (v m_4 n_5 s_6 i_7) (v m_4 n_5 (+ s_6 i_7) (+ i_7 1)) :guard (<= i_7 n_5) :vars ((m_4 Int) (n_5 Int) (s_6 Int) (i_7 Int)))
(rule (u m_8 n_9 s_10 i_11) (v m_8 n_9 s_10 i_11) :guard (not (> m_8 n_9)) :vars ((m_8 Int) (n_9 Int) (s_10 Int) (i_11 Int)))
(rule (u m_12 n_13 s_14 i_15) (return 0) :guard (> m_12 n_13) :vars ((m_12 Int) (n_13 Int) (s_14 Int) (i_15 Int)))
(rule (sum2 m_16 n_17) (u m_16 n_17 0 m_16) :vars ((m_16 Int) (n_17 Int)))

Confluent by Newmans Lemma with proof:
terminating and no critical pairs

Elapsed Time:  13.22 ms