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