YES Input: [ f(g(a),?y) -> ?y ] Make it flat: [ f(!cl_0,?y) -> ?y, g(a) -> !cl_0 ] Time: 0.000 [s] Make it Complete (R^): [ f(!cl_0,!cl_0) = !cl_0, g(a) = f(!cl_0,!cl_0), f(!cl_0,?y) = ?y, g(a) = !cl_0 ] Time: 0.000 [s] CPNF: [ a … a, !cl_0 … !cl_0 ] 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: 0.000 [s] problems/r6.trs: Success(UNC) real 0.01 user 0.01 sys 0.00