Let set_solver not use eauto by default.
In most cases there is a lot of duplicate proof search performed by both naive_solver and eauto. Especially since naive_solver calls its tactic (in the case of set_solver this used to be eauto) quite eagerly this made it very slow. Note that set_solver is this too slow and should be improved.
Showing with 13 additions and 23 deletions