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))
    *(s(x),y) -> +(*(x,y),y)
    +(s(x),y) -> s(+(x,y))
    div(zero(),s(y)) -> zero()
    *(zero(),x) -> zero()
    +(zero(),x) -> x
    -(zero(),x) -> zero()
    -(x,zero()) -> x
    +(x1,zero()) -> x1
    *(x1,zero()) -> zero()
    -(s(x),s(y)) -> -(x,y)
    +(x2,s(x1)) -> s(+(x1,x2))
    *(x2,s(x1)) -> +(*(x1,x2),x2)
    *(x2,+(x1,x3)) -> +(*(x1,x2)
                       ,*(x3,x2))
)