MAYBE

(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)))

Confluence could not be determined.

Elapsed Time:   5.52 ms