(VAR x y1 y2)
(THEORY (AC f))
(RULES
f(x,one) -> x
f(i(x),x) -> one
phi(one, y1) -> y1
phi(y1, phi(y2, x)) -> phi(f(y1,y2), x)
)