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