YES (format LCTRS :logic QF_LIA) (fun return 1 :sort (Int Unit)) (fun sumfrom 2 :sort (Int Int Unit)) (fun tmp 2 :sort (Int Unit Unit)) (rule (tmp m_0 (return n_1)) (return (+ m_0 n_1)) :vars ((m_0 Int) (n_1 Int))) (rule (sumfrom m_2 n_3) (tmp n_3 (sumfrom m_2 (- n_3 1))) :guard (<= m_2 n_3) :vars ((m_2 Int) (n_3 Int))) (rule (sumfrom m_4 n_5) (return 0) :guard (> m_4 n_5) :vars ((m_4 Int) (n_5 Int))) Confluent by Almost Parallel Closedness with proof: no critical pairs Elapsed Time: 19.36 ms