Why 'Is not 2QBF' ?

[BoltMaud]

Hello,
Thank you for your tool. I installed it and the tests passed. I created my own file but I don't understand what is wrong in my file, I've got the error :
Is not 2QBF. Currently not supported.
I attached the file : not_working.txt
Thanks for your time.
BoltMaud

[MarkusRabe]

Hi BoltMaud! Thanks for your question. Your file contains unquantified (free) variables, such as variable 1498. In typical QBF literature these would be considered to be implicitly existentially quantified (outside of any quantifier listed in the formula), such that the quantifier prefix would be exists-forall-exists, which is not 2QBF.

Looking at your formula, it appears likely that these free variables were meant to be quantified by the inner existential quantifier. If you add these free variables to the inner existential quantifier explicitly, CADET will accept the formula as a 2QBF.

Let me know if that works, or if I can help you somehow!