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

Make it flat:
   [ h(!cl_3,!cl_4) -> h(!cr_6,!cr_7),
     !cl_4 -> !cl_4,
     h(a,!cl_1) -> !cl_4,
     !cr_7 -> h(c,b),
     !cr_6 -> f(b),
     f(!cl_1) -> h(!cr_0,!cr_5),
     !cl_2 -> !cl_2,
     h(!cl_0,c) -> !cl_2,
     !cr_5 -> h(c,!cr_4),
     !cr_4 -> h(c,!cr_3),
     !cr_3 -> h(!cr_2,a),
     !cr_2 -> f(!cr_1),
     !cr_1 -> h(b,b),
     !cr_0 -> f(b),
     f(b) -> !cl_0,
     c -> a,
     a -> h(!cr_8,b),
     !cr_8 -> h(b,b),
     h(a,c) -> !cl_1,
     !cl_1 -> !cl_1,
     h(!cl_2,b) -> !cl_3,
     !cl_3 -> !cl_3 ]
Time: 0.001 [s]

Make it Complete (R^):
   [ h(!cr_0,!cr_7) = h(!cl_3,!cl_4),
     h(!cr_0,!cr_7) = h(!cl_0,!cr_7),
     h(!cr_0,!cr_7) = h(!cr_6,!cr_7),
     h(!cl_0,!cr_7) = h(!cr_6,!cr_7),
     h(!cl_0,!cr_7) = h(!cl_3,!cl_4),
     h(!cl_3,!cl_4) = h(!cr_6,!cr_7),
     h(c,!cl_1) = h(a,!cl_1),
     h(c,!cl_1) = !cl_4,
     h(a,!cl_1) = !cl_4,
     h(a,b) = h(c,b),
     h(a,b) = !cr_7,
     !cr_7 = h(c,b),
     !cr_6 = !cl_0,
     h(!cr_6,c) = !cl_2,
     h(!cr_6,c) = h(!cl_0,c),
     h(!cr_6,a) = h(!cl_0,c),
     h(!cr_6,a) = h(!cr_0,c),
     h(!cr_6,c) = h(!cr_0,a),
     h(!cr_6,a) = h(!cr_6,c),
     h(!cr_6,a) = h(!cl_0,a),
     h(!cr_6,c) = h(!cr_0,c),
     h(!cr_6,c) = h(!cl_0,a),
     h(!cr_6,a) = h(!cr_0,a),
     h(!cr_6,a) = !cl_2,
     h(!cr_6,!cr_5) = f(!cl_1),
     h(!cr_0,!cr_5) = h(!cr_6,!cr_5),
     h(!cr_6,!cr_5) = h(!cl_0,!cr_5),
     !cr_6 = !cr_0,
     !cr_6 = f(b),
     h(!cl_0,!cr_5) = h(!cr_0,!cr_5),
     h(!cl_0,!cr_5) = f(!cl_1),
     f(!cl_1) = h(!cr_0,!cr_5),
     h(!cl_0,a) = !cl_2,
     h(!cr_0,a) = !cl_2,
     h(!cl_0,a) = h(!cr_0,c),
     h(!cl_0,a) = h(!cr_0,a),
     h(!cr_0,c) = h(!cr_0,a),
     h(!cl_0,a) = h(!cl_0,c),
     h(!cr_0,a) = h(!cl_0,c),
     h(!cr_0,c) = h(!cl_0,c),
     h(!cr_0,c) = !cl_2,
     h(!cl_0,c) = !cl_2,
     h(a,!cr_4) = h(c,!cr_4),
     h(a,!cr_4) = !cr_5,
     !cr_5 = h(c,!cr_4),
     h(a,!cr_3) = h(c,!cr_3),
     h(a,!cr_3) = !cr_4,
     !cr_4 = h(c,!cr_3),
     h(!cr_2,c) = h(!cr_2,a),
     h(!cr_2,c) = !cr_3,
     !cr_3 = h(!cr_2,a),
     f(!cr_8) = f(!cr_1),
     f(!cr_8) = !cr_2,
     !cr_2 = f(!cr_1),
     h(!cr_1,b) = a,
     h(!cr_1,b) = h(!cr_8,b),
     h(!cr_1,b) = c,
     !cr_1 = !cr_8,
     !cr_1 = h(b,b),
     !cr_0 = !cl_0,
     !cr_0 = f(b),
     f(b) = !cl_0,
     h(c,c) = !cl_1,
     c = h(!cr_8,b),
     h(c,a) = !cl_1,
     h(c,c) = h(a,a),
     h(c,c) = h(c,a),
     h(a,a) = h(c,a),
     h(c,c) = h(a,c),
     h(c,a) = h(a,c),
     h(a,a) = h(a,c),
     h(a,a) = !cl_1,
     c = a,
     a = h(!cr_8,b),
     !cr_8 = h(b,b),
     h(a,c) = !cl_1,
     h(!cl_2,b) = !cl_3 ]
Time: 0.033 [s]

CPNF:
   [ !cr_5 … h(h(h(b,b),b),h(h(h(b,b),b),h(f(h(b,b)),h(h(b,b),b)))),
     !cl_3 … h(h(!cl_0,h(h(b,b),b)),b),
     !cr_4 … h(h(h(b,b),b),h(f(h(b,b)),h(h(b,b),b))),
     !cl_4 … h(h(h(b,b),b),h(h(h(b,b),b),h(h(b,b),b))),
     !cr_7 … h(h(h(b,b),b),b),
     !cr_3 … h(f(h(b,b)),h(h(b,b),b)),
     !cl_1 … h(h(h(b,b),b),h(h(b,b),b)),
     !cl_2 … h(!cl_0,h(h(b,b),b)),
     a … h(h(b,b),b),
     !cr_2 … f(h(b,b)),
     !cr_1 … h(b,b),
     !cl_0 … !cl_0,
     b … b ]
Time: 0.000 [s]

Now checking all the pairs in CW...

Time to check pairs: 0.000 [s]

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

proof:
     h(!cl_0,h(h(h(b,b),b),b))
->R^ h(!cl_0,h(h(!cr_8,b),b))
->R^ h(!cl_0,h(h(!cr_1,b),b))
->R^ h(!cl_0,h(c,b))
->R^ h(!cl_0,h(a,b))
->R^ h(!cl_0,!cr_7)

     h(h(h(!cl_0,h(h(b,b),b)),b),h(h(h(b,b),b),h(h(h(b,b),b),h(h(b,b),b))))
->R^ h(h(h(!cl_0,h(!cr_8,b)),b),h(h(h(b,b),b),h(h(h(b,b),b),h(h(b,b),b))))
->R^ h(h(h(!cl_0,h(!cr_1,b)),b),h(h(h(b,b),b),h(h(h(b,b),b),h(h(b,b),b))))
->R^ h(h(h(!cl_0,h(!cr_1,b)),b),h(h(h(b,b),b),h(h(!cr_8,b),h(h(b,b),b))))
->R^ h(h(h(!cl_0,h(!cr_1,b)),b),h(h(h(b,b),b),h(h(!cr_1,b),h(h(b,b),b))))
->R^ h(h(h(!cl_0,h(!cr_1,b)),b),h(h(h(b,b),b),h(h(!cr_1,b),h(!cr_8,b))))
->R^ h(h(h(!cl_0,h(!cr_1,b)),b),h(h(h(b,b),b),h(h(!cr_1,b),h(!cr_1,b))))
->R^ h(h(h(!cl_0,c),b),h(h(h(b,b),b),h(h(!cr_1,b),h(!cr_1,b))))
->R^ h(h(h(!cl_0,a),b),h(h(h(b,b),b),h(h(!cr_1,b),h(!cr_1,b))))
->R^ h(h(h(!cl_0,a),b),h(h(!cr_8,b),h(h(!cr_1,b),h(!cr_1,b))))
->R^ h(h(h(!cl_0,a),b),h(h(!cr_1,b),h(h(!cr_1,b),h(!cr_1,b))))
->R^ h(h(h(!cl_0,a),b),h(h(!cr_1,b),h(c,h(!cr_1,b))))
->R^ h(h(h(!cl_0,a),b),h(h(!cr_1,b),h(a,h(!cr_1,b))))
->R^ h(h(h(!cl_0,a),b),h(h(!cr_1,b),h(a,c)))
->R^ h(h(h(!cl_0,a),b),h(h(!cr_1,b),h(a,a)))
->R^ h(h(!cl_2,b),h(h(!cr_1,b),h(a,a)))
->R^ h(h(!cl_2,b),h(c,h(a,a)))
->R^ h(h(!cl_2,b),h(a,h(a,a)))
->R^ h(h(!cl_2,b),h(a,!cl_1))
->R^ h(!cl_3,h(a,!cl_1))
->R^ h(!cl_3,!cl_4)
->R^ h(!cl_0,!cr_7)
Total Time: 0.038 [s]

problems/667.trs: Success(not UNC)
real 0.05
user 0.05
sys 0.00