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

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

Make it Complete (R^):
   [ f(?x,?x,c) = h(c,c),
     f(?x,?x,c) = f(?x_1,?x_1,c),
     f(?x,?x,c) = c,
     f(?x,?x,?y) = f(?x_1,?x_1,?y),
     h(!cr_0,c) = g(c),
     h(!cr_0,c) = f(c,c,!cr_0),
     f(?x_1,?x_1,!cr_0) = g(c),
     f(?x_1,?x_1,!cr_0) = f(c,c,!cr_0),
     f(?x_1,?x_1,!cr_0) = h(!cr_0,c),
     f(?x_1,?x_1,!cr_0) = f(?x_3,?x_3,!cr_0),
     !cr_0 = f(?x_1,?x_1,!cr_0),
     h(!cr_0,c) = !cr_0,
     f(?x,?x,?y) = h(?y,c),
     f(c,c,!cr_0) = g(c),
     !cr_0 = f(c,c,!cr_0),
     !cr_0 = g(c),
     g(?x) = f(?x,c,!cr_0),
     c = h(c,c) ]
Time: 0.005 [s]

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

problems/79.trs: Success(UNC)
real 0.02
user 0.01
sys 0.01