#include <stdio.h>
int main() {
   printf("%15d",0xABCDEF);
    return 0;
}