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

Proof:
 sorted: (order)
 0:f(a(x),x) -> f(x,a(x))
   f(b(x),x) -> f(x,b(x))
   a(x) -> b(x)
 1:g(b(x),y) -> g(a(a(x)),y)
   g(c(x),y) -> y
   a(x) -> b(x)
 -----
 sorts
   [1>3, 2>4, 2>8, 3>7, 4>5, 4>7, 5>6]
 sort attachment (non-strict)
   f : 3 x 7 -> 1
   a : 7 -> 7
   b : 7 -> 7
   g : 4 x 8 -> 2
   c : 6 -> 5
 -----
 0:f(a(x),x) -> f(x,a(x))
   f(b(x),x) -> f(x,b(x))
   a(x) -> b(x)
   Church Rosser Transformation Processor (kb):
    f(a(x),x) -> f(x,a(x))
    f(b(x),x) -> f(x,b(x))
    a(x) -> b(x)
    critical peaks: joinable
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [b](x0) = x0,
      
      [f](x0, x1) = x0 + x1 + 4,
      
      [a](x0) = x0 + 3
     orientation:
      f(a(x),x) = 2x + 7 >= 2x + 7 = f(x,a(x))
      
      f(b(x),x) = 2x + 4 >= 2x + 4 = f(x,b(x))
      
      a(x) = x + 3 >= x = b(x)
     problem:
      f(a(x),x) -> f(x,a(x))
      f(b(x),x) -> f(x,b(x))
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [b](x0) = x0 + 1,
       
       [f](x0, x1) = 2x0 + x1 + 1,
       
       [a](x0) = x0
      orientation:
       f(a(x),x) = 3x + 1 >= 3x + 1 = f(x,a(x))
       
       f(b(x),x) = 3x + 3 >= 3x + 2 = f(x,b(x))
      problem:
       f(a(x),x) -> f(x,a(x))
      Matrix Interpretation Processor: dim=3
       
       interpretation:
                      [1 0 1]     [1 0 0]  
        [f](x0, x1) = [1 1 0]x0 + [1 1 0]x1
                      [0 0 1]     [0 0 1]  ,
        
                  [1 1 0]     [0]
        [a](x0) = [1 1 0]x0 + [0]
                  [0 0 1]     [1]
       orientation:
                    [2 1 1]    [1]    [2 1 1]    [0]            
        f(a(x),x) = [3 3 0]x + [0] >= [3 3 0]x + [0] = f(x,a(x))
                    [0 0 2]    [1]    [0 0 2]    [1]            
       problem:
        
       Qed
  
  
  1:g(b(x),y) -> g(a(a(x)),y)
    g(c(x),y) -> y
    a(x) -> b(x)
    Church Rosser Transformation Processor:
     
     strict:
      
     weak:
      
     critical peaks: 0
     Qed