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