SUCCESS
0.02 (total time)


COMPLETED TRS

 
 a(s(x), s(y)) -> a(x, a(s(x), y)),
  a(s(x), z()) -> a(x, s(z())),
     a(z(), x) -> s(x)



STATISTICS

number of inference steps: 5 

total time:   0.02
orient:       0.01
rewrite:      0.00
deduce:       0.01
termination:  0.01

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