I mean, there might not be a point in optimizing a mechanical search of all possible contradictions in ZFC. Surely any contradiction would be ridiculously complex, and probably doesn't exist. No human-achievable amount of optimization will distinguish between those two.