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.
#!/usr/bin/env bash
#
# Wrapper for SPASS that also outputs the Flotter-generated CNF (needed for
# Isar proof reconstruction)
#
# Author: Jasmin Blanchette, TU Muenchen
options=${@:1:$(($#-1))}
name=${@:$(($#)):1}
$SPASS_HOME/tptp2dfg $name $name.fof.dfg
$SPASS_HOME/SPASS -Flotter $name.fof.dfg \
| sed 's/description({$/description({*/' \
> $name.cnf.dfg
rm -f $name.fof.dfg
cat $name.cnf.dfg
$SPASS_HOME/SPASS $options $name.cnf.dfg
rm -f $name.cnf.dfg