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