1 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_1-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 27512 | | 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 (11136 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 8.00 MB CPU time : 0.014997 s UNSATISFIABLE 2 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_2-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29132 | | Parse time: 0.02 s | | Eliminated clauses: 0.09 Mb | | Simplification time: 0.12 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 636 17628 101908 | 100 5 4.1 17.5 | 22.180 % | | 250 | 621 17628 101908 | 249 5 3.8 16.2 | 22.585 % | | 475 | 590 17628 101908 | 461 5 3.8 22.2 | 23.422 % | | 699 | 502 17628 101908 | 664 5 3.6 18.2 | 25.796 % | ==================================================================================== restarts : 5 (33.79 /sec) (139.80 confs/res) conflicts : 699 (4724 /sec) decisions : 2130 (0.00 % random) (14394 /sec) propagations : 19135 (129311 /sec) conflict literals : 3397 (19.35 % deleted) average of lbd : 3.58 Memory used : 10.00 MB CPU time : 0.147977 s UNSATISFIABLE 3 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_3-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29144 | | Parse time: 0.02 s | | Eliminated clauses: 0.15 Mb | | Simplification time: 0.17 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 642 18396 109460 | 100 5 4.1 19.6 | 20.319 % | | 250 | 610 18396 109460 | 246 5 3.3 16.4 | 21.182 % | | 475 | 563 18396 109460 | 460 5 3.4 17.2 | 22.450 % | | 812 | 322 18396 109460 | 780 5 3.6 18.5 | 28.953 % | | 1206 | 284 18396 109460 | 1165 5 3.7 22.6 | 29.978 % | ==================================================================================== restarts : 15 (78.55 /sec) (80.40 confs/res) conflicts : 1206 (6315 /sec) decisions : 3275 (0.00 % random) (17149 /sec) propagations : 19791 (103634 /sec) conflict literals : 5518 (10.70 % deleted) average of lbd : 3.70 Memory used : 10.00 MB CPU time : 0.19097 s UNSATISFIABLE 4 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_4-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29161 | | Parse time: 0.02 s | | Eliminated clauses: 0.17 Mb | | Simplification time: 0.19 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 641 17948 106932 | 100 5 3.8 17.8 | 18.295 % | | 250 | 612 17948 106932 | 248 5 3.3 17.0 | 19.077 % | | 475 | 593 17948 106932 | 470 5 3.3 18.2 | 19.590 % | | 812 | 554 17948 106932 | 797 5 3.6 19.9 | 20.642 % | | 1318 | 539 17948 106932 | 1299 6 4.2 29.1 | 21.047 % | | 2077 | 476 17948 106932 | 2044 6 4.4 33.2 | 22.747 % | | 2915 | 360 17948 106932 | 2864 6 4.3 32.3 | 25.877 % | ==================================================================================== restarts : 39 (161.85 /sec) (74.74 confs/res) conflicts : 2915 (12097 /sec) decisions : 9253 (0.00 % random) (38400 /sec) propagations : 56260 (233480 /sec) conflict literals : 17753 (10.78 % deleted) average of lbd : 4.29 Memory used : 10.00 MB CPU time : 0.240963 s UNSATISFIABLE 5 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_5-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29164 | | Parse time: 0.01 s | | Eliminated clauses: 0.20 Mb | | Simplification time: 0.23 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 641 17692 106068 | 100 5 3.8 17.8 | 18.025 % | | 250 | 612 17692 106068 | 248 5 3.3 17.0 | 18.807 % | | 475 | 611 17692 106068 | 472 5 3.6 20.4 | 18.834 % | | 812 | 593 17692 106068 | 805 6 4.3 34.7 | 19.320 % | | 1318 | 542 17692 106068 | 1306 6 4.7 43.1 | 20.696 % | | 2077 | 492 17692 106068 | 2054 6 4.9 49.4 | 22.045 % | | 2842 | 371 17692 106068 | 2803 6 4.7 43.1 | 25.310 % | ==================================================================================== restarts : 40 (140.87 /sec) (71.05 confs/res) conflicts : 2842 (10009 /sec) decisions : 9649 (0.00 % random) (33981 /sec) propagations : 58359 (205521 /sec) conflict literals : 18232 (10.72 % deleted) average of lbd : 4.65 Memory used : 11.00 MB CPU time : 0.283956 s UNSATISFIABLE 6 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_6-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29159 | | Parse time: 0.02 s | | Eliminated clauses: 0.21 Mb | | Simplification time: 0.22 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 641 18172 109844 | 100 5 3.8 17.8 | 17.782 % | | 250 | 612 18172 109844 | 248 5 3.3 17.0 | 18.564 % | | 475 | 593 18172 109844 | 469 5 3.4 19.6 | 19.077 % | | 812 | 509 18172 109844 | 792 5 3.8 29.9 | 21.344 % | | 1318 | 490 18172 109844 | 1290 5 4.2 38.4 | 21.856 % | | 2077 | 486 18172 109844 | 2046 6 4.5 43.1 | 21.964 % | | 3216 | 482 18172 109844 | 3181 7 4.5 34.6 | 22.072 % | | 4323 | 324 12821 78648 | 3338 7 4.7 27.6 | 26.336 % | ==================================================================================== restarts : 45 (143.79 /sec) (96.07 confs/res) conflicts : 4323 (13814 /sec) decisions : 11626 (0.00 % random) (37149 /sec) propagations : 97601 (311872 /sec) conflict literals : 30489 (21.68 % deleted) average of lbd : 4.67 Memory used : 11.00 MB CPU time : 0.312952 s UNSATISFIABLE 7 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_7-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29165 | | Parse time: 0.02 s | | Eliminated clauses: 0.23 Mb | | Simplification time: 0.25 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 619 18844 116340 | 90 5 4.0 30.4 | 17.647 % | | 250 | 613 18844 116340 | 237 5 3.3 23.2 | 17.809 % | | 475 | 568 18844 116340 | 456 5 3.4 21.9 | 19.023 % | | 812 | 519 18844 116340 | 784 5 4.2 38.8 | 20.345 % | | 1318 | 485 18844 116340 | 1281 6 4.8 52.5 | 21.263 % | | 2077 | 481 18844 116340 | 2038 6 5.0 50.9 | 21.371 % | | 3216 | 475 18844 116340 | 3172 7 5.0 42.5 | 21.533 % | | 4924 | 471 13142 81887 | 4312 9 5.4 32.4 | 21.641 % | | 5002 | 471 13142 81887 | 4390 9 5.4 32.0 | 21.641 % | < ReduceDB 1 ( 51 restarts, 98 cnfs/res, 50.0% reduced, 38b 568g 777g3) > | 5002 | 471 13142 81887 | 2195 8 4.0 32.0 | 21.641 % | | 7486 | 470 13142 81887 | 4678 9 4.9 24.5 | 21.668 % | | 8952 | 316 13011 81092 | 6120 9 4.8 21.6 | 25.823 % | ==================================================================================== restarts : 64 (127.51 /sec) (139.88 confs/res) conflicts : 8952 (17835 /sec) decisions : 18901 (0.00 % random) (37657 /sec) propagations : 279431 (556721 /sec) conflict literals : 81495 (28.08 % deleted) average of lbd : 4.79 Memory used : 11.00 MB CPU time : 0.501923 s UNSATISFIABLE 8 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_8-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29170 | | Parse time: 0.02 s | | Eliminated clauses: 0.23 Mb | | Simplification time: 0.24 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 645 18268 112244 | 100 5 4.0 18.8 | 16.946 % | | 250 | 618 18268 112244 | 239 5 3.8 17.2 | 17.674 % | | 475 | 605 18268 112244 | 460 5 3.8 20.5 | 18.025 % | | 812 | 550 18268 112244 | 786 5 4.1 28.5 | 19.509 % | | 1318 | 490 18268 112244 | 1279 6 4.7 45.3 | 21.128 % | | 2077 | 481 18268 112244 | 2035 6 5.1 57.7 | 21.371 % | | 3216 | 471 18268 112244 | 3170 7 5.4 63.0 | 21.641 % | | 4924 | 460 12823 79629 | 4287 7 5.8 60.6 | 21.937 % | | 5003 | 460 12823 79629 | 4366 7 5.8 60.4 | 21.937 % | < ReduceDB 1 ( 78 restarts, 64 cnfs/res, 50.0% reduced, 40b 314g 600g3) > | 5003 | 460 12823 79629 | 2183 7 4.7 60.4 | 21.937 % | | 7486 | 448 12823 79629 | 4659 8 5.4 54.8 | 22.261 % | | 11330 | 442 11898 73726 | 8373 11 6.2 47.9 | 22.423 % | | 15003 | 440 11898 73726 | 12044 12 6.6 44.3 | 22.477 % | < ReduceDB 2 ( 195 restarts, 77 cnfs/res, 50.0% reduced, 74b 1174g 2161g3) > | 15003 | 440 11898 73726 | 6024 9 4.6 44.3 | 22.477 % | | 17096 | 440 11393 70496 | 8065 11 5.3 42.5 | 22.477 % | | 25745 | 436 10909 67478 | 16622 14 6.5 37.0 | 22.585 % | | 30001 | 436 10909 67478 | 20878 14 6.6 35.2 | 22.585 % | < ReduceDB 3 ( 307 restarts, 98 cnfs/res, 50.0% reduced, 84b 2557g 3480g3) > | 30001 | 436 10909 67478 | 10439 10 4.6 35.2 | 22.585 % | | 38719 | 436 10909 67478 | 19157 13 6.0 32.7 | 22.585 % | | 50002 | 435 10763 66554 | 30420 15 6.6 30.2 | 22.612 % | < ReduceDB 4 ( 414 restarts, 121 cnfs/res, 50.0% reduced, 90b 3696g 4932g3) > | 50002 | 435 10763 66554 | 15211 10 4.7 30.2 | 22.612 % | | 58180 | 435 10763 66554 | 23389 13 5.7 29.0 | 22.612 % | | 75002 | 432 10609 65620 | 37708 14 6.3 25.9 | 22.693 % | < ReduceDB 5 ( 513 restarts, 146 cnfs/res, 50.0% reduced, 92b 5454g 5867g3) > | 75002 | 432 10609 65620 | 18854 10 4.5 25.9 | 22.693 % | | 84607 | 298 10458 64706 | 24178 10 4.8 24.0 | 26.309 % | ==================================================================================== restarts : 520 (108.55 /sec) (162.71 confs/res) conflicts : 84607 (17662 /sec) decisions : 146679 (0.00 % random) (30620 /sec) propagations : 2407474 (502576 /sec) conflict literals : 1249298 (24.28 % deleted) average of lbd : 4.78 Memory used : 13.00 MB CPU time : 4.79027 s UNSATISFIABLE 9 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_9-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29163 | | Parse time: 0.02 s | | Eliminated clauses: 0.24 Mb | | Simplification time: 0.24 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 619 17788 108916 | 90 5 4.0 30.4 | 17.701 % | | 250 | 613 17788 108916 | 237 5 3.3 23.2 | 17.863 % | | 475 | 574 17788 108916 | 455 5 3.9 30.7 | 18.915 % | | 812 | 500 17788 108916 | 773 5 4.3 38.7 | 20.912 % | | 1318 | 489 17788 108916 | 1274 6 4.8 54.1 | 21.209 % | | 2077 | 485 17788 108916 | 2031 6 5.3 64.5 | 21.317 % | | 3216 | 481 17788 108916 | 3169 7 5.5 64.7 | 21.425 % | | 4924 | 476 17788 108916 | 4874 7 5.6 62.5 | 21.560 % | | 5001 | 476 17788 108916 | 4951 7 5.6 62.2 | 21.560 % | < ReduceDB 1 ( 77 restarts, 65 cnfs/res, 50.3% reduced, 98b 454g 744g3) > | 5001 | 476 17788 108916 | 2491 6 4.3 62.2 | 21.560 % | | 7486 | 464 13272 82051 | 4697 8 5.6 59.0 | 21.883 % | | 11330 | 457 12688 78407 | 8457 10 6.5 50.3 | 22.072 % | | 15001 | 454 12348 76246 | 12095 12 7.0 45.6 | 22.153 % | < ReduceDB 2 ( 213 restarts, 70 cnfs/res, 50.0% reduced, 66b 1228g 2029g3) > | 15001 | 454 12348 76246 | 6047 9 5.1 45.6 | 22.153 % | | 17096 | 454 12348 76246 | 8142 11 6.1 43.5 | 22.153 % | | 25745 | 448 12154 75026 | 16740 15 7.6 37.1 | 22.315 % | | 30001 | 448 12154 75026 | 20996 15 7.9 35.0 | 22.315 % | < ReduceDB 3 ( 358 restarts, 84 cnfs/res, 50.0% reduced, 69b 2161g 3233g3) > | 30001 | 448 12154 75026 | 10498 11 5.4 35.0 | 22.315 % | | 38719 | 447 12023 74213 | 19190 14 7.4 32.5 | 22.342 % | | 50001 | 447 11903 73493 | 30450 16 8.1 29.9 | 22.342 % | < ReduceDB 4 ( 509 restarts, 98 cnfs/res, 50.0% reduced, 67b 3027g 4180g3) > | 50001 | 447 11903 73493 | 15225 12 5.7 29.9 | 22.342 % | | 58180 | 447 11903 73493 | 23404 14 7.2 28.7 | 22.343 % | | 75003 | 447 11903 73493 | 40227 16 8.3 26.9 | 22.342 % | < ReduceDB 5 ( 697 restarts, 108 cnfs/res, 50.0% reduced, 70b 3936g 5103g3) > | 75003 | 447 11903 73493 | 20113 12 6.1 26.9 | 22.342 % | | 87372 | 447 11903 73493 | 32482 14 7.6 25.7 | 22.342 % | | 105003 | 447 11903 73493 | 50113 15 8.4 24.3 | 22.342 % | < ReduceDB 6 ( 847 restarts, 124 cnfs/res, 50.0% reduced, 71b 5088g 6140g3) > | 105003 | 447 11903 73493 | 25056 12 6.2 24.3 | 22.342 % | | 131161 | 445 11718 72383 | 46326 14 7.8 22.4 | 22.396 % | | 140002 | 445 11718 72383 | 55167 14 8.0 21.9 | 22.396 % | < ReduceDB 7 ( 948 restarts, 148 cnfs/res, 50.0% reduced, 62b 6276g 6971g3) > | 140002 | 445 11718 72383 | 27583 11 5.9 21.9 | 22.396 % | | 180001 | 445 11718 72383 | 67582 13 7.9 20.0 | 22.396 % | < ReduceDB 8 (1031 restarts, 175 cnfs/res, 44.9% reduced, 62b 7323g 7824g3) > | 180001 | 445 11718 72383 | 30351 10 5.6 20.0 | 22.396 % | | 196845 | 445 11718 72383 | 47195 12 6.9 19.5 | 22.396 % | | 225002 | 445 11718 72383 | 75352 13 7.7 18.7 | 22.396 % | < ReduceDB 9 (1110 restarts, 203 cnfs/res, 44.9% reduced, 63b 8416g 8821g3) > | 225002 | 445 11718 72383 | 33837 10 5.5 18.7 | 22.396 % | | 275002 | 445 11718 72383 | 83837 12 7.3 17.4 | 22.396 % | < ReduceDB 10 (1160 restarts, 237 cnfs/res, 42.3% reduced, 65b 9373g 9738g3) > | 275002 | 445 11718 72383 | 35448 10 5.1 17.4 | 22.396 % | | 295371 | 444 11624 71819 | 38334 10 5.3 16.9 | 22.423 % | | 308987 | 401 11441 70721 | 31949 9 4.6 16.5 | 23.583 % | ==================================================================================== restarts : 1160 (44.76 /sec) (266.37 confs/res) conflicts : 308987 (11923 /sec) decisions : 429009 (0.00 % random) (16554 /sec) propagations : 9297746 (358778 /sec) conflict literals : 4593055 (26.58 % deleted) average of lbd : 4.62 Memory used : 26.00 MB CPU time : 25.9151 s UNSATISFIABLE 10 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_10-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29159 | | Parse time: 0.01 s | | Eliminated clauses: 0.23 Mb | | Simplification time: 0.14 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 620 17948 110228 | 88 5 3.7 30.2 | 17.377 % | | 250 | 616 17948 110228 | 235 4 3.4 24.5 | 17.485 % | | 475 | 600 17948 110228 | 455 5 4.0 31.3 | 17.917 % | | 812 | 333 17948 110228 | 785 6 4.9 53.5 | 25.121 % | | 1318 | 333 17948 110228 | 1291 6 5.1 58.7 | 25.121 % | | 2077 | 333 17948 110228 | 2050 6 5.4 62.1 | 25.121 % | | 3216 | 333 17948 110228 | 3189 6 5.5 64.3 | 25.121 % | | 4924 | 331 17948 110228 | 4895 7 5.6 64.2 | 25.175 % | | 5001 | 331 17948 110228 | 4972 7 5.6 64.1 | 25.175 % | < ReduceDB 1 ( 77 restarts, 65 cnfs/res, 50.0% reduced, 69b 484g 749g3) > | 5001 | 331 17948 110228 | 2488 6 4.4 64.1 | 25.175 % | | 7486 | 329 11937 73586 | 4718 7 5.6 60.1 | 25.229 % | | 11330 | 327 11459 70670 | 8487 11 7.1 52.0 | 25.283 % | | 15001 | 327 11459 70670 | 12158 13 7.9 46.8 | 25.283 % | < ReduceDB 2 ( 235 restarts, 64 cnfs/res, 50.0% reduced, 38b 1580g 1863g3) > | 15001 | 327 11459 70670 | 6081 9 5.3 46.8 | 25.283 % | | 17096 | 327 11459 70670 | 8176 11 6.6 44.7 | 25.283 % | | 25745 | 327 11459 70670 | 16825 15 8.7 39.2 | 25.283 % | | 30002 | 327 11459 70670 | 21082 16 9.2 37.4 | 25.283 % | < ReduceDB 3 ( 414 restarts, 72 cnfs/res, 50.0% reduced, 45b 2767g 2847g3) > | 30002 | 327 11459 70670 | 10541 11 6.0 37.4 | 25.283 % | | 38719 | 327 11459 70670 | 19258 15 8.2 35.0 | 25.283 % | | 50001 | 327 11459 70670 | 30540 17 9.2 32.5 | 25.283 % | < ReduceDB 4 ( 543 restarts, 92 cnfs/res, 50.0% reduced, 52b 3797g 3710g3) > | 50001 | 327 11459 70670 | 15270 12 6.4 32.5 | 25.283 % | | 58180 | 327 11459 70670 | 23449 15 8.2 31.5 | 25.283 % | | 75001 | 327 11459 70670 | 40270 17 9.4 29.9 | 25.283 % | < ReduceDB 5 ( 708 restarts, 106 cnfs/res, 50.0% reduced, 57b 5029g 4609g3) > | 75001 | 327 11459 70670 | 20135 12 6.7 29.9 | 25.283 % | | 87372 | 327 11459 70670 | 32506 16 8.5 29.1 | 25.283 % | | 105001 | 326 11339 69939 | 50113 17 9.6 28.3 | 25.310 % | < ReduceDB 6 ( 921 restarts, 114 cnfs/res, 50.0% reduced, 57b 6053g 5391g3) > | 105001 | 326 11339 69939 | 25056 13 7.1 28.3 | 25.310 % | | 131161 | 326 11339 69939 | 51216 17 9.4 27.2 | 25.310 % | | 140001 | 326 11339 69939 | 60056 17 9.8 26.8 | 25.310 % | < ReduceDB 7 (1117 restarts, 125 cnfs/res, 45.6% reduced, 59b 6978g 6186g3) > | 140001 | 326 11339 69939 | 27389 12 6.9 26.8 | 25.310 % | | 180001 | 326 11339 69939 | 67389 16 9.3 25.3 | 25.310 % | < ReduceDB 8 (1245 restarts, 145 cnfs/res, 44.3% reduced, 59b 8567g 7415g3) > | 180001 | 326 11339 69939 | 29854 11 6.1 25.3 | 25.310 % | | 196845 | 326 11339 69939 | 46698 14 7.5 24.7 | 25.310 % | | 225001 | 326 11339 69939 | 74854 16 8.6 23.8 | 25.310 % | < ReduceDB 9 (1353 restarts, 166 cnfs/res, 44.6% reduced, 60b 9855g 8718g3) > | 225001 | 326 11339 69939 | 33387 11 5.8 23.8 | 25.310 % | | 275003 | 326 11339 69939 | 83389 16 9.0 22.8 | 25.310 % | < ReduceDB 10 (1542 restarts, 178 cnfs/res, 43.7% reduced, 62b 11388g 9723g3) > | 275003 | 326 11339 69939 | 36444 11 5.8 22.8 | 25.310 % | | 295371 | 326 11339 69939 | 56812 14 7.5 22.4 | 25.310 % | | 330001 | 326 11339 69939 | 91442 15 8.8 21.9 | 25.310 % | < ReduceDB 11 (1735 restarts, 190 cnfs/res, 42.0% reduced, 62b 12518g 10600g3) > | 330001 | 326 11339 69939 | 38377 11 5.5 21.9 | 25.310 % | | 390001 | 325 11220 69213 | 98359 15 8.6 21.2 | 25.337 % | < ReduceDB 12 (1961 restarts, 199 cnfs/res, 41.4% reduced, 59b 13817g 11700g3) > | 390001 | 325 11220 69213 | 40714 10 5.2 21.2 | 25.337 % | | 443160 | 325 11220 69213 | 93873 15 8.2 20.6 | 25.337 % | | 455002 | 325 11220 69213 | 105715 15 8.5 20.5 | 25.337 % | < ReduceDB 13 (2181 restarts, 209 cnfs/res, 41.9% reduced, 59b 15048g 12615g3) > | 455002 | 325 11220 69213 | 44283 11 5.3 20.5 | 25.337 % | | 525003 | 325 11220 69213 | 114284 15 8.6 19.9 | 25.337 % | < ReduceDB 14 (2417 restarts, 217 cnfs/res, 40.5% reduced, 59b 16450g 13371g3) > | 525003 | 325 11220 69213 | 46264 10 5.1 19.9 | 25.337 % | | 600001 | 325 11220 69213 | 121262 15 8.7 19.5 | 25.337 % | < ReduceDB 15 (2700 restarts, 222 cnfs/res, 39.7% reduced, 59b 17296g 14406g3) > | 600001 | 325 11220 69213 | 48088 10 5.0 19.5 | 25.337 % | | 664843 | 325 11220 69213 | 112930 15 8.4 19.2 | 25.337 % | | 680001 | 325 11220 69213 | 128088 15 8.8 19.1 | 25.337 % | < ReduceDB 16 (3055 restarts, 223 cnfs/res, 39.5% reduced, 59b 18294g 15273g3) > | 680001 | 325 11220 69213 | 50643 10 5.0 19.1 | 25.337 % | | 765002 | 325 11220 69213 | 135644 15 8.7 18.7 | 25.337 % | < ReduceDB 17 (3346 restarts, 229 cnfs/res, 39.0% reduced, 59b 19317g 16086g3) > | 765002 | 325 11220 69213 | 52953 10 5.0 18.7 | 25.337 % | | 855001 | 325 11220 69213 | 142952 15 8.8 18.4 | 25.337 % | < ReduceDB 18 (3802 restarts, 225 cnfs/res, 38.5% reduced, 59b 20506g 16973g3) > | 855001 | 325 11220 69213 | 55049 10 4.9 18.4 | 25.337 % | | 950002 | 325 11220 69213 | 150050 15 8.9 18.2 | 25.337 % | < ReduceDB 19 (4341 restarts, 219 cnfs/res, 38.2% reduced, 59b 21480g 17877g3) > | 950002 | 325 11220 69213 | 57389 10 4.7 18.2 | 25.337 % | | 997368 | 325 11220 69213 | 104755 13 7.8 18.1 | 25.337 % | | 1050001 | 325 11220 69213 | 157388 14 8.7 17.9 | 25.337 % | < ReduceDB 20 (4863 restarts, 216 cnfs/res, 37.0% reduced, 59b 22490g 18554g3) > | 1050001 | 325 11220 69213 | 58224 10 4.7 17.9 | 25.337 % | | 1155002 | 325 11220 69213 | 163225 14 8.5 17.6 | 25.337 % | < ReduceDB 21 (5270 restarts, 219 cnfs/res, 37.7% reduced, 60b 23686g 19499g3) > | 1155002 | 325 11220 69213 | 61494 10 4.6 17.6 | 25.337 % | | 1265001 | 324 11156 68821 | 150843 14 8.6 17.4 | 25.364 % | < ReduceDB 22 (5785 restarts, 219 cnfs/res, 40.2% reduced, 57b 23431g 18644g3) > | 1265001 | 324 11156 68821 | 60636 10 4.6 17.4 | 25.364 % | | 1380002 | 324 11156 68821 | 175637 14 8.8 17.1 | 25.364 % | < ReduceDB 23 (6267 restarts, 220 cnfs/res, 36.4% reduced, 57b 24406g 19689g3) > | 1380002 | 324 11156 68821 | 63905 10 4.6 17.1 | 25.364 % | | 1496156 | 324 11156 68821 | 180059 13 8.3 16.9 | 25.364 % | | 1500004 | 324 11156 68821 | 183907 13 8.4 16.9 | 25.364 % | < ReduceDB 24 (6717 restarts, 223 cnfs/res, 36.0% reduced, 57b 25340g 21076g3) > | 1500004 | 324 11156 68821 | 66169 10 4.5 16.9 | 25.364 % | | 1625002 | 324 11156 68821 | 191167 13 8.1 16.6 | 25.364 % | < ReduceDB 25 (6966 restarts, 233 cnfs/res, 35.7% reduced, 57b 26370g 22291g3) > | 1625002 | 324 11156 68821 | 68317 10 4.3 16.6 | 25.364 % | | 1732835 | 222 11062 68257 | 153501 11 7.0 16.2 | 28.117 % | ==================================================================================== restarts : 6982 (26.55 /sec) (248.19 confs/res) conflicts : 1732835 (6589 /sec) decisions : 2150731 (0.00 % random) (8178 /sec) propagations : 35537511 (135129 /sec) conflict literals : 29021672 (18.49 % deleted) average of lbd : 6.95 Memory used : 56.00 MB CPU time : 262.989 s UNSATISFIABLE 11 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_11-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29179 | | Parse time: 0.01 s | | Eliminated clauses: 0.27 Mb | | Simplification time: 0.18 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 619 17852 110324 | 90 5 4.0 30.4 | 16.676 % | | 250 | 613 17852 110324 | 237 5 3.3 23.2 | 16.838 % | | 475 | 584 17852 110324 | 456 5 3.9 27.7 | 17.620 % | | 812 | 518 17852 110324 | 786 6 4.7 48.4 | 19.401 % | | 1318 | 496 17852 110324 | 1282 7 5.4 59.9 | 19.995 % | | 2077 | 488 17852 110324 | 2036 7 5.7 69.2 | 20.210 % | | 3216 | 480 17852 110324 | 3170 7 6.0 75.5 | 20.426 % | | 4924 | 478 17852 110324 | 4876 8 6.2 77.0 | 20.480 % | | 5004 | 478 17852 110324 | 4956 8 6.3 77.3 | 20.480 % | < ReduceDB 1 ( 85 restarts, 59 cnfs/res, 50.2% reduced, 69b 300g 609g3) > | 5004 | 478 17852 110324 | 2486 6 5.1 77.3 | 20.480 % | | 7486 | 471 13217 81956 | 4723 8 6.2 78.8 | 20.669 % | | 11330 | 471 13106 81229 | 8562 8 6.7 77.4 | 20.669 % | | 15001 | 466 13106 81229 | 12229 9 7.0 75.5 | 20.804 % | < ReduceDB 2 ( 222 restarts, 68 cnfs/res, 50.0% reduced, 59b 656g 1582g3) > | 15001 | 466 13106 81229 | 6120 8 5.7 75.5 | 20.804 % | | 17096 | 466 12951 80321 | 8191 9 6.4 74.2 | 20.804 % | | 25745 | 442 12617 78230 | 16747 13 7.8 68.7 | 21.452 % | | 30001 | 440 12617 78230 | 21002 14 8.2 66.3 | 21.506 % | < ReduceDB 3 ( 444 restarts, 68 cnfs/res, 50.0% reduced, 80b 1517g 3078g3) > | 30001 | 440 12617 78230 | 10506 10 5.8 66.3 | 21.506 % | | 38719 | 438 11277 69868 | 18939 15 8.0 63.2 | 21.560 % | | 50002 | 438 11277 69868 | 30222 18 9.2 60.0 | 21.560 % | < ReduceDB 4 ( 709 restarts, 71 cnfs/res, 50.0% reduced, 65b 2467g 4813g3) > | 50002 | 438 11277 69868 | 15116 12 6.1 60.0 | 21.560 % | | 58180 | 438 11277 69868 | 23294 16 7.8 58.3 | 21.560 % | | 75001 | 436 11261 69783 | 40114 20 9.2 55.2 | 21.614 % | < ReduceDB 5 ( 945 restarts, 79 cnfs/res, 50.0% reduced, 69b 3839g 6187g3) > | 75001 | 436 11261 69783 | 20060 13 6.1 55.2 | 21.614 % | | 87372 | 436 11261 69783 | 32431 18 7.9 53.7 | 21.614 % | | 105001 | 436 11261 69783 | 50060 21 8.9 51.9 | 21.614 % | < ReduceDB 6 (1126 restarts, 93 cnfs/res, 50.0% reduced, 70b 5009g 7587g3) > | 105001 | 436 11261 69783 | 25031 14 6.1 51.9 | 21.614 % | | 131161 | 436 11261 69783 | 51191 20 8.8 49.8 | 21.614 % | | 140003 | 436 11261 69783 | 60033 21 9.1 49.2 | 21.614 % | < ReduceDB 7 (1359 restarts, 103 cnfs/res, 50.0% reduced, 70b 6249g 8895g3) > | 140003 | 436 11261 69783 | 30017 15 6.1 49.2 | 21.614 % | | 180001 | 436 11261 69783 | 70015 21 9.3 47.1 | 21.614 % | < ReduceDB 8 (1638 restarts, 110 cnfs/res, 49.0% reduced, 74b 7377g 10037g3) > | 180001 | 436 11261 69783 | 34317 14 6.3 47.1 | 21.614 % | | 196845 | 435 11139 69035 | 51137 19 7.9 46.5 | 21.641 % | | 225002 | 435 11139 69035 | 79294 22 9.0 45.6 | 21.641 % | < ReduceDB 9 (1857 restarts, 121 cnfs/res, 45.1% reduced, 72b 8396g 11171g3) > | 225002 | 435 11139 69035 | 35728 14 5.7 45.6 | 21.641 % | | 275004 | 434 11017 68287 | 85686 21 9.1 44.2 | 21.668 % | < ReduceDB 10 (2177 restarts, 126 cnfs/res, 45.6% reduced, 75b 9547g 12137g3) > | 275004 | 434 11017 68287 | 39089 14 5.9 44.2 | 21.668 % | | 295371 | 434 11017 68287 | 59456 19 7.8 43.7 | 21.668 % | | 330001 | 434 11017 68287 | 94086 22 9.3 43.1 | 21.668 % | < ReduceDB 11 (2546 restarts, 130 cnfs/res, 44.6% reduced, 77b 10563g 13277g3) > | 330001 | 434 11017 68287 | 41983 14 5.8 43.1 | 21.668 % | | 390002 | 434 11017 68287 | 101984 21 9.1 42.1 | 21.668 % | < ReduceDB 12 (2872 restarts, 136 cnfs/res, 43.7% reduced, 77b 11608g 14364g3) > | 390002 | 434 11017 68287 | 44547 14 5.5 42.1 | 21.668 % | | 443160 | 434 11017 68287 | 97705 21 8.6 41.3 | 21.668 % | | 455002 | 434 11017 68287 | 109547 21 8.9 41.1 | 21.668 % | < ReduceDB 13 (3240 restarts, 140 cnfs/res, 42.9% reduced, 78b 12806g 15453g3) > | 455002 | 434 11017 68287 | 47006 13 5.4 41.1 | 21.668 % | | 525001 | 434 11017 68287 | 117005 21 9.1 40.3 | 21.668 % | < ReduceDB 14 (3680 restarts, 143 cnfs/res, 42.1% reduced, 82b 13924g 16431g3) > | 525001 | 434 11017 68287 | 49265 13 5.4 40.3 | 21.668 % | | 600004 | 434 11017 68287 | 124268 21 9.1 39.5 | 21.668 % | < ReduceDB 15 (4118 restarts, 146 cnfs/res, 41.7% reduced, 84b 14915g 17463g3) > | 600004 | 434 11017 68287 | 51843 13 5.3 39.5 | 21.668 % | | 664843 | 434 11017 68287 | 116682 20 8.5 38.8 | 21.668 % | | 680001 | 434 11017 68287 | 131840 21 8.8 38.7 | 21.668 % | < ReduceDB 16 (4481 restarts, 152 cnfs/res, 40.2% reduced, 85b 15899g 18452g3) > | 680001 | 434 11017 68287 | 53007 13 5.0 38.7 | 21.668 % | | 765001 | 434 11017 68287 | 138007 21 9.1 38.2 | 21.668 % | < ReduceDB 17 (5063 restarts, 151 cnfs/res, 39.7% reduced, 86b 16909g 19458g3) > | 765001 | 434 11017 68287 | 54847 13 5.0 38.2 | 21.668 % | | 855002 | 434 11017 68287 | 144848 21 9.0 37.6 | 21.668 % | < ReduceDB 18 (5596 restarts, 153 cnfs/res, 38.2% reduced, 88b 17896g 20418g3) > | 855002 | 434 11017 68287 | 55338 13 4.9 37.6 | 21.668 % | | 950001 | 434 11017 68287 | 150337 21 8.9 37.1 | 21.668 % | < ReduceDB 19 (6090 restarts, 156 cnfs/res, 38.1% reduced, 89b 18927g 21319g3) > | 950001 | 434 11017 68287 | 57307 12 4.9 37.1 | 21.668 % | | 997368 | 434 11017 68287 | 104674 18 7.9 36.9 | 21.668 % | | 1050001 | 434 11017 68287 | 157307 21 9.1 36.6 | 21.668 % | < ReduceDB 20 (6752 restarts, 156 cnfs/res, 39.2% reduced, 90b 19955g 22253g3) > | 1050001 | 434 11017 68287 | 61650 12 5.0 36.6 | 21.668 % | | 1155003 | 434 11017 68287 | 166652 21 9.1 36.2 | 21.668 % | < ReduceDB 21 (7446 restarts, 155 cnfs/res, 38.2% reduced, 92b 21073g 23393g3) > | 1155003 | 434 11017 68287 | 63598 12 4.8 36.2 | 21.668 % | | 1265001 | 434 11017 68287 | 173596 20 9.0 35.8 | 21.668 % | < ReduceDB 22 (8169 restarts, 155 cnfs/res, 38.2% reduced, 96b 21946g 24342g3) > | 1265001 | 434 11017 68287 | 66323 12 4.7 35.8 | 21.668 % | | 1380001 | 434 11017 68287 | 181323 21 9.1 35.4 | 21.668 % | < ReduceDB 23 (8952 restarts, 154 cnfs/res, 37.3% reduced, 98b 22879g 25424g3) > | 1380001 | 434 11017 68287 | 67680 12 4.6 35.4 | 21.668 % | | 1496156 | 434 11017 68287 | 183835 20 9.2 35.2 | 21.668 % | | 1500003 | 434 11017 68287 | 187682 21 9.2 35.1 | 21.668 % | < ReduceDB 24 (9871 restarts, 152 cnfs/res, 37.2% reduced, 99b 24032g 26630g3) > | 1500003 | 434 11017 68287 | 69909 12 4.6 35.1 | 21.668 % | | 1625002 | 434 11017 68287 | 194908 20 9.0 34.8 | 21.668 % | < ReduceDB 25 (10703 restarts, 152 cnfs/res, 37.6% reduced, 99b 25202g 27629g3) > | 1625002 | 434 11017 68287 | 73281 12 4.7 34.8 | 21.668 % | | 1755002 | 434 11017 68287 | 203281 20 9.0 34.5 | 21.668 % | < ReduceDB 26 (11621 restarts, 151 cnfs/res, 38.1% reduced, 101b 26231g 28775g3) > | 1755002 | 434 11017 68287 | 77353 13 4.7 34.5 | 21.668 % | | 1890001 | 433 10892 67524 | 212270 20 9.1 34.3 | 21.695 % | < ReduceDB 27 (12658 restarts, 149 cnfs/res, 36.5% reduced, 97b 27267g 29601g3) > | 1890001 | 433 10892 67524 | 77563 12 4.5 34.3 | 21.695 % | | 2030006 | 433 10892 67524 | 217568 20 9.1 34.1 | 21.695 % | < ReduceDB 28 (13618 restarts, 149 cnfs/res, 35.9% reduced, 97b 28368g 30622g3) > | 2030006 | 433 10892 67524 | 78035 12 4.4 34.1 | 21.695 % | | 2175001 | 433 10892 67524 | 223030 20 9.1 33.9 | 21.695 % | < ReduceDB 29 (14677 restarts, 148 cnfs/res, 36.6% reduced, 98b 29415g 31720g3) > | 2175001 | 433 10892 67524 | 81685 12 4.4 33.9 | 21.695 % | | 2244338 | 433 10892 67524 | 151022 18 7.5 33.7 | 21.695 % | | 2325003 | 433 10892 67524 | 231687 20 8.9 33.6 | 21.695 % | < ReduceDB 30 (15739 restarts, 148 cnfs/res, 35.9% reduced, 99b 30641g 32913g3) > | 2325003 | 433 10892 67524 | 83271 12 4.4 33.6 | 21.695 % | | 2480002 | 433 10892 67524 | 238270 20 8.8 33.4 | 21.695 % | < ReduceDB 31 (16764 restarts, 148 cnfs/res, 36.8% reduced, 102b 31872g 33955g3) > | 2480002 | 433 10892 67524 | 87757 12 4.4 33.4 | 21.695 % | | 2640003 | 433 10892 67524 | 247758 20 8.9 33.1 | 21.695 % | < ReduceDB 32 (17622 restarts, 150 cnfs/res, 36.3% reduced, 103b 33053g 35402g3) > | 2640003 | 433 10892 67524 | 89910 12 4.1 33.1 | 21.695 % | | 2805001 | 433 10892 67524 | 254908 20 8.6 32.8 | 21.695 % | < ReduceDB 33 (18421 restarts, 152 cnfs/res, 35.1% reduced, 103b 34142g 36400g3) > | 2805001 | 433 10892 67524 | 89418 11 4.1 32.8 | 21.695 % | | 2975002 | 433 10892 67524 | 259419 20 8.9 32.6 | 21.695 % | < ReduceDB 34 (19735 restarts, 151 cnfs/res, 35.9% reduced, 103b 35419g 37473g3) > | 2975002 | 433 10892 67524 | 93180 12 4.0 32.6 | 21.695 % | | 3150001 | 433 10892 67524 | 268179 20 8.9 32.3 | 21.695 % | < ReduceDB 35 (20974 restarts, 150 cnfs/res, 34.9% reduced, 103b 36517g 38450g3) > | 3150001 | 433 10892 67524 | 93516 11 4.0 32.3 | 21.695 % | | 3330003 | 433 10892 67524 | 273518 20 8.8 32.2 | 21.695 % | < ReduceDB 36 (22277 restarts, 149 cnfs/res, 35.6% reduced, 103b 37826g 39610g3) > | 3330003 | 433 10892 67524 | 97340 12 3.8 32.2 | 21.695 % | | 3366612 | 433 10892 67524 | 133949 15 5.9 32.1 | 21.695 % | | 3515001 | 433 10892 67524 | 282338 20 8.9 32.0 | 21.695 % | < ReduceDB 37 (23744 restarts, 148 cnfs/res, 35.6% reduced, 104b 39036g 40724g3) > | 3515001 | 433 10892 67524 | 100564 12 4.1 32.0 | 21.695 % | | 3705002 | 433 10892 67524 | 290565 19 8.8 31.8 | 21.695 % | < ReduceDB 38 (25042 restarts, 148 cnfs/res, 35.8% reduced, 105b 40089g 41813g3) > | 3705002 | 433 10892 67524 | 103916 12 4.2 31.8 | 21.695 % | | 3900001 | 433 10892 67524 | 298915 19 9.2 31.7 | 21.695 % | < ReduceDB 39 (26626 restarts, 146 cnfs/res, 35.9% reduced, 105b 41334g 43116g3) > | 3900001 | 433 10892 67524 | 107366 12 4.0 31.7 | 21.695 % | | 4100002 | 433 10892 67524 | 307367 19 8.9 31.5 | 21.695 % | < ReduceDB 40 (28042 restarts, 146 cnfs/res, 35.3% reduced, 105b 42771g 44629g3) > | 4100002 | 433 10892 67524 | 108540 11 3.9 31.5 | 21.695 % | | 4305003 | 433 10892 67524 | 313541 19 8.8 31.3 | 21.695 % | < ReduceDB 41 (29513 restarts, 146 cnfs/res, 35.1% reduced, 105b 44178g 46025g3) > | 4305003 | 433 10892 67524 | 110193 11 3.9 31.3 | 21.695 % | | 4515002 | 433 10892 67524 | 320192 19 8.9 31.1 | 21.695 % | < ReduceDB 42 (31213 restarts, 145 cnfs/res, 36.2% reduced, 105b 45562g 47079g3) > | 4515002 | 433 10892 67524 | 115998 12 4.1 31.1 | 21.695 % | | 4730002 | 433 10892 67524 | 330998 20 8.7 30.9 | 21.695 % | < ReduceDB 43 (32528 restarts, 145 cnfs/res, 35.6% reduced, 105b 46875g 48708g3) > | 4730002 | 433 10892 67524 | 117843 11 3.9 30.9 | 21.695 % | | 4950002 | 433 10892 67524 | 337843 19 9.1 30.8 | 21.695 % | < ReduceDB 44 (34374 restarts, 144 cnfs/res, 35.6% reduced, 106b 48650g 49952g3) > | 4950002 | 433 10892 67524 | 120188 11 3.8 30.8 | 21.695 % | | 5050023 | 433 10892 67524 | 220209 16 7.3 30.7 | 21.695 % | | 5175001 | 433 10892 67524 | 345187 18 8.8 30.6 | 21.695 % | < ReduceDB 45 (35829 restarts, 144 cnfs/res, 35.8% reduced, 106b 50203g 51529g3) > | 5175001 | 433 10892 67524 | 123474 11 3.8 30.6 | 21.695 % | | 5405001 | 433 10892 67524 | 353474 19 8.6 30.4 | 21.695 % | < ReduceDB 46 (37056 restarts, 146 cnfs/res, 36.1% reduced, 107b 51890g 53105g3) > | 5405001 | 433 10892 67524 | 127521 12 3.8 30.4 | 21.695 % | | 5640002 | 432 10757 66668 | 362485 18 8.5 30.1 | 21.722 % | < ReduceDB 47 (38308 restarts, 147 cnfs/res, 34.9% reduced, 107b 53730g 54414g3) > | 5640002 | 432 10757 66668 | 126426 11 3.4 30.1 | 21.722 % | | 5880001 | 432 10757 66668 | 366425 18 8.7 29.9 | 21.722 % | < ReduceDB 48 (39748 restarts, 148 cnfs/res, 36.1% reduced, 108b 55651g 55995g3) > | 5880001 | 432 10757 66668 | 132293 11 3.7 29.9 | 21.722 % | | 6125002 | 432 10757 66668 | 377294 18 8.7 29.6 | 21.722 % | < ReduceDB 49 (40926 restarts, 150 cnfs/res, 35.1% reduced, 108b 57668g 57349g3) > | 6125002 | 432 10757 66668 | 132485 11 3.5 29.6 | 21.722 % | | 6375002 | 432 10757 66668 | 382485 18 8.5 29.3 | 21.722 % | < ReduceDB 50 (41781 restarts, 153 cnfs/res, 36.1% reduced, 108b 59762g 59456g3) > | 6375002 | 432 10757 66668 | 137994 11 3.6 29.3 | 21.722 % | | 6630002 | 432 10757 66668 | 392994 18 8.9 29.0 | 21.722 % | < ReduceDB 51 (42719 restarts, 155 cnfs/res, 36.4% reduced, 108b 62034g 61332g3) > | 6630002 | 432 10757 66668 | 143208 11 3.6 29.0 | 21.722 % | | 6890001 | 432 10757 66668 | 403207 17 9.1 28.7 | 21.722 % | < ReduceDB 52 (43869 restarts, 157 cnfs/res, 36.8% reduced, 108b 64770g 63456g3) > | 6890001 | 432 10757 66668 | 148531 11 3.6 28.7 | 21.722 % | | 7155001 | 432 10757 66668 | 413531 17 8.8 28.3 | 21.722 % | < ReduceDB 53 (44589 restarts, 160 cnfs/res, 36.6% reduced, 108b 66978g 65387g3) > | 7155001 | 432 10757 66668 | 151525 11 3.5 28.3 | 21.722 % | | 7425001 | 432 10757 66668 | 421525 17 9.0 28.0 | 21.722 % | < ReduceDB 54 (45640 restarts, 163 cnfs/res, 37.0% reduced, 108b 69284g 67412g3) > | 7425001 | 432 10757 66668 | 155828 11 3.4 28.0 | 21.722 % | | 7575139 | 432 10757 66668 | 305966 15 7.6 27.9 | 21.722 % | | 7700003 | 432 10757 66668 | 430830 17 8.9 27.7 | 21.722 % | < ReduceDB 55 (46727 restarts, 165 cnfs/res, 37.0% reduced, 108b 71637g 68906g3) > | 7700003 | 432 10757 66668 | 159572 11 3.5 27.7 | 21.722 % | | 7980001 | 432 10757 66668 | 439570 16 8.9 27.4 | 21.722 % | < ReduceDB 56 (47654 restarts, 167 cnfs/res, 37.3% reduced, 109b 73820g 70361g3) > | 7980001 | 432 10757 66668 | 164044 11 3.5 27.4 | 21.722 % | | 8265003 | 432 10757 66668 | 449046 16 9.1 27.2 | 21.722 % | < ReduceDB 57 (48801 restarts, 169 cnfs/res, 37.1% reduced, 109b 75740g 71931g3) > | 8265003 | 432 10757 66668 | 166809 11 3.4 27.2 | 21.722 % | | 8555001 | 432 10757 66668 | 456807 16 9.2 26.9 | 21.722 % | < ReduceDB 58 (50048 restarts, 171 cnfs/res, 37.3% reduced, 109b 77812g 72999g3) > | 8555001 | 432 10757 66668 | 170575 11 3.5 26.9 | 21.722 % | | 8850001 | 432 10757 66668 | 465575 16 9.0 26.6 | 21.722 % | < ReduceDB 59 (51096 restarts, 173 cnfs/res, 37.2% reduced, 109b 79560g 73904g3) > | 8850001 | 432 10757 66668 | 173073 11 3.4 26.6 | 21.722 % | | 9150001 | 432 10757 66668 | 473073 16 9.2 26.4 | 21.722 % | < ReduceDB 60 (52326 restarts, 175 cnfs/res, 37.3% reduced, 109b 81307g 75169g3) > | 9150001 | 432 10757 66668 | 176390 11 3.5 26.4 | 21.722 % | | 9455001 | 432 10757 66668 | 481390 16 9.2 26.1 | 21.722 % | < ReduceDB 61 (53573 restarts, 176 cnfs/res, 37.2% reduced, 109b 82986g 76114g3) > | 9455001 | 432 10757 66668 | 179127 11 3.5 26.1 | 21.722 % | | 9765002 | 432 10757 66668 | 489128 16 9.0 25.9 | 21.722 % | < ReduceDB 62 (54595 restarts, 179 cnfs/res, 36.9% reduced, 109b 84291g 76946g3) > | 9765002 | 432 10757 66668 | 180395 10 3.3 25.9 | 21.722 % | | 10080004 | 432 10757 66668 | 495397 16 9.1 25.6 | 21.722 % | < ReduceDB 63 (55799 restarts, 181 cnfs/res, 37.0% reduced, 109b 85732g 77635g3) > | 10080004 | 432 10757 66668 | 183180 11 3.4 25.6 | 21.722 % | | 10400002 | 432 10757 66668 | 503178 15 9.0 25.4 | 21.722 % | < ReduceDB 64 (56802 restarts, 183 cnfs/res, 36.9% reduced, 109b 87324g 78397g3) > | 10400002 | 432 10757 66668 | 185539 10 3.3 25.4 | 21.722 % | | 10725002 | 432 10757 66668 | 510539 15 9.1 25.2 | 21.722 % | < ReduceDB 65 (57998 restarts, 185 cnfs/res, 37.1% reduced, 109b 88769g 79342g3) > | 10725002 | 432 10757 66668 | 189373 10 3.3 25.2 | 21.722 % | | 11055003 | 432 10757 66668 | 519374 16 9.0 25.0 | 21.722 % | < ReduceDB 66 (59085 restarts, 187 cnfs/res, 36.6% reduced, 109b 89996g 79949g3) > | 11055003 | 432 10757 66668 | 189984 11 3.3 25.0 | 21.722 % | | 11362814 | 432 10757 66668 | 497795 15 8.9 24.8 | 21.722 % | | 11390002 | 432 10757 66668 | 524983 15 9.0 24.7 | 21.722 % | < ReduceDB 67 (60081 restarts, 190 cnfs/res, 36.1% reduced, 109b 91098g 80689g3) > | 11390002 | 432 10757 66668 | 189304 10 3.2 24.7 | 21.722 % | | 11730004 | 432 10757 66668 | 529306 16 9.0 24.5 | 21.722 % | < ReduceDB 68 (61114 restarts, 192 cnfs/res, 36.4% reduced, 109b 92122g 81292g3) > | 11730004 | 432 10757 66668 | 192799 10 3.3 24.5 | 21.722 % | | 12075001 | 432 10757 66668 | 537796 15 9.0 24.3 | 21.722 % | < ReduceDB 69 (62045 restarts, 195 cnfs/res, 36.4% reduced, 109b 93310g 81982g3) > | 12075001 | 432 10757 66668 | 195692 11 3.4 24.3 | 21.722 % | | 12425003 | 432 10757 66668 | 545694 15 9.0 24.1 | 21.722 % | < ReduceDB 70 (63019 restarts, 197 cnfs/res, 36.0% reduced, 109b 94262g 82576g3) > | 12425003 | 432 10757 66668 | 196474 10 3.3 24.1 | 21.722 % | | 12780001 | 432 10757 66668 | 551472 15 9.0 23.9 | 21.722 % | < ReduceDB 71 (63974 restarts, 200 cnfs/res, 36.0% reduced, 109b 95339g 83366g3) > | 12780001 | 432 10757 66668 | 198552 10 3.3 23.9 | 21.722 % | | 13140003 | 432 10757 66668 | 558554 15 8.6 23.7 | 21.722 % | < ReduceDB 72 (64721 restarts, 203 cnfs/res, 35.5% reduced, 111b 96223g 83975g3) > | 13140003 | 432 10757 66668 | 198524 10 3.2 23.7 | 21.722 % | | 13322798 | 432 10757 66668 | 381319 14 7.5 23.6 | 21.722 % | ==================================================================================== restarts : 65079 (11.04 /sec) (204.72 confs/res) conflicts : 13322798 (2260 /sec) decisions : 17510586 (0.00 % random) (2971 /sec) propagations : 328335394 (55706 /sec) conflict literals : 283292330 (21.06 % deleted) average of lbd : 7.48 Memory used : 164.00 MB CPU time : 5894.04 s INDETERMINATE 12 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_12-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29174 | | Parse time: 0.01 s | | Eliminated clauses: 0.25 Mb | | Simplification time: 0.17 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 646 17916 111092 | 100 5 4.0 18.7 | 16.271 % | | 250 | 609 17916 111092 | 248 5 3.5 13.9 | 17.269 % | | 475 | 599 17916 111092 | 468 4 3.4 18.2 | 17.539 % | | 812 | 559 17916 111092 | 796 5 4.1 38.2 | 18.618 % | | 1318 | 511 17916 111092 | 1295 6 5.1 66.2 | 19.914 % | | 2077 | 496 17916 111092 | 2051 7 5.6 79.6 | 20.318 % | | 3216 | 485 17916 111092 | 3186 7 5.8 83.2 | 20.615 % | | 4924 | 480 13376 83195 | 4438 7 6.4 87.7 | 20.750 % | | 5001 | 479 13376 83195 | 4514 7 6.4 87.8 | 20.777 % | < ReduceDB 1 ( 87 restarts, 57 cnfs/res, 50.0% reduced, 31b 202g 442g3) > | 5001 | 479 13376 83195 | 2258 7 5.4 87.8 | 20.777 % | | 5177 | 479 13376 83195 | 2434 7 5.4 87.4 | 20.777 % | ==================================================================================== restarts : 87 (361.05 /sec) (59.51 confs/res) conflicts : 5177 (21485 /sec) decisions : 28769 (0.00 % random) (119392 /sec) propagations : 100204 (415848 /sec) conflict literals : 36901 (3.52 % deleted) average of lbd : 5.43 Memory used : 11.00 MB CPU time : 0.240963 s INDETERMINATE 13 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_13-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29170 | | Parse time: 0.01 s | | Eliminated clauses: 0.05 Mb | | Simplification time: 0.02 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 1804 24413 88788 | 0 nan nan nan | 15.785 % | ==================================================================================== restarts : 1 (32.26 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 585 (18874 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 9.00 MB CPU time : 0.030995 s INDETERMINATE 14 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_14-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29166 | | Parse time: 0.01 s | | Eliminated clauses: 0.04 Mb | | Simplification time: 0.02 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 1926 24929 86954 | 0 nan nan nan | 15.758 % | ==================================================================================== restarts : 1 (38.47 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 584 (22465 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 9.00 MB CPU time : 0.025996 s INDETERMINATE 15 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_15-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29168 | | Parse time: 0.01 s | | Eliminated clauses: 0.04 Mb | | Simplification time: 0.02 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 1972 24967 86318 | 0 nan nan nan | 15.839 % | ==================================================================================== restarts : 1 (37.04 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 587 (21745 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 9.00 MB CPU time : 0.026995 s INDETERMINATE 16 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_16-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29171 | | Parse time: 0.01 s | | Eliminated clauses: 0.04 Mb | | Simplification time: 0.02 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 1940 25027 87289 | 0 nan nan nan | 15.434 % | ==================================================================================== restarts : 1 (37.04 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 572 (21189 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 9.00 MB CPU time : 0.026995 s INDETERMINATE 17 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_17-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29166 | | Parse time: 0.01 s | | Eliminated clauses: 0.04 Mb | | Simplification time: 0.02 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 2038 25257 86506 | 0 nan nan nan | 15.300 % | ==================================================================================== restarts : 1 (34.49 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 567 (19555 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 9.00 MB CPU time : 0.028995 s INDETERMINATE 18 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_18-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29166 | | Parse time: 0.01 s | | Eliminated clauses: 0.04 Mb | | Simplification time: 0.02 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 1951 25365 88559 | 0 nan nan nan | 15.003 % | ==================================================================================== restarts : 1 (35.72 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 556 (19861 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 9.00 MB CPU time : 0.027995 s INDETERMINATE 19 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_19-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29178 | | Parse time: 0.01 s | | Eliminated clauses: 0.05 Mb | | Simplification time: 0.02 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 1831 24459 87076 | 0 nan nan nan | 15.111 % | ==================================================================================== restarts : 1 (35.72 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 560 (20004 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 9.00 MB CPU time : 0.027995 s INDETERMINATE 20 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_20-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29185 | | Parse time: 0.01 s | | Eliminated clauses: 0.04 Mb | | Simplification time: 0.02 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 1847 24674 87664 | 0 nan nan nan | 14.922 % | ==================================================================================== restarts : 1 (37.04 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 553 (20485 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 9.00 MB CPU time : 0.026995 s INDETERMINATE 21 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_21-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29181 | | Parse time: 0.01 s | | Eliminated clauses: 0.04 Mb | | Simplification time: 0.02 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 1881 24724 86672 | 0 nan nan nan | 15.030 % | ==================================================================================== restarts : 1 (35.72 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 557 (19896 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 9.00 MB CPU time : 0.027995 s INDETERMINATE 22 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_22-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29173 | | Parse time: 0.01 s | | Eliminated clauses: 0.04 Mb | | Simplification time: 0.02 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 1912 24934 87178 | 0 nan nan nan | 15.030 % | ==================================================================================== restarts : 1 (34.49 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 557 (19210 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 9.00 MB CPU time : 0.028995 s INDETERMINATE 23 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_23-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29186 | | Parse time: 0.01 s | | Eliminated clauses: 0.04 Mb | | Simplification time: 0.02 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 1945 25238 88124 | 0 nan nan nan | 14.382 % | ==================================================================================== restarts : 1 (35.72 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 533 (19039 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 9.00 MB CPU time : 0.027995 s INDETERMINATE 24 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_24-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29183 | | Parse time: 0.01 s | | Eliminated clauses: 0.04 Mb | | Simplification time: 0.02 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 1853 24581 86395 | 0 nan nan nan | 14.679 % | ==================================================================================== restarts : 1 (35.72 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 544 (19432 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 9.00 MB CPU time : 0.027995 s INDETERMINATE 25 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_25-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29183 | | Parse time: 0.01 s | | Eliminated clauses: 0.04 Mb | | Simplification time: 0.02 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 1884 24634 86276 | 0 nan nan nan | 15.057 % | ==================================================================================== restarts : 1 (34.49 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 558 (19245 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 9.00 MB CPU time : 0.028995 s INDETERMINATE 26 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_26-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29182 | | Parse time: 0.01 s | | Eliminated clauses: 0.04 Mb | | Simplification time: 0.02 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 1958 25426 88815 | 0 nan nan nan | 14.517 % | ==================================================================================== restarts : 1 (35.72 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 538 (19218 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 9.00 MB CPU time : 0.027995 s INDETERMINATE 27 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_27-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29186 | | Parse time: 0.01 s | | Eliminated clauses: 0.04 Mb | | Simplification time: 0.02 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 1921 25048 87619 | 0 nan nan nan | 14.760 % | ==================================================================================== restarts : 1 (37.04 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 547 (20263 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 9.00 MB CPU time : 0.026995 s INDETERMINATE 28 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_28-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29196 | | Parse time: 0.01 s | | Eliminated clauses: 0.05 Mb | | Simplification time: 0.02 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 1851 24464 85977 | 0 nan nan nan | 14.571 % | ==================================================================================== restarts : 1 (34.49 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 540 (18624 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 9.00 MB CPU time : 0.028995 s INDETERMINATE 29 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_29-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29201 | | Parse time: 0.01 s | | Eliminated clauses: 0.04 Mb | | Simplification time: 0.02 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 1917 25076 87789 | 0 nan nan nan | 13.815 % | ==================================================================================== restarts : 1 (35.72 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 512 (18289 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 9.00 MB CPU time : 0.027995 s INDETERMINATE 30 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_30-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29189 | | Parse time: 0.01 s | | Eliminated clauses: 0.04 Mb | | Simplification time: 0.02 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 1899 24955 87456 | 0 nan nan nan | 15.192 % | ==================================================================================== restarts : 1 (34.49 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 563 (19417 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 9.00 MB CPU time : 0.028995 s INDETERMINATE 31 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_31-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29199 | | Parse time: 0.01 s | | Eliminated clauses: 0.04 Mb | | Simplification time: 0.02 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 1914 24898 87086 | 0 nan nan nan | 15.326 % | ==================================================================================== restarts : 1 (35.72 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 568 (20289 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 9.00 MB CPU time : 0.027995 s INDETERMINATE 32 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_32-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29205 | | Parse time: 0.01 s | | Eliminated clauses: 0.04 Mb | | Simplification time: 0.02 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 1932 24768 85962 | 0 nan nan nan | 15.893 % | ==================================================================================== restarts : 1 (35.72 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 589 (21039 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 9.00 MB CPU time : 0.027995 s INDETERMINATE 33 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_33-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29237 | | Parse time: 0.01 s | | Eliminated clauses: 0.05 Mb | | Simplification time: 0.02 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 1814 25105 91122 | 0 nan nan nan | 13.815 % | ==================================================================================== restarts : 1 (34.49 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 512 (17658 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 9.00 MB CPU time : 0.028995 s INDETERMINATE