<?php $dice = trim(fgets(STDIN)); echo $dice*3.5.PHP_EOL;