implicitly, older goals are resolved first, if some goals have equal
weights. This is encoded in the "w <=" comparison; if this is set to
"w <", the heuristic becomes much less effective.
Preliminary results:
1. For typed matching, either heuristic 32 or 34 are best, and far
superior to the previous best (3).
2. For untyped matching, partial tests indicate that heuristic 1 is
best, which is rather interesting.
