(meta-info (comment "Ctrl example from examples-transformed/nat_ackermann.ctrs"))
(format LCTRS :logic QF_LIA)
(fun ack 2 :sort (Unit Unit Unit))
(fun s 1 :sort (Unit Unit))
(fun O 0 :sort (Unit))

(rule (ack (s m) (s n)) (ack m (ack (s m) n)))
(rule (ack (s m) O) (ack m (s O)))
(rule (ack O n) (s n))