SUCCESS
233.19 (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:   233.19
orient:       231.61
rewrite:      0.95
deduce:       0.37
termination:  231.48

external termination prover: aprove07
calls to termination prover: 133 (yes: 113, timeouts: 0)
time limit per call:         5.0