#include <bits/stdc++.h>

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

int main(void) {

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

	unsigned long long R = 0, C = 0, ans = 0;
	std::cin >> R >> C;

	if (R == C) {
		if (R % 2 == 0) {
			ans = R*R / 4 - 1;
		}
		else {
			ans = (R*R + 3) / 4 - 1;
		}
	}
	else {
		if (R % 2 == 0 || C % 2 == 0) {
			ans = R*C / 2 - 1;
		}
		else {
			ans = (R*C + 1) / 2 - 1;
		}
	}

	std::cout << ans << std::endl;

}