19 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_19-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29178 | | Parse time: 0.01 s | | Eliminated clauses: 0.33 Mb | | Simplification time: 0.32 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 606 16568 103305 | 98 5 4.0 19.8 | 16.109 % | | 250 | 605 16568 103305 | 247 5 3.5 16.7 | 16.136 % | | 475 | 591 16568 103305 | 466 5 4.0 26.7 | 16.514 % | | 812 | 581 16568 103305 | 802 7 5.3 64.4 | 16.784 % | | 1318 | 581 16568 103305 | 1308 8 7.0 81.5 | 16.784 % | | 2077 | 570 16568 103305 | 2064 9 7.3 96.0 | 17.080 % | | 3216 | 549 16568 103305 | 3197 9 7.5 105.4 | 17.647 % | | 4924 | 505 12989 80499 | 4601 9 7.7 109.2 | 18.834 % | | 5001 | 505 12989 80499 | 4678 9 7.8 109.5 | 18.834 % | < ReduceDB 1 ( 87 restarts, 57 cnfs/res, 50.0% reduced, 24b 134g 203g3) > | 5001 | 505 12989 80499 | 2339 8 6.5 109.5 | 18.834 % | | 6799 | 493 12989 80499 | 4131 8 6.9 109.5 | 19.158 % | ==================================================================================== restarts : 110 (249.47 /sec) (61.81 confs/res) conflicts : 6799 (15420 /sec) decisions : 39201 (0.00 % random) (88905 /sec) propagations : 131413 (298035 /sec) conflict literals : 58109 (1.83 % deleted) average of lbd : 6.88 Memory used : 11.00 MB CPU time : 0.440932 s SATISFIABLE 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.02 s | | Eliminated clauses: 0.32 Mb | | Simplification time: 0.34 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 618 16764 105012 | 99 5 4.0 18.1 | 15.785 % | | 250 | 602 16764 105012 | 237 4 3.4 15.3 | 16.217 % | | 475 | 600 16764 105012 | 460 6 4.6 50.8 | 16.271 % | | 812 | 587 16764 105012 | 794 6 4.9 62.8 | 16.622 % | | 1318 | 543 16764 105012 | 1292 7 5.6 71.5 | 17.809 % | | 2077 | 542 16764 105012 | 2050 8 6.8 84.2 | 17.836 % | | 3216 | 541 16764 105012 | 3188 9 7.4 97.3 | 17.863 % | | 4924 | 531 13014 80442 | 4586 9 8.0 104.1 | 18.133 % | | 5001 | 531 13014 80442 | 4663 9 8.0 103.9 | 18.133 % | < ReduceDB 1 ( 88 restarts, 57 cnfs/res, 50.1% reduced, 36b 152g 238g3) > | 5001 | 531 13014 80442 | 2338 8 6.8 103.9 | 18.133 % | | 7486 | 497 13014 80442 | 4822 8 7.3 107.1 | 19.050 % | | 9927 | 493 12599 78076 | 7192 9 7.8 108.7 | 19.158 % | ==================================================================================== restarts : 169 (320.12 /sec) (58.74 confs/res) conflicts : 9927 (18804 /sec) decisions : 60173 (0.00 % random) (113982 /sec) propagations : 213437 (404299 /sec) conflict literals : 89912 (2.41 % deleted) average of lbd : 7.75 Memory used : 11.00 MB CPU time : 0.527919 s SATISFIABLE 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.31 Mb | | Simplification time: 0.28 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 639 16316 101332 | 100 5 3.9 18.1 | 15.327 % | | 250 | 617 16316 101332 | 248 5 3.6 13.3 | 15.920 % | | 475 | 600 16316 101332 | 459 6 4.3 42.0 | 16.379 % | | 812 | 586 16316 101332 | 792 6 5.4 74.3 | 16.757 % | | 1318 | 581 16316 101332 | 1297 7 5.9 91.8 | 16.892 % | | 2077 | 581 16316 101332 | 2056 7 6.1 99.9 | 16.892 % | | 3216 | 536 16316 101332 | 3194 8 6.7 108.5 | 18.106 % | | 4535 | 521 12818 79158 | 4138 8 7.1 112.5 | 18.511 % | ==================================================================================== restarts : 76 (211.73 /sec) (59.67 confs/res) conflicts : 4535 (12634 /sec) decisions : 29108 (0.00 % random) (81093 /sec) propagations : 99558 (277363 /sec) conflict literals : 36516 (3.38 % deleted) average of lbd : 7.11 Memory used : 10.00 MB CPU time : 0.358945 s SATISFIABLE 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.30 Mb | | Simplification time: 0.30 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 618 16124 100468 | 99 5 4.0 18.1 | 15.974 % | | 250 | 602 16124 100468 | 237 4 3.4 15.3 | 16.406 % | | 475 | 599 16124 100468 | 459 5 3.8 28.9 | 16.487 % | | 812 | 548 16124 100468 | 790 6 4.7 52.7 | 17.863 % | | 1318 | 514 16124 100468 | 1287 7 5.7 73.4 | 18.780 % | | 2077 | 504 16124 100468 | 2042 8 6.6 88.1 | 19.050 % | | 3216 | 504 16124 100468 | 3181 8 7.0 99.9 | 19.050 % | | 4924 | 500 12080 74026 | 4584 9 7.7 107.4 | 19.158 % | | 5001 | 500 12080 74026 | 4661 9 7.7 107.5 | 19.158 % | < ReduceDB 1 ( 93 restarts, 54 cnfs/res, 50.0% reduced, 12b 102g 252g3) > | 5001 | 500 12080 74026 | 2330 8 6.7 107.5 | 19.158 % | | 7486 | 492 12080 74026 | 4811 9 7.8 112.6 | 19.374 % | | 9323 | 490 12080 74026 | 6647 9 8.0 114.1 | 19.428 % | ==================================================================================== restarts : 167 (360.75 /sec) (55.83 confs/res) conflicts : 9323 (20139 /sec) decisions : 55355 (0.00 % random) (119576 /sec) propagations : 186424 (402705 /sec) conflict literals : 83756 (1.86 % deleted) average of lbd : 8.04 Memory used : 11.00 MB CPU time : 0.462929 s SATISFIABLE 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.02 s | | Eliminated clauses: 0.33 Mb | | Simplification time: 0.33 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 642 17020 107636 | 100 5 4.1 19.6 | 14.841 % | | 250 | 610 17020 107636 | 246 5 3.3 16.4 | 15.704 % | | 475 | 596 17020 107636 | 464 5 3.7 31.5 | 16.082 % | | 812 | 550 17020 107636 | 788 6 4.5 52.9 | 17.323 % | | 1318 | 546 17020 107636 | 1292 7 6.0 85.9 | 17.431 % | | 2077 | 511 17020 107636 | 2043 8 6.8 98.2 | 18.376 % | | 3216 | 505 17020 107636 | 3179 8 7.0 108.5 | 18.538 % | | 4388 | 505 13077 81621 | 3986 9 7.7 115.2 | 18.538 % | ==================================================================================== restarts : 81 (195.68 /sec) (54.17 confs/res) conflicts : 4388 (10601 /sec) decisions : 26654 (0.00 % random) (64391 /sec) propagations : 91207 (220340 /sec) conflict literals : 36181 (2.56 % deleted) average of lbd : 7.71 Memory used : 11.00 MB CPU time : 0.413937 s SATISFIABLE 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.32 Mb | | Simplification time: 0.32 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 640 16476 103572 | 100 5 3.8 18.1 | 14.895 % | | 250 | 610 16476 103572 | 241 5 3.6 23.5 | 15.704 % | | 475 | 604 16476 103572 | 463 6 4.4 47.9 | 15.866 % | | 812 | 592 16476 103572 | 793 7 5.4 77.8 | 16.190 % | | 1318 | 538 16476 103572 | 1291 7 6.3 100.5 | 17.647 % | | 2077 | 510 16476 103572 | 2040 8 6.9 110.5 | 18.403 % | | 3216 | 505 16476 103572 | 3176 8 7.2 115.5 | 18.538 % | | 4486 | 499 12480 77216 | 4128 9 7.7 119.0 | 18.699 % | ==================================================================================== restarts : 80 (197.56 /sec) (56.08 confs/res) conflicts : 4486 (11078 /sec) decisions : 28262 (0.00 % random) (69793 /sec) propagations : 94271 (232804 /sec) conflict literals : 36903 (2.51 % deleted) average of lbd : 7.67 Memory used : 11.00 MB CPU time : 0.404938 s SATISFIABLE 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.02 s | | Eliminated clauses: 0.30 Mb | | Simplification time: 0.27 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 641 16348 102356 | 100 5 3.8 17.8 | 15.246 % | | 250 | 612 16348 102356 | 248 5 3.3 17.0 | 16.028 % | | 475 | 590 16348 102356 | 471 5 3.3 19.2 | 16.622 % | | 812 | 515 16348 102356 | 794 6 4.5 54.8 | 18.645 % | | 1318 | 502 16348 102356 | 1297 7 5.6 81.5 | 18.996 % | | 2077 | 495 16348 102356 | 2052 8 6.8 97.2 | 19.185 % | | 2716 | 495 16348 102356 | 2691 8 7.2 106.4 | 19.185 % | ==================================================================================== restarts : 49 (148.96 /sec) (55.43 confs/res) conflicts : 2716 (8257 /sec) decisions : 15903 (0.00 % random) (48345 /sec) propagations : 57414 (174538 /sec) conflict literals : 22189 (4.33 % deleted) average of lbd : 7.23 Memory used : 10.00 MB CPU time : 0.328949 s SATISFIABLE 26 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_26-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29182 | | Parse time: 0.01 s | | Eliminated clauses: 0.30 Mb | | Simplification time: 0.28 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 640 16092 100756 | 100 5 3.8 18.1 | 15.138 % | | 250 | 611 16092 100756 | 242 5 3.6 18.5 | 15.920 % | | 475 | 608 16092 100756 | 465 5 4.2 47.2 | 16.001 % | | 812 | 540 16092 100756 | 789 6 4.5 64.2 | 17.836 % | | 1318 | 511 16092 100756 | 1290 7 5.9 97.2 | 18.618 % | | 2077 | 495 16092 100756 | 2046 8 6.5 109.0 | 19.050 % | | 3216 | 478 16092 100756 | 3183 8 7.2 118.2 | 19.509 % | | 4924 | 478 11938 73310 | 4452 9 8.2 121.1 | 19.509 % | | 4987 | 478 11938 73310 | 4515 9 8.2 121.2 | 19.509 % | ==================================================================================== restarts : 89 (238.64 /sec) (56.03 confs/res) conflicts : 4987 (13372 /sec) decisions : 31278 (0.00 % random) (83868 /sec) propagations : 103237 (276817 /sec) conflict literals : 43338 (2.29 % deleted) average of lbd : 8.20 Memory used : 10.00 MB CPU time : 0.372943 s SATISFIABLE 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.02 s | | Eliminated clauses: 0.34 Mb | | Simplification time: 0.28 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 639 15836 99316 | 100 5 3.9 18.1 | 15.246 % | | 250 | 617 15836 99316 | 248 5 3.6 13.3 | 15.839 % | | 475 | 588 15836 99316 | 455 5 3.8 23.3 | 16.622 % | | 812 | 575 15836 99316 | 786 6 5.2 73.0 | 16.972 % | | 1318 | 385 15836 99316 | 1274 7 5.4 80.3 | 22.099 % | | 1460 | 385 15836 99316 | 1416 7 5.7 86.6 | 22.099 % | ==================================================================================== restarts : 20 (62.71 /sec) (73.00 confs/res) conflicts : 1460 (4578 /sec) decisions : 7959 (0.00 % random) (24954 /sec) propagations : 32113 (100683 /sec) conflict literals : 9801 (7.07 % deleted) average of lbd : 5.75 Memory used : 10.00 MB CPU time : 0.318951 s SATISFIABLE 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.02 s | | Eliminated clauses: 0.31 Mb | | Simplification time: 0.30 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 640 15804 99284 | 100 5 3.8 18.1 | 14.706 % | | 250 | 611 15804 99284 | 242 5 3.5 18.9 | 15.488 % | | 475 | 595 15804 99284 | 461 5 3.7 35.7 | 15.920 % | | 812 | 532 15804 99284 | 789 6 5.1 77.0 | 17.620 % | | 1318 | 530 15804 99284 | 1294 8 6.7 102.9 | 17.674 % | | 2077 | 515 15804 99284 | 2046 9 7.4 111.1 | 18.079 % | | 2295 | 513 15804 99284 | 2262 8 7.3 108.4 | 18.133 % | ==================================================================================== restarts : 40 (114.96 /sec) (57.38 confs/res) conflicts : 2295 (6596 /sec) decisions : 14075 (0.00 % random) (40452 /sec) propagations : 50251 (144421 /sec) conflict literals : 19074 (3.58 % deleted) average of lbd : 7.29 Memory used : 11.00 MB CPU time : 0.347947 s SATISFIABLE 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.02 s | | Eliminated clauses: 0.33 Mb | | Simplification time: 0.29 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 640 15676 98772 | 100 5 3.8 18.1 | 14.301 % | | 250 | 611 15676 98772 | 242 5 3.8 17.8 | 15.084 % | | 475 | 598 15676 98772 | 463 5 4.2 40.3 | 15.434 % | | 812 | 598 15676 98772 | 800 7 5.6 78.2 | 15.434 % | | 1318 | 543 15676 98772 | 1302 7 5.9 91.6 | 16.919 % | | 2077 | 526 15676 98772 | 2054 8 6.8 112.0 | 17.377 % | | 2494 | 526 15676 98772 | 2471 8 7.1 116.9 | 17.377 % | ==================================================================================== restarts : 43 (125.02 /sec) (58.00 confs/res) conflicts : 2494 (7251 /sec) decisions : 16185 (0.00 % random) (47057 /sec) propagations : 60939 (177176 /sec) conflict literals : 20301 (4.65 % deleted) average of lbd : 7.05 Memory used : 11.00 MB CPU time : 0.343947 s SATISFIABLE 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.02 s | | Eliminated clauses: 0.30 Mb | | Simplification time: 0.30 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 636 14908 93492 | 100 5 4.1 17.5 | 15.461 % | | 250 | 621 14908 93492 | 249 5 3.8 16.2 | 15.866 % | | 475 | 594 14908 93492 | 462 6 4.4 46.5 | 16.595 % | | 812 | 582 14908 93492 | 793 6 4.9 75.7 | 16.919 % | | 1279 | 336 14908 93492 | 1251 7 5.7 91.9 | 23.556 % | ==================================================================================== restarts : 19 (56.89 /sec) (67.32 confs/res) conflicts : 1279 (3830 /sec) decisions : 7522 (0.00 % random) (22524 /sec) propagations : 30123 (90202 /sec) conflict literals : 8583 (9.26 % deleted) average of lbd : 5.72 Memory used : 11.00 MB CPU time : 0.333949 s SATISFIABLE 31 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_31-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29199 | | Parse time: 0.01 s | | Eliminated clauses: 0.32 Mb | | Simplification time: 0.29 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 636 14748 93460 | 100 5 4.1 17.5 | 15.542 % | | 250 | 621 14748 93460 | 249 5 3.8 16.2 | 15.947 % | | 475 | 594 14748 93460 | 462 6 4.4 50.2 | 16.676 % | | 524 | 594 14748 93460 | 511 6 4.5 62.1 | 16.676 % | ==================================================================================== restarts : 6 (18.87 /sec) (87.33 confs/res) conflicts : 524 (1648 /sec) decisions : 2888 (0.00 % random) (9083 /sec) propagations : 15802 (49699 /sec) conflict literals : 2981 (18.77 % deleted) average of lbd : 4.54 Memory used : 11.00 MB CPU time : 0.317951 s SATISFIABLE 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.02 s | | Eliminated clauses: 0.28 Mb | | Simplification time: 0.31 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 636 14076 87412 | 100 5 4.1 17.5 | 15.893 % | | 250 | 621 14076 87412 | 249 5 3.8 16.2 | 16.298 % | | 475 | 592 14076 87412 | 461 6 4.1 41.5 | 17.080 % | | 812 | 577 14076 87412 | 792 6 5.0 66.5 | 17.485 % | | 1318 | 565 14076 87412 | 1293 8 6.7 97.6 | 17.809 % | | 2077 | 529 14076 87412 | 2048 9 7.6 109.1 | 18.780 % | | 2643 | 527 14076 87412 | 2613 9 8.0 112.8 | 18.834 % | ==================================================================================== restarts : 46 (127.80 /sec) (57.46 confs/res) conflicts : 2643 (7343 /sec) decisions : 17113 (0.00 % random) (47543 /sec) propagations : 64699 (179747 /sec) conflict literals : 23535 (4.06 % deleted) average of lbd : 8.03 Memory used : 11.00 MB CPU time : 0.359945 s SATISFIABLE 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.02 s | | Eliminated clauses: 0.37 Mb | | Simplification time: 0.49 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 514 11861 72829 | 98 4 3.2 15.5 | 14.733 % | | 250 | 496 11861 72829 | 241 4 3.2 24.2 | 15.219 % | | 475 | 448 11861 72829 | 460 5 4.3 59.8 | 16.514 % | | 812 | 448 11861 72829 | 797 7 6.4 90.7 | 16.514 % | | 1318 | 448 11861 72829 | 1303 8 7.8 112.2 | 16.514 % | | 2077 | 448 11861 72829 | 2062 9 8.5 120.1 | 16.514 % | | 3216 | 439 11861 72829 | 3197 9 8.7 128.0 | 16.757 % | | 3951 | 439 11861 72829 | 3932 9 8.8 130.4 | 16.757 % | ==================================================================================== restarts : 74 (133.59 /sec) (53.39 confs/res) conflicts : 3951 (7133 /sec) decisions : 26652 (0.00 % random) (48116 /sec) propagations : 70821 (127855 /sec) conflict literals : 37311 (1.35 % deleted) average of lbd : 8.76 Memory used : 11.00 MB CPU time : 0.553915 s SATISFIABLE