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