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