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

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

Make it Complete (R^):
   [ g(b) = !cr_0,
     !cr_0 = h(?x_2),
     !cr_0 = f(?x_2),
     !cr_0 = c(b),
     !cr_0 = c(a),
     !cr_0 = f(!cr_0),
     !cr_0 = h(!cr_0),
     !cr_0 = g(a),
     g(b) = f(!cr_0),
     g(a) = h(!cr_0),
     f(!cr_0) = h(?x_2),
     f(!cr_0) = f(?x_2),
     f(!cr_0) = c(b),
     c(b) = h(!cr_0),
     h(!cr_0) = f(?x_1),
     h(!cr_0) = h(?x_1),
     h(!cr_0) = g(b),
     h(!cr_0) = f(!cr_0),
     c(a) = h(!cr_0),
     f(!cr_0) = c(a),
     g(a) = f(!cr_0),
     c(b) = g(b),
     g(a) = c(a),
     g(b) = f(?x_1),
     g(a) = c(b),
     g(a) = f(?x_1),
     g(a) = g(b),
     g(a) = h(?x_1),
     g(b) = h(?x_1),
     g(b) = c(a),
     c(a) = h(?x),
     c(a) = c(b),
     c(a) = f(?x),
     a = b,
     f(?x) = c(b),
     f(?x) = f(?x_1),
     f(?x) = h(?x_1),
     f(?x) = h(?x),
     h(?x) = h(?x_1),
     h(?x) = c(b) ]
Time: 0.029 [s]

The number of normal forms that must be checked: 38
Time: 0.001 [s]

Now checking all the pairs...

Time to check pairs: 0.002 [s]

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

problems/22.trs: Success(UNC)
real 0.06
user 0.06
sys 0.00