SUCCESS
1.91 (total time)


COMPLETED TRS

 
    f(x, f(i(x), y)) -> y,
           f(x, e()) -> x,
          f(x, i(x)) -> e(),
       f(f(x, y), z) -> f(x, f(y, z)),
           f(e(), x) -> x,
          f(i(x), x) -> e(),
    f(i(x), f(x, y)) -> y,
 f(h(x), f(h(y), z)) -> f(h(f(x, y)), z),
       f(h(x), h(y)) -> h(f(x, y)),
          i(f(x, y)) -> f(i(y), i(x)),
              i(e()) -> e(),
             i(i(x)) -> x,
             i(h(x)) -> h(i(x)),
              h(e()) -> e()



STATISTICS

number of inference steps: 45 

total time:   1.91
orient:       0.74
rewrite:      0.89
deduce:       0.25
termination:  0.68

termination checked internally with TTT2
calls to termination prover: 133 (yes: 109, timeouts: 0)
time limit per call:         0.7