SUCCESS 0.33 (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.33 orient: 0.32 rewrite: 0.00 deduce: 0.01 termination: 0.30 external termination prover: ttt2fast calls to termination prover: 10 (yes: 10, timeouts: 0) time limit per call: 1.0