MAYBE

(format LCTRS :logic QF_LIA)
(fun proc_F 1 :sort (Int result_proc))
(fun return_proc 1 :sort (Int result_proc))
(fun u 2 :sort (Int result_proc result_proc))

(rule (u n_0 (return_proc m_1)) (return_proc (+ n_0 m_1)) :vars ((n_0 Int) (m_1 Int)))
(rule (proc_F n_2) (u n_2 (proc_F (- n_2 1))) :guard (> n_2 0) :vars ((n_2 Int)))
(rule (proc_F n_3) (return_proc n_3) :guard (<= n_3 0) :vars ((n_3 Int)))

Confluence could not be determined.

Elapsed Time:   4.83 ms