prove the current goal using bdds
(bdd :vars nil :bdd-constructors (cons) :prove t :literal :all)
The general form is as shown in the latter example above, but with any
keyword-value pairs omitted and with values as described for the :bdd hint; see hints.
This command simply calls the theorem prover with the indicated bdd hint
for the top-level goal. Note that if :prove is t (the default),
then the proof will succeed entirely using bdds or else it will fail
immediately. See bdd.