<?php
$moji = trim(fgets(STDIN));
$count = substr_count($moji, "575");
echo $count >= 1 ? "YES" : "NO";