WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 6912 | | Number of clauses: 13539 | | Parse time: 0.00 s | | | =============================================================================== Solved by unit propagation restarts : 0 conflicts : 0 (0 /sec) decisions : 0 (-nan % random) (0 /sec) propagations : 167 (83542 /sec) conflict literals : 0 (-nan % deleted) Memory used : 7.00 MB CPU time : 0.001999 s UNSATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 6912 | | Number of clauses: 14028 | | Parse time: 0.00 s | | | =============================================================================== Solved by unit propagation restarts : 0 conflicts : 0 (0 /sec) decisions : 0 (-nan % random) (0 /sec) propagations : 337 (168584 /sec) conflict literals : 0 (-nan % deleted) Memory used : 7.00 MB CPU time : 0.001999 s UNSATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 6912 | | Number of clauses: 15171 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== =============================================================================== restarts : 1 conflicts : 14 (4668 /sec) decisions : 44 (0.00 % random) (14672 /sec) propagations : 1580 (526842 /sec) conflict literals : 25 (3.85 % deleted) Memory used : 7.00 MB CPU time : 0.002999 s UNSATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 6912 | | Number of clauses: 15188 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 6123 14003 46942 | 5134 88 5 | 11.415 % | =============================================================================== restarts : 2 conflicts : 131 (32758 /sec) decisions : 3966 (0.00 % random) (991748 /sec) propagations : 39532 (9885471 /sec) conflict literals : 571 (19.24 % deleted) Memory used : 7.00 MB CPU time : 0.003999 s UNSATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 6912 | | Number of clauses: 15191 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 6202 13765 46216 | 5047 87 7 | 10.272 % | =============================================================================== restarts : 2 conflicts : 199 (49762 /sec) decisions : 2745 (0.00 % random) (686422 /sec) propagations : 39633 (9910728 /sec) conflict literals : 1076 (31.94 % deleted) Memory used : 7.00 MB CPU time : 0.003999 s UNSATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 6912 | | Number of clauses: 15186 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 6087 13770 46108 | 5049 87 7 | 11.936 % | | 250 | 6087 13770 46108 | 5553 237 7 | 11.936 % | | 475 | 6077 12382 41317 | 6109 327 8 | 12.080 % | =============================================================================== restarts : 6 conflicts : 744 (93023 /sec) decisions : 4046 (0.00 % random) (505876 /sec) propagations : 93302 (11665666 /sec) conflict literals : 5084 (36.66 % deleted) Memory used : 7.00 MB CPU time : 0.007998 s UNSATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 6912 | | Number of clauses: 15192 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 6292 14366 47983 | 5267 93 10 | 8.970 % | | 250 | 6276 14366 47983 | 5794 242 10 | 9.201 % | | 475 | 6274 13719 45599 | 6373 464 9 | 9.230 % | | 812 | 6274 13719 45599 | 7011 801 9 | 9.230 % | | 1318 | 6274 13719 45599 | 7712 1307 9 | 9.230 % | | 2077 | 6274 13719 45599 | 8483 2066 10 | 9.230 % | | 3216 | 6274 13719 45599 | 9331 3205 10 | 9.230 % | | 4924 | 6274 13719 45599 | 10264 4913 10 | 9.230 % | =============================================================================== restarts : 31 conflicts : 6487 (77238 /sec) decisions : 11847 (0.00 % random) (141058 /sec) propagations : 960714 (11438842 /sec) conflict literals : 57580 (43.17 % deleted) Memory used : 7.00 MB CPU time : 0.083987 s UNSATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 6912 | | Number of clauses: 15197 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 6287 14139 47344 | 5184 95 11 | 9.042 % | | 250 | 6162 13149 43722 | 5702 236 11 | 10.851 % | | 475 | 6079 12457 41483 | 6273 444 12 | 12.052 % | | 812 | 6079 12359 41105 | 6900 780 11 | 12.052 % | | 1318 | 6079 12359 41105 | 7590 1286 12 | 12.052 % | | 2077 | 6079 12359 41105 | 8349 2045 12 | 12.052 % | | 3216 | 6079 12359 41105 | 9184 3184 12 | 12.052 % | | 4924 | 6079 12359 41105 | 10102 4892 12 | 12.052 % | | 7486 | 6079 12359 41105 | 11113 7454 12 | 12.052 % | | 11330 | 6079 12359 41105 | 12224 11298 11 | 12.052 % | =============================================================================== restarts : 62 conflicts : 15339 (72025 /sec) decisions : 32257 (0.00 % random) (151465 /sec) propagations : 2425811 (11390549 /sec) conflict literals : 160347 (34.68 % deleted) Memory used : 8.00 MB CPU time : 0.212967 s UNSATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 6912 | | Number of clauses: 15190 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 6230 14152 47482 | 5189 93 14 | 9.867 % | | 250 | 6127 13025 43406 | 5707 237 12 | 11.357 % | | 475 | 6101 13025 43406 | 6278 461 12 | 11.733 % | | 812 | 6101 12532 41688 | 6906 796 13 | 11.733 % | | 1318 | 6101 12532 41688 | 7597 1302 14 | 11.733 % | | 2077 | 6101 12532 41688 | 8357 2061 14 | 11.733 % | | 3216 | 6073 12433 41308 | 9192 3198 14 | 12.138 % | | 4924 | 6073 12433 41308 | 10112 4906 14 | 12.138 % | | 7486 | 6073 12433 41308 | 11123 7468 15 | 12.138 % | | 11330 | 6069 12347 41010 | 12235 11310 15 | 12.196 % | | 17096 | 6015 12006 39832 | 13459 10470 14 | 12.977 % | | 25745 | 6015 12006 39832 | 14805 11914 13 | 12.977 % | | 38719 | 5983 11923 39548 | 16285 8981 13 | 13.440 % | | 58180 | 5983 11923 39548 | 17914 10868 13 | 13.440 % | | 87372 | 5983 11923 39548 | 19705 11539 11 | 13.440 % | =============================================================================== restarts : 347 conflicts : 127171 (59798 /sec) decisions : 229069 (0.00 % random) (107712 /sec) propagations : 19717750 (9271629 /sec) conflict literals : 1647263 (31.14 % deleted) Memory used : 8.00 MB CPU time : 2.12668 s UNSATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 6912 | | Number of clauses: 15186 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 6282 14414 48258 | 5285 91 11 | 9.115 % | | 250 | 6151 13262 44132 | 5813 230 12 | 11.010 % | | 475 | 6151 13001 43184 | 6395 454 12 | 11.010 % | | 812 | 6111 12918 42900 | 7034 787 13 | 11.589 % | | 1318 | 6095 12766 42408 | 7737 1290 14 | 11.820 % | | 2077 | 6049 12599 41830 | 8511 2045 15 | 12.486 % | | 3216 | 6049 12599 41830 | 9362 3184 16 | 12.486 % | | 4924 | 6019 12502 41454 | 10299 4891 16 | 12.920 % | | 7486 | 6019 12502 41454 | 11329 7453 17 | 12.920 % | | 11330 | 6019 12502 41454 | 12462 11297 17 | 12.920 % | | 17096 | 6019 12502 41454 | 13708 10266 17 | 12.920 % | | 25745 | 6019 12502 41454 | 15079 11513 17 | 12.920 % | | 38719 | 5987 12405 41078 | 16587 8372 17 | 13.383 % | | 58180 | 5987 12405 41078 | 18245 10129 17 | 13.383 % | | 87372 | 5953 12306 40698 | 20070 10182 17 | 13.874 % | | 131161 | 5897 12139 40120 | 22077 11165 16 | 14.685 % | | 196845 | 5859 12040 39740 | 24285 18422 17 | 15.234 % | | 295371 | 5837 11972 39542 | 26713 14160 15 | 15.553 % | | 443160 | 5755 11777 38788 | 29384 18722 14 | 16.739 % | | 664843 | 5567 11383 37272 | 32323 26080 14 | 19.459 % | | 997368 | 5436 11052 36122 | 35555 19619 17 | 21.354 % | | 1496156 | 5436 11052 36122 | 39111 23630 14 | 21.354 % | =============================================================================== restarts : 3997 conflicts : 2026741 (39735 /sec) decisions : 3706073 (0.00 % random) (72659 /sec) propagations : 301629746 (5913585 /sec) conflict literals : 31503257 (29.78 % deleted) Memory used : 18.00 MB CPU time : 51.0062 s UNSATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 6912 | | Number of clauses: 15206 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 6356 14607 48844 | 5355 97 11 | 8.044 % | | 250 | 6319 14144 47128 | 5891 242 13 | 8.579 % | | 475 | 6299 14144 47128 | 6480 466 15 | 8.869 % | | 812 | 6275 13538 45002 | 7128 792 15 | 9.216 % | | 1318 | 6233 13287 44130 | 7841 1293 16 | 9.824 % | | 2077 | 6233 13287 44130 | 8625 2052 16 | 9.824 % | | 3216 | 6227 13219 43932 | 9488 3189 18 | 9.910 % | | 4924 | 6197 13034 43254 | 10437 4894 18 | 10.344 % | | 7486 | 6173 12936 42876 | 11480 7454 19 | 10.692 % | | 11330 | 6137 12765 42290 | 12628 11293 20 | 11.212 % | | 17096 | 6137 12765 42290 | 13891 10259 19 | 11.212 % | | 25745 | 6127 12697 42092 | 15281 11503 19 | 11.357 % | | 38719 | 6099 12613 41806 | 16809 8308 22 | 11.762 % | | 58180 | 6099 12613 41806 | 18490 10109 19 | 11.762 % | | 87372 | 6069 12512 41422 | 20339 19941 20 | 12.196 % | | 131161 | 5847 11921 39148 | 22372 20173 19 | 15.408 % | | 196845 | 5595 11367 37132 | 24610 13715 24 | 19.054 % | | 295371 | 5443 10960 35768 | 27071 16931 19 | 21.253 % | | 443160 | 5429 10890 35566 | 29778 28767 24 | 21.455 % | | 664843 | 5333 10654 34788 | 32756 21680 19 | 22.844 % | | 997368 | 5257 10487 34210 | 36031 17265 22 | 23.944 % | | 1496156 | 5257 10487 34210 | 39634 20394 18 | 23.944 % | | 2244338 | 5195 10388 33830 | 43598 40908 22 | 24.841 % | | 3366612 | 5178 10324 33640 | 47958 30504 20 | 25.087 % | | 5050023 | 5178 10324 33640 | 52754 49228 24 | 25.087 % | | 7575139 | 5178 10324 33640 | 58029 45689 22 | 25.087 % | | 11362814 | 5178 10324 33640 | 63832 18794 23 | 25.087 % | | 17044326 | 5178 10324 33640 | 70215 34912 23 | 25.087 % | | 25566595 | 5178 10324 33640 | 77237 38884 24 | 25.087 % | | 38349998 | 5178 10324 33640 | 84961 63083 23 | 25.087 % | | 57525103 | 5178 10324 33640 | 93457 74932 23 | 25.087 % | | 86287761 | 5178 10324 33640 | 102802 29465 19 | 25.087 % | =============================================================================== restarts : 126457 conflicts : 95730118 (26818 /sec) decisions : 167287708 (0.00 % random) (46864 /sec) propagations : 16692445433 (4676241 /sec) conflict literals : 2184407699 (25.12 % deleted) Memory used : 91.00 MB CPU time : 3569.63 s INDETERMINATE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 6912 | | Number of clauses: 15201 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 6333 14225 47585 | 5215 99 13 | 8.377 % | =============================================================================== restarts : 3 conflicts : 248 (24805 /sec) decisions : 8590 (0.00 % random) (859172 /sec) propagations : 69112 (6912583 /sec) conflict literals : 3407 (10.51 % deleted) Memory used : 7.00 MB CPU time : 0.009998 s SATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 6912 | | Number of clauses: 15197 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 6326 14196 47408 | 5205 99 13 | 8.478 % | | 250 | 6288 13820 45992 | 5725 242 15 | 9.028 % | | 475 | 6200 13300 44156 | 6298 456 15 | 10.301 % | =============================================================================== restarts : 5 conflicts : 516 (34407 /sec) decisions : 13778 (0.00 % random) (918717 /sec) propagations : 137077 (9140295 /sec) conflict literals : 7696 (11.45 % deleted) Memory used : 7.00 MB CPU time : 0.014997 s SATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 6912 | | Number of clauses: 15193 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 6314 13951 46728 | 5115 100 14 | 8.652 % | | 250 | 6290 13673 45690 | 5626 246 15 | 8.999 % | | 475 | 6222 13673 45690 | 6189 467 15 | 9.983 % | | 812 | 6175 13276 44168 | 6808 798 16 | 10.663 % | | 1318 | 6111 12908 42824 | 7489 1300 17 | 11.589 % | | 2077 | 6040 12473 41284 | 8238 2052 18 | 12.616 % | | 3216 | 6040 12473 41284 | 9062 3191 20 | 12.616 % | | 4924 | 6006 12373 40902 | 9968 4897 21 | 13.108 % | | 7486 | 6006 12373 40902 | 10965 7459 22 | 13.108 % | | 11330 | 5970 12275 40524 | 12061 11301 23 | 13.628 % | | 17096 | 5922 12111 39952 | 13267 10458 22 | 14.323 % | | 25745 | 5839 11929 39280 | 14594 11947 23 | 15.524 % | | 38719 | 5795 11831 38902 | 16054 8833 23 | 16.160 % | | 58180 | 5795 11831 38902 | 17659 10831 22 | 16.160 % | | 87372 | 5749 11733 38524 | 19425 11119 27 | 16.826 % | | 131161 | 5749 11733 38524 | 21368 12772 23 | 16.826 % | | 196845 | 5749 11733 38524 | 23504 21222 25 | 16.826 % | | 295371 | 5701 11633 38142 | 25855 16579 23 | 17.520 % | | 443160 | 5599 11437 37386 | 28441 17936 29 | 18.996 % | | 664843 | 5545 11338 37006 | 31285 14634 24 | 19.777 % | | 997368 | 5545 11338 37006 | 34413 27987 29 | 19.777 % | | 1496156 | 5545 11338 37006 | 37854 34034 22 | 19.777 % | | 2244338 | 5467 11066 36028 | 41640 29322 35 | 20.906 % | | 3366612 | 5349 10882 35360 | 45804 21514 22 | 22.613 % | | 5050023 | 5287 10798 35074 | 50384 46993 27 | 23.510 % | | 7575139 | 5287 10798 35074 | 55423 43429 31 | 23.510 % | | 11362814 | 5287 10798 35074 | 60965 35264 28 | 23.510 % | | 17044326 | 5287 10798 35074 | 67062 53937 26 | 23.510 % | | 25566595 | 5287 10798 35074 | 73768 59467 24 | 23.510 % | | 38349998 | 5287 10798 35074 | 81145 19459 30 | 23.510 % | | 57525103 | 5287 10798 35074 | 89260 26379 31 | 23.510 % | | 86287761 | 5287 10798 35074 | 98186 29909 23 | 23.510 % | =============================================================================== restarts : 124922 conflicts : 94877386 (26586 /sec) decisions : 288229420 (0.00 % random) (80765 /sec) propagations : 17089490966 (4788643 /sec) conflict literals : 2605989958 (27.97 % deleted) Memory used : 83.00 MB CPU time : 3568.75 s INDETERMINATE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 6912 | | Number of clauses: 15195 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 6273 13837 46317 | 5073 97 13 | 9.245 % | | 250 | 6239 13461 44901 | 5580 245 16 | 9.737 % | | 475 | 6218 13461 44901 | 6139 468 18 | 10.041 % | | 812 | 6196 13160 43753 | 6752 802 20 | 10.359 % | | 1318 | 6172 13059 43369 | 7428 1304 21 | 10.706 % | | 2077 | 6172 13059 43369 | 8171 2063 23 | 10.706 % | | 3216 | 6172 13059 43369 | 8988 3202 25 | 10.706 % | | 4924 | 6172 13059 43369 | 9886 4910 24 | 10.706 % | | 7486 | 6146 12961 42991 | 10875 7470 25 | 11.082 % | | 11330 | 6146 12961 42991 | 11963 11314 25 | 11.082 % | | 17096 | 6088 12765 42235 | 13159 10672 25 | 11.921 % | | 25745 | 6088 12765 42235 | 14475 12311 27 | 11.921 % | | 38719 | 6021 12583 41563 | 15923 9485 26 | 12.891 % | | 58180 | 6021 12583 41563 | 17515 12102 25 | 12.891 % | | 87372 | 6021 12583 41563 | 19266 13445 29 | 12.891 % | | 131161 | 5985 12485 41185 | 21193 16311 29 | 13.411 % | | 196845 | 5907 12288 40427 | 23312 14209 31 | 14.540 % | | 295371 | 5865 12189 40047 | 25644 12274 24 | 15.148 % | | 443160 | 5775 11992 39289 | 28208 17031 27 | 16.450 % | | 664843 | 5677 11793 38527 | 31029 18334 26 | 17.867 % | | 997368 | 5457 11398 37009 | 34132 18029 32 | 21.050 % | | 1496156 | 5457 11398 37009 | 37545 24142 24 | 21.050 % | | 2244338 | 5454 11333 36817 | 41300 29713 31 | 21.094 % | | 3366612 | 5454 11333 36817 | 45430 21803 24 | 21.094 % | | 5050023 | 5394 11233 36435 | 49973 47041 30 | 21.962 % | | 7575139 | 5394 11233 36435 | 54970 20315 30 | 21.962 % | | 11362814 | 5394 11233 36435 | 60467 30518 33 | 21.962 % | | 17044326 | 5389 11153 36157 | 66514 33384 29 | 22.034 % | | 25566595 | 5389 11153 36157 | 73165 58948 27 | 22.034 % | | 38349998 | 5262 10969 35481 | 80482 59634 31 | 23.872 % | | 57525103 | 5262 10969 35481 | 88530 75730 33 | 23.872 % | | 86287761 | 5262 10969 35481 | 97383 84950 26 | 23.872 % | =============================================================================== restarts : 118360 conflicts : 90437969 (25338 /sec) decisions : 212841199 (0.00 % random) (59633 /sec) propagations : 16364639587 (4584949 /sec) conflict literals : 2615309604 (26.04 % deleted) Memory used : 94.00 MB CPU time : 3569.21 s INDETERMINATE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 6912 | | Number of clauses: 15198 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 6202 14113 47183 | 5174 88 13 | 10.272 % | =============================================================================== restarts : 2 conflicts : 200 (22227 /sec) decisions : 10286 (0.00 % random) (1143143 /sec) propagations : 77718 (8637253 /sec) conflict literals : 2596 (6.82 % deleted) Memory used : 7.00 MB CPU time : 0.008998 s SATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 6912 | | Number of clauses: 15193 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 6321 14166 47409 | 5194 98 13 | 8.550 % | | 250 | 6295 13770 45889 | 5713 244 16 | 8.927 % | | 475 | 6241 13572 45129 | 6284 465 17 | 9.708 % | | 812 | 6241 13474 44751 | 6913 802 19 | 9.708 % | | 1318 | 6219 13375 44371 | 7604 1307 22 | 10.026 % | | 2077 | 6195 13275 43989 | 8365 2064 22 | 10.373 % | | 3216 | 6195 13275 43989 | 9201 3203 24 | 10.373 % | | 4924 | 6169 13175 43607 | 10122 4909 24 | 10.749 % | | 7486 | 6111 12978 42849 | 11134 7467 26 | 11.589 % | | 11330 | 6079 12878 42467 | 12247 11309 27 | 12.052 % | | 17096 | 6045 12779 42087 | 13472 10469 29 | 12.543 % | | 25745 | 6009 12679 41705 | 14819 11911 30 | 13.064 % | | 38719 | 6009 12679 41705 | 16301 8617 29 | 13.064 % | | 58180 | 5971 12579 41323 | 17931 10392 26 | 13.614 % | | 87372 | 5931 12479 40941 | 19724 20334 32 | 14.193 % | | 131161 | 5799 12182 39801 | 21697 20391 28 | 16.102 % | | 196845 | 5701 11982 39037 | 23867 15189 39 | 17.520 % | | 295371 | 5595 11784 38277 | 26253 18272 29 | 19.054 % | | 443160 | 5539 11684 37895 | 28879 25010 34 | 19.864 % | | 664843 | 5359 11385 36751 | 31767 23963 31 | 22.468 % | | 997368 | 5359 11385 36751 | 34943 15488 44 | 22.468 % | | 1496156 | 5295 11285 36369 | 38438 31776 30 | 23.394 % | | 2244338 | 5295 11285 36369 | 42282 24403 37 | 23.394 % | | 3366612 | 5295 11285 36369 | 46510 40907 30 | 23.394 % | | 5050023 | 5295 11285 36369 | 51161 39268 40 | 23.394 % | | 7575139 | 5295 11285 36369 | 56277 44854 41 | 23.394 % | | 11362814 | 5295 11285 36369 | 61905 50873 59 | 23.394 % | | 17044326 | 5295 11285 36369 | 68095 30485 37 | 23.394 % | | 25566595 | 5295 11285 36369 | 74905 43735 38 | 23.394 % | | 38349998 | 5295 11285 36369 | 82396 64268 37 | 23.394 % | | 57525103 | 5295 11285 36369 | 90635 65204 43 | 23.394 % | | 86287761 | 5295 11285 36369 | 99699 17311 26 | 23.394 % | =============================================================================== restarts : 119617 conflicts : 91353772 (25584 /sec) decisions : 215413539 (0.00 % random) (60328 /sec) propagations : 18999750419 (5320981 /sec) conflict literals : 3412540202 (22.83 % deleted) Memory used : 114.00 MB CPU time : 3570.72 s INDETERMINATE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 6912 | | Number of clauses: 15193 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 6232 14532 48688 | 5328 90 13 | 9.838 % | | 250 | 6182 13345 44130 | 5861 238 21 | 10.561 % | | 475 | 6154 13245 43748 | 6447 462 21 | 10.967 % | | 812 | 6124 13245 43748 | 7092 798 22 | 11.400 % | | 1318 | 6124 13146 43368 | 7801 1304 23 | 11.400 % | | 2077 | 6092 13046 42986 | 8581 2061 23 | 11.863 % | | 3216 | 6092 13046 42986 | 9439 3200 27 | 11.863 % | | 4924 | 6092 13046 42986 | 10383 4908 27 | 11.863 % | | 7486 | 6092 13046 42986 | 11421 7470 29 | 11.863 % | | 11330 | 6058 12946 42604 | 12564 11312 29 | 12.355 % | | 17096 | 6022 12846 42222 | 13820 10271 30 | 12.876 % | | 25745 | 5984 12747 41842 | 15202 11510 33 | 13.426 % | | 38719 | 5984 12747 41842 | 16722 16370 32 | 13.426 % | | 58180 | 5944 12648 41462 | 18395 17534 30 | 14.005 % | | 87372 | 5858 12448 40698 | 20234 16953 33 | 15.249 % | | 131161 | 5812 12349 40318 | 22258 17060 33 | 15.914 % | | 196845 | 5714 12151 39558 | 24483 22749 34 | 17.332 % | | 295371 | 5608 11953 38798 | 26932 24333 32 | 18.866 % | | 443160 | 5552 11853 38416 | 29625 25561 44 | 19.676 % | | 664843 | 5552 11853 38416 | 32588 27578 34 | 19.676 % | | 997368 | 5552 11853 38416 | 35846 17635 45 | 19.676 % | | 1496156 | 5552 11853 38416 | 39431 30458 32 | 19.676 % | | 2244338 | 5552 11853 38416 | 43374 28866 48 | 19.676 % | | 3366612 | 5434 11655 37656 | 47712 45376 34 | 21.383 % | | 5050023 | 5434 11655 37656 | 52483 17897 49 | 21.383 % | | 7575139 | 5434 11655 37656 | 57731 33393 35 | 21.383 % | | 11362814 | 5434 11655 37656 | 63504 37634 50 | 21.383 % | | 17044326 | 5434 11655 37656 | 69855 22475 43 | 21.383 % | | 25566595 | 5434 11655 37656 | 76840 51965 40 | 21.383 % | | 38349998 | 5434 11655 37656 | 84524 69700 33 | 21.383 % | | 57525103 | 5434 11655 37656 | 92977 55697 56 | 21.383 % | =============================================================================== restarts : 112057 conflicts : 85533259 (23946 /sec) decisions : 242464896 (0.00 % random) (67882 /sec) propagations : 19504793645 (5460663 /sec) conflict literals : 3452707014 (26.15 % deleted) Memory used : 114.00 MB CPU time : 3571.87 s INDETERMINATE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 6912 | | Number of clauses: 15205 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 6321 14505 48467 | 5318 95 15 | 8.550 % | | 250 | 6287 13912 46189 | 5850 243 18 | 9.042 % | =============================================================================== restarts : 3 conflicts : 250 (25005 /sec) decisions : 10795 (0.00 % random) (1079716 /sec) propagations : 78761 (7877676 /sec) conflict literals : 4472 (6.83 % deleted) Memory used : 7.00 MB CPU time : 0.009998 s SATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 6912 | | Number of clauses: 15212 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 6349 14505 48469 | 5318 97 15 | 8.145 % | | 250 | 6337 14105 46941 | 5850 244 17 | 8.319 % | | 475 | 6337 14105 46941 | 6435 469 23 | 8.319 % | =============================================================================== restarts : 6 conflicts : 627 (41808 /sec) decisions : 12674 (0.00 % random) (845102 /sec) propagations : 142374 (9493499 /sec) conflict literals : 15172 (10.96 % deleted) Memory used : 7.00 MB CPU time : 0.014997 s SATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 6912 | | Number of clauses: 15208 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 6333 14476 48407 | 5307 96 16 | 8.377 % | =============================================================================== restarts : 2 conflicts : 199 (24881 /sec) decisions : 9507 (0.00 % random) (1188672 /sec) propagations : 59315 (7416229 /sec) conflict literals : 3755 (8.93 % deleted) Memory used : 7.00 MB CPU time : 0.007998 s SATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 6912 | | Number of clauses: 15200 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 6343 14364 48001 | 5266 98 16 | 8.232 % | | 250 | 6301 13867 46097 | 5793 244 17 | 8.840 % | | 475 | 6301 13867 46097 | 6372 469 22 | 8.840 % | =============================================================================== restarts : 5 conflicts : 510 (36436 /sec) decisions : 11461 (0.00 % random) (818818 /sec) propagations : 121305 (8666500 /sec) conflict literals : 11099 (9.48 % deleted) Memory used : 7.00 MB CPU time : 0.013997 s SATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 6912 | | Number of clauses: 15213 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 6383 14644 48937 | 5369 99 17 | 7.653 % | | 250 | 6377 14444 48173 | 5906 247 24 | 7.740 % | =============================================================================== restarts : 3 conflicts : 324 (29460 /sec) decisions : 9850 (0.00 % random) (895617 /sec) propagations : 78418 (7130205 /sec) conflict literals : 7221 (8.06 % deleted) Memory used : 7.00 MB CPU time : 0.010998 s SATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 6912 | | Number of clauses: 15210 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 6376 14618 48885 | 5359 97 17 | 7.755 % | =============================================================================== restarts : 2 conflicts : 139 (19863 /sec) decisions : 8127 (0.00 % random) (1161332 /sec) propagations : 44980 (6427551 /sec) conflict literals : 2476 (4.36 % deleted) Memory used : 7.00 MB CPU time : 0.006998 s SATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 6912 | | Number of clauses: 15210 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 6337 14209 47337 | 5209 99 14 | 8.319 % | | 250 | 6337 14109 46955 | 5730 249 22 | 8.319 % | =============================================================================== restarts : 4 conflicts : 451 (34698 /sec) decisions : 11957 (0.00 % random) (919911 /sec) propagations : 99108 (7624865 /sec) conflict literals : 10312 (7.91 % deleted) Memory used : 7.00 MB CPU time : 0.012998 s SATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 6912 | | Number of clauses: 15209 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 6353 14298 47699 | 5242 99 15 | 8.087 % | =============================================================================== restarts : 3 conflicts : 216 (24005 /sec) decisions : 8697 (0.00 % random) (966548 /sec) propagations : 57454 (6385197 /sec) conflict literals : 4353 (5.90 % deleted) Memory used : 7.00 MB CPU time : 0.008998 s SATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 6912 | | Number of clauses: 15213 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 6292 14017 46597 | 5139 97 15 | 8.970 % | | 250 | 6251 13617 45069 | 5653 245 21 | 9.563 % | | 475 | 6251 13617 45069 | 6218 470 26 | 9.563 % | =============================================================================== restarts : 5 conflicts : 515 (39621 /sec) decisions : 10602 (0.00 % random) (815664 /sec) propagations : 110704 (8517003 /sec) conflict literals : 13500 (7.34 % deleted) Memory used : 7.00 MB CPU time : 0.012998 s SATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 6912 | | Number of clauses: 15223 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 6358 14277 47494 | 5234 99 18 | 8.015 % | =============================================================================== restarts : 2 conflicts : 169 (21130 /sec) decisions : 6951 (0.00 % random) (869092 /sec) propagations : 43413 (5427982 /sec) conflict literals : 2910 (4.28 % deleted) Memory used : 7.00 MB CPU time : 0.007998 s SATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 6912 | | Number of clauses: 15228 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 6385 14360 47675 | 5265 100 15 | 7.624 % | | 250 | 6373 14360 47675 | 5791 249 20 | 7.798 % | | 475 | 6373 14259 47291 | 6371 472 26 | 7.798 % | =============================================================================== restarts : 6 conflicts : 743 (43714 /sec) decisions : 12318 (0.00 % random) (724716 /sec) propagations : 145663 (8569924 /sec) conflict literals : 18025 (6.57 % deleted) Memory used : 7.00 MB CPU time : 0.016997 s SATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 6912 | | Number of clauses: 15216 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 6260 13672 45354 | 5013 100 20 | 9.433 % | | 250 | 6238 13672 45354 | 5514 249 22 | 9.751 % | =============================================================================== restarts : 3 conflicts : 350 (38898 /sec) decisions : 8323 (0.00 % random) (924983 /sec) propagations : 62115 (6903201 /sec) conflict literals : 8566 (6.90 % deleted) Memory used : 7.00 MB CPU time : 0.008998 s SATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 6912 | | Number of clauses: 15226 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 6162 13316 43924 | 4882 100 19 | 10.851 % | =============================================================================== restarts : 2 conflicts : 154 (25671 /sec) decisions : 6575 (0.00 % random) (1096016 /sec) propagations : 34899 (5817470 /sec) conflict literals : 3113 (2.05 % deleted) Memory used : 7.00 MB CPU time : 0.005999 s SATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 6912 | | Number of clauses: 15232 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 6113 13124 43341 | 4812 100 27 | 11.560 % | =============================================================================== restarts : 3 conflicts : 225 (32152 /sec) decisions : 6634 (0.00 % random) (947985 /sec) propagations : 44771 (6397685 /sec) conflict literals : 6006 (1.70 % deleted) Memory used : 7.00 MB CPU time : 0.006998 s SATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 6912 | | Number of clauses: 15264 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 6400 14816 49472 | 5432 100 23 | 7.407 % | =============================================================================== restarts : 2 conflicts : 166 (23721 /sec) decisions : 6041 (0.00 % random) (863247 /sec) propagations : 33290 (4757073 /sec) conflict literals : 3876 (1.75 % deleted) Memory used : 7.00 MB CPU time : 0.006998 s