(meta-info (comment "Ctrl example from examples-transformed/ackermann.ctrs"))
(format LCTRS :logic QF_LIA)

(fun ackermann 2 :sort (Int Int  Int))
(fun U2 4 :sort (Int Int Int Int  Int))
(fun U7 4 :sort (Int Int Int Int  Int))

(rule (ackermann  x y) (U2  x y x y))
(rule (U7  x y m n) (U7  x y (-  m 1) 1) :guard (and (<= n 0) (> m 0)))
(rule (U7  x y m n) (+  n 1) :guard (and (<= n 0) (not (> m 0))))
(rule (U7  x y m n) (U7  x y (-  m 1) (U2  m (-  n 1) m (-  n 1))) :guard (and (not (<= n 0)) (> m 0)))
(rule (U7  x y m n) (+  n 1) :guard (and (not (<= n 0)) (not (> m 0))))
(rule (U2  x y m n) 0 :guard (or (< y 0) (< x 0)))
(rule (U2  x y m n) (U7  x y m n) :guard (and (not (or (< y 0) (< x 0))) (> m 0)))
(rule (U2  x y m n) (+  n 1) :guard (and (not (or (< y 0) (< x 0))) (not (> m 0))))