YES

Problem:
 a__U11(tt(),M,N) -> a__U12(tt(),M,N)
 a__U12(tt(),M,N) -> s(a__plus(mark(N),mark(M)))
 a__plus(N,0()) -> mark(N)
 a__plus(N,s(M)) -> a__U11(tt(),M,N)
 mark(U11(X1,X2,X3)) -> a__U11(mark(X1),X2,X3)
 mark(U12(X1,X2,X3)) -> a__U12(mark(X1),X2,X3)
 mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2))
 mark(tt()) -> tt()
 mark(s(X)) -> s(mark(X))
 mark(0()) -> 0()
 a__U11(X1,X2,X3) -> U11(X1,X2,X3)
 a__U12(X1,X2,X3) -> U12(X1,X2,X3)
 a__plus(X1,X2) -> plus(X1,X2)

Proof:
 Matrix Interpretation Processor: dim=1
  
  interpretation:
   [plus](x0, x1) = x0 + x1,
   
   [U12](x0, x1, x2) = 4x0 + x1 + x2,
   
   [U11](x0, x1, x2) = 5x0 + x1 + x2,
   
   [0] = 4,
   
   [s](x0) = x0,
   
   [a__plus](x0, x1) = x0 + x1,
   
   [mark](x0) = x0,
   
   [a__U12](x0, x1, x2) = 4x0 + x1 + x2,
   
   [a__U11](x0, x1, x2) = 5x0 + x1 + x2,
   
   [tt] = 0
  orientation:
   a__U11(tt(),M,N) = M + N >= M + N = a__U12(tt(),M,N)
   
   a__U12(tt(),M,N) = M + N >= M + N = s(a__plus(mark(N),mark(M)))
   
   a__plus(N,0()) = N + 4 >= N = mark(N)
   
   a__plus(N,s(M)) = M + N >= M + N = a__U11(tt(),M,N)
   
   mark(U11(X1,X2,X3)) = 5X1 + X2 + X3 >= 5X1 + X2 + X3 = a__U11(mark(X1),X2,X3)
   
   mark(U12(X1,X2,X3)) = 4X1 + X2 + X3 >= 4X1 + X2 + X3 = a__U12(mark(X1),X2,X3)
   
   mark(plus(X1,X2)) = X1 + X2 >= X1 + X2 = a__plus(mark(X1),mark(X2))
   
   mark(tt()) = 0 >= 0 = tt()
   
   mark(s(X)) = X >= X = s(mark(X))
   
   mark(0()) = 4 >= 4 = 0()
   
   a__U11(X1,X2,X3) = 5X1 + X2 + X3 >= 5X1 + X2 + X3 = U11(X1,X2,X3)
   
   a__U12(X1,X2,X3) = 4X1 + X2 + X3 >= 4X1 + X2 + X3 = U12(X1,X2,X3)
   
   a__plus(X1,X2) = X1 + X2 >= X1 + X2 = plus(X1,X2)
  problem:
   a__U11(tt(),M,N) -> a__U12(tt(),M,N)
   a__U12(tt(),M,N) -> s(a__plus(mark(N),mark(M)))
   a__plus(N,s(M)) -> a__U11(tt(),M,N)
   mark(U11(X1,X2,X3)) -> a__U11(mark(X1),X2,X3)
   mark(U12(X1,X2,X3)) -> a__U12(mark(X1),X2,X3)
   mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2))
   mark(tt()) -> tt()
   mark(s(X)) -> s(mark(X))
   mark(0()) -> 0()
   a__U11(X1,X2,X3) -> U11(X1,X2,X3)
   a__U12(X1,X2,X3) -> U12(X1,X2,X3)
   a__plus(X1,X2) -> plus(X1,X2)
  Matrix Interpretation Processor: dim=3
   
   interpretation:
                     [1 0 0]     [1 1 0]  
    [plus](x0, x1) = [1 0 0]x0 + [0 1 0]x1
                     [0 0 0]     [0 0 0]  ,
    
                        [1 0 0]     [1 1 0]     [1 0 0]     [0]
    [U12](x0, x1, x2) = [0 0 0]x0 + [0 1 0]x1 + [1 0 0]x2 + [1]
                        [0 0 0]     [0 0 0]     [0 0 0]     [0],
    
                        [1 0 0]     [1 1 0]     [1 0 0]     [1]
    [U11](x0, x1, x2) = [1 1 0]x0 + [0 1 0]x1 + [1 0 0]x2 + [0]
                        [0 0 0]     [0 0 0]     [0 0 0]     [0],
    
          [1]
    [0] = [0]
          [0],
    
              [1 0 0]     [0]
    [s](x0) = [0 1 0]x0 + [1]
              [0 0 0]     [0],
    
                        [1 0 0]     [1 1 0]  
    [a__plus](x0, x1) = [1 0 0]x0 + [0 1 0]x1
                        [0 0 0]     [0 1 0]  ,
    
                 [1 0 0]  
    [mark](x0) = [0 1 0]x0
                 [1 0 0]  ,
    
                           [1 0 0]     [1 1 0]     [1 0 0]     [0]
    [a__U12](x0, x1, x2) = [0 0 0]x0 + [0 1 0]x1 + [1 0 0]x2 + [1]
                           [0 0 0]     [0 0 0]     [0 0 0]     [0],
    
                           [1 0 0]     [1 1 0]     [1 0 0]     [1]
    [a__U11](x0, x1, x2) = [1 1 0]x0 + [0 1 0]x1 + [1 0 0]x2 + [0]
                           [0 0 1]     [0 1 0]     [0 0 0]     [1],
    
           [0]
    [tt] = [1]
           [0]
   orientation:
                       [1 1 0]    [1 0 0]    [1]    [1 1 0]    [1 0 0]    [0]                   
    a__U11(tt(),M,N) = [0 1 0]M + [1 0 0]N + [1] >= [0 1 0]M + [1 0 0]N + [1] = a__U12(tt(),M,N)
                       [0 1 0]    [0 0 0]    [1]    [0 0 0]    [0 0 0]    [0]                   
    
                       [1 1 0]    [1 0 0]    [0]    [1 1 0]    [1 0 0]    [0]                              
    a__U12(tt(),M,N) = [0 1 0]M + [1 0 0]N + [1] >= [0 1 0]M + [1 0 0]N + [1] = s(a__plus(mark(N),mark(M)))
                       [0 0 0]    [0 0 0]    [0]    [0 0 0]    [0 0 0]    [0]                              
    
                      [1 1 0]    [1 0 0]    [1]    [1 1 0]    [1 0 0]    [1]                   
    a__plus(N,s(M)) = [0 1 0]M + [1 0 0]N + [1] >= [0 1 0]M + [1 0 0]N + [1] = a__U11(tt(),M,N)
                      [0 1 0]    [0 0 0]    [1]    [0 1 0]    [0 0 0]    [1]                   
    
                          [1 0 0]     [1 1 0]     [1 0 0]     [1]    [1 0 0]     [1 1 0]     [1 0 0]     [1]                         
    mark(U11(X1,X2,X3)) = [1 1 0]X1 + [0 1 0]X2 + [1 0 0]X3 + [0] >= [1 1 0]X1 + [0 1 0]X2 + [1 0 0]X3 + [0] = a__U11(mark(X1),X2,X3)
                          [1 0 0]     [1 1 0]     [1 0 0]     [1]    [1 0 0]     [0 1 0]     [0 0 0]     [1]                         
    
                          [1 0 0]     [1 1 0]     [1 0 0]     [0]    [1 0 0]     [1 1 0]     [1 0 0]     [0]                         
    mark(U12(X1,X2,X3)) = [0 0 0]X1 + [0 1 0]X2 + [1 0 0]X3 + [1] >= [0 0 0]X1 + [0 1 0]X2 + [1 0 0]X3 + [1] = a__U12(mark(X1),X2,X3)
                          [1 0 0]     [1 1 0]     [1 0 0]     [0]    [0 0 0]     [0 0 0]     [0 0 0]     [0]                         
    
                        [1 0 0]     [1 1 0]      [1 0 0]     [1 1 0]                               
    mark(plus(X1,X2)) = [1 0 0]X1 + [0 1 0]X2 >= [1 0 0]X1 + [0 1 0]X2 = a__plus(mark(X1),mark(X2))
                        [1 0 0]     [1 1 0]      [0 0 0]     [0 1 0]                               
    
                 [0]    [0]       
    mark(tt()) = [1] >= [1] = tt()
                 [0]    [0]       
    
                 [1 0 0]    [0]    [1 0 0]    [0]             
    mark(s(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = s(mark(X))
                 [1 0 0]    [0]    [0 0 0]    [0]             
    
                [1]    [1]      
    mark(0()) = [0] >= [0] = 0()
                [1]    [0]      
    
                       [1 0 0]     [1 1 0]     [1 0 0]     [1]    [1 0 0]     [1 1 0]     [1 0 0]     [1]                
    a__U11(X1,X2,X3) = [1 1 0]X1 + [0 1 0]X2 + [1 0 0]X3 + [0] >= [1 1 0]X1 + [0 1 0]X2 + [1 0 0]X3 + [0] = U11(X1,X2,X3)
                       [0 0 1]     [0 1 0]     [0 0 0]     [1]    [0 0 0]     [0 0 0]     [0 0 0]     [0]                
    
                       [1 0 0]     [1 1 0]     [1 0 0]     [0]    [1 0 0]     [1 1 0]     [1 0 0]     [0]                
    a__U12(X1,X2,X3) = [0 0 0]X1 + [0 1 0]X2 + [1 0 0]X3 + [1] >= [0 0 0]X1 + [0 1 0]X2 + [1 0 0]X3 + [1] = U12(X1,X2,X3)
                       [0 0 0]     [0 0 0]     [0 0 0]     [0]    [0 0 0]     [0 0 0]     [0 0 0]     [0]                
    
                     [1 0 0]     [1 1 0]      [1 0 0]     [1 1 0]                
    a__plus(X1,X2) = [1 0 0]X1 + [0 1 0]X2 >= [1 0 0]X1 + [0 1 0]X2 = plus(X1,X2)
                     [0 0 0]     [0 1 0]      [0 0 0]     [0 0 0]                
   problem:
    a__U12(tt(),M,N) -> s(a__plus(mark(N),mark(M)))
    a__plus(N,s(M)) -> a__U11(tt(),M,N)
    mark(U11(X1,X2,X3)) -> a__U11(mark(X1),X2,X3)
    mark(U12(X1,X2,X3)) -> a__U12(mark(X1),X2,X3)
    mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2))
    mark(tt()) -> tt()
    mark(s(X)) -> s(mark(X))
    mark(0()) -> 0()
    a__U11(X1,X2,X3) -> U11(X1,X2,X3)
    a__U12(X1,X2,X3) -> U12(X1,X2,X3)
    a__plus(X1,X2) -> plus(X1,X2)
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [plus](x0, x1) = 2x0 + x1,
     
     [U12](x0, x1, x2) = 3x0 + x1 + 2x2 + 4,
     
     [U11](x0, x1, x2) = x0 + x1 + 2x2,
     
     [0] = 0,
     
     [s](x0) = x0,
     
     [a__plus](x0, x1) = 2x0 + x1,
     
     [mark](x0) = x0,
     
     [a__U12](x0, x1, x2) = 3x0 + x1 + 2x2 + 4,
     
     [a__U11](x0, x1, x2) = x0 + x1 + 2x2,
     
     [tt] = 0
    orientation:
     a__U12(tt(),M,N) = M + 2N + 4 >= M + 2N = s(a__plus(mark(N),mark(M)))
     
     a__plus(N,s(M)) = M + 2N >= M + 2N = a__U11(tt(),M,N)
     
     mark(U11(X1,X2,X3)) = X1 + X2 + 2X3 >= X1 + X2 + 2X3 = a__U11(mark(X1),X2,X3)
     
     mark(U12(X1,X2,X3)) = 3X1 + X2 + 2X3 + 4 >= 3X1 + X2 + 2X3 + 4 = a__U12(mark(X1),X2,X3)
     
     mark(plus(X1,X2)) = 2X1 + X2 >= 2X1 + X2 = a__plus(mark(X1),mark(X2))
     
     mark(tt()) = 0 >= 0 = tt()
     
     mark(s(X)) = X >= X = s(mark(X))
     
     mark(0()) = 0 >= 0 = 0()
     
     a__U11(X1,X2,X3) = X1 + X2 + 2X3 >= X1 + X2 + 2X3 = U11(X1,X2,X3)
     
     a__U12(X1,X2,X3) = 3X1 + X2 + 2X3 + 4 >= 3X1 + X2 + 2X3 + 4 = U12(X1,X2,X3)
     
     a__plus(X1,X2) = 2X1 + X2 >= 2X1 + X2 = plus(X1,X2)
    problem:
     a__plus(N,s(M)) -> a__U11(tt(),M,N)
     mark(U11(X1,X2,X3)) -> a__U11(mark(X1),X2,X3)
     mark(U12(X1,X2,X3)) -> a__U12(mark(X1),X2,X3)
     mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2))
     mark(tt()) -> tt()
     mark(s(X)) -> s(mark(X))
     mark(0()) -> 0()
     a__U11(X1,X2,X3) -> U11(X1,X2,X3)
     a__U12(X1,X2,X3) -> U12(X1,X2,X3)
     a__plus(X1,X2) -> plus(X1,X2)
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [plus](x0, x1) = x0 + x1 + 4,
      
      [U12](x0, x1, x2) = x0 + 2x1 + 2x2,
      
      [U11](x0, x1, x2) = 2x0 + 4x1 + x2 + 2,
      
      [0] = 0,
      
      [s](x0) = 4x0 + 2,
      
      [a__plus](x0, x1) = x0 + x1 + 4,
      
      [mark](x0) = 2x0,
      
      [a__U12](x0, x1, x2) = x0 + 4x1 + 2x2,
      
      [a__U11](x0, x1, x2) = 2x0 + 4x1 + x2 + 2,
      
      [tt] = 2
     orientation:
      a__plus(N,s(M)) = 4M + N + 6 >= 4M + N + 6 = a__U11(tt(),M,N)
      
      mark(U11(X1,X2,X3)) = 4X1 + 8X2 + 2X3 + 4 >= 4X1 + 4X2 + X3 + 2 = a__U11(mark(X1),X2,X3)
      
      mark(U12(X1,X2,X3)) = 2X1 + 4X2 + 4X3 >= 2X1 + 4X2 + 2X3 = a__U12(mark(X1),X2,X3)
      
      mark(plus(X1,X2)) = 2X1 + 2X2 + 8 >= 2X1 + 2X2 + 4 = a__plus(mark(X1),mark(X2))
      
      mark(tt()) = 4 >= 2 = tt()
      
      mark(s(X)) = 8X + 4 >= 8X + 2 = s(mark(X))
      
      mark(0()) = 0 >= 0 = 0()
      
      a__U11(X1,X2,X3) = 2X1 + 4X2 + X3 + 2 >= 2X1 + 4X2 + X3 + 2 = U11(X1,X2,X3)
      
      a__U12(X1,X2,X3) = X1 + 4X2 + 2X3 >= X1 + 2X2 + 2X3 = U12(X1,X2,X3)
      
      a__plus(X1,X2) = X1 + X2 + 4 >= X1 + X2 + 4 = plus(X1,X2)
     problem:
      a__plus(N,s(M)) -> a__U11(tt(),M,N)
      mark(U12(X1,X2,X3)) -> a__U12(mark(X1),X2,X3)
      mark(0()) -> 0()
      a__U11(X1,X2,X3) -> U11(X1,X2,X3)
      a__U12(X1,X2,X3) -> U12(X1,X2,X3)
      a__plus(X1,X2) -> plus(X1,X2)
     DP Processor:
      DPs:
       a__plus#(N,s(M)) -> a__U11#(tt(),M,N)
       mark#(U12(X1,X2,X3)) -> mark#(X1)
       mark#(U12(X1,X2,X3)) -> a__U12#(mark(X1),X2,X3)
      TRS:
       a__plus(N,s(M)) -> a__U11(tt(),M,N)
       mark(U12(X1,X2,X3)) -> a__U12(mark(X1),X2,X3)
       mark(0()) -> 0()
       a__U11(X1,X2,X3) -> U11(X1,X2,X3)
       a__U12(X1,X2,X3) -> U12(X1,X2,X3)
       a__plus(X1,X2) -> plus(X1,X2)
      TDG Processor:
       DPs:
        a__plus#(N,s(M)) -> a__U11#(tt(),M,N)
        mark#(U12(X1,X2,X3)) -> mark#(X1)
        mark#(U12(X1,X2,X3)) -> a__U12#(mark(X1),X2,X3)
       TRS:
        a__plus(N,s(M)) -> a__U11(tt(),M,N)
        mark(U12(X1,X2,X3)) -> a__U12(mark(X1),X2,X3)
        mark(0()) -> 0()
        a__U11(X1,X2,X3) -> U11(X1,X2,X3)
        a__U12(X1,X2,X3) -> U12(X1,X2,X3)
        a__plus(X1,X2) -> plus(X1,X2)
       graph:
        mark#(U12(X1,X2,X3)) -> mark#(X1) ->
        mark#(U12(X1,X2,X3)) -> a__U12#(mark(X1),X2,X3)
        mark#(U12(X1,X2,X3)) -> mark#(X1) -> mark#(U12(X1,X2,X3)) -> mark#(X1)
       SCC Processor:
        #sccs: 1
        #rules: 1
        #arcs: 2/9
        DPs:
         mark#(U12(X1,X2,X3)) -> mark#(X1)
        TRS:
         a__plus(N,s(M)) -> a__U11(tt(),M,N)
         mark(U12(X1,X2,X3)) -> a__U12(mark(X1),X2,X3)
         mark(0()) -> 0()
         a__U11(X1,X2,X3) -> U11(X1,X2,X3)
         a__U12(X1,X2,X3) -> U12(X1,X2,X3)
         a__plus(X1,X2) -> plus(X1,X2)
        Subterm Criterion Processor:
         simple projection:
          pi(mark#) = 0
         problem:
          DPs:
           
          TRS:
           a__plus(N,s(M)) -> a__U11(tt(),M,N)
           mark(U12(X1,X2,X3)) -> a__U12(mark(X1),X2,X3)
           mark(0()) -> 0()
           a__U11(X1,X2,X3) -> U11(X1,X2,X3)
           a__U12(X1,X2,X3) -> U12(X1,X2,X3)
           a__plus(X1,X2) -> plus(X1,X2)
         Qed