Name | mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-markshare1.opb |
MD5SUM | 6f06e375914e0285ec75de90ad627758 |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 3584 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 120 |
Biggest coefficient in the objective function | 524288 |
Number of bits for the biggest coefficient in the objective function | 20 |
Sum of the numbers in the objective function | 6291450 |
Number of bits of the sum of numbers in the objective function | 23 |
Biggest number in a constraint | 524288 |
Number of bits of the biggest number in a constraint | 20 |
Biggest sum of numbers in a constraint | 6291450 |
Number of bits of the biggest sum of numbers | 23 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1195.33 |
Number of variables | 170 |
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 | 70 |
LAUNCH ON wulflinc7 THE 2005-09-20 03:42:34 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3300 boxname=wulflinc7 idbench=956 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 6f06e375914e0285ec75de90ad627758 /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-markshare1.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-markshare1.opb IDLAUNCH: 3300 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.050 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 : 2 cpu MHz : 451.050 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: 913896 kB Buffers: 3492 kB Cached: 92460 kB SwapCached: 744 kB Active: 24452 kB Inactive: 74068 kB HighTotal: 131008 kB HighFree: 34412 kB LowTotal: 903652 kB LowFree: 879484 kB SwapTotal: 2097136 kB SwapFree: 2095884 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5664 kB Slab: 16416 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-20 04:02:45 (client local time) WITH STATUS 10 IN 1210.12 SECONDS stats: 3300 7 1210.12 10
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: 405119 bits: 20/19 c ---[ 8]---> Adder-cost: 314 maxlim: 431743 bits: 20/19 c ---[ 6]---> Adder-cost: 348 maxlim: 435327 bits: 20/19 c ---[ 4]---> Adder-cost: 318 maxlim: 411775 bits: 20/19 c ---[ 2]---> Adder-cost: 312 maxlim: 410751 bits: 20/19 c ---[ 0]---> Adder-cost: 314 maxlim: 411135 bits: 20/19 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 583 5.8 | 11.212 % | c ============================================================================== c [1mFound solution: 511232[0m c ---[ 0]---> Sorter-cost: 855 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 | 115 | 14928 50449 | 4976 115 713 6.2 | 11.212 % | c | 218 | 14920 50423 | 5473 217 7283 33.6 | 8.450 % | c | 368 | 14920 50423 | 6020 367 18769 51.1 | 8.450 % | c | 593 | 14920 50423 | 6623 592 36809 62.2 | 8.450 % | c | 930 | 14912 50397 | 7285 928 58825 63.4 | 8.484 % | c ============================================================================== c [1mFound solution: 508160[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 | 1311 | 14927 50468 | 4975 1309 91930 70.2 | 8.484 % | c | 1414 | 14927 50468 | 5472 1412 98927 70.1 | 8.489 % | c | 1567 | 14919 50442 | 6019 1564 113420 72.5 | 8.523 % | c | 1794 | 14919 50442 | 6621 1791 129324 72.2 | 8.523 % | c ============================================================================== c [1mFound solution: 481280[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 | 1899 | 14937 50494 | 4979 1896 134567 71.0 | 8.523 % | c | 1999 | 14937 50494 | 5476 1996 140754 70.5 | 8.519 % | c | 2149 | 14937 50494 | 6024 2146 148833 69.4 | 8.519 % | c | 2374 | 14937 50494 | 6627 2371 164400 69.3 | 8.519 % | c ============================================================================== c [1mFound solution: 435072[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 | 2433 | 14949 50522 | 4983 2430 167546 68.9 | 8.519 % | c | 2534 | 14949 50522 | 5481 2531 177093 70.0 | 8.533 % | c | 2685 | 14941 50496 | 6029 2681 186556 69.6 | 8.567 % | c | 2911 | 14941 50496 | 6632 2907 203514 70.0 | 8.567 % | c | 3249 | 14941 50496 | 7295 3245 244508 75.3 | 8.567 % | c | 3755 | 14941 50496 | 8025 3751 292255 77.9 | 8.567 % | c | 4514 | 14941 50496 | 8827 4510 341575 75.7 | 8.567 % | c | 5654 | 14941 50496 | 9710 5650 468535 82.9 | 8.567 % | c | 7362 | 14933 50470 | 10681 7357 615477 83.7 | 8.600 % | c | 9925 | 14925 50444 | 11749 9919 841229 84.8 | 8.634 % | c ============================================================================== c [1mFound solution: 430720[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 | 10164 | 14939 50476 | 4979 10158 857755 84.4 | 8.634 % | c | 10264 | 14939 50476 | 5476 5179 384424 74.2 | 8.644 % | c | 10414 | 14939 50476 | 6024 5329 396662 74.4 | 8.644 % | c | 10639 | 14939 50476 | 6627 5554 417897 75.2 | 8.644 % | c | 10977 | 14939 50476 | 7289 5892 445678 75.6 | 8.644 % | c | 11483 | 14939 50476 | 8018 6398 493666 77.2 | 8.644 % | c | 12242 | 14939 50476 | 8820 7157 567456 79.3 | 8.644 % | c | 13381 | 14939 50476 | 9702 8296 676789 81.6 | 8.644 % | c ============================================================================== c [1mFound solution: 424576[0m c ---[ 0]---> Sorter-cost: 8 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 | 14095 | 14945 50493 | 4981 9010 744526 82.6 | 8.644 % | c | 14195 | 14945 50493 | 5479 4605 343883 74.7 | 8.669 % | c | 14346 | 14945 50493 | 6027 4756 352759 74.2 | 8.669 % | c | 14571 | 14945 50493 | 6629 4981 365164 73.3 | 8.669 % | c | 14909 | 14945 50493 | 7292 5319 391290 73.6 | 8.669 % | c ============================================================================== c [1mFound solution: 401408[0m c ---[ 0]---> Sorter-cost: 8 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 | 15041 | 14955 50515 | 4985 5451 404775 74.3 | 8.669 % | c | 15142 | 14955 50515 | 5483 2827 161070 57.0 | 8.691 % | c | 15293 | 14955 50515 | 6031 2978 169426 56.9 | 8.691 % | c | 15519 | 14955 50515 | 6635 3204 190669 59.5 | 8.691 % | c | 15856 | 14955 50515 | 7298 3541 210095 59.3 | 8.691 % | c | 16364 | 14949 50497 | 8028 4048 257813 63.7 | 8.725 % | c | 17124 | 14949 50497 | 8831 4808 319608 66.5 | 8.725 % | c | 18263 | 14949 50497 | 9714 5947 408827 68.7 | 8.725 % | c | 19973 | 14949 50497 | 10685 7657 514369 67.2 | 8.725 % | c | 22535 | 14949 50497 | 11754 10219 725324 71.0 | 8.725 % | c | 26379 | 14941 50471 | 12929 7738 611167 79.0 | 8.758 % | c ============================================================================== c [1mFound solution: 396032[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 | 27088 | 14953 50499 | 4984 8447 701896 83.1 | 8.758 % | c | 27189 | 14953 50499 | 5482 4325 322480 74.6 | 8.777 % | c | 27340 | 14953 50499 | 6030 4476 334565 74.7 | 8.777 % | c | 27566 | 14953 50499 | 6633 4702 352775 75.0 | 8.777 % | c | 27904 | 14953 50499 | 7297 5040 379892 75.4 | 8.777 % | c | 28410 | 14953 50499 | 8026 5546 421562 76.0 | 8.777 % | c | 29169 | 14953 50499 | 8829 6305 474041 75.2 | 8.777 % | c | 30309 | 14953 50499 | 9712 7445 580343 78.0 | 8.777 % | c | 32018 | 14947 50486 | 10683 9153 744520 81.3 | 8.844 % | c | 34580 | 14947 50486 | 11752 5864 429656 73.3 | 8.844 % | c | 38424 | 14939 50460 | 12927 9707 719681 74.1 | 8.878 % | c | 44191 | 14917 50390 | 14219 8519 572810 67.2 | 8.978 % | c ============================================================================== c [1mFound solution: 389248[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 | 47913 | 14929 50422 | 4976 12241 889985 72.7 | 8.978 % | c | 48015 | 14929 50422 | 5473 3163 161261 51.0 | 8.991 % | c | 48166 | 14929 50422 | 6020 3314 174071 52.5 | 8.991 % | c | 48392 | 14929 50422 | 6623 3540 195446 55.2 | 8.991 % | c | 48730 | 14929 50422 | 7285 3878 223677 57.7 | 8.991 % | c | 49237 | 14929 50422 | 8013 4385 278053 63.4 | 8.991 % | c | 49998 | 14929 50422 | 8815 5146 360261 70.0 | 8.991 % | c | 51138 | 14929 50422 | 9696 6286 457548 72.8 | 8.991 % | c | 52847 | 14929 50422 | 10666 7995 595650 74.5 | 8.991 % | c | 55410 | 14929 50422 | 11733 10558 774167 73.3 | 8.991 % | c ============================================================================== c [1mFound solution: 377728[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 | 56352 | 14920 50389 | 4973 11498 829497 72.1 | 8.991 % | c | 56453 | 14920 50389 | 5470 2976 126077 42.4 | 9.076 % | c | 56603 | 14920 50389 | 6017 3126 135668 43.4 | 9.076 % | c | 56829 | 14920 50389 | 6619 3352 154566 46.1 | 9.076 % | c | 57167 | 14920 50389 | 7280 3690 180132 48.8 | 9.076 % | c | 57674 | 14920 50389 | 8009 4197 208039 49.6 | 9.076 % | c | 58435 | 14920 50389 | 8809 4958 280274 56.5 | 9.076 % | c | 59576 | 14920 50389 | 9690 6099 363954 59.7 | 9.076 % | c | 61285 | 14920 50389 | 10660 7808 488158 62.5 | 9.076 % | c | 63848 | 14920 50389 | 11726 10371 708658 68.3 | 9.076 % | c | 67693 | 14920 50389 | 12898 7831 507587 64.8 | 9.076 % | c ============================================================================== c [1mFound solution: 306944[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 | 72031 | 14923 50389 | 4974 12168 780818 64.2 | 9.076 % | c | 72132 | 14923 50389 | 5471 3143 114668 36.5 | 9.124 % | c | 72283 | 14923 50389 | 6018 3294 126047 38.3 | 9.124 % | c | 72509 | 14923 50389 | 6620 3520 134740 38.3 | 9.124 % | c | 72846 | 14923 50389 | 7282 3857 148492 38.5 | 9.124 % | c | 73353 | 14923 50389 | 8010 4364 174667 40.0 | 9.124 % | c ============================================================================== c [1mFound solution: 282624[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 | 74024 | 14934 50414 | 4978 5035 211786 42.1 | 9.124 % | c | 74125 | 14934 50414 | 5475 5136 215318 41.9 | 9.139 % | c | 74275 | 14934 50414 | 6023 5286 219636 41.6 | 9.139 % | c | 74502 | 14934 50414 | 6625 5513 225641 40.9 | 9.139 % | c | 74840 | 14934 50414 | 7288 5851 247004 42.2 | 9.139 % | c | 75348 | 14934 50414 | 8017 6359 269180 42.3 | 9.139 % | c | 76107 | 14934 50414 | 8818 7118 317253 44.6 | 9.139 % | c | 77246 | 14934 50414 | 9700 8257 408361 49.5 | 9.139 % | c ============================================================================== c [1mFound solution: 280960[0m c ---[ 0]---> Sorter-cost: 8 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 | 77625 | 14944 50437 | 4981 8636 434637 50.3 | 9.139 % | c | 77725 | 14944 50437 | 5479 4418 204354 46.3 | 9.157 % | c | 77876 | 14944 50437 | 6027 4569 209208 45.8 | 9.157 % | c | 78105 | 14944 50437 | 6629 4798 214379 44.7 | 9.157 % | c | 78442 | 14944 50437 | 7292 5135 229599 44.7 | 9.157 % | c | 78948 | 14944 50437 | 8021 5641 259177 45.9 | 9.157 % | c | 79708 | 14944 50437 | 8824 6401 306245 47.8 | 9.157 % | c | 80847 | 14944 50437 | 9706 7540 367966 48.8 | 9.157 % | c | 82555 | 14944 50437 | 10677 9248 448135 48.5 | 9.157 % | c | 85117 | 14944 50437 | 11744 6099 224259 36.8 | 9.157 % | c | 88961 | 14944 50437 | 12919 9943 423222 42.6 | 9.157 % | c | 94727 | 14944 50437 | 14211 8805 393689 44.7 | 9.157 % | c ============================================================================== c [1mFound solution: 276864[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 | 95408 | 14951 50454 | 4983 9486 452297 47.7 | 9.157 % | c | 95508 | 14951 50454 | 5481 4843 225668 46.6 | 9.181 % | c | 95660 | 14951 50454 | 6029 4995 228247 45.7 | 9.181 % | c | 95886 | 14951 50454 | 6632 5221 235950 45.2 | 9.181 % | c | 96224 | 14951 50454 | 7295 5559 268280 48.3 | 9.181 % | c | 96732 | 14951 50454 | 8025 6067 288367 47.5 | 9.181 % | c | 97491 | 14951 50454 | 8827 6826 312807 45.8 | 9.181 % | c ============================================================================== c [1mFound solution: 270976[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 | 98233 | 14960 50474 | 4986 7568 367612 48.6 | 9.181 % | c | 98337 | 14960 50474 | 5484 3888 149120 38.4 | 9.202 % | c | 98487 | 14960 50474 | 6033 4038 153879 38.1 | 9.202 % | c | 98712 | 14960 50474 | 6636 4263 159883 37.5 | 9.202 % | c | 99049 | 14960 50474 | 7300 4600 183162 39.8 | 9.202 % | c | 99556 | 14960 50474 | 8030 5107 209351 41.0 | 9.202 % | c | 100316 | 14960 50474 | 8833 5867 237677 40.5 | 9.202 % | c | 101455 | 14960 50474 | 9716 7006 288228 41.1 | 9.202 % | c | 103163 | 14960 50474 | 10687 8714 351450 40.3 | 9.202 % | c | 105728 | 14960 50474 | 11756 11279 479582 42.5 | 9.202 % | c | 109572 | 14960 50474 | 12932 8939 396000 44.3 | 9.202 % | c | 115338 | 14960 50474 | 14225 7801 349348 44.8 | 9.202 % | c | 123987 | 14960 50474 | 15648 8933 343695 38.5 | 9.202 % | c ============================================================================== c [1mFound solution: 254080[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 | 131533 | 14968 50495 | 4989 16479 780422 47.4 | 9.202 % | c | 131634 | 14968 50495 | 5487 4221 168757 40.0 | 9.220 % | c | 131784 | 14968 50495 | 6036 4371 169898 38.9 | 9.220 % | c | 132010 | 14968 50495 | 6640 4597 176589 38.4 | 9.220 % | c | 132347 | 14968 50495 | 7304 4934 189055 38.3 | 9.220 % | c | 132853 | 14968 50495 | 8034 5440 207752 38.2 | 9.220 % | c | 133613 | 14968 50495 | 8838 6200 227931 36.8 | 9.220 % | c | 134753 | 14968 50495 | 9722 7340 283754 38.7 | 9.220 % | c | 136462 | 14968 50495 | 10694 9049 447766 49.5 | 9.220 % | c | 139024 | 14968 50495 | 11763 11611 572585 49.3 | 9.220 % | c | 142869 | 14968 50495 | 12940 9385 443339 47.2 | 9.220 % | c | 148635 | 14968 50495 | 14234 8359 334862 40.1 | 9.220 % | c | 157284 | 14968 50495 | 15657 9559 389308 40.7 | 9.220 % | c | 170258 | 14968 50495 | 17223 14357 698508 48.7 | 9.220 % | c | 189721 | 14968 50495 | 18945 15791 813245 51.5 | 9.220 % | c ============================================================================== c [1mFound solution: 235264[0m c ---[ 0]---> Sorter-cost: 8 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 | 209972 | 14970 50498 | 4990 16339 752560 46.1 | 9.220 % | c | 210072 | 14970 50498 | 5489 4185 160957 38.5 | 9.301 % | c | 210223 | 14970 50498 | 6037 4336 168165 38.8 | 9.301 % | c | 210448 | 14970 50498 | 6641 4561 175463 38.5 | 9.301 % | c | 210786 | 14970 50498 | 7305 4899 180956 36.9 | 9.301 % | c | 211292 | 14970 50498 | 8036 5405 191541 35.4 | 9.301 % | c | 212051 | 14970 50498 | 8840 6164 213220 34.6 | 9.301 % | c | 213190 | 14962 50480 | 9724 7300 275218 37.7 | 9.367 % | c | 214901 | 14962 50480 | 10696 9011 369149 41.0 | 9.367 % | c | 217464 | 14962 50480 | 11766 11574 526142 45.5 | 9.367 % | c ============================================================================== c [1mFound solution: 212736[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 | 220832 | 14972 50503 | 4990 8677 442359 51.0 | 9.367 % | c | 220932 | 14972 50503 | 5489 4439 192659 43.4 | 9.381 % | c | 221082 | 14972 50503 | 6037 4589 200285 43.6 | 9.381 % | c | 221309 | 14972 50503 | 6641 4816 206834 42.9 | 9.381 % | c | 221648 | 14972 50503 | 7305 5155 218113 42.3 | 9.381 % | c | 222155 | 14963 50484 | 8036 5660 230180 40.7 | 9.480 % | c | 222915 | 14963 50484 | 8840 6420 265964 41.4 | 9.480 % | c | 224054 | 14963 50484 | 9724 7559 305271 40.4 | 9.480 % | c | 225762 | 14963 50484 | 10696 9267 361057 39.0 | 9.480 % | c | 228325 | 14963 50484 | 11766 6101 188143 30.8 | 9.480 % | c | 232172 | 14963 50484 | 12942 9948 383964 38.6 | 9.480 % | c ============================================================================== c [1mFound solution: 154752[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 | 236058 | 14972 50507 | 4990 7150 228313 31.9 | 9.480 % | c | 236160 | 14972 50507 | 5489 3677 92931 25.3 | 9.497 % | c | 236311 | 14972 50507 | 6037 3828 100768 26.3 | 9.497 % | c | 236537 | 14972 50507 | 6641 4054 109068 26.9 | 9.497 % | c | 236874 | 14972 50507 | 7305 4391 119615 27.2 | 9.497 % | c | 237380 | 14972 50507 | 8036 4897 138079 28.2 | 9.497 % | c | 238140 | 14972 50507 | 8840 5657 159058 28.1 | 9.498 % | c | 239280 | 14972 50507 | 9724 6797 192745 28.4 | 9.497 % | c | 240991 | 14972 50507 | 10696 8508 277679 32.6 | 9.497 % | c | 243553 | 14972 50507 | 11766 11070 376719 34.0 | 9.497 % | c | 247397 | 14972 50507 | 12942 8658 405878 46.9 | 9.497 % | c | 253164 | 14972 50507 | 14237 7523 301861 40.1 | 9.497 % | c | 261814 | 14972 50507 | 15660 8724 389636 44.7 | 9.497 % | c | 274788 | 14972 50507 | 17226 13516 547618 40.5 | 9.497 % | c | 294251 | 14964 50485 | 18949 14913 697316 46.8 | 9.563 % | c | 323444 | 14948 50449 | 20844 14609 643927 44.1 | 9.727 % | c | 367234 | 14929 50406 | 22928 15159 664222 43.8 | 9.924 % | c | 432918 | 14919 50384 | 25221 21945 980206 44.7 | 10.023 % | c | 531444 | 14914 50373 | 27743 16971 739734 43.6 | 10.089 % | c ============================================================================== c [1mFound solution: 147072[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 | 551980 | 14919 50385 | 4973 22813 921144 40.4 | 10.089 % | c | 552080 | 14919 50385 | 5470 2952 67935 23.0 | 10.174 % | c | 552231 | 14919 50385 | 6017 3103 69955 22.5 | 10.174 % | c | 552457 | 14919 50385 | 6619 3329 85586 25.7 | 10.174 % | c | 552796 | 14919 50385 | 7280 3668 100834 27.5 | 10.174 % | c | 553304 | 14919 50385 | 8009 4176 118179 28.3 | 10.174 % | c | 554063 | 14919 50385 | 8809 4935 154288 31.3 | 10.174 % | c | 555203 | 14919 50385 | 9690 6075 205886 33.9 | 10.174 % | c | 556915 | 14919 50385 | 10660 7787 287187 36.9 | 10.174 % | c | 559478 | 14919 50385 | 11726 10350 387740 37.5 | 10.174 % | c | 563322 | 14919 50385 | 12898 7968 290882 36.5 | 10.174 % | c | 569088 | 14919 50385 | 14188 6967 262229 37.6 | 10.174 % | c | 577739 | 14919 50385 | 15607 8244 334493 40.6 | 10.174 % | c | 590714 | 14919 50385 | 17168 13102 586851 44.8 | 10.174 % | c ============================================================================== c [1mFound solution: 141440[0m c ---[ 0]---> Sorter-cost: 8 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 | 591860 | 14931 50412 | 4977 14248 635435 44.6 | 10.174 % | c | 591963 | 14931 50412 | 5474 3665 110627 30.2 | 10.187 % | c | 592113 | 14931 50412 | 6022 3815 113648 29.8 | 10.187 % | c | 592338 | 14931 50412 | 6624 4040 124359 30.8 | 10.187 % | c | 592676 | 14931 50412 | 7286 4378 135745 31.0 | 10.187 % | c | 593185 | 14931 50412 | 8015 4887 154926 31.7 | 10.187 % | c ============================================================================== c [1mFound solution: 127360[0m c ---[ 0]---> Sorter-cost: 7 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 | 593687 | 14892 50276 | 4964 5383 187551 34.8 | 10.187 % | c | 593787 | 14892 50276 | 5460 2792 79830 28.6 | 10.402 % | c | 593937 | 14892 50276 | 6006 2942 82515 28.0 | 10.402 % | c | 594162 | 14892 50276 | 6607 3167 90802 28.7 | 10.402 % | c | 594499 | 14892 50276 | 7267 3504 102574 29.3 | 10.402 % | c | 595005 | 14892 50276 | 7994 4010 121322 30.3 | 10.402 % | c | 595765 | 14892 50276 | 8794 4770 157152 32.9 | 10.402 % | c | 596904 | 14892 50276 | 9673 5909 201729 34.1 | 10.402 % | c | 598613 | 14892 50276 | 10640 7618 290927 38.2 | 10.402 % | c | 601175 | 14892 50276 | 11704 10180 403974 39.7 | 10.402 % | c | 605019 | 14851 50183 | 12875 7787 288315 37.0 | 10.795 % | c | 610786 | 14851 50183 | 14162 13554 589955 43.5 | 10.795 % | c | 619435 | 14829 50132 | 15579 14797 637237 43.1 | 11.057 % | c | 632410 | 14829 50132 | 17137 11330 497016 43.9 | 11.057 % | c | 651871 | 14829 50132 | 18850 12828 544496 42.4 | 11.057 % | c | 681063 | 14818 50106 | 20735 12477 417985 33.5 | 11.187 % | c | 724852 | 14797 50058 | 22809 13453 508999 37.8 | 11.416 % | c ============================================================================== c [1mFound solution: 117632[0m c ---[ 0]---> Sorter-cost: 7 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 | 725185 | 14804 50076 | 4934 13786 517662 37.5 | 11.416 % | c | 725287 | 14804 50076 | 5427 3549 91459 25.8 | 11.430 % | c | 725438 | 14804 50076 | 5970 3700 96454 26.1 | 11.430 % | c | 725663 | 14804 50076 | 6567 3925 103115 26.3 | 11.430 % | c | 726000 | 14804 50076 | 7223 4262 109958 25.8 | 11.430 % | c | 726506 | 14804 50076 | 7946 4768 126560 26.5 | 11.430 % | c | 727266 | 14804 50076 | 8740 5528 156340 28.3 | 11.430 % | c | 728405 | 14804 50076 | 9614 6667 194011 29.1 | 11.430 % | c | 730114 | 14804 50076 | 10576 8376 265522 31.7 | 11.430 % | c | 732676 | 14804 50076 | 11634 10938 367817 33.6 | 11.430 % | c | 736521 | 14804 50076 | 12797 8592 319410 37.2 | 11.430 % | c ============================================================================== c [1mFound solution: 113536[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 | 738861 | 14810 50092 | 4936 10932 465586 42.6 | 11.430 % | c | 738961 | 14810 50092 | 5429 2833 99866 35.3 | 11.444 % | c | 739112 | 14810 50092 | 5972 2984 102707 34.4 | 11.444 % | c | 739339 | 14810 50092 | 6569 3211 107372 33.4 | 11.444 % | c | 739677 | 14810 50092 | 7226 3549 115876 32.7 | 11.444 % | c | 740183 | 14810 50092 | 7949 4055 128536 31.7 | 11.444 % | c | 740943 | 14810 50092 | 8744 4815 150532 31.3 | 11.444 % | c | 742083 | 14810 50092 | 9618 5955 182592 30.7 | 11.444 % | c | 743791 | 14810 50092 | 10580 7663 261883 34.2 | 11.444 % | c | 746355 | 14810 50092 | 11638 10227 355624 34.8 | 11.444 % | c | 750199 | 14810 50092 | 12802 7898 256703 32.5 | 11.444 % | c | 755965 | 14810 50092 | 14082 6952 251331 36.2 | 11.444 % | c | 764615 | 14810 50092 | 15491 8135 295700 36.3 | 11.444 % | c | 777590 | 14810 50092 | 17040 12960 564926 43.6 | 11.444 % | c | 797051 | 14810 50092 | 18744 14662 547954 37.4 | 11.444 % | c | 826243 | 14790 50045 | 20618 14787 532928 36.0 | 11.705 % | c | 870032 | 14790 50045 | 22680 15957 753152 47.2 | 11.705 % |
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing Stack size limit: 67108864 bytes Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb Enforcing VSIZE limit: 994918400 bytes Current StackSize limit: 67108864 bytes Raw data (/proc/10047/stat): 10047 (minisat+_script) R 10046 10047 15400 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1797179298 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/10047/statm): 174 3 169 147 0 27 0 [pid=10047] vsize: 696 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libtermcap.so.2 open syscall for file tls/i686/libtermcap.so.2 open syscall for file tls/mmx/libtermcap.so.2 open syscall for file tls/libtermcap.so.2 open syscall for file i686/mmx/libtermcap.so.2 open syscall for file i686/libtermcap.so.2 open syscall for file mmx/libtermcap.so.2 open syscall for file libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/libtermcap.so.2 open syscall for file /etc/ld.so.cache open syscall for file /lib/libtermcap.so.2 open syscall for file tls/i686/mmx/libdl.so.2 open syscall for file tls/i686/libdl.so.2 open syscall for file tls/mmx/libdl.so.2 open syscall for file tls/libdl.so.2 open syscall for file i686/mmx/libdl.so.2 open syscall for file i686/libdl.so.2 open syscall for file mmx/libdl.so.2 open syscall for file libdl.so.2 open syscall for file /oldhome/oroussel/lib/libdl.so.2 open syscall for file /lib/libdl.so.2 open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /lib/tls/libc.so.6 open syscall for file /dev/tty open syscall for file /etc/mtab open syscall for file /proc/meminfo open syscall for file /oldhome/oroussel/solvers/minisat+_script New process pid=10048 New process pid=10049 New process pid=10050 One traced child (pid=10049) exited with status: 0 execve syscall for /bin/sed executable open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=10050) exited with status: 0 One traced child (pid=10048) exited with status: 0 New process pid=10051 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-markshare1.opb [startup+10.003 s] Raw data (loadavg): 0.93 0.96 0.91 2/57 10051 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 1043 0 0 0 979 8 0 0 25 0 1 0 1797179303 4575232 1029 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10051/statm): 1117 1029 145 145 0 972 0 [pid=10051] vsize: 4468 Current children cumulated CPU time (s) 9.87 Current children cumulated vsize (Kb) 6592 [startup+20.0046 s] Raw data (loadavg): 0.94 0.96 0.91 2/57 10051 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 1440 0 0 0 1971 11 0 0 25 0 1 0 1797179303 6217728 1426 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 1518 1426 145 145 0 1373 0 [pid=10051] vsize: 6072 Current children cumulated CPU time (s) 19.82 Current children cumulated vsize (Kb) 8196 [startup+30.0053 s] Raw data (loadavg): 0.95 0.96 0.91 2/57 10051 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 1459 0 0 0 2970 12 0 0 25 0 1 0 1797179303 6295552 1445 4294967295 134512640 135094434 3221224432 3221223024 134556688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 1537 1445 145 145 0 1392 0 [pid=10051] vsize: 6148 Current children cumulated CPU time (s) 29.82 Current children cumulated vsize (Kb) 8272 [startup+40.0059 s] Raw data (loadavg): 0.96 0.96 0.91 2/57 10051 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 1459 0 0 0 3970 12 0 0 25 0 1 0 1797179303 6295552 1445 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 1537 1445 145 145 0 1392 0 [pid=10051] vsize: 6148 Current children cumulated CPU time (s) 39.82 Current children cumulated vsize (Kb) 8272 [startup+50.0075 s] Raw data (loadavg): 0.96 0.96 0.91 2/57 10051 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 1521 0 0 0 4969 13 0 0 25 0 1 0 1797179303 6545408 1507 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 1598 1507 145 145 0 1453 0 [pid=10051] vsize: 6392 Current children cumulated CPU time (s) 49.82 Current children cumulated vsize (Kb) 8516 [startup+60.0082 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 10051 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 1678 0 0 0 5965 14 0 0 25 0 1 0 1797179303 7184384 1664 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10051/statm): 1754 1664 145 145 0 1609 0 [pid=10051] vsize: 7016 Current children cumulated CPU time (s) 59.79 Current children cumulated vsize (Kb) 9140 [startup+70.0098 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 10051 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 1678 0 0 0 6964 14 0 0 25 0 1 0 1797179303 7184384 1664 4294967295 134512640 135094434 3221224432 3221223056 134562085 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 1754 1664 145 145 0 1609 0 [pid=10051] vsize: 7016 Current children cumulated CPU time (s) 69.78 Current children cumulated vsize (Kb) 9140 [startup+80.0104 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 10051 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 1678 0 0 0 7965 14 0 0 25 0 1 0 1797179303 7184384 1664 4294967295 134512640 135094434 3221224432 3221223088 134558398 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 1754 1664 145 145 0 1609 0 [pid=10051] vsize: 7016 Current children cumulated CPU time (s) 79.79 Current children cumulated vsize (Kb) 9140 [startup+90.0111 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 10051 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 1707 0 0 0 8964 15 0 0 25 0 1 0 1797179303 7311360 1693 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 1785 1693 145 145 0 1640 0 [pid=10051] vsize: 7140 Current children cumulated CPU time (s) 89.79 Current children cumulated vsize (Kb) 9264 [startup+100.012 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 10051 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 1727 0 0 0 9964 15 0 0 25 0 1 0 1797179303 7397376 1713 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 1806 1713 145 145 0 1661 0 [pid=10051] vsize: 7224 Current children cumulated CPU time (s) 99.79 Current children cumulated vsize (Kb) 9348 [startup+110.012 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 10051 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 1851 0 0 0 10963 16 0 0 25 0 1 0 1797179303 7917568 1837 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 1933 1837 145 145 0 1788 0 [pid=10051] vsize: 7732 Current children cumulated CPU time (s) 109.79 Current children cumulated vsize (Kb) 9856 [startup+120.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10051 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 1855 0 0 0 11963 16 0 0 25 0 1 0 1797179303 7933952 1841 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 1937 1841 145 145 0 1792 0 [pid=10051] vsize: 7748 Current children cumulated CPU time (s) 119.79 Current children cumulated vsize (Kb) 9872 [startup+130.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10051 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 1855 0 0 0 12963 16 0 0 25 0 1 0 1797179303 7933952 1841 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 1937 1841 145 145 0 1792 0 [pid=10051] vsize: 7748 Current children cumulated CPU time (s) 129.79 Current children cumulated vsize (Kb) 9872 [startup+140.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10051 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 1855 0 0 0 13963 16 0 0 25 0 1 0 1797179303 7933952 1841 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 1937 1841 145 145 0 1792 0 [pid=10051] vsize: 7748 Current children cumulated CPU time (s) 139.79 Current children cumulated vsize (Kb) 9872 [startup+150.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10051 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 1855 0 0 0 14963 16 0 0 25 0 1 0 1797179303 7933952 1841 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 1937 1841 145 145 0 1792 0 [pid=10051] vsize: 7748 Current children cumulated CPU time (s) 149.79 Current children cumulated vsize (Kb) 9872 [startup+160.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10051 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 1855 0 0 0 15964 16 0 0 25 0 1 0 1797179303 7933952 1841 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 1937 1841 145 145 0 1792 0 [pid=10051] vsize: 7748 Current children cumulated CPU time (s) 159.8 Current children cumulated vsize (Kb) 9872 [startup+170.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10051 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 1855 0 0 0 16964 16 0 0 25 0 1 0 1797179303 7933952 1841 4294967295 134512640 135094434 3221224432 3221223076 134558040 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 1937 1841 145 145 0 1792 0 [pid=10051] vsize: 7748 Current children cumulated CPU time (s) 169.8 Current children cumulated vsize (Kb) 9872 [startup+180.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10051 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 1855 0 0 0 17964 16 0 0 25 0 1 0 1797179303 7933952 1841 4294967295 134512640 135094434 3221224432 3221223120 134554793 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 1937 1841 145 145 0 1792 0 [pid=10051] vsize: 7748 Current children cumulated CPU time (s) 179.8 Current children cumulated vsize (Kb) 9872 [startup+190.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10051 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 1855 0 0 0 18964 16 0 0 25 0 1 0 1797179303 7933952 1841 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 1937 1841 145 145 0 1792 0 [pid=10051] vsize: 7748 Current children cumulated CPU time (s) 189.8 Current children cumulated vsize (Kb) 9872 [startup+200.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10051 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 1855 0 0 0 19964 17 0 0 25 0 1 0 1797179303 7933952 1841 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 1937 1841 145 145 0 1792 0 [pid=10051] vsize: 7748 Current children cumulated CPU time (s) 199.81 Current children cumulated vsize (Kb) 9872 [startup+210.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10051 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 1855 0 0 0 20964 17 0 0 25 0 1 0 1797179303 7933952 1841 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 1937 1841 145 145 0 1792 0 [pid=10051] vsize: 7748 Current children cumulated CPU time (s) 209.81 Current children cumulated vsize (Kb) 9872 [startup+220.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10051 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 1855 0 0 0 21964 17 0 0 25 0 1 0 1797179303 7933952 1841 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 1937 1841 145 145 0 1792 0 [pid=10051] vsize: 7748 Current children cumulated CPU time (s) 219.81 Current children cumulated vsize (Kb) 9872 [startup+230.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10051 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 1856 0 0 0 22964 17 0 0 25 0 1 0 1797179303 7933952 1842 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 1937 1842 145 145 0 1792 0 [pid=10051] vsize: 7748 Current children cumulated CPU time (s) 229.81 Current children cumulated vsize (Kb) 9872 [startup+240.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10051 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 1874 0 0 0 23964 17 0 0 25 0 1 0 1797179303 8065024 1860 4294967295 134512640 135094434 3221224432 3221223088 134557896 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 1969 1860 145 145 0 1824 0 [pid=10051] vsize: 7876 Current children cumulated CPU time (s) 239.81 Current children cumulated vsize (Kb) 10000 [startup+250.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10051 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 1874 0 0 0 24965 17 0 0 25 0 1 0 1797179303 8065024 1860 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 1969 1860 145 145 0 1824 0 [pid=10051] vsize: 7876 Current children cumulated CPU time (s) 249.82 Current children cumulated vsize (Kb) 10000 [startup+260.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10051 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 1874 0 0 0 25965 17 0 0 25 0 1 0 1797179303 8065024 1860 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 1969 1860 145 145 0 1824 0 [pid=10051] vsize: 7876 Current children cumulated CPU time (s) 259.82 Current children cumulated vsize (Kb) 10000 [startup+270.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10051 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 1874 0 0 0 26965 17 0 0 25 0 1 0 1797179303 8065024 1860 4294967295 134512640 135094434 3221224432 3221223088 134558123 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 1969 1860 145 145 0 1824 0 [pid=10051] vsize: 7876 Current children cumulated CPU time (s) 269.82 Current children cumulated vsize (Kb) 10000 [startup+280.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10051 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 1970 0 0 0 27963 18 0 0 25 0 1 0 1797179303 8454144 1956 4294967295 134512640 135094434 3221224432 3221223104 134555943 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 2064 1956 145 145 0 1919 0 [pid=10051] vsize: 8256 Current children cumulated CPU time (s) 279.81 Current children cumulated vsize (Kb) 10380 [startup+290.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10051 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 2026 0 0 0 28963 18 0 0 25 0 1 0 1797179303 8683520 2012 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 2120 2012 145 145 0 1975 0 [pid=10051] vsize: 8480 Current children cumulated CPU time (s) 289.81 Current children cumulated vsize (Kb) 10604 [startup+300.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10051 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 2030 0 0 0 29963 18 0 0 25 0 1 0 1797179303 8699904 2016 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 2124 2016 145 145 0 1979 0 [pid=10051] vsize: 8496 Current children cumulated CPU time (s) 299.81 Current children cumulated vsize (Kb) 10620 [startup+310.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10051 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 2197 0 0 0 30961 19 0 0 25 0 1 0 1797179303 9375744 2183 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 2289 2183 145 145 0 2144 0 [pid=10051] vsize: 9156 Current children cumulated CPU time (s) 309.8 Current children cumulated vsize (Kb) 11280 [startup+320.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10051 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 2200 0 0 0 31961 19 0 0 25 0 1 0 1797179303 9388032 2186 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 2292 2186 145 145 0 2147 0 [pid=10051] vsize: 9168 Current children cumulated CPU time (s) 319.8 Current children cumulated vsize (Kb) 11292 [startup+330.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10051 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 2200 0 0 0 32961 19 0 0 25 0 1 0 1797179303 9388032 2186 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 2292 2186 145 145 0 2147 0 [pid=10051] vsize: 9168 Current children cumulated CPU time (s) 329.8 Current children cumulated vsize (Kb) 11292 [startup+340.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10051 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 2200 0 0 0 33961 19 0 0 25 0 1 0 1797179303 9388032 2186 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 2292 2186 145 145 0 2147 0 [pid=10051] vsize: 9168 Current children cumulated CPU time (s) 339.8 Current children cumulated vsize (Kb) 11292 [startup+350.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10051 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 2200 0 0 0 34961 19 0 0 25 0 1 0 1797179303 9388032 2186 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 2292 2186 145 145 0 2147 0 [pid=10051] vsize: 9168 Current children cumulated CPU time (s) 349.8 Current children cumulated vsize (Kb) 11292 [startup+360.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10051 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 2200 0 0 0 35961 19 0 0 25 0 1 0 1797179303 9388032 2186 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 2292 2186 145 145 0 2147 0 [pid=10051] vsize: 9168 Current children cumulated CPU time (s) 359.8 Current children cumulated vsize (Kb) 11292 [startup+370.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10051 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 2200 0 0 0 36961 19 0 0 25 0 1 0 1797179303 9388032 2186 4294967295 134512640 135094434 3221224432 3221223056 134562144 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 2292 2186 145 145 0 2147 0 [pid=10051] vsize: 9168 Current children cumulated CPU time (s) 369.8 Current children cumulated vsize (Kb) 11292 [startup+380.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10051 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 2200 0 0 0 37962 19 0 0 25 0 1 0 1797179303 9388032 2186 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 2292 2186 145 145 0 2147 0 [pid=10051] vsize: 9168 Current children cumulated CPU time (s) 379.81 Current children cumulated vsize (Kb) 11292 [startup+390.035 s] Raw data (loadavg): 1.15 1.00 0.92 2/60 10086 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 2200 0 0 0 38962 19 0 0 25 0 1 0 1797179303 9388032 2186 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 2292 2186 145 145 0 2147 0 [pid=10051] vsize: 9168 Current children cumulated CPU time (s) 389.81 Current children cumulated vsize (Kb) 11292 [startup+400.04 s] Raw data (loadavg): 1.13 1.00 0.92 2/57 10102 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 2200 0 0 0 39962 19 0 0 25 0 1 0 1797179303 9388032 2186 4294967295 134512640 135094434 3221224432 3221223072 134556681 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 2292 2186 145 145 0 2147 0 [pid=10051] vsize: 9168 Current children cumulated CPU time (s) 399.81 Current children cumulated vsize (Kb) 11292 [startup+410.04 s] Raw data (loadavg): 1.11 1.00 0.92 2/57 10102 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 2200 0 0 0 40962 19 0 0 25 0 1 0 1797179303 9388032 2186 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 2292 2186 145 145 0 2147 0 [pid=10051] vsize: 9168 Current children cumulated CPU time (s) 409.81 Current children cumulated vsize (Kb) 11292 [startup+420.041 s] Raw data (loadavg): 1.09 1.00 0.92 2/57 10102 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 2242 0 0 0 41962 20 0 0 25 0 1 0 1797179303 9564160 2228 4294967295 134512640 135094434 3221224432 3221223088 134557917 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 2335 2228 145 145 0 2190 0 [pid=10051] vsize: 9340 Current children cumulated CPU time (s) 419.82 Current children cumulated vsize (Kb) 11464 [startup+430.042 s] Raw data (loadavg): 1.08 1.00 0.92 2/57 10102 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 2253 0 0 0 42962 20 0 0 25 0 1 0 1797179303 9605120 2239 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 2345 2239 145 145 0 2200 0 [pid=10051] vsize: 9380 Current children cumulated CPU time (s) 429.82 Current children cumulated vsize (Kb) 11504 [startup+440.042 s] Raw data (loadavg): 1.07 1.00 0.92 2/57 10102 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 2345 0 0 0 43961 21 0 0 25 0 1 0 1797179303 9998336 2331 4294967295 134512640 135094434 3221224432 3221223076 134562166 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 2441 2331 145 145 0 2296 0 [pid=10051] vsize: 9764 Current children cumulated CPU time (s) 439.82 Current children cumulated vsize (Kb) 11888 [startup+450.043 s] Raw data (loadavg): 1.06 1.00 0.92 2/57 10102 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 2359 0 0 0 44961 21 0 0 25 0 1 0 1797179303 10055680 2345 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 2455 2345 145 145 0 2310 0 [pid=10051] vsize: 9820 Current children cumulated CPU time (s) 449.82 Current children cumulated vsize (Kb) 11944 [startup+460.043 s] Raw data (loadavg): 1.05 1.00 0.92 2/57 10104 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 2362 0 0 0 45961 21 0 0 25 0 1 0 1797179303 10072064 2348 4294967295 134512640 135094434 3221224432 3221223088 134558176 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 2459 2348 145 145 0 2314 0 [pid=10051] vsize: 9836 Current children cumulated CPU time (s) 459.82 Current children cumulated vsize (Kb) 11960 [startup+470.045 s] Raw data (loadavg): 1.04 1.00 0.92 2/57 10106 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 2362 0 0 0 46961 21 0 0 25 0 1 0 1797179303 10072064 2348 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 2459 2348 145 145 0 2314 0 [pid=10051] vsize: 9836 Current children cumulated CPU time (s) 469.82 Current children cumulated vsize (Kb) 11960 [startup+480.046 s] Raw data (loadavg): 1.03 1.00 0.92 2/57 10106 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 2420 0 0 0 47960 22 0 0 25 0 1 0 1797179303 10309632 2406 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 2517 2406 145 145 0 2372 0 [pid=10051] vsize: 10068 Current children cumulated CPU time (s) 479.82 Current children cumulated vsize (Kb) 12192 [startup+490.046 s] Raw data (loadavg): 1.03 1.00 0.92 2/57 10106 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 2454 0 0 0 48959 22 0 0 25 0 1 0 1797179303 10448896 2440 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 2551 2440 145 145 0 2406 0 [pid=10051] vsize: 10204 Current children cumulated CPU time (s) 489.81 Current children cumulated vsize (Kb) 12328 [startup+500.048 s] Raw data (loadavg): 1.02 1.00 0.92 2/57 10106 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 2611 0 0 0 49956 23 0 0 25 0 1 0 1797179303 11083776 2597 4294967295 134512640 135094434 3221224432 3221223088 134558135 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 2706 2597 145 145 0 2561 0 [pid=10051] vsize: 10824 Current children cumulated CPU time (s) 499.79 Current children cumulated vsize (Kb) 12948 [startup+510.049 s] Raw data (loadavg): 1.02 1.00 0.92 2/57 10106 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 2621 0 0 0 50957 23 0 0 25 0 1 0 1797179303 11124736 2607 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 2716 2607 145 145 0 2571 0 [pid=10051] vsize: 10864 Current children cumulated CPU time (s) 509.8 Current children cumulated vsize (Kb) 12988 [startup+520.05 s] Raw data (loadavg): 1.02 1.00 0.92 2/57 10106 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 2670 0 0 0 51956 24 0 0 25 0 1 0 1797179303 11325440 2656 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 2765 2656 145 145 0 2620 0 [pid=10051] vsize: 11060 Current children cumulated CPU time (s) 519.8 Current children cumulated vsize (Kb) 13184 [startup+530.051 s] Raw data (loadavg): 1.01 1.00 0.92 2/57 10106 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 2692 0 0 0 52956 24 0 0 25 0 1 0 1797179303 11423744 2678 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 2789 2678 145 145 0 2644 0 [pid=10051] vsize: 11156 Current children cumulated CPU time (s) 529.8 Current children cumulated vsize (Kb) 13280 [startup+540.052 s] Raw data (loadavg): 1.01 1.00 0.92 2/57 10106 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 2696 0 0 0 53957 24 0 0 25 0 1 0 1797179303 11440128 2682 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 2793 2682 145 145 0 2648 0 [pid=10051] vsize: 11172 Current children cumulated CPU time (s) 539.81 Current children cumulated vsize (Kb) 13296 [startup+550.052 s] Raw data (loadavg): 1.01 1.00 0.92 2/57 10106 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 2738 0 0 0 54956 24 0 0 25 0 1 0 1797179303 11616256 2724 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 2836 2724 145 145 0 2691 0 [pid=10051] vsize: 11344 Current children cumulated CPU time (s) 549.8 Current children cumulated vsize (Kb) 13468 [startup+560.053 s] Raw data (loadavg): 1.01 1.00 0.92 2/57 10106 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 2757 0 0 0 55956 24 0 0 25 0 1 0 1797179303 11694080 2743 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 2855 2743 145 145 0 2710 0 [pid=10051] vsize: 11420 Current children cumulated CPU time (s) 559.8 Current children cumulated vsize (Kb) 13544 [startup+570.052 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10106 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 2782 0 0 0 56956 24 0 0 25 0 1 0 1797179303 11796480 2768 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 2880 2768 145 145 0 2735 0 [pid=10051] vsize: 11520 Current children cumulated CPU time (s) 569.8 Current children cumulated vsize (Kb) 13644 [startup+580.053 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10106 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 2786 0 0 0 57956 24 0 0 25 0 1 0 1797179303 11812864 2772 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 2884 2772 145 145 0 2739 0 [pid=10051] vsize: 11536 Current children cumulated CPU time (s) 579.8 Current children cumulated vsize (Kb) 13660 [startup+590.054 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10106 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 2804 0 0 0 58956 25 0 0 25 0 1 0 1797179303 11882496 2790 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 2901 2790 145 145 0 2756 0 [pid=10051] vsize: 11604 Current children cumulated CPU time (s) 589.81 Current children cumulated vsize (Kb) 13728 [startup+600.055 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10106 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 2807 0 0 0 59957 25 0 0 25 0 1 0 1797179303 11890688 2793 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 2903 2793 145 145 0 2758 0 [pid=10051] vsize: 11612 Current children cumulated CPU time (s) 599.82 Current children cumulated vsize (Kb) 13736 [startup+610.056 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10106 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 2822 0 0 0 60957 25 0 0 25 0 1 0 1797179303 11952128 2808 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 2918 2808 145 145 0 2773 0 [pid=10051] vsize: 11672 Current children cumulated CPU time (s) 609.82 Current children cumulated vsize (Kb) 13796 [startup+620.057 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10106 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 2826 0 0 0 61957 25 0 0 25 0 1 0 1797179303 11968512 2812 4294967295 134512640 135094434 3221224432 3221223088 134558123 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 2922 2812 145 145 0 2777 0 [pid=10051] vsize: 11688 Current children cumulated CPU time (s) 619.82 Current children cumulated vsize (Kb) 13812 [startup+630.057 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10106 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 2863 0 0 0 62956 25 0 0 25 0 1 0 1797179303 12124160 2849 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 2960 2849 145 145 0 2815 0 [pid=10051] vsize: 11840 Current children cumulated CPU time (s) 629.81 Current children cumulated vsize (Kb) 13964 [startup+640.058 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10106 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 2867 0 0 0 63957 25 0 0 25 0 1 0 1797179303 12140544 2853 4294967295 134512640 135094434 3221224432 3221223120 134554733 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 2964 2853 145 145 0 2819 0 [pid=10051] vsize: 11856 Current children cumulated CPU time (s) 639.82 Current children cumulated vsize (Kb) 13980 [startup+650.058 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10106 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 2903 0 0 0 64956 26 0 0 25 0 1 0 1797179303 12304384 2889 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 3004 2889 145 145 0 2859 0 [pid=10051] vsize: 12016 Current children cumulated CPU time (s) 649.82 Current children cumulated vsize (Kb) 14140 [startup+660.059 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10106 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 2909 0 0 0 65956 26 0 0 25 0 1 0 1797179303 12328960 2895 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 3010 2895 145 145 0 2865 0 [pid=10051] vsize: 12040 Current children cumulated CPU time (s) 659.82 Current children cumulated vsize (Kb) 14164 [startup+670.059 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10106 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 2922 0 0 0 66956 26 0 0 25 0 1 0 1797179303 12394496 2908 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 3026 2908 145 145 0 2881 0 [pid=10051] vsize: 12104 Current children cumulated CPU time (s) 669.82 Current children cumulated vsize (Kb) 14228 [startup+680.059 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10106 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 2930 0 0 0 67955 26 0 0 25 0 1 0 1797179303 12427264 2916 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10051/statm): 3034 2916 145 145 0 2889 0 [pid=10051] vsize: 12136 Current children cumulated CPU time (s) 679.81 Current children cumulated vsize (Kb) 14260 [startup+690.06 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10106 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 2993 0 0 0 68954 27 0 0 25 0 1 0 1797179303 12709888 2979 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 3103 2979 145 145 0 2958 0 [pid=10051] vsize: 12412 Current children cumulated CPU time (s) 689.81 Current children cumulated vsize (Kb) 14536 [startup+700.062 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10106 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 2998 0 0 0 69954 27 0 0 25 0 1 0 1797179303 12734464 2984 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 3109 2984 145 145 0 2964 0 [pid=10051] vsize: 12436 Current children cumulated CPU time (s) 699.81 Current children cumulated vsize (Kb) 14560 [startup+710.062 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10106 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3002 0 0 0 70954 27 0 0 25 0 1 0 1797179303 12759040 2988 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 3115 2988 145 145 0 2970 0 [pid=10051] vsize: 12460 Current children cumulated CPU time (s) 709.81 Current children cumulated vsize (Kb) 14584 [startup+720.063 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10106 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3009 0 0 0 71955 27 0 0 25 0 1 0 1797179303 12783616 2995 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 3121 2995 145 145 0 2976 0 [pid=10051] vsize: 12484 Current children cumulated CPU time (s) 719.82 Current children cumulated vsize (Kb) 14608 [startup+730.063 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10106 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3009 0 0 0 72955 27 0 0 25 0 1 0 1797179303 12783616 2995 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 3121 2995 145 145 0 2976 0 [pid=10051] vsize: 12484 Current children cumulated CPU time (s) 729.82 Current children cumulated vsize (Kb) 14608 [startup+740.064 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10106 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3040 0 0 0 73954 27 0 0 25 0 1 0 1797179303 12914688 3026 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 3153 3026 145 145 0 3008 0 [pid=10051] vsize: 12612 Current children cumulated CPU time (s) 739.81 Current children cumulated vsize (Kb) 14736 [startup+750.065 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3042 0 0 0 74954 28 0 0 25 0 1 0 1797179303 12922880 3028 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10051/statm): 3155 3028 145 145 0 3010 0 [pid=10051] vsize: 12620 Current children cumulated CPU time (s) 749.82 Current children cumulated vsize (Kb) 14744 [startup+760.065 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3063 0 0 0 75953 28 0 0 25 0 1 0 1797179303 13012992 3049 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10051/statm): 3177 3049 145 145 0 3032 0 [pid=10051] vsize: 12708 Current children cumulated CPU time (s) 759.81 Current children cumulated vsize (Kb) 14832 [startup+770.066 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3063 0 0 0 76953 29 0 0 25 0 1 0 1797179303 13012992 3049 4294967295 134512640 135094434 3221224432 3221223088 134557914 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10051/statm): 3177 3049 145 145 0 3032 0 [pid=10051] vsize: 12708 Current children cumulated CPU time (s) 769.82 Current children cumulated vsize (Kb) 14832 [startup+780.067 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3063 0 0 0 77952 29 0 0 25 0 1 0 1797179303 13012992 3049 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10051/statm): 3177 3049 145 145 0 3032 0 [pid=10051] vsize: 12708 Current children cumulated CPU time (s) 779.81 Current children cumulated vsize (Kb) 14832 [startup+790.067 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3063 0 0 0 78951 30 0 0 25 0 1 0 1797179303 13012992 3049 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10051/statm): 3177 3049 145 145 0 3032 0 [pid=10051] vsize: 12708 Current children cumulated CPU time (s) 789.81 Current children cumulated vsize (Kb) 14832 [startup+800.069 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3063 0 0 0 79951 31 0 0 25 0 1 0 1797179303 13012992 3049 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10051/statm): 3177 3049 145 145 0 3032 0 [pid=10051] vsize: 12708 Current children cumulated CPU time (s) 799.82 Current children cumulated vsize (Kb) 14832 [startup+810.07 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3063 0 0 0 80950 32 0 0 25 0 1 0 1797179303 13012992 3049 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10051/statm): 3177 3049 145 145 0 3032 0 [pid=10051] vsize: 12708 Current children cumulated CPU time (s) 809.82 Current children cumulated vsize (Kb) 14832 [startup+820.07 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3063 0 0 0 81950 32 0 0 25 0 1 0 1797179303 13012992 3049 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10051/statm): 3177 3049 145 145 0 3032 0 [pid=10051] vsize: 12708 Current children cumulated CPU time (s) 819.82 Current children cumulated vsize (Kb) 14832 [startup+830.071 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3063 0 0 0 82949 33 0 0 25 0 1 0 1797179303 13012992 3049 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10051/statm): 3177 3049 145 145 0 3032 0 [pid=10051] vsize: 12708 Current children cumulated CPU time (s) 829.82 Current children cumulated vsize (Kb) 14832 [startup+840.071 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3063 0 0 0 83949 33 0 0 25 0 1 0 1797179303 13012992 3049 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10051/statm): 3177 3049 145 145 0 3032 0 [pid=10051] vsize: 12708 Current children cumulated CPU time (s) 839.82 Current children cumulated vsize (Kb) 14832 [startup+850.072 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3063 0 0 0 84948 33 0 0 25 0 1 0 1797179303 13012992 3049 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10051/statm): 3177 3049 145 145 0 3032 0 [pid=10051] vsize: 12708 Current children cumulated CPU time (s) 849.81 Current children cumulated vsize (Kb) 14832 [startup+860.073 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3063 0 0 0 85948 34 0 0 25 0 1 0 1797179303 13012992 3049 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10051/statm): 3177 3049 145 145 0 3032 0 [pid=10051] vsize: 12708 Current children cumulated CPU time (s) 859.82 Current children cumulated vsize (Kb) 14832 [startup+870.073 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3063 0 0 0 86947 35 0 0 25 0 1 0 1797179303 13012992 3049 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10051/statm): 3177 3049 145 145 0 3032 0 [pid=10051] vsize: 12708 Current children cumulated CPU time (s) 869.82 Current children cumulated vsize (Kb) 14832 [startup+880.075 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3063 0 0 0 87947 35 0 0 25 0 1 0 1797179303 13012992 3049 4294967295 134512640 135094434 3221224432 3221223024 134557199 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10051/statm): 3177 3049 145 145 0 3032 0 [pid=10051] vsize: 12708 Current children cumulated CPU time (s) 879.82 Current children cumulated vsize (Kb) 14832 [startup+890.076 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3063 0 0 0 88946 36 0 0 25 0 1 0 1797179303 13012992 3049 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10051/statm): 3177 3049 145 145 0 3032 0 [pid=10051] vsize: 12708 Current children cumulated CPU time (s) 889.82 Current children cumulated vsize (Kb) 14832 [startup+900.077 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3063 0 0 0 89945 37 0 0 25 0 1 0 1797179303 13012992 3049 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10051/statm): 3177 3049 145 145 0 3032 0 [pid=10051] vsize: 12708 Current children cumulated CPU time (s) 899.82 Current children cumulated vsize (Kb) 14832 [startup+910.078 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3063 0 0 0 90945 37 0 0 25 0 1 0 1797179303 13012992 3049 4294967295 134512640 135094434 3221224432 3221223024 134551454 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10051/statm): 3177 3049 145 145 0 3032 0 [pid=10051] vsize: 12708 Current children cumulated CPU time (s) 909.82 Current children cumulated vsize (Kb) 14832 [startup+920.078 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3063 0 0 0 91944 38 0 0 25 0 1 0 1797179303 13012992 3049 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10051/statm): 3177 3049 145 145 0 3032 0 [pid=10051] vsize: 12708 Current children cumulated CPU time (s) 919.82 Current children cumulated vsize (Kb) 14832 [startup+930.08 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3063 0 0 0 92944 38 0 0 25 0 1 0 1797179303 13012992 3049 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10051/statm): 3177 3049 145 145 0 3032 0 [pid=10051] vsize: 12708 Current children cumulated CPU time (s) 929.82 Current children cumulated vsize (Kb) 14832 [startup+940.081 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3065 0 0 0 93944 39 0 0 25 0 1 0 1797179303 13029376 3051 4294967295 134512640 135094434 3221224432 3221223088 134558172 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10051/statm): 3181 3051 145 145 0 3036 0 [pid=10051] vsize: 12724 Current children cumulated CPU time (s) 939.83 Current children cumulated vsize (Kb) 14848 [startup+950.082 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3065 0 0 0 94943 39 0 0 25 0 1 0 1797179303 13029376 3051 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10051/statm): 3181 3051 145 145 0 3036 0 [pid=10051] vsize: 12724 Current children cumulated CPU time (s) 949.82 Current children cumulated vsize (Kb) 14848 [startup+960.083 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3065 0 0 0 95943 39 0 0 25 0 1 0 1797179303 13029376 3051 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10051/statm): 3181 3051 145 145 0 3036 0 [pid=10051] vsize: 12724 Current children cumulated CPU time (s) 959.82 Current children cumulated vsize (Kb) 14848 [startup+970.083 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3065 0 0 0 96943 40 0 0 25 0 1 0 1797179303 13029376 3051 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10051/statm): 3181 3051 145 145 0 3036 0 [pid=10051] vsize: 12724 Current children cumulated CPU time (s) 969.83 Current children cumulated vsize (Kb) 14848 [startup+980.084 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3065 0 0 0 97943 40 0 0 25 0 1 0 1797179303 13029376 3051 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 3181 3051 145 145 0 3036 0 [pid=10051] vsize: 12724 Current children cumulated CPU time (s) 979.83 Current children cumulated vsize (Kb) 14848 [startup+990.085 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3065 0 0 0 98943 40 0 0 25 0 1 0 1797179303 13029376 3051 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 3181 3051 145 145 0 3036 0 [pid=10051] vsize: 12724 Current children cumulated CPU time (s) 989.83 Current children cumulated vsize (Kb) 14848 [startup+1000.09 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3065 0 0 0 99943 40 0 0 25 0 1 0 1797179303 13029376 3051 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10051/statm): 3181 3051 145 145 0 3036 0 [pid=10051] vsize: 12724 Current children cumulated CPU time (s) 999.83 Current children cumulated vsize (Kb) 14848 [startup+1010.09 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3065 0 0 0 100942 40 0 0 25 0 1 0 1797179303 13029376 3051 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 3181 3051 145 145 0 3036 0 [pid=10051] vsize: 12724 Current children cumulated CPU time (s) 1009.82 Current children cumulated vsize (Kb) 14848 [startup+1020.09 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3065 0 0 0 101942 40 0 0 25 0 1 0 1797179303 13029376 3051 4294967295 134512640 135094434 3221224432 3221223088 134557925 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 3181 3051 145 145 0 3036 0 [pid=10051] vsize: 12724 Current children cumulated CPU time (s) 1019.82 Current children cumulated vsize (Kb) 14848 [startup+1030.09 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3065 0 0 0 102943 40 0 0 25 0 1 0 1797179303 13029376 3051 4294967295 134512640 135094434 3221224432 3221223088 134558426 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 3181 3051 145 145 0 3036 0 [pid=10051] vsize: 12724 Current children cumulated CPU time (s) 1029.83 Current children cumulated vsize (Kb) 14848 [startup+1040.09 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3065 0 0 0 103943 41 0 0 25 0 1 0 1797179303 13029376 3051 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 3181 3051 145 145 0 3036 0 [pid=10051] vsize: 12724 Current children cumulated CPU time (s) 1039.84 Current children cumulated vsize (Kb) 14848 [startup+1050.09 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3065 0 0 0 104943 41 0 0 25 0 1 0 1797179303 13029376 3051 4294967295 134512640 135094434 3221224432 3221223016 134552439 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 3181 3051 145 145 0 3036 0 [pid=10051] vsize: 12724 Current children cumulated CPU time (s) 1049.84 Current children cumulated vsize (Kb) 14848 [startup+1060.09 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3065 0 0 0 105943 41 0 0 25 0 1 0 1797179303 13029376 3051 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 3181 3051 145 145 0 3036 0 [pid=10051] vsize: 12724 Current children cumulated CPU time (s) 1059.84 Current children cumulated vsize (Kb) 14848 [startup+1070.09 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3065 0 0 0 106944 41 0 0 25 0 1 0 1797179303 13029376 3051 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 3181 3051 145 145 0 3036 0 [pid=10051] vsize: 12724 Current children cumulated CPU time (s) 1069.85 Current children cumulated vsize (Kb) 14848 [startup+1080.09 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3065 0 0 0 107944 41 0 0 25 0 1 0 1797179303 13029376 3051 4294967295 134512640 135094434 3221224432 3221223088 134557914 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 3181 3051 145 145 0 3036 0 [pid=10051] vsize: 12724 Current children cumulated CPU time (s) 1079.85 Current children cumulated vsize (Kb) 14848 [startup+1090.09 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3065 0 0 0 108944 41 0 0 25 0 1 0 1797179303 13029376 3051 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 3181 3051 145 145 0 3036 0 [pid=10051] vsize: 12724 Current children cumulated CPU time (s) 1089.85 Current children cumulated vsize (Kb) 14848 [startup+1100.09 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3065 0 0 0 109944 41 0 0 25 0 1 0 1797179303 13029376 3051 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 3181 3051 145 145 0 3036 0 [pid=10051] vsize: 12724 Current children cumulated CPU time (s) 1099.85 Current children cumulated vsize (Kb) 14848 [startup+1110.09 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3065 0 0 0 110944 41 0 0 25 0 1 0 1797179303 13029376 3051 4294967295 134512640 135094434 3221224432 3221223088 134558141 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 3181 3051 145 145 0 3036 0 [pid=10051] vsize: 12724 Current children cumulated CPU time (s) 1109.85 Current children cumulated vsize (Kb) 14848 [startup+1120.09 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3065 0 0 0 111945 41 0 0 25 0 1 0 1797179303 13029376 3051 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 3181 3051 145 145 0 3036 0 [pid=10051] vsize: 12724 Current children cumulated CPU time (s) 1119.86 Current children cumulated vsize (Kb) 14848 [startup+1130.09 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3065 0 0 0 112945 41 0 0 25 0 1 0 1797179303 13029376 3051 4294967295 134512640 135094434 3221224432 3221223056 134557604 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 3181 3051 145 145 0 3036 0 [pid=10051] vsize: 12724 Current children cumulated CPU time (s) 1129.86 Current children cumulated vsize (Kb) 14848 [startup+1140.1 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3122 0 0 0 113945 41 0 0 25 0 1 0 1797179303 13262848 3108 4294967295 134512640 135094434 3221224432 3221223056 134562125 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 3238 3108 145 145 0 3093 0 [pid=10051] vsize: 12952 Current children cumulated CPU time (s) 1139.86 Current children cumulated vsize (Kb) 15076 [startup+1150.1 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3126 0 0 0 114945 41 0 0 25 0 1 0 1797179303 13279232 3112 4294967295 134512640 135094434 3221224432 3221223104 134555673 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 3242 3112 145 145 0 3097 0 [pid=10051] vsize: 12968 Current children cumulated CPU time (s) 1149.86 Current children cumulated vsize (Kb) 15092 [startup+1160.1 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3135 0 0 0 115945 41 0 0 25 0 1 0 1797179303 13320192 3121 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 3252 3121 145 145 0 3107 0 [pid=10051] vsize: 13008 Current children cumulated CPU time (s) 1159.86 Current children cumulated vsize (Kb) 15132 [startup+1170.1 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3213 0 0 0 116944 41 0 0 25 0 1 0 1797179303 13647872 3199 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 3332 3199 145 145 0 3187 0 [pid=10051] vsize: 13328 Current children cumulated CPU time (s) 1169.85 Current children cumulated vsize (Kb) 15452 [startup+1180.1 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3222 0 0 0 117944 41 0 0 25 0 1 0 1797179303 13713408 3208 4294967295 134512640 135094434 3221224432 3221223044 134563089 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 3348 3208 145 145 0 3203 0 [pid=10051] vsize: 13392 Current children cumulated CPU time (s) 1179.85 Current children cumulated vsize (Kb) 15516 [startup+1190.1 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3227 0 0 0 118944 41 0 0 25 0 1 0 1797179303 13717504 3213 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 3349 3213 145 145 0 3204 0 [pid=10051] vsize: 13396 Current children cumulated CPU time (s) 1189.85 Current children cumulated vsize (Kb) 15520 [startup+1200.1 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3227 0 0 0 119958 41 0 0 25 0 1 0 1797179303 13717504 3213 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 3349 3213 145 145 0 3204 0 [pid=10051] vsize: 13396 Current children cumulated CPU time (s) 1199.99 Current children cumulated vsize (Kb) 15520 [startup+1210.23 s] Raw data (loadavg): 1.00 1.00 0.92 3/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3227 0 0 0 120968 41 0 0 25 0 1 0 1797179303 13717504 3213 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 3349 3213 145 145 0 3204 0 [pid=10051] vsize: 13396 Current children cumulated CPU time (s) 1210.09 Current children cumulated vsize (Kb) 15520 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.34 s] Raw data (loadavg): 1.00 1.00 0.92 3/57 10108 Raw data (/proc/10047/stat): 10047 (minisat+_script) S 10046 10047 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797179298 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10047/statm): 531 226 485 147 0 384 0 [pid=10047] vsize: 2124 Raw data (/proc/10051/stat): 10051 (minisat+_64-bit) R 10047 10047 15400 0 -1 0 3227 0 0 0 120969 41 0 0 25 0 1 0 1797179303 13717504 3213 4294967295 134512640 135094434 3221224432 3221223024 134551908 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10051/statm): 3349 3213 145 145 0 3204 0 [pid=10051] vsize: 13396 Current children cumulated CPU time (s) 1210.1 Current children cumulated vsize (Kb) 15520 Sending SIGTERM to -10047 Sleeping 2 seconds One traced child (pid=10047) ended because it received signal 15 (SIGTERM) One traced child (pid=10051) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.39 CPU time (s): 1210.12 CPU user time (s): 1209.69 CPU system time (s): 0.426935 CPU usage (%): 99.9774 Max. virtual memory (cumulated for all children) (Kb): 15520
ERROR: no interpretation found !