1 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_1-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 13539 | | Parse time: 0.01 s | | Simplification time: 0.00 s | | | ==================================================================================== Solved by simplification restarts : 0 (0.00 /sec) (nan confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 167 (18560 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 7.00 MB CPU time : 0.008998 s UNSATISFIABLE 2 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_2-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 14028 | | Parse time: 0.01 s | | Simplification time: 0.00 s | | | ==================================================================================== Solved by simplification restarts : 0 (0.00 /sec) (nan confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 337 (37453 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 7.00 MB CPU time : 0.008998 s UNSATISFIABLE 3 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_3-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 15171 | | Parse time: 0.01 s | | Eliminated clauses: 0.20 Mb | | Simplification time: 0.05 s | | | ==================================================================================== Solved by simplification restarts : 0 (0.00 /sec) (nan confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 1050 (18424 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 8.00 MB CPU time : 0.056991 s UNSATISFIABLE 4 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_4-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 15188 | | Parse time: 0.01 s | | Eliminated clauses: 0.21 Mb | | Simplification time: 0.06 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 24 | 90 446 1723 | 21 4 3.5 16.8 | 11.560 % | ==================================================================================== restarts : 1 (13.70 /sec) (24.00 confs/res) conflicts : 24 (329 /sec) decisions : 55 (0.00 % random) (754 /sec) propagations : 1121 (15359 /sec) conflict literals : 87 (6.45 % deleted) average of lbd : 3.52 Memory used : 8.00 MB CPU time : 0.072988 s UNSATISFIABLE 5 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_5-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 15191 | | Parse time: 0.01 s | | Eliminated clauses: 0.21 Mb | | Simplification time: 0.06 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 245 1165 5422 | 100 9 7.2 130.4 | 12.341 % | | 250 | 245 1165 5422 | 250 9 6.8 86.0 | 12.341 % | | 398 | 230 1165 5422 | 393 8 5.6 57.0 | 12.558 % | ==================================================================================== restarts : 1 (13.52 /sec) (398.00 confs/res) conflicts : 398 (5379 /sec) decisions : 577 (0.00 % random) (7799 /sec) propagations : 5092 (68822 /sec) conflict literals : 2961 (8.95 % deleted) average of lbd : 5.56 Memory used : 8.00 MB CPU time : 0.073988 s UNSATISFIABLE 6 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_6-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 15186 | | Parse time: 0.01 s | | Eliminated clauses: 0.20 Mb | | Simplification time: 0.06 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 453 2052 9235 | 100 20 18.5 326.2 | 11.646 % | | 250 | 453 2052 9235 | 250 18 15.8 260.1 | 11.646 % | | 475 | 453 2052 9235 | 475 12 10.6 140.6 | 11.646 % | | 812 | 452 2052 9235 | 811 10 7.9 84.7 | 11.661 % | | 937 | 412 2052 9235 | 927 9 7.2 74.0 | 12.240 % | ==================================================================================== restarts : 2 (25.00 /sec) (468.50 confs/res) conflicts : 937 (11714 /sec) decisions : 1549 (0.00 % random) (19366 /sec) propagations : 16476 (205983 /sec) conflict literals : 8308 (16.94 % deleted) average of lbd : 7.24 Memory used : 8.00 MB CPU time : 0.079987 s UNSATISFIABLE 7 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_7-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 15192 | | Parse time: 0.01 s | | Eliminated clauses: 0.19 Mb | | Simplification time: 0.07 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 803 3205 14478 | 100 38 36.5 499.9 | 11.386 % | | 250 | 803 3205 14478 | 250 39 36.4 439.8 | 11.386 % | | 475 | 803 3205 14478 | 475 38 34.7 381.0 | 11.386 % | | 812 | 803 3205 14478 | 812 31 27.6 281.5 | 11.386 % | | 1318 | 803 3205 14478 | 1318 23 19.9 178.4 | 11.386 % | | 2077 | 803 3205 14478 | 2077 18 14.9 116.7 | 11.386 % | | 3216 | 803 3205 14478 | 3216 14 11.7 78.5 | 11.386 % | | 4924 | 802 3161 14265 | 1828 17 13.2 54.2 | 11.400 % | | 5002 | 802 3161 14265 | 1906 16 12.8 53.4 | 11.400 % | < ReduceDB 1 ( 2 restarts, 2501 cnfs/res, 50.4% reduced, 1b 159g 299g3) > | 5002 | 802 3161 14265 | 960 8 4.2 53.4 | 11.400 % | | 6696 | 760 3011 13552 | 1192 7 3.8 41.7 | 12.008 % | ==================================================================================== restarts : 2 (11.11 /sec) (3348.00 confs/res) conflicts : 6696 (37206 /sec) decisions : 9940 (0.00 % random) (55231 /sec) propagations : 206254 (1146034 /sec) conflict literals : 72406 (24.02 % deleted) average of lbd : 3.82 Memory used : 8.00 MB CPU time : 0.179972 s UNSATISFIABLE 8 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_8-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 15197 | | Parse time: 0.01 s | | Eliminated clauses: 0.20 Mb | | Simplification time: 0.07 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 859 3519 16393 | 100 29 26.6 696.1 | 10.185 % | | 250 | 859 3519 16393 | 250 20 16.9 378.2 | 10.185 % | | 475 | 859 3519 16393 | 475 15 11.7 220.2 | 10.185 % | | 812 | 859 3519 16393 | 812 14 10.0 145.9 | 10.185 % | | 1318 | 859 3519 16393 | 1318 12 8.6 101.3 | 10.185 % | | 2077 | 859 3519 16393 | 2077 12 8.0 75.3 | 10.185 % | | 3216 | 859 3519 16393 | 3216 12 7.9 62.3 | 10.185 % | | 4924 | 859 3519 16393 | 4924 12 7.7 52.2 | 10.185 % | | 5001 | 859 3519 16393 | 5001 12 7.7 51.8 | 10.185 % | < ReduceDB 1 ( 16 restarts, 313 cnfs/res, 50.0% reduced, 0b 157g 440g3) > | 5001 | 859 3519 16393 | 2503 11 6.1 51.8 | 10.185 % | | 7486 | 859 3519 16393 | 4988 11 6.4 44.5 | 10.185 % | | 11330 | 859 3519 16393 | 8832 11 6.6 38.7 | 10.185 % | | 15001 | 859 3519 16393 | 12503 11 6.6 34.8 | 10.185 % | < ReduceDB 2 ( 22 restarts, 682 cnfs/res, 50.0% reduced, 0b 479g 1315g3) > | 15001 | 859 3519 16393 | 6253 10 5.5 34.8 | 10.185 % | | 17096 | 859 3519 16393 | 8348 11 5.8 33.2 | 10.185 % | | 25745 | 859 3519 16393 | 16997 10 6.0 28.2 | 10.185 % | | 26774 | 768 3445 15994 | 16109 10 5.8 27.4 | 11.502 % | ==================================================================================== restarts : 33 (47.90 /sec) (811.33 confs/res) conflicts : 26774 (38865 /sec) decisions : 38194 (0.00 % random) (55442 /sec) propagations : 858314 (1245929 /sec) conflict literals : 285831 (21.64 % deleted) average of lbd : 5.83 Memory used : 8.00 MB CPU time : 0.688895 s UNSATISFIABLE 9 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_9-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 15190 | | Parse time: 0.01 s | | Eliminated clauses: 0.19 Mb | | Simplification time: 0.07 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 1147 4525 21319 | 100 32 29.5 1014.0 | 10.938 % | | 250 | 1147 4525 21319 | 250 22 19.3 594.5 | 10.938 % | | 475 | 1147 4525 21319 | 475 18 14.2 359.1 | 10.938 % | | 812 | 1147 4525 21319 | 812 16 12.0 238.7 | 10.938 % | | 1318 | 1147 4525 21319 | 1318 15 10.9 174.7 | 10.938 % | | 2077 | 1147 4525 21319 | 2077 15 10.4 133.1 | 10.938 % | | 3216 | 1147 4525 21319 | 3216 14 10.0 102.7 | 10.938 % | | 4924 | 1147 4525 21319 | 4924 13 9.6 78.4 | 10.938 % | | 5002 | 1147 4525 21319 | 5002 13 9.6 77.6 | 10.938 % | < ReduceDB 1 ( 2 restarts, 2501 cnfs/res, 50.0% reduced, 0b 122g 236g3) > | 5002 | 1147 4525 21319 | 2503 11 7.5 77.6 | 10.938 % | | 7486 | 1147 4525 21319 | 4987 11 7.7 58.2 | 10.938 % | | 11330 | 1147 4525 21319 | 8831 11 7.8 47.8 | 10.938 % | | 15001 | 1147 4525 21319 | 12502 12 7.7 42.6 | 10.938 % | < ReduceDB 2 ( 13 restarts, 1154 cnfs/res, 50.0% reduced, 0b 330g 757g3) > | 15001 | 1147 4525 21319 | 6253 12 7.1 42.6 | 10.938 % | | 17096 | 1147 4525 21319 | 8348 12 7.2 40.4 | 10.938 % | | 25745 | 1147 4525 21319 | 16997 12 7.4 36.2 | 10.938 % | | 30003 | 1147 4525 21319 | 21255 12 7.4 34.1 | 10.938 % | < ReduceDB 3 ( 37 restarts, 811 cnfs/res, 50.0% reduced, 0b 755g 1678g3) > | 30003 | 1147 4525 21319 | 10627 12 6.4 34.1 | 10.938 % | | 38719 | 1147 4525 21319 | 19343 12 7.1 31.5 | 10.938 % | | 50001 | 1147 4525 21319 | 30625 12 7.5 28.0 | 10.938 % | < ReduceDB 4 ( 91 restarts, 549 cnfs/res, 50.0% reduced, 0b 1189g 2559g3) > | 50001 | 1147 4525 21319 | 15312 11 6.5 28.0 | 10.938 % | | 58180 | 1147 4525 21319 | 23491 11 7.0 25.7 | 10.938 % | | 68907 | 1076 4384 20640 | 20423 10 6.0 23.0 | 11.965 % | ==================================================================================== restarts : 108 (39.99 /sec) (638.03 confs/res) conflicts : 68907 (25516 /sec) decisions : 98013 (0.00 % random) (36293 /sec) propagations : 2731238 (1011349 /sec) conflict literals : 798548 (23.63 % deleted) average of lbd : 6.04 Memory used : 9.00 MB CPU time : 2.70059 s UNSATISFIABLE 10 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_10-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 15186 | | Parse time: 0.01 s | | Eliminated clauses: 0.19 Mb | | Simplification time: 0.07 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 1496 5532 25331 | 100 35 32.1 1108.3 | 9.910 % | | 250 | 1496 5532 25331 | 250 22 19.4 477.5 | 9.910 % | | 475 | 1496 5532 25331 | 475 18 15.2 267.6 | 9.910 % | | 812 | 1496 5532 25331 | 812 16 13.1 169.0 | 9.910 % | | 1318 | 1496 5532 25331 | 1318 15 12.0 113.6 | 9.910 % | | 2077 | 1496 5532 25331 | 2077 15 11.5 93.8 | 9.910 % | | 3216 | 1496 5532 25331 | 3216 15 11.5 75.5 | 9.910 % | | 4924 | 1496 5532 25331 | 4924 15 11.5 63.6 | 9.910 % | | 5001 | 1496 5532 25331 | 5001 15 11.5 63.2 | 9.910 % | < ReduceDB 1 ( 10 restarts, 500 cnfs/res, 50.0% reduced, 0b 91g 166g3) > | 5001 | 1496 5532 25331 | 2501 14 9.8 63.2 | 9.910 % | | 7486 | 1496 5532 25331 | 4986 14 10.3 54.3 | 9.910 % | | 11330 | 1496 5532 25331 | 8830 14 10.4 45.3 | 9.910 % | | 15001 | 1496 5532 25331 | 12501 15 10.6 42.0 | 9.910 % | < ReduceDB 2 ( 25 restarts, 600 cnfs/res, 50.0% reduced, 0b 230g 530g3) > | 15001 | 1496 5532 25331 | 6251 14 9.8 42.0 | 9.910 % | | 17096 | 1496 5532 25331 | 8346 15 9.7 40.8 | 9.910 % | | 25745 | 1496 5532 25331 | 16995 16 10.4 37.6 | 9.910 % | | 30002 | 1496 5532 25331 | 21252 16 10.5 36.2 | 9.910 % | < ReduceDB 3 ( 94 restarts, 319 cnfs/res, 50.0% reduced, 0b 747g 1274g3) > | 30002 | 1496 5532 25331 | 10626 15 9.1 36.2 | 9.910 % | | 38719 | 1496 5532 25331 | 19343 15 9.9 34.3 | 9.910 % | | 50001 | 1496 5532 25331 | 30625 16 10.4 32.8 | 9.910 % | < ReduceDB 4 ( 199 restarts, 251 cnfs/res, 50.0% reduced, 0b 1235g 1928g3) > | 50001 | 1496 5532 25331 | 15312 16 9.1 32.8 | 9.910 % | | 58180 | 1496 5532 25331 | 23491 17 9.8 32.1 | 9.910 % | | 75004 | 1496 5532 25331 | 40315 17 10.6 31.0 | 9.910 % | < ReduceDB 5 ( 369 restarts, 203 cnfs/res, 46.8% reduced, 0b 1828g 2471g3) > | 75004 | 1496 5532 25331 | 18870 15 8.8 31.0 | 9.910 % | | 87372 | 1496 5532 25331 | 31238 16 9.8 30.1 | 9.910 % | | 105002 | 1496 5532 25331 | 48868 16 10.3 29.1 | 9.910 % | < ReduceDB 6 ( 495 restarts, 212 cnfs/res, 40.9% reduced, 0b 2355g 3210g3) > | 105002 | 1496 5532 25331 | 19994 14 8.1 29.1 | 9.910 % | | 131161 | 1496 5532 25331 | 46153 15 9.7 27.4 | 9.910 % | | 140001 | 1496 5532 25331 | 54993 15 10.0 26.8 | 9.910 % | < ReduceDB 7 ( 596 restarts, 235 cnfs/res, 37.3% reduced, 0b 2776g 3841g3) > | 140001 | 1496 5532 25331 | 20530 12 7.9 26.8 | 9.910 % | | 180002 | 1496 5532 25331 | 60531 15 9.9 25.7 | 9.910 % | < ReduceDB 8 ( 790 restarts, 228 cnfs/res, 37.3% reduced, 0b 3334g 4551g3) > | 180002 | 1496 5532 25331 | 22567 13 7.5 25.7 | 9.910 % | | 196845 | 1496 5532 25331 | 39410 14 9.1 25.1 | 9.910 % | | 225002 | 1496 5532 25331 | 67567 14 9.8 24.2 | 9.910 % | < ReduceDB 9 ( 908 restarts, 248 cnfs/res, 36.9% reduced, 0b 3764g 5165g3) > | 225002 | 1496 5532 25331 | 24906 12 7.3 24.2 | 9.910 % | | 275001 | 1496 5532 25331 | 74905 14 9.3 22.7 | 9.910 % | < ReduceDB 10 ( 937 restarts, 293 cnfs/res, 32.5% reduced, 0b 4069g 5698g3) > | 275001 | 1496 5532 25331 | 24356 12 6.9 22.7 | 9.910 % | | 295371 | 1496 5532 25331 | 44726 13 8.4 22.3 | 9.910 % | | 330001 | 1496 5532 25331 | 79356 13 8.8 21.4 | 9.910 % | < ReduceDB 11 (1003 restarts, 329 cnfs/res, 32.3% reduced, 0b 4512g 6441g3) > | 330001 | 1496 5532 25331 | 25602 11 6.0 21.4 | 9.910 % | | 390003 | 1495 5438 24788 | 39528 11 6.9 19.9 | 9.925 % | < ReduceDB 12 (1022 restarts, 382 cnfs/res, 37.5% reduced, 1b 4555g 6450g3) > | 390003 | 1495 5438 24788 | 14825 10 4.1 19.9 | 9.925 % | | 443160 | 1495 5438 24788 | 67982 12 7.6 19.0 | 9.925 % | | 455003 | 1493 5386 24571 | 72178 11 7.5 18.7 | 9.954 % | < ReduceDB 13 (1036 restarts, 439 cnfs/res, 34.9% reduced, 12b 4980g 7678g3) > | 455003 | 1493 5386 24571 | 25213 10 4.7 18.7 | 9.954 % | | 464005 | 1422 5386 24571 | 34202 10 5.1 18.5 | 10.981 % | ==================================================================================== restarts : 1037 (36.24 /sec) (447.45 confs/res) conflicts : 464005 (16217 /sec) decisions : 652607 (0.00 % random) (22808 /sec) propagations : 20408913 (713283 /sec) conflict literals : 6556534 (21.07 % deleted) average of lbd : 5.06 Memory used : 24.00 MB CPU time : 28.6126 s UNSATISFIABLE 11 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_11-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 15206 | | Parse time: 0.01 s | | Eliminated clauses: 0.18 Mb | | Simplification time: 0.07 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 1469 5354 24712 | 100 48 45.5 1331.2 | 11.502 % | | 250 | 1469 5354 24712 | 250 28 23.7 723.0 | 11.502 % | | 475 | 1469 5354 24712 | 475 24 18.1 486.7 | 11.502 % | | 812 | 1469 5354 24712 | 812 23 16.1 376.4 | 11.502 % | | 1318 | 1469 5354 24712 | 1318 24 15.5 311.9 | 11.502 % | | 2077 | 1469 5354 24712 | 2077 21 13.8 239.6 | 11.502 % | | 3216 | 1469 5354 24712 | 3216 21 13.5 173.8 | 11.502 % | | 4924 | 1469 5354 24712 | 4924 21 13.3 131.8 | 11.502 % | | 5002 | 1469 5354 24712 | 5002 21 13.2 131.5 | 11.502 % | < ReduceDB 1 ( 7 restarts, 715 cnfs/res, 50.0% reduced, 0b 67g 207g3) > | 5002 | 1469 5354 24712 | 2502 18 11.0 131.5 | 11.502 % | | 7486 | 1469 5354 24712 | 4986 19 11.6 107.8 | 11.502 % | | 11330 | 1469 5354 24712 | 8830 19 11.4 88.5 | 11.502 % | | 15003 | 1469 5354 24712 | 12503 19 11.5 81.9 | 11.502 % | < ReduceDB 2 ( 34 restarts, 441 cnfs/res, 50.0% reduced, 0b 299g 724g3) > | 15003 | 1469 5354 24712 | 6251 17 9.7 81.9 | 11.502 % | | 17096 | 1469 5354 24712 | 8344 18 10.5 79.3 | 11.502 % | | 25745 | 1469 5354 24712 | 16993 18 11.0 71.5 | 11.502 % | | 30003 | 1469 5354 24712 | 21251 18 11.2 69.9 | 11.502 % | < ReduceDB 3 ( 116 restarts, 259 cnfs/res, 50.0% reduced, 0b 655g 1345g3) > | 30003 | 1469 5354 24712 | 10625 16 9.6 69.9 | 11.502 % | | 38719 | 1469 5354 24712 | 19341 18 10.6 66.2 | 11.502 % | | 50002 | 1469 5354 24712 | 30624 18 11.1 63.6 | 11.502 % | < ReduceDB 4 ( 207 restarts, 242 cnfs/res, 50.0% reduced, 0b 1137g 2064g3) > | 50002 | 1469 5354 24712 | 15312 16 9.4 63.6 | 11.502 % | | 58180 | 1469 5354 24712 | 23490 17 9.9 61.4 | 11.502 % | | 75003 | 1469 5354 24712 | 40313 19 10.7 58.3 | 11.502 % | < ReduceDB 5 ( 288 restarts, 260 cnfs/res, 44.8% reduced, 0b 1591g 2808g3) > | 75003 | 1469 5354 24712 | 18053 17 8.9 58.3 | 11.502 % | | 87372 | 1469 5354 24712 | 30422 18 10.2 56.7 | 11.502 % | | 105002 | 1469 5354 24712 | 48052 19 10.7 54.7 | 11.502 % | < ReduceDB 6 ( 392 restarts, 268 cnfs/res, 39.9% reduced, 0b 1936g 3382g3) > | 105002 | 1469 5354 24712 | 19155 16 8.5 54.7 | 11.502 % | | 131161 | 1469 5354 24712 | 45314 18 10.3 53.0 | 11.502 % | | 140001 | 1469 5354 24712 | 54154 18 10.6 52.1 | 11.502 % | < ReduceDB 7 ( 525 restarts, 267 cnfs/res, 38.5% reduced, 0b 2279g 4147g3) > | 140001 | 1469 5354 24712 | 20839 16 8.3 52.1 | 11.502 % | | 180001 | 1469 5354 24712 | 60839 19 10.2 49.6 | 11.502 % | < ReduceDB 8 ( 685 restarts, 263 cnfs/res, 38.6% reduced, 0b 2676g 5056g3) > | 180001 | 1469 5354 24712 | 23460 16 7.8 49.6 | 11.502 % | | 196845 | 1469 5354 24712 | 40304 18 9.1 48.7 | 11.502 % | | 225002 | 1469 5354 24712 | 68461 19 10.3 47.9 | 11.502 % | < ReduceDB 9 ( 910 restarts, 247 cnfs/res, 36.8% reduced, 1b 3052g 5705g3) > | 225002 | 1469 5354 24712 | 25187 15 7.7 47.9 | 11.502 % | | 275004 | 1469 5354 24712 | 75189 19 10.6 46.6 | 11.502 % | < ReduceDB 10 (1171 restarts, 235 cnfs/res, 33.8% reduced, 1b 3398g 6171g3) > | 275004 | 1469 5354 24712 | 25413 15 7.6 46.6 | 11.502 % | | 295371 | 1469 5354 24712 | 45780 18 9.2 46.1 | 11.502 % | | 330001 | 1469 5354 24712 | 80410 19 10.3 45.3 | 11.502 % | < ReduceDB 11 (1378 restarts, 239 cnfs/res, 33.3% reduced, 1b 3711g 6618g3) > | 330001 | 1469 5354 24712 | 26745 16 7.3 45.3 | 11.502 % | | 390003 | 1469 5354 24712 | 86747 19 10.4 44.3 | 11.502 % | < ReduceDB 12 (1634 restarts, 239 cnfs/res, 31.2% reduced, 1b 3952g 7001g3) > | 390003 | 1469 5354 24712 | 27037 15 7.6 44.3 | 11.502 % | | 443160 | 1469 5354 24712 | 80194 19 9.9 43.5 | 11.502 % | | 455002 | 1469 5354 24712 | 92036 19 10.2 43.3 | 11.502 % | < ReduceDB 13 (1912 restarts, 238 cnfs/res, 32.1% reduced, 1b 4239g 7535g3) > | 455002 | 1469 5354 24712 | 29521 16 7.2 43.3 | 11.502 % | | 525001 | 1469 5354 24712 | 99520 19 9.9 42.4 | 11.502 % | < ReduceDB 14 (2169 restarts, 242 cnfs/res, 29.9% reduced, 1b 4564g 8091g3) > | 525001 | 1469 5354 24712 | 29756 16 6.0 42.4 | 11.502 % | | 600001 | 1469 5354 24712 | 104756 20 9.8 41.8 | 11.502 % | < ReduceDB 15 (2563 restarts, 234 cnfs/res, 27.4% reduced, 2b 4833g 8701g3) > | 600001 | 1469 5354 24712 | 28673 15 6.4 41.8 | 11.502 % | | 664843 | 1469 5354 24712 | 93515 19 9.8 41.4 | 11.502 % | | 680006 | 1469 5354 24712 | 108678 19 9.8 41.3 | 11.502 % | < ReduceDB 16 (2981 restarts, 228 cnfs/res, 28.6% reduced, 2b 5120g 9136g3) > | 680006 | 1469 5354 24712 | 31109 16 6.0 41.3 | 11.502 % | | 765003 | 1469 5354 24712 | 116106 19 10.0 40.8 | 11.502 % | < ReduceDB 17 (3523 restarts, 217 cnfs/res, 28.1% reduced, 3b 5378g 9714g3) > | 765003 | 1469 5354 24712 | 32680 15 7.1 40.8 | 11.502 % | | 855001 | 1469 5354 24712 | 122678 19 10.1 40.3 | 11.502 % | < ReduceDB 18 (3993 restarts, 214 cnfs/res, 27.4% reduced, 3b 5650g 10338g3) > | 855001 | 1469 5354 24712 | 33618 15 6.6 40.3 | 11.502 % | | 950004 | 1469 5354 24712 | 128621 19 10.1 39.8 | 11.502 % | < ReduceDB 19 (4512 restarts, 211 cnfs/res, 26.6% reduced, 3b 5960g 11334g3) > | 950004 | 1469 5354 24712 | 34238 15 6.6 39.8 | 11.502 % | | 997368 | 1469 5354 24712 | 81602 18 9.2 39.5 | 11.502 % | | 1050001 | 1469 5354 24712 | 134235 19 9.7 39.1 | 11.502 % | < ReduceDB 20 (4891 restarts, 215 cnfs/res, 25.7% reduced, 3b 6211g 12186g3) > | 1050001 | 1469 5354 24712 | 34475 14 5.9 39.1 | 11.502 % | | 1155001 | 1469 5354 24712 | 139475 18 9.7 38.6 | 11.502 % | < ReduceDB 21 (5364 restarts, 215 cnfs/res, 27.0% reduced, 3b 6538g 12856g3) > | 1155001 | 1469 5354 24712 | 37644 14 6.2 38.6 | 11.502 % | | 1265001 | 1469 5354 24712 | 147644 19 9.7 38.1 | 11.502 % | < ReduceDB 22 (5910 restarts, 214 cnfs/res, 26.7% reduced, 3b 6871g 14033g3) > | 1265001 | 1469 5354 24712 | 39351 14 6.0 38.1 | 11.502 % | | 1380002 | 1469 5354 24712 | 154352 19 9.5 37.5 | 11.502 % | < ReduceDB 23 (6408 restarts, 215 cnfs/res, 27.2% reduced, 3b 7237g 15234g3) > | 1380002 | 1469 5354 24712 | 41982 14 5.9 37.5 | 11.502 % | | 1496156 | 1469 5354 24712 | 158136 19 9.6 37.1 | 11.502 % | | 1500002 | 1469 5354 24712 | 161982 19 9.6 37.1 | 11.502 % | < ReduceDB 24 (6966 restarts, 215 cnfs/res, 25.6% reduced, 3b 7536g 16248g3) > | 1500002 | 1469 5354 24712 | 41510 14 5.7 37.1 | 11.502 % | | 1625001 | 1469 5354 24712 | 166509 18 9.6 36.7 | 11.502 % | < ReduceDB 25 (7541 restarts, 215 cnfs/res, 26.1% reduced, 3b 7910g 17451g3) > | 1625001 | 1469 5354 24712 | 43535 14 5.6 36.7 | 11.502 % | | 1755001 | 1469 5354 24712 | 173535 18 9.4 36.3 | 11.502 % | < ReduceDB 26 (8126 restarts, 216 cnfs/res, 26.3% reduced, 3b 8474g 19360g3) > | 1755001 | 1469 5354 24712 | 45679 14 5.2 36.3 | 11.502 % | | 1890003 | 1469 5354 24712 | 180681 17 8.9 35.7 | 11.502 % | < ReduceDB 27 (8478 restarts, 223 cnfs/res, 25.7% reduced, 3b 8962g 21068g3) > | 1890003 | 1469 5354 24712 | 46498 13 5.1 35.7 | 11.502 % | | 2030002 | 1469 5354 24712 | 186497 17 8.5 35.2 | 11.502 % | < ReduceDB 28 (8744 restarts, 232 cnfs/res, 26.2% reduced, 3b 9364g 22686g3) > | 2030002 | 1469 5354 24712 | 48795 13 5.1 35.2 | 11.502 % | | 2175001 | 1469 5354 24712 | 193794 17 8.8 34.7 | 11.502 % | < ReduceDB 29 (9064 restarts, 240 cnfs/res, 26.0% reduced, 3b 9815g 24091g3) > | 2175001 | 1469 5354 24712 | 50462 13 5.0 34.7 | 11.502 % | | 2244338 | 1469 5354 24712 | 119799 16 7.9 34.5 | 11.502 % | | 2325002 | 1469 5354 24712 | 200463 16 8.4 34.1 | 11.502 % | < ReduceDB 30 (9337 restarts, 249 cnfs/res, 27.0% reduced, 3b 10288g 25871g3) > | 2325002 | 1469 5354 24712 | 54168 13 4.4 34.1 | 11.502 % | | 2480002 | 1469 5354 24712 | 209168 16 8.3 33.7 | 11.502 % | < ReduceDB 31 (9610 restarts, 258 cnfs/res, 26.5% reduced, 3b 10784g 27404g3) > | 2480002 | 1469 5354 24712 | 55380 13 4.6 33.7 | 11.502 % | | 2640001 | 1469 5354 24712 | 215379 15 8.4 33.1 | 11.502 % | < ReduceDB 32 (9840 restarts, 268 cnfs/res, 25.8% reduced, 3b 11144g 28549g3) > | 2640001 | 1469 5354 24712 | 55640 13 4.6 33.1 | 11.502 % | | 2805002 | 1469 5354 24712 | 220641 16 8.3 32.7 | 11.502 % | < ReduceDB 33 (10182 restarts, 275 cnfs/res, 26.0% reduced, 3b 11500g 29882g3) > | 2805002 | 1469 5354 24712 | 57466 13 4.7 32.7 | 11.502 % | | 2975002 | 1469 5354 24712 | 227466 15 8.7 32.3 | 11.502 % | < ReduceDB 34 (10520 restarts, 283 cnfs/res, 26.1% reduced, 3b 11815g 30764g3) > | 2975002 | 1469 5354 24712 | 59410 12 4.5 32.3 | 11.502 % | | 3150003 | 1469 5354 24712 | 234411 16 8.4 31.9 | 11.502 % | < ReduceDB 35 (10863 restarts, 290 cnfs/res, 25.7% reduced, 3b 12195g 31966g3) > | 3150003 | 1469 5354 24712 | 60357 13 4.4 31.9 | 11.502 % | | 3330001 | 1469 5354 24712 | 240355 15 8.4 31.5 | 11.502 % | < ReduceDB 36 (11194 restarts, 297 cnfs/res, 25.9% reduced, 3b 12671g 33253g3) > | 3330001 | 1469 5354 24712 | 62357 12 4.3 31.5 | 11.502 % | | 3366612 | 1469 5354 24712 | 98968 14 6.6 31.4 | 11.502 % | | 3515001 | 1469 5354 24712 | 247357 15 8.3 31.0 | 11.502 % | < ReduceDB 37 (11530 restarts, 305 cnfs/res, 25.3% reduced, 3b 13084g 34539g3) > | 3515001 | 1469 5354 24712 | 62660 12 4.2 31.0 | 11.502 % | | 3705001 | 1469 5354 24712 | 252660 15 8.3 30.6 | 11.502 % | < ReduceDB 38 (12003 restarts, 309 cnfs/res, 25.6% reduced, 3b 13692g 36124g3) > | 3705001 | 1469 5354 24712 | 64663 12 4.1 30.6 | 11.502 % | | 3900001 | 1469 5354 24712 | 259663 15 8.4 30.3 | 11.502 % | < ReduceDB 39 (12569 restarts, 310 cnfs/res, 26.4% reduced, 3b 14279g 37437g3) > | 3900001 | 1469 5354 24712 | 68427 12 4.3 30.3 | 11.502 % | | 4100002 | 1469 5354 24712 | 268428 15 8.4 29.9 | 11.502 % | < ReduceDB 40 (13125 restarts, 312 cnfs/res, 26.0% reduced, 3b 14708g 38531g3) > | 4100002 | 1469 5354 24712 | 69757 12 4.1 29.9 | 11.502 % | | 4305002 | 1469 5354 24712 | 274757 15 8.3 29.5 | 11.502 % | < ReduceDB 41 (13714 restarts, 314 cnfs/res, 26.0% reduced, 3b 15211g 39512g3) > | 4305002 | 1469 5354 24712 | 71365 12 4.3 29.5 | 11.502 % | | 4515002 | 1469 5354 24712 | 281365 15 8.5 29.1 | 11.502 % | < ReduceDB 42 (14322 restarts, 315 cnfs/res, 25.9% reduced, 3b 15792g 40740g3) > | 4515002 | 1469 5354 24712 | 72862 12 4.1 29.1 | 11.502 % | | 4730002 | 1469 5354 24712 | 287862 15 8.6 28.8 | 11.502 % | < ReduceDB 43 (15131 restarts, 313 cnfs/res, 26.1% reduced, 3b 16330g 41766g3) > | 4730002 | 1469 5354 24712 | 75095 12 4.3 28.8 | 11.502 % | | 4950001 | 1469 5354 24712 | 295094 14 9.0 28.4 | 11.502 % | < ReduceDB 44 (16261 restarts, 304 cnfs/res, 26.5% reduced, 3b 16931g 42818g3) > | 4950001 | 1469 5354 24712 | 78126 12 4.4 28.4 | 11.502 % | | 5050023 | 1469 5354 24712 | 178148 14 8.2 28.2 | 11.502 % | | 5175002 | 1469 5354 24712 | 303127 14 9.4 28.0 | 11.502 % | < ReduceDB 45 (17635 restarts, 293 cnfs/res, 26.6% reduced, 3b 17373g 43609g3) > | 5175002 | 1469 5354 24712 | 80610 12 4.6 28.0 | 11.502 % | | 5405001 | 1469 5354 24712 | 310609 14 9.5 27.5 | 11.502 % | < ReduceDB 46 (18941 restarts, 285 cnfs/res, 26.8% reduced, 3b 17815g 44523g3) > | 5405001 | 1469 5354 24712 | 83113 12 4.6 27.5 | 11.502 % | | 5640001 | 1469 5354 24712 | 318113 14 9.9 27.1 | 11.502 % | < ReduceDB 47 (20397 restarts, 277 cnfs/res, 26.3% reduced, 3b 18269g 45011g3) > | 5640001 | 1469 5354 24712 | 83514 12 4.5 27.1 | 11.502 % | | 5880001 | 1469 5354 24712 | 323514 14 9.7 26.7 | 11.502 % | < ReduceDB 48 (21584 restarts, 272 cnfs/res, 26.0% reduced, 3b 18670g 45389g3) > | 5880001 | 1469 5354 24712 | 84093 12 4.5 26.7 | 11.502 % | | 6125003 | 1469 5354 24712 | 329095 14 9.5 26.3 | 11.502 % | < ReduceDB 49 (22538 restarts, 272 cnfs/res, 25.2% reduced, 3b 19080g 45783g3) > | 6125003 | 1469 5354 24712 | 82909 12 4.3 26.3 | 11.502 % | | 6375002 | 1469 5354 24712 | 332908 14 9.6 25.9 | 11.502 % | < ReduceDB 50 (23515 restarts, 271 cnfs/res, 26.4% reduced, 3b 19394g 46139g3) > | 6375002 | 1469 5354 24712 | 87740 12 4.6 25.9 | 11.502 % | | 6630002 | 1469 5354 24712 | 342740 14 9.5 25.5 | 11.502 % | < ReduceDB 51 (24410 restarts, 272 cnfs/res, 25.0% reduced, 3b 19666g 46483g3) > | 6630002 | 1469 5354 24712 | 85684 12 4.2 25.5 | 11.502 % | | 6890002 | 1469 5354 24712 | 345684 14 9.4 25.1 | 11.502 % | < ReduceDB 52 (25169 restarts, 274 cnfs/res, 25.0% reduced, 3b 19992g 46825g3) > | 6890002 | 1469 5354 24712 | 86561 11 4.1 25.1 | 11.502 % | | 7155003 | 1469 5354 24712 | 351562 14 9.0 24.7 | 11.502 % | < ReduceDB 53 (25720 restarts, 278 cnfs/res, 25.2% reduced, 3b 20299g 47265g3) > | 7155003 | 1469 5354 24712 | 88462 12 4.2 24.7 | 11.502 % | | 7425003 | 1469 5354 24712 | 358462 13 8.7 24.3 | 11.502 % | < ReduceDB 54 (26086 restarts, 285 cnfs/res, 25.0% reduced, 4b 20676g 47860g3) > | 7425003 | 1469 5354 24712 | 89614 12 4.3 24.3 | 11.502 % | | 7575139 | 1469 5354 24712 | 239750 14 8.1 24.1 | 11.502 % | | 7700001 | 1469 5354 24712 | 364612 14 8.7 24.0 | 11.502 % | < ReduceDB 55 (26580 restarts, 290 cnfs/res, 25.0% reduced, 5b 21148g 48990g3) > | 7700001 | 1469 5354 24712 | 91152 12 4.2 24.0 | 11.502 % | | 7980001 | 1469 5354 24712 | 371152 13 8.4 23.6 | 11.502 % | < ReduceDB 56 (27034 restarts, 295 cnfs/res, 25.7% reduced, 6b 21902g 50830g3) > | 7980001 | 1469 5354 24712 | 95422 11 4.1 23.6 | 11.502 % | | 8250127 | 1287 4130 18668 | 30476 11 3.7 23.2 | 14.135 % | ==================================================================================== restarts : 27201 (16.02 /sec) (303.30 confs/res) conflicts : 8250127 (4860 /sec) decisions : 11759826 (0.00 % random) (6927 /sec) propagations : 344308337 (202820 /sec) conflict literals : 134829449 (18.67 % deleted) average of lbd : 3.75 Memory used : 84.00 MB CPU time : 1697.61 s UNSATISFIABLE 12 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_12-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 15201 | | Parse time: 0.01 s | | Eliminated clauses: 0.18 Mb | | Simplification time: 0.07 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 1738 6253 29206 | 100 38 34.5 961.7 | 10.402 % | | 250 | 1738 6253 29206 | 250 32 28.5 689.2 | 10.402 % | | 475 | 1738 6253 29206 | 475 25 21.4 465.6 | 10.402 % | | 812 | 1738 6253 29206 | 812 24 18.2 351.9 | 10.402 % | | 1229 | 1738 6253 29206 | 1229 23 17.3 297.7 | 10.402 % | ==================================================================================== restarts : 3 (28.31 /sec) (409.67 confs/res) conflicts : 1229 (11596 /sec) decisions : 9549 (0.00 % random) (90099 /sec) propagations : 68099 (642546 /sec) conflict literals : 28502 (11.98 % deleted) average of lbd : 17.30 Memory used : 8.00 MB CPU time : 0.105983 s SATISFIABLE 13 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_13-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 15197 | | Parse time: 0.01 s | | Eliminated clauses: 0.18 Mb | | Simplification time: 0.07 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 1828 6461 30198 | 100 40 37.2 1686.0 | 10.460 % | | 250 | 1828 6461 30198 | 250 31 27.4 996.7 | 10.460 % | | 475 | 1828 6461 30198 | 475 26 20.5 606.9 | 10.460 % | | 812 | 1828 6461 30198 | 812 24 18.4 421.7 | 10.460 % | | 1215 | 1828 6461 30198 | 1215 23 16.7 339.6 | 10.460 % | ==================================================================================== restarts : 3 (28.04 /sec) (405.00 confs/res) conflicts : 1215 (11357 /sec) decisions : 9559 (0.00 % random) (89351 /sec) propagations : 71485 (668190 /sec) conflict literals : 27513 (16.50 % deleted) average of lbd : 16.65 Memory used : 8.00 MB CPU time : 0.106983 s SATISFIABLE 14 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_14-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 15193 | | Parse time: 0.01 s | | Eliminated clauses: 0.17 Mb | | Simplification time: 0.06 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 2089 7388 34734 | 100 45 43.5 1901.6 | 9.954 % | | 250 | 2089 7388 34734 | 250 30 27.0 1063.5 | 9.954 % | | 475 | 2089 7388 34734 | 475 27 21.9 676.2 | 9.954 % | | 812 | 2089 7388 34734 | 812 28 21.4 478.5 | 9.954 % | | 1318 | 2089 7388 34734 | 1318 29 21.2 367.1 | 9.954 % | | 2077 | 2089 7388 34734 | 2077 29 20.9 273.7 | 9.954 % | | 3216 | 2089 7388 34734 | 3216 27 19.8 192.7 | 9.954 % | | 4924 | 2089 7388 34734 | 4924 27 19.3 141.3 | 9.954 % | | 5001 | 2089 7388 34734 | 5001 27 19.2 140.0 | 9.954 % | < ReduceDB 1 ( 6 restarts, 834 cnfs/res, 50.0% reduced, 0b 24g 88g3) > | 5001 | 2089 7388 34734 | 2501 23 16.2 140.0 | 9.954 % | | 7486 | 2089 7388 34734 | 4986 23 16.7 117.1 | 9.954 % | | 11330 | 2089 7388 34734 | 8830 23 15.5 94.0 | 9.954 % | | 15004 | 2089 7388 34734 | 12504 24 15.1 82.1 | 9.954 % | < ReduceDB 2 ( 17 restarts, 883 cnfs/res, 50.0% reduced, 0b 108g 377g3) > | 15004 | 2089 7388 34734 | 6252 22 12.8 82.1 | 9.954 % | | 17096 | 2089 7388 34734 | 8344 22 13.6 78.8 | 9.954 % | | 25745 | 2089 7388 34734 | 16993 22 14.4 73.0 | 9.954 % | | 30002 | 2089 7388 34734 | 21250 22 14.4 69.0 | 9.954 % | < ReduceDB 3 ( 103 restarts, 291 cnfs/res, 50.0% reduced, 0b 271g 764g3) > | 30002 | 2089 7388 34734 | 10625 19 13.3 69.0 | 9.954 % | | 38719 | 2089 7388 34734 | 19342 20 14.3 67.3 | 9.954 % | | 50002 | 2089 7388 34734 | 30625 20 14.6 66.1 | 9.954 % | < ReduceDB 4 ( 261 restarts, 192 cnfs/res, 45.4% reduced, 1b 533g 1250g3) > | 50002 | 2089 7388 34734 | 13890 19 12.9 66.1 | 9.954 % | | 58180 | 2089 7388 34734 | 22068 20 13.9 64.8 | 9.954 % | | 75001 | 2089 7388 34734 | 38889 21 14.5 62.2 | 9.954 % | < ReduceDB 5 ( 443 restarts, 169 cnfs/res, 40.8% reduced, 1b 798g 1817g3) > | 75001 | 2089 7388 34734 | 15871 18 12.2 62.2 | 9.954 % | | 87372 | 2089 7388 34734 | 28242 20 13.8 61.6 | 9.954 % | | 105001 | 2089 7388 34734 | 45871 20 14.6 60.3 | 9.954 % | < ReduceDB 6 ( 726 restarts, 145 cnfs/res, 36.6% reduced, 1b 1076g 2158g3) > | 105001 | 2089 7388 34734 | 16772 18 12.4 60.3 | 9.954 % | | 131161 | 2089 7388 34734 | 42932 20 14.3 58.7 | 9.954 % | | 140001 | 2089 7388 34734 | 51772 20 14.4 57.5 | 9.954 % | < ReduceDB 7 ( 972 restarts, 144 cnfs/res, 34.1% reduced, 1b 1362g 2668g3) > | 140001 | 2089 7388 34734 | 17676 18 11.5 57.5 | 9.954 % | | 180001 | 2089 7388 34734 | 57676 24 12.5 54.9 | 9.954 % | < ReduceDB 8 (1061 restarts, 170 cnfs/res, 31.4% reduced, 1b 1557g 3208g3) > | 180001 | 2089 7388 34734 | 18117 23 9.7 54.9 | 9.954 % | | 196845 | 2089 7388 34734 | 34961 26 10.8 53.9 | 9.954 % | | 225001 | 2089 7388 34734 | 63117 26 12.2 53.5 | 9.954 % | < ReduceDB 9 (1249 restarts, 180 cnfs/res, 27.2% reduced, 1b 1710g 3398g3) > | 225001 | 2089 7388 34734 | 17156 17 11.2 53.5 | 9.954 % | | 275001 | 2089 7388 34734 | 67156 21 14.0 52.7 | 9.954 % | < ReduceDB 10 (1719 restarts, 160 cnfs/res, 29.8% reduced, 1b 1972g 3875g3) > | 275001 | 2089 7388 34734 | 20023 16 10.9 52.7 | 9.954 % | | 295371 | 2089 7388 34734 | 40393 19 13.4 52.5 | 9.954 % | | 330002 | 2089 7388 34734 | 75024 20 14.7 52.2 | 9.954 % | < ReduceDB 11 (2367 restarts, 139 cnfs/res, 29.5% reduced, 1b 2279g 4485g3) > | 330002 | 2089 7388 34734 | 22116 17 10.6 52.2 | 9.954 % | | 390002 | 2089 7388 34734 | 82116 21 14.6 51.4 | 9.954 % | < ReduceDB 12 (2942 restarts, 133 cnfs/res, 27.9% reduced, 1b 2590g 5081g3) > | 390002 | 2089 7388 34734 | 22912 16 10.2 51.4 | 9.954 % | | 443160 | 2089 7388 34734 | 76070 20 14.6 51.2 | 9.954 % | | 455002 | 2089 7388 34734 | 87912 21 14.8 51.1 | 9.954 % | < ReduceDB 13 (3698 restarts, 123 cnfs/res, 26.9% reduced, 1b 2876g 5549g3) > | 455002 | 2089 7388 34734 | 23634 17 10.1 51.1 | 9.954 % | | 525001 | 2089 7388 34734 | 93633 21 14.7 50.4 | 9.954 % | < ReduceDB 14 (4344 restarts, 121 cnfs/res, 26.0% reduced, 1b 3164g 6048g3) > | 525001 | 2089 7388 34734 | 24361 16 10.0 50.4 | 9.954 % | | 600001 | 2089 7388 34734 | 99361 21 14.5 49.4 | 9.954 % | < ReduceDB 15 (4932 restarts, 122 cnfs/res, 25.4% reduced, 1b 3486g 6632g3) > | 600001 | 2089 7388 34734 | 25202 16 9.6 49.4 | 9.954 % | | 664843 | 2089 7388 34734 | 90044 20 14.3 48.4 | 9.954 % | | 680002 | 2089 7388 34734 | 105203 21 14.5 48.3 | 9.954 % | < ReduceDB 16 (5435 restarts, 125 cnfs/res, 25.0% reduced, 1b 3828g 7128g3) > | 680002 | 2089 7388 34734 | 26299 16 9.5 48.3 | 9.954 % | | 765002 | 2089 7388 34734 | 111299 21 14.8 47.2 | 9.954 % | < ReduceDB 17 (5968 restarts, 128 cnfs/res, 25.0% reduced, 1b 4164g 7646g3) > | 765002 | 2089 7388 34734 | 27823 16 9.5 47.2 | 9.954 % | | 855001 | 2089 7388 34734 | 117822 21 14.1 46.0 | 9.954 % | < ReduceDB 18 (6401 restarts, 134 cnfs/res, 25.0% reduced, 1b 4528g 8207g3) > | 855001 | 2089 7388 34734 | 29454 17 9.2 46.0 | 9.954 % | | 950001 | 2089 7388 34734 | 124454 21 14.3 45.1 | 9.954 % | < ReduceDB 19 (6915 restarts, 137 cnfs/res, 25.0% reduced, 3b 4924g 8657g3) > | 950001 | 2089 7388 34734 | 31112 15 9.5 45.1 | 9.954 % | | 997368 | 2089 7388 34734 | 78479 19 13.4 44.7 | 9.954 % | | 1050002 | 2089 7388 34734 | 131113 21 14.5 44.2 | 9.954 % | < ReduceDB 20 (7478 restarts, 140 cnfs/res, 25.0% reduced, 3b 5249g 9087g3) > | 1050002 | 2089 7388 34734 | 32777 17 9.5 44.2 | 9.954 % | | 1155001 | 2089 7388 34734 | 137776 21 14.5 43.3 | 9.954 % | < ReduceDB 21 (7992 restarts, 145 cnfs/res, 25.0% reduced, 3b 5615g 9525g3) > | 1155001 | 2089 7388 34734 | 34443 17 9.5 43.3 | 9.954 % | | 1265001 | 2089 7388 34734 | 144443 21 14.8 42.7 | 9.954 % | < ReduceDB 22 (8707 restarts, 145 cnfs/res, 25.0% reduced, 3b 5974g 9976g3) > | 1265001 | 2089 7388 34734 | 36109 16 9.5 42.7 | 9.954 % | | 1380001 | 2089 7388 34734 | 151109 20 14.9 42.3 | 9.954 % | < ReduceDB 23 (9670 restarts, 143 cnfs/res, 25.0% reduced, 3b 6362g 10543g3) > | 1380001 | 2089 7388 34734 | 37776 15 9.2 42.3 | 9.954 % | | 1496156 | 2089 7388 34734 | 153931 20 14.4 41.7 | 9.954 % | | 1500001 | 2089 7388 34734 | 157776 20 14.5 41.6 | 9.954 % | < ReduceDB 24 (10327 restarts, 145 cnfs/res, 25.0% reduced, 3b 6737g 11139g3) > | 1500001 | 2089 7388 34734 | 39443 15 9.5 41.6 | 9.954 % | | 1625002 | 2089 7388 34734 | 164444 20 14.9 41.1 | 9.954 % | < ReduceDB 25 (11122 restarts, 146 cnfs/res, 25.0% reduced, 3b 7093g 11784g3) > | 1625002 | 2089 7388 34734 | 41110 15 9.7 41.1 | 9.954 % | | 1755001 | 2089 7388 34734 | 171109 20 14.9 40.5 | 9.954 % | < ReduceDB 26 (11924 restarts, 147 cnfs/res, 25.0% reduced, 3b 7496g 12352g3) > | 1755001 | 2089 7388 34734 | 42776 15 9.4 40.5 | 9.954 % | | 1890001 | 2089 7388 34734 | 177776 20 15.0 40.2 | 9.954 % | < ReduceDB 27 (12991 restarts, 145 cnfs/res, 25.0% reduced, 3b 7937g 12983g3) > | 1890001 | 2089 7388 34734 | 44443 15 9.3 40.2 | 9.954 % | | 2030001 | 2089 7388 34734 | 184443 20 14.7 39.6 | 9.954 % | < ReduceDB 28 (13733 restarts, 148 cnfs/res, 25.0% reduced, 3b 8376g 13809g3) > | 2030001 | 2089 7388 34734 | 46109 15 8.9 39.6 | 9.954 % | | 2175001 | 2089 7388 34734 | 191109 19 14.1 38.9 | 9.954 % | < ReduceDB 29 (14266 restarts, 152 cnfs/res, 25.0% reduced, 3b 8790g 14378g3) > | 2175001 | 2089 7388 34734 | 47776 16 8.6 38.9 | 9.954 % | | 2244338 | 2089 7388 34734 | 117113 19 12.9 38.7 | 9.954 % | | 2325001 | 2089 7388 34734 | 197776 21 13.8 38.3 | 9.954 % | < ReduceDB 30 (14801 restarts, 157 cnfs/res, 25.0% reduced, 3b 9119g 15028g3) > | 2325001 | 2089 7388 34734 | 49443 15 8.8 38.3 | 9.954 % | | 2480001 | 2089 7388 34734 | 204443 19 14.0 37.7 | 9.954 % | < ReduceDB 31 (15196 restarts, 163 cnfs/res, 25.0% reduced, 3b 9676g 15951g3) > | 2480001 | 2089 7388 34734 | 51109 14 8.6 37.7 | 9.954 % | | 2640002 | 2089 7388 34734 | 211110 19 14.1 37.0 | 9.954 % | < ReduceDB 32 (15564 restarts, 170 cnfs/res, 25.0% reduced, 3b 10280g 16961g3) > | 2640002 | 2089 7388 34734 | 52776 14 8.6 37.0 | 9.954 % | | 2805001 | 2089 7388 34734 | 217775 19 14.4 36.4 | 9.954 % | < ReduceDB 33 (16008 restarts, 175 cnfs/res, 25.0% reduced, 3b 10917g 17577g3) > | 2805001 | 2089 7388 34734 | 54442 14 8.8 36.4 | 9.954 % | | 2975001 | 2089 7388 34734 | 224442 19 14.3 36.0 | 9.954 % | < ReduceDB 34 (16662 restarts, 179 cnfs/res, 25.0% reduced, 3b 11456g 18193g3) > | 2975001 | 2089 7388 34734 | 56109 15 8.7 36.0 | 9.954 % | | 3150003 | 2089 7388 34734 | 231111 19 14.4 35.6 | 9.954 % | < ReduceDB 35 (17413 restarts, 181 cnfs/res, 25.0% reduced, 3b 11971g 18957g3) > | 3150003 | 2089 7388 34734 | 57776 14 8.8 35.6 | 9.954 % | | 3330003 | 2089 7388 34734 | 237776 19 14.5 35.3 | 9.954 % | < ReduceDB 36 (18237 restarts, 183 cnfs/res, 25.0% reduced, 3b 12517g 19605g3) > | 3330003 | 2089 7388 34734 | 59443 14 8.5 35.3 | 9.954 % | | 3366612 | 2089 7388 34734 | 96052 16 10.9 35.1 | 9.954 % | | 3515001 | 2089 7388 34734 | 244441 19 14.2 34.8 | 9.954 % | < ReduceDB 37 (18744 restarts, 188 cnfs/res, 25.0% reduced, 3b 13064g 20300g3) > | 3515001 | 2089 7388 34734 | 61109 14 8.2 34.8 | 9.954 % | | 3705001 | 2089 7388 34734 | 251109 19 14.1 34.5 | 9.954 % | < ReduceDB 38 (19608 restarts, 189 cnfs/res, 25.0% reduced, 3b 13584g 20715g3) > | 3705001 | 2089 7388 34734 | 62776 14 8.4 34.5 | 9.954 % | | 3900001 | 2089 7388 34734 | 257776 19 14.1 34.1 | 9.954 % | < ReduceDB 39 (20190 restarts, 193 cnfs/res, 25.0% reduced, 3b 14117g 21284g3) > | 3900001 | 2089 7388 34734 | 64443 14 8.2 34.1 | 9.954 % | | 4100004 | 2089 7388 34734 | 264446 18 13.9 33.7 | 9.954 % | < ReduceDB 40 (20692 restarts, 198 cnfs/res, 25.0% reduced, 3b 14591g 21690g3) > | 4100004 | 2089 7388 34734 | 66110 14 8.3 33.7 | 9.954 % | | 4305003 | 2089 7388 34734 | 271109 18 14.1 33.3 | 9.954 % | < ReduceDB 41 (21406 restarts, 201 cnfs/res, 25.0% reduced, 3b 15063g 22158g3) > | 4305003 | 2089 7388 34734 | 67776 14 8.1 33.3 | 9.954 % | | 4515001 | 2089 7388 34734 | 277774 19 14.2 33.1 | 9.954 % | < ReduceDB 42 (22346 restarts, 202 cnfs/res, 25.0% reduced, 3b 15553g 22539g3) > | 4515001 | 2089 7388 34734 | 69442 15 8.5 33.1 | 9.954 % | | 4730001 | 2089 7388 34734 | 284442 19 14.5 32.8 | 9.954 % | < ReduceDB 43 (23203 restarts, 204 cnfs/res, 25.0% reduced, 3b 16045g 23031g3) > | 4730001 | 2089 7388 34734 | 71109 14 8.6 32.8 | 9.954 % | | 4950002 | 2089 7388 34734 | 291110 19 14.4 32.7 | 9.954 % | < ReduceDB 44 (24415 restarts, 203 cnfs/res, 25.0% reduced, 3b 16568g 23616g3) > | 4950002 | 2089 7388 34734 | 72776 14 8.4 32.7 | 9.954 % | | 5050023 | 2089 7388 34734 | 172797 17 12.9 32.5 | 9.954 % | | 5175001 | 2089 7388 34734 | 297775 19 14.4 32.4 | 9.954 % | < ReduceDB 45 (25193 restarts, 205 cnfs/res, 25.0% reduced, 3b 16962g 23914g3) > | 5175001 | 2089 7388 34734 | 74442 14 8.5 32.4 | 9.954 % | | 5405002 | 2089 7388 34734 | 304443 19 14.5 32.1 | 9.954 % | < ReduceDB 46 (26169 restarts, 207 cnfs/res, 25.0% reduced, 3b 17401g 24476g3) > | 5405002 | 2089 7388 34734 | 76109 14 8.3 32.1 | 9.954 % | | 5640001 | 2089 7388 34734 | 311108 19 14.4 31.9 | 9.954 % | < ReduceDB 47 (27225 restarts, 207 cnfs/res, 25.0% reduced, 3b 17865g 24828g3) > | 5640001 | 2089 7388 34734 | 77776 14 8.4 31.9 | 9.954 % | | 5880001 | 2089 7388 34734 | 317776 19 14.5 31.7 | 9.954 % | < ReduceDB 48 (28226 restarts, 208 cnfs/res, 25.0% reduced, 3b 18297g 25184g3) > | 5880001 | 2089 7388 34734 | 79443 14 8.5 31.7 | 9.954 % | | 6125002 | 2089 7388 34734 | 324444 18 14.0 31.4 | 9.954 % | < ReduceDB 49 (28846 restarts, 212 cnfs/res, 25.0% reduced, 3b 18627g 25407g3) > | 6125002 | 2089 7388 34734 | 81110 13 8.0 31.4 | 9.954 % | | 6375002 | 2089 7388 34734 | 331110 18 14.3 31.2 | 9.954 % | < ReduceDB 50 (29875 restarts, 213 cnfs/res, 25.0% reduced, 3b 19047g 25680g3) > | 6375002 | 2089 7388 34734 | 82776 14 8.7 31.2 | 9.954 % | | 6630001 | 2089 7388 34734 | 337775 18 14.3 31.0 | 9.954 % | < ReduceDB 51 (30505 restarts, 217 cnfs/res, 25.0% reduced, 3b 19463g 26021g3) > | 6630001 | 2089 7388 34734 | 84442 14 8.1 31.0 | 9.954 % | | 6890003 | 2089 7388 34734 | 344444 19 14.5 30.8 | 9.954 % | < ReduceDB 52 (31710 restarts, 217 cnfs/res, 25.0% reduced, 3b 19988g 26390g3) > | 6890003 | 2089 7388 34734 | 86110 14 8.6 30.8 | 9.954 % | | 7155001 | 2089 7388 34734 | 351108 19 14.4 30.7 | 9.954 % | < ReduceDB 53 (32851 restarts, 218 cnfs/res, 25.0% reduced, 3b 20430g 26970g3) > | 7155001 | 2089 7388 34734 | 87776 14 8.5 30.7 | 9.954 % | | 7425001 | 2089 7388 34734 | 357776 18 14.0 30.5 | 9.954 % | < ReduceDB 54 (33743 restarts, 220 cnfs/res, 25.0% reduced, 3b 20762g 27322g3) > | 7425001 | 2089 7388 34734 | 89443 14 7.9 30.5 | 9.954 % | | 7575139 | 2089 7388 34734 | 239581 18 12.9 30.4 | 9.954 % | | 7700001 | 2089 7388 34734 | 364443 18 13.9 30.3 | 9.954 % | < ReduceDB 55 (34682 restarts, 222 cnfs/res, 25.0% reduced, 3b 21149g 27661g3) > | 7700001 | 2089 7388 34734 | 91109 14 8.1 30.3 | 9.954 % | | 7980002 | 2089 7388 34734 | 371110 18 14.2 30.1 | 9.954 % | < ReduceDB 56 (35640 restarts, 224 cnfs/res, 25.0% reduced, 3b 21488g 27984g3) > | 7980002 | 2089 7388 34734 | 92776 14 8.5 30.1 | 9.954 % | | 8265002 | 2089 7388 34734 | 377776 18 14.4 30.0 | 9.954 % | < ReduceDB 57 (36849 restarts, 224 cnfs/res, 25.0% reduced, 3b 21892g 28351g3) > | 8265002 | 2089 7388 34734 | 94443 14 8.7 30.0 | 9.954 % | | 8555003 | 2089 7388 34734 | 384444 19 14.6 29.9 | 9.954 % | < ReduceDB 58 (38321 restarts, 223 cnfs/res, 25.0% reduced, 3b 22396g 28789g3) > | 8555003 | 2089 7388 34734 | 96110 14 8.5 29.9 | 9.954 % | | 8850001 | 2089 7388 34734 | 391108 18 13.9 29.7 | 9.954 % | < ReduceDB 59 (39214 restarts, 226 cnfs/res, 25.0% reduced, 3b 22774g 29363g3) > | 8850001 | 2089 7388 34734 | 97776 14 7.9 29.7 | 9.954 % | | 9150002 | 2089 7388 34734 | 397777 18 14.0 29.5 | 9.954 % | < ReduceDB 60 (40360 restarts, 227 cnfs/res, 25.0% reduced, 3b 23075g 29612g3) > | 9150002 | 2089 7388 34734 | 99443 14 8.2 29.5 | 9.954 % | | 9455001 | 2089 7388 34734 | 404442 18 14.3 29.4 | 9.954 % | < ReduceDB 61 (41675 restarts, 227 cnfs/res, 25.0% reduced, 3b 23460g 30003g3) > | 9455001 | 2089 7388 34734 | 101109 14 8.6 29.4 | 9.954 % | | 9765001 | 2089 7388 34734 | 411109 18 14.4 29.3 | 9.954 % | < ReduceDB 62 (43233 restarts, 226 cnfs/res, 25.0% reduced, 3b 23966g 30555g3) > | 9765001 | 2089 7388 34734 | 102776 14 8.6 29.3 | 9.954 % | | 10080003 | 2089 7388 34734 | 417778 19 14.6 29.2 | 9.954 % | < ReduceDB 63 (44816 restarts, 225 cnfs/res, 25.0% reduced, 3b 24315g 30853g3) > | 10080003 | 2089 7388 34734 | 104443 14 8.7 29.2 | 9.954 % | | 10400002 | 2089 7388 34734 | 424442 18 14.2 29.0 | 9.954 % | < ReduceDB 64 (45757 restarts, 227 cnfs/res, 25.0% reduced, 3b 24646g 31094g3) > | 10400002 | 2089 7388 34734 | 106109 14 8.9 29.0 | 9.954 % | | 10725002 | 2089 7388 34734 | 431109 18 14.4 28.9 | 9.954 % | < ReduceDB 65 (46714 restarts, 230 cnfs/res, 25.0% reduced, 3b 24980g 31363g3) > | 10725002 | 2089 7388 34734 | 107776 14 8.4 28.9 | 9.954 % | | 11055002 | 2089 7388 34734 | 437776 19 14.3 28.7 | 9.954 % | < ReduceDB 66 (47900 restarts, 231 cnfs/res, 25.0% reduced, 3b 25353g 31746g3) > | 11055002 | 2089 7388 34734 | 109443 14 9.0 28.7 | 9.954 % | | 11362814 | 2089 7388 34734 | 417255 18 14.3 28.7 | 9.954 % | | 11390001 | 2089 7388 34734 | 444442 18 14.4 28.6 | 9.954 % | < ReduceDB 67 (49346 restarts, 231 cnfs/res, 25.0% reduced, 3b 25661g 32035g3) > | 11390001 | 2089 7388 34734 | 111109 15 8.9 28.6 | 9.954 % | | 11730001 | 2089 7388 34734 | 451109 19 14.7 28.6 | 9.954 % | < ReduceDB 68 (50977 restarts, 230 cnfs/res, 25.0% reduced, 3b 26068g 32377g3) > | 11730001 | 2089 7388 34734 | 112776 14 8.8 28.6 | 9.954 % | | 12075001 | 2089 7388 34734 | 457776 19 14.8 28.5 | 9.954 % | < ReduceDB 69 (52876 restarts, 228 cnfs/res, 25.0% reduced, 3b 26432g 32845g3) > | 12075001 | 2089 7388 34734 | 114443 14 8.8 28.5 | 9.954 % | | 12425001 | 2089 7388 34734 | 464443 18 14.4 28.4 | 9.954 % | < ReduceDB 70 (54342 restarts, 229 cnfs/res, 25.0% reduced, 3b 26830g 33232g3) > | 12425001 | 2089 7388 34734 | 116109 14 8.9 28.4 | 9.954 % | | 12780003 | 2089 7388 34734 | 471111 19 14.6 28.3 | 9.954 % | < ReduceDB 71 (56515 restarts, 226 cnfs/res, 25.0% reduced, 3b 27216g 33782g3) > | 12780003 | 2089 7388 34734 | 117776 14 8.7 28.3 | 9.954 % | | 13140002 | 2089 7388 34734 | 477775 18 14.3 28.2 | 9.954 % | < ReduceDB 72 (57561 restarts, 228 cnfs/res, 25.0% reduced, 3b 27526g 34125g3) > | 13140002 | 2089 7388 34734 | 119442 14 8.8 28.2 | 9.954 % | | 13505001 | 2089 7388 34734 | 484441 19 14.6 28.1 | 9.954 % | < ReduceDB 73 (59307 restarts, 228 cnfs/res, 25.0% reduced, 3b 27912g 34343g3) > | 13505001 | 2089 7388 34734 | 121109 15 8.8 28.1 | 9.954 % | | 13875004 | 2089 7388 34734 | 491112 19 14.5 28.0 | 9.954 % | < ReduceDB 74 (60762 restarts, 228 cnfs/res, 25.0% reduced, 3b 28244g 34515g3) > | 13875004 | 2089 7388 34734 | 122777 14 9.0 28.0 | 9.954 % | | 14250001 | 2089 7388 34734 | 497774 19 14.7 28.0 | 9.954 % | < ReduceDB 75 (62638 restarts, 227 cnfs/res, 25.0% reduced, 3b 28801g 35087g3) > | 14250001 | 2089 7388 34734 | 124442 14 8.9 28.0 | 9.954 % | | 14630001 | 2089 7388 34734 | 504442 18 14.4 27.9 | 9.954 % | < ReduceDB 76 (64064 restarts, 228 cnfs/res, 25.0% reduced, 3b 29117g 35390g3) > | 14630001 | 2089 7388 34734 | 126109 14 8.7 27.9 | 9.954 % | | 15015001 | 2089 7388 34734 | 511109 18 14.5 27.8 | 9.954 % | < ReduceDB 77 (65781 restarts, 228 cnfs/res, 25.0% reduced, 3b 29471g 35674g3) > | 15015001 | 2089 7388 34734 | 127776 14 8.8 27.8 | 9.954 % | | 15405001 | 2089 7388 34734 | 517776 18 14.3 27.7 | 9.954 % | < ReduceDB 78 (67275 restarts, 229 cnfs/res, 25.0% reduced, 3b 29878g 36140g3) > | 15405001 | 2089 7388 34734 | 129443 15 9.2 27.7 | 9.954 % | | 15800001 | 2089 7388 34734 | 524443 18 14.1 27.6 | 9.954 % | < ReduceDB 79 (69264 restarts, 228 cnfs/res, 25.0% reduced, 3b 30281g 36535g3) > | 15800001 | 2089 7388 34734 | 131109 15 8.9 27.6 | 9.954 % | | 16200002 | 2089 7388 34734 | 531110 18 14.1 27.5 | 9.954 % | < ReduceDB 80 (70478 restarts, 230 cnfs/res, 25.0% reduced, 3b 30638g 36808g3) > | 16200002 | 2089 7388 34734 | 132776 15 9.0 27.5 | 9.954 % | | 16605001 | 2089 7388 34734 | 537775 18 14.3 27.4 | 9.954 % | < ReduceDB 81 (71931 restarts, 231 cnfs/res, 25.0% reduced, 3b 30990g 37188g3) > | 16605001 | 2089 7388 34734 | 134442 14 8.5 27.4 | 9.954 % | | 17015002 | 2089 7388 34734 | 544443 18 14.1 27.3 | 9.954 % | < ReduceDB 82 (72983 restarts, 233 cnfs/res, 25.0% reduced, 3b 31290g 37473g3) > | 17015002 | 2089 7388 34734 | 136109 14 8.8 27.3 | 9.954 % | | 17044326 | 2089 7388 34734 | 165433 15 10.1 27.3 | 9.954 % | | 17430001 | 2089 7388 34734 | 551108 18 14.0 27.2 | 9.954 % | < ReduceDB 83 (74523 restarts, 234 cnfs/res, 25.0% reduced, 3b 31553g 37975g3) > | 17430001 | 2089 7388 34734 | 137776 15 9.0 27.2 | 9.954 % | | 17850002 | 2089 7388 34734 | 557777 19 14.6 27.1 | 9.954 % | < ReduceDB 84 (76509 restarts, 233 cnfs/res, 25.0% reduced, 3b 31974g 38432g3) > | 17850002 | 2089 7388 34734 | 139443 15 9.0 27.1 | 9.954 % | | 18275001 | 2089 7388 34734 | 564442 18 14.2 27.0 | 9.954 % | < ReduceDB 85 (77825 restarts, 235 cnfs/res, 25.0% reduced, 3b 32250g 38649g3) > | 18275001 | 2089 7388 34734 | 141109 14 8.4 27.0 | 9.954 % | | 18564008 | 2089 7388 34734 | 430116 18 13.4 27.0 | 9.954 % | ==================================================================================== restarts : 79272 (17.83 /sec) (234.18 confs/res) conflicts : 18564008 (4174 /sec) decisions : 45166865 (0.00 % random) (10156 /sec) propagations : 1404317287 (315783 /sec) conflict literals : 373766825 (20.05 % deleted) average of lbd : 13.42 Memory used : 175.00 MB CPU time : 4447.09 s INDETERMINATE 15 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_15-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 15195 | | 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 | 2451 8318 38472 | 100 72 69.5 2250.9 | 10.388 % | | 250 | 2451 8318 38472 | 250 45 39.8 1225.4 | 10.388 % | | 475 | 2451 8318 38472 | 475 36 28.9 779.4 | 10.388 % | | 812 | 2451 8318 38472 | 812 32 23.7 570.3 | 10.388 % | | 1318 | 2451 8318 38472 | 1318 30 22.2 387.8 | 10.388 % | | 2077 | 2451 8318 38472 | 2077 28 21.0 277.5 | 10.388 % | | 3216 | 2451 8318 38472 | 3216 26 19.7 197.9 | 10.388 % | | 4924 | 2451 8318 38472 | 4924 26 19.0 148.9 | 10.388 % | | 5001 | 2451 8318 38472 | 5001 26 19.0 147.5 | 10.388 % | < ReduceDB 1 ( 6 restarts, 834 cnfs/res, 50.0% reduced, 0b 28g 112g3) > | 5001 | 2451 8318 38472 | 2503 22 15.3 147.5 | 10.388 % | | 6823 | 2451 8318 38472 | 4325 25 16.8 122.0 | 10.388 % | ==================================================================================== restarts : 6 (25.98 /sec) (1137.17 confs/res) conflicts : 6823 (29541 /sec) decisions : 19918 (0.00 % random) (86239 /sec) propagations : 539080 (2334043 /sec) conflict literals : 182251 (18.82 % deleted) average of lbd : 16.80 Memory used : 8.00 MB CPU time : 0.230964 s INDETERMINATE 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.03 Mb | | Simplification time: 0.02 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 5531 12450 41179 | 0 nan nan nan | 8.377 % | ==================================================================================== restarts : 1 (38.47 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 579 (22273 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 8.00 MB CPU time : 0.025996 s INDETERMINATE 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.02 Mb | | Simplification time: 0.01 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 5698 12702 41338 | 0 nan nan nan | 8.304 % | ==================================================================================== restarts : 1 (43.49 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 574 (24961 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 8.00 MB CPU time : 0.022996 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.02 Mb | | Simplification time: 0.01 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 5841 13200 43921 | 0 nan nan nan | 7.957 % | ==================================================================================== restarts : 1 (43.49 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 550 (23917 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 8.00 MB CPU time : 0.022996 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.02 Mb | | Simplification time: 0.01 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 5842 13191 43597 | 0 nan nan nan | 7.827 % | ==================================================================================== restarts : 1 (41.67 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 541 (22545 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 8.00 MB CPU time : 0.023996 s INDETERMINATE 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.03 Mb | | Simplification time: 0.01 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 5615 12896 43570 | 0 nan nan nan | 7.812 % | ==================================================================================== restarts : 1 (40.01 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 540 (21603 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 8.00 MB CPU time : 0.024996 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.02 Mb | | Simplification time: 0.01 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 5673 12989 43827 | 0 nan nan nan | 7.856 % | ==================================================================================== restarts : 1 (40.01 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 543 (21723 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 8.00 MB CPU time : 0.024996 s INDETERMINATE 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.03 Mb | | Simplification time: 0.02 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 5468 12704 43702 | 0 nan nan nan | 7.972 % | ==================================================================================== restarts : 1 (38.47 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 551 (21196 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 8.00 MB CPU time : 0.025996 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 | | Simplification time: 0.01 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 6387 14047 43961 | 0 nan nan nan | 7.595 % | ==================================================================================== restarts : 1 (45.46 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 525 (23868 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 8.00 MB CPU time : 0.021996 s INDETERMINATE 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.02 Mb | | Simplification time: 0.01 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 5759 13173 44288 | 0 nan nan nan | 7.595 % | ==================================================================================== restarts : 1 (43.49 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 525 (22830 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 8.00 MB CPU time : 0.022996 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.02 Mb | | Simplification time: 0.01 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 5662 12814 42501 | 0 nan nan nan | 8.145 % | ==================================================================================== restarts : 1 (45.46 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 563 (25596 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 8.00 MB CPU time : 0.021996 s INDETERMINATE 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.03 Mb | | Simplification time: 0.01 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 5593 12796 43117 | 0 nan nan nan | 7.943 % | ==================================================================================== restarts : 1 (38.47 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 549 (21119 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 8.00 MB CPU time : 0.025996 s INDETERMINATE 27 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_27-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 15213 | | Parse time: 0.01 s | | Eliminated clauses: 0.02 Mb | | Simplification time: 0.01 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 5869 12906 41255 | 0 nan nan nan | 8.464 % | ==================================================================================== restarts : 1 (45.46 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 585 (26596 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 8.00 MB CPU time : 0.021996 s INDETERMINATE 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.02 Mb | | Simplification time: 0.01 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 5768 12966 42486 | 0 nan nan nan | 7.841 % | ==================================================================================== restarts : 1 (43.49 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 542 (23569 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 8.00 MB CPU time : 0.022996 s INDETERMINATE 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.02 Mb | | Simplification time: 0.01 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 5702 12969 42834 | 0 nan nan nan | 7.624 % | ==================================================================================== restarts : 1 (43.49 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 527 (22917 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 8.00 MB CPU time : 0.022996 s INDETERMINATE 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 | | Eliminated clauses: 0.02 Mb | | Simplification time: 0.01 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 5604 12441 40384 | 0 nan nan nan | 9.433 % | ==================================================================================== restarts : 1 (40.01 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 652 (26084 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 8.00 MB CPU time : 0.024996 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.02 Mb | | Simplification time: 0.01 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 5490 12174 39247 | 0 nan nan nan | 10.851 % | ==================================================================================== restarts : 1 (43.49 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 750 (32614 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 8.00 MB CPU time : 0.022996 s INDETERMINATE 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.02 Mb | | Simplification time: 0.01 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 5531 12100 38606 | 0 nan nan nan | 11.560 % | ==================================================================================== restarts : 1 (41.67 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 799 (33297 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 8.00 MB CPU time : 0.023996 s INDETERMINATE 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.02 Mb | | Simplification time: 0.02 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 5764 13341 44942 | 0 nan nan nan | 7.407 % | ==================================================================================== restarts : 1 (37.04 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 512 (18966 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 8.00 MB CPU time : 0.026995 s INDETERMINATE