YES (format LCTRS :logic QF_LIA) (fun return 1 :sort (Int Unit)) (fun sum2 2 :sort (Int Int Unit)) (fun u 4 :sort (Int Int Int Int Unit)) (fun v 4 :sort (Int Int Int Int Unit)) (rule (v m_0 n_1 s_2 i_3) (return s_2) :guard (not (<= i_3 n_1)) :vars ((m_0 Int) (n_1 Int) (s_2 Int) (i_3 Int))) (rule (v m_4 n_5 s_6 i_7) (v m_4 n_5 (+ s_6 i_7) (+ i_7 1)) :guard (<= i_7 n_5) :vars ((m_4 Int) (n_5 Int) (s_6 Int) (i_7 Int))) (rule (u m_8 n_9 s_10 i_11) (v m_8 n_9 s_10 i_11) :guard (not (> m_8 n_9)) :vars ((m_8 Int) (n_9 Int) (s_10 Int) (i_11 Int))) (rule (u m_12 n_13 s_14 i_15) (return 0) :guard (> m_12 n_13) :vars ((m_12 Int) (n_13 Int) (s_14 Int) (i_15 Int))) (rule (sum2 m_16 n_17) (u m_16 n_17 0 m_16) :vars ((m_16 Int) (n_17 Int))) Confluent by Parallel Closedness with proof: no critical pairs Elapsed Time: 15.87 ms