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

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