#include <stdio.h>
#include <time.h>
time_t xx = 1234567890 ;
main() { printf("%s",ctime(&xx)); }