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

(fun f1 2 :sort (Int Int  Int))
(fun u_14 1 :sort (Int  Int))
(fun u_11 2 :sort (Int Int  Int))
(fun u_7 1 :sort (Int  Int))
(fun u_34 1 :sort (Int  Int))

(rule (u_14  w_5) w_5 :vars ((w_5 Int)))
(rule (u_11  m w_4) (u_14  (f1  (-  m 1) w_4)) :vars ((m Int) (w_4 Int)))
(rule (u_7  w_3) w_3 :vars ((w_3 Int)))
(rule (f1  m n) (u_11  m (f1  m (-  n 1))) :guard (and (distinct m 0) (or (<= m 0) (distinct n 0))) :vars ((m Int) (n Int)))
(rule (f1  m n) (u_7  (f1  (-  m 1) 1)) :guard (and (and (distinct m 0) (> m 0)) (= n 0)) :vars ((m Int) (n Int)))
(rule (f1  m n) (+  n 1) :guard (= m 0) :vars ((m Int) (n Int)))