In reply to Paul Kaefer.

You are correct, Paul. It started as a less than 128-core machine. But my imagination settled on 128. It is still running as a condition of the theorem to be true. Happy belated April's Fools Day!