SUCCESS
2793.21 (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:   2793.21
orient:       2779.50
rewrite:      11.87
deduce:       2.37
termination:  2770.50

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