Let $G$ be a finite group, and let $K$ be a field of characteristic zero. Let $\phi(x_1,\ldots,x_n)$ be a first order formula in the language of group theory (so $\phi$ can be for example something of the form $\exists y\in G$ $y^2=x$ or $\exists y_1,y_2\in G $ $ x_1=y_1y_2,x_2=y_2y_1$). For every such formula $\phi$ we consider the element $$t_{\phi}:=\sum_{\{(g_1,\ldots g_n)\in G^n| \phi(g_1,\ldots g_n)\}}g_1\otimes g_2\otimes\cdots\otimes g_n$$ In other words, $t_{\phi}$ is the sum over all tuples who satisfy the formula $\phi$. If now $\mu:G\to G$ is a group automorphism, then $\phi(g_1,\ldots,g_n)$ holds if and only if $\phi(\mu(g_1),\ldots,\mu(g_n))$ holds. It thus follows that the elements $t_{\phi}$ are all $Aut(G)$-invariants inside $(KG)^{\otimes n}$.
Is there an elementary proof that the elements $t_{\phi}$ span the invariant subspace $(KG^{\otimes n})^{Aut(G)}$?