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

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

Make it Complete (R^):
   [ h(g,a,a') = h(f,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(g,a',a'),
     h(g,a,a') = h(f,a',a'),
     h(g,a',a) = h(f,a',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(f,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(g,a',a) = h(g,a',a'),
     h(g,a',a) = h(g,a,a),
     h(g,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(g,a',a'),
     h(f,a,a') = h(f,a',a'),
     h(f,a',a) = h(f,a',a'),
     h(f,a',a) = h(f,a,a),
     h(f,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(f,a',a'),
     h(f,a,a) = h(g,a,a),
     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'),
     a = a',
     h(?x,a',?y) = h(?x,?y,a'),
     h(?x,a',?y) = h(?x,?y,?y),
     h(?x,?y,a') = h(?x,?y,?y) ]
Time: 0.082 [s]

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

problems/64.trs: Success(UNC)
real 0.10
user 0.09
sys 0.01