Klever

As a mistake experimental implementation of alternative verification tasks generation strategies was merged to master (see #7237). I just was so tired to continue support of that monster branch having too many incompatible changes relatively master but in addition implementing an initial test set for rule specifications as well as quite many improvements in rule specifications themselves.

As a result of merge all strategies except the anolog of the old one don't work even on toy examples. Even though soon we will redesign and reimplement very much of these strategies from scratch, it has sense to fix that dead code, e.g. to understand better what we need to take into account in designing a new approach.