static void femul(uint32_t out[22], const uint32_t in1[22], const uint32_t in2[22]) {
  { const uint32_t x44 = in1[21];
  { const uint32_t x45 = in1[20];
  { const uint32_t x43 = in1[19];
  { const uint32_t x41 = in1[18];
  { const uint32_t x39 = in1[17];
  { const uint32_t x37 = in1[16];
  { const uint32_t x35 = in1[15];
  { const uint32_t x33 = in1[14];
  { const uint32_t x31 = in1[13];
  { const uint32_t x29 = in1[12];
  { const uint32_t x27 = in1[11];
  { const uint32_t x25 = in1[10];
  { const uint32_t x23 = in1[9];
  { const uint32_t x21 = in1[8];
  { const uint32_t x19 = in1[7];
  { const uint32_t x17 = in1[6];
  { const uint32_t x15 = in1[5];
  { const uint32_t x13 = in1[4];
  { const uint32_t x11 = in1[3];
  { const uint32_t x9 = in1[2];
  { const uint32_t x7 = in1[1];
  { const uint32_t x5 = in1[0];
  { const uint32_t x86 = in2[21];
  { const uint32_t x87 = in2[20];
  { const uint32_t x85 = in2[19];
  { const uint32_t x83 = in2[18];
  { const uint32_t x81 = in2[17];
  { const uint32_t x79 = in2[16];
  { const uint32_t x77 = in2[15];
  { const uint32_t x75 = in2[14];
  { const uint32_t x73 = in2[13];
  { const uint32_t x71 = in2[12];
  { const uint32_t x69 = in2[11];
  { const uint32_t x67 = in2[10];
  { const uint32_t x65 = in2[9];
  { const uint32_t x63 = in2[8];
  { const uint32_t x61 = in2[7];
  { const uint32_t x59 = in2[6];
  { const uint32_t x57 = in2[5];
  { const uint32_t x55 = in2[4];
  { const uint32_t x53 = in2[3];
  { const uint32_t x51 = in2[2];
  { const uint32_t x49 = in2[1];
  { const uint32_t x47 = in2[0];
  { uint64_t x88 = (((uint64_t)x5 * x86) + ((0x2 * ((uint64_t)x7 * x87)) + ((0x2 * ((uint64_t)x9 * x85)) + ((0x2 * ((uint64_t)x11 * x83)) + (((uint64_t)x13 * x81) + ((0x2 * ((uint64_t)x15 * x79)) + ((0x2 * ((uint64_t)x17 * x77)) + ((0x2 * ((uint64_t)x19 * x75)) + (((uint64_t)x21 * x73) + ((0x2 * ((uint64_t)x23 * x71)) + ((0x2 * ((uint64_t)x25 * x69)) + ((0x2 * ((uint64_t)x27 * x67)) + ((0x2 * ((uint64_t)x29 * x65)) + (((uint64_t)x31 * x63) + ((0x2 * ((uint64_t)x33 * x61)) + ((0x2 * ((uint64_t)x35 * x59)) + ((0x2 * ((uint64_t)x37 * x57)) + (((uint64_t)x39 * x55) + ((0x2 * ((uint64_t)x41 * x53)) + ((0x2 * ((uint64_t)x43 * x51)) + ((0x2 * ((uint64_t)x45 * x49)) + ((uint64_t)x44 * x47))))))))))))))))))))));
  { uint64_t x89 = ((((uint64_t)x5 * x87) + ((0x2 * ((uint64_t)x7 * x85)) + ((0x2 * ((uint64_t)x9 * x83)) + (((uint64_t)x11 * x81) + (((uint64_t)x13 * x79) + ((0x2 * ((uint64_t)x15 * x77)) + ((0x2 * ((uint64_t)x17 * x75)) + (((uint64_t)x19 * x73) + (((uint64_t)x21 * x71) + ((0x2 * ((uint64_t)x23 * x69)) + ((0x2 * ((uint64_t)x25 * x67)) + ((0x2 * ((uint64_t)x27 * x65)) + (((uint64_t)x29 * x63) + (((uint64_t)x31 * x61) + ((0x2 * ((uint64_t)x33 * x59)) + ((0x2 * ((uint64_t)x35 * x57)) + (((uint64_t)x37 * x55) + (((uint64_t)x39 * x53) + ((0x2 * ((uint64_t)x41 * x51)) + ((0x2 * ((uint64_t)x43 * x49)) + ((uint64_t)x45 * x47))))))))))))))))))))) + (0xbb * ((uint64_t)x44 * x86)));
  { uint64_t x90 = ((((uint64_t)x5 * x85) + ((0x2 * ((uint64_t)x7 * x83)) + (((uint64_t)x9 * x81) + (((uint64_t)x11 * x79) + (((uint64_t)x13 * x77) + ((0x2 * ((uint64_t)x15 * x75)) + (((uint64_t)x17 * x73) + (((uint64_t)x19 * x71) + (((uint64_t)x21 * x69) + ((0x2 * ((uint64_t)x23 * x67)) + ((0x2 * ((uint64_t)x25 * x65)) + (((uint64_t)x27 * x63) + (((uint64_t)x29 * x61) + (((uint64_t)x31 * x59) + ((0x2 * ((uint64_t)x33 * x57)) + (((uint64_t)x35 * x55) + (((uint64_t)x37 * x53) + (((uint64_t)x39 * x51) + ((0x2 * ((uint64_t)x41 * x49)) + ((uint64_t)x43 * x47)))))))))))))))))))) + (0xbb * (((uint64_t)x45 * x86) + ((uint64_t)x44 * x87))));
  { uint64_t x91 = ((((uint64_t)x5 * x83) + (((uint64_t)x7 * x81) + (((uint64_t)x9 * x79) + (((uint64_t)x11 * x77) + (((uint64_t)x13 * x75) + (((uint64_t)x15 * x73) + (((uint64_t)x17 * x71) + (((uint64_t)x19 * x69) + (((uint64_t)x21 * x67) + ((0x2 * ((uint64_t)x23 * x65)) + (((uint64_t)x25 * x63) + (((uint64_t)x27 * x61) + (((uint64_t)x29 * x59) + (((uint64_t)x31 * x57) + (((uint64_t)x33 * x55) + (((uint64_t)x35 * x53) + (((uint64_t)x37 * x51) + (((uint64_t)x39 * x49) + ((uint64_t)x41 * x47))))))))))))))))))) + (0xbb * (((uint64_t)x43 * x86) + (((uint64_t)x45 * x87) + ((uint64_t)x44 * x85)))));
  { uint64_t x92 = ((((uint64_t)x5 * x81) + ((0x2 * ((uint64_t)x7 * x79)) + ((0x2 * ((uint64_t)x9 * x77)) + ((0x2 * ((uint64_t)x11 * x75)) + (((uint64_t)x13 * x73) + ((0x2 * ((uint64_t)x15 * x71)) + ((0x2 * ((uint64_t)x17 * x69)) + ((0x2 * ((uint64_t)x19 * x67)) + ((0x2 * ((uint64_t)x21 * x65)) + ((0x2 * ((uint64_t)x23 * x63)) + ((0x2 * ((uint64_t)x25 * x61)) + ((0x2 * ((uint64_t)x27 * x59)) + ((0x2 * ((uint64_t)x29 * x57)) + (((uint64_t)x31 * x55) + ((0x2 * ((uint64_t)x33 * x53)) + ((0x2 * ((uint64_t)x35 * x51)) + ((0x2 * ((uint64_t)x37 * x49)) + ((uint64_t)x39 * x47)))))))))))))))))) + (0xbb * ((0x2 * ((uint64_t)x41 * x86)) + ((0x2 * ((uint64_t)x43 * x87)) + ((0x2 * ((uint64_t)x45 * x85)) + (0x2 * ((uint64_t)x44 * x83)))))));
  { uint64_t x93 = ((((uint64_t)x5 * x79) + ((0x2 * ((uint64_t)x7 * x77)) + ((0x2 * ((uint64_t)x9 * x75)) + (((uint64_t)x11 * x73) + (((uint64_t)x13 * x71) + ((0x2 * ((uint64_t)x15 * x69)) + ((0x2 * ((uint64_t)x17 * x67)) + ((0x2 * ((uint64_t)x19 * x65)) + (((uint64_t)x21 * x63) + ((0x2 * ((uint64_t)x23 * x61)) + ((0x2 * ((uint64_t)x25 * x59)) + ((0x2 * ((uint64_t)x27 * x57)) + (((uint64_t)x29 * x55) + (((uint64_t)x31 * x53) + ((0x2 * ((uint64_t)x33 * x51)) + ((0x2 * ((uint64_t)x35 * x49)) + ((uint64_t)x37 * x47))))))))))))))))) + (0xbb * (((uint64_t)x39 * x86) + ((0x2 * ((uint64_t)x41 * x87)) + ((0x2 * ((uint64_t)x43 * x85)) + ((0x2 * ((uint64_t)x45 * x83)) + ((uint64_t)x44 * x81)))))));
  { uint64_t x94 = ((((uint64_t)x5 * x77) + ((0x2 * ((uint64_t)x7 * x75)) + (((uint64_t)x9 * x73) + (((uint64_t)x11 * x71) + (((uint64_t)x13 * x69) + ((0x2 * ((uint64_t)x15 * x67)) + ((0x2 * ((uint64_t)x17 * x65)) + (((uint64_t)x19 * x63) + (((uint64_t)x21 * x61) + ((0x2 * ((uint64_t)x23 * x59)) + ((0x2 * ((uint64_t)x25 * x57)) + (((uint64_t)x27 * x55) + (((uint64_t)x29 * x53) + (((uint64_t)x31 * x51) + ((0x2 * ((uint64_t)x33 * x49)) + ((uint64_t)x35 * x47)))))))))))))))) + (0xbb * (((uint64_t)x37 * x86) + (((uint64_t)x39 * x87) + ((0x2 * ((uint64_t)x41 * x85)) + ((0x2 * ((uint64_t)x43 * x83)) + (((uint64_t)x45 * x81) + ((uint64_t)x44 * x79))))))));
  { uint64_t x95 = ((((uint64_t)x5 * x75) + (((uint64_t)x7 * x73) + (((uint64_t)x9 * x71) + (((uint64_t)x11 * x69) + (((uint64_t)x13 * x67) + ((0x2 * ((uint64_t)x15 * x65)) + (((uint64_t)x17 * x63) + (((uint64_t)x19 * x61) + (((uint64_t)x21 * x59) + ((0x2 * ((uint64_t)x23 * x57)) + (((uint64_t)x25 * x55) + (((uint64_t)x27 * x53) + (((uint64_t)x29 * x51) + (((uint64_t)x31 * x49) + ((uint64_t)x33 * x47))))))))))))))) + (0xbb * (((uint64_t)x35 * x86) + (((uint64_t)x37 * x87) + (((uint64_t)x39 * x85) + ((0x2 * ((uint64_t)x41 * x83)) + (((uint64_t)x43 * x81) + (((uint64_t)x45 * x79) + ((uint64_t)x44 * x77)))))))));
  { uint64_t x96 = ((((uint64_t)x5 * x73) + ((0x2 * ((uint64_t)x7 * x71)) + ((0x2 * ((uint64_t)x9 * x69)) + ((0x2 * ((uint64_t)x11 * x67)) + ((0x2 * ((uint64_t)x13 * x65)) + ((0x2 * ((uint64_t)x15 * x63)) + ((0x2 * ((uint64_t)x17 * x61)) + ((0x2 * ((uint64_t)x19 * x59)) + ((0x2 * ((uint64_t)x21 * x57)) + ((0x2 * ((uint64_t)x23 * x55)) + ((0x2 * ((uint64_t)x25 * x53)) + ((0x2 * ((uint64_t)x27 * x51)) + ((0x2 * ((uint64_t)x29 * x49)) + ((uint64_t)x31 * x47)))))))))))))) + (0xbb * ((0x2 * ((uint64_t)x33 * x86)) + ((0x2 * ((uint64_t)x35 * x87)) + ((0x2 * ((uint64_t)x37 * x85)) + ((0x2 * ((uint64_t)x39 * x83)) + ((0x2 * ((uint64_t)x41 * x81)) + ((0x2 * ((uint64_t)x43 * x79)) + ((0x2 * ((uint64_t)x45 * x77)) + (0x2 * ((uint64_t)x44 * x75)))))))))));
  { uint64_t x97 = ((((uint64_t)x5 * x71) + ((0x2 * ((uint64_t)x7 * x69)) + ((0x2 * ((uint64_t)x9 * x67)) + ((0x2 * ((uint64_t)x11 * x65)) + (((uint64_t)x13 * x63) + ((0x2 * ((uint64_t)x15 * x61)) + ((0x2 * ((uint64_t)x17 * x59)) + ((0x2 * ((uint64_t)x19 * x57)) + (((uint64_t)x21 * x55) + ((0x2 * ((uint64_t)x23 * x53)) + ((0x2 * ((uint64_t)x25 * x51)) + ((0x2 * ((uint64_t)x27 * x49)) + ((uint64_t)x29 * x47))))))))))))) + (0xbb * (((uint64_t)x31 * x86) + ((0x2 * ((uint64_t)x33 * x87)) + ((0x2 * ((uint64_t)x35 * x85)) + ((0x2 * ((uint64_t)x37 * x83)) + (((uint64_t)x39 * x81) + ((0x2 * ((uint64_t)x41 * x79)) + ((0x2 * ((uint64_t)x43 * x77)) + ((0x2 * ((uint64_t)x45 * x75)) + ((uint64_t)x44 * x73)))))))))));
  { uint64_t x98 = ((((uint64_t)x5 * x69) + ((0x2 * ((uint64_t)x7 * x67)) + ((0x2 * ((uint64_t)x9 * x65)) + (((uint64_t)x11 * x63) + (((uint64_t)x13 * x61) + ((0x2 * ((uint64_t)x15 * x59)) + ((0x2 * ((uint64_t)x17 * x57)) + (((uint64_t)x19 * x55) + (((uint64_t)x21 * x53) + ((0x2 * ((uint64_t)x23 * x51)) + ((0x2 * ((uint64_t)x25 * x49)) + ((uint64_t)x27 * x47)))))))))))) + (0xbb * (((uint64_t)x29 * x86) + (((uint64_t)x31 * x87) + ((0x2 * ((uint64_t)x33 * x85)) + ((0x2 * ((uint64_t)x35 * x83)) + (((uint64_t)x37 * x81) + (((uint64_t)x39 * x79) + ((0x2 * ((uint64_t)x41 * x77)) + ((0x2 * ((uint64_t)x43 * x75)) + (((uint64_t)x45 * x73) + ((uint64_t)x44 * x71))))))))))));
  { uint64_t x99 = ((((uint64_t)x5 * x67) + ((0x2 * ((uint64_t)x7 * x65)) + (((uint64_t)x9 * x63) + (((uint64_t)x11 * x61) + (((uint64_t)x13 * x59) + ((0x2 * ((uint64_t)x15 * x57)) + (((uint64_t)x17 * x55) + (((uint64_t)x19 * x53) + (((uint64_t)x21 * x51) + ((0x2 * ((uint64_t)x23 * x49)) + ((uint64_t)x25 * x47))))))))))) + (0xbb * (((uint64_t)x27 * x86) + (((uint64_t)x29 * x87) + (((uint64_t)x31 * x85) + ((0x2 * ((uint64_t)x33 * x83)) + (((uint64_t)x35 * x81) + (((uint64_t)x37 * x79) + (((uint64_t)x39 * x77) + ((0x2 * ((uint64_t)x41 * x75)) + (((uint64_t)x43 * x73) + (((uint64_t)x45 * x71) + ((uint64_t)x44 * x69)))))))))))));
  { uint64_t x100 = ((((uint64_t)x5 * x65) + (((uint64_t)x7 * x63) + (((uint64_t)x9 * x61) + (((uint64_t)x11 * x59) + (((uint64_t)x13 * x57) + (((uint64_t)x15 * x55) + (((uint64_t)x17 * x53) + (((uint64_t)x19 * x51) + (((uint64_t)x21 * x49) + ((uint64_t)x23 * x47)))))))))) + (0xbb * (((uint64_t)x25 * x86) + (((uint64_t)x27 * x87) + (((uint64_t)x29 * x85) + (((uint64_t)x31 * x83) + (((uint64_t)x33 * x81) + (((uint64_t)x35 * x79) + (((uint64_t)x37 * x77) + (((uint64_t)x39 * x75) + (((uint64_t)x41 * x73) + (((uint64_t)x43 * x71) + (((uint64_t)x45 * x69) + ((uint64_t)x44 * x67))))))))))))));
  { uint64_t x101 = ((((uint64_t)x5 * x63) + ((0x2 * ((uint64_t)x7 * x61)) + ((0x2 * ((uint64_t)x9 * x59)) + ((0x2 * ((uint64_t)x11 * x57)) + (((uint64_t)x13 * x55) + ((0x2 * ((uint64_t)x15 * x53)) + ((0x2 * ((uint64_t)x17 * x51)) + ((0x2 * ((uint64_t)x19 * x49)) + ((uint64_t)x21 * x47))))))))) + (0xbb * ((0x2 * ((uint64_t)x23 * x86)) + ((0x2 * ((uint64_t)x25 * x87)) + ((0x2 * ((uint64_t)x27 * x85)) + ((0x2 * ((uint64_t)x29 * x83)) + (((uint64_t)x31 * x81) + ((0x2 * ((uint64_t)x33 * x79)) + ((0x2 * ((uint64_t)x35 * x77)) + ((0x2 * ((uint64_t)x37 * x75)) + (((uint64_t)x39 * x73) + ((0x2 * ((uint64_t)x41 * x71)) + ((0x2 * ((uint64_t)x43 * x69)) + ((0x2 * ((uint64_t)x45 * x67)) + (0x2 * ((uint64_t)x44 * x65))))))))))))))));
  { uint64_t x102 = ((((uint64_t)x5 * x61) + ((0x2 * ((uint64_t)x7 * x59)) + ((0x2 * ((uint64_t)x9 * x57)) + (((uint64_t)x11 * x55) + (((uint64_t)x13 * x53) + ((0x2 * ((uint64_t)x15 * x51)) + ((0x2 * ((uint64_t)x17 * x49)) + ((uint64_t)x19 * x47)))))))) + (0xbb * (((uint64_t)x21 * x86) + ((0x2 * ((uint64_t)x23 * x87)) + ((0x2 * ((uint64_t)x25 * x85)) + ((0x2 * ((uint64_t)x27 * x83)) + (((uint64_t)x29 * x81) + (((uint64_t)x31 * x79) + ((0x2 * ((uint64_t)x33 * x77)) + ((0x2 * ((uint64_t)x35 * x75)) + (((uint64_t)x37 * x73) + (((uint64_t)x39 * x71) + ((0x2 * ((uint64_t)x41 * x69)) + ((0x2 * ((uint64_t)x43 * x67)) + ((0x2 * ((uint64_t)x45 * x65)) + ((uint64_t)x44 * x63))))))))))))))));
  { uint64_t x103 = ((((uint64_t)x5 * x59) + ((0x2 * ((uint64_t)x7 * x57)) + (((uint64_t)x9 * x55) + (((uint64_t)x11 * x53) + (((uint64_t)x13 * x51) + ((0x2 * ((uint64_t)x15 * x49)) + ((uint64_t)x17 * x47))))))) + (0xbb * (((uint64_t)x19 * x86) + (((uint64_t)x21 * x87) + ((0x2 * ((uint64_t)x23 * x85)) + ((0x2 * ((uint64_t)x25 * x83)) + (((uint64_t)x27 * x81) + (((uint64_t)x29 * x79) + (((uint64_t)x31 * x77) + ((0x2 * ((uint64_t)x33 * x75)) + (((uint64_t)x35 * x73) + (((uint64_t)x37 * x71) + (((uint64_t)x39 * x69) + ((0x2 * ((uint64_t)x41 * x67)) + ((0x2 * ((uint64_t)x43 * x65)) + (((uint64_t)x45 * x63) + ((uint64_t)x44 * x61)))))))))))))))));
  { uint64_t x104 = ((((uint64_t)x5 * x57) + (((uint64_t)x7 * x55) + (((uint64_t)x9 * x53) + (((uint64_t)x11 * x51) + (((uint64_t)x13 * x49) + ((uint64_t)x15 * x47)))))) + (0xbb * (((uint64_t)x17 * x86) + (((uint64_t)x19 * x87) + (((uint64_t)x21 * x85) + ((0x2 * ((uint64_t)x23 * x83)) + (((uint64_t)x25 * x81) + (((uint64_t)x27 * x79) + (((uint64_t)x29 * x77) + (((uint64_t)x31 * x75) + (((uint64_t)x33 * x73) + (((uint64_t)x35 * x71) + (((uint64_t)x37 * x69) + (((uint64_t)x39 * x67) + ((0x2 * ((uint64_t)x41 * x65)) + (((uint64_t)x43 * x63) + (((uint64_t)x45 * x61) + ((uint64_t)x44 * x59))))))))))))))))));
  { uint64_t x105 = ((((uint64_t)x5 * x55) + ((0x2 * ((uint64_t)x7 * x53)) + ((0x2 * ((uint64_t)x9 * x51)) + ((0x2 * ((uint64_t)x11 * x49)) + ((uint64_t)x13 * x47))))) + (0xbb * ((0x2 * ((uint64_t)x15 * x86)) + ((0x2 * ((uint64_t)x17 * x87)) + ((0x2 * ((uint64_t)x19 * x85)) + ((0x2 * ((uint64_t)x21 * x83)) + ((0x2 * ((uint64_t)x23 * x81)) + ((0x2 * ((uint64_t)x25 * x79)) + ((0x2 * ((uint64_t)x27 * x77)) + ((0x2 * ((uint64_t)x29 * x75)) + (((uint64_t)x31 * x73) + ((0x2 * ((uint64_t)x33 * x71)) + ((0x2 * ((uint64_t)x35 * x69)) + ((0x2 * ((uint64_t)x37 * x67)) + ((0x2 * ((uint64_t)x39 * x65)) + ((0x2 * ((uint64_t)x41 * x63)) + ((0x2 * ((uint64_t)x43 * x61)) + ((0x2 * ((uint64_t)x45 * x59)) + (0x2 * ((uint64_t)x44 * x57))))))))))))))))))));
  { uint64_t x106 = ((((uint64_t)x5 * x53) + ((0x2 * ((uint64_t)x7 * x51)) + ((0x2 * ((uint64_t)x9 * x49)) + ((uint64_t)x11 * x47)))) + (0xbb * (((uint64_t)x13 * x86) + ((0x2 * ((uint64_t)x15 * x87)) + ((0x2 * ((uint64_t)x17 * x85)) + ((0x2 * ((uint64_t)x19 * x83)) + (((uint64_t)x21 * x81) + ((0x2 * ((uint64_t)x23 * x79)) + ((0x2 * ((uint64_t)x25 * x77)) + ((0x2 * ((uint64_t)x27 * x75)) + (((uint64_t)x29 * x73) + (((uint64_t)x31 * x71) + ((0x2 * ((uint64_t)x33 * x69)) + ((0x2 * ((uint64_t)x35 * x67)) + ((0x2 * ((uint64_t)x37 * x65)) + (((uint64_t)x39 * x63) + ((0x2 * ((uint64_t)x41 * x61)) + ((0x2 * ((uint64_t)x43 * x59)) + ((0x2 * ((uint64_t)x45 * x57)) + ((uint64_t)x44 * x55))))))))))))))))))));
  { uint64_t x107 = ((((uint64_t)x5 * x51) + ((0x2 * ((uint64_t)x7 * x49)) + ((uint64_t)x9 * x47))) + (0xbb * (((uint64_t)x11 * x86) + (((uint64_t)x13 * x87) + ((0x2 * ((uint64_t)x15 * x85)) + ((0x2 * ((uint64_t)x17 * x83)) + (((uint64_t)x19 * x81) + (((uint64_t)x21 * x79) + ((0x2 * ((uint64_t)x23 * x77)) + ((0x2 * ((uint64_t)x25 * x75)) + (((uint64_t)x27 * x73) + (((uint64_t)x29 * x71) + (((uint64_t)x31 * x69) + ((0x2 * ((uint64_t)x33 * x67)) + ((0x2 * ((uint64_t)x35 * x65)) + (((uint64_t)x37 * x63) + (((uint64_t)x39 * x61) + ((0x2 * ((uint64_t)x41 * x59)) + ((0x2 * ((uint64_t)x43 * x57)) + (((uint64_t)x45 * x55) + ((uint64_t)x44 * x53)))))))))))))))))))));
  { uint64_t x108 = ((((uint64_t)x5 * x49) + ((uint64_t)x7 * x47)) + (0xbb * (((uint64_t)x9 * x86) + (((uint64_t)x11 * x87) + (((uint64_t)x13 * x85) + ((0x2 * ((uint64_t)x15 * x83)) + (((uint64_t)x17 * x81) + (((uint64_t)x19 * x79) + (((uint64_t)x21 * x77) + ((0x2 * ((uint64_t)x23 * x75)) + (((uint64_t)x25 * x73) + (((uint64_t)x27 * x71) + (((uint64_t)x29 * x69) + (((uint64_t)x31 * x67) + ((0x2 * ((uint64_t)x33 * x65)) + (((uint64_t)x35 * x63) + (((uint64_t)x37 * x61) + (((uint64_t)x39 * x59) + ((0x2 * ((uint64_t)x41 * x57)) + (((uint64_t)x43 * x55) + (((uint64_t)x45 * x53) + ((uint64_t)x44 * x51))))))))))))))))))))));
  { uint64_t x109 = (((uint64_t)x5 * x47) + (0xbb * ((0x2 * ((uint64_t)x7 * x86)) + ((0x2 * ((uint64_t)x9 * x87)) + ((0x2 * ((uint64_t)x11 * x85)) + ((0x2 * ((uint64_t)x13 * x83)) + ((0x2 * ((uint64_t)x15 * x81)) + ((0x2 * ((uint64_t)x17 * x79)) + ((0x2 * ((uint64_t)x19 * x77)) + ((0x2 * ((uint64_t)x21 * x75)) + ((0x2 * ((uint64_t)x23 * x73)) + ((0x2 * ((uint64_t)x25 * x71)) + ((0x2 * ((uint64_t)x27 * x69)) + ((0x2 * ((uint64_t)x29 * x67)) + ((0x2 * ((uint64_t)x31 * x65)) + ((0x2 * ((uint64_t)x33 * x63)) + ((0x2 * ((uint64_t)x35 * x61)) + ((0x2 * ((uint64_t)x37 * x59)) + ((0x2 * ((uint64_t)x39 * x57)) + ((0x2 * ((uint64_t)x41 * x55)) + ((0x2 * ((uint64_t)x43 * x53)) + ((0x2 * ((uint64_t)x45 * x51)) + (0x2 * ((uint64_t)x44 * x49))))))))))))))))))))))));
  { uint64_t x110 = (x109 >> 0x18);
  { uint32_t x111 = ((uint32_t)x109 & 0xffffff);
  { uint64_t x112 = (x110 + x108);
  { uint64_t x113 = (x112 >> 0x17);
  { uint32_t x114 = ((uint32_t)x112 & 0x7fffff);
  { uint64_t x115 = (x113 + x107);
  { uint64_t x116 = (x115 >> 0x17);
  { uint32_t x117 = ((uint32_t)x115 & 0x7fffff);
  { uint64_t x118 = (x116 + x106);
  { uint64_t x119 = (x118 >> 0x17);
  { uint32_t x120 = ((uint32_t)x118 & 0x7fffff);
  { uint64_t x121 = (x119 + x105);
  { uint64_t x122 = (x121 >> 0x18);
  { uint32_t x123 = ((uint32_t)x121 & 0xffffff);
  { uint64_t x124 = (x122 + x104);
  { uint64_t x125 = (x124 >> 0x17);
  { uint32_t x126 = ((uint32_t)x124 & 0x7fffff);
  { uint64_t x127 = (x125 + x103);
  { uint64_t x128 = (x127 >> 0x17);
  { uint32_t x129 = ((uint32_t)x127 & 0x7fffff);
  { uint64_t x130 = (x128 + x102);
  { uint64_t x131 = (x130 >> 0x17);
  { uint32_t x132 = ((uint32_t)x130 & 0x7fffff);
  { uint64_t x133 = (x131 + x101);
  { uint64_t x134 = (x133 >> 0x18);
  { uint32_t x135 = ((uint32_t)x133 & 0xffffff);
  { uint64_t x136 = (x134 + x100);
  { uint64_t x137 = (x136 >> 0x17);
  { uint32_t x138 = ((uint32_t)x136 & 0x7fffff);
  { uint64_t x139 = (x137 + x99);
  { uint64_t x140 = (x139 >> 0x17);
  { uint32_t x141 = ((uint32_t)x139 & 0x7fffff);
  { uint64_t x142 = (x140 + x98);
  { uint64_t x143 = (x142 >> 0x17);
  { uint32_t x144 = ((uint32_t)x142 & 0x7fffff);
  { uint64_t x145 = (x143 + x97);
  { uint64_t x146 = (x145 >> 0x17);
  { uint32_t x147 = ((uint32_t)x145 & 0x7fffff);
  { uint64_t x148 = (x146 + x96);
  { uint64_t x149 = (x148 >> 0x18);
  { uint32_t x150 = ((uint32_t)x148 & 0xffffff);
  { uint64_t x151 = (x149 + x95);
  { uint64_t x152 = (x151 >> 0x17);
  { uint32_t x153 = ((uint32_t)x151 & 0x7fffff);
  { uint64_t x154 = (x152 + x94);
  { uint64_t x155 = (x154 >> 0x17);
  { uint32_t x156 = ((uint32_t)x154 & 0x7fffff);
  { uint64_t x157 = (x155 + x93);
  { uint64_t x158 = (x157 >> 0x17);
  { uint32_t x159 = ((uint32_t)x157 & 0x7fffff);
  { uint64_t x160 = (x158 + x92);
  { uint64_t x161 = (x160 >> 0x18);
  { uint32_t x162 = ((uint32_t)x160 & 0xffffff);
  { uint64_t x163 = (x161 + x91);
  { uint64_t x164 = (x163 >> 0x17);
  { uint32_t x165 = ((uint32_t)x163 & 0x7fffff);
  { uint64_t x166 = (x164 + x90);
  { uint64_t x167 = (x166 >> 0x17);
  { uint32_t x168 = ((uint32_t)x166 & 0x7fffff);
  { uint64_t x169 = (x167 + x89);
  { uint64_t x170 = (x169 >> 0x17);
  { uint32_t x171 = ((uint32_t)x169 & 0x7fffff);
  { uint64_t x172 = (x170 + x88);
  { uint64_t x173 = (x172 >> 0x17);
  { uint32_t x174 = ((uint32_t)x172 & 0x7fffff);
  { uint64_t x175 = (x111 + (0xbb * x173));
  { uint32_t x176 = (uint32_t) (x175 >> 0x18);
  { uint32_t x177 = ((uint32_t)x175 & 0xffffff);
  { uint32_t x178 = (x176 + x114);
  { uint32_t x179 = (x178 >> 0x17);
  { uint32_t x180 = (x178 & 0x7fffff);
  out[0] = x177;
  out[1] = x180;
  out[2] = (x179 + x117);
  out[3] = x120;
  out[4] = x123;
  out[5] = x126;
  out[6] = x129;
  out[7] = x132;
  out[8] = x135;
  out[9] = x138;
  out[10] = x141;
  out[11] = x144;
  out[12] = x147;
  out[13] = x150;
  out[14] = x153;
  out[15] = x156;
  out[16] = x159;
  out[17] = x162;
  out[18] = x165;
  out[19] = x168;
  out[20] = x171;
  out[21] = x174;
  }}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}
}