direct translation from CLIF to TPTP format without the LADR detour