added parser of tptp