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 -> a, b -> b, h(h(b,c),b) -> f(f(h(b,c))), h(h(a,f(f(f(a)))),a) -> h(h(f(h(c,h(c,f(b)))),b),c), a -> h(h(f(h(b,c)),f(h(a,a))),a) ] Make it flat: [ h(!cl_4,a) -> h(!cr_6,c), !cl_4 -> !cl_4, h(a,!cl_3) -> !cl_4, !cr_6 -> h(!cr_5,b), !cr_5 -> f(!cr_4), !cr_4 -> h(c,!cr_3), !cr_3 -> h(c,!cr_2), !cr_2 -> f(b), h(!cl_1,b) -> f(!cr_1), !cl_2 -> !cl_2, f(!cl_0) -> !cl_2, !cr_1 -> f(!cr_0), !cr_0 -> h(b,c), b -> b, c -> a, !cl_0 -> !cl_0, f(a) -> !cl_0, a -> h(!cr_11,a), !cr_11 -> h(!cr_8,!cr_10), !cr_10 -> f(!cr_9), !cr_9 -> h(a,a), !cr_8 -> f(!cr_7), !cr_7 -> h(b,c), h(b,c) -> !cl_1, !cl_1 -> !cl_1, f(!cl_2) -> !cl_3, !cl_3 -> !cl_3 ] Time: 0.001 [s] Make it Complete (R^): [ h(!cr_6,a) = h(!cl_4,a), h(!cr_6,a) = h(!cr_6,c), h(!cr_6,a) = h(!cl_4,c), h(!cl_4,c) = h(!cl_4,a), h(!cl_4,c) = h(!cr_6,c), h(!cl_4,a) = h(!cr_6,c), h(c,!cl_3) = h(a,!cl_3), h(c,!cl_3) = !cl_4, h(a,!cl_3) = !cl_4, !cr_6 = h(!cr_5,b), !cr_5 = f(!cr_4), h(a,!cr_3) = h(c,!cr_3), h(a,!cr_3) = !cr_4, !cr_4 = h(c,!cr_3), h(a,!cr_2) = h(c,!cr_2), h(a,!cr_2) = !cr_3, !cr_3 = h(c,!cr_2), !cr_2 = f(b), f(!cr_8) = h(!cl_1,b), h(!cr_7,b) = f(!cr_1), h(!cr_7,b) = f(!cr_8), f(!cr_8) = f(!cr_1), f(!cr_8) = h(!cr_0,b), h(!cr_7,b) = h(!cr_0,b), h(!cr_7,b) = h(!cl_1,b), h(!cr_0,b) = h(!cl_1,b), h(!cr_0,b) = f(!cr_1), h(!cl_1,b) = f(!cr_1), f(!cl_0) = !cl_2, f(!cr_7) = !cr_1, f(!cl_1) = !cr_1, h(!cr_1,!cr_10) = h(!cr_8,!cr_10), h(!cr_1,!cr_10) = !cr_11, !cr_1 = !cr_8, !cr_1 = f(!cr_0), h(b,a) = !cr_0, !cr_0 = !cl_1, f(!cr_0) = !cr_8, f(!cr_7) = f(!cr_0), f(!cr_0) = f(!cl_1), !cr_0 = !cr_7, !cr_0 = h(b,c), h(a,c) = !cr_9, h(c,c) = !cr_9, h(a,c) = h(c,a), h(a,c) = h(c,c), h(c,a) = h(c,c), h(a,c) = h(a,a), h(c,c) = h(a,a), h(c,a) = h(a,a), h(c,a) = !cr_9, h(!cr_11,c) = a, h(!cr_11,c) = h(!cr_11,a), h(!cr_11,c) = c, c = h(!cr_11,a), f(c) = f(a), f(c) = !cl_0, h(b,a) = !cl_1, h(b,a) = h(b,c), h(b,a) = !cr_7, c = a, f(a) = !cl_0, a = h(!cr_11,a), !cr_11 = h(!cr_8,!cr_10), !cr_10 = f(!cr_9), !cr_9 = h(a,a), f(!cl_1) = f(!cr_7), f(!cl_1) = !cr_8, !cr_8 = f(!cr_7), !cr_7 = !cl_1, !cr_7 = h(b,c), h(b,c) = !cl_1, f(!cl_2) = !cl_3 ] Time: 0.020 [s] CPNF: [ ] 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.024 [s] problems/659.trs: Success(UNC) real 0.06 user 0.04 sys 0.00