SUCCESS 2.23 (total time) COMPLETED TRS div(x, y) -> *(x, i(y)) i(i(x)) -> x i(one) -> one i(*(x, y)) -> *(i(y), i(x)) *(i(x), *(x, y)) -> y *(i(x), x) -> one *(one, x) -> x *(*(x, y), z) -> *(x, *(y, z)) *(x, i(x)) -> one *(x, one) -> x *(x, *(i(x), y)) -> y