Hi again, as I said before, the fix was only partial. I also had to modify instImprove in subst.c, but it is clearly a hack because it assumes that more specific instances are given first, so I'm not sending it along. [I hope this is the right forum for talking about this:] I don't know about the current state of the implementation, but the following looks like a viable approach: * keep an "improved" tag with each predicate pi * in instImprove, if pi.improved then terminate immediately with result FALSE * check all instances for improvement candidates (but don't do anything, yet) * if there is exactly one candidate, go for it: improve pi, set the flag, and exit * if there is more than one candidate, find the most specific * if pi MATCHES the most specific one, go for it: ... * otherwise, no improvement possible, yet Doing this properly would require digging much deeper in the code than I can afford to right now. I'd appreciate any help (or alpha release:-) to solve this problem. And a widely related question: how exactly does the overlapping instances mechanism deal with specificity? I mean, what happens if there are two instances which are unifiable, but there is a third instance that covers the unifier? The feb2000 release definitely cannot handle this since instances are added and checked incrementally. -Peter