SUCCESS 85.30 (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 STATISTICS number of inference steps: 29 total time: 85.30 orient: 84.75 rewrite: 0.34 deduce: 0.18 termination: 84.70 external termination prover: aprove07 calls to termination prover: 51 (yes: 44, timeouts: 0) time limit per call: 5.0