According to Geoff Sutcliffe:

1. Lots of type formulae are named "type", and lots of axioms are named
   "axiom". Unique names are required, e.g., ...
   tff(type, type, general: $tType).
   tff(type, type, symbol: $tType).
   tff(type, type, f__integer__: ($int) > general).
   tff(type, type, f__symbolic__: (symbol) > general).
   etc.
   tff(axiom, axiom, ![X: general]: (p__is_integer__(X) <=> (?[N: $int]: (X = f__integer__(N))))).
   tff(axiom, axiom, ![X1: general]: (p__is_symbolic__(X1) <=> (?[X2: symbol]: (X1 = f__symbolic__(X2))))).
   tff(axiom, axiom, ![X: general]: ((X = c__infimum__) | p__is_integer__(X) | p__is_symbolic__(X) | (X = c__supremum__))).

I suggest using the symbol as part of the name for types, e.g., ...
tff(general_type, type, general: $tType).
tff(symbol_type, type, symbol: $tType).
tff(f__integer__-decl, type, f__integer__: ($int) > general).
tff(f__symbolic___decl, type, f__symbolic__: (symbol) > general).
etc.
Note the "_type" suffix for declaring types, and the "_decl" suffix when
declaring symbols - it's an informal standard we use. I'm not sure what
you might do for axioms - I can automatically add unique indices if you
don't have a more meaningful idea.

2. You need some ()s, because TPTP does not have symbol precedences. For
   example, in the formula left_0 ...
   ... & ~~tq(V1, V2) => hq(V1, V2) & (V1 = X & V2 = Y & ...
   ... needs ()s to show if it's ...
   ... & ~~tq(V1, V2) => ( hq(V1, V2) & (V1 = X & V2 = Y & ... )
   ... or ...
   ... & ( ~~tq(V1, V2) => hq(V1, V2) ) & (V1 = X & V2 = Y & ...

One way to check for TPTP syntax compliance is put a problem into SystemB4TPTP.