(VAR x y z)
(THEORY (AC f))
(RULES
f(x,g(y,z)) -> g(f(x,y), f(x,z))
f(x,u1(y)) -> u1(f(x,y))
f(x,u2(y)) -> u2(f(x,y))
u1(g(x,y)) -> g(u1(x), u1(y))
u2(g(x,y)) -> g(u2(x), u2(y))
u2(u1(x)) -> u1(u2(x))
)