Protect some Unicode in a .sig file's comments

.sig files weren't being checked with the call to grep previously.

Improve HolQbfLib.decide_any

(Progress on #1)

It should now deal with free variables in the input term. Also, fixed a
bug for dealing with a sequence of multiple innermost universal
quantifiers, and in so doing redesigned qbf_prenex_conv substantially.

Also, added another self test and made the self test check for decide_any
check whether an appropriate theorem was produced (rather than assuming
any theorem returned is ok).

Progress on HolQbfLib.decide_any

It should now accept any closed QBF (variables, conjunctions,
disjunctions, implications, quantifiers) as long as all quantified
variables occur somewhere (or maybe even some examples where they
don't).

Improvements to functions in QbfConv welcome.