#include "math.h"

$input double x;
$assume(-10 < x && x < 10);

int main() {
  double y = -2. * ((-x / 5.) - 1./3.);
  
  $assume(y != 0);
  y = pow(y, 1./2.);	
  $assert(y - 1>= 0);
  return (int)y;
}