Make hoarescratch.sc work with fix to tptp output.