#include<stdio.h>

int main(void){
	double a,b,c,d;
	scanf("%lf%lf",&c,&d);
	if(c*5/2 < d){printf("%.20lf",c*7000);}
	else if(d*3 < c){printf("%.20lf",d*4000);}
	else{
		a = (c*5/2-d)*6/13;
		b = (d*3-c)*5/13;
		c = a*4/3;
		d = b*7/5;
		printf("%.20lf\n",c*1000+d*2000);
	}
	return 0;
}