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