keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
this is rather involved because the Flotter FOF-to-CNF translator is normally implicit.
We must make this an explicit step and parse the Flotter output to find out which clauses correspond to which formulas.