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

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