Problem:
 a(f(x),y) -> f(a(f(y),x))
 a(b(x),y) -> a(x,b(x))
 a(g(x),x) -> g(b(g(x)))

Proof:
 Church Rosser Transformation Processor (to relative problem):
  strict:
   a(f(x),y) -> f(a(f(y),x))
   a(b(x),y) -> a(x,b(x))
   a(g(x),x) -> g(b(g(x)))
  weak:
   
  original problem:
   a(f(x),y) -> f(a(f(y),x))
   a(b(x),y) -> a(x,b(x))
   a(g(x),x) -> g(b(g(x)))
  critical peaks: 
   Matrix Interpretation Processor: dim=2
    
    interpretation:
               [1 0]     [1]
     [g](x0) = [0 0]x0 + [0],
     
               [1 0]     [0]
     [b](x0) = [2 2]x0 + [1],
     
                   [1 1]     [2 0]     [1]
     [a](x0, x1) = [1 1]x0 + [2 0]x1 + [2],
     
               [1 0]     [0]
     [f](x0) = [1 0]x0 + [1]
    orientation:
                 [2 0]    [2 0]    [2]    [2 0]    [2 0]    [2]               
     a(f(x),y) = [2 0]x + [2 0]y + [3] >= [2 0]x + [2 0]y + [3] = f(a(f(y),x))
     
                 [3 2]    [2 0]    [2]    [3 1]    [1]            
     a(b(x),y) = [3 2]x + [2 0]y + [3] >= [3 1]x + [2] = a(x,b(x))
     
                 [3 0]    [2]    [1 0]    [2]             
     a(g(x),x) = [3 0]x + [3] >= [0 0]x + [0] = g(b(g(x)))
    problem:
     strict:
      a(f(x),y) -> f(a(f(y),x))
      a(g(x),x) -> g(b(g(x)))
     weak:
      
     original problem:
      a(f(x),y) -> f(a(f(y),x))
      a(b(x),y) -> a(x,b(x))
      a(g(x),x) -> g(b(g(x)))
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [g](x0) = x0 + 4,
      
      [b](x0) = x0 + 4,
      
      [a](x0, x1) = 2x0 + 2x1 + 6,
      
      [f](x0) = x0
     orientation:
      a(f(x),y) = 2x + 2y + 6 >= 2x + 2y + 6 = f(a(f(y),x))
      
      a(g(x),x) = 4x + 14 >= x + 12 = g(b(g(x)))
     problem:
      strict:
       a(f(x),y) -> f(a(f(y),x))
      weak:
       
      original problem:
       a(f(x),y) -> f(a(f(y),x))
       a(b(x),y) -> a(x,b(x))
       a(g(x),x) -> g(b(g(x)))
     KH confluence processor
      Split input TRS into two TRSs S and T:
      
      TRS S:
       a(f(x),y) -> f(a(f(y),x))
      
      TRS T:
       a(b(x),y) -> a(x,b(x))
       a(g(x),x) -> g(b(g(x)))
      
      As established above, T/S is terminating.
      T is strongly non-overlapping on S and S is strongly non-overlapping on 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 (no redundant rules):
       strict:
        a(f(x),y) -> f(a(f(y),x))
       weak:
        
       critical peaks: 0
       Closedness Processor (*feeble*):
        
        Qed