tptp.gen 876 Bytes