If a Turing Machine were to guess,
With less computational stress,
Polynomially check
That its guess was not dreck,
Thus avoiding enumerative mess.
The machine would then certainly be
Witness to a language in NP.
By guessing, we shirk
Exponential-time work.
Nondeterminism can do search for free.
Cook and Levin, I am now recalling
Found a language L that's really galling:
If there is time compaction
To prove satisfaction
Then P=NP--appalling!
It is computational fate
To encounter such barriers we hate.
Yet there are computations
To find estimations
Within factors approximate.