NO (ignored inputs)COMMENT [111] p. 27 Input: [ a -> b, f(?x,a) -> b, f(b,b) -> b ] Make it flat: [ a -> b, f(?x,a) -> b, f(b,b) -> b ] Time: 0.000 [s] Make it Complete (R^): [ a = f(b,b), f(b,a) = b, f(a,b) = b, a = f(?x,a), f(b,a) = f(?x,a), f(a,b) = f(?x,a), f(?x,b) = b, f(?x_1,b) = f(?x,a), f(b,a) = f(?x,b), f(a,a) = f(?x,b), f(b,a) = f(a,b), f(b,a) = f(a,a), f(a,b) = f(a,a), f(b,a) = f(b,b), a = f(?x_1,b), f(a,b) = a, f(b,a) = a, a = f(a,a), f(a,a) = b, f(a,a) = f(?x_1,a), f(a,a) = f(b,b), f(a,b) = f(b,b), f(a,b) = f(?x,b), f(?x,b) = f(?x_1,b), f(?x,b) = f(b,b), a = b, f(?x,a) = f(b,b), f(?x,a) = f(?x_1,a), f(?x,a) = b, f(b,b) = b ] Time: 0.022 [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^ b ->R^ a b ->R^ a Total Time: 0.022 [s] problems/505.trs: Success(not UNC) real 0.06 user 0.03 sys 0.00