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 + 6,
      
      [a](x0) = x0 + 1
     orientation:
      f(a(x),x) = 2x + 7 >= 2x + 7 = f(x,a(x))
      
      f(b(x),x) = 2x + 6 >= 2x + 6 = f(x,b(x))
      
      a(x) = x + 1 >= 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) = 4x0 + 1,
       
       [f](x0, x1) = 5x0 + 4x1,
       
       [a](x0) = x0
      orientation:
       f(a(x),x) = 9x >= 9x = f(x,a(x))
       
       f(b(x),x) = 24x + 5 >= 21x + 4 = f(x,b(x))
      problem:
       f(a(x),x) -> f(x,a(x))
      Matrix Interpretation Processor: dim=1
       
       interpretation:
        [f](x0, x1) = 2x0 + x1 + 1,
        
        [a](x0) = 2x0 + 1
       orientation:
        f(a(x),x) = 5x + 3 >= 4x + 2 = f(x,a(x))
       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:
      g(b(x),y) -> g(a(a(x)),y)
      g(c(x),y) -> y
      a(x) -> b(x)
     weak:
      
     critical peaks: 0
     Closedness Processor (*parallel*):
      
      strict:
       
      weak:
       
      Qed