#include <stdio.h>

int main() {
    int i=0xABCDEF;
printf("%15d",i);
    return 0;
}