// 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 main()
{
	int ans = 0;
	s = p + ins(p+1);
	if (*s >= '2' && *s <= '4') {
		while (*--s >= '3' && *s <= '5');
		if (*s == '1' && *(s-1) == 0) ans = 1;
		else if (*s == '7' || *s == '8') {
			while (*--s == '6' || *s == '7');
			if (*s == 0) ans = 1;
		}
	}
	puts(ans? "Yes": "No");
	return 0;
}