Problem:
 F(x,A(G(x))) -> G(F(x,x))
 F(x,G(x)) -> G(F(x,x))
 A(x) -> x
 H(x) -> H(B(H(x)))

Proof:
 sorted: (order)
 0:H(x) -> H(B(H(x)))
 1:F(x,A(G(x))) -> G(F(x,x))
   F(x,G(x)) -> G(F(x,x))
   A(x) -> x
 -----
 sorts
   []
 sort attachment (non-strict)
   F : 2 x 2 -> 2
   A : 2 -> 2
   G : 2 -> 2
   H : 1 -> 1
   B : 1 -> 1
 -----
 0:H(x) -> H(B(H(x)))
   Church Rosser Transformation Processor:
    
    strict:
     H(x) -> H(B(H(x)))
    weak:
     
    critical peaks: 0
    Closedness Processor (*parallel*):
     
     strict:
      
     weak:
      
     Qed
 
 
 1:F(x,A(G(x))) -> G(F(x,x))
   F(x,G(x)) -> G(F(x,x))
   A(x) -> x
   Church Rosser Transformation Processor (kb):
    F(x,A(G(x))) -> G(F(x,x))
    F(x,G(x)) -> G(F(x,x))
    A(x) -> x
    critical peaks: joinable
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [F](x0, x1) = x0 + x1,
      
      [A](x0) = 4x0 + 1,
      
      [G](x0) = x0
     orientation:
      F(x,A(G(x))) = 5x + 1 >= 2x = G(F(x,x))
      
      F(x,G(x)) = 2x >= 2x = G(F(x,x))
      
      A(x) = 4x + 1 >= x = x
     problem:
      F(x,G(x)) -> G(F(x,x))
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [F](x0, x1) = 2x0 + 4x1,
       
       [G](x0) = x0 + 6
      orientation:
       F(x,G(x)) = 6x + 24 >= 6x + 6 = G(F(x,x))
      problem:
       
      Qed