SUCCESS 31.22 (total time) COMPLETED TRS g(g(x)) -> g(x), g(f(x)) -> f(x), g(*(x, y)) -> f(y), f(g(x)) -> g(x), f(f(x)) -> f(x), f(*(x, y)) -> g(x), *(g(x), y) -> *(x, y), *(f(x), g(x)) -> x, *(f(x), x) -> f(x), *(*(z, x), y) -> *(f(x), y), *(x, g(x)) -> g(x), *(x, f(y)) -> *(x, y), *(x, *(y, z)) -> *(x, g(y)) STATISTICS number of inference steps: 92 total time: 31.22 orient: 5.53 rewrite: 22.22 deduce: 3.27 termination: 5.11 termination checked internally with ttt2fast termination checks: 220 (yes: 147, timeouts: 0) timelimit per check: 0.7