MAYBE

Problem:
 s(b(x1)) -> b(s(s(s(x1))))
 s(b(s(x1))) -> b(t(x1))
 t(b(x1)) -> b(s(x1))
 t(b(s(x1))) -> u(t(b(x1)))
 b(u(x1)) -> b(s(x1))
 t(s(x1)) -> t(t(x1))
 t(u(x1)) -> u(t(x1))
 s(u(x1)) -> s(s(x1))

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