Parallel proving should be a big bonus. Nipkow found that on the Isabelle test set, using 3 theorem proves in parallel gave as good results in 5 seconds as the best among them gave in 120.