Extend and simplify yellow marking

Extend yellow marking based on sketches of proofs: we now deal with any number
of variables, not only 2 or 3, and the code is simpler. It should not change
anything for the 2 and 3 cases. And "make test" passes.

Remove old *_norigid heuristics, that have been unused for a long time and are
incompatible with our invariants anyway.