SUCCESS 0.00 (total time) COMPLETED TRS plus(x, z()) -> x, plus(x, s(y)) -> s(plus(x, y)) STATISTICS number of inference steps: 3 total time: 0.00 orient: 0.00 rewrite: 0.00 deduce: 0.00 termination: 0.00 termination checked internally with TTT2 calls to termination prover: 3 (yes: 3, timeouts: 0) time limit per call: 0.7