YES(?,O(n^2))

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

Proof:
 Matrix Interpretation Processor:
  dimension: 2
  interpretation:
             [1 6]     [1]
   [b](x0) = [0 1]x0 + [2],
   
             [1 7]     [2]
   [d](x0) = [0 1]x0 + [3],
   
             [1 3]     [0]
   [c](x0) = [0 1]x0 + [1],
   
             [1 5]     [0]
   [a](x0) = [0 1]x0 + [2]
  orientation:
              [1  10]     [10]    [1  10]     [9]           
   a(a(x1)) = [0  1 ]x1 + [4 ] >= [0  1 ]x1 + [4] = d(c(x1))
   
              [1  11]     [11]    [1 9]     [9]              
   a(b(x1)) = [0  1 ]x1 + [4 ] >= [0 1]x1 + [3] = c(c(c(x1)))
   
              [1  12]     [14]    [1  11]     [13]              
   b(b(x1)) = [0  1 ]x1 + [4 ] >= [0  1 ]x1 + [4 ] = a(c(c(x1)))
   
              [1 6]     [3]    [1 6]     [1]        
   c(c(x1)) = [0 1]x1 + [2] >= [0 1]x1 + [2] = b(x1)
   
              [1  10]     [11]    [1  10]     [10]           
   c(d(x1)) = [0  1 ]x1 + [4 ] >= [0  1 ]x1 + [4 ] = a(a(x1))
   
              [1  14]     [25]    [1  14]     [24]              
   d(d(x1)) = [0  1 ]x1 + [6 ] >= [0  1 ]x1 + [5 ] = b(a(c(x1)))
  problem:
   
  Qed