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

(sort Unit)
(fun + (-> Unit Unit Unit))
(fun * (-> Unit Unit Unit))

(rule (+ x y) (+ y x))
(rule (* (+ x y) z) (+ (* x z) (* y z)))
(rule (* (+ y x) z) (+ (* x z) (* y z)))