SUCCESS
0.15 (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:   0.15
orient:       0.05
rewrite:      0.06
deduce:       0.03
termination:  0.05

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