MAYBE

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

Proof:
 RT Transformation Processor:
  strict:
   a(a(b(x1))) -> b(a(b(c(a(x1)))))
   b(a(x1)) -> a(b(b(x1)))
   b(c(a(x1))) -> c(a(b(x1)))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 2
   interpretation:
              [1 0]     [1]
    [c](x0) = [0 0]x0 + [3],
    
              [1 6]     [1]
    [a](x0) = [0 0]x0 + [4],
    
                
    [b](x0) = x0
   orientation:
                  [1 6]     [26]    [1 6]     [21]                    
    a(a(b(x1))) = [0 0]x1 + [4 ] >= [0 0]x1 + [4 ] = b(a(b(c(a(x1)))))
    
               [1 6]     [1]    [1 6]     [1]              
    b(a(x1)) = [0 0]x1 + [4] >= [0 0]x1 + [4] = a(b(b(x1)))
    
                  [1 6]     [2]    [1 6]     [2]              
    b(c(a(x1))) = [0 0]x1 + [3] >= [0 0]x1 + [3] = c(a(b(x1)))
   problem:
    strict:
     b(a(x1)) -> a(b(b(x1)))
     b(c(a(x1))) -> c(a(b(x1)))
    weak:
     a(a(b(x1))) -> b(a(b(c(a(x1)))))
   Open