YES
(ignored inputs)COMMENT doi:10.1007/BFb0052357 [21] TRS R_2 submitted by: Takahito Aoto , Junichi Yoshida , and Yoshihito Toyama
Input:
   [ a -> c,
     b -> c,
     f(a,b) -> d,
     f(?x,c) -> f(c,c),
     f(c,?x) -> f(c,c),
     d -> f(a,c),
     d -> f(c,b) ]

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

Make it Complete (R^):
   [ f(a,a) = d,
     f(a,a) = f(c,b),
     f(c,a) = f(c,?x),
     f(a,?x) = f(c,c),
     f(a,a) = f(c,c),
     f(c,a) = f(a,c),
     f(a,?x_1) = f(a,c),
     f(a,a) = f(c,?x_1),
     f(a,?x_1) = f(c,b),
     f(a,?x_1) = d,
     f(c,a) = f(c,b),
     f(c,a) = d,
     f(a,?x_1) = f(c,?x),
     f(c,a) = f(?x,c),
     f(?x,a) = f(c,c),
     f(?x_1,a) = f(?x,c),
     f(?x,a) = d,
     f(?x,a) = f(c,b),
     f(a,a) = f(?x,c),
     f(?x,a) = f(a,c),
     f(a,?x_1) = f(?x,c),
     f(?x,a) = f(c,?x_1),
     f(?x_1,a) = f(a,b),
     f(c,a) = f(a,b),
     f(a,?x_2) = f(a,b),
     f(a,a) = f(a,b),
     a = b,
     f(b,a) = f(b,?x_2),
     f(b,a) = f(b,b),
     f(c,a) = f(b,c),
     f(b,a) = f(c,c),
     f(b,a) = f(a,b),
     f(b,a) = f(?x_1,b),
     f(a,?x_1) = f(?x,b),
     f(?x,a) = f(b,?x_1),
     f(a,a) = f(?x,b),
     f(?x,a) = f(b,b),
     f(?x,a) = f(?x_1,b),
     f(c,a) = f(?x,b),
     f(?x,a) = f(b,c),
     f(c,a) = f(?x,a),
     f(?x,a) = f(a,?x_1),
     f(?x,a) = f(a,a),
     f(?x,a) = f(?x_1,a),
     f(?x,a) = f(b,a),
     f(b,a) = f(?x,c),
     f(a,?x) = f(b,?x_1),
     f(b,a) = d,
     f(b,a) = f(c,b),
     f(c,a) = f(b,b),
     f(a,?x_1) = f(b,b),
     f(a,a) = f(b,?x_1),
     f(a,a) = f(b,c),
     f(b,a) = f(a,c),
     f(c,a) = f(b,?x),
     f(a,?x) = f(b,c),
     f(c,a) = f(a,?x),
     f(a,?x) = f(a,?x_1),
     f(c,a) = f(c,c),
     f(c,a) = f(b,a),
     f(c,a) = f(a,a),
     f(a,a) = f(a,?x_1),
     f(b,a) = f(a,a),
     f(a,?x) = f(b,a),
     f(b,a) = f(b,c),
     f(b,a) = f(c,?x),
     f(a,a) = f(a,c),
     f(a,a) = f(b,b),
     a = c,
     f(b,b) = d,
     f(b,b) = f(a,c),
     f(b,c) = f(c,?x),
     f(b,?x) = f(c,c),
     f(b,c) = f(a,c),
     f(b,?x_1) = f(a,c),
     f(b,b) = f(c,?x_1),
     f(b,?x_1) = f(c,b),
     f(b,?x_1) = d,
     f(b,b) = f(c,c),
     f(b,c) = f(c,b),
     f(b,c) = d,
     f(b,?x_1) = f(c,?x),
     f(b,c) = f(?x,c),
     f(?x,b) = f(c,c),
     f(?x_1,b) = f(?x,c),
     f(?x,b) = d,
     f(b,b) = f(?x,c),
     f(?x,b) = f(c,b),
     f(?x,b) = f(a,c),
     f(b,?x_1) = f(?x,c),
     f(?x,b) = f(c,?x_1),
     f(?x_1,b) = f(b,b),
     f(?x_1,b) = f(b,?x_4),
     f(?x_1,b) = f(b,c),
     f(?x_1,b) = f(?x_3,b),
     f(?x_1,b) = f(a,b),
     f(b,c) = f(a,b),
     f(b,c) = f(c,c),
     f(b,c) = f(b,b),
     f(b,c) = f(b,?x_2),
     f(b,?x_2) = f(b,b),
     f(b,?x_2) = f(b,?x_5),
     f(b,?x_2) = f(a,b),
     f(b,b) = f(c,b),
     f(b,b) = f(a,b),
     b = c,
     f(a,b) = f(c,b),
     f(a,b) = f(a,c),
     f(a,b) = f(c,?x_2),
     f(a,b) = f(c,c),
     f(a,b) = f(?x_1,c),
     f(a,b) = d,
     f(?x,c) = f(c,?x_1),
     f(?x,c) = f(a,c),
     f(?x,c) = f(c,b),
     f(?x,c) = d,
     f(?x,c) = f(?x_1,c),
     f(?x,c) = f(c,c),
     f(c,?x) = f(c,?x_1),
     f(c,c) = d,
     f(c,c) = f(c,b),
     f(c,?x_1) = d,
     f(c,?x_1) = f(c,b),
     f(a,c) = f(c,?x_1),
     f(c,c) = f(a,c),
     f(c,?x) = f(c,c),
     f(a,c) = f(c,b),
     d = f(a,c),
     d = f(c,b) ]
Time: 1.930 [s]

CPNF:
   [ a … c ]
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: 1.932 [s]

problems/74.trs: Success(UNC)
real 2.23
user 1.94
sys 0.01