YES

(format LCTRS :logic QF_LIA)
(fun sum 2 :sort (Int Int Int))

(rule (sum n_0 m_1) 0 :guard (< n_0 m_1) :vars ((n_0 Int) (m_1 Int)))
(rule (sum n_2 m_3) (+ n_2 (sum (- n_2 1) m_3)) :guard (>= n_2 m_3) :vars ((n_2 Int) (m_3 Int)))

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

Elapsed Time:  11.70 ms