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 wulflinc1 THE 2005-05-25 19:15:12 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=22157 boxname=wulflinc1 idbench=973 idsolver=15 numberseed=0 MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814 /oldhome/oroussel/solvers/minisat+_script MD5SUM BENCH: 10386fd19d9976c249ce2be861b38a70 /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-20-10-markshare1.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-20-10-markshare1.opb IDLAUNCH: 22157 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.053 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 : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.053 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: 574808 kB Buffers: 35796 kB Cached: 394748 kB SwapCached: 3976 kB Active: 82320 kB Inactive: 355112 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 574556 kB SwapTotal: 2097136 kB SwapFree: 2092844 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6968 kB Slab: 16680 kB Committed_AS: 92716 kB PageTables: 332 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-05-25 19:35:42 (client local time) WITH STATUS 152 IN 1229.84 SECONDS stats: 22157 7 1229.84 152 #### 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 % | c | 806441 | 14555 49450 | 7812 5231 133539 25.5 | 15.018 % | c | 807201 | 14515 49360 | 8593 5987 160022 26.7 | 15.404 % | c | 808340 | 14515 49360 | 9453 7126 199759 28.0 | 15.404 % | c | 810048 | 14515 49360 | 10398 8834 256370 29.0 | 15.404 % | c | 812610 | 14515 49360 | 11438 5831 160906 27.6 | 15.404 % | c | 816457 | 14515 49360 | 12582 9678 325951 33.7 | 15.404 % | c | 822225 | 14515 49360 | 13840 8694 311482 35.8 | 15.404 % | c | 830874 | 14515 49360 | 15224 10000 353400 35.3 | 15.404 % | c | 843848 | 14515 49360 | 16746 14905 612050 41.1 | 15.404 % | /oldhome/oroussel/solvers/minisat+_script: line 9: 25311 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@" #### 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.91 0.97 0.93 2/55 25307 Raw data (stat): 25307 (runsolver) R 25306 8378 8377 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 726243575 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 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.0002 s] Raw data (loadavg): 0.93 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+20.0001 s] Raw data (loadavg): 0.94 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+30.0008 s] Raw data (loadavg): 0.95 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+40.0005 s] Raw data (loadavg): 0.95 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+50.0013 s] Raw data (loadavg): 0.96 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+60.0011 s] Raw data (loadavg): 0.97 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+70.0009 s] Raw data (loadavg): 0.97 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+80.0016 s] Raw data (loadavg): 0.98 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+90.0014 s] Raw data (loadavg): 0.98 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+100.001 s] Raw data (loadavg): 0.98 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+110.002 s] Raw data (loadavg): 0.98 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+120.002 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+130.002 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+140.001 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+150.001 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+160.001 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+170.001 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+180.001 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+190 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+200.001 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+210.001 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+220.001 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+230.001 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+240.001 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+250.002 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+260.003 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+270.002 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+280.002 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+290.008 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+300.009 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+310.009 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+320.008 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+330.009 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+340.009 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+350.009 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+360.009 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+370.009 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+380.009 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+390.009 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+400.01 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+410.009 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+420.01 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+430.01 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+440.01 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+450.009 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+460.009 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+470.009 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+480.009 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+490.009 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+500.008 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+510.009 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+520.009 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+530.009 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+540.014 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+550.014 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+560.014 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+570.014 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+580.014 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+590.014 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+600.015 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+610.016 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+620.016 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+630.015 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+640.015 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+650.016 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+660.016 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+670.015 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+680.016 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+690.016 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+700.016 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+710.016 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+720.016 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+730.016 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+740.016 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+750.017 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+760.017 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+770.016 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+780.016 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+790.017 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+800.017 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+810.016 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+820.016 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+830.016 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+840.016 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+850.017 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+860.017 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+870.017 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+880.017 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+890.023 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+900.129 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+910.128 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+920.128 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+930.129 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+940.129 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+950.129 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+960.133 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+970.133 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+980.133 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+990.133 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1000.13 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1010.13 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1020.13 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1030.13 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1040.13 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1050.13 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1060.13 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1070.13 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1080.13 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1090.13 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1100.14 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1110.13 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1120.13 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1130.13 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1140.13 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1150.13 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1160.13 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1170.13 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1180.13 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1190.13 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1200.14 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1210.13 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1220.13 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1229.7 s] Raw data (loadavg): 0.99 0.97 0.93 1/54 25311 Raw data (stat): 25307 (minisat+_script) S 25306 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 726243575 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 0 Child status: 152 Real time (s): 1229.7 CPU time (s): 1229.84 CPU user time (s): 1229.69 CPU system time (s): 0.153976 CPU usage (%): 100.011 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####