12 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_12-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29174 | | Parse time: 0.01 s | | Eliminated clauses: 0.25 Mb | | Simplification time: 0.27 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 646 17916 111092 | 100 5 4.0 18.7 | 16.271 % | | 250 | 609 17916 111092 | 248 5 3.5 13.9 | 17.269 % | | 475 | 599 17916 111092 | 468 4 3.4 18.2 | 17.539 % | | 812 | 559 17916 111092 | 796 5 4.1 38.2 | 18.618 % | | 1318 | 511 17916 111092 | 1295 6 5.1 66.2 | 19.914 % | | 2077 | 496 17916 111092 | 2051 7 5.6 79.6 | 20.318 % | | 3216 | 485 17916 111092 | 3186 7 5.8 83.2 | 20.615 % | | 4924 | 480 13376 83195 | 4438 7 6.4 87.7 | 20.750 % | | 5001 | 479 13376 83195 | 4514 7 6.4 87.8 | 20.777 % | < ReduceDB 1 ( 87 restarts, 57 cnfs/res, 50.0% reduced, 31b 202g 442g3) > | 5001 | 479 13376 83195 | 2258 7 5.4 87.8 | 20.777 % | | 7486 | 470 13376 83195 | 4739 7 6.2 89.1 | 21.020 % | | 9738 | 465 12893 80087 | 6952 8 6.5 88.8 | 21.155 % | ==================================================================================== restarts : 159 (353.39 /sec) (61.25 confs/res) conflicts : 9738 (21643 /sec) decisions : 58507 (0.00 % random) (130035 /sec) propagations : 204728 (455021 /sec) conflict literals : 75727 (2.66 % deleted) average of lbd : 6.52 Memory used : 11.00 MB CPU time : 0.449931 s SATISFIABLE 13 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_13-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29170 | | Parse time: 0.01 s | | Eliminated clauses: 0.26 Mb | | Simplification time: 0.26 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 646 17916 111508 | 100 5 4.0 18.7 | 16.271 % | | 250 | 609 17916 111508 | 248 5 3.5 13.9 | 17.269 % | | 475 | 594 17916 111508 | 468 5 3.4 17.4 | 17.674 % | | 812 | 552 17916 111508 | 793 5 4.0 34.2 | 18.808 % | | 1318 | 534 17916 111508 | 1295 6 5.0 63.8 | 19.293 % | | 2077 | 512 17916 111508 | 2050 7 5.6 79.0 | 19.887 % | | 3216 | 492 17916 111508 | 3185 7 6.0 86.0 | 20.426 % | | 4924 | 484 13521 84311 | 4410 8 6.6 90.2 | 20.642 % | | 5003 | 484 13521 84311 | 4489 8 6.6 90.0 | 20.642 % | < ReduceDB 1 ( 86 restarts, 58 cnfs/res, 50.0% reduced, 20b 185g 405g3) > | 5003 | 484 13521 84311 | 2244 7 5.7 90.0 | 20.642 % | | 5145 | 484 13521 84311 | 2386 7 5.7 89.8 | 20.642 % | ==================================================================================== restarts : 86 (247.16 /sec) (59.83 confs/res) conflicts : 5145 (14787 /sec) decisions : 27267 (0.00 % random) (78365 /sec) propagations : 96495 (277327 /sec) conflict literals : 37970 (3.73 % deleted) average of lbd : 5.71 Memory used : 10.00 MB CPU time : 0.347947 s SATISFIABLE 14 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_14-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29166 | | Parse time: 0.01 s | | Eliminated clauses: 0.28 Mb | | Simplification time: 0.29 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 637 18012 113332 | 100 5 4.2 18.2 | 16.406 % | | 250 | 607 18012 113332 | 247 5 3.6 16.1 | 17.215 % | | 475 | 586 18012 113332 | 461 5 3.5 19.1 | 17.782 % | | 812 | 567 18012 113332 | 794 6 4.6 47.8 | 18.295 % | | 1318 | 537 18012 113332 | 1295 7 5.7 64.8 | 19.104 % | | 2077 | 507 18012 113332 | 2047 8 6.1 76.9 | 19.914 % | | 3216 | 506 18012 113332 | 3185 8 6.5 81.7 | 19.941 % | | 4924 | 506 13205 82195 | 4495 9 7.2 86.4 | 19.941 % | | 5002 | 506 13205 82195 | 4573 9 7.2 86.5 | 19.941 % | < ReduceDB 1 ( 88 restarts, 57 cnfs/res, 50.0% reduced, 39b 149g 329g3) > | 5002 | 506 13205 82195 | 2287 8 6.1 86.5 | 19.941 % | | 7486 | 506 13205 82195 | 4771 8 6.8 88.6 | 19.941 % | | 11330 | 505 13075 81383 | 8576 9 7.4 88.0 | 19.968 % | | 15001 | 505 13075 81383 | 12247 10 7.8 86.5 | 19.968 % | < ReduceDB 2 ( 237 restarts, 63 cnfs/res, 50.0% reduced, 73b 384g 1194g3) > | 15001 | 505 13075 81383 | 6126 9 6.6 86.5 | 19.968 % | | 17096 | 505 13075 81383 | 8221 9 7.2 85.5 | 19.968 % | | 25745 | 502 12945 80571 | 16846 11 8.5 82.0 | 20.049 % | | 30001 | 500 12885 80143 | 21101 12 8.9 80.1 | 20.103 % | < ReduceDB 3 ( 437 restarts, 69 cnfs/res, 50.0% reduced, 90b 779g 2232g3) > | 30001 | 500 12885 80143 | 10553 11 7.2 80.1 | 20.103 % | | 38719 | 498 12581 78203 | 19226 13 8.7 77.1 | 20.157 % | | 50001 | 498 12581 78203 | 30508 15 10.0 74.5 | 20.157 % | < ReduceDB 4 ( 718 restarts, 70 cnfs/res, 50.0% reduced, 103b 1403g 3527g3) > | 50001 | 498 12581 78203 | 15257 12 7.6 74.5 | 20.157 % | | 58180 | 498 12581 78203 | 23436 15 9.6 72.6 | 20.157 % | | 75001 | 495 12546 77978 | 40252 19 11.8 69.9 | 20.237 % | < ReduceDB 5 (1126 restarts, 67 cnfs/res, 50.0% reduced, 118b 2273g 4874g3) > | 75001 | 495 12546 77978 | 20135 14 8.2 69.9 | 20.237 % | | 87372 | 454 12546 77978 | 32502 18 10.9 68.2 | 21.344 % | | 105001 | 454 11417 70669 | 49622 22 13.0 66.0 | 21.344 % | < ReduceDB 6 (1613 restarts, 65 cnfs/res, 50.0% reduced, 89b 3036g 5830g3) > | 105001 | 454 11417 70669 | 24811 15 8.8 66.0 | 21.344 % | | 131161 | 445 11290 69822 | 50871 22 12.8 63.8 | 21.587 % | | 140002 | 445 11290 69822 | 59712 23 13.4 63.1 | 21.587 % | < ReduceDB 7 (2099 restarts, 67 cnfs/res, 50.0% reduced, 91b 3974g 7007g3) > | 140002 | 445 11290 69822 | 29861 15 8.7 63.1 | 21.587 % | | 180003 | 445 11290 69822 | 69862 24 13.6 60.7 | 21.587 % | < ReduceDB 8 (2609 restarts, 69 cnfs/res, 48.4% reduced, 93b 4955g 8105g3) > | 180003 | 445 11290 69822 | 33786 16 8.8 60.7 | 21.587 % | | 196845 | 445 11290 69822 | 50628 21 11.8 60.0 | 21.587 % | | 225001 | 445 11290 69822 | 78784 24 13.8 59.0 | 21.587 % | < ReduceDB 9 (3147 restarts, 71 cnfs/res, 45.8% reduced, 94b 5905g 9121g3) > | 225001 | 445 11290 69822 | 36069 15 8.4 59.0 | 21.587 % | | 275002 | 440 11220 69342 | 86008 25 13.5 57.4 | 21.722 % | < ReduceDB 10 (3533 restarts, 78 cnfs/res, 42.1% reduced, 91b 6925g 10038g3) > | 275002 | 440 11220 69342 | 36207 15 7.9 57.4 | 21.722 % | | 295371 | 440 11220 69342 | 56576 21 11.2 56.8 | 21.722 % | | 330003 | 440 11220 69342 | 91208 25 13.5 56.1 | 21.722 % | < ReduceDB 11 (3997 restarts, 83 cnfs/res, 42.0% reduced, 91b 8151g 11253g3) > | 330003 | 440 11220 69342 | 38264 15 7.7 56.1 | 21.722 % | | 390003 | 440 11220 69342 | 98264 25 13.2 54.8 | 21.722 % | < ReduceDB 12 (4377 restarts, 89 cnfs/res, 40.6% reduced, 91b 9443g 12384g3) > | 390003 | 440 11220 69342 | 39859 15 7.4 54.8 | 21.722 % | | 443160 | 439 11130 68802 | 93003 24 12.8 54.0 | 21.749 % | | 455001 | 439 11130 68802 | 104844 25 13.2 53.8 | 21.749 % | < ReduceDB 13 (4787 restarts, 95 cnfs/res, 39.7% reduced, 91b 10587g 13349g3) > | 455001 | 439 11130 68802 | 41670 14 7.0 53.8 | 21.749 % | | 525002 | 439 11130 68802 | 111671 25 13.1 52.9 | 21.749 % | < ReduceDB 14 (5215 restarts, 101 cnfs/res, 40.1% reduced, 91b 11730g 14427g3) > | 525002 | 439 11130 68802 | 44743 14 7.0 52.9 | 21.749 % | | 600002 | 439 11130 68802 | 119743 25 13.1 52.2 | 21.749 % | < ReduceDB 15 (5724 restarts, 105 cnfs/res, 39.3% reduced, 92b 12809g 15601g3) > | 600002 | 439 11130 68802 | 47106 14 6.9 52.2 | 21.749 % | | 664843 | 439 11130 68802 | 111947 24 12.5 51.6 | 21.749 % | | 680004 | 439 11130 68802 | 127108 25 13.0 51.4 | 21.749 % | < ReduceDB 16 (6157 restarts, 110 cnfs/res, 38.1% reduced, 92b 14051g 16844g3) > | 680004 | 439 11130 68802 | 48426 14 6.7 51.4 | 21.749 % | | 765003 | 439 11130 68802 | 133425 25 13.2 50.9 | 21.749 % | < ReduceDB 17 (6727 restarts, 114 cnfs/res, 38.6% reduced, 93b 15235g 17819g3) > | 765003 | 439 11130 68802 | 51488 13 6.5 50.9 | 21.749 % | | 855001 | 439 11130 68802 | 141486 25 13.1 50.2 | 21.749 % | < ReduceDB 18 (7255 restarts, 118 cnfs/res, 38.1% reduced, 93b 16408g 18799g3) > | 855001 | 439 11130 68802 | 53974 13 6.4 50.2 | 21.749 % | | 950001 | 439 11130 68802 | 148974 24 12.9 49.7 | 21.749 % | < ReduceDB 19 (7834 restarts, 121 cnfs/res, 37.0% reduced, 93b 17521g 19829g3) > | 950001 | 439 11130 68802 | 55147 13 5.9 49.7 | 21.749 % | | 997368 | 439 11130 68802 | 102514 21 10.8 49.4 | 21.749 % | | 1050002 | 439 11130 68802 | 155148 25 12.7 49.1 | 21.749 % | < ReduceDB 20 (8436 restarts, 124 cnfs/res, 37.1% reduced, 96b 18553g 20773g3) > | 1050002 | 439 11130 68802 | 57484 13 5.9 49.1 | 21.749 % | | 1155003 | 439 11130 68802 | 162485 25 12.7 48.5 | 21.749 % | < ReduceDB 21 (9030 restarts, 128 cnfs/res, 37.6% reduced, 97b 19756g 21814g3) > | 1155003 | 439 11130 68802 | 61100 12 5.9 48.5 | 21.749 % | | 1265001 | 439 11130 68802 | 171098 25 12.7 48.0 | 21.749 % | < ReduceDB 22 (9601 restarts, 132 cnfs/res, 36.7% reduced, 99b 20801g 22883g3) > | 1265001 | 439 11130 68802 | 62878 13 5.8 48.0 | 21.749 % | | 1380001 | 439 11130 68802 | 177878 24 12.6 47.5 | 21.749 % | < ReduceDB 23 (10208 restarts, 135 cnfs/res, 35.7% reduced, 100b 21976g 23830g3) > | 1380001 | 439 11130 68802 | 63452 12 5.3 47.5 | 21.749 % | | 1496156 | 439 11130 68802 | 179607 24 12.3 47.0 | 21.749 % | | 1500002 | 439 11130 68802 | 183453 24 12.4 47.0 | 21.749 % | < ReduceDB 24 (10862 restarts, 138 cnfs/res, 36.5% reduced, 101b 23119g 24598g3) > | 1500002 | 439 11130 68802 | 67018 12 5.6 47.0 | 21.749 % | | 1625001 | 439 11130 68802 | 192017 24 12.6 46.5 | 21.749 % | < ReduceDB 25 (11517 restarts, 141 cnfs/res, 34.8% reduced, 101b 24375g 25501g3) > | 1625001 | 439 11130 68802 | 66872 13 5.3 46.5 | 21.749 % | | 1755001 | 439 11130 68802 | 196872 25 12.4 46.1 | 21.749 % | < ReduceDB 26 (12197 restarts, 144 cnfs/res, 35.9% reduced, 101b 25394g 26224g3) > | 1755001 | 439 11130 68802 | 70757 12 5.6 46.1 | 21.749 % | | 1890001 | 439 11130 68802 | 205757 24 12.5 45.7 | 21.749 % | < ReduceDB 27 (12944 restarts, 146 cnfs/res, 35.5% reduced, 101b 26444g 27162g3) > | 1890001 | 439 11130 68802 | 72995 12 5.4 45.7 | 21.749 % | | 2030001 | 439 11130 68802 | 212995 24 12.4 45.4 | 21.749 % | < ReduceDB 28 (13639 restarts, 149 cnfs/res, 34.7% reduced, 101b 27540g 28327g3) > | 2030001 | 439 11130 68802 | 73916 12 5.1 45.4 | 21.749 % | | 2175001 | 439 11130 68802 | 218916 24 12.3 44.9 | 21.749 % | < ReduceDB 29 (14344 restarts, 152 cnfs/res, 34.6% reduced, 103b 28568g 29027g3) > | 2175001 | 439 11130 68802 | 75676 12 5.1 44.9 | 21.749 % | | 2244338 | 439 11130 68802 | 145013 20 10.1 44.7 | 21.749 % | | 2325002 | 439 11130 68802 | 225677 24 12.3 44.5 | 21.749 % | < ReduceDB 30 (15053 restarts, 154 cnfs/res, 34.0% reduced, 103b 29745g 29773g3) > | 2325002 | 439 11130 68802 | 76785 12 5.0 44.5 | 21.749 % | | 2480003 | 439 11130 68802 | 231786 24 12.7 44.3 | 21.749 % | < ReduceDB 31 (16072 restarts, 154 cnfs/res, 34.4% reduced, 103b 30820g 30589g3) > | 2480003 | 439 11130 68802 | 79664 12 5.1 44.3 | 21.749 % | | 2640001 | 439 11130 68802 | 239662 24 12.7 44.2 | 21.749 % | < ReduceDB 32 (17261 restarts, 153 cnfs/res, 34.6% reduced, 104b 31820g 31551g3) > | 2640001 | 439 11130 68802 | 82996 12 5.1 44.2 | 21.749 % | | 2805001 | 439 11130 68802 | 247996 24 12.5 43.9 | 21.749 % | < ReduceDB 33 (18252 restarts, 154 cnfs/res, 34.1% reduced, 104b 32912g 32725g3) > | 2805001 | 439 11130 68802 | 84483 12 5.0 43.9 | 21.749 % | | 2975002 | 439 11130 68802 | 254484 24 12.5 43.6 | 21.749 % | < ReduceDB 34 (19292 restarts, 154 cnfs/res, 33.3% reduced, 105b 34180g 33363g3) > | 2975002 | 439 11130 68802 | 84708 11 4.8 43.6 | 21.749 % | | 3150004 | 439 11130 68802 | 259710 24 12.4 43.4 | 21.749 % | < ReduceDB 35 (20427 restarts, 154 cnfs/res, 33.9% reduced, 105b 35367g 34273g3) > | 3150004 | 439 11130 68802 | 88145 11 4.9 43.4 | 21.749 % | | 3330001 | 439 11130 68802 | 268142 24 12.7 43.2 | 21.749 % | < ReduceDB 36 (21772 restarts, 153 cnfs/res, 34.5% reduced, 106b 36693g 35433g3) > | 3330001 | 439 11130 68802 | 92510 11 4.9 43.2 | 21.749 % | | 3366612 | 439 11130 68802 | 129121 16 8.1 43.2 | 21.749 % | | 3515001 | 439 11130 68802 | 277510 24 12.8 43.0 | 21.749 % | < ReduceDB 37 (23042 restarts, 153 cnfs/res, 34.0% reduced, 108b 37836g 36372g3) > | 3515001 | 439 11130 68802 | 94389 11 4.9 43.0 | 21.749 % | | 3705002 | 439 11130 68802 | 284390 24 12.5 42.8 | 21.749 % | < ReduceDB 38 (24247 restarts, 153 cnfs/res, 33.9% reduced, 109b 38782g 37403g3) > | 3705002 | 439 11130 68802 | 96457 11 4.8 42.8 | 21.749 % | | 3900002 | 439 11130 68802 | 291457 24 12.3 42.5 | 21.749 % | < ReduceDB 39 (25382 restarts, 154 cnfs/res, 33.7% reduced, 110b 40038g 38395g3) > | 3900002 | 439 11130 68802 | 98244 11 4.6 42.5 | 21.749 % | | 4100002 | 439 11130 68802 | 298244 24 12.6 42.4 | 21.749 % | < ReduceDB 40 (26879 restarts, 153 cnfs/res, 33.5% reduced, 110b 41195g 39561g3) > | 4100002 | 439 11130 68802 | 99811 11 4.7 42.4 | 21.749 % | | 4305001 | 434 11076 68454 | 304801 24 12.5 42.3 | 21.883 % | < ReduceDB 41 (28342 restarts, 152 cnfs/res, 33.7% reduced, 110b 42330g 40504g3) > | 4305001 | 434 11076 68454 | 102751 11 4.6 42.3 | 21.883 % | | 4515002 | 434 11076 68454 | 312752 24 12.3 42.1 | 21.883 % | < ReduceDB 42 (29731 restarts, 152 cnfs/res, 32.9% reduced, 110b 43782g 41603g3) > | 4515002 | 434 11076 68454 | 102996 11 4.3 42.1 | 21.883 % | | 4730004 | 434 11076 68454 | 317998 24 12.3 41.9 | 21.883 % | < ReduceDB 43 (30969 restarts, 153 cnfs/res, 33.2% reduced, 111b 44923g 42250g3) > | 4730004 | 434 11076 68454 | 105528 11 4.4 41.9 | 21.883 % | | 4950001 | 434 11076 68454 | 325525 24 12.5 41.7 | 21.883 % | < ReduceDB 44 (32468 restarts, 152 cnfs/res, 33.4% reduced, 111b 46172g 43399g3) > | 4950001 | 434 11076 68454 | 108606 11 4.4 41.7 | 21.883 % | | 5050023 | 434 11076 68454 | 208628 20 10.2 41.7 | 21.883 % | | 5175001 | 434 11076 68454 | 333606 24 12.2 41.6 | 21.883 % | < ReduceDB 45 (33811 restarts, 153 cnfs/res, 32.4% reduced, 111b 47269g 44317g3) > | 5175001 | 434 11076 68454 | 107937 11 4.1 41.6 | 21.883 % | | 5405001 | 434 11076 68454 | 337937 24 11.6 41.3 | 21.883 % | < ReduceDB 46 (35079 restarts, 154 cnfs/res, 32.7% reduced, 111b 48475g 45199g3) > | 5405001 | 434 11076 68454 | 110526 11 4.2 41.3 | 21.883 % | | 5640002 | 434 11076 68454 | 345527 24 12.4 41.2 | 21.883 % | < ReduceDB 47 (36769 restarts, 153 cnfs/res, 33.0% reduced, 111b 49540g 46101g3) > | 5640002 | 434 11076 68454 | 114102 11 4.2 41.2 | 21.883 % | | 5880002 | 434 11076 68454 | 354102 24 12.4 41.1 | 21.883 % | < ReduceDB 48 (38620 restarts, 152 cnfs/res, 32.5% reduced, 111b 50793g 47263g3) > | 5880002 | 434 11076 68454 | 115241 11 4.2 41.1 | 21.883 % | | 6125001 | 434 11076 68454 | 360240 24 12.1 41.0 | 21.883 % | < ReduceDB 49 (40099 restarts, 153 cnfs/res, 32.9% reduced, 112b 51902g 48035g3) > | 6125001 | 434 11076 68454 | 118474 11 4.1 41.0 | 21.883 % | | 6375002 | 434 11076 68454 | 368475 24 12.2 40.9 | 21.883 % | < ReduceDB 50 (41804 restarts, 152 cnfs/res, 33.0% reduced, 112b 53067g 48960g3) > | 6375002 | 434 11076 68454 | 121452 11 4.3 40.9 | 21.883 % | | 6630002 | 434 11076 68454 | 376452 24 12.6 40.8 | 21.883 % | < ReduceDB 51 (43718 restarts, 152 cnfs/res, 32.7% reduced, 112b 54237g 49990g3) > | 6630002 | 434 11076 68454 | 122920 11 4.1 40.8 | 21.883 % | | 6890003 | 434 11076 68454 | 382921 24 12.4 40.6 | 21.883 % | < ReduceDB 52 (45460 restarts, 152 cnfs/res, 32.4% reduced, 113b 55359g 51318g3) > | 6890003 | 434 11076 68454 | 124096 11 4.2 40.6 | 21.883 % | | 7155003 | 434 11076 68454 | 389096 24 12.3 40.5 | 21.883 % | < ReduceDB 53 (47279 restarts, 151 cnfs/res, 32.8% reduced, 113b 56520g 52393g3) > | 7155003 | 434 11076 68454 | 127704 11 4.1 40.5 | 21.883 % | | 7425001 | 434 11076 68454 | 397702 24 12.0 40.4 | 21.883 % | < ReduceDB 54 (49095 restarts, 151 cnfs/res, 32.7% reduced, 113b 57694g 53710g3) > | 7425001 | 434 11076 68454 | 129978 10 4.0 40.4 | 21.883 % | | 7575139 | 434 11076 68454 | 280116 21 10.2 40.3 | 21.883 % | | 7700001 | 434 11076 68454 | 404978 24 12.1 40.3 | 21.883 % | < ReduceDB 55 (50745 restarts, 152 cnfs/res, 32.8% reduced, 113b 58875g 54992g3) > | 7700001 | 434 11076 68454 | 132849 10 4.1 40.3 | 21.883 % | | 7980004 | 434 11076 68454 | 412852 24 12.4 40.2 | 21.883 % | < ReduceDB 56 (52920 restarts, 151 cnfs/res, 33.0% reduced, 114b 60291g 56428g3) > | 7980004 | 434 11076 68454 | 136169 10 4.1 40.2 | 21.883 % | | 8265001 | 434 11076 68454 | 421166 24 12.5 40.0 | 21.883 % | < ReduceDB 57 (54982 restarts, 150 cnfs/res, 33.0% reduced, 115b 61547g 57648g3) > | 8265001 | 434 11076 68454 | 138935 10 4.1 40.0 | 21.883 % | | 8555001 | 434 11076 68454 | 428935 24 12.3 39.9 | 21.883 % | < ReduceDB 58 (56870 restarts, 150 cnfs/res, 32.3% reduced, 115b 62803g 58935g3) > | 8555001 | 434 11076 68454 | 138603 11 3.9 39.9 | 21.883 % | | 8850004 | 434 11076 68454 | 433606 24 12.3 39.8 | 21.883 % | < ReduceDB 59 (58994 restarts, 150 cnfs/res, 32.9% reduced, 115b 64203g 59895g3) > | 8850004 | 434 11076 68454 | 142529 10 3.9 39.8 | 21.883 % | | 9150001 | 434 11076 68454 | 442526 24 12.4 39.8 | 21.884 % | < ReduceDB 60 (61203 restarts, 150 cnfs/res, 32.9% reduced, 115b 65429g 61101g3) > | 9150001 | 434 11076 68454 | 145703 11 4.0 39.8 | 21.884 % | | 9455001 | 434 11076 68454 | 450703 24 11.9 39.6 | 21.883 % | < ReduceDB 61 (62962 restarts, 150 cnfs/res, 33.0% reduced, 115b 66842g 62650g3) > | 9455001 | 434 11076 68454 | 148641 10 4.0 39.6 | 21.883 % | | 9765001 | 434 11076 68454 | 458641 24 12.2 39.5 | 21.883 % | < ReduceDB 62 (65265 restarts, 150 cnfs/res, 32.4% reduced, 115b 68096g 63751g3) > | 9765001 | 434 11076 68454 | 148818 10 3.7 39.5 | 21.883 % | | 9864665 | 434 11076 68454 | 248482 18 8.6 39.5 | 21.883 % | ==================================================================================== restarts : 65898 (22.31 /sec) (149.70 confs/res) conflicts : 9864665 (3340 /sec) decisions : 16086934 (0.00 % random) (5447 /sec) propagations : 263410968 (89189 /sec) conflict literals : 297478545 (13.67 % deleted) average of lbd : 8.65 Memory used : 129.00 MB CPU time : 2953.41 s INDETERMINATE 15 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_15-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29168 | | Parse time: 0.01 s | | Eliminated clauses: 0.29 Mb | | Simplification time: 0.18 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 637 17884 113300 | 0 nan nan nan | 16.433 % | ==================================================================================== restarts : 1 (5.13 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 609 (3124 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 11.00 MB CPU time : 0.19497 s INDETERMINATE 16 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_16-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29171 | | Parse time: 0.01 s | | Eliminated clauses: 0.25 Mb | | Simplification time: 0.16 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 658 18010 112886 | 0 nan nan nan | 16.055 % | ==================================================================================== restarts : 1 (5.95 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 595 (3542 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 11.00 MB CPU time : 0.167974 s INDETERMINATE 17 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_17-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29166 | | Parse time: 0.01 s | | Eliminated clauses: 0.29 Mb | | Simplification time: 0.18 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 635 16692 103434 | 0 nan nan nan | 15.920 % | ==================================================================================== restarts : 1 (5.16 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 590 (3042 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 10.00 MB CPU time : 0.19397 s INDETERMINATE 18 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_18-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29166 | | Parse time: 0.01 s | | Eliminated clauses: 0.29 Mb | | Simplification time: 0.18 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 642 16959 105468 | 0 nan nan nan | 15.623 % | ==================================================================================== restarts : 1 (5.26 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 579 (3048 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 11.00 MB CPU time : 0.189971 s INDETERMINATE 19 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_19-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29178 | | Parse time: 0.01 s | | Eliminated clauses: 0.33 Mb | | Simplification time: 0.21 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 606 16568 103305 | 98 5 4.0 19.8 | 16.109 % | | 250 | 605 16568 103305 | 247 5 3.5 16.7 | 16.136 % | | 475 | 591 16568 103305 | 466 5 4.0 26.7 | 16.514 % | | 506 | 591 16568 103305 | 497 5 4.1 32.4 | 16.514 % | ==================================================================================== restarts : 7 (31.54 /sec) (72.29 confs/res) conflicts : 506 (2280 /sec) decisions : 1877 (0.00 % random) (8456 /sec) propagations : 13255 (59716 /sec) conflict literals : 2708 (15.35 % deleted) average of lbd : 4.11 Memory used : 11.00 MB CPU time : 0.221966 s INDETERMINATE 20 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_20-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29185 | | Parse time: 0.01 s | | Eliminated clauses: 0.32 Mb | | Simplification time: 0.20 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 638 16764 105012 | 0 nan nan nan | 15.246 % | ==================================================================================== restarts : 1 (4.61 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 565 (2604 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 11.00 MB CPU time : 0.216967 s INDETERMINATE 21 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_21-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29181 | | Parse time: 0.01 s | | Eliminated clauses: 0.28 Mb | | Simplification time: 0.16 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 656 16910 105187 | 0 nan nan nan | 15.326 % | ==================================================================================== restarts : 1 (6.06 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 568 (3443 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 10.00 MB CPU time : 0.164974 s INDETERMINATE 22 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_22-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29173 | | Parse time: 0.01 s | | Eliminated clauses: 0.27 Mb | | Simplification time: 0.16 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 653 16659 103664 | 0 nan nan nan | 15.434 % | ==================================================================================== restarts : 1 (5.78 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 572 (3307 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 11.00 MB CPU time : 0.172973 s INDETERMINATE 23 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_23-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29186 | | Parse time: 0.01 s | | Eliminated clauses: 0.30 Mb | | Simplification time: 0.16 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 658 18379 117275 | 0 nan nan nan | 14.841 % | ==================================================================================== restarts : 1 (5.75 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 550 (3161 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 11.00 MB CPU time : 0.173973 s INDETERMINATE 24 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_24-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29183 | | Parse time: 0.01 s | | Eliminated clauses: 0.29 Mb | | Simplification time: 0.16 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 664 17322 108797 | 0 nan nan nan | 14.895 % | ==================================================================================== restarts : 1 (5.92 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 552 (3267 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 11.00 MB CPU time : 0.168974 s INDETERMINATE 25 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_25-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29183 | | Parse time: 0.01 s | | Eliminated clauses: 0.30 Mb | | Simplification time: 0.16 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 641 16348 102356 | 0 nan nan nan | 15.246 % | ==================================================================================== restarts : 1 (5.85 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 565 (3305 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 10.00 MB CPU time : 0.170974 s INDETERMINATE 26 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_26-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29182 | | Parse time: 0.01 s | | Eliminated clauses: 0.30 Mb | | Simplification time: 0.18 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 640 16092 100756 | 100 5 3.8 18.1 | 15.138 % | | 250 | 611 16092 100756 | 242 5 3.6 18.5 | 15.920 % | | 413 | 608 16092 100756 | 403 5 3.9 28.6 | 16.001 % | ==================================================================================== restarts : 5 (26.18 /sec) (82.60 confs/res) conflicts : 413 (2163 /sec) decisions : 1455 (0.00 % random) (7619 /sec) propagations : 9939 (52045 /sec) conflict literals : 2019 (19.82 % deleted) average of lbd : 3.87 Memory used : 10.00 MB CPU time : 0.19097 s INDETERMINATE 27 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_27-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29186 | | Parse time: 0.01 s | | Eliminated clauses: 0.32 Mb | | Simplification time: 0.16 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 648 16515 104132 | 0 nan nan nan | 15.246 % | ==================================================================================== restarts : 1 (5.81 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 565 (3285 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 10.00 MB CPU time : 0.171973 s INDETERMINATE 28 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_28-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29196 | | Parse time: 0.01 s | | Eliminated clauses: 0.31 Mb | | Simplification time: 0.17 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 640 15959 99966 | 0 nan nan nan | 14.706 % | ==================================================================================== restarts : 1 (5.68 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 545 (3097 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 11.00 MB CPU time : 0.175973 s INDETERMINATE 29 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_29-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29201 | | Parse time: 0.01 s | | Eliminated clauses: 0.33 Mb | | Simplification time: 0.16 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 640 15831 99454 | 0 nan nan nan | 14.301 % | ==================================================================================== restarts : 1 (5.92 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 530 (3137 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 11.00 MB CPU time : 0.168974 s INDETERMINATE 30 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_30-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29189 | | Parse time: 0.01 s | | Eliminated clauses: 0.30 Mb | | Simplification time: 0.16 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 636 16471 104030 | 0 nan nan nan | 15.461 % | ==================================================================================== restarts : 1 (5.95 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 573 (3411 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 11.00 MB CPU time : 0.167974 s INDETERMINATE 31 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_31-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29199 | | Parse time: 0.01 s | | Eliminated clauses: 0.32 Mb | | Simplification time: 0.17 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 636 16183 103102 | 0 nan nan nan | 15.542 % | ==================================================================================== restarts : 1 (5.62 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 576 (3236 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 10.00 MB CPU time : 0.177972 s INDETERMINATE 32 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_32-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29205 | | Parse time: 0.01 s | | Eliminated clauses: 0.28 Mb | | Simplification time: 0.16 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 636 16407 103326 | 0 nan nan nan | 15.893 % | ==================================================================================== restarts : 1 (5.85 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 589 (3445 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 11.00 MB CPU time : 0.170974 s INDETERMINATE 33 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_33-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29237 | | Parse time: 0.01 s | | Eliminated clauses: 0.25 Mb | | Simplification time: 0.16 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 664 19575 125374 | 0 nan nan nan | 13.815 % | ==================================================================================== restarts : 1 (5.99 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 512 (3066 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 11.00 MB CPU time : 0.166974 s INDETERMINATE