operator.  The result depends only on the two input operators and the proof
direction (imply or refute), so it's easy to cache.  This provides a very
large savings in cases such as Sergey Konoplev's long NOT-IN-list example,
where predtest spends all its time repeatedly figuring out that the same pair
of operators cannot be used to prove anything.  (But of course the O(N^2)
behavior still catches up with you eventually.)  I'm not convinced it buys
a whole lot when constraint_exclusion isn't turned on, but it's not a lot
of added code so we might as well cache all the time.