#include <stdint.h>
#include <stdlib.h>
uint64_t add9se_0BB(const uint64_t B,const uint64_t A)
{
uint64_t dout_50, dout_51, dout_55, dout_56, dout_57, dout_58, dout_59, dout_61;
uint64_t O;
dout_50=((A >> 7)&1)^((B >> 7)&1);
dout_51=((A >> 7)&1)&((B >> 7)&1);
dout_55=((A >> 8)&1)^((B >> 8)&1);
dout_56=((A >> 8)&1)&((B >> 8)&1);
dout_57=dout_55&dout_51;
dout_58=dout_55^dout_51;
dout_59=dout_56|dout_57;
dout_61=dout_55^dout_59;
O = 0;
O |= (dout_61&1) << 0;
O |= (dout_61&1) << 1;
O |= (((A >> 6)&1)&1) << 2;
O |= (((B >> 2)&1)&1) << 3;
O |= (((A >> 6)&1)&1) << 4;
O |= (((A >> 6)&1)&1) << 5;
O |= (((B >> 6)&1)&1) << 6;
O |= (dout_50&1) << 7;
O |= (dout_58&1) << 8;
O |= (dout_61&1) << 9;
return O;
}