YES(?,O(n^2))

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

Proof:
 RT Transformation Processor:
  strict:
   a(b(x1)) -> b(a(x1))
   b(a(x1)) -> a(c(b(x1)))
  weak:
   
  Bounds Processor:
   bound: 2
   enrichment: match-rt
   automaton:
    final states: {4}
    transitions:
     b1(15) -> 16*
     b1(19) -> 20*
     a1(17) -> 18*
     c1(16) -> 17*
     a2(36) -> 37*
     a0(4) -> 4*
     c2(35) -> 36*
     b0(4) -> 4*
     b2(34) -> 35*
     c0(4) -> 4*
     4 -> 15*
     17 -> 34,19
     18 -> 16,4
     20 -> 16*
     37 -> 16*
   problem:
    strict:
     a(b(x1)) -> b(a(x1))
    weak:
     b(a(x1)) -> a(c(b(x1)))
   Matrix Interpretation Processor:
    dimension: 2
    interpretation:
               [1 0]  
     [c](x0) = [0 0]x0,
     
               [1 1]     [9]
     [a](x0) = [0 1]x0 + [0],
     
                    [6]
     [b](x0) = x0 + [1]
    orientation:
                [1 1]     [16]    [1 1]     [15]           
     a(b(x1)) = [0 1]x1 + [1 ] >= [0 1]x1 + [1 ] = b(a(x1))
     
                [1 1]     [15]    [1 0]     [15]              
     b(a(x1)) = [0 1]x1 + [1 ] >= [0 0]x1 + [0 ] = a(c(b(x1)))
    problem:
     strict:
      
     weak:
      a(b(x1)) -> b(a(x1))
      b(a(x1)) -> a(c(b(x1)))
    Qed