(meta-info (comment "Example 19 from Winkler et al. 2018"))
(format LCTRS :logic QF_LIA)

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

(rule (f x) (g x x) :guard (<= x 0))
(rule (h (f x)) (h x) :guard (>= x 0))
(rule (g (f x) y) (g x z) :guard (and (> x 0) (> z x)))
(rule (g x (+ x y)) (f y) :guard (and (> x 0) (> y 0)))