MAYBE

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

Proof:
 RT Transformation Processor:
  strict:
   a(a(b(x1))) -> c(d(x1))
   b(e(b(x1))) -> e(d(x1))
   b(d(x1)) -> e(b(x1))
   b(b(b(x1))) -> e(e(x1))
   e(e(e(x1))) -> d(e(x1))
   d(x1) -> b(e(x1))
   c(d(a(x1))) -> c(x1)
   d(c(x1)) -> c(d(a(x1)))
   a(x1) -> e(b(x1))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [e](x0) = x0 + 5,
    
    [c](x0) = x0,
    
    [d](x0) = x0,
    
    [a](x0) = x0 + 21,
    
    [b](x0) = x0 + 10
   orientation:
    a(a(b(x1))) = x1 + 52 >= x1 = c(d(x1))
    
    b(e(b(x1))) = x1 + 25 >= x1 + 5 = e(d(x1))
    
    b(d(x1)) = x1 + 10 >= x1 + 15 = e(b(x1))
    
    b(b(b(x1))) = x1 + 30 >= x1 + 10 = e(e(x1))
    
    e(e(e(x1))) = x1 + 15 >= x1 + 5 = d(e(x1))
    
    d(x1) = x1 >= x1 + 15 = b(e(x1))
    
    c(d(a(x1))) = x1 + 21 >= x1 = c(x1)
    
    d(c(x1)) = x1 >= x1 + 21 = c(d(a(x1)))
    
    a(x1) = x1 + 21 >= x1 + 15 = e(b(x1))
   problem:
    strict:
     b(d(x1)) -> e(b(x1))
     d(x1) -> b(e(x1))
     d(c(x1)) -> c(d(a(x1)))
    weak:
     a(a(b(x1))) -> c(d(x1))
     b(e(b(x1))) -> e(d(x1))
     b(b(b(x1))) -> e(e(x1))
     e(e(e(x1))) -> d(e(x1))
     c(d(a(x1))) -> c(x1)
     a(x1) -> e(b(x1))
   Matrix Interpretation Processor:
    dimension: 1
    interpretation:
     [e](x0) = x0 + 4,
     
     [c](x0) = x0,
     
     [d](x0) = x0 + 5,
     
     [a](x0) = x0 + 18,
     
     [b](x0) = x0 + 9
    orientation:
     b(d(x1)) = x1 + 14 >= x1 + 13 = e(b(x1))
     
     d(x1) = x1 + 5 >= x1 + 13 = b(e(x1))
     
     d(c(x1)) = x1 + 5 >= x1 + 23 = c(d(a(x1)))
     
     a(a(b(x1))) = x1 + 45 >= x1 + 5 = c(d(x1))
     
     b(e(b(x1))) = x1 + 22 >= x1 + 9 = e(d(x1))
     
     b(b(b(x1))) = x1 + 27 >= x1 + 8 = e(e(x1))
     
     e(e(e(x1))) = x1 + 12 >= x1 + 9 = d(e(x1))
     
     c(d(a(x1))) = x1 + 23 >= x1 = c(x1)
     
     a(x1) = x1 + 18 >= x1 + 13 = e(b(x1))
    problem:
     strict:
      d(x1) -> b(e(x1))
      d(c(x1)) -> c(d(a(x1)))
     weak:
      b(d(x1)) -> e(b(x1))
      a(a(b(x1))) -> c(d(x1))
      b(e(b(x1))) -> e(d(x1))
      b(b(b(x1))) -> e(e(x1))
      e(e(e(x1))) -> d(e(x1))
      c(d(a(x1))) -> c(x1)
      a(x1) -> e(b(x1))
    Arctic Interpretation Processor:
     dimension: 2
     interpretation:
                [0  -&]  
      [e](x0) = [-& -&]x0,
      
                [0  -&]  
      [c](x0) = [3  1 ]x0,
      
                [0  1 ]  
      [d](x0) = [-& 4 ]x0,
      
                [3  1 ]  
      [a](x0) = [0  -&]x0,
      
                [0  1 ]  
      [b](x0) = [-& 4 ]x0
     orientation:
              [0  1 ]      [0  -&]             
      d(x1) = [-& 4 ]x1 >= [-& -&]x1 = b(e(x1))
      
                 [4 2]      [3 1]                
      d(c(x1)) = [7 5]x1 >= [6 4]x1 = c(d(a(x1)))
      
                 [0  5 ]      [0  1 ]             
      b(d(x1)) = [-& 8 ]x1 >= [-& -&]x1 = e(b(x1))
      
                    [6 8]      [0 1]             
      a(a(b(x1))) = [3 5]x1 >= [3 5]x1 = c(d(x1))
      
                    [0  1 ]      [0  1 ]             
      b(e(b(x1))) = [-& -&]x1 >= [-& -&]x1 = e(d(x1))
      
                    [0  9 ]      [0  -&]             
      b(b(b(x1))) = [-& 12]x1 >= [-& -&]x1 = e(e(x1))
      
                    [0  -&]      [0  -&]             
      e(e(e(x1))) = [-& -&]x1 >= [-& -&]x1 = d(e(x1))
      
                    [3 1]      [0  -&]          
      c(d(a(x1))) = [6 4]x1 >= [3  1 ]x1 = c(x1)
      
              [3  1 ]      [0  1 ]             
      a(x1) = [0  -&]x1 >= [-& -&]x1 = e(b(x1))
     problem:
      strict:
       d(x1) -> b(e(x1))
      weak:
       d(c(x1)) -> c(d(a(x1)))
       b(d(x1)) -> e(b(x1))
       a(a(b(x1))) -> c(d(x1))
       b(e(b(x1))) -> e(d(x1))
       b(b(b(x1))) -> e(e(x1))
       e(e(e(x1))) -> d(e(x1))
       c(d(a(x1))) -> c(x1)
       a(x1) -> e(b(x1))
     Open