SUCCESS 954.90 (total time) COMPLETED TRS g(g(x)) -> g(x), g(f(x)) -> *(x, f(x)), g(one()) -> one(), g(*(x, y)) -> g(y), *(g(x), y) -> y, *(f(g(x)), y) -> y, *(f(f(x)), y) -> *(x, y), *(f(one()), x) -> x, *(f(*(x, y)), z) -> *(f(y), *(f(x), z)), *(f(x), *(x, y)) -> y, *(f(x), x) -> g(x), *(one(), x) -> x, *(*(x, y), z) -> *(x, *(y, z)), *(x, g(x)) -> x, *(x, *(f(x), y)) -> y STATISTICS number of inference steps: 252 total time: 954.90 orient: 552.07 rewrite: 363.49 deduce: 35.99 termination: 541.97 termination checked internally with ttt2fast termination checks: 1071 (yes: 328, timeouts: 643) timelimit per check: 0.7