Most annoying problem in my implementation of the query system is that it will not solve implications if the implicates are far away from each other. For instance, if the graph of known facts is something like this

Integer ----> Rational --> Real --> Complex
  ^  ^
  |  |
  |   -------
  |         |
Prime      Even
  ^
  |
  |
MersennePrime

Then it will not know how to handle the query: Is x complex assuming it is a Mersenne prime ?. This is because the vertices MersennePrime and Complex are far away from each other and the query function does not load the complete graph of known facts, but rather a small subgraph centered on the assumed facts ... This was done so for efficiency reasons, because in the initial implementation I feared that the graph of known facts could become huge and thus making it unfeasible to search into. But things have changed now. Known facts is not huge at all, roughly having over 20 vertices, so it is feasible to build the complete graph the first time query() is called and store it for future uses. And, most important, we have implemented fast algorithms for the problem of boolean satisfiability (DPLL under sympy.logic.algorithms.dpll), so all is ready to implement these ideas in the following days. Interestingly, there seems to me many open source libraries for solving this problem. One that caught my attention early is MiniSAT, a nice little program written in C++ which is really fast