Reads the use_theories payload of an Isabelle server into SZS values.

Isabelle does not print SZS lines. Its result is a list of messages with positions, and the verdict for a lemma is read from the messages at its position. classify/1 treats every message as one bucket; per_lemma/3 buckets them by the line range each lemma covers.

Verdict precedence

Within a bucket, the signals read from its messages are reconciled in this order, each step short-circuiting:

1. :counter_satisfiable — a Nitpick or Quickcheck counterexample disproves the goal and dominates any concurrent proof attempt.
2. :theorem from a sledgehammer or metis found a proof line.
3. :satisfiable — a Nitpick or Quickcheck model.
4. A Failed to finish proof or Failed to apply initial proof method error vetoes a theorem name: echo from the same bucket: Isabelle prints the goal at the by position whether or not the method closed it.
5. :theorem from a theorem name: completion.
6. :timeout, :memory_out, then :gave_up.

A bucket with no signal is :gave_up. Messages are read one at a time, never across their concatenation: Nitpick found a model followed by Nitpick found no counterexample reads as a model, not as a counterexample.