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

(sort Unit)
(fun f (-> Int Unit  Unit))
(fun d Unit)
(fun a Unit)
(fun c Unit)
(fun b Unit)

(rule d d)
(rule (f x b) c :guard (<= x 10) :var ((x Int)))
(rule a b)
(rule (f x a) c :guard (<= x 3) :var ((x Int)))