YES (ignored inputs)COMMENT Cops #647 - #721: generated ground TRSs; evenly distributed in the UNR/UNC/NFP/CR hierarchy submitted by: Bertram Felgenhauer Input: [ c -> h(c,c), f(c) -> c, f(b) -> b, a -> b, a -> h(h(a,a),h(c,b)) ] Make it flat: [ c -> h(c,c), f(c) -> c, f(b) -> b, a -> b, !cr_0 -> h(a,a), !cr_1 -> h(c,b), a -> h(!cr_0,!cr_1) ] Time: 0.000 [s] Make it Complete (R^): [ h(c,c) = f(c), c = h(c,c), f(c) = c, a = f(b), f(a) = b, f(a) = a, f(a) = f(b), f(a) = h(!cr_0,!cr_1), f(b) = h(!cr_0,!cr_1), f(b) = b, h(c,a) = h(c,b), h(c,a) = !cr_1, b = h(!cr_0,!cr_1), h(a,b) = !cr_0, h(b,b) = !cr_0, h(a,b) = h(b,a), h(a,b) = h(b,b), h(b,a) = h(b,b), h(a,b) = h(a,a), h(b,b) = h(a,a), h(b,a) = h(a,a), h(b,a) = !cr_0, a = b, !cr_0 = h(a,a), !cr_1 = h(c,b), a = h(!cr_0,!cr_1) ] Time: 0.006 [s] CPNF: [ !cr_0 … h(b,b), a … b ] Time: 0.000 [s] Now checking all the pairs in CW... Time to check pairs: 0.000 [s] The TRS has Uniqueness of Normal Forms. Total Time: 0.006 [s] problems/688.trs: Success(UNC) real 0.03 user 0.02 sys 0.01