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] CPNF: [ a … f(?x,b), a … b ] Time: 0.000 [s] The TRS doesn't have Uniqueness of Normal Forms. Counter Example: f(?x,b) <->* b proof: f(?x,b) ->R^ f(?x,a) ->R^ a b ->R^ a Total Time: 0.002 [s] problems/r2.trs: Success(not UNC) real 0.02 user 0.01 sys 0.01