This question is not asking for a solution, but rather as a check / validation of my thought process.
Given the form: $W = \forall X.((\forall Y.\exists Z. R(X,Y,Z)) \land \forall S. \exists T. R(X, S,T))$
The algorithm I learnt states, that I have to 1th bring $W$ into prenex form. Doing so I bring all quantors to the beginning, if necessary resolve all variable dependencies by defining fresh variables. The exact sequence of the operators has to be maintained in the process!
2th I look for something of the form: $ \forall x_1. \forall x_2. \forall x_3 \dots \exists y_1 \exists y_2 (R(y_1, y_2))$ and replace it by something like $ \forall x_1. \forall x_2. \forall x_3 (R(g(x_1, x_2, x_3, \dots), f(x_1, x_2, x_3, \dots))) $
In the above example $W$, following strictly the rules stated previously, I would expect the result:
Prenexform: $\forall X.\forall Y. \exists Z. \forall S. \exists T. (R(X,Y,Z)) \land R(X, S,T)) $
Skolemform: $ \forall X.\forall Y. \forall S. (R(X,Y,g(X,Y)) \land R(X, S,f(X,Y,S)) $, which might be correct, but kinda dumb looking.
Thus the question arises, if the rules above are absolut, if there were not a way to soften them and for example allow to switch the order of $\forall$ and $\exists$ operators.
Any constructive comments/answers to my question are appreciated.