(ignored inputs)COMMENT due to Levy , from p.814 of \cite{Hue80}
Rewrite Rules:
   [ F(A,A) -> G(B,B),
     A -> A',
     F(A',?x) -> F(?x,?x),
     F(?x,A') -> F(?x,?x),
     G(B,B) -> F(A,A),
     B -> B',
     G(B',?x) -> G(?x,?x),
     G(?x,B') -> G(?x,?x) ]
Apply Direct Methods...
Inner CPs:
   [ F(A',A) = G(B,B),
     F(A,A') = G(B,B),
     G(B',B) = F(A,A),
     G(B,B') = F(A,A) ]
Outer CPs:
   [ F(A',A') = F(A',A'),
     G(B',B') = G(B',B') ]
not Overlay, check Termination...
unknown/not Terminating
unknown Knuth&Bendix
Left-Linear, not Right-Linear
unknown Development Closed
inner CP cond (upside-parallel)
innter CP Cond (outside)
unknown Upside-Parallel-Closed/Outside-Closed
(inner) Parallel CPs:
   [ F(A,A') = G(B,B) {},
     F(A',A) = G(B,B) {},
     F(A',A') = G(B,B) {},
     G(B,B') = F(A,A) {},
     G(B',B) = F(A,A) {},
     G(B',B') = F(A,A) {} ]
unknown Toyama (Parallel CPs)
Simultaneous CPs:
   [ G(B',B') = G(B',B'),
     F(A,A) = G(B,B'),
     F(A,A) = G(B',B),
     G(B,B') = F(A,A),
     G(B',B) = F(A,A),
     G(B',B') = F(A,A),
     F(A',A') = F(A',A'),
     G(B,B) = F(A,A'),
     G(B,B) = F(A',A),
     F(A,A') = G(B,B),
     F(A',A) = G(B,B),
     F(A',A') = G(B,B) ]
unknown Okui (Simultaneous CPs)
unknown Strongly Depth-Preserving & Non-E-Overlapping
check Locally Decreasing Diagrams by Rule Labelling...
Critical Pair <F(A',A), G(B,B)> by Rules <1, 0> preceded by [(F,1)]
 joinable by a reduction of rules <[([],2)], [([],4)]>
Critical Pair <F(A,A'), G(B,B)> by Rules <1, 0> preceded by [(F,2)]
 joinable by a reduction of rules <[([],3)], [([],4)]>
Critical Pair <G(B',B), F(A,A)> by Rules <5, 4> preceded by [(G,1)]
 joinable by a reduction of rules <[([],6)], [([],0)]>
Critical Pair <G(B,B'), F(A,A)> by Rules <5, 4> preceded by [(G,2)]
 joinable by a reduction of rules <[([],7)], [([],0)]>
Critical Pair <F(A',A'), F(A',A')> by Rules <3, 2> preceded by []
 joinable by a reduction of rules <[], []>
Critical Pair <G(B',B'), G(B',B')> by Rules <7, 6> preceded by []
 joinable by a reduction of rules <[], []>
unknown Diagram Decreasing
check by Reduction-Preserving Completion...
STEP: 1 (parallel)
S:
   [ A -> A',
     F(A',?x) -> F(?x,?x),
     F(?x,A') -> F(?x,?x),
     B -> B',
     G(B',?x) -> G(?x,?x),
     G(?x,B') -> G(?x,?x) ]
P:
   [ F(A,A) -> G(B,B),
     G(B,B) -> F(A,A) ]
S: unknown termination
failure(Step 1)
STEP: 2 (linear)
S:
   [ A -> A',
     F(A',?x) -> F(?x,?x),
     F(?x,A') -> F(?x,?x),
     B -> B',
     G(B',?x) -> G(?x,?x),
     G(?x,B') -> G(?x,?x) ]
P:
   [ F(A,A) -> G(B,B),
     G(B,B) -> F(A,A) ]
S: not linear
failure(Step 2)
STEP: 3 (relative)
S:
   [ A -> A',
     F(A',?x) -> F(?x,?x),
     F(?x,A') -> F(?x,?x),
     B -> B',
     G(B',?x) -> G(?x,?x),
     G(?x,B') -> G(?x,?x) ]
P:
   [ F(A,A) -> G(B,B),
     G(B,B) -> F(A,A) ]
Check relative termination:
   [ A -> A',
     F(A',?x) -> F(?x,?x),
     F(?x,A') -> F(?x,?x),
     B -> B',
     G(B',?x) -> G(?x,?x),
     G(?x,B') -> G(?x,?x) ]
   [ F(A,A) -> G(B,B),
     G(B,B) -> F(A,A) ]
unknown relative termination
S/P: unknown relative termination
failure(Step 3)
failure(no possibility remains)
unknown Reduction-Preserving Completion
check Non-Confluence...Find Non-Joinable CP reducts: <G(B',B'), F(A',A')> from G(B,B)
Not Confluent
Direct Methods: not CR

Final result: not CR
/local-scratch/hzankl/2012/cops2012/49.trs: Success(not CR)
(135 msec.)