SUCCESS
5.01 (total time)


COMPLETED TRS


              rev(x) -> reviter(x, nil()),
 reviter(.(x, y), z) -> reviter(y, .(x, z)),
   reviter(nil(), x) -> x,
 @(reviter(x, y), z) -> reviter(x, @(y, z)),
       @(.(x, y), z) -> .(x, @(y, z)),
         @(nil(), x) -> x,
       @(@(x, y), z) -> @(x, @(y, z))



STATISTICS

number of inference steps: 11

total time:   5.01
orient:       4.89
rewrite:      0.06
deduce:       0.03
termination:  4.84

external termination prover: ttt2fast
calls to termination prover: 65 (yes: 55, timeouts: 0)
timelimit per call:          1.0