(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))

(rule (f x y) (g x (+ 1 1)))
(rule (f x y) (h (g y (+ 1 1))))