Predicate logic rectified form

Question

I have this predicate logic expression

$$\forall X (\forall X p(X) \vee q(X))$$

Which of these expressions are the rectified form?

$$ \forall Y (\forall X p(X) \vee q(Y)) $$

$$ \forall X( \forall Y p(Y) \vee q(Y)) $$

I have been told that the rectified form of a predicate can be obtained by renaming bound variables so that no variable appears in two quantifiers. According to that in my opinion the answer should be the first one but using software I get the second one.

Answer 1

I am with you. The first one is equivalent to the original, but in the second one the $Y$ in $q(Y)$ has become a free variable and the $\forall X$ is a null quantifier, while the original expression did not have any free variables or null quantifiers. Are you sure the software did not say $\forall X (\forall Y p(Y) \lor q(X))$? What software is this?