YES

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

Proof:
 AT confluence processor
  Complete TRS T' of input TRS:
  a(a(x)) -> a(b(a(x)))
  b(a(b(x))) -> a(c(a(x)))
  
   T' = (P union S) with
  
   TRS P:
  
   TRS S:a(a(x)) -> a(b(a(x)))
         b(a(b(x))) -> a(c(a(x)))
  
  S is linear and P is reversible.
  
   CP(S,S) = 
  a(a(b(a(x23)))) = a(b(a(a(x23)))), b(a(a(c(a(x24))))) = a(c(a(a(b(x24)))))
  
   CP(S,P union P^-1) = 
  
   CP(P union P^-1,S) = 
  
  
  We have to check termination of S:
  
  Matrix Interpretation Processor: dim=3
   
   interpretation:
              [1 0 1]     [0]
    [b](x0) = [0 0 0]x0 + [1]
              [0 0 0]     [0],
    
              [1 0 1]     [0]
    [a](x0) = [0 0 0]x0 + [1]
              [0 1 0]     [0],
    
              [1 0 0]  
    [c](x0) = [0 0 0]x0
              [0 0 0]  
   orientation:
              [1 1 1]    [0]    [1 1 1]    [0]             
    a(a(x)) = [0 0 0]x + [1] >= [0 0 0]x + [1] = a(b(a(x)))
              [0 0 0]    [1]    [0 0 0]    [1]             
    
                 [1 0 1]    [1]    [1 0 1]    [0]             
    b(a(b(x))) = [0 0 0]x + [1] >= [0 0 0]x + [1] = a(c(a(x)))
                 [0 0 0]    [0]    [0 0 0]    [0]             
   problem:
    a(a(x)) -> a(b(a(x)))
   Matrix Interpretation Processor: dim=2
    
    interpretation:
               [2 0]     [2]
     [b](x0) = [0 0]x0 + [0],
     
               [1 1]     [0]
     [a](x0) = [1 1]x0 + [3]
    orientation:
               [2 2]    [3]    [2 2]    [2]             
     a(a(x)) = [2 2]x + [6] >= [2 2]x + [5] = a(b(a(x)))
    problem:
     
    Qed