YES (format LCTRS :logic QF_LIA) (fun return 1 :sort (Int Unit)) (fun sum2 2 :sort (Int Int Unit)) (fun u 3 :sort (Int Int Int Unit)) (fun v 3 :sort (Int Int Int Unit)) (fun w 3 :sort (Int Int Int Unit)) (rule (u m_0 n_1 sum_2) (return 0) :guard (not (<= m_0 n_1)) :vars ((m_0 Int) (n_1 Int) (sum_2 Int))) (rule (w m_3 n_4 sum_5) (v m_3 n_4 sum_5) :guard (not (> m_3 n_4)) :vars ((m_3 Int) (n_4 Int) (sum_5 Int))) (rule (w m_6 n_7 sum_8) (return sum_8) :guard (> m_6 n_7) :vars ((m_6 Int) (n_7 Int) (sum_8 Int))) (rule (v m_9 n_10 sum_11) (w (+ m_9 1) n_10 (+ sum_11 m_9)) :vars ((m_9 Int) (n_10 Int) (sum_11 Int))) (rule (u m_12 n_13 sum_14) (v m_12 n_13 sum_14) :guard (<= m_12 n_13) :vars ((m_12 Int) (n_13 Int) (sum_14 Int))) (rule (sum2 m_15 n_16) (u m_15 n_16 0) :vars ((m_15 Int) (n_16 Int))) Confluent by Parallel Closedness with proof: no critical pairs Elapsed Time: 15.04 ms