MAYBE

Problem:
 r(r(x1)) -> s(r(x1))
 r(s(x1)) -> s(r(x1))
 r(n(x1)) -> s(r(x1))
 r(b(x1)) -> u(s(b(x1)))
 r(u(x1)) -> u(r(x1))
 s(u(x1)) -> u(s(x1))
 n(u(x1)) -> u(n(x1))
 t(r(u(x1))) -> t(c(r(x1)))
 t(s(u(x1))) -> t(c(r(x1)))
 t(n(u(x1))) -> t(c(r(x1)))
 c(u(x1)) -> u(c(x1))
 c(s(x1)) -> s(c(x1))
 c(r(x1)) -> r(c(x1))
 c(n(x1)) -> n(c(x1))
 c(n(x1)) -> n(x1)

Proof:
 Complexity Transformation Processor:
  strict:
   r(r(x1)) -> s(r(x1))
   r(s(x1)) -> s(r(x1))
   r(n(x1)) -> s(r(x1))
   r(b(x1)) -> u(s(b(x1)))
   r(u(x1)) -> u(r(x1))
   s(u(x1)) -> u(s(x1))
   n(u(x1)) -> u(n(x1))
   t(r(u(x1))) -> t(c(r(x1)))
   t(s(u(x1))) -> t(c(r(x1)))
   t(n(u(x1))) -> t(c(r(x1)))
   c(u(x1)) -> u(c(x1))
   c(s(x1)) -> s(c(x1))
   c(r(x1)) -> r(c(x1))
   c(n(x1)) -> n(c(x1))
   c(n(x1)) -> n(x1)
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [c](x0) = x0 + 1,
     
     [t](x0) = x0,
     
     [u](x0) = x0 + 1,
     
     [b](x0) = x0,
     
     [n](x0) = x0 + 1,
     
     [s](x0) = x0,
     
     [r](x0) = x0
    orientation:
     r(r(x1)) = x1 >= x1 = s(r(x1))
     
     r(s(x1)) = x1 >= x1 = s(r(x1))
     
     r(n(x1)) = x1 + 1 >= x1 = s(r(x1))
     
     r(b(x1)) = x1 >= x1 + 1 = u(s(b(x1)))
     
     r(u(x1)) = x1 + 1 >= x1 + 1 = u(r(x1))
     
     s(u(x1)) = x1 + 1 >= x1 + 1 = u(s(x1))
     
     n(u(x1)) = x1 + 2 >= x1 + 2 = u(n(x1))
     
     t(r(u(x1))) = x1 + 1 >= x1 + 1 = t(c(r(x1)))
     
     t(s(u(x1))) = x1 + 1 >= x1 + 1 = t(c(r(x1)))
     
     t(n(u(x1))) = x1 + 2 >= x1 + 1 = t(c(r(x1)))
     
     c(u(x1)) = x1 + 2 >= x1 + 2 = u(c(x1))
     
     c(s(x1)) = x1 + 1 >= x1 + 1 = s(c(x1))
     
     c(r(x1)) = x1 + 1 >= x1 + 1 = r(c(x1))
     
     c(n(x1)) = x1 + 2 >= x1 + 2 = n(c(x1))
     
     c(n(x1)) = x1 + 2 >= x1 + 1 = n(x1)
    problem:
     strict:
      r(r(x1)) -> s(r(x1))
      r(s(x1)) -> s(r(x1))
      r(b(x1)) -> u(s(b(x1)))
      r(u(x1)) -> u(r(x1))
      s(u(x1)) -> u(s(x1))
      n(u(x1)) -> u(n(x1))
      t(r(u(x1))) -> t(c(r(x1)))
      t(s(u(x1))) -> t(c(r(x1)))
      c(u(x1)) -> u(c(x1))
      c(s(x1)) -> s(c(x1))
      c(r(x1)) -> r(c(x1))
      c(n(x1)) -> n(c(x1))
     weak:
      r(n(x1)) -> s(r(x1))
      t(n(u(x1))) -> t(c(r(x1)))
      c(n(x1)) -> n(x1)
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [c](x0) = x0,
       
       [t](x0) = x0 + 1,
       
       [u](x0) = x0 + 1,
       
       [b](x0) = x0,
       
       [n](x0) = x0,
       
       [s](x0) = x0,
       
       [r](x0) = x0 + 1
      orientation:
       r(r(x1)) = x1 + 2 >= x1 + 1 = s(r(x1))
       
       r(s(x1)) = x1 + 1 >= x1 + 1 = s(r(x1))
       
       r(b(x1)) = x1 + 1 >= x1 + 1 = u(s(b(x1)))
       
       r(u(x1)) = x1 + 2 >= x1 + 2 = u(r(x1))
       
       s(u(x1)) = x1 + 1 >= x1 + 1 = u(s(x1))
       
       n(u(x1)) = x1 + 1 >= x1 + 1 = u(n(x1))
       
       t(r(u(x1))) = x1 + 3 >= x1 + 2 = t(c(r(x1)))
       
       t(s(u(x1))) = x1 + 2 >= x1 + 2 = t(c(r(x1)))
       
       c(u(x1)) = x1 + 1 >= x1 + 1 = u(c(x1))
       
       c(s(x1)) = x1 >= x1 = s(c(x1))
       
       c(r(x1)) = x1 + 1 >= x1 + 1 = r(c(x1))
       
       c(n(x1)) = x1 >= x1 = n(c(x1))
       
       r(n(x1)) = x1 + 1 >= x1 + 1 = s(r(x1))
       
       t(n(u(x1))) = x1 + 2 >= x1 + 2 = t(c(r(x1)))
       
       c(n(x1)) = x1 >= x1 = n(x1)
      problem:
       strict:
        r(s(x1)) -> s(r(x1))
        r(b(x1)) -> u(s(b(x1)))
        r(u(x1)) -> u(r(x1))
        s(u(x1)) -> u(s(x1))
        n(u(x1)) -> u(n(x1))
        t(s(u(x1))) -> t(c(r(x1)))
        c(u(x1)) -> u(c(x1))
        c(s(x1)) -> s(c(x1))
        c(r(x1)) -> r(c(x1))
        c(n(x1)) -> n(c(x1))
       weak:
        r(r(x1)) -> s(r(x1))
        t(r(u(x1))) -> t(c(r(x1)))
        r(n(x1)) -> s(r(x1))
        t(n(u(x1))) -> t(c(r(x1)))
        c(n(x1)) -> n(x1)
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [c](x0) = x0,
         
         [t](x0) = x0,
         
         [u](x0) = x0 + 1,
         
         [b](x0) = x0 + 1,
         
         [n](x0) = x0,
         
         [s](x0) = x0,
         
         [r](x0) = x0
        orientation:
         r(s(x1)) = x1 >= x1 = s(r(x1))
         
         r(b(x1)) = x1 + 1 >= x1 + 2 = u(s(b(x1)))
         
         r(u(x1)) = x1 + 1 >= x1 + 1 = u(r(x1))
         
         s(u(x1)) = x1 + 1 >= x1 + 1 = u(s(x1))
         
         n(u(x1)) = x1 + 1 >= x1 + 1 = u(n(x1))
         
         t(s(u(x1))) = x1 + 1 >= x1 = t(c(r(x1)))
         
         c(u(x1)) = x1 + 1 >= x1 + 1 = u(c(x1))
         
         c(s(x1)) = x1 >= x1 = s(c(x1))
         
         c(r(x1)) = x1 >= x1 = r(c(x1))
         
         c(n(x1)) = x1 >= x1 = n(c(x1))
         
         r(r(x1)) = x1 >= x1 = s(r(x1))
         
         t(r(u(x1))) = x1 + 1 >= x1 = t(c(r(x1)))
         
         r(n(x1)) = x1 >= x1 = s(r(x1))
         
         t(n(u(x1))) = x1 + 1 >= x1 = t(c(r(x1)))
         
         c(n(x1)) = x1 >= x1 = n(x1)
        problem:
         strict:
          r(s(x1)) -> s(r(x1))
          r(b(x1)) -> u(s(b(x1)))
          r(u(x1)) -> u(r(x1))
          s(u(x1)) -> u(s(x1))
          n(u(x1)) -> u(n(x1))
          c(u(x1)) -> u(c(x1))
          c(s(x1)) -> s(c(x1))
          c(r(x1)) -> r(c(x1))
          c(n(x1)) -> n(c(x1))
         weak:
          t(s(u(x1))) -> t(c(r(x1)))
          r(r(x1)) -> s(r(x1))
          t(r(u(x1))) -> t(c(r(x1)))
          r(n(x1)) -> s(r(x1))
          t(n(u(x1))) -> t(c(r(x1)))
          c(n(x1)) -> n(x1)
        Matrix Interpretation Processor:
         dimension: 2
         max_matrix:
          [1 1]
          [0 1]
          interpretation:
                       
           [c](x0) = x0,
           
                     [1 0]     [1]
           [t](x0) = [0 0]x0 + [0],
           
                          [0]
           [u](x0) = x0 + [1],
           
                     [1 0]     [1]
           [b](x0) = [0 0]x0 + [0],
           
                     [1 1]     [0]
           [n](x0) = [0 1]x0 + [1],
           
                       
           [s](x0) = x0,
           
                          [0]
           [r](x0) = x0 + [1]
          orientation:
                           [0]         [0]           
           r(s(x1)) = x1 + [1] >= x1 + [1] = s(r(x1))
           
                      [1 0]     [1]    [1 0]     [1]              
           r(b(x1)) = [0 0]x1 + [1] >= [0 0]x1 + [1] = u(s(b(x1)))
           
                           [0]         [0]           
           r(u(x1)) = x1 + [2] >= x1 + [2] = u(r(x1))
           
                           [0]         [0]           
           s(u(x1)) = x1 + [1] >= x1 + [1] = u(s(x1))
           
                      [1 1]     [1]    [1 1]     [0]           
           n(u(x1)) = [0 1]x1 + [2] >= [0 1]x1 + [2] = u(n(x1))
           
                           [0]         [0]           
           c(u(x1)) = x1 + [1] >= x1 + [1] = u(c(x1))
           
                                         
           c(s(x1)) = x1 >= x1 = s(c(x1))
           
                           [0]         [0]           
           c(r(x1)) = x1 + [1] >= x1 + [1] = r(c(x1))
           
                      [1 1]     [0]    [1 1]     [0]           
           c(n(x1)) = [0 1]x1 + [1] >= [0 1]x1 + [1] = n(c(x1))
           
                         [1 0]     [1]    [1 0]     [1]              
           t(s(u(x1))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = t(c(r(x1)))
           
                           [0]         [0]           
           r(r(x1)) = x1 + [2] >= x1 + [1] = s(r(x1))
           
                         [1 0]     [1]    [1 0]     [1]              
           t(r(u(x1))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = t(c(r(x1)))
           
                      [1 1]     [0]         [0]           
           r(n(x1)) = [0 1]x1 + [2] >= x1 + [1] = s(r(x1))
           
                         [1 1]     [2]    [1 0]     [1]              
           t(n(u(x1))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = t(c(r(x1)))
           
                      [1 1]     [0]    [1 1]     [0]        
           c(n(x1)) = [0 1]x1 + [1] >= [0 1]x1 + [1] = n(x1)
          problem:
           strict:
            r(s(x1)) -> s(r(x1))
            r(b(x1)) -> u(s(b(x1)))
            r(u(x1)) -> u(r(x1))
            s(u(x1)) -> u(s(x1))
            c(u(x1)) -> u(c(x1))
            c(s(x1)) -> s(c(x1))
            c(r(x1)) -> r(c(x1))
            c(n(x1)) -> n(c(x1))
           weak:
            n(u(x1)) -> u(n(x1))
            t(s(u(x1))) -> t(c(r(x1)))
            r(r(x1)) -> s(r(x1))
            t(r(u(x1))) -> t(c(r(x1)))
            r(n(x1)) -> s(r(x1))
            t(n(u(x1))) -> t(c(r(x1)))
            c(n(x1)) -> n(x1)
          Matrix Interpretation Processor:
           dimension: 3
           max_matrix:
            [1 1 1]
            [0 1 1]
            [0 0 1]
            interpretation:
                       [1 0 1]  
             [c](x0) = [0 1 0]x0
                       [0 0 1]  ,
             
                       [1 0 1]     [0]
             [t](x0) = [0 0 0]x0 + [1]
                       [0 0 1]     [0],
             
                       [1 0 1]     [0]
             [u](x0) = [0 1 0]x0 + [1]
                       [0 0 1]     [0],
             
                       [1 0 0]  
             [b](x0) = [0 0 1]x0
                       [0 0 0]  ,
             
                       [1 1 0]     [0]
             [n](x0) = [0 1 0]x0 + [0]
                       [0 0 1]     [1],
             
                         
             [s](x0) = x0
                         ,
             
                            [0]
             [r](x0) = x0 + [1]
                            [0]
            orientation:
                             [0]         [0]           
             r(s(x1)) = x1 + [1] >= x1 + [1] = s(r(x1))
                             [0]         [0]           
             
                        [1 0 0]     [0]    [1 0 0]     [0]              
             r(b(x1)) = [0 0 1]x1 + [1] >= [0 0 1]x1 + [1] = u(s(b(x1)))
                        [0 0 0]     [0]    [0 0 0]     [0]              
             
                        [1 0 1]     [0]    [1 0 1]     [0]           
             r(u(x1)) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = u(r(x1))
                        [0 0 1]     [0]    [0 0 1]     [0]           
             
                        [1 0 1]     [0]    [1 0 1]     [0]           
             s(u(x1)) = [0 1 0]x1 + [1] >= [0 1 0]x1 + [1] = u(s(x1))
                        [0 0 1]     [0]    [0 0 1]     [0]           
             
                        [1 0 2]     [0]    [1 0 2]     [0]           
             c(u(x1)) = [0 1 0]x1 + [1] >= [0 1 0]x1 + [1] = u(c(x1))
                        [0 0 1]     [0]    [0 0 1]     [0]           
             
                        [1 0 1]      [1 0 1]             
             c(s(x1)) = [0 1 0]x1 >= [0 1 0]x1 = s(c(x1))
                        [0 0 1]      [0 0 1]             
             
                        [1 0 1]     [0]    [1 0 1]     [0]           
             c(r(x1)) = [0 1 0]x1 + [1] >= [0 1 0]x1 + [1] = r(c(x1))
                        [0 0 1]     [0]    [0 0 1]     [0]           
             
                        [1 1 1]     [1]    [1 1 1]     [0]           
             c(n(x1)) = [0 1 0]x1 + [0] >= [0 1 0]x1 + [0] = n(c(x1))
                        [0 0 1]     [1]    [0 0 1]     [1]           
             
                        [1 1 1]     [1]    [1 1 1]     [1]           
             n(u(x1)) = [0 1 0]x1 + [1] >= [0 1 0]x1 + [1] = u(n(x1))
                        [0 0 1]     [1]    [0 0 1]     [1]           
             
                           [1 0 2]     [0]    [1 0 2]     [0]              
             t(s(u(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = t(c(r(x1)))
                           [0 0 1]     [0]    [0 0 1]     [0]              
             
                             [0]         [0]           
             r(r(x1)) = x1 + [2] >= x1 + [1] = s(r(x1))
                             [0]         [0]           
             
                           [1 0 2]     [0]    [1 0 2]     [0]              
             t(r(u(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = t(c(r(x1)))
                           [0 0 1]     [0]    [0 0 1]     [0]              
             
                        [1 1 0]     [0]         [0]           
             r(n(x1)) = [0 1 0]x1 + [1] >= x1 + [1] = s(r(x1))
                        [0 0 1]     [1]         [0]           
             
                           [1 1 2]     [2]    [1 0 2]     [0]              
             t(n(u(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = t(c(r(x1)))
                           [0 0 1]     [1]    [0 0 1]     [0]              
             
                        [1 1 1]     [1]    [1 1 0]     [0]        
             c(n(x1)) = [0 1 0]x1 + [0] >= [0 1 0]x1 + [0] = n(x1)
                        [0 0 1]     [1]    [0 0 1]     [1]        
            problem:
             strict:
              r(s(x1)) -> s(r(x1))
              r(b(x1)) -> u(s(b(x1)))
              r(u(x1)) -> u(r(x1))
              s(u(x1)) -> u(s(x1))
              c(u(x1)) -> u(c(x1))
              c(s(x1)) -> s(c(x1))
              c(r(x1)) -> r(c(x1))
             weak:
              c(n(x1)) -> n(c(x1))
              n(u(x1)) -> u(n(x1))
              t(s(u(x1))) -> t(c(r(x1)))
              r(r(x1)) -> s(r(x1))
              t(r(u(x1))) -> t(c(r(x1)))
              r(n(x1)) -> s(r(x1))
              t(n(u(x1))) -> t(c(r(x1)))
              c(n(x1)) -> n(x1)
            Open