NO
(ignored inputs)COMMENT [11] Example 3.3.2 submitted by: Takahito Aoto , Junichi Yoshida , and Yoshihito Toyama
Input:
   [ f(b) -> a,
     f(b) -> f(c),
     f(c) -> f(b),
     f(c) -> d,
     b -> e,
     c -> e',
     f(e) -> a,
     f(e') -> d ]

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

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

The number of normal forms that must be checked: 30
Time: 0.001 [s]

Now checking all the pairs...

Time to check pairs: 0.000 [s]

The TRS doesn't have Uniqueness of Normal Forms.
Counter Example: 
     f(f(f(f(f(f(a))))))
<->* f(f(f(f(f(f(d))))))

proof:
     f(f(f(f(f(f(a))))))

     f(f(f(f(f(f(d))))))
->R^ f(f(f(f(f(f(a))))))
Total Time: 0.004 [s]

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