A SAT solver might very well have optimizations that make it end up running in 2^200 on average instead of what brute force would give.
The problem is, since the instance is so large, we don't know what happens. No one has ever ran one to completion.
So no, it's not in the hardest class of instances for its size. Its difficulty is unknown.
That puts it in the hardest class of instances for its size (subject to available knowledge), because all instances can be solved by brute force.