SUCCESS 913.77 (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: 94 total time: 913.77 orient: 897.17 rewrite: 13.72 deduce: 2.43 termination: 896.85 external termination prover: aprove07 calls to termination prover: 225 (yes: 153, timeouts: 0) time limit per call: 5.0