Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/GAP/pkg/sonata/nri/   (GAP Algebra Version 4.15.1©)  Datei vom 23.8.2025 mit Größe 386 kB image not shown  

Impressum nri16_4.nr   Sprache: unbekannt

 
Spracherkennung für: .nr vermutete Sprache: Unknown {[0] [0] [0]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen]

NI16_4 := rec(
  group_name := "16/4",
  group_generators := [ (1,2), (3,4), (5,6,7,8) ],
  elements := rec(
      1 := (),
      2 := (5,6,7,8),
      3 := (5,7)(6,8),
      4 := (5,8,7,6),
      5 := (3,4),
      6 := (3,4)(5,6,7,8),
      7 := (3,4)(5,7)(6,8),
      8 := (3,4)(5,8,7,6),
      9 := (1,2),
      10 := (1,2)(5,6,7,8),
      11 := (1,2)(5,7)(6,8),
      12 := (1,2)(5,8,7,6),
      13 := (1,2)(3,4),
      14 := (1,2)(3,4)(5,6,7,8),
      15 := (1,2)(3,4)(5,7)(6,8),
      16 := (1,2)(3,4)(5,8,7,6) ),
  group_endomorphisms := rec(
      1 := [ 1111111111111111 ],
      2 := [ 1111111133333333 ],
      3 := [ 1111111155555555 ],
      4 := [ 1111111177777777 ],
      5 := [ 1111111199999999 ],
      6 := [ 111111111111111111111111 ],
      7 := [ 111111111313131313131313 ],
      8 := [ 111111111515151515151515 ],
      9 := [ 1111333311113333 ],
      10 := [ 1111333333331111 ],
      11 := [ 1111333355557777 ],
      12 := [ 1111333377775555 ],
      13 := [ 11113333999911111111 ],
      14 := [ 11113333111111119999 ],
      15 := [ 111133331313131315151515 ],
      16 := [ 111133331515151513131313 ],
      17 := [ 1111555511115555 ],
      18 := [ 1111555533337777 ],
      19 := [ 1111555555551111 ],
      20 := [ 1111555577773333 ],
      21 := [ 11115555999913131313 ],
      22 := [ 111155551111111115151515 ],
      23 := [ 11115555131313139999 ],
      24 := [ 111155551515151511111111 ],
      25 := [ 1111777711117777 ],
      26 := [ 1111777733335555 ],
      27 := [ 1111777755553333 ],
      28 := [ 1111777777771111 ],
      29 := [ 11117777999915151515 ],
      30 := [ 111177771111111113131313 ],
      31 := [ 111177771313131311111111 ],
      32 := [ 11117777151515159999 ],
      33 := [ 1111999911119999 ],
      34 := [ 11119999333311111111 ],
      35 := [ 11119999555513131313 ],
      36 := [ 11119999777715151515 ],
      37 := [ 1111999999991111 ],
      38 := [ 11119999111111113333 ],
      39 := [ 11119999131313135555 ],
      40 := [ 11119999151515157777 ],
      41 := [ 111111111111111111111111 ],
      42 := [ 11111111111133339999 ],
      43 := [ 111111111111555515151515 ],
      44 := [ 111111111111777713131313 ],
      45 := [ 11111111111199993333 ],
      46 := [ 111111111111111111111111 ],
      47 := [ 111111111111131313137777 ],
      48 := [ 111111111111151515155555 ],
      49 := [ 111113131313111113131313 ],
      50 := [ 111113131313333315151515 ],
      51 := [ 11111313131355559999 ],
      52 := [ 111113131313777711111111 ],
      53 := [ 11111313131399995555 ],
      54 := [ 111113131313111111117777 ],
      55 := [ 111113131313131313131111 ],
      56 := [ 111113131313151515153333 ],
      57 := [ 111115151515111115151515 ],
      58 := [ 111115151515333313131313 ],
      59 := [ 111115151515555511111111 ],
      60 := [ 11111515151577779999 ],
      61 := [ 11111515151599997777 ],
      62 := [ 111115151515111111115555 ],
      63 := [ 111115151515131313133333 ],
      64 := [ 111115151515151515151111 ],
      65 := [ 1234123412341234 ],
      66 := [ 1234123434123412 ],
      67 := [ 1234123456785678 ],
      68 := [ 1234123478567856 ],
      69 := [ 1234123491011129101112 ],
      70 := [ 1234123411129101112910 ],
      71 := [ 123412341314151613141516 ],
      72 := [ 123412341516131415161314 ],
      73 := [ 1234341212343412 ],
      74 := [ 1234341234121234 ],
      75 := [ 1234341256787856 ],
      76 := [ 1234341278565678 ],
      77 := [ 1234341291011121112910 ],
      78 := [ 1234341211129109101112 ],
      79 := [ 123434121314151615161314 ],
      80 := [ 123434121516131413141516 ],
      81 := [ 1234567812345678 ],
      82 := [ 1234567834127856 ],
      83 := [ 1234567856781234 ],
      84 := [ 1234567878563412 ],
      85 := [ 12345678111291015161314 ],
      86 := [ 12345678131415169101112 ],
      87 := [ 12345678151613141112910 ],
      88 := [ 1234785612347856 ],
      89 := [ 1234785634125678 ],
      90 := [ 1234785656783412 ],
      91 := [ 1234785678561234 ],
      92 := [ 12347856910111215161314 ],
      93 := [ 12347856111291013141516 ],
      94 := [ 12347856131415161112910 ],
      95 := [ 12347856151613149101112 ],
      96 := [ 1234910111212349101112 ],
      97 := [ 1234910111234121112910 ],
      98 := [ 12349101112567813141516 ],
      99 := [ 12349101112785615161314 ],
      100 := [ 1234910111291011121234 ],
      101 := [ 1234910111211129103412 ],
      102 := [ 12349101112131415165678 ],
      103 := [ 12349101112151613147856 ],
      104 := [ 1234111291012341112910 ],
      105 := [ 1234111291034129101112 ],
      106 := [ 12341112910567815161314 ],
      107 := [ 12341112910785613141516 ],
      108 := [ 1234111291091011123412 ],
      109 := [ 1234111291011129101234 ],
      110 := [ 12341112910131415167856 ],
      111 := [ 12341112910151613145678 ],
      112 := [ 123413141516123413141516 ],
      113 := [ 123413141516341215161314 ],
      114 := [ 12341314151656789101112 ],
      115 := [ 12341314151678561112910 ],
      116 := [ 12341314151691011125678 ],
      117 := [ 12341314151611129107856 ],
      118 := [ 123413141516131415161234 ],
      119 := [ 123413141516151613143412 ],
      120 := [ 123415161314123415161314 ],
      121 := [ 123415161314341213141516 ],
      122 := [ 12341516131456781112910 ],
      123 := [ 12341516131478569101112 ],
      124 := [ 12341516131491011127856 ],
      125 := [ 12341516131411129105678 ],
      126 := [ 123415161314131415163412 ],
      127 := [ 123415161314151613141234 ],
      128 := [ 1313131313131313 ],
      129 := [ 1313131331313131 ],
      130 := [ 1313131357575757 ],
      131 := [ 1313131375757575 ],
      132 := [ 13131313911911911911 ],
      133 := [ 13131313119119119119 ],
      134 := [ 131313131315131513151315 ],
      135 := [ 131313131513151315131513 ],
      136 := [ 1313313113133131 ],
      137 := [ 1313313131311313 ],
      138 := [ 1313313157577575 ],
      139 := [ 1313313175755757 ],
      140 := [ 13133131911911119119 ],
      141 := [ 13133131119119911911 ],
      142 := [ 131331311315131515131513 ],
      143 := [ 131331311513151313151315 ],
      144 := [ 1313575713135757 ],
      145 := [ 1313575731317575 ],
      146 := [ 1313575757571313 ],
      147 := [ 1313575775753131 ],
      148 := [ 1313575791191113151315 ],
      149 := [ 1313575711911915131513 ],
      150 := [ 1313575713151315911911 ],
      151 := [ 1313575715131513119119 ],
      152 := [ 1313757513137575 ],
      153 := [ 1313757531315757 ],
      154 := [ 1313757557573131 ],
      155 := [ 1313757575751313 ],
      156 := [ 1313757591191115131513 ],
      157 := [ 1313757511911913151315 ],
      158 := [ 1313757513151315119119 ],
      159 := [ 1313757515131513911911 ],
      160 := [ 13139119111313911911 ],
      161 := [ 13139119113131119119 ],
      162 := [ 1313911911575713151315 ],
      163 := [ 1313911911757515131513 ],
      164 := [ 13139119119119111313 ],
      165 := [ 13139119111191193131 ],
      166 := [ 1313911911131513155757 ],
      167 := [ 1313911911151315137575 ],
      168 := [ 13131191191313119119 ],
      169 := [ 13131191193131911911 ],
      170 := [ 1313119119575715131513 ],
      171 := [ 1313119119757513151315 ],
      172 := [ 13131191199119113131 ],
      173 := [ 13131191191191191313 ],
      174 := [ 1313119119131513157575 ],
      175 := [ 1313119119151315135757 ],
      176 := [ 131313151315131313151315 ],
      177 := [ 131313151315313115131513 ],
      178 := [ 1313131513155757911911 ],
      179 := [ 1313131513157575119119 ],
      180 := [ 1313131513159119115757 ],
      181 := [ 1313131513151191197575 ],
      182 := [ 131313151315131513151313 ],
      183 := [ 131313151315151315133131 ],
      184 := [ 131315131513131315131513 ],
      185 := [ 131315131513313113151315 ],
      186 := [ 1313151315135757119119 ],
      187 := [ 1313151315137575911911 ],
      188 := [ 1313151315139119117575 ],
      189 := [ 1313151315131191195757 ],
      190 := [ 131315131513131513153131 ],
      191 := [ 131315131513151315131313 ],
      192 := [ 1432143214321432 ],
      193 := [ 1432143232143214 ],
      194 := [ 1432143258765876 ],
      195 := [ 1432143276587658 ],
      196 := [ 1432143291211109121110 ],
      197 := [ 1432143211109121110912 ],
      198 := [ 143214321316151413161514 ],
      199 := [ 143214321514131615141316 ],
      200 := [ 1432321414323214 ],
      201 := [ 1432321432141432 ],
      202 := [ 1432321458767658 ],
      203 := [ 1432321476585876 ],
      204 := [ 1432321491211101110912 ],
      205 := [ 1432321411109129121110 ],
      206 := [ 143232141316151415141316 ],
      207 := [ 143232141514131613161514 ],
      208 := [ 1432587614325876 ],
      209 := [ 1432587632147658 ],
      210 := [ 1432587658761432 ],
      211 := [ 1432587676583214 ],
      212 := [ 14325876912111013161514 ],
      213 := [ 14325876111091215141316 ],
      214 := [ 14325876131615149121110 ],
      215 := [ 14325876151413161110912 ],
      216 := [ 1432765814327658 ],
      217 := [ 1432765832145876 ],
      218 := [ 1432765858763214 ],
      219 := [ 1432765876581432 ],
      220 := [ 14327658912111015141316 ],
      221 := [ 14327658111091213161514 ],
      222 := [ 14327658131615141110912 ],
      223 := [ 14327658151413169121110 ],
      224 := [ 1432912111014329121110 ],
      225 := [ 1432912111032141110912 ],
      226 := [ 14329121110587613161514 ],
      227 := [ 14329121110765815141316 ],
      228 := [ 1432912111091211101432 ],
      229 := [ 1432912111011109123214 ],
      230 := [ 14329121110131615145876 ],
      231 := [ 14329121110151413167658 ],
      232 := [ 1432111091214321110912 ],
      233 := [ 1432111091232149121110 ],
      234 := [ 14321110912587615141316 ],
      235 := [ 14321110912765813161514 ],
      236 := [ 1432111091291211103214 ],
      237 := [ 1432111091211109121432 ],
      238 := [ 14321110912131615147658 ],
      239 := [ 14321110912151413165876 ],
      240 := [ 143213161514143213161514 ],
      241 := [ 143213161514321415141316 ],
      242 := [ 14321316151458769121110 ],
      243 := [ 14321316151476581110912 ],
      244 := [ 14321316151491211105876 ],
      245 := [ 14321316151411109127658 ],
      246 := [ 143213161514131615141432 ],
      247 := [ 143213161514151413163214 ],
      248 := [ 143215141316143215141316 ],
      249 := [ 143215141316321413161514 ],
      250 := [ 14321514131658761110912 ],
      251 := [ 14321514131676589121110 ],
      252 := [ 14321514131691211107658 ],
      253 := [ 14321514131611109125876 ],
      254 := [ 143215141316131615143214 ],
      255 := [ 143215141316151413161432 ],
      256 := [ 1515151515151515 ],
      257 := [ 1515151537373737 ],
      258 := [ 1515151551515151 ],
      259 := [ 1515151573737373 ],
      260 := [ 15151515913913913913 ],
      261 := [ 151515151115111511151115 ],
      262 := [ 15151515139139139139 ],
      263 := [ 151515151511151115111511 ],
      264 := [ 1515373715153737 ],
      265 := [ 1515373737371515 ],
      266 := [ 1515373751517373 ],
      267 := [ 1515373773735151 ],
      268 := [ 1515373791391311151115 ],
      269 := [ 1515373711151115913913 ],
      270 := [ 1515373713913915111511 ],
      271 := [ 1515373715111511139139 ],
      272 := [ 1515515115155151 ],
      273 := [ 1515515137377373 ],
      274 := [ 1515515151511515 ],
      275 := [ 1515515173733737 ],
      276 := [ 15155151913913139139 ],
      277 := [ 151551511115111515111511 ],
      278 := [ 15155151139139913913 ],
      279 := [ 151551511511151111151115 ],
      280 := [ 1515737315157373 ],
      281 := [ 1515737337375151 ],
      282 := [ 1515737351513737 ],
      283 := [ 1515737373731515 ],
      284 := [ 1515737391391315111511 ],
      285 := [ 1515737311151115139139 ],
      286 := [ 1515737313913911151115 ],
      287 := [ 1515737315111511913913 ],
      288 := [ 15159139131515913913 ],
      289 := [ 1515913913373711151115 ],
      290 := [ 15159139135151139139 ],
      291 := [ 1515913913737315111511 ],
      292 := [ 15159139139139131515 ],
      293 := [ 1515913913111511153737 ],
      294 := [ 15159139131391395151 ],
      295 := [ 1515913913151115117373 ],
      296 := [ 151511151115151511151115 ],
      297 := [ 1515111511153737913913 ],
      298 := [ 151511151115515115111511 ],
      299 := [ 1515111511157373139139 ],
      300 := [ 1515111511159139133737 ],
      301 := [ 151511151115111511151515 ],
      302 := [ 1515111511151391397373 ],
      303 := [ 151511151115151115115151 ],
      304 := [ 15151391391515139139 ],
      305 := [ 1515139139373715111511 ],
      306 := [ 15151391395151913913 ],
      307 := [ 1515139139737311151115 ],
      308 := [ 15151391399139135151 ],
      309 := [ 1515139139111511157373 ],
      310 := [ 15151391391391391515 ],
      311 := [ 1515139139151115113737 ],
      312 := [ 151515111511151515111511 ],
      313 := [ 1515151115113737139139 ],
      314 := [ 151515111511515111151115 ],
      315 := [ 1515151115117373913913 ],
      316 := [ 1515151115119139137373 ],
      317 := [ 151515111511111511155151 ],
      318 := [ 1515151115111391393737 ],
      319 := [ 151515111511151115111515 ],
      320 := [ 1638163816381638 ],
      321 := [ 1638163838163816 ],
      322 := [ 1638163852745274 ],
      323 := [ 1638163874527452 ],
      324 := [ 1638163891411169141116 ],
      325 := [ 1638163811169141116914 ],
      326 := [ 163816381310151213101512 ],
      327 := [ 163816381512131015121310 ],
      328 := [ 1638381616383816 ],
      329 := [ 1638381638161638 ],
      330 := [ 1638381652747452 ],
      331 := [ 1638381674525274 ],
      332 := [ 1638381691411161116914 ],
      333 := [ 1638381611169149141116 ],
      334 := [ 163838161310151215121310 ],
      335 := [ 163838161512131013101512 ],
      336 := [ 1638527416385274 ],
      337 := [ 1638527438167452 ],
      338 := [ 1638527452741638 ],
      339 := [ 1638527474523816 ],
      340 := [ 16385274914111613101512 ],
      341 := [ 16385274111691415121310 ],
      342 := [ 16385274131015129141116 ],
      343 := [ 16385274151213101116914 ],
      344 := [ 1638745216387452 ],
      345 := [ 1638745238165274 ],
      346 := [ 1638745252743816 ],
      347 := [ 1638745274521638 ],
      348 := [ 16387452914111615121310 ],
      349 := [ 16387452111691413101512 ],
      350 := [ 16387452131015121116914 ],
      351 := [ 16387452151213109141116 ],
      352 := [ 1638914111616389141116 ],
      353 := [ 1638914111638161116914 ],
      354 := [ 16389141116527413101512 ],
      355 := [ 16389141116745215121310 ],
      356 := [ 1638914111691411161638 ],
      357 := [ 1638914111611169143816 ],
      358 := [ 16389141116131015125274 ],
      359 := [ 16389141116151213107452 ],
      360 := [ 1638111691416381116914 ],
      361 := [ 1638111691438169141116 ],
      362 := [ 16381116914527415121310 ],
      363 := [ 16381116914745213101512 ],
      364 := [ 1638111691491411163816 ],
      365 := [ 1638111691411169141638 ],
      366 := [ 16381116914131015127452 ],
      367 := [ 16381116914151213105274 ],
      368 := [ 163813101512163813101512 ],
      369 := [ 163813101512381615121310 ],
      370 := [ 16381310151252749141116 ],
      371 := [ 16381310151274521116914 ],
      372 := [ 16381310151291411165274 ],
      373 := [ 16381310151211169147452 ],
      374 := [ 163813101512131015121638 ],
      375 := [ 163813101512151213103816 ],
      376 := [ 163815121310163815121310 ],
      377 := [ 163815121310381613101512 ],
      378 := [ 16381512131052741116914 ],
      379 := [ 16381512131074529141116 ],
      380 := [ 16381512131091411167452 ],
      381 := [ 16381512131011169145274 ],
      382 := [ 163815121310131015123816 ],
      383 := [ 163815121310151213101638 ],
      384 := [ 1717171717171717 ],
      385 := [ 1717171735353535 ],
      386 := [ 1717171753535353 ],
      387 := [ 1717171771717171 ],
      388 := [ 17171717915915915915 ],
      389 := [ 171717171113111311131113 ],
      390 := [ 171717171311131113111311 ],
      391 := [ 17171717159159159159 ],
      392 := [ 1717353517173535 ],
      393 := [ 1717353535351717 ],
      394 := [ 1717353553537171 ],
      395 := [ 1717353571715353 ],
      396 := [ 1717353591591511131113 ],
      397 := [ 1717353511131113915915 ],
      398 := [ 1717353513111311159159 ],
      399 := [ 1717353515915913111311 ],
      400 := [ 1717535317175353 ],
      401 := [ 1717535335357171 ],
      402 := [ 1717535353531717 ],
      403 := [ 1717535371713535 ],
      404 := [ 1717535391591513111311 ],
      405 := [ 1717535311131113159159 ],
      406 := [ 1717535313111311915915 ],
      407 := [ 1717535315915911131113 ],
      408 := [ 1717717117177171 ],
      409 := [ 1717717135355353 ],
      410 := [ 1717717153533535 ],
      411 := [ 1717717171711717 ],
      412 := [ 17177171915915159159 ],
      413 := [ 171771711113111313111311 ],
      414 := [ 171771711311131111131113 ],
      415 := [ 17177171159159915915 ],
      416 := [ 17179159151717915915 ],
      417 := [ 1717915915353511131113 ],
      418 := [ 1717915915535313111311 ],
      419 := [ 17179159157171159159 ],
      420 := [ 17179159159159151717 ],
      421 := [ 1717915915111311133535 ],
      422 := [ 1717915915131113115353 ],
      423 := [ 17179159151591597171 ],
      424 := [ 171711131113171711131113 ],
      425 := [ 1717111311133535915915 ],
      426 := [ 1717111311135353159159 ],
      427 := [ 171711131113717113111311 ],
      428 := [ 1717111311139159153535 ],
      429 := [ 171711131113111311131717 ],
      430 := [ 171711131113131113117171 ],
      431 := [ 1717111311131591595353 ],
      432 := [ 171713111311171713111311 ],
      433 := [ 1717131113113535159159 ],
      434 := [ 1717131113115353915915 ],
      435 := [ 171713111311717111131113 ],
      436 := [ 1717131113119159155353 ],
      437 := [ 171713111311111311137171 ],
      438 := [ 171713111311131113111717 ],
      439 := [ 1717131113111591593535 ],
      440 := [ 17171591591717159159 ],
      441 := [ 1717159159353513111311 ],
      442 := [ 1717159159535311131113 ],
      443 := [ 17171591597171915915 ],
      444 := [ 17171591599159157171 ],
      445 := [ 1717159159111311135353 ],
      446 := [ 1717159159131113113535 ],
      447 := [ 17171591591591591717 ],
      448 := [ 1836183618361836 ],
      449 := [ 1836183636183618 ],
      450 := [ 1836183654725472 ],
      451 := [ 1836183672547254 ],
      452 := [ 1836183691611149161114 ],
      453 := [ 1836183611149161114916 ],
      454 := [ 183618361312151013121510 ],
      455 := [ 183618361510131215101312 ],
      456 := [ 1836361818363618 ],
      457 := [ 1836361836181836 ],
      458 := [ 1836361854727254 ],
      459 := [ 1836361872545472 ],
      460 := [ 1836361891611141114916 ],
      461 := [ 1836361811149169161114 ],
      462 := [ 183636181312151015101312 ],
      463 := [ 183636181510131213121510 ],
      464 := [ 1836547218365472 ],
      465 := [ 1836547236187254 ],
      466 := [ 1836547254721836 ],
      467 := [ 1836547272543618 ],
      468 := [ 18365472916111413121510 ],
      469 := [ 18365472111491615101312 ],
      470 := [ 18365472131215109161114 ],
      471 := [ 18365472151013121114916 ],
      472 := [ 1836725418367254 ],
      473 := [ 1836725436185472 ],
      474 := [ 1836725454723618 ],
      475 := [ 1836725472541836 ],
      476 := [ 18367254916111415101312 ],
      477 := [ 18367254111491613121510 ],
      478 := [ 18367254131215101114916 ],
      479 := [ 18367254151013129161114 ],
      480 := [ 1836916111418369161114 ],
      481 := [ 1836916111436181114916 ],
      482 := [ 18369161114547213121510 ],
      483 := [ 18369161114725415101312 ],
      484 := [ 1836916111491611141836 ],
      485 := [ 1836916111411149163618 ],
      486 := [ 18369161114131215105472 ],
      487 := [ 18369161114151013127254 ],
      488 := [ 1836111491618361114916 ],
      489 := [ 1836111491636189161114 ],
      490 := [ 18361114916547215101312 ],
      491 := [ 18361114916725413121510 ],
      492 := [ 1836111491691611143618 ],
      493 := [ 1836111491611149161836 ],
      494 := [ 18361114916131215107254 ],
      495 := [ 18361114916151013125472 ],
      496 := [ 183613121510183613121510 ],
      497 := [ 183613121510361815101312 ],
      498 := [ 18361312151054729161114 ],
      499 := [ 18361312151072541114916 ],
      500 := [ 18361312151091611145472 ],
      501 := [ 18361312151011149167254 ],
      502 := [ 183613121510131215101836 ],
      503 := [ 183613121510151013123618 ],
      504 := [ 183615101312183615101312 ],
      505 := [ 183615101312361813121510 ],
      506 := [ 18361510131254721114916 ],
      507 := [ 18361510131272549161114 ],
      508 := [ 18361510131291611147254 ],
      509 := [ 18361510131211149165472 ],
      510 := [ 183615101312131215103618 ],
      511 := [ 183615101312151013121836 ],
      512 := [ 1919191919191919 ],
      513 := [ 19191919311311311311 ],
      514 := [ 19191919513513513513 ],
      515 := [ 19191919715715715715 ],
      516 := [ 1919191991919191 ],
      517 := [ 19191919113113113113 ],
      518 := [ 19191919135135135135 ],
      519 := [ 19191919157157157157 ],
      520 := [ 19193113111919311311 ],
      521 := [ 19193113113113111919 ],
      522 := [ 1919311311513513715715 ],
      523 := [ 1919311311715715513513 ],
      524 := [ 19193113119191113113 ],
      525 := [ 19193113111131139191 ],
      526 := [ 1919311311135135157157 ],
      527 := [ 1919311311157157135135 ],
      528 := [ 19195135131919513513 ],
      529 := [ 1919513513311311715715 ],
      530 := [ 19195135135135131919 ],
      531 := [ 1919513513715715311311 ],
      532 := [ 19195135139191135135 ],
      533 := [ 1919513513113113157157 ],
      534 := [ 19195135131351359191 ],
      535 := [ 1919513513157157113113 ],
      536 := [ 19197157151919715715 ],
      537 := [ 1919715715311311513513 ],
      538 := [ 1919715715513513311311 ],
      539 := [ 19197157157157151919 ],
      540 := [ 19197157159191157157 ],
      541 := [ 1919715715113113135135 ],
      542 := [ 1919715715135135113113 ],
      543 := [ 19197157151571579191 ],
      544 := [ 1919919119199191 ],
      545 := [ 19199191311311113113 ],
      546 := [ 19199191513513135135 ],
      547 := [ 19199191715715157157 ],
      548 := [ 1919919191911919 ],
      549 := [ 19199191113113311311 ],
      550 := [ 19199191135135513513 ],
      551 := [ 19199191157157715715 ],
      552 := [ 19191131131919113113 ],
      553 := [ 19191131133113119191 ],
      554 := [ 1919113113513513157157 ],
      555 := [ 1919113113715715135135 ],
      556 := [ 19191131139191311311 ],
      557 := [ 19191131131131131919 ],
      558 := [ 1919113113135135715715 ],
      559 := [ 1919113113157157513513 ],
      560 := [ 19191351351919135135 ],
      561 := [ 1919135135311311157157 ],
      562 := [ 19191351355135139191 ],
      563 := [ 1919135135715715113113 ],
      564 := [ 19191351359191513513 ],
      565 := [ 1919135135113113715715 ],
      566 := [ 19191351351351351919 ],
      567 := [ 1919135135157157311311 ],
      568 := [ 19191571571919157157 ],
      569 := [ 1919157157311311135135 ],
      570 := [ 1919157157513513113113 ],
      571 := [ 19191571577157159191 ],
      572 := [ 19191571579191715715 ],
      573 := [ 1919157157113113513513 ],
      574 := [ 1919157157135135311311 ],
      575 := [ 19191571571571571919 ],
      576 := [ 110312110312110312110312 ],
      577 := [ 110312110312312110312110 ],
      578 := [ 110312110312514716514716 ],
      579 := [ 110312110312716514716514 ],
      580 := [ 1103121103129211492114 ],
      581 := [ 1103121103121149211492 ],
      582 := [ 110312110312136158136158 ],
      583 := [ 110312110312158136158136 ],
      584 := [ 110312312110110312312110 ],
      585 := [ 110312312110312110110312 ],
      586 := [ 110312312110514716716514 ],
      587 := [ 110312312110716514514716 ],
      588 := [ 1103123121109211411492 ],
      589 := [ 1103123121101149292114 ],
      590 := [ 110312312110136158158136 ],
      591 := [ 110312312110158136136158 ],
      592 := [ 110312514716110312514716 ],
      593 := [ 110312514716312110716514 ],
      594 := [ 110312514716514716110312 ],
      595 := [ 110312514716716514312110 ],
      596 := [ 11031251471692114136158 ],
      597 := [ 11031251471611492158136 ],
      598 := [ 11031251471613615892114 ],
      599 := [ 11031251471615813611492 ],
      600 := [ 110312716514110312716514 ],
      601 := [ 110312716514312110514716 ],
      602 := [ 110312716514514716312110 ],
      603 := [ 110312716514716514110312 ],
      604 := [ 11031271651492114158136 ],
      605 := [ 11031271651411492136158 ],
      606 := [ 11031271651413615811492 ],
      607 := [ 11031271651415813692114 ],
      608 := [ 1103129211411031292114 ],
      609 := [ 1103129211431211011492 ],
      610 := [ 11031292114514716136158 ],
      611 := [ 11031292114716514158136 ],
      612 := [ 1103129211492114110312 ],
      613 := [ 1103129211411492312110 ],
      614 := [ 11031292114136158514716 ],
      615 := [ 11031292114158136716514 ],
      616 := [ 1103121149211031211492 ],
      617 := [ 1103121149231211092114 ],
      618 := [ 11031211492514716158136 ],
      619 := [ 11031211492716514136158 ],
      620 := [ 1103121149292114312110 ],
      621 := [ 1103121149211492110312 ],
      622 := [ 11031211492136158716514 ],
      623 := [ 11031211492158136514716 ],
      624 := [ 110312136158110312136158 ],
      625 := [ 110312136158312110158136 ],
      626 := [ 11031213615851471692114 ],
      627 := [ 11031213615871651411492 ],
      628 := [ 11031213615892114514716 ],
      629 := [ 11031213615811492716514 ],
      630 := [ 110312136158136158110312 ],
      631 := [ 110312136158158136312110 ],
      632 := [ 110312158136110312158136 ],
      633 := [ 110312158136312110136158 ],
      634 := [ 11031215813651471611492 ],
      635 := [ 11031215813671651492114 ],
      636 := [ 11031215813692114716514 ],
      637 := [ 11031215813611492514716 ],
      638 := [ 110312158136136158312110 ],
      639 := [ 110312158136158136110312 ],
      640 := [ 111111111111111111111111 ],
      641 := [ 11111111111139393939 ],
      642 := [ 111111111111515515515515 ],
      643 := [ 111111111111713713713713 ],
      644 := [ 11111111111193939393 ],
      645 := [ 111111111111111111111111 ],
      646 := [ 111111111111137137137137 ],
      647 := [ 111111111111155155155155 ],
      648 := [ 11111139391111113939 ],
      649 := [ 11111139393939111111 ],
      650 := [ 1111113939515515713713 ],
      651 := [ 1111113939713713515515 ],
      652 := [ 11111139399393111111 ],
      653 := [ 11111139391111119393 ],
      654 := [ 1111113939137137155155 ],
      655 := [ 1111113939155155137137 ],
      656 := [ 111111515515111111515515 ],
      657 := [ 1111115155153939713713 ],
      658 := [ 111111515515515515111111 ],
      659 := [ 1111115155157137133939 ],
      660 := [ 1111115155159393137137 ],
      661 := [ 111111515515111111155155 ],
      662 := [ 1111115155151371379393 ],
      663 := [ 111111515515155155111111 ],
      664 := [ 111111713713111111713713 ],
      665 := [ 1111117137133939515515 ],
      666 := [ 1111117137135155153939 ],
      667 := [ 111111713713713713111111 ],
      668 := [ 1111117137139393155155 ],
      669 := [ 111111713713111111137137 ],
      670 := [ 111111713713137137111111 ],
      671 := [ 1111117137131551559393 ],
      672 := [ 11111193931111119393 ],
      673 := [ 11111193933939111111 ],
      674 := [ 1111119393515515137137 ],
      675 := [ 1111119393713713155155 ],
      676 := [ 11111193939393111111 ],
      677 := [ 11111193931111113939 ],
      678 := [ 1111119393137137515515 ],
      679 := [ 1111119393155155713713 ],
      680 := [ 111111111111111111111111 ],
      681 := [ 11111111111139399393 ],
      682 := [ 111111111111515515155155 ],
      683 := [ 111111111111713713137137 ],
      684 := [ 11111111111193933939 ],
      685 := [ 111111111111111111111111 ],
      686 := [ 111111111111137137713713 ],
      687 := [ 111111111111155155515515 ],
      688 := [ 111111137137111111137137 ],
      689 := [ 1111111371373939155155 ],
      690 := [ 1111111371375155159393 ],
      691 := [ 111111137137713713111111 ],
      692 := [ 1111111371379393515515 ],
      693 := [ 111111137137111111713713 ],
      694 := [ 111111137137137137111111 ],
      695 := [ 1111111371371551553939 ],
      696 := [ 111111155155111111155155 ],
      697 := [ 1111111551553939137137 ],
      698 := [ 111111155155515515111111 ],
      699 := [ 1111111551557137139393 ],
      700 := [ 1111111551559393713713 ],
      701 := [ 111111155155111111515515 ],
      702 := [ 1111111551551371373939 ],
      703 := [ 111111155155155155111111 ],
      704 := [ 112310112310112310112310 ],
      705 := [ 112310112310310112310112 ],
      706 := [ 112310112310516714516714 ],
      707 := [ 112310112310714516714516 ],
      708 := [ 1123101123109411294112 ],
      709 := [ 1123101123101129411294 ],
      710 := [ 112310112310138156138156 ],
      711 := [ 112310112310156138156138 ],
      712 := [ 112310310112112310310112 ],
      713 := [ 112310310112310112112310 ],
      714 := [ 112310310112516714714516 ],
      715 := [ 112310310112714516516714 ],
      716 := [ 1123103101129411211294 ],
      717 := [ 1123103101121129494112 ],
      718 := [ 112310310112138156156138 ],
      719 := [ 112310310112156138138156 ],
      720 := [ 112310516714112310516714 ],
      721 := [ 112310516714310112714516 ],
      722 := [ 112310516714516714112310 ],
      723 := [ 112310516714714516310112 ],
      724 := [ 11231051671494112138156 ],
      725 := [ 11231051671411294156138 ],
      726 := [ 11231051671413815694112 ],
      727 := [ 11231051671415613811294 ],
      728 := [ 112310714516112310714516 ],
      729 := [ 112310714516310112516714 ],
      730 := [ 112310714516516714310112 ],
      731 := [ 112310714516714516112310 ],
      732 := [ 11231071451694112156138 ],
      733 := [ 11231071451611294138156 ],
      734 := [ 11231071451613815611294 ],
      735 := [ 11231071451615613894112 ],
      736 := [ 1123109411211231094112 ],
      737 := [ 1123109411231011211294 ],
      738 := [ 11231094112516714138156 ],
      739 := [ 11231094112714516156138 ],
      740 := [ 1123109411294112112310 ],
      741 := [ 1123109411211294310112 ],
      742 := [ 11231094112138156516714 ],
      743 := [ 11231094112156138714516 ],
      744 := [ 1123101129411231011294 ],
      745 := [ 1123101129431011294112 ],
      746 := [ 11231011294516714156138 ],
      747 := [ 11231011294714516138156 ],
      748 := [ 1123101129494112310112 ],
      749 := [ 1123101129411294112310 ],
      750 := [ 11231011294138156714516 ],
      751 := [ 11231011294156138516714 ],
      752 := [ 112310138156112310138156 ],
      753 := [ 112310138156310112156138 ],
      754 := [ 11231013815651671494112 ],
      755 := [ 11231013815671451611294 ],
      756 := [ 11231013815694112516714 ],
      757 := [ 11231013815611294714516 ],
      758 := [ 112310138156138156112310 ],
      759 := [ 112310138156156138310112 ],
      760 := [ 112310156138112310156138 ],
      761 := [ 112310156138310112138156 ],
      762 := [ 11231015613851671411294 ],
      763 := [ 11231015613871451694112 ],
      764 := [ 11231015613894112714516 ],
      765 := [ 11231015613811294516714 ],
      766 := [ 112310156138138156310112 ],
      767 := [ 112310156138156138112310 ],
      768 := [ 113113113113113113113113 ],
      769 := [ 113113113113315315315315 ],
      770 := [ 11311311311359595959 ],
      771 := [ 113113113113711711711711 ],
      772 := [ 11311311311395959595 ],
      773 := [ 113113113113117117117117 ],
      774 := [ 113113113113131131131131 ],
      775 := [ 113113113113153153153153 ],
      776 := [ 113113315315113113315315 ],
      777 := [ 113113315315315315113113 ],
      778 := [ 1131133153155959711711 ],
      779 := [ 1131133153157117115959 ],
      780 := [ 1131133153159595117117 ],
      781 := [ 1131133153151171179595 ],
      782 := [ 113113315315131131153153 ],
      783 := [ 113113315315153153131131 ],
      784 := [ 11311359591131135959 ],
      785 := [ 1131135959315315711711 ],
      786 := [ 11311359595959113113 ],
      787 := [ 1131135959711711315315 ],
      788 := [ 11311359599595131131 ],
      789 := [ 1131135959117117153153 ],
      790 := [ 11311359591311319595 ],
      791 := [ 1131135959153153117117 ],
      792 := [ 113113711711113113711711 ],
      793 := [ 1131137117113153155959 ],
      794 := [ 1131137117115959315315 ],
      795 := [ 113113711711711711113113 ],
      796 := [ 1131137117119595153153 ],
      797 := [ 113113711711117117131131 ],
      798 := [ 113113711711131131117117 ],
      799 := [ 1131137117111531539595 ],
      800 := [ 11311395951131139595 ],
      801 := [ 1131139595315315117117 ],
      802 := [ 11311395955959131131 ],
      803 := [ 1131139595711711153153 ],
      804 := [ 11311395959595113113 ],
      805 := [ 1131139595117117315315 ],
      806 := [ 11311395951311315959 ],
      807 := [ 1131139595153153711711 ],
      808 := [ 113113117117113113117117 ],
      809 := [ 1131131171173153159595 ],
      810 := [ 1131131171175959153153 ],
      811 := [ 113113117117711711131131 ],
      812 := [ 1131131171179595315315 ],
      813 := [ 113113117117117117113113 ],
      814 := [ 113113117117131131711711 ],
      815 := [ 1131131171171531535959 ],
      816 := [ 113113131131113113131131 ],
      817 := [ 113113131131315315153153 ],
      818 := [ 11311313113159599595 ],
      819 := [ 113113131131711711117117 ],
      820 := [ 11311313113195955959 ],
      821 := [ 113113131131117117711711 ],
      822 := [ 113113131131131131113113 ],
      823 := [ 113113131131153153315315 ],
      824 := [ 113113153153113113153153 ],
      825 := [ 113113153153315315131131 ],
      826 := [ 1131131531535959117117 ],
      827 := [ 1131131531537117119595 ],
      828 := [ 1131131531539595711711 ],
      829 := [ 1131131531531171175959 ],
      830 := [ 113113153153131131315315 ],
      831 := [ 113113153153153153113113 ],
      832 := [ 114316114316114316114316 ],
      833 := [ 114316114316316114316114 ],
      834 := [ 114316114316510712510712 ],
      835 := [ 114316114316712510712510 ],
      836 := [ 1143161143169611896118 ],
      837 := [ 1143161143161189611896 ],
      838 := [ 114316114316132154132154 ],
      839 := [ 114316114316154132154132 ],
      840 := [ 114316316114114316316114 ],
      841 := [ 114316316114316114114316 ],
      842 := [ 114316316114510712712510 ],
      843 := [ 114316316114712510510712 ],
      844 := [ 1143163161149611811896 ],
      845 := [ 1143163161141189696118 ],
      846 := [ 114316316114132154154132 ],
      847 := [ 114316316114154132132154 ],
      848 := [ 114316510712114316510712 ],
      849 := [ 114316510712316114712510 ],
      850 := [ 114316510712510712114316 ],
      851 := [ 114316510712712510316114 ],
      852 := [ 11431651071296118132154 ],
      853 := [ 11431651071211896154132 ],
      854 := [ 11431651071213215496118 ],
      855 := [ 11431651071215413211896 ],
      856 := [ 114316712510114316712510 ],
      857 := [ 114316712510316114510712 ],
      858 := [ 114316712510510712316114 ],
      859 := [ 114316712510712510114316 ],
      860 := [ 11431671251096118154132 ],
      861 := [ 11431671251011896132154 ],
      862 := [ 11431671251013215411896 ],
      863 := [ 11431671251015413296118 ],
      864 := [ 1143169611811431696118 ],
      865 := [ 1143169611831611411896 ],
      866 := [ 11431696118510712132154 ],
      867 := [ 11431696118712510154132 ],
      868 := [ 1143169611896118114316 ],
      869 := [ 1143169611811896316114 ],
      870 := [ 11431696118132154510712 ],
      871 := [ 11431696118154132712510 ],
      872 := [ 1143161189611431611896 ],
      873 := [ 1143161189631611496118 ],
      874 := [ 11431611896510712154132 ],
      875 := [ 11431611896712510132154 ],
      876 := [ 1143161189696118316114 ],
      877 := [ 1143161189611896114316 ],
      878 := [ 11431611896132154712510 ],
      879 := [ 11431611896154132510712 ],
      880 := [ 114316132154114316132154 ],
      881 := [ 114316132154316114154132 ],
      882 := [ 11431613215451071296118 ],
      883 := [ 11431613215471251011896 ],
      884 := [ 11431613215496118510712 ],
      885 := [ 11431613215411896712510 ],
      886 := [ 114316132154132154114316 ],
      887 := [ 114316132154154132316114 ],
      888 := [ 114316154132114316154132 ],
      889 := [ 114316154132316114132154 ],
      890 := [ 11431615413251071211896 ],
      891 := [ 11431615413271251096118 ],
      892 := [ 11431615413296118712510 ],
      893 := [ 11431615413211896510712 ],
      894 := [ 114316154132132154316114 ],
      895 := [ 114316154132154132114316 ],
      896 := [ 115115115115115115115115 ],
      897 := [ 115115115115313313313313 ],
      898 := [ 115115115115511511511511 ],
      899 := [ 11511511511579797979 ],
      900 := [ 11511511511597979797 ],
      901 := [ 115115115115115115115115 ],
      902 := [ 115115115115133133133133 ],
      903 := [ 115115115115151151151151 ],
      904 := [ 115115313313115115313313 ],
      905 := [ 115115313313313313115115 ],
      906 := [ 1151153133135115117979 ],
      907 := [ 1151153133137979511511 ],
      908 := [ 1151153133139797115115 ],
      909 := [ 1151153133131151159797 ],
      910 := [ 115115313313133133151151 ],
      911 := [ 115115313313151151133133 ],
      912 := [ 115115511511115115511511 ],
      913 := [ 1151155115113133137979 ],
      914 := [ 115115511511511511115115 ],
      915 := [ 1151155115117979313313 ],
      916 := [ 1151155115119797133133 ],
      917 := [ 115115511511115115151151 ],
      918 := [ 1151155115111331339797 ],
      919 := [ 115115511511151151115115 ],
      920 := [ 11511579791151157979 ],
      921 := [ 1151157979313313511511 ],
      922 := [ 1151157979511511313313 ],
      923 := [ 11511579797979115115 ],
      924 := [ 11511579799797151151 ],
      925 := [ 1151157979115115133133 ],
      926 := [ 1151157979133133115115 ],
      927 := [ 11511579791511519797 ],
      928 := [ 11511597971151159797 ],
      929 := [ 1151159797313313115115 ],
      930 := [ 1151159797511511133133 ],
      931 := [ 11511597977979151151 ],
      932 := [ 11511597979797115115 ],
      933 := [ 1151159797115115313313 ],
      934 := [ 1151159797133133511511 ],
      935 := [ 11511597971511517979 ],
      936 := [ 115115115115115115115115 ],
      937 := [ 1151151151153133139797 ],
      938 := [ 115115115115511511151151 ],
      939 := [ 1151151151157979133133 ],
      940 := [ 1151151151159797313313 ],
      941 := [ 115115115115115115115115 ],
      942 := [ 1151151151151331337979 ],
      943 := [ 115115115115151151511511 ],
      944 := [ 115115133133115115133133 ],
      945 := [ 115115133133313313151151 ],
      946 := [ 1151151331335115119797 ],
      947 := [ 1151151331337979115115 ],
      948 := [ 1151151331339797511511 ],
      949 := [ 1151151331331151157979 ],
      950 := [ 115115133133133133115115 ],
      951 := [ 115115133133151151313313 ],
      952 := [ 115115151151115115151151 ],
      953 := [ 115115151151313313133133 ],
      954 := [ 115115151151511511115115 ],
      955 := [ 11511515115179799797 ],
      956 := [ 11511515115197977979 ],
      957 := [ 115115151151115115511511 ],
      958 := [ 115115151151133133313313 ],
      959 := [ 115115151151151151115115 ],
      960 := [ 116314116314116314116314 ],
      961 := [ 116314116314314116314116 ],
      962 := [ 116314116314512710512710 ],
      963 := [ 116314116314710512710512 ],
      964 := [ 1163141163149811698116 ],
      965 := [ 1163141163141169811698 ],
      966 := [ 116314116314134152134152 ],
      967 := [ 116314116314152134152134 ],
      968 := [ 116314314116116314314116 ],
      969 := [ 116314314116314116116314 ],
      970 := [ 116314314116512710710512 ],
      971 := [ 116314314116710512512710 ],
      972 := [ 1163143141169811611698 ],
      973 := [ 1163143141161169898116 ],
      974 := [ 116314314116134152152134 ],
      975 := [ 116314314116152134134152 ],
      976 := [ 116314512710116314512710 ],
      977 := [ 116314512710314116710512 ],
      978 := [ 116314512710512710116314 ],
      979 := [ 116314512710710512314116 ],
      980 := [ 11631451271098116134152 ],
      981 := [ 11631451271011698152134 ],
      982 := [ 11631451271013415298116 ],
      983 := [ 11631451271015213411698 ],
      984 := [ 116314710512116314710512 ],
      985 := [ 116314710512314116512710 ],
      986 := [ 116314710512512710314116 ],
      987 := [ 116314710512710512116314 ],
      988 := [ 11631471051298116152134 ],
      989 := [ 11631471051211698134152 ],
      990 := [ 11631471051213415211698 ],
      991 := [ 11631471051215213498116 ],
      992 := [ 1163149811611631498116 ],
      993 := [ 1163149811631411611698 ],
      994 := [ 11631498116512710134152 ],
      995 := [ 11631498116710512152134 ],
      996 := [ 1163149811698116116314 ],
      997 := [ 1163149811611698314116 ],
      998 := [ 11631498116134152512710 ],
      999 := [ 11631498116152134710512 ],
      1000 := [ 1163141169811631411698 ],
      1001 := [ 1163141169831411698116 ],
      1002 := [ 11631411698512710152134 ],
      1003 := [ 11631411698710512134152 ],
      1004 := [ 1163141169898116314116 ],
      1005 := [ 1163141169811698116314 ],
      1006 := [ 11631411698134152710512 ],
      1007 := [ 11631411698152134512710 ],
      1008 := [ 116314134152116314134152 ],
      1009 := [ 116314134152314116152134 ],
      1010 := [ 11631413415251271098116 ],
      1011 := [ 11631413415271051211698 ],
      1012 := [ 11631413415298116512710 ],
      1013 := [ 11631413415211698710512 ],
      1014 := [ 116314134152134152116314 ],
      1015 := [ 116314134152152134314116 ],
      1016 := [ 116314152134116314152134 ],
      1017 := [ 116314152134314116134152 ],
      1018 := [ 11631415213451271011698 ],
      1019 := [ 11631415213471051298116 ],
      1020 := [ 11631415213498116710512 ],
      1021 := [ 11631415213411698512710 ],
      1022 := [ 116314152134134152314116 ],
      1023 := [ 116314152134152134116314 ],
      1024 := [ 12345678910111213141516 ] ),
  classes := rec(
      1 := rec(
          phi := [ 16526636746856967071024885 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125340341
              342343348349350351354355358359362363366367
              370371372373378379380381596597598599604605
              606607610611614615618619622623626627628629
              634635636637852853854855860861862863866867
              870871874875878879882883884885890891892893
              1024 ] ),
      2 := rec(
          phi := [ 1652663674685696702110242285 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125340341
              342343348349350351354355358359362363366367
              370371372373378379380381596597598599604605
              606607610611614615618619622623626627628629
              634635636637852853854855860861862863866867
              870871874875878879882883884885890891892893
              1024 ] ),
      3 := rec(
          phi := [ 16526636746858668771024885 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125340341
              342343348349350351354355358359362363366367
              370371372373378379380381596597598599604605
              606607610611614615618619622623626627628629
              634635636637852853854855860861862863866867
              870871874875878879882883884885890891892893
              1024 ] ),
      4 := rec(
          phi := [ 165266367468211024228523862487 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125340341
              342343348349350351354355358359362363366367
              370371372373378379380381596597598599604605
              606607610611614615618619622623626627628629
              634635636637852853854855860861862863866867
              870871874875878879882883884885890891892893
              1024 ] ),
      5 := rec(
          phi := [ 16526638148256967071024885 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125340341
              342343348349350351354355358359362363366367
              370371372373378379380381596597598599604605
              606607610611614615618619622623626627628629
              634635636637852853854855860861862863866867
              870871874875878879882883884885890891892893
              1024 ] ),
      6 := rec(
          phi := [ 1652663320432156967071024885 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125340341
              342343348349350351354355358359362363366367
              370371372373378379380381596597598599604605
              606607610611614615618619622623626627628629
              634635636637852853854855860861862863866867
              870871874875878879882883884885890891892893
              1024 ] ),
      7 := rec(
          phi := [ 1652663320432158668771024885 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125354355
              358359362363366367370371372373378379380381
              5965975985996046056066071024 ] ),
      8 := rec(
          phi := [ 165266332043215866341710248343 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125354355
              358359362363366367370371372373378379380381
              5965975985996046056066071024 ] ),
      9 := rec(
          phi := [ 165266332043215340687710248343 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125354355
              358359362363366367370371372373378379380381
              5965975985996046056066071024 ] ),
      10 := rec(
          phi := [ 165266332043215340634171024885 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125354355
              358359362363366367370371372373378379380381
              5965975985996046056066071024 ] ),
      11 := rec(
          phi := [ 165266178118825696702110242285 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125340341
              342343348349350351354355358359362363366367
              370371372373378379380381596597598599604605
              606607610611614615618619622623626627628629
              634635636637852853854855860861862863866867
              870871874875878879882883884885890891892893
              1024 ] ),
      12 := rec(
          phi := [ 1652662568125782569670260102426185 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125340341
              342343348349350351354355358359362363366367
              370371372373378379380381596597598599604605
              606607610611614615618619622623626627628629
              634635636637852853854855860861862863866867
              870871874875878879882883884885890891892893
              1024 ] ),
      13 := rec(
          phi := [ 165266256320432156967071024885 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125340341
              342343348349350351354355358359362363366367
              370371372373378379380381596597598599604605
              606607610611614615618619622623626627628629
              634635636637852853854855860861862863866867
              870871874875878879882883884885890891892893
              1024 ] ),
      14 := rec(
          phi := [ 1652662563204321569670260102426185 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125340341
              342343348349350351354355358359362363366367
              370371372373378379380381596597598599604605
              606607610611614615618619622623626627628629
              634635636637852853854855860861862863866867
              870871874875878879882883884885890891892893
              1024 ] ),
      15 := rec(
          phi := [ 165266256320432158668771024885 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125354355
              358359362363366367370371372373378379380381
              5965975985996046056066071024 ] ),
      16 := rec(
          phi := [ 16526625632043215866341710248343 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125354355
              358359362363366367370371372373378379380381
              5965975985996046056066071024 ] ),
      17 := rec(
          phi := [ 16526625632043215340687710248343 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125354355
              358359362363366367370371372373378379380381
              5965975985996046056066071024 ] ),
      18 := rec(
          phi := [ 16526625632043215340634171024885 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125354355
              358359362363366367370371372373378379380381
              5965975985996046056066071024 ] ),
      19 := rec(
          phi := [ 165266256320432153406341260102426185 ]
           ,
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125340341
              342343348349350351354355358359362363366367
              370371372373378379380381596597598599604605
              606607610611614615618619622623626627628629
              634635636637852853854855860861862863866867
              870871874875878879882883884885890891892893
              1024 ] ),
      20 := rec(
          phi := [ 165266256320432153402638726010248343 ]
           ,
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253354355358359362363
              366367370371372373378379380381482483486487
              490491494495498499500501506507508509596597
              598599604605606607724725726727732733734735
              1024 ] ),
      21 := rec(
          phi := [ 16526625632025732156967071024885 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125340341
              342343348349350351354355358359362363366367
              370371372373378379380381596597598599604605
              606607610611614615618619622623626627628629
              634635636637852853854855860861862863866867
              870871874875878879882883884885890891892893
              1024 ] ),
      22 := rec(
          phi := [ 1652662563202573215696702110242285 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125340341
              342343348349350351354355358359362363366367
              370371372373378379380381596597598599604605
              606607610611614615618619622623626627628629
              634635636637852853854855860861862863866867
              870871874875878879882883884885890891892893
              1024 ] ),
      23 := rec(
          phi := [ 165266256320257321569670260102426185 ]
           ,
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125340341
              342343348349350351354355358359362363366367
              370371372373378379380381596597598599604605
              606607610611614615618619622623626627628629
              634635636637852853854855860861862863866867
              870871874875878879882883884885890891892893
              1024 ] ),
      24 := rec(
          phi := [ 16526625632025732158668771024885 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125354355
              358359362363366367370371372373378379380381
              5965975985996046056066071024 ] ),
      25 := rec(
          phi := [ 1652662563202573215866341710248343 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125354355
              358359362363366367370371372373378379380381
              5965975985996046056066071024 ] ),
      26 := rec(
          phi := [ 1652662563202573215340687710248343 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125354355
              358359362363366367370371372373378379380381
              5965975985996046056066071024 ] ),
      27 := rec(
          phi := [ 1652662563202573215340634171024885 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125354355
              358359362363366367370371372373378379380381
              5965975985996046056066071024 ] ),
      28 := rec(
          phi := [ 165266256320257321534063412601024261
              85 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125340341
              342343348349350351354355358359362363366367
              370371372373378379380381596597598599604605
              606607610611614615618619622623626627628629
              634635636637852853854855860861862863866867
              870871874875878879882883884885890891892893
              1024 ] ),
      29 := rec(
          phi := [ 16526625632025732153402638726010248
              343 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253354355358359362363
              366367370371372373378379380381482483486487
              490491494495498499500501506507508509596597
              598599604605606607724725726727732733734735
              1024 ] ),
      30 := rec(
          phi := [ 165266256320257321211024228523862487 ]
           ,
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125340341
              342343348349350351354355358359362363366367
              370371372373378379380381596597598599604605
              606607610611614615618619622623626627628629
              634635636637852853854855860861862863866867
              870871874875878879882883884885890891892893
              1024 ] ),
      31 := rec(
          phi := [ 1652662563202573212110242285276340277
              341 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125354355
              358359362363366367370371372373378379380381
              5965975985996046056066071024 ] ),
      32 := rec(
          phi := [ 16527338148856967771024892 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125340341
              342343348349350351354355358359362363366367
              370371372373378379380381596597598599604605
              606607610611614615618619622623626627628629
              634635636637852853854855860861862863866867
              870871874875878879882883884885890891892893
              1024 ] ),
      33 := rec(
          phi := [ 165219236741945696196710248212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      34 := rec(
          phi := [ 16521923674194569619621102422212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      35 := rec(
          phi := [ 165219236741945866214710248212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      36 := rec(
          phi := [ 1652192367419421102422212238624214 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      37 := rec(
          phi := [ 165219238142085696196710248212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      38 := rec(
          phi := [ 1652192332044485696196710248212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      39 := rec(
          phi := [ 1652192332044485866214710248212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253354355358359362363
              366367370371372373378379380381482483486487
              490491494495498499500501506507508509596597
              598599604605606607724725726727732733734735
              1024 ] ),
      40 := rec(
          phi := [ 1652192332044485866468710248470 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253354355358359362363
              366367370371372373378379380381482483486487
              490491494495498499500501506507508509596597
              598599604605606607724725726727732733734735
              1024 ] ),
      41 := rec(
          phi := [ 16521923320444853406214710248470 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253354355358359362363
              366367370371372373378379380381482483486487
              490491494495498499500501506507508509596597
              598599604605606607724725726727732733734735
              1024 ] ),
      42 := rec(
          phi := [ 16521923320444853406468710248212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253354355358359362363
              366367370371372373378379380381482483486487
              490491494495498499500501506507508509596597
              598599604605606607724725726727732733734735
              1024 ] ),
      43 := rec(
          phi := [ 1652192178118208569619621102422212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      44 := rec(
          phi := [ 1652192256814208569619626010248212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      45 := rec(
          phi := [ 16521922568125720856961962601024261
              212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      46 := rec(
          phi := [ 165219225632044485696196710248212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      47 := rec(
          phi := [ 16521922563204448569619671024261212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      48 := rec(
          phi := [ 16521922563204448569619626010248212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      49 := rec(
          phi := [ 1652192256320444856961962601024261212 
             ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      50 := rec(
          phi := [ 165219225632044485866214710248212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253354355358359362363
              366367370371372373378379380381482483486487
              490491494495498499500501506507508509596597
              598599604605606607724725726727732733734735
              1024 ] ),
      51 := rec(
          phi := [ 165219225632044485866468710248470 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253354355358359362363
              366367370371372373378379380381482483486487
              490491494495498499500501506507508509596597
              598599604605606607724725726727732733734735
              1024 ] ),
      52 := rec(
          phi := [ 1652192256320444853406214710248470 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253354355358359362363
              366367370371372373378379380381482483486487
              490491494495498499500501506507508509596597
              598599604605606607724725726727732733734735
              1024 ] ),
      53 := rec(
          phi := [ 1652192256320444853406468710248212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253354355358359362363
              366367370371372373378379380381482483486487
              490491494495498499500501506507508509596597
              598599604605606607724725726727732733734735
              1024 ] ),
      54 := rec(
          phi := [ 165219225632044485340646871024261212 ]
           ,
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      55 := rec(
          phi := [ 165219225632044485340646826010248212 ]
           ,
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      56 := rec(
          phi := [ 16521922563204448534064682601024261
              212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      57 := rec(
          phi := [ 16521922563204448534026346826010248
              212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      58 := rec(
          phi := [ 16521922563202574485696196710248212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      59 := rec(
          phi := [ 1652192256320257448569619671024261212 
             ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      60 := rec(
          phi := [ 1652192256320257448569619621102422212 
             ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      61 := rec(
          phi := [ 1652192256320257448569619626010248212 
             ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      62 := rec(
          phi := [ 165219225632025744856961962601024261
              212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      63 := rec(
          phi := [ 16521922563202574485866214710248212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253354355358359362363
              366367370371372373378379380381482483486487
              490491494495498499500501506507508509596597
              598599604605606607724725726727732733734735
              1024 ] ),
      64 := rec(
          phi := [ 16521922563202574485866468710248470 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253354355358359362363
              366367370371372373378379380381482483486487
              490491494495498499500501506507508509596597
              598599604605606607724725726727732733734735
              1024 ] ),
      65 := rec(
          phi := [ 165219225632025744853406214710248470 ]
           ,
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253354355358359362363
              366367370371372373378379380381482483486487
              490491494495498499500501506507508509596597
              598599604605606607724725726727732733734735
              1024 ] ),
      66 := rec(
          phi := [ 165219225632025744853406468710248212 ]
           ,
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253354355358359362363
              366367370371372373378379380381482483486487
              490491494495498499500501506507508509596597
              598599604605606607724725726727732733734735
              1024 ] ),
      67 := rec(
          phi := [ 16521922563202574485340646871024261
              212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      68 := rec(
          phi := [ 16521922563202574485340646826010248
              212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      69 := rec(
          phi := [ 1652192256320257448534064682601024261
              212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      70 := rec(
          phi := [ 1652192256320257448534026346826010248
              212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      71 := rec(
          phi := [ 165219225632025744821102422212238624
              214 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      72 := rec(
          phi := [ 165219225632025744821102422212276340
              277468 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253354355358359362363
              366367370371372373378379380381482483486487
              490491494495498499500501506507508509596597
              598599604605606607724725726727732733734735
              1024 ] ),
      73 := rec(
          phi := [ 1651286617811448251269640705281024656
              85 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125340341
              342343348349350351354355358359362363366367
              370371372373378379380381596597598599604605
              606607610611614615618619622623626627628629
              634635636637852853854855860861862863866867
              870871874875878879882883884885890891892893
              1024 ] ),
      74 := rec(
          phi := [ 16512866256673846851269640705141024642
              85 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125340341
              342343348349350351354355358359362363366367
              370371372373378379380381596597598599604605
              606607610611614615618619622623626627628629
              634635636637852853854855860861862863866867
              870871874875878879882883884885890891892893
              1024 ] ),
      75 := rec(
          phi := [ 16512866256673846851269640707681024896
              85 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125340341
              342343348349350351354355358359362363366367
              370371372373378379380381596597598599604605
              606607610611614615618619622623626627628629
              634635636637852853854855860861862863866867
              870871874875878879882883884885890891892893
              1024 ] ),
      76 := rec(
          phi := [ 16512866256673846851286640877681024896
              85 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125340341
              342343348349350351354355358359362363366367
              370371372373378379380381596597598599604605
              606607610611614615618619622623626627628629
              634635636637852853854855860861862863866867
              870871874875878879882883884885890891892893
              1024 ] ),
      77 := rec(
          phi := [ 16512866256813848251269640707681024896
              85 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125340341
              342343348349350351354355358359362363366367
              370371372373378379380381596597598599604605
              606607610611614615618619622623626627628629
              634635636637852853854855860861862863866867
              870871874875878879882883884885890891892893
              1024 ] ),
      78 := rec(
          phi := [ 1651286625632013032151269640705141024
              64285 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125340341
              342343348349350351354355358359362363366367
              370371372373378379380381596597598599604605
              606607610611614615618619622623626627628629
              634635636637852853854855860861862863866867
              870871874875878879882883884885890891892893
              1024 ] ),
      79 := rec(
          phi := [ 1651286625632013032151269640707681024
              89685 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125340341
              342343348349350351354355358359362363366367
              370371372373378379380381596597598599604605
              606607610611614615618619622623626627628629
              634635636637852853854855860861862863866867
              870871874875878879882883884885890891892893
              1024 ] ),
      80 := rec(
          phi := [ 1651286625632013032151286640877681024
              89685 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125354355
              358359362363366367370371372373378379380381
              5965975985996046056066071024 ] ),
      81 := rec(
          phi := [ 16512866256320130321512866403417681024
              896343 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125354355
              358359362363366367370371372373378379380381
              5965975985996046056066071024 ] ),
      82 := rec(
          phi := [ 16512866256320130321512340640877681024
              896343 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125354355
              358359362363366367370371372373378379380381
              5965975985996046056066071024 ] ),
      83 := rec(
          phi := [ 165128662563201303215123406403415141024
              64285 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125340341
              342343348349350351354355358359362363366367
              370371372373378379380381596597598599604605
              606607610611614615618619622623626627628629
              634635636637852853854855860861862863866867
              870871874875878879882883884885890891892893
              1024 ] ),
      84 := rec(
          phi := [ 165128662563201303215123406403417681024
              89685 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125354355
              358359362363366367370371372373378379380381
              5965975985996046056066071024 ] ),
      85 := rec(
          phi := [ 16512866256320130321512340898875141024
              896343 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253354355358359362363
              366367370371372373378379380381482483486487
              490491494495498499500501506507508509596597
              598599604605606607724725726727732733734735
              1024 ] ),
      86 := rec(
          phi := [ 1651286625632038432151269640705141024
              64285 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125340341
              342343348349350351354355358359362363366367
              370371372373378379380381596597598599604605
              606607610611614615618619622623626627628629
              634635636637852853854855860861862863866867
              870871874875878879882883884885890891892893
              1024 ] ),
      87 := rec(
          phi := [ 1651286625632038432151269640707681024
              89685 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125340341
              342343348349350351354355358359362363366367
              370371372373378379380381596597598599604605
              606607610611614615618619622623626627628629
              634635636637852853854855860861862863866867
              870871874875878879882883884885890891892893
              1024 ] ),
      88 := rec(
          phi := [ 1651286625632038432151286640877681024
              89685 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125354355
              358359362363366367370371372373378379380381
              5965975985996046056066071024 ] ),
      89 := rec(
          phi := [ 16512866256320384321512866403417681024
              896343 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125354355
              358359362363366367370371372373378379380381
              5965975985996046056066071024 ] ),
      90 := rec(
          phi := [ 16512866256320384321512340640877681024
              896343 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125354355
              358359362363366367370371372373378379380381
              5965975985996046056066071024 ] ),
      91 := rec(
          phi := [ 165128662563203843215123406403415141024
              64285 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125340341
              342343348349350351354355358359362363366367
              370371372373378379380381596597598599604605
              606607610611614615618619622623626627628629
              634635636637852853854855860861862863866867
              870871874875878879882883884885890891892893
              1024 ] ),
      92 := rec(
          phi := [ 165128662563203843215123406403417681024
              89685 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125354355
              358359362363366367370371372373378379380381
              5965975985996046056066071024 ] ),
      93 := rec(
          phi := [ 16512866256320384321512340898875141024
              896343 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253354355358359362363
              366367370371372373378379380381482483486487
              490491494495498499500501506507508509596597
              598599604605606607724725726727732733734735
              1024 ] ),
      94 := rec(
          phi := [ 16512819236713019456913219671024134
              212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      95 := rec(
          phi := [ 165128192367130194569132196211024148
              212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      96 := rec(
          phi := [ 16512819236713019458613221471024134
              212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      97 := rec(
          phi := [ 1651281923671301942110241482122386150
              214 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      98 := rec(
          phi := [ 16512819238113020856913219671024134
              212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      99 := rec(
          phi := [ 16512819238138420856913219671024388
              212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      100 := rec(
          phi := [ 165128192332013044856913219671024134
              212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      101 := rec(
          phi := [ 165128192332013044858613221471024134
              212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253354355358359362363
              366367370371372373378379380381482483486487
              490491494495498499500501506507508509596597
              598599604605606607724725726727732733734735
              1024 ] ),
      102 := rec(
          phi := [ 165128192332013044858613246871024134
              470 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253354355358359362363
              366367370371372373378379380381482483486487
              490491494495498499500501506507508509596597
              598599604605606607724725726727732733734735
              1024 ] ),
      103 := rec(
          phi := [ 1651281923320130448534013221471024134
              470 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253354355358359362363
              366367370371372373378379380381482483486487
              490491494495498499500501506507508509596597
              598599604605606607724725726727732733734735
              1024 ] ),
      104 := rec(
          phi := [ 1651281923320130448534013246871024134
              212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253354355358359362363
              366367370371372373378379380381482483486487
              490491494495498499500501506507508509596597
              598599604605606607724725726727732733734735
              1024 ] ),
      105 := rec(
          phi := [ 165128192332038444856913219671024134
              212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      106 := rec(
          phi := [ 165128192332038444856913219671024388
              212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      107 := rec(
          phi := [ 165128192332038444858613221471024134
              212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253354355358359362363
              366367370371372373378379380381482483486487
              490491494495498499500501506507508509596597
              598599604605606607724725726727732733734735
              1024 ] ),
      108 := rec(
          phi := [ 165128192332038444858613246871024134
              470 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253354355358359362363
              366367370371372373378379380381482483486487
              490491494495498499500501506507508509596597
              598599604605606607724725726727732733734735
              1024 ] ),
      109 := rec(
          phi := [ 165128192332038444858639021471024388
              212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253354355358359362363
              366367370371372373378379380381482483486487
              490491494495498499500501506507508509596597
              598599604605606607724725726727732733734735
              1024 ] ),
      110 := rec(
          phi := [ 165128192332038444858639046871024388
              470 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253354355358359362363
              366367370371372373378379380381482483486487
              490491494495498499500501506507508509596597
              598599604605606607724725726727732733734735
              1024 ] ),
      111 := rec(
          phi := [ 1651281923320384448534013221471024134
              470 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253354355358359362363
              366367370371372373378379380381482483486487
              490491494495498499500501506507508509596597
              598599604605606607724725726727732733734735
              1024 ] ),
      112 := rec(
          phi := [ 1651281923320384448534013246871024134
              212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253354355358359362363
              366367370371372373378379380381482483486487
              490491494495498499500501506507508509596597
              598599604605606607724725726727732733734735
              1024 ] ),
      113 := rec(
          phi := [ 1651281923320384448534013246871024388
              212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      114 := rec(
          phi := [ 1651281923320384448534039021471024388
              470 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253354355358359362363
              366367370371372373378379380381482483486487
              490491494495498499500501506507508509596597
              598599604605606607724725726727732733734735
              1024 ] ),
      115 := rec(
          phi := [ 1651281923320384448534039046871024388
              212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253354355358359362363
              366367370371372373378379380381482483486487
              490491494495498499500501506507508509596597
              598599604605606607724725726727732733734735
              1024 ] ),
      116 := rec(
          phi := [ 1651281921781144208569132196211024148
              212 ],
          autos_yielding_iso_nrs := [ 85868792939495102103110111
              212213214215220221222223230231238239340341
              342343348349350351358359366367468469470471
              476477478479486487494495596597598599604605
              606607614615622623724725726727732733734735
              742743750751852853854855860861862863870871
              87887998098198298398898999099199899910061007
              1024 ] ),
      117 := rec(
          phi := [ 1651281921781144208512696401965281024
              656212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      118 := rec(
          phi := [ 1651281921781144208512576640704211024
              148212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      119 := rec(
          phi := [ 1651281921781144208512576640704491024
              176212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      120 := rec(
          phi := [ 1651281921781144208512576640704491024
              656212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      121 := rec(
          phi := [ 16512819217811442085125766407045281024
              656212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      122 := rec(
          phi := [ 16512819217116144244512576640704491024
              176212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351358359366367372373380381468469470471
              476477478479486487494495500501508509610611
              618619626627634635738739746747754755762763
              1024 ] ),
      123 := rec(
          phi := [ 16512819217116144724512576640704491024
              176756 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351358359366367372373380381468469470471
              476477478479486487494495500501508509610611
              618619626627634635738739746747754755762763
              1024 ] ),
      124 := rec(
          phi := [ 16512819217116688244512576640704491024
              656212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351358359366367372373380381468469470471
              476477478479486487494495500501508509610611
              618619626627634635738739746747754755762763
              1024 ] ),
      125 := rec(
          phi := [ 16512819217116688724512576640704491024
              656756 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351358359366367372373380381468469470471
              476477478479486487494495500501508509610611
              618619626627634635738739746747754755762763
              1024 ] ),
      126 := rec(
          phi := [ 16512819217596144244512576640704491024
              176756 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351358359366367372373380381468469470471
              476477478479486487494495500501508509610611
              618619626627634635738739746747754755762763
              1024 ] ),
      127 := rec(
          phi := [ 16512819217596144724512576640704491024
              176212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351358359366367372373380381468469470471
              476477478479486487494495500501508509610611
              618619626627634635738739746747754755762763
              1024 ] ),
      128 := rec(
          phi := [ 16512819217596144724512576640704491024
              656212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      129 := rec(
          phi := [ 165128192175961447245125766407045281024
              656212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      130 := rec(
          phi := [ 16512819217596688244512576640704491024
              656756 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351358359366367372373380381468469470471
              476477478479486487494495500501508509610611
              618619626627634635738739746747754755762763
              1024 ] ),
      131 := rec(
          phi := [ 16512819217596688724512576640704491024
              656212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351358359366367372373380381468469470471
              476477478479486487494495500501508509610611
              618619626627634635738739746747754755762763
              1024 ] ),
      132 := rec(
          phi := [ 1651281922110241482123598162226768832
              896960 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      133 := rec(
          phi := [ 1651281922110241482123910216623051114
              178242 ],
          autos_yielding_iso_nrs := 
           [ 8592939899106107114115122123212213220221
              226227234235242243250251340341348349354355
              362363370371378379468469476477482483490491
              498499506507596597604605610611618619626627
              634635724725732733738739746747754755762763
              852853860861866867874875882883890891980981
              9889899949951002100310101011101810191024 ] ),
      134 := rec(
          phi := [ 165128192211024148212512576640704532596
              660724 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351358359366367372373380381468469470471
              476477478479486487494495500501508509610611
              618619626627634635738739746747754755762763
              1024 ] ),
      135 := rec(
          phi := [ 165128192211024148212512576640704768832
              896960 ],
          autos_yielding_iso_nrs := 
           [ 8592939899106107114115122123212213220221
              226227234235242243250251340341348349354355
              362363370371378379468469476477482483490491
              498499506507596597604605610611618619626627
              634635724725732733738739746747754755762763
              852853860861866867874875882883890891980981
              9889899949951002100310101011101810191024 ] ),
      136 := rec(
          phi := [ 16512819225667384194512696401965141024
              642212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      137 := rec(
          phi := [ 16512819225667384194512696401965141024
              896212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      138 := rec(
          phi := [ 16512819225667384194512696401967681024
              642212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      139 := rec(
          phi := [ 16512819225667384194512696401967681024
              896212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      140 := rec(
          phi := [ 16512819225667384194512866402147681024
              896212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      141 := rec(
          phi := [ 16512819225681130208512696401967681024
              642212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      142 := rec(
          phi := [ 16512819225681384194512696402247681024
              896226 ],
          autos_yielding_iso_nrs := [ 85868792939495102103110111
              212213214215220221222223230231238239340341
              342343348349350351358359366367468469470471
              476477478479486487494495596597598599604605
              606607614615622623724725726727732733734735
              742743750751852853854855860861862863870871
              87887998098198298398898999099199899910061007
              1024 ] ),
      143 := rec(
          phi := [ 16512819225681384208512696401967681024
              896212 ],
          autos_yielding_iso_nrs := [ 85868792939495102103110111
              212213214215220221222223230231238239340341
              342343348349350351358359366367468469470471
              476477478479486487494495596597598599604605
              606607614615622623724725726727732733734735
              742743750751852853854855860861862863870871
              87887998098198298398898999099199899910061007
              1024 ] ),
      144 := rec(
          phi := [ 165128192256813842085125761607042881024
              416212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      145 := rec(
          phi := [ 165128192256813842085125761607042881024
              896212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      146 := rec(
          phi := [ 165128192256813842085125761607047681024
              416212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      147 := rec(
          phi := [ 165128192256813842085125761607047681024
              896212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      148 := rec(
          phi := [ 165128192256813842085125766407042881024
              416212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      149 := rec(
          phi := [ 165128192256813842085125766407042881024
              896212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      150 := rec(
          phi := [ 165128192256813842085125766407047681024
              416212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      151 := rec(
          phi := [ 165128192256813842085125766407047681024
              896212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      152 := rec(
          phi := [ 165128192256983842265121024640212768832
              182960 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355362363370371378379468469470471
              476477478479482483490491498499506507614615
              622623628629636637742743750751756757764765
              1024 ] ),
      153 := rec(
          phi := [ 165128192256983842265121024640212768832
              896960 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355362363370371378379468469470471
              476477478479482483490491498499506507614615
              622623628629636637742743750751756757764765
              1024 ] ),
      154 := rec(
          phi := [ 165128192256983849805121024640994768832
              182960 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355362363370371378379468469470471
              476477478479482483490491498499506507614615
              622623628629636637742743750751756757764765
              1024 ] ),
      155 := rec(
          phi := [ 165128192256983849805121024640994768832
              896960 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355362363370371378379468469470471
              476477478479482483490491498499506507614615
              622623628629636637742743750751756757764765
              1024 ] ),
      156 := rec(
          phi := [ 1651281922561023842305121146402427681024
              896212 ],
          autos_yielding_iso_nrs := [ 85868792939495102103110111
              212213214215220221222223230231238239340341
              342343348349350351358359366367468469470471
              476477478479486487494495596597598599604605
              606607614615622623724725726727732733734735
              742743750751852853854855860861862863870871
              87887998098198298398898999099199899910061007
              1024 ] ),
      157 := rec(
          phi := [ 1651281922561023842445121146402147681024
              896226 ],
          autos_yielding_iso_nrs := [ 85868792939495102103110111
              212213214215220221222223230231238239340341
              342343348349350351358359366367468469470471
              476477478479486487494495596597598599604605
              606607614615622623724725726727732733734735
              742743750751852853854855860861862863870871
              87887998098198298398898999099199899910061007
              1024 ] ),
      158 := rec(
          phi := [ 1651281922563201304485123406402147681024
              896470 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253354355358359362363
              366367370371372373378379380381482483486487
              490491494495498499500501506507508509596597
              598599604605606607724725726727732733734735
              1024 ] ),
      159 := rec(
          phi := [ 1651281922563201304485123406404685141024
              642212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      160 := rec(
          phi := [ 1651281922563201304485123406404685141024
              896212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      161 := rec(
          phi := [ 1651281922563201304485123406404687681024
              642212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      162 := rec(
          phi := [ 1651281922563201304485123406404687681024
              896212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253354355358359362363
              366367370371372373378379380381482483486487
              490491494495498499500501506507508509596597
              598599604605606607724725726727732733734735
              1024 ] ),
      163 := rec(
          phi := [ 1651281922563201304485123408984685141024
              896212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      164 := rec(
          phi := [ 1651281922563203844485123406402147681024
              896470 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253354355358359362363
              366367370371372373378379380381482483486487
              490491494495498499500501506507508509596597
              598599604605606607724725726727732733734735
              1024 ] ),
      165 := rec(
          phi := [ 1651281922563203844485123406404685141024
              642212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      166 := rec(
          phi := [ 1651281922563203844485123406404685141024
              896212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      167 := rec(
          phi := [ 1651281922563203844485123406404687681024
              642212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      168 := rec(
          phi := [ 1651281922563203844485123406404687681024
              896212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253354355358359362363
              366367370371372373378379380381482483486487
              490491494495498499500501506507508509596597
              598599604605606607724725726727732733734735
              1024 ] ),
      169 := rec(
          phi := [ 1651281922563203844485123408984685141024
              896212 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      170 := rec(
          phi := [ 1651281922563203844485125766407047681024
              896212 ],
          autos_yielding_iso_nrs := [ 85868792939495102103110111
              212213214215220221222223230231238239358359
              3663674864874944951024 ] ),
      171 := rec(
          phi := [ 1651281922563203844485125766407047681024
              896226 ],
          autos_yielding_iso_nrs := [ 85868792939495102103110111
              212213214215220221222223230231238239340341
              342343348349350351358359366367468469470471
              476477478479486487494495596597598599604605
              606607614615622623724725726727732733734735
              742743750751852853854855860861862863870871
              87887998098198298398898999099199899910061007
              1024 ] ),
      172 := rec(
          phi := [ 169977171024259233100411084911657124 ]
           ,
          autos_yielding_iso_nrs := [ 86929498102106110114116122
              1243403423483503583663723806106186266341024 ] )
       ,
      173 := rec(
          phi := [ 169977171024259233580415884959657604 ]
           ,
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125340341
              342343348349350351354355358359362363366367
              370371372373378379380381596597598599604605
              606607610611614615618619622623626627628629
              634635636637852853854855860861862863866867
              870871874875878879882883884885890891892893
              1024 ] ),
      174 := rec(
          phi := [ 1699771710242592512580520588528596536
              604 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125340341
              342343348349350351354355358359362363366367
              370371372373378379380381596597598599604605
              606607610611614615618619622623626627628629
              634635636637852853854855860861862863866867
              870871874875878879882883884885890891892893
              1024 ] ),
      175 := rec(
          phi := [ 1699771710242592512716520708528732536
              724 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125340341
              342343348349350351354355358359362363366367
              370371372373378379380381596597598599604605
              606607610611614615618619622623626627628629
              634635636637852853854855860861862863866867
              870871874875878879882883884885890891892893
              1024 ] ),
      176 := rec(
          phi := [ 16991961710242521233100412284911657
              244 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351358359366367372373380381468469470471
              476477478479486487494495500501508509610611
              618619626627634635738739746747754755762763
              1024 ] ),
      177 := rec(
          phi := [ 16991961710242521233580417084959657
              724 ],
          autos_yielding_iso_nrs := [ 86929498102106110114116122
              124212214220222226230234238242244250252340
              342348350354358362366370372378380468470476
              478482486490494498500506508596598604606610
              614618622626628634636724726732734738742746
              750754756762764852854860862866870874878882
              8848908929809829889909949981002100610101012
              101810201024 ] ),
      178 := rec(
          phi := [ 1699196171024252123358064070849596656
              724 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      179 := rec(
          phi := [ 16991961710242521233581417094959757
              725 ],
          autos_yielding_iso_nrs := [ 86929498102106110114116122
              124212214220222226230234238242244250252340
              342348350354358362366370372378380468470476
              478482486490494498500506508596598604606610
              614618622626628634636724726732734738742746
              750754756762764852854860862866870874878882
              8848908929809829889909949981002100610101012
              101810201024 ] ),
      180 := rec(
          phi := [ 169919617102425212512580520708528596
              536724 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      181 := rec(
          phi := [ 169919617102425212512580640708528596
              656724 ],
          autos_yielding_iso_nrs := [ 86929498102106110114116122
              124212214220222226230234238242244250252340
              342348350354358362366370372378380468470476
              478482486490494498500506508596598604606610
              614618622626628634636724726732734738742746
              750754756762764852854860862866870874878882
              8848908929809829889909949981002100610101012
              101810201024 ] ),
      182 := rec(
          phi := [ 169919617102425212512581640709528597
              656725 ],
          autos_yielding_iso_nrs := [ 86929498102106110114116122
              124212214220222226230234238242244250252340
              342348350354358362366370372378380468470476
              478482486490494498500506508596598604606610
              614618622626628634636724726732734738742746
              750754756762764852854860862866870874878882
              8848908929809829889909949981002100610101012
              101810201024 ] ),
      183 := rec(
          phi := [ 16996201710242563633580411084959657
              124 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351358359366367372373380381468469470471
              476477478479486487494495500501508509610611
              618619626627634635738739746747754755762763
              1024 ] ),
      184 := rec(
          phi := [ 16912877256102438492512100640108768116
              896124 ],
          autos_yielding_iso_nrs := [ 86929498102106110114116122
              1243403423483503583663723806106186266341024 ] )
       ,
      185 := rec(
          phi := [ 16912877256102438492512580640588768596
              896604 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125340341
              342343348349350351354355358359362363366367
              370371372373378379380381596597598599604605
              606607610611614615618619622623626627628629
              634635636637852853854855860861862863866867
              870871874875878879882883884885890891892893
              1024 ] ),
      186 := rec(
          phi := [ 16912877256102438492513580641588769596
              897604 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125340341
              342343348349350351354355358359362363366367
              370371372373378379380381596597598599604605
              606607610611614615618619622623626627628629
              634635636637852853854855860861862863866867
              870871874875878879882883884885890891892893
              1024 ] ),
      187 := rec(
          phi := [ 1691281961710241442123310016022849116
              176244 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351358359366367372373380381468469470471
              476477478479486487494495500501508509610611
              618619626627634635738739746747754755762763
              1024 ] ),
      188 := rec(
          phi := [ 16912819617102414421233580417084959657
              724 ],
          autos_yielding_iso_nrs := [ 86929498102106110114116122
              124212214220222226230234238242244250252340
              342348350354358362366370372378380468470476
              478482486490494498500506508596598604606610
              614618622626628634636724726732734738742746
              750754756762764852854860862866870874878882
              8848908929809829889909949981002100610101012
              101810201024 ] ),
      189 := rec(
          phi := [ 1691281961710241442123358016070849596
              176724 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      190 := rec(
          phi := [ 1691281961710241442123358064070849596
              656724 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      191 := rec(
          phi := [ 16912819617102414421233581417094959757
              725 ],
          autos_yielding_iso_nrs := [ 86929498102106110114116122
              124212214220222226230234238242244250252340
              342348350354358362366370372378380468470476
              478482486490494498500506508596598604606610
              614618622626628634636724726732734738742746
              750754756762764852854860862866870874878882
              8848908929809829889909949981002100610101012
              101810201024 ] ),
      192 := rec(
          phi := [ 169128196171024144212512580640708528596
              656724 ],
          autos_yielding_iso_nrs := [ 86929498102106110114116122
              124212214220222226230234238242244250252340
              342348350354358362366370372378380468470476
              478482486490494498500506508596598604606610
              614618622626628634636724726732734738742746
              750754756762764852854860862866870874878882
              8848908929809829889909949981002100610101012
              101810201024 ] ),
      193 := rec(
          phi := [ 169128196171024144212512581640709528597
              656725 ],
          autos_yielding_iso_nrs := [ 86929498102106110114116122
              124212214220222226230234238242244250252340
              342348350354358362366370372378380468470476
              478482486490494498500506508596598604606610
              614618622626628634636724726732734738742746
              750754756762764852854860862866870874878882
              8848908929809829889909949981002100610101012
              101810201024 ] ),
      194 := rec(
          phi := [ 169128196171024144212513580641708529596
              657724 ],
          autos_yielding_iso_nrs := [ 86929498102106110114116122
              124212214220222226230234238242244250252340
              342348350354358362366370372378380468470476
              478482486490494498500506508596598604606610
              614618622626628634636724726732734738742746
              750754756762764852854860862866870874878882
              8848908929809829889909949981002100610101012
              101810201024 ] ),
      195 := rec(
          phi := [ 169128196171024144212513581641709529597
              657725 ],
          autos_yielding_iso_nrs := [ 86929498102106110114116122
              124212214220222226230234238242244250252340
              342348350354358362366370372378380468470476
              478482486490494498500506508596598604606610
              614618622626628634636724726732734738742746
              750754756762764852854860862866870874878882
              8848908929809829889909949981002100610101012
              101810201024 ] ),
      196 := rec(
          phi := [ 1691281962561024384212168580640708424596
              896724 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      197 := rec(
          phi := [ 1691281962561024384212512100640228768116
              896244 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351358359366367372373380381468469470471
              476477478479486487494495500501508509610611
              618619626627634635738739746747754755762763
              1024 ] ),
      198 := rec(
          phi := [ 1691281962561024384212512580520708768596
              776724 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      199 := rec(
          phi := [ 1691281962561024384212512580640708768596
              896724 ],
          autos_yielding_iso_nrs := [ 86929498102106110114116122
              124212214220222226230234238242244250252340
              342348350354358362366370372378380468470476
              478482486490494498500506508596598604606610
              614618622626628634636724726732734738742746
              750754756762764852854860862866870874878882
              8848908929809829889909949981002100610101012
              101810201024 ] ),
      200 := rec(
          phi := [ 1691281962561024384212512581640709768597
              896725 ],
          autos_yielding_iso_nrs := [ 86929498102106110114116122
              124212214220222226230234238242244250252340
              342348350354358362366370372378380468470476
              478482486490494498500506508596598604606610
              614618622626628634636724726732734738742746
              750754756762764852854860862866870874878882
              8848908929809829889909949981002100610101012
              101810201024 ] ),
      201 := rec(
          phi := [ 1691281962561024384212513580641708769596
              897724 ],
          autos_yielding_iso_nrs := [ 86929498102106110114116122
              124212214220222226230234238242244250252340
              342348350354358362366370372378380468470476
              478482486490494498500506508596598604606610
              614618622626628634636724726732734738742746
              750754756762764852854860862866870874878882
              8848908929809829889909949981002100610101012
              101810201024 ] ),
      202 := rec(
          phi := [ 1691281962561024384212513581641709769597
              897725 ],
          autos_yielding_iso_nrs := [ 86929498102106110114116122
              124212214220222226230234238242244250252340
              342348350354358362366370372378380468470476
              478482486490494498500506508596598604606610
              614618622626628634636724726732734738742746
              750754756762764852854860862866870874878882
              8848908929809829889909949981002100610101012
              101810201024 ] ),
      203 := rec(
          phi := [ 16912862017102414463616858041108184596
              57124 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351358359366367372373380381468469470471
              476477478479486487494495500501508509610611
              618619626627634635738739746747754755762763
              1024 ] ),
      204 := rec(
          phi := [ 1691286202561024384636512580640108768596
              896124 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351358359366367372373380381468469470471
              476477478479486487494495500501508509610611
              618619626627634635738739746747754755762763
              1024 ] ),
      205 := rec(
          phi := [ 16955219617102456821251223641108528252
              57124 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351358359366367372373380381468469470471
              476477478479486487494495500501508509610611
              618619626627634635738739746747754755762763
              1024 ] ),
      206 := rec(
          phi := [ 16955219617102456821251258041708528596
              57724 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      207 := rec(
          phi := [ 1695521962561024808212512580640708768596
              896724 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      208 := rec(
          phi := [ 16955262017102456863651258041108528596
              57124 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351358359366367372373380381468469470471
              476477478479486487494495500501508509610611
              618619626627634635738739746747754755762763
              1024 ] ),
      209 := rec(
          phi := [ 12121281024256468384340512724640596769
              980897852 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      210 := rec(
          phi := [ 12121281024256468384340512724640596777
              980905852 ],
          autos_yielding_iso_nrs := [ 86102212214230340342358468470
              4865965986147247267428528548709809829981024 ] )
       ,
      211 := rec(
          phi := [ 12121281024256468384340512724640596768
              980896852 ],
          autos_yielding_iso_nrs := [ 2123404685967248529801024 ] ),
      212 := rec(
          phi := [ 12121281024256468384340512724642596768
              980898852 ],
          autos_yielding_iso_nrs := 
           [ 8592939899106107114115122123212213220221
              226227234235242243250251340341348349354355
              362363370371378379468469476477482483490491
              498499506507596597604605610611618619626627
              634635724725732733738739746747754755762763
              852853860861866867874875882883890891980981
              9889899949951002100310101011101810191024 ] ),
      213 := rec(
          phi := [ 12121281024256468384340512725640597768
              981896853 ],
          autos_yielding_iso_nrs := [ 98114212226242340354370468482
              49859661062672473875485286688298099410101024 ] 
         ),
      214 := rec(
          phi := [ 12121281024256468384340512725640597769
              981897853 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      215 := rec(
          phi := [ 12121281024256468384340512725640597776
              981904853 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      216 := rec(
          phi := [ 12121281024256468384340512725640597777
              981905853 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      217 := rec(
          phi := [ 12121281024256468384340512726640598768
              982896854 ],
          autos_yielding_iso_nrs := [ 9298106114122212220226234242
              250340348354362370378468476482490498506596
              604610618626634724732738746754762852860866
              8748828909809889941002101010181024 ] ),
      218 := rec(
          phi := [ 12121281024256468384340512726642598768
              982898854 ],
          autos_yielding_iso_nrs := 
           [ 8592939899106107114115122123212213220221
              226227234235242243250251340341348349354355
              362363370371378379468469476477482483490491
              498499506507596597604605610611618619626627
              634635724725732733738739746747754755762763
              852853860861866867874875882883890891980981
              9889899949951002100310101011101810191024 ] ),
      219 := rec(
          phi := [ 12121281024256468384340512732640604768
              988896860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      220 := rec(
          phi := [ 12121281024256468384340512732640604769
              988897860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      221 := rec(
          phi := [ 12121281024256468384340512732640604776
              988904860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      222 := rec(
          phi := [ 12121281024256468384340512732640604777
              988905860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      223 := rec(
          phi := [ 12121281024256468384340512733640605769
              989897861 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      224 := rec(
          phi := [ 12121281024256468384340512733640605776
              989904861 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      225 := rec(
          phi := [ 12121281024256468384340512733640605777
              989905861 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      226 := rec(
          phi := [ 12121281024256468384340513726641598769
              982897854 ],
          autos_yielding_iso_nrs := [ 9298106114122212220226234242
              250340348354362370378468476482490498506596
              604610618626634724732738746754762852860866
              8748828909809889941002101010181024 ] ),
      227 := rec(
          phi := [ 12121281024256468384340513724641596769
              980897852 ],
          autos_yielding_iso_nrs := [ 98114212226242340354370468482
              49859661062672473875485286688298099410101024 ] 
         ),
      228 := rec(
          phi := [ 12121281024256468384340513724641596776
              980904852 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      229 := rec(
          phi := [ 12121281024256468384340513724641596777
              980905852 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      230 := rec(
          phi := [ 12121281024256468384340513725641597769
              981897853 ],
          autos_yielding_iso_nrs := [ 98114212226242340354370468482
              49859661062672473875485286688298099410101024 ] 
         ),
      231 := rec(
          phi := [ 12121281024256468384340513725641597776
              981904853 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      232 := rec(
          phi := [ 12121281024256468384340513725641597777
              981905853 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      233 := rec(
          phi := [ 12121281024256468384340513732641604769
              988897860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      234 := rec(
          phi := [ 12121281024256468384340513732641604776
              988904860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      235 := rec(
          phi := [ 12121281024256468384340513732641604777
              988905860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      236 := rec(
          phi := [ 12121281024256468384340513733641605776
              989904861 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      237 := rec(
          phi := [ 12121281024256468384340513733641605777
              989905861 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      238 := rec(
          phi := [ 12121281024256468384340514725642597770
              981898853 ],
          autos_yielding_iso_nrs := [ 9298106114122212220226234242
              250340348354362370378468476482490498506596
              604610618626634724732738746754762852860866
              8748828909809889941002101010181024 ] ),
      239 := rec(
          phi := [ 12121281024256468384340514727642599770
              983898855 ],
          autos_yielding_iso_nrs := [ 9298106114122212220226234242
              250340348354362370378468476482490498506596
              604610618626634724732738746754762852860866
              8748828909809889941002101010181024 ] ),
      240 := rec(
          phi := [ 12121281024256468384340514724642596770
              980898852 ],
          autos_yielding_iso_nrs := [ 9298106114122212220226234242
              250340348354362370378468476482490498506596
              604610618626634724732738746754762852860866
              8748828909809889941002101010181024 ] ),
      241 := rec(
          phi := [ 12121281024256468384340514726642598770
              982898854 ],
          autos_yielding_iso_nrs := [ 9298106114122212220226234242
              250340348354362370378468476482490498506596
              604610618626634724732738746754762852860866
              8748828909809889941002101010181024 ] ),
      242 := rec(
          phi := [ 12121281024256468384340520724648596776
              980904852 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      243 := rec(
          phi := [ 12121281024256468384340520724648596777
              980905852 ],
          autos_yielding_iso_nrs := [ 98114212226242340354370468482
              49859661062672473875485286688298099410101024 ] 
         ),
      244 := rec(
          phi := [ 12121281024256468384340520725648597776
              981904853 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      245 := rec(
          phi := [ 12121281024256468384340520725648597777
              981905853 ],
          autos_yielding_iso_nrs := [ 98114212226242340354370468482
              49859661062672473875485286688298099410101024 ] 
         ),
      246 := rec(
          phi := [ 12121281024256468384340520732648604776
              988904860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      247 := rec(
          phi := [ 12121281024256468384340520732648604777
              988905860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      248 := rec(
          phi := [ 12121281024256468384340520733648605776
              989904861 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      249 := rec(
          phi := [ 12121281024256468384340521724649596776
              980904852 ],
          autos_yielding_iso_nrs := [ 98114212226242340354370468482
              49859661062672473875485286688298099410101024 ] 
         ),
      250 := rec(
          phi := [ 12121281024256468384340521725649597776
              981904853 ],
          autos_yielding_iso_nrs := [ 98114212226242340354370468482
              49859661062672473875485286688298099410101024 ] 
         ),
      251 := rec(
          phi := [ 12121281024256468384340521732649604776
              988904860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      252 := rec(
          phi := [ 12121281024256469384341512734640606768
              991896863 ],
          autos_yielding_iso_nrs := [ 9298106114122212220226234242
              250340348354362370378468476482490498506596
              604610618626634724732738746754762852860866
              8748828909809889941002101010181024 ] ),
      253 := rec(
          phi := [ 12121281024256469384341512725640597769
              980897852 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      254 := rec(
          phi := [ 12121281024256469384341512725640597776
              980904852 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      255 := rec(
          phi := [ 12121281024256469384341512725640597777
              980905852 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      256 := rec(
          phi := [ 12121281024256469384341512732640604768
              989896861 ],
          autos_yielding_iso_nrs := [ 2123404685967248529801024 ] ),
      257 := rec(
          phi := [ 12121281024256469384341512732640604769
              989897861 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      258 := rec(
          phi := [ 12121281024256469384341512732640604777
              989905861 ],
          autos_yielding_iso_nrs := [ 86102212214230340342358468470
              4865965986147247267428528548709809829981024 ] )
       ,
      259 := rec(
          phi := [ 12121281024256469384341512733640605768
              988896860 ],
          autos_yielding_iso_nrs := [ 98114212226242340354370468482
              49859661062672473875485286688298099410101024 ] 
         ),
      260 := rec(
          phi := [ 12121281024256469384341512733640605769
              988897860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      261 := rec(
          phi := [ 12121281024256469384341512733640605776
              988904860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      262 := rec(
          phi := [ 12121281024256469384341512733640605777
              988905860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      263 := rec(
          phi := [ 12121281024256469384341513734641606769
              991897863 ],
          autos_yielding_iso_nrs := [ 9298106114122212220226234242
              250340348354362370378468476482490498506596
              604610618626634724732738746754762852860866
              8748828909809889941002101010181024 ] ),
      264 := rec(
          phi := [ 12121281024256469384341513724641596769
              981897853 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      265 := rec(
          phi := [ 12121281024256469384341513724641596776
              981904853 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      266 := rec(
          phi := [ 12121281024256469384341513724641596777
              981905853 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      267 := rec(
          phi := [ 12121281024256469384341513725641597776
              980904852 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      268 := rec(
          phi := [ 12121281024256469384341513725641597777
              980905852 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      269 := rec(
          phi := [ 12121281024256469384341513732641604769
              989897861 ],
          autos_yielding_iso_nrs := [ 98114212226242340354370468482
              49859661062672473875485286688298099410101024 ] 
         ),
      270 := rec(
          phi := [ 12121281024256469384341513732641604776
              989904861 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      271 := rec(
          phi := [ 12121281024256469384341513732641604777
              989905861 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      272 := rec(
          phi := [ 12121281024256469384341513733641605769
              988897860 ],
          autos_yielding_iso_nrs := [ 98114212226242340354370468482
              49859661062672473875485286688298099410101024 ] 
         ),
      273 := rec(
          phi := [ 12121281024256469384341513733641605776
              988904860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      274 := rec(
          phi := [ 12121281024256469384341513733641605777
              988905860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      275 := rec(
          phi := [ 12121281024256469384341514724642596770
              981898853 ],
          autos_yielding_iso_nrs := [ 86929498102106110114116122
              124212214220222226230234238242244250252340
              342348350354358362366370372378380468470476
              478482486490494498500506508596598604606610
              614618622626628634636724726732734738742746
              750754756762764852854860862866870874878882
              8848908929809829889909949981002100610101012
              101810201024 ] ),
      276 := rec(
          phi := [ 12121281024256469384341520724648596776
              981904853 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      277 := rec(
          phi := [ 12121281024256469384341520724648596777
              981905853 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      278 := rec(
          phi := [ 12121281024256469384341520725648597776
              980904852 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      279 := rec(
          phi := [ 12121281024256469384341520732648604776
              989904861 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      280 := rec(
          phi := [ 12121281024256469384341520732648604777
              989905861 ],
          autos_yielding_iso_nrs := [ 98114212226242340354370468482
              49859661062672473875485286688298099410101024 ] 
         ),
      281 := rec(
          phi := [ 12121281024256469384341520733648605776
              988904860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      282 := rec(
          phi := [ 12121281024256469384341520733648605777
              988905860 ],
          autos_yielding_iso_nrs := [ 98114212226242340354370468482
              49859661062672473875485286688298099410101024 ] 
         ),
      283 := rec(
          phi := [ 12121281024256469384341521724649596776
              981904853 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      284 := rec(
          phi := [ 12121281024256469384341521732649604776
              989904861 ],
          autos_yielding_iso_nrs := [ 98114212226242340354370468482
              49859661062672473875485286688298099410101024 ] 
         ),
      285 := rec(
          phi := [ 12121281024256469384341521733649605776
              988904860 ],
          autos_yielding_iso_nrs := [ 98114212226242340354370468482
              49859661062672473875485286688298099410101024 ] 
         ),
      286 := rec(
          phi := [ 12121281024256476384348512725640597769
              989897861 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      287 := rec(
          phi := [ 12121281024256476384348512725640597777
              989905861 ],
          autos_yielding_iso_nrs := [ 86102212214230340342358468470
              4865965986147247267428528548709809829981024 ] )
       ,
      288 := rec(
          phi := [ 12121281024256476384348512733640605768
              981896853 ],
          autos_yielding_iso_nrs := [ 86212214340342468470596598724
              7268528549809821024 ] ),
      289 := rec(
          phi := [ 12121281024256476384348512733640605769
              981897853 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      290 := rec(
          phi := [ 12121281024256476384348512733640605776
              981904853 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      291 := rec(
          phi := [ 12121281024256476384348512733640605777
              981905853 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      292 := rec(
          phi := [ 12121281024256476384348513724641596768
              988896860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      293 := rec(
          phi := [ 12121281024256476384348513724641596769
              988897860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      294 := rec(
          phi := [ 12121281024256476384348513724641596776
              988904860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      295 := rec(
          phi := [ 12121281024256476384348513724641596777
              988905860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      296 := rec(
          phi := [ 12121281024256476384348513725641597769
              989897861 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      297 := rec(
          phi := [ 12121281024256476384348513725641597776
              989904861 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      298 := rec(
          phi := [ 12121281024256476384348513725641597777
              989905861 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      299 := rec(
          phi := [ 12121281024256476384348513732641604769
              980897852 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      300 := rec(
          phi := [ 12121281024256476384348513732641604776
              980904852 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      301 := rec(
          phi := [ 12121281024256476384348513732641604777
              980905852 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      302 := rec(
          phi := [ 12121281024256476384348513733641605769
              981897853 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      303 := rec(
          phi := [ 12121281024256476384348513733641605776
              981904853 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      304 := rec(
          phi := [ 12121281024256476384348513733641605777
              981905853 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      305 := rec(
          phi := [ 12121281024256476384348520724648596768
              988896860 ],
          autos_yielding_iso_nrs := [ 8698212214226340342354468470
              4825965986107247267388528548669809829941024 ] )
       ,
      306 := rec(
          phi := [ 12121281024256476384348520724648596769
              988897860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      307 := rec(
          phi := [ 12121281024256476384348520724648596776
              988904860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      308 := rec(
          phi := [ 12121281024256476384348520724648596777
              988905860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      309 := rec(
          phi := [ 12121281024256476384348520725648597769
              989897861 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      310 := rec(
          phi := [ 12121281024256476384348520725648597776
              989904861 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      311 := rec(
          phi := [ 12121281024256476384348520725648597777
              989905861 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      312 := rec(
          phi := [ 12121281024256476384348520732648604769
              980897852 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      313 := rec(
          phi := [ 12121281024256476384348520732648604776
              980904852 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      314 := rec(
          phi := [ 12121281024256476384348520732648604777
              980905852 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      315 := rec(
          phi := [ 12121281024256476384348520733648605769
              981897853 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      316 := rec(
          phi := [ 12121281024256476384348520733648605776
              981904853 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      317 := rec(
          phi := [ 12121281024256476384348520733648605777
              981905853 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      318 := rec(
          phi := [ 12121281024256476384348521724649596769
              988897860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      319 := rec(
          phi := [ 12121281024256476384348521724649596776
              988904860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      320 := rec(
          phi := [ 12121281024256476384348521724649596777
              988905860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      321 := rec(
          phi := [ 12121281024256476384348521725649597769
              989897861 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      322 := rec(
          phi := [ 12121281024256476384348521725649597776
              989904861 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      323 := rec(
          phi := [ 12121281024256476384348521725649597777
              989905861 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      324 := rec(
          phi := [ 12121281024256476384348521732649604769
              980897852 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      325 := rec(
          phi := [ 12121281024256476384348521732649604776
              980904852 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      326 := rec(
          phi := [ 12121281024256476384348521732649604777
              980905852 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      327 := rec(
          phi := [ 12121281024256476384348521733649605769
              981897853 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      328 := rec(
          phi := [ 12121281024256476384348521733649605776
              981904853 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      329 := rec(
          phi := [ 12121281024256476384348521733649605777
              981905853 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      330 := rec(
          phi := [ 12121281024256482384354512738640610777
              980905852 ],
          autos_yielding_iso_nrs := [ 858687102103212213214215230
              231340341342343358359468469470471486487596
              597598599614615724725726727742743852853854
              8558708719809819829839989991024 ] ),
      331 := rec(
          phi := [ 12121281024256483384355512746640618777
              989905861 ],
          autos_yielding_iso_nrs := [ 858687102103212213214215230
              231340341342343358359468469470471486487596
              597598599614615724725726727742743852853854
              8558708719809819829839989991024 ] ),
      332 := rec(
          phi := [ 12121281024257468385340513726641598769
              982897854 ],
          autos_yielding_iso_nrs := [ 9298106114122212220226234242
              250340348354362370378468476482490498506596
              604610618626634724732738746754762852860866
              8748828909809889941002101010181024 ] ),
      333 := rec(
          phi := [ 12121281024257468385340513724641596769
              980897852 ],
          autos_yielding_iso_nrs := [ 98114212226242340354370468482
              49859661062672473875485286688298099410101024 ] 
         ),
      334 := rec(
          phi := [ 12121281024257468385340513724641596776
              980904852 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      335 := rec(
          phi := [ 12121281024257468385340513724641596777
              980905852 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      336 := rec(
          phi := [ 12121281024257468385340513725641597769
              981897853 ],
          autos_yielding_iso_nrs := [ 98114212226242340354370468482
              49859661062672473875485286688298099410101024 ] 
         ),
      337 := rec(
          phi := [ 12121281024257468385340513725641597776
              981904853 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      338 := rec(
          phi := [ 12121281024257468385340513725641597777
              981905853 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      339 := rec(
          phi := [ 12121281024257468385340513732641604769
              988897860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      340 := rec(
          phi := [ 12121281024257468385340513732641604776
              988904860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      341 := rec(
          phi := [ 12121281024257468385340513732641604777
              988905860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      342 := rec(
          phi := [ 12121281024257468385340513733641605776
              989904861 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      343 := rec(
          phi := [ 12121281024257468385340513733641605777
              989905861 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      344 := rec(
          phi := [ 12121281024257468385340520724648596777
              980905852 ],
          autos_yielding_iso_nrs := [ 2123404685967248529801024 ] ),
      345 := rec(
          phi := [ 12121281024257468385340520725648597776
              981904853 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      346 := rec(
          phi := [ 12121281024257468385340520725648597777
              981905853 ],
          autos_yielding_iso_nrs := [ 98114212226242340354370468482
              49859661062672473875485286688298099410101024 ] 
         ),
      347 := rec(
          phi := [ 12121281024257468385340520732648604776
              988904860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      348 := rec(
          phi := [ 12121281024257468385340520732648604777
              988905860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      349 := rec(
          phi := [ 12121281024257468385340520733648605776
              989904861 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      350 := rec(
          phi := [ 12121281024257468385340521724649596776
              980904852 ],
          autos_yielding_iso_nrs := [ 98114212226242340354370468482
              49859661062672473875485286688298099410101024 ] 
         ),
      351 := rec(
          phi := [ 12121281024257468385340521725649597776
              981904853 ],
          autos_yielding_iso_nrs := [ 98114212226242340354370468482
              49859661062672473875485286688298099410101024 ] 
         ),
      352 := rec(
          phi := [ 12121281024257468385340521732649604776
              988904860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      353 := rec(
          phi := [ 12121281024257468385340522724650596778
              980906852 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      354 := rec(
          phi := [ 12121281024257468385340522725650597778
              981906853 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      355 := rec(
          phi := [ 12121281024257469385341513734641606769
              991897863 ],
          autos_yielding_iso_nrs := [ 9298106114122212220226234242
              250340348354362370378468476482490498506596
              604610618626634724732738746754762852860866
              8748828909809889941002101010181024 ] ),
      356 := rec(
          phi := [ 12121281024257469385341513724641596769
              981897853 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      357 := rec(
          phi := [ 12121281024257469385341513724641596776
              981904853 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      358 := rec(
          phi := [ 12121281024257469385341513724641596777
              981905853 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      359 := rec(
          phi := [ 12121281024257469385341513725641597776
              980904852 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      360 := rec(
          phi := [ 12121281024257469385341513732641604769
              989897861 ],
          autos_yielding_iso_nrs := [ 98114212226242340354370468482
              49859661062672473875485286688298099410101024 ] 
         ),
      361 := rec(
          phi := [ 12121281024257469385341513732641604776
              989904861 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      362 := rec(
          phi := [ 12121281024257469385341513732641604777
              989905861 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      363 := rec(
          phi := [ 12121281024257469385341513733641605769
              988897860 ],
          autos_yielding_iso_nrs := [ 98114212226242340354370468482
              49859661062672473875485286688298099410101024 ] 
         ),
      364 := rec(
          phi := [ 12121281024257469385341513733641605776
              988904860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      365 := rec(
          phi := [ 12121281024257469385341513733641605777
              988905860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      366 := rec(
          phi := [ 12121281024257469385341520725648597776
              980904852 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      367 := rec(
          phi := [ 12121281024257469385341520732648604777
              989905861 ],
          autos_yielding_iso_nrs := [ 2123404685967248529801024 ] ),
      368 := rec(
          phi := [ 12121281024257469385341520733648605776
              988904860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      369 := rec(
          phi := [ 12121281024257469385341520733648605777
              988905860 ],
          autos_yielding_iso_nrs := [ 98114212226242340354370468482
              49859661062672473875485286688298099410101024 ] 
         ),
      370 := rec(
          phi := [ 12121281024257469385341521724649596776
              981904853 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      371 := rec(
          phi := [ 12121281024257469385341521732649604776
              989904861 ],
          autos_yielding_iso_nrs := [ 98114212226242340354370468482
              49859661062672473875485286688298099410101024 ] 
         ),
      372 := rec(
          phi := [ 12121281024257469385341521733649605776
              988904860 ],
          autos_yielding_iso_nrs := [ 98114212226242340354370468482
              49859661062672473875485286688298099410101024 ] 
         ),
      373 := rec(
          phi := [ 12121281024257469385341522724650596778
              981906853 ],
          autos_yielding_iso_nrs := [ 86929498102106110114116122
              124212214220222226230234238242244250252340
              342348350354358362366370372378380468470476
              478482486490494498500506508596598604606610
              614618622626628634636724726732734738742746
              750754756762764852854860862866870874878882
              8848908929809829889909949981002100610101012
              101810201024 ] ),
      374 := rec(
          phi := [ 12121281024257469385341522734650606779
              991907863 ],
          autos_yielding_iso_nrs := [ 9298106114122212220226234242
              250340348354362370378468476482490498506596
              604610618626634724732738746754762852860866
              8748828909809889941002101010181024 ] ),
      375 := rec(
          phi := [ 12121281024257469385341522735650607779
              990907862 ],
          autos_yielding_iso_nrs := [ 9298106114122212220226234242
              250340348354362370378468476482490498506596
              604610618626634724732738746754762852860866
              8748828909809889941002101010181024 ] ),
      376 := rec(
          phi := [ 12121281024257476385348513724641596769
              988897860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      377 := rec(
          phi := [ 12121281024257476385348513724641596776
              988904860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      378 := rec(
          phi := [ 12121281024257476385348513724641596777
              988905860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      379 := rec(
          phi := [ 12121281024257476385348513725641597769
              989897861 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      380 := rec(
          phi := [ 12121281024257476385348513725641597776
              989904861 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      381 := rec(
          phi := [ 12121281024257476385348513732641604769
              980897852 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      382 := rec(
          phi := [ 12121281024257476385348513732641604776
              980904852 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      383 := rec(
          phi := [ 12121281024257476385348513733641605769
              981897853 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      384 := rec(
          phi := [ 12121281024257476385348513733641605776
              981904853 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      385 := rec(
          phi := [ 12121281024257476385348513733641605777
              981905853 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      386 := rec(
          phi := [ 12121281024257476385348520725648597769
              989897861 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      387 := rec(
          phi := [ 12121281024257476385348520733648605769
              981897853 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      388 := rec(
          phi := [ 12121281024257476385348520733648605777
              981905853 ],
          autos_yielding_iso_nrs := [ 86212214340342468470596598724
              7268528549809821024 ] ),
      389 := rec(
          phi := [ 12121281024257476385348521724649596769
              988897860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      390 := rec(
          phi := [ 12121281024257476385348521724649596776
              988904860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      391 := rec(
          phi := [ 12121281024257476385348521725649597769
              989897861 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      392 := rec(
          phi := [ 12121281024257476385348521725649597776
              989904861 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      393 := rec(
          phi := [ 12121281024257476385348521732649604769
              980897852 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      394 := rec(
          phi := [ 12121281024257476385348521732649604776
              980904852 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      395 := rec(
          phi := [ 12121281024257476385348521733649605769
              981897853 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      396 := rec(
          phi := [ 12121281024257476385348521733649605776
              981904853 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      397 := rec(
          phi := [ 12121281024264468392340513724641596769
              980897852 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      398 := rec(
          phi := [ 12121281024264468392340513725641597769
              981897853 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      399 := rec(
          phi := [ 12121281024264468392340513725641597776
              981904853 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      400 := rec(
          phi := [ 12121281024264468392340513732641604769
              988897860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      401 := rec(
          phi := [ 12121281024264468392340513732641604776
              988904860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      402 := rec(
          phi := [ 12121281024264468392340513733641605769
              989897861 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      403 := rec(
          phi := [ 12121281024264468392340513733641605776
              989904861 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      404 := rec(
          phi := [ 12121281024264468392340521724649596769
              980897852 ],
          autos_yielding_iso_nrs := [ 86212214340342468470596598724
              7268528549809821024 ] ),
      405 := rec(
          phi := [ 12121281024264468392340521725649597769
              981897853 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      406 := rec(
          phi := [ 12121281024264468392340521725649597776
              981904853 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      407 := rec(
          phi := [ 12121281024264468392340521732649604769
              988897860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      408 := rec(
          phi := [ 12121281024264468392340521732649604776
              988904860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      409 := rec(
          phi := [ 12121281024264468392340521733649605769
              989897861 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      410 := rec(
          phi := [ 12121281024264468392340521733649605776
              989904861 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      411 := rec(
          phi := [ 12121281024264469392341513732641604769
              989897861 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      412 := rec(
          phi := [ 12121281024264469392341513733641605769
              988897860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      413 := rec(
          phi := [ 12121281024264469392341513733641605776
              988904860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      414 := rec(
          phi := [ 12121281024264469392341521732649604769
              989897861 ],
          autos_yielding_iso_nrs := [ 86212214340342468470596598724
              7268528549809821024 ] ),
      415 := rec(
          phi := [ 12121281024264469392341521733649605769
              988897860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      416 := rec(
          phi := [ 12121281024264469392341521733649605776
              988904860 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      417 := rec(
          phi := [ 12121281024264476392348513733641605769
              981897853 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      418 := rec(
          phi := [ 12121281024264476392348513733641605776
              981904853 ],
          autos_yielding_iso_nrs := [ 8698102114116212214226230242
              244340342354358370372468470482486498500596
              598610614626628724726738742754756852854866
              870882884980982994998101010121024 ] ),
      419 := rec(
          phi := [ 12121281024264476392348521733649605769
              981897853 ],
          autos_yielding_iso_nrs := [ 86212214340342468470596598724
              7268528549809821024 ] ),
      420 := rec(
          phi := [ 12121281024264477392349521725649597769
              988897860 ],
          autos_yielding_iso_nrs := [ 86212214340342468470596598724
              7268528549809821024 ] ),
      421 := rec(
          phi := [ 12121301024256468386340512724640596768
              980896852 ],
          autos_yielding_iso_nrs := [ 9298106114122212220226234242
              250340348354362370378468476482490498506596
              604610618626634724732738746754762852860866
              8748828909809889941002101010181024 ] ),
      422 := rec(
          phi := [ 12121301024256468386340512724642596768
              980898852 ],
          autos_yielding_iso_nrs := 
           [ 8592939899106107114115122123212213220221
              226227234235242243250251340341348349354355
              362363370371378379468469476477482483490491
              498499506507596597604605610611618619626627
              634635724725732733738739746747754755762763
              852853860861866867874875882883890891980981
              9889899949951002100310101011101810191024 ] ),
      423 := rec(
          phi := [ 12121301024256468386340512725640597768
              981896853 ],
          autos_yielding_iso_nrs := [ 9298106114122212220226234242
              250340348354362370378468476482490498506596
              604610618626634724732738746754762852860866
              8748828909809889941002101010181024 ] ),
      424 := rec(
          phi := [ 12121301024256468386340512726640598768
              982896854 ],
          autos_yielding_iso_nrs := [ 9298106114122212220226234242
              250340348354362370378468476482490498506596
              604610618626634724732738746754762852860866
              8748828909809889941002101010181024 ] ),
      425 := rec(
          phi := [ 12121301024256468386340512726642598768
              982898854 ],
          autos_yielding_iso_nrs := 
           [ 8592939899106107114115122123212213220221
              226227234235242243250251340341348349354355
              362363370371378379468469476477482483490491
              498499506507596597604605610611618619626627
              634635724725732733738739746747754755762763
              852853860861866867874875882883890891980981
              9889899949951002100310101011101810191024 ] ),
      426 := rec(
          phi := [ 12121301024256468386340512727640599768
              983896855 ],
          autos_yielding_iso_nrs := [ 9298106114122212220226234242
              250340348354362370378468476482490498506596
              604610618626634724732738746754762852860866
              8748828909809889941002101010181024 ] ),
      427 := rec(
          phi := [ 12121301024256468386340514725642597770
              981898853 ],
          autos_yielding_iso_nrs := [ 9298106114122212220226234242
              250340348354362370378468476482490498506596
              604610618626634724732738746754762852860866
              8748828909809889941002101010181024 ] ),
      428 := rec(
          phi := [ 12121301024256468386340514727642599770
              983898855 ],
          autos_yielding_iso_nrs := [ 9298106114122212220226234242
              250340348354362370378468476482490498506596
              604610618626634724732738746754762852860866
              8748828909809889941002101010181024 ] ),
      429 := rec(
          phi := [ 12121301024256468386340514724642596770
              980898852 ],
          autos_yielding_iso_nrs := [ 9298106114122212220226234242
              250340348354362370378468476482490498506596
              604610618626634724732738746754762852860866
              8748828909809889941002101010181024 ] ),
      430 := rec(
          phi := [ 12121301024256468386340514726642598770
              982898854 ],
          autos_yielding_iso_nrs := [ 9298106114122212220226234242
              250340348354362370378468476482490498506596
              604610618626634724732738746754762852860866
              8748828909809889941002101010181024 ] ),
      431 := rec(
          phi := [ 12121301024256469386341512724640596768
              981896853 ],
          autos_yielding_iso_nrs := [ 86929498102106110114116122
              124212214220222226230234238242244250252340
              342348350354358362366370372378380468470476
              478482486490494498500506508596598604606610
              614618622626628634636724726732734738742746
              750754756762764852854860862866870874878882
              8848908929809829889909949981002100610101012
              101810201024 ] ),
      432 := rec(
          phi := [ 12121301024256469386341514724642596770
              981898853 ],
          autos_yielding_iso_nrs := [ 86929498102106110114116122
              124212214220222226230234238242244250252340
              342348350354358362366370372378380468470476
              478482486490494498500506508596598604606610
              614618622626628634636724726732734738742746
              750754756762764852854860862866870874878882
              8848908929809829889909949981002100610101012
              101810201024 ] ),
      433 := rec(
          phi := [ 12141281024256469384343512732640607768
              989896862 ],
          autos_yielding_iso_nrs := 
           [ 8592939899106107114115122123212213220221
              226227234235242243250251340341348349354355
              362363370371378379468469476477482483490491
              498499506507596597604605610611618619626627
              634635724725732733738739746747754755762763
              852853860861866867874875882883890891980981
              9889899949951002100310101011101810191024 ] ),
      434 := rec(
          phi := [ 12141281024256469384343513732641607769
              989897862 ],
          autos_yielding_iso_nrs := 
           [ 8592939899106107114115122123212213220221
              226227234235242243250251340341348349354355
              362363370371378379468469476477482483490491
              498499506507596597604605610611618619626627
              634635724725732733738739746747754755762763
              852853860861866867874875882883890891980981
              9889899949951002100310101011101810191024 ] ),
      435 := rec(
          phi := [ 12141281024256470384340512724640598768
              980896854 ],
          autos_yielding_iso_nrs := 
           [ 8592939899106107114115122123212213220221
              226227234235242243250251340341348349354355
              362363370371378379468469476477482483490491
              498499506507596597604605610611618619626627
              634635724725732733738739746747754755762763
              852853860861866867874875882883890891980981
              9889899949951002100310101011101810191024 ] ),
      436 := rec(
          phi := [ 12141281024256470384340512724642598768
              980898854 ],
          autos_yielding_iso_nrs := 
           [ 8592939899106107114115122123212213220221
              226227234235242243250251340341348349354355
              362363370371378379468469476477482483490491
              498499506507596597604605610611618619626627
              634635724725732733738739746747754755762763
              852853860861866867874875882883890891980981
              9889899949951002100310101011101810191024 ] ),
      437 := rec(
          phi := [ 12141281024256470384340512726642596768
              982898852 ],
          autos_yielding_iso_nrs := 
           [ 8592939899106107114115122123212213220221
              226227234235242243250251340341348349354355
              362363370371378379468469476477482483490491
              498499506507596597604605610611618619626627
              634635724725732733738739746747754755762763
              852853860861866867874875882883890891980981
              9889899949951002100310101011101810191024 ] ),
      438 := rec(
          phi := [ 12141281024256470384340513724641598769
              980897854 ],
          autos_yielding_iso_nrs := 
           [ 8592939899106107114115122123212213220221
              226227234235242243250251340341348349354355
              362363370371378379468469476477482483490491
              498499506507596597604605610611618619626627
              634635724725732733738739746747754755762763
              852853860861866867874875882883890891980981
              9889899949951002100310101011101810191024 ] ),
      439 := rec(
          phi := [ 12141281024256470384340514724642598770
              980898854 ],
          autos_yielding_iso_nrs := 
           [ 8592939899106107114115122123212213220221
              226227234235242243250251340341348349354355
              362363370371378379468469476477482483490491
              498499506507596597604605610611618619626627
              634635724725732733738739746747754755762763
              852853860861866867874875882883890891980981
              9889899949951002100310101011101810191024 ] ),
      440 := rec(
          phi := [ 12141281024256470384340515724643598771
              980899854 ],
          autos_yielding_iso_nrs := 
           [ 8592939899106107114115122123212213220221
              226227234235242243250251340341348349354355
              362363370371378379468469476477482483490491
              498499506507596597604605610611618619626627
              634635724725732733738739746747754755762763
              852853860861866867874875882883890891980981
              9889899949951002100310101011101810191024 ] ),
      441 := rec(
          phi := [ 12141281024257469385343512732640607768
              989896862 ],
          autos_yielding_iso_nrs := 
           [ 8592939899106107114115122123212213220221
              226227234235242243250251340341348349354355
              362363370371378379468469476477482483490491
              498499506507596597604605610611618619626627
              634635724725732733738739746747754755762763
              852853860861866867874875882883890891980981
              9889899949951002100310101011101810191024 ] ),
      442 := rec(
          phi := [ 12141281024257469385343513732641607769
              989897862 ],
          autos_yielding_iso_nrs := 
           [ 8592939899106107114115122123212213220221
              226227234235242243250251340341348349354355
              362363370371378379468469476477482483490491
              498499506507596597604605610611618619626627
              634635724725732733738739746747754755762763
              852853860861866867874875882883890891980981
              9889899949951002100310101011101810191024 ] ),
      443 := rec(
          phi := [ 12141281024257470385340512724640598768
              980896854 ],
          autos_yielding_iso_nrs := 
           [ 8592939899106107114115122123212213220221
              226227234235242243250251340341348349354355
              362363370371378379468469476477482483490491
              498499506507596597604605610611618619626627
              634635724725732733738739746747754755762763
              852853860861866867874875882883890891980981
              9889899949951002100310101011101810191024 ] ),
      444 := rec(
          phi := [ 12141281024257470385340513724641598769
              980897854 ],
          autos_yielding_iso_nrs := 
           [ 8592939899106107114115122123212213220221
              226227234235242243250251340341348349354355
              362363370371378379468469476477482483490491
              498499506507596597604605610611618619626627
              634635724725732733738739746747754755762763
              852853860861866867874875882883890891980981
              9889899949951002100310101011101810191024 ] ),
      445 := rec(
          phi := [ 12141301024256470386340512724640598768
              980896854 ],
          autos_yielding_iso_nrs := 
           [ 8592939899106107114115122123212213220221
              226227234235242243250251340341348349354355
              362363370371378379468469476477482483490491
              498499506507596597604605610611618619626627
              634635724725732733738739746747754755762763
              852853860861866867874875882883890891980981
              9889899949951002100310101011101810191024 ] ),
      446 := rec(
          phi := [ 12141301024256470386340512724642598768
              980898854 ],
          autos_yielding_iso_nrs := 
           [ 8592939899106107114115122123212213220221
              226227234235242243250251340341348349354355
              362363370371378379468469476477482483490491
              498499506507596597604605610611618619626627
              634635724725732733738739746747754755762763
              852853860861866867874875882883890891980981
              9889899949951002100310101011101810191024 ] ),
      447 := rec(
          phi := [ 12141301024256470386340512726642596768
              982898852 ],
          autos_yielding_iso_nrs := 
           [ 8592939899106107114115122123212213220221
              226227234235242243250251340341348349354355
              362363370371378379468469476477482483490491
              498499506507596597604605610611618619626627
              634635724725732733738739746747754755762763
              852853860861866867874875882883890891980981
              9889899949951002100310101011101810191024 ] ),
      448 := rec(
          phi := [ 12141301024256470386340514724642598770
              980898854 ],
          autos_yielding_iso_nrs := 
           [ 8592939899106107114115122123212213220221
              226227234235242243250251340341348349354355
              362363370371378379468469476477482483490491
              498499506507596597604605610611618619626627
              634635724725732733738739746747754755762763
              852853860861866867874875882883890891980981
              9889899949951002100310101011101810191024 ] ),
      449 := rec(
          phi := [ 12141311024259470384340512724640598768
              980896854 ],
          autos_yielding_iso_nrs := 
           [ 8592939899106107114115122123212213220221
              226227234235242243250251340341348349354355
              362363370371378379468469476477482483490491
              498499506507596597604605610611618619626627
              634635724725732733738739746747754755762763
              852853860861866867874875882883890891980981
              9889899949951002100310101011101810191024 ] ),
      450 := rec(
          phi := [ 12141311024259470384340515724643598771
              980899854 ],
          autos_yielding_iso_nrs := 
           [ 8592939899106107114115122123212213220221
              226227234235242243250251340341348349354355
              362363370371378379468469476477482483490491
              498499506507596597604605610611618619626627
              634635724725732733738739746747754755762763
              852853860861866867874875882883890891980981
              9889899949951002100310101011101810191024 ] ),
      451 := rec(
          phi := [ 5691377211024299237100451085311661124 
             ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125340341
              342343348349350351354355358359362363366367
              370371372373378379380381596597598599604605
              606607610611614615618619622623626627628629
              634635636637852853854855860861862863866867
              870871874875878879882883884885890891892893
              1024 ] ),
      452 := rec(
          phi := [ 56913772110242992516580524588532596540
              604 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125340341
              342343348349350351354355358359362363366367
              370371372373378379380381596597598599604605
              606607610611614615618619622623626627628629
              634635636637852853854855860861862863866867
              870871874875878879882883884885890891892893
              1024 ] ),
      453 := rec(
          phi := [ 56913772110242992516716524708532732540
              724 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125340341
              342343348349350351354355358359362363366367
              370371372373378379380381596597598599604605
              606607610611614615618619622623626627628629
              634635636637852853854855860861862863866867
              870871874875878879882883884885890891892893
              1024 ] ),
      454 := rec(
          phi := [ 569131962110242921237100452285311661
              244 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      455 := rec(
          phi := [ 569131962110242921237236451085325261
              124 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      456 := rec(
          phi := [ 5691319621102429212516580524708532596
              540724 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      457 := rec(
          phi := [ 56913277260102438892516580644588772596
              900604 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125340341
              342343348349350351354355358359362363366367
              370371372373378379380381596597598599604605
              606607610611614615618619622623626627628629
              634635636637852853854855860861862863866867
              870871874875878879882883884885890891892893
              1024 ] ),
      458 := rec(
          phi := [ 56913277260102438892516716644708772732
              900724 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125340341
              342343348349350351354355358359362363366367
              370371372373378379380381596597598599604605
              606607610611614615618619622623626627628629
              634635636637852853854855860861862863866867
              870871874875878879882883884885890891892893
              1024 ] ),
      459 := rec(
          phi := [ 5691321962110241482123710016422853116
              180244 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      460 := rec(
          phi := [ 569132196211024148212516580644708532596
              660724 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      461 := rec(
          phi := [ 5691321962601024388212516580644708772596
              900724 ],
          autos_yielding_iso_nrs := [ 858687929394959899102103
              106107110111114115116117122123124125212213
              214215220221222223226227230231234235238239
              242243244245250251252253340341342343348349
              350351354355358359362363366367370371372373
              378379380381468469470471476477478479482483
              486487490491494495498499500501506507508509
              596597598599604605606607610611614615618619
              622623626627628629634635636637724725726727
              732733734735738739742743746747750751754755
              756757762763764765852853854855860861862863
              866867870871874875878879882883884885890891
              892893980981982983988989990991994995998999
              100210031006100710101011101210131018101910201021
              1024 ] ),
      462 := rec(
          phi := [ 52121321024260468388340516724644596772
              980900852 ],
          autos_yielding_iso_nrs := 
           [ 8586879899102103114115116117212213214215
              226227230231242243244245340341342343354355
              358359370371372373468469470471482483486487
              498499500501596597598599610611614615626627
              628629724725726727738739742743754755756757
              852853854855866867870871882883884885980981
              98298399499599899910101011101210131024 ] ),
      463 := rec(
          phi := [ 52121321024260468388340516732644604772
              988900860 ],
          autos_yielding_iso_nrs := 
           [ 8586879899102103114115116117212213214215
              226227230231242243244245340341342343354355
              358359370371372373468469470471482483486487
              498499500501596597598599610611614615626627
              628629724725726727738739742743754755756757
              852853854855866867870871882883884885980981
              98298399499599899910101011101210131024 ] ),
      464 := rec(
          phi := [ 52121321024260476388348516724644596772
              988900860 ],
          autos_yielding_iso_nrs := 
           [ 8586879899102103114115116117212213214215
              226227230231242243244245340341342343354355
              358359370371372373468469470471482483486487
              498499500501596597598599610611614615626627
              628629724725726727738739742743754755756757
              852853854855866867870871882883884885980981
              98298399499599899910101011101210131024 ] ),
      465 := rec(
          phi := [ 52121321024260476388348516732644604772
              980900852 ],
          autos_yielding_iso_nrs := 
           [ 8586879899102103114115116117212213214215
              226227230231242243244245340341342343354355
              358359370371372373468469470471482483486487
              498499500501596597598599610611614615626627
              628629724725726727738739742743754755756757
              852853854855866867870871882883884885980981
              98298399499599899910101011101210131024 ] ),
      466 := rec(
          phi := [ 52121321024268468396340516724644596780
              980908852 ],
          autos_yielding_iso_nrs := 
           [ 8586879899102103114115116117212213214215
              226227230231242243244245340341342343354355
              358359370371372373468469470471482483486487
              498499500501596597598599610611614615626627
              628629724725726727738739742743754755756757
              852853854855866867870871882883884885980981
              98298399499599899910101011101210131024 ] ),
      467 := rec(
          phi := [ 52121321024268468396340516732644604780
              988908860 ],
          autos_yielding_iso_nrs := 
           [ 8586879899102103114115116117212213214215
              226227230231242243244245340341342343354355
              358359370371372373468469470471482483486487
              498499500501596597598599610611614615626627
              628629724725726727738739742743754755756757
              852853854855866867870871882883884885980981
              98298399499599899910101011101210131024 ] ),
      468 := rec(
          phi := [ 52121321024268476396348516724644596780
              988908860 ],
          autos_yielding_iso_nrs := 
           [ 8586879899102103114115116117212213214215
              226227230231242243244245340341342343354355
              358359370371372373468469470471482483486487
              498499500501596597598599610611614615626627
              628629724725726727738739742743754755756757
              852853854855866867870871882883884885980981
              98298399499599899910101011101210131024 ] ),
      469 := rec(
          phi := [ 52121321024268476396348516732644604780
              980908852 ],
          autos_yielding_iso_nrs := 
           [ 8586879899102103114115116117212213214215
              226227230231242243244245340341342343354355
              358359370371372373468469470471482483486487
              498499500501596597598599610611614615626627
              628629724725726727738739742743754755756757
              852853854855866867870871882883884885980981
              98298399499599899910101011101210131024 ] ),
      470 := rec(
          phi := [ 212121481024276468404340532724660596788
              980916852 ],
          autos_yielding_iso_nrs := [ 859293212213220221340341348
              349468469476477596597604605724725732733852
              8538608619809819889891024 ] ) ) );

[1.294QuellennavigatorsProjekt 2026-06-29]