YES
(ignored inputs)COMMENT doi:10.1007/3-540-61064-2_39 [10] Example 7 submitted by: Takahito Aoto , Junichi Yoshida , and Yoshihito Toyama
Input:
   [ f(a,b) -> c,
     a -> a',
     b -> b',
     c -> f(a',b),
     c -> f(a,b'),
     c -> f(a,b) ]

Make it flat:
   [ f(a,b) -> c,
     a -> a',
     b -> b',
     c -> f(a',b),
     c -> f(a,b'),
     c -> f(a,b) ]
Time: 0.000 [s]

Make it Complete (R^):
   [ f(a,b) = c,
     a = a',
     f(a,b) = f(a',b),
     f(a',b') = c,
     f(a,b) = f(a,b'),
     f(a,b) = f(a',b'),
     f(a',b') = f(a',b),
     f(a',b') = f(a,b'),
     b = b',
     f(a',b) = f(a,b'),
     c = f(a',b),
     c = f(a,b') ]
Time: 0.002 [s]

CPNF:
   [ c … f(a',b'),
     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.002 [s]

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