(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))
f(x,u3(y)) -> u3(f(x,y))
u1(g(x,y)) -> g(u1(x), u1(y))
u2(g(x,y)) -> g(u2(x), u2(y))
u3(g(x,y)) -> g(u3(x), u3(y))
u2(u1(x)) -> u1(u2(x))
u3(u1(x)) -> u1(u3(x))
u3(u2(x)) -> u2(u3(x))
)