(n60 x) → *
Function: n60$inline
(defun n60$inline (x) (declare (xargs :guard (integerp x))) (mbe :logic (loghead 60 x) :exec (logand 1152921504606846975 x)))
