(meta-info (comment "Ctrl example from examples-transformed/vidal1.ctrs"))
(format LCTRS :logic QF_LIA)
(fun fun7 2 :sort (Int Int Unit))
(fun fun1 2 :sort (Int Int Unit))
(fun fun6 2 :sort (Int Int Unit))
(fun fun5 2 :sort (Int Int Unit))
(fun fun4 2 :sort (Int Int Unit))
(fun fun3 2 :sort (Int Int Unit))
(fun fun2 3 :sort (Int Int Int Unit))
(fun fun8 2 :sort (Int Int Unit))

(rule (fun7 x y) (fun1 x y))
(rule (fun6 x y) (fun7 x (- y 1)))
(rule (fun5 x y) (fun7 x y))
(rule (fun4 x y) (fun5 x input))
(rule (fun3 x y) (fun4 (- x 1) y))
(rule (fun2 x y i) (fun6 x y) :guard (not (= i 1)))
(rule (fun2 x y i) (fun3 x y) :guard (= i 1))
(rule (fun1 x y) (fun8 x y) :guard (and (<= x 0) (<= y 0)))
(rule (fun1 x y) (fun2 x y input) :guard (and (> x 0) (> y 0)))