MAYBE
(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) ]
Try persistent and layer-preserving decomposition...
Sort Assignment:
 A : =>21
 B : =>17
 F : 21*21=>15
 G : 17*17=>15
 A' : =>21
 B' : =>17
maximal types: {15,17,21}
...decomposition failed.
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) ]
unknown Non-Omega-Overlapping
unknown Right-Reducible
Check distinct normal forms in critical pair closure...failed
Obtained TRSs:
   [ 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) ]
unknown UNC Completion (General)
Check distinct normal forms in critical pair closure...failed
problems/49.trs: Failure(unknown UNC)
(0 msec.)