SUCCESS
96.94 (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:   96.94
orient:       96.40
rewrite:      0.34
deduce:       0.16
termination:  96.15

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