YES
(ignored inputs)COMMENT [20] Example 4.2.2 submitted by: Takahito Aoto , Junichi Yoshida , and Yoshihito Toyama
Input:
   [ F(?x,?y) -> c(?y),
     G(?x) -> ?x,
     f(?x) -> g(?x),
     g(?x) -> c(?x) ]

Make it flat:
   [ F(?x,?y) -> c(?y),
     G(?x) -> ?x,
     f(?x) -> g(?x),
     g(?x) -> c(?x) ]
Time: 0.000 [s]

Make it Complete (R^):
   [ F(?x,?y) = g(?y),
     F(?x,?y) = f(?y),
     F(?x,?y) = F(?x_1,?y),
     F(?x,?y) = c(?y),
     G(?x) = ?x,
     f(?x) = c(?x),
     f(?x) = g(?x),
     g(?x) = c(?x) ]
Time: 0.002 [s]

The number of normal forms that must be checked: 4
Time: 0.000 [s]

Now checking all the pairs...

Time to check pairs: 0.000 [s]

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

problems/71.trs: Success(UNC)
real 0.02
user 0.02
sys 0.00