#include <stdio.h>

#define N 10

int main(void){
    int c1,c2,c3;
    int cnt;
     
    while (scanf("%d %d %d", &c1,&c2,&c3)!=EOF){
        cnt=0;
        for (int i=1; i<=N; i++){
            if (i!=c1 && i!=c2 && i!=c3){
                if (c1+c2+i <= 20) cnt++;
            }
        }
        printf(cnt>3 ? "YES\n" : "NO\n");
    }
    return 0;
}