YES (ignored inputs)COMMENT [11] Example 3.4.23 submitted by: Takahito Aoto , Junichi Yoshida , and Yoshihito Toyama Input: [ f(a) -> b, f(a) -> f(c), a -> d, f(d) -> b, f(c) -> b, d -> c ] Make it flat: [ f(a) -> b, f(a) -> f(c), a -> d, f(d) -> b, f(c) -> b, d -> c ] Time: 0.000 [s] Make it Complete (R^): [ f(a) = b, f(a) = f(c), f(a) = f(d), a = c, a = d, f(d) = f(c), f(d) = b, f(c) = b, d = c ] Time: 0.001 [s] CPNF: [ b … b, a … c ] 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.001 [s] problems/40.trs: Success(UNC) real 0.02 user 0.01 sys 0.00