NO (ignored inputs)COMMENT [111] p. 29 ( GUNC & ~UNC & ~GNFP ) Input: [ a -> a, f(b,?x) -> b, f(?x,a) -> a ] Make it flat: [ a -> a, f(b,?x) -> b, f(?x,a) -> a ] Time: 0.000 [s] Make it Complete (R^): [ f(b,?x) = f(b,?x_1), f(?x,b) = a, f(?x_1,b) = f(?x,a), f(?x_1,b) = b, f(?x_1,b) = f(b,?x_2), f(a,?x) = b, f(?x_1,b) = f(?x_4,b), f(?x_1,b) = f(a,?x_2), f(a,?x_2) = f(?x_1,a), f(a,?x_2) = f(b,?x_5), f(a,?x_2) = f(a,?x_5), f(a,?x_2) = a, b = a, f(b,?x_2) = a, f(?x_1,a) = f(b,?x_2), b = f(?x_1,a), f(b,?x) = b, f(?x,a) = f(?x_1,a), f(?x,a) = a ] Time: 0.014 [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.014 [s] problems/510.trs: Success(not UNC) real 0.03 user 0.02 sys 0.01