SUCCESS 2.71 (total time) COMPLETED TRS *(x, y) -> d(x, i(y)), i(i(x)) -> x, i(one()) -> one(), i(d(x, y)) -> d(y, x), d(i(x), d(y, d(x, z))) -> d(i(z), y), d(i(y), d(x, y)) -> i(x), d(one(), x) -> i(x), d(d(x, y), z) -> d(x, d(z, i(y))), d(z, d(y, d(i(z), x))) -> d(i(x), y), d(x, one()) -> x, d(x, x) -> one(), d(y, d(x, i(y))) -> i(x) STATISTICS number of inference steps: 29 total time: 2.71 orient: 0.49 rewrite: 1.84 deduce: 0.33 termination: 0.43 termination checked internally with ttt2fast termination checks: 53 (yes: 43, timeouts: 0) timelimit per check: 0.7