text_formalization/nonlinear/formal_tests/ineq_ids.hl

   1 (* id, C verification time in ms *)\r
   2 let ineq_ids =\r
   3 [\r
   4 "GRKIBMP split(1/2)",0;\r
   5 "GRKIBMP split(0/2)",0;\r
   6 "HJKDESR1a",0;\r
   7 "ZTGIJCF0",0;\r
   8 "TSKAJXY-delta_x4",0;\r
   9 "OXLZLEZ 6346351218 0 0",0;\r
  10 "OXLZLEZ 6346351218 0 1",0;\r
  11 "OXLZLEZ 6346351218 0 2",0;\r
  12 "OXLZLEZ 6346351218 0 3",0;\r
  13 "OXLZLEZ 6346351218 0 4",0;\r
  14 "OXLZLEZ 6346351218 0 5",0;\r
  15 "OXLZLEZ 6346351218 0 6",0;\r
  16 "OXLZLEZ 6346351218 0 7",0;\r
  17 "OXLZLEZ 6346351218 0 8",0;\r
  18 "OXLZLEZ 6346351218 0 9",0;\r
  19 "OXLZLEZ 6346351218 0 10",0;\r
  20 "OXLZLEZ 6346351218 0 11",0;\r
  21 "OXLZLEZ 6346351218 0 12",0;\r
  22 "OXLZLEZ 6346351218 0 13",0;\r
  23 "OXLZLEZ 6346351218 0 14",0;\r
  24 "OXLZLEZ 6346351218 0 15",0;\r
  25 "OXLZLEZ 6346351218 0 16",0;\r
  26 "OXLZLEZ 6346351218 0 17",0;\r
  27 "OXLZLEZ 6346351218 0 18",0;\r
  28 "OXLZLEZ 6346351218 0 19",0;\r
  29 "OXLZLEZ 6346351218 0 20",0;\r
  30 "OXLZLEZ 6346351218 0 21",0;\r
  31 "OXLZLEZ 6346351218 0 22",0;\r
  32 "OXLZLEZ 6346351218 0 23",0;\r
  33 "OXLZLEZ 6346351218 0 24",0;\r
  34 "OXLZLEZ 6346351218 0 25",0;\r
  35 "OXLZLEZ 6346351218 0 26",0;\r
  36 "OXLZLEZ 6346351218 0 27",0;\r
  37 "OXLZLEZ 6346351218 0 28",0;\r
  38 "OXLZLEZ 6346351218 0 29",0;\r
  39 "OXLZLEZ 6346351218 0 30",0;\r
  40 "OXLZLEZ 6346351218 0 31",0;\r
  41 "OXLZLEZ 6346351218 0 32",0;\r
  42 "OXLZLEZ 6346351218 0 33",0;\r
  43 "OXLZLEZ 6346351218 0 34",0;\r
  44 "OXLZLEZ 6346351218 0 35",0;\r
  45 "OXLZLEZ 6346351218 0 36",0;\r
  46 "OXLZLEZ 6346351218 0 37",0;\r
  47 "OXLZLEZ 6346351218 0 38",0;\r
  48 "OXLZLEZ 6346351218 0 39",0;\r
  49 "OXLZLEZ 6346351218 0 40",0;\r
  50 "OXLZLEZ 6346351218 0 41",0;\r
  51 "OXLZLEZ 6346351218 0 42",0;\r
  52 "OXLZLEZ 6346351218 0 43",0;\r
  53 "OXLZLEZ 6346351218 0 44",0;\r
  54 "OXLZLEZ 6346351218 0 45",0;\r
  55 "1965189142 34",0;\r
  56 "6096597438 a",0;\r
  57 "4717061266",0;\r
  58 "1117202051",0;\r
  59 "4559601669",0;\r
  60 "4559601669b",0;\r
  61 "2485876245a",0;\r
  62 "JNTEFVP 1",1;\r
  63 "TSKAJXY-eulerA",1;\r
  64 "5512912661",2;\r
  65 "6843920790",2;\r
  66 "BIXPCGW b",2;\r
  67 "4828966562",3;\r
  68 "TSKAJXY-RIBCYXU sharp",3;\r
  69 "8055810915",3;\r
  70 "6459846571",3;\r
  71 "ZTGIJCF4 1 1 1 1 1821661595 split(16/32)",4;\r
  72 "QITNPEA4 1 1 1 1 3803737830 split(16/32)",4;\r
  73 "ZTGIJCF4 1 1 1 1 1821661595 split(0/32)",5;\r
  74 "QITNPEA4 1 1 1 1 3803737830 split(0/32)",5;\r
  75 "SDCCMGA a",5;\r
  76 "2485876245b",5;\r
  77 "SDCCMGA b",6;\r
  78 "QITNPEA4 1 1 1 1 3803737830 split(1/32)",8;\r
  79 "ZTGIJCF4 1 1 1 1 1821661595 split(8/32)",8;\r
  80 "ZTGIJCF4 1 1 1 1 1821661595 split(4/32)",8;\r
  81 "ZTGIJCF4 1 1 1 1 1821661595 split(1/32)",9;\r
  82 "TSKAJXY-GXSABWC DIV",9;\r
  83 "QITNPEA 4003532128 a",10;\r
  84 "ZTGIJCF4 1 1 1 1 1821661595 split(24/32)",10;\r
  85 "ZTGIJCF4 1 1 1 1 1821661595 split(17/32)",10;\r
  86 "QITNPEA4 1 1 1 1 3803737830 split(8/32)",10;\r
  87 "QITNPEA4 1 1 1 1 3803737830 split(4/32)",10;\r
  88 "8520556953",11;\r
  89 "ZTGIJCF4 1 1 1 1 1821661595 split(18/32)",11;\r
  90 "6096597438 b",11;\r
  91 "7459553847",12;\r
  92 "ZTGIJCF4 1 1 1 1 1821661595 split(20/32)",12;\r
  93 "QITNPEA4 1 1 1 1 3803737830 split(20/32)",12;\r
  94 "7459553847",13;\r
  95 "4528012043",13;\r
  96 "ZTGIJCF4 1 1 1 1 1821661595 split(2/32)",13;\r
  97 "QITNPEA4 1 1 1 1 3803737830 split(17/32)",13;\r
  98 "4528012043",14;\r
  99 "QITNPEA4 1 1 1 1 3803737830 split(24/32)",14;\r
 100 "QITNPEA4 1 1 1 1 3803737830 split(18/32)",14;\r
 101 "QITNPEA4 1 1 1 1 3803737830 split(2/32)",14;\r
 102 "BIXPCGW 7274157868 split(63/64)",20;\r
 103 "ZTGIJCF4 1 1 1 1 1821661595 split(12/32)",20;\r
 104 "9816718044",21;\r
 105 "ZTGIJCF4 1 1 0 1 1821661595 split(0/16)",21;\r
 106 "ZTGIJCF4 1 1 1 1 1821661595 split(5/32)",21;\r
 107 "9816718044",22;\r
 108 "BIXPCGW 7274157868 split(31/64)",22;\r
 109 "QITNPEA4 1 1 1 1 3803737830 split(12/32)",22;\r
 110 "QITNPEA4 1 1 1 1 3803737830 split(5/32)",22;\r
 111 "ZTGIJCF4 1 1 1 1 1821661595 split(28/32)",23;\r
 112 "ZTGIJCF4 1 1 1 1 1821661595 split(6/32)",23;\r
 113 "QITNPEA4 1 1 1 1 3803737830 split(10/32)",24;\r
 114 "QITNPEA4 1 1 1 1 3803737830 split(3/32)",24;\r
 115 "4143829594",25;\r
 116 "ZTGIJCF4 1 1 1 1 1821661595 split(10/32)",25;\r
 117 "ZTGIJCF4 1 1 1 1 1821661595 split(3/32)",25;\r
 118 "QITNPEA 3725403817",25;\r
 119 "4143829594",26;\r
 120 "ZTGIJCF4 0 1 1 1 1821661595 split(0/16)",26;\r
 121 "ZTGIJCF4 1 1 0 1 1821661595 split(8/16)",26;\r
 122 "ZTGIJCF4 1 1 1 0 1821661595 split(0/16)",26;\r
 123 "7697147739 delta issue",27;\r
 124 "ZTGIJCF4 1 1 1 1 1821661595 split(22/32)",27;\r
 125 "QITNPEA4 1 1 1 1 3803737830 split(6/32)",27;\r
 126 "2200527225",28;\r
 127 "3106201101",28;\r
 128 "ZTGIJCF4 1 1 1 1 1821661595 split(21/32)",28;\r
 129 "3106201101",29;\r
 130 "2200527225",29;\r
 131 "ZTGIJCF4 1 1 1 1 1821661595 split(26/32)",29;\r
 132 "ZTGIJCF4 1 1 1 1 1821661595 split(19/32)",29;\r
 133 "QITNPEA4 1 1 0 1 3803737830 split(0/16)",29;\r
 134 "QITNPEA4 1 1 1 1 3803737830 split(22/32)",29;\r
 135 "QITNPEA4 1 1 1 1 3803737830 split(21/32)",31;\r
 136 "QITNPEA4 1 1 1 1 3803737830 split(26/32)",32;\r
 137 "QITNPEA4 1 1 1 1 3803737830 split(19/32)",32;\r
 138 "QITNPEA4 1 1 1 1 3803737830 split(28/32)",33;\r
 139 "ZTGIJCF4 0 1 1 1 1821661595 split(8/16)",34;\r
 140 "ZTGIJCF4 1 1 1 0 1821661595 split(8/16)",35;\r
 141 "QITNPEA4 0 1 1 1 3803737830 split(0/16)",35;\r
 142 "QITNPEA4 1 0 1 1 3803737830 split(0/16)",35;\r
 143 "QITNPEA4 1 1 1 0 3803737830 split(0/16)",36;\r
 144 "9977174768",37;\r
 145 "QITNPEA4 0 1 1 1 3803737830 split(8/16)",37;\r
 146 "QITNPEA4 1 1 0 1 3803737830 split(8/16)",37;\r
 147 "QITNPEA4 1 1 1 1 3803737830 split(9/32)",37;\r
 148 "2559885109",38;\r
 149 "9977174768",38;\r
 150 "ZTGIJCF4 1 1 1 1 1821661595 split(9/32)",38;\r
 151 "ZTGIJCF4 1 0 1 1 1821661595 split(0/16)",39;\r
 152 "8673686234 a",40;\r
 153 "BIXPCGW 7274157868 split(29/64)",44;\r
 154 "BIXPCGW 7274157868 split(15/64)",45;\r
 155 "ZTGIJCF4 1 1 1 1 1821661595 split(25/32)",45;\r
 156 "QITNPEA4 1 1 1 0 3803737830 split(8/16)",46;\r
 157 "2900061606",47;\r
 158 "QITNPEA4 1 0 1 1 3803737830 split(8/16)",47;\r
 159 "QITNPEA4 1 1 1 1 3803737830 split(25/32)",47;\r
 160 "BIXPCGW 7274157868 split(23/64)",49;\r
 161 "7097350062a",50;\r
 162 "ZTGIJCF4 1 0 1 1 1821661595 split(8/16)",50;\r
 163 "7097350062a",51;\r
 164 "BIXPCGW 7274157868 split(27/64)",52;\r
 165 "BIXPCGW 7274157868 split(30/64)",53;\r
 166 "1080462150",55;\r
 167 "ZTGIJCF4 1 1 1 1 1821661595 split(14/32)",57;\r
 168 "QITNPEA4 1 1 1 1 3803737830 split(14/32)",58;\r
 169 "ZTGIJCF4 1 1 1 1 1821661595 split(7/32)",58;\r
 170 "ZTGIJCF4 1 1 0 1 1821661595 split(2/16)",60;\r
 171 "2570626711",60;\r
 172 "QITNPEA4 1 1 1 1 3803737830 split(7/32)",61;\r
 173 "BIXPCGW 7274157868 split(59/64)",64;\r
 174 "ZTGIJCF4 1 1 1 1 1821661595 split(23/32)",64;\r
 175 "BIXPCGW 7274157868 split(47/64)",66;\r
 176 "ZTGIJCF4 0 1 1 1 1821661595 split(2/16)",68;\r
 177 "7067938795",70;\r
 178 "ZTGIJCF4 0 1 1 1 1821661595 split(1/16)",71;\r
 179 "QZECFIC wt2 split(0/4)",73;\r
 180 "ZTGIJCF4 1 1 1 0 1821661595 split(1/16)",74;\r
 181 "ZTGIJCF4 1 1 1 1 1821661595 split(13/32)",74;\r
 182 "OMKYNLT 0 3",74;\r
 183 "QITNPEA4 1 1 1 1 3803737830 split(23/32)",75;\r
 184 "ZTGIJCF4 1 1 0 1 1821661595 split(1/16)",76;\r
 185 "ZTGIJCF4 1 1 0 1 1821661595 split(4/16)",77;\r
 186 "BIXPCGW 7274157868 split(14/64)",78;\r
 187 "GLFVCVK4 2477216213 split(31/64)",79;\r
 188 "BIXPCGW 7274157868 split(21/64)",79;\r
 189 "ZTGIJCF4 0 1 1 1 1821661595 split(4/16)",79;\r
 190 "ZTGIJCF4 1 1 1 0 1821661595 split(2/16)",79;\r
 191 "ZTGIJCF4 1 1 1 0 1821661595 split(4/16)",80;\r
 192 "QITNPEA4 1 1 0 1 3803737830 split(4/16)",81;\r
 193 "QITNPEA4 1 1 0 1 3803737830 split(2/16)",82;\r
 194 "QITNPEA4 1 1 1 1 3803737830 split(13/32)",82;\r
 195 "BIXPCGW 7274157868 split(62/64)",83;\r
 196 "QITNPEA4 1 1 0 1 3803737830 split(1/16)",83;\r
 197 "ZTGIJCF4 1 1 1 1 1821661595 split(30/32)",84;\r
 198 "1965189142 a",85;\r
 199 "QITNPEA4 1 1 1 1 3803737830 split(11/32)",86;\r
 200 "7645170609",86;\r
 201 "ZTGIJCF4 0 1 1 1 1821661595 split(9/16)",86;\r
 202 "QITNPEA4 1 1 1 0 3803737830 split(1/16)",86;\r
 203 "ZTGIJCF4 0 1 1 1 1821661595 split(10/16)",87;\r
 204 "ZTGIJCF4 1 1 1 1 1821661595 split(11/32)",87;\r
 205 "QITNPEA4 1 0 1 1 3803737830 split(2/16)",87;\r
 206 "OMKYNLT 3336871894",87;\r
 207 "QITNPEA4 0 1 1 1 3803737830 split(2/16)",88;\r
 208 "QITNPEA4 1 1 1 1 3803737830 split(30/32)",88;\r
 209 "7645170609",90;\r
 210 "OMKYNLT 2 1",90;\r
 211 "BIXPCGW 7274157868 split(55/64)",90;\r
 212 "QITNPEA4 1 1 1 0 3803737830 split(4/16)",90;\r
 213 "QITNPEA4 0 1 1 1 3803737830 split(1/16)",91;\r
 214 "ZTGIJCF4 1 1 1 1 1821661595 split(27/32)",92;\r
 215 "ZTGIJCF4 1 1 1 1 1821661595 split(29/32)",93;\r
 216 "ZTGIJCF4 1 1 0 1 1821661595 split(12/16)",94;\r
 217 "ZTGIJCF4 1 1 0 1 1821661595 split(9/16)",94;\r
 218 "ZTGIJCF4 1 0 1 1 1821661595 split(2/16)",95;\r
 219 "ZTGIJCF4 1 1 1 0 1821661595 split(9/16)",96;\r
 220 "ZTGIJCF4 1 1 1 0 1821661595 split(12/16)",98;\r
 221 "QITNPEA4 1 1 1 1 3803737830 split(27/32)",98;\r
 222 "QITNPEA4 1 1 1 0 3803737830 split(2/16)",99;\r
 223 "QITNPEA4 0 1 1 1 3803737830 split(4/16)",100;\r
 224 "GLFVCVK4 2477216213 split(63/64)",101;\r
 225 "QITNPEA4 1 1 1 1 3803737830 split(29/32)",103;\r
 226 "QITNPEA4 1 0 1 1 3803737830 split(1/16)",104;\r
 227 "BIXPCGW 7274157868 split(7/64)",105;\r
 228 "TSKAJXY-IYOUOBF sharp v2",108;\r
 229 "QITNPEA4 1 1 0 1 3803737830 split(12/16)",109;\r
 230 "QITNPEA4 1 1 0 1 3803737830 split(9/16)",109;\r
 231 "BIXPCGW 7274157868 split(61/64)",110;\r
 232 "QITNPEA4 0 1 1 1 3803737830 split(9/16)",110;\r
 233 "BIXPCGW 7274157868 split(28/64)",111;\r
 234 "QITNPEA4 0 1 1 1 3803737830 split(10/16)",112;\r
 235 "QITNPEA4 1 0 1 1 3803737830 split(10/16)",112;\r
 236 "QITNPEA4 1 0 1 1 3803737830 split(4/16)",115;\r
 237 "QITNPEA4 1 1 1 0 3803737830 split(12/16)",120;\r
 238 "ZTGIJCF4 1 1 0 1 1821661595 split(10/16)",122;\r
 239 "QITNPEA4 1 1 1 0 3803737830 split(9/16)",122;\r
 240 "5026777310",125;\r
 241 "ZTGIJCF4 1 0 1 1 1821661595 split(10/16)",126;\r
 242 "9459075374",126;\r
 243 "ZTGIJCF4 1 0 1 1 1821661595 split(1/16)",127;\r
 244 "9459075374",128;\r
 245 "ZTGIJCF4 1 0 1 1 1821661595 split(4/16)",128;\r
 246 "QITNPEA4 1 0 1 1 3803737830 split(9/16)",136;\r
 247 "ZTGIJCF4 1 0 1 1 1821661595 split(9/16)",147;\r
 248 "ZTGIJCF4 0 1 1 1 1821661595 split(12/16)",147;\r
 249 "QITNPEA4 1 0 1 1 3803737830 split(12/16)",150;\r
 250 "ZTGIJCF4 1 1 1 0 1821661595 split(10/16)",155;\r
 251 "BIXPCGW 7274157868 split(13/64)",156;\r
 252 "BIXPCGW 7274157868 split(46/64)",158;\r
 253 "BIXPCGW 7274157868 split(43/64)",160;\r
 254 "QITNPEA4 1 1 0 1 3803737830 split(10/16)",161;\r
 255 "OMKYNLT 1 2",161;\r
 256 "BIXPCGW 7274157868 split(53/64)",162;\r
 257 "ZTGIJCF4 1 0 1 1 1821661595 split(12/16)",162;\r
 258 "BIXPCGW 7274157868 split(22/64)",163;\r
 259 "BIXPCGW 7274157868 split(11/64)",170;\r
 260 "BIXPCGW 7274157868 split(58/64)",173;\r
 261 "ZTGIJCF4 1 1 1 1 1821661595 split(15/32)",179;\r
 262 "BIXPCGW 7274157868 split(19/64)",181;\r
 263 "4680581274 delta issue",184;\r
 264 "BIXPCGW 7274157868 split(26/64)",184;\r
 265 "7881254908",186;\r
 266 "BIXPCGW 7274157868 split(51/64)",188;\r
 267 "QITNPEA4 1 1 1 1 3803737830 split(15/32)",188;\r
 268 "QITNPEA4 0 1 1 1 3803737830 split(12/16)",198;\r
 269 "ZTGIJCF4 1 1 0 1 1821661595 split(3/16)",200;\r
 270 "QITNPEA4 1 1 1 0 3803737830 split(10/16)",201;\r
 271 "ZTGIJCF4 1 1 1 0 1821661595 split(6/16)",206;\r
 272 "ZTGIJCF4 1 1 1 1 1821661595 split(31/32)",214;\r
 273 "7881254908",217;\r
 274 "ZTGIJCF4 0 1 1 1 1821661595 split(6/16)",222;\r
 275 "ZTGIJCF4 0 1 1 1 1821661595 split(5/16)",223;\r
 276 "ZTGIJCF4 0 1 1 0 1821661595 split(0/8)",225;\r
 277 "BIXPCGW 7274157868 split(39/64)",227;\r
 278 "ZTGIJCF4 1 1 0 1 1821661595 split(6/16)",228;\r
 279 "BIXPCGW 7274157868 split(45/64)",230;\r
 280 "ZTGIJCF4 0 1 0 1 1821661595 split(0/8)",231;\r
 281 "QITNPEA4 1 1 0 1 3803737830 split(3/16)",233;\r
 282 "GLFVCVK4 2477216213 split(15/64)",235;\r
 283 "ZTGIJCF4 0 1 1 1 1821661595 split(3/16)",235;\r
 284 "QITNPEA4 1 1 0 1 3803737830 split(6/16)",236;\r
 285 "BIXPCGW 7274157868 split(54/64)",237;\r
 286 "GLFVCVK4 2477216213 split(23/64)",238;\r
 287 "ZTGIJCF4 1 1 0 0 1821661595 split(0/8)",244;\r
 288 "ZTGIJCF4 1 1 1 0 1821661595 split(5/16)",244;\r
 289 "ZTGIJCF4 1 1 1 0 1821661595 split(3/16)",244;\r
 290 "GLFVCVK4 2477216213 split(30/64)",245;\r
 291 "QITNPEA4 1 1 1 1 3803737830 split(31/32)",247;\r
 292 "BIXPCGW 7274157868 split(25/64)",248;\r
 293 "BIXPCGW 7274157868 split(57/64)",250;\r
 294 "BIXPCGW 7274157868 split(3/64)",253;\r
 295 "QITNPEA4 1 1 1 0 3803737830 split(5/16)",254;\r
 296 "QITNPEA4 0 1 1 1 3803737830 split(3/16)",256;\r
 297 "QITNPEA4 1 1 1 0 3803737830 split(3/16)",257;\r
 298 "BIXPCGW 7274157868 split(6/64)",260;\r
 299 "ZTGIJCF4 0 1 1 1 1821661595 split(11/16)",267;\r
 300 "QITNPEA4 1 1 1 0 3803737830 split(6/16)",267;\r
 301 "QITNPEA4 1 0 1 1 3803737830 split(3/16)",272;\r
 302 "QITNPEA4 0 0 1 1 3803737830 split(0/8)",273;\r
 303 "BIXPCGW 7274157868 split(24/64)",275;\r
 304 "GLFVCVK4 2477216213 split(29/64)",276;\r
 305 "BIXPCGW 7274157868 split(60/64)",280;\r
 306 "ZTGIJCF4 1 1 0 1 1821661595 split(11/16)",280;\r
 307 "ZTGIJCF4 0 0 1 1 1821661595 split(0/8)",280;\r
 308 "GLFVCVK4 2477216213 split(27/64)",285;\r
 309 "QZECFIC wt2 split(2/4)",286;\r
 310 "ZTGIJCF4 1 1 0 1 1821661595 split(14/16)",290;\r
 311 "BIXPCGW 7274157868 split(10/64)",293;\r
 312 "BIXPCGW 7274157868 split(12/64)",294;\r
 313 "BIXPCGW 7274157868 split(5/64)",295;\r
 314 "QITNPEA4 0 1 1 1 3803737830 split(6/16)",296;\r
 315 "BIXPCGW 7274157868 split(20/64)",300;\r
 316 "QITNPEA4 0 1 1 1 3803737830 split(5/16)",303;\r
 317 "BIXPCGW 7274157868 split(17/64)",307;\r
 318 "ZTGIJCF4 1 1 1 0 1821661595 split(13/16)",318;\r
 319 "ZTGIJCF4 1 0 1 1 1821661595 split(3/16)",318;\r
 320 "QITNPEA4 1 0 1 1 3803737830 split(6/16)",322;\r
 321 "QITNPEA4 0 1 1 0 3803737830 split(0/8)",324;\r
 322 "GLFVCVK4 2477216213 split(55/64)",326;\r
 323 "GLFVCVK4 2477216213 split(47/64)",330;\r
 324 "QITNPEA4 0 1 1 1 3803737830 split(11/16)",344;\r
 325 "9269152105",348;\r
 326 "ZTGIJCF4 1 0 1 1 1821661595 split(6/16)",357;\r
 327 "QITNPEA4 0 1 0 1 3803737830 split(0/8)",357;\r
 328 "QITNPEA4 1 1 0 0 3803737830 split(0/8)",362;\r
 329 "QITNPEA4 1 1 0 1 3803737830 split(14/16)",365;\r
 330 "QITNPEA4 1 0 1 1 3803737830 split(11/16)",367;\r
 331 "ZTGIJCF4 0 1 1 1 1821661595 split(13/16)",371;\r
 332 "QITNPEA4 1 1 0 1 3803737830 split(11/16)",373;\r
 333 "5490182221",375;\r
 334 "QITNPEA4 1 0 1 0 3803737830 split(0/8)",376;\r
 335 "GLFVCVK4 2477216213 y4crit split(0/8)",378;\r
 336 "GLFVCVK4 2477216213 split(59/64)",380;\r
 337 "9507202313",382;\r
 338 "QITNPEA4 1 0 0 1 3803737830 split(0/8)",383;\r
 339 "QITNPEA4 1 1 1 0 3803737830 split(13/16)",388;\r
 340 "QITNPEA1 1 1 9063653052 split(0/8)",389;\r
 341 "ZTGIJCF4 0 1 1 1 1821661595 split(14/16)",395;\r
 342 "ZTGIJCF4 0 0 1 1 1821661595 split(4/8)",397;\r
 343 "GLFVCVK4 2477216213 split(62/64)",398;\r
 344 "BIXPCGW 7274157868 split(35/64)",398;\r
 345 "ZTGIJCF4 1 0 1 1 1821661595 split(11/16)",400;\r
 346 "3872614111",404;\r
 347 "ZTGIJCF4 1 1 1 0 1821661595 split(14/16)",407;\r
 348 "ZTGIJCF4 1 1 1 0 1821661595 split(11/16)",412;\r
 349 "QITNPEA4 0 0 1 1 3803737830 split(4/8)",418;\r
 350 "9925287433",418;\r
 351 "ZTGIJCF4 1 0 1 0 1821661595 split(0/8)",422;\r
 352 "4841020453",424;\r
 353 "BIXPCGW 7274157868 split(56/64)",433;\r
 354 "GLFVCVK4 2477216213 split(61/64)",436;\r
 355 "ZTGIJCF4 0 1 0 1 1821661595 split(4/8)",454;\r
 356 "ZTGIJCF4 0 1 1 0 1821661595 split(4/8)",454;\r
 357 "QITNPEA4 1 0 1 1 3803737830 split(14/16)",455;\r
 358 "2390583444",456;\r
 359 "ZTGIJCF4 1 1 0 0 1821661595 split(4/8)",463;\r
 360 "ZTGIJCF4 1 1 0 1 1821661595 split(5/16)",470;\r
 361 "6619134733",474;\r
 362 "7043724150 a reduced",481;\r
 363 "BIXPCGW 7274157868 split(1/64)",489;\r
 364 "QITNPEA4 1 1 0 1 3803737830 split(5/16)",493;\r
 365 "ZTGIJCF4 1 0 1 1 1821661595 split(14/16)",496;\r
 366 "BIXPCGW 7274157868 split(2/64)",498;\r
 367 "QITNPEA1 2 1 9063653052 split(0/4)",503;\r
 368 "BIXPCGW 7274157868 split(42/64)",503;\r
 369 "2739661360",507;\r
 370 "ZTGIJCF4 1 0 0 1 1821661595 split(0/8)",507;\r
 371 "2739661360",509;\r
 372 "7720405539",520;\r
 373 "GLFVCVK4 2477216213 y4crit split(2/8)",527;\r
 374 "3139693500",528;\r
 375 "BIXPCGW 7274157868 split(49/64)",529;\r
 376 "QITNPEA4 0 1 1 1 3803737830 split(13/16)",529;\r
 377 "QITNPEA4 1 1 1 0 3803737830 split(11/16)",529;\r
 378 "QITNPEA1 1 1 9063653052 split(2/8)",529;\r
 379 "BIXPCGW 7274157868 split(37/64)",530;\r
 380 "QITNPEA4 0 1 1 1 3803737830 split(14/16)",532;\r
 381 "BIXPCGW 7274157868 split(8/64)",533;\r
 382 "QITNPEA4 1 0 1 1 3803737830 split(5/16)",533;\r
 383 "QITNPEA4 1 1 1 0 3803737830 split(14/16)",536;\r
 384 "BIXPCGW 7274157868 split(16/64)",537;\r
 385 "QITNPEA4 1 0 0 1 3803737830 split(4/8)",542;\r
 386 "5735387903",547;\r
 387 "BIXPCGW 7274157868 split(38/64)",548;\r
 388 "ZTGIJCF4 1 1 0 1 1821661595 split(13/16)",555;\r
 389 "QZECFIC wt2 split(1/4)",569;\r
 390 "2535350075",574;\r
 391 "ZTGIJCF4 1 0 1 0 1821661595 split(4/8)",577;\r
 392 "4922521904",578;\r
 393 "QITNPEA4 1 1 0 1 3803737830 split(13/16)",588;\r
 394 "QITNPEA4 1 0 1 0 3803737830 split(4/8)",590;\r
 395 "BIXPCGW 7274157868 split(4/64)",591;\r
 396 "ZTGIJCF4 1 0 0 1 1821661595 split(4/8)",593;\r
 397 "2535350075",594;\r
 398 "4922521904",600;\r
 399 "ZTGIJCF4 1 1 1 0 1821661595 split(7/16)",621;\r
 400 "181212899 4",622;\r
 401 "181212899 5",628;\r
 402 "ZTGIJCF4 1 0 1 1 1821661595 split(5/16)",638;\r
 403 "1550635295",638;\r
 404 "MKFKQWU",670;\r
 405 "ZTGIJCF4 0 1 1 1 1821661595 split(7/16)",674;\r
 406 "ZTGIJCF4 0 1 0 1 1821661595 split(1/8)",680;\r
 407 "181212899 3",685;\r
 408 "ZTGIJCF4 0 1 1 0 1821661595 split(1/8)",690;\r
 409 "ZTGIJCF4 1 1 0 0 1821661595 split(2/8)",690;\r
 410 "9563139965 e",694;\r
 411 "181212899 2",697;\r
 412 "6987934000",705;\r
 413 "2923748598",708;\r
 414 "QITNPEA4 0 1 1 0 3803737830 split(4/8)",714;\r
 415 "QITNPEA4 0 1 0 1 3803737830 split(4/8)",718;\r
 416 "4306175952",724;\r
 417 "BIXPCGW 7274157868 split(44/64)",727;\r
 418 "BIXPCGW 7274157868 split(52/64)",728;\r
 419 "7316455966",730;\r
 420 "BIXPCGW 7080972881 a",734;\r
 421 "BIXPCGW 7274157868 split(18/64)",737;\r
 422 "QITNPEA4 1 1 0 0 3803737830 split(4/8)",737;\r
 423 "BIXPCGW 7274157868 split(9/64)",737;\r
 424 "QZECFIC wt2 split(3/4)",740;\r
 425 "QITNPEA4 1 1 1 0 3803737830 split(7/16)",741;\r
 426 "GLFVCVK4 2477216213 y4crit split(1/8)",773;\r
 427 "6410081357",781;\r
 428 "QITNPEA1 1 1 9063653052 split(1/8)",785;\r
 429 "GLFVCVK4 2477216213 y4crit split(4/8)",805;\r
 430 "QITNPEA1 1 1 9063653052 split(4/8)",816;\r
 431 "BIXPCGW 7274157868 split(50/64)",822;\r
 432 "QITNPEA4 0 0 1 1 3803737830 split(1/8)",827;\r
 433 "QITNPEA4 1 0 1 1 3803737830 split(13/16)",829;\r
 434 "QITNPEA4 0 0 1 1 3803737830 split(2/8)",838;\r
 435 "GLFVCVK4 2477216213 split(21/64)",840;\r
 436 "BIXPCGW 7274157868 split(40/64)",843;\r
 437 "BIXPCGW 7274157868 split(33/64)",844;\r
 438 "BIXPCGW 7274157868 split(41/64)",845;\r
 439 "ZTGIJCF4 0 0 1 1 1821661595 split(1/8)",881;\r
 440 "GLFVCVK4 2477216213 split(14/64)",885;\r
 441 "ZTGIJCF4 1 0 1 1 1821661595 split(13/16)",888;\r
 442 "6836427086",890;\r
 443 "ZTGIJCF4 0 0 1 1 1821661595 split(2/8)",892;\r
 444 "QITNPEA4 0 1 1 1 3803737830 split(7/16)",892;\r
 445 "4222324842",898;\r
 446 "QITNPEA1 2 1 9063653052 split(1/4)",900;\r
 447 "OXLZLEZ 6346351218 1 30",901;\r
 448 "BIXPCGW 7274157868 split(34/64)",914;\r
 449 "BIXPCGW 7274157868 split(48/64)",923;\r
 450 "QITNPEA4 0 1 0 1 3803737830 split(1/8)",924;\r
 451 "QITNPEA4 0 1 1 0 3803737830 split(1/8)",924;\r
 452 "QITNPEA4 1 1 0 0 3803737830 split(2/8)",935;\r
 453 "1894886027",937;\r
 454 "QITNPEA1 2 1 9063653052 split(2/4)",945;\r
 455 "ZTGIJCF4 0 1 1 1 1821661595 split(15/16)",966;\r
 456 "BIXPCGW 7274157868 split(0/64)",999;\r
 457 "QITNPEA1 1 2 9063653052 split(0/4)",1048;\r
 458 "ZTGIJCF4 1 1 0 1 1821661595 split(7/16)",1069;\r
 459 "ZTGIJCF4 1 1 1 0 1821661595 split(15/16)",1073;\r
 460 "ZTGIJCF4 0 1 0 1 1821661595 split(2/8)",1079;\r
 461 "RQWUDDU split(0/2)",1083;\r
 462 "ZTGIJCF4 0 1 1 0 1821661595 split(2/8)",1086;\r
 463 "ZTGIJCF4 1 1 0 0 1821661595 split(1/8)",1095;\r
 464 "6284721194",1109;\r
 465 "GLFVCVK4 2477216213 split(7/64)",1130;\r
 466 "QITNPEA4 1 1 0 1 3803737830 split(7/16)",1130;\r
 467 "QITNPEA1 1 1 9063653052 split(3/8)",1152;\r
 468 "QITNPEA1 1 1 9063653052 split(6/8)",1153;\r
 469 "GLFVCVK4 2477216213 y4crit split(3/8)",1156;\r
 470 "GLFVCVK4 2477216213 y4crit split(6/8)",1159;\r
 471 "ZTGIJCF4 1 1 0 1 1821661595 split(15/16)",1169;\r
 472 "1284543870",1171;\r
 473 "GLFVCVK4 2477216213 split(28/64)",1174;\r
 474 "3020140039",1197;\r
 475 "ZTGIJCF4 0 1 0 1 1821661595 split(5/8)",1208;\r
 476 "QITNPEA4 1 0 1 0 3803737830 split(1/8)",1219;\r
 477 "ZTGIJCF4 0 1 1 0 1821661595 split(5/8)",1226;\r
 478 "ZTGIJCF4 1 1 0 0 1821661595 split(6/8)",1230;\r
 479 "QITNPEA4 1 0 1 0 3803737830 split(2/8)",1232;\r
 480 "1836408787",1235;\r
 481 "5835568093",1249;\r
 482 "GLFVCVK4 2477216213 split(13/64)",1253;\r
 483 "GLFVCVK4 2477216213 split(22/64)",1255;\r
 484 "QITNPEA1 2 2 9063653052 split(0/2)",1258;\r
 485 "7409690040",1267;\r
 486 "5756588587",1271;\r
 487 "ZTGIJCF4 0 0 1 1 1821661595 split(5/8)",1292;\r
 488 "QITNPEA4 0 0 1 1 3803737830 split(5/8)",1299;\r
 489 "ZTGIJCF4 1 0 1 0 1821661595 split(1/8)",1312;\r
 490 "ZTGIJCF4 1 0 1 0 1821661595 split(2/8)",1314;\r
 491 "9229542852",1326;\r
 492 "QITNPEA4 0 0 1 1 3803737830 split(6/8)",1328;\r
 493 "ZTGIJCF4 0 0 1 1 1821661595 split(6/8)",1334;\r
 494 "QITNPEA4 1 1 1 0 3803737830 split(15/16)",1355;\r
 495 "BIXPCGW 1738910218 a",1356;\r
 496 "QITNPEA4 0 1 1 1 3803737830 split(15/16)",1361;\r
 497 "QITNPEA4 1 1 0 1 3803737830 split(15/16)",1390;\r
 498 "OXLZLEZ 6346351218 1 29",1398;\r
 499 "BIXPCGW 7274157868 split(32/64)",1436;\r
 500 "GLFVCVK4 2477216213 split(19/64)",1500;\r
 501 "QITNPEA4 1 0 1 1 3803737830 split(7/16)",1521;\r
 502 "4002562507",1523;\r
 503 "4041673283",1578;\r
 504 "QITNPEA1 1 2 9063653052 split(1/4)",1625;\r
 505 "GLFVCVK4 2477216213 split(11/64)",1626;\r
 506 "GLFVCVK4 2477216213 split(25/64)",1674;\r
 507 "GLFVCVK4 2477216213 split(45/64)",1683;\r
 508 "QITNPEA4 0 1 0 1 3803737830 split(2/8)",1689;\r
 509 "QITNPEA4 0 1 1 0 3803737830 split(2/8)",1697;\r
 510 "GLFVCVK4 2477216213 split(26/64)",1703;\r
 511 "GLFVCVK4 2477216213 split(54/64)",1717;\r
 512 "GLFVCVK4 2477216213 split(53/64)",1719;\r
 513 "QITNPEA4 1 1 0 0 3803737830 split(1/8)",1733;\r
 514 "GLFVCVK4 2477216213 split(46/64)",1753;\r
 515 "QITNPEA1 1 1 9063653052 split(5/8)",1798;\r
 516 "GLFVCVK4 2477216213 y4crit split(5/8)",1801;\r
 517 "QITNPEA4 0 1 0 1 3803737830 split(5/8)",1801;\r
 518 "GLFVCVK4 2477216213 split(39/64)",1820;\r
 519 "ZTGIJCF4 1 0 1 1 1821661595 split(7/16)",1843;\r
 520 "QITNPEA4 0 1 1 0 3803737830 split(5/8)",1858;\r
 521 "BIXPCGW 6652007036 a",1860;\r
 522 "OXLZLEZ 6346351218 4 44",1863;\r
 523 "QITNPEA4 1 1 0 0 3803737830 split(6/8)",1864;\r
 524 "OXLZLEZ 6346351218 2 44",1865;\r
 525 "3566713650",1920;\r
 526 "GLFVCVK4 2477216213 split(60/64)",1947;\r
 527 "RQWUDDU split(1/2)",1972;\r
 528 "OXLZLEZ 6346351218 3 30",1985;\r
 529 "QITNPEA4 1 0 0 1 3803737830 split(2/8)",1991;\r
 530 "QITNPEA4 1 0 1 1 3803737830 split(15/16)",1994;\r
 531 "QITNPEA4 1 0 0 1 3803737830 split(1/8)",2033;\r
 532 "8657368829",2037;\r
 533 "QITNPEA1 2 1 9063653052 split(3/4)",2053;\r
 534 "5766053833",2064;\r
 535 "GLFVCVK4 2477216213 split(51/64)",2124;\r
 536 "GLFVCVK4 2477216213 split(57/64)",2178;\r
 537 "TSKAJXY-XLLIPLS",2179;\r
 538 "QITNPEA4 1 0 1 0 3803737830 split(5/8)",2183;\r
 539 "ZTGIJCF4 0 1 0 1 1821661595 split(6/8)",2194;\r
 540 "QITNPEA4 1 0 1 0 3803737830 split(6/8)",2213;\r
 541 "ZTGIJCF4 1 1 0 0 1821661595 split(5/8)",2226;\r
 542 "1248932983",2228;\r
 543 "ZTGIJCF4 0 1 1 0 1821661595 split(6/8)",2237;\r
 544 "5298513205",2244;\r
 545 "ZTGIJCF4 1 0 1 0 1821661595 split(5/8)",2246;\r
 546 "QITNPEA1 1 2 9063653052 split(2/4)",2266;\r
 547 "ZTGIJCF4 1 0 1 0 1821661595 split(6/8)",2272;\r
 548 "GLFVCVK4 2477216213 split(43/64)",2285;\r
 549 "ZTGIJCF4 1 0 1 1 1821661595 split(15/16)",2305;\r
 550 "9641946727",2311;\r
 551 "GLFVCVK4 2477216213 split(58/64)",2315;\r
 552 "OXLZLEZ 6346351218 4 31",2327;\r
 553 "OXLZLEZ 6346351218 2 31",2328;\r
 554 "QZECFIC wt1 split(0/2)",2417;\r
 555 "7743522046",2481;\r
 556 "ZTGIJCF4 1 0 0 1 1821661595 split(1/8)",2512;\r
 557 "ZTGIJCF4 1 0 0 1 1821661595 split(2/8)",2521;\r
 558 "9414951439",2550;\r
 559 "OXLZLEZ 6346351218 1 43",2578;\r
 560 "5943578801",2585;\r
 561 "OXLZLEZ 6346351218 3 29",2698;\r
 562 "9185711902",2707;\r
 563 "OXLZLEZ 6346351218 1 7",2721;\r
 564 "QITNPEA4 0 0 1 1 3803737830 split(3/8)",2722;\r
 565 "3980286827",2728;\r
 566 "3425739813",2740;\r
 567 "9291937879",2753;\r
 568 "QITNPEA4 1 0 0 1 3803737830 split(5/8)",2755;\r
 569 "QITNPEA1 1 1 9063653052 split(7/8)",2772;\r
 570 "GLFVCVK4 2477216213 y4crit split(7/8)",2782;\r
 571 "QITNPEA4 1 0 0 1 3803737830 split(6/8)",2801;\r
 572 "3137600529",2844;\r
 573 "ZTGIJCF4 0 0 1 1 1821661595 split(3/8)",2866;\r
 574 "OXLZLEZ 6346351218 1 40",2877;\r
 575 "7718591733",2903;\r
 576 "9922699028",2957;\r
 577 "ZTGIJCF4 0 1 0 1 1821661595 split(3/8)",3072;\r
 578 "QITNPEA1 2 2 9063653052 split(1/2)",3100;\r
 579 "ZTGIJCF4 0 1 1 0 1821661595 split(3/8)",3101;\r
 580 "OXLZLEZ 6346351218 2 21",3112;\r
 581 "9563139965 f",3149;\r
 582 "OXLZLEZ 6346351218 4 27",3154;\r
 583 "OXLZLEZ 6346351218 4 20",3155;\r
 584 "OXLZLEZ 6346351218 2 20",3161;\r
 585 "ZTGIJCF4 1 1 0 0 1821661595 split(3/8)",3175;\r
 586 "ZTGIJCF4 1 0 0 1 1821661595 split(5/8)",3207;\r
 587 "OXLZLEZ 6346351218 1 26",3210;\r
 588 "OXLZLEZ 6346351218 2 28",3264;\r
 589 "8199484193",3323;\r
 590 "GLFVCVK4 2477216213 split(3/64)",3358;\r
 591 "OXLZLEZ 6346351218 2 19",3372;\r
 592 "OXLZLEZ 6346351218 3 43",3377;\r
 593 "ZTGIJCF4 1 0 0 1 1821661595 split(6/8)",3395;\r
 594 "OXLZLEZ 6346351218 4 28",3456;\r
 595 "GLFVCVK4 2477216213 split(24/64)",3501;\r
 596 "OXLZLEZ 6346351218 4 41",3511;\r
 597 "QITNPEA4 0 1 0 1 3803737830 split(6/8)",3537;\r
 598 "QITNPEA4 0 1 1 0 3803737830 split(6/8)",3557;\r
 599 "QITNPEA4 1 1 0 0 3803737830 split(5/8)",3658;\r
 600 "OXLZLEZ 6346351218 2 42",3670;\r
 601 "OXLZLEZ 6346351218 3 17",3674;\r
 602 "OXLZLEZ 6346351218 1 18",3695;\r
 603 "OXLZLEZ 6346351218 1 17",3695;\r
 604 "OXLZLEZ 6346351218 1 16",3711;\r
 605 "GLFVCVK4 2477216213 split(17/64)",3740;\r
 606 "QITNPEA1 1 2 9063653052 split(3/4)",3759;\r
 607 "OXLZLEZ 6346351218 1 25",3766;\r
 608 "OXLZLEZ 6346351218 3 18",3818;\r
 609 "OXLZLEZ 6346351218 4 42",3819;\r
 610 "ZTGIJCF4 1 0 0 0 1821661595 split(0/4)",3942;\r
 611 "ZTGIJCF4 0 0 1 0 1821661595 split(0/4)",3949;\r
 612 "ZTGIJCF4 0 0 0 1 1821661595 split(0/4)",3975;\r
 613 "7819193535",4032;\r
 614 "2151506422",4075;\r
 615 "QITNPEA4 0 0 1 1 3803737830 split(7/8)",4131;\r
 616 "8384511215",4157;\r
 617 "ZTGIJCF4 0 0 1 1 1821661595 split(7/8)",4193;\r
 618 "QITNPEA4 1 0 0 0 3803737830 split(0/4)",4252;\r
 619 "QITNPEA4 0 0 0 1 3803737830 split(0/4)",4262;\r
 620 "QITNPEA4 0 0 1 0 3803737830 split(0/4)",4280;\r
 621 "7291663656",4421;\r
 622 "QITNPEA4 0 1 0 1 3803737830 split(3/8)",4572;\r
 623 "QITNPEA1 1 0 9063653052 split(0/4)",4581;\r
 624 "QITNPEA4 0 1 1 0 3803737830 split(3/8)",4597;\r
 625 "ZTGIJCF4 0 1 0 0 1821661595 split(0/4)",4633;\r
 626 "5760733457",4649;\r
 627 "5202826650 a",4691;\r
 628 "9995621667",4699;\r
 629 "QITNPEA4 1 0 1 0 3803737830 split(3/8)",4713;\r
 630 "QITNPEA4 1 1 0 0 3803737830 split(3/8)",4715;\r
 631 "6725783616",4864;\r
 632 "QITNPEA  5400790175 a split(0/4)",5054;\r
 633 "ZTGIJCF4 1 0 1 0 1821661595 split(3/8)",5089;\r
 634 "GLFVCVK4 2477216213 split(20/64)",5144;\r
 635 "181212899 1",5181;\r
 636 "181212899 0",5226;\r
 637 "MKFKQWU halfwt",5307;\r
 638 "3221740746 a",5611;\r
 639 "9861833891",6705;\r
 640 "5405130650",8072;\r
 641 "3603097872",13611;\r
 642 "5493250206",43794;\r
 643 ];;