MAYBE

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:
 RT Transformation Processor:
  strict:
   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))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [5](x0) = x0 + 17,
    
    [6](x0) = x0 + 5,
    
    [2](x0) = x0 + 6,
    
    [4](x0) = x0 + 7,
    
    [3](x0) = x0 + 5,
    
    [1](x0) = x0
   orientation:
    1(1(x1)) = x1 >= x1 + 12 = 4(3(x1))
    
    1(2(x1)) = x1 + 6 >= x1 + 6 = 2(1(x1))
    
    2(2(x1)) = x1 + 12 >= x1 = 1(1(1(x1)))
    
    3(3(x1)) = x1 + 10 >= x1 + 22 = 5(6(x1))
    
    3(4(x1)) = x1 + 12 >= x1 = 1(1(x1))
    
    4(4(x1)) = x1 + 14 >= x1 + 5 = 3(x1)
    
    5(5(x1)) = x1 + 34 >= x1 + 11 = 6(2(x1))
    
    5(6(x1)) = x1 + 22 >= x1 + 6 = 1(2(x1))
    
    6(6(x1)) = x1 + 10 >= x1 + 6 = 2(1(x1))
   problem:
    strict:
     1(1(x1)) -> 4(3(x1))
     1(2(x1)) -> 2(1(x1))
     3(3(x1)) -> 5(6(x1))
    weak:
     2(2(x1)) -> 1(1(1(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:
    dimension: 1
    interpretation:
     [5](x0) = x0,
     
     [6](x0) = x0,
     
     [2](x0) = x0,
     
     [4](x0) = x0 + 3,
     
     [3](x0) = x0 + 2,
     
     [1](x0) = x0
    orientation:
     1(1(x1)) = x1 >= x1 + 5 = 4(3(x1))
     
     1(2(x1)) = x1 >= x1 = 2(1(x1))
     
     3(3(x1)) = x1 + 4 >= x1 = 5(6(x1))
     
     2(2(x1)) = x1 >= x1 = 1(1(1(x1)))
     
     3(4(x1)) = x1 + 5 >= x1 = 1(1(x1))
     
     4(4(x1)) = x1 + 6 >= x1 + 2 = 3(x1)
     
     5(5(x1)) = x1 >= x1 = 6(2(x1))
     
     5(6(x1)) = x1 >= x1 = 1(2(x1))
     
     6(6(x1)) = x1 >= x1 = 2(1(x1))
    problem:
     strict:
      1(1(x1)) -> 4(3(x1))
      1(2(x1)) -> 2(1(x1))
     weak:
      3(3(x1)) -> 5(6(x1))
      2(2(x1)) -> 1(1(1(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))
    Open