SUCCESS
13.26 (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:   13.26
orient:       13.25
rewrite:      0.01
deduce:       0.01
termination:  13.23

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