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:
     
    weak:
     
    critical peaks: 0
    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) = x0 + 1,
      
      [G](x0) = x0
     orientation:
      F(x,A(G(x))) = 2x + 1 >= 2x = G(F(x,x))
      
      F(x,G(x)) = 2x >= 2x = G(F(x,x))
      
      A(x) = x + 1 >= x = x
     problem:
      F(x,G(x)) -> G(F(x,x))
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [F](x0, x1) = x0 + 2x1 + 2,
       
       [G](x0) = x0 + 4
      orientation:
       F(x,G(x)) = 3x + 10 >= 3x + 6 = G(F(x,x))
      problem:
       
      Qed