MAYBE

Problem:
 a(d(x1)) -> d(b(x1))
 a(x1) -> b(b(b(x1)))
 d(x1) -> x1
 a(x1) -> x1
 b(d(b(x1))) -> a(d(x1))
 b(c(x1)) -> c(d(d(x1)))
 a(c(x1)) -> b(b(c(d(x1))))

Proof:
 RT Transformation Processor:
  strict:
   a(d(x1)) -> d(b(x1))
   a(x1) -> b(b(b(x1)))
   d(x1) -> x1
   a(x1) -> x1
   b(d(b(x1))) -> a(d(x1))
   b(c(x1)) -> c(d(d(x1)))
   a(c(x1)) -> b(b(c(d(x1))))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [c](x0) = x0 + 12,
    
    [b](x0) = x0 + 2,
    
    [a](x0) = x0,
    
    [d](x0) = x0 + 16
   orientation:
    a(d(x1)) = x1 + 16 >= x1 + 18 = d(b(x1))
    
    a(x1) = x1 >= x1 + 6 = b(b(b(x1)))
    
    d(x1) = x1 + 16 >= x1 = x1
    
    a(x1) = x1 >= x1 = x1
    
    b(d(b(x1))) = x1 + 20 >= x1 + 16 = a(d(x1))
    
    b(c(x1)) = x1 + 14 >= x1 + 44 = c(d(d(x1)))
    
    a(c(x1)) = x1 + 12 >= x1 + 32 = b(b(c(d(x1))))
   problem:
    strict:
     a(d(x1)) -> d(b(x1))
     a(x1) -> b(b(b(x1)))
     a(x1) -> x1
     b(c(x1)) -> c(d(d(x1)))
     a(c(x1)) -> b(b(c(d(x1))))
    weak:
     d(x1) -> x1
     b(d(b(x1))) -> a(d(x1))
   Matrix Interpretation Processor:
    dimension: 1
    interpretation:
     [c](x0) = x0 + 16,
     
     [b](x0) = x0 + 16,
     
     [a](x0) = x0 + 20,
     
     [d](x0) = x0 + 3
    orientation:
     a(d(x1)) = x1 + 23 >= x1 + 19 = d(b(x1))
     
     a(x1) = x1 + 20 >= x1 + 48 = b(b(b(x1)))
     
     a(x1) = x1 + 20 >= x1 = x1
     
     b(c(x1)) = x1 + 32 >= x1 + 22 = c(d(d(x1)))
     
     a(c(x1)) = x1 + 36 >= x1 + 51 = b(b(c(d(x1))))
     
     d(x1) = x1 + 3 >= x1 = x1
     
     b(d(b(x1))) = x1 + 35 >= x1 + 23 = a(d(x1))
    problem:
     strict:
      a(x1) -> b(b(b(x1)))
      a(c(x1)) -> b(b(c(d(x1))))
     weak:
      a(d(x1)) -> d(b(x1))
      a(x1) -> x1
      b(c(x1)) -> c(d(d(x1)))
      d(x1) -> x1
      b(d(b(x1))) -> a(d(x1))
    Arctic Interpretation Processor:
     dimension: 2
     interpretation:
                [2  -&]  
      [c](x0) = [1  -&]x0,
      
                [0  0 ]  
      [b](x0) = [-& 0 ]x0,
      
                [1 0]  
      [a](x0) = [0 0]x0,
      
                [0  -&]  
      [d](x0) = [1  4 ]x0
     orientation:
              [1 0]      [0  0 ]                
      a(x1) = [0 0]x1 >= [-& 0 ]x1 = b(b(b(x1)))
      
                 [3  -&]      [2  -&]                   
      a(c(x1)) = [2  -&]x1 >= [1  -&]x1 = b(b(c(d(x1))))
      
                 [1 4]      [0 0]             
      a(d(x1)) = [1 4]x1 >= [1 4]x1 = d(b(x1))
      
              [1 0]             
      a(x1) = [0 0]x1 >= x1 = x1
      
                 [2  -&]      [2  -&]                
      b(c(x1)) = [1  -&]x1 >= [1  -&]x1 = c(d(d(x1)))
      
              [0  -&]             
      d(x1) = [1  4 ]x1 >= x1 = x1
      
                    [1 4]      [1 4]             
      b(d(b(x1))) = [1 4]x1 >= [1 4]x1 = a(d(x1))
     problem:
      strict:
       a(x1) -> b(b(b(x1)))
      weak:
       a(c(x1)) -> b(b(c(d(x1))))
       a(d(x1)) -> d(b(x1))
       a(x1) -> x1
       b(c(x1)) -> c(d(d(x1)))
       d(x1) -> x1
       b(d(b(x1))) -> a(d(x1))
     Open