BEGIN {
	print 9223372036854775808
	printf("%d\n", 9223372036854775808)
}