YES (ignored inputs)COMMENT Cops #647 - #721: generated ground TRSs; evenly distributed in the UNR/UNC/NFP/CR hierarchy submitted by: Bertram Felgenhauer Input: [ f(b) -> b, b -> h(h(c,f(b)),a) ] Make it flat: [ f(b) -> b, !cr_0 -> f(b), !cr_1 -> h(c,!cr_0), b -> h(!cr_1,a) ] Time: 0.000 [s] Make it Complete (R^): [ f(b) = h(!cr_1,a), h(c,b) = h(c,!cr_0), h(c,b) = !cr_1, !cr_0 = h(!cr_1,a), f(!cr_0) = !cr_0, f(!cr_0) = h(!cr_1,a), f(!cr_0) = f(b), f(!cr_0) = b, b = !cr_0, f(b) = b, !cr_0 = f(b), !cr_1 = h(c,!cr_0), b = h(!cr_1,a) ] Time: 0.001 [s] CPNF: [ c … c, a … a ] 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.002 [s] problems/647.trs: Success(UNC) real 0.02 user 0.01 sys 0.01