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),
     g -> f,
     f -> g ]

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),
     g -> f,
     f -> g ]
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(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(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(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(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(g,a',a'),
     h(g,a,a) = h(f,a',a'),
     h(f,a,a) = h(g,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,a) = h(?x,a',a),
     h(?x,a,?y) = h(?x,?y,?y),
     a = a',
     h(?x,a',?y) = h(?x,?y,?y),
     g = f ]
Time: 0.048 [s]

CPNF:
   [ 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.049 [s]

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