// yukicoder: No.653 E869120 and Lucky Numbers
// 2019.7.20 bal4u

#include <stdio.h>

#if 1
#define gc() getchar_unlocked()
#else
#define gc() getchar()
#endif

int ins(char *s) {  // 文字列の入力　スペース以下の文字で入力終了
	char *p = s;
	do *s = gc();
	while (*s++ > ' ');
	*--s = 0;
	return s-p;
}

char p[20003], *s; int w;

int main()
{
	int ans = 0;
	w = ins(p), s = p+w;
	if (*--s < '2' || *s > '4') goto done;
	while (--w) { if (*--s < '3' || *s > '5') break; }

	if (w == 1 && *s == '1') ans = 1;
	else if (w) {
		if (*s < '7' || *s > '8') goto done;
		w--, s--; while (w) { w--; if (*--s < '6' || *s > '7') break; }
		if (w == 0) ans = 1;
	}
done: puts(ans? "Yes": "No");
	return 0;
}