MAYBE

Problem:
 +(x,0()) -> x
 +(x,s(y)) -> s(+(x,y))
 +(0(),y) -> y
 +(s(x),y) -> s(+(x,y))
 +(x,+(y,z)) -> +(+(x,y),z)
 f(g(f(x))) -> f(h(s(0()),x))
 f(g(h(x,y))) -> f(h(s(x),y))
 f(h(x,h(y,z))) -> f(h(+(x,y),z))

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