(format LCTRS :logic QF_LIA)
(fun sum 2 :sort (Int Int Int))

(rule (sum n m) 0 :guard (< n m))
(rule (sum n m) (+ n (sum (- n 1) m)) :guard (>= n m))