MAYBE

Problem:
 .(1(),x) -> x
 .(x,1()) -> x
 .(i(x),x) -> 1()
 .(x,i(x)) -> 1()
 i(1()) -> 1()
 i(i(x)) -> x
 .(i(y),.(y,z)) -> z
 .(y,.(i(y),z)) -> z
 .(.(x,y),z) -> .(x,.(y,z))
 i(.(x,y)) -> .(i(y),i(x))

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