Handle nested (universal) quantifiers in QCF algorithm.  Make relevant domain instantiation breadth-first.