YES

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

(rule (u m_0 n_1 sum_2) (return 0) :guard (not (<= m_0 n_1)) :vars ((m_0 Int) (n_1 Int) (sum_2 Int)))
(rule (w m_3 n_4 sum_5) (v m_3 n_4 sum_5) :guard (not (> m_3 n_4)) :vars ((m_3 Int) (n_4 Int) (sum_5 Int)))
(rule (w m_6 n_7 sum_8) (return sum_8) :guard (> m_6 n_7) :vars ((m_6 Int) (n_7 Int) (sum_8 Int)))
(rule (v m_9 n_10 sum_11) (w (+ m_9 1) n_10 (+ sum_11 m_9)) :vars ((m_9 Int) (n_10 Int) (sum_11 Int)))
(rule (u m_12 n_13 sum_14) (v m_12 n_13 sum_14) :guard (<= m_12 n_13) :vars ((m_12 Int) (n_13 Int) (sum_14 Int)))
(rule (sum2 m_15 n_16) (u m_15 n_16 0) :vars ((m_15 Int) (n_16 Int)))

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

Elapsed Time:  13.96 ms