SUCCESS
1.18 (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:   1.18
orient:       0.31
rewrite:      0.60
deduce:       0.22
termination:  0.27

termination checked internally with ttt2fast
termination checks: 51 (yes: 44, timeouts: 0)
timelimit per check: 0.7