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