; @author Jonas Schöpf
; Ctrl example from examples/llreve/llreve_rec_mccarthy91a.ctrs
(format LCTRS :smtlib 2.6)
(theory Ints)
(fun u_18 (-> Int Int))
(fun u_15 (-> Int Int))
(fun f2 (-> Int Int))

(rule (u_18 w_6) w_6 :var ((w_6 Int)))
(rule (u_15 w_5) (u_18 (f2 w_5)) :var ((w_5 Int)))
(rule (f2 x) (- x 10) :guard (>= x 101) :var ((x Int)))
(rule (f2 x) (u_15 (f2 (+ 11 x))) :guard (< x 101) :var ((x Int)))