SUCCESS
5.04 (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:   5.04
orient:       2.55
rewrite:      1.89
deduce:       0.53
termination:  2.36

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