NO Input: [ f(?x,?y) -> a, f(k(l(a1,a2),a1,a3),?y) -> a, f(?x,u) -> a, a -> g(b1,u,?x), b1 -> b, b -> h(?x,d), h(?y,d) -> i(c), u -> j(v) ] Make it flat: [ f(!cl_1,?y) -> a, k(!cl_0,a1,a3) -> !cl_1, f(?x,u) -> a, a -> g(b1,u,?x), b1 -> b, b -> h(?x,d), h(?y,d) -> i(c), u -> j(v), l(a1,a2) -> !cl_0, f(?x,?y) -> a ] Time: 0.000 [s] Make it Complete (R^): [ f(!cl_1,?y) = f(?x_1,?y_1), f(!cl_1,?y) = g(b1,u,?x_1), f(!cl_1,?y) = g(b,u,?x_1), f(!cl_1,?y) = f(?x_1,u), f(!cl_1,?y) = f(!cl_1,?y_1), f(!cl_1,?y) = a, k(!cl_0,a1,a3) = !cl_1, f(?x,u) = f(?x_1,?y_1), f(?x,u) = g(b1,u,?x_1), f(?x,u) = g(b,u,?x_1), f(?x,u) = f(?x_1,u), f(?x,u) = a, g(b,u,?x) = a, g(b,u,?x) = f(?x_1,?y_1), g(b1,u,?x) = f(?x_1,?y_1), g(b,u,?x) = g(b,u,?x_1), g(b,u,?x_1) = g(b1,u,?x), g(b1,u,?x) = g(b1,u,?x_1), a = g(b1,u,?x), b1 = h(?x,d), b1 = i(c), b1 = b, b = i(c), b = h(?x,d), h(?y,d) = h(?y_1,d), h(?y,d) = i(c), u = j(v), l(a1,a2) = !cl_0, f(?x,?y) = f(?x_1,?y_1), f(?x,?y) = a ] Time: 0.013 [s] CPNF: [ a … g(i(c),j(v),?x_1), a … g(i(c),j(v),?x), b … i(c), u … j(v), a3 … a3, !cl_1 … !cl_1, d … d, c … c, v … v, a2 … a2, a1 … a1, !cl_0 … !cl_0 ] Time: 0.000 [s] The TRS doesn't have Uniqueness of Normal Forms. Counter Example: g(i(c),j(v),?x) <->* g(i(c),j(v),?x_1) proof: g(i(c),j(v),?x) ->R^ g(h(?!,d),j(v),?x) ->R^ g(b,j(v),?x) ->R^ g(b,u,?x) ->R^ g(b,u,?!) ->R^ f(?!,?!) ->R^ a g(i(c),j(v),?x_1) ->R^ g(h(?!,d),j(v),?x_1) ->R^ g(b,j(v),?x_1) ->R^ g(b,u,?x_1) ->R^ g(b,u,?!) ->R^ f(?!,?!) ->R^ a Total Time: 0.014 [s] problems/r8.trs: Success(not UNC) real 0.03 user 0.02 sys 0.00