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