(meta-info (comment "Ctrl example from examples-transformed/notsn.ctrs"))
(format LCTRS :logic QF_LIA)
(fun f 2 :sort (Int Int Int))

(rule (f x y) 0 :guard (or (or (>= (- x 1) y) (< (- x 1) 0)) (< y 0)))
(rule (f x y) 0 :guard (or (< x 0) (<= y 0)))
(rule (f 0 y) 0 :guard (>= y 0))
(rule (f x y) (f (- x 1) y) :guard (and (and (< (- x 1) y) (>= (- x 1) 0)) (>= y 0)))