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

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