MAYBE

(format LCTRS :logic QF_LIA)
(fun geq 2 :sort (Int Int Bool))
(fun plus 2 :sort (Int Int Int))
(fun sum 1 :sort (Int Int))
(fun sum2 2 :sort (Bool Int Int))

(rule (sum x_0) (sum2 (geq 0 x_0) x_0) :vars ((x_0 Int)))
(rule (sum2 true x_1) 0 :vars ((x_1 Int)))
(rule (sum2 false x_2) (plus x_2 (sum (plus x_2 (- 1)))) :vars ((x_2 Int)))
(rule (plus n_3 m_4) k_5 :guard (= (+ n_3 m_4) k_5) :vars ((n_3 Int) (m_4 Int) (k_5 Int)))
(rule (geq n_6 m_7) true :guard (>= n_6 m_7) :vars ((n_6 Int) (m_7 Int)))
(rule (geq n_8 m_9) false :guard (< n_8 m_9) :vars ((n_8 Int) (m_9 Int)))

Confluence could not be determined.

Elapsed Time:  16.77 ms