YES

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

Proof:
 Church Rosser Transformation Processor (to relative problem):
  strict:
   a(a(x)) -> a(b(a(x)))
   b(a(b(x))) -> a(c(a(x)))
  weak:
   
  original problem:
   a(a(x)) -> a(b(a(x)))
   b(a(b(x))) -> a(c(a(x)))
  critical peaks: 
   Matrix Interpretation Processor: dim=3
    
    interpretation:
               [1 0 0]  
     [c](x0) = [0 0 0]x0
               [0 0 0]  ,
     
               [1 1 0]     [0]
     [b](x0) = [0 0 0]x0 + [0]
               [0 0 0]     [1],
     
               [1 1 0]     [0]
     [a](x0) = [0 0 1]x0 + [0]
               [0 0 0]     [1]
    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 1 0]    [1]    [1 1 0]    [0]             
     b(a(b(x))) = [0 0 0]x + [0] >= [0 0 0]x + [0] = a(c(a(x)))
                  [0 0 0]    [1]    [0 0 0]    [1]             
    problem:
     strict:
      a(a(x)) -> a(b(a(x)))
     weak:
      
     original problem:
      a(a(x)) -> a(b(a(x)))
      b(a(b(x))) -> a(c(a(x)))
    Bounds Processor:
     bound: 2
     enrichment: match-rt
     automaton:
      final states: {3}
      transitions:
       b2(19) -> 20*
       b0(3) -> 3*
       a1(10) -> 11*
       a1(8) -> 9*
       b1(12) -> 13*
       b1(9) -> 10*
       a2(20) -> 21*
       a2(18) -> 19*
       a0(3) -> 3*
       3 -> 8*
       10 -> 18*
       11 -> 9,12,3
       13 -> 10*
       21 -> 9*
     problem:
      strict:
       
      weak:
       
      original problem:
       a(a(x)) -> a(b(a(x)))
       b(a(b(x))) -> a(c(a(x)))
     KH confluence processor
      Split input TRS into two TRSs S and T:
      
      TRS S:
       a(a(x)) -> a(b(a(x)))
      
      TRS T:
       b(a(b(x))) -> a(c(a(x)))
      
      As established above, T/S is terminating.
      T is strongly non-overlapping on S and S is strongly non-overlapping on T
      
       We get the following critical pairs, which are also S-critical pairs:
      
      b(a(a(c(a(x29))))) = a(c(a(a(b(x29)))))
      
       all these critical pairs are joinable with S union T.
      
      Please install theorem prover 'Prover9' and 'Mace4' for handling more TRSs.
      
       All S-critical pairs are joinable.
      
      We have to check confluence of S.
      
      Church Rosser Transformation Processor (kb):
       a(a(x)) -> a(b(a(x)))
       critical peaks: joinable
       DP Processor:
        DPs:
         a#(a(x)) -> a#(b(a(x)))
        TRS:
         a(a(x)) -> a(b(a(x)))
        EDG Processor:
         DPs:
          a#(a(x)) -> a#(b(a(x)))
         TRS:
          a(a(x)) -> a(b(a(x)))
         graph:
          
         SCC Processor:
          #sccs: 0
          #rules: 0
          #arcs: 0/1