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

(theory Ints)

(fun f (-> Int Int Int))
(fun g (-> Int Int))
(fun a Int)
(fun b Int)

(rule (f (g x) y) (f b y))
(rule (g x) a)
(rule (f a x) x)
(rule (f b x) x)