YES
(ignored inputs)COMMENT doi:10.1007/11805618_6 [7] Example 1 submitted by: Takahito Aoto , Junichi Yoshida , and Yoshihito Toyama
Input:
   [ g(a) -> f(g(a)),
     g(b) -> c,
     a -> b,
     f(?x) -> h(?x,?x),
     h(?x,?y) -> c ]

Make it flat:
   [ !cr_0 -> g(a),
     g(a) -> f(!cr_0),
     g(b) -> c,
     a -> b,
     f(?x) -> h(?x,?x),
     h(?x,?y) -> c ]
Time: 0.000 [s]

Make it Complete (R^):
   [ g(b) = !cr_0,
     !cr_0 = f(?x_2),
     !cr_0 = h(?x_4,?y_4),
     !cr_0 = h(?x_2,?x_2),
     f(c) = g(a),
     f(c) = c,
     h(!cr_0,c) = c,
     h(c,!cr_0) = c,
     f(c) = h(!cr_0,!cr_0),
     h(!cr_0,c) = f(!cr_0),
     h(c,!cr_0) = f(!cr_0),
     h(!cr_0,c) = g(b),
     h(c,!cr_0) = g(b),
     h(!cr_0,c) = f(?x_1),
     h(c,!cr_0) = f(?x_1),
     h(!cr_0,c) = h(?x_1,?x_1),
     h(c,!cr_0) = h(?x_1,?x_1),
     h(!cr_0,c) = h(?x_1,?y_1),
     h(c,!cr_0) = h(?x_1,?y_1),
     f(c) = h(?x_2,?x_2),
     f(c) = h(?x_4,?y_4),
     f(c) = f(?x_2),
     h(!cr_0,c) = g(a),
     h(c,!cr_0) = g(a),
     f(c) = g(b),
     h(!cr_0,c) = !cr_0,
     h(c,!cr_0) = !cr_0,
     f(c) = f(!cr_0),
     c = h(c,c),
     h(c,c) = g(a),
     h(c,c) = h(!cr_0,!cr_0),
     h(c,c) = f(!cr_0),
     h(c,!cr_0) = f(c),
     h(!cr_0,c) = h(c,c),
     h(!cr_0,!cr_0) = h(c,!cr_0),
     h(c,c) = h(c,!cr_0),
     h(c,!cr_0) = h(!cr_0,c),
     h(!cr_0,c) = h(!cr_0,!cr_0),
     h(!cr_0,c) = f(c),
     h(c,c) = h(?x_2,?y_2),
     h(c,c) = h(?x_1,?x_1),
     h(c,c) = f(?x_1),
     h(c,c) = g(b),
     h(c,c) = f(c),
     !cr_0 = h(c,c),
     f(c) = !cr_0,
     !cr_0 = c,
     !cr_0 = f(!cr_0),
     !cr_0 = h(!cr_0,!cr_0),
     !cr_0 = g(a),
     g(b) = f(!cr_0),
     g(a) = h(!cr_0,!cr_0),
     f(!cr_0) = f(?x_2),
     f(!cr_0) = h(?x_4,?y_4),
     f(!cr_0) = h(?x_2,?x_2),
     h(!cr_0,!cr_0) = h(?x_1,?y_1),
     h(!cr_0,!cr_0) = h(?x_1,?x_1),
     h(!cr_0,!cr_0) = f(?x_1),
     h(!cr_0,!cr_0) = g(b),
     h(!cr_0,!cr_0) = f(!cr_0),
     c = h(!cr_0,!cr_0),
     f(!cr_0) = c,
     g(a) = f(!cr_0),
     g(a) = c,
     g(b) = h(?x_1,?y_1),
     g(b) = h(?x_1,?x_1),
     g(a) = h(?x_1,?x_1),
     g(a) = h(?x_3,?y_3),
     g(a) = g(b),
     g(a) = f(?x_1),
     g(b) = f(?x_1),
     g(b) = c,
     a = b,
     f(?x) = c,
     f(?x) = f(?x_1),
     h(?x,?x) = c,
     h(?x,?x) = f(?x_1),
     h(?x,?x) = h(?x_2,?x_2),
     h(?x_1,?y_1) = h(?x,?x),
     f(?x) = h(?x_1,?y_1),
     f(?x) = h(?x,?x),
     h(?x,?y) = h(?x_1,?y_1),
     h(?x,?y) = c ]
Time: 0.261 [s]

The number of normal forms that must be checked: 86
Time: 1.618 [s]

Now checking all the pairs...

Time to check pairs: 0.006 [s]

The TRS has Uniqueness of Normal Forms.
Total Time: 1.887 [s]

problems/19.trs: Success(UNC)
real 1.92
user 1.89
sys 0.00