SUCCESS
13.97 (total time)


COMPLETED TRS


            h(one()) -> one(),
             i(h(x)) -> h(i(x)),
             i(i(x)) -> x,
            i(one()) -> one(),
          i(*(x, y)) -> *(i(y), i(x)),
       *(h(x), h(y)) -> h(*(x, y)),
          *(i(x), x) -> one(),
         *(one(), x) -> x,
 *(*(x, h(y)), h(z)) -> *(x, h(*(y, z))),
    *(*(x, i(y)), y) -> x,
    *(*(x, y), i(y)) -> x,
          *(x, i(x)) -> one(),
         *(x, one()) -> x,
       *(x, *(y, z)) -> *(*(x, y), z)



STATISTICS

number of inference steps: 45

total time:   13.97
orient:       11.57
rewrite:      1.81
deduce:       0.51
termination:  11.30

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