> First, write a bash script P1 that runs a SAT solver on every possible SAT problem and halts if any of them take exponential time. You don't actually have to run P1, just call HALTS(P1, Solver) to see if the solver solves all problems in polynomial time.

That's not recursively enumerable, that's Π₂. And ABC conjecture looks even harder.