WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 3706 | | Number of clauses: 27512 | | Parse time: 0.00 s | | | =============================================================================== Solved by unit propagation restarts : 0 conflicts : 0 (0 /sec) decisions : 0 (-nan % random) (0 /sec) propagations : 167 (55685 /sec) conflict literals : 0 (-nan % 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: 3706 | | Number of clauses: 29132 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 3066 27120 81642 | 9944 100 5 | 17.269 % | | 250 | 3046 27120 81642 | 10938 246 5 | 17.809 % | | 475 | 2973 27120 81642 | 12032 463 5 | 19.779 % | | 812 | 2770 27120 81642 | 13235 764 5 | 25.256 % | =============================================================================== restarts : 7 conflicts : 1058 (96199 /sec) decisions : 5259 (0.00 % random) (478178 /sec) propagations : 67010 (6092926 /sec) conflict literals : 4853 (13.54 % deleted) Memory used : 7.00 MB CPU time : 0.010998 s UNSATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 3706 | | Number of clauses: 29144 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 3047 26880 80787 | 9856 100 6 | 17.782 % | | 250 | 3043 26880 80787 | 10841 249 5 | 17.890 % | | 475 | 3004 26880 80787 | 11925 471 6 | 18.942 % | | 812 | 2795 26880 80787 | 13118 776 6 | 24.582 % | | 1318 | 2452 18844 54656 | 14430 778 6 | 33.837 % | =============================================================================== restarts : 10 conflicts : 1531 (90075 /sec) decisions : 8656 (0.00 % random) (509266 /sec) propagations : 146655 (8628287 /sec) conflict literals : 7841 (13.16 % deleted) Memory used : 7.00 MB CPU time : 0.016997 s UNSATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 3706 | | Number of clauses: 29161 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 3124 28216 85110 | 10345 100 6 | 15.704 % | | 250 | 3106 28216 85110 | 11380 246 5 | 16.190 % | | 475 | 3072 28216 85110 | 12518 463 5 | 17.108 % | | 812 | 2824 28216 85110 | 13770 749 5 | 23.799 % | | 1318 | 2178 18115 52178 | 15147 760 6 | 41.231 % | =============================================================================== restarts : 10 conflicts : 1532 (85125 /sec) decisions : 9658 (0.00 % random) (536645 /sec) propagations : 172107 (9563094 /sec) conflict literals : 7611 (13.04 % deleted) Memory used : 7.00 MB CPU time : 0.017997 s UNSATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 3706 | | Number of clauses: 29164 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 3120 28098 84744 | 10302 100 6 | 15.812 % | | 250 | 3116 28098 84744 | 11332 249 5 | 15.920 % | | 475 | 3110 28098 84744 | 12466 472 5 | 16.082 % | | 812 | 3013 28098 84744 | 13712 782 5 | 18.700 % | | 1318 | 2446 21676 63184 | 15084 800 6 | 33.999 % | =============================================================================== restarts : 13 conflicts : 1860 (93019 /sec) decisions : 11525 (0.00 % random) (576365 /sec) propagations : 206493 (10326715 /sec) conflict literals : 11193 (11.41 % deleted) Memory used : 7.00 MB CPU time : 0.019996 s UNSATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 3706 | | Number of clauses: 29159 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 3112 28043 84456 | 10282 100 6 | 16.028 % | | 250 | 3108 28043 84456 | 11310 249 5 | 16.136 % | | 475 | 3100 28043 84456 | 12441 472 5 | 16.352 % | | 812 | 2944 28043 84456 | 13685 769 5 | 20.561 % | | 1318 | 2410 18365 52734 | 15054 596 6 | 34.970 % | | 2077 | 2240 14123 40870 | 16559 1156 11 | 39.557 % | =============================================================================== restarts : 14 conflicts : 2098 (83933 /sec) decisions : 11164 (0.00 % random) (446631 /sec) propagations : 246289 (9853137 /sec) conflict literals : 15957 (13.86 % deleted) Memory used : 7.00 MB CPU time : 0.024996 s UNSATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 3706 | | Number of clauses: 29165 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 3139 28429 85701 | 10423 100 6 | 15.300 % | | 250 | 3137 28429 85701 | 11466 249 6 | 15.354 % | | 475 | 3137 28429 85701 | 12612 474 6 | 15.354 % | | 812 | 2956 28429 85701 | 13874 772 5 | 20.237 % | | 1318 | 2629 22275 64895 | 15261 969 6 | 29.061 % | | 2077 | 2480 17184 49635 | 16787 1368 19 | 33.082 % | | 3216 | 2356 15423 44473 | 18466 2418 22 | 36.427 % | | 4924 | 2343 15255 44039 | 20313 4048 22 | 36.778 % | =============================================================================== restarts : 30 conflicts : 5702 (66313 /sec) decisions : 21892 (0.00 % random) (254600 /sec) propagations : 802978 (9338474 /sec) conflict literals : 104350 (38.69 % deleted) Memory used : 7.00 MB CPU time : 0.085986 s UNSATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 3706 | | Number of clauses: 29170 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 3132 28292 85332 | 10373 99 6 | 15.488 % | | 250 | 3130 28292 85332 | 11411 248 5 | 15.542 % | | 475 | 3091 28292 85332 | 12552 465 5 | 16.595 % | | 812 | 3021 28292 85332 | 13807 784 5 | 18.484 % | | 1318 | 2809 22078 63404 | 15188 892 6 | 24.204 % | | 2077 | 2240 14190 40869 | 16707 1150 10 | 39.558 % | | 3216 | 2182 13311 38606 | 18377 2206 20 | 41.123 % | | 4924 | 2097 12668 36958 | 20215 3824 28 | 43.416 % | | 7486 | 2057 12173 35663 | 22237 6315 30 | 44.496 % | | 11330 | 2049 11961 35117 | 24460 10125 28 | 44.712 % | | 17096 | 2047 11949 35086 | 26906 15889 25 | 44.766 % | =============================================================================== restarts : 91 conflicts : 24355 (46575 /sec) decisions : 57596 (0.00 % random) (110143 /sec) propagations : 2733854 (5228054 /sec) conflict literals : 533625 (24.86 % deleted) Memory used : 7.00 MB CPU time : 0.52292 s UNSATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 3706 | | Number of clauses: 29163 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 3130 28305 85470 | 10378 100 6 | 15.542 % | | 250 | 3124 28305 85470 | 11416 248 5 | 15.704 % | | 475 | 3112 28305 85470 | 12557 469 5 | 16.028 % | | 812 | 2983 28305 85470 | 13813 773 5 | 19.509 % | | 1318 | 2616 22303 64250 | 15195 803 6 | 29.412 % | | 2077 | 2332 15099 43375 | 16714 1140 8 | 37.075 % | | 3216 | 2209 13799 39913 | 18386 2098 18 | 40.394 % | | 4924 | 2195 13718 39710 | 20224 3785 24 | 40.772 % | | 7486 | 2195 13625 39481 | 22247 6344 28 | 40.773 % | | 11330 | 2195 13625 39481 | 24471 10188 27 | 40.773 % | | 17096 | 2195 13625 39481 | 26919 15954 26 | 40.773 % | | 25745 | 2143 13073 38015 | 29611 24516 27 | 42.177 % | | 38719 | 2136 12991 37789 | 32572 18412 28 | 42.365 % | =============================================================================== restarts : 185 conflicts : 57903 (30053 /sec) decisions : 100109 (0.00 % random) (51959 /sec) propagations : 5583196 (2897792 /sec) conflict literals : 1415781 (36.34 % deleted) Memory used : 12.00 MB CPU time : 1.92671 s UNSATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 3706 | | Number of clauses: 29159 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 3140 28447 85886 | 10430 100 5 | 15.273 % | | 250 | 3138 28447 85886 | 11473 249 5 | 15.327 % | | 475 | 3130 28447 85886 | 12620 471 5 | 15.542 % | | 812 | 3005 28447 85886 | 13883 770 5 | 18.915 % | | 1318 | 2223 13610 38385 | 15271 405 7 | 40.016 % | | 2077 | 2061 12228 34965 | 16798 1001 17 | 44.387 % | | 3216 | 2052 12010 34421 | 18478 2124 47 | 44.630 % | | 4924 | 2027 11961 34299 | 20326 3807 62 | 45.305 % | | 7486 | 2022 11711 33674 | 22358 6361 63 | 45.440 % | | 11330 | 2009 11691 33624 | 24594 10191 59 | 45.791 % | | 17096 | 2001 11558 33295 | 27054 15948 53 | 46.006 % | | 25745 | 2001 11498 33150 | 29759 24590 52 | 46.006 % | | 38719 | 1995 11438 33000 | 32735 19112 41 | 46.168 % | | 58180 | 1929 10931 31775 | 36009 18376 30 | 47.949 % | | 87372 | 1864 10460 30488 | 39610 17849 23 | 49.703 % | =============================================================================== restarts : 255 conflicts : 90833 (15596 /sec) decisions : 142689 (0.00 % random) (24500 /sec) propagations : 8495443 (1458667 /sec) conflict literals : 3168469 (17.87 % deleted) Memory used : 19.00 MB CPU time : 5.82411 s UNSATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 3706 | | Number of clauses: 29179 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 3162 28610 86382 | 10490 100 6 | 14.679 % | | 250 | 3162 28610 86382 | 11539 250 6 | 14.679 % | | 475 | 3146 28610 86382 | 12693 469 5 | 15.111 % | | 812 | 3069 28610 86382 | 13962 784 5 | 17.188 % | | 1318 | 2758 21072 60188 | 15358 779 6 | 25.580 % | | 2077 | 2426 16034 45751 | 16894 1125 7 | 34.539 % | | 3216 | 2299 14729 42382 | 18584 2152 28 | 37.966 % | | 4924 | 2258 14242 41089 | 20442 3797 40 | 39.072 % | | 7486 | 2253 14152 40854 | 22486 6346 50 | 39.207 % | | 11330 | 2155 14064 40630 | 24735 10156 54 | 41.852 % | | 17096 | 2145 13138 38137 | 27209 15811 56 | 42.121 % | | 25745 | 2007 12847 37397 | 29930 24373 55 | 45.846 % | | 38719 | 1985 11648 34327 | 32923 19347 48 | 46.439 % | | 58180 | 1968 11568 34132 | 36215 19899 47 | 46.897 % | | 87372 | 1951 11298 33422 | 39837 27804 44 | 47.356 % | | 131161 | 1931 11125 32993 | 43820 17162 43 | 47.896 % | | 196845 | 1889 10777 32134 | 48202 22864 43 | 49.029 % | | 295371 | 1829 10281 30815 | 53023 19603 43 | 50.648 % | | 443160 | 1602 8621 26201 | 58325 54398 41 | 56.773 % | =============================================================================== restarts : 1420 conflicts : 663329 (13158 /sec) decisions : 972393 (0.00 % random) (19288 /sec) propagations : 56477249 (1120262 /sec) conflict literals : 30594174 (20.36 % deleted) Memory used : 39.00 MB CPU time : 50.4143 s UNSATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 3706 | | Number of clauses: 29174 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 3143 28348 85483 | 10394 100 5 | 15.192 % | | 250 | 3103 28348 85483 | 11433 234 5 | 16.271 % | | 475 | 3091 28348 85483 | 12577 456 5 | 16.595 % | | 812 | 2993 28348 85483 | 13834 779 5 | 19.239 % | | 1318 | 2886 22849 65301 | 15218 922 6 | 22.126 % | | 2077 | 2526 17129 49002 | 16740 1212 10 | 31.840 % | | 3216 | 2445 16047 46069 | 18414 2255 37 | 34.026 % | =============================================================================== restarts : 21 conflicts : 3825 (40270 /sec) decisions : 35517 (0.00 % random) (373922 /sec) propagations : 679780 (7156709 /sec) conflict literals : 134316 (7.04 % deleted) Memory used : 7.00 MB CPU time : 0.094985 s SATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 3706 | | Number of clauses: 29170 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 3140 28319 85306 | 10383 99 6 | 15.273 % | | 250 | 3136 28319 85306 | 11421 247 5 | 15.380 % | | 475 | 3108 28319 85306 | 12564 465 5 | 16.136 % | | 812 | 3053 28319 85306 | 13820 791 5 | 17.620 % | | 1318 | 2804 21546 61363 | 15202 766 6 | 24.339 % | | 2077 | 2582 17560 49737 | 16722 1259 10 | 30.329 % | | 3216 | 2518 16775 47714 | 18395 2343 40 | 32.056 % | | 4924 | 2445 16414 46781 | 20234 3986 57 | 34.026 % | | 7486 | 2397 15458 44290 | 22258 6434 71 | 35.322 % | | 11330 | 2379 15309 43908 | 24484 10255 76 | 35.808 % | | 17096 | 2349 15309 43908 | 26932 15994 81 | 36.617 % | | 25745 | 2297 14845 42704 | 29625 24554 85 | 38.019 % | | 38719 | 2252 14254 41212 | 32588 19928 105 | 39.234 % | | 58180 | 2240 14075 40747 | 35847 19572 93 | 39.558 % | | 87372 | 2205 13848 40189 | 39431 26214 71 | 40.502 % | | 131161 | 2022 12313 36244 | 43375 16033 75 | 45.440 % | =============================================================================== restarts : 440 conflicts : 160639 (15154 /sec) decisions : 373836 (0.00 % random) (35266 /sec) propagations : 17763939 (1675782 /sec) conflict literals : 14641081 (16.90 % deleted) Memory used : 38.00 MB CPU time : 10.6004 s SATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 3706 | | Number of clauses: 29166 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 3132 28164 84896 | 10326 100 6 | 15.488 % | | 250 | 3132 28164 84896 | 11359 250 6 | 15.488 % | | 475 | 3115 28164 84896 | 12495 472 5 | 15.947 % | | 812 | 2974 28164 84896 | 13744 786 5 | 19.752 % | | 1318 | 2745 21344 60798 | 15119 713 6 | 25.932 % | | 2077 | 2505 16941 48090 | 16631 1158 9 | 32.407 % | | 3216 | 2349 15254 43712 | 18294 2142 28 | 36.616 % | | 4924 | 2252 14497 41697 | 20124 3733 50 | 39.234 % | | 7486 | 2241 14329 41263 | 22136 6271 79 | 39.530 % | | 11330 | 2220 14276 41124 | 24350 10090 88 | 40.098 % | | 17096 | 2216 13989 40353 | 26785 15815 98 | 40.206 % | | 25745 | 2195 13953 40260 | 29463 24443 100 | 40.772 % | | 38719 | 2187 13621 39386 | 32409 19030 103 | 40.988 % | | 58180 | 2157 13533 39157 | 35650 17197 107 | 41.797 % | | 87372 | 2150 13300 38541 | 39216 21659 112 | 41.986 % | | 131161 | 2129 13251 38419 | 43137 38585 110 | 42.553 % | | 196845 | 1829 10581 30995 | 47451 35976 100 | 50.648 % | =============================================================================== restarts : 511 conflicts : 211926 (11872 /sec) decisions : 438678 (0.00 % random) (24574 /sec) propagations : 27315933 (1530194 /sec) conflict literals : 23483535 (13.58 % deleted) Memory used : 52.00 MB CPU time : 17.8513 s UNSATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 3706 | | Number of clauses: 29168 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 3125 28080 84575 | 10296 99 5 | 15.677 % | | 250 | 3119 28080 84575 | 11325 247 5 | 15.839 % | | 475 | 3075 28080 84575 | 12458 465 5 | 17.027 % | | 812 | 2850 28080 84575 | 13703 737 5 | 23.098 % | | 1318 | 2405 17247 48126 | 15074 501 8 | 35.105 % | =============================================================================== restarts : 11 conflicts : 1609 (61894 /sec) decisions : 13862 (0.00 % random) (533236 /sec) propagations : 191876 (7380982 /sec) conflict literals : 8979 (8.36 % deleted) Memory used : 7.00 MB CPU time : 0.025996 s UNSATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 3706 | | Number of clauses: 29171 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 3143 28266 85171 | 10364 100 6 | 15.192 % | | 250 | 3143 28266 85171 | 11400 250 6 | 15.192 % | | 475 | 3121 28266 85171 | 12540 469 6 | 15.785 % | | 812 | 3041 28266 85171 | 13794 784 6 | 17.944 % | | 1318 | 2986 24135 69508 | 15174 947 6 | 19.428 % | | 2077 | 2656 18762 52989 | 16691 1227 8 | 28.332 % | | 3216 | 2536 17388 49374 | 18360 2218 28 | 31.571 % | | 4924 | 2497 16943 48216 | 20196 3882 70 | 32.624 % | | 7486 | 2485 16588 47256 | 22216 6413 85 | 32.947 % | | 11330 | 2456 16311 46539 | 24438 10209 94 | 33.730 % | | 17096 | 2445 16311 46539 | 26882 15966 114 | 34.026 % | | 25745 | 2419 16147 46127 | 29570 24598 122 | 34.728 % | | 38719 | 2390 15693 45003 | 32527 19510 134 | 35.511 % | | 58180 | 2356 15693 45003 | 35780 18850 122 | 36.427 % | | 87372 | 2343 15189 43714 | 39358 23900 161 | 36.779 % | =============================================================================== restarts : 268 conflicts : 104515 (14086 /sec) decisions : 286731 (0.00 % random) (38644 /sec) propagations : 13887421 (1871652 /sec) conflict literals : 15390484 (16.01 % deleted) Memory used : 52.00 MB CPU time : 7.41987 s SATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 3706 | | Number of clauses: 29166 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 3145 28319 85397 | 10383 100 6 | 15.138 % | | 250 | 3145 28319 85397 | 11421 250 6 | 15.138 % | | 475 | 3135 28319 85397 | 12564 471 6 | 15.407 % | | 812 | 3064 28319 85397 | 13820 787 6 | 17.323 % | | 1318 | 2865 22967 65903 | 15202 753 6 | 22.693 % | =============================================================================== restarts : 13 conflicts : 1872 (53495 /sec) decisions : 19027 (0.00 % random) (543722 /sec) propagations : 265344 (7582557 /sec) conflict literals : 11039 (9.94 % deleted) Memory used : 7.00 MB CPU time : 0.034994 s UNSATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 3706 | | Number of clauses: 29166 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 3156 28535 86226 | 10462 100 7 | 14.841 % | | 250 | 3152 28535 86226 | 11509 249 5 | 14.949 % | | 475 | 3141 28535 86226 | 12660 468 5 | 15.246 % | | 812 | 3058 28535 86226 | 13926 772 6 | 17.485 % | | 1318 | 3023 24947 72213 | 15318 993 7 | 18.430 % | | 2077 | 2742 19506 54976 | 16850 1209 9 | 26.012 % | =============================================================================== restarts : 14 conflicts : 2250 (42460 /sec) decisions : 29747 (0.00 % random) (561359 /sec) propagations : 445704 (8410938 /sec) conflict literals : 17439 (7.79 % deleted) Memory used : 7.00 MB CPU time : 0.052991 s UNSATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 3706 | | Number of clauses: 29178 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 3167 28538 86095 | 10463 100 7 | 14.544 % | | 250 | 3165 28538 86095 | 11510 249 6 | 14.598 % | | 475 | 3131 28538 86095 | 12661 463 7 | 15.515 % | | 812 | 3073 28538 86095 | 13927 780 7 | 17.081 % | | 1318 | 2977 25322 72937 | 15320 1187 7 | 19.671 % | | 2077 | 2745 19746 55387 | 16852 1259 9 | 25.931 % | =============================================================================== restarts : 15 conflicts : 2956 (33982 /sec) decisions : 49789 (0.00 % random) (572379 /sec) propagations : 735235 (8452337 /sec) conflict literals : 56188 (7.00 % deleted) Memory used : 7.00 MB CPU time : 0.086986 s SATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 3706 | | Number of clauses: 29185 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 3169 28538 86097 | 10463 100 6 | 14.490 % | | 250 | 3159 28538 86097 | 11510 245 5 | 14.760 % | | 475 | 3149 28538 86097 | 12661 465 5 | 15.030 % | | 812 | 3098 28538 86097 | 13927 790 6 | 16.406 % | | 1318 | 2887 23906 68312 | 15320 905 7 | 22.099 % | | 2077 | 2706 19158 54140 | 16852 1216 9 | 26.983 % | =============================================================================== restarts : 14 conflicts : 2405 (41472 /sec) decisions : 32504 (0.00 % random) (560501 /sec) propagations : 511589 (8821869 /sec) conflict literals : 16896 (5.85 % deleted) Memory used : 7.00 MB CPU time : 0.057991 s SATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 3706 | | Number of clauses: 29181 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 3165 28509 86035 | 10453 100 7 | 14.598 % | | 250 | 3165 28509 86035 | 11498 250 8 | 14.598 % | | 475 | 3137 28509 86035 | 12648 473 7 | 15.353 % | | 812 | 3119 28509 86035 | 13913 800 6 | 15.839 % | | 1318 | 3039 26073 76533 | 15304 999 6 | 17.998 % | | 2077 | 2797 20658 58313 | 16835 1265 7 | 24.528 % | =============================================================================== restarts : 15 conflicts : 2471 (41190 /sec) decisions : 37397 (0.00 % random) (623387 /sec) propagations : 507364 (8457476 /sec) conflict literals : 27846 (5.43 % deleted) Memory used : 7.00 MB CPU time : 0.05999 s SATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 3706 | | Number of clauses: 29173 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 3161 28427 85719 | 10423 100 6 | 14.706 % | | 250 | 3149 28427 85719 | 11465 247 5 | 15.030 % | | 475 | 3141 28427 85719 | 12612 468 6 | 15.246 % | | 812 | 3045 28427 85719 | 13873 783 6 | 17.836 % | | 1318 | 2927 22189 62760 | 15260 688 7 | 21.020 % | =============================================================================== restarts : 13 conflicts : 1826 (43483 /sec) decisions : 22338 (0.00 % random) (531946 /sec) propagations : 352310 (8389732 /sec) conflict literals : 11733 (8.94 % deleted) Memory used : 7.00 MB CPU time : 0.041993 s SATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 3706 | | Number of clauses: 29186 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 3181 28647 86475 | 10503 100 6 | 14.166 % | | 250 | 3179 28647 86475 | 11554 249 5 | 14.220 % | | 475 | 3152 28647 86475 | 12709 465 5 | 14.949 % | | 812 | 3085 28647 86475 | 13980 780 5 | 16.757 % | | 1318 | 3048 24938 72006 | 15378 943 6 | 17.755 % | | 2077 | 2769 19988 56486 | 16916 1256 8 | 25.283 % | | 3216 | 2691 18893 53661 | 18608 2298 45 | 27.388 % | =============================================================================== restarts : 18 conflicts : 3537 (35376 /sec) decisions : 50651 (0.00 % random) (506591 /sec) propagations : 785572 (7856977 /sec) conflict literals : 146629 (2.85 % deleted) Memory used : 8.00 MB CPU time : 0.099984 s SATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 3706 | | Number of clauses: 29183 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 3181 28621 86423 | 10494 100 6 | 14.166 % | | 250 | 3165 28621 86423 | 11543 246 5 | 14.598 % | | 475 | 3151 28621 86423 | 12698 464 5 | 14.976 % | | 812 | 3032 28621 86423 | 13968 767 5 | 18.187 % | | 1318 | 2972 23013 65447 | 15364 781 7 | 19.806 % | =============================================================================== restarts : 12 conflicts : 1746 (58210 /sec) decisions : 18052 (0.00 % random) (601834 /sec) propagations : 265196 (8841340 /sec) conflict literals : 10610 (8.61 % deleted) Memory used : 8.00 MB CPU time : 0.029995 s SATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 3706 | | Number of clauses: 29183 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 3163 28332 85235 | 10388 100 6 | 14.652 % | | 250 | 3157 28332 85235 | 11427 249 5 | 14.814 % | | 475 | 3131 28332 85235 | 12569 467 5 | 15.515 % | | 812 | 3066 28332 85235 | 13826 780 5 | 17.269 % | | 1318 | 3034 25290 73218 | 15209 994 6 | 18.133 % | =============================================================================== restarts : 12 conflicts : 1782 (54010 /sec) decisions : 16591 (0.00 % random) (502849 /sec) propagations : 239537 (7260017 /sec) conflict literals : 10674 (7.67 % deleted) Memory used : 7.00 MB CPU time : 0.032994 s SATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 3706 | | Number of clauses: 29182 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 3169 28391 85507 | 10410 100 6 | 14.490 % | | 250 | 3167 28391 85507 | 11451 249 5 | 14.544 % | | 475 | 3139 28391 85507 | 12596 466 5 | 15.300 % | | 812 | 3059 28391 85507 | 13855 778 5 | 17.458 % | | 1318 | 2991 24280 69609 | 15241 1003 6 | 19.293 % | =============================================================================== restarts : 12 conflicts : 1726 (52313 /sec) decisions : 17300 (0.00 % random) (524338 /sec) propagations : 268242 (8130024 /sec) conflict literals : 10798 (8.72 % deleted) Memory used : 7.00 MB CPU time : 0.032994 s SATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 3706 | | Number of clauses: 29186 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 3159 28200 84675 | 10340 98 5 | 14.760 % | | 250 | 3151 28200 84675 | 11374 244 5 | 14.976 % | | 475 | 3139 28200 84675 | 12511 464 5 | 15.300 % | | 812 | 3056 28200 84675 | 13762 776 5 | 17.539 % | | 1318 | 3043 24602 70459 | 15138 948 6 | 17.890 % | =============================================================================== restarts : 9 conflicts : 1322 (69590 /sec) decisions : 10376 (0.00 % random) (546192 /sec) propagations : 114020 (6002000 /sec) conflict literals : 7343 (13.64 % deleted) Memory used : 7.00 MB CPU time : 0.018997 s SATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 3706 | | Number of clauses: 29196 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 3180 28400 85392 | 10413 99 5 | 14.193 % | | 250 | 3178 28400 85392 | 11454 248 5 | 14.247 % | | 475 | 3166 28400 85392 | 12600 469 5 | 14.571 % | | 812 | 3082 28400 85392 | 13860 772 5 | 16.838 % | | 1318 | 2989 23891 68006 | 15246 834 6 | 19.347 % | =============================================================================== restarts : 10 conflicts : 1560 (60009 /sec) decisions : 16880 (0.00 % random) (649331 /sec) propagations : 226722 (8721419 /sec) conflict literals : 9969 (10.11 % deleted) Memory used : 7.00 MB CPU time : 0.025996 s SATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 3706 | | Number of clauses: 29201 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 3199 28483 85573 | 10443 100 6 | 13.681 % | | 250 | 3199 28483 85573 | 11488 250 6 | 13.681 % | | 475 | 3183 28483 85573 | 12636 468 5 | 14.112 % | | 812 | 3108 28483 85573 | 13900 784 5 | 16.136 % | | 1318 | 3064 24818 71535 | 15290 916 7 | 17.323 % | | 2077 | 2959 22537 63800 | 16819 1430 28 | 20.157 % | | 3216 | 2944 22036 62164 | 18501 2514 77 | 20.561 % | =============================================================================== restarts : 23 conflicts : 4437 (34943 /sec) decisions : 35513 (0.00 % random) (279674 /sec) propagations : 686134 (5403481 /sec) conflict literals : 383090 (4.32 % deleted) Memory used : 8.00 MB CPU time : 0.12698 s SATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 3706 | | Number of clauses: 29189 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 3144 27945 83702 | 10246 100 6 | 15.165 % | | 250 | 3144 27945 83702 | 11271 250 6 | 15.165 % | | 475 | 3114 27945 83702 | 12398 467 5 | 15.974 % | | 812 | 3054 27945 83702 | 13638 784 5 | 17.593 % | | 1318 | 3012 24519 70527 | 15001 869 6 | 18.727 % | | 2077 | 2946 23192 66210 | 16502 1492 29 | 20.507 % | | 3216 | 2944 22698 64759 | 18152 2553 85 | 20.561 % | =============================================================================== restarts : 17 conflicts : 3366 (39146 /sec) decisions : 24583 (0.00 % random) (285895 /sec) propagations : 459140 (5339706 /sec) conflict literals : 236482 (3.14 % deleted) Memory used : 8.00 MB CPU time : 0.085986 s SATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 3706 | | Number of clauses: 29199 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 3138 27709 82632 | 10159 100 6 | 15.327 % | | 250 | 3128 27709 82632 | 11175 247 5 | 15.596 % | | 475 | 3124 27709 82632 | 12293 470 5 | 15.704 % | | 812 | 3059 27709 82632 | 13522 788 5 | 17.458 % | =============================================================================== restarts : 7 conflicts : 1066 (82013 /sec) decisions : 5939 (0.00 % random) (456916 /sec) propagations : 63667 (4898215 /sec) conflict literals : 5772 (13.99 % 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: 3706 | | Number of clauses: 29205 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 3117 27547 82139 | 10100 100 6 | 15.893 % | | 250 | 3117 27547 82139 | 11110 250 6 | 15.893 % | | 475 | 3099 27547 82139 | 12221 472 6 | 16.379 % | | 812 | 3048 27547 82139 | 13443 800 6 | 17.755 % | | 1318 | 3048 27547 82139 | 14788 1306 22 | 17.755 % | | 2077 | 2952 23252 66888 | 16267 1566 41 | 20.345 % | | 3216 | 2952 23252 66888 | 17893 2705 76 | 20.345 % | | 4924 | 2947 23214 66777 | 19683 4410 107 | 20.480 % | =============================================================================== restarts : 30 conflicts : 5625 (35607 /sec) decisions : 34254 (0.00 % random) (216832 /sec) propagations : 739411 (4680557 /sec) conflict literals : 641067 (2.99 % deleted) Memory used : 7.00 MB CPU time : 0.157975 s SATISFIABLE WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 3706 | | Number of clauses: 29237 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 3194 28789 86920 | 10555 100 5 | 13.815 % | | 250 | 3194 28789 86920 | 11611 250 6 | 13.815 % | | 475 | 3186 28789 86920 | 12772 472 6 | 14.031 % | | 812 | 3136 28789 86920 | 14049 798 5 | 15.380 % | | 1318 | 3082 26341 77500 | 15454 939 7 | 16.838 % | =============================================================================== restarts : 9 conflicts : 1378 (76568 /sec) decisions : 9234 (0.00 % random) (513086 /sec) propagations : 110001 (6112185 /sec) conflict literals : 8289 (11.46 % deleted) Memory used : 7.00 MB CPU time : 0.017997 s SATISFIABLE