SUCCESS
25.97 (total time)


COMPLETED TRS

 
          g(x, y) -> f(x, *(x, i(y))),
        f(1(), x) -> x,
          i(i(x)) -> x,
           i(1()) -> 1(),
       i(*(x, y)) -> *(i(y), i(x)),
       *(i(x), x) -> 1(),
        *(1(), x) -> x,
 *(*(x, i(y)), y) -> x,
 *(*(x, y), i(y)) -> x,
       *(x, i(x)) -> 1(),
        *(x, 1()) -> x,
    *(x, *(y, z)) -> *(*(x, y), z)



STATISTICS

number of inference steps: 75 

total time:   25.97
orient:       15.13
rewrite:      9.38
deduce:       1.23
termination:  14.47

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