; @author Jonas Schöpf
; Ctrl example from examples/nat_ackermann.ctrs
(format LCTRS :smtlib 2.6)
(theory Ints)
(sort Unit)
(fun ack (-> Unit Unit Unit))
(fun s (-> Unit Unit))
(fun O 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))