SUCCESS
218.96 (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:   218.96
orient:       217.70
rewrite:      0.96
deduce:       0.26
termination:  216.86

external termination prover: aprove07
calls to termination prover: 135 (yes: 115, timeouts: 0)
time limit per call:         5.0