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] CPNF: [ a … a, c … e', a … d ] Time: 0.000 [s] The TRS doesn't have Uniqueness of Normal Forms. Counter Example: a <->* d proof: a d ->R^ a Total Time: 0.002 [s] problems/39.trs: Success(not UNC) real 0.02 user 0.01 sys 0.01