YES

Problem:
 1(1(x1)) -> 4(3(x1))
 1(2(x1)) -> 2(1(x1))
 2(2(x1)) -> 1(1(1(x1)))
 3(3(x1)) -> 5(6(x1))
 3(4(x1)) -> 1(1(x1))
 4(4(x1)) -> 3(x1)
 5(5(x1)) -> 6(2(x1))
 5(6(x1)) -> 1(2(x1))
 6(6(x1)) -> 2(1(x1))

Proof:
 DP Processor:
  DPs:
   1#(1(x1)) -> 3#(x1)
   1#(1(x1)) -> 4#(3(x1))
   1#(2(x1)) -> 1#(x1)
   1#(2(x1)) -> 2#(1(x1))
   2#(2(x1)) -> 1#(x1)
   2#(2(x1)) -> 1#(1(x1))
   2#(2(x1)) -> 1#(1(1(x1)))
   3#(3(x1)) -> 6#(x1)
   3#(3(x1)) -> 5#(6(x1))
   3#(4(x1)) -> 1#(x1)
   3#(4(x1)) -> 1#(1(x1))
   4#(4(x1)) -> 3#(x1)
   5#(5(x1)) -> 2#(x1)
   5#(5(x1)) -> 6#(2(x1))
   5#(6(x1)) -> 2#(x1)
   5#(6(x1)) -> 1#(2(x1))
   6#(6(x1)) -> 1#(x1)
   6#(6(x1)) -> 2#(1(x1))
  TRS:
   1(1(x1)) -> 4(3(x1))
   1(2(x1)) -> 2(1(x1))
   2(2(x1)) -> 1(1(1(x1)))
   3(3(x1)) -> 5(6(x1))
   3(4(x1)) -> 1(1(x1))
   4(4(x1)) -> 3(x1)
   5(5(x1)) -> 6(2(x1))
   5(6(x1)) -> 1(2(x1))
   6(6(x1)) -> 2(1(x1))
  TDG Processor:
   DPs:
    1#(1(x1)) -> 3#(x1)
    1#(1(x1)) -> 4#(3(x1))
    1#(2(x1)) -> 1#(x1)
    1#(2(x1)) -> 2#(1(x1))
    2#(2(x1)) -> 1#(x1)
    2#(2(x1)) -> 1#(1(x1))
    2#(2(x1)) -> 1#(1(1(x1)))
    3#(3(x1)) -> 6#(x1)
    3#(3(x1)) -> 5#(6(x1))
    3#(4(x1)) -> 1#(x1)
    3#(4(x1)) -> 1#(1(x1))
    4#(4(x1)) -> 3#(x1)
    5#(5(x1)) -> 2#(x1)
    5#(5(x1)) -> 6#(2(x1))
    5#(6(x1)) -> 2#(x1)
    5#(6(x1)) -> 1#(2(x1))
    6#(6(x1)) -> 1#(x1)
    6#(6(x1)) -> 2#(1(x1))
   TRS:
    1(1(x1)) -> 4(3(x1))
    1(2(x1)) -> 2(1(x1))
    2(2(x1)) -> 1(1(1(x1)))
    3(3(x1)) -> 5(6(x1))
    3(4(x1)) -> 1(1(x1))
    4(4(x1)) -> 3(x1)
    5(5(x1)) -> 6(2(x1))
    5(6(x1)) -> 1(2(x1))
    6(6(x1)) -> 2(1(x1))
   graph:
    5#(5(x1)) -> 6#(2(x1)) -> 6#(6(x1)) -> 2#(1(x1))
    5#(5(x1)) -> 6#(2(x1)) -> 6#(6(x1)) -> 1#(x1)
    5#(5(x1)) -> 2#(x1) -> 2#(2(x1)) -> 1#(1(1(x1)))
    5#(5(x1)) -> 2#(x1) -> 2#(2(x1)) -> 1#(1(x1))
    5#(5(x1)) -> 2#(x1) -> 2#(2(x1)) -> 1#(x1)
    5#(6(x1)) -> 2#(x1) -> 2#(2(x1)) -> 1#(1(1(x1)))
    5#(6(x1)) -> 2#(x1) -> 2#(2(x1)) -> 1#(1(x1))
    5#(6(x1)) -> 2#(x1) -> 2#(2(x1)) -> 1#(x1)
    5#(6(x1)) -> 1#(2(x1)) -> 1#(2(x1)) -> 2#(1(x1))
    5#(6(x1)) -> 1#(2(x1)) -> 1#(2(x1)) -> 1#(x1)
    5#(6(x1)) -> 1#(2(x1)) -> 1#(1(x1)) -> 4#(3(x1))
    5#(6(x1)) -> 1#(2(x1)) -> 1#(1(x1)) -> 3#(x1)
    6#(6(x1)) -> 2#(1(x1)) -> 2#(2(x1)) -> 1#(1(1(x1)))
    6#(6(x1)) -> 2#(1(x1)) -> 2#(2(x1)) -> 1#(1(x1))
    6#(6(x1)) -> 2#(1(x1)) -> 2#(2(x1)) -> 1#(x1)
    6#(6(x1)) -> 1#(x1) -> 1#(2(x1)) -> 2#(1(x1))
    6#(6(x1)) -> 1#(x1) -> 1#(2(x1)) -> 1#(x1)
    6#(6(x1)) -> 1#(x1) -> 1#(1(x1)) -> 4#(3(x1))
    6#(6(x1)) -> 1#(x1) -> 1#(1(x1)) -> 3#(x1)
    2#(2(x1)) -> 1#(1(1(x1))) -> 1#(2(x1)) -> 2#(1(x1))
    2#(2(x1)) -> 1#(1(1(x1))) -> 1#(2(x1)) -> 1#(x1)
    2#(2(x1)) -> 1#(1(1(x1))) -> 1#(1(x1)) -> 4#(3(x1))
    2#(2(x1)) -> 1#(1(1(x1))) -> 1#(1(x1)) -> 3#(x1)
    2#(2(x1)) -> 1#(1(x1)) -> 1#(2(x1)) -> 2#(1(x1))
    2#(2(x1)) -> 1#(1(x1)) -> 1#(2(x1)) -> 1#(x1)
    2#(2(x1)) -> 1#(1(x1)) -> 1#(1(x1)) -> 4#(3(x1))
    2#(2(x1)) -> 1#(1(x1)) -> 1#(1(x1)) -> 3#(x1)
    2#(2(x1)) -> 1#(x1) -> 1#(2(x1)) -> 2#(1(x1))
    2#(2(x1)) -> 1#(x1) -> 1#(2(x1)) -> 1#(x1)
    2#(2(x1)) -> 1#(x1) -> 1#(1(x1)) -> 4#(3(x1))
    2#(2(x1)) -> 1#(x1) -> 1#(1(x1)) -> 3#(x1)
    4#(4(x1)) -> 3#(x1) -> 3#(4(x1)) -> 1#(1(x1))
    4#(4(x1)) -> 3#(x1) -> 3#(4(x1)) -> 1#(x1)
    4#(4(x1)) -> 3#(x1) -> 3#(3(x1)) -> 5#(6(x1))
    4#(4(x1)) -> 3#(x1) -> 3#(3(x1)) -> 6#(x1)
    3#(4(x1)) -> 1#(1(x1)) -> 1#(2(x1)) -> 2#(1(x1))
    3#(4(x1)) -> 1#(1(x1)) -> 1#(2(x1)) -> 1#(x1)
    3#(4(x1)) -> 1#(1(x1)) -> 1#(1(x1)) -> 4#(3(x1))
    3#(4(x1)) -> 1#(1(x1)) -> 1#(1(x1)) -> 3#(x1)
    3#(4(x1)) -> 1#(x1) -> 1#(2(x1)) -> 2#(1(x1))
    3#(4(x1)) -> 1#(x1) -> 1#(2(x1)) -> 1#(x1)
    3#(4(x1)) -> 1#(x1) -> 1#(1(x1)) -> 4#(3(x1))
    3#(4(x1)) -> 1#(x1) -> 1#(1(x1)) -> 3#(x1)
    3#(3(x1)) -> 5#(6(x1)) -> 5#(6(x1)) -> 1#(2(x1))
    3#(3(x1)) -> 5#(6(x1)) -> 5#(6(x1)) -> 2#(x1)
    3#(3(x1)) -> 5#(6(x1)) -> 5#(5(x1)) -> 6#(2(x1))
    3#(3(x1)) -> 5#(6(x1)) -> 5#(5(x1)) -> 2#(x1)
    3#(3(x1)) -> 6#(x1) -> 6#(6(x1)) -> 2#(1(x1))
    3#(3(x1)) -> 6#(x1) -> 6#(6(x1)) -> 1#(x1)
    1#(2(x1)) -> 2#(1(x1)) -> 2#(2(x1)) -> 1#(1(1(x1)))
    1#(2(x1)) -> 2#(1(x1)) -> 2#(2(x1)) -> 1#(1(x1))
    1#(2(x1)) -> 2#(1(x1)) -> 2#(2(x1)) -> 1#(x1)
    1#(2(x1)) -> 1#(x1) -> 1#(2(x1)) -> 2#(1(x1))
    1#(2(x1)) -> 1#(x1) -> 1#(2(x1)) -> 1#(x1)
    1#(2(x1)) -> 1#(x1) -> 1#(1(x1)) -> 4#(3(x1))
    1#(2(x1)) -> 1#(x1) -> 1#(1(x1)) -> 3#(x1)
    1#(1(x1)) -> 4#(3(x1)) -> 4#(4(x1)) -> 3#(x1)
    1#(1(x1)) -> 3#(x1) -> 3#(4(x1)) -> 1#(1(x1))
    1#(1(x1)) -> 3#(x1) -> 3#(4(x1)) -> 1#(x1)
    1#(1(x1)) -> 3#(x1) -> 3#(3(x1)) -> 5#(6(x1))
    1#(1(x1)) -> 3#(x1) -> 3#(3(x1)) -> 6#(x1)
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [5#](x0) = 2x0 + 21,
     
     [6#](x0) = 2x0 + 18,
     
     [2#](x0) = 2x0 + 24,
     
     [4#](x0) = 2x0 + 4,
     
     [3#](x0) = 2x0 + 20,
     
     [1#](x0) = 2x0 + 12,
     
     [5](x0) = x0 + 17,
     
     [6](x0) = x0 + 15,
     
     [2](x0) = x0 + 18,
     
     [4](x0) = x0 + 8,
     
     [3](x0) = x0 + 16,
     
     [1](x0) = x0 + 12
    orientation:
     1#(1(x1)) = 2x1 + 36 >= 2x1 + 20 = 3#(x1)
     
     1#(1(x1)) = 2x1 + 36 >= 2x1 + 36 = 4#(3(x1))
     
     1#(2(x1)) = 2x1 + 48 >= 2x1 + 12 = 1#(x1)
     
     1#(2(x1)) = 2x1 + 48 >= 2x1 + 48 = 2#(1(x1))
     
     2#(2(x1)) = 2x1 + 60 >= 2x1 + 12 = 1#(x1)
     
     2#(2(x1)) = 2x1 + 60 >= 2x1 + 36 = 1#(1(x1))
     
     2#(2(x1)) = 2x1 + 60 >= 2x1 + 60 = 1#(1(1(x1)))
     
     3#(3(x1)) = 2x1 + 52 >= 2x1 + 18 = 6#(x1)
     
     3#(3(x1)) = 2x1 + 52 >= 2x1 + 51 = 5#(6(x1))
     
     3#(4(x1)) = 2x1 + 36 >= 2x1 + 12 = 1#(x1)
     
     3#(4(x1)) = 2x1 + 36 >= 2x1 + 36 = 1#(1(x1))
     
     4#(4(x1)) = 2x1 + 20 >= 2x1 + 20 = 3#(x1)
     
     5#(5(x1)) = 2x1 + 55 >= 2x1 + 24 = 2#(x1)
     
     5#(5(x1)) = 2x1 + 55 >= 2x1 + 54 = 6#(2(x1))
     
     5#(6(x1)) = 2x1 + 51 >= 2x1 + 24 = 2#(x1)
     
     5#(6(x1)) = 2x1 + 51 >= 2x1 + 48 = 1#(2(x1))
     
     6#(6(x1)) = 2x1 + 48 >= 2x1 + 12 = 1#(x1)
     
     6#(6(x1)) = 2x1 + 48 >= 2x1 + 48 = 2#(1(x1))
     
     1(1(x1)) = x1 + 24 >= x1 + 24 = 4(3(x1))
     
     1(2(x1)) = x1 + 30 >= x1 + 30 = 2(1(x1))
     
     2(2(x1)) = x1 + 36 >= x1 + 36 = 1(1(1(x1)))
     
     3(3(x1)) = x1 + 32 >= x1 + 32 = 5(6(x1))
     
     3(4(x1)) = x1 + 24 >= x1 + 24 = 1(1(x1))
     
     4(4(x1)) = x1 + 16 >= x1 + 16 = 3(x1)
     
     5(5(x1)) = x1 + 34 >= x1 + 33 = 6(2(x1))
     
     5(6(x1)) = x1 + 32 >= x1 + 30 = 1(2(x1))
     
     6(6(x1)) = x1 + 30 >= x1 + 30 = 2(1(x1))
    problem:
     DPs:
      1#(1(x1)) -> 4#(3(x1))
      1#(2(x1)) -> 2#(1(x1))
      2#(2(x1)) -> 1#(1(1(x1)))
      3#(4(x1)) -> 1#(1(x1))
      4#(4(x1)) -> 3#(x1)
      6#(6(x1)) -> 2#(1(x1))
     TRS:
      1(1(x1)) -> 4(3(x1))
      1(2(x1)) -> 2(1(x1))
      2(2(x1)) -> 1(1(1(x1)))
      3(3(x1)) -> 5(6(x1))
      3(4(x1)) -> 1(1(x1))
      4(4(x1)) -> 3(x1)
      5(5(x1)) -> 6(2(x1))
      5(6(x1)) -> 1(2(x1))
      6(6(x1)) -> 2(1(x1))
    EDG Processor:
     DPs:
      1#(1(x1)) -> 4#(3(x1))
      1#(2(x1)) -> 2#(1(x1))
      2#(2(x1)) -> 1#(1(1(x1)))
      3#(4(x1)) -> 1#(1(x1))
      4#(4(x1)) -> 3#(x1)
      6#(6(x1)) -> 2#(1(x1))
     TRS:
      1(1(x1)) -> 4(3(x1))
      1(2(x1)) -> 2(1(x1))
      2(2(x1)) -> 1(1(1(x1)))
      3(3(x1)) -> 5(6(x1))
      3(4(x1)) -> 1(1(x1))
      4(4(x1)) -> 3(x1)
      5(5(x1)) -> 6(2(x1))
      5(6(x1)) -> 1(2(x1))
      6(6(x1)) -> 2(1(x1))
     graph:
      6#(6(x1)) -> 2#(1(x1)) -> 2#(2(x1)) -> 1#(1(1(x1)))
      2#(2(x1)) -> 1#(1(1(x1))) -> 1#(1(x1)) -> 4#(3(x1))
      2#(2(x1)) -> 1#(1(1(x1))) -> 1#(2(x1)) -> 2#(1(x1))
      4#(4(x1)) -> 3#(x1) -> 3#(4(x1)) -> 1#(1(x1))
      3#(4(x1)) -> 1#(1(x1)) -> 1#(1(x1)) -> 4#(3(x1))
      3#(4(x1)) -> 1#(1(x1)) -> 1#(2(x1)) -> 2#(1(x1))
      1#(2(x1)) -> 2#(1(x1)) -> 2#(2(x1)) -> 1#(1(1(x1)))
      1#(1(x1)) -> 4#(3(x1)) -> 4#(4(x1)) -> 3#(x1)
     SCC Processor:
      #sccs: 1
      #rules: 5
      #arcs: 8/36
      DPs:
       2#(2(x1)) -> 1#(1(1(x1)))
       1#(2(x1)) -> 2#(1(x1))
       1#(1(x1)) -> 4#(3(x1))
       4#(4(x1)) -> 3#(x1)
       3#(4(x1)) -> 1#(1(x1))
      TRS:
       1(1(x1)) -> 4(3(x1))
       1(2(x1)) -> 2(1(x1))
       2(2(x1)) -> 1(1(1(x1)))
       3(3(x1)) -> 5(6(x1))
       3(4(x1)) -> 1(1(x1))
       4(4(x1)) -> 3(x1)
       5(5(x1)) -> 6(2(x1))
       5(6(x1)) -> 1(2(x1))
       6(6(x1)) -> 2(1(x1))
      Matrix Interpretation Processor: dim=1
       
       interpretation:
        [2#](x0) = x0 + 15,
        
        [4#](x0) = x0 + 2,
        
        [3#](x0) = x0 + 12,
        
        [1#](x0) = x0 + 7,
        
        [5](x0) = x0 + 22,
        
        [6](x0) = x0 + 20,
        
        [2](x0) = x0 + 24,
        
        [4](x0) = x0 + 11,
        
        [3](x0) = x0 + 21,
        
        [1](x0) = x0 + 16
       orientation:
        2#(2(x1)) = x1 + 39 >= x1 + 39 = 1#(1(1(x1)))
        
        1#(2(x1)) = x1 + 31 >= x1 + 31 = 2#(1(x1))
        
        1#(1(x1)) = x1 + 23 >= x1 + 23 = 4#(3(x1))
        
        4#(4(x1)) = x1 + 13 >= x1 + 12 = 3#(x1)
        
        3#(4(x1)) = x1 + 23 >= x1 + 23 = 1#(1(x1))
        
        1(1(x1)) = x1 + 32 >= x1 + 32 = 4(3(x1))
        
        1(2(x1)) = x1 + 40 >= x1 + 40 = 2(1(x1))
        
        2(2(x1)) = x1 + 48 >= x1 + 48 = 1(1(1(x1)))
        
        3(3(x1)) = x1 + 42 >= x1 + 42 = 5(6(x1))
        
        3(4(x1)) = x1 + 32 >= x1 + 32 = 1(1(x1))
        
        4(4(x1)) = x1 + 22 >= x1 + 21 = 3(x1)
        
        5(5(x1)) = x1 + 44 >= x1 + 44 = 6(2(x1))
        
        5(6(x1)) = x1 + 42 >= x1 + 40 = 1(2(x1))
        
        6(6(x1)) = x1 + 40 >= x1 + 40 = 2(1(x1))
       problem:
        DPs:
         2#(2(x1)) -> 1#(1(1(x1)))
         1#(2(x1)) -> 2#(1(x1))
         1#(1(x1)) -> 4#(3(x1))
         3#(4(x1)) -> 1#(1(x1))
        TRS:
         1(1(x1)) -> 4(3(x1))
         1(2(x1)) -> 2(1(x1))
         2(2(x1)) -> 1(1(1(x1)))
         3(3(x1)) -> 5(6(x1))
         3(4(x1)) -> 1(1(x1))
         4(4(x1)) -> 3(x1)
         5(5(x1)) -> 6(2(x1))
         5(6(x1)) -> 1(2(x1))
         6(6(x1)) -> 2(1(x1))
       EDG Processor:
        DPs:
         2#(2(x1)) -> 1#(1(1(x1)))
         1#(2(x1)) -> 2#(1(x1))
         1#(1(x1)) -> 4#(3(x1))
         3#(4(x1)) -> 1#(1(x1))
        TRS:
         1(1(x1)) -> 4(3(x1))
         1(2(x1)) -> 2(1(x1))
         2(2(x1)) -> 1(1(1(x1)))
         3(3(x1)) -> 5(6(x1))
         3(4(x1)) -> 1(1(x1))
         4(4(x1)) -> 3(x1)
         5(5(x1)) -> 6(2(x1))
         5(6(x1)) -> 1(2(x1))
         6(6(x1)) -> 2(1(x1))
        graph:
         2#(2(x1)) -> 1#(1(1(x1))) -> 1#(2(x1)) -> 2#(1(x1))
         2#(2(x1)) -> 1#(1(1(x1))) -> 1#(1(x1)) -> 4#(3(x1))
         3#(4(x1)) -> 1#(1(x1)) -> 1#(2(x1)) -> 2#(1(x1))
         3#(4(x1)) -> 1#(1(x1)) -> 1#(1(x1)) -> 4#(3(x1))
         1#(2(x1)) -> 2#(1(x1)) -> 2#(2(x1)) -> 1#(1(1(x1)))
        SCC Processor:
         #sccs: 1
         #rules: 2
         #arcs: 5/16
         DPs:
          2#(2(x1)) -> 1#(1(1(x1)))
          1#(2(x1)) -> 2#(1(x1))
         TRS:
          1(1(x1)) -> 4(3(x1))
          1(2(x1)) -> 2(1(x1))
          2(2(x1)) -> 1(1(1(x1)))
          3(3(x1)) -> 5(6(x1))
          3(4(x1)) -> 1(1(x1))
          4(4(x1)) -> 3(x1)
          5(5(x1)) -> 6(2(x1))
          5(6(x1)) -> 1(2(x1))
          6(6(x1)) -> 2(1(x1))
         Matrix Interpretation Processor: dim=1
          
          interpretation:
           [2#](x0) = x0 + 16,
           
           [1#](x0) = x0 + 8,
           
           [5](x0) = x0 + 21,
           
           [6](x0) = x0 + 19,
           
           [2](x0) = x0 + 23,
           
           [4](x0) = x0 + 10,
           
           [3](x0) = x0 + 20,
           
           [1](x0) = x0 + 15
          orientation:
           2#(2(x1)) = x1 + 39 >= x1 + 38 = 1#(1(1(x1)))
           
           1#(2(x1)) = x1 + 31 >= x1 + 31 = 2#(1(x1))
           
           1(1(x1)) = x1 + 30 >= x1 + 30 = 4(3(x1))
           
           1(2(x1)) = x1 + 38 >= x1 + 38 = 2(1(x1))
           
           2(2(x1)) = x1 + 46 >= x1 + 45 = 1(1(1(x1)))
           
           3(3(x1)) = x1 + 40 >= x1 + 40 = 5(6(x1))
           
           3(4(x1)) = x1 + 30 >= x1 + 30 = 1(1(x1))
           
           4(4(x1)) = x1 + 20 >= x1 + 20 = 3(x1)
           
           5(5(x1)) = x1 + 42 >= x1 + 42 = 6(2(x1))
           
           5(6(x1)) = x1 + 40 >= x1 + 38 = 1(2(x1))
           
           6(6(x1)) = x1 + 38 >= x1 + 38 = 2(1(x1))
          problem:
           DPs:
            1#(2(x1)) -> 2#(1(x1))
           TRS:
            1(1(x1)) -> 4(3(x1))
            1(2(x1)) -> 2(1(x1))
            2(2(x1)) -> 1(1(1(x1)))
            3(3(x1)) -> 5(6(x1))
            3(4(x1)) -> 1(1(x1))
            4(4(x1)) -> 3(x1)
            5(5(x1)) -> 6(2(x1))
            5(6(x1)) -> 1(2(x1))
            6(6(x1)) -> 2(1(x1))
          EDG Processor:
           DPs:
            1#(2(x1)) -> 2#(1(x1))
           TRS:
            1(1(x1)) -> 4(3(x1))
            1(2(x1)) -> 2(1(x1))
            2(2(x1)) -> 1(1(1(x1)))
            3(3(x1)) -> 5(6(x1))
            3(4(x1)) -> 1(1(x1))
            4(4(x1)) -> 3(x1)
            5(5(x1)) -> 6(2(x1))
            5(6(x1)) -> 1(2(x1))
            6(6(x1)) -> 2(1(x1))
           graph:
            
           Qed