SUCCESS
4.45 (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:   4.45
orient:       3.59
rewrite:      0.61
deduce:       0.22
termination:  3.54

external termination prover: ttt2fast
calls to termination prover: 51 (yes: 44, timeouts: 0)
timelimit per call:          1.0