; @author Jonas Schöpf
; @doi 10.1007/978-3-319-43144-4_18
; Example 4
(format LCTRS :smtlib 2.6)
(theory Core)

(sort Unit)
(fun f (-> Unit Unit Unit Unit Unit))
(fun a Unit)
(fun b Unit)
(fun c Unit)
(fun d Unit)

(rule (f a a b b) (f c c c c))
(rule a b)
(rule a c)
(rule b a)
(rule b c)