SUCCESS
12.64 (total time)


COMPLETED TRS

 
       f(x0, f(y0, z0)) -> f(f(x0, y0), z0),
             f(x0, e()) -> x0,
           f(x0, i(x0)) -> e(),
    f(f(x1, x0), i(x0)) -> x1,
 f(f(x1, h(x0)), h(y0)) -> f(x1, h(f(x0, y0))),
    f(f(x3, i(x0)), x0) -> x3,
             f(e(), x0) -> x0,
           f(i(x2), x2) -> e(),
        f(h(x0), h(y0)) -> h(f(x0, y0)),
           i(f(y0, z0)) -> f(i(z0), i(y0)),
                 i(e()) -> e(),
               i(i(x2)) -> x2,
               i(h(x2)) -> h(i(x2)),
                 h(e()) -> e()



STATISTICS

total time:   12.64
termination:  4.89

external termination prover: ttt2fast
calls to termination prover: 105 (yes: 104, timeouts: 0)
time limit per call:         1.0