#include<stdio.h>

int main(void){
int c1,c2,c3,c,i,count=0;
	
	while(scanf("%d%d%d",&c1,&c2,&c3)!=EOF){
	c=c1+c2;
	for(i=1;i<=10;i++){
	if(c+i<=20 && c1!=i && c2!=i && c3!=i)count++;
	}
	if(count*100/7>=50)printf("YES\n");
	else printf("NO\n");
	count=0;
	}
	return 0;
}