YES
(ignored inputs)COMMENT doi:10.1145/322217.322230 [12] p. 814 , attributed to Levy submitted by: Takahito Aoto , Junichi Yoshida , and Yoshihito Toyama
Input:
   [ 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) ]

Make it flat:
   [ 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) ]
Time: 0.000 [s]

Make it Complete (R^):
   [ 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'),
     G(B,B') = F(A',A'),
     G(B',B) = F(A',A'),
     F(A',A) = G(B',B'),
     G(B',B) = F(A,A'),
     F(A',A) = G(B',B),
     G(B,B') = F(A',A),
     G(B,B') = F(A,A'),
     F(A,A') = G(B',B'),
     F(A',A') = G(B',B'),
     G(B,B) = F(A',A'),
     F(A,A) = G(B,B),
     F(?x,A) = F(?x,?x),
     F(A,?x) = F(?x,?x),
     F(?x,A) = F(A',?x),
     F(?x,A) = F(?x,A'),
     F(?x,A) = F(A,?x),
     F(A,A') = F(A',A'),
     F(A,?x) = F(A',?x),
     F(A,A) = F(A',A'),
     F(A,A) = F(A,A'),
     F(A,A) = F(A',A),
     F(A,A') = F(A',A),
     F(A',A') = F(A',A),
     F(A,?x) = F(?x,A'),
     A = A',
     F(A',?x) = F(?x,A'),
     F(A',?x) = F(?x,?x),
     F(?x,A') = F(?x,?x),
     G(?x,B) = G(?x,?x),
     G(B,?x) = G(?x,?x),
     G(?x,B) = G(B',?x),
     G(?x,B) = G(?x,B'),
     G(?x,B) = G(B,?x),
     G(B,B') = G(B',B'),
     G(B,?x) = G(B',?x),
     G(B,B) = G(B',B'),
     G(B,B) = G(B,B'),
     G(B,B) = G(B',B),
     G(B,B') = G(B',B),
     G(B',B') = G(B',B),
     G(B,?x) = G(?x,B'),
     B = B',
     G(B',?x) = G(?x,B'),
     G(B',?x) = G(?x,?x),
     G(?x,B') = G(?x,?x) ]
Time: 0.054 [s]

CPNF:
   [ A … A',
     B … B' ]
Time: 0.000 [s]

Now checking all the pairs in CW...

Time to check pairs: 0.000 [s]

The TRS has Uniqueness of Normal Forms.
Total Time: 0.055 [s]

problems/49.trs: Success(UNC)
real 0.07
user 0.06
sys 0.01