jukebox

Jukebox is a suite of tools for transforming problems in first-order logic. It reads problems in TPTP (FOF and TFF) format. Currently it can translate typed problems to untyped (by efficiently encoding types) and clausify problems (both typed and untyped).