#include <bits/stdc++.h>

//const static double	de_PI	= 3.14159265358979323846;
//const static double	de_EPS	= 0.000001;
//const static int	de_MOD = 1000000007;
//const static int	de_MAX = 999999999;
//const static int	de_MIN = -999999999;

int main(void) {

	//std::ifstream inf("123.txt");	std::cin.rdbuf(inf.rdbuf());

	int A = 0, B = 0, ans = 0;
	std::cin >> A >> B;
	ans = 50 * A + ((500 * A) / (8 + 2 * B));
	std::cout << ans << std::endl;
}