YES

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:
 Matrix Interpretation Processor: dim=1
  
  interpretation:
   [check](x0) = x0,
   
   [top](x0) = x0,
   
   [up](x0) = x0,
   
   [bot] = 0,
   
   [no](x0) = 4x0 + 1,
   
   [sent](x0) = 2x0,
   
   [rec](x0) = 2x0
  orientation:
   rec(rec(x)) = 4x >= 4x = sent(rec(x))
   
   rec(sent(x)) = 4x >= 4x = sent(rec(x))
   
   rec(no(x)) = 8x + 2 >= 4x = sent(rec(x))
   
   rec(bot()) = 0 >= 0 = up(sent(bot()))
   
   rec(up(x)) = 2x >= 2x = up(rec(x))
   
   sent(up(x)) = 2x >= 2x = up(sent(x))
   
   no(up(x)) = 4x + 1 >= 4x + 1 = up(no(x))
   
   top(rec(up(x))) = 2x >= 2x = top(check(rec(x)))
   
   top(sent(up(x))) = 2x >= 2x = top(check(rec(x)))
   
   top(no(up(x))) = 4x + 1 >= 2x = top(check(rec(x)))
   
   check(up(x)) = x >= x = up(check(x))
   
   check(sent(x)) = 2x >= 2x = sent(check(x))
   
   check(rec(x)) = 2x >= 2x = rec(check(x))
   
   check(no(x)) = 4x + 1 >= 4x + 1 = no(check(x))
   
   check(no(x)) = 4x + 1 >= 4x + 1 = no(x)
  problem:
   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))
   top(rec(up(x))) -> top(check(rec(x)))
   top(sent(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)
  Matrix Interpretation Processor: dim=3
   
   interpretation:
                  [1 0 0]  
    [check](x0) = [0 0 0]x0
                  [0 0 1]  ,
    
                [1 0 0]  
    [top](x0) = [0 0 1]x0
                [0 0 0]  ,
    
               [1 0 1]     [0]
    [up](x0) = [0 1 0]x0 + [0]
               [0 1 0]     [1],
    
            [0]
    [bot] = [0]
            [0],
    
               [1 0 0]  
    [no](x0) = [0 0 0]x0
               [0 0 1]  ,
    
                   
    [sent](x0) = x0
                   ,
    
                [1 0 1]     [0]
    [rec](x0) = [0 1 0]x0 + [0]
                [0 1 0]     [1]
   orientation:
                  [1 1 1]    [1]    [1 0 1]    [0]               
    rec(rec(x)) = [0 1 0]x + [0] >= [0 1 0]x + [0] = sent(rec(x))
                  [0 1 0]    [1]    [0 1 0]    [1]               
    
                   [1 0 1]    [0]    [1 0 1]    [0]               
    rec(sent(x)) = [0 1 0]x + [0] >= [0 1 0]x + [0] = sent(rec(x))
                   [0 1 0]    [1]    [0 1 0]    [1]               
    
                 [0]    [0]                  
    rec(bot()) = [0] >= [0] = up(sent(bot()))
                 [1]    [1]                  
    
                 [1 1 1]    [1]    [1 1 1]    [1]             
    rec(up(x)) = [0 1 0]x + [0] >= [0 1 0]x + [0] = up(rec(x))
                 [0 1 0]    [1]    [0 1 0]    [1]             
    
                  [1 0 1]    [0]    [1 0 1]    [0]              
    sent(up(x)) = [0 1 0]x + [0] >= [0 1 0]x + [0] = up(sent(x))
                  [0 1 0]    [1]    [0 1 0]    [1]              
    
                [1 0 1]    [0]    [1 0 1]    [0]            
    no(up(x)) = [0 0 0]x + [0] >= [0 0 0]x + [0] = up(no(x))
                [0 1 0]    [1]    [0 0 0]    [1]            
    
                      [1 1 1]    [1]    [1 0 1]    [0]                     
    top(rec(up(x))) = [0 1 0]x + [1] >= [0 1 0]x + [1] = top(check(rec(x)))
                      [0 0 0]    [0]    [0 0 0]    [0]                     
    
                       [1 0 1]    [0]    [1 0 1]    [0]                     
    top(sent(up(x))) = [0 1 0]x + [1] >= [0 1 0]x + [1] = top(check(rec(x)))
                       [0 0 0]    [0]    [0 0 0]    [0]                     
    
                   [1 0 1]    [0]    [1 0 1]    [0]               
    check(up(x)) = [0 0 0]x + [0] >= [0 0 0]x + [0] = up(check(x))
                   [0 1 0]    [1]    [0 0 0]    [1]               
    
                     [1 0 0]     [1 0 0]                  
    check(sent(x)) = [0 0 0]x >= [0 0 0]x = sent(check(x))
                     [0 0 1]     [0 0 1]                  
    
                    [1 0 1]    [0]    [1 0 1]    [0]                
    check(rec(x)) = [0 0 0]x + [0] >= [0 0 0]x + [0] = rec(check(x))
                    [0 1 0]    [1]    [0 0 0]    [1]                
    
                   [1 0 0]     [1 0 0]                
    check(no(x)) = [0 0 0]x >= [0 0 0]x = no(check(x))
                   [0 0 1]     [0 0 1]                
    
                   [1 0 0]     [1 0 0]         
    check(no(x)) = [0 0 0]x >= [0 0 0]x = no(x)
                   [0 0 1]     [0 0 1]         
   problem:
    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))
    top(sent(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)
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [check](x0) = 2x0,
     
     [top](x0) = x0 + 3,
     
     [up](x0) = x0,
     
     [bot] = 0,
     
     [no](x0) = 4x0 + 1,
     
     [sent](x0) = 4x0,
     
     [rec](x0) = x0
    orientation:
     rec(sent(x)) = 4x >= 4x = sent(rec(x))
     
     rec(bot()) = 0 >= 0 = up(sent(bot()))
     
     rec(up(x)) = x >= x = up(rec(x))
     
     sent(up(x)) = 4x >= 4x = up(sent(x))
     
     no(up(x)) = 4x + 1 >= 4x + 1 = up(no(x))
     
     top(sent(up(x))) = 4x + 3 >= 2x + 3 = top(check(rec(x)))
     
     check(up(x)) = 2x >= 2x = up(check(x))
     
     check(sent(x)) = 8x >= 8x = sent(check(x))
     
     check(rec(x)) = 2x >= 2x = rec(check(x))
     
     check(no(x)) = 8x + 2 >= 8x + 1 = no(check(x))
     
     check(no(x)) = 8x + 2 >= 4x + 1 = no(x)
    problem:
     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))
     top(sent(up(x))) -> top(check(rec(x)))
     check(up(x)) -> up(check(x))
     check(sent(x)) -> sent(check(x))
     check(rec(x)) -> rec(check(x))
    DP Processor:
     DPs:
      rec#(sent(x)) -> rec#(x)
      rec#(sent(x)) -> sent#(rec(x))
      rec#(bot()) -> sent#(bot())
      rec#(up(x)) -> rec#(x)
      sent#(up(x)) -> sent#(x)
      no#(up(x)) -> no#(x)
      top#(sent(up(x))) -> rec#(x)
      top#(sent(up(x))) -> check#(rec(x))
      top#(sent(up(x))) -> top#(check(rec(x)))
      check#(up(x)) -> check#(x)
      check#(sent(x)) -> check#(x)
      check#(sent(x)) -> sent#(check(x))
      check#(rec(x)) -> check#(x)
      check#(rec(x)) -> rec#(check(x))
     TRS:
      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))
      top(sent(up(x))) -> top(check(rec(x)))
      check(up(x)) -> up(check(x))
      check(sent(x)) -> sent(check(x))
      check(rec(x)) -> rec(check(x))
     TDG Processor:
      DPs:
       rec#(sent(x)) -> rec#(x)
       rec#(sent(x)) -> sent#(rec(x))
       rec#(bot()) -> sent#(bot())
       rec#(up(x)) -> rec#(x)
       sent#(up(x)) -> sent#(x)
       no#(up(x)) -> no#(x)
       top#(sent(up(x))) -> rec#(x)
       top#(sent(up(x))) -> check#(rec(x))
       top#(sent(up(x))) -> top#(check(rec(x)))
       check#(up(x)) -> check#(x)
       check#(sent(x)) -> check#(x)
       check#(sent(x)) -> sent#(check(x))
       check#(rec(x)) -> check#(x)
       check#(rec(x)) -> rec#(check(x))
      TRS:
       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))
       top(sent(up(x))) -> top(check(rec(x)))
       check(up(x)) -> up(check(x))
       check(sent(x)) -> sent(check(x))
       check(rec(x)) -> rec(check(x))
      graph:
       check#(up(x)) -> check#(x) -> check#(rec(x)) -> rec#(check(x))
       check#(up(x)) -> check#(x) -> check#(rec(x)) -> check#(x)
       check#(up(x)) -> check#(x) -> check#(sent(x)) -> sent#(check(x))
       check#(up(x)) -> check#(x) -> check#(sent(x)) -> check#(x)
       check#(up(x)) -> check#(x) -> check#(up(x)) -> check#(x)
       check#(sent(x)) -> check#(x) -> check#(rec(x)) -> rec#(check(x))
       check#(sent(x)) -> check#(x) -> check#(rec(x)) -> check#(x)
       check#(sent(x)) -> check#(x) ->
       check#(sent(x)) -> sent#(check(x))
       check#(sent(x)) -> check#(x) -> check#(sent(x)) -> check#(x)
       check#(sent(x)) -> check#(x) -> check#(up(x)) -> check#(x)
       check#(sent(x)) -> sent#(check(x)) -> sent#(up(x)) -> sent#(x)
       check#(rec(x)) -> check#(x) -> check#(rec(x)) -> rec#(check(x))
       check#(rec(x)) -> check#(x) -> check#(rec(x)) -> check#(x)
       check#(rec(x)) -> check#(x) -> check#(sent(x)) -> sent#(check(x))
       check#(rec(x)) -> check#(x) -> check#(sent(x)) -> check#(x)
       check#(rec(x)) -> check#(x) -> check#(up(x)) -> check#(x)
       check#(rec(x)) -> rec#(check(x)) -> rec#(up(x)) -> rec#(x)
       check#(rec(x)) -> rec#(check(x)) ->
       rec#(bot()) -> sent#(bot())
       check#(rec(x)) -> rec#(check(x)) ->
       rec#(sent(x)) -> sent#(rec(x))
       check#(rec(x)) -> rec#(check(x)) ->
       rec#(sent(x)) -> rec#(x)
       top#(sent(up(x))) -> check#(rec(x)) ->
       check#(rec(x)) -> rec#(check(x))
       top#(sent(up(x))) -> check#(rec(x)) ->
       check#(rec(x)) -> check#(x)
       top#(sent(up(x))) -> check#(rec(x)) ->
       check#(sent(x)) -> sent#(check(x))
       top#(sent(up(x))) -> check#(rec(x)) ->
       check#(sent(x)) -> check#(x)
       top#(sent(up(x))) -> check#(rec(x)) ->
       check#(up(x)) -> check#(x)
       top#(sent(up(x))) -> top#(check(rec(x))) ->
       top#(sent(up(x))) -> top#(check(rec(x)))
       top#(sent(up(x))) -> top#(check(rec(x))) ->
       top#(sent(up(x))) -> check#(rec(x))
       top#(sent(up(x))) -> top#(check(rec(x))) ->
       top#(sent(up(x))) -> rec#(x)
       top#(sent(up(x))) -> rec#(x) -> rec#(up(x)) -> rec#(x)
       top#(sent(up(x))) -> rec#(x) -> rec#(bot()) -> sent#(bot())
       top#(sent(up(x))) -> rec#(x) -> rec#(sent(x)) -> sent#(rec(x))
       top#(sent(up(x))) -> rec#(x) -> rec#(sent(x)) -> rec#(x)
       no#(up(x)) -> no#(x) -> no#(up(x)) -> no#(x)
       sent#(up(x)) -> sent#(x) -> sent#(up(x)) -> sent#(x)
       rec#(up(x)) -> rec#(x) -> rec#(up(x)) -> rec#(x)
       rec#(up(x)) -> rec#(x) -> rec#(bot()) -> sent#(bot())
       rec#(up(x)) -> rec#(x) -> rec#(sent(x)) -> sent#(rec(x))
       rec#(up(x)) -> rec#(x) -> rec#(sent(x)) -> rec#(x)
       rec#(bot()) -> sent#(bot()) -> sent#(up(x)) -> sent#(x)
       rec#(sent(x)) -> sent#(rec(x)) -> sent#(up(x)) -> sent#(x)
       rec#(sent(x)) -> rec#(x) -> rec#(up(x)) -> rec#(x)
       rec#(sent(x)) -> rec#(x) -> rec#(bot()) -> sent#(bot())
       rec#(sent(x)) -> rec#(x) -> rec#(sent(x)) -> sent#(rec(x))
       rec#(sent(x)) -> rec#(x) -> rec#(sent(x)) -> rec#(x)
      SCC Processor:
       #sccs: 5
       #rules: 8
       #arcs: 44/196
       DPs:
        no#(up(x)) -> no#(x)
       TRS:
        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))
        top(sent(up(x))) -> top(check(rec(x)))
        check(up(x)) -> up(check(x))
        check(sent(x)) -> sent(check(x))
        check(rec(x)) -> rec(check(x))
       Subterm Criterion Processor:
        simple projection:
         pi(no#) = 0
        problem:
         DPs:
          
         TRS:
          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))
          top(sent(up(x))) -> top(check(rec(x)))
          check(up(x)) -> up(check(x))
          check(sent(x)) -> sent(check(x))
          check(rec(x)) -> rec(check(x))
        Qed
       
       DPs:
        top#(sent(up(x))) -> top#(check(rec(x)))
       TRS:
        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))
        top(sent(up(x))) -> top(check(rec(x)))
        check(up(x)) -> up(check(x))
        check(sent(x)) -> sent(check(x))
        check(rec(x)) -> rec(check(x))
       Usable Rule Processor:
        DPs:
         top#(sent(up(x))) -> top#(check(rec(x)))
        TRS:
         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))
        Semantic Labeling Processor:
         dimension: 2
         usable rules:
          
         interpretation:
                        [0 0]  
          [check](x0) = [0 1]x0,
          
                          [0]
          [up](x0) = x0 + [1],
          
                  [1]
          [bot] = [0],
          
                            [0]
          [sent](x0) = x0 + [1],
          
                      [1 0]     [0]
          [rec](x0) = [1 1]x0 + [1]
          labeled:
           top#
          usable (for model):
           top#
           sent
           up
           check
           rec
           bot
          argument filtering:
           pi(rec) = 0
           pi(sent) = 0
           pi(bot) = []
           pi(up) = 0
           pi(check) = 0
           pi(top#) = []
         precedence:
          top# ~ check ~ up ~ bot ~ sent ~ rec
         problem:
          DPs:
           
          TRS:
           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))
         Qed
       
       DPs:
        check#(up(x)) -> check#(x)
        check#(sent(x)) -> check#(x)
        check#(rec(x)) -> check#(x)
       TRS:
        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))
        top(sent(up(x))) -> top(check(rec(x)))
        check(up(x)) -> up(check(x))
        check(sent(x)) -> sent(check(x))
        check(rec(x)) -> rec(check(x))
       Subterm Criterion Processor:
        simple projection:
         pi(check#) = 0
        problem:
         DPs:
          
         TRS:
          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))
          top(sent(up(x))) -> top(check(rec(x)))
          check(up(x)) -> up(check(x))
          check(sent(x)) -> sent(check(x))
          check(rec(x)) -> rec(check(x))
        Qed
       
       DPs:
        rec#(sent(x)) -> rec#(x)
        rec#(up(x)) -> rec#(x)
       TRS:
        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))
        top(sent(up(x))) -> top(check(rec(x)))
        check(up(x)) -> up(check(x))
        check(sent(x)) -> sent(check(x))
        check(rec(x)) -> rec(check(x))
       Subterm Criterion Processor:
        simple projection:
         pi(rec#) = 0
        problem:
         DPs:
          
         TRS:
          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))
          top(sent(up(x))) -> top(check(rec(x)))
          check(up(x)) -> up(check(x))
          check(sent(x)) -> sent(check(x))
          check(rec(x)) -> rec(check(x))
        Qed
       
       DPs:
        sent#(up(x)) -> sent#(x)
       TRS:
        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))
        top(sent(up(x))) -> top(check(rec(x)))
        check(up(x)) -> up(check(x))
        check(sent(x)) -> sent(check(x))
        check(rec(x)) -> rec(check(x))
       Subterm Criterion Processor:
        simple projection:
         pi(sent#) = 0
        problem:
         DPs:
          
         TRS:
          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))
          top(sent(up(x))) -> top(check(rec(x)))
          check(up(x)) -> up(check(x))
          check(sent(x)) -> sent(check(x))
          check(rec(x)) -> rec(check(x))
        Qed