I wrote:
>> 2. Put some arbitrary limit on the number of subconditions in an AND or
>> OR clause before we give up and don't attempt to prove anything about
>> it.
> So option #2 with a cutoff of 100 items or so is looking like the
> best response.
I've applied a patch along this line to 8.2 and up, and also installed
some code (in HEAD only) to cache the results of proof-operator lookup.
regards, tom lane