YES

(format LCTRS :logic QF_LIA)
(fun return 1 :sort (Int Unit))
(fun sum1 1 :sort (Int Unit))

(rule (sum1 n_0) (return (div (* n_0 (+ n_0 1)) 2)) :guard (not (< n_0 0)) :vars ((n_0 Int)))
(rule (sum1 n_1) (return 0) :guard (< n_1 0) :vars ((n_1 Int)))

Confluent by Weak Orthogonality with proof:
no critical pairs

Elapsed Time:   9.61 ms