YES
(VAR x y z)
(RULES
multiply(x,inverse(x)) -> identity()
inverse(inverse(x)) -> x
multiply(inverse(x),x) -> identity()
multiply(inverse(x),multiply(x,y)) -> y
multiply(x,multiply(inverse(x),y)) -> y
multiply(multiply(x,y),z) -> multiply(x,multiply(y,z))
inverse(identity()) -> identity()
multiply(x,identity()) -> x
multiply(identity(),x) -> x
double_divide(y,x) -> multiply(inverse(y),inverse(x))
inverse(multiply(y,x)) -> multiply(inverse(x),inverse(y))
)