MAYBE

(format LCTRS)
(fun * 2 :sort (Unit Unit Unit))
(fun + 2 :sort (Unit Unit Unit))

(rule (+ x_0 y_1) (+ y_1 x_0) :vars ((x_0 Unit) (y_1 Unit)))
(rule (* (+ x_2 y_3) z_4) (+ (* x_2 z_4) (* y_3 z_4)) :vars ((x_2 Unit) (y_3 Unit) (z_4 Unit)))
(rule (* (+ y_5 x_6) z_7) (+ (* x_6 z_7) (* y_5 z_7)) :vars ((y_5 Unit) (x_6 Unit) (z_7 Unit)))

Confluence could not be determined.

Elapsed Time:  19.27 ms