c model ISR_TJ c /home/toda/src/NuSMV-2.6.0-Linux_untouched/binary/bin/NuSMV -bmc -bmc_length 20 -n 0 /home/toda/2022solver/bin/../tmp/DSJR500.1c_02.smv > DSJR500.1c_02.log c ECC Heuristic Algorithm by Alessio Conte, Roberto Grossi and Andrea Marino. University of Pisa. c This code is compiled using Java 1.8 c Parsing: 500 c Reading graph from file.. c Removing duplicates................. c Done. c Algotithm object created, class=it.unipi.di.clq.eps.lists.EPSc c Edges: 121275 c 0 cliques c 2 cliques c 4 cliques c 8 cliques c 16 cliques c 32 cliques c 64 cliques c 128 cliques c 256 cliques c The solution is correct. c Cliques: 304 c Sum: 13527 c MaxSize: 0 c Time: 1995 c Aborted: false c ML = 499 c SIZE = 500 c Removed 0 cliques to minimalize solution. c Result saved! c Clique size distribution: {[2,21][3,4][4,5][5,2][6,3][7,4][8,1][10,4][11,2][14,1][16,1][17,1][18,1][19,4][20,3][21,1][22,3][23,3][24,2][25,1][26,1][27,1][28,4][29,1][30,1][31,2][32,1][33,4][34,5][36,1][37,2][38,1][39,3][40,3][41,5][42,1][43,1][44,1][45,2][46,5][47,2][48,2][49,6][50,6][51,11][52,3][53,4][54,5][55,4][56,10][57,8][58,16][59,18][60,24][61,16][62,17][63,19][64,11][65,5][66,2][67,3]} c NODE covering index distribution:{[17,4][18,4][19,4][20,19][21,15][22,32][23,21][24,46][25,40][26,50][27,44][28,46][29,31][30,35][31,25][32,23][33,29][34,11][35,11][36,2][37,4][38,3][39,1]} c EDGE covering index distrubution:{[1,23787][2,31167][3,27362][4,18887][5,10777][6,5238][7,2299][8,1002][9,399][10,184][11,89][12,30][13,22][14,14][15,9][16,4][17,1][18,2][21,1][22,1]} c Total edges:121275 c Distributions saved! c *** This is NuSMV 2.6.0 (compiled on Wed Oct 14 15:36:56 2015) c *** Enabled addons are: compass c *** For more information on NuSMV see c *** or email to . c *** Please report bugs to > c c *** Copyright (c) 2010-2014, Fondazione Bruno Kessler c c *** This version of NuSMV is linked to the CUDD library version 2.4.1 c *** Copyright (c) 1995-2004, Regents of the University of Colorado c c *** This version of NuSMV is linked to the MiniSat SAT solver. c *** See http://minisat.se/MiniSat.html c *** Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson c *** Copyright (c) 2007-2010, Niklas Sorensson c c -- no counterexample found with bound 0 c -- no counterexample found with bound 1 c -- no counterexample found with bound 2 c -- no counterexample found with bound 3 c -- no counterexample found with bound 4 c -- specification G ((((((((((((state.token[1] = v1 & state.token[2] = v8) & state.token[3] = v35) & state.token[4] = v61) & state.token[5] = v83) & state.token[6] = v148) & state.token[7] = v201) & state.token[8] = v234) & state.token[9] = v284) & state.token[10] = v301) & state.token[11] = v382) & state.token[12] = v472) -> G !((((((((((((((((((((((state.token[1] = v28 | state.token[1] = v35) | state.token[1] = v61) | state.token[1] = v148) | state.token[1] = v201) | state.token[1] = v234) | state.token[1] = v284) | state.token[1] = v301) | state.token[1] = v382) | state.token[1] = v383) | state.token[1] = v459) | state.token[1] = v472) & (((((((((((state.token[2] = v28 | state.token[2] = v35) | state.token[2] = v61) | state.token[2] = v148) | state.token[2] = v201) | state.token[2] = v234) | state.token[2] = v284) | state.token[2] = v301) | state.token[2] = v382) | state.token[2] = v383) | state.token[2] = v459) | state.token[2] = v472)) & (((((((((((state.token[3] = v28 | state.token[3] = v35) | state.token[3] = v61) | state.token[3] = v148) | state.token[3] = v201) | state.token[3] = v234) | state.token[3] = v284) | state.token[3] = v301) | state.token[3] = v382) | state.token[3] = v383) | state.token[3] = v459) | state.token[3] = v472)) & (((((((((((state.token[4] = v28 | state.token[4] = v35) | state.token[4] = v61) | state.token[4] = v148) | state.token[4] = v201) | state.token[4] = v234) | state.token[4] = v284) | state.token[4] = v301) | state.token[4] = v382) | state.token[4] = v383) | state.token[4] = v459) | state.token[4] = v472)) & (((((((((((state.token[5] = v28 | state.token[5] = v35) | state.token[5] = v61) | state.token[5] = v148) | state.token[5] = v201) | state.token[5] = v234) | state.token[5] = v284) | state.token[5] = v301) | state.token[5] = v382) | state.token[5] = v383) | state.token[5] = v459) | state.token[5] = v472)) & (((((((((((state.token[6] = v28 | state.token[6] = v35) | state.token[6] = v61) | state.token[6] = v148) | state.token[6] = v201) | state.token[6] = v234) | state.token[6] = v284) | state.token[6] = v301) | state.token[6] = v382) | state.token[6] = v383) | state.token[6] = v459) | state.token[6] = v472)) & (((((((((((state.token[7] = v28 | state.token[7] = v35) | state.token[7] = v61) | state.token[7] = v148) | state.token[7] = v201) | state.token[7] = v234) | state.token[7] = v284) | state.token[7] = v301) | state.token[7] = v382) | state.token[7] = v383) | state.token[7] = v459) | state.token[7] = v472)) & (((((((((((state.token[8] = v28 | state.token[8] = v35) | state.token[8] = v61) | state.token[8] = v148) | state.token[8] = v201) | state.token[8] = v234) | state.token[8] = v284) | state.token[8] = v301) | state.token[8] = v382) | state.token[8] = v383) | state.token[8] = v459) | state.token[8] = v472)) & (((((((((((state.token[9] = v28 | state.token[9] = v35) | state.token[9] = v61) | state.token[9] = v148) | state.token[9] = v201) | state.token[9] = v234) | state.token[9] = v284) | state.token[9] = v301) | state.token[9] = v382) | state.token[9] = v383) | state.token[9] = v459) | state.token[9] = v472)) & (((((((((((state.token[10] = v28 | state.token[10] = v35) | state.token[10] = v61) | state.token[10] = v148) | state.token[10] = v201) | state.token[10] = v234) | state.token[10] = v284) | state.token[10] = v301) | state.token[10] = v382) | state.token[10] = v383) | state.token[10] = v459) | state.token[10] = v472)) & (((((((((((state.token[11] = v28 | state.token[11] = v35) | state.token[11] = v61) | state.token[11] = v148) | state.token[11] = v201) | state.token[11] = v234) | state.token[11] = v284) | state.token[11] = v301) | state.token[11] = v382) | state.token[11] = v383) | state.token[11] = v459) | state.token[11] = v472)) & (((((((((((state.token[12] = v28 | state.token[12] = v35) | state.token[12] = v61) | state.token[12] = v148) | state.token[12] = v201) | state.token[12] = v234) | state.token[12] = v284) | state.token[12] = v301) | state.token[12] = v382) | state.token[12] = v383) | state.token[12] = v459) | state.token[12] = v472))) is false c -- as demonstrated by the following execution sequence c Trace Description: BMC Counterexample c Trace Type: Counterexample c -> State: 1.1 <- c state.token[1] = 0ud304_29552967085015037795294769993487274108870244113633950380804256944311782204853833152539394048 c state.token[2] = 0ud304_1010332006415128621012608815208711375806185065241195861109111989857577601397876232036608 c state.token[3] = 0ud304_3885341489798431065882031941726189072733889170332995095084476755596159958959460974594 c state.token[4] = 0ud304_474414663616440802377153038630412106716002368611048454630766349778581144519835648 c state.token[5] = 0ud304_7958389745120991662034124611135909195979532561333102855977724089325148470290604930105344 c state.token[6] = 0ud304_3980528560206760654162595589714096888738580699221775520131184639735587224767572725727232 c state.token[7] = 0ud304_238126438583932385021971474767555740071147254325578812674019344038938273527103488 c state.token[8] = 0ud304_65895328824296843177603839097225726958759529922458171806209284121316475382869864336064576 c state.token[9] = 0ud304_963390182456250106119483735583265284278960956750464726450905325159437284329654272 c state.token[10] = 0ud304_60769541119309564231711971269001967806210739163087970751683647658823342760895971328 c state.token[11] = 0ud304_132101514314152691992171996222876067101098711872280712215558792775610151491737052250112 c state.token[12] = 0ud304_497323236415670242901314229571634244929688703656808488334295056920330911312587714985984 c state.tid = 1 c state.vid = 3 c state.target = 0ud304_0 c v500 = 0ud304_32326499829987168943283682492899540574596324782706882182530875259287575707450911534088192 c v499 = 0ud304_8532578773837299636806836020309104283915446145120770116104743634186318153259863152793747456 c v498 = 0ud304_128313281280338734147989252915153817699400775322067974808597859390471244340727790910309376 c v497 = 0ud304_2116611579497897922086271257476531585494205827000000437384284092968315733853484380344811520 c v496 = 0ud304_255175387134150488133885538310897458412914898598954433052386627521043585041014140421799936 c v495 = 0ud304_4074571218715077598644614563160095709046271644734042150436735009046067077403352956797976576 c v494 = 0ud304_518210812369103681755319798430434534221826434920128138622816502760992815079928802438152192 c v493 = 0ud304_8150133217255075247980452801053739444645812206734227296927178799685633087274289291312758784 c v492 = 0ud304_79571793748126559438643263358105309747648157518814117660239792018225513038273622141042688 c v491 = 0ud304_1018774435638124807933578647355045599977270969740161206679274983282373251321817487749939200 c v490 = 0ud304_254753949508689546260620784794115840039822317309795325406453487337465772212347530943397888 c v489 = 0ud304_4009668832556102336128971202982702039205413318849968017879753796699955718025644282478592 c v488 = 0ud304_127874241430896486456267391084894548804086514766022702808426833533489270855149985709686784 c v487 = 0ud304_513486303279780681571223032971368171544199835694496263955688337283250821707072238411317248 c v486 = 0ud304_9947440805486047026480302399614920667270735958590402817995938300677051425886811432419328 c v485 = 0ud304_8148269207963191727462418439204531405021338696179677688516684412829333576169461482505895936 c v484 = 0ud304_270559412371780541114175235405134176875552563051633730304401643773566189965597103401992192 c v483 = 0ud304_4328703396181361485229973649727123619626467299153602622051208486128531476991204119927586816 c v482 = 0ud304_1050370108864191912849893094450405363461544444834187398047206833458789892091761010623381504 c v481 = 0ud304_1026599733599946012550462703537478057438499955586492378444952466657640807917815339541331968 c v480 = 0ud304_7957294147992659975865299712140188553044520916494263492825026386725685259141546946592768 c v479 = 0ud304_95501602741831343959248156062070082318055633334630388371022154294780413738553911902470144 c v478 = 0ud304_4074079844761378275311120272139040356314871229421225346194559475816535821120520401169940480 c v477 = 0ud304_636612717421409495033468371005232441259620072363747767417373407664599214842749955063414784 c v476 = 0ud304_16172719002063708643412286510775327545825100189560481682779743964189038264398613806317568 c v475 = 0ud304_127330289990787973737442130819894383204669043653226550873811890789916568556693395114819584 c v474 = 0ud304_16336074701631644580197215954580037205286695109533694685693337715183202086395830000498507776 c v473 = 0ud304_6392620628834317302195359709755624044014182158825504179586666283003240228953588715243962368 c v472 = 0ud304_497323236415670242901314229571634244929688703656808488334295056920330911312587714985984 c v471 = 0ud304_11936030876469239638557389633507181456055947806632301776097370836185845523938281311436800 c v470 = 0ud304_4122034512553532852809524030804733418164018156333998062219917934514810107445452832426164224 c v469 = 0ud304_31859777895338538585050354744428429412292488074730693902302619912308452369752594516541440 c v468 = 0ud304_1020633555598803583937219264798061485301864248326131822691284479605407859559969520158244864 c v467 = 0ud304_2037043778431627910571634836723093868049556143804792299835489079902788342282509728786415616 c v466 = 0ud304_16411667757510589593291607801665365513382645212033344641589622153250337134422190255505408 c v465 = 0ud304_510751206656105255340500349209040319685253732720466769221614777274464609657416974445051904 c v464 = 0ud304_64653965299533663482991653428711652645862480452209982631522566074147863146843325096525824 c v463 = 0ud304_2166340161998772042266509916079469537706892124566987153298235979534818599553053301533835264 c v462 = 0ud304_16423867247981631657461164045674886438220912652558793058739636923406262848738946550037741568 c v461 = 0ud304_763904157689649357652230437104195923680739521255983577728528685448241772212711511352672256 c v460 = 0ud304_286462327520796288869661201092171991443699517873961309531491645206836064417525694990385152 c v459 = 0ud304_1018580199103097333569352042938907722256919612835132364624398081121498555187377341483450368 c v458 = 0ud304_1026475160233258664360311867592607293890165108143951815057655630539379438074733214128144384 c v457 = 0ud304_1527784753048709942191010134634303796998469958727186023794932216106563146149107333876154368 c v456 = 0ud304_509912216498633328090734157023033383402700811149879558815510632746925136211161088941621248 c v455 = 0ud304_1018537414857323278739861766124994923075893525614423679845902676974398023690478996433141760 c v454 = 0ud304_543077036291439197327076308531234367632456567773841995638999467148962035979552338581913600 c v453 = 0ud304_525173385195818084779802477069174699264997296912215219718688045654575457514189142718676992 c v452 = 0ud304_509321167136298138602263512260980329759337171139932718255019467881026793792121483416305664 c v451 = 0ud304_4137857558342348043353528984550341160016673782516975829465089016473531719604002663331528704 c v450 = 0ud304_4074076323911125498685417435863156275968453429312195717484601494275037044582325075595755520 c v449 = 0ud304_513361913155659455298121443619969195484960727074376226156268022320504010610604664187518976 c v448 = 0ud304_1019512635603452799328523141475101056582661214222209807155553200449114501567712957883744256 c v447 = 0ud304_63719540168932923408013905615096417802172657572236908099156357014252796762170813310828544 c v446 = 0ud304_8179973632114392339162240645569882020440565612465230605485894228492359767403149702603997184 c v445 = 0ud304_1018766653609366231104805736793739259007371683873092498469998932537947158437551053004079104 c v444 = 0ud304_16298279061467529829243365324603210646694010548225410356876808745950548760591628729464127488 c v443 = 0ud304_1084415260327401924394527298394782354893752081512855736005162064890912126702377237454258176 c v442 = 0ud304_8148210078445654621627594947009446514714367195702433467357044960820250543534536656710336512 c v441 = 0ud304_8657406922792321058262720429814743944969856828774034555026282594174517532613346589864361984 c v440 = 0ud304_16296288319109689178268219663965108424689673763921507536891251522429366595119529760401653760 c v439 = 0ud304_135404022032691643754732365331657900452858474993371854016371900078604961659716055993417728 c v438 = 0ud304_8284192923553209096315883775052705575747544106463481092495706359989277741853193362548457472 c v437 = 0ud304_270559457862092415246137209257354796353041523627831008779567402121941661930343613331406848 c v436 = 0ud304_2053571973953449427226116792354508621729443431151904155354422604723017333097892479038980096 c v435 = 0ud304_33072480888499649983498838233520024345720927409010956871838777360251700448130320453074944 c v434 = 0ud304_4074087737331711251840670917177237745756812237598954067078425527995758146046266962897534976 c v433 = 0ud304_15977601721849847013058687599900587226147036887420214174805176320165277700763167720734720 c v432 = 0ud304_509264852444557535908834500413574717462347963918042586547957415448835106548414351530786816 c v431 = 0ud304_4098005635321240021025392137404194010874115468986295276972315906520636496936737889524383744 c v430 = 0ud304_8757770898276497135467078239740589622702864718082995030337247597103190684390503576068161536 c v429 = 0ud304_8402781176890415914714223700951298427563211321984176061380242732194633856959838127071952896 c v428 = 0ud304_4078058385121559080563051352581561331461704913234602356424410539802989141022962159559114752 c v427 = 0ud304_144223738795981685455327669746111433502471700475380605796790845230953441084118794030284800 c v426 = 0ud304_2037036462023943260125520293536075644479156765567154514013134402342636550065286906185252992 c v425 = 0ud304_16296598645407633414839882383260745937304738198607707595370319779474043660077443260683911168 c v424 = 0ud304_16423695812291097412056642212988142219122822091579648067814677022752151040076329726737645568 c v423 = 0ud304_2045088460309567617962841790334305796100667525872876198412483286712442627510907838685773824 c v422 = 0ud304_16312202165639115577367449970988274101975789666449204654853987335491163495011591964038529024 c v421 = 0ud304_8156367708959603639909152005699432310788191879224168661162164458540901043829407244877824000 c v420 = 0ud304_8219774478399793087562791320118865626385856498779486944157880978936993685206443081695494144 c v419 = 0ud304_144223738566712017446235582386124645420102804066084016565107261706215833667572698456260608 c v418 = 0ud304_16550980444845760244169059236893110362567970856829272099024507701750036034315619549031989280 c v417 = 0ud304_4205373619340038612965684801593497971531296657399482217998659823409281462152512792873140224 c v416 = 0ud304_1528314130214509404583026869077671493586484519588164402654583561420630592291884202524147712 c v415 = 0ud304_16054230903612067009596310667271118479624303000514970479866356204136678910082554682933248 c v414 = 0ud304_16298277255392536851161330721387941901835374619822104785135080734983763080608320737075265536 c v413 = 0ud304_4105904529020195633090798263454343045897943826444899669272006545262617938010577907147079680 c v412 = 0ud304_16296785149093162468486855851467170466185455553085443603729116401748015641992472010430611456 c v411 = 0ud304_2041264195183973660311026444901438428109764144958265358897789684446468991712118722044887040 c v410 = 0ud304_2164414954850957643492169756516672664603057170026965496792598951898772029683132899031777280 c v409 = 0ud304_39785936703761161496744718615714842047304273143883750866599140009498155478227451293728768 c v408 = 0ud304_4332929850917542094539427320052228447353281995206648631096335833395146589727115005885677568 c v407 = 0ud304_286489510660314406016919537961580946413042766514433504879416504611039127576775955792789504 c v406 = 0ud304_2037036767440862953183906339616472560596003278869677331475934830425586441911824138509484048 c v405 = 0ud304_2077382569363055164891043177501113387341700516266962427332233875824639005942484529341005824 c v404 = 0ud304_3186878396804422890089321473219770606507438364282386334455744363738665935229358130824478720 c v403 = 0ud304_32827222735178374118046675793328277053450159126767181196620183225458083156773663974359040 c v402 = 0ud304_4074072438365868764628211594021645316869387201586871484810762180780414650162339433475473408 c v401 = 0ud304_65647639496980606894919605172549371523238617040621779040452359486797737500952766273552384 c v400 = 0ud304_16296350947534405173590048469736431310246963729164267420755912857816737809173084597571813376 c v399 = 0ud304_6111108172904217844266023213936239421854018777509266611998453158653193584690444456389771264 c v398 = 0ud304_286458442213318522936819349035753456164058393294526223106072177586845678997663925372194816 c v397 = 0ud304_135520642630072003606480868790978843982440544847590645721384151269826569834713801264463873 c v396 = 0ud304_4040751329177645252717849602434031205765983875432519703269836654173211336802622616111104 c v395 = 0ud304_257613467290638325837972735158994558172829429229178052536390381709314179530609868526321664 c v394 = 0ud304_4074200169056706730230853230493308700613535716490807641010286960701249328325000916728020992 c v393 = 0ud304_127315750268958007671651615434160761913480774623579216544174496901415350373848026355597440 c v392 = 0ud304_8148213842848560846387295175505936972155400828491714307749096134005313686090760117903425552 c v391 = 0ud304_124334721948783162549066404468044734945000135214655438905712454841870700989737393455104 c v390 = 0ud304_2037052489020534982632583905808619983925071433469172354072750196546703487185764086123069440 c v389 = 0ud304_511574656352653369166020592806575077469174149941921868394854989576710006827467671718592512 c v388 = 0ud304_256619032880405789689585423163071092415593710872879644762384859571475381034310480366141440 c v387 = 0ud304_509259115501817020436144570926563479155443387569319037112914779116248796621443046152601600 c v386 = 0ud304_318286901660981009643140995623312357811789526396607146073393192399383922902403058220662784 c v385 = 0ud304_67637178114067458549275817972190721830959211589430559271718479758236879021681977218564096 c v384 = 0ud304_1026490739243700106223457646547497639208106920135292290112078308235185909265678084132077568 c v383 = 0ud304_4082029132047490040702941748293814426198665043087460809164394352330202112845709941669888000 c v382 = 0ud304_132101514314152691992171996222876067101098711872280712215558792775610151491737052250112 c v381 = 0ud304_763890194757072767434889336921941340032689651490012823004503073283782077547617941154955264 c v380 = 0ud304_16411909635178192139706710416187951166640869990189790528559096094121473591693865830580224 c v379 = 0ud304_1019516520926445037143796552357692349655374606991187900524432221613309666760813315750887424 c v378 = 0ud304_3190888095771327844768288272821068530246381174690841350312866092785022318214187383535960064 c v377 = 0ud304_262588854328727393375813715563632296045135762748790454043803651670733380480978213383700480 c v376 = 0ud304_128310381742415343641030413119108598970203886486451974298258709968752676001164435258343424 c v375 = 0ud304_2037284883632008907920357715334797808585849240747780663163021508588122055473577712066494464 c v374 = 0ud304_63665175294391549352164112597829191884131125408114318467911443201776677150576377400918016 c v373 = 0ud304_5975649542143606606688926029865953741567571390827066266531600299438691361098682786119680 c v372 = 0ud304_2293281846004506853807188850297197677134381972151349986072377028799120242099835863193092096 c v371 = 0ud304_1020522852825762398142641840584814265264809040627603503875213302321507950142085056272793600 c v370 = 0ud304_255748970425213268050817711166688034262586470252807073555345603914958618560618478807547904 c v369 = 0ud304_2037533360517454162776488959704673328430132850057453294429410047375471572035741238039674880 c v368 = 0ud304_573165278488258928658493265754627129287860037016074536127183706425472257560323703940579328 c v367 = 0ud304_497353590741607068847804780724917908258424579880874068940080534666417989365257994240000 c v366 = 0ud304_64900684250503605597273426699980260701198743630172097541512888812240178577908686617837568 c v365 = 0ud304_1018557086335122310611566225953523709648834844654886962016142617473971264489495631035891712 c v364 = 0ud304_1019039594779627180381031858604458832757307650884203034912625381283196934491041413331943936 c v363 = 0ud304_799703656721242109442253475649119221388077593128433986857549274607485243203124890645299200 c v362 = 0ud304_256685326397475425888979300963713158142634610072723742485430462414278770455496074505224192 c v361 = 0ud304_8219776428658841554230489026561571578570385120205034770227768270810632905993745814167486464 c v360 = 0ud304_2037168077989603419472151545675221886293399474417800051200435238826939496569747959732764672 c v359 = 0ud304_4137760413514911216066568068671229381378217143172927967743204620164726492801574998896541696 c v358 = 0ud304_4076061731285771310602577197945871253941792686625076617198041221295942364059950028584648704 c v357 = 0ud304_2068870495562092164646175019587455213148140488187660358049582345379251229371455230797938688 c v356 = 0ud304_2164599932897391864213547075195137370372312478710456663310635244210920377978860853153234944 c v355 = 0ud304_1086652760697232569031003227108316995303928578506321787265667050752862490678823708526641152 c v354 = 0ud304_8148206101574688563062785600959556260580041996233076047527474404362745733333183224233328640 c v353 = 0ud304_8152246840066719725061542295525205612707256417451383708412282020056134277651416012617154560 c v352 = 0ud304_63688457437014056315697405247465836248391037617803119646646142833792236664847115684413440 c v351 = 0ud304_4713693756105418081981613292200777920976616881493234800893249348133258070475496428897566720 c v350 = 0ud304_513299756999653983503386535615102442839263878613624871943319783744920067670568853961703424 c v349 = 0ud304_16300299907606025598664190307801110101154659076987661474781219999008023333677010434113142784 c v348 = 0ud304_2552885656790299073273173043367306943937020508663172237622952080833595191563121023269208064 c v347 = 0ud304_254630498790677438195380385088873552648814095597909963458383616672263544876889754583433216 c v346 = 0ud304_1018642336052436989719606369683153597868394612644244107633777235718684684958945135613181952 c v345 = 0ud304_8149637817730894555171243090242702068653651993958758612717694976677678460010261986156740608 c v344 = 0ud304_8150133262787187905336502377541233390686940634034999828574835163271513073978519385035243520 c v343 = 0ud304_2041018569573673373358307860640092804704063280597407182337010453659724500970191291955544064 c v342 = 0ud304_2291673254486182215195198522864400506851349522316638410957512183358977842197166185265496064 c v341 = 0ud304_2196179897652848331352437361580459571706494300015708096602875051842154271849627713909293064 c v340 = 0ud304_2045010905324929102890288079689334208668549405578951307234890795505349309323062118056984576 c v339 = 0ud304_16038681963693673175648948328211175642818732561815947454366479342280216385772728103206912 c v338 = 0ud304_135271920366452921627758541021551934643756003650531092395566613476422030387359591489863680 c v337 = 0ud304_16297282517920103455508688560588157820858081474628773758311626156789971644637100151802953728 c v336 = 0ud304_4077055922797347582153170915390293189049332087690346251255365476862202126707294300358574080 c v335 = 0ud304_8148921003251599786954937817817101605436492371976019998316574579025668983342413683789660160 c v334 = 0ud304_16296412202254995417407444952260373411976440371383545375338525059851089101359858970416644096 c v333 = 0ud304_8149263854199100574807391902362595171371654058000284352929380447178857958761589619386482688 c v332 = 0ud304_16297290470657888807642937741614192980364837275933195937623848526711000579397042666372857856 c v331 = 0ud304_1020569507255501120183268681995271830769651010827655226959156314781754395868980895769690112 c v330 = 0ud304_1026506242682298785740516807414127896606078258165879345647521132980110066461552454160875520 c v329 = 0ud304_16296536851721736464688992196720152257805976437388672425354054257259118056995006494155997184 c v328 = 0ud304_383937423846400308507316321333649827285864243839263823148042926344250543055606625945518080 c v327 = 0ud304_8148145855595850110128067453024799844385848561784360162774254340259499375519785396127924224 c v326 = 0ud304_1528320929540753141409608208569774361329295144160625211519398314047202777621554046263361536 c v325 = 0ud304_8179972842894097645041433584783437819850130701658271632214137494230500547122809865076998144 c v324 = 0ud304_262648849895212373103874819625276766603614783268422481879693650128044128845709362558140416 c v323 = 0ud304_254629983212975463643214604586859662444283050856541969220361834887826631294403022371684352 c v322 = 0ud304_127316934053978246116544550376436511225378278170459018198274985880369525776047492701356032 c v321 = 0ud304_16302310084745776607564942808798287182839308845472338630575844229802883219215215940736122880 c v320 = 0ud304_32326496278412200842393866686092673996206277503286514416794905480455897551813048532992000 c v319 = 0ud304_4074324507450770151557375273174051127978796718133079723896739113244266328848329234075090944 c v318 = 0ud304_2546419346877778072368188354521107691299224605368598323940747348118990550474719707717959680 c v317 = 0ud304_8150195369380068577843370310409433197948156002463296163372081939295638721633704432866689024 c v316 = 0ud304_1019512635131080780522479093893755743225622789263239079904530969441562540564206743208853504 c v315 = 0ud304_159392097810317730371536871190846115259155836115854990147987056601130180890301222923272192 c v314 = 0ud304_63906400247646883492370913399250321275058714959960545658061514640592088640213434698301440 c v313 = 0ud304_79572264201597102254865657581713098428703197115912726608775875940149365029081738408624160 c v312 = 0ud304_31906393893383978372759738865816761779369320511988013021072306993392357477288015501983744 c v311 = 0ud304_4076186066898624828478792072798624976080914379311231676071025251712219816280594334441537536 c v310 = 0ud304_17905822487772521209259035210453682377946564604769252390238980883489881008678139231993856 c v309 = 0ud304_4145686809850206589958527597311112551394655246027762237755674176235483791638084556370739200 c v308 = 0ud304_16909483293706191012715514155467601171395503325777603289739266454346658648871736363188224 c v307 = 0ud304_1145837169350156613074528449522847181509099535188018245442817992982017047979062515445268480 c v306 = 0ud304_262712942421063384989548513253746851219047306311916583698325002209523493004669863491272704 c v305 = 0ud304_1018580457121226614522333489383511830913976538484520954022366308153093742943453231320137728 c v304 = 0ud304_15929919064728567782943357985731436622296148735989025980857380745680758425572559110012928 c v303 = 0ud304_254878280143518115693090144263313752412603561480504654711081324593899563434903845428264960 c v302 = 0ud304_31833543804781804529728014177049345350815785870024689438785868415459628613966530170847232 c v301 = 0ud304_60769541119309564231711971269001967806210739163087970751683647658823342760895971328 c v300 = 0ud304_16296474337601311583044486193971403357716480839500244558794697532176467111696491723324653568 c v299 = 0ud304_533130752548361899627687777128077622252092509306146168797881720676083461730787940221583360 c v298 = 0ud304_16554911434960347360684445753776032087237606077112222110369426359159748352944789152593870848 c v297 = 0ud304_1022506287540082729976247143824714341338361112096725948311717190111505164885431612958834688 c v296 = 0ud304_2037083571781703544327205588782835131720023675404091059725473020046016072822584590657912832 c v295 = 0ud304_8181966265907284391724116838070092517190385048798466302135693182558552870028902063214166016 c v294 = 0ud304_572920815234600248555526668767102637654151425770201116160084869958560265099732661236137984 c v293 = 0ud304_4201388659043295893493459653797274350995642171117811942891785822542385601293661414535200768 c v292 = 0ud304_2037657637972312827796392062894030050791397390409429013863990720618228015497123713769275392 c v291 = 0ud304_254637336014332934281905722230828542640463940984534464379933779714788882517739778019950592 c v290 = 0ud304_15916346942524086611304423244004228720531044929344819005127185607103845593820218800472064 c v289 = 0ud304_2038047135493367225925460058213681720945211622812351940857974540617752971143719545229803520 c v288 = 0ud304_1019015372173194176122339539011872095351740243543117412085365182528699135602887529768943616 c v287 = 0ud304_513270606295678575935085162762474641368197920889293498702618267519733691311563880632680448 c v286 = 0ud304_1026490706992351140096047062559684531911844177456578877180090596985514047725892543734349824 c v285 = 0ud304_3979572402825353120328118091878702227708167522118376911636256142398400011720682433939456 c v284 = 0ud304_963390182456250106119483735583265284278960956750464726450905325159437284329654272 c v283 = 0ud304_71616974853408957059007028203743698600253148355599131851638532010777264657985788977348608 c v282 = 0ud304_4075315291233753879085788383364125664011048909459112209004839069467077244765730037575974912 c v281 = 0ud304_2237954816046454335342977825360229432026967217552027664762777388625131827067103930744832 c v280 = 0ud304_4989077627786577778531877131821920924950934193633738369107039027609308140993511054901248 c v279 = 0ud304_8689483815922503074244359123243556103742270167585280894188010408185647308249078533866913792 c v278 = 0ud304_286458203261984106043883270011136594000831157551963998592932799283031137534070539151212544 c v277 = 0ud304_1018519930836139806126556226503386818998118272981990272679858996523636822583213404649947136 c v276 = 0ud304_4074079859938465652596027005403155325228790031984406816970450687809144752165866732911591424 c v275 = 0ud304_7988259257326185889059975832772635865564329065920705965255839602789749639263788835274752 c v274 = 0ud304_254878280113990680624753285929771658669823871305450749646946976039834952025608956040708096 c v273 = 0ud304_31955052619394135611098500598292350154550145307023286112648651376573059081423357292314624 c v272 = 0ud304_2053948976950931073463620081583982684477908608799043185020781036691287638629033869855162368 c v271 = 0ud304_8148152161740166742666160605396971202944372395221284585464685764417602233797923277354565632 c v270 = 0ud304_4583339749710122708751082383006794578644669120714558410186991018476888460245599018540859392 c v269 = 0ud304_4109895012724645122036201701623743135044240956547977601463661077932275632047702859298373632 c v268 = 0ud304_8149216273759417190443969628569127808812695894406147408795850448002125212987876373610627072 c v267 = 0ud304_541091574155018555715160548650059248603256316669928622962067116450123693208818737337073664 c v266 = 0ud304_1022497181142564644962112738613052631482085471562323318682371616479868509806313899022090240 c v265 = 0ud304_4074577107527425899231804956346683871151394752950487054771310080255825070135768599519821824 c v264 = 0ud304_1018523816296456698757811189859651078853231168051426322744243681224517814006707752666136576 c v263 = 0ud304_127377160553690688389485839441873536727791456372604386785194170849385960657543021706887168 c v262 = 0ud304_16296540486644760645978966878171547786143501523998892525067354376508078215884245366596435968 c v261 = 0ud304_16296295824185535910348387652139217360613385463493436810819573689955648066522863409012146240 c v260 = 0ud304_16296361692804077997954985850051195401658396323169467808301467691662006687348825858978611200 c v259 = 0ud304_509258996040160481683047099017928685589820598937975722534275453045859699837195475186876416 c v258 = 0ud304_4097943475605193198013206865445820178541741843298969363440099870254808089189194388356464640 c v257 = 0ud304_517224058080836500731532504083298915460518453118447391057318692525054127553181923034529792 c v256 = 0ud304_10698666367047715462615996590888599812134439826061750090088473206295987803933878865199628288 c v255 = 0ud304_8164089362228172443502672864205790051289913248763916302075767323858847951976867735082631168 c v254 = 0ud304_8156240949532827813252446572279492956089542784899616579849727606082791938360936103457849344 c v253 = 0ud304_8156606300988266260050514710590952434494019459383348008752998441533731326806452698106298368 c v252 = 0ud304_16304742325615812967788674553295195933663931278489684191212774869600095493997066223798452224 c v251 = 0ud304_8168223333854624011817720089050105330660571298707625098769449163141499870621527081972924416 c v250 = 0ud304_9649550045426462154127244975060929617315727854652860229086668983256074426969314531427221504 c v249 = 0ud304_1020538614296663135802756896528870509435753718980504939822979612313286137241367307161174016 c v248 = 0ud304_8164066049962941042222164134006728917154951873885008297789094705229133394851756483496902656 c v247 = 0ud304_8152372124215250728281685704722161827273612280482275387277528470479797802012070504443150336 c v246 = 0ud304_16805795960702945219182501451881063717239558018154128789792041080813581294188381691382333440 c v245 = 0ud304_143606091386502826797797499127096259856950228478281000306579702986944330517820774629769216 c v244 = 0ud304_6174770287133299460928936645411103912635967920577385088717245118043084188329592860239200256 c v243 = 0ud304_2037084543353683098617722293255458175262928895358515361474163627323367075786757721517195264 c v242 = 0ud304_10694951984125896127391856325541881018330694011737990943206653200964987936313373294612971520 c v241 = 0ud304_2238197693884221185962300724522046318368579132907647080747956731180153018571758860632064 c v240 = 0ud304_31953200064537692346567815709232169103738567320128502142393012752608195277530799573827584 c v239 = 0ud304_254755774315962235636905764730014298936695979988407068347481308893320487983778426710392832 c v238 = 0ud304_318286871318011291741436149869417087704337924314292477757347425207661906095908340625326080 c v237 = 0ud304_135279692879874266103424144673993770432739309605952118870439624914516455276536995646537728 c v236 = 0ud304_4098502956776188628691532431549230528991696912923497951325594108447520163000080160050380800 c v235 = 0ud304_67636081687599963200334127292692940162011917792715332421240222888766234904917118709399552 c v234 = 0ud304_65895328824296843177603839097225726958759529922458171806209284121316475382869864336064576 c v233 = 0ud304_71615031714748224824637673866225332254940629246592962920778246376989762636538414601863168 c v232 = 0ud304_129801486594276073569252421858045891393649098932244344013025889154596466887463080449540096 c v231 = 0ud304_159144923021824691468219962264004537269416494533779685611659711215116989965218781388079104 c v230 = 0ud304_8275956099944413421027031350641298445486876188550222090706932284578922530369700132326211584 c v229 = 0ud304_8148152161680765365552201538163665228485171211983865507641501824165553545161455920822091776 c v228 = 0ud304_8148148763908246073628954073306380602119374150488025735901832209448943346991494280666677248 c v227 = 0ud304_2068872919829852377071170363907641532920684177437324588643814437955230802845075026883903488 c v226 = 0ud304_1173682872107531713292516357531453035142464234809900340358134875345511134049833966773469184 c v225 = 0ud304_541150332345146743459304021541430730394581088883522986360523013854648645118554223293759488 c v224 = 0ud304_190972246332678833515060690335177982689674527040280029990715648565501687864286820744298496 c v223 = 0ud304_6302212189315362454193605506498746184068671488178324174803392323531809346592521548703203328 c v222 = 0ud304_254691723629512545340357871362714761302824928235917502193597078855901539822951954988924928 c v221 = 0ud304_509259973010353194192056035106168035831442396052469997985057826624142624759131583755059200 c v220 = 0ud304_509259237391532147480701832291117073699544845932949563731300017210665628350261075285901314 c v219 = 0ud304_11939643130191338408921131809272233726124540983191881534618247343732421645828614885736448 c v218 = 0ud304_16328118532486180379536379315340592397556062328891822237897463418975424349979365094526550016 c v217 = 0ud304_73823315042846239898648470698922223900258817555927058927803528317373373582298008518656 c v216 = 0ud304_16841362091532896603079083137723472870622805354863330098257534674350610741917149341805445120 c v215 = 0ud304_254692149062211790039186979665879756478316493331019237283334215706362829868810946060746752 c v214 = 0ud304_2100697251139466783356988843438584608778007921095942200179777190489812536410981659943370752 c v213 = 0ud304_513392994435774814027523459955689954030700588891374677674634699375988168428445906356928512 c v212 = 0ud304_33849062896860561325913888053153852978864322958920675261678011244747609061592836465491968 c v211 = 0ud304_4137744990647793519877655932132125735783435187879298374250513692853012350060270966303358976 c v210 = 0ud304_254660640467549463219581111212280645719731771789133764427533345699034681665158628629282816 c v209 = 0ud304_4075315262657612790417866974814456414645251302932903301607604703967027267292660517625135104 c v208 = 0ud304_8148268238518472624084683459827352711488641499504920651582994607961105801373762815757647872 c v207 = 0ud304_373481904090132321587411924047768811501925886872202977150148848080498907223880844181504 c v206 = 0ud304_4078306979391288383910030754485034643308709609131951186563795926477371115918778180955013120 c v205 = 0ud304_4111907373002362876504097512151894891458667181932283029282421414129721698656797759222317056 c v204 = 0ud304_525173339664458027194658719296348545781715878699037058431404537997936200662100981099528192 c v203 = 0ud304_16948906239694451980933113113058241333007387735490552132937293018223300062653796413452845056 c v202 = 0ud304_63907023338789502258767538903030006093821027920510644380471219982422855374636704965066752 c v201 = 0ud304_238126438583932385021971474767555740071147254325578812674019344038938273527103488 c v200 = 0ud304_8405807859113759114226128642126666063850992579920475649768372793708960865043683200276103168 c v199 = 0ud304_4594352770741015469235541666860063973351986714523318243797940013403072868852315663793913856 c v198 = 0ud304_4075097685764411174775727554429164078688413941987851046196384863037930382876323991986896896 c v197 = 0ud304_259603218868335015032033376193000825252098487274740547151637442889159483974830110151802880 c v196 = 0ud304_4074088222639517952231530836190390537180886476175544347145893997524605534462484884679032832 c v195 = 0ud304_1018517988642569569599636577144287704970903588479194458571274159097009951302857882618299392 c v194 = 0ud304_63843870488927763510697255625435244205122745264964362068238601316483764092071070138368000 c v193 = 0ud304_64683118704356962173496744588743032367809046547942000257552031006628491881959997761912832 c v192 = 0ud304_7957295096500053635388428396124529124897428291229328967219089651350983514517574541901824 c v191 = 0ud304_511248317392725928725011505177881437701498869442197007310140785791644849088514289309843968 c v190 = 0ud304_127594553564617900740401892927792684761365396838021045374768958480606056750384973317406720 c v189 = 0ud304_1209494239357866615742269941217730005331182840358426238692342813610206932369819883605590016 c v188 = 0ud304_67635994315029445990820561773423662054557421985330263955732736859101647797464650569744384 c v187 = 0ud304_8148408108455558814606245883498929012530876347410908836310412843780092707641451558303956992 c v186 = 0ud304_64659798999253246393226988633538405560470153513240311783022549075807255140576857753124864 c v185 = 0ud304_1147822037252478249550888523344484986357647101341460091068252087983387738052623592182513664 c v184 = 0ud304_1034447907708107722463039900645016232285486603787022704363424887943702732406473166505902080 c v183 = 0ud304_1784895038158503146274408112633520254601892827997834160764496504181276610168392368481370112 c v182 = 0ud304_16941059489128973812974077775545103050524698397703657720708928591390639406633722488817664 c v181 = 0ud304_16297317427093316727385010430942594377920040776620605871975441220531162088472761674657431552 c v180 = 0ud304_4074569526446115182021613000486452762630412816664596033041239069160712227432369910204858368 c v179 = 0ud304_4074817967893536102485883844576766160272577348237909119284402573270363244732125615080079360 c v178 = 0ud304_64156642066597639487762935291971779829166510147087958095764708853165440192070695784546304 c v177 = 0ud304_16336074703054490535746681774815627795652865956830102601390254615890044846748860464653926400 c v176 = 0ud304_16296322780620497040803357007672115511111825256358914696511794295536437597595524689098178560 c v175 = 0ud304_16304742412409799795992670742682743543253958012714662499585730931985578748991736937822814208 c v174 = 0ud304_33849062778401635588561565447937490596698423071882919291669371097065520606693615464349952 c v173 = 0ud304_16425094559735001385493383933839822554860938653445040811371844858411437910208552624971579392 c v172 = 0ud304_511311425695154168412065614348379314883589435391112665279023049869440787490257735411302400 c v171 = 0ud304_8219766707783146922699072878698254183267667613286686869519637847021367304403825907722092544 c v170 = 0ud304_7957657987981285850593378903295879214950490156197308332037215927186288514497962831773696 c v169 = 0ud304_8152184899482265126421586025996027149573400516201164693493480684167124503691471456852508672 c v168 = 0ud304_509260936989656089224464329261393302175396664628142557931203100499872268910052598412738560 c v167 = 0ud304_16296412657508298160453623892899794589994915678598618640153462357441676839766150367305271296 c v166 = 0ud304_8148144937380815054556689349049894296353058612576349747283586472102273816433310839380901892 c v165 = 0ud304_16296322778723359447204618460724915350475828561814122695369233526794612568494187750780567556 c v164 = 0ud304_127688226630271666513504726663197345712754576261279545927164246226129943375731019929878528 c v163 = 0ud304_16300281998660055828263911717856026296682048502788675774875719978670898230282070840087412736 c v162 = 0ud304_35807396335969282965448695564277847029663665593805460870356128768853213870951622835699712 c v161 = 0ud304_16297282457682278217705680488726011029780955978358288791757565322325926391678573040791191552 c v160 = 0ud304_1050533201869265220171070614727591677501576635529267434070791211684735247938622608891707392 c v159 = 0ud304_16314440139191483857257703597659821807701523975846800918090368395745664180770121383311048704 c v158 = 0ud304_131293349767604211523291071693532020171219064262660958978654899081434186022885710907834368 c v157 = 0ud304_16304245075418737231589310198615357879732516688829583730256408067503685601214983631383035904 c v156 = 0ud304_2039025292994808729420082874046856868340627546881751949895129750916051748244075241329917952 c v155 = 0ud304_12731474882448444830594953252653867871536580298472214517812346864966833946918972260941299712 c v154 = 0ud304_127314748765921469487984033180439896436117543084600348790796671394873000225193050675085312 c v153 = 0ud304_4074103039639872497546916903833699734715395090723728405646777893145795988652514615408723968 c v152 = 0ud304_11939643604511013013672481973370636387561025766953167180589458643238907492863548665626624 c v151 = 0ud304_127439081229027038567042994282953397602152221976823209625648030884472624238351745753808896 c v150 = 0ud304_64154705205836723883948359191911386121505177081854215982538106366600012830622518578511872 c v149 = 0ud304_254882052535035336078117045493535772411951299378133369123744247526675792794282026562748416 c v148 = 0ud304_3980528560206760654162595589714096888738580699221775520131184639735587224767572725727232 c v147 = 0ud304_8148645235329190433745268763289098443430896157063436699273490969959647624776325103609708544 c v146 = 0ud304_262587657233080736204887156513898977392872027910151293041199226235419195688810923891359744 c v145 = 0ud304_2037105912417501919372525278683076023634010393214694450540745767011140294225013245380395008 c v144 = 0ud304_18401202701197648840746518649407565225018180086607926336497259656341089395531886549270529 c v143 = 0ud304_16360442522164372478787290998381697961682617247620744920313941554660955201307380104967487488 c v142 = 0ud304_65770999023063109473658635989991182463792612211218597695354004876836296997508432537845760 c v141 = 0ud304_1067259794118301564869086199357548677413254488129683395976764420995427144313923742929518592 c v140 = 0ud304_4074569397563983317101543584915442974374426398507680896531723791813572721893002170911948800 c v139 = 0ud304_32831108072904475549365139801890772394409667147677581725267005744008317933441509970935808 c v138 = 0ud304_254662527156750832385190352078593011170778429443277954926561501585293645782171725351354368 c v137 = 0ud304_5124418628708439982699837377737997029490101954139770849282258788371018036720455886844198912 c v136 = 0ud304_573942112713175762260857925067797691669260961484264427368693929991796747138987542295085056 c v135 = 0ud304_7964946252632253498541558941719144347942953743374892696445326467632669409509637909118976 c v134 = 0ud304_7957293199420811818239182391839355883225146606952576402335599727913117692965694667227136 c v133 = 0ud304_8149138555675675891452073989493066334073989008720047286570256376285910170159180080035659776 c v132 = 0ud304_33849062896744769235810694182788452752080553949249522259630811422979406467455170792914944 c v131 = 0ud304_2051944021581943545222024709239807933592150007062070597006899022688500822443324902211584 c v130 = 0ud304_16296319386754361717471857072886689585082832153539887519187759323221532946092686830225850368 c v129 = 0ud304_4074134604691283716823990034269581993355201342859416384364216825605899138298521323200053248 c v128 = 0ud304_48001406132289940773545573012302328919666365154372494188137517557080458848911095951785984 c v127 = 0ud304_4076064178596852213761397355821270192067166763872276325280698660500211508763473739859886080 c v126 = 0ud304_16360943959588025696650571922370585093117163588338987368800492501862355210458447917961183232 c v125 = 0ud304_2116611640710227969627049668301397815500201661420529144549221378882480007505742666194223104 c v124 = 0ud304_4090048583114758639929175309586377767850979494956326146124873620085202622542930221994082304 c v123 = 0ud304_8148656785251096465705575406228367743091694948957777884664918148478908904775686955129110528 c v122 = 0ud304_1019016282797500288286360311561602198472286240912939898900163631402072952682796778782720000 c v121 = 0ud304_636637858355680736599844546888580068455695706151185852988130144133102239633543463453065216 c v120 = 0ud304_16298284874297096744491407982068195214870156328774857077625727631598574075030237158660112384 c v119 = 0ud304_2100817928269113612333888724390076265861406235245231523690852903416614460924165766680412160 c v118 = 0ud304_270543840607043421672834366637286004227191837678936851865897123792478665094319039525683200 c v117 = 0ud304_1050346722733319847686431382057291310361059830626167761884223271949104286795927548315303936 c v116 = 0ud304_10185211116156974255087631633243068699138273875084961804305698843097336731621547696996745216 c v115 = 0ud304_139250569037484452296300655484777516154919742635862544920880505190857743821447884835913728 c v114 = 0ud304_1084357048038832357856859991870922151769978567225028639854175823764922253873737255983513600 c v113 = 0ud304_2037047639952370013845255345123195765644043242182000250477332636083020321665250564574806016 c v112 = 0ud304_1018642561810680718596249300583410199323138422999482850806301227832402399689834627332046848 c v111 = 0ud304_4074118641225527329470984953586846797094754143325023347541611240368074071611886881810153472 c v110 = 0ud304_4491450486237491568608430697061640850950258158155427772597459260114144775402718205313024 c v109 = 0ud304_2004836223557317311859607662697637930648365349383332893789224959318970402932579496886272 c v108 = 0ud304_8148206070757317861342451516774430847286414482929607706403964440205486835053987063327096832 c v107 = 0ud304_506065276071676352918699517434683819318710695708223366651691090918265323095468252594176 c v106 = 0ud304_16312210168699214328002632878313949212405961526993208144144035726429888127008688256013303808 c v105 = 0ud304_68133321331471644790359626371628492180164209715793486597887808789676794642083831428939776 c v104 = 0ud304_2069875337074493370620641392866254559969712688720837331983815059502703266989336829452353536 c v103 = 0ud304_2547301278602525096595825825284324180969556295623086505047094695251610148618145327847833600 c v102 = 0ud304_16296559784795144396906964692183225460692443715882987612582784594795347064884417174932815872 c v101 = 0ud304_509771864421983226026973567026658990659225147107385484845395770929070190696346917785305088 c v100 = 0ud304_16869204179028329106521288043159187463178609623321486817563687791038899806535116210380472320 c v99 = 0ud304_2037036101551125051009258092752953221323038877410887355767741456347584165895554325433810944 c v98 = 0ud304_16298279048191285162722241875841070585802461009763205691545179448121115969345694618552893440 c v97 = 0ud304_15945441448198542533634551576142879599446745622084739029885924142145963612726323557957632 c v96 = 0ud304_8148151679868003933469805990234552503648590277045609375617413302442951341248055935391236096 c v95 = 0ud304_509266780188256540649769403589047762178633140160544025249746237787752843189468224217415680 c v94 = 0ud304_17442184094240962942632470202676345443630482630181432243497698964417765108735661453531414528 c v93 = 0ud304_16296287811891242458782491978315046121267166336667857762659766156830303458234666625301225480 c v92 = 0ud304_63658353183507059365275088331598762107378750619755016208208638167002932890613938892308480 c v91 = 0ud304_8149138567730786711688641824608580788028693974539310273452923522329673848025730863608102912 c v90 = 0ud304_8148143921463614426893871356036019954218694455804907722417785717705876015453135357662461952 c v89 = 0ud304_1038412496042111252581845147630555543205224063119563843437437071744252557788515537589895168 c v88 = 0ud304_4201410014167121522240452440545943978314962315996596374874018697119629507015354411426775040 c v87 = 0ud304_18396988966573441822745237178954727993156346851606680624410973894582161026727976789774172160 c v86 = 0ud304_16329111265699565187508091715165148382863153318296673747900443265161987853520714751558025216 c v85 = 0ud304_16296598645524583424003320512935954771122159334339884666836973606973805243867491909679185920 c v84 = 0ud304_8149138612637737900011996343169566047931069626366019571517120415907068139004756553759719424 c v83 = 0ud304_7958389745120991662034124611135909195979532561333102855977724089325148470290604930105344 c v82 = 0ud304_18341778297696560863849199181893320732314005498796514927653993153849532814444100448451297280 c v81 = 0ud304_4109879227595258509179705104308194231960218433799833072297598405465165381640407590144835584 c v80 = 0ud304_16360073423849806162407728172979212646666186330939870440951507214823353881366297315276488704 c v79 = 0ud304_32326010396510943089979500973199462312135770244639602528122341368964009072590280896544768 c v78 = 0ud304_16312361454995175828425031373444864102809508293597056308005291778769819775749655302431047680 c v77 = 0ud304_4074074866672774138979837451971733044702956460094838010744876502653563431858435504155394048 c v76 = 0ud304_541103347779801823415599505845015102792091473744153739092127247183089698090453864611315712 c v75 = 0ud304_2101874554553057252102872768941350248083313978531650390786302156192459125899614639183888384 c v74 = 0ud304_16300328805116608724694964827705958040402274461374924168443027756523996866582387763387039744 c v73 = 0ud304_127346074061424317045201709419929821425944376317289334324805504295195262459702554189103104 c v72 = 0ud304_2039025277342960075446350318863778062329062998834260112676723864049279374907017817525059584 c v71 = 0ud304_39785858919267290164176021957879840311936387458120983468755033830857559103351561413328896 c v70 = 0ud304_8275476145467446415122993880968341820481225725608565894641572528981104637270062924707135488 c v69 = 0ud304_509509659086590114801301140113300009477706295670054231668247392137241764407336724301086720 c v68 = 0ud304_77708660237327073222608570272446040649643043254391041134426447798623583352568460607488 c v67 = 0ud304_16328241042043196367662693267561699754398186361815718159273500413561947147414304507908063232 c v66 = 0ud304_637607485474187463171144490648322856596609426956208509687348571409124926680203780335599616 c v65 = 0ud304_509321175139847456283455985346724742909030820533270405236247828760552833636162877331079168 c v64 = 0ud304_2038031595327694804911174138036581943148975827573171337184129171583333773848714683772571648 c v63 = 0ud304_8404782137221765614513742672754497688892348588004954976828334929264977428948842740851933184 c v62 = 0ud304_2041045644931051603095024547928110172608328563491588888413861572389419162287215309718814720 c v61 = 0ud304_474414663616440802377153038630412106716002368611048454630766349778581144519835648 c v60 = 0ud304_143354515647299468831850091056448260040613204187841665875536624407970757478287626869932032 c v59 = 0ud304_258615891551445944033888994595215798137154126003969952902880142567237572874804258626600960 c v58 = 0ud304_4336658623509064040043277131280474777806720894999811450910446586054937654732179069422534656 c v57 = 0ud304_63676800951238930502510748666063943863046669783900865184043188882551363491809728575569920 c v56 = 0ud304_1034433789819693822922626049645587079138707978343542915404053522188664687728647995593326592 c v55 = 0ud304_1038412867944069913684451167983443394575527810244623194800707672973432210453516507427110912 c v54 = 0ud304_8148175476316007443334528209767824480792040227406136202476884574674890281234889314242920448 c v53 = 0ud304_31900566116381178692764753604084050351806661486883974482792622121013686065354225355849728 c v52 = 0ud304_140964911550082104647505975435609220673958625207048175337071605174441649279042209186816 c v51 = 0ud304_280494206102142183266678901278966540594964075341491222530888379250404366541674432021135360 c v50 = 0ud304_8150265303925654070178478615786775708899738623939856695602208791929842035563919532793790464 c v49 = 0ud304_17060300693320215820891200153298574601595576024675018247338471429822213335340256595906920448 c v48 = 0ud304_4075191112090982348267267640457589392806585320791209865444163824780389616364854146991390720 c v47 = 0ud304_2045024230826846579384120363275552565903307846362671472753538686329482087636076370920996864 c v46 = 0ud304_4328957929493237775865740532275474880670582612066149215039566129996851747348523662671085568 c v45 = 0ud304_2054943500598916250847340546346076928311018356034456138800739190118476381428249757931798528 c v44 = 0ud304_2038031138828741012520515228075888134500031297689746018170429473169389669115293823282446336 c v43 = 0ud304_518210842722841940285441178984580580665221185716630371134300588783575453831165947123073024 c v42 = 0ud304_16328121356449590240098540601642663095047532444109179021384501440647042510868042586353827840 c v41 = 0ud304_16932864964341217857879708676149500483711716716562533276816198337644307211423583414914121728 c v40 = 0ud304_48001406132290859423808680793508593670252471765210870613637290232405054764863742709596160 c v39 = 0ud304_8152122737872046978435214901754337400035400608468559471696785984261626644344023330085404672 c v38 = 0ud304_4475909137414615275765215457946352298989839296693028325300730377103858571498861403045888 c v37 = 0ud304_16332095205292171985961479569974423975149199259877155376350447399793950674119236564578992128 c v36 = 0ud304_7961087474542528238264274557917683066277090666819624520597167624600433828923281047027712 c v35 = 0ud304_3885341489798431065882031941726189072733889170332995095084476755596159958959460974594 c v34 = 0ud304_381945256737109711934052563839816553401465434501261346663248491183989059808460490191929344 c v33 = 0ud304_373007663693611951477860516758641903516492195553658200202599569134808717516622081818624 c v32 = 0ud304_3980528568507549291836328319956602652741673978438098496322834907204590825690132817905664 c v31 = 0ud304_4074072924492524126878969999131904984858668352953017832967384477443889448349921916638724096 c v30 = 0ud304_1018797736282982989287235182415298980870991830506640900965469934315300237951185414753615872 c v29 = 0ud304_3055553972120038056629647172769211964791514993335704476725288495820884274669326517116346368 c v28 = 0ud304_15914952664850682532507237473353222740246645791022133591847389250546386143804083327213568 c v27 = 0ud304_127346089711912159340434470161852123750685686177959098718576142011496623799893273390088192 c v26 = 0ud304_525188882794191109184784311969658413169161329432203083404182088524070949954568039537049600 c v25 = 0ud304_1275138751659525582816044455831093792246854374466227091398911650311761468332046695339655168 c v24 = 0ud304_517216226634331574616020209491100888675797765737612459424095634932535563847187178935287808 c v23 = 0ud304_1277126071812236349832842671365330528600340125828390371874373821502309873224835368071725056 c v22 = 0ud304_8657403627926171383730111383004810779062651070523017387413707292421442589728641967775023104 c v21 = 0ud304_4074212068137116040336831828123816219250306209270907841467896415705780281347303392759775232 c v20 = 0ud304_318318925343618908676418467486352107689854598232332117780339099160882809637701891739615232 c v19 = 0ud304_9489693506162914768571562277935258724472393170004977324575573470008447217771697120051462144 c v18 = 0ud304_16298300415677936460214744979398238679694617758630491295870518559737404128319357431693967360 c v17 = 0ud304_95501603927531457201467727955578688894661413378064687133783999893362406031524183849041920 c v16 = 0ud304_62165530562473957301104247030595686563972100293577099497099237467231869942872024285184 c v15 = 0ud304_16296536487471442171423189109736989997594823513883890240066653362606734544438495319840260096 c v14 = 0ud304_131297477938652818465193934677138634089731003220778030166723661620844030193927345668096000 c v13 = 0ud304_8164097223942382419685386336476888762445102843022115558159913997732059557242901713702092800 c v12 = 0ud304_255126820396793457850598431215506803554402555972556752300410604039752812362288195277160448 c v11 = 0ud304_16296293640594524346878926414134902138787076089391584231570131617201716785530503158017556480 c v10 = 0ud304_2037036010482962721779471914491950999806040876699119901809196838880231012793331794713772032 c v9 = 0ud304_259603215140291321573039879027097975850362860758188695249473378079909364929294828237225984 c v8 = 0ud304_1010332006415128621012608815208711375806185065241195861109111989857577601397876232036608 c v7 = 0ud304_8149140562896106826038361920312017492449025638150120518101924465035622533509205009700487168 c v6 = 0ud304_2039025332359951035366642173786814110428672090522276005054535420599956347934102922360520704 c v5 = 0ud304_4074071983260373708382135712935574650959037751321638930809383459138993843029442064250044416 c v4 = 0ud304_2072858792678432313146164802981266400690794889466932938038546605292875967095922899195789312 c v3 = 0ud304_763888491125432282819985884735275151627805768574975712373949767200160215988868189939302400 c v2 = 0ud304_745985806894249614163216437178016317099659441778891864200640028164724209897269547237376 c v1 = 0ud304_29552967085015037795294769993487274108870244113633950380804256944311782204853833152539394048 c v0 = 0ud304_0 c -> State: 1.2 <- c state.vid = 28 c state.target = 0ud304_763888491125432282819985884735275151627805768574975712373949767200160215988868189939302400 c -> State: 1.3 <- c state.token[1] = 0ud304_763888491125432282819985884735275151627805768574975712373949767200160215988868189939302400 c state.tid = 2 c state.vid = 459 c state.target = 0ud304_15914952664850682532507237473353222740246645791022133591847389250546386143804083327213568 c -> State: 1.4 <- c state.token[2] = 0ud304_15914952664850682532507237473353222740246645791022133591847389250546386143804083327213568 c state.tid = 5 c state.vid = 383 c state.target = 0ud304_1018580199103097333569352042938907722256919612835132364624398081121498555187377341483450368 c -> State: 1.5 <- c state.token[5] = 0ud304_1018580199103097333569352042938907722256919612835132364624398081121498555187377341483450368 c state.tid = 1 c state.vid = 64 c state.target = 0ud304_4082029132047490040702941748293814426198665043087460809164394352330202112845709941669888000 c -> State: 1.6 <- c state.token[1] = 0ud304_4082029132047490040702941748293814426198665043087460809164394352330202112845709941669888000 c state.vid = 1 c state.target = 0ud304_2038031595327694804911174138036581943148975827573171337184129171583333773848714683772571648 s 1 8 35 61 83 148 201 234 284 301 382 472 t 28 35 61 148 201 234 284 301 382 383 459 472 a YES a 1 8 35 61 83 148 201 234 284 301 382 472 a 3 8 35 61 83 148 201 234 284 301 382 472 a 3 28 35 61 83 148 201 234 284 301 382 472 a 3 28 35 61 148 201 234 284 301 382 459 472 a 28 35 61 148 201 234 284 301 382 383 459 472