#include<stdio.h>
#include<string.h>
int main()
{
 char a[10]="12345";
 gets(a);
 strcat(a,"6789");
 printf("%s\n",a+1);
 return 0;
}