MAYBE

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

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