SUCCESS
246.64 (total time)


COMPLETED TRS


            g(one()) -> one(),
            f(one()) -> one(),
             i(g(x)) -> g(i(x)),
             i(f(x)) -> f(i(x)),
             i(i(x)) -> x,
            i(one()) -> one(),
          i(*(x, y)) -> *(i(y), i(x)),
       *(g(x), g(y)) -> g(*(x, y)),
       *(f(y), g(x)) -> *(g(x), f(y)),
       *(f(x), f(y)) -> f(*(x, y)),
          *(i(x), x) -> one(),
         *(one(), x) -> x,
 *(*(x, g(y)), g(z)) -> *(x, g(*(y, z))),
 *(*(x, f(z)), g(y)) -> *(*(x, g(y)), f(z)),
 *(*(x, f(y)), f(z)) -> *(x, f(*(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: 77

total time:   246.64
orient:       218.09
rewrite:      19.25
deduce:       2.89
termination:  209.64

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