(meta-info (comment "Ctrl example from confluence/cr.ctrs"))
(format LCTRS :logic QF_LIA)

(fun f 2 :sort (Int Unit  Unit))
(fun d 0 :sort ( Unit))
(fun a 0 :sort ( Unit))
(fun c 0 :sort ( Unit))
(fun b 0 :sort ( Unit))

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