Name | normalized-opb/mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-markshare1.opb |
MD5SUM | 10386fd19d9976c249ce2be861b38a70 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 63488 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 180 |
Biggest coefficient in the objective function | 536870912 |
Number of bits for the biggest coefficient in the objective function | 30 |
Sum of the numbers in the objective function | 6442450938 |
Number of bits of the sum of numbers in the objective function | 33 |
Biggest number in a constraint | 536870912 |
Number of bits of the biggest number in a constraint | 30 |
Biggest sum of numbers in a constraint | 6442450938 |
Number of bits of the biggest sum of numbers | 33 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1175.12 |
Number of variables | 230 |
Total number of constraints | 56 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 50 |
Number of constraints which are nor clauses,nor cardinality constraints | 6 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 80 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc21 THE 2005-04-21 08:23:31 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=12641 boxname=wulflinc21 idbench=973 idsolver=5 numberseed=0 MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4 /oldhome/oroussel/solvers/minisat+ MD5SUM BENCH: 10386fd19d9976c249ce2be861b38a70 /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-markshare1.opb REAL COMMAND: minisat+ /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-markshare1.opb IDLAUNCH: 12641 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.161 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.161 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 621076 kB Buffers: 3616 kB Cached: 387112 kB SwapCached: 0 kB Active: 28284 kB Inactive: 365352 kB HighTotal: 131008 kB HighFree: 22288 kB LowTotal: 903652 kB LowFree: 598788 kB SwapTotal: 2097892 kB SwapFree: 2097804 kB Dirty: 40 kB Writeback: 0 kB Mapped: 6948 kB Slab: 14304 kB Committed_AS: 63796 kB PageTables: 332 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-21 08:43:33 (client local time) WITH STATUS 10 IN 1200.19 SECONDS stats: 12641 7 1200.19 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 12 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ###### c -- Clauses(.)/Splits(s): (none) c ---[ 10]---> Adder-cost: 304 maxlim: 3240959 bits: 23/22 c ---[ 8]---> Adder-cost: 314 maxlim: 3453951 bits: 23/22 c ---[ 6]---> Adder-cost: 348 maxlim: 3482623 bits: 23/22 c ---[ 4]---> Adder-cost: 318 maxlim: 3294207 bits: 23/22 c ---[ 2]---> Adder-cost: 312 maxlim: 3286015 bits: 23/22 c ---[ 0]---> Adder-cost: 314 maxlim: 3289087 bits: 23/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 12820 45524 | 4273 0 0 nan | 0.000 % | c | 100 | 12820 45524 | 4700 100 594 5.9 | 14.261 % | c ============================================================================== c [1mFound solution: 4615168[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 850 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 141 | 14814 50194 | 4938 141 1027 7.3 | 14.261 % | c | 241 | 14814 50194 | 5431 241 12192 50.6 | 10.969 % | c | 393 | 14814 50194 | 5974 393 26032 66.2 | 10.969 % | c | 618 | 14814 50194 | 6572 618 37060 60.0 | 10.969 % | c | 955 | 14814 50194 | 7229 955 69049 72.3 | 10.969 % | c ============================================================================== c [1mFound solution: 4444160[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1006 | 14929 50490 | 4976 1006 70987 70.6 | 10.969 % | c | 1107 | 14929 50490 | 5473 1107 85930 77.6 | 10.770 % | c ============================================================================== c [1mFound solution: 4152320[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1139 | 14941 50532 | 4980 1139 86375 75.8 | 10.770 % | c | 1240 | 14941 50532 | 5478 1240 94355 76.1 | 10.771 % | c | 1390 | 14941 50532 | 6025 1390 106104 76.3 | 10.771 % | c ============================================================================== c [1mFound solution: 3231744[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1590 | 14951 50556 | 4983 1590 117597 74.0 | 10.771 % | c | 1691 | 14951 50556 | 5481 1691 130635 77.3 | 10.786 % | c | 1841 | 14951 50556 | 6029 1841 142489 77.4 | 10.786 % | c | 2067 | 14943 50530 | 6632 2066 165570 80.1 | 10.819 % | c | 2404 | 14943 50530 | 7295 2403 186034 77.4 | 10.819 % | c | 2910 | 14943 50530 | 8025 2909 234223 80.5 | 10.819 % | c | 3669 | 14935 50504 | 8827 3667 297711 81.2 | 10.852 % | c | 4810 | 14919 50452 | 9710 4806 397534 82.7 | 10.917 % | c | 6518 | 14919 50452 | 10681 6514 543132 83.4 | 10.917 % | c | 9081 | 14919 50452 | 11749 9077 695094 76.6 | 10.917 % | c ============================================================================== c [1mFound solution: 3212288[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 11955 | 14931 50479 | 4977 11951 922500 77.2 | 10.917 % | c | 12056 | 14931 50479 | 5474 3089 184035 59.6 | 10.932 % | c | 12207 | 14931 50479 | 6022 3240 193746 59.8 | 10.932 % | c | 12433 | 14931 50479 | 6624 3466 204232 58.9 | 10.932 % | c | 12770 | 14931 50479 | 7286 3803 246752 64.9 | 10.932 % | c | 13278 | 14923 50453 | 8015 4310 287955 66.8 | 10.965 % | c | 14042 | 14923 50453 | 8817 5074 357875 70.5 | 10.965 % | c | 15182 | 14923 50453 | 9698 6214 454785 73.2 | 10.965 % | c | 16891 | 14923 50453 | 10668 7923 596983 75.3 | 10.965 % | c | 19453 | 14915 50427 | 11735 10484 806542 76.9 | 10.998 % | c | 23299 | 14907 50401 | 12909 7910 531028 67.1 | 11.031 % | c | 29065 | 14891 50349 | 14199 13674 1005814 73.6 | 11.097 % | c | 37715 | 14884 50334 | 15619 14705 1118217 76.0 | 11.162 % | c ============================================================================== c [1mFound solution: 3169280[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 45485 | 14886 50339 | 4962 14152 1130949 79.9 | 11.162 % | c | 45586 | 14886 50339 | 5458 3639 207343 57.0 | 11.253 % | c | 45736 | 14886 50339 | 6004 3789 218603 57.7 | 11.253 % | c | 45961 | 14886 50339 | 6604 4014 238535 59.4 | 11.253 % | c | 46300 | 14886 50339 | 7264 4353 272968 62.7 | 11.253 % | c | 46807 | 14878 50313 | 7991 4859 321893 66.2 | 11.286 % | c | 47567 | 14878 50313 | 8790 5619 395734 70.4 | 11.286 % | c | 48706 | 14878 50313 | 9669 6758 514295 76.1 | 11.286 % | c | 50414 | 14878 50313 | 10636 8466 674245 79.6 | 11.286 % | c | 52979 | 14878 50313 | 11700 11031 894758 81.1 | 11.286 % | c | 56823 | 14878 50313 | 12870 8476 585487 69.1 | 11.286 % | c | 62589 | 14878 50313 | 14157 7246 470267 64.9 | 11.286 % | c | 71238 | 14878 50313 | 15572 8340 484689 58.1 | 11.286 % | c ============================================================================== c [1mFound solution: 3042304[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 81326 | 14886 50332 | 4962 10127 656025 64.8 | 11.286 % | c | 81428 | 14886 50332 | 5458 5166 279097 54.0 | 11.300 % | c | 81579 | 14886 50332 | 6004 5317 292474 55.0 | 11.300 % | c | 81804 | 14886 50332 | 6604 5542 307973 55.6 | 11.300 % | c | 82141 | 14886 50332 | 7264 5879 344300 58.6 | 11.300 % | c | 82647 | 14886 50332 | 7991 6385 389480 61.0 | 11.300 % | c | 83406 | 14886 50332 | 8790 7144 439505 61.5 | 11.300 % | c | 84547 | 14886 50332 | 9669 8285 529161 63.9 | 11.300 % | c | 86259 | 14886 50332 | 10636 9997 662102 66.2 | 11.300 % | c | 88822 | 14886 50332 | 11700 6767 420905 62.2 | 11.300 % | c | 92668 | 14886 50332 | 12870 10613 744951 70.2 | 11.300 % | c | 98434 | 14886 50332 | 14157 9409 652200 69.3 | 11.300 % | c | 107085 | 14886 50332 | 15572 10478 637247 60.8 | 11.300 % | c ============================================================================== c [1mFound solution: 3005440[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 111385 | 14888 50336 | 4962 14777 921886 62.4 | 11.300 % | c | 111486 | 14888 50336 | 5458 3796 173019 45.6 | 11.344 % | c | 111636 | 14888 50336 | 6004 3946 179318 45.4 | 11.344 % | c | 111861 | 14888 50336 | 6604 4171 192217 46.1 | 11.344 % | c | 112199 | 14880 50310 | 7264 4508 220479 48.9 | 11.376 % | c | 112705 | 14880 50310 | 7991 5014 263662 52.6 | 11.376 % | c | 113465 | 14880 50310 | 8790 5774 310667 53.8 | 11.376 % | c | 114604 | 14880 50310 | 9669 6913 409090 59.2 | 11.376 % | c | 116313 | 14872 50284 | 10636 8621 542723 63.0 | 11.409 % | c | 118875 | 14864 50258 | 11700 11182 716184 64.0 | 11.442 % | c | 122719 | 14864 50258 | 12870 8765 560433 63.9 | 11.442 % | c ============================================================================== c [1mFound solution: 2816000[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 124383 | 14877 50289 | 4959 10429 657968 63.1 | 11.442 % | c | 124484 | 14877 50289 | 5454 5316 265689 50.0 | 11.448 % | c | 124635 | 14877 50289 | 6000 5467 270323 49.4 | 11.448 % | c | 124860 | 14877 50289 | 6600 5692 292327 51.4 | 11.448 % | c | 125197 | 14877 50289 | 7260 6029 329895 54.7 | 11.448 % | c | 125703 | 14877 50289 | 7986 6535 361239 55.3 | 11.448 % | c | 126462 | 14877 50289 | 8785 7294 391859 53.7 | 11.448 % | c | 127603 | 14877 50289 | 9663 8435 478713 56.8 | 11.448 % | c | 129311 | 14877 50289 | 10630 10143 570334 56.2 | 11.448 % | c | 131874 | 14877 50289 | 11693 7035 309663 44.0 | 11.448 % | c ============================================================================== c [1mFound solution: 1213440[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 132830 | 14885 50302 | 4961 7990 344228 43.1 | 11.448 % | c | 132930 | 14885 50302 | 5457 4095 130652 31.9 | 11.487 % | c | 133082 | 14885 50302 | 6002 4247 140906 33.2 | 11.487 % | c | 133308 | 14885 50302 | 6603 4473 145839 32.6 | 11.487 % | c | 133645 | 14885 50302 | 7263 4810 163247 33.9 | 11.487 % | c | 134152 | 14885 50302 | 7989 5317 180646 34.0 | 11.487 % | c | 134911 | 14867 50262 | 8788 6074 210613 34.7 | 11.650 % | c | 136050 | 14867 50262 | 9667 7213 249425 34.6 | 11.650 % | c | 137760 | 14839 50199 | 10634 8921 304715 34.2 | 11.910 % | c | 140322 | 14839 50199 | 11697 11483 433802 37.8 | 11.910 % | c | 144166 | 14839 50199 | 12867 9063 353815 39.0 | 11.910 % | c | 149933 | 14839 50199 | 14154 7885 325078 41.2 | 11.910 % | c | 158582 | 14839 50199 | 15569 9129 370373 40.6 | 11.910 % | c | 171556 | 14839 50199 | 17126 13879 596591 43.0 | 11.910 % | c ============================================================================== c [1mFound solution: 1145856[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 183021 | 14849 50222 | 4949 16407 675729 41.2 | 11.910 % | c | 183123 | 14849 50222 | 5443 4204 124504 29.6 | 11.927 % | c | 183273 | 14849 50222 | 5988 4354 127342 29.2 | 11.927 % | c | 183498 | 14849 50222 | 6587 4579 133579 29.2 | 11.927 % | c | 183836 | 14849 50222 | 7245 4917 140722 28.6 | 11.927 % | c | 184343 | 14849 50222 | 7970 5424 153528 28.3 | 11.927 % | c | 185102 | 14849 50222 | 8767 6183 178163 28.8 | 11.927 % | c | 186244 | 14849 50222 | 9644 7325 224903 30.7 | 11.927 % | c | 187953 | 14849 50222 | 10608 9034 306970 34.0 | 11.927 % | c | 190516 | 14849 50222 | 11669 5935 207351 34.9 | 11.927 % | c | 194361 | 14849 50222 | 12836 9780 381421 39.0 | 11.927 % | c | 200127 | 14849 50222 | 14120 8789 336369 38.3 | 11.927 % | c | 208776 | 14849 50222 | 15532 10045 375187 37.4 | 11.927 % | c | 221750 | 14849 50222 | 17085 14863 663052 44.6 | 11.927 % | c ============================================================================== c [1mFound solution: 882688[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 226679 | 14815 50095 | 4938 10932 449646 41.1 | 11.927 % | c | 226780 | 14815 50095 | 5431 2834 95029 33.5 | 12.131 % | c | 226930 | 14815 50095 | 5974 2984 100132 33.6 | 12.131 % | c | 227155 | 14815 50095 | 6572 3209 103870 32.4 | 12.131 % | c | 227493 | 14815 50095 | 7229 3547 112944 31.8 | 12.131 % | c | 228002 | 14815 50095 | 7952 4056 131115 32.3 | 12.131 % | c | 228763 | 14815 50095 | 8747 4817 152790 31.7 | 12.131 % | c | 229903 | 14815 50095 | 9622 5957 192874 32.4 | 12.131 % | c | 231611 | 14815 50095 | 10585 7665 256994 33.5 | 12.131 % | c | 234173 | 14815 50095 | 11643 10227 369004 36.1 | 12.131 % | c | 238017 | 14815 50095 | 12807 7881 286356 36.3 | 12.131 % | c | 243784 | 14815 50095 | 14088 6898 265127 38.4 | 12.131 % | c | 252433 | 14725 49888 | 15497 8166 240170 29.4 | 13.104 % | c | 265408 | 14698 49827 | 17047 12985 490542 37.8 | 13.428 % | c ============================================================================== c [1mFound solution: 804864[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 267580 | 14710 49855 | 4903 15157 570717 37.7 | 13.428 % | c | 267682 | 14710 49855 | 5393 3892 103008 26.5 | 13.430 % | c | 267833 | 14710 49855 | 5932 4043 104747 25.9 | 13.430 % | c | 268058 | 14710 49855 | 6525 4268 108961 25.5 | 13.430 % | c | 268395 | 14710 49855 | 7178 4605 114605 24.9 | 13.430 % | c | 268901 | 14710 49855 | 7896 5111 127137 24.9 | 13.430 % | c | 269662 | 14710 49855 | 8685 5872 146984 25.0 | 13.430 % | c | 270803 | 14710 49855 | 9554 7013 203504 29.0 | 13.430 % | c | 272514 | 14710 49855 | 10510 8724 270568 31.0 | 13.430 % | c | 275076 | 14710 49855 | 11561 5653 166684 29.5 | 13.430 % | c | 278920 | 14710 49855 | 12717 9497 351916 37.1 | 13.430 % | c | 284686 | 14697 49825 | 13988 8584 333786 38.9 | 13.592 % | c | 293335 | 14697 49825 | 15387 9940 408374 41.1 | 13.592 % | c | 306309 | 14697 49825 | 16926 14883 678759 45.6 | 13.592 % | c | 325770 | 14697 49825 | 18619 16738 728728 43.5 | 13.592 % | c | 354962 | 14697 49825 | 20481 16697 780600 46.8 | 13.592 % | c | 398751 | 14673 49772 | 22529 18038 685094 38.0 | 13.819 % | c | 464435 | 14665 49750 | 24782 13779 573078 41.6 | 13.884 % | c | 562961 | 14665 49750 | 27260 22883 1101452 48.1 | 13.884 % | c | 710752 | 14658 49735 | 29986 15376 652286 42.4 | 13.948 % | c ============================================================================== c [1mFound solution: 623616[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 746664 | 14638 49690 | 4879 17992 706327 39.3 | 13.948 % | c | 746764 | 14638 49690 | 5366 4598 126096 27.4 | 14.193 % | c | 746914 | 14638 49690 | 5903 4748 127793 26.9 | 14.193 % | c | 747139 | 14638 49690 | 6493 4973 134208 27.0 | 14.193 % | c | 747476 | 14638 49690 | 7143 5310 144194 27.2 | 14.193 % | c | 747983 | 14638 49690 | 7857 5817 154204 26.5 | 14.193 % | c | 748742 | 14638 49690 | 8643 6576 178501 27.1 | 14.193 % | c | 749883 | 14638 49690 | 9507 7717 235750 30.5 | 14.193 % | c | 751592 | 14638 49690 | 10458 9426 293678 31.2 | 14.193 % | c | 754155 | 14638 49690 | 11504 6266 192414 30.7 | 14.193 % | c | 758000 | 14613 49633 | 12654 10109 337355 33.4 | 14.452 % | c | 763767 | 14613 49633 | 13920 9088 320912 35.3 | 14.452 % | c | 772417 | 14613 49633 | 15312 10244 395768 38.6 | 14.452 % | c | 785392 | 14613 49633 | 16843 15023 729672 48.6 | 14.452 % | c ============================================================================== c [1mFound solution: 500736[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 800439 | 14548 49432 | 4849 12558 596683 47.5 | 14.452 % | c | 800539 | 14548 49432 | 5333 3240 104489 32.2 | 15.010 % | c | 800690 | 14548 49432 | 5867 3391 107542 31.7 | 15.010 % | c | 800917 | 14548 49432 | 6454 3618 115679 32.0 | 15.010 % | c | 801254 | 14548 49432 | 7099 3955 123167 31.1 | 15.010 % | c | 801762 | 14548 49432 | 7809 4463 134634 30.2 | 15.010 % | c | 802521 | 14548 49432 | 8590 5222 157497 30.2 | 15.010 % | c | 803660 | 14548 49432 | 9449 6361 201480 31.7 | 15.010 % | c ============================================================================== c [1mFound solution: 478208[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 805121 | 14555 49450 | 4851 7822 238002 30.4 | 15.010 % | c | 805221 | 14555 49450 | 5336 4011 93709 23.4 | 15.018 % | c | 805371 | 14555 49450 | 5869 4161 95436 22.9 | 15.018 % | c | 805596 | 14555 49450 | 6456 4386 98503 22.5 | 15.018 % | c | 805933 | 14555 49450 | 7102 4723 109884 23.3 | 15.018 % | #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.72 0.92 0.92 2/55 6967 Raw data (stat): 6967 (runsolver) R 6966 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420874988 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0006 s] Raw data (loadavg): 0.76 0.92 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 1214 0 0 0 996 3 0 0 25 0 1 0 420874988 6430720 1192 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1570 1192 603 41 0 1529 0 vsize: 6280 [startup+20.0013 s] Raw data (loadavg): 0.80 0.93 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 1572 0 0 0 1994 5 0 0 25 0 1 0 420874988 7929856 1550 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1936 1550 603 41 0 1895 0 vsize: 7744 [startup+30.0009 s] Raw data (loadavg): 0.83 0.93 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 1732 0 0 0 2993 6 0 0 25 0 1 0 420874988 8597504 1710 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2099 1710 603 41 0 2058 0 vsize: 8396 [startup+40.0006 s] Raw data (loadavg): 0.85 0.93 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 1732 0 0 0 3993 6 0 0 25 0 1 0 420874988 8597504 1710 4294967295 134512640 134672761 3221224624 3221223792 134560813 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2099 1710 603 41 0 2058 0 vsize: 8396 [startup+50.0013 s] Raw data (loadavg): 0.88 0.93 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 1868 0 0 0 4993 6 0 0 25 0 1 0 420874988 9125888 1846 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2228 1846 603 41 0 2187 0 vsize: 8912 [startup+60.0024 s] Raw data (loadavg): 0.89 0.93 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 1868 0 0 0 5993 7 0 0 25 0 1 0 420874988 9125888 1846 4294967295 134512640 134672761 3221224624 3221223792 134560970 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2228 1846 603 41 0 2187 0 vsize: 8912 [startup+70.0027 s] Raw data (loadavg): 0.91 0.93 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2052 0 0 0 6992 7 0 0 25 0 1 0 420874988 9928704 2030 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2424 2030 603 41 0 2383 0 vsize: 9696 [startup+80.0023 s] Raw data (loadavg): 0.92 0.94 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2073 0 0 0 7992 7 0 0 25 0 1 0 420874988 10063872 2051 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2457 2051 603 41 0 2416 0 vsize: 9828 [startup+90.0021 s] Raw data (loadavg): 0.93 0.94 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2077 0 0 0 8992 8 0 0 25 0 1 0 420874988 10063872 2055 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2457 2055 603 41 0 2416 0 vsize: 9828 [startup+100.002 s] Raw data (loadavg): 0.94 0.94 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2273 0 0 0 9991 8 0 0 25 0 1 0 420874988 10944512 2251 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2672 2251 603 41 0 2631 0 vsize: 10688 [startup+110.002 s] Raw data (loadavg): 0.95 0.94 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2279 0 0 0 10991 8 0 0 25 0 1 0 420874988 10944512 2257 4294967295 134512640 134672761 3221224624 3221223776 134561249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2672 2257 603 41 0 2631 0 vsize: 10688 [startup+120.003 s] Raw data (loadavg): 0.96 0.94 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2280 0 0 0 11991 9 0 0 25 0 1 0 420874988 10944512 2258 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2672 2258 603 41 0 2631 0 vsize: 10688 [startup+130.003 s] Raw data (loadavg): 0.97 0.94 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2280 0 0 0 12991 9 0 0 25 0 1 0 420874988 10944512 2258 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2672 2258 603 41 0 2631 0 vsize: 10688 [startup+140.002 s] Raw data (loadavg): 0.97 0.95 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2280 0 0 0 13991 9 0 0 25 0 1 0 420874988 10944512 2258 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2672 2258 603 41 0 2631 0 vsize: 10688 [startup+150.003 s] Raw data (loadavg): 0.97 0.95 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2280 0 0 0 14991 9 0 0 25 0 1 0 420874988 10944512 2258 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2672 2258 603 41 0 2631 0 vsize: 10688 [startup+160.004 s] Raw data (loadavg): 0.98 0.95 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2280 0 0 0 15991 9 0 0 25 0 1 0 420874988 10944512 2258 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2672 2258 603 41 0 2631 0 vsize: 10688 [startup+170.004 s] Raw data (loadavg): 0.98 0.95 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2280 0 0 0 16991 9 0 0 25 0 1 0 420874988 10944512 2258 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2672 2258 603 41 0 2631 0 vsize: 10688 [startup+180.004 s] Raw data (loadavg): 0.98 0.95 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2280 0 0 0 17991 9 0 0 25 0 1 0 420874988 10944512 2258 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2672 2258 603 41 0 2631 0 vsize: 10688 [startup+190.004 s] Raw data (loadavg): 0.98 0.95 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2280 0 0 0 18991 9 0 0 25 0 1 0 420874988 10944512 2258 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2672 2258 603 41 0 2631 0 vsize: 10688 [startup+200.004 s] Raw data (loadavg): 0.99 0.95 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2280 0 0 0 19991 9 0 0 25 0 1 0 420874988 10944512 2258 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2672 2258 603 41 0 2631 0 vsize: 10688 [startup+210.004 s] Raw data (loadavg): 0.99 0.95 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2280 0 0 0 20991 9 0 0 25 0 1 0 420874988 10944512 2258 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2672 2258 603 41 0 2631 0 vsize: 10688 [startup+220.005 s] Raw data (loadavg): 0.99 0.95 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2280 0 0 0 21991 10 0 0 25 0 1 0 420874988 10944512 2258 4294967295 134512640 134672761 3221224624 3221223792 134560970 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2672 2258 603 41 0 2631 0 vsize: 10688 [startup+230.005 s] Raw data (loadavg): 0.99 0.95 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2280 0 0 0 22992 10 0 0 25 0 1 0 420874988 10944512 2258 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2672 2258 603 41 0 2631 0 vsize: 10688 [startup+240.006 s] Raw data (loadavg): 0.99 0.95 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2280 0 0 0 23991 10 0 0 25 0 1 0 420874988 10944512 2258 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2672 2258 603 41 0 2631 0 vsize: 10688 [startup+250.006 s] Raw data (loadavg): 0.99 0.96 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2280 0 0 0 24991 10 0 0 25 0 1 0 420874988 10944512 2258 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2672 2258 603 41 0 2631 0 vsize: 10688 [startup+260.007 s] Raw data (loadavg): 0.99 0.96 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2280 0 0 0 25991 10 0 0 25 0 1 0 420874988 10944512 2258 4294967295 134512640 134672761 3221224624 3221223792 134561154 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2672 2258 603 41 0 2631 0 vsize: 10688 [startup+270.006 s] Raw data (loadavg): 0.99 0.96 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2280 0 0 0 26991 10 0 0 25 0 1 0 420874988 10944512 2258 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2672 2258 603 41 0 2631 0 vsize: 10688 [startup+280.006 s] Raw data (loadavg): 0.99 0.96 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2280 0 0 0 27991 11 0 0 25 0 1 0 420874988 10944512 2258 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2672 2258 603 41 0 2631 0 vsize: 10688 [startup+290.007 s] Raw data (loadavg): 0.99 0.96 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2280 0 0 0 28991 11 0 0 25 0 1 0 420874988 10944512 2258 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2672 2258 603 41 0 2631 0 vsize: 10688 [startup+300.007 s] Raw data (loadavg): 0.99 0.96 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2280 0 0 0 29991 11 0 0 25 0 1 0 420874988 10944512 2258 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2672 2258 603 41 0 2631 0 vsize: 10688 [startup+310.007 s] Raw data (loadavg): 0.99 0.96 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2280 0 0 0 30991 11 0 0 25 0 1 0 420874988 10944512 2258 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2672 2258 603 41 0 2631 0 vsize: 10688 [startup+320.008 s] Raw data (loadavg): 0.99 0.96 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2280 0 0 0 31991 11 0 0 25 0 1 0 420874988 10944512 2258 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2672 2258 603 41 0 2631 0 vsize: 10688 [startup+330.007 s] Raw data (loadavg): 0.99 0.96 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2280 0 0 0 32991 11 0 0 25 0 1 0 420874988 10944512 2258 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2672 2258 603 41 0 2631 0 vsize: 10688 [startup+340.007 s] Raw data (loadavg): 0.99 0.96 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2280 0 0 0 33991 11 0 0 25 0 1 0 420874988 10944512 2258 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2672 2258 603 41 0 2631 0 vsize: 10688 [startup+350.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2280 0 0 0 34991 11 0 0 25 0 1 0 420874988 10944512 2258 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2672 2258 603 41 0 2631 0 vsize: 10688 [startup+360.008 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2280 0 0 0 35992 11 0 0 25 0 1 0 420874988 10944512 2258 4294967295 134512640 134672761 3221224624 3221223728 134559941 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2672 2258 603 41 0 2631 0 vsize: 10688 [startup+370.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2282 0 0 0 36992 11 0 0 25 0 1 0 420874988 10944512 2260 4294967295 134512640 134672761 3221224624 3221223792 134560917 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2672 2260 603 41 0 2631 0 vsize: 10688 [startup+380.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2282 0 0 0 37992 11 0 0 25 0 1 0 420874988 10944512 2260 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2672 2260 603 41 0 2631 0 vsize: 10688 [startup+390.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2282 0 0 0 38992 11 0 0 25 0 1 0 420874988 10944512 2260 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2672 2260 603 41 0 2631 0 vsize: 10688 [startup+400.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2282 0 0 0 39992 11 0 0 25 0 1 0 420874988 10944512 2260 4294967295 134512640 134672761 3221224624 3221223760 134560697 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2672 2260 603 41 0 2631 0 vsize: 10688 [startup+410.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2282 0 0 0 40992 11 0 0 25 0 1 0 420874988 10944512 2260 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2672 2260 603 41 0 2631 0 vsize: 10688 [startup+420.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2282 0 0 0 41992 11 0 0 25 0 1 0 420874988 10944512 2260 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2672 2260 603 41 0 2631 0 vsize: 10688 [startup+430.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2282 0 0 0 42993 11 0 0 25 0 1 0 420874988 10944512 2260 4294967295 134512640 134672761 3221224624 3221223728 134555087 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2672 2260 603 41 0 2631 0 vsize: 10688 [startup+440.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2282 0 0 0 43993 11 0 0 25 0 1 0 420874988 10944512 2260 4294967295 134512640 134672761 3221224624 3221223792 134560813 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2672 2260 603 41 0 2631 0 vsize: 10688 [startup+450.005 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2282 0 0 0 44993 11 0 0 25 0 1 0 420874988 10944512 2260 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2672 2260 603 41 0 2631 0 vsize: 10688 [startup+460.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2282 0 0 0 45993 11 0 0 25 0 1 0 420874988 10944512 2260 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2672 2260 603 41 0 2631 0 vsize: 10688 [startup+470.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2282 0 0 0 46993 11 0 0 25 0 1 0 420874988 10944512 2260 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2672 2260 603 41 0 2631 0 vsize: 10688 [startup+480.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2282 0 0 0 47993 11 0 0 25 0 1 0 420874988 10944512 2260 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2672 2260 603 41 0 2631 0 vsize: 10688 [startup+490.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2316 0 0 0 48994 11 0 0 25 0 1 0 420874988 11075584 2294 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2704 2294 603 41 0 2663 0 vsize: 10816 [startup+500.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2324 0 0 0 49994 11 0 0 25 0 1 0 420874988 11075584 2302 4294967295 134512640 134672761 3221224624 3221223792 134560909 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2704 2302 603 41 0 2663 0 vsize: 10816 [startup+510.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2377 0 0 0 50994 11 0 0 25 0 1 0 420874988 11345920 2355 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2770 2355 603 41 0 2729 0 vsize: 11080 [startup+520.005 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2456 0 0 0 51993 12 0 0 25 0 1 0 420874988 11612160 2434 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2835 2434 603 41 0 2794 0 vsize: 11340 [startup+530.005 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2563 0 0 0 52993 12 0 0 25 0 1 0 420874988 12025856 2541 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2936 2541 603 41 0 2895 0 vsize: 11744 [startup+540.005 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2606 0 0 0 53993 12 0 0 25 0 1 0 420874988 12288000 2584 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3000 2584 603 41 0 2959 0 vsize: 12000 [startup+550.004 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2620 0 0 0 54994 12 0 0 25 0 1 0 420874988 12288000 2598 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3000 2598 603 41 0 2959 0 vsize: 12000 [startup+560.005 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2620 0 0 0 55994 12 0 0 25 0 1 0 420874988 12288000 2598 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3000 2598 603 41 0 2959 0 vsize: 12000 [startup+570.005 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2627 0 0 0 56994 12 0 0 25 0 1 0 420874988 12423168 2605 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3033 2605 603 41 0 2992 0 vsize: 12132 [startup+580.004 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2634 0 0 0 57994 12 0 0 25 0 1 0 420874988 12423168 2612 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3033 2612 603 41 0 2992 0 vsize: 12132 [startup+590.005 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2635 0 0 0 58994 12 0 0 25 0 1 0 420874988 12423168 2613 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3033 2613 603 41 0 2992 0 vsize: 12132 [startup+600.005 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2696 0 0 0 59994 12 0 0 25 0 1 0 420874988 12701696 2674 4294967295 134512640 134672761 3221224624 3221223728 134554671 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3101 2674 603 41 0 3060 0 vsize: 12404 [startup+610.005 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2696 0 0 0 60995 12 0 0 25 0 1 0 420874988 12701696 2674 4294967295 134512640 134672761 3221224624 3221223808 134558923 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3101 2674 603 41 0 3060 0 vsize: 12404 [startup+620.009 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2751 0 0 0 61995 12 0 0 25 0 1 0 420874988 12836864 2729 4294967295 134512640 134672761 3221224624 3221223780 134561241 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3134 2729 603 41 0 3093 0 vsize: 12536 [startup+630.009 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2759 0 0 0 62995 12 0 0 25 0 1 0 420874988 12976128 2737 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3168 2737 603 41 0 3127 0 vsize: 12672 [startup+640.009 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2763 0 0 0 63995 12 0 0 25 0 1 0 420874988 12976128 2741 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3168 2741 603 41 0 3127 0 vsize: 12672 [startup+650.008 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2775 0 0 0 64996 12 0 0 25 0 1 0 420874988 12976128 2753 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3168 2753 603 41 0 3127 0 vsize: 12672 [startup+660.009 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2790 0 0 0 65996 12 0 0 25 0 1 0 420874988 13111296 2768 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3201 2768 603 41 0 3160 0 vsize: 12804 [startup+670.009 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2811 0 0 0 66996 12 0 0 25 0 1 0 420874988 13111296 2789 4294967295 134512640 134672761 3221224624 3221223760 134560709 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3201 2789 603 41 0 3160 0 vsize: 12804 [startup+680.008 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2822 0 0 0 67996 12 0 0 25 0 1 0 420874988 13250560 2800 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3235 2800 603 41 0 3194 0 vsize: 12940 [startup+690.009 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2823 0 0 0 68996 12 0 0 25 0 1 0 420874988 13250560 2801 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3235 2801 603 41 0 3194 0 vsize: 12940 [startup+700.009 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2945 0 0 0 69996 13 0 0 25 0 1 0 420874988 13651968 2923 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3333 2923 603 41 0 3292 0 vsize: 13332 [startup+710.008 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 2954 0 0 0 70996 13 0 0 25 0 1 0 420874988 13791232 2932 4294967295 134512640 134672761 3221224624 3221223792 134560920 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3367 2932 603 41 0 3326 0 vsize: 13468 [startup+720.008 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3002 0 0 0 71996 13 0 0 25 0 1 0 420874988 13926400 2980 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3400 2980 603 41 0 3359 0 vsize: 13600 [startup+730.008 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3003 0 0 0 72996 13 0 0 25 0 1 0 420874988 13926400 2981 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3400 2981 603 41 0 3359 0 vsize: 13600 [startup+740.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3003 0 0 0 73996 13 0 0 25 0 1 0 420874988 13926400 2981 4294967295 134512640 134672761 3221224624 3221223808 134559596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3400 2981 603 41 0 3359 0 vsize: 13600 [startup+750.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3012 0 0 0 74996 13 0 0 25 0 1 0 420874988 14061568 2990 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3433 2990 603 41 0 3392 0 vsize: 13732 [startup+760.008 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3059 0 0 0 75996 14 0 0 25 0 1 0 420874988 14192640 3037 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3465 3037 603 41 0 3424 0 vsize: 13860 [startup+770.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3063 0 0 0 76996 14 0 0 25 0 1 0 420874988 14192640 3041 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3465 3041 603 41 0 3424 0 vsize: 13860 [startup+780.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3125 0 0 0 77996 14 0 0 25 0 1 0 420874988 14454784 3103 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3529 3103 603 41 0 3488 0 vsize: 14116 [startup+790.008 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3138 0 0 0 78997 14 0 0 25 0 1 0 420874988 14589952 3116 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3562 3116 603 41 0 3521 0 vsize: 14248 [startup+800.008 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3163 0 0 0 79997 14 0 0 25 0 1 0 420874988 14589952 3141 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3562 3141 603 41 0 3521 0 vsize: 14248 [startup+810.008 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3166 0 0 0 80997 14 0 0 25 0 1 0 420874988 14725120 3144 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3595 3144 603 41 0 3554 0 vsize: 14380 [startup+820.008 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3180 0 0 0 81997 14 0 0 25 0 1 0 420874988 14725120 3158 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3595 3158 603 41 0 3554 0 vsize: 14380 [startup+830.008 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3183 0 0 0 82997 14 0 0 25 0 1 0 420874988 14725120 3161 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3595 3161 603 41 0 3554 0 vsize: 14380 [startup+840.009 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3199 0 0 0 83996 14 0 0 25 0 1 0 420874988 14860288 3177 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3628 3177 603 41 0 3587 0 vsize: 14512 [startup+850.009 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3290 0 0 0 84996 15 0 0 25 0 1 0 420874988 15122432 3268 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3692 3268 603 41 0 3651 0 vsize: 14768 [startup+860.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3296 0 0 0 85996 15 0 0 25 0 1 0 420874988 15122432 3274 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3692 3274 603 41 0 3651 0 vsize: 14768 [startup+870.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3301 0 0 0 86996 15 0 0 25 0 1 0 420874988 15265792 3279 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3727 3279 603 41 0 3686 0 vsize: 14908 [startup+880.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3301 0 0 0 87996 15 0 0 25 0 1 0 420874988 15265792 3279 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3727 3279 603 41 0 3686 0 vsize: 14908 [startup+890.011 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3306 0 0 0 88996 16 0 0 25 0 1 0 420874988 15265792 3284 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3727 3284 603 41 0 3686 0 vsize: 14908 [startup+900.012 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3306 0 0 0 89996 16 0 0 25 0 1 0 420874988 15265792 3284 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3727 3284 603 41 0 3686 0 vsize: 14908 [startup+910.012 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3306 0 0 0 90996 16 0 0 25 0 1 0 420874988 15265792 3284 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3727 3284 603 41 0 3686 0 vsize: 14908 [startup+920.012 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3306 0 0 0 91996 16 0 0 25 0 1 0 420874988 15265792 3284 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3727 3284 603 41 0 3686 0 vsize: 14908 [startup+930.011 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3306 0 0 0 92996 16 0 0 25 0 1 0 420874988 15265792 3284 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3727 3284 603 41 0 3686 0 vsize: 14908 [startup+940.011 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3378 0 0 0 93996 16 0 0 25 0 1 0 420874988 15532032 3356 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3792 3356 603 41 0 3751 0 vsize: 15168 [startup+950.011 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3379 0 0 0 94996 16 0 0 25 0 1 0 420874988 15532032 3357 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3792 3357 603 41 0 3751 0 vsize: 15168 [startup+960.012 s] Raw data (loadavg): 1.07 0.99 0.93 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3434 0 0 0 95996 16 0 0 25 0 1 0 420874988 15810560 3412 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3860 3412 603 41 0 3819 0 vsize: 15440 [startup+970.012 s] Raw data (loadavg): 1.06 0.99 0.93 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3470 0 0 0 96996 17 0 0 25 0 1 0 420874988 15945728 3448 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3893 3448 603 41 0 3852 0 vsize: 15572 [startup+980.012 s] Raw data (loadavg): 1.05 0.99 0.93 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3471 0 0 0 97996 17 0 0 25 0 1 0 420874988 15945728 3449 4294967295 134512640 134672761 3221224624 3221223792 134561016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3893 3449 603 41 0 3852 0 vsize: 15572 [startup+990.011 s] Raw data (loadavg): 1.04 0.99 0.93 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3504 0 0 0 98996 17 0 0 25 0 1 0 420874988 16076800 3482 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3925 3482 603 41 0 3884 0 vsize: 15700 [startup+1000.01 s] Raw data (loadavg): 1.04 0.99 0.93 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3508 0 0 0 99996 17 0 0 25 0 1 0 420874988 16076800 3486 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3925 3486 603 41 0 3884 0 vsize: 15700 [startup+1010.01 s] Raw data (loadavg): 1.03 0.99 0.93 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3522 0 0 0 100997 17 0 0 25 0 1 0 420874988 16228352 3500 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3962 3500 603 41 0 3921 0 vsize: 15848 [startup+1020.01 s] Raw data (loadavg): 1.03 0.99 0.93 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3536 0 0 0 101997 17 0 0 25 0 1 0 420874988 16228352 3514 4294967295 134512640 134672761 3221224624 3221223808 134558651 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3962 3514 603 41 0 3921 0 vsize: 15848 [startup+1030.01 s] Raw data (loadavg): 1.02 0.99 0.93 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3537 0 0 0 102997 17 0 0 25 0 1 0 420874988 16228352 3515 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3962 3515 603 41 0 3921 0 vsize: 15848 [startup+1040.01 s] Raw data (loadavg): 1.02 0.99 0.93 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3537 0 0 0 103997 17 0 0 25 0 1 0 420874988 16228352 3515 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3962 3515 603 41 0 3921 0 vsize: 15848 [startup+1050.01 s] Raw data (loadavg): 1.01 0.99 0.93 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3537 0 0 0 104997 17 0 0 25 0 1 0 420874988 16228352 3515 4294967295 134512640 134672761 3221224624 3221223808 134559363 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3962 3515 603 41 0 3921 0 vsize: 15848 [startup+1060.01 s] Raw data (loadavg): 1.01 0.99 0.93 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3542 0 0 0 105997 17 0 0 25 0 1 0 420874988 16228352 3520 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3962 3520 603 41 0 3921 0 vsize: 15848 [startup+1070.01 s] Raw data (loadavg): 1.01 0.99 0.93 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3554 0 0 0 106998 17 0 0 25 0 1 0 420874988 16379904 3532 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3999 3532 603 41 0 3958 0 vsize: 15996 [startup+1080.01 s] Raw data (loadavg): 1.01 0.99 0.93 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3554 0 0 0 107998 17 0 0 25 0 1 0 420874988 16379904 3532 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3999 3532 603 41 0 3958 0 vsize: 15996 [startup+1090.01 s] Raw data (loadavg): 1.01 0.99 0.93 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3560 0 0 0 108998 17 0 0 25 0 1 0 420874988 16379904 3538 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3999 3538 603 41 0 3958 0 vsize: 15996 [startup+1100.01 s] Raw data (loadavg): 1.00 0.99 0.93 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3560 0 0 0 109998 17 0 0 25 0 1 0 420874988 16379904 3538 4294967295 134512640 134672761 3221224624 3221223728 134560367 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3999 3538 603 41 0 3958 0 vsize: 15996 [startup+1110.01 s] Raw data (loadavg): 1.00 0.99 0.93 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3560 0 0 0 110998 17 0 0 25 0 1 0 420874988 16379904 3538 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3999 3538 603 41 0 3958 0 vsize: 15996 [startup+1120.01 s] Raw data (loadavg): 1.00 0.99 0.93 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3562 0 0 0 111998 18 0 0 25 0 1 0 420874988 16379904 3540 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3999 3540 603 41 0 3958 0 vsize: 15996 [startup+1130.01 s] Raw data (loadavg): 1.00 0.99 0.93 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3562 0 0 0 112998 18 0 0 25 0 1 0 420874988 16379904 3540 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3999 3540 603 41 0 3958 0 vsize: 15996 [startup+1140.01 s] Raw data (loadavg): 1.00 0.99 0.93 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3562 0 0 0 113998 18 0 0 25 0 1 0 420874988 16379904 3540 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3999 3540 603 41 0 3958 0 vsize: 15996 [startup+1150.01 s] Raw data (loadavg): 1.00 0.99 0.93 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3562 0 0 0 114998 18 0 0 25 0 1 0 420874988 16379904 3540 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3999 3540 603 41 0 3958 0 vsize: 15996 [startup+1160.01 s] Raw data (loadavg): 1.00 0.99 0.93 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3562 0 0 0 115998 18 0 0 25 0 1 0 420874988 16379904 3540 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3999 3540 603 41 0 3958 0 vsize: 15996 [startup+1170.01 s] Raw data (loadavg): 1.00 0.99 0.93 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3562 0 0 0 116998 18 0 0 25 0 1 0 420874988 16379904 3540 4294967295 134512640 134672761 3221224624 3221223808 134559405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3999 3540 603 41 0 3958 0 vsize: 15996 [startup+1180.01 s] Raw data (loadavg): 1.00 0.99 0.93 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3562 0 0 0 117998 18 0 0 25 0 1 0 420874988 16379904 3540 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3999 3540 603 41 0 3958 0 vsize: 15996 [startup+1190.01 s] Raw data (loadavg): 1.00 0.99 0.93 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3562 0 0 0 118998 18 0 0 25 0 1 0 420874988 16379904 3540 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3999 3540 603 41 0 3958 0 vsize: 15996 [startup+1200.01 s] Raw data (loadavg): 1.00 0.99 0.93 2/55 6967 Raw data (stat): 6967 (minisat+) R 6966 30927 30926 0 -1 0 3562 0 0 0 119999 18 0 0 25 0 1 0 420874988 16379904 3540 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3999 3540 603 41 0 3958 0 vsize: 15996 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.03 s] Raw data (loadavg): 1.00 0.99 0.93 1/55 6967 Raw data (stat): 6967 (minisat+) Z 6966 30927 30926 0 -1 12 3565 0 0 0 119999 19 0 0 25 0 1 0 420874988 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Maximum CPU time exceeded: sending SIGTERM and SIGKILL Child status: 10 Real time (s): 1200.02 CPU time (s): 1200.19 CPU user time (s): 1199.99 CPU system time (s): 0.19397 CPU usage (%): 100.013 Max. virtual memory (Kb): 15996 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####