NO (ignored inputs)COMMENT doi:10.1007/3-540-45744-5_49 [153] Example 13 submitted by: Raul Gutierrez and Salvador Lucas Input: [ a -> b, f(g(a)) -> f(a) ] Make it flat: [ f(!cl_0) -> f(a), a -> b, !cl_0 -> !cl_0, g(a) -> !cl_0 ] Time: 0.000 [s] Make it Complete (R^): [ f(b) = f(a), f(b) = f(!cl_0), f(!cl_0) = f(a), g(b) = g(a), g(b) = !cl_0, a = b, g(a) = !cl_0 ] Time: 0.000 [s] The number of normal forms that must be checked: 45 Time: 0.002 [s] Now checking all the pairs... Time to check pairs: 0.002 [s] The TRS doesn't have Uniqueness of Normal Forms. Counter Example: f(f(b)) <->* f(f(g(b))) proof: f(f(b)) ->R^ f(f(a)) ->R^ f(f(!cl_0)) f(f(g(b))) ->R^ f(f(g(a))) ->R^ f(f(!cl_0)) Total Time: 0.005 [s] problems/800.trs: Success(not UNC) real 0.03 user 0.02 sys 0.01