NO (ignored inputs)COMMENT cops number: 38 submitted by: Takahito Aoto , Junichi Yoshida , Yoshihito Toyama [11] Example 3.3.1 input TRS: [ b -> a, b -> c, c -> b, c -> d ] Try persistent and layer-preserving decomposition... Sort Assignment: a : =>5 b : =>5 c : =>5 d : =>5 maximal types: {5} ...decomposition failed. TRS: [ b -> a, b -> c, c -> b, c -> d ] Input: [ b -> a, b -> c, c -> b, c -> d ] Make it flat: [ b -> a, b -> c, c -> b, c -> d ] Time: 0.000 [s] Make it Complete (R^): [ a = c, a = d, b = a, b = d, b = c, c = d ] Time: 0.001 [s] CPNF: [ a … a, a … d ] Time: 0.000 [s] The TRS doesn't have Uniqueness of Normal Forms. Counter Example: a <->* d proof: a d ->R^ c ->R^ b ->R^ a Total Time: 0.001 [s] cops-LMxTnH3N.trs: Success(not UNC) (1 msec.)