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

(fun u_25 1 :sort (Int  Int))
(fun u_31 2 :sort (Int Int  Int))
(fun f2 2 :sort (Int Int  Int))
(fun u_34 1 :sort (Int  Int))

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