MAYBE

Problem:
 rec(rec(x)) -> sent(rec(x))
 rec(sent(x)) -> sent(rec(x))
 rec(no(x)) -> sent(rec(x))
 rec(bot()) -> up(sent(bot()))
 rec(up(x)) -> up(rec(x))
 sent(up(x)) -> up(sent(x))
 no(up(x)) -> up(no(x))
 top(rec(up(x))) -> top(check(rec(x)))
 top(sent(up(x))) -> top(check(rec(x)))
 top(no(up(x))) -> top(check(rec(x)))
 check(up(x)) -> up(check(x))
 check(sent(x)) -> sent(check(x))
 check(rec(x)) -> rec(check(x))
 check(no(x)) -> no(check(x))
 check(no(x)) -> no(x)

Proof:
 Complexity Transformation Processor:
  strict:
   rec(rec(x)) -> sent(rec(x))
   rec(sent(x)) -> sent(rec(x))
   rec(no(x)) -> sent(rec(x))
   rec(bot()) -> up(sent(bot()))
   rec(up(x)) -> up(rec(x))
   sent(up(x)) -> up(sent(x))
   no(up(x)) -> up(no(x))
   top(rec(up(x))) -> top(check(rec(x)))
   top(sent(up(x))) -> top(check(rec(x)))
   top(no(up(x))) -> top(check(rec(x)))
   check(up(x)) -> up(check(x))
   check(sent(x)) -> sent(check(x))
   check(rec(x)) -> rec(check(x))
   check(no(x)) -> no(check(x))
   check(no(x)) -> no(x)
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [check](x0) = x0 + 1,
     
     [top](x0) = x0 + 1,
     
     [up](x0) = x0,
     
     [bot] = 0,
     
     [no](x0) = x0 + 1,
     
     [sent](x0) = x0 + 1,
     
     [rec](x0) = x0
    orientation:
     rec(rec(x)) = x >= x + 1 = sent(rec(x))
     
     rec(sent(x)) = x + 1 >= x + 1 = sent(rec(x))
     
     rec(no(x)) = x + 1 >= x + 1 = sent(rec(x))
     
     rec(bot()) = 0 >= 1 = up(sent(bot()))
     
     rec(up(x)) = x >= x = up(rec(x))
     
     sent(up(x)) = x + 1 >= x + 1 = up(sent(x))
     
     no(up(x)) = x + 1 >= x + 1 = up(no(x))
     
     top(rec(up(x))) = x + 1 >= x + 2 = top(check(rec(x)))
     
     top(sent(up(x))) = x + 2 >= x + 2 = top(check(rec(x)))
     
     top(no(up(x))) = x + 2 >= x + 2 = top(check(rec(x)))
     
     check(up(x)) = x + 1 >= x + 1 = up(check(x))
     
     check(sent(x)) = x + 2 >= x + 2 = sent(check(x))
     
     check(rec(x)) = x + 1 >= x + 1 = rec(check(x))
     
     check(no(x)) = x + 2 >= x + 2 = no(check(x))
     
     check(no(x)) = x + 2 >= x + 1 = no(x)
    problem:
     strict:
      rec(rec(x)) -> sent(rec(x))
      rec(sent(x)) -> sent(rec(x))
      rec(no(x)) -> sent(rec(x))
      rec(bot()) -> up(sent(bot()))
      rec(up(x)) -> up(rec(x))
      sent(up(x)) -> up(sent(x))
      no(up(x)) -> up(no(x))
      top(rec(up(x))) -> top(check(rec(x)))
      top(sent(up(x))) -> top(check(rec(x)))
      top(no(up(x))) -> top(check(rec(x)))
      check(up(x)) -> up(check(x))
      check(sent(x)) -> sent(check(x))
      check(rec(x)) -> rec(check(x))
      check(no(x)) -> no(check(x))
     weak:
      check(no(x)) -> no(x)
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [check](x0) = x0,
       
       [top](x0) = x0,
       
       [up](x0) = x0 + 1,
       
       [bot] = 1,
       
       [no](x0) = x0,
       
       [sent](x0) = x0,
       
       [rec](x0) = x0
      orientation:
       rec(rec(x)) = x >= x = sent(rec(x))
       
       rec(sent(x)) = x >= x = sent(rec(x))
       
       rec(no(x)) = x >= x = sent(rec(x))
       
       rec(bot()) = 1 >= 2 = up(sent(bot()))
       
       rec(up(x)) = x + 1 >= x + 1 = up(rec(x))
       
       sent(up(x)) = x + 1 >= x + 1 = up(sent(x))
       
       no(up(x)) = x + 1 >= x + 1 = up(no(x))
       
       top(rec(up(x))) = x + 1 >= x = top(check(rec(x)))
       
       top(sent(up(x))) = x + 1 >= x = top(check(rec(x)))
       
       top(no(up(x))) = x + 1 >= x = top(check(rec(x)))
       
       check(up(x)) = x + 1 >= x + 1 = up(check(x))
       
       check(sent(x)) = x >= x = sent(check(x))
       
       check(rec(x)) = x >= x = rec(check(x))
       
       check(no(x)) = x >= x = no(check(x))
       
       check(no(x)) = x >= x = no(x)
      problem:
       strict:
        rec(rec(x)) -> sent(rec(x))
        rec(sent(x)) -> sent(rec(x))
        rec(no(x)) -> sent(rec(x))
        rec(bot()) -> up(sent(bot()))
        rec(up(x)) -> up(rec(x))
        sent(up(x)) -> up(sent(x))
        no(up(x)) -> up(no(x))
        check(up(x)) -> up(check(x))
        check(sent(x)) -> sent(check(x))
        check(rec(x)) -> rec(check(x))
        check(no(x)) -> no(check(x))
       weak:
        top(rec(up(x))) -> top(check(rec(x)))
        top(sent(up(x))) -> top(check(rec(x)))
        top(no(up(x))) -> top(check(rec(x)))
        check(no(x)) -> no(x)
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [check](x0) = x0,
         
         [top](x0) = x0,
         
         [up](x0) = x0,
         
         [bot] = 0,
         
         [no](x0) = x0 + 1,
         
         [sent](x0) = x0,
         
         [rec](x0) = x0
        orientation:
         rec(rec(x)) = x >= x = sent(rec(x))
         
         rec(sent(x)) = x >= x = sent(rec(x))
         
         rec(no(x)) = x + 1 >= x = sent(rec(x))
         
         rec(bot()) = 0 >= 0 = up(sent(bot()))
         
         rec(up(x)) = x >= x = up(rec(x))
         
         sent(up(x)) = x >= x = up(sent(x))
         
         no(up(x)) = x + 1 >= x + 1 = up(no(x))
         
         check(up(x)) = x >= x = up(check(x))
         
         check(sent(x)) = x >= x = sent(check(x))
         
         check(rec(x)) = x >= x = rec(check(x))
         
         check(no(x)) = x + 1 >= x + 1 = no(check(x))
         
         top(rec(up(x))) = x >= x = top(check(rec(x)))
         
         top(sent(up(x))) = x >= x = top(check(rec(x)))
         
         top(no(up(x))) = x + 1 >= x = top(check(rec(x)))
         
         check(no(x)) = x + 1 >= x + 1 = no(x)
        problem:
         strict:
          rec(rec(x)) -> sent(rec(x))
          rec(sent(x)) -> sent(rec(x))
          rec(bot()) -> up(sent(bot()))
          rec(up(x)) -> up(rec(x))
          sent(up(x)) -> up(sent(x))
          no(up(x)) -> up(no(x))
          check(up(x)) -> up(check(x))
          check(sent(x)) -> sent(check(x))
          check(rec(x)) -> rec(check(x))
          check(no(x)) -> no(check(x))
         weak:
          rec(no(x)) -> sent(rec(x))
          top(rec(up(x))) -> top(check(rec(x)))
          top(sent(up(x))) -> top(check(rec(x)))
          top(no(up(x))) -> top(check(rec(x)))
          check(no(x)) -> no(x)
        Matrix Interpretation Processor:
         dimension: 1
         max_matrix:
          1
          interpretation:
           [check](x0) = x0,
           
           [top](x0) = x0,
           
           [up](x0) = x0 + 1,
           
           [bot] = 0,
           
           [no](x0) = x0,
           
           [sent](x0) = x0,
           
           [rec](x0) = x0 + 1
          orientation:
           rec(rec(x)) = x + 2 >= x + 1 = sent(rec(x))
           
           rec(sent(x)) = x + 1 >= x + 1 = sent(rec(x))
           
           rec(bot()) = 1 >= 1 = up(sent(bot()))
           
           rec(up(x)) = x + 2 >= x + 2 = up(rec(x))
           
           sent(up(x)) = x + 1 >= x + 1 = up(sent(x))
           
           no(up(x)) = x + 1 >= x + 1 = up(no(x))
           
           check(up(x)) = x + 1 >= x + 1 = up(check(x))
           
           check(sent(x)) = x >= x = sent(check(x))
           
           check(rec(x)) = x + 1 >= x + 1 = rec(check(x))
           
           check(no(x)) = x >= x = no(check(x))
           
           rec(no(x)) = x + 1 >= x + 1 = sent(rec(x))
           
           top(rec(up(x))) = x + 2 >= x + 1 = top(check(rec(x)))
           
           top(sent(up(x))) = x + 1 >= x + 1 = top(check(rec(x)))
           
           top(no(up(x))) = x + 1 >= x + 1 = top(check(rec(x)))
           
           check(no(x)) = x >= x = no(x)
          problem:
           strict:
            rec(sent(x)) -> sent(rec(x))
            rec(bot()) -> up(sent(bot()))
            rec(up(x)) -> up(rec(x))
            sent(up(x)) -> up(sent(x))
            no(up(x)) -> up(no(x))
            check(up(x)) -> up(check(x))
            check(sent(x)) -> sent(check(x))
            check(rec(x)) -> rec(check(x))
            check(no(x)) -> no(check(x))
           weak:
            rec(rec(x)) -> sent(rec(x))
            rec(no(x)) -> sent(rec(x))
            top(rec(up(x))) -> top(check(rec(x)))
            top(sent(up(x))) -> top(check(rec(x)))
            top(no(up(x))) -> top(check(rec(x)))
            check(no(x)) -> no(x)
          Matrix Interpretation Processor:
           dimension: 2
           max_matrix:
            [1 1]
            [0 1]
            interpretation:
                             
             [check](x0) = x0,
             
                         [1 0]  
             [top](x0) = [0 0]x0,
             
                             [0]
             [up](x0) = x0 + [1],
             
                     [0]
             [bot] = [0],
             
                        [1 1]     [1]
             [no](x0) = [0 1]x0 + [0],
             
                            
             [sent](x0) = x0,
             
                              [0]
             [rec](x0) = x0 + [1]
            orientation:
                                [0]        [0]               
             rec(sent(x)) = x + [1] >= x + [1] = sent(rec(x))
             
                          [0]    [0]                  
             rec(bot()) = [1] >= [1] = up(sent(bot()))
             
                              [0]        [0]             
             rec(up(x)) = x + [2] >= x + [2] = up(rec(x))
             
                               [0]        [0]              
             sent(up(x)) = x + [1] >= x + [1] = up(sent(x))
             
                         [1 1]    [2]    [1 1]    [1]            
             no(up(x)) = [0 1]x + [1] >= [0 1]x + [1] = up(no(x))
             
                                [0]        [0]               
             check(up(x)) = x + [1] >= x + [1] = up(check(x))
             
                                                     
             check(sent(x)) = x >= x = sent(check(x))
             
                                 [0]        [0]                
             check(rec(x)) = x + [1] >= x + [1] = rec(check(x))
             
                            [1 1]    [1]    [1 1]    [1]               
             check(no(x)) = [0 1]x + [0] >= [0 1]x + [0] = no(check(x))
             
                               [0]        [0]               
             rec(rec(x)) = x + [2] >= x + [1] = sent(rec(x))
             
                          [1 1]    [1]        [0]               
             rec(no(x)) = [0 1]x + [1] >= x + [1] = sent(rec(x))
             
                               [1 0]     [1 0]                      
             top(rec(up(x))) = [0 0]x >= [0 0]x = top(check(rec(x)))
             
                                [1 0]     [1 0]                      
             top(sent(up(x))) = [0 0]x >= [0 0]x = top(check(rec(x)))
             
                              [1 1]    [2]    [1 0]                      
             top(no(up(x))) = [0 0]x + [0] >= [0 0]x = top(check(rec(x)))
             
                            [1 1]    [1]    [1 1]    [1]        
             check(no(x)) = [0 1]x + [0] >= [0 1]x + [0] = no(x)
            problem:
             strict:
              rec(sent(x)) -> sent(rec(x))
              rec(bot()) -> up(sent(bot()))
              rec(up(x)) -> up(rec(x))
              sent(up(x)) -> up(sent(x))
              check(up(x)) -> up(check(x))
              check(sent(x)) -> sent(check(x))
              check(rec(x)) -> rec(check(x))
              check(no(x)) -> no(check(x))
             weak:
              no(up(x)) -> up(no(x))
              rec(rec(x)) -> sent(rec(x))
              rec(no(x)) -> sent(rec(x))
              top(rec(up(x))) -> top(check(rec(x)))
              top(sent(up(x))) -> top(check(rec(x)))
              top(no(up(x))) -> top(check(rec(x)))
              check(no(x)) -> no(x)
            Matrix Interpretation Processor:
             dimension: 3
             max_matrix:
              [1 1 1]
              [0 1 0]
              [0 0 1]
              interpretation:
                             [1 0 1]  
               [check](x0) = [0 1 0]x0
                             [0 0 1]  ,
               
                           [1 0 0]  
               [top](x0) = [0 0 0]x0
                           [0 0 0]  ,
               
                          [1 0 1]     [0]
               [up](x0) = [0 1 0]x0 + [1]
                          [0 0 1]     [0],
               
                       [0]
               [bot] = [0]
                       [0],
               
                          [1 1 0]     [1]
               [no](x0) = [0 1 0]x0 + [0]
                          [0 0 1]     [1],
               
                              
               [sent](x0) = x0
                              ,
               
                                [0]
               [rec](x0) = x0 + [1]
                                [0]
              orientation:
                                  [0]        [0]               
               rec(sent(x)) = x + [1] >= x + [1] = sent(rec(x))
                                  [0]        [0]               
               
                            [0]    [0]                  
               rec(bot()) = [1] >= [1] = up(sent(bot()))
                            [0]    [0]                  
               
                            [1 0 1]    [0]    [1 0 1]    [0]             
               rec(up(x)) = [0 1 0]x + [2] >= [0 1 0]x + [2] = up(rec(x))
                            [0 0 1]    [0]    [0 0 1]    [0]             
               
                             [1 0 1]    [0]    [1 0 1]    [0]              
               sent(up(x)) = [0 1 0]x + [1] >= [0 1 0]x + [1] = up(sent(x))
                             [0 0 1]    [0]    [0 0 1]    [0]              
               
                              [1 0 2]    [0]    [1 0 2]    [0]               
               check(up(x)) = [0 1 0]x + [1] >= [0 1 0]x + [1] = up(check(x))
                              [0 0 1]    [0]    [0 0 1]    [0]               
               
                                [1 0 1]     [1 0 1]                  
               check(sent(x)) = [0 1 0]x >= [0 1 0]x = sent(check(x))
                                [0 0 1]     [0 0 1]                  
               
                               [1 0 1]    [0]    [1 0 1]    [0]                
               check(rec(x)) = [0 1 0]x + [1] >= [0 1 0]x + [1] = rec(check(x))
                               [0 0 1]    [0]    [0 0 1]    [0]                
               
                              [1 1 1]    [2]    [1 1 1]    [1]               
               check(no(x)) = [0 1 0]x + [0] >= [0 1 0]x + [0] = no(check(x))
                              [0 0 1]    [1]    [0 0 1]    [1]               
               
                           [1 1 1]    [2]    [1 1 1]    [2]            
               no(up(x)) = [0 1 0]x + [1] >= [0 1 0]x + [1] = up(no(x))
                           [0 0 1]    [1]    [0 0 1]    [1]            
               
                                 [0]        [0]               
               rec(rec(x)) = x + [2] >= x + [1] = sent(rec(x))
                                 [0]        [0]               
               
                            [1 1 0]    [1]        [0]               
               rec(no(x)) = [0 1 0]x + [1] >= x + [1] = sent(rec(x))
                            [0 0 1]    [1]        [0]               
               
                                 [1 0 1]     [1 0 1]                      
               top(rec(up(x))) = [0 0 0]x >= [0 0 0]x = top(check(rec(x)))
                                 [0 0 0]     [0 0 0]                      
               
                                  [1 0 1]     [1 0 1]                      
               top(sent(up(x))) = [0 0 0]x >= [0 0 0]x = top(check(rec(x)))
                                  [0 0 0]     [0 0 0]                      
               
                                [1 1 1]    [2]    [1 0 1]                      
               top(no(up(x))) = [0 0 0]x + [0] >= [0 0 0]x = top(check(rec(x)))
                                [0 0 0]    [0]    [0 0 0]                      
               
                              [1 1 1]    [2]    [1 1 0]    [1]        
               check(no(x)) = [0 1 0]x + [0] >= [0 1 0]x + [0] = no(x)
                              [0 0 1]    [1]    [0 0 1]    [1]        
              problem:
               strict:
                rec(sent(x)) -> sent(rec(x))
                rec(bot()) -> up(sent(bot()))
                rec(up(x)) -> up(rec(x))
                sent(up(x)) -> up(sent(x))
                check(up(x)) -> up(check(x))
                check(sent(x)) -> sent(check(x))
                check(rec(x)) -> rec(check(x))
               weak:
                check(no(x)) -> no(check(x))
                no(up(x)) -> up(no(x))
                rec(rec(x)) -> sent(rec(x))
                rec(no(x)) -> sent(rec(x))
                top(rec(up(x))) -> top(check(rec(x)))
                top(sent(up(x))) -> top(check(rec(x)))
                top(no(up(x))) -> top(check(rec(x)))
                check(no(x)) -> no(x)
              Open