SUCCESS 665.29 (total time) COMPLETED TRS g(one()) -> one(), f(one()) -> one(), i(g(x2)) -> g(i(x2)), i(f(x2)) -> f(i(x2)), i(i(x2)) -> x2, i(one()) -> one(), i(*(x0, y0)) -> *(i(y0), i(x0)), *(g(y0), f(x0)) -> *(f(x0), g(y0)), *(g(y0), *(f(x0), z1)) -> *(f(x0), *(g(y0), z1)), *(g(x0), g(y0)) -> g(*(x0, y0)), *(g(x0), *(g(y0), z1)) -> *(g(*(x0, y0)), z1), *(f(x0), f(y0)) -> f(*(x0, y0)), *(f(x0), *(f(y0), z1)) -> *(f(*(x0, y0)), z1), *(i(x0), *(x0, z1)) -> z1, *(i(x0), x0) -> one(), *(one(), x0) -> x0, *(*(x0, y0), z0) -> *(x0, *(y0, z0)), *(x2, i(x2)) -> one(), *(x2, *(i(x2), z1)) -> z1, *(x0, one()) -> x0 STATISTICS total time: 665.29 termination: 241.48 external termination prover: ttt2fast calls to termination prover: 1384 (yes: 49, timeouts: 0) timelimit per call: 1.0