SUCCESS
46.03 (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:   46.03
orient:       32.53
rewrite:      11.94
deduce:       1.33
termination:  31.52

external termination prover: ttt2fast
calls to termination prover: 282 (yes: 172, timeouts: 0)
timelimit per call:          1.0