NO Input: [ f(?x) -> g(a,?x), f(?x) -> g(?x,a), g(?x,?x) -> f(?x) ] Make it flat: [ f(?x) -> g(a,?x), f(?x) -> g(?x,a), g(?x,?x) -> f(?x) ] Time: 0.000 [s] Make it Complete (R^): [ g(a,?x) = g(?x,?x), g(a,?x) = g(?x,a), f(?x) = g(a,?x), g(a,a) = f(a), g(?x,a) = g(?x,?x), f(?x) = g(?x,a), g(?x,?x) = f(?x) ] Time: 0.001 [s] CPNF: [ a … a ] 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: g(a,?x) <->* g(?x,a) proof: g(a,?x) ->R^ f(?x) g(?x,a) ->R^ f(?x) Total Time: 0.001 [s] problems/r11.trs: Success(not UNC) real 0.02 user 0.00 sys 0.01