YES (format LCTRS :logic QF_LIA) (fun sum 2 :sort (Int Int Int)) (rule (sum n_0 m_1) 0 :guard (< n_0 m_1) :vars ((n_0 Int) (m_1 Int))) (rule (sum n_2 m_3) (+ n_2 (sum (- n_2 1) m_3)) :guard (>= n_2 m_3) :vars ((n_2 Int) (m_3 Int))) Confluent by Parallel Closedness with proof: no critical pairs Elapsed Time: 12.59 ms