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