Explicitly make the formulas.
Define function after *PROPOSITIONAL-SYMBOLIC-ATTACKS* is defined.