; @author Jonas Schöpf
; associative and commutative function f
(format LCTRS :smtlib 2.6)
(theory Core)

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

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