MAYBE

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

Proof:
 Complexity Transformation Processor:
  strict:
   a(a(b(x1))) -> b(a(b(x1)))
   b(a(x1)) -> a(b(b(x1)))
   b(c(a(x1))) -> c(c(a(a(b(x1)))))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [c](x0) = x0,
     
     [a](x0) = x0 + 1,
     
     [b](x0) = x0
    orientation:
     a(a(b(x1))) = x1 + 2 >= x1 + 1 = b(a(b(x1)))
     
     b(a(x1)) = x1 + 1 >= x1 + 1 = a(b(b(x1)))
     
     b(c(a(x1))) = x1 + 1 >= x1 + 2 = c(c(a(a(b(x1)))))
    problem:
     strict:
      b(a(x1)) -> a(b(b(x1)))
      b(c(a(x1))) -> c(c(a(a(b(x1)))))
     weak:
      a(a(b(x1))) -> b(a(b(x1)))
    Bounds Processor:
     bound: 1
     enrichment: match
     automaton:
      final states: {4}
      transitions:
       a1(40) -> 41*
       a1(20) -> 21*
       a1(21) -> 22*
       b1(57) -> 58*
       b1(42) -> 43*
       b1(39) -> 40*
       b1(19) -> 20*
       c1(22) -> 23*
       c1(23) -> 24*
       b0(4) -> 4*
       a0(4) -> 4*
       c0(4) -> 4*
       4 -> 19*
       20 -> 41,21,4,39
       21 -> 43,58,57
       24 -> 20,4
       40 -> 42*
       41 -> 40,20,4
       43 -> 20*
       58 -> 22*
     problem:
      strict:
       b(a(x1)) -> a(b(b(x1)))
      weak:
       b(c(a(x1))) -> c(c(a(a(b(x1)))))
       a(a(b(x1))) -> b(a(b(x1)))
     Open