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