Indeed the "symmetrized square-free monomials" seem to generate. (Order lexicographically and look what the highest term in a product looks like. Now use that to concoct rewriting rules.) They also seem to be independent, as the transcendence degree matches. One may wish to check the degree of the full ring as a module over the predicted subring. For example, K[x,y] as a module over K[x+y,xy] has basis 1, x, but why?
Wilberd