remove USE_ALLOCATOR where it very likely makes no difference

[MichaelRawson]

In #499 we got rid of quite a few of the old allocator macros. However, it's not possible to remove any more without possibly affecting performance significantly.

This PR removes only those USE_ALLOCATOR instances where in my opinion it's unlikely to make a difference. This could be because:

1. The code is unused.
2. The object is only likely to be created a small number of times: inference engines, decision procedures, SAT solvers, main loops, indices, and the like.
3. The object is used a moderate number of times, but mostly during parsing: symbols, types.
4. The object is never heap-allocated.

This removes roughly two-thirds of the USE_ALLOCATOR instances, which allows us to focus on the trickier ones. In my view this could go in without performance testing, but of course I don't object if you think it needs it.

[quickbeam123]

This seems to be actually helping the notorious discount10 from 8746.8 to 8753.4 TPTP FOL probs in 10000 Mi on average.