SUCCESS
44.22 (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:   44.22
orient:       33.62
rewrite:      9.10
deduce:       1.22
termination:  32.89

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