MAYBE

Problem:
 f(s(s(s(s(s(s(s(s(x)))))))),y,y) -> f(id(s(s(s(s(s(s(s(s(x))))))))),y,y)
 id(s(x)) -> s(id(x))
 id(0()) -> 0()

Proof:
 Complexity Transformation Processor:
  strict:
   f(s(s(s(s(s(s(s(s(x)))))))),y,y) -> f(id(s(s(s(s(s(s(s(s(x))))))))),y,y)
   id(s(x)) -> s(id(x))
   id(0()) -> 0()
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [0] = 1,
     
     [id](x0) = x0 + 1,
     
     [f](x0, x1, x2) = x0 + x1 + x2,
     
     [s](x0) = x0
    orientation:
     f(s(s(s(s(s(s(s(s(x)))))))),y,y) = x + 2y >= x + 2y + 1 = f(id(s(s(s(s(s(s(s(s(x))))))))),y,y)
     
     id(s(x)) = x + 1 >= x + 1 = s(id(x))
     
     id(0()) = 2 >= 1 = 0()
    problem:
     strict:
      f(s(s(s(s(s(s(s(s(x)))))))),y,y) -> f(id(s(s(s(s(s(s(s(s(x))))))))),y,y)
      id(s(x)) -> s(id(x))
     weak:
      id(0()) -> 0()
    Open