Fix a bug that converted each Square into Neg during variable renaming.
Disabled DFSThenBFS and BFSFalsifyOnly.  Improved formula formatting. 
Improved code for processing tightness levels.