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

(sort Unit)
(fun f (-> Unit Unit Unit))

(rule (f (f x y) z) (f x (f y z)))
(rule (f x y) (f y x))