The following benchmarks result from a transformation of Q-ALL SAT instances
to quantified Boolean formulas in the Q-DIMACS format. For details, see
Remshagen and Truemper,
"An Effective Algorithm for the Futile Questioning
Problem," Journal of Automated Reasoning 34(1), 31-47, 2005.