YES(?,O(n^2))

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

Proof:
 Complexity Transformation Processor:
  strict:
   a(b(x1)) -> b(a(x1))
   b(a(x1)) -> a(a(c(b(x1))))
  weak:
   
  Bounds Processor:
   bound: 2
   enrichment: match
   automaton:
    final states: {4}
    transitions:
     b1(21) -> 22*
     b1(16) -> 17*
     a1(19) -> 20*
     a1(18) -> 19*
     c1(17) -> 18*
     a2(54) -> 55*
     a2(39) -> 40*
     a2(53) -> 54*
     a2(38) -> 39*
     a0(4) -> 4*
     c2(52) -> 53*
     c2(37) -> 38*
     b0(4) -> 4*
     b2(51) -> 52*
     b2(36) -> 37*
     c0(4) -> 4*
     4 -> 16*
     18 -> 51*
     19 -> 36,21
     20 -> 17,4
     22 -> 17*
     40 -> 17*
     55 -> 37,22
   problem:
    strict:
     a(b(x1)) -> b(a(x1))
    weak:
     b(a(x1)) -> a(a(c(b(x1))))
   Matrix Interpretation Processor:
    dimension: 2
    max_matrix:
     [1 1]
     [0 1]
     interpretation:
                [1 0]  
      [c](x0) = [0 0]x0,
      
                [1 1]  
      [a](x0) = [0 1]x0,
      
                [1 1]     [1]
      [b](x0) = [0 1]x0 + [1]
     orientation:
                 [1 2]     [2]    [1 2]     [1]           
      a(b(x1)) = [0 1]x1 + [1] >= [0 1]x1 + [1] = b(a(x1))
      
                 [1 2]     [1]    [1 1]     [1]                 
      b(a(x1)) = [0 1]x1 + [1] >= [0 0]x1 + [0] = a(a(c(b(x1))))
     problem:
      strict:
       
      weak:
       a(b(x1)) -> b(a(x1))
       b(a(x1)) -> a(a(c(b(x1))))
     Qed