Does the Isabelle tool "dimacs2hol" from 2004 still have a purpose? The DIMACS CNF format appears to be an old proposal for SAT, predating newer things like SMT-LIB. So this looks like a candidate for deletion. Makarius