YES
(THEORY
    (AC
        p m
    )
    
)
(VAR
    x y x1
)
(RULES
    exp(p(x,y)) -> m(exp(x),exp(y))
    m(x,one()) -> x
    p(x,zero()) -> x
    exp(zero()) -> one()
    p(zero(),x1) -> x1
    m(one(),x1) -> x1
)