NO Input: [ a -> b, a -> c, c -> c, d -> c, d -> e ] Make it flat: [ a -> b, a -> c, c -> c, d -> c, d -> e ] Time: 0.000 [s] Make it Complete (R^): [ b = c, b = e, b = d, a = b, a = d, a = e, a = c, c = e, d = c, d = e ] Time: 0.001 [s] CPNF: [ a … b, a … e ] Time: 0.000 [s] The TRS doesn't have Uniqueness of Normal Forms. Counter Example: b <->* e proof: b ->R^ a e ->R^ d ->R^ c ->R^ a Total Time: 0.001 [s] problems/r1.trs: Success(not UNC) real 0.04 user 0.01 sys 0.01