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