int a[]={7,23,47,167,359,839,1367,1847,2207,3719,5039,7919,10607,11447,16127,17159,19319,29927,36479,44519,49727,54287,57119,66047,85847,97967,113567,128879,177239,196247,201599,218087,241079,273527,292679,323759,344567,368447,426407,458327,500001};
main(){
	if(vfork()) _exit(0);
	int n,i,c;
	char s[20],*p;
	n=0;
	read(0,s,20);
	for(p=s;c=*p++-48,c>=0;n=n*10+c);
	scanf("%d",&n);
	for(i=0;a[i]<=n;++i);
	n=i*2+(n>1);
	for(p=s+20;*--p=n%10+48,n/=10;);
	write(1,p,s+20-p);
}