(meta-info (comment "Ctrl example from examples-transformed/frocosex18.ctrs"))
(format LCTRS :logic QF_LIA)

(fun f 2 :sort (Int Int  Unit))
(fun g 1 :sort (Int  Unit))

(rule (f  x4 (+  x4 y4)) (g  y4) :guard (> x4 0))
(rule (f  x3 y3) (g  y3) :guard (< x3 y3))
(rule (f  x2 y2) (g  x2) :guard (<= x2 y2))
(rule (f  x1 y1) (g  (+  x1 y1)) :guard (>= x1 y1))