NO
(ignored inputs)COMMENT doi:10.23638/LMCS-13 ( 2:4 ) 2017 [131] Example 5.11 submitted by: Julian Nagele
Input:
   [ a -> b,
     f(a,b) -> f(a,a),
     f(b,a) -> f(a,a),
     f(a,a) -> c,
     g(?x) -> f(?x,?x) ]

Make it flat:
   [ a -> b,
     f(a,b) -> f(a,a),
     f(b,a) -> f(a,a),
     f(a,a) -> c,
     g(?x) -> f(?x,?x) ]
Time: 0.000 [s]

Make it Complete (R^):
   [ g(b) = c,
     g(b) = f(a,a),
     f(b,b) = f(a,a),
     f(b,b) = c,
     g(b) = f(b,a),
     f(b,b) = g(a),
     f(b,b) = f(a,b),
     f(b,b) = f(b,a),
     f(b,b) = g(b),
     g(b) = g(a),
     g(b) = f(a,b),
     a = b,
     f(a,b) = g(a),
     f(a,b) = c,
     f(a,b) = f(b,a),
     f(a,b) = f(a,a),
     f(b,a) = g(a),
     f(b,a) = c,
     f(b,a) = f(a,a),
     g(a) = f(a,a),
     c = g(a),
     f(a,a) = c,
     g(?x) = f(?x,?x) ]
Time: 0.008 [s]

CPNF:
   [ c … f(b,b),
     a … b,
     c … c ]
Time: 0.000 [s]

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

proof:
     f(b,b)
->R^ f(a,b)
->R^ f(a,a)
->R^ c

     c
Total Time: 0.009 [s]

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