YES (ignored inputs)COMMENT doi:10.4230/LIPIcs.RTA.2012.165 [37] Example 3.1 ( R ) Input: [ a -> b, a -> f(a), b -> f(f(b)) ] Make it flat: [ a -> b, a -> f(a), !cr_0 -> f(b), b -> f(!cr_0) ] Time: 0.000 [s] Make it Complete (R^): [ a = f(!cr_0), f(a) = !cr_0, f(b) = a, f(b) = b, f(b) = f(a), !cr_0 = a, !cr_0 = b, f(!cr_0) = !cr_0, f(b) = f(!cr_0), f(a) = f(!cr_0), b = f(a), a = b, a = f(a), !cr_0 = f(b), b = f(!cr_0) ] Time: 0.002 [s] The number of normal forms that must be checked: 8 Time: 0.000 [s] Now checking all the pairs... Time to check pairs: 0.000 [s] The TRS has Uniqueness of Normal Forms. Total Time: 0.003 [s] problems/212.trs: Success(UNC) real 0.02 user 0.01 sys 0.00