YES
(THEORY
    (AC
        p m
    )
    
)
(VAR
    x2 x3 x1 x y z
)
(RULES
    m(p(x2,x3),x1) -> p(m(x1,x2)
                       ,m(x1,x3))
    m(x2,s(x1)) -> p(m(x1,x2),x2)
    p(x2,s(x1)) -> s(p(x1,x2))
    m(zero(),x1) -> zero()
    p(zero(),x1) -> x1
    p(x,zero()) -> x
    m(x,zero()) -> zero()
    p(s(x),y) -> s(p(x,y))
    m(s(x),y) -> p(m(x,y),y)
    m(x,p(y,z)) -> p(m(x,y),m(x,z))
)