What I want is to give the generators and relations, as well as an integer $n$, then tell the program to compute the number of elements having word length $\leq n$.
Can someone please show me how to do this? I have very little knowledge of group theory software.
Thanks!
For a given f.g. recursively presented group $G$ and finite generating family, this is algorithmically solvable iff the word problem is solvable.
Indeed, if the word problem is solvable, consider all group words of length $\le n$, compare any two to check what is the "equality in $G$" equivalence relation is, and output the number of classes.
Conversely, consider two group words, say both of length $\le n$. Compute the cardinal $c_n$ of the $n$-ball. Enumerating consequences of relators within the $n$-ball eventually reaches $c_n$ equivalence classes within the $n$-ball. Once reached, just check whether your two elements lie in the same class.