In case anyone is interested, this test gives an idea of the sort of thing I want to do in the assumptions system (https://code.google.com/p/sympy/issues/detail?id=3929). This would be the result of a query like `ask(~Q.zero(x) & ~Q.zero(y), Q.zero(x*y))` (i.e., is it possible for both `x` and `y` to be nonzero given that `x*y` is zero?).  The assumptions handler system would generate the relevant facts for the problem (here, `facts`), and it would then check `satisfiable(And(assumptions, facts, query))` and `satisfiable(And(assumptions, facts, ~query))`. In this case, they give `False` and a model, respectively, meaning that the query is not true given the set of assumptions, so `ask` would return `False`. If the first had returned a model and the second `False`, the answer would be `True`, and if both returned a model, then the answer would be `None` (if both return `False`, then either the assumptions, the generated facts, or the combination of both are contradictory).