Ticket #789: Bug.hs

File Bug.hs, 51.0 KB (added by dbueno, 7 years ago)

Triggers linkBCO: >= 64k insns in BCO

Line 
1module Bug where
2
3import Data.Set (Set)
4import qualified Data.Set as Set
5
6newtype Lit = L {unLit :: Int} deriving (Eq, Ord)
7inLit f = L . f . unLit
8
9instance Show Lit where
10    show l = if ul < 0 then "~" ++ show (abs ul) else show ul
11        where ul = unLit l
12instance Read Lit where
13    readsPrec i s = map (\(i,s) -> (L i, s)) (readsPrec i s :: [(Int, String)])
14
15instance Num Lit where
16    _ + _ = error "+ doesn't make sense for literals"
17    _ - _ = error "- doesn't make sense for literals"
18    _ * _ = error "* doesn't make sense for literals"
19    signum _ = error "signum doesn't make sense for literals"
20    negate   = inLit negate
21    abs      = inLit abs
22    fromInteger l | l == 0    = error "0 is not a literal"
23                  | otherwise = L $ fromInteger l
24
25type Clause = [Lit]
26
27data GenCNF a = CNF {
28      numVars :: Int,
29      numClauses :: Int,
30      clauses :: Set a
31    }
32                deriving (Show, Read, Eq)
33type CNF = GenCNF Clause
34
35
36prob :: CNF =
37    CNF {numVars = 765, numClauses = 3723, clauses = Set.fromList [[-765,-746,-764],[-764,-762,-761,-760,-759,-757,-756,-755,-753,-751,-750,-749,-748,-745,-744,-51,50],[-763,-746,-762],[-754,-303,-753],[-754,140,-761],[-752,-271,-751],[-747,-746,-745],[-743,51],[-742,51],[-741,51],[-740,51],[-739,596,737],[-738,-596,737],[-737,259,-407,-258,312,736],[-736,51],[-735,596,715],[-734,725],[-733,725],[-732,725],[-731,725],[-730,725],[-729,725],[-728,725],[-727,725],[-726,725],[-725,-717,-665,-630,-598,616,602,601,600,432,312,145,716],[-724,717],[-723,719,722],[-722,472,245,156,-158,121,115,71,721],[-721,717],[-720,717],[-719,-724],[-719,-720],[-719,-718],[-718,717],[-716,-596,715],[-715,536,-407,-258,-259,714],[-714,51],[-713,51],[-712,51],[-711,51],[-710,51],[-709,599,708],[-708,706],[-707,706],[-706,-597,596],[-705,598,597],[-704,702],[-703,702],[-702,-699,624,620,698],[-701,700,699],[-698,-619],[-697,629,628],[-696,665],[-695,681,694],[-694,-509,693],[-693,665],[-692,665],[-691,-690],[-690,665],[-689,665],[-688,665],[-687,665],[-686,665],[-685,599,684],[-684,682],[-683,682],[-682,-424,681],[-682,113,-424,-451,-441,-378,111,-110,161,90,63,696],[-681,-692],[-681,-690],[-681,-689],[-681,-688],[-681,-687],[-681,-686],[-681,-666],[-680,599,679],[-679,677],[-678,677],[-677,-494,-413,-205,-162,-278,112,-69,695],[-677,-413,676],[-676,-690],[-676,-688],[-676,-687],[-676,-686],[-676,-666],[-675,599,674],[-674,672],[-673,672],[-672,-57,671],[-671,-690],[-671,-686],[-671,-666],[-670,599,669],[-669,667],[-668,667],[-667,-54,691],[-666,665],[-665,-630,616,602,601,600,432,145,629],[-665,-630,616,602,601,600,432,312,145,700],[-664,630],[-663,648,662],[-662,-632,-498,-315,661],[-662,-498,733],[-661,630],[-660,630],[-659,-731],[-659,-658],[-658,630],[-657,630],[-656,630],[-655,630],[-654,630],[-653,630],[-652,599,651],[-651,649],[-650,649],[-649,-632,113,-424,-451,-441,111,-110,-334,-315,161,90,63,664],[-649,-424,648],[-649,113,-424,-451,-441,111,-110,-334,161,90,63,734],[-648,-732],[-648,-731],[-648,-730],[-648,-729],[-648,-728],[-648,-727],[-648,-726],[-648,-660],[-648,-658],[-648,-656],[-648,-655],[-648,-654],[-648,-653],[-648,-631],[-647,599,646],[-646,644],[-645,644],[-644,-494,-413,-205,-162,-278,112,-69,663],[-644,-413,643],[-643,-731],[-643,-729],[-643,-728],[-643,-727],[-643,-726],[-643,-658],[-643,-655],[-643,-654],[-643,-653],[-643,-631],[-642,599,641],[-641,639],[-640,639],[-639,-57,638],[-638,-731],[-638,-727],[-638,-726],[-638,-658],[-638,-653],[-638,-631],[-637,599,636],[-636,634],[-635,634],[-634,-54,659],[-633,599,632],[-632,-657],[-631,630],[-628,-625,620,624],[-627,599,626],[-626,625],[-624,-705],[-624,-704],[-624,-703],[-624,-698],[-624,-619],[-623,599,622],[-622,625],[-621,599,620],[-620,-705],[-620,-704],[-620,-703],[-620,-698],[-620,-624],[-620,-619],[-619,-598,597],[-618,599,598],[-617,616],[-616,-738],[-616,-731],[-616,-716],[-616,-707],[-616,-700],[-616,-690],[-616,-683],[-616,-678],[-616,-673],[-616,-668],[-616,-658],[-616,-657],[-616,-650],[-616,-645],[-616,-640],[-616,-635],[-616,-629],[-616,-599],[-615,602],[-614,610],[-613,612,611],[-612,-611],[-611,610],[-610,-615],[-610,-609],[-609,602],[-608,602],[-607,606,605],[-605,-608],[-605,432,427,426,285,71,-6,144,604],[-604,602],[-603,602],[-602,-738],[-602,-731],[-602,-716],[-602,-707],[-602,-700],[-602,-690],[-602,-683],[-602,-678],[-602,-673],[-602,-668],[-602,-658],[-602,-657],[-602,-650],[-602,-645],[-602,-640],[-602,-635],[-602,-629],[-602,-599],[-601,-738],[-601,-731],[-601,-716],[-601,-707],[-601,-700],[-601,-690],[-601,-683],[-601,-678],[-601,-673],[-601,-668],[-601,-658],[-601,-657],[-601,-650],[-601,-645],[-601,-640],[-601,-635],[-601,-629],[-601,-599],[-600,-738],[-600,-731],[-600,-716],[-600,-707],[-600,-700],[-600,-690],[-600,-683],[-600,-678],[-600,-673],[-600,-668],[-600,-658],[-600,-657],[-600,-650],[-600,-645],[-600,-640],[-600,-635],[-600,-629],[-600,-599],[-599,-708],[-599,-684],[-599,-679],[-599,-674],[-599,-669],[-599,-651],[-599,-646],[-599,-641],[-599,-636],[-598,-738],[-596,-743],[-596,-742],[-596,-741],[-596,-740],[-596,-713],[-596,-712],[-596,-711],[-596,-710],[-596,-595],[-595,51],[-594,-743],[-594,-593],[-593,51],[-592,257,590],[-591,-257,590],[-589,51],[-588,423,586],[-587,-681,694],[-587,-648,662],[-587,-423,586],[-586,-582,581],[-585,109,584],[-584,257,582],[-583,-257,582],[-581,51],[-580,51],[-579,51],[-578,572],[-577,572],[-576,572],[-575,572],[-574,572],[-573,572],[-572,-568,-451,-441,161,90,63,-113,587],[-572,-568,-451,-441,161,90,63,567],[-572,-451,90,63,606],[-571,568],[-570,568],[-569,568],[-567,-735],[-567,-719,722],[-567,-535],[-566,558],[-565,558],[-564,558],[-563,558],[-562,558],[-561,558],[-560,558],[-559,558],[-557,551],[-556,-723],[-556,-555],[-555,551],[-554,551],[-553,-720],[-553,-718],[-553,-570],[-553,-569],[-553,-554],[-553,-552],[-552,551],[-550,544],[-549,544],[-548,544],[-547,544],[-546,544],[-545,544],[-544,-537,-359,-313,161,90,-259,-145,63,583],[-544,-537,-359,-313,161,90,-145,63,536],[-543,539,542],[-542,471,96,-101,71,541],[-541,537],[-540,537],[-539,-720],[-539,-718],[-539,-554],[-539,-552],[-539,-540],[-539,-538],[-538,537],[-536,-714],[-536,-535],[-535,51],[-534,109,533],[-532,51],[-531,66,530],[-529,51],[-528,66,527],[-526,51],[-525,51],[-524,113,424],[-523,521],[-522,521],[-521,-513,512],[-520,516,515],[-519,517],[-518,517],[-517,-145,516],[-515,514,513],[-512,-719],[-512,-425],[-512,616],[-511,461,460],[-510,377,509],[-508,500],[-507,500],[-506,500],[-505,500],[-504,500],[-503,500],[-502,500],[-501,500],[-500,-462,-145,461],[-499,333,498],[-497,462],[-496,494],[-495,494],[-494,-413,-509,-205,-162,-278,112,-148,-69,508],[-494,-413,-498,-315,-205,-162,-278,112,-155,-153,-69,497],[-494,-413,-498,-205,-162,-278,112,-155,-69,566],[-494,-413,-108,-205,-162,-278,112,-69,588],[-494,-205,-162,-278,112,493],[-493,-740],[-493,-732],[-493,-692],[-493,-660],[-493,-580],[-493,-565],[-493,-507],[-493,-470],[-492,487],[-491,487],[-490,487],[-489,487],[-488,487],[-487,-484,63,556],[-487,-484,415,-542,87,76,71,63,19,-40,557],[-487,-484,415,471,96,-101,87,76,71,63,19,-40,571],[-486,-718],[-486,-569],[-486,-552],[-486,-495],[-486,-485],[-485,484],[-483,478],[-482,478],[-481,478],[-480,478],[-479,478],[-478,-473,-205,-162,112,63,472],[-478,-473,471,-327,-67,-205,-162,112,-68,63,499],[-477,59,19,-18,496],[-477,63,59,19,-18,476],[-476,473],[-475,-718],[-475,-569],[-475,-552],[-475,-538],[-475,-495],[-475,-474],[-474,473],[-472,-740],[-472,-732],[-472,-721],[-472,-692],[-472,-660],[-472,-580],[-472,-565],[-472,-555],[-472,-539,542],[-472,-507],[-472,-470],[-471,-740],[-471,-732],[-471,-692],[-471,-660],[-471,-585],[-471,-580],[-471,-571],[-471,-565],[-471,-543],[-471,-541],[-471,-510],[-471,-507],[-471,-499],[-471,-475,477],[-471,-470],[-470,462],[-469,462],[-468,462],[-467,462],[-466,462],[-465,462],[-464,462],[-463,462],[-460,440,439],[-459,451],[-458,451],[-457,451],[-456,451],[-455,451],[-454,-506],[-454,-504],[-454,-503],[-454,-502],[-454,-501],[-454,-459],[-454,-457],[-454,-456],[-454,-455],[-454,-452],[-453,-506],[-453,-502],[-453,-501],[-453,-459],[-453,-455],[-453,-452],[-452,451],[-451,-441,-359,-313,90,-145,63,519],[-451,-441,90,63,440],[-451,-441,161,90,63,514],[-451,-295,90,63,614],[-451,90,63,612],[-450,441],[-449,441],[-448,441],[-447,441],[-446,441],[-445,441],[-444,-578],[-444,-576],[-444,-575],[-444,-574],[-444,-573],[-444,-564],[-444,-562],[-444,-561],[-444,-560],[-444,-559],[-444,-468],[-444,-466],[-444,-465],[-444,-464],[-444,-463],[-444,-449],[-444,-447],[-444,-446],[-444,-445],[-444,-442],[-443,-578],[-443,-574],[-443,-573],[-443,-564],[-443,-560],[-443,-559],[-443,-468],[-443,-464],[-443,-463],[-443,-449],[-443,-445],[-443,-442],[-442,441],[-440,-739],[-440,-579],[-440,-518],[-439,-436,432,435],[-438,436],[-437,436],[-435,-719],[-435,-524],[-435,-523],[-435,-522],[-435,-425],[-435,616],[-434,432],[-433,432],[-432,-738],[-432,-731],[-432,-719],[-432,-716],[-432,-707],[-432,-700],[-432,-690],[-432,-683],[-432,-678],[-432,-673],[-432,-668],[-432,-658],[-432,-657],[-432,-650],[-432,-645],[-432,-640],[-432,-635],[-432,-629],[-432,-617],[-432,-615],[-432,-609],[-432,-608],[-432,-604],[-432,-603],[-432,-599],[-432,-524],[-432,-523],[-432,-522],[-432,-435],[-432,-425],[-431,427],[-431,601],[-430,427],[-430,601],[-429,427],[-429,601],[-428,427],[-428,601],[-427,-719],[-427,-617],[-427,-615],[-427,-609],[-427,-608],[-427,-604],[-427,-603],[-427,-524],[-427,-523],[-427,-522],[-427,-438],[-427,-437],[-427,-425],[-426,-719],[-426,-617],[-426,-615],[-426,-609],[-426,-608],[-426,-604],[-426,-603],[-426,-524],[-426,-523],[-426,-522],[-426,-438],[-426,-437],[-426,-425],[-425,-113,424],[-424,-256,423],[-423,-743],[-423,-740],[-423,-713],[-423,-712],[-423,-711],[-423,-710],[-423,-595],[-423,-593],[-423,-580],[-423,-532],[-423,-529],[-423,-526],[-423,-525],[-423,-52],[-422,69,413],[-421,419],[-420,419],[-419,-416,415],[-418,161,417],[-417,-63,416],[-415,-724],[-415,-723],[-415,-571],[-415,-557],[-415,-555],[-415,-553],[-415,-414],[-415,432],[-414,-69,413],[-413,-155,444],[-413,-148,454],[-413,-108,412],[-412,-743],[-412,-712],[-412,-711],[-412,-710],[-412,-595],[-412,-593],[-412,-529],[-412,-526],[-412,-525],[-412,-52],[-411,-743],[-411,-710],[-411,-595],[-411,-593],[-411,-525],[-411,-52],[-410,407],[-409,145,408],[-408,407],[-407,-258,257],[-406,259,258],[-405,403],[-404,403],[-403,-400,399],[-402,-700,699],[-402,-516,515],[-402,401,400],[-399,-261],[-398,-629,628],[-398,-461,460],[-398,312,311],[-397,-690],[-397,-506],[-397,-395],[-396,-506],[-396,-459],[-396,-395],[-395,359],[-394,377,393],[-393,-185,165,-74,63,392],[-392,359],[-391,370,390],[-389,359],[-388,370,387],[-386,359],[-385,359],[-384,145,90,63,383],[-383,378],[-382,378],[-381,90,-145,63,380],[-380,378],[-379,378],[-378,-110,377],[-377,-692],[-377,-690],[-377,-688],[-377,-687],[-377,-686],[-377,-666],[-377,-507],[-377,-506],[-377,-504],[-377,-503],[-377,-502],[-377,-501],[-377,-395],[-377,-389],[-377,-386],[-377,-385],[-377,-360],[-376,112,145,382],[-376,145,63,375],[-375,371],[-374,371],[-373,371],[-372,371],[-371,-478,-473,471,-67,-205,-162,112,-68,63,510],[-371,-67,370],[-371,68,-67,63,394],[-370,-690],[-370,-686],[-370,-666],[-370,-506],[-370,-502],[-370,-501],[-370,-395],[-370,-385],[-370,-360],[-369,145,59,-61,64,374],[-369,145,368],[-368,366],[-367,366],[-366,25,63,-57,388],[-366,63,-57,-25,391],[-366,63,-57,365],[-365,-690],[-365,-686],[-365,-666],[-365,-506],[-365,-502],[-365,-501],[-365,-395],[-365,-385],[-365,-360],[-364,145,363],[-363,361],[-362,361],[-361,-54,397],[-360,359],[-359,-313,90,-145,63,312],[-359,-313,161,90,-145,63,401],[-358,313],[-357,-731],[-357,-658],[-357,-564],[-357,-550],[-357,-468],[-357,-355],[-356,-578],[-356,-564],[-356,-550],[-356,-468],[-356,-449],[-356,-355],[-355,313],[-354,333,352],[-353,-377,393],[-353,-333,352],[-353,-109,533],[-352,-315,-227,165,-221,-74,63,351],[-352,165,-221,-74,63,549],[-351,313],[-350,326,347],[-349,-718],[-349,-569],[-349,-552],[-349,-538],[-349,-495],[-349,-485],[-349,-474],[-349,-471],[-349,-348],[-349,475,477],[-349,484],[-348,-370,390],[-348,-326,347],[-348,-66,530],[-346,313],[-345,326,343],[-344,-370,387],[-344,-326,343],[-344,-66,527],[-342,313],[-341,313],[-340,145,90,63,339],[-339,334],[-338,334],[-337,90,-145,63,336],[-336,334],[-335,334],[-333,-732],[-333,-731],[-333,-729],[-333,-728],[-333,-727],[-333,-726],[-333,-660],[-333,-658],[-333,-655],[-333,-654],[-333,-653],[-333,-631],[-333,-565],[-333,-564],[-333,-562],[-333,-561],[-333,-560],[-333,-559],[-333,-550],[-333,-548],[-333,-547],[-333,-546],[-333,-545],[-333,-470],[-333,-468],[-333,-466],[-333,-465],[-333,-464],[-333,-463],[-333,-355],[-333,-346],[-333,-342],[-333,-341],[-333,-314],[-332,112,145,338],[-332,145,63,331],[-331,327],[-330,327],[-329,327],[-328,327],[-327,-67,326],[-326,-731],[-326,-727],[-326,-726],[-326,-658],[-326,-653],[-326,-631],[-326,-564],[-326,-560],[-326,-559],[-326,-550],[-326,-546],[-326,-545],[-326,-468],[-326,-464],[-326,-463],[-326,-355],[-326,-341],[-326,-314],[-325,145,59,-61,64,330],[-325,145,324],[-324,322],[-323,322],[-322,25,63,-57,345],[-322,63,-57,-25,350],[-322,63,-57,321],[-321,-731],[-321,-727],[-321,-726],[-321,-658],[-321,-653],[-321,-631],[-321,-564],[-321,-560],[-321,-559],[-321,-550],[-321,-546],[-321,-545],[-321,-468],[-321,-464],[-321,-463],[-321,-355],[-321,-341],[-321,-314],[-320,145,319],[-319,317],[-318,317],[-317,-54,357],[-316,-599,632],[-316,145,315],[-315,-657],[-315,-469],[-315,-358],[-314,313],[-312,-736],[-312,-716],[-312,-700],[-312,-579],[-312,-518],[-311,-306,300,305],[-310,-599,626],[-310,145,309],[-309,269,115,266,264,308],[-308,306],[-307,306],[-305,-406],[-305,-405],[-305,-404],[-305,-261],[-304,-112,303],[-303,-158,-744],[-303,121,115,71,302],[-302,300],[-301,300],[-300,-406],[-300,-405],[-300,-404],[-300,-305],[-300,-261],[-299,269],[-298,294,112,297],[-297,290],[-296,290],[-295,294,90,63,293],[-294,-297],[-294,-293],[-293,290],[-292,-162,112,90,63,291],[-291,290],[-290,-299],[-290,-287],[-289,-112,288],[-288,-752,-760],[-287,269],[-286,269],[-285,-604],[-285,-112,284],[-284,-273],[-283,-606,605],[-283,277,276],[-282,278],[-281,278],[-280,278],[-279,278],[-276,-286],[-275,-112,274],[-274,-752,-759],[-273,269],[-272,-112,271],[-270,269],[-269,-406],[-269,-405],[-269,-404],[-269,-308],[-269,-307],[-269,-261],[-268,145,267],[-267,266],[-266,-406],[-266,-405],[-266,-404],[-266,-308],[-266,-307],[-266,-261],[-265,-599,620],[-265,145,264],[-264,-406],[-264,-405],[-264,-404],[-264,-308],[-264,-307],[-264,-261],[-263,-599,622],[-263,145,262],[-261,-259,258],[-260,-599,598],[-260,145,259],[-259,-736],[-259,-591],[-259,-579],[-257,-743],[-257,-740],[-257,-713],[-257,-712],[-257,-711],[-257,-710],[-257,-595],[-257,-593],[-257,-580],[-257,-532],[-257,-529],[-257,-526],[-257,-525],[-257,-52],[-256,-145,410],[-256,90,63,255],[-255,253],[-254,253],[-253,-110,109],[-253,111,-110,161,592],[-252,111,110],[-251,249],[-250,249],[-249,-246,245],[-248,-514,513],[-248,-401,400],[-248,-161,417],[-248,247,246],[-245,-721],[-245,-555],[-245,-539],[-245,-114],[-245,300],[-244,-440,439],[-244,-312,311],[-244,161,160],[-243,205],[-242,205],[-241,165,239],[-240,-165,239],[-239,164,209,238,63,482],[-239,164,209,238,282],[-238,-491],[-238,-482],[-238,-282],[-238,-240],[-238,-237],[-237,205],[-236,220,235],[-235,165,233],[-234,-165,233],[-233,164,-210,-24,281],[-233,164,-210,63,-24,481],[-232,205],[-231,165,229],[-230,-165,229],[-229,164,209,53,-208,-54,280],[-229,164,209,53,-208,63,-54,480],[-228,205],[-227,-450],[-227,-358],[-227,-243],[-227,-239,164,209,238,-207,237],[-227,-233,164,-210,-207,-24,232],[-227,-229,164,209,53,-208,-207,-54,228],[-227,-211,164,209,-208,-207,-54,-53,206],[-227,-165,-207,-164,242],[-226,221],[-225,221],[-224,112,63,223],[-223,221],[-222,221],[-221,-74,220],[-220,-578],[-220,-576],[-220,-550],[-220,-548],[-220,-449],[-220,-447],[-220,-355],[-220,-346],[-220,-241],[-220,-231],[-220,-213],[-219,-145,59,-61,64,328],[-219,-145,323],[-219,-57,443],[-219,90,63,59,-61,64,225],[-219,90,63,218],[-218,216],[-217,216],[-216,63,-57,215],[-215,-578],[-215,-550],[-215,-449],[-215,-355],[-215,-241],[-215,-231],[-215,-213],[-214,-145,318],[-214,-54,356],[-213,165,211],[-212,-165,211],[-211,164,209,-208,-54,-53,279],[-211,164,209,-208,63,-54,-53,479],[-210,-24,209],[-210,112,59,-61,64,222],[-210,112,217],[-209,-491],[-209,-489],[-209,-488],[-209,-482],[-209,-480],[-209,-479],[-209,-282],[-209,-280],[-209,-279],[-209,-240],[-209,-237],[-209,-230],[-209,-228],[-209,-212],[-209,-206],[-208,-54,238],[-207,-243],[-207,112,227],[-206,205],[-205,-162,112,63,247],[-205,-162,112,161],[-204,165,202],[-203,-165,202],[-202,173,201,164,200],[-201,-203],[-201,-200],[-200,162],[-199,184,198],[-198,165,196],[-197,-165,196],[-196,-174,164,-24,195],[-195,162],[-194,165,192],[-193,-165,192],[-192,173,-172,164,53,-54,191],[-191,162],[-190,185],[-189,185],[-188,112,63,187],[-187,185],[-186,185],[-185,-74,184],[-184,-459],[-184,-457],[-184,-395],[-184,-389],[-184,-204],[-184,-194],[-184,-177],[-183,-145,59,-61,64,372],[-183,-145,367],[-183,-57,453],[-183,90,63,59,-61,64,189],[-183,90,63,182],[-182,180],[-181,180],[-180,25,63,-57,199],[-180,63,-57,179],[-179,-459],[-179,-395],[-179,-204],[-179,-194],[-179,-177],[-178,-145,362],[-178,-54,396],[-177,165,175],[-176,-165,175],[-175,173,-172,164,-54,-53,171],[-174,-24,173],[-174,112,59,-61,64,186],[-174,112,181],[-174,164,-24,197],[-173,-203],[-173,-200],[-173,-193],[-173,-191],[-173,-176],[-173,-171],[-172,-54,201],[-171,162],[-170,169],[-168,165],[-167,165],[-167,754],[-166,165],[-166,758],[-165,-578],[-165,-577],[-165,-576],[-165,-550],[-165,-549],[-165,-548],[-165,-459],[-165,-458],[-165,-457],[-165,-449],[-165,-448],[-165,-447],[-165,-395],[-165,-392],[-165,-389],[-165,-355],[-165,-351],[-165,-346],[-165,-164,163],[-165,63,-164,483],[-164,-491],[-164,-490],[-164,-489],[-164,-488],[-164,-482],[-164,-481],[-164,-480],[-164,-479],[-164,-282],[-164,-281],[-164,-280],[-164,-279],[-164,-240],[-164,-237],[-164,-234],[-164,-232],[-164,-230],[-164,-228],[-164,-212],[-164,-206],[-164,-203],[-164,-200],[-164,-197],[-164,-195],[-164,-193],[-164,-191],[-164,-176],[-164,-171],[-163,162],[-163,278],[-162,-278,112,277],[-162,112,-138,296],[-162,112,294],[-161,-734],[-161,-696],[-161,-664],[-161,-592],[-161,-587],[-161,-583],[-161,-567],[-161,-536],[-161,-514],[-161,-401],[-160,-157,121,71,156],[-160,-157,121,115,71,301],[-159,-112,158],[-158,157],[-156,-721],[-156,-555],[-156,-539],[-156,-252],[-156,-251],[-156,-250],[-156,-114],[-155,-150,149],[-154,-145,309],[-154,150],[-153,-469],[-153,-450],[-153,-145,315],[-153,-142,152],[-153,-112,227],[-152,150],[-151,150],[-149,147],[-148,147],[-147,144,143,-69,-8,146],[-146,145],[-145,-738],[-145,-731],[-145,-716],[-145,-700],[-145,-690],[-145,-658],[-145,-657],[-145,-629],[-145,-408],[-145,-383],[-145,-382],[-145,-375],[-145,-374],[-145,-368],[-145,-363],[-145,-339],[-145,-338],[-145,-331],[-145,-330],[-145,-324],[-145,-319],[-145,-304],[-145,-289],[-145,-275],[-145,-272],[-145,-159],[-145,-155,63,329],[-145,-148,63,373],[-145,-141],[-144,-719],[-144,-615],[-144,-609],[-144,-608],[-144,-604],[-144,-603],[-144,-524],[-144,-523],[-144,-522],[-144,-438],[-144,-437],[-144,-425],[-144,-289],[-144,-275],[-144,-272],[-144,-159],[-144,-146],[-144,-145,264],[-144,-141],[-143,-304],[-143,-289],[-143,-275],[-143,-272],[-143,-159],[-143,-146],[-143,-145,267],[-143,-141],[-143,426],[-142,-145,262],[-142,-113,151],[-141,-112,140],[-140,-303,-750],[-140,157],[-140,761],[-139,121],[-139,266],[-138,-431],[-138,-430],[-138,63,137],[-137,135],[-136,135],[-135,-139],[-135,-132],[-134,63,133],[-132,121],[-132,266],[-131,121],[-131,266],[-130,63,129],[-129,125,-127,131],[-129,127,-125,124],[-128,-428],[-128,63,127],[-128,112,284],[-127,-124],[-126,-429],[-126,-277,276],[-126,63,125],[-125,-131],[-124,121],[-124,266],[-123,63,122],[-123,427],[-123,601],[-122,121],[-122,266],[-121,-721],[-121,-555],[-121,-539],[-121,-302],[-121,-301],[-121,-299],[-121,-287],[-121,-286],[-121,-273],[-121,-270],[-121,-252],[-121,-251],[-121,-250],[-121,-156],[-121,-114],[-120,63,119],[-119,-101,-748],[-119,71,118],[-118,115],[-117,-101,-755],[-117,-74,-756],[-117,71,116],[-116,115],[-115,-721],[-115,-555],[-115,-539],[-115,-406],[-115,-405],[-115,-404],[-115,-308],[-115,-307],[-115,-302],[-115,-301],[-115,-261],[-115,-252],[-115,-251],[-115,-250],[-115,-114],[-114,-111,110],[-113,-742],[-113,-739],[-113,-734],[-113,-696],[-113,-664],[-113,-589],[-113,-579],[-113,-145,259],[-113,-112,111],[-112,-723],[-112,-695],[-112,-663],[-112,-588],[-112,-585],[-112,-566],[-112,-555],[-112,-510],[-112,-508],[-112,-499],[-112,-497],[-112,-493],[-112,-472],[-112,-382],[-112,-379],[-112,-353],[-112,-338],[-112,-335],[-112,-297],[-112,-296],[-112,-294],[-112,-291],[-112,-277],[-112,-254],[-112,-247],[-112,-243],[-112,-241],[-112,-223],[-112,-222],[-112,-217],[-112,-204],[-112,-187],[-112,-186],[-112,-181],[-112,-161],[-111,-734],[-111,-696],[-111,-664],[-111,-592],[-111,-377,509],[-111,-353],[-111,-333,498],[-111,-109,584],[-111,156,-140,121,115,71,251],[-110,-334,333],[-109,-743],[-109,-740],[-109,-712],[-109,-711],[-109,-710],[-109,-595],[-109,-593],[-109,-580],[-109,-529],[-109,-526],[-109,-525],[-109,-52],[-108,63,107],[-108,112,254],[-107,105],[-106,105],[-105,-478,-473,471,-67,-205,-162,112,-68,63,585],[-105,-67,66],[-105,68,-67,63,534],[-104,68,67],[-103,99],[-103,757],[-102,63,101],[-101,71,100],[-100,99],[-100,757],[-99,-97,96],[-98,-247,246],[-98,63,97],[-98,63,416],[-96,-571],[-96,-543],[-96,-541],[-96,-475],[-96,-70],[-96,115],[-95,92],[-94,92],[-93,92],[-92,-167],[-92,-90],[-92,-12,-8,170],[-91,-167],[-91,-90],[-91,164],[-91,169],[-90,-742],[-90,-734],[-90,-696],[-90,-664],[-90,-614],[-90,-612],[-90,-606],[-90,-591],[-90,-589],[-90,-587],[-90,-583],[-90,-578],[-90,-567],[-90,-550],[-90,-536],[-90,-519],[-90,-514],[-90,-459],[-90,-450],[-90,-449],[-90,-440],[-90,-401],[-90,-395],[-90,-383],[-90,-380],[-90,-358],[-90,-355],[-90,-339],[-90,-336],[-90,-312],[-90,-293],[-90,-291],[-90,-255],[-90,-231],[-90,-226],[-90,-225],[-90,-218],[-90,-213],[-90,-194],[-90,-190],[-90,-189],[-90,-182],[-90,-177],[-90,-112],[-90,-75],[-90,145],[-90,165],[-90,754],[-89,-168],[-89,-167],[-89,-161,160],[-89,-90],[-87,-724],[-87,-723],[-87,-571],[-87,-557],[-87,-555],[-87,-553],[-87,-422],[-87,-421],[-87,-420],[-87,-414],[-87,-102],[-87,-75],[-87,63,117],[-86,76],[-86,266],[-86,426],[-86,600],[-85,-86],[-85,-83],[-85,59,-61,64,136],[-84,-63,133],[-83,76],[-83,266],[-83,426],[-83,600],[-82,-63,122],[-82,76],[-82,266],[-82,426],[-82,600],[-81,76],[-81,266],[-81,426],[-81,600],[-80,-79,78,77],[-80,-63,129],[-80,79,-78,81],[-79,-81],[-79,-63,125],[-78,-77],[-78,-63,127],[-77,76],[-77,266],[-77,426],[-77,600],[-76,-724],[-76,-723],[-76,-571],[-76,-557],[-76,-555],[-76,-553],[-76,-434],[-76,-433],[-76,-431],[-76,-430],[-76,-429],[-76,-428],[-76,-422],[-76,-421],[-76,-420],[-76,-414],[-76,-304],[-76,-289],[-76,-275],[-76,-272],[-76,-168],[-76,-167],[-76,-159],[-76,-141],[-76,-134],[-76,-130],[-76,-123],[-76,-120],[-76,-102],[-76,-90],[-76,-87],[-76,-75],[-75,63,74],[-74,-119,-749],[-74,71,-68,103],[-74,71,104],[-73,71],[-73,266],[-73,601],[-72,71],[-72,266],[-72,601],[-71,-724],[-71,-723],[-71,-721],[-71,-719],[-71,-617],[-71,-615],[-71,-609],[-71,-608],[-71,-604],[-71,-603],[-71,-571],[-71,-557],[-71,-555],[-71,-553],[-71,-543],[-71,-541],[-71,-539],[-71,-524],[-71,-523],[-71,-522],[-71,-475],[-71,-438],[-71,-437],[-71,-434],[-71,-433],[-71,-425],[-71,-422],[-71,-421],[-71,-420],[-71,-414],[-71,-302],[-71,-301],[-71,-299],[-71,-287],[-71,-286],[-71,-273],[-71,-270],[-71,-252],[-71,-251],[-71,-250],[-71,-156],[-71,-118],[-71,-116],[-71,-114],[-71,-104],[-71,-103],[-71,-100],[-71,-70],[-70,-68,67],[-69,-730],[-69,-713],[-69,-689],[-69,-656],[-69,-577],[-69,-563],[-69,-532],[-69,-505],[-69,-467],[-69,-458],[-69,-448],[-69,-8,93],[-69,63,68],[-69,112,111],[-68,-534],[-68,-394],[-68,-354],[-68,-344],[-66,-743],[-66,-710],[-66,-595],[-66,-593],[-66,-525],[-66,-52],[-65,-57,411],[-65,25,63,-57,528],[-65,59,-61,64,106],[-65,63,-57,-25,531],[-65,63,-57,56],[-64,-471],[-64,-374],[-64,-372],[-64,-348],[-64,-344],[-64,-330],[-64,-328],[-64,-225],[-64,-222],[-64,-189],[-64,-186],[-64,-168],[-64,-166],[-64,-136],[-64,-106],[-64,-63],[-63,-742],[-63,-740],[-63,-734],[-63,-732],[-63,-724],[-63,-696],[-63,-692],[-63,-664],[-63,-660],[-63,-614],[-63,-612],[-63,-606],[-63,-591],[-63,-589],[-63,-587],[-63,-585],[-63,-583],[-63,-580],[-63,-578],[-63,-577],[-63,-576],[-63,-571],[-63,-567],[-63,-565],[-63,-557],[-63,-556],[-63,-550],[-63,-549],[-63,-548],[-63,-536],[-63,-534],[-63,-531],[-63,-528],[-63,-519],[-63,-514],[-63,-510],[-63,-507],[-63,-499],[-63,-492],[-63,-491],[-63,-490],[-63,-489],[-63,-488],[-63,-483],[-63,-482],[-63,-481],[-63,-480],[-63,-479],[-63,-476],[-63,-472],[-63,-470],[-63,-459],[-63,-458],[-63,-457],[-63,-450],[-63,-449],[-63,-448],[-63,-447],[-63,-440],[-63,-401],[-63,-395],[-63,-394],[-63,-392],[-63,-391],[-63,-389],[-63,-388],[-63,-383],[-63,-380],[-63,-375],[-63,-373],[-63,-365],[-63,-358],[-63,-355],[-63,-354],[-63,-351],[-63,-350],[-63,-349],[-63,-346],[-63,-345],[-63,-339],[-63,-336],[-63,-331],[-63,-329],[-63,-321],[-63,-312],[-63,-293],[-63,-291],[-63,-255],[-63,-247],[-63,-236],[-63,-231],[-63,-226],[-63,-225],[-63,-223],[-63,-220,235],[-63,-218],[-63,-215],[-63,-213],[-63,-199],[-63,-194],[-63,-190],[-63,-189],[-63,-187],[-63,-184,198],[-63,-182],[-63,-179],[-63,-177],[-63,-137],[-63,-112],[-63,-107],[-63,-56],[-63,145],[-63,165],[-63,758],[-62,25,57],[-61,-60,59],[-60,-63,97],[-59,-720],[-59,-570],[-59,-554],[-59,-496],[-59,-486],[-59,-476],[-59,-471],[-59,-374],[-59,-372],[-59,-349],[-59,-348],[-59,-344],[-59,-330],[-59,-328],[-59,-225],[-59,-222],[-59,-189],[-59,-186],[-59,-168],[-59,-166],[-59,-136],[-59,-106],[-59,-63],[-59,-58],[-59,71],[-59,266],[-59,601],[-58,-25,57],[-56,-743],[-56,-710],[-56,-595],[-56,-593],[-56,-525],[-56,-52],[-55,-54,594],[-53,-727],[-53,-710],[-53,-686],[-53,-653],[-53,-574],[-53,-560],[-53,-546],[-53,-525],[-53,-502],[-53,-489],[-53,-480],[-53,-464],[-53,-455],[-53,-445],[-53,-385],[-53,-341],[-53,-280],[-53,-231],[-53,-230],[-53,-228],[-53,-194],[-53,-193],[-53,-191],[-52,51],[-50,1],[-49,145,747],[-47,-42,-46],[-47,145,763],[-45,-43],[-44,-47],[-43,-42,-41],[-43,145,765],[-42,-49,-48],[-42,145,746],[-40,88],[-40,92],[-40,112,158],[-38,-145,747],[-38,-4,-37],[-35,-63,119],[-35,-24,-34],[-35,-18,-36],[-32,112,271],[-30,-40,-39],[-30,-9,-29],[-30,-8,-33],[-30,112,303],[-27,-63,117],[-27,-24,-26],[-27,-18,-28],[-25,-728],[-25,-711],[-25,-687],[-25,-654],[-25,-575],[-25,-561],[-25,-528],[-25,-526],[-25,-503],[-25,-465],[-25,-456],[-25,-446],[-25,-388],[-25,-345],[-25,-236],[-25,-199],[-25,-63,68],[-25,19,-24,23],[-24,-63,74],[-23,15],[-23,61],[-22,19],[-22,266],[-22,426],[-22,600],[-21,19],[-21,266],[-21,426],[-21,600],[-20,19],[-20,266],[-20,426],[-20,600],[-19,-724],[-19,-723],[-19,-720],[-19,-571],[-19,-570],[-19,-557],[-19,-555],[-19,-554],[-19,-553],[-19,-496],[-19,-486],[-19,-476],[-19,-434],[-19,-433],[-19,-431],[-19,-430],[-19,-429],[-19,-428],[-19,-422],[-19,-421],[-19,-420],[-19,-414],[-19,-349],[-19,-304],[-19,-289],[-19,-275],[-19,-272],[-19,-167],[-19,-159],[-19,-141],[-19,-134],[-19,-130],[-19,-123],[-19,-120],[-19,-102],[-19,-90],[-19,-87],[-19,-75],[-19,-73],[-19,-72],[-19,-62],[-19,-58],[-19,-23],[-19,-17],[-18,-63,101],[-17,15],[-17,61],[-16,164],[-14,112,274],[-12,-95],[-12,-32,-31],[-12,-14,-13],[-12,-11,-10],[-12,112,752],[-11,112,288],[-9,8,-7],[-9,164],[-8,7],[-8,88],[-8,112,140],[-6,-145,763],[-6,-4,-5],[-6,150],[-4,-145,746],[-4,-112,752],[-4,-3,-2],[-3,-145,765],[-1],[2,1],[3,-609],[3,-289],[3,-145,-765],[3,2],[4,-145,-746],[4,-112,-752],[4,2],[4,5],[4,37],[5,1],[6,-615],[6,-608],[6,-604],[6,-275],[6,-145,-763],[6,5],[7,1],[8,-422],[8,-421],[8,-414],[8,-170],[8,-146],[8,-95],[8,-93],[8,-90],[8,-75],[8,33],[8,40,-88],[8,112,-140],[9,-167],[9,7],[9,29],[10,1],[11,-430],[11,-134],[11,10],[11,112,-288],[12,-170],[12,-90],[12,-8,95],[12,10],[12,13],[12,31],[12,112,-752],[13,1],[14,-431],[14,-429],[14,-428],[14,-130],[14,13],[14,112,-274],[15,1],[16,-166],[16,15],[18,-720],[18,-570],[18,-554],[18,-496],[18,-486],[18,-476],[18,-349],[18,-63,-101],[18,-17],[18,28],[18,36],[19,-35,73],[19,-27,72],[19,-24,62],[19,-18,17],[22,21,20,-19],[23,17,-61],[23,17,-16,-15],[24,-490],[24,-481],[24,-281],[24,-234],[24,-232],[24,-209],[24,-197],[24,-195],[24,-173],[24,-63,-74],[24,-62],[24,-58],[24,-23],[24,26],[24,34],[25,-729],[25,-712],[25,-688],[25,-655],[25,-576],[25,-562],[25,-548],[25,-531],[25,-529],[25,-504],[25,-466],[25,-457],[25,-447],[25,-391],[25,-389],[25,-350],[25,-346],[25,-216,63,-57,236],[25,-63,-68],[25,-23],[26,1],[27,-72],[27,-63,-117],[27,26],[27,28],[28,1],[29,1],[30,-434],[30,-120],[30,29],[30,33],[30,39],[30,112,-303],[31,1],[32,-123],[32,31],[32,112,-271],[33,1],[34,1],[35,-73],[35,-63,-119],[35,34],[35,36],[36,1],[37,1],[38,-603],[38,-272],[38,-145,-747],[38,37],[39,1],[40,-724],[40,-723],[40,-571],[40,-557],[40,-555],[40,-553],[40,-420],[40,-102],[40,39],[40,112,-158],[41,1],[42,41],[42,46],[42,48],[42,145,-746],[43,41],[43,145,-765],[44,-45,47],[44,-43],[45,-47],[45,-44,43],[46,1],[47,46],[47,145,-763],[48,1],[49,48],[49,145,-747],[50,-48,-46,-41,-39,-37,-36,-34,-33,-31,-29,-28,-26,-15,-13,-10,-7,-5,-2,-1],[51,-50],[53,-726],[53,-666],[53,-631],[53,-595],[53,-573],[53,-559],[53,-545],[53,-501],[53,-488],[53,-479],[53,-463],[53,-452],[53,-442],[53,-360],[53,-314],[53,-279],[53,-213],[53,-212],[53,-206],[53,-177],[53,-176],[53,-171],[53,-52],[54,-727],[54,-726],[54,-710],[54,-691],[54,-686],[54,-666],[54,-659],[54,-653],[54,-631],[54,-595],[54,-594],[54,-574],[54,-573],[54,-560],[54,-559],[54,-546],[54,-545],[54,-525],[54,-502],[54,-501],[54,-489],[54,-488],[54,-480],[54,-479],[54,-464],[54,-463],[54,-455],[54,-452],[54,-445],[54,-442],[54,-397],[54,-396],[54,-385],[54,-360],[54,-357],[54,-356],[54,-341],[54,-314],[54,-280],[54,-279],[54,-238],[54,-231],[54,-230],[54,-228],[54,-213],[54,-212],[54,-206],[54,-201],[54,-194],[54,-193],[54,-191],[54,-177],[54,-176],[54,-171],[54,-52],[55,-710],[55,-595],[55,-594],[55,-525],[55,-52],[57,-729],[57,-728],[57,-712],[57,-711],[57,-688],[57,-687],[57,-671],[57,-655],[57,-654],[57,-638],[57,-576],[57,-575],[57,-562],[57,-561],[57,-548],[57,-531],[57,-529],[57,-528],[57,-526],[57,-504],[57,-503],[57,-466],[57,-465],[57,-457],[57,-456],[57,-453],[57,-447],[57,-446],[57,-443],[57,-411],[57,-391],[57,-389],[57,-388],[57,-365],[57,-350],[57,-346],[57,-345],[57,-321],[57,-236],[57,-215],[57,-199],[57,-179],[57,-56],[58,-25,-57],[59,-61,64,63],[59,19,-24,58],[59,19,-18,486],[59,64,-16,166],[59,73,72,-71],[60,-63,-97],[60,-59],[61,-471],[61,-374],[61,-372],[61,-348],[61,-344],[61,-330],[61,-328],[61,-225],[61,-222],[61,-189],[61,-186],[61,-168],[61,-136],[61,-106],[61,-63],[61,-59],[62,25,-57],[63,-220,-235],[63,-184,-198],[63,-164,492],[63,59,19,-18,349],[63,166,-758],[65,-712],[65,-711],[65,-531],[65,-529],[65,-528],[65,-526],[65,-411],[65,-106],[65,-56],[67,-740],[67,-732],[67,-692],[67,-660],[67,-585],[67,-580],[67,-565],[67,-534],[67,-510],[67,-507],[67,-499],[67,-470],[67,-394],[67,-370],[67,-354],[67,-326],[67,-66],[68,-740],[68,-732],[68,-692],[68,-660],[68,-585],[68,-580],[68,-565],[68,-510],[68,-507],[68,-499],[68,-470],[68,-348],[68,-327,-67,63,354],[68,-103],[68,59,-61,64,344],[69,-740],[69,-732],[69,-695],[69,-692],[69,-663],[69,-660],[69,-588],[69,-580],[69,-566],[69,-565],[69,-508],[69,-507],[69,-497],[69,-470],[69,-421],[69,-413,-393,-148,505],[69,-413,-352,-315,-155,-153,467],[69,-413,-352,-155,563],[69,-413,-227,165,-221,-74,-155,63,-153,448],[69,-413,-185,165,-74,-148,63,458],[69,-413,165,-221,-74,-155,63,577],[69,-146],[69,-93],[69,63,-68],[69,112,-111],[70,-68,-67],[74,-577],[74,-549],[74,-458],[74,-448],[74,-392],[74,-351],[74,-220],[74,-184],[74,-104],[74,-103],[74,-70],[74,749],[74,756],[75,63,-74],[76,-89,19,-88,87],[76,19,-32,123],[76,19,-30,120],[76,19,-14,130],[76,19,-11,134],[76,71,-89,19,-88,433],[76,71,19,-30,434],[76,89,59,-61,-169,64,168],[76,89,92,19,-12,91,-8,90],[76,89,92,19,91,-9,167],[76,126,-128,19,-14,429],[76,128,-126,19,-14,428],[78,-86],[78,-81],[78,-63,-127],[79,-86],[79,-77],[79,-63,-125],[80,-86],[80,-81],[80,-77],[80,-63,-129],[82,-63,-122],[84,-83],[84,-63,-133],[85,-136],[85,-84,83],[85,-80,-79,-78,86],[86,83,82,81,77,-76],[86,83,82,81,77,22,21,20,-600],[86,83,82,81,77,143,22,21,20,-426],[87,63,-117],[87,76,19,-40,102],[87,76,71,19,-69,-8,421],[87,76,71,19,-40,420],[87,76,71,19,-8,422],[88,-433],[88,-87],[89,-433],[89,-161,-160],[89,-87],[90,-155,63,226],[90,-148,63,190],[90,63,112],[90,87,76,19,-8,75],[90,146,63,-145],[91,9,16,-164],[92,-170],[95,94,93,40,-92],[96,-101,71,475],[96,-74,71,70],[96,118,116,-115],[97,-96],[98,-247,-246],[98,63,-416],[98,63,-97],[99,-96],[101,-571],[101,-543],[101,-541],[101,-475],[101,-100],[101,748],[101,755],[102,63,-101],[103,100,-758,-757],[103,100,-99],[104,68,-67],[105,-740],[105,-585],[105,-580],[105,-534],[105,-66],[107,106,-105],[108,-740],[108,-713],[108,-588],[108,-580],[108,-532],[108,-412],[108,-254],[108,-107],[110,-734],[110,-696],[110,-664],[110,-592],[110,-377],[110,-333],[110,-109],[111,-377,-509],[111,-333,-498],[111,-251],[111,-205,-162,112,353],[111,-109,-584],[112,-145,-155,335],[112,-145,-148,379],[113,-735],[113,-587],[113,-535],[113,-523],[113,-424,-451,-441,-590,-256,90,63,589],[113,-424,440,-500,-462,-256,-145,739],[113,-424,440,-500,-462,259,-407,-256,-258,312,-145,579],[113,-151],[113,-145,-259],[113,-112,-111],[114,-111,-110],[117,-116],[117,755],[117,756],[119,-118],[119,748],[119,749],[120,63,-119],[121,-271,71,270],[123,63,-122],[125,-139],[125,-124],[126,-431],[126,-428],[126,-277,-276],[126,63,-125],[127,-139],[127,-131],[128,-431],[128,-429],[128,63,-127],[128,112,-284],[129,-139],[129,-131],[129,-124],[130,63,-129],[133,-132],[134,63,-133],[135,-133,132],[135,-129,-127,-125,139],[137,136,-135],[138,-296],[138,-137],[138,76,-128,-126,19,-14,431],[138,76,19,-11,430],[139,132,131,124,122,-121],[139,132,131,124,122,267,86,83,59,82,73,72,81,77,22,21,20,-266],[140,-252],[140,-251],[140,-114],[140,750],[141,-112,-140],[142,-524],[142,-523],[142,-437],[142,-425],[142,-152],[142,-151],[142,-145,-262],[142,-141],[143,-145,-267],[144,-617],[144,-304],[144,-145,-264],[145,-739],[145,-735],[145,-591],[145,-583],[145,-579],[145,-564],[145,-550],[145,-536],[145,-535],[145,-519],[145,-518],[145,-516],[145,-506],[145,-469],[145,-468],[145,-461],[145,-410],[145,-401],[145,-395],[145,-380],[145,-379],[145,-373],[145,-372],[145,-367],[145,-362],[145,-358],[145,-355],[145,-336],[145,-335],[145,-329],[145,-328],[145,-323],[145,-318],[145,-312],[145,76,19,-154,144,143,159],[145,76,19,-144,143,304],[145,76,19,-6,144,143,275],[145,76,19,144,-38,143,272],[145,76,19,144,-3,143,289],[145,76,19,144,143,-142,141],[147,-146],[148,-508],[148,-507],[148,-505],[148,-458],[148,-454],[148,-379],[148,-373],[148,-190],[149,148,-147],[150,-149],[153,-497],[153,-470],[153,-468],[153,-467],[153,-466],[153,-465],[153,-464],[153,-463],[153,-449],[153,-448],[153,-447],[153,-446],[153,-445],[153,-442],[153,-152],[153,-145,-315],[153,-112,-227],[153,227,90,63,450],[153,315,-145,469],[154,-719],[154,-522],[154,-438],[154,-159],[154,-145,-309],[154,6,152,151,-150],[155,-577],[155,-566],[155,-565],[155,-563],[155,-497],[155,-470],[155,-467],[155,-448],[155,-444],[155,-335],[155,-329],[155,-226],[155,-149],[156,-158,121,115,71,250],[156,-140,121,115,71,252],[157,-301],[157,-156],[158,-721],[158,-555],[158,-539],[158,-250],[158,140,-157],[158,744],[159,-112,-158],[160,-301],[160,-156],[162,-723],[162,-695],[162,-663],[162,-588],[162,-585],[162,-566],[162,-555],[162,-510],[162,-508],[162,-499],[162,-497],[162,-493],[162,-472],[162,-353],[162,-296],[162,-294],[162,-291],[162,-277],[162,-247],[162,-161],[164,-492],[164,-483],[164,-242],[164,-210,-24,234],[164,-210,63,-24,490],[164,-163],[164,209,-208,-54,-53,212],[164,209,-208,63,-54,-53,488],[164,209,53,-208,-54,230],[164,209,53,-208,63,-54,489],[164,209,238,63,491],[164,209,238,240],[165,-483],[165,-242],[165,-163],[167,90,-754],[168,167,90,63,166,-165],[169,-168],[170,91,-169],[172,-201],[172,-193],[172,-191],[172,-176],[172,-171],[173,-172,164,-54,-53,176],[173,-172,164,53,-54,193],[173,201,164,203],[174,-197],[174,-195],[174,-186],[174,-181],[174,-173],[175,-452],[175,-360],[175,-171],[176,-165,-175],[177,165,-175],[178,-502],[178,-501],[178,-455],[178,-452],[178,-396],[178,-362],[178,-194],[178,-177],[180,-457],[180,-389],[180,-199],[180,-179],[182,181,-180],[183,-504],[183,-503],[183,-457],[183,-456],[183,-453],[183,-372],[183,-367],[183,-189],[183,-182],[184,179,-178,53,90,63,-54,194],[184,179,-178,90,63,-54,-53,177],[184,179,112,204],[185,-458],[185,-392],[185,-184],[188,-187],[190,189,187,186,-185],[192,-455],[192,-385],[192,-191],[193,-165,-192],[194,165,-192],[196,-456],[196,-386],[196,-195],[197,-165,-196],[198,165,-196],[199,184,-198],[200,195,191,171,163,-162],[202,-200],[203,-165,-202],[204,165,-202],[205,-723],[205,-695],[205,-663],[205,-588],[205,-585],[205,-566],[205,-555],[205,-510],[205,-508],[205,-499],[205,-497],[205,-493],[205,-472],[205,-353],[205,-247],[205,-161],[207,-242],[207,-237],[207,-232],[207,-228],[207,-206],[207,112,-227],[208,-489],[208,-488],[208,-480],[208,-479],[208,-280],[208,-279],[208,-238],[208,-230],[208,-228],[208,-212],[208,-206],[210,-490],[210,-481],[210,-281],[210,-234],[210,-232],[210,-222],[210,-217],[210,-209],[211,-573],[211,-545],[211,-479],[211,-442],[211,-314],[211,-279],[211,-206],[212,-165,-211],[213,165,-211],[214,-574],[214,-573],[214,-560],[214,-559],[214,-464],[214,-463],[214,-445],[214,-442],[214,-356],[214,-318],[214,-231],[214,-213],[216,-576],[216,-548],[216,-447],[216,-346],[216,-236],[216,-215],[218,217,-216],[219,-576],[219,-575],[219,-562],[219,-561],[219,-466],[219,-465],[219,-447],[219,-446],[219,-443],[219,-328],[219,-323],[219,-225],[219,-218],[220,215,-214,53,90,63,-54,231],[220,215,-214,90,63,-54,-53,213],[220,215,112,241],[221,-577],[221,-549],[221,-448],[221,-351],[221,-220],[224,-223],[226,225,223,222,-221],[227,-449],[227,-448],[227,-447],[227,-446],[227,-445],[227,-442],[227,-355],[227,-351],[227,-346],[227,-342],[227,-341],[227,-314],[227,-242],[227,-237],[227,-232],[227,-228],[227,-206],[227,207,112,243],[229,-574],[229,-546],[229,-480],[229,-445],[229,-341],[229,-280],[229,-228],[230,-165,-229],[231,165,-229],[233,-575],[233,-547],[233,-481],[233,-446],[233,-342],[233,-281],[233,-232],[234,-165,-233],[235,165,-233],[236,220,-235],[239,-482],[239,-282],[239,-237],[240,-165,-239],[241,165,-239],[243,242,237,232,228,206,-205],[244,-440,-439],[244,-312,-311],[244,161,-160],[245,156,-158,121,115,71,539],[245,156,-140,121,115,71,114],[245,302,301,-300],[246,-245],[248,-514,-513],[248,-401,-400],[248,-161,-417],[248,247,-246],[249,-245],[251,250,-249],[252,111,-110],[253,-592],[253,-109],[255,254,-253],[256,-742],[256,-739],[256,-735],[256,-589],[256,-579],[256,-535],[256,-423],[256,-410],[256,-255],[258,-736],[258,-714],[258,-579],[258,-535],[258,-257],[259,-714],[259,-583],[259,-535],[259,-405],[259,-359,-313,90,-145,63,591],[260,-599,-598],[260,145,-259],[261,-259,-258],[262,-406],[262,-405],[262,-307],[262,-261],[263,-599,-622],[263,145,-262],[265,-599,-620],[265,145,-264],[268,145,-267],[269,115,266,264,-262,307],[271,-270],[271,751],[272,-112,-271],[274,-299],[274,-286],[274,-273],[274,759],[275,-112,-274],[276,-299],[276,-284,-274,121,71,286],[276,-273],[278,-723],[278,-695],[278,-663],[278,-588],[278,-566],[278,-555],[278,-508],[278,-497],[278,-493],[278,-277],[282,281,280,279,163,-278],[283,-606,-605],[283,277,-276],[284,-299],[284,-286],[284,-276,-274,121,71,273],[285,-615],[285,-608],[285,-112,-284],[288,-287],[288,760],[289,-112,-288],[290,-288,121,71,287],[290,-284,-276,-274,121,71,299],[292,-291],[295,-614],[295,-293],[297,296,293,291,-290],[298,-297],[299,287,286,273,270,-269],[303,-302],[303,744],[303,750],[303,753],[304,-112,-303],[305,-309,300,269,115,266,264,404],[305,300,269,115,266,264,-262,-259,405],[305,300,269,115,266,264,-262,406],[306,-305],[308,307,-306],[309,-404],[309,-308],[310,-599,-626],[310,145,-309],[311,-305],[313,-591],[313,-583],[313,-536],[313,-519],[313,-401],[313,-312],[315,-664],[315,-661],[315,-660],[315,-658],[315,-656],[315,-655],[315,-654],[315,-653],[315,-631],[315,-497],[315,-470],[315,-468],[315,-467],[315,-466],[315,-465],[315,-464],[315,-463],[315,-355],[315,-351],[315,-346],[315,-342],[315,-341],[315,-314],[315,227,90,-145,63,358],[316,-599,-632],[316,145,-315],[317,-727],[317,-726],[317,-653],[317,-631],[317,-560],[317,-559],[317,-546],[317,-545],[317,-464],[317,-463],[317,-357],[317,-341],[317,-314],[319,318,-317],[320,-635],[320,-319],[322,-350],[322,-345],[322,-321],[324,323,-322],[325,-640],[325,-330],[325,-324],[327,-732],[327,-660],[327,-565],[327,-499],[327,-470],[327,-354],[327,-326],[331,330,329,328,-327],[332,-645],[332,-338],[332,-331],[333,-347,-315,-227,165,220,-216,63,-57,-25,346],[333,-347,165,220,-216,63,-57,-25,548],[333,-343,-315,-227,-233,342],[333,-343,-233,547],[333,326,321,-317,-315,-227,-229,53,-54,341],[333,326,321,-317,-315,-227,-211,-54,-53,314],[333,326,321,-317,-229,53,-54,546],[333,326,321,-317,-211,-54,-53,545],[333,326,321,357,-315,-227,165,220,215,356,90,-145,63,355],[333,326,321,357,165,220,215,356,90,-145,63,550],[334,-734],[334,-664],[334,-333],[337,-336],[339,338,336,335,-334],[340,-650],[340,-339],[343,-728],[343,-654],[343,-561],[343,-547],[343,-465],[343,-342],[344,-370,-387],[344,-326,-343],[344,-66,-527],[345,326,-343],[347,-729],[347,-655],[347,-562],[347,-548],[347,-466],[347,-346],[348,-370,-390],[348,-326,-347],[348,-66,-530],[349,-68,59,-61,64,348],[349,59,-61,64,471],[349,475,-477],[350,326,-347],[352,-730],[352,-656],[352,-563],[352,-549],[352,-467],[352,-351],[353,-377,-393],[353,-333,-352],[353,-109,-533],[354,333,-352],[358,355,351,346,342,341,314,-313],[359,-591],[359,-583],[359,-536],[359,-519],[359,-401],[359,-312],[361,-686],[361,-666],[361,-502],[361,-501],[361,-397],[361,-385],[361,-360],[363,362,-361],[364,-668],[364,-363],[366,-391],[366,-388],[366,-365],[368,367,-366],[369,-673],[369,-374],[369,-368],[371,-692],[371,-510],[371,-507],[371,-394],[371,-370],[375,374,373,372,-371],[376,-678],[376,-382],[376,-375],[377,-390,184,-180,165,63,-57,-25,389],[377,-387,-196,386],[377,370,365,-361,-192,53,-54,385],[377,370,365,-361,-175,-54,-53,360],[377,370,365,397,184,179,396,165,90,-145,63,395],[378,-696],[378,-377],[381,-380],[383,382,380,379,-378],[384,-683],[384,-383],[387,-687],[387,-503],[387,-386],[388,370,-387],[390,-688],[390,-504],[390,-389],[391,370,-390],[393,-689],[393,-505],[393,-392],[394,377,-393],[395,392,389,386,385,360,-359],[398,-629,-628],[398,-461,-460],[398,312,-311],[399,305,300,269,115,266,264,-262,261],[400,-399],[402,-700,-699],[402,-516,-515],[402,401,-400],[403,-399],[405,404,-403],[406,259,-258],[407,-736],[407,-714],[407,-579],[407,-535],[407,-257],[409,-707],[409,-408],[410,408,-407],[413,-740],[413,-732],[413,-730],[413,-713],[413,-695],[413,-692],[413,-689],[413,-676],[413,-663],[413,-660],[413,-656],[413,-643],[413,-588],[413,-580],[413,-577],[413,-566],[413,-565],[413,-563],[413,-532],[413,-508],[413,-507],[413,-505],[413,-497],[413,-470],[413,-467],[413,-458],[413,-454],[413,-448],[413,-444],[413,-412],[414,-69,-413],[415,87,76,71,19,-40,553],[415,87,76,71,19,-8,414],[415,434,433,-432],[416,-415],[417,-63,-416],[418,161,-417],[419,-415],[421,420,-419],[422,69,-413],[423,69,-413,257,-533,-108,532],[423,412,257,109,-530,-65,-57,-25,529],[423,412,257,109,-527,-65,25,-57,526],[423,412,411,257,109,66,56,-55,-54,-53,52],[423,412,411,257,109,66,56,-55,53,-54,525],[423,412,411,257,109,66,56,594,593],[423,493,-487,-484,-413,257,109,-105,-108,472,471,-67,-68,63,-69,580],[424,-742],[424,-739],[424,-735],[424,-734],[424,-696],[424,-681],[424,-664],[424,-648],[424,-589],[424,-579],[424,-535],[424,-423],[425,-113,-424],[427,426,71,-154,144,438],[427,426,71,144,-142,437],[431,430,429,428,123,-427],[431,430,429,428,123,59,73,72,-601],[432,427,426,71,-144,617],[432,427,426,71,144,-38,603],[435,432,427,426,71,-154,144,522],[435,432,427,426,71,144,-142,-113,523],[435,432,427,426,71,144,-142,524],[436,-435],[438,437,-436],[439,-435],[440,-500,-462,312,-145,518],[441,-742],[441,-734],[441,-696],[441,-664],[441,-589],[441,-587],[441,-567],[441,-519],[441,-514],[441,-440],[444,-233,25,-219,-57,575],[444,-227,-233,25,-219,-57,-153,446],[444,-227,165,220,-216,-219,63,-57,-25,-153,447],[444,165,220,-216,-219,63,-57,-25,576],[444,333,-347,-315,-219,-57,-25,-153,466],[444,333,-347,-219,-57,-25,562],[444,333,-343,-315,25,-219,-57,-153,465],[444,333,-343,25,-219,-57,561],[444,443,-229,-214,53,-54,574],[444,443,-227,-229,-214,53,-54,-153,445],[444,443,-227,-211,-214,-54,-153,-53,442],[444,443,-227,165,220,215,356,90,63,-153,449],[444,443,-211,-214,-54,-53,573],[444,443,165,220,215,356,90,63,578],[444,443,333,326,321,-317,-315,-214,-54,-153,-53,463],[444,443,333,326,321,-317,-315,-214,53,-54,-153,464],[444,443,333,326,321,-317,-214,-54,-53,559],[444,443,333,326,321,-317,-214,53,-54,560],[444,443,333,326,321,357,-315,356,-145,-153,468],[444,443,333,326,321,357,356,-145,564],[450,449,448,447,446,445,442,-441],[451,-742],[451,-734],[451,-696],[451,-664],[451,-614],[451,-612],[451,-606],[451,-589],[451,-587],[451,-567],[451,-519],[451,-514],[451,-440],[454,-196,-183,25,-57,456],[454,184,-180,-183,165,63,-57,-25,457],[454,377,-390,-183,-57,-25,504],[454,377,-387,-183,25,-57,503],[454,453,-192,-178,53,-54,455],[454,453,-175,-178,-54,-53,452],[454,453,184,179,396,165,90,63,459],[454,453,377,370,365,-361,-178,-54,-53,501],[454,453,377,370,365,-361,-178,53,-54,502],[454,453,377,370,365,397,396,-145,506],[459,458,457,456,455,452,-451],[460,440,-439],[462,-739],[462,-579],[462,-518],[462,-461],[471,-475,-477],[471,96,-101,71,543],[472,-539,-542],[473,-585],[473,-510],[473,-499],[473,-472],[475,349,474],[476,474,-473],[477,-720],[477,-570],[477,-554],[477,-540],[477,-496],[477,-476],[478,-585],[478,-510],[478,-499],[478,-472],[483,482,481,480,479,-478],[484,-740],[484,-732],[484,-724],[484,-692],[484,-660],[484,-580],[484,-571],[484,-565],[484,-557],[484,-556],[484,-507],[484,-470],[485,349,-484],[486,349,485],[486,475,349,495],[487,-740],[487,-732],[487,-724],[487,-692],[487,-660],[487,-580],[487,-571],[487,-565],[487,-557],[487,-556],[487,-507],[487,-470],[492,491,490,489,488,-487],[493,-487,-484,-413,333,472,471,-327,-67,-315,-155,-68,63,-153,-69,470],[493,-487,-484,-413,333,472,471,-327,-67,-155,-68,63,-69,565],[493,-487,-484,-413,377,-371,472,471,-67,-148,-68,63,-69,507],[494,-723],[494,-695],[494,-663],[494,-588],[494,-566],[494,-555],[494,-508],[494,-497],[494,-493],[496,495,-494],[497,470,469,468,467,466,465,464,463,-462],[498,-733],[498,-661],[498,-566],[498,-497],[499,333,-498],[500,-739],[500,-579],[500,-518],[500,-461],[508,507,506,505,504,503,502,501,-500],[509,-693],[509,-508],[510,377,-509],[511,461,-460],[512,435,432,427,426,71,-154,144,719],[512,435,432,427,426,71,144,-142,425],[513,-512],[515,514,-513],[517,-735],[517,-535],[517,-516],[519,518,-517],[520,516,-515],[521,-512],[523,522,-521],[524,113,-424],[527,-711],[527,-526],[528,66,-527],[530,-712],[530,-529],[531,66,-530],[533,-713],[533,-532],[534,109,-533],[537,-583],[537,-536],[539,-477,540],[539,475,349,538],[541,540,538,-537],[542,-724],[542,-557],[542,-541],[543,539,-542],[544,-583],[544,-536],[550,549,548,547,546,545,-544],[551,-735],[551,-535],[553,-477,59,19,-18,570],[553,486,475,349,569],[553,486,539,475,349,552],[553,539,-477,59,19,-18,554],[556,-494,415,-205,-162,-278,112,87,76,71,19,-40,723],[556,-494,415,472,245,156,-205,-158,-162,-278,112,121,115,87,76,71,19,-40,555],[557,555,554,552,-551],[558,-735],[558,-535],[566,565,564,563,562,561,560,559,-558],[567,-719,-722],[567,-558,-551,-424,-517,-256,-145,-113,735],[567,-558,-551,-424,-517,536,-407,-256,-258,-259,-145,-113,535],[568,-587],[568,-567],[571,570,569,-568],[572,-606],[572,-587],[572,-567],[578,577,576,575,574,573,-572],[582,-741],[582,-581],[583,-257,-582],[584,257,-582],[585,109,-584],[586,-741],[586,-581],[587,-681,-694],[587,-648,-662],[587,-423,-586],[588,423,-586],[590,-742],[590,-589],[591,-257,-590],[592,257,-590],[596,-586,-582,741],[596,113,-424,-451,-441,-590,-256,90,63,742],[596,423,69,-413,257,-533,-108,713],[596,423,412,257,109,-530,-65,-57,-25,712],[596,423,412,257,109,-527,-65,25,-57,711],[596,423,412,411,257,109,66,56,-55,-54,-53,595],[596,423,412,411,257,109,66,56,-55,53,-54,710],[596,423,412,411,257,109,66,56,594,743],[596,423,493,-487,-484,-413,257,109,-105,-108,472,471,-67,-68,63,-69,740],[597,-596],[598,-716],[598,-704],[598,-665,-630,616,602,601,600,432,145,738],[605,-615],[605,-604],[605,432,427,426,71,-285,-6,144,608],[607,606,-605],[610,-605,432,427,426,71,-285,-6,144,615],[610,432,427,426,71,144,-3,609],[613,-611],[614,611,-610],[615,609,608,604,603,-602],[616,602,601,600,432,-409,707],[616,602,601,600,432,-384,683],[616,602,601,600,432,-376,678],[616,602,601,600,432,-369,673],[616,602,601,600,432,-364,668],[616,602,601,600,432,-340,650],[616,602,601,600,432,-332,645],[616,602,601,600,432,-325,640],[616,602,601,600,432,-320,635],[616,602,601,600,432,599],[617,512,435,-616],[618,599,-598],[619,-598,-597],[621,599,-620],[622,-705],[622,-704],[622,-619],[623,599,-622],[624,-626,620,703],[624,-622,620,-598,704],[624,-622,620,705],[625,-624],[626,-703],[626,622,-625],[627,599,-626],[628,-624],[630,-738],[630,-716],[630,-700],[630,-629],[632,-664],[632,-661],[632,-660],[632,-658],[632,-656],[632,-655],[632,-654],[632,-653],[632,-631],[632,616,602,601,600,432,315,145,657],[633,599,-632],[634,-727],[634,-726],[634,-659],[634,-653],[634,-631],[636,635,-634],[637,-636],[639,-729],[639,-728],[639,-655],[639,-654],[639,-638],[641,640,-639],[642,-641],[644,-732],[644,-730],[644,-663],[644,-660],[644,-656],[644,-643],[646,645,-644],[647,-646],[648,-644,-632,69,-413,-352,-315,656],[648,-644,-632,493,-487,-484,-413,333,472,471,-327,-67,-315,-68,63,-69,660],[648,-644,69,-413,-352,730],[648,-644,493,-487,-484,-413,333,472,471,-327,-67,-68,63,-69,732],[648,643,-639,-632,333,-347,-315,-57,-25,655],[648,643,-639,-632,333,-343,-315,25,-57,654],[648,643,-639,333,-347,-57,-25,729],[648,643,-639,333,-343,25,-57,728],[648,643,638,-634,-632,333,326,321,-317,-315,-54,-53,631],[648,643,638,-634,-632,333,326,321,-317,-315,53,-54,653],[648,643,638,-634,333,326,321,-317,-54,-53,726],[648,643,638,-634,333,326,321,-317,53,-54,727],[648,643,638,659,-632,616,602,601,600,432,333,326,321,357,-315,145,658],[648,643,638,659,616,602,601,600,432,333,326,321,357,145,731],[649,-734],[649,-664],[649,-648],[651,650,-649],[652,-651],[662,-733],[662,-661],[663,648,-662],[664,661,660,658,657,656,655,654,653,631,-630],[665,-738],[665,-716],[665,-700],[665,-629],[667,-691],[667,-686],[667,-666],[669,668,-667],[670,-669],[672,-688],[672,-687],[672,-671],[674,673,-672],[675,-674],[677,-695],[677,-692],[677,-689],[677,-676],[679,678,-677],[680,-679],[681,-677,69,-413,-393,689],[681,-677,493,-487,-484,-413,377,-371,472,471,-67,-68,63,-69,692],[681,676,-672,377,-390,-57,-25,688],[681,676,-672,377,-387,25,-57,687],[681,676,671,-667,377,370,365,-361,-54,-53,666],[681,676,671,-667,377,370,365,-361,53,-54,686],[681,676,671,691,616,602,601,600,432,377,370,365,397,145,690],[682,-696],[682,-681],[684,683,-682],[685,-684],[694,-693],[695,681,-694],[696,693,692,690,689,688,687,686,666,-665],[697,629,-628],[698,624,-622,620,619],[699,-698],[701,700,-699],[702,-698],[704,703,-702],[705,598,-597],[706,-596],[708,707,-706],[709,-708],[715,-714],[716,-596,-715],[717,-716],[719,-487,-484,415,-542,87,76,71,63,19,-40,724],[719,553,486,539,475,349,718],[719,553,539,-477,59,19,-18,720],[722,-721],[723,719,-722],[724,721,720,718,-717],[725,-716],[734,733,732,731,730,729,728,727,726,-725],[735,596,-715],[737,-736],[738,-596,-737],[739,596,-737],[743,742,741,740,736,714,713,712,711,710,595,593,589,581,580,579,535,532,529,526,525,52,-51],[744,-50],[745,-50],[746,745],[746,762],[746,764],[747,745],[748,-50],[749,-50],[750,-50],[751,-50],[752,751],[752,759],[752,760],[753,-50],[754,753],[754,761],[755,-50],[756,-50],[757,-50],[758,757],[759,-50],[760,-50],[761,-50],[762,-50],[763,762],[764,-50],[765,764]]}