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