Latest version of METIS_TAC.

The biggest change is that scheduling provers is done by number of
inferences, not time used, so METIS_TAC is now completely
deterministic. If it works for you on a subgoal, it will work every
time HOL4 is built.

New version of Metis:

+ Uses finite models to guide clause selection in resolution.
+ A Metis test for when HOL is compiled using MLton.