YES
(ignored inputs)COMMENT doi:10.1016/0890-5401 ( 90 ) 90015-A [24] p. 188 submitted by: Takahito Aoto , Junichi Yoshida , and Yoshihito Toyama
Input:
   [ g(f(a)) -> f(g(f(a))),
     g(f(a)) -> f(f(a)),
     f(f(a)) -> f(a) ]

Make it flat:
   [ f(!cl_0) -> f(a),
     g(!cl_0) -> f(!cr_2),
     !cr_2 -> f(a),
     g(!cl_0) -> f(!cr_1),
     !cr_1 -> g(!cr_0),
     !cr_0 -> f(a),
     f(a) -> !cl_0 ]
Time: 0.000 [s]

Make it Complete (R^):
   [ f(!cr_0) = f(a),
     f(!cr_2) = f(a),
     f(!cl_0) = !cl_0,
     f(!cl_0) = !cr_0,
     f(!cl_0) = !cr_2,
     f(a) = f(!cr_1),
     f(a) = g(!cr_2),
     f(a) = g(!cr_0),
     f(a) = !cr_1,
     g(!cl_0) = !cl_0,
     g(!cl_0) = !cr_0,
     g(!cr_0) = !cr_2,
     g(!cr_2) = !cr_2,
     !cr_2 = !cr_1,
     !cr_2 = f(!cr_1),
     !cr_2 = f(!cr_2),
     !cr_0 = f(!cr_0),
     f(!cr_2) = !cl_0,
     !cl_0 = g(!cr_2),
     !cl_0 = !cr_1,
     !cl_0 = g(!cr_0),
     g(!cr_1) = !cr_1,
     g(!cr_1) = g(!cl_0),
     g(!cr_1) = f(!cr_1),
     g(!cr_1) = g(!cr_2),
     g(!cr_1) = f(!cr_0),
     g(!cr_1) = f(!cl_0),
     g(!cr_1) = f(!cr_2),
     !cl_0 = g(!cr_1),
     !cr_2 = g(!cr_1),
     g(!cr_1) = f(a),
     g(!cr_1) = g(!cr_0),
     g(!cr_1) = !cr_0,
     !cr_0 = !cr_1,
     !cr_0 = g(!cr_0),
     !cr_0 = g(!cr_2),
     !cr_0 = f(!cr_2),
     !cr_0 = f(!cr_1),
     !cl_0 = f(!cr_1),
     !cl_0 = f(!cr_0),
     !cr_2 = f(!cr_0),
     g(!cl_0) = !cr_2,
     f(a) = g(!cl_0),
     f(!cl_0) = f(a),
     f(!cr_0) = g(!cl_0),
     f(!cl_0) = g(!cl_0),
     g(!cr_0) = f(!cr_2),
     g(!cr_2) = f(!cr_2),
     f(!cr_2) = !cr_1,
     f(!cr_0) = f(!cr_1),
     f(!cl_0) = !cr_1,
     f(!cl_0) = g(!cr_0),
     g(!cr_0) = f(!cr_0),
     f(!cr_0) = !cr_1,
     f(!cr_0) = g(!cr_2),
     f(!cl_0) = g(!cr_2),
     f(!cr_0) = f(!cl_0),
     f(!cr_0) = f(!cr_2),
     f(!cl_0) = f(!cr_2),
     f(!cl_0) = f(!cr_1),
     f(!cr_2) = f(!cr_1),
     g(!cl_0) = f(!cr_2),
     !cr_2 = !cl_0,
     g(!cr_2) = !cr_1,
     g(!cr_2) = g(!cl_0),
     g(!cr_2) = g(!cr_0),
     g(!cr_2) = f(!cr_1),
     !cr_2 = !cr_0,
     !cr_2 = f(a),
     g(!cr_0) = f(!cr_1),
     f(!cr_1) = !cr_1,
     g(!cl_0) = f(!cr_1),
     g(!cl_0) = g(!cr_0),
     g(!cl_0) = !cr_1,
     !cr_1 = g(!cr_0),
     !cr_0 = !cl_0,
     !cr_0 = f(a),
     f(a) = !cl_0 ]
Time: 0.070 [s]

The number of normal forms that must be checked: 159
Time: 0.008 [s]

Now checking all the pairs...

Time to check pairs: 0.024 [s]

The TRS has Uniqueness of Normal Forms.
Total Time: 0.103 [s]

problems/81.trs: Success(UNC)
real 0.14
user 0.10
sys 0.01