(format LCTRS :logic QF_LIA)

(fun f 2 :sort (Int Int Int))
(fun g 2 :sort (Int Int Int))
(fun h 1 :sort (Int Int))
(fun a 0 :sort (Int))
(fun b 0 :sort (Int))

(rule (f x y) (g a (+ y y)) :guard (and (>= y x) (= y 1)))
(rule (h (f x y)) (h (g b 2)) :guard (>= x y))
(rule a b)
(rule (g x y) (g y x))