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.5_02.smv > DSJR500.5_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: 58862
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: 401
c Sum: 7549
c MaxSize: 0
c Time: 672
c Aborted: false
c ML = 499
c SIZE = 500
c Removed 0 cliques to minimalize solution.
c Result saved!
c Clique size distribution: {[2,50][3,46][4,29][5,29][6,17][7,18][8,13][9,10][10,12][11,12][12,10][13,11][14,2][15,6][16,5][17,5][18,5][19,9][20,6][21,4][22,4][23,6][24,3][25,2][26,3][27,2][28,5][29,1][30,4][31,1][32,4][33,2][34,1][35,2][36,2][38,3][39,2][40,1][41,1][42,3][45,2][46,1][47,1][48,1][49,1][50,2][52,1][53,1][54,4][56,1][57,1][59,2][62,1][64,1][65,1][69,3][72,2][75,1][85,1][87,2][88,1][90,1][91,3][92,1][93,1][94,1][96,1][97,1][98,1][99,1][101,1][102,1][103,2][112,1][113,1][116,1][118,1]}
c NODE covering index distribution:{[3,2][4,2][5,5][6,11][7,12][8,20][9,38][10,28][11,33][12,36][13,40][14,32][15,36][16,31][17,27][18,26][19,15][20,13][21,17][22,12][23,7][24,11][25,9][26,7][27,10][28,7][29,6][30,5][31,1][33,1]}
c EDGE covering index distrubution:{[1,14288][2,13238][3,11036][4,7578][5,4863][6,2951][7,1920][8,1075][9,664][10,407][11,266][12,177][13,129][14,96][15,45][16,35][17,28][18,21][19,17][20,10][21,6][22,6][23,3][24,3]}
c Total edges:58862
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 <http://nusmv.fbk.eu>
c *** or email to <nusmv-users@list.fbk.eu>.
c *** Please report bugs to <Please report bugs to <nusmv-users@fbk.eu>>
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 -- no counterexample found with bound 5
c -- specification  G ((((((state.token[1] = v17 & state.token[2] = v106) & state.token[3] = v164) & state.token[4] = v329) & state.token[5] = v464) & state.token[6] = v495) ->  G !((((((((((state.token[1] = v106 | state.token[1] = v164) | state.token[1] = v222) | state.token[1] = v273) | state.token[1] = v447) | state.token[1] = v464) & (((((state.token[2] = v106 | state.token[2] = v164) | state.token[2] = v222) | state.token[2] = v273) | state.token[2] = v447) | state.token[2] = v464)) & (((((state.token[3] = v106 | state.token[3] = v164) | state.token[3] = v222) | state.token[3] = v273) | state.token[3] = v447) | state.token[3] = v464)) & (((((state.token[4] = v106 | state.token[4] = v164) | state.token[4] = v222) | state.token[4] = v273) | state.token[4] = v447) | state.token[4] = v464)) & (((((state.token[5] = v106 | state.token[5] = v164) | state.token[5] = v222) | state.token[5] = v273) | state.token[5] = v447) | state.token[5] = v464)) & (((((state.token[6] = v106 | state.token[6] = v164) | state.token[6] = v222) | state.token[6] = v273) | state.token[6] = v447) | state.token[6] = v464)))    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] = 0ud401_40633321238628162200345757056543918937012381617836338123349543806174057237704190342229764656747298378117678003912704
c     state.token[2] = 0ud401_1261480606167361984773244139351810840829611768061298702727465974223273859735893260632399676552350808501568272712335360
c     state.token[3] = 0ud401_20176294607756459772192828866740262027966220554336639015217476467583471934017512027007338009999334930465017000395538432
c     state.token[4] = 0ud401_78806426694564054436323056376142587580661803067971914692518609966002620767357509627484955278505947095460863610454016
c     state.token[5] = 0ud401_736354543521011269181275594123663694605194709835244971824983784345284940485640987622540476425236000764666091444973338624
c     state.token[6] = 0ud401_307828173409331868845930000782371982852186346474056855321969451408242964611567154146006853259854665086594860449792
c     state.tid = 1
c     state.vid = 239
c     state.target = 0ud401_0
c     v500 = 0ud401_1331590801823801921850321931705238854447515892435356969449572714360891341480924167749669889719510779773652814184579072000
c     v499 = 0ud401_10087221433238736672403083689792816870305616025224494241366244090419019484474895376526325153644203293505006081306263552
c     v498 = 0ud401_161391079122691901131266443416604687080141325316089855862913314355112457360951665258251429161955623367293330089276604416
c     v497 = 0ud401_726258394770132504788301260152070283509832827134951112351941031604278096368048352573995663024736054287903987244554256384
c     v496 = 0ud401_307828173409611836939223707518633291575341240681509308589729549321310679657605283840606196847200427327243681792000
c     v495 = 0ud401_307828173409331868845930000782371982852186346474056855321969451408242964611567154146006853259854665086594860449792
c     v494 = 0ud401_10087221456724162640125458182950768634210682143596442806616708928397277543998768164077325740170019897474050393173393408
c     v493 = 0ud401_737005291114724920423608078053529942569790893165662761213841302359987975194407606130214209549047491621011898608258121728
c     v492 = 0ud401_494260343347621615584019209112631820267181832597854428745953752197159515820958432812477038822284573005460552724948975616
c     v491 = 0ud401_60922896670657288699485431588457368572548516473599941368912440343203759991995526090906754735190180692346649691966930944
c     v490 = 0ud401_728149691067566320426254319092503240846298414661279120322430033385559677070827767831478370240401568711345694173648912384
c     v489 = 0ud401_1334112539840313647837420200376713782776694327310907662191202832932900032598885641437698535244819694932400660534446260224
c     v488 = 0ud401_3313078905619341990271205144050652061114011226212603787887477830464722759784254332554324053471872229496860046417830608896
c     v487 = 0ud401_2611646237409973269443688707079259307873320798329335578168169907867183957845988193305659199151238163879781597638394118144
c     v486 = 0ud401_1775298368804138682819557202324697309100592914116893761296631690934588795450112454858026651112587316768499513563946418176
c     v485 = 0ud401_726258394770132504788301527150449773623593126526799160064182431579009770955599091731156841921269788685085058849809891328
c     v484 = 0ud401_26480615600353845497800717842792032916874523277516172102895153968934835295387539000985482640593482465475202755151790080
c     v483 = 0ud401_26480615599179574208599983960112344087811159480092867417736862112213223919662231574034220308198118569231320099615408128
c     v482 = 0ud401_317683484773640009459450478483563042337789427646797780924378358035538936436957704373219633843975443175310535730135040
c     v481 = 0ud401_616257576013352531883804513361106846082279501405589421046915616670755167672910295097839509245484959658953196699648
c     v480 = 0ud401_60920434045270016284278338332769188386217008392584675088016708008437114858509724366066824732518132093977507928848990208
c     v479 = 0ud401_1331590801824260478229856480002880027396234551537849324487794238985376077854834852456136922925067769385433265518724251648
c     v478 = 0ud401_3313078992196020348645214623823306978401431912927433998162129633303160597591116391135613202737881544527935563285147942912
c     v477 = 0ud401_1613946807125575256781475633985324313762780068263962434993509846696355788494136813555452368121190881359227964365584990208
c     v476 = 0ud401_1657013248116143394794411946696129956347237826982786950693402132980402718291307947173191061337013181902958082838556049408
c     v475 = 0ud401_1334112616797063163599463140141750402542777656318556870388010712669291400511095001433270451534711142877240250958170030080
c     v474 = 0ud401_20493975697163449263800995260769510965468927586457416781001740253697959825888959914259501103574604572567888131346399232
c     v473 = 0ud401_39402006196430315128153884967512532881568834385820509336028017674177537763386401054424820852509508592546586973700096
c     v472 = 0ud401_39404413452577676078624610578924814608828834882146081502519994478140946037229214451323126365413032026009486277738496
c     v471 = 0ud401_738236604353220682375099094559089080405847045450066918526997371752840767394817382309454079871935693932800468485998116864
c     v470 = 0ud401_645563085929607592565344651782147304526500607330882514601222249299822286941373312226825433722609797787727101592330043392
c     v469 = 0ud401_1818975194577181262273237887311504804843655568948636592622557957446965694810811060699657839306963706948920007852543705088
c     v468 = 0ud401_736354543558591462495404684802916401851901532247354944878877381834101274529764159385235450781633693091980917867519410176
c     v467 = 0ud401_39402008544972898038692377228915168449831897777707462773389122612200827474716931496300062353378821763424111502032896
c     v466 = 0ud401_496939718247425011068553094578672470204739843425433585406087739183244835627645441554335234522524394549105168589057425408
c     v465 = 0ud401_728149691067566320426254319092375926097746013830847837557184132793615238020091023203324265034076995400570916204267438080
c     v464 = 0ud401_736354543521011269181275594123663694605194709835244971824983784345284940485640987622540476425236000764666091444973338624
c     v463 = 0ud401_736354580834656971111237954790904741400864586759839568993814349391869706637203479130609747484169697706994433331210223616
c     v462 = 0ud401_39402008544972915536698232530017900562023278332728211087413973421453751242509922940849741799098158734327206696189952
c     v461 = 0ud401_161392310454762170196038314105663431705594597021663172688529208995490189383972618887445389132661965931917184048981606400
c     v460 = 0ud401_2607784859968288165208081343824878550804460128999314117060116715302854934549275323430996641379747998979681665541182849024
c     v459 = 0ud401_1291164341051999572331283214551959344126049543786206381496655081280289506331345223522661338449118351758014743542585360384
c     v458 = 0ud401_6324662301173379349568046147941970823862903852390512059380097155883867308353803910521636670979387115485526009797672960
c     v457 = 0ud401_1334112539840313647837420200376709804190788228534918525013463560117512893770335672341503033841657586477501164241410850816
c     v456 = 0ud401_2609045705151304199241414223472019803801180545056412264449716904363695359201580187209349019184547682238391856859340341248
c     v455 = 0ud401_1331590801824242238851768209613281015665812044356403418192154344178534760703197535141558368002795604673031426889442394112
c     v454 = 0ud401_2467435202486415505960335466731759764467707610730922121126229901552637831878402935031786679897436496996211280052224
c     v453 = 0ud401_2609045705001291041767248263057549429953681594943441639704276877305650575407713889035374015780282214039381672773082415104
c     v452 = 0ud401_726287946429781322091605693328826548361917980764220287054404505155938172080882658723810885149544496727232423993016320000
c     v451 = 0ud401_2609045704925844110183968689740618140875919951448262277239672207234128731082348124084740584532730073807660471711130714112
c     v450 = 0ud401_1331590799410252432765262267435599079184462389082606513133992249425127511954731337208854566630720080992488826397075177504
c     v449 = 0ud401_90782568620764646927824691708213455924013820425809241730700841145155725990292698820103263405114319864046866683857469440
c     v448 = 0ud401_2609065406154402396480986187197458105070430278492478505371143481718839857783156141570892187328492816516625034279338901504
c     v447 = 0ud401_161392310435385538179867359727792314206334493277679670671245307750076977148180042252525801839068750967572340612197777408
c     v446 = 0ud401_161392310435385538249859249942121642690424160258431546337414835067286744479870971986391561305242868746298511516495773696
c     v445 = 0ud401_161392310454210574889910028362015881755368580253235107803193526910393658511491014905216809014188987704354295593937403904
c     v444 = 0ud401_1331590801824242238851768209613277037079920766063252375011468921878069061875643488186367776277524428936605889177579421696
c     v443 = 0ud401_161392310454211721569226000204776973682388074293303254042015447572530521910385227385534194710906818077644893108624687104
c     v442 = 0ud401_4239849221341046546381676017106217086598960459955087975612481625250406584559398040343564202625718035001361669800532639744
c     v441 = 0ud401_20491510657327613366147387003255409495725916373918458989170329309758678931213723722979355399688047590340544440666423296
c     v440 = 0ud401_484173429780169665545726553788432172236146191688281707862249927095553462689254335601756962607289474565263815273831497728
c     v439 = 0ud401_40465862780347447865065590332187038520421274340009263243107585145905109171340224065263460508248604356315011183544369152
c     v438 = 0ud401_60920429235454806763467887615112926283071582204373094008642597298990954273810291970259475619033483338895320981883060224
c     v437 = 0ud401_26480615599179574208599983960112344087336875082576827021268582145277586915860159847009146270319205544645505745523048448
c     v436 = 0ud401_1613946807125575256781475633985325308409252888063403008297364102128804728689049614499735100806213527596613775465128132608
c     v435 = 0ud401_726258394770132504928216954953034075841607177638382567576593073161630205397450453884413482771461244644622752590889746432
c     v434 = 0ud401_161392310435386684929175221785839584493941882356979631289351688393930720234948035552412775275273732780912266720650985472
c     v433 = 0ud401_494417989892542090637934923350875994710099096176015950484328146514281743390032721950471640894026021588453465420472516608
c     v432 = 0ud401_736354543502259624496945040897324254843741198958915111086064464809191238660257375223383439394754073737697420928186581120
c     v431 = 0ud401_20496435908395730538301407868948734574514050150493948484455233599411042681663696527015202583063395568680111209369829376
c     v430 = 0ud401_90782260773804043753065198705390225709712432417297109245353587328938016968345834220801552417342717917675140245367029760
c     v429 = 0ud401_39402008544990833494633570057380460333247419169130046534527504493881346143374988678082856246155881377214583137107968
c     v428 = 0ud401_171478031229764330186071359870366087733744592650899089123467546622798756113715419145640255466327645549736758429681188864
c     v427 = 0ud401_736354543521011269181275602467363053915031899506979351428525826555897325632436595882467302162167406273373410465736032256
c     v426 = 0ud401_161391079122691901132360068780014711030494819246626249207963473428331941733823767326526519296221995496458579874779496448
c     v425 = 0ud401_90782568620764646927824841894802043443813091272433495622895935656868050075644511528809623501931891596024981463221927936
c     v424 = 0ud401_40662872799880277930004853703842628597038677137684963945315834841301504828941033745331513933685828354602217211166720000
c     v423 = 0ud401_161392310454210574888816402999686043874497142683303564571943293028760385281601615979623442388186470199048238474440212480
c     v422 = 0ud401_1331590801823801778506658432325769378771209472886566193437887025351420072420820236784863447484826959160951152181172502528
c     v421 = 0ud401_655649384310494632450390225038133256047321832954771920844004479365235074980978948357518855285611642012119991347016892416
c     v420 = 0ud401_2609045705076150835481494016195174596585030440627147745640653332495041534851593654229038707299027357981708559044497641472
c     v419 = 0ud401_40426460772096079181761297647071311080149308081794240203218746784924582922812231252731648340153984655820093964679118848
c     v418 = 0ud401_1291164343456906873063700989815906209441145506268117351852639690734374314211585173374345784171531487335202264146967003136
c     v417 = 0ud401_1331590801824260478229856446628082622214716789727272693314545795239270683287195638766033687258887111485719018284341264384
c     v416 = 0ud401_728307299211017516603211779672826418410176518015627081213836391705805052118300085495235163892066559992355965264302440448
c     v415 = 0ud401_26485540851128394807703320716322511323167071358262017923331002103275958666426955815925358051083216544641694723651665920
c     v414 = 0ud401_1261499846600177860785973556484061169247804965650560600869941445796439443956594701443150194042746364348610536173731840
c     v413 = 0ud401_40465862780347447865065590332441668017463085100792818954145901911682470798366431145031929069666706195911996516318838784
c     v412 = 0ud401_1271332161035515482211777261080295993443888014195515829595447907999032940750358701070337672270044459483775725513736192
c     v411 = 0ud401_496939718247443359057481009935953272893145099125040144682214835602095816610475770837876406403594195532476877594513375232
c     v410 = 0ud401_10087221437935821837967700370883394702290249851066566638243490402832545147010180152634369301286339733540599712458997760
c     v409 = 0ud401_2588574540388081964525997733795345424038684135544725466961751792530317432358528353673856330488473800200256310652943992832
c     v408 = 0ud401_2612375184219674814500261299284032000809974594091718399400402426415949109590051609485671436170336013760418142667352834048
c     v407 = 0ud401_40746602062905560388059387433682846703681083731022461527869297347379347461729041497589715074699952786899935216711761928
c     v406 = 0ud401_161392310454173878912049915243756277507933317672422258012419586697908334203098025408840069295560515912579425010014224384
c     v405 = 0ud401_1261499846600177869537112438577957826047447976640614148523375802754428407974091222499814883839738698731406307903930624
c     v404 = 0ud401_727519259870255258081393823976288576327082124867389253466088448294793705652254530009248826775847072163590060926373462016
c     v403 = 0ud401_25539907131860555871808214975087211251973381492453669644582916898395390549357515119162704447863806529788325550545174528
c     v402 = 0ud401_2953756657278560533814381399138437461635653776041039330709162957726892335803488407761725094535680416615292262272854917120
c     v401 = 0ud401_726258395977283392334000275598401208417574571476367848944258513804924234136455179019012022595733590373433541795592011776
c     v400 = 0ud401_40426460772096079181761297647071311080149308081801141949565537336452051890245760080414405028161477604686987588320362496
c     v399 = 0ud401_494260343347034462020384901279513148510810753213965223641291162003478470782436837635276020382720349236541217166300545024
c     v398 = 0ud401_1291164341052586851320640205614249967651371416097987839494400385130290886514359588200225292886930190914838547148474155008
c     v397 = 0ud401_496939727871780037259130659400599592321446123697474951259039490761930019391981785324110138935716559258643701918641160192
c     v396 = 0ud401_171477838799579268099264005990948515307907323732002410043473879295339222696080632092931835736713458685864618748159197184
c     v395 = 0ud401_161392310435972691812417019820247557244353338504859390128519380123566107786973438000384976259600376683439059651941892096
c     v394 = 0ud401_726258394770132504928216954953033577547036321738875876734613972929030651620096237010626281681596884965877624207117910016
c     v393 = 0ud401_1271332159861315862665154289088048640532600571074754291872576180687384102611178802488905304062896819597117859441934336
c     v392 = 0ud401_161391079122691901132360068778996193057504676924005534940941663825837367606094087808504841024363931573788345870348976128
c     v391 = 0ud401_601226901190109850287850716419348427890034955875071586706400233273224198693411239469140621766280599607693017088
c     v390 = 0ud401_2612197875041493416407736093983090863531790943925279870604682192298101489313810566305500376332274921617404424748225527808
c     v389 = 0ud401_1261481658312145568843618237600225074144950210569031805169367440035582358542159258658358047819893579683493951507005440
c     v388 = 0ud401_2612375184219674814500261299284016086466350078672764555427947966847586578863821535421741722627556756772092679163893252096
c     v387 = 0ud401_726287946279474596794148722240158209582149630540577668626354724838555721053515182489064049082281626125726041812798275584
c     v386 = 0ud401_3922489552530242204323607566867755241874393007966831846611591701014374392655380087983691693686297105682125776747285708801
c     v385 = 0ud401_726258394770132504928216954953034075841609030354214694190401074207389484421806161473063488015840442335784403602707054592
c     v384 = 0ud401_20496435908395730503269084493056556751651915678138380303328957029728004923974984639113725025935328739260398728736932096
c     v383 = 0ud401_1261480607341704950179161167814300901750687035797559870066387085687827977520394175149040314576547374555543660075679744
c     v382 = 0ud401_1331590801824260478229890655795454761957552871885148037321627882257733784299154005121861429403572942780780066600074084352
c     v381 = 0ud401_733193166799343027119169179253933579400686521047398201712409159853888105935957269667592687411616813198739100662180610048
c     v380 = 0ud401_2609045705076150835481494016195178575170929129613997902371732313245749718139828915604489907895748085948907484640473776128
c     v379 = 0ud401_39402008544990834724962036544155436921982118198307191239288143284313720677956301800888442572338335880572395904303104
c     v378 = 0ud401_320143714647482474845067649258560416088886249046644522724288261278088017655584062220425290677434707238570518860791808
c     v377 = 0ud401_80695924947791906779211006344458013056064171578779543092539757584259332439593652494739359528352018789546685744715661312
c     v376 = 0ud401_496939718247434185063017087457294534775566341910853400178051866729393906331902824081336288456475842269148814826765549568
c     v375 = 0ud401_1331590801824242238851768243004374741683376862694494216888136400351553574032179982407800740971025748252502055662504640512
c     v374 = 0ud401_39402008544972898038690291304075280522979141636849717357337300958865293404478895262589808505349320311200884155482112
c     v373 = 0ud401_315216049864725900664205101916176474278252027816409630524699879933877483578544709830499634416575477364159896650514432
c     v372 = 0ud401_1331590811443748988164519509272128079625291680855708149633778597336040254639961590199183370066292814206763760769120075776
c     v371 = 0ud401_737005291847475935516085992030138468408994418186688922960868202820618756422354662453852945614720296731506945779382091776
c     v370 = 0ud401_1613946807125579413747717084701098340565076744558314637503705554085265697539286402403831943320894427104810719915177680896
c     v369 = 0ud401_1291164341051999268303432469713301856462072398242822241392510059682700694638981835537963951509307244905420871451520532480
c     v368 = 0ud401_1777977560968618203503728538499538997005135008320141904755372249312659829787406693351851981277356225735419941533610147840
c     v367 = 0ud401_1334112616797356731382939356248633113984587661837294534711455867471419560391353183304066296676279249873741664745389293568
c     v366 = 0ud401_726258394168903310239508202489959115882973029360058619831567504479955064737744389524863056907281717255722774998200352768
c     v365 = 0ud401_1657013212044877847965659433054510075721318336240978515009310199270392379267483052225650654411842606114987136432511909888
c     v364 = 0ud401_726287946429790491606563081232606900764579846491532009268846157202397022287457807839737965505698336949270675042642952192
c     v363 = 0ud401_39402008544972915536698167376695344984989515984816527615155082020663102584692564188536859837802666982869246186356736
c     v362 = 0ud401_736354543502259624496945040897324254844689767761014607203167832810933426055299361208894845049590048585324246434440019968
c     v361 = 0ud401_494260381863646867806499446283282310135866648073562844972555643517296436086757079387809616499799126306658999477989277696
c     v360 = 0ud401_1291164343466301043394796322727472089000085874132251517850171336273981291561795605278993822800291692321623917421406453760
c     v359 = 0ud401_3922312188188236358142578169489361515523205720085391166909804175593527725449742722832069671145804007293529282338432745472
c     v358 = 0ud401_728149691072263405451835028101418618959892666534988946743374457167385583248600033277417236419578871129062167478259417088
c     v357 = 0ud401_736354543521013571638870552388985009666899668276710719120606025749837370352380283028196973116351001237333737247051087872
c     v356 = 0ud401_736354543521014718388178555764366102190733356503197334391948152717942731855785774615946458725204506831833378591103516672
c     v355 = 0ud401_1818443267420719350480048400009157937077235017272097793188676070247758088862292284851766090956386135809321313263635398656
c     v354 = 0ud401_727529109169350554323181531785756631037101534236643644064397911036137773040336980776456819809231365858168008822927392768
c     v353 = 0ud401_484173391300988590610281473740153128953014423527334081430060517839454471607926391411599752410033704528663727286050095136
c     v352 = 0ud401_2650733029961695310844222967134063661077197748924291799326865693373625877271379172332985754992690824366443843813006901248
c     v351 = 0ud401_736355157956155014909903090577136279611217631195638189517810496652382448206320957217703803618619612235747191973067358208
c     v350 = 0ud401_726267630221256477601356905207199399213108612365629259868411380876079563464499920751319945218927217421323241438591336448
c     v349 = 0ud401_2607863664055545334821661929153078229970159109883087708235216051186800830581549217532051949410114649473242970027204804608
c     v348 = 0ud401_252330755509957619537669498570162509774968414933391218559884713568743444665807719779636630947403778693446514356957216768
c     v347 = 0ud401_2612375261176718166832681966130736511027938929674134505067065321515902833778761797945520501745695959851751577628874637312
c     v346 = 0ud401_2948723050986971139095012743421690126469665958946597359084169100678396507176579973584016687687040913438587170116392189952
c     v345 = 0ud401_736354543521013571638870552388985009666899668276710287761459351339600655680138890714106194922040240588174321064263811072
c     v344 = 0ud401_2612372798551330892178277744373546670332920316427821910372503772574944399142598773064786683765420059133750424406398599168
c     v343 = 0ud401_484173429761289584938891996459613965079810006311262196506758913846920811139322012067860298143589110976944497894235308032
c     v342 = 0ud401_494260381867756512722179432552866926217033532940759454605587691946396936514547910834731167208526672047858439721190424576
c     v341 = 0ud401_20496438322550721679008088516489519838930662012570627525830291139647368609895551046934754424917479819174942360817631232
c     v340 = 0ud401_736355157974906659594237924638653933917041304971795536391965386023640036352816610450354896573837989834497745842708938752
c     v339 = 0ud401_2630975518713487398401220400813726534620377922101650949088033558259321050539922417153793182966898046942314047365969870848
c     v338 = 0ud401_1777977705281858395007879678270426483853601575351756612909145549362536753330880263228796383633423763261423213619277987840
c     v337 = 0ud401_2607863663980391972181648268759746867487688058303871216998922804643005644943668277018448053081738813539129605395979436032
c     v336 = 0ud401_1775298445761256726160186600940572621599474426792956685073790712020829255271130638459288724030234410268980344637121101824
c     v335 = 0ud401_1331590888401081051451323867343853399739421837076610310731994242359176626000185022006113699653821862865274576485792874496
c     v334 = 0ud401_726268245421986035346929361226474258147346276369511500635048161559656778759122055223458305641503805046999654739264667648
c     v333 = 0ud401_1331511995397253998928229571368888297346448810342222166948483809231954984845451770641030703205033972406218168266716610560
c     v332 = 0ud401_601229194688725840359362327240243729976975752440060754987523970862063585615622713956075576661495640270034698240
c     v331 = 0ud401_727529109169350554320994281056899546674392836778790016527582124247678599655234709389912221701494732616161322473913057280
c     v330 = 0ud401_118208435239501707253537364532963946417743601203821489084511030022179837056242294835109176909673185713998242410135552
c     v329 = 0ud401_78806426694564054436323056376142587580661803067971914692518609966002620767357509627484955278505947095460863610454016
c     v328 = 0ud401_494260343346961070065749743941696764429301811679936023999716584693412358497827304042456051591563629660352893037368573952
c     v327 = 0ud401_461761048454659993934718117018332288974497200036158219698985104782662026154148443306815429843715588000107473141760
c     v326 = 0ud401_2631285809511976675581706607820574938991386729389323341441133665548368944099345838739149149857386713431743996523628724224
c     v325 = 0ud401_1331590801824260478229890622420657325693332834462464559670794333252930059077819636968569631761378620858237378713599606784
c     v324 = 0ud401_39404422846712153623375794599455721819914636931044539866905355421205079445959013933214672674529326478464860439969792
c     v323 = 0ud401_25534981879911735269936639020311612677030597351302726378100225468471327325228355644907958281185962769542450014763089920
c     v322 = 0ud401_161392310435385538179867359727792314206334493277679670671245508617332509521964484997787344484394066242946563461301141504
c     v321 = 0ud401_1331590888401081051451323867344863960548203151785790916803935217532839146415532104431030367205365202593028690886231326720
c     v320 = 0ud401_3922159505414537245365176667722250437549841899464519181304229992107661101331389874712398372695263633724158088588768182272
c     v319 = 0ud401_20493973292109060591937161539360221797045055289695311777190597057620933740257243056750223709968222740664248543874121728
c     v318 = 0ud401_494259227474529546682164403379193879049576059280516074313590111815561324091965689802184985063886896684654299479743135744
c     v317 = 0ud401_1291164341052586421290606594214817893764867661229328055837169886781343824443132583411715023614914178719642147986706792448
c     v316 = 0ud401_736512496631249789554075472482350090374311183570892407174088398774192839082136330291623658505344510136547089811993788416
c     v315 = 0ud401_726287946279474592314659237884549788406556673758640656249092759754208248463599021522726634794617985285567918002071928832
c     v314 = 0ud401_2609065415698879457353368886483628876439779737378741850297337688655450211317591533058462970533234750305369724514493005824
c     v313 = 0ud401_2609045714620926046725052473781622630343021298794529712400074206051098513890359981693126008250032922101353794557198729216
c     v312 = 0ud401_1221157365239510264697525827919556774215272125657045855818068686644155593118423109342407979562685626277420840942967980032
c     v311 = 0ud401_461761048454939962027490342544651969259568255570923425386139053598928860256822974804183325878313923813391531507712
c     v310 = 0ud401_1260884039946633899522955107481666279991769923494174982258633488286028996899233522955266673340874847415705017880936448
c     v309 = 0ud401_39402008544972915536698232561846587688544276575105516661923386307446366909717145539488094383838235722792923182399488
c     v308 = 0ud401_1775337693853291850671476091485546750625419594429869910127689038832144034328080270377879814136340047482931117815859511296
c     v307 = 0ud401_1788556807277501907100062270692822191170942979992743227564629110425221993964636197431015110980944667834394511464969797632
c     v306 = 0ud401_728149690768117966999078829488349943970305855020291091614688202338918839637167746250910034630780150508860801457489707008
c     v305 = 0ud401_25539907132154124851127453077964132861948567774415387599284713991314576922376955352660944738207122206273378539066621952
c     v304 = 0ud401_3315443045262027604013367763992217394776491151794350359328519905103073647466110658132036955990308457140379850010330660864
c     v303 = 0ud401_26800752090884341120591102191134131499861635470417164249633910291443282947479410077476111333099411055423733784687673344
c     v302 = 0ud401_2608730493836394889168675654170697139477422757428749760924891370323817833922124334018957002023969376220936647255670128640
c     v301 = 0ud401_1291164341051999267743496284168882632509841591277452167061198387623864705356004177470993510846532017660022737083975073792
c     v300 = 0ud401_39402008544972898038692369080771262874745353945904510901736494938461982851966288916958076511455109543285215020974144
c     v299 = 0ud401_2609695847798324576910511759017413279502062434397188364037181864992890807206889827388630366370559142195437244131783475200
c     v298 = 0ud401_726258393868289859504473502933992338039525038691080320156234190557829967736515486207174065897319496472294697331001917440
c     v297 = 0ud401_738394212453233014896422555257362222509064205571239530088289701664562696813763050691390002449307776496128953014504390656
c     v296 = 0ud401_601229194688794191944511796361931809113543210293906966518181628843797231679471491524178369130953725231562227712
c     v295 = 0ud401_78806426694564614919321282038862551599470674500517272132509274362973039293942074823182779202148672585918602662641664
c     v294 = 0ud401_2608750195290413262292040418961245969047751356977950837881218158587269958811803129268792309987509404178284256292086218752
c     v293 = 0ud401_1775298368804138396132230203565758357717626799914999144992865735319517972948776887264890370035595978320531760712008073216
c     v292 = 0ud401_3318122468222474931652778607841102681160833105308345140335045767882330133007356694499860622978353591453432956905706225664
c     v291 = 0ud401_25534981879911735267749388295524618281429032379589720115834803681877238111575252743609348007515522275620473296564256768
c     v290 = 0ud401_1334112539840313647837420200376713782776679505018804373738383181190841299071515570071627749992364731907661005826614624256
c     v289 = 0ud401_2609065415699182198050773029041684664957912741515532573241129762704733357885511315390977455354600081068309219091872219136
c     v288 = 0ud401_1334112616873170620513268964842150065045265830480836336614993849225596530299255558677616770568672582329647345613586563072
c     v287 = 0ud401_496939718247452533051945007768646940702723410426942500560930594009431684766785801819469747653797595248878929102684291072
c     v286 = 0ud401_161391079122691901131266443938085897021769763400811952095714123584288366139431693870247111237663822602305537002874863616
c     v285 = 0ud401_496939718247425011068553127953470030735236661553097135089160526442756144841016740529390230490270674221321762177959329792
c     v284 = 0ud401_40746602062900833406779951090321437502972734810314425579848363539603910048024344840596332421395477485015891860508377088
c     v283 = 0ud401_10087221433238736672420034175845037447482931426285632139246987876303892377191879786442638757738108412038690238021763072
c     v282 = 0ud401_726258394168905603738141280457757595689954783019444731875913467755565202752982362520119762114287903569434489394424709120
c     v281 = 0ud401_3643927786931734401843677093323441150834721769286091934990590238828862856039855253745845279545340938842576223774243291136
c     v280 = 0ud401_1775298176411548793617196925837414153043693303937858002457091710961918130677993588099322988399989376869048018705997366272
c     v279 = 0ud401_494260381867756512721085806147003741377508636753298886904522920862628270347409094948703611598779249145987296145551982592
c     v278 = 0ud401_26800752090884341120591102189097095523527149384134915068942327191187103860336105539042809393527226888359500024027021312
c     v277 = 0ud401_736355157956118238301235997031165749897972023973034847800311831225685156728138925615657305160240327626776118221749616644
c     v276 = 0ud401_2609065406154402400960475671553193848704511313926809899666035165988457715680866903969901245138357299594315709794882682880
c     v275 = 0ud401_2948723052194122017681237241034100255462407546568928962506556703977083074044984792199164792863976873484320570025764192256
c     v274 = 0ud401_35836052580101091146930863522823191689582859100723632427471068023571379571090471194890058570305036615680
c     v273 = 0ud401_39402008544972898038692369080771141695081788595857776669508871211782666278340858246991470709206525117708621007814656
c     v272 = 0ud401_2592208860396424303259880419696205165119977182368718357573476760731130770604204743843323597950077927873092456031881003008
c     v271 = 0ud401_3322535511217490336338954163185948064089871488466331793647837305577384708268020289865549016077560051901841322660409114624
c     v270 = 0ud401_161391079141516937771317088858788401752065495280703548911030688016529921837424549093831537532630907274552351934788927488
c     v269 = 0ud401_2609045705000997473943888897017463348092070084825576604520094119483670862489262152791297835759394574470310156953561595904
c     v268 = 0ud401_1775298445761256717201207632229292184160849403052313953082226973475710211387613382209623778727237907411462395513846890496
c     v267 = 0ud401_497441949536669535895537695275684842102470226138246598561494570534867243999488171157852112812943094267961408435011977216
c     v266 = 0ud401_2622996489769297785174312830754435687688665858897952496683150705193123483185696703414386402905235718506415710165574615040
c     v265 = 0ud401_484173429761272383699272096459559883290151401406512572742693118309734134049829867595475486572787727271459196010795892736
c     v264 = 0ud401_726258394619823485992092125907241425599303913385065302413634503268890855910452521942373173887384432699272214716572762112
c     v263 = 0ud401_2612375261176718166833228511813552773895271755853200639220971306764821721232068620797571273002585198807451015504317120516
c     v262 = 0ud401_1613946807125575256781338897440227939253286749678716535118152882861738276046114615756123367106334918167675140416013860864
c     v261 = 0ud401_20491525086773241928577671162705987052760620859649065251213348715715233535926475286980760630311665712472541165061668864
c     v260 = 0ud401_1221157365239519438691989788205603217498853334019164674479349732446514835667316869975010640164032310386371334030239989760
c     v259 = 0ud401_1263350872747945595983201166645480150334719552031333744915890599955826035800726429613530278066427207965047469035749376
c     v258 = 0ud401_2918301057528137909061151789873066285559147577639767415154029720404254001804379341798485628867815622787434090700570886144
c     v257 = 0ud401_26485541001435120105228647170878967032277531589125176995263271520482355879446619328625856195994392860438658671913730050
c     v256 = 0ud401_2918299980578565393677089144050145479570597690727899333459408405686534733684392692972133029656741477737572749602126299136
c     v255 = 0ud401_1331511995397107501704133205551084156169346235004151083241898071343605718856916731378639457792208727080346930199522181120
c     v254 = 0ud401_1775298176411548363586206394250874994602513912742689550713697931898559843022607676452196813485520446715987098219587829760
c     v253 = 0ud401_1291164343456906873063700989815906209441145506268117351852536846699541738833950487800435949764970066343600165405507715072
c     v252 = 0ud401_461761085150637854047836376622579724237078233741883924330009385168677341970015791758270378068335895729022743609344
c     v251 = 0ud401_484173391282749560853472493355623650106741524987564670111768215532441619247711505281855797071488811526736456630470180864
c     v250 = 0ud401_733193147860704813625441989839209107947555017262916344526636950942684093424552555268320455640590596248026521623785897984
c     v249 = 0ud401_484173429780059586571133735436655617107563681994432920528027266088450894859440364267506235061112284403028263728278667264
c     v248 = 0ud401_1657052611561765888056232371691389354829422434253612112200840973197647094736559776872634186406730442913981628562783862784
c     v247 = 0ud401_2591898570804852119581208891028973046626713751238716331895354780034922436617121027932762209837435351567971586880105873408
c     v246 = 0ud401_2609045714620935220719516434067541758878081601761845906833730981084431740197532118346527779708452951020055318492715417600
c     v245 = 0ud401_2609385552264575352013130352991367979266102269511381865147554607514536779290596306468965383124313028740635806453528002560
c     v244 = 0ud401_616257576013352531883804513361106846082279501405589421448650127735502736558400818183130159876035708104788844478464
c     v243 = 0ud401_3318122448987984570690796153714628139754694287600576975676641664229628071560013926834546471114310400769716028198363332608
c     v242 = 0ud401_726258394619823485992092392905620915713064212762778573607648828606956150492048765322574151664850155281646810587457388544
c     v241 = 0ud401_1062308340886405900070520900357078112479741951213999878561994371595354673733624282282435563038966526534306027280514678784
c     v240 = 0ud401_161391079141516937771317088858788401752065495280703548911030688016529921837513752074625660025197050147642945380812849152
c     v239 = 0ud401_78806426694564054299619886347748182914304347198746775990170001668282638385002133739335154249558701867612833534967808
c     v238 = 0ud401_20176294607756459772192828866740262027972704907800227852617760995915918210941103071140702985402822841916247448945688576
c     v237 = 0ud401_2608735419087169442949316602513668070391027462714440660910312146484308315754065573644385261461921590514798296086198878208
c     v236 = 0ud401_6307404835680317301228244858433564031758433407385748682776358072437524148100828349649202481928373086124949052701278208
c     v235 = 0ud401_3922469796213021936076651885042211329469039726779084186682125640804971992033507372269926983342071414602762042702884241408
c     v234 = 0ud401_1334112616872510092912410636928001901600938254973907697472529894142082316393302245765149329411552971824439553824714129408
c     v233 = 0ud401_646833800480309433899391957999429148936776389578925345868995006525159951110266076751815610016861964218607735199393382400
c     v232 = 0ud401_726258394168903310239508202489959115882971176630091716699532428797720967650053580805923715334155801751511604841114763264
c     v231 = 0ud401_40746602062754048410514402813779165037756332545518306910779071857978893476804534973685467100894755374922303829494988800
c     v230 = 0ud401_737162323126645038439702654502776186461468951812211041421541677892942619359767902397365895285399485553289481451493916672
c     v229 = 0ud401_1331590801823948705796741307894805430938977986992548222913208362182424956653638468422160412931114837726375097988076797952
c     v228 = 0ud401_20496435917496333007143186803344676694758267530467934708707214737378938065785662989737993250521972850527875401322070016
c     v227 = 0ud401_171477838799580414848572001026704305177005689586528931956491687436844457333997872950528875518265325037412762108207038464
c     v226 = 0ud401_736354542318557466801072981444313286423314604509091395711686803610684821471109584393400445872664727772292855054766964736
c     v225 = 0ud401_2914679805416065195282173278064008634978417896207324844202664053585068880707743048217626689839932950747627709305716736000
c     v224 = 0ud401_35835915876930792208685590241433996834877531194240371627360414527031025114823378181077285540593521393664
c     v223 = 0ud401_171477992708968887529641651410826180837681303583260199718520258748619305503067058380218818932132668249469171408966778880
c     v222 = 0ud401_3922179242492496608341196172494203685352841317739198297394149209711660163004790753097868203338845120293874420318465949696
c     v221 = 0ud401_1231312693691361317288759529709186226427455570411743070030628658560478282173499769302957065159392351939291435368448
c     v220 = 0ud401_1261499846600177860785973556484061169247804965650560495557649777239252700366640851182001681282499941415654917614878720
c     v219 = 0ud401_736345038142491794341804635938517307609041514643553495056890344121182948499682920873991912668681945909105406001494884352
c     v218 = 0ud401_2608755120165421002837617053741036038529000364980264982342893899657720953718385544876214353835530095283362565308098281472
c     v217 = 0ud401_494889736826631575972029923591271438091646798608399298387739201879531138006122490463245538133946726852467379730898747392
c     v216 = 0ud401_315218464166501547726447466928650681280619895342691821766824961479461275190400117187301441566671418010000802548023296
c     v215 = 0ud401_3942643640230497010977756574395542222582057683359178348331528302572851163384519399747518949159515277191937140363351818240
c     v214 = 0ud401_3922469851527171461875324450250695273438492846843980959290686680797821260290715738163045032793303096487308511842509258752
c     v213 = 0ud401_2609045705001291041767248262927179127468274485422261115646076674998356597847718559661933999396465968968550235489523728384
c     v212 = 0ud401_497412551946118118416558743099506260446565547281894358661827550058288613046415793710353552966754934434821004268830457856
c     v211 = 0ud401_252330909424044324203603921535162900960930198250391116463944739015235823229612902501102753382425184097281467283738198016
c     v210 = 0ud401_2956126895696374566961175587071195042388379197084135970528905078007292312287869145669482674940507815351627620596775387136
c     v209 = 0ud401_3338138581516727449313170997690210077470244504188136860117902484342640430013114452675287168261403551558266675799286349824
c     v208 = 0ud401_3079691827623601061377521012935564653073096178922374124603554979184960237334497434240132006412342470617418495681439465472
c     v207 = 0ud401_497411465223210570290702099732209999583270190096519454988515876270105917428200558685957508945604178097602311187712704544
c     v206 = 0ud401_736354543521012424959554589407392082892335132563774612234595666407838587277965755562424786025154818463375874118289195008
c     v205 = 0ud401_1291164341051999268303432469713301856462068229727609724971066982835201382583469195798772899382761377080745243528008826880
c     v204 = 0ud401_1385227385843843455221557501342573978997664226818008472172981940937163287030699449353941444997014224553605744033792
c     v203 = 0ud401_161392002607212147044830918629040718663220396375883518686598779997755011321401318155291379996794649846861011976621916160
c     v202 = 0ud401_494260343347621597667154897053098916305264598491258693285919903130847024052461177017158346252068021697389688053626306560
c     v201 = 0ud401_40426460772096079146628582878207146068588915666160189149082026508962700466416738204581387646343518705736316800750059520
c     v200 = 0ud401_20491525086773241929124483843917654377411448895266254587985230797279697178004807303737543676921992262631986705475829760
c     v199 = 0ud401_2607863663980391972179461018034844529069280409231015337134968295954670898852786329349728930551227957964349574615918444544
c     v198 = 0ud401_726258395822277288372295005585034981269204770764993262130481527772428734221302945432988063910548530389525337244031778816
c     v197 = 0ud401_171477992708968887599650762500169945239611672887045113202711620482627280349328882368865926303013421866545181396115128320
c     v196 = 0ud401_494259265990701295848772938626521667033419010044049942871081929608843325440351276193321549086086806468755424238985281552
c     v195 = 0ud401_726268245426683192044324731246615301666815595327603502717956589707333217883472663362469379350396747966150586487304880128
c     v194 = 0ud401_161392310435385538249859249942121642690424160258431546337414835851924461403206067465865239206201170759020884480462159872
c     v193 = 0ud401_2407256147343315763842941389842274292552272817576378837221365447277141443234140328082155506660935889581376536576
c     v192 = 0ud401_1775455976828924404167559880238834473158096724315134161511566168668228321359150191258319378584150639709984058941005365248
c     v191 = 0ud401_2609045705001291041767248262927417842621736361623073322655463941030166116832161404882985859876860035251085101632870940672
c     v190 = 0ud401_307828173409611836939223707518633291575341240681719933173066663694706516061421768432284973624497195617476990205952
c     v189 = 0ud401_2948723050991668215301581441166252245372767107838450189548833573516805332275210112914448014602283738914326415103018139648
c     v188 = 0ud401_1334112539840313647837420200376713782776679505018804373738383181190841299071515570071627749992364731907661005826614624256
c     v187 = 0ud401_10087221433238736672420167674971109588751505093124966143648603753164850901901217129931041531629244905896425958938771456
c     v186 = 0ud401_1291164343466301043394796322727472089000085874132251517428922169599752544770123494544312093524716146422705930920861368320
c     v185 = 0ud401_3914160830821292286163426866051060482778033453669230050771757580783715991644836626793796029630475479842520105155387457536
c     v184 = 0ud401_118208435239501711628038806197516215084057884873487921691544357882900447575519302553425973379697964337760734229299200
c     v183 = 0ud401_739684752628849580446863725790944876046421579248849039698597332375248018926110913325545749089260225382706750716104409088
c     v182 = 0ud401_320143714647483034781253193454983558407587734329539684089622549149155995177749021578276693680764640822318512008593408
c     v181 = 0ud401_1291165572365298818720042459214231249489919085843958965690245990313319892863553789846808247390278232432955122360124440576
c     v180 = 0ud401_3338138581516727449313170997690209589860011721515525233082508914955321267959129966592023629928170669292115769723010940928
c     v179 = 0ud401_737005291922620124170384695036555404222671994714947578265977765558757117156038954278892503069627681328718906386552979456
c     v178 = 0ud401_3335616853195320739286811761659347667030257036453138917170720074434054201962280826005037287312758285306075541688090099712
c     v177 = 0ud401_726258395977283392334052073544762895457886869788036120440324898420363192564663404341382128122908864207131629901456605184
c     v176 = 0ud401_1331590801814554822117976962145651337679453486010682796908546201905706138100154648614826751692312484256998830630563250176
c     v175 = 0ud401_3916682549598231400478718788566298664700818557496686374834886161363195622125463950944759980290439338021524720082007097344
c     v174 = 0ud401_161392310435385538249859249942121642690424160258431546337414835851924461403206067465865239206201170759020884480462159872
c     v173 = 0ud401_1261499846600177869534976451542036915965052954934444596407969629209942260066373199845822082812696956684491949399343104
c     v172 = 0ud401_2609045704926137679127234602533847796068490888069054230137478293217440734037193990116248110005138259025223870890794549248
c     v171 = 0ud401_320143705253312143749734737700638028931538139543914327091008778448924131526726864255242418637903984473834937103941632
c     v170 = 0ud401_20491510657327613366146319009737200381445346651035720440770796863097432794869194268778802582416804817872946923372019712
c     v169 = 0ud401_737162937580538059202727217513416824869881249046472136488171838403536249916938802635874678253783677992538629131628183552
c     v168 = 0ud401_1331511995397107662948256636554723220910210417662885288494282128424020381516589241989784015427510374196578806805773156352
c     v167 = 0ud401_2467435202486415505960335466731759764467711144425051677894889068150562320990096395835987800800794529619962585153536
c     v166 = 0ud401_315216049864725900664205101924133645942293601505108287413370183295059903654607712329899019245667514892822502069764096
c     v165 = 0ud401_26800752090884341120591102189101074109418429486523552459993055251204548270291044528124545273305226397850590013827317760
c     v164 = 0ud401_20176294607756459772192828866740262027966220554336639015217476467583471934017512027007338009999334930465017000395538432
c     v163 = 0ud401_728149691067566320426254319092503240906977174766721553777856349255235238210512506004464296261152801475013245957086117888
c     v162 = 0ud401_3338301201368961349034381063700861469114341593342674531936843504720134282610027282716992726211794488904739248252513157120
c     v161 = 0ud401_2690054383372980141277781315488741184001108654808108624947599948587653362448931484298180848734487509287181315932348743680
c     v160 = 0ud401_1291164341052605199309568126186852113106377749271486764870508002890135457271837797324405636955812258178232189583200616448
c     v159 = 0ud401_726258394770132504928285306538183046669672962433473302402281259473746064508734542342076592712841208276592193060695179264
c     v158 = 0ud401_726287946429790491606580168998523965559830051707578621900698213368708322351432601522379923195488180811488805322261266432
c     v157 = 0ud401_736355157956118309973072018699046401508958764372134021221187007653960828070919728527834476620855703107813409154932932608
c     v156 = 0ud401_484173429761271237019956115751679890421589881715303500013019853696990895405517072137822849841719716327667205727315820544
c     v155 = 0ud401_736355157974906659594237915256066366792558631871827801779626866726235185375739778578147145022792303946798424639227822080
c     v154 = 0ud401_3322535473340267806568975475911070341419686580740034587451148979130464876557297973575744168894646030137713402841925682176
c     v153 = 0ud401_1657052611524189242567630228407124806315971413780016079905731631650429633545107434350540134727878342331836544544034258944
c     v152 = 0ud401_40465862778439256977464744131083447707271059954356456765519738379214883390419300325577494368100398005943886321448648704
c     v151 = 0ud401_484173429761272383699272096459559883290151405025015361408824024452059316310530878055205578405752477969211137642138173440
c     v150 = 0ud401_1818403865414522956000836122012020213346642364014015545426814869339663309345949173277074763763910262044885317429135147008
c     v149 = 0ud401_40465862778439258097371291012565260779674618452298862482657586021174607149797973544631271639534080803324560231878361088
c     v148 = 0ud401_1231315629351410723587601495085994791022577793275167578354045324459250728561558757624663237654297943857525453488128
c     v147 = 0ud401_2607784859968288165164336329329218310374341192229465771772103994429717010668473982774925512778933563068220520217175916544
c     v146 = 0ud401_1334112616873170620513268964842150065045265859428856866587562673176104361826823763942772167748033993090148202498991587328
c     v145 = 0ud401_736512496631249789554075405732755217845871108726464089375584817439676515254049564780210549285517475401994524137437003776
c     v144 = 0ud401_1331511995397712859895551050034879477431339813975848601031691969281549267028755057767885851591652121211968259490588917760
c     v143 = 0ud401_161391079141516937491348996086626532806645662673687478834610745577348101616094112695394664465494607569465251670970597376
c     v142 = 0ud401_20491510657621181189540928838191728388738452516646491214881903033768191338794138234541477092325889432537861191479853056
c     v141 = 0ud401_161391079122691901132360068780014711030494819246626249207963473428367859598062811596644293054670830867949644072955674624
c     v140 = 0ud401_1775573884678895373185802142973757529022554030995451895522903606546767190187647375710642183549519855160440400682682417152
c     v139 = 0ud401_1331590801824242273585173013925525955594245388394298957784806127667645442227695431310344211019966031403783629307451015168
c     v138 = 0ud401_1385226780360208833842677926826848358524468892484913439283765560579804124594312858464086700877136063150318216544256
c     v137 = 0ud401_1261499846602543031233713313656338361294336126703646786222783526244794341306565553566620357922524275918032539717468160
c     v136 = 0ud401_171477838837155949493620272933949265722937144506455848819977107022556150535456788731090453687891046887301008624619356161
c     v135 = 0ud401_35836052580101091146930863522823191689582859100723632427471068023571379571090471194890058711042524971008
c     v134 = 0ud401_161391079122691901202351958994344039522173036587634879057412148837449053663564250319033938506942521765294422968321966080
c     v133 = 0ud401_25539907130979853559742672451055317358974078733891857715868970407521101374194475985991357101029226195597393344608600064
c     v132 = 0ud401_728149690766943695698942909975145841225900272219507834088074162874508428599832656134878078586819009688891630849858994176
c     v131 = 0ud401_726258394770132504788301527150449773623593126512774811487504005962942347043441025639176923178248795345858481048250220546
c     v130 = 0ud401_315216049864725900664205101916176474278250218565015297459146386637236722829984502486989233787597473822128299745214464
c     v129 = 0ud401_1775298176411548650273533393074999097197829365790136261018890590909985597068008614827342202890127449354840427119310274560
c     v128 = 0ud401_39404413452577658307212536902104171785803000141737886998602604013816210868396236628586120943076340328788372022624256
c     v127 = 0ud401_1613946807125575256781338897407635363631934972298421404102780080006254178725668527308313464703837265825354131218827837440
c     v126 = 0ud401_3921681679209552312694899587619990121727807909134219764690338779579139596587906604067865832639553875991851374501655740416
c     v125 = 0ud401_161392310435385538249859249942121642675247059537918037970856564028634944568450223899454414126128748704563323525406916608
c     v124 = 0ud401_484173391282750707532788474064012901939036173272801083499410890080094313845106003372220195796635060333337323950879801344
c     v123 = 0ud401_737162938181762666894272257981751756397348919787703926478839144458289585901848131346443434571494958582996806408524009472
c     v122 = 0ud401_1331590801823801778506658432325769378771209936054923169662615386785999901839466736884432783684227539531859664937301311488
c     v121 = 0ud401_726258394770132504928285306538183046669672962447608078920508735844923509262246775959219549178458104866085820235654365200
c     v120 = 0ud401_1263962471987452524487879878583968138394922976960183361142133083504386032345057028587060655279248917487608000791183360
c     v119 = 0ud401_161392310454210574888816402999622386500236689993107675591524354126948933545339844731751469507459982334016546255186952192
c     v118 = 0ud401_1657051382626256097412875152483006329299812531558634868187122631664028605631623053580306277436540631412351617225296183296
c     v117 = 0ud401_726287946425093406580999461162941076694573657234488285236411837535345358210319894068772219596085863242093769284829315072
c     v116 = 0ud401_494260304868512785854977816317477714655754049753265227796342319279017106758616473759104123556296034820822230933497184256
c     v115 = 0ud401_26485540851128394807701184729286590413084676336555848371216399398753602013657008774317535831357434723211820668001714176
c     v114 = 0ud401_496939727867073921442765415981843768974285346408841933898561417678544578068251426336616415240640041364787100669871915008
c     v113 = 0ud401_1261481658312217242853540576845257144082778362760791826701347134318150036979521793108895444525455327871371362544123904
c     v112 = 0ud401_601229194688794191944511796361931809113543210293907368448852122822199891042521452281638406930708392689832821248
c     v111 = 0ud401_1331590801814554822117976962145651306596751209946704813613889304356079471631458089173276404817977931197958883122993954816
c     v110 = 0ud401_728149691072263405451817940205131251679233506361339590326457635531206730060694402930627163490925343124948296781822689280
c     v109 = 0ud401_1331511995397712859335614864490428424807156344554471895757518207390428361118114327501740561313432065150115581730899361792
c     v108 = 0ud401_315218463872933169864846900007819415618244952805170004499508475350155140166654031943318515969407627123881603397320704
c     v107 = 0ud401_494260381863665215795427366871671484453055837031497952592100475581955815345855845583437120637452634486242371916523372544
c     v106 = 0ud401_1261480606167361984773244139351810840829611768061298702727465974223273859735893260632399676552350808501568272712335360
c     v105 = 0ud401_10087221437935821977934658860708789549428368744125681954989595418050698710129240132050797365699032274336957228411518976
c     v104 = 0ud401_2914679805565344004288651401730016151659978708838520457117598819206506061636479309594555040390328375769680484814448230400
c     v103 = 0ud401_2650733046797222528764557743701290896782806040297978199515097332494404628092584833137067997937653524500638319342184824832
c     v102 = 0ud401_2592208861598878105640082698627644868034391650574577064016687316039604044144953426565129572172193277233081008235047026688
c     v101 = 0ud401_2608735419087169438478507769472042227850996269793192011525545329208921188117130907796222928458387473304525626805472722944
c     v100 = 0ud401_161392002607230495033758705701943860188679749629055636297813571846176971454968207560094637508113495726257476057241223168
c     v99 = 0ud401_2607863663980391972179461018034836540814795577034842563372385821974510094422948237948477656431093076959209188949533655040
c     v98 = 0ud401_2612375184219674814499714754648236315435002387304129484699861496070563469576842493822044734223548029613788250261409497088
c     v97 = 0ud401_738236604465950726348243088454821729168478346596422335473773491421087193361865653114854574331386059434910507295599230976
c     v96 = 0ud401_2622996489769297785174312832840360527455179611236840874874367275322167169632861652310886554634836063828929377020934094848
c     v95 = 0ud401_737143198098835615366972795881855634196630837520474399462610972124058109840093499045816525056216946291666735262056054784
c     v94 = 0ud401_728149691067557146291806312420343909100702251354368909162026493798418127945800445288930394273586803663921994168629460992
c     v93 = 0ud401_3335616852894707288691761109532456580237482369475197354929178495195450042859772153791573008369125150956072389322007904256
c     v92 = 0ud401_736374859560450221706340705098071894028519236680538246645554365375034940788602188332124527708048333942671391185682038784
c     v91 = 0ud401_1331590811443450832263904766138199003960561639367671793618884128338465937934868024060434354714058178550934503638026944512
c     v90 = 0ud401_4239892317286076130512263127258563565667118865055823891390735293475296697187106570006631950819856459508471892788199292928
c     v89 = 0ud401_2467435202486415505960335466731759764467711144426736674561585983139190511070366025671293807159910375047650638561280
c     v88 = 0ud401_315216049864725900664205101661546977236441267032853919473527609802443934370302508359798617778046083206439092493484032
c     v87 = 0ud401_2643167849506795914922862677765609670000728364570172044551775287825864988214950515408925980328933964779910691685450907648
c     v86 = 0ud401_78806426694564614919321282038862551599586466589754594800679287623194557084818652758051382802993041582352323567419392
c     v85 = 0ud401_646833800480308860524738227479930736345312863436673715859713819208263393520169383404571096222516499416050918037060059136
c     v84 = 0ud401_2918930258764776933919911667695171487568190092198505824883835533371468059129780474271156910519931165291608836825149341696
c     v83 = 0ud401_726258395977283392334000275598401208417574803032276770540195211673561485654383215168429571367897819023091941867815698432
c     v82 = 0ud401_1775573836543171219486327472655953587676006148494309430317802839134873719101532052244370818761778823670778928412992995328
c     v81 = 0ud401_736374859560441047711876744812025450259270805276342684815739858872435934349312688977527359815092294312239618064266559488
c     v80 = 0ud401_161390925208605196466425512314806056799456000421903865511102181937654754116740979372082037813686059090362618090375610368
c     v79 = 0ud401_2462625387276894695509617810469533305098055682376341619012662153898182088931232915888772922779036914295400311029760
c     v78 = 0ud401_726258393868289859644457549320105102170699627339362195057019338526156060895171792136241600728431638706078890190088175616
c     v77 = 0ud401_2632236363671323150840920874379556294058271612808668178116503489004124662037410316209655389396643850574786134896636067840
c     v76 = 0ud401_25539907130686284580419162374106305267215897515169115980426732239987412444109241097033187678207521759493291761182179328
c     v75 = 0ud401_2648211311109602833871421514414138658640678312997378939707739751633359992764759108549012619292856022702476800048270147584
c     v74 = 0ud401_1334112616797723691196493779288045511270142458358753510760134758656989911015343949240255828759324138976414156305595367424
c     v73 = 0ud401_1223679093636088685361575913770391906681932120769627601139413422143239468531257002033339477690661626608000444163678011392
c     v72 = 0ud401_728149691067566320428441569817286251799334618102104409168925422052119414131750283433468710580957784500811656517038112768
c     v71 = 0ud401_461761085150917817868634528317786294092959308315963252078637032652061452134166698099653620647873867511565054377984
c     v70 = 0ud401_161392310435386684929175221785839584493941882356758775406254390352732808047355170737934339788164280411147065945489408000
c     v69 = 0ud401_726258394770132504928216954953034075841609030311810364635719850297390344403976106204168133020485271503057071886376632320
c     v68 = 0ud401_320141300639275210565739981924715840112608702088844211652934024394216372510690227028712839605578113760224289455341568
c     v67 = 0ud401_726258395977283392334052073544762895457886869788036120440324898420363192564663404341382128122908864207131629901456605184
c     v66 = 0ud401_2608750195290413262292040952958004949275271955733377488109033477915191145527997234349753128787919983865035615970663596032
c     v65 = 0ud401_733193147860704813625441989839208610620524332296145919892535898687638486271926155141601999722746447138048136072812036096
c     v64 = 0ud401_39404413452541822528042883041533456079372291536381276699994950981884098631506708152231096121045858461989913831145472
c     v63 = 0ud401_4239897242537007213854235364831122888851725200002245486444544067040504053943320956352501982717007068345108635165885726720
c     v62 = 0ud401_3313078982576389929601404335676175478379136922581774872768076964314569362566168333350426840097655000938451242887025786880
c     v61 = 0ud401_2607863673675175753863282830588390754419283574013938642113219399439935380867328080537705557309193633899461445677209354240
c     v60 = 0ud401_2608730494287315065061182214346809984482823286185869634077011940797064083974333152987047889747974705650796521532648587264
c     v59 = 0ud401_726258395822277288372295005715405283754611873049168208856830892245094215802327915132432914812074770880723268026165624832
c     v58 = 0ud401_1261480606167433658792244557943632556024990694646609867119495272902062076305905461239755253959928407292516520326856704
c     v57 = 0ud401_2591898588686802128733146592101911473247136393353892678709636721777834332911333349054951444661582343487836077795315810304
c     v56 = 0ud401_726258393868289859644457549320105101199365181226497659597288385114396607573968372610171840102524829373716940272896573440
c     v55 = 0ud401_20176294607756459772192828866740262028440504951852679411685756434519108937830734129290133351018847559418308903496056832
c     v54 = 0ud401_118208435239501112321340215405576611759193480137026938135746410554062147493894679167392584061727516069318430411456512
c     v53 = 0ud401_171477992713667128473485392702921600697460533676541691137693326407273240036560922313464190150550587592444387501908434944
c     v52 = 0ud401_39402008544972915536696154753321917969409520410059101055320659313368143035326368521102712372875981672460061392240640
c     v51 = 0ud401_20496435917496333042175510177446486979310248049542659130157528472586556580058896475050704887380173761429208267275370496
c     v50 = 0ud401_736512496631323754884441152288599539348184675874733150314882410141712965473549027969811290425122154645152527400994605056
c     v49 = 0ud401_2651361016205218660144475825181252453192075953327389845461956708073540883813594503310683208183324166418188320154197164032
c     v48 = 0ud401_2609378780495671347490256458904823780009582848429307519665279086053994030119249488140645095426997968567039712404166410240
c     v47 = 0ud401_20176294607756459772192828866740262027966220554336633960227476376837013856275556366238346129766054230291045518915141632
c     v46 = 0ud401_1331590801824242238851768209629573324890596654753413744011437528294055678533841036856949882328187248168923917602997141504
c     v45 = 0ud401_736354543558591462495405218282268182410725336923698280507358143610611088565147320266953336257064319348619107908750147584
c     v44 = 0ud401_26800752090884341120625277983708866061179984765724382919822828328972372052050972009792531040908570395509778110060953600
c     v43 = 0ud401_1291165572365280470731114538642138362922756669148432377490759306859211634816717998306837227164394849202006880466480660480
c     v42 = 0ud401_736354543502259624496940768923252413024524977710534879734512798414992256201880062860970860389704530587645708879358066688
c     v41 = 0ud401_21437178045301918952670069697919010418535596717548683764740914636001824654199928497455099331889425870560414023158858240
c     v40 = 0ud401_726258394619823485992091591910482445371783314601369206989151703319427506735384489301330741294013852068325333936122101760
c     v39 = 0ud401_315220859679935421474655819572438698840484093214269794763795088465787181542627974407409021428191961502050379815190528
c     v38 = 0ud401_2467435202486415505960335482646103329580880159704839058491193699754401345836468620043736262004949187177348272750592
c     v37 = 0ud401_60920429235454806763467887615112926283071582204386897922585345100794593961233154050292798371515491395798542585333547008
c     v36 = 0ud401_2607863663979213115010714492366778641325113074879289008550456072347628257500709167099569920805865129108766295066941587456
c     v35 = 0ud401_1331590888401081051451323867343853399739407015689132720288205700762796035901081587244456888156022149087965562663056965632
c     v34 = 0ud401_736344691821706609125096573423731942625373641456505276289166498906524031180784794804499995628375523915024613590756753408
c     v33 = 0ud401_3922469813048558045766115069362087318979091063124082426900738502776478516283762219896770207901632260506368080145926848512
c     v32 = 0ud401_3315443026022766765930123825134557050511336474039228062905760770857937123052051977331895241885573254034411615050897817600
c     v31 = 0ud401_60841625222915232808776713264820579270274251748715115291110447700322182135988366225766514421576987926615107636452917248
c     v30 = 0ud401_39402008544972898038692377228915047033026133669667490253687096782017061286981921474871103344878832597758399945375744
c     v29 = 0ud401_1331511997811408989548233874245569091543599776576381376472235308052946727843113068399569025707850646221544710538033889280
c     v28 = 0ud401_726268245421986107018761110916208996956835784923131819419839113438825987642113299774562355711952610266751887101445275648
c     v27 = 0ud401_1261480606167361984773244139351810840829611768061298702727465974217287549029385882279437383477544913253057573018402816
c     v26 = 0ud401_1221157211325432734026055632238982316427570776099841082339914798744343927817975025601384287068567610523274885953941929984
c     v25 = 0ud401_161391079141480241793456975740530786797575871846238680446548127314623764446753566363232111418537891767372586919814758528
c     v24 = 0ud401_484173391300988590610281473740153128937837322806820573115952679064690314281805379834060710566765181775861063639009067008
c     v23 = 0ud401_2918301057528137479030129251943378298656004078030751216291156914001789914461425424236291411461269082514572309365310619648
c     v22 = 0ud401_1143003189018026066078757686683078327717034390780862257011989151259461056211809585244788474859761164542395747067358085128
c     v21 = 0ud401_25534981879911735269936639020307630205801534606707341481191186988858968528552107274203983331919942604831552059257913344
c     v20 = 0ud401_728149691067566320426254319092503239874932473100141927017757200063318681970629304587631768996445287199145515307935727616
c     v19 = 0ud401_171477877611593991089606882076672699008611529650099079919475258371480689308177831778304554879021712184379976921521324032
c     v18 = 0ud401_736355158557345215642649993468137904655956354051187480393110222415147224348205016772189641504010619837703944517567119360
c     v17 = 0ud401_40633321238628162200345757056543918937012381617836338123349543806174057237704190342229764656747298378117678003912704
c     v16 = 0ud401_161392310435972691742425146781187062996830301983347456322634541381283335944298962846484127902624516336681544995349463040
c     v15 = 0ud401_2608730493836394889168674586177179179021907275520380629012379122216961069925172377529998368633851041277666495478999547904
c     v14 = 0ud401_1331590801824260478229890622420657356776035110074599013133766600766778128754963899533568647200484762966456993575434452992
c     v13 = 0ud401_2608750810946760152627610394511815323810059552556877985330099837635330523917462500016967764424288368808361193371951169536
c     v12 = 0ud401_39404422846712153896782135205289384149034001596096044799749488197519132475565990389185926978319530387201285513281536
c     v11 = 0ud401_320143714647482474845067649258560416207399452381037648740313164434480091343384113454225467910157888495793973881733120
c     v10 = 0ud401_3318122381645796573280958514780266739476522146496897892737393189454658285805646736789647482734954466456937439219767312384
c     v9 = 0ud401_1777977561062706700717197275061801665653521001110874070615111613322717885177973671444469544891832937064453958911647547392
c     v8 = 0ud401_1775298176411548363586206194116164391691924894566426401230916009884659272720193949214839480332124578237670464566339829824
c     v7 = 0ud401_2607784859968288165173085332228350606733449406033024181989422296691118722421162825602767101142786893207757149682043715584
c     v6 = 0ud401_494889736826632149626652280879754357245547595068084926680291012129779176096061580881656952303753638289193197610685431808
c     v5 = 0ud401_118208435239501711628038805942886718042247124089932631902394364414000227660610637578576731230747279613354825633234944
c     v4 = 0ud401_161391079141516937841309112051908440706246033486518051956465034745295820551283550195585766315449921398041155980731875328
c     v3 = 0ud401_726258394770132504928216954953034075841607177638382567576593073161821767340058689991708276149855042737308060720453189632
c     v2 = 0ud401_10087221433238736672420034175845037447484784043174323125465466465398511359944139598388576310649136579889097297476190208
c     v1 = 0ud401_3338138581554304130637552328293478733252261898513739554357885644669711904436340712127812170965812406591121784011527028736
c     v0 = 0ud401_0
c   -> State: 1.2 <-
c     state.tid = 4
c     state.vid = 429
c     state.target = 0ud401_78806426694564054299619886347748182914304347198746775990170001668282638385002133739335154249558701867612833534967808
c   -> State: 1.3 <-
c     state.token[4] = 0ud401_78806426694564054299619886347748182914304347198746775990170001668282638385002133739335154249558701867612833534967808
c     state.tid = 1
c     state.vid = 222
c     state.target = 0ud401_39402008544990833494633570057380460333247419169130046534527504493881346143374988678082856246155881377214583137107968
c   -> State: 1.4 <-
c     state.token[1] = 0ud401_39402008544990833494633570057380460333247419169130046534527504493881346143374988678082856246155881377214583137107968
c     state.tid = 4
c     state.vid = 273
c     state.target = 0ud401_3922179242492496608341196172494203685352841317739198297394149209711660163004790753097868203338845120293874420318465949696
c   -> State: 1.5 <-
c     state.token[4] = 0ud401_3922179242492496608341196172494203685352841317739198297394149209711660163004790753097868203338845120293874420318465949696
c     state.tid = 1
c     state.vid = 447
c     state.target = 0ud401_39402008544972898038692369080771141695081788595857776669508871211782666278340858246991470709206525117708621007814656
c   -> State: 1.6 <-
c     state.token[1] = 0ud401_39402008544972898038692369080771141695081788595857776669508871211782666278340858246991470709206525117708621007814656
c     state.tid = 6
c     state.vid = 16
c     state.target = 0ud401_161392310435385538179867359727792314206334493277679670671245307750076977148180042252525801839068750967572340612197777408
c   -> State: 1.7 <-
c     state.token[6] = 0ud401_161392310435385538179867359727792314206334493277679670671245307750076977148180042252525801839068750967572340612197777408
c     state.tid = 1
c     state.vid = 1
c     state.target = 0ud401_161392310435972691742425146781187062996830301983347456322634541381283335944298962846484127902624516336681544995349463040
s 17 27 326 329 464 495
t 106 164 222 273 447 464
a YES
a 17 27 326 329 464 495
a 17 164 326 329 464 495
a 17 106 164 329 464 495
a 17 106 164 239 464 495
a 106 164 239 429 464 495
a 106 164 222 429 464 495
a 106 164 222 273 464 495
a 106 164 222 273 447 464