Complexity of minimizing the index of a subgroup of the free group

Let $$\Sigma$$ be a finite alphabet and $$G$$ the free group generated by $$\Sigma$$. Let $$W$$ be a finite subset of $$G$$. (Represented as a list of formal expressions of the form $$a_1^{\pm 1}\ldots a_n^{\pm 1}$$ with $$a_i\in\Sigma$$.) Let $$k$$ be a natural number (represented in unary). We want to decide whether there is a subgroup $$H$$ of $$G$$ s.t.

i. The index of $$H$$ in $$G$$ is at most $$k$$.

ii. $$H$$ is disjoint from $$W$$.

What is the computational complexity of this decision problem?

Currently all I know is that it's in $$\mathrm{NP}$$. Indeed, given $$H$$ as above we can construct the following certificate: Choose a bijection of $$G/H$$ with $$\{1,2\ldots n\}$$ (where $$n$$ is the index of $$H$$), s.t. the coset of the unit is mapped to $$1$$. For every $$a\in\Sigma$$, describe the element of $$\mathrm{S}_n$$ (permutations of $$n$$ elements) induced by $$a$$'s action on $$G/H$$. To validate the certificate, we only need to check that for every $$w\in W$$, the resulting element of $$S_n$$ doesn't preserve $$1$$.

We can also interpret $$G/H$$ as the state space of a permutation automaton with input alphabet $$\Sigma$$. Our problem is then deciding the existence of a permutation automaton with at most $$k$$ states which maps every word in $$W$$ to a non-initial state. This is similar to the well-known problem of deciding the existence of an arbitrary deterministic automaton with at most $$k$$ states that accepts given words and rejects given words. The latter problem is known to be NP-complete (Gold 1978), but the constraint that the automaton is permutation might change things substantially (for example, learning permutation automata is known to be easier in the active setting, see Rivest and Schapire 1993).