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