YES

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

Proof:
 Church Rosser Transformation Processor:
  b(x75) -> c(x75)
  c(c(x79)) -> x79
  a(x81) -> x81
  critical peaks: joinable
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [b](x0) = x0,
    
    [a](x0) = x0 + 1,
    
    [c](x0) = x0
   orientation:
    b(x75) = x75 >= x75 = c(x75)
    
    c(c(x79)) = x79 >= x79 = x79
    
    a(x81) = x81 + 1 >= x81 = x81
   problem:
    b(x75) -> c(x75)
    c(c(x79)) -> x79
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [b](x0) = 4x0 + 4,
     
     [c](x0) = 2x0 + 4
    orientation:
     b(x75) = 4x75 + 4 >= 2x75 + 4 = c(x75)
     
     c(c(x79)) = 4x79 + 12 >= x79 = x79
    problem:
     b(x75) -> c(x75)
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [b](x0) = 4x0 + 1,
      
      [c](x0) = 4x0
     orientation:
      b(x75) = 4x75 + 1 >= 4x75 = c(x75)
     problem:
      
     Qed