SUCCESS 175.47 (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: 175.47 orient: 152.70 rewrite: 18.77 deduce: 2.85 termination: 143.87 termination checked internally with ttt2fast termination checks: 1072 (yes: 917, timeouts: 19) timelimit per check: 0.7