NO Input: [ f(?x,a) -> a, a -> b ] Make it flat: [ f(?x,a) -> a, a -> b ] Time: 0.000 [s] Make it Complete (R^): [ b = f(?x,a), b = f(?x,b), f(?x,b) = a, f(?x,b) = f(?x_1,b), f(?x_1,b) = f(?x,a), f(?x,a) = f(?x_1,a), f(?x,a) = a, a = b ] Time: 0.001 [s] The number of normal forms that must be checked: 905 Time: 0.176 [s] Now checking all the pairs... Time to check pairs: 0.000 [s] The TRS doesn't have Uniqueness of Normal Forms. Counter Example: f(f(?!cx_2,?!cx_3),b) <->* f(f(?!cx_3,?!cx_3),b) proof: f(f(?!cx_2,?!cx_3),b) ->R^ f(f(?!cx_2,?!cx_3),a) ->R^ a f(f(?!cx_3,?!cx_3),b) ->R^ f(f(?!cx_3,?!cx_3),a) ->R^ a Total Time: 0.177 [s] problems/r2.trs: Success(not UNC) real 0.23 user 0.18 sys 0.01