even more aggressive instantiation of quantified literals in clauses
added a switch -splitClauses for turning CNF conversion on/off