YES
(ignored inputs)COMMENT [16] Example 2 submitted by: Takahito Aoto , Junichi Yoshida , and Yoshihito Toyama
Input:
   [ a -> a',
     h(?x,a',?y) -> h(?x,?y,?y),
     h(?x,?y,a') -> h(?x,?y,?y),
     g -> f,
     h(f,a,a) -> h(g,a,a),
     h(g,a,a) -> h(f,a,a) ]

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

Make it Complete (R^):
   [ h(?x,?y,a) = h(?x,?y,?y),
     h(?x,a,?y) = h(?x,?y,?y),
     h(?x,?y,a) = h(?x,a',?y),
     h(?x,?y,a) = h(?x,?y,a'),
     h(?x,?y,a) = h(?x,a,?y),
     h(?x,a,a') = h(?x,a',a'),
     h(?x,a,?y) = h(?x,a',?y),
     h(?x,a,a) = h(?x,a',a'),
     h(?x,a,a) = h(?x,a,a'),
     h(?x,a,a) = h(?x,a',a),
     h(?x,a,a') = h(?x,a',a),
     h(?x,a',a') = h(?x,a',a),
     h(?x,a,?y) = h(?x,?y,a'),
     h(f,a',a') = h(g,a,a),
     h(g,a',a') = h(f,a,a'),
     h(f,a',a') = h(g,a,a'),
     h(g,a',a') = h(g,a,a),
     h(f,a',a') = h(f,a,a),
     h(g,a',a') = h(f,a,a),
     h(g,a',a') = h(f,a',a),
     h(f,a',a') = h(f,a',a),
     h(f,a',a') = h(f,a,a'),
     h(g,a',a') = h(g,a',a),
     h(g,a',a') = h(g,a,a'),
     h(g,a',a') = h(f,a',a'),
     h(f,a',a') = h(g,a',a),
     a = a',
     h(g,a',a) = h(f,a,a),
     h(f,a',a) = h(g,a,a),
     h(?x,a',?y) = h(?x,?y,a'),
     h(g,a',a) = h(f,a,a'),
     h(g,a',a) = h(g,a,a),
     h(g,a',a) = h(f,a',a),
     h(g,a',a) = h(g,a,a'),
     h(f,a',a) = h(f,a,a'),
     h(f,a',a) = h(f,a,a),
     h(f,a',a) = h(g,a,a'),
     h(?x,a',?y) = h(?x,?y,?y),
     h(g,a,a') = h(f,a,a),
     h(f,a,a) = h(f,a,a'),
     h(g,a,a') = h(g,a,a),
     h(f,a,a') = h(g,a,a'),
     h(f,a,a') = h(g,a,a),
     h(?x,?y,a') = h(?x,?y,?y),
     g = f,
     h(f,a,a) = h(g,a,a) ]
Time: 0.094 [s]

CPNF:
   [ a … a',
     f … f ]
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.095 [s]

problems/61.trs: Success(UNC)
real 0.11
user 0.10
sys 0.01