; @author Jonas Schöpf
; Ctrl example from examples/llreve/llreve_rec_ackermanna.ctrs
(format LCTRS :smtlib 2.6)
(theory Ints)

(fun u_25 (-> Int  Int))
(fun u_31 (-> Int Int  Int))
(fun f2 (-> Int Int  Int))
(fun u_34 (-> Int  Int))

(rule (u_34  w_10) w_10 :var ((w_10 Int)))
(rule (u_31  m w_9) (u_34  (f2  (-  m 1) w_9)) :var ((w_9 Int) (m Int)))
(rule (u_25  w_8) w_8 :var ((w_8 Int)))
(rule (f2  m n) (u_31  m (f2  m (-  n 1))) :guard (and (or (<= m 0) (distinct n 0)) (distinct m 0)) :var ((n Int) (m Int)))
(rule (f2  m n) (+  n 1) :guard (and (or (<= m 0) (distinct n 0)) (= m 0)) :var ((n Int) (m Int)))
(rule (f2  m n) (u_25  (f2  (-  m 1) 1)) :guard (and (> m 0) (= n 0)) :var ((n Int) (m Int)))