SUCCESS 513.27 (total time) COMPLETED TRS g(x, y) -> f(x, +(x, -(y)), y), f(0(), x, y) -> x, -(-(x)) -> x, -(0()) -> 0(), -(+(x, y)) -> +(-(y), -(x)), +(-(x), x) -> 0(), +(0(), x) -> x, +(+(x, -(y)), y) -> x, +(+(x, y), -(y)) -> x, +(x, -(x)) -> 0(), +(x, 0()) -> x, +(x, +(y, z)) -> +(+(x, y), z) STATISTICS number of inference steps: 67 total time: 513.27 orient: 508.77 rewrite: 3.89 deduce: 0.73 termination: 508.14 external termination prover: aprove07 calls to termination prover: 242 (yes: 164, timeouts: 0) time limit per call: 5.0