There exists a polynomial time reduction from SAT to the problem of asking Eliezer Yudkowsky whether a formula is satisfiable. It only remains to be proved that he is not using any hyper-computable processes.