; @author Jonas Schöpf
; @author Fabian Mitterwallner
; @author Aart Middeldorp
; @doi 10.48550/arXiv.2402.13552
; Example 6
(format LCTRS :smtlib 2.6)

(theory Ints)

(fun f (-> Int Int Int))
(fun g (-> Int Int Int))
(fun c (-> Int Int Int))
(fun h (-> Int Int))

(rule (f x y) (h (g y (* 2 2))) :guard (and (<= x y) (= y 2)))
(rule (f x y) (c 4 x) :guard (<= y x))
(rule (g x y) (g y x))
(rule (c x y) (g 4 2) :guard (not (= x y)))
(rule (h x) x)