32-4-6 Sudoku s koněm: důkaz optimality Toto je výstup programu, který SAT solverem ověřuje, jestli se dá najít řešení s daným prefixem. Prefix rozšiřujeme od největší možné hodnoty, tak zajistíme, že najdeme největší možné skóre. Všechny nalezené modely (dvě symetrická řešení - ostatní symetrie jsme omezili) jsou vypsány. Jde o jediné optimální řešení, což jsme dokázali tím, že jsme opakovaně řešili SAT se zakázanými už nalezenými modely. 99999999 ...Not satisfiable [792.04ms] 99999998 ...OK [1.68s] 999999989 ...Not satisfiable [812.99ms] 999999988 ...OK [7.55s] 9999999889 ...OK [7.20s] 99999998899 ...Not satisfiable [779.70ms] 99999998898 ...OK [5.97s] 999999988989 ...Not satisfiable [800.42ms] 999999988988 ...OK [4.88s] 9999999889889 ...Not satisfiable [787.07ms] 9999999889888 ...OK [5.13s] 99999998898889 ...Not satisfiable [796.74ms] 99999998898888 ...OK [5.43s] 999999988988889 ...OK [7.43s] 9999999889888898 ...Not satisfiable [786.78ms] 9999999889888897 ...OK [6.87s] 99999998898888978 ...Not satisfiable [801.50ms] 99999998898888977 ...OK [3.49s] 999999988988889778 ...OK [8.06s] 9999999889888897788 ...Not satisfiable [806.94ms] 9999999889888897787 ...OK [5.71s] 99999998898888977878 ...Not satisfiable [793.49ms] 99999998898888977877 ...OK [3.58s] 999999988988889778778 ...Not satisfiable [814.58ms] 999999988988889778777 ...OK [7.55s] 9999999889888897787778 ...Not satisfiable [786.90ms] 9999999889888897787777 ...OK [7.19s] 99999998898888977877778 ...Not satisfiable [791.02ms] 99999998898888977877777 ...Not satisfiable [4.10s] 99999998898888977877776 ...OK [10.08s] 999999988988889778777768 ...Not satisfiable [837.02ms] 999999988988889778777767 ...Not satisfiable [4.06s] 999999988988889778777766 ...OK [9.26s] 9999999889888897787777668 ...Not satisfiable [4.28s] 9999999889888897787777667 ...OK [9.11s] 99999998898888977877776678 ...Not satisfiable [798.46ms] 99999998898888977877776677 ...Not satisfiable [796.73ms] 99999998898888977877776676 ...Not satisfiable [4.36s] 99999998898888977877776675 ...OK [13.18s] 999999988988889778777766758 ...Not satisfiable [3.17s] 999999988988889778777766757 ...Not satisfiable [811.19ms] 999999988988889778777766756 ...OK [7.80s] 9999999889888897787777667568 ...Not satisfiable [780.78ms] 9999999889888897787777667567 ...OK [8.33s] 99999998898888977877776675678 ...Not satisfiable [796.31ms] 99999998898888977877776675677 ...Not satisfiable [794.68ms] 99999998898888977877776675676 ...Not satisfiable [6.74s] 99999998898888977877776675675 ...OK [9.61s] 999999988988889778777766756758 ...Not satisfiable [815.13ms] 999999988988889778777766756757 ...Not satisfiable [821.91ms] 999999988988889778777766756756 ...OK [6.39s] 9999999889888897787777667567568 ...Not satisfiable [1.10s] 9999999889888897787777667567567 ...Not satisfiable [1.02s] 9999999889888897787777667567566 ...Not satisfiable [8.01s] 9999999889888897787777667567565 ...OK [5.38s] 99999998898888977877776675675658 ...Not satisfiable [796.68ms] 99999998898888977877776675675657 ...Not satisfiable [873.11ms] 99999998898888977877776675675656 ...Not satisfiable [5.54s] 99999998898888977877776675675655 ...Not satisfiable [5.87s] 99999998898888977877776675675654 ...OK [8.01s] 999999988988889778777766756756548 ...Not satisfiable [3.90s] 999999988988889778777766756756547 ...Not satisfiable [2.64s] 999999988988889778777766756756546 ...OK [7.31s] 9999999889888897787777667567565468 ...Not satisfiable [788.10ms] 9999999889888897787777667567565467 ...Not satisfiable [811.74ms] 9999999889888897787777667567565466 ...OK [6.34s] 99999998898888977877776675675654668 ...Not satisfiable [2.26s] 99999998898888977877776675675654667 ...Not satisfiable [2.49s] 99999998898888977877776675675654666 ...Not satisfiable [1.78s] 99999998898888977877776675675654665 ...OK [6.06s] 999999988988889778777766756756546658 ...Not satisfiable [797.47ms] 999999988988889778777766756756546657 ...Not satisfiable [822.97ms] 999999988988889778777766756756546656 ...Not satisfiable [1.04s] 999999988988889778777766756756546655 ...Not satisfiable [11.33s] 999999988988889778777766756756546654 ...OK [3.34s] 9999999889888897787777667567565466548 ...Not satisfiable [4.84s] 9999999889888897787777667567565466547 ...Not satisfiable [2.47s] 9999999889888897787777667567565466546 ...Not satisfiable [5.95s] 9999999889888897787777667567565466545 ...Not satisfiable [9.03s] 9999999889888897787777667567565466544 ...OK [4.68s] 99999998898888977877776675675654665448 ...Not satisfiable [792.26ms] 99999998898888977877776675675654665447 ...Not satisfiable [829.80ms] 99999998898888977877776675675654665446 ...Not satisfiable [1.92s] 99999998898888977877776675675654665445 ...Not satisfiable [4.58s] 99999998898888977877776675675654665444 ...Not satisfiable [6.85s] 99999998898888977877776675675654665443 ...OK [4.96s] 999999988988889778777766756756546654438 ...Not satisfiable [5.15s] 999999988988889778777766756756546654437 ...Not satisfiable [1.18s] 999999988988889778777766756756546654436 ...Not satisfiable [11.24s] 999999988988889778777766756756546654435 ...Not satisfiable [7.91s] 999999988988889778777766756756546654434 ...Not satisfiable [6.21s] 999999988988889778777766756756546654433 ...OK [4.31s] 9999999889888897787777667567565466544338 ...Not satisfiable [807.19ms] 9999999889888897787777667567565466544337 ...Not satisfiable [814.60ms] 9999999889888897787777667567565466544336 ...Not satisfiable [5.16s] 9999999889888897787777667567565466544335 ...Not satisfiable [11.22s] 9999999889888897787777667567565466544334 ...OK [4.96s] 99999998898888977877776675675654665443348 ...Not satisfiable [2.61s] 99999998898888977877776675675654665443347 ...Not satisfiable [1.08s] 99999998898888977877776675675654665443346 ...OK [4.50s] 999999988988889778777766756756546654433468 ...Not satisfiable [793.95ms] 999999988988889778777766756756546654433467 ...Not satisfiable [841.30ms] 999999988988889778777766756756546654433466 ...Not satisfiable [881.80ms] 999999988988889778777766756756546654433465 ...Not satisfiable [2.47s] 999999988988889778777766756756546654433464 ...Not satisfiable [3.55s] 999999988988889778777766756756546654433463 ...Not satisfiable [7.55s] 999999988988889778777766756756546654433462 ...OK [4.60s] 9999999889888897787777667567565466544334628 ...Not satisfiable [1.50s] 9999999889888897787777667567565466544334627 ...Not satisfiable [885.86ms] 9999999889888897787777667567565466544334626 ...Not satisfiable [2.10s] 9999999889888897787777667567565466544334625 ...Not satisfiable [2.31s] 9999999889888897787777667567565466544334624 ...Not satisfiable [2.32s] 9999999889888897787777667567565466544334623 ...OK [3.35s] 99999998898888977877776675675654665443346238 ...Not satisfiable [1.18s] 99999998898888977877776675675654665443346237 ...Not satisfiable [876.43ms] 99999998898888977877776675675654665443346236 ...Not satisfiable [1.35s] 99999998898888977877776675675654665443346235 ...OK [3.06s] 999999988988889778777766756756546654433462358 ...Not satisfiable [997.89ms] 999999988988889778777766756756546654433462357 ...Not satisfiable [849.35ms] 999999988988889778777766756756546654433462356 ...Not satisfiable [1.09s] 999999988988889778777766756756546654433462355 ...OK [2.10s] 9999999889888897787777667567565466544334623558 ...Not satisfiable [793.42ms] 9999999889888897787777667567565466544334623557 ...Not satisfiable [828.16ms] 9999999889888897787777667567565466544334623556 ...Not satisfiable [988.14ms] 9999999889888897787777667567565466544334623555 ...Not satisfiable [1.05s] 9999999889888897787777667567565466544334623554 ...OK [2.11s] 99999998898888977877776675675654665443346235548 ...Not satisfiable [979.87ms] 99999998898888977877776675675654665443346235547 ...Not satisfiable [832.18ms] 99999998898888977877776675675654665443346235546 ...Not satisfiable [1.08s] 99999998898888977877776675675654665443346235545 ...Not satisfiable [1.19s] 99999998898888977877776675675654665443346235544 ...Not satisfiable [1.30s] 99999998898888977877776675675654665443346235543 ...Not satisfiable [1.20s] 99999998898888977877776675675654665443346235542 ...Not satisfiable [1.68s] 99999998898888977877776675675654665443346235541 ...OK [1.49s] 999999988988889778777766756756546654433462355418 ...Not satisfiable [794.36ms] 999999988988889778777766756756546654433462355417 ...Not satisfiable [833.48ms] 999999988988889778777766756756546654433462355416 ...Not satisfiable [1.95s] 999999988988889778777766756756546654433462355415 ...OK [1.05s] 9999999889888897787777667567565466544334623554158 ...Not satisfiable [877.11ms] 9999999889888897787777667567565466544334623554157 ...Not satisfiable [808.65ms] 9999999889888897787777667567565466544334623554156 ...Not satisfiable [1.56s] 9999999889888897787777667567565466544334623554155 ...Not satisfiable [978.51ms] 9999999889888897787777667567565466544334623554154 ...Not satisfiable [1.04s] 9999999889888897787777667567565466544334623554153 ...Not satisfiable [1.07s] 9999999889888897787777667567565466544334623554152 ...Not satisfiable [1.29s] 9999999889888897787777667567565466544334623554151 ...OK [1.52s] 99999998898888977877776675675654665443346235541518 ...Not satisfiable [783.51ms] 99999998898888977877776675675654665443346235541517 ...Not satisfiable [812.62ms] 99999998898888977877776675675654665443346235541516 ...Not satisfiable [1.04s] 99999998898888977877776675675654665443346235541515 ...Not satisfiable [1.05s] 99999998898888977877776675675654665443346235541514 ...Not satisfiable [1.07s] 99999998898888977877776675675654665443346235541513 ...OK [1.19s] 999999988988889778777766756756546654433462355415138 ...Not satisfiable [926.37ms] 999999988988889778777766756756546654433462355415137 ...Not satisfiable [855.31ms] 999999988988889778777766756756546654433462355415136 ...Not satisfiable [1.10s] 999999988988889778777766756756546654433462355415135 ...Not satisfiable [1.19s] 999999988988889778777766756756546654433462355415134 ...Not satisfiable [1.18s] 999999988988889778777766756756546654433462355415133 ...Not satisfiable [1.21s] 999999988988889778777766756756546654433462355415132 ...OK [1.11s] 9999999889888897787777667567565466544334623554151328 ...Not satisfiable [786.46ms] 9999999889888897787777667567565466544334623554151327 ...Not satisfiable [816.48ms] 9999999889888897787777667567565466544334623554151326 ...Not satisfiable [1.09s] 9999999889888897787777667567565466544334623554151325 ...Not satisfiable [1.09s] 9999999889888897787777667567565466544334623554151324 ...Not satisfiable [1.58s] 9999999889888897787777667567565466544334623554151323 ...Not satisfiable [1.18s] 9999999889888897787777667567565466544334623554151322 ...OK [1.02s] 99999998898888977877776675675654665443346235541513228 ...Not satisfiable [1.07s] 99999998898888977877776675675654665443346235541513227 ...Not satisfiable [876.01ms] 99999998898888977877776675675654665443346235541513226 ...Not satisfiable [1.05s] 99999998898888977877776675675654665443346235541513225 ...OK [1.07s] 999999988988889778777766756756546654433462355415132258 ...Not satisfiable [776.45ms] 999999988988889778777766756756546654433462355415132257 ...Not satisfiable [802.22ms] 999999988988889778777766756756546654433462355415132256 ...Not satisfiable [1.06s] 999999988988889778777766756756546654433462355415132255 ...Not satisfiable [1.12s] 999999988988889778777766756756546654433462355415132254 ...Not satisfiable [1.14s] 999999988988889778777766756756546654433462355415132253 ...Not satisfiable [1.14s] 999999988988889778777766756756546654433462355415132252 ...Not satisfiable [1.09s] 999999988988889778777766756756546654433462355415132251 ...OK [1.04s] 9999999889888897787777667567565466544334623554151322518 ...Not satisfiable [974.61ms] 9999999889888897787777667567565466544334623554151322517 ...Not satisfiable [928.76ms] 9999999889888897787777667567565466544334623554151322516 ...Not satisfiable [1.15s] 9999999889888897787777667567565466544334623554151322515 ...Not satisfiable [1.05s] 9999999889888897787777667567565466544334623554151322514 ...Not satisfiable [1.14s] 9999999889888897787777667567565466544334623554151322513 ...Not satisfiable [1.08s] 9999999889888897787777667567565466544334623554151322512 ...Not satisfiable [1.04s] 9999999889888897787777667567565466544334623554151322511 ...OK [996.33ms] 99999998898888977877776675675654665443346235541513225118 ...Not satisfiable [775.04ms] 99999998898888977877776675675654665443346235541513225117 ...Not satisfiable [802.53ms] 99999998898888977877776675675654665443346235541513225116 ...Not satisfiable [1.03s] 99999998898888977877776675675654665443346235541513225115 ...Not satisfiable [1.10s] 99999998898888977877776675675654665443346235541513225114 ...OK [1.52s] 999999988988889778777766756756546654433462355415132251148 ...OK [1.31s] 9999999889888897787777667567565466544334623554151322511488 ...Not satisfiable [786.01ms] 9999999889888897787777667567565466544334623554151322511487 ...Not satisfiable [796.99ms] 9999999889888897787777667567565466544334623554151322511486 ...Not satisfiable [860.07ms] 9999999889888897787777667567565466544334623554151322511485 ...Not satisfiable [970.96ms] 9999999889888897787777667567565466544334623554151322511484 ...Not satisfiable [794.41ms] 9999999889888897787777667567565466544334623554151322511483 ...Not satisfiable [1.05s] 9999999889888897787777667567565466544334623554151322511482 ...Not satisfiable [1.13s] 9999999889888897787777667567565466544334623554151322511481 ...OK [881.33ms] 99999998898888977877776675675654665443346235541513225114818 ...Not satisfiable [787.54ms] 99999998898888977877776675675654665443346235541513225114817 ...Not satisfiable [768.19ms] 99999998898888977877776675675654665443346235541513225114816 ...Not satisfiable [882.90ms] 99999998898888977877776675675654665443346235541513225114815 ...Not satisfiable [1.01s] 99999998898888977877776675675654665443346235541513225114814 ...Not satisfiable [1.05s] 99999998898888977877776675675654665443346235541513225114813 ...Not satisfiable [925.32ms] 99999998898888977877776675675654665443346235541513225114812 ...Not satisfiable [1.20s] 99999998898888977877776675675654665443346235541513225114811 ...OK [948.10ms] 999999988988889778777766756756546654433462355415132251148118 ...Not satisfiable [774.39ms] 999999988988889778777766756756546654433462355415132251148117 ...Not satisfiable [786.38ms] 999999988988889778777766756756546654433462355415132251148116 ...Not satisfiable [909.26ms] 999999988988889778777766756756546654433462355415132251148115 ...OK [882.99ms] 9999999889888897787777667567565466544334623554151322511481158 ...Not satisfiable [781.93ms] 9999999889888897787777667567565466544334623554151322511481157 ...Not satisfiable [782.27ms] 9999999889888897787777667567565466544334623554151322511481156 ...OK [880.44ms] 99999998898888977877776675675654665443346235541513225114811568 ...Not satisfiable [780.04ms] 99999998898888977877776675675654665443346235541513225114811567 ...Not satisfiable [789.76ms] 99999998898888977877776675675654665443346235541513225114811566 ...Not satisfiable [882.89ms] 99999998898888977877776675675654665443346235541513225114811564 ...Not satisfiable [1.06s] 99999998898888977877776675675654665443346235541513225114811563 ...OK [917.37ms] 999999988988889778777766756756546654433462355415132251148115638 ...Not satisfiable [832.63ms] 999999988988889778777766756756546654433462355415132251148115637 ...Not satisfiable [804.92ms] 999999988988889778777766756756546654433462355415132251148115636 ...Not satisfiable [851.95ms] 999999988988889778777766756756546654433462355415132251148115634 ...Not satisfiable [882.31ms] 999999988988889778777766756756546654433462355415132251148115633 ...Not satisfiable [897.77ms] 999999988988889778777766756756546654433462355415132251148115632 ...OK [857.20ms] 9999999889888897787777667567565466544334623554151322511481156328 ...Not satisfiable [786.68ms] 9999999889888897787777667567565466544334623554151322511481156327 ...Not satisfiable [796.64ms] 9999999889888897787777667567565466544334623554151322511481156326 ...Not satisfiable [983.08ms] 9999999889888897787777667567565466544334623554151322511481156324 ...OK [879.70ms] 99999998898888977877776675675654665443346235541513225114811563248 ...Not satisfiable [893.39ms] 99999998898888977877776675675654665443346235541513225114811563247 ...Not satisfiable [825.30ms] 99999998898888977877776675675654665443346235541513225114811563246 ...Not satisfiable [897.18ms] 99999998898888977877776675675654665443346235541513225114811563244 ...Not satisfiable [847.86ms] 99999998898888977877776675675654665443346235541513225114811563243 ...Not satisfiable [919.75ms] 99999998898888977877776675675654665443346235541513225114811563242 ...Not satisfiable [1.03s] 99999998898888977877776675675654665443346235541513225114811563241 ...OK [877.89ms] 999999988988889778777766756756546654433462355415132251148115632418 ...Not satisfiable [838.65ms] 999999988988889778777766756756546654433462355415132251148115632417 ...Not satisfiable [820.93ms] 999999988988889778777766756756546654433462355415132251148115632416 ...Not satisfiable [1.04s] 999999988988889778777766756756546654433462355415132251148115632414 ...Not satisfiable [938.50ms] 999999988988889778777766756756546654433462355415132251148115632413 ...OK [866.30ms] 9999999889888897787777667567565466544334623554151322511481156324138 ...Not satisfiable [957.58ms] 9999999889888897787777667567565466544334623554151322511481156324137 ...Not satisfiable [886.49ms] 9999999889888897787777667567565466544334623554151322511481156324136 ...Not satisfiable [891.84ms] 9999999889888897787777667567565466544334623554151322511481156324134 ...Not satisfiable [907.61ms] 9999999889888897787777667567565466544334623554151322511481156324133 ...Not satisfiable [880.85ms] 9999999889888897787777667567565466544334623554151322511481156324132 ...OK [871.10ms] 99999998898888977877776675675654665443346235541513225114811563241328 ...Not satisfiable [776.93ms] 99999998898888977877776675675654665443346235541513225114811563241327 ...Not satisfiable [800.16ms] 99999998898888977877776675675654665443346235541513225114811563241326 ...Not satisfiable [900.50ms] 99999998898888977877776675675654665443346235541513225114811563241324 ...Not satisfiable [910.93ms] 99999998898888977877776675675654665443346235541513225114811563241323 ...OK [869.07ms] 999999988988889778777766756756546654433462355415132251148115632413238 ...Not satisfiable [875.12ms] 999999988988889778777766756756546654433462355415132251148115632413237 ...Not satisfiable [863.03ms] 999999988988889778777766756756546654433462355415132251148115632413236 ...Not satisfiable [954.42ms] 999999988988889778777766756756546654433462355415132251148115632413234 ...Not satisfiable [914.06ms] 999999988988889778777766756756546654433462355415132251148115632413233 ...Not satisfiable [892.11ms] 999999988988889778777766756756546654433462355415132251148115632413232 ...OK [857.23ms] 9999999889888897787777667567565466544334623554151322511481156324132328 ...Not satisfiable [770.52ms] 9999999889888897787777667567565466544334623554151322511481156324132327 ...Not satisfiable [787.17ms] 9999999889888897787777667567565466544334623554151322511481156324132326 ...Not satisfiable [926.86ms] 9999999889888897787777667567565466544334623554151322511481156324132324 ...Not satisfiable [909.57ms] 9999999889888897787777667567565466544334623554151322511481156324132323 ...Not satisfiable [877.44ms] 9999999889888897787777667567565466544334623554151322511481156324132322 ...OK [860.81ms] 99999998898888977877776675675654665443346235541513225114811563241323228 ...Not satisfiable [952.30ms] 99999998898888977877776675675654665443346235541513225114811563241323227 ...Not satisfiable [841.60ms] 99999998898888977877776675675654665443346235541513225114811563241323226 ...Not satisfiable [994.94ms] 99999998898888977877776675675654665443346235541513225114811563241323224 ...Not satisfiable [871.37ms] 99999998898888977877776675675654665443346235541513225114811563241323223 ...OK [844.35ms] 999999988988889778777766756756546654433462355415132251148115632413232238 ...Not satisfiable [829.03ms] 999999988988889778777766756756546654433462355415132251148115632413232237 ...Not satisfiable [834.19ms] 999999988988889778777766756756546654433462355415132251148115632413232236 ...Not satisfiable [890.10ms] 999999988988889778777766756756546654433462355415132251148115632413232234 ...OK [941.11ms] 9999999889888897787777667567565466544334623554151322511481156324132322348 ...Not satisfiable [1.03s] 9999999889888897787777667567565466544334623554151322511481156324132322347 ...Not satisfiable [902.25ms] 9999999889888897787777667567565466544334623554151322511481156324132322346 ...Not satisfiable [978.97ms] 9999999889888897787777667567565466544334623554151322511481156324132322344 ...Not satisfiable [928.15ms] 9999999889888897787777667567565466544334623554151322511481156324132322343 ...Not satisfiable [1.12s] 9999999889888897787777667567565466544334623554151322511481156324132322342 ...Not satisfiable [1.11s] 9999999889888897787777667567565466544334623554151322511481156324132322341 ...OK [921.18ms] 99999998898888977877776675675654665443346235541513225114811563241323223418 ...Not satisfiable [825.70ms] 99999998898888977877776675675654665443346235541513225114811563241323223417 ...Not satisfiable [862.74ms] 99999998898888977877776675675654665443346235541513225114811563241323223416 ...OK [902.73ms] 999999988988889778777766756756546654433462355415132251148115632413232234168 ...Not satisfiable [887.13ms] 999999988988889778777766756756546654433462355415132251148115632413232234167 ...Not satisfiable [832.57ms] 999999988988889778777766756756546654433462355415132251148115632413232234164 ...Not satisfiable [914.34ms] 999999988988889778777766756756546654433462355415132251148115632413232234163 ...Not satisfiable [953.35ms] 999999988988889778777766756756546654433462355415132251148115632413232234162 ...Not satisfiable [1.25s] 999999988988889778777766756756546654433462355415132251148115632413232234161 ...OK [898.97ms] 9999999889888897787777667567565466544334623554151322511481156324132322341618 ...Not satisfiable [813.14ms] 9999999889888897787777667567565466544334623554151322511481156324132322341617 ...Not satisfiable [841.26ms] 9999999889888897787777667567565466544334623554151322511481156324132322341614 ...Not satisfiable [906.65ms] 9999999889888897787777667567565466544334623554151322511481156324132322341613 ...OK [860.88ms] 99999998898888977877776675675654665443346235541513225114811563241323223416138 ...Not satisfiable [974.10ms] 99999998898888977877776675675654665443346235541513225114811563241323223416137 ...OK [876.19ms] 999999988988889778777766756756546654433462355415132251148115632413232234161378 ...Not satisfiable [803.20ms] 999999988988889778777766756756546654433462355415132251148115632413232234161374 ...OK [859.44ms] 9999999889888897787777667567565466544334623554151322511481156324132322341613748 ...OK [870.45ms] 99999998898888977877776675675654665443346235541513225114811563241323223416137482 ...OK [852.24ms] 999999988988889778777766756756546654433462355415132251148115632413232234161374822 ...OK [851.94ms] Finding solution #1 ...OK [858.83ms] 8 5 3 2 1 7 6 4 9 2 9 1 6 4 8 7 5 3 7 4 6 9 3 5 2 8 1 4 2 5 1 8 9 3 7 6 1 6 8 3 7 4 5 9 2 9 3 7 5 6 2 8 1 4 6 1 4 8 5 3 9 2 7 3 8 2 7 9 1 4 6 5 5 7 9 4 2 6 1 3 8 56 25 70 41 58 27 60 63 14 69 0 57 26 71 12 15 28 61 24 55 40 1 42 59 62 13 64 39 68 43 72 11 2 65 16 29 54 23 10 67 18 45 30 3 80 9 38 19 44 73 66 17 46 31 22 53 36 7 34 49 4 79 76 37 8 51 20 5 74 77 32 47 52 21 6 35 50 33 48 75 78 Finding solution #2 ...OK [901.84ms] 8 2 7 4 1 9 6 3 5 5 9 4 2 6 3 1 8 7 3 1 6 5 8 7 4 2 9 2 6 9 1 3 5 8 7 4 1 4 3 8 7 6 5 9 2 7 8 5 9 4 2 3 1 6 6 7 2 3 5 8 9 4 1 4 5 8 7 9 1 2 6 3 9 3 1 6 2 4 7 5 8 56 69 24 39 54 9 22 37 52 25 0 55 68 23 38 53 8 21 70 57 40 43 10 19 36 51 6 41 26 1 72 67 44 7 20 35 58 71 42 11 18 73 34 5 50 27 12 59 2 45 66 49 74 33 60 15 62 65 30 17 4 77 48 63 28 13 16 3 46 79 32 75 14 61 64 29 80 31 76 47 78 Finding solution #3 ...Not satisfiable [859.49ms]