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.003 [s] The number of normal forms that must be checked: 9 Time: 0.000 [s] Now checking all the pairs... Time to check pairs: 0.000 [s] The TRS doesn't have Uniqueness of Normal Forms. Counter Example: g(a,?!cx) <->* g(?!cx,a) proof: g(a,?!cx) ->R^ f(?!cx) g(?!cx,a) ->R^ f(?!cx) Total Time: 0.003 [s] problems/r11.trs: Success(not UNC) real 0.32 user 0.02 sys 0.00