YES (ignored inputs)COMMENT Cops #647 - #721: generated ground TRSs; evenly distributed in the UNR/UNC/NFP/CR hierarchy submitted by: Bertram Felgenhauer Input: [ b -> h(c,f(b)), a -> c, h(h(h(f(a),a),a),f(f(f(h(h(f(b),b),b))))) -> a, c -> h(f(h(c,f(f(c)))),f(b)) ] Make it flat: [ h(!cl_2,!cl_8) -> a, !cl_8 -> !cl_8, f(!cl_7) -> !cl_8, !cl_6 -> !cl_6, f(!cl_5) -> !cl_6, !cl_4 -> !cl_4, h(!cl_3,b) -> !cl_4, !cl_2 -> !cl_2, h(!cl_1,a) -> !cl_2, a -> c, b -> h(c,!cr_0), !cr_0 -> f(b), !cl_0 -> !cl_0, f(a) -> !cl_0, c -> h(!cr_4,!cr_5), !cr_5 -> f(b), !cr_4 -> f(!cr_3), !cr_3 -> h(c,!cr_2), !cr_2 -> f(!cr_1), !cr_1 -> f(c), h(!cl_0,a) -> !cl_1, !cl_1 -> !cl_1, f(b) -> !cl_3, !cl_3 -> !cl_3, h(!cl_4,b) -> !cl_5, !cl_5 -> !cl_5, f(!cl_6) -> !cl_7, !cl_7 -> !cl_7 ] Time: 0.002 [s] Make it Complete (R^): [ c = h(!cl_2,!cl_8), h(!cl_2,!cl_8) = h(!cr_4,!cr_0), h(!cl_2,!cl_8) = h(!cr_4,!cl_3), h(!cl_2,!cl_8) = h(!cr_4,!cr_5), h(!cl_2,!cl_8) = a, f(!cl_7) = !cl_8, f(!cl_5) = !cl_6, h(!cr_5,b) = !cl_4, h(!cr_5,b) = h(!cr_0,b), h(!cr_5,b) = h(!cl_3,b), h(!cr_0,b) = h(!cl_3,b), h(!cr_0,b) = !cl_4, h(!cl_3,b) = !cl_4, h(!cl_1,c) = h(!cl_1,a), h(!cl_1,c) = !cl_2, h(!cl_1,a) = !cl_2, f(a) = !cr_1, h(a,!cr_2) = h(c,!cr_2), h(a,!cr_2) = !cr_3, a = h(!cr_4,!cr_5), a = h(!cr_4,!cl_3), a = h(!cr_4,!cr_0), h(a,!cr_0) = b, h(a,!cl_3) = b, h(a,!cr_0) = h(c,!cl_3), h(a,!cl_3) = h(c,!cr_0), h(a,!cr_0) = h(c,!cr_5), h(a,!cr_0) = h(c,!cr_0), h(a,!cr_5) = h(c,!cr_0), h(a,!cl_3) = h(c,!cr_5), h(a,!cr_0) = h(a,!cl_3), h(a,!cr_0) = h(a,!cr_5), h(a,!cl_3) = h(a,!cr_5), h(a,!cl_3) = h(c,!cl_3), h(a,!cr_5) = h(c,!cl_3), h(a,!cr_5) = h(c,!cr_5), h(a,!cr_5) = b, h(!cl_0,c) = !cl_1, f(c) = f(a), f(!cl_0) = f(!cr_1), f(!cl_0) = !cr_2, h(!cr_1,c) = !cl_1, h(!cl_0,c) = h(!cr_1,a), h(!cl_0,c) = h(!cr_1,c), h(!cr_1,a) = h(!cr_1,c), h(!cl_0,c) = h(!cl_0,a), h(!cr_1,c) = h(!cl_0,a), h(!cr_1,a) = h(!cl_0,a), h(!cr_1,a) = !cl_1, !cl_0 = !cr_1, f(c) = !cl_0, a = c, h(c,!cr_5) = b, h(c,!cr_5) = h(c,!cl_3), h(c,!cr_5) = h(c,!cr_0), h(c,!cl_3) = h(c,!cr_0), h(c,!cl_3) = b, b = h(c,!cr_0), !cr_0 = !cl_3, h(!cr_4,!cr_0) = c, h(!cr_4,!cr_5) = h(!cr_4,!cr_0), h(!cr_4,!cr_0) = h(!cr_4,!cl_3), !cr_0 = !cr_5, !cr_0 = f(b), f(a) = !cl_0, h(!cr_4,!cl_3) = h(!cr_4,!cr_5), h(!cr_4,!cl_3) = c, c = h(!cr_4,!cr_5), !cr_5 = !cl_3, !cr_5 = f(b), !cr_4 = f(!cr_3), !cr_3 = h(c,!cr_2), !cr_2 = f(!cr_1), !cr_1 = f(c), h(!cl_0,a) = !cl_1, f(b) = !cl_3, h(!cl_4,b) = !cl_5, f(!cl_6) = !cl_7 ] Time: 0.054 [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.062 [s] problems/686.trs: Success(UNC) real 0.09 user 0.07 sys 0.01