SUCCESS 112.73 (total time) COMPLETED TRS inverse(inverse(x)) -> x inverse(multiply(x, y)) -> divide(inverse(y), x) inverse(identity) -> identity inverse(divide(x, y)) -> divide(y, x) multiply(inverse(x), x) -> identity multiply(identity, x) -> x multiply(divide(x, y), y) -> x multiply(x, inverse(y)) -> divide(x, y) multiply(x, multiply(y, z)) -> multiply(multiply(x, y), z) multiply(x, identity) -> x multiply(x, divide(y, z)) -> divide(multiply(x, y), z) divide(multiply(x, y), y) -> x divide(identity, x) -> inverse(x) divide(x, inverse(y)) -> multiply(x, y) divide(x, multiply(z, y)) -> divide(divide(x, y), z) divide(x, identity) -> x divide(x, divide(z, y)) -> divide(multiply(x, y), z) divide(x, x) -> identity