SUCCESS
246.56 (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:   246.56
termination:  233.63

external termination prover: aprove07
calls to termination prover: 101 (yes: 100, timeouts: 1)
time limit per call:         5.0