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=1
   
   interpretation:
    [plus](x0, x1) = x0 + 5x1,
    
    [U12](x0, x1, x2) = x0 + 5x1 + x2 + 1,
    
    [U11](x0, x1, x2) = x0 + 5x1 + x2 + 1,
    
    [0] = 1,
    
    [s](x0) = x0 + 2,
    
    [a__plus](x0, x1) = x0 + 5x1,
    
    [mark](x0) = x0,
    
    [a__U12](x0, x1, x2) = x0 + 5x1 + x2 + 1,
    
    [a__U11](x0, x1, x2) = x0 + 5x1 + x2 + 1,
    
    [tt] = 2
   orientation:
    a__U11(tt(),M,N) = 5M + N + 3 >= 5M + N + 3 = a__U12(tt(),M,N)
    
    a__U12(tt(),M,N) = 5M + N + 3 >= 5M + N + 2 = s(a__plus(mark(N),mark(M)))
    
    a__plus(N,s(M)) = 5M + N + 10 >= 5M + N + 3 = a__U11(tt(),M,N)
    
    mark(U11(X1,X2,X3)) = X1 + 5X2 + X3 + 1 >= X1 + 5X2 + X3 + 1 = a__U11(mark(X1),X2,X3)
    
    mark(U12(X1,X2,X3)) = X1 + 5X2 + X3 + 1 >= X1 + 5X2 + X3 + 1 = a__U12(mark(X1),X2,X3)
    
    mark(plus(X1,X2)) = X1 + 5X2 >= X1 + 5X2 = a__plus(mark(X1),mark(X2))
    
    mark(tt()) = 2 >= 2 = tt()
    
    mark(s(X)) = X + 2 >= X + 2 = s(mark(X))
    
    mark(0()) = 1 >= 1 = 0()
    
    a__U11(X1,X2,X3) = X1 + 5X2 + X3 + 1 >= X1 + 5X2 + X3 + 1 = U11(X1,X2,X3)
    
    a__U12(X1,X2,X3) = X1 + 5X2 + X3 + 1 >= X1 + 5X2 + X3 + 1 = U12(X1,X2,X3)
    
    a__plus(X1,X2) = X1 + 5X2 >= X1 + 5X2 = plus(X1,X2)
   problem:
    a__U11(tt(),M,N) -> a__U12(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) = x0 + 2x1 + x2,
     
     [U11](x0, x1, x2) = 5x0 + 2x1 + x2,
     
     [0] = 0,
     
     [s](x0) = 4x0,
     
     [a__plus](x0, x1) = 2x0 + x1,
     
     [mark](x0) = 4x0,
     
     [a__U12](x0, x1, x2) = x0 + 4x1 + 2x2,
     
     [a__U11](x0, x1, x2) = 5x0 + 4x1 + 2x2,
     
     [tt] = 2
    orientation:
     a__U11(tt(),M,N) = 4M + 2N + 10 >= 4M + 2N + 2 = a__U12(tt(),M,N)
     
     mark(U11(X1,X2,X3)) = 20X1 + 8X2 + 4X3 >= 20X1 + 4X2 + 2X3 = a__U11(mark(X1),X2,X3)
     
     mark(U12(X1,X2,X3)) = 4X1 + 8X2 + 4X3 >= 4X1 + 4X2 + 2X3 = a__U12(mark(X1),X2,X3)
     
     mark(plus(X1,X2)) = 8X1 + 4X2 >= 8X1 + 4X2 = a__plus(mark(X1),mark(X2))
     
     mark(tt()) = 8 >= 2 = tt()
     
     mark(s(X)) = 16X >= 16X = s(mark(X))
     
     mark(0()) = 0 >= 0 = 0()
     
     a__U11(X1,X2,X3) = 5X1 + 4X2 + 2X3 >= 5X1 + 2X2 + X3 = U11(X1,X2,X3)
     
     a__U12(X1,X2,X3) = X1 + 4X2 + 2X3 >= X1 + 2X2 + X3 = U12(X1,X2,X3)
     
     a__plus(X1,X2) = 2X1 + X2 >= 2X1 + X2 = plus(X1,X2)
    problem:
     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(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 + 2x1 + 3,
      
      [U12](x0, x1, x2) = x0 + x1 + x2 + 1,
      
      [U11](x0, x1, x2) = x0 + x1 + x2 + 1,
      
      [0] = 0,
      
      [s](x0) = 2x0 + 4,
      
      [a__plus](x0, x1) = 2x0 + 2x1 + 4,
      
      [mark](x0) = 4x0,
      
      [a__U12](x0, x1, x2) = x0 + 4x1 + 2x2 + 4,
      
      [a__U11](x0, x1, x2) = x0 + 4x1 + 4x2 + 4
     orientation:
      mark(U11(X1,X2,X3)) = 4X1 + 4X2 + 4X3 + 4 >= 4X1 + 4X2 + 4X3 + 4 = a__U11(mark(X1),X2,X3)
      
      mark(U12(X1,X2,X3)) = 4X1 + 4X2 + 4X3 + 4 >= 4X1 + 4X2 + 2X3 + 4 = a__U12(mark(X1),X2,X3)
      
      mark(plus(X1,X2)) = 8X1 + 8X2 + 12 >= 8X1 + 8X2 + 4 = a__plus(mark(X1),mark(X2))
      
      mark(s(X)) = 8X + 16 >= 8X + 4 = s(mark(X))
      
      mark(0()) = 0 >= 0 = 0()
      
      a__U11(X1,X2,X3) = X1 + 4X2 + 4X3 + 4 >= X1 + X2 + X3 + 1 = U11(X1,X2,X3)
      
      a__U12(X1,X2,X3) = X1 + 4X2 + 2X3 + 4 >= X1 + X2 + X3 + 1 = U12(X1,X2,X3)
      
      a__plus(X1,X2) = 2X1 + 2X2 + 4 >= 2X1 + 2X2 + 3 = plus(X1,X2)
     problem:
      mark(U11(X1,X2,X3)) -> a__U11(mark(X1),X2,X3)
      mark(U12(X1,X2,X3)) -> a__U12(mark(X1),X2,X3)
      mark(0()) -> 0()
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [U12](x0, x1, x2) = x0 + x1 + x2,
       
       [U11](x0, x1, x2) = 3x0 + x1 + x2 + 5,
       
       [0] = 0,
       
       [mark](x0) = 4x0 + 7,
       
       [a__U12](x0, x1, x2) = x0 + 4x1 + 4x2,
       
       [a__U11](x0, x1, x2) = 3x0 + 4x1 + 4x2 + 6
      orientation:
       mark(U11(X1,X2,X3)) = 12X1 + 4X2 + 4X3 + 27 >= 12X1 + 4X2 + 4X3 + 27 = a__U11(mark(X1),X2,X3)
       
       mark(U12(X1,X2,X3)) = 4X1 + 4X2 + 4X3 + 7 >= 4X1 + 4X2 + 4X3 + 7 = a__U12(mark(X1),X2,X3)
       
       mark(0()) = 7 >= 0 = 0()
      problem:
       mark(U11(X1,X2,X3)) -> a__U11(mark(X1),X2,X3)
       mark(U12(X1,X2,X3)) -> a__U12(mark(X1),X2,X3)
      Matrix Interpretation Processor: dim=1
       
       interpretation:
        [U12](x0, x1, x2) = x0 + x1 + x2 + 5,
        
        [U11](x0, x1, x2) = x0 + x1 + x2 + 4,
        
        [mark](x0) = x0,
        
        [a__U12](x0, x1, x2) = x0 + x1 + x2,
        
        [a__U11](x0, x1, x2) = x0 + x1 + x2 + 4
       orientation:
        mark(U11(X1,X2,X3)) = X1 + X2 + X3 + 4 >= X1 + X2 + X3 + 4 = a__U11(mark(X1),X2,X3)
        
        mark(U12(X1,X2,X3)) = X1 + X2 + X3 + 5 >= X1 + X2 + X3 = a__U12(mark(X1),X2,X3)
       problem:
        mark(U11(X1,X2,X3)) -> a__U11(mark(X1),X2,X3)
       DP Processor:
        DPs:
         mark#(U11(X1,X2,X3)) -> mark#(X1)
        TRS:
         mark(U11(X1,X2,X3)) -> a__U11(mark(X1),X2,X3)
        Subterm Criterion Processor:
         simple projection:
          pi(mark#) = 0
         problem:
          DPs:
           
          TRS:
           mark(U11(X1,X2,X3)) -> a__U11(mark(X1),X2,X3)
         Qed