(VAR )
(THEORY (AC + *))
(RULES
        +(a,*(b,c)) -> +(b,f(*(a,c)))
        *(a,+(b,c)) -> *(b,f(+(a,c)))
)