remove USE_ALLOCATOR

[MichaelRawson]

USE_ALLOCATOR has some history. It used to be mandatory and everything got routed through Vampire's internal allocator. Nowadays system allocators are better so we don't mandate it any more, but USE_ALLOCATOR remains for alleged performance reasons. There are certainly more than strictly required for performance, but I don't know how many.

This is the first try: I couldn't demonstrate any performance difference by just removing all instances, but if @quickbeam123 can with his higher level of compute I will go back to square one and try removing just the really silly ones.

Attached is a log of randomised 1-second DISCOUNT runs on FOF. The right column is the Vampire without USE_ALLOCATOR. This can be used to generate a report

samples		29212

1 wins		754
2 wins		732
both		9141

mean diff	+0.00045s
min diff	-0.96700s
max diff	+0.97900s

p (wins)	0.58593
p (diff)	0.70523

i.e. after an afternoon of compute there was not a statistically-significant difference in timing or win rate on the 1-second runs. The difference in solved problems looks concerning, but this tended to fluctuate back and forth and for the majority of the afternoon Vampire 2 was in the lead, so...trust statistics?

[MichaelRawson]

log.csv