Problem:
 F(c(x)) -> G(x)
 G(x) -> F(x)
 c(x) -> x

Proof:
 Church Rosser Transformation Processor (kb):
  F(c(x)) -> G(x)
  G(x) -> F(x)
  c(x) -> 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]  
    [F](x0) = [0 0 0]x0
              [0 0 0]  ,
    
                   [1]
    [c](x0) = x0 + [0]
                   [0]
   orientation:
              [1 0 0]    [1]    [1 0 0]        
    F(c(x)) = [0 0 0]x + [0] >= [0 0 0]x = G(x)
              [0 0 0]    [0]    [0 0 0]        
    
           [1 0 0]     [1 0 0]        
    G(x) = [0 0 0]x >= [0 0 0]x = F(x)
           [0 0 0]     [0 0 0]        
    
               [1]         
    c(x) = x + [0] >= x = x
               [0]         
   problem:
    G(x) -> F(x)
   Matrix Interpretation Processor: dim=3
    
    interpretation:
               [1 0 0]     [1]
     [G](x0) = [0 0 0]x0 + [0]
               [0 0 0]     [0],
     
               [1 0 0]  
     [F](x0) = [0 0 0]x0
               [0 0 0]  
    orientation:
            [1 0 0]    [1]    [1 0 0]        
     G(x) = [0 0 0]x + [0] >= [0 0 0]x = F(x)
            [0 0 0]    [0]    [0 0 0]        
    problem:
     
    Qed