Working on SAT.lhs.  Subject to minimal testing, tseitin now seems to be working.