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

Proof:
 Church Rosser Transformation Processor:
  strict:
   
  weak:
   
  critical peaks: 0
  Redundant Rules Transformation:
   F(x,x) -> A()
   G(x) -> F(x,G(x))
   C() -> G(C())
   G(C()) -> F(G(C()),G(C()))
   G(C()) -> F(C(),G(G(C())))
   C() -> F(C(),G(C()))
   C() -> G(G(C()))
   F(F(x,x),A()) -> A()
   F(A(),F(x,x)) -> A()
   F(C(),G(C())) -> A()
   F(G(C()),C()) -> A()
   Nonconfluence Processor:
    terms: G(A()) *<- G(C()) ->* A()
    Qed
    
    first automaton:
     final states: {1028}
     transitions:
      F(1029,1028) -> 1028*
      A() -> 1029*
      G(1029) -> 1028*
    
    second automaton:
     final states: {7}
     transitions:
      A() -> 7*