(n65 x) → *
Function: n65$inline
(defun n65$inline (x) (declare (xargs :guard (integerp x))) (mbe :logic (loghead 65 x) :exec (logand 36893488147419103231 x)))
