YES

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

Proof:
 AT confluence processor
  Complete TRS T' of input TRS:
  a(s(x)) -> s(a(x))
  b(a(b(s(x)))) -> a(b(s(a(x))))
  b(a(b(b(x)))) -> a(b(a(b(x))))
  a(b(a(a(x)))) -> b(a(b(a(x))))
  
   T' = (P union S) with
  
   TRS P:
  
   TRS S:a(s(x)) -> s(a(x))
         b(a(b(s(x)))) -> a(b(s(a(x))))
         b(a(b(b(x)))) -> a(b(a(b(x))))
         a(b(a(a(x)))) -> b(a(b(a(x))))
  
  S is linear and P is reversible.
  
   CP(S,S) = 
  a(b(a(s(a(x117))))) = b(a(b(a(s(x117))))), b(a(b(a(b(s(a(x118))))))) = 
  a(b(a(b(a(b(s(x118))))))), b(a(b(a(b(a(b(x119))))))) = a(b(a(b(a(b(b(x119))))))), 
  a(b(a(b(a(b(a(x120))))))) = b(a(b(a(b(a(a(x120)))))))
  
   CP(S,P union P^-1) = 
  
   CP(P union P^-1,S) = 
  
  
  We have to check termination of S:
  
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [a](x0) = 2x0 + 1,
    
    [s](x0) = 2x0 + 2,
    
    [b](x0) = 2x0 + 1
   orientation:
    a(s(x)) = 4x + 5 >= 4x + 4 = s(a(x))
    
    b(a(b(s(x)))) = 16x + 23 >= 16x + 19 = a(b(s(a(x))))
    
    b(a(b(b(x)))) = 16x + 15 >= 16x + 15 = a(b(a(b(x))))
    
    a(b(a(a(x)))) = 16x + 15 >= 16x + 15 = b(a(b(a(x))))
   problem:
    b(a(b(b(x)))) -> a(b(a(b(x))))
    a(b(a(a(x)))) -> b(a(b(a(x))))
   String Reversal Processor:
    b(b(a(b(x)))) -> b(a(b(a(x))))
    a(a(b(a(x)))) -> a(b(a(b(x))))
    Bounds Processor:
     bound: 0
     enrichment: match
     automaton:
      final states: {6,1}
      transitions:
       a0(7) -> 8*
       a0(4) -> 5*
       a0(9) -> 6*
       a0(2) -> 3*
       f30() -> 2*
       b0(3) -> 4*
       b0(2) -> 7*
       b0(8) -> 9*
       b0(5) -> 1*
       6 -> 3*
       1 -> 7*
     problem:
      
     Qed