z3_tptp