Objective level literals in Formulas get special treatment.

The objective level literals should only be SF literals (which occur
there due to regression of K or B literals).
After regression, but before reduction, we check for each literal
outside of any K or B modality whether or not it is entailed and
replace the literal with True or False, respectively. For this to work,
regression skips these literals. When checking their truth, we do
regress the literal alone given that the BAT is in regression mode.

Notice that maintaining a set of SF literals is not sufficient, because
we usually don't add trivially true SF literals for non-sensing actions.

By the way, these trivially true SF literals lead to no additional
entailments because due to regression we end up with a trivially true
formula.

An open problem is how to integrate this with the ESL style, i.e., when
not using regression.