Handle nested (universal) quantifiers in QCF algorithm.  Make relevant domain instantiation breadth-first.
Add variable ordering for QCF to accelerate matching procedure.  Preparing for QCF_MC mode.
Do not use transitive closure module for cycle detection in datatypes (was bottleneck).
minor fix for merge