16 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_16-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 15198 | | Parse time: 0.01 s | | Eliminated clauses: 0.17 Mb | | Simplification time: 0.07 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 2404 8095 37245 | 100 61 58.2 2245.8 | 9.201 % | | 250 | 2404 8095 37245 | 250 44 40.4 1472.5 | 9.201 % | | 475 | 2404 8095 37245 | 475 35 29.0 936.8 | 9.201 % | | 812 | 2404 8095 37245 | 812 33 25.4 659.5 | 9.201 % | | 1246 | 2404 8095 37245 | 1246 31 23.7 499.3 | 9.201 % | ==================================================================================== restarts : 3 (29.42 /sec) (415.33 confs/res) conflicts : 1246 (12218 /sec) decisions : 12530 (0.00 % random) (122862 /sec) propagations : 88839 (871107 /sec) conflict literals : 38879 (10.39 % deleted) average of lbd : 23.72 Memory used : 8.00 MB CPU time : 0.101984 s SATISFIABLE 17 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_17-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 15193 | | Parse time: 0.01 s | | Eliminated clauses: 0.16 Mb | | Simplification time: 0.06 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 2752 8939 40191 | 100 62 59.1 2250.1 | 9.563 % | | 250 | 2752 8939 40191 | 250 62 58.5 1672.7 | 9.563 % | | 475 | 2752 8939 40191 | 475 45 39.2 1068.7 | 9.563 % | | 812 | 2752 8939 40191 | 812 40 33.4 728.0 | 9.563 % | | 1318 | 2752 8939 40191 | 1318 40 31.9 527.9 | 9.563 % | | 2077 | 2752 8939 40191 | 2077 40 31.6 409.2 | 9.563 % | | 3216 | 2752 8939 40191 | 3216 38 29.3 323.3 | 9.563 % | | 4924 | 2752 8939 40191 | 4924 35 27.2 244.2 | 9.563 % | | 5001 | 2752 8939 40191 | 5001 35 27.2 241.5 | 9.563 % | < ReduceDB 1 ( 3 restarts, 1667 cnfs/res, 50.2% reduced, 0b 8g 43g3) > | 5001 | 2752 8939 40191 | 2509 29 21.1 241.5 | 9.563 % | | 7486 | 2752 8939 40191 | 4994 29 21.7 187.4 | 9.563 % | | 11330 | 2752 8939 40191 | 8838 29 20.9 148.2 | 9.563 % | | 15001 | 2752 8939 40191 | 12509 29 20.1 128.4 | 9.563 % | < ReduceDB 2 ( 11 restarts, 1364 cnfs/res, 50.0% reduced, 0b 34g 149g3) > | 15001 | 2752 8939 40191 | 6256 27 17.6 128.4 | 9.563 % | | 17096 | 2752 8939 40191 | 8351 27 17.1 120.8 | 9.563 % | | 25745 | 2752 8939 40191 | 17000 26 17.4 115.6 | 9.563 % | | 30001 | 2752 8939 40191 | 21256 25 17.4 113.3 | 9.563 % | < ReduceDB 3 ( 113 restarts, 265 cnfs/res, 50.0% reduced, 0b 78g 417g3) > | 30001 | 2752 8939 40191 | 10628 22 16.4 113.3 | 9.563 % | | 38719 | 2752 8939 40191 | 19346 22 16.5 114.2 | 9.563 % | | 50001 | 2752 8939 40191 | 30628 22 16.7 113.5 | 9.563 % | < ReduceDB 4 ( 342 restarts, 146 cnfs/res, 43.5% reduced, 0b 155g 741g3) > | 50001 | 2752 8939 40191 | 13316 20 14.8 113.5 | 9.563 % | | 58180 | 2752 8939 40191 | 21495 21 15.6 113.3 | 9.563 % | | 75001 | 2752 8939 40191 | 38316 22 16.2 111.9 | 9.563 % | < ReduceDB 5 ( 596 restarts, 126 cnfs/res, 38.7% reduced, 0b 276g 1263g3) > | 75001 | 2752 8939 40191 | 14831 20 14.0 111.9 | 9.563 % | | 87372 | 2752 8939 40191 | 27202 21 15.2 111.6 | 9.563 % | | 105001 | 2752 8939 40191 | 44831 22 16.0 110.1 | 9.563 % | < ReduceDB 6 ( 932 restarts, 113 cnfs/res, 35.8% reduced, 0b 393g 1705g3) > | 105001 | 2752 8939 40191 | 16034 19 13.6 110.1 | 9.563 % | | 131161 | 2752 8939 40191 | 42194 21 15.6 109.5 | 9.563 % | | 140001 | 2752 8939 40191 | 51034 22 15.9 108.7 | 9.563 % | < ReduceDB 7 (1349 restarts, 104 cnfs/res, 33.4% reduced, 1b 525g 2181g3) > | 140001 | 2752 8939 40191 | 17042 19 13.2 108.7 | 9.563 % | | 180001 | 2752 8939 40191 | 57042 22 15.7 107.1 | 9.563 % | < ReduceDB 8 (1796 restarts, 100 cnfs/res, 31.8% reduced, 1b 679g 2733g3) > | 180001 | 2752 8939 40191 | 18117 18 12.7 107.1 | 9.563 % | | 196845 | 2752 8939 40191 | 34961 20 14.5 106.7 | 9.563 % | | 225001 | 2752 8939 40191 | 63117 22 15.7 106.0 | 9.563 % | < ReduceDB 9 (2320 restarts, 97 cnfs/res, 30.1% reduced, 4b 904g 3276g3) > | 225001 | 2752 8939 40191 | 19012 18 12.3 106.0 | 9.563 % | | 275002 | 2752 8939 40191 | 69013 22 15.7 104.0 | 9.563 % | < ReduceDB 10 (2814 restarts, 98 cnfs/res, 28.8% reduced, 5b 1121g 3871g3) > | 275002 | 2752 8939 40191 | 19884 18 11.7 104.0 | 9.563 % | | 295371 | 2752 8939 40191 | 40253 20 14.3 103.3 | 9.563 % | | 330001 | 2752 8939 40191 | 74883 22 15.7 102.1 | 9.563 % | < ReduceDB 11 (3362 restarts, 98 cnfs/res, 27.9% reduced, 6b 1363g 4422g3) > | 330001 | 2752 8939 40191 | 20880 18 11.6 102.1 | 9.563 % | | 390002 | 2752 8939 40191 | 80881 22 15.8 100.4 | 9.563 % | < ReduceDB 12 (3958 restarts, 99 cnfs/res, 27.2% reduced, 6b 1617g 5036g3) > | 390002 | 2752 8939 40191 | 21996 17 11.3 100.4 | 9.563 % | | 443160 | 2752 8939 40191 | 75154 22 15.2 98.7 | 9.563 % | | 455001 | 2752 8939 40191 | 86995 22 15.5 98.4 | 9.563 % | < ReduceDB 13 (4563 restarts, 100 cnfs/res, 26.5% reduced, 6b 1903g 5616g3) > | 455001 | 2752 8939 40191 | 23024 17 11.1 98.4 | 9.563 % | | 525002 | 2752 8939 40191 | 93025 22 15.5 96.8 | 9.563 % | < ReduceDB 14 (5207 restarts, 101 cnfs/res, 25.6% reduced, 8b 2198g 6132g3) > | 525002 | 2752 8939 40191 | 23831 18 10.6 96.8 | 9.563 % | | 600001 | 2752 8939 40191 | 98830 22 15.6 94.9 | 9.563 % | < ReduceDB 15 (5823 restarts, 103 cnfs/res, 25.0% reduced, 8b 2479g 6611g3) > | 600001 | 2752 8939 40191 | 24706 17 10.6 94.9 | 9.563 % | | 664843 | 2752 8939 40191 | 89548 22 15.3 93.7 | 9.563 % | | 680002 | 2752 8939 40191 | 104707 22 15.6 93.4 | 9.563 % | < ReduceDB 16 (6538 restarts, 104 cnfs/res, 25.0% reduced, 9b 2741g 6999g3) > | 680002 | 2752 8939 40191 | 26175 17 10.5 93.4 | 9.563 % | | 765001 | 2752 8939 40191 | 111174 22 15.7 91.7 | 9.563 % | < ReduceDB 17 (7195 restarts, 106 cnfs/res, 25.0% reduced, 9b 3032g 7431g3) > | 765001 | 2752 8939 40191 | 27792 17 10.6 91.7 | 9.563 % | | 855002 | 2752 8939 40191 | 117793 22 15.7 90.3 | 9.563 % | < ReduceDB 18 (7995 restarts, 107 cnfs/res, 25.0% reduced, 9b 3269g 7809g3) > | 855002 | 2752 8939 40191 | 29447 17 10.3 90.3 | 9.563 % | | 950001 | 2752 8939 40191 | 124446 22 15.5 88.8 | 9.563 % | < ReduceDB 19 (8739 restarts, 109 cnfs/res, 25.0% reduced, 9b 3554g 8288g3) > | 950001 | 2752 8939 40191 | 31110 17 10.1 88.8 | 9.563 % | | 997368 | 2752 8939 40191 | 78477 21 14.4 88.0 | 9.563 % | | 1050001 | 2752 8939 40191 | 131110 22 15.6 87.4 | 9.563 % | < ReduceDB 20 (9520 restarts, 110 cnfs/res, 25.0% reduced, 9b 3862g 8791g3) > | 1050001 | 2752 8939 40191 | 32776 17 10.4 87.4 | 9.563 % | | 1155001 | 2752 8939 40191 | 137776 22 15.6 86.0 | 9.563 % | < ReduceDB 21 (10270 restarts, 112 cnfs/res, 25.0% reduced, 9b 4165g 9343g3) > | 1155001 | 2752 8939 40191 | 34443 17 10.3 86.0 | 9.563 % | | 1265002 | 2752 8939 40191 | 144444 23 15.4 84.1 | 9.563 % | < ReduceDB 22 (10881 restarts, 116 cnfs/res, 25.0% reduced, 9b 4476g 9963g3) > | 1265002 | 2752 8939 40191 | 36110 17 10.2 84.1 | 9.563 % | | 1380001 | 2752 8939 40191 | 151109 22 15.4 83.0 | 9.563 % | < ReduceDB 23 (11755 restarts, 117 cnfs/res, 25.0% reduced, 9b 4723g 10483g3) > | 1380001 | 2752 8939 40191 | 37776 18 9.7 83.0 | 9.563 % | | 1496156 | 2752 8939 40191 | 153931 22 15.3 82.0 | 9.563 % | | 1500003 | 2752 8939 40191 | 157778 22 15.3 82.0 | 9.563 % | < ReduceDB 24 (12683 restarts, 118 cnfs/res, 25.0% reduced, 9b 5086g 11086g3) > | 1500003 | 2752 8939 40191 | 39443 17 10.0 82.0 | 9.563 % | | 1625002 | 2752 8939 40191 | 164442 22 15.5 81.1 | 9.563 % | < ReduceDB 25 (13649 restarts, 119 cnfs/res, 25.0% reduced, 9b 5401g 11723g3) > | 1625002 | 2752 8939 40191 | 41109 17 10.0 81.1 | 9.563 % | | 1755001 | 2752 8939 40191 | 171108 22 15.4 80.2 | 9.563 % | < ReduceDB 26 (14677 restarts, 120 cnfs/res, 25.0% reduced, 9b 5623g 12183g3) > | 1755001 | 2752 8939 40191 | 42776 17 9.9 80.2 | 9.563 % | | 1890001 | 2752 8939 40191 | 177776 23 15.2 79.0 | 9.563 % | < ReduceDB 27 (15484 restarts, 122 cnfs/res, 25.0% reduced, 9b 5915g 12751g3) > | 1890001 | 2752 8939 40191 | 44443 17 10.0 79.0 | 9.563 % | | 2030001 | 2752 8939 40191 | 184443 22 15.3 78.2 | 9.563 % | < ReduceDB 28 (16510 restarts, 123 cnfs/res, 25.0% reduced, 9b 6204g 13374g3) > | 2030001 | 2752 8939 40191 | 46109 17 9.8 78.2 | 9.563 % | | 2175002 | 2752 8939 40191 | 191110 22 15.3 77.3 | 9.563 % | < ReduceDB 29 (17427 restarts, 125 cnfs/res, 25.0% reduced, 9b 6553g 13983g3) > | 2175002 | 2752 8939 40191 | 47776 17 9.8 77.3 | 9.563 % | | 2244338 | 2752 8939 40191 | 117112 21 14.0 77.0 | 9.563 % | | 2325002 | 2752 8939 40191 | 197776 23 15.1 76.5 | 9.563 % | < ReduceDB 30 (18481 restarts, 126 cnfs/res, 25.0% reduced, 9b 6793g 14541g3) > | 2325002 | 2752 8939 40191 | 49443 18 9.6 76.5 | 9.563 % | | 2480003 | 2752 8939 40191 | 204444 22 15.2 75.7 | 9.563 % | < ReduceDB 31 (19575 restarts, 127 cnfs/res, 25.0% reduced, 9b 7091g 15115g3) > | 2480003 | 2752 8939 40191 | 51110 17 9.8 75.7 | 9.563 % | | 2640002 | 2752 8939 40191 | 211109 22 15.5 75.0 | 9.563 % | < ReduceDB 32 (20805 restarts, 127 cnfs/res, 25.0% reduced, 9b 7443g 15625g3) > | 2640002 | 2752 8939 40191 | 52776 17 9.7 75.0 | 9.563 % | | 2805001 | 2752 8939 40191 | 217775 22 15.1 74.2 | 9.563 % | < ReduceDB 33 (21804 restarts, 129 cnfs/res, 25.0% reduced, 9b 7761g 16145g3) > | 2805001 | 2752 8939 40191 | 54442 17 9.7 74.2 | 9.563 % | | 2975001 | 2752 8939 40191 | 224442 22 15.2 73.6 | 9.563 % | < ReduceDB 34 (22959 restarts, 130 cnfs/res, 25.0% reduced, 9b 8118g 16864g3) > | 2975001 | 2752 8939 40191 | 56109 17 9.2 73.6 | 9.563 % | | 3150001 | 2752 8939 40191 | 231109 22 15.1 72.9 | 9.563 % | < ReduceDB 35 (24214 restarts, 130 cnfs/res, 25.0% reduced, 9b 8472g 17456g3) > | 3150001 | 2752 8939 40191 | 57776 17 9.5 72.9 | 9.563 % | | 3330002 | 2752 8939 40191 | 237777 22 15.0 72.2 | 9.563 % | < ReduceDB 36 (25260 restarts, 132 cnfs/res, 25.0% reduced, 9b 8753g 18053g3) > | 3330002 | 2752 8939 40191 | 59443 17 9.5 72.2 | 9.563 % | | 3366612 | 2752 8939 40191 | 96053 19 12.2 72.0 | 9.563 % | | 3515001 | 2752 8939 40191 | 244442 22 15.2 71.6 | 9.563 % | < ReduceDB 37 (26548 restarts, 132 cnfs/res, 25.0% reduced, 9b 9057g 18645g3) > | 3515001 | 2752 8939 40191 | 61109 17 9.3 71.6 | 9.563 % | | 3705001 | 2752 8939 40191 | 251109 22 15.1 71.1 | 9.563 % | < ReduceDB 38 (27901 restarts, 133 cnfs/res, 25.0% reduced, 9b 9350g 19204g3) > | 3705001 | 2752 8939 40191 | 62776 16 9.4 71.1 | 9.563 % | | 3900002 | 2752 8939 40191 | 257777 22 15.1 70.5 | 9.563 % | < ReduceDB 39 (29203 restarts, 134 cnfs/res, 25.0% reduced, 9b 9657g 19820g3) > | 3900002 | 2752 8939 40191 | 64443 17 9.2 70.5 | 9.563 % | | 4100001 | 2752 8939 40191 | 264442 22 15.0 69.8 | 9.563 % | < ReduceDB 40 (30400 restarts, 135 cnfs/res, 25.0% reduced, 9b 9964g 20473g3) > | 4100001 | 2752 8939 40191 | 66109 17 9.2 69.8 | 9.563 % | | 4305002 | 2752 8939 40191 | 271110 22 15.1 69.3 | 9.563 % | < ReduceDB 41 (31696 restarts, 136 cnfs/res, 25.0% reduced, 9b 10278g 21144g3) > | 4305002 | 2752 8939 40191 | 67776 16 9.5 69.3 | 9.563 % | | 4515001 | 2752 8939 40191 | 277775 22 14.9 68.8 | 9.563 % | < ReduceDB 42 (32941 restarts, 137 cnfs/res, 25.0% reduced, 9b 10508g 21932g3) > | 4515001 | 2752 8939 40191 | 69442 17 9.1 68.8 | 9.563 % | | 4730001 | 2752 8939 40191 | 284442 22 14.9 68.3 | 9.563 % | < ReduceDB 43 (34232 restarts, 138 cnfs/res, 25.0% reduced, 9b 10770g 22587g3) > | 4730001 | 2752 8939 40191 | 71109 16 9.4 68.3 | 9.563 % | | 4950003 | 2752 8939 40191 | 291111 22 14.7 67.7 | 9.563 % | < ReduceDB 44 (35348 restarts, 140 cnfs/res, 25.0% reduced, 9b 11110g 23314g3) > | 4950003 | 2752 8939 40191 | 72776 16 9.2 67.7 | 9.563 % | | 5050023 | 2752 8939 40191 | 172796 21 13.4 67.5 | 9.563 % | | 5175001 | 2752 8939 40191 | 297774 22 14.7 67.1 | 9.563 % | < ReduceDB 45 (36458 restarts, 142 cnfs/res, 25.0% reduced, 9b 11453g 24120g3) > | 5175001 | 2752 8939 40191 | 74442 17 9.0 67.1 | 9.563 % | | 5405002 | 2752 8939 40191 | 304443 22 14.4 66.4 | 9.563 % | < ReduceDB 46 (37476 restarts, 144 cnfs/res, 25.0% reduced, 9b 11722g 24726g3) > | 5405002 | 2752 8939 40191 | 76109 17 9.2 66.4 | 9.563 % | | 5640001 | 2752 8939 40191 | 311108 22 14.8 66.0 | 9.563 % | < ReduceDB 47 (38945 restarts, 145 cnfs/res, 25.0% reduced, 9b 12065g 25459g3) > | 5640001 | 2752 8939 40191 | 77776 16 8.9 66.0 | 9.563 % | | 5880001 | 2752 8939 40191 | 317776 22 14.8 65.5 | 9.563 % | < ReduceDB 48 (40463 restarts, 145 cnfs/res, 25.0% reduced, 9b 12357g 26100g3) > | 5880001 | 2752 8939 40191 | 79443 16 9.0 65.5 | 9.563 % | | 6125001 | 2752 8939 40191 | 324443 22 14.6 65.1 | 9.563 % | < ReduceDB 49 (41975 restarts, 146 cnfs/res, 25.0% reduced, 9b 12626g 26916g3) > | 6125001 | 2752 8939 40191 | 81109 17 8.7 65.1 | 9.563 % | | 6375003 | 2752 8939 40191 | 331111 22 14.8 64.7 | 9.563 % | < ReduceDB 50 (43683 restarts, 146 cnfs/res, 25.0% reduced, 9b 12915g 27670g3) > | 6375003 | 2752 8939 40191 | 82776 16 8.9 64.7 | 9.563 % | | 6630001 | 2752 8939 40191 | 337774 22 14.6 64.3 | 9.563 % | < ReduceDB 51 (45143 restarts, 147 cnfs/res, 25.0% reduced, 9b 13208g 28533g3) > | 6630001 | 2752 8939 40191 | 84442 17 8.5 64.3 | 9.563 % | | 6890002 | 2752 8939 40191 | 344443 22 14.4 63.8 | 9.563 % | < ReduceDB 52 (46461 restarts, 148 cnfs/res, 25.0% reduced, 9b 13513g 29263g3) > | 6890002 | 2752 8939 40191 | 86109 16 8.8 63.8 | 9.563 % | | 7155001 | 2752 8939 40191 | 351108 22 14.6 63.4 | 9.563 % | < ReduceDB 53 (48010 restarts, 149 cnfs/res, 25.0% reduced, 9b 13804g 29850g3) > | 7155001 | 2752 8939 40191 | 87776 16 8.8 63.4 | 9.563 % | | 7425001 | 2752 8939 40191 | 357776 22 14.5 63.0 | 9.563 % | < ReduceDB 54 (49563 restarts, 150 cnfs/res, 25.0% reduced, 9b 14146g 30549g3) > | 7425001 | 2752 8939 40191 | 89443 16 8.7 63.0 | 9.563 % | | 7575139 | 2752 8939 40191 | 239581 20 13.6 62.8 | 9.563 % | | 7700002 | 2752 8939 40191 | 364444 21 14.6 62.6 | 9.563 % | < ReduceDB 55 (51406 restarts, 150 cnfs/res, 25.0% reduced, 9b 14511g 31196g3) > | 7700002 | 2752 8939 40191 | 91110 16 8.7 62.6 | 9.563 % | | 7980001 | 2752 8939 40191 | 371109 22 14.5 62.2 | 9.563 % | < ReduceDB 56 (52830 restarts, 151 cnfs/res, 25.0% reduced, 9b 14808g 31919g3) > | 7980001 | 2752 8939 40191 | 92776 16 8.6 62.2 | 9.563 % | | 8265001 | 2752 8939 40191 | 377776 22 14.0 61.8 | 9.563 % | < ReduceDB 57 (54199 restarts, 152 cnfs/res, 25.0% reduced, 9b 15082g 32765g3) > | 8265001 | 2752 8939 40191 | 94443 16 8.3 61.8 | 9.563 % | | 8555002 | 2752 8939 40191 | 384444 22 14.4 61.5 | 9.563 % | < ReduceDB 58 (55887 restarts, 153 cnfs/res, 25.0% reduced, 9b 15409g 33396g3) > | 8555002 | 2752 8939 40191 | 96110 16 8.5 61.5 | 9.563 % | | 8850001 | 2752 8939 40191 | 391109 22 14.2 61.0 | 9.563 % | < ReduceDB 59 (56889 restarts, 156 cnfs/res, 25.0% reduced, 9b 15706g 34367g3) > | 8850001 | 2752 8939 40191 | 97776 16 8.7 61.0 | 9.563 % | | 9150001 | 2752 8939 40191 | 397776 21 14.4 60.6 | 9.563 % | < ReduceDB 60 (58527 restarts, 156 cnfs/res, 25.0% reduced, 9b 16056g 35207g3) > | 9150001 | 2752 8939 40191 | 99443 16 8.6 60.6 | 9.563 % | | 9455001 | 2752 8939 40191 | 404443 22 14.3 60.2 | 9.563 % | < ReduceDB 61 (60064 restarts, 157 cnfs/res, 25.0% reduced, 9b 16404g 35974g3) > | 9455001 | 2752 8939 40191 | 101109 16 8.5 60.2 | 9.563 % | | 9765001 | 2752 8939 40191 | 411109 22 14.2 59.9 | 9.563 % | < ReduceDB 62 (61657 restarts, 158 cnfs/res, 25.0% reduced, 10b 16710g 36786g3) > | 9765001 | 2752 8939 40191 | 102776 16 8.4 59.9 | 9.563 % | | 10080001 | 2752 8939 40191 | 417776 21 14.0 59.4 | 9.563 % | < ReduceDB 63 (63000 restarts, 160 cnfs/res, 25.0% reduced, 10b 17059g 37557g3) > | 10080001 | 2752 8939 40191 | 104443 16 8.4 59.4 | 9.563 % | | 10400001 | 2752 8939 40191 | 424443 21 14.3 59.1 | 9.563 % | < ReduceDB 64 (64863 restarts, 160 cnfs/res, 25.0% reduced, 10b 17337g 38441g3) > | 10400001 | 2752 8939 40191 | 106109 16 8.2 59.1 | 9.563 % | | 10725003 | 2752 8939 40191 | 431111 21 14.4 58.8 | 9.563 % | < ReduceDB 65 (66491 restarts, 161 cnfs/res, 25.0% reduced, 10b 17675g 39236g3) > | 10725003 | 2752 8939 40191 | 107776 16 8.5 58.8 | 9.563 % | | 11055002 | 2752 8939 40191 | 437775 22 14.2 58.4 | 9.563 % | < ReduceDB 66 (67828 restarts, 163 cnfs/res, 25.0% reduced, 10b 17988g 39982g3) > | 11055002 | 2752 8939 40191 | 109442 16 8.3 58.4 | 9.563 % | | 11362814 | 2752 8939 40191 | 417254 21 14.0 58.1 | 9.563 % | | 11390001 | 2752 8939 40191 | 444441 21 14.1 58.1 | 9.563 % | < ReduceDB 67 (69428 restarts, 164 cnfs/res, 25.0% reduced, 10b 18324g 40793g3) > | 11390001 | 2752 8939 40191 | 111109 15 8.1 58.1 | 9.563 % | | 11730003 | 2752 8939 40191 | 451111 21 13.8 57.6 | 9.563 % | < ReduceDB 68 (70469 restarts, 166 cnfs/res, 25.0% reduced, 10b 18637g 41380g3) > | 11730003 | 2752 8939 40191 | 112776 17 7.8 57.6 | 9.563 % | | 12075002 | 2752 8939 40191 | 457775 21 14.1 57.4 | 9.563 % | < ReduceDB 69 (72535 restarts, 166 cnfs/res, 25.0% reduced, 10b 19003g 42059g3) > | 12075002 | 2752 8939 40191 | 114442 16 8.3 57.4 | 9.563 % | | 12425002 | 2752 8939 40191 | 464442 21 14.1 57.1 | 9.563 % | < ReduceDB 70 (74327 restarts, 167 cnfs/res, 25.0% reduced, 10b 19359g 43021g3) > | 12425002 | 2752 8939 40191 | 116109 15 8.1 57.1 | 9.563 % | | 12780001 | 2752 8939 40191 | 471108 21 14.0 56.7 | 9.563 % | < ReduceDB 71 (75834 restarts, 169 cnfs/res, 25.0% reduced, 10b 19720g 43922g3) > | 12780001 | 2752 8939 40191 | 117776 16 8.1 56.7 | 9.563 % | | 13140001 | 2752 8939 40191 | 477776 21 13.9 56.4 | 9.563 % | < ReduceDB 72 (77529 restarts, 169 cnfs/res, 25.0% reduced, 10b 20019g 44738g3) > | 13140001 | 2752 8939 40191 | 119443 16 7.7 56.4 | 9.563 % | | 13505004 | 2752 8939 40191 | 484446 21 14.0 56.1 | 9.563 % | < ReduceDB 73 (79066 restarts, 171 cnfs/res, 25.0% reduced, 10b 20357g 45567g3) > | 13505004 | 2752 8939 40191 | 121110 16 8.1 56.1 | 9.563 % | | 13875001 | 2752 8939 40191 | 491107 21 14.1 55.8 | 9.563 % | < ReduceDB 74 (80567 restarts, 172 cnfs/res, 25.0% reduced, 10b 20657g 46161g3) > | 13875001 | 2752 8939 40191 | 122775 16 8.2 55.8 | 9.563 % | | 14250001 | 2752 8939 40191 | 497775 21 13.9 55.5 | 9.563 % | < ReduceDB 75 (82028 restarts, 174 cnfs/res, 25.0% reduced, 10b 20973g 47012g3) > | 14250001 | 2752 8939 40191 | 124442 16 8.0 55.5 | 9.563 % | | 14630001 | 2752 8939 40191 | 504442 21 14.0 55.2 | 9.563 % | < ReduceDB 76 (83866 restarts, 174 cnfs/res, 25.0% reduced, 10b 21335g 48113g3) > | 14630001 | 2752 8939 40191 | 126109 15 8.0 55.2 | 9.563 % | | 15015001 | 2752 8939 40191 | 511109 21 13.7 54.9 | 9.563 % | < ReduceDB 77 (85227 restarts, 176 cnfs/res, 25.0% reduced, 10b 21661g 49049g3) > | 15015001 | 2752 8939 40191 | 127776 16 7.7 54.9 | 9.563 % | | 15405002 | 2752 8939 40191 | 517777 21 13.7 54.6 | 9.563 % | < ReduceDB 78 (86788 restarts, 178 cnfs/res, 25.0% reduced, 10b 21951g 49701g3) > | 15405002 | 2752 8939 40191 | 129443 15 8.1 54.6 | 9.563 % | | 15800002 | 2752 8939 40191 | 524443 21 14.2 54.3 | 9.563 % | < ReduceDB 79 (88474 restarts, 179 cnfs/res, 25.0% reduced, 10b 22269g 50640g3) > | 15800002 | 2752 8939 40191 | 131109 16 8.1 54.3 | 9.563 % | | 16200001 | 2752 8939 40191 | 531108 21 14.1 54.1 | 9.563 % | < ReduceDB 80 (90604 restarts, 179 cnfs/res, 25.0% reduced, 10b 22616g 51384g3) > | 16200001 | 2752 8939 40191 | 132776 15 8.0 54.1 | 9.563 % | | 16605003 | 2752 8939 40191 | 537778 21 13.9 53.8 | 9.563 % | < ReduceDB 81 (92135 restarts, 180 cnfs/res, 25.0% reduced, 10b 22990g 52219g3) > | 16605003 | 2752 8939 40191 | 134443 15 7.8 53.8 | 9.563 % | | 17015001 | 2752 8939 40191 | 544441 21 13.7 53.5 | 9.563 % | < ReduceDB 82 (93796 restarts, 181 cnfs/res, 25.0% reduced, 10b 23314g 52963g3) > | 17015001 | 2752 8939 40191 | 136109 16 7.7 53.5 | 9.563 % | | 17044326 | 2752 8939 40191 | 165434 17 9.0 53.5 | 9.563 % | | 17430001 | 2752 8939 40191 | 551109 21 13.9 53.3 | 9.563 % | < ReduceDB 83 (95482 restarts, 183 cnfs/res, 25.0% reduced, 10b 23667g 53728g3) > | 17430001 | 2752 8939 40191 | 137776 15 8.0 53.3 | 9.563 % | | 17850001 | 2752 8939 40191 | 557776 21 14.1 53.0 | 9.563 % | < ReduceDB 84 (97409 restarts, 183 cnfs/res, 25.0% reduced, 10b 23990g 54454g3) > | 17850001 | 2752 8939 40191 | 139443 15 8.1 53.0 | 9.563 % | | 18275001 | 2752 8939 40191 | 564443 21 14.0 52.8 | 9.563 % | < ReduceDB 85 (99431 restarts, 184 cnfs/res, 25.0% reduced, 10b 24383g 55273g3) > | 18275001 | 2752 8939 40191 | 141109 15 7.8 52.8 | 9.563 % | | 18529597 | 2752 8939 40191 | 395705 20 13.1 52.6 | 9.563 % | ==================================================================================== restarts : 100498 (34.12 /sec) (184.38 confs/res) conflicts : 18529597 (6290 /sec) decisions : 63364159 (0.00 % random) (21510 /sec) propagations : 1841124267 (625005 /sec) conflict literals : 431763234 (16.19 % deleted) average of lbd : 13.09 Memory used : 161.00 MB CPU time : 2945.78 s INDETERMINATE 18 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_18-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 15193 | | Parse time: 0.01 s | | Eliminated clauses: 0.14 Mb | | Simplification time: 0.06 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 3073 9771 44084 | 100 58 55.8 2078.6 | 9.071 % | | 250 | 3073 9771 44084 | 250 38 32.9 1090.0 | 9.071 % | | 475 | 3073 9771 44084 | 475 35 28.0 736.9 | 9.071 % | | 812 | 3073 9771 44084 | 812 33 24.9 556.0 | 9.071 % | | 1318 | 3073 9771 44084 | 1318 31 23.1 418.8 | 9.071 % | | 2077 | 3073 9771 44084 | 2077 30 22.1 299.6 | 9.071 % | | 3216 | 3073 9771 44084 | 3216 29 20.9 227.8 | 9.071 % | | 4924 | 3073 9771 44084 | 4924 28 20.5 184.2 | 9.071 % | | 5001 | 3073 9771 44084 | 5001 28 20.5 182.5 | 9.071 % | < ReduceDB 1 ( 12 restarts, 417 cnfs/res, 50.0% reduced, 0b 19g 64g3) > | 5001 | 3073 9771 44084 | 2501 25 17.9 182.5 | 9.071 % | | 7486 | 3073 9771 44084 | 4986 25 18.6 157.0 | 9.071 % | | 11330 | 3073 9771 44084 | 8830 25 18.3 139.6 | 9.071 % | | 14843 | 3073 9771 44084 | 12343 24 18.1 129.3 | 9.071 % | ==================================================================================== restarts : 76 (162.77 /sec) (195.30 confs/res) conflicts : 14843 (31789 /sec) decisions : 94003 (0.00 % random) (201322 /sec) propagations : 1274025 (2728520 /sec) conflict literals : 374327 (14.34 % deleted) average of lbd : 18.09 Memory used : 8.00 MB CPU time : 0.466929 s INDETERMINATE 19 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_19-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 15205 | | Parse time: 0.01 s | | Eliminated clauses: 0.14 Mb | | Simplification time: 0.06 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 3067 9771 44101 | 100 66 64.0 2803.9 | 8.840 % | | 250 | 3067 9771 44101 | 250 48 44.6 1598.5 | 8.840 % | | 475 | 3067 9771 44101 | 475 39 32.2 975.4 | 8.840 % | | 812 | 3067 9771 44101 | 812 38 28.7 672.5 | 8.840 % | | 1318 | 3067 9771 44101 | 1318 37 27.2 512.2 | 8.840 % | | 1633 | 3067 9771 44101 | 1633 36 26.7 461.1 | 8.840 % | ==================================================================================== restarts : 5 (43.87 /sec) (326.60 confs/res) conflicts : 1633 (14327 /sec) decisions : 12350 (0.00 % random) (108350 /sec) propagations : 145998 (1280886 /sec) conflict literals : 58738 (13.36 % deleted) average of lbd : 26.71 Memory used : 8.00 MB CPU time : 0.113982 s SATISFIABLE 20 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_20-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 15212 | | Parse time: 0.01 s | | Eliminated clauses: 0.13 Mb | | Simplification time: 0.05 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 3247 10221 45960 | 0 nan nan nan | 9.679 % | ==================================================================================== restarts : 1 (17.24 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 669 (11536 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 8.00 MB CPU time : 0.057991 s INDETERMINATE 21 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_21-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 15208 | | Parse time: 0.01 s | | Eliminated clauses: 0.14 Mb | | Simplification time: 0.05 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 3113 9889 44957 | 100 47 44.5 2946.2 | 8.854 % | | 250 | 3113 9889 44957 | 250 38 35.0 1786.3 | 8.854 % | | 475 | 3113 9889 44957 | 475 34 27.6 1125.1 | 8.854 % | | 812 | 3113 9889 44957 | 812 36 27.5 803.3 | 8.854 % | | 1318 | 3113 9889 44957 | 1318 36 26.2 615.3 | 8.854 % | | 1830 | 3113 9889 44957 | 1830 33 24.6 477.3 | 8.854 % | ==================================================================================== restarts : 5 (43.87 /sec) (366.00 confs/res) conflicts : 1830 (16055 /sec) decisions : 19237 (0.00 % random) (168772 /sec) propagations : 184107 (1615229 /sec) conflict literals : 60496 (11.92 % deleted) average of lbd : 24.61 Memory used : 8.00 MB CPU time : 0.113982 s SATISFIABLE 22 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_22-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 15200 | | Parse time: 0.01 s | | Eliminated clauses: 0.08 Mb | | Simplification time: 0.02 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 4423 11658 46841 | 0 nan nan nan | 8.044 % | ==================================================================================== restarts : 1 (30.31 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 556 (16852 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 8.00 MB CPU time : 0.032994 s INDETERMINATE 23 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_23-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 15213 | | Parse time: 0.01 s | | Eliminated clauses: 0.14 Mb | | Simplification time: 0.06 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 3168 10033 45922 | 100 75 72.4 2532.8 | 8.275 % | | 250 | 3168 10033 45922 | 250 43 39.2 1352.1 | 8.275 % | | 475 | 3168 10033 45922 | 475 41 33.5 907.7 | 8.275 % | | 798 | 3168 10033 45922 | 798 40 30.6 665.1 | 8.275 % | ==================================================================================== restarts : 3 (34.10 /sec) (266.00 confs/res) conflicts : 798 (9070 /sec) decisions : 13151 (0.00 % random) (149467 /sec) propagations : 72752 (826859 /sec) conflict literals : 31928 (6.57 % deleted) average of lbd : 30.62 Memory used : 9.00 MB CPU time : 0.087986 s SATISFIABLE 24 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_24-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 15210 | | Parse time: 0.01 s | | Eliminated clauses: 0.14 Mb | | Simplification time: 0.06 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 3148 9995 45778 | 100 62 57.8 2992.8 | 8.145 % | | 250 | 3148 9995 45778 | 250 64 59.6 2828.2 | 8.145 % | | 287 | 3148 9995 45778 | 287 58 54.0 2568.5 | 8.145 % | ==================================================================================== restarts : 2 (27.03 /sec) (143.50 confs/res) conflicts : 287 (3879 /sec) decisions : 10559 (0.00 % random) (142712 /sec) propagations : 18813 (254271 /sec) conflict literals : 16751 (0.98 % deleted) average of lbd : 53.99 Memory used : 8.00 MB CPU time : 0.073988 s INDETERMINATE 25 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_25-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 15210 | | Parse time: 0.01 s | | Eliminated clauses: 0.14 Mb | | Simplification time: 0.05 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 3161 10004 45809 | 100 52 47.6 3004.2 | 8.464 % | | 250 | 3161 10004 45809 | 250 42 38.4 2208.0 | 8.464 % | | 475 | 3161 10004 45809 | 475 43 36.0 1444.2 | 8.464 % | | 490 | 3161 10004 45809 | 490 42 35.4 1406.6 | 8.464 % | ==================================================================================== restarts : 3 (39.48 /sec) (163.33 confs/res) conflicts : 490 (6448 /sec) decisions : 14244 (0.00 % random) (187451 /sec) propagations : 47632 (626836 /sec) conflict literals : 20812 (4.03 % deleted) average of lbd : 35.39 Memory used : 8.00 MB CPU time : 0.075988 s SATISFIABLE 26 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_26-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 15209 | | Parse time: 0.01 s | | Eliminated clauses: 0.14 Mb | | Simplification time: 0.05 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 3152 10027 46108 | 100 56 52.3 2998.3 | 8.435 % | | 250 | 3152 10027 46108 | 250 51 47.4 2475.8 | 8.435 % | | 475 | 3152 10027 46108 | 475 39 33.9 1536.8 | 8.435 % | | 747 | 3152 10027 46108 | 747 38 32.0 1135.8 | 8.435 % | ==================================================================================== restarts : 3 (38.97 /sec) (249.00 confs/res) conflicts : 747 (9703 /sec) decisions : 14148 (0.00 % random) (183769 /sec) propagations : 59921 (778316 /sec) conflict literals : 28171 (3.63 % deleted) average of lbd : 32.02 Memory used : 9.00 MB CPU time : 0.076988 s SATISFIABLE 27 28 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_28-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 15223 | | Parse time: 0.01 s | | Eliminated clauses: 0.14 Mb | | Simplification time: 0.05 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 3152 10037 46255 | 100 35 32.1 2089.4 | 8.174 % | | 250 | 3152 10037 46255 | 250 30 25.4 1223.7 | 8.174 % | | 320 | 3152 10037 46255 | 320 31 25.6 1054.8 | 8.174 % | ==================================================================================== restarts : 3 (43.49 /sec) (106.67 confs/res) conflicts : 320 (4638 /sec) decisions : 15997 (0.00 % random) (231878 /sec) propagations : 36317 (526417 /sec) conflict literals : 9873 (2.71 % deleted) average of lbd : 25.64 Memory used : 9.00 MB CPU time : 0.068989 s SATISFIABLE 29 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_29-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 15228 | | Parse time: 0.01 s | | Eliminated clauses: 0.15 Mb | | Simplification time: 0.05 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 3152 10034 46271 | 100 33 30.4 2013.2 | 7.957 % | | 250 | 3152 10034 46271 | 250 30 25.0 1163.1 | 7.957 % | | 380 | 3152 10034 46271 | 380 31 25.6 900.0 | 7.957 % | ==================================================================================== restarts : 3 (40.01 /sec) (126.67 confs/res) conflicts : 380 (5067 /sec) decisions : 17581 (0.00 % random) (234451 /sec) propagations : 47634 (635222 /sec) conflict literals : 11905 (2.06 % deleted) average of lbd : 25.57 Memory used : 9.00 MB CPU time : 0.074988 s SATISFIABLE 30 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_30-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 15216 | | Parse time: 0.01 s | | Simplification time: 0.01 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 6260 14336 44662 | 0 nan nan nan | 9.433 % | ==================================================================================== restarts : 1 (50.01 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 652 (32607 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 8.00 MB CPU time : 0.019996 s INDETERMINATE 31 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_31-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 15226 | | Parse time: 0.01 s | | Eliminated clauses: 0.13 Mb | | Simplification time: 0.04 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 3236 10162 46852 | 100 103 100.0 2983.2 | 10.966 % | | 250 | 3236 10162 46852 | 250 61 55.3 1687.7 | 10.966 % | | 285 | 3236 10162 46852 | 285 57 50.8 1554.0 | 10.966 % | ==================================================================================== restarts : 2 (31.25 /sec) (142.50 confs/res) conflicts : 285 (4454 /sec) decisions : 11023 (0.00 % random) (172261 /sec) propagations : 29975 (468433 /sec) conflict literals : 16125 (0.89 % deleted) average of lbd : 50.80 Memory used : 8.00 MB CPU time : 0.06399 s SATISFIABLE 32 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_32-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 15232 | | Parse time: 0.01 s | | Eliminated clauses: 0.12 Mb | | Simplification time: 0.04 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 3425 10475 47920 | 100 55 52.9 2208.4 | 11.560 % | | 250 | 3425 10475 47920 | 250 50 43.7 1508.3 | 11.560 % | | 455 | 3425 10475 47920 | 455 46 35.8 1276.7 | 11.560 % | ==================================================================================== restarts : 2 (31.75 /sec) (227.50 confs/res) conflicts : 455 (7223 /sec) decisions : 11953 (0.00 % random) (189760 /sec) propagations : 45562 (723321 /sec) conflict literals : 20704 (2.88 % deleted) average of lbd : 35.78 Memory used : 8.00 MB CPU time : 0.06299 s SATISFIABLE 33 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_33-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 15264 | | Parse time: 0.01 s | | Eliminated clauses: 0.11 Mb | | Simplification time: 0.04 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 4160 11771 52164 | 100 37 32.3 1380.8 | 7.407 % | | 250 | 4160 11771 52164 | 250 37 21.3 897.2 | 7.407 % | | 321 | 4160 11771 52164 | 321 37 19.9 818.0 | 7.407 % | ==================================================================================== restarts : 1 (17.86 /sec) (321.00 confs/res) conflicts : 321 (5733 /sec) decisions : 8790 (0.00 % random) (156990 /sec) propagations : 40348 (720616 /sec) conflict literals : 11838 (6.35 % deleted) average of lbd : 19.88 Memory used : 9.00 MB CPU time : 0.055991 s INDETERMINATE