YES
exiting with thread!
(VAR x y z )
(RULES 
        *(i(x),x) -> one
        *(*(x,y),z) -> *(x,*(y,z))
        div(x,y) -> *(x,i(y))
        *(i(x),*(x,z)) -> z
        i(one) -> one
        *(one,x) -> x
        i(i(x)) -> x
        *(x,one) -> x
        *(x,i(x)) -> one
        *(x,*(i(x),z)) -> z
        i(*(y,x)) -> *(i(x),i(y))
        
)