YES
(ignored inputs)COMMENT Cops #647 - #721: generated ground TRSs; evenly distributed in the UNR/UNC/NFP/CR hierarchy submitted by: Bertram Felgenhauer
Input:
   [ c -> c,
     a -> f(h(h(f(a),f(f(c))),b)),
     c -> a,
     h(c,f(b)) -> c ]

Make it flat:
   [ h(c,!cl_0) -> c,
     c -> a,
     a -> f(!cr_4),
     !cr_4 -> h(!cr_3,b),
     !cr_3 -> h(!cr_0,!cr_2),
     !cr_2 -> f(!cr_1),
     !cr_1 -> f(c),
     !cr_0 -> f(a),
     c -> c,
     f(b) -> !cl_0 ]
Time: 0.000 [s]

Make it Complete (R^):
   [ a = h(c,!cl_0),
     h(a,!cl_0) = c,
     h(a,!cl_0) = a,
     h(a,!cl_0) = h(c,!cl_0),
     h(a,!cl_0) = f(!cr_4),
     h(c,!cl_0) = f(!cr_4),
     h(c,!cl_0) = c,
     f(c) = !cr_0,
     c = f(!cr_4),
     f(a) = f(c),
     h(!cr_1,!cr_2) = h(!cr_0,!cr_2),
     h(!cr_1,!cr_2) = !cr_3,
     f(!cr_0) = f(!cr_1),
     f(!cr_0) = !cr_2,
     !cr_1 = !cr_0,
     f(a) = !cr_1,
     c = a,
     a = f(!cr_4),
     !cr_4 = h(!cr_3,b),
     !cr_3 = h(!cr_0,!cr_2),
     !cr_2 = f(!cr_1),
     !cr_1 = f(c),
     !cr_0 = f(a),
     f(b) = !cl_0 ]
Time: 0.004 [s]

CPNF:
   [ b … b,
     !cl_0 … !cl_0 ]
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/685.trs: Success(UNC)
real 0.02
user 0.02
sys 0.00