Use known_facts_cnf in newask()

This slows it down a bit, because the SAT problem it solves is much larger
(and it also takes longer to generate the relevant facts).

This also changes a test, because in the new assumptions, Q.nonzero means
Q.real and ~Q.zero, not just ~Q.zero.