(VAR x y)
(THEORY (AC p))
(RULES
p(x,one) -> x
p(x,x) -> x
p(T(x),x) -> T(x)
T(p(x,T(y))) -> p(T(p(x,y)),T(y))
L(p(x,T(y))) -> p(L(p(x,y)),L(y))
)