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

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

Make it Complete (R^):
   [ f(!cl_1) = f(!cr_0),
     f(!cl_1) = b,
     f(!cl_0) = !cl_1,
     h(a,b) = h(c,b),
     h(a,b) = !cr_0,
     f(a) = f(c),
     f(a) = !cl_0,
     c = a,
     f(c) = !cl_0,
     !cr_0 = h(c,b),
     b = f(!cr_0) ]
Time: 0.001 [s]

CPNF:
   [ b … f(h(a,f(f(f(a))))),
     !cr_0 … h(a,f(f(f(a)))),
     b … f(f(f(a))),
     !cl_1 … f(f(a)),
     !cl_0 … f(a),
     a … a ]
Time: 0.000 [s]

The TRS doesn't have Uniqueness of Normal Forms.
Counter Example: 
     f(h(a,f(f(f(a)))))
<->* f(f(f(a)))

proof:
     f(h(a,f(f(f(a)))))
->R^ f(h(a,f(f(!cl_0))))
->R^ f(h(a,f(!cl_1)))
->R^ f(h(a,b))
->R^ f(!cr_0)
->R^ b

     f(f(f(a)))
->R^ f(f(!cl_0))
->R^ f(!cl_1)
->R^ b
Total Time: 0.001 [s]

problems/664.trs: Success(not UNC)
real 0.02
user 0.01
sys 0.00