2023: d24: ex2: add solution

2023/d24/ex1/ex1.py

@@ -0,0 +1,78 @@
+#!/usr/bin/env python
+
+import itertools
+import sys
+from decimal import Decimal
+from typing import NamedTuple
+
+
+class Point(NamedTuple):
+    x: int
+    y: int
+    z: int
+
+
+class HailStone(NamedTuple):
+    pos: Point
+    vel: Point
+
+
+def solve(input: list[str]) -> int:
+    def parse_line(line: str) -> HailStone:
+        pos, vel = line.split(" @ ")
+        return HailStone(
+            Point(*map(int, pos.split(", "))), Point(*map(int, vel.split(", ")))
+        )
+
+    def parse(input: list[str]) -> list[HailStone]:
+        return [parse_line(line) for line in input]
+
+    def intersections(hailstones: list[HailStone], boundaries: tuple[int, int]) -> int:
+        def intersects(a: HailStone, b: HailStone) -> bool:
+            # According to wikipedia, if:
+            # x = a_px + t * a_vx = b_px + u * b_vx
+            # y = a_py + t * a_vy = b_py + u * b_vy
+            # then:
+            # t = ((a_px-b_px)*(-b_vy) - (a_py-b_py)*(-b_vx)) / ((-a_vx)*(-b_vy) - (-a_vy)*(-b_vx))
+            # u = ((a_px-b_px)*(-a_vy) - (a_py-b_py)*(-a_vx)) / ((-a_vx)*(-b_vy) - (-a_vy)*(-b_vx))
+            (a_px, a_py, _), (a_vx, a_vy, _) = a
+            (b_px, b_py, _), (b_vx, b_vy, _) = b
+
+            # Use rationals for extra precision, just in case
+            denom = Decimal(a_vx * b_vy - a_vy * b_vx)
+
+            # Parallel lines
+            if denom == 0:
+                return False
+
+            t = ((a_px - b_px) * (-b_vy) - (a_py - b_py) * (-b_vx)) / denom
+            u = ((a_px - b_px) * (-a_vy) - (a_py - b_py) * (-a_vx)) / denom
+
+            # Intersects in the past
+            if t < 0 or u < 0:
+                return False
+
+            x = a_px + t * a_vx
+            y = a_py + t * a_vy
+
+            # Outside our observation area
+            if not boundaries[0] <= x <= boundaries[1]:
+                return False
+            if not boundaries[0] <= y <= boundaries[1]:
+                return False
+
+            return True
+
+        return sum(intersects(a, b) for a, b in itertools.combinations(hailstones, 2))
+
+    hailstones = parse(input)
+    return intersections(hailstones, (200000000000000, 400000000000000))
+
+
+def main() -> None:
+    input = sys.stdin.read().splitlines()
+    print(solve(input))
+
+
+if __name__ == "__main__":
+    main()

2023/d24/ex1/input

@@ -0,0 +1,300 @@
+260346828765750, 357833641339849, 229809969824403 @ 64, -114, 106
+340220726383465, 393110064924024, 226146987100003 @ -79, -61, 158
+11361697274707, 101596061919750, 46099495948720 @ 328, 162, 333
+360204609690721, 527678808395772, 271703202326380 @ -132, -458, 20
+228800225183261, 405333190838676, 284309641117406 @ 29, -233, 35
+347686754070960, 372761595433127, 227908656106580 @ -134, 452, 245
+420404387574505, 320613771806244, 282039825133426 @ -209, -99, 24
+239697674964055, 219683531868878, 291640535034286 @ 36, 12, 18
+270083622615715, 298192739573649, 450720525831403 @ 71, 50, -394
+210388952361528, 202933503071430, 369359171934512 @ 62, 13, -71
+323626194439723, 331061672127276, 297678575959794 @ -45, 7, -61
+304808549150934, 383205509992906, 523319353604760 @ -22, -163, -463
+187934586489225, 219381841648824, 260929087075428 @ 73, -29, 61
+334112509601119, 400144558186712, 244055841518098 @ 18, 155, 66
+246253930315613, 304696957680568, 94020244355048 @ 53, -63, 311
+342955905222035, 388277972401036, 257476145906070 @ -94, -111, 34
+327736098163477, 330547943777790, 153376586381074 @ -71, -90, 230
+261048582174545, 197767231455944, 278362708671168 @ -10, -13, 43
+262232829717925, 400052820669654, 363505406595748 @ 25, -212, -101
+324188029882468, 362855685632781, 234741485808022 @ 110, 502, 163
+205507378373754, 312370561869725, 214016656029865 @ 148, -46, 132
+239592601431541, 142078397267946, 285236791773286 @ 17, 58, 34
+144373393337221, 188196109756908, 173981678832424 @ 99, -22, 149
+288873332238259, 312782225890490, 274590086150334 @ 18, -6, 14
+186182198786950, 402152186162636, 135534511498564 @ 96, -225, 213
+231239063521245, 186020667465684, 343869538475528 @ 13, -20, -19
+250272260456639, 161173847651144, 288550442540870 @ 10, 51, 28
+296318163416530, 282047552083869, 393397156658776 @ 116, 426, -591
+324596493713872, 398326967096844, 254282763206956 @ 32, -9, 5
+215625978065245, 203168177356104, 420679288194328 @ 35, -25, -104
+191086370171245, 60115319750904, 146260480280128 @ 243, 573, 296
+322860700705485, 459545877374104, 448537560287088 @ -59, -309, -299
+314822321873915, 398359415059524, 264470104210778 @ 140, 49, -94
+269210714892168, 256327147227716, 398338379562592 @ 52, 95, -231
+302666483817653, 275410751736752, 326439099654152 @ -40, -40, -37
+270142822739620, 344779311267669, 324492644181298 @ 52, -80, -85
+374865332232522, 402789242720040, 323870419231066 @ -182, -173, -141
+243208589268314, 367086212824621, 199057002427101 @ 140, -102, 184
+250464382830742, 135024447362895, 320243825003503 @ -8, 24, 6
+355922778067984, 378321615748686, 241250226323332 @ -130, -107, 85
+316218511102785, 354948779738048, 394814158202160 @ 86, 273, -913
+321455854706509, 396440824238416, 314920648255344 @ 9, -75, -257
+169378410757153, 225633601154640, 335902593841960 @ 104, -23, -27
+310941798903565, 333771112844784, 286883552058694 @ 101, 351, -182
+411974191700116, 414045748557315, 447602203181716 @ -232, -222, -323
+282375423819373, 240799415094852, 287697942997588 @ -23, -28, 26
+424528361387804, 462909748733920, 382166946506320 @ -278, -325, -231
+163339958801001, 272115353229508, 302748903558972 @ 230, 32, -28
+258865845218325, 331436090977439, 237682017090608 @ 37, -100, 89
+302915997518781, 347231423515616, 296218913365336 @ -43, -147, 9
+201550834032262, 308185564073751, 181635624713110 @ 224, 24, 219
+326879140563285, 302444228750105, 363158049251869 @ -59, 38, -192
+199437546908251, 165065778022384, 281783000883451 @ 135, 171, 18
+275634964575007, 320652660558480, 161650608601594 @ 82, 39, 294
+299888387753175, 162477657523014, 431376299337848 @ -46, 58, -143
+392193811586581, 352294886790018, 355391098486984 @ -187, -111, -127
+368009114122653, 158595116827656, 240204738709240 @ -127, 64, 84
+235057921833792, 208902653782308, 369261469240150 @ 10, -41, -45
+333864628161721, 403967975589003, 236655090656734 @ 17, 100, 147
+315707153676205, 346742558497233, 239838980741152 @ -19, -16, 89
+265733060020157, 382781265854024, 325370365767928 @ 44, -169, -69
+244493835144625, 206378827546980, 278922806636032 @ 216, 460, -33
+336468228693530, 357997678992397, 445536876104649 @ -64, 78, -800
+334116663241987, 417641320056889, 460730643073845 @ -81, -234, -296
+283712214409060, 217794347554444, 318592790485419 @ 6, 111, -50
+181035782538969, 34330093599444, 116481838981164 @ 59, 121, 203
+267636391438175, 116019071284224, 274907016053068 @ -13, 91, 45
+359932116674365, 372724315764974, 242720827369528 @ -195, 137, 81
+413732861285365, 274346810098864, 265789907811328 @ -234, 50, 36
+353859733044440, 444601519540446, 186716148862678 @ -124, -287, 231
+266823502975823, 342804454729090, 139439752620420 @ 62, -72, 295
+299232903030949, 283130841945486, 266625316859842 @ -27, -23, 43
+275731283415043, 290995753064250, 269990654468416 @ 12, -32, 37
+284336299470177, 363011315559156, 245656891783664 @ 65, -65, 73
+300184773969053, 264674528467624, 288447324797656 @ -35, -19, 15
+364327543902318, 203179466147145, 202143114372903 @ -160, 454, 206
+240582515099049, 257855786814120, 267367130583972 @ 95, 67, 35
+322071439136631, 320755095987098, 240900218113582 @ -62, -76, 84
+407030376195355, 238248420347409, 280351241837773 @ -197, 44, 22
+363480833508100, 302741435647038, 374292309644818 @ -184, 337, -509
+305986467673468, 242537468667456, 312444331887847 @ 32, 395, -156
+252027155370005, 237764087612499, 383247340881198 @ 5, -44, -77
+372582774757039, 423473229980586, 294285328077664 @ -173, -231, -55
+284005653462811, 279636127688541, 343422083098399 @ 23, 50, -122
+307762320034081, 264568258469028, 248848044023842 @ -57, -71, 74
+356296354200217, 324248100646422, 270336780779350 @ -125, -18, 20
+310365295172069, 398733724603568, 271146207120040 @ 38, -112, -33
+332525984343205, 424881352868134, 234357444969968 @ 33, -126, 173
+352583954626249, 349239276790500, 353167414266244 @ -116, -82, -152
+297714119036800, 324271023294864, 362116453319623 @ -10, -53, -146
+285957271760765, 299826994507224, 268344479706678 @ 13, -5, 32
+243189693681529, 258702209578860, 199942339459600 @ 190, 242, 203
+326701397847709, 290194546332360, 296193493706296 @ -43, 195, -87
+292362934918391, 337984495256987, 353443507882303 @ 7, -66, -144
+329560214366727, 287131872509690, 283601935331544 @ -58, 144, -31
+419657717017333, 394749569068172, 492465483328742 @ -207, -207, -278
+424741311206371, 418004503651488, 366948667795378 @ -212, -241, -94
+289511348263829, 369752819333130, 313407769490726 @ 73, -56, -140
+317864241152929, 333597843545268, 280181752022452 @ -20, 40, -30
+159013055331421, 197040084742216, 154846454650744 @ 129, 27, 189
+310161956929405, 317608137512664, 286534497733492 @ -19, 11, -21
+328398331752021, 408235207737374, 277347063815996 @ 37, -19, -211
+352713775673581, 329046721759478, 139004188330392 @ -123, 50, 385
+303904706761629, 256397200765768, 300376317070392 @ -37, 8, -7
+273217189299031, 372821204372277, 128406796773907 @ 95, -92, 392
+152269575075685, 112586975003184, 246776862071728 @ 138, 132, 76
+316077180975508, 285040325144306, 333644269613969 @ -48, 5, -82
+291214477117667, 139137384078822, 239703215510530 @ -46, 28, 84
+282383815400461, 202954623809304, 225038200055848 @ 24, 196, 116
+168593234159600, 148914293359439, 291033865957193 @ 94, 48, 28
+398831545490785, 308451835604503, 274399283929173 @ -159, -126, 46
+240709939960879, 308439888753675, 278202135723646 @ 59, -72, 27
+279404244431973, 251750459409020, 95468761809964 @ 35, 114, 384
+420662877939440, 344775968361866, 525951427053175 @ -274, -55, -570
+327071630965000, 395761942422854, 262797011894253 @ 114, 245, -164
+334223852961341, 422841882209224, 241141724398936 @ 38, -69, 102
+331008090348665, 334101214652224, 233563791181228 @ -68, -31, 102
+365681210920495, 502432633101754, 311612110753818 @ -138, -388, -46
+349308710499373, 385266962186136, 265604633087480 @ -150, 292, -163
+302146562278813, 327132561288801, 243383000145796 @ 157, 400, 77
+253538164543510, 405218794636794, 381768323339290 @ 96, -199, -217
+235161774756385, 227712177337092, 326407943699224 @ 16, -48, -7
+236032878960545, 237730556620694, 427906712868538 @ 17, -55, -117
+329543688711978, 407035805550239, 145778919294318 @ -82, -234, 191
+179368688878425, 325143400816138, 366229488873984 @ 131, -112, -91
+371231992850378, 316638751988811, 236103319042700 @ -212, 244, 109
+339808454446741, 351596138940235, 279082311533963 @ -75, 170, -104
+351596216557693, 415490735560152, 387962665814524 @ -123, -193, -412
+278688411144475, 219677637474000, 280342089549808 @ -29, -37, 41
+227585847055153, 347006074356246, 373749729539980 @ 67, -140, -105
+312933684342933, 200941440991884, 335002534040332 @ -61, 16, -30
+280319712864331, 341572097476173, 270405943273150 @ 119, 58, -13
+334263217258791, 436302126934828, 368237906560810 @ -86, -267, -78
+258254831954108, 147783583066962, 333731768562520 @ -8, 37, -15
+355801879637895, 341787614777264, 302534030878548 @ -122, -73, -41
+131266234587925, 22532917085508, 198037908529672 @ 111, 140, 125
+341625668908842, 329754211784895, 301962684556755 @ -92, -8, -62
+105063826836925, 158508866142744, 351476391746242 @ 141, 11, -28
+412949842167537, 462762493467832, 334895606045844 @ -220, -313, -82
+329069085317565, 377407266331234, 426073969564998 @ -19, 44, -868
+217418593657566, 204726057801614, 242720827369528 @ 70, 41, 81
+338084512203857, 410004688486632, 239975437178400 @ -38, -5, 107
+379384638630079, 369543475974252, 402174952375396 @ -200, -71, -381
+386154908209069, 395639474455092, 280370845418350 @ -235, -131, -42
+275382644671282, 36951187740642, 151193435620480 @ 40, 537, 265
+356619952566811, 324712560155565, 331988520420058 @ -141, 124, -229
+358547496942130, 408300560102454, 267115051708363 @ -172, -115, -46
+346306312397521, 383668766131808, 228673142584364 @ -108, 5, 152
+359754386397630, 458720322718534, 559318866468353 @ -118, -295, -314
+351347143979005, 365572803517800, 259774637417128 @ -119, -57, 31
+302183764989621, 364256687909996, 265155690823964 @ 35, -36, 10
+330924340196260, 296427648577092, 141164605133864 @ -84, -113, 193
+364641746578165, 515395099355088, 306019572461464 @ -174, -558, -155
+339224696083261, 358367099969064, 263593215134050 @ -83, -29, 18
+193992358862501, 185968153834072, 367909202669970 @ 97, 59, -82
+336367817216524, 421844251871834, 247462114434092 @ 18, -39, 13
+161312373767566, 150227310716099, 291400675391663 @ 108, 56, 26
+231266455520539, 145495597439120, 287703190551144 @ 42, 95, 25
+206550308007613, 468743856845808, 162840383607640 @ 53, -303, 169
+429512031935863, 262967063704113, 273355464244561 @ -185, -92, 50
+380308299578381, 391625299100696, 505418060665704 @ -181, -163, -521
+330850564652410, 441663420225969, 416132167014268 @ -52, -282, -515
+375615981345391, 246897309609150, 541040247329687 @ -141, -11, -322
+257612492222965, 491419444805616, 398469152274232 @ 26, -346, -143
+292985656154761, 317945193289904, 184697849249204 @ 60, 101, 260
+232877219665201, 405217862288709, 271226801912872 @ 89, -214, 33
+348259631347512, 204238531298826, 312600183336479 @ -106, 169, -50
+268746780353590, 281608151109144, 383837866458733 @ 126, 195, -338
+122524059468689, 287919639112272, 167740167865852 @ 203, -65, 183
+312459888298897, 326923346974976, 225415511869904 @ 27, 167, 149
+319608062021405, 211487145992136, 254111710998584 @ -64, 49, 65
+242932724018775, 99557446164529, 454532431171443 @ 7, 84, -140
+257306506153525, 384718831609032, 260164650130816 @ 6, -205, 60
+346820458626153, 114882415853663, 188792118714110 @ -103, 294, 175
+313007300086521, 358742568002607, 296850115847834 @ -7, -38, -77
+178290472099096, 100952248470583, 338895184944207 @ 162, 260, -70
+232626084330181, 190661053821264, 325127462135648 @ 30, 16, -14
+372111394423630, 360975162645164, 266126939035668 @ -132, -177, 53
+448046725470493, 357813853076325, 323596691049628 @ -227, -170, -19
+241095145890565, 149424858214964, 213990140128028 @ 81, 233, 131
+335893091355037, 420535970089352, 269657513849720 @ 9, -52, -256
+344781417999610, 437369362040334, 233000501863018 @ -102, -263, 195
+317912587490765, 356977339413256, 421028144913168 @ -49, -117, -254
+349219513788590, 431309506759549, 505578881772528 @ -104, -262, -199
+301801136650301, 321621066036596, 298591305543704 @ 5, 14, -55
+197415955491805, 446870993170456, 251710862420360 @ 81, -280, 70
+328275156333949, 224085796039851, 111193637396461 @ -67, 152, 340
+333989052779735, 163119706265934, 181122434623568 @ -86, 70, 157
+318880316206670, 372095178926389, 267474120557491 @ 16, 26, -30
+308122992582769, 210364537012149, 317548450311542 @ -63, -44, 7
+348091459536315, 236767606013484, 310471779320178 @ -109, 295, -109
+341518034630073, 288253587957497, 238209449374690 @ -95, -70, 87
+340212283132345, 393453588795138, 268600848335248 @ -69, 40, -99
+280974192791863, 258914295404854, 280705588435520 @ -12, -24, 29
+282538583056945, 227062101647424, 243979447408168 @ 98, 401, 77
+288833639276521, 496224937883232, 345769934484472 @ 48, -423, -191
+255548451712998, 156282887184168, 316053658342303 @ -8, 19, 6
+285854755263325, 24984747817020, 476670900347380 @ -19, 294, -238
+212112768985246, 234501742570219, 124155071921577 @ 54, -34, 218
+338869855674325, 386664870421884, 174537446814868 @ -45, 220, 732
+304602699119581, 247415356610292, 237730462264480 @ -51, -40, 87
+201522270417337, 285205884453340, 399540925660236 @ 108, -48, -146
+326757229359428, 287469465594148, 258423126039770 @ -56, 95, 43
+333951128919449, 331322625326732, 453397225792116 @ -73, -7, -437
+292988972896088, 332905942698000, 252990122356426 @ 172, 283, 27
+384958618115821, 247508925135802, 401083403479964 @ -147, -43, -107
+281596559976835, 382226933972694, 280187261925958 @ 74, -116, -22
+347338880183865, 322738236098574, 448691665190778 @ -113, 304, -944
+264955694979067, 403952665234368, 153053196172780 @ 98, -185, 303
+307782647476363, 347773192266981, 271590305749501 @ 27, 40, -18
+367152045806920, 234243125497029, 252417867018223 @ -134, 46, 66
+291454116512653, 164941797533448, 386772051012232 @ -43, 19, -71
+244648686644621, 74473321237288, 423822977537712 @ 67, 335, -220
+371738115903269, 322834069329616, 327860913687192 @ -200, 158, -235
+306768194985703, 387225033930552, 320815377161014 @ 62, -53, -252
+314261905759726, 359781050506104, 334488218815414 @ -68, -189, -13
+272373310391389, 340174705578844, 270905323294753 @ 93, -9, 6
+217782060320639, 239743874379665, 75868546325352 @ 59, -22, 289
+375894419111917, 291779701795464, 439527813829720 @ -172, 71, -377
+489310372402870, 369981901801572, 334584256505716 @ -244, -201, -11
+257287473074670, 248009697251629, 291838103346963 @ 20, -10, 14
+145816820913779, 235003443009532, 348328300988480 @ 187, 23, -71
+345816222735610, 360157990964114, 299937550423123 @ -108, 273, -318
+198350092222519, 292429071608601, 336794186804518 @ 103, -68, -49
+224117248246469, 256297365293626, 431101666985804 @ 25, -82, -113
+110752387242301, 184626622675488, 288176733731296 @ 189, 43, 25
+326386961847376, 380573313647966, 266642825749899 @ -30, -51, -10
+128348548472147, 111177263615478, 63927760725468 @ 167, 133, 301
+286769988964609, 239257934452668, 200225830580262 @ 147, 577, 262
+337769607994122, 285274570185288, 298358572970588 @ -82, 115, -59
+292165954153983, 324666184042451, 243761085630574 @ 203, 384, 75
+320912056048390, 123348286817445, 257833508272936 @ -74, 64, 65
+275106210350605, 341850774826676, 304041305857796 @ 21, -103, -25
+328442104512972, 322558730340121, 489791000831846 @ -52, 68, -641
+339487928899561, 487418253546930, 498243712822242 @ -81, -446, -832
+313331026360933, 89709042465912, 204146867542768 @ -6, 769, 196
+236706269641310, 293781162907014, 364847958773123 @ 112, 13, -158
+279538407522829, 550131597783768, 19696530142084 @ -11, -421, 383
+293211307380926, 66094240565832, 430550575300350 @ -46, 115, -113
+333271637399793, 378355761107144, 214818391269928 @ 22, 371, 381
+325843512544115, 345217705337008, 292415233095689 @ -49, -21, -52
+420441557359870, 544064033960014, 314667303990353 @ -252, -483, -64
+268021405413465, 141044605679204, 314940805901424 @ 26, 216, -37
+260570202145320, 286363783957099, 11222456353998 @ 70, 36, 547
+319692915981775, 345999953400321, 189560446260662 @ 171, 730, 659
+179836906988840, 161203920328134, 39447901645168 @ 76, 25, 297
+350563758679413, 170556089358608, 247112200983672 @ -110, 218, 73
+334834073919370, 431635295115685, 207831261623386 @ -54, -240, 243
+361548280279369, 514189435413504, 398272723391668 @ -157, -529, -449
+370493312287576, 369938091892587, 473584283816371 @ -172, -78, -568
+303398968194050, 329366057677029, 243711831026538 @ -16, -50, 79
+270438813902908, 181490663000820, 289337244663856 @ -10, 39, 25
+254400483963875, 307642322287124, 244804645542848 @ 74, -19, 77
+312146397234765, 425334009313609, 517539480249663 @ -19, -238, -598
+113152039807619, 170070593691318, 157094384321022 @ 155, 25, 175
+275763389008533, 328212728463508, 74579605699968 @ 175, 168, 751
+195679788641677, 146550228445368, 280886425143448 @ 252, 418, -9
+331428536369057, 248257965259956, 174388217330008 @ -76, 64, 201
+281502442529605, 315900614706024, 293545970458528 @ -6, -89, 6
+519947284600358, 495701506799977, 419122501309588 @ -278, -328, -99
+172419326257043, 226353669769664, 351368934567462 @ 80, -49, -32
+333706656973399, 229744717806640, 313816869852676 @ -78, 135, -57
+267110402141650, 334660667695204, 295521975932789 @ 96, -9, -52
+216242569512810, 464422278901794, 343577846341774 @ 46, -299, -33
+229078419153034, 153290184037422, 330424902401150 @ 30, 49, -17
+198482350250745, 256015754330784, 229632043763513 @ 113, -5, 100
+322342956622625, 251344925510174, 281036336770388 @ -55, 101, 5
+286653289685853, 135859734501602, 298784647322574 @ -35, 65, 19
+114350058038805, 256004530503232, 295548005515368 @ 206, -28, 11
+267152206820407, 208276927258334, 265366704385984 @ 24, 96, 45
+443347397696629, 432287272587360, 333152076807796 @ -205, -263, -16
+288113563819415, 368647980128949, 49381325869643 @ 11, -134, 458
+217051686880615, 396484783975299, 247977484403728 @ 95, -206, 73
+261955486249395, 213440321942711, 282504619066439 @ 11, 30, 28
+214851418383385, 353352589684520, 69821891934088 @ 36, -181, 261
+211609119179538, 309269445218725, 261017025857522 @ 148, -30, 47
+318311090115901, 253689393162648, 244445467490848 @ -23, 265, 76
+296107616866830, 302129547578124, 283898755233783 @ 8, 31, -10
+133307131141155, 208333592171909, 289852225700998 @ 143, -6, 27
+331131130717605, 450517268725624, 357079438353828 @ 7, -369, -824
+355952604648953, 347503897397628, 320112678217674 @ -121, -95, -68
+328870765387125, 338472631582090, 302600646110641 @ -59, -15, -72
+326694164461003, 399342005912190, 256114962145246 @ 118, 200, -82
+309971204357293, 351186397545063, 309670007599705 @ 13, 12, -136
+300655266617485, 264279702750096, 413188486071736 @ -29, 8, -191
+349273400687770, 405472194021129, 160563578253598 @ -122, -112, 479
+288009504704101, 133540166340720, 189529189481656 @ 88, 738, 257
+318448889127518, 416349712478154, 237218397927819 @ 10, -179, 104
+220627166761237, 276302047504788, 412602211652320 @ 95, -16, -185
+433765655562877, 447565923223816, 455098276440024 @ -228, -283, -226
+349499197910978, 273042374600336, 161722557881602 @ -106, -37, 195
+237911712305755, 31778891691315, 380349689977690 @ 11, 150, -61
+317838779215960, 284602693333544, 348099634409958 @ -60, -45, -73
+246758131645855, 62136719247558, 177190186553584 @ 86, 442, 205
+441789526685301, 266733891477927, 336243814605428 @ -203, -86, -19
+322304061345021, 385318425241968, 285881931602400 @ 5, -23, -121
+272335950995355, 98284487215684, 346429929262348 @ -28, 65, -21
+249239072203677, 216041964124516, 322374425884550 @ 29, 29, -26
+254887883472677, 321843066365532, 298590923399276 @ 47, -80, -10
+109646561831065, 179014251500964, 294694065764008 @ 136, -10, 29

2023/d24/ex2/ex2.py

@@ -0,0 +1,65 @@
+#!/usr/bin/env python
+
+import sys
+from typing import NamedTuple
+
+import z3
+
+
+class Point(NamedTuple):
+    x: int
+    y: int
+    z: int
+
+
+class HailStone(NamedTuple):
+    pos: Point
+    vel: Point
+
+
+def solve(input: list[str]) -> int:
+    def parse_line(line: str) -> HailStone:
+        pos, vel = line.split(" @ ")
+        return HailStone(
+            Point(*map(int, pos.split(", "))), Point(*map(int, vel.split(", ")))
+        )
+
+    def parse(input: list[str]) -> list[HailStone]:
+        return [parse_line(line) for line in input]
+
+    # Bringing out the big guns to solve this
+    def run_z3(hailstones: list[HailStone]) -> HailStone:
+        solver = z3.Solver()
+
+        px, py, pz = (z3.Int(f"stone_p{coord}") for coord in ("x", "y", "z"))
+        vx, vy, vz = (z3.Int(f"stone_v{coord}") for coord in ("x", "y", "z"))
+
+        for i, other in enumerate(hailstones):
+            t = z3.Int(f"t_{i}")
+            # Must be in the future
+            solver.add(t >= 0)
+            # Must hit the hailstone
+            solver.add((px + vx * t) == (other.pos.x + other.vel.x * t))
+            solver.add((py + vy * t) == (other.pos.y + other.vel.y * t))
+            solver.add((pz + vz * t) == (other.pos.z + other.vel.z * t))
+
+        assert solver.check() == z3.sat  # Sanity check
+
+        model = solver.model()
+        return HailStone(
+            Point(*(model.eval(v).as_long() for v in (px, py, pz))),  # type: ignore
+            Point(*(model.eval(v).as_long() for v in (vx, vy, vz))),  # type: ignore
+        )
+
+    hailstones = parse(input)
+    stone = run_z3(hailstones)
+    return sum(stone.pos)
+
+
+def main() -> None:
+    input = sys.stdin.read().splitlines()
+    print(solve(input))
+
+
+if __name__ == "__main__":
+    main()

2023/d24/ex2/input

@@ -0,0 +1,300 @@
+260346828765750, 357833641339849, 229809969824403 @ 64, -114, 106
+340220726383465, 393110064924024, 226146987100003 @ -79, -61, 158
+11361697274707, 101596061919750, 46099495948720 @ 328, 162, 333
+360204609690721, 527678808395772, 271703202326380 @ -132, -458, 20
+228800225183261, 405333190838676, 284309641117406 @ 29, -233, 35
+347686754070960, 372761595433127, 227908656106580 @ -134, 452, 245
+420404387574505, 320613771806244, 282039825133426 @ -209, -99, 24
+239697674964055, 219683531868878, 291640535034286 @ 36, 12, 18
+270083622615715, 298192739573649, 450720525831403 @ 71, 50, -394
+210388952361528, 202933503071430, 369359171934512 @ 62, 13, -71
+323626194439723, 331061672127276, 297678575959794 @ -45, 7, -61
+304808549150934, 383205509992906, 523319353604760 @ -22, -163, -463
+187934586489225, 219381841648824, 260929087075428 @ 73, -29, 61
+334112509601119, 400144558186712, 244055841518098 @ 18, 155, 66
+246253930315613, 304696957680568, 94020244355048 @ 53, -63, 311
+342955905222035, 388277972401036, 257476145906070 @ -94, -111, 34
+327736098163477, 330547943777790, 153376586381074 @ -71, -90, 230
+261048582174545, 197767231455944, 278362708671168 @ -10, -13, 43
+262232829717925, 400052820669654, 363505406595748 @ 25, -212, -101
+324188029882468, 362855685632781, 234741485808022 @ 110, 502, 163
+205507378373754, 312370561869725, 214016656029865 @ 148, -46, 132
+239592601431541, 142078397267946, 285236791773286 @ 17, 58, 34
+144373393337221, 188196109756908, 173981678832424 @ 99, -22, 149
+288873332238259, 312782225890490, 274590086150334 @ 18, -6, 14
+186182198786950, 402152186162636, 135534511498564 @ 96, -225, 213
+231239063521245, 186020667465684, 343869538475528 @ 13, -20, -19
+250272260456639, 161173847651144, 288550442540870 @ 10, 51, 28
+296318163416530, 282047552083869, 393397156658776 @ 116, 426, -591
+324596493713872, 398326967096844, 254282763206956 @ 32, -9, 5
+215625978065245, 203168177356104, 420679288194328 @ 35, -25, -104
+191086370171245, 60115319750904, 146260480280128 @ 243, 573, 296
+322860700705485, 459545877374104, 448537560287088 @ -59, -309, -299
+314822321873915, 398359415059524, 264470104210778 @ 140, 49, -94
+269210714892168, 256327147227716, 398338379562592 @ 52, 95, -231
+302666483817653, 275410751736752, 326439099654152 @ -40, -40, -37
+270142822739620, 344779311267669, 324492644181298 @ 52, -80, -85
+374865332232522, 402789242720040, 323870419231066 @ -182, -173, -141
+243208589268314, 367086212824621, 199057002427101 @ 140, -102, 184
+250464382830742, 135024447362895, 320243825003503 @ -8, 24, 6
+355922778067984, 378321615748686, 241250226323332 @ -130, -107, 85
+316218511102785, 354948779738048, 394814158202160 @ 86, 273, -913
+321455854706509, 396440824238416, 314920648255344 @ 9, -75, -257
+169378410757153, 225633601154640, 335902593841960 @ 104, -23, -27
+310941798903565, 333771112844784, 286883552058694 @ 101, 351, -182
+411974191700116, 414045748557315, 447602203181716 @ -232, -222, -323
+282375423819373, 240799415094852, 287697942997588 @ -23, -28, 26
+424528361387804, 462909748733920, 382166946506320 @ -278, -325, -231
+163339958801001, 272115353229508, 302748903558972 @ 230, 32, -28
+258865845218325, 331436090977439, 237682017090608 @ 37, -100, 89
+302915997518781, 347231423515616, 296218913365336 @ -43, -147, 9
+201550834032262, 308185564073751, 181635624713110 @ 224, 24, 219
+326879140563285, 302444228750105, 363158049251869 @ -59, 38, -192
+199437546908251, 165065778022384, 281783000883451 @ 135, 171, 18
+275634964575007, 320652660558480, 161650608601594 @ 82, 39, 294
+299888387753175, 162477657523014, 431376299337848 @ -46, 58, -143
+392193811586581, 352294886790018, 355391098486984 @ -187, -111, -127
+368009114122653, 158595116827656, 240204738709240 @ -127, 64, 84
+235057921833792, 208902653782308, 369261469240150 @ 10, -41, -45
+333864628161721, 403967975589003, 236655090656734 @ 17, 100, 147
+315707153676205, 346742558497233, 239838980741152 @ -19, -16, 89
+265733060020157, 382781265854024, 325370365767928 @ 44, -169, -69
+244493835144625, 206378827546980, 278922806636032 @ 216, 460, -33
+336468228693530, 357997678992397, 445536876104649 @ -64, 78, -800
+334116663241987, 417641320056889, 460730643073845 @ -81, -234, -296
+283712214409060, 217794347554444, 318592790485419 @ 6, 111, -50
+181035782538969, 34330093599444, 116481838981164 @ 59, 121, 203
+267636391438175, 116019071284224, 274907016053068 @ -13, 91, 45
+359932116674365, 372724315764974, 242720827369528 @ -195, 137, 81
+413732861285365, 274346810098864, 265789907811328 @ -234, 50, 36
+353859733044440, 444601519540446, 186716148862678 @ -124, -287, 231
+266823502975823, 342804454729090, 139439752620420 @ 62, -72, 295
+299232903030949, 283130841945486, 266625316859842 @ -27, -23, 43
+275731283415043, 290995753064250, 269990654468416 @ 12, -32, 37
+284336299470177, 363011315559156, 245656891783664 @ 65, -65, 73
+300184773969053, 264674528467624, 288447324797656 @ -35, -19, 15
+364327543902318, 203179466147145, 202143114372903 @ -160, 454, 206
+240582515099049, 257855786814120, 267367130583972 @ 95, 67, 35
+322071439136631, 320755095987098, 240900218113582 @ -62, -76, 84
+407030376195355, 238248420347409, 280351241837773 @ -197, 44, 22
+363480833508100, 302741435647038, 374292309644818 @ -184, 337, -509
+305986467673468, 242537468667456, 312444331887847 @ 32, 395, -156
+252027155370005, 237764087612499, 383247340881198 @ 5, -44, -77
+372582774757039, 423473229980586, 294285328077664 @ -173, -231, -55
+284005653462811, 279636127688541, 343422083098399 @ 23, 50, -122
+307762320034081, 264568258469028, 248848044023842 @ -57, -71, 74
+356296354200217, 324248100646422, 270336780779350 @ -125, -18, 20
+310365295172069, 398733724603568, 271146207120040 @ 38, -112, -33
+332525984343205, 424881352868134, 234357444969968 @ 33, -126, 173
+352583954626249, 349239276790500, 353167414266244 @ -116, -82, -152
+297714119036800, 324271023294864, 362116453319623 @ -10, -53, -146
+285957271760765, 299826994507224, 268344479706678 @ 13, -5, 32
+243189693681529, 258702209578860, 199942339459600 @ 190, 242, 203
+326701397847709, 290194546332360, 296193493706296 @ -43, 195, -87
+292362934918391, 337984495256987, 353443507882303 @ 7, -66, -144
+329560214366727, 287131872509690, 283601935331544 @ -58, 144, -31
+419657717017333, 394749569068172, 492465483328742 @ -207, -207, -278
+424741311206371, 418004503651488, 366948667795378 @ -212, -241, -94
+289511348263829, 369752819333130, 313407769490726 @ 73, -56, -140
+317864241152929, 333597843545268, 280181752022452 @ -20, 40, -30
+159013055331421, 197040084742216, 154846454650744 @ 129, 27, 189
+310161956929405, 317608137512664, 286534497733492 @ -19, 11, -21
+328398331752021, 408235207737374, 277347063815996 @ 37, -19, -211
+352713775673581, 329046721759478, 139004188330392 @ -123, 50, 385
+303904706761629, 256397200765768, 300376317070392 @ -37, 8, -7
+273217189299031, 372821204372277, 128406796773907 @ 95, -92, 392
+152269575075685, 112586975003184, 246776862071728 @ 138, 132, 76
+316077180975508, 285040325144306, 333644269613969 @ -48, 5, -82
+291214477117667, 139137384078822, 239703215510530 @ -46, 28, 84
+282383815400461, 202954623809304, 225038200055848 @ 24, 196, 116
+168593234159600, 148914293359439, 291033865957193 @ 94, 48, 28
+398831545490785, 308451835604503, 274399283929173 @ -159, -126, 46
+240709939960879, 308439888753675, 278202135723646 @ 59, -72, 27
+279404244431973, 251750459409020, 95468761809964 @ 35, 114, 384
+420662877939440, 344775968361866, 525951427053175 @ -274, -55, -570
+327071630965000, 395761942422854, 262797011894253 @ 114, 245, -164
+334223852961341, 422841882209224, 241141724398936 @ 38, -69, 102
+331008090348665, 334101214652224, 233563791181228 @ -68, -31, 102
+365681210920495, 502432633101754, 311612110753818 @ -138, -388, -46
+349308710499373, 385266962186136, 265604633087480 @ -150, 292, -163
+302146562278813, 327132561288801, 243383000145796 @ 157, 400, 77
+253538164543510, 405218794636794, 381768323339290 @ 96, -199, -217
+235161774756385, 227712177337092, 326407943699224 @ 16, -48, -7
+236032878960545, 237730556620694, 427906712868538 @ 17, -55, -117
+329543688711978, 407035805550239, 145778919294318 @ -82, -234, 191
+179368688878425, 325143400816138, 366229488873984 @ 131, -112, -91
+371231992850378, 316638751988811, 236103319042700 @ -212, 244, 109
+339808454446741, 351596138940235, 279082311533963 @ -75, 170, -104
+351596216557693, 415490735560152, 387962665814524 @ -123, -193, -412
+278688411144475, 219677637474000, 280342089549808 @ -29, -37, 41
+227585847055153, 347006074356246, 373749729539980 @ 67, -140, -105
+312933684342933, 200941440991884, 335002534040332 @ -61, 16, -30
+280319712864331, 341572097476173, 270405943273150 @ 119, 58, -13
+334263217258791, 436302126934828, 368237906560810 @ -86, -267, -78
+258254831954108, 147783583066962, 333731768562520 @ -8, 37, -15
+355801879637895, 341787614777264, 302534030878548 @ -122, -73, -41
+131266234587925, 22532917085508, 198037908529672 @ 111, 140, 125
+341625668908842, 329754211784895, 301962684556755 @ -92, -8, -62
+105063826836925, 158508866142744, 351476391746242 @ 141, 11, -28
+412949842167537, 462762493467832, 334895606045844 @ -220, -313, -82
+329069085317565, 377407266331234, 426073969564998 @ -19, 44, -868
+217418593657566, 204726057801614, 242720827369528 @ 70, 41, 81
+338084512203857, 410004688486632, 239975437178400 @ -38, -5, 107
+379384638630079, 369543475974252, 402174952375396 @ -200, -71, -381
+386154908209069, 395639474455092, 280370845418350 @ -235, -131, -42
+275382644671282, 36951187740642, 151193435620480 @ 40, 537, 265
+356619952566811, 324712560155565, 331988520420058 @ -141, 124, -229
+358547496942130, 408300560102454, 267115051708363 @ -172, -115, -46
+346306312397521, 383668766131808, 228673142584364 @ -108, 5, 152
+359754386397630, 458720322718534, 559318866468353 @ -118, -295, -314
+351347143979005, 365572803517800, 259774637417128 @ -119, -57, 31
+302183764989621, 364256687909996, 265155690823964 @ 35, -36, 10
+330924340196260, 296427648577092, 141164605133864 @ -84, -113, 193
+364641746578165, 515395099355088, 306019572461464 @ -174, -558, -155
+339224696083261, 358367099969064, 263593215134050 @ -83, -29, 18
+193992358862501, 185968153834072, 367909202669970 @ 97, 59, -82
+336367817216524, 421844251871834, 247462114434092 @ 18, -39, 13
+161312373767566, 150227310716099, 291400675391663 @ 108, 56, 26
+231266455520539, 145495597439120, 287703190551144 @ 42, 95, 25
+206550308007613, 468743856845808, 162840383607640 @ 53, -303, 169
+429512031935863, 262967063704113, 273355464244561 @ -185, -92, 50
+380308299578381, 391625299100696, 505418060665704 @ -181, -163, -521
+330850564652410, 441663420225969, 416132167014268 @ -52, -282, -515
+375615981345391, 246897309609150, 541040247329687 @ -141, -11, -322
+257612492222965, 491419444805616, 398469152274232 @ 26, -346, -143
+292985656154761, 317945193289904, 184697849249204 @ 60, 101, 260
+232877219665201, 405217862288709, 271226801912872 @ 89, -214, 33
+348259631347512, 204238531298826, 312600183336479 @ -106, 169, -50
+268746780353590, 281608151109144, 383837866458733 @ 126, 195, -338
+122524059468689, 287919639112272, 167740167865852 @ 203, -65, 183
+312459888298897, 326923346974976, 225415511869904 @ 27, 167, 149
+319608062021405, 211487145992136, 254111710998584 @ -64, 49, 65
+242932724018775, 99557446164529, 454532431171443 @ 7, 84, -140
+257306506153525, 384718831609032, 260164650130816 @ 6, -205, 60
+346820458626153, 114882415853663, 188792118714110 @ -103, 294, 175
+313007300086521, 358742568002607, 296850115847834 @ -7, -38, -77
+178290472099096, 100952248470583, 338895184944207 @ 162, 260, -70
+232626084330181, 190661053821264, 325127462135648 @ 30, 16, -14
+372111394423630, 360975162645164, 266126939035668 @ -132, -177, 53
+448046725470493, 357813853076325, 323596691049628 @ -227, -170, -19
+241095145890565, 149424858214964, 213990140128028 @ 81, 233, 131
+335893091355037, 420535970089352, 269657513849720 @ 9, -52, -256
+344781417999610, 437369362040334, 233000501863018 @ -102, -263, 195
+317912587490765, 356977339413256, 421028144913168 @ -49, -117, -254
+349219513788590, 431309506759549, 505578881772528 @ -104, -262, -199
+301801136650301, 321621066036596, 298591305543704 @ 5, 14, -55
+197415955491805, 446870993170456, 251710862420360 @ 81, -280, 70
+328275156333949, 224085796039851, 111193637396461 @ -67, 152, 340
+333989052779735, 163119706265934, 181122434623568 @ -86, 70, 157
+318880316206670, 372095178926389, 267474120557491 @ 16, 26, -30
+308122992582769, 210364537012149, 317548450311542 @ -63, -44, 7
+348091459536315, 236767606013484, 310471779320178 @ -109, 295, -109
+341518034630073, 288253587957497, 238209449374690 @ -95, -70, 87
+340212283132345, 393453588795138, 268600848335248 @ -69, 40, -99
+280974192791863, 258914295404854, 280705588435520 @ -12, -24, 29
+282538583056945, 227062101647424, 243979447408168 @ 98, 401, 77
+288833639276521, 496224937883232, 345769934484472 @ 48, -423, -191
+255548451712998, 156282887184168, 316053658342303 @ -8, 19, 6
+285854755263325, 24984747817020, 476670900347380 @ -19, 294, -238
+212112768985246, 234501742570219, 124155071921577 @ 54, -34, 218
+338869855674325, 386664870421884, 174537446814868 @ -45, 220, 732
+304602699119581, 247415356610292, 237730462264480 @ -51, -40, 87
+201522270417337, 285205884453340, 399540925660236 @ 108, -48, -146
+326757229359428, 287469465594148, 258423126039770 @ -56, 95, 43
+333951128919449, 331322625326732, 453397225792116 @ -73, -7, -437
+292988972896088, 332905942698000, 252990122356426 @ 172, 283, 27
+384958618115821, 247508925135802, 401083403479964 @ -147, -43, -107
+281596559976835, 382226933972694, 280187261925958 @ 74, -116, -22
+347338880183865, 322738236098574, 448691665190778 @ -113, 304, -944
+264955694979067, 403952665234368, 153053196172780 @ 98, -185, 303
+307782647476363, 347773192266981, 271590305749501 @ 27, 40, -18
+367152045806920, 234243125497029, 252417867018223 @ -134, 46, 66
+291454116512653, 164941797533448, 386772051012232 @ -43, 19, -71
+244648686644621, 74473321237288, 423822977537712 @ 67, 335, -220
+371738115903269, 322834069329616, 327860913687192 @ -200, 158, -235
+306768194985703, 387225033930552, 320815377161014 @ 62, -53, -252
+314261905759726, 359781050506104, 334488218815414 @ -68, -189, -13
+272373310391389, 340174705578844, 270905323294753 @ 93, -9, 6
+217782060320639, 239743874379665, 75868546325352 @ 59, -22, 289
+375894419111917, 291779701795464, 439527813829720 @ -172, 71, -377
+489310372402870, 369981901801572, 334584256505716 @ -244, -201, -11
+257287473074670, 248009697251629, 291838103346963 @ 20, -10, 14
+145816820913779, 235003443009532, 348328300988480 @ 187, 23, -71
+345816222735610, 360157990964114, 299937550423123 @ -108, 273, -318
+198350092222519, 292429071608601, 336794186804518 @ 103, -68, -49
+224117248246469, 256297365293626, 431101666985804 @ 25, -82, -113
+110752387242301, 184626622675488, 288176733731296 @ 189, 43, 25
+326386961847376, 380573313647966, 266642825749899 @ -30, -51, -10
+128348548472147, 111177263615478, 63927760725468 @ 167, 133, 301
+286769988964609, 239257934452668, 200225830580262 @ 147, 577, 262
+337769607994122, 285274570185288, 298358572970588 @ -82, 115, -59
+292165954153983, 324666184042451, 243761085630574 @ 203, 384, 75
+320912056048390, 123348286817445, 257833508272936 @ -74, 64, 65
+275106210350605, 341850774826676, 304041305857796 @ 21, -103, -25
+328442104512972, 322558730340121, 489791000831846 @ -52, 68, -641
+339487928899561, 487418253546930, 498243712822242 @ -81, -446, -832
+313331026360933, 89709042465912, 204146867542768 @ -6, 769, 196
+236706269641310, 293781162907014, 364847958773123 @ 112, 13, -158
+279538407522829, 550131597783768, 19696530142084 @ -11, -421, 383
+293211307380926, 66094240565832, 430550575300350 @ -46, 115, -113
+333271637399793, 378355761107144, 214818391269928 @ 22, 371, 381
+325843512544115, 345217705337008, 292415233095689 @ -49, -21, -52
+420441557359870, 544064033960014, 314667303990353 @ -252, -483, -64
+268021405413465, 141044605679204, 314940805901424 @ 26, 216, -37
+260570202145320, 286363783957099, 11222456353998 @ 70, 36, 547
+319692915981775, 345999953400321, 189560446260662 @ 171, 730, 659
+179836906988840, 161203920328134, 39447901645168 @ 76, 25, 297
+350563758679413, 170556089358608, 247112200983672 @ -110, 218, 73
+334834073919370, 431635295115685, 207831261623386 @ -54, -240, 243
+361548280279369, 514189435413504, 398272723391668 @ -157, -529, -449
+370493312287576, 369938091892587, 473584283816371 @ -172, -78, -568
+303398968194050, 329366057677029, 243711831026538 @ -16, -50, 79
+270438813902908, 181490663000820, 289337244663856 @ -10, 39, 25
+254400483963875, 307642322287124, 244804645542848 @ 74, -19, 77
+312146397234765, 425334009313609, 517539480249663 @ -19, -238, -598
+113152039807619, 170070593691318, 157094384321022 @ 155, 25, 175
+275763389008533, 328212728463508, 74579605699968 @ 175, 168, 751
+195679788641677, 146550228445368, 280886425143448 @ 252, 418, -9
+331428536369057, 248257965259956, 174388217330008 @ -76, 64, 201
+281502442529605, 315900614706024, 293545970458528 @ -6, -89, 6
+519947284600358, 495701506799977, 419122501309588 @ -278, -328, -99
+172419326257043, 226353669769664, 351368934567462 @ 80, -49, -32
+333706656973399, 229744717806640, 313816869852676 @ -78, 135, -57
+267110402141650, 334660667695204, 295521975932789 @ 96, -9, -52
+216242569512810, 464422278901794, 343577846341774 @ 46, -299, -33
+229078419153034, 153290184037422, 330424902401150 @ 30, 49, -17
+198482350250745, 256015754330784, 229632043763513 @ 113, -5, 100
+322342956622625, 251344925510174, 281036336770388 @ -55, 101, 5
+286653289685853, 135859734501602, 298784647322574 @ -35, 65, 19
+114350058038805, 256004530503232, 295548005515368 @ 206, -28, 11
+267152206820407, 208276927258334, 265366704385984 @ 24, 96, 45
+443347397696629, 432287272587360, 333152076807796 @ -205, -263, -16
+288113563819415, 368647980128949, 49381325869643 @ 11, -134, 458
+217051686880615, 396484783975299, 247977484403728 @ 95, -206, 73
+261955486249395, 213440321942711, 282504619066439 @ 11, 30, 28
+214851418383385, 353352589684520, 69821891934088 @ 36, -181, 261
+211609119179538, 309269445218725, 261017025857522 @ 148, -30, 47
+318311090115901, 253689393162648, 244445467490848 @ -23, 265, 76
+296107616866830, 302129547578124, 283898755233783 @ 8, 31, -10
+133307131141155, 208333592171909, 289852225700998 @ 143, -6, 27
+331131130717605, 450517268725624, 357079438353828 @ 7, -369, -824
+355952604648953, 347503897397628, 320112678217674 @ -121, -95, -68
+328870765387125, 338472631582090, 302600646110641 @ -59, -15, -72
+326694164461003, 399342005912190, 256114962145246 @ 118, 200, -82
+309971204357293, 351186397545063, 309670007599705 @ 13, 12, -136
+300655266617485, 264279702750096, 413188486071736 @ -29, 8, -191
+349273400687770, 405472194021129, 160563578253598 @ -122, -112, 479
+288009504704101, 133540166340720, 189529189481656 @ 88, 738, 257
+318448889127518, 416349712478154, 237218397927819 @ 10, -179, 104
+220627166761237, 276302047504788, 412602211652320 @ 95, -16, -185
+433765655562877, 447565923223816, 455098276440024 @ -228, -283, -226
+349499197910978, 273042374600336, 161722557881602 @ -106, -37, 195
+237911712305755, 31778891691315, 380349689977690 @ 11, 150, -61
+317838779215960, 284602693333544, 348099634409958 @ -60, -45, -73
+246758131645855, 62136719247558, 177190186553584 @ 86, 442, 205
+441789526685301, 266733891477927, 336243814605428 @ -203, -86, -19
+322304061345021, 385318425241968, 285881931602400 @ 5, -23, -121
+272335950995355, 98284487215684, 346429929262348 @ -28, 65, -21
+249239072203677, 216041964124516, 322374425884550 @ 29, 29, -26
+254887883472677, 321843066365532, 298590923399276 @ 47, -80, -10
+109646561831065, 179014251500964, 294694065764008 @ 136, -10, 29