MAYBE

Problem:
 c(c(c(b(x)))) -> a(1(),b(c(x)))
 b(c(b(c(x)))) -> a(0(),a(1(),x))
 a(0(),x) -> c(c(x))
 a(1(),x) -> c(b(x))

Proof:
 RT Transformation Processor:
  strict:
   c(c(c(b(x)))) -> a(1(),b(c(x)))
   b(c(b(c(x)))) -> a(0(),a(1(),x))
   a(0(),x) -> c(c(x))
   a(1(),x) -> c(b(x))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [0] = 25,
    
    [a](x0, x1) = x0 + x1 + 3,
    
    [1] = 6,
    
    [c](x0) = x0,
    
    [b](x0) = x0
   orientation:
    c(c(c(b(x)))) = x >= x + 9 = a(1(),b(c(x)))
    
    b(c(b(c(x)))) = x >= x + 37 = a(0(),a(1(),x))
    
    a(0(),x) = x + 28 >= x = c(c(x))
    
    a(1(),x) = x + 9 >= x = c(b(x))
   problem:
    strict:
     c(c(c(b(x)))) -> a(1(),b(c(x)))
     b(c(b(c(x)))) -> a(0(),a(1(),x))
    weak:
     a(0(),x) -> c(c(x))
     a(1(),x) -> c(b(x))
   Matrix Interpretation Processor:
    dimension: 1
    interpretation:
     [0] = 3,
     
     [a](x0, x1) = x0 + x1 + 1,
     
     [1] = 25,
     
     [c](x0) = x0,
     
     [b](x0) = x0 + 16
    orientation:
     c(c(c(b(x)))) = x + 16 >= x + 42 = a(1(),b(c(x)))
     
     b(c(b(c(x)))) = x + 32 >= x + 30 = a(0(),a(1(),x))
     
     a(0(),x) = x + 4 >= x = c(c(x))
     
     a(1(),x) = x + 26 >= x + 16 = c(b(x))
    problem:
     strict:
      c(c(c(b(x)))) -> a(1(),b(c(x)))
     weak:
      b(c(b(c(x)))) -> a(0(),a(1(),x))
      a(0(),x) -> c(c(x))
      a(1(),x) -> c(b(x))
    Open