SUCCESS 6.19 (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: 6.19 orient: 3.97 rewrite: 1.85 deduce: 0.34 termination: 3.91 external termination prover: ttt2fast calls to termination prover: 53 (yes: 43, timeouts: 0) timelimit per call: 1.0