Vallst prologue

    A vallst prologue, which is different from the ordinary prologue beginning
    with a 'p', is a line whose first non-white characters are "cv". If numbers
    follow the vallst prologue start, like this:
    "cv [<nrOf3Clauses> [<nrOfLitOccs>]]", the number <nrOf3Clauses> will be
    taken to be the number of ternary clauses and <nrOfLitOccs> will be taken
    to be the number of literal occurrences, modulo some special accounting (do
    a search on "special accounting"). It's not important that nrOf3Clauses is
    exactly accurate but any fairly accurate estimate might be helpful for
    memory efficiency reasons. Try to make nrOfLitOccs an upper bound.
      A vallst prologue must come before the ordinary 'p'-prologue.
      If there are many vallst prologues defining <nrOf3Clauses>, it's the last
    one (containing a <nrOf3Clauses> number) that counts. The same goes for
    <nrOfLitOccs>.

---