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 TRS:
   [ 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) ]
TRS:
   [ 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) ]
confluent TRS:
   [ 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),
     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) ]
UNC Completion (Development Closed)
problems/49.trs: Success(UNC)
(4 msec.)