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