Only continue strategy execution if all parallel provers failed

The previous code improperly handled parallel provers when a prover failed: it would launch an instance of the strategy for each failed prover!

Instead, this changes the code to use a semaphore like construct to only continue the strategy execution if the whole batch of provers failed.