Day 24

Very, very shamelessly stolen from the r/adventofcode main thread where everyone was using this "Z3" library to solve equations. I'm not good at math, and this problem feels more like Advent of Linear Algebra than Code. Although it appears that Z3 doesn't work on mac since I had to switch back to my desktop PC for this one :(.

inputs/24.txt

@@ -0,0 +1,300 @@
+385803404726014, 386664184220541, 365612177547870 @ -192, -149, -36
+67771006464582, 193910554798739, 21517103663672 @ 280, 136, 426
+334054450538558, 356919582763697, 188448277532212 @ 84, -25, -48
+312676332944619, 337964672568504, 98227917525187 @ -35, -48, 372
+262053228716736, 348276320363511, 253216606954466 @ 37, -86, 31
+333526091894424, 327836481184227, 164687124486536 @ -65, 10, 196
+136308365945474, 334381606808383, 125587682445786 @ 158, -78, 267
+323717230671270, 328009829437175, 337115590656098 @ -108, -69, -33
+291700494449310, 337446891146933, 403527094306834 @ -89, -94, -36
+213920672175570, 65552798424640, 292480960528288 @ -8, 190, 81
+290980325848551, 318625443662390, 251065702879428 @ 73, 38, -87
+356219743903424, 372738065198325, 173629044789054 @ -91, -167, 45
+335569387143705, 220611972353945, 227370838301783 @ -123, 93, 118
+378989155122831, 373893551581799, 490516490184776 @ -183, -133, -179
+316964152354417, 377191852958393, 518250352298454 @ -97, -139, -301
+269488686042498, 302755736242613, 265930073075472 @ 40, 17, -15
+559034149216678, 519679436133677, 532650491704570 @ -390, -301, -211
+199481489198585, 29551954045775, 151234141438259 @ 111, 443, 232
+289629941437250, 268620305703325, 221264962397498 @ -7, 87, 85
+275358066553404, 274068078596243, 240507508125410 @ 37, 90, 31
+276827079064164, 101633616581386, 186011557695457 @ -26, 300, 176
+297663782856030, 402738199321925, 248211515653058 @ -71, -175, 93
+214575905428670, 285484598087669, 365634404691522 @ -9, -40, 5
+109561933588174, 237133241090922, 359706372666613 @ 92, 6, 18
+204240989840562, 334494358985081, 304086354165818 @ 30, -85, 43
+321555343478910, 357901758547385, 179203142613938 @ -24, -90, 147
+197324045077571, 308437347447096, 289742356642898 @ 135, -18, -17
+330975278295456, 345099029477697, 232960502418240 @ -53, -45, -40
+244758240275994, 148270370569025, 341619712434766 @ -11, 158, -16
+275658599167282, 139017182984065, 117542199700234 @ -25, 238, 285
+306387523207370, 360386737589534, 239496726901865 @ 56, -94, -98
+357978580614954, 356129825909997, 225719435454654 @ -146, -83, -15
+223671617009415, 329633075621279, 185533024675454 @ -29, -89, 195
+328411184086263, 388776342220522, 226872420062246 @ 139, -300, -389
+261336027047322, 256924147052505, 490381349202074 @ -23, 28, -239
+259930234799528, 371376965446663, 398040751251448 @ 129, -134, -462
+309284828898720, 323783526933825, 183744555090348 @ -23, -9, 152
+402330549565980, 498319351820615, 224808408030698 @ -203, -256, 155
+260202009982316, 216765106205019, 391896653167292 @ -55, 34, -26
+218982781599390, 67441612502790, 343883169644443 @ -20, 174, 36
+141849861082606, 232846248045093, 298748171766178 @ 54, 7, 83
+295185614280178, 182720577600545, 349236005990226 @ -27, 248, -165
+353023837337862, 362911500852077, 178701730402454 @ -18, -41, -94
+336507751402422, 441255078475877, 200229369315490 @ -71, -379, 71
+407581083289150, 362016498148165, 484015244537058 @ -267, -111, -537
+359880934389328, 226140351047332, 261590777229804 @ -150, 474, -219
+347056408084827, 283233021180721, 257388407347698 @ -23, 621, -657
+340294299033135, 285814062952309, 301398631300820 @ -89, 145, -251
+343359441017486, 357125315534487, 232880222781344 @ -100, -89, -23
+276206766363022, 349761305163973, 268152110657634 @ 45, -81, -45
+218499461041551, 258580353794663, 67849322645429 @ 17, 11, 334
+320248703670408, 295949247586567, 523439851127110 @ -101, -20, -315
+157580579887306, 153170757185349, 338622077484314 @ 80, 129, 7
+307640117451810, 410639435468045, 191294064358058 @ 89, -317, 65
+279333655319378, 268697691571573, 321070678033174 @ -10, 57, -79
+101435702073642, 337593450996443, 217618781821226 @ 162, -88, 147
+281338616293444, 205173494417713, 405155680382762 @ -81, 39, -29
+305661112743537, 420943144739793, 32241092006606 @ 97, -363, 787
+133047406299795, 332977572633730, 325570110580388 @ 73, -90, 49
+261489653779791, 355604852293248, 416249793033393 @ 73, -96, -382
+297873526074638, 237609011571077, 306287788749922 @ -61, 80, -13
+75576223796421, 167271768716129, 326600796406246 @ 127, 77, 51
+368252371944453, 343681121537330, 318054747911234 @ -177, -62, -193
+257149017625896, 403190872971397, 229440103526506 @ 34, -191, 87
+298005527228420, 281558791324245, 185293403577978 @ 45, 153, 131
+231602837664582, 101831236085297, 248521570744193 @ -28, 149, 128
+21252359315130, 21059531300255, 296125502732428 @ 184, 227, 81
+326602929473897, 340345994409110, 167594701873270 @ 9, 8, 171
+206330983367810, 272938599374485, 395597149200268 @ 6, -23, -36
+351549447904744, 318374618742317, 161108832503782 @ 27, 701, 149
+358111963088490, 352897661018525, 224279296470638 @ -129, -17, -242
+212305971866400, 216719158308705, 163041168183408 @ 70, 109, 213
+122577883308246, 176570270577385, 328470128003018 @ 130, 108, 13
+154379461786055, 156233048283330, 348097559718843 @ 53, 94, 24
+356118881302399, 188357412111249, 432270259923649 @ -145, 357, -516
+312634097133068, 451625774431512, 240165746735963 @ -46, -320, 28
+322897425919563, 280361425482827, 266947247491067 @ -103, 7, 56
+247585462288306, 310054234293952, 206044866280632 @ 168, 42, 81
+332607322558998, 305073031807001, 198798422489378 @ 10, 236, -17
+346536342417746, 386729620079641, 174268720304075 @ -48, -251, 100
+263876827856802, 427231721855813, 419953205489726 @ -55, -191, -66
+230753367061233, 325785277680899, 222305688880290 @ -35, -85, 159
+327146814427546, 297764481490689, 323003800135077 @ -16, 165, -460
+217482538469814, 202660948344989, 454198049536778 @ -22, 35, -67
+296199290528334, 245132082060181, 177066898565634 @ -92, 6, 201
+408872309569249, 350194185909070, 399144319536734 @ -225, -102, -101
+204142977649481, 217263391762093, 334611894084506 @ 29, 57, 7
+156704074837923, 232660472512901, 150915372815002 @ 127, 65, 231
+262327739537240, 314643700556177, 301997229498712 @ -19, -49, 14
+278164973199595, 438588939449196, 556014086873722 @ -9, -254, -505
+188464600595613, 357554529643547, 237970497821327 @ 113, -109, 94
+357893786525068, 385127898943489, 211678676681904 @ -145, -185, 26
+253118981308590, 88305653891225, 387537254229338 @ 20, 342, -163
+224753255269584, 428122393179597, 196648126327102 @ -5, -195, 177
+257844812203428, 474271472239727, 253608788201084 @ -63, -228, 130
+373522691552600, 249243808996561, 385902748709550 @ -199, 279, -555
+270491902410066, 294828689638902, 226582983241252 @ 40, 36, 69
+350568288964932, 325542602065395, 250512969350620 @ -113, 48, -156
+299879234623062, 149609032430601, 316083749535490 @ -56, 247, -49
+355759022426610, 399693237586045, 184148731797008 @ -134, -251, 112
+332275347951406, 155290138306308, 396310198678714 @ -132, 94, -25
+235090558147606, 118090735142509, 477784936530930 @ -22, 151, -133
+344536162610454, 333902401000940, 137203812026846 @ -60, 68, 331
+229764703931928, 286687790172347, 319014212319227 @ 34, -5, -18
+185589808729674, 323861854502775, 238965459280866 @ 112, -57, 95
+320329244342052, 380820007422950, 218743038252635 @ 34, -182, -64
+246323943658186, 319621711816065, 151311573960653 @ 168, 13, 238
+339899765593806, 351164577547109, 188639419559426 @ 12, 7, -19
+358958708239014, 356233140374949, 167650617335746 @ -101, 61, 59
+301296072448918, 336944897376310, 236672437707952 @ 20, -32, -15
+308813680617720, 323852727492110, 226410292584878 @ -30, -16, 51
+270764004306455, 548897325139115, 272911011482208 @ -13, -421, 33
+416810836165746, 406270086757761, 366948146706072 @ -230, -173, -36
+340338210994969, 323659246867766, 308886653932197 @ -117, -34, -90
+294782196886326, 314641921331837, 119889635452098 @ 97, 80, 363
+239345735629865, 213305416050295, 316553531846293 @ 35, 123, -34
+250544640362382, 299394738294149, 389706947690642 @ 24, -11, -166
+172163857890230, 220701506103165, 147168783541098 @ 282, 219, 245
+353149672821376, 473828597637297, 202528453563016 @ -127, -513, 54
+334761798631230, 238063182603797, 397425700070642 @ -134, 11, -31
+231294599142882, 266453629608965, 323083388744138 @ 42, 33, -37
+330626140721340, 219970028603525, 154730675449814 @ -129, 33, 225
+294742744027950, 251237230248770, 382666022989453 @ -68, 38, -94
+395640117641435, 271609279927070, 404013260156423 @ -199, -22, -44
+84145249222510, 202868062374993, 236124926340014 @ 236, 111, 109
+1147480396461, 328680810927084, 131081474315112 @ 205, -86, 249
+244578437707646, 181216989480941, 222406715810762 @ -18, 104, 142
+174303061990920, 200995288271765, 403466453112628 @ 25, 41, -24
+154000694867609, 147888010807127, 192734316982710 @ 137, 191, 171
+359313433797054, 444410665275881, 233762006860118 @ -136, -670, -332
+170571375161550, 252160944152645, 323932174944098 @ 34, -7, 51
+301382407091205, 218691969485375, 230168407528178 @ -43, 167, 79
+13025967189744, 119198576824901, 219020178573794 @ 195, 129, 159
+299848790911604, 299268300504307, 233302584702507 @ 78, 139, -70
+296888874680574, 316408018949579, 202311509285726 @ 100, 82, 41
+308456279989635, 307944306411035, 216077983664093 @ 21, 79, 22
+280711194242082, 352651376961857, 217109177418680 @ 110, -73, 22
+317256339757982, 192641114167013, 549053473440466 @ -103, 107, -298
+325989811826545, 171275237613355, 169425821040108 @ -19, 643, 173
+344941366910185, 255664705016710, 283718958985976 @ -139, 28, 49
+333251554537668, 365970089150282, 191866673285414 @ 50, -106, -29
+136968447517980, 400178308236315, 164869428513653 @ 82, -161, 214
+373682252861358, 401209311098893, 461257166168554 @ -176, -164, -126
+110827505798240, 287103948755763, 234916989725528 @ 126, -33, 133
+181498722876475, 265800912276387, 400841712935079 @ 51, -5, -66
+282115148812350, 293536077022345, 291225145069398 @ -8, 18, -36
+238252128186552, 188195777557738, 34996867375215 @ 22, 142, 404
+300014726902704, 178330721552265, 355195683167534 @ -101, 63, 25
+336744885426510, 350145796378565, 197103013221602 @ 111, 68, -198
+277501417377102, 470547254553125, 251637352470722 @ -8, -312, 50
+325225573544340, 231333623404767, 532183304522428 @ -119, 36, -222
+252511759947316, 317700280746416, 278149919520943 @ 50, -28, -12
+352890165412422, 336553287210569, 165267666249632 @ -76, 149, 149
+231348934600938, 254366523311037, 321747568814130 @ 34, 45, -25
+99287769103293, 128363597102876, 358183613415347 @ 107, 120, 16
+310579399159782, 357874859020073, 168900411964496 @ -40, -101, 194
+304053648301086, 309756584336021, 273944390963354 @ -102, -65, 100
+227639566933102, 256269293168281, 393834857944522 @ -28, -14, -15
+364056728028564, 328107026665253, 194844842320688 @ -165, -79, 178
+117354187118730, 124060602692789, 280020403532510 @ 81, 117, 100
+367011027830526, 250974647820149, 234309930017042 @ -171, 90, 80
+499904695450707, 478096080039786, 400757439302230 @ -323, -254, -61
+258040640626680, 312821058997749, 253745803620360 @ 46, -15, 29
+342350112377290, 337453812074005, 216597774328568 @ -42, 57, -128
+272589395905592, 362308351555047, 281416220790402 @ -13, -116, 15
+254277242373293, 486631552262484, 490219334751415 @ 59, -368, -460
+161464040078175, 177414221021094, 279559359116066 @ 151, 172, 31
+271812745641950, 327994886405985, 240547308085498 @ 180, 27, -93
+245547729072884, 250274242326647, 472465189929400 @ 77, 116, -424
+160017509685689, 386811739271505, 16060707315447 @ 63, -147, 380
+371408674786340, 368262083877290, 389270226210888 @ -202, -124, -855
+360848133478764, 335103859842419, 182536368199064 @ -146, 131, 25
+251415280525654, 265943852903625, 330163268299966 @ -12, 13, -13
+321378846481318, 269457275174747, 173946518956310 @ 24, 320, 145
+11609655378627, 86538947451740, 95867546502558 @ 415, 338, 323
+286476102094380, 372895613985005, 250761758718563 @ -10, -135, 34
+330249873564054, 376664151566117, 210874209509762 @ 142, -199, -281
+499914264357868, 460785966374769, 495870771492540 @ -411, -293, -390
+287025888751506, 315531236758649, 300662204953754 @ -17, -24, -55
+223296940143084, 310054592958761, 322315758351584 @ 107, -13, -98
+326888619499966, 284689293726849, 218896669238574 @ -48, 142, 24
+136239981548592, 400278990524767, 193497573497578 @ 82, -161, 183
+210561337637436, 225291686049970, 397870532857904 @ 22, 48, -71
+321848340476710, 305217776298849, 281081004739732 @ -64, 27, -78
+336438868463707, 348440111731678, 161679514523864 @ 57, 42, 181
+202575747710135, 258762689214605, 347513749995954 @ 11, -7, 15
+238409058372980, 313541653919600, 525712129016558 @ -22, -64, -197
+343106497521703, 370478769013508, 189320588944772 @ 105, -148, -215
+278653216285502, 139407367317109, 176975843111351 @ -52, 177, 196
+339643481027335, 337940842063855, 318841836094623 @ -129, -81, -18
+272356973044620, 286712261570935, 200719417926296 @ 46, 63, 121
+302906543748560, 302070911420845, 336766303991058 @ -81, -35, -25
+279222457335950, 312050730496005, 102341745970018 @ 158, 91, 431
+328547437601940, 333036626051585, 170617947872498 @ 93, 139, 119
+166638972882204, 250217091134834, 264006464658458 @ 202, 94, 23
+331862432860233, 336017505125100, 266490747895086 @ -83, -42, -61
+348882493761512, 399114947259306, 166868462711687 @ -118, -224, 190
+230880012567652, 152141032227571, 169979553304102 @ 93, 294, 197
+358671515142894, 359947272094261, 166634558141522 @ -122, -44, 130
+289647550517313, 414969996099002, 295461046245800 @ -57, -194, 21
+307575296006526, 303123297926029, 349977687288050 @ -38, 22, -215
+198786071327086, 292232694474279, 222993048305210 @ 44, -30, 139
+159215452463678, 221120051631181, 323115866538978 @ 32, 15, 63
+204534524932740, 62143454981063, 202682901675275 @ 46, 279, 162
+343359996629860, 364940274724195, 397134152420168 @ -114, -117, -383
+304932388434574, 180020546020549, 559488775282050 @ -106, 61, -178
+344622367429566, 271420746735293, 221794988056370 @ -46, 492, -191
+339707915865138, 433810942794301, 245552005360652 @ -122, -243, 64
+270252908062274, 293297964646059, 354986279299102 @ -30, -18, -63
+282085465044174, 152586385812549, 257148919074762 @ -68, 129, 104
+338794761942670, 475878171239173, 345229924058658 @ -54, -609, -627
+362956160157885, 356717926656095, 206778734147333 @ -161, 19, -378
+364219281383314, 383339262542702, 188489546365184 @ -168, -184, 97
+115985308065173, 419174535304638, 407917045548223 @ 77, -176, -22
+312753822248310, 291068067221525, 276958509886238 @ -94, -19, 56
+331612953739722, 341064297287381, 310812615029474 @ 13, 29, -641
+287465373724936, 319985803709435, 234870510667634 @ 45, 8, 7
+172212516198570, 289414744474577, 507608710608818 @ 21, -50, -117
+309215269980450, 281323554498441, 375557559571768 @ -74, 19, -142
+345237241565322, 439789038980931, 317319012156084 @ -146, -198, 62
+136236608164242, 204408369714737, 146875047362282 @ 163, 110, 237
+347149919610198, 355890620027765, 156303109326674 @ -53, -37, 225
+316087982604084, 292935285798693, 286260137414128 @ -35, 81, -132
+286688628133875, 213343995914435, 355792292221283 @ -43, 119, -92
+348242123716546, 372698104033365, 175629601536716 @ -6, -167, 22
+214427509021692, 231441141824881, 289710620646632 @ 178, 189, -83
+296728342720366, 500554200874617, 531845107148234 @ -12, -428, -635
+189530777124854, 336891148766333, 428264214534178 @ 15, -94, -57
+346805416215694, 304141377162341, 215670420933634 @ -66, 260, -130
+122846468064180, 240393315048620, 273299109906698 @ 182, 58, 55
+245431668678792, 158857280796983, 313221035815784 @ 30, 219, -35
+249150807637086, 236979316821965, 98713323753410 @ -30, 28, 291
+361137978353174, 281507210536999, 344843742655434 @ -160, 42, -141
+206554425526542, 225228566865989, 366127275139298 @ -7, 17, 13
+263100540524910, 327775089854501, 185350182259010 @ 111, -14, 144
+259570749464581, 240022292669580, 259176203591873 @ 33, 118, 28
+318617855203545, 473799498745136, 203304516316088 @ -59, -374, 113
+344991269514359, 384609075054521, 175814200859719 @ 17, -283, 32
+294149490465512, 336888681466399, 214461568604558 @ 15, -44, 73
+268217034231045, 246342332854445, 315317044433315 @ -9, 73, -36
+326670925035519, 332864273810972, 216177568193195 @ -15, 20, -20
+331326531537705, 397247514831405, 354957752366778 @ -119, -167, -57
+291070468901155, 303205932797500, 274215786828898 @ -7, 16, -33
+138151674503660, 98067558875400, 288521213148108 @ 126, 222, 53
+365208521217536, 512041671699004, 231661683223733 @ -166, -270, 148
+356211081141222, 372214614835685, 153452665853450 @ -37, -187, 280
+323765442571726, 345632817800261, 182778811713890 @ -42, -55, 142
+254709505868332, 317989160069186, 252775492763325 @ 162, 26, -66
+353111062175862, 372020836587373, 176974127522570 @ -5, -176, -98
+227044590569750, 213039856604975, 351877513853748 @ -12, 47, 5
+199710109883440, 93411462486105, 274387189002473 @ 90, 301, 40
+154846141458601, 308672678971386, 462714529941148 @ 47, -66, -87
+283162731133017, 278511724283134, 122344762985860 @ 37, 100, 309
+278452443212631, 269128033327091, 368778544617365 @ -23, 39, -130
+116850894919422, 230400566950229, 165050987749346 @ 302, 135, 207
+260697705868248, 331507689359744, 230934509869239 @ 58, -46, 62
+345883734794082, 404319736386014, 165508639034243 @ -96, -266, 188
+338518007127116, 197895428534989, 333026065429020 @ -82, 441, -363
+501219359367120, 412285025575991, 553543190879582 @ -374, -193, -381
+315802188788550, 335952206092989, 221378550288190 @ 46, 19, -64
+318355888692006, 379462736241893, 346108974688070 @ -62, -151, -208
+258432198353802, 116363585901746, 279158788196090 @ 48, 384, -25
+331495566132405, 329696949720270, 262637093449293 @ -71, -12, -88
+225128317377718, 98339882122589, 405612346982306 @ 9, 212, -89
+339590953497350, 387529697719375, 418409016132703 @ -60, -209, -930
+188156378042670, 144991106399203, 54479747459418 @ 76, 180, 363
+189508861409856, 220025770701113, 300342334256882 @ 39, 47, 55
+355470936519087, 377588730568583, 186025958729126 @ -123, -173, 67
+357617990656670, 278931805125261, 301898192453698 @ -154, 34, -37
+213886629816471, 247221744883994, 187412927602760 @ 117, 102, 165
+296374173800760, 169384218125771, 83441210687864 @ 111, 694, 524
+236639955898698, 151938093144053, 194945971221898 @ 67, 269, 153
+288917518632726, 492724869524685, 228500513113072 @ -8, -387, 72
+295727746197582, 360474744238229, 503124831753782 @ -68, -115, -270
+282189594610170, 282491392005509, 436551439705984 @ -74, -31, -88
+314954230601466, 420548190234857, 214580005953260 @ 64, -371, -51
+357847064816890, 337336638576149, 184267494146994 @ -109, 197, -61
+348706752056672, 275377145397879, 169020924918062 @ -73, 460, 145
+214663556424384, 302115053921987, 548387355035240 @ -15, -60, -170
+137816123354705, 68881532714919, 90822718496989 @ 141, 279, 312
+248891797596266, 313785440491389, 60802879347282 @ 89, -5, 435
+469165669056299, 304541996543790, 499226179275000 @ -271, -62, -123
+265821000515835, 161895492455969, 181634450597243 @ 11, 245, 178
+356285242983476, 347728362889153, 158843970135404 @ -81, 127, 196
+324775129764550, 347016718050565, 202162951243018 @ 159, 57, -160
+235138827258360, 84780944337545, 375637426198508 @ 19, 279, -90
+207155653686690, 268708428643649, 269113419224924 @ 216, 117, -51
+328903202326354, 314642642432431, 231385235953726 @ -42, 66, -43
+351348584362654, 328210234088285, 183423860793722 @ -46, 278, -44
+133923271127655, 15946363179440, 218432342211833 @ 77, 244, 158
+261067422616210, 294587005892105, 54887803745498 @ 71, 44, 457
+331821353676594, 422141575447479, 299518708308799 @ 40, -473, -706
+369931379292600, 277109566356635, 291555687461348 @ -207, 460, -640
+271201570580361, 319931769006502, 233949945157639 @ 37, -20, 54
+219929906219867, 351074327917355, 267765680025459 @ 77, -97, 36
+292339075455432, 199741793871233, 285373325473232 @ -71, 95, 54
+346900087043760, 288681201410123, 253127416209530 @ -114, 119, -73
+347544901928734, 345957012938925, 155174759798780 @ 68, 213, 244
+241918384900110, 396704843204545, 178323238720558 @ 76, -182, 180
+305784694247844, 291026924781121, 547325893026114 @ -77, -9, -369

inputs/24a.txt

@@ -0,0 +1,5 @@
+19, 13, 30 @ -2,  1, -2
+18, 19, 22 @ -1, -1, -2
+20, 25, 34 @ -2, -2, -4
+12, 31, 28 @ -1, -2, -1
+20, 19, 15 @  1, -5, -3