YES
(ignored inputs)COMMENT [17] Example 4 submitted by: Takahito Aoto , Junichi Yoshida , and Yoshihito Toyama
input TRS:
   [ 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) ]
TRS:
   [ 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) ]
confluent TRS:
   [ 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),
     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) ]
UNC Completion (Development Closed)
problems/64.trs: Success(UNC)
(8 msec.)