SUCCESS
0.59 (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: 35 

total time:   0.59
orient:       0.12
rewrite:      0.32
deduce:       0.14
termination:  0.11

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