YES (ignored inputs)COMMENT doi:10.1007/s10817-011-9238-x [33] p. 499 with small correction: b1/c1 instead of b0/c0 Input: [ a1 -> b1, a1 -> c1, b1 -> b2, c1 -> c2, a2 -> b2, a2 -> c2, b2 -> b3, c2 -> c3, a3 -> b3, a3 -> c3, b3 -> b4, c3 -> c4, a4 -> b4, a4 -> c4, b4 -> b5, c4 -> c5, a5 -> b5, a5 -> c5, b5 -> b6, c5 -> c6, a6 -> b6, a6 -> c6, b6 -> b7, c6 -> b7, b7 -> b1, b7 -> c1 ] Make it flat: [ a1 -> b1, a1 -> c1, b1 -> b2, c1 -> c2, a2 -> b2, a2 -> c2, b2 -> b3, c2 -> c3, a3 -> b3, a3 -> c3, b3 -> b4, c3 -> c4, a4 -> b4, a4 -> c4, b4 -> b5, c4 -> c5, a5 -> b5, a5 -> c5, b5 -> b6, c5 -> c6, a6 -> b6, a6 -> c6, b6 -> b7, c6 -> b7, b7 -> b1, b7 -> c1 ] Time: 0.000 [s] Make it Complete (R^): [ a1 = b1, a1 = b7, a1 = c6, a1 = b6, a1 = a6, a1 = c5, a1 = b5, a1 = a5, a1 = c4, a1 = b4, a1 = a4, a1 = c3, a1 = b3, a1 = a3, a1 = b2, a1 = a2, a1 = c2, a1 = c1, b1 = b2, c1 = c2, a2 = b2, a2 = c3, a2 = a3, a2 = b3, a2 = c5, a2 = a5, a2 = b5, a2 = b7, a2 = b1, a2 = b6, a2 = a6, a2 = c6, a2 = b4, a2 = a4, a2 = c1, a2 = c4, a2 = c2, b2 = b4, b2 = c3, b2 = a4, b2 = b6, b2 = c5, b2 = a6, b2 = c1, b2 = c6, b2 = b7, b2 = a5, b2 = c4, b2 = b5, b2 = a3, b2 = c2, b2 = b3, c2 = c4, c2 = a4, c2 = b4, c2 = c6, c2 = a6, c2 = b6, c2 = b1, c2 = b7, c2 = b5, c2 = a5, c2 = c5, c2 = b3, c2 = a3, c2 = c3, a3 = b3, a3 = c4, a3 = a4, a3 = b4, a3 = c6, a3 = a6, a3 = b6, a3 = c1, a3 = b1, a3 = b7, a3 = b5, a3 = a5, a3 = c5, a3 = c3, b3 = b5, b3 = c4, b3 = a5, b3 = b7, b3 = c6, b3 = b1, b3 = c1, b3 = a6, b3 = c5, b3 = b6, b3 = a4, b3 = c3, b3 = b4, c3 = c5, c3 = a5, c3 = b5, c3 = b7, c3 = b1, c3 = c1, c3 = b6, c3 = a6, c3 = c6, c3 = b4, c3 = a4, c3 = c4, a4 = b4, a4 = c5, a4 = a5, a4 = b5, a4 = b7, a4 = b1, a4 = c1, a4 = b6, a4 = a6, a4 = c6, a4 = c4, b4 = b6, b4 = c5, b4 = a6, b4 = c1, b4 = b1, b4 = c6, b4 = b7, b4 = a5, b4 = c4, b4 = b5, c4 = c6, c4 = a6, c4 = b6, c4 = c1, c4 = b1, c4 = b7, c4 = b5, c4 = a5, c4 = c5, a5 = b5, a5 = c6, a5 = a6, a5 = b6, a5 = c1, a5 = b1, a5 = b7, a5 = c5, b5 = b7, b5 = c6, b5 = b1, b5 = c1, b5 = a6, b5 = c5, b5 = b6, c5 = b7, c5 = b1, c5 = c1, c5 = b6, c5 = a6, c5 = c6, a6 = b6, a6 = b7, a6 = b1, a6 = c1, a6 = c6, b6 = c1, b6 = b1, b6 = c6, b6 = b7, c6 = c1, c6 = b1, c6 = b7, b1 = c1, b7 = b1, b7 = c1 ] Time: 0.441 [s] The number of normal forms that must be checked: 0 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.443 [s] problems/116.trs: Success(UNC) real 0.76 user 0.45 sys 0.01