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