YES
exiting with thread!
(VAR a x y z )
(RULES 
        inverse(identity) -> identity
        multiply(inverse(x),x) -> identity
        multiply(x,identity) -> x
        multiply(a,multiply(inverse(a),x)) -> x
        multiply(x,inverse(x)) -> identity
        multiply(identity,x) -> x
        inverse(inverse(x)) -> x
        divide(a,x) -> multiply(a,inverse(x))
        multiply(inverse(y),multiply(y,x)) -> x
        inverse(multiply(y,x)) -> multiply(inverse(x),inverse(y))
        multiply(multiply(x,y),z) -> multiply(x,multiply(y,z))
        
)