I managed to overcome the overhead in ask() that arises when converting between symbol and integer representation of sentences in conjunctive normal. The result went beyond what I expected. The test suite for the query module got 10x times faster in my laptop. From 26 seconds, it descended to an impressive 2.03 secs. There is still room for improvement, but it is no longer "so desperately slow". I'll submit those patches soon to sympy's trunk, but in the meantime they are in my logic branch: git pull http://fa.bianp.net/git/sympy.git logic