SUCCESS
51.19 (total time)


COMPLETED TRS

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



STATISTICS

number of inference steps: 14 

total time:   51.19
orient:       51.09
rewrite:      0.06
deduce:       0.04
termination:  50.97

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