SUCCESS 27.71 (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: 77 total time: 27.71 orient: 13.67 rewrite: 12.44 deduce: 1.38 termination: 13.05 termination checked internally with ttt2fast termination checks: 282 (yes: 172, timeouts: 0) timelimit per check: 0.7