[eynsham]

Oh, you’re right! Well, hm, how about SAT-PRIME' = {φ: φ is satisfiable and its Gödel number (under some scheme) has [some property]}.

[suyjuris]

I would guess that this can work, but it seems impossible to prove. I do not have any good candidates for an NP problem that is provably harder than SAT for a deterministic Turing machine, though I would not be surprised if some tricky diagonalisation argument works.