NO
(ignored inputs)COMMENT [11] Example 3.3.2 submitted by: Takahito Aoto , Junichi Yoshida , and Yoshihito Toyama
input TRS:
   [ f(b) -> a,
     f(b) -> f(c),
     f(c) -> f(b),
     f(c) -> d,
     b -> e,
     c -> e',
     f(e) -> a,
     f(e') -> d ]
TRS:
   [ f(b) -> a,
     f(b) -> f(c),
     f(c) -> f(b),
     f(c) -> d,
     b -> e,
     c -> e',
     f(e) -> a,
     f(e') -> d ]
constructed TRS:
   [ f(b) -> a,
     f(b) -> f(c),
     f(c) -> f(b),
     f(c) -> d,
     b -> e,
     c -> e',
     f(e) -> a,
     f(e') -> d ]
convertible distinct normal forms: d = a
UNC Completion (Strongly Closed)
problems/39.trs: Success(not UNC)
(0 msec.)