YES(?,O(n^2))

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

Proof:
 Matrix Interpretation Processor:
  dimension: 2
  interpretation:
             [1 4]     [10]
   [a](x0) = [0 1]x0 + [13],
   
             [1 3]     [0]
   [b](x0) = [0 1]x0 + [9],
   
             [1 1]     [0]
   [c](x0) = [0 1]x0 + [4]
  orientation:
              [1 4]     [12]    [1 4]     [10]        
   b(c(x1)) = [0 1]x1 + [13] >= [0 1]x1 + [13] = a(x1)
   
              [1 6]     [27]    [1 5]     [26]           
   b(b(x1)) = [0 1]x1 + [18] >= [0 1]x1 + [17] = a(c(x1))
   
           [1 4]     [10]    [1 4]     [9 ]           
   a(x1) = [0 1]x1 + [13] >= [0 1]x1 + [13] = c(b(x1))
   
                 [1 3]     [12]    [1 3]     [0]        
   c(c(c(x1))) = [0 1]x1 + [12] >= [0 1]x1 + [9] = b(x1)
  problem:
   
  Qed