(meta-info (comment "Ctrl example from confluence/orthogonality_example.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) :vars ((x4 Int) (y4 Int)))
(rule (f  x3 y3) (g  y3) :guard (< x3 y3) :vars ((x3 Int) (y3 Int)))
(rule (f  x2 y2) (g  x2) :guard (<= x2 y2) :vars ((x2 Int) (y2 Int)))
(rule (f  x1 y1) (g  (+  x1 y1)) :guard (>= x1 y1) :vars ((x1 Int) (y1 Int)))