Name | mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-markshare1.opb |
MD5SUM | ba87f5dfbaed559dc55bc00bf07dc880 |
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.34 |
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 wulflinc15 THE 2005-09-20 04:24:55 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3366 boxname=wulflinc15 idbench=1022 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: ba87f5dfbaed559dc55bc00bf07dc880 /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-markshare1.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-markshare1.opb IDLAUNCH: 3366 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 450.999 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 : 450.999 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: 901168 kB Buffers: 6968 kB Cached: 97076 kB SwapCached: 744 kB Active: 32360 kB Inactive: 74312 kB HighTotal: 131008 kB HighFree: 32228 kB LowTotal: 903652 kB LowFree: 868940 kB SwapTotal: 2097136 kB SwapFree: 2095884 kB Dirty: 24 kB Writeback: 0 kB Mapped: 5720 kB Slab: 21116 kB Committed_AS: 64132 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-20 04:45:05 (client local time) WITH STATUS 10 IN 1209.91 SECONDS stats: 3366 7 1209.91 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/31378/stat): 31378 (minisat+_script) R 31377 31378 31778 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1797399698 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/31378/statm): 174 3 169 147 0 27 0 [pid=31378] 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=31379 New process pid=31380 New process pid=31381 execve syscall for /bin/sed executable One traced child (pid=31380) exited with status: 0 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=31381) exited with status: 0 One traced child (pid=31379) exited with status: 0 New process pid=31382 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-markshare1.opb [startup+10.0034 s] Raw data (loadavg): 0.93 0.96 0.94 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 1046 0 0 0 980 7 0 0 25 0 1 0 1797399703 4587520 1032 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31382/statm): 1120 1032 145 145 0 975 0 [pid=31382] vsize: 4480 Current children cumulated CPU time (s) 9.87 Current children cumulated vsize (Kb) 6604 [startup+20.0052 s] Raw data (loadavg): 0.94 0.96 0.94 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 1441 0 0 0 1973 10 0 0 25 0 1 0 1797399703 6221824 1427 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 1519 1427 145 145 0 1374 0 [pid=31382] vsize: 6076 Current children cumulated CPU time (s) 19.83 Current children cumulated vsize (Kb) 8200 [startup+30.006 s] Raw data (loadavg): 1.03 0.98 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 1459 0 0 0 2972 10 0 0 25 0 1 0 1797399703 6295552 1445 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31382/statm): 1537 1445 145 145 0 1392 0 [pid=31382] vsize: 6148 Current children cumulated CPU time (s) 29.82 Current children cumulated vsize (Kb) 8272 [startup+40.0068 s] Raw data (loadavg): 1.10 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 1459 0 0 0 3971 10 0 0 25 0 1 0 1797399703 6295552 1445 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 1537 1445 145 145 0 1392 0 [pid=31382] vsize: 6148 Current children cumulated CPU time (s) 39.81 Current children cumulated vsize (Kb) 8272 [startup+50.0086 s] Raw data (loadavg): 1.08 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 1514 0 0 0 4970 11 0 0 25 0 1 0 1797399703 6516736 1500 4294967295 134512640 135094434 3221224432 3221223104 134556073 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 1591 1500 145 145 0 1446 0 [pid=31382] vsize: 6364 Current children cumulated CPU time (s) 49.81 Current children cumulated vsize (Kb) 8488 [startup+60.0095 s] Raw data (loadavg): 1.07 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 1678 0 0 0 5967 12 0 0 25 0 1 0 1797399703 7184384 1664 4294967295 134512640 135094434 3221224432 3221223008 134552446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31382/statm): 1754 1664 145 145 0 1609 0 [pid=31382] vsize: 7016 Current children cumulated CPU time (s) 59.79 Current children cumulated vsize (Kb) 9140 [startup+70.0113 s] Raw data (loadavg): 1.06 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 1678 0 0 0 6966 12 0 0 25 0 1 0 1797399703 7184384 1664 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 1754 1664 145 145 0 1609 0 [pid=31382] vsize: 7016 Current children cumulated CPU time (s) 69.78 Current children cumulated vsize (Kb) 9140 [startup+80.0121 s] Raw data (loadavg): 1.05 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 1678 0 0 0 7966 12 0 0 25 0 1 0 1797399703 7184384 1664 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 1754 1664 145 145 0 1609 0 [pid=31382] vsize: 7016 Current children cumulated CPU time (s) 79.78 Current children cumulated vsize (Kb) 9140 [startup+90.0119 s] Raw data (loadavg): 1.04 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 1707 0 0 0 8966 13 0 0 25 0 1 0 1797399703 7311360 1693 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 1785 1693 145 145 0 1640 0 [pid=31382] vsize: 7140 Current children cumulated CPU time (s) 89.79 Current children cumulated vsize (Kb) 9264 [startup+100.013 s] Raw data (loadavg): 1.03 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 1717 0 0 0 9966 13 0 0 25 0 1 0 1797399703 7360512 1703 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 1797 1703 145 145 0 1652 0 [pid=31382] vsize: 7188 Current children cumulated CPU time (s) 99.79 Current children cumulated vsize (Kb) 9312 [startup+110.014 s] Raw data (loadavg): 1.03 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 1851 0 0 0 10963 14 0 0 25 0 1 0 1797399703 7917568 1837 4294967295 134512640 135094434 3221224432 3221223024 134557037 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 1933 1837 145 145 0 1788 0 [pid=31382] vsize: 7732 Current children cumulated CPU time (s) 109.77 Current children cumulated vsize (Kb) 9856 [startup+120.014 s] Raw data (loadavg): 1.02 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 1855 0 0 0 11963 14 0 0 25 0 1 0 1797399703 7933952 1841 4294967295 134512640 135094434 3221224432 3221223024 134551463 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 1937 1841 145 145 0 1792 0 [pid=31382] vsize: 7748 Current children cumulated CPU time (s) 119.77 Current children cumulated vsize (Kb) 9872 [startup+130.015 s] Raw data (loadavg): 1.02 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 1855 0 0 0 12963 14 0 0 25 0 1 0 1797399703 7933952 1841 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 1937 1841 145 145 0 1792 0 [pid=31382] vsize: 7748 Current children cumulated CPU time (s) 129.77 Current children cumulated vsize (Kb) 9872 [startup+140.016 s] Raw data (loadavg): 1.02 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 1855 0 0 0 13964 14 0 0 25 0 1 0 1797399703 7933952 1841 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 1937 1841 145 145 0 1792 0 [pid=31382] vsize: 7748 Current children cumulated CPU time (s) 139.78 Current children cumulated vsize (Kb) 9872 [startup+150.017 s] Raw data (loadavg): 1.01 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 1855 0 0 0 14964 14 0 0 25 0 1 0 1797399703 7933952 1841 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 1937 1841 145 145 0 1792 0 [pid=31382] vsize: 7748 Current children cumulated CPU time (s) 149.78 Current children cumulated vsize (Kb) 9872 [startup+160.018 s] Raw data (loadavg): 1.01 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 1855 0 0 0 15964 14 0 0 25 0 1 0 1797399703 7933952 1841 4294967295 134512640 135094434 3221224432 3221223104 134555849 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 1937 1841 145 145 0 1792 0 [pid=31382] vsize: 7748 Current children cumulated CPU time (s) 159.78 Current children cumulated vsize (Kb) 9872 [startup+170.019 s] Raw data (loadavg): 1.01 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 1855 0 0 0 16964 14 0 0 25 0 1 0 1797399703 7933952 1841 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 1937 1841 145 145 0 1792 0 [pid=31382] vsize: 7748 Current children cumulated CPU time (s) 169.78 Current children cumulated vsize (Kb) 9872 [startup+180.02 s] Raw data (loadavg): 1.01 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 1855 0 0 0 17965 14 0 0 25 0 1 0 1797399703 7933952 1841 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 1937 1841 145 145 0 1792 0 [pid=31382] vsize: 7748 Current children cumulated CPU time (s) 179.79 Current children cumulated vsize (Kb) 9872 [startup+190.021 s] Raw data (loadavg): 1.01 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 1855 0 0 0 18965 14 0 0 25 0 1 0 1797399703 7933952 1841 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 1937 1841 145 145 0 1792 0 [pid=31382] vsize: 7748 Current children cumulated CPU time (s) 189.79 Current children cumulated vsize (Kb) 9872 [startup+200.024 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 1855 0 0 0 19965 14 0 0 25 0 1 0 1797399703 7933952 1841 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 1937 1841 145 145 0 1792 0 [pid=31382] vsize: 7748 Current children cumulated CPU time (s) 199.79 Current children cumulated vsize (Kb) 9872 [startup+210.025 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 1855 0 0 0 20965 14 0 0 25 0 1 0 1797399703 7933952 1841 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 1937 1841 145 145 0 1792 0 [pid=31382] vsize: 7748 Current children cumulated CPU time (s) 209.79 Current children cumulated vsize (Kb) 9872 [startup+220.027 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 1855 0 0 0 21966 14 0 0 25 0 1 0 1797399703 7933952 1841 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 1937 1841 145 145 0 1792 0 [pid=31382] vsize: 7748 Current children cumulated CPU time (s) 219.8 Current children cumulated vsize (Kb) 9872 [startup+230.027 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 1856 0 0 0 22966 14 0 0 25 0 1 0 1797399703 7933952 1842 4294967295 134512640 135094434 3221224432 3221223120 134554676 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 1937 1842 145 145 0 1792 0 [pid=31382] vsize: 7748 Current children cumulated CPU time (s) 229.8 Current children cumulated vsize (Kb) 9872 [startup+240.028 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 1874 0 0 0 23966 14 0 0 25 0 1 0 1797399703 8065024 1860 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 1969 1860 145 145 0 1824 0 [pid=31382] vsize: 7876 Current children cumulated CPU time (s) 239.8 Current children cumulated vsize (Kb) 10000 [startup+250.029 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 1874 0 0 0 24966 14 0 0 25 0 1 0 1797399703 8065024 1860 4294967295 134512640 135094434 3221224432 3221223088 134557972 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 1969 1860 145 145 0 1824 0 [pid=31382] vsize: 7876 Current children cumulated CPU time (s) 249.8 Current children cumulated vsize (Kb) 10000 [startup+260.03 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 1874 0 0 0 25966 14 0 0 25 0 1 0 1797399703 8065024 1860 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 1969 1860 145 145 0 1824 0 [pid=31382] vsize: 7876 Current children cumulated CPU time (s) 259.8 Current children cumulated vsize (Kb) 10000 [startup+270.031 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 1874 0 0 0 26967 14 0 0 25 0 1 0 1797399703 8065024 1860 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 1969 1860 145 145 0 1824 0 [pid=31382] vsize: 7876 Current children cumulated CPU time (s) 269.81 Current children cumulated vsize (Kb) 10000 [startup+280.032 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 1970 0 0 0 27965 16 0 0 25 0 1 0 1797399703 8454144 1956 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 2064 1956 145 145 0 1919 0 [pid=31382] vsize: 8256 Current children cumulated CPU time (s) 279.81 Current children cumulated vsize (Kb) 10380 [startup+290.033 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 1999 0 0 0 28965 16 0 0 25 0 1 0 1797399703 8572928 1985 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 2093 1985 145 145 0 1948 0 [pid=31382] vsize: 8372 Current children cumulated CPU time (s) 289.81 Current children cumulated vsize (Kb) 10496 [startup+300.034 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 2029 0 0 0 29965 16 0 0 25 0 1 0 1797399703 8699904 2015 4294967295 134512640 135094434 3221224432 3221223024 134557404 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 2124 2015 145 145 0 1979 0 [pid=31382] vsize: 8496 Current children cumulated CPU time (s) 299.81 Current children cumulated vsize (Kb) 10620 [startup+310.035 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 2197 0 0 0 30961 18 0 0 25 0 1 0 1797399703 9375744 2183 4294967295 134512640 135094434 3221224432 3221223104 134556543 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 2289 2183 145 145 0 2144 0 [pid=31382] vsize: 9156 Current children cumulated CPU time (s) 309.79 Current children cumulated vsize (Kb) 11280 [startup+320.036 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 2200 0 0 0 31961 18 0 0 25 0 1 0 1797399703 9388032 2186 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 2292 2186 145 145 0 2147 0 [pid=31382] vsize: 9168 Current children cumulated CPU time (s) 319.79 Current children cumulated vsize (Kb) 11292 [startup+330.037 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 2200 0 0 0 32961 18 0 0 25 0 1 0 1797399703 9388032 2186 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 2292 2186 145 145 0 2147 0 [pid=31382] vsize: 9168 Current children cumulated CPU time (s) 329.79 Current children cumulated vsize (Kb) 11292 [startup+340.037 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 2200 0 0 0 33961 18 0 0 25 0 1 0 1797399703 9388032 2186 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 2292 2186 145 145 0 2147 0 [pid=31382] vsize: 9168 Current children cumulated CPU time (s) 339.79 Current children cumulated vsize (Kb) 11292 [startup+350.039 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 2200 0 0 0 34961 18 0 0 25 0 1 0 1797399703 9388032 2186 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 2292 2186 145 145 0 2147 0 [pid=31382] vsize: 9168 Current children cumulated CPU time (s) 349.79 Current children cumulated vsize (Kb) 11292 [startup+360.04 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 2200 0 0 0 35962 18 0 0 25 0 1 0 1797399703 9388032 2186 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 2292 2186 145 145 0 2147 0 [pid=31382] vsize: 9168 Current children cumulated CPU time (s) 359.8 Current children cumulated vsize (Kb) 11292 [startup+370.042 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 2200 0 0 0 36962 18 0 0 25 0 1 0 1797399703 9388032 2186 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 2292 2186 145 145 0 2147 0 [pid=31382] vsize: 9168 Current children cumulated CPU time (s) 369.8 Current children cumulated vsize (Kb) 11292 [startup+380.043 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 2200 0 0 0 37962 18 0 0 25 0 1 0 1797399703 9388032 2186 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 2292 2186 145 145 0 2147 0 [pid=31382] vsize: 9168 Current children cumulated CPU time (s) 379.8 Current children cumulated vsize (Kb) 11292 [startup+390.042 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 2200 0 0 0 38962 18 0 0 25 0 1 0 1797399703 9388032 2186 4294967295 134512640 135094434 3221224432 3221223104 134556073 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 2292 2186 145 145 0 2147 0 [pid=31382] vsize: 9168 Current children cumulated CPU time (s) 389.8 Current children cumulated vsize (Kb) 11292 [startup+400.044 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 2200 0 0 0 39963 18 0 0 25 0 1 0 1797399703 9388032 2186 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 2292 2186 145 145 0 2147 0 [pid=31382] vsize: 9168 Current children cumulated CPU time (s) 399.81 Current children cumulated vsize (Kb) 11292 [startup+410.045 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 2200 0 0 0 40963 18 0 0 25 0 1 0 1797399703 9388032 2186 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 2292 2186 145 145 0 2147 0 [pid=31382] vsize: 9168 Current children cumulated CPU time (s) 409.81 Current children cumulated vsize (Kb) 11292 [startup+420.046 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 2242 0 0 0 41962 19 0 0 25 0 1 0 1797399703 9564160 2228 4294967295 134512640 135094434 3221224432 3221223088 134557882 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 2335 2228 145 145 0 2190 0 [pid=31382] vsize: 9340 Current children cumulated CPU time (s) 419.81 Current children cumulated vsize (Kb) 11464 [startup+430.047 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 2253 0 0 0 42962 19 0 0 25 0 1 0 1797399703 9605120 2239 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 2345 2239 145 145 0 2200 0 [pid=31382] vsize: 9380 Current children cumulated CPU time (s) 429.81 Current children cumulated vsize (Kb) 11504 [startup+440.047 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 2345 0 0 0 43962 19 0 0 25 0 1 0 1797399703 9998336 2331 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 2441 2331 145 145 0 2296 0 [pid=31382] vsize: 9764 Current children cumulated CPU time (s) 439.81 Current children cumulated vsize (Kb) 11888 [startup+450.048 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 2356 0 0 0 44962 19 0 0 25 0 1 0 1797399703 10039296 2342 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 2451 2342 145 145 0 2306 0 [pid=31382] vsize: 9804 Current children cumulated CPU time (s) 449.81 Current children cumulated vsize (Kb) 11928 [startup+460.049 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 2362 0 0 0 45962 19 0 0 25 0 1 0 1797399703 10072064 2348 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 2459 2348 145 145 0 2314 0 [pid=31382] vsize: 9836 Current children cumulated CPU time (s) 459.81 Current children cumulated vsize (Kb) 11960 [startup+470.05 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 2362 0 0 0 46962 19 0 0 25 0 1 0 1797399703 10072064 2348 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 2459 2348 145 145 0 2314 0 [pid=31382] vsize: 9836 Current children cumulated CPU time (s) 469.81 Current children cumulated vsize (Kb) 11960 [startup+480.051 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 2362 0 0 0 47963 19 0 0 25 0 1 0 1797399703 10072064 2348 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 2459 2348 145 145 0 2314 0 [pid=31382] vsize: 9836 Current children cumulated CPU time (s) 479.82 Current children cumulated vsize (Kb) 11960 [startup+490.052 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 2454 0 0 0 48961 20 0 0 25 0 1 0 1797399703 10448896 2440 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 2551 2440 145 145 0 2406 0 [pid=31382] vsize: 10204 Current children cumulated CPU time (s) 489.81 Current children cumulated vsize (Kb) 12328 [startup+500.053 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 2602 0 0 0 49958 21 0 0 25 0 1 0 1797399703 11046912 2588 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 2697 2588 145 145 0 2552 0 [pid=31382] vsize: 10788 Current children cumulated CPU time (s) 499.79 Current children cumulated vsize (Kb) 12912 [startup+510.053 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 2611 0 0 0 50958 21 0 0 25 0 1 0 1797399703 11083776 2597 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 2706 2597 145 145 0 2561 0 [pid=31382] vsize: 10824 Current children cumulated CPU time (s) 509.79 Current children cumulated vsize (Kb) 12948 [startup+520.055 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 2670 0 0 0 51958 21 0 0 25 0 1 0 1797399703 11325440 2656 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 2765 2656 145 145 0 2620 0 [pid=31382] vsize: 11060 Current children cumulated CPU time (s) 519.79 Current children cumulated vsize (Kb) 13184 [startup+530.056 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 2690 0 0 0 52958 21 0 0 25 0 1 0 1797399703 11423744 2676 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 2789 2676 145 145 0 2644 0 [pid=31382] vsize: 11156 Current children cumulated CPU time (s) 529.79 Current children cumulated vsize (Kb) 13280 [startup+540.057 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 2695 0 0 0 53958 22 0 0 25 0 1 0 1797399703 11440128 2681 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 2793 2681 145 145 0 2648 0 [pid=31382] vsize: 11172 Current children cumulated CPU time (s) 539.8 Current children cumulated vsize (Kb) 13296 [startup+550.059 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 2712 0 0 0 54959 22 0 0 25 0 1 0 1797399703 11513856 2698 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 2811 2698 145 145 0 2666 0 [pid=31382] vsize: 11244 Current children cumulated CPU time (s) 549.81 Current children cumulated vsize (Kb) 13368 [startup+560.059 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 2757 0 0 0 55958 22 0 0 25 0 1 0 1797399703 11694080 2743 4294967295 134512640 135094434 3221224432 3221223024 134785278 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 2855 2743 145 145 0 2710 0 [pid=31382] vsize: 11420 Current children cumulated CPU time (s) 559.8 Current children cumulated vsize (Kb) 13544 [startup+570.06 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 2777 0 0 0 56958 22 0 0 25 0 1 0 1797399703 11776000 2763 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 2875 2763 145 145 0 2730 0 [pid=31382] vsize: 11500 Current children cumulated CPU time (s) 569.8 Current children cumulated vsize (Kb) 13624 [startup+580.062 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 2786 0 0 0 57958 22 0 0 25 0 1 0 1797399703 11812864 2772 4294967295 134512640 135094434 3221224432 3221222896 134781511 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 2884 2772 145 145 0 2739 0 [pid=31382] vsize: 11536 Current children cumulated CPU time (s) 579.8 Current children cumulated vsize (Kb) 13660 [startup+590.062 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 2789 0 0 0 58958 22 0 0 25 0 1 0 1797399703 11829248 2775 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31382/statm): 2888 2775 145 145 0 2743 0 [pid=31382] vsize: 11552 Current children cumulated CPU time (s) 589.8 Current children cumulated vsize (Kb) 13676 [startup+600.064 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 2806 0 0 0 59957 23 0 0 25 0 1 0 1797399703 11890688 2792 4294967295 134512640 135094434 3221224432 3221223088 134558169 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 2903 2792 145 145 0 2758 0 [pid=31382] vsize: 11612 Current children cumulated CPU time (s) 599.8 Current children cumulated vsize (Kb) 13736 [startup+610.064 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 2814 0 0 0 60957 23 0 0 25 0 1 0 1797399703 11919360 2800 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 2910 2800 145 145 0 2765 0 [pid=31382] vsize: 11640 Current children cumulated CPU time (s) 609.8 Current children cumulated vsize (Kb) 13764 [startup+620.064 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 2822 0 0 0 61957 23 0 0 25 0 1 0 1797399703 11952128 2808 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 2918 2808 145 145 0 2773 0 [pid=31382] vsize: 11672 Current children cumulated CPU time (s) 619.8 Current children cumulated vsize (Kb) 13796 [startup+630.065 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 2860 0 0 0 62956 23 0 0 25 0 1 0 1797399703 12111872 2846 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 2957 2846 145 145 0 2812 0 [pid=31382] vsize: 11828 Current children cumulated CPU time (s) 629.79 Current children cumulated vsize (Kb) 13952 [startup+640.066 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 2867 0 0 0 63956 23 0 0 25 0 1 0 1797399703 12140544 2853 4294967295 134512640 135094434 3221224432 3221223024 134557251 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 2964 2853 145 145 0 2819 0 [pid=31382] vsize: 11856 Current children cumulated CPU time (s) 639.79 Current children cumulated vsize (Kb) 13980 [startup+650.067 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 2901 0 0 0 64956 24 0 0 25 0 1 0 1797399703 12296192 2887 4294967295 134512640 135094434 3221224432 3221222336 134562815 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3002 2887 145 145 0 2857 0 [pid=31382] vsize: 12008 Current children cumulated CPU time (s) 649.8 Current children cumulated vsize (Kb) 14132 [startup+660.068 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 2908 0 0 0 65956 24 0 0 25 0 1 0 1797399703 12328960 2894 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3010 2894 145 145 0 2865 0 [pid=31382] vsize: 12040 Current children cumulated CPU time (s) 659.8 Current children cumulated vsize (Kb) 14164 [startup+670.068 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 2913 0 0 0 66956 24 0 0 25 0 1 0 1797399703 12345344 2899 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3014 2899 145 145 0 2869 0 [pid=31382] vsize: 12056 Current children cumulated CPU time (s) 669.8 Current children cumulated vsize (Kb) 14180 [startup+680.069 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 2923 0 0 0 67957 24 0 0 25 0 1 0 1797399703 12394496 2909 4294967295 134512640 135094434 3221224432 3221223104 134556526 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3026 2909 145 145 0 2881 0 [pid=31382] vsize: 12104 Current children cumulated CPU time (s) 679.81 Current children cumulated vsize (Kb) 14228 [startup+690.07 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 2945 0 0 0 68957 24 0 0 25 0 1 0 1797399703 12509184 2931 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3054 2931 145 145 0 2909 0 [pid=31382] vsize: 12216 Current children cumulated CPU time (s) 689.81 Current children cumulated vsize (Kb) 14340 [startup+700.072 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 2998 0 0 0 69956 24 0 0 25 0 1 0 1797399703 12734464 2984 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3109 2984 145 145 0 2964 0 [pid=31382] vsize: 12436 Current children cumulated CPU time (s) 699.8 Current children cumulated vsize (Kb) 14560 [startup+710.073 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 2998 0 0 0 70956 24 0 0 25 0 1 0 1797399703 12734464 2984 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3109 2984 145 145 0 2964 0 [pid=31382] vsize: 12436 Current children cumulated CPU time (s) 709.8 Current children cumulated vsize (Kb) 14560 [startup+720.073 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3009 0 0 0 71956 24 0 0 25 0 1 0 1797399703 12783616 2995 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3121 2995 145 145 0 2976 0 [pid=31382] vsize: 12484 Current children cumulated CPU time (s) 719.8 Current children cumulated vsize (Kb) 14608 [startup+730.074 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3009 0 0 0 72956 24 0 0 25 0 1 0 1797399703 12783616 2995 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3121 2995 145 145 0 2976 0 [pid=31382] vsize: 12484 Current children cumulated CPU time (s) 729.8 Current children cumulated vsize (Kb) 14608 [startup+740.074 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3038 0 0 0 73956 25 0 0 25 0 1 0 1797399703 12906496 3024 4294967295 134512640 135094434 3221224432 3221223088 134557818 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3151 3024 145 145 0 3006 0 [pid=31382] vsize: 12604 Current children cumulated CPU time (s) 739.81 Current children cumulated vsize (Kb) 14728 [startup+750.076 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3042 0 0 0 74956 25 0 0 25 0 1 0 1797399703 12922880 3028 4294967295 134512640 135094434 3221224432 3221223056 134557681 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3155 3028 145 145 0 3010 0 [pid=31382] vsize: 12620 Current children cumulated CPU time (s) 749.81 Current children cumulated vsize (Kb) 14744 [startup+760.077 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3054 0 0 0 75956 25 0 0 25 0 1 0 1797399703 12980224 3040 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3169 3040 145 145 0 3024 0 [pid=31382] vsize: 12676 Current children cumulated CPU time (s) 759.81 Current children cumulated vsize (Kb) 14800 [startup+770.077 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3063 0 0 0 76956 25 0 0 25 0 1 0 1797399703 13012992 3049 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3177 3049 145 145 0 3032 0 [pid=31382] vsize: 12708 Current children cumulated CPU time (s) 769.81 Current children cumulated vsize (Kb) 14832 [startup+780.077 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3063 0 0 0 77956 25 0 0 25 0 1 0 1797399703 13012992 3049 4294967295 134512640 135094434 3221224432 3221222992 134550343 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3177 3049 145 145 0 3032 0 [pid=31382] vsize: 12708 Current children cumulated CPU time (s) 779.81 Current children cumulated vsize (Kb) 14832 [startup+790.078 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3063 0 0 0 78956 25 0 0 25 0 1 0 1797399703 13012992 3049 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3177 3049 145 145 0 3032 0 [pid=31382] vsize: 12708 Current children cumulated CPU time (s) 789.81 Current children cumulated vsize (Kb) 14832 [startup+800.079 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3063 0 0 0 79957 25 0 0 25 0 1 0 1797399703 13012992 3049 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3177 3049 145 145 0 3032 0 [pid=31382] vsize: 12708 Current children cumulated CPU time (s) 799.82 Current children cumulated vsize (Kb) 14832 [startup+810.08 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3063 0 0 0 80957 25 0 0 25 0 1 0 1797399703 13012992 3049 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3177 3049 145 145 0 3032 0 [pid=31382] vsize: 12708 Current children cumulated CPU time (s) 809.82 Current children cumulated vsize (Kb) 14832 [startup+820.081 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3063 0 0 0 81957 25 0 0 25 0 1 0 1797399703 13012992 3049 4294967295 134512640 135094434 3221224432 3221223024 134551780 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3177 3049 145 145 0 3032 0 [pid=31382] vsize: 12708 Current children cumulated CPU time (s) 819.82 Current children cumulated vsize (Kb) 14832 [startup+830.082 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3063 0 0 0 82957 25 0 0 25 0 1 0 1797399703 13012992 3049 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3177 3049 145 145 0 3032 0 [pid=31382] vsize: 12708 Current children cumulated CPU time (s) 829.82 Current children cumulated vsize (Kb) 14832 [startup+840.082 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3063 0 0 0 83957 25 0 0 25 0 1 0 1797399703 13012992 3049 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3177 3049 145 145 0 3032 0 [pid=31382] vsize: 12708 Current children cumulated CPU time (s) 839.82 Current children cumulated vsize (Kb) 14832 [startup+850.083 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3063 0 0 0 84958 25 0 0 25 0 1 0 1797399703 13012992 3049 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3177 3049 145 145 0 3032 0 [pid=31382] vsize: 12708 Current children cumulated CPU time (s) 849.83 Current children cumulated vsize (Kb) 14832 [startup+860.084 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3063 0 0 0 85958 25 0 0 25 0 1 0 1797399703 13012992 3049 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3177 3049 145 145 0 3032 0 [pid=31382] vsize: 12708 Current children cumulated CPU time (s) 859.83 Current children cumulated vsize (Kb) 14832 [startup+870.085 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3063 0 0 0 86958 25 0 0 25 0 1 0 1797399703 13012992 3049 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3177 3049 145 145 0 3032 0 [pid=31382] vsize: 12708 Current children cumulated CPU time (s) 869.83 Current children cumulated vsize (Kb) 14832 [startup+880.086 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3063 0 0 0 87958 25 0 0 25 0 1 0 1797399703 13012992 3049 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3177 3049 145 145 0 3032 0 [pid=31382] vsize: 12708 Current children cumulated CPU time (s) 879.83 Current children cumulated vsize (Kb) 14832 [startup+890.086 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3063 0 0 0 88958 25 0 0 25 0 1 0 1797399703 13012992 3049 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3177 3049 145 145 0 3032 0 [pid=31382] vsize: 12708 Current children cumulated CPU time (s) 889.83 Current children cumulated vsize (Kb) 14832 [startup+900.087 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3063 0 0 0 89959 25 0 0 25 0 1 0 1797399703 13012992 3049 4294967295 134512640 135094434 3221224432 3221223024 134551876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3177 3049 145 145 0 3032 0 [pid=31382] vsize: 12708 Current children cumulated CPU time (s) 899.84 Current children cumulated vsize (Kb) 14832 [startup+910.088 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3063 0 0 0 90959 25 0 0 25 0 1 0 1797399703 13012992 3049 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3177 3049 145 145 0 3032 0 [pid=31382] vsize: 12708 Current children cumulated CPU time (s) 909.84 Current children cumulated vsize (Kb) 14832 [startup+920.088 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3063 0 0 0 91959 25 0 0 25 0 1 0 1797399703 13012992 3049 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3177 3049 145 145 0 3032 0 [pid=31382] vsize: 12708 Current children cumulated CPU time (s) 919.84 Current children cumulated vsize (Kb) 14832 [startup+930.089 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3063 0 0 0 92959 25 0 0 25 0 1 0 1797399703 13012992 3049 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3177 3049 145 145 0 3032 0 [pid=31382] vsize: 12708 Current children cumulated CPU time (s) 929.84 Current children cumulated vsize (Kb) 14832 [startup+940.09 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3065 0 0 0 93959 25 0 0 25 0 1 0 1797399703 13029376 3051 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3181 3051 145 145 0 3036 0 [pid=31382] vsize: 12724 Current children cumulated CPU time (s) 939.84 Current children cumulated vsize (Kb) 14848 [startup+950.09 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3065 0 0 0 94960 25 0 0 25 0 1 0 1797399703 13029376 3051 4294967295 134512640 135094434 3221224432 3221223104 134556552 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3181 3051 145 145 0 3036 0 [pid=31382] vsize: 12724 Current children cumulated CPU time (s) 949.85 Current children cumulated vsize (Kb) 14848 [startup+960.091 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3065 0 0 0 95960 25 0 0 25 0 1 0 1797399703 13029376 3051 4294967295 134512640 135094434 3221224432 3221223088 134558284 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3181 3051 145 145 0 3036 0 [pid=31382] vsize: 12724 Current children cumulated CPU time (s) 959.85 Current children cumulated vsize (Kb) 14848 [startup+970.092 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3065 0 0 0 96960 25 0 0 25 0 1 0 1797399703 13029376 3051 4294967295 134512640 135094434 3221224432 3221223076 134558040 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3181 3051 145 145 0 3036 0 [pid=31382] vsize: 12724 Current children cumulated CPU time (s) 969.85 Current children cumulated vsize (Kb) 14848 [startup+980.093 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3065 0 0 0 97960 25 0 0 25 0 1 0 1797399703 13029376 3051 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3181 3051 145 145 0 3036 0 [pid=31382] vsize: 12724 Current children cumulated CPU time (s) 979.85 Current children cumulated vsize (Kb) 14848 [startup+990.094 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3065 0 0 0 98961 25 0 0 25 0 1 0 1797399703 13029376 3051 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3181 3051 145 145 0 3036 0 [pid=31382] vsize: 12724 Current children cumulated CPU time (s) 989.86 Current children cumulated vsize (Kb) 14848 [startup+1000.1 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3065 0 0 0 99961 25 0 0 25 0 1 0 1797399703 13029376 3051 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3181 3051 145 145 0 3036 0 [pid=31382] vsize: 12724 Current children cumulated CPU time (s) 999.86 Current children cumulated vsize (Kb) 14848 [startup+1010.1 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3065 0 0 0 100961 25 0 0 25 0 1 0 1797399703 13029376 3051 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3181 3051 145 145 0 3036 0 [pid=31382] vsize: 12724 Current children cumulated CPU time (s) 1009.86 Current children cumulated vsize (Kb) 14848 [startup+1020.1 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3065 0 0 0 101961 25 0 0 25 0 1 0 1797399703 13029376 3051 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3181 3051 145 145 0 3036 0 [pid=31382] vsize: 12724 Current children cumulated CPU time (s) 1019.86 Current children cumulated vsize (Kb) 14848 [startup+1030.1 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3065 0 0 0 102961 25 0 0 25 0 1 0 1797399703 13029376 3051 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3181 3051 145 145 0 3036 0 [pid=31382] vsize: 12724 Current children cumulated CPU time (s) 1029.86 Current children cumulated vsize (Kb) 14848 [startup+1040.1 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3065 0 0 0 103961 25 0 0 25 0 1 0 1797399703 13029376 3051 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3181 3051 145 145 0 3036 0 [pid=31382] vsize: 12724 Current children cumulated CPU time (s) 1039.86 Current children cumulated vsize (Kb) 14848 [startup+1050.1 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3065 0 0 0 104962 25 0 0 25 0 1 0 1797399703 13029376 3051 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3181 3051 145 145 0 3036 0 [pid=31382] vsize: 12724 Current children cumulated CPU time (s) 1049.87 Current children cumulated vsize (Kb) 14848 [startup+1060.1 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3065 0 0 0 105962 25 0 0 25 0 1 0 1797399703 13029376 3051 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3181 3051 145 145 0 3036 0 [pid=31382] vsize: 12724 Current children cumulated CPU time (s) 1059.87 Current children cumulated vsize (Kb) 14848 [startup+1070.1 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3065 0 0 0 106962 25 0 0 25 0 1 0 1797399703 13029376 3051 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3181 3051 145 145 0 3036 0 [pid=31382] vsize: 12724 Current children cumulated CPU time (s) 1069.87 Current children cumulated vsize (Kb) 14848 [startup+1080.1 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3065 0 0 0 107963 25 0 0 25 0 1 0 1797399703 13029376 3051 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3181 3051 145 145 0 3036 0 [pid=31382] vsize: 12724 Current children cumulated CPU time (s) 1079.88 Current children cumulated vsize (Kb) 14848 [startup+1090.1 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3065 0 0 0 108963 25 0 0 25 0 1 0 1797399703 13029376 3051 4294967295 134512640 135094434 3221224432 3221223120 134554687 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3181 3051 145 145 0 3036 0 [pid=31382] vsize: 12724 Current children cumulated CPU time (s) 1089.88 Current children cumulated vsize (Kb) 14848 [startup+1100.1 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3065 0 0 0 109963 25 0 0 25 0 1 0 1797399703 13029376 3051 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3181 3051 145 145 0 3036 0 [pid=31382] vsize: 12724 Current children cumulated CPU time (s) 1099.88 Current children cumulated vsize (Kb) 14848 [startup+1110.1 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3065 0 0 0 110963 25 0 0 25 0 1 0 1797399703 13029376 3051 4294967295 134512640 135094434 3221224432 3221223024 134785275 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3181 3051 145 145 0 3036 0 [pid=31382] vsize: 12724 Current children cumulated CPU time (s) 1109.88 Current children cumulated vsize (Kb) 14848 [startup+1120.11 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3065 0 0 0 111964 25 0 0 25 0 1 0 1797399703 13029376 3051 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3181 3051 145 145 0 3036 0 [pid=31382] vsize: 12724 Current children cumulated CPU time (s) 1119.89 Current children cumulated vsize (Kb) 14848 [startup+1130.11 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3065 0 0 0 112964 25 0 0 25 0 1 0 1797399703 13029376 3051 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3181 3051 145 145 0 3036 0 [pid=31382] vsize: 12724 Current children cumulated CPU time (s) 1129.89 Current children cumulated vsize (Kb) 14848 [startup+1140.11 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3122 0 0 0 113963 26 0 0 25 0 1 0 1797399703 13262848 3108 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3238 3108 145 145 0 3093 0 [pid=31382] vsize: 12952 Current children cumulated CPU time (s) 1139.89 Current children cumulated vsize (Kb) 15076 [startup+1150.11 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3124 0 0 0 114963 26 0 0 25 0 1 0 1797399703 13271040 3110 4294967295 134512640 135094434 3221224432 3221223088 134557896 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3240 3110 145 145 0 3095 0 [pid=31382] vsize: 12960 Current children cumulated CPU time (s) 1149.89 Current children cumulated vsize (Kb) 15084 [startup+1160.11 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3132 0 0 0 115963 26 0 0 25 0 1 0 1797399703 13303808 3118 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3248 3118 145 145 0 3103 0 [pid=31382] vsize: 12992 Current children cumulated CPU time (s) 1159.89 Current children cumulated vsize (Kb) 15116 [startup+1170.11 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3142 0 0 0 116963 26 0 0 25 0 1 0 1797399703 13369344 3128 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3264 3128 145 145 0 3119 0 [pid=31382] vsize: 13056 Current children cumulated CPU time (s) 1169.89 Current children cumulated vsize (Kb) 15180 [startup+1180.11 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3220 0 0 0 117962 27 0 0 25 0 1 0 1797399703 13680640 3206 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3340 3206 145 145 0 3195 0 [pid=31382] vsize: 13360 Current children cumulated CPU time (s) 1179.89 Current children cumulated vsize (Kb) 15484 [startup+1190.11 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3223 0 0 0 118962 27 0 0 25 0 1 0 1797399703 13713408 3209 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3348 3209 145 145 0 3203 0 [pid=31382] vsize: 13392 Current children cumulated CPU time (s) 1189.89 Current children cumulated vsize (Kb) 15516 [startup+1200.11 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3227 0 0 0 119962 27 0 0 25 0 1 0 1797399703 13717504 3213 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3349 3213 145 145 0 3204 0 [pid=31382] vsize: 13396 Current children cumulated CPU time (s) 1199.89 Current children cumulated vsize (Kb) 15520 [startup+1210.11 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3227 0 0 0 120963 27 0 0 25 0 1 0 1797399703 13717504 3213 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3349 3213 145 145 0 3204 0 [pid=31382] vsize: 13396 Current children cumulated CPU time (s) 1209.9 Current children cumulated vsize (Kb) 15520 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.11 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 31382 Raw data (/proc/31378/stat): 31378 (minisat+_script) S 31377 31378 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797399698 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31378/statm): 531 226 485 147 0 384 0 [pid=31378] vsize: 2124 Raw data (/proc/31382/stat): 31382 (minisat+_64-bit) R 31378 31378 31778 0 -1 0 3227 0 0 0 120963 27 0 0 25 0 1 0 1797399703 13717504 3213 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31382/statm): 3349 3213 145 145 0 3204 0 [pid=31382] vsize: 13396 Current children cumulated CPU time (s) 1209.9 Current children cumulated vsize (Kb) 15520 Sending SIGTERM to -31378 Sleeping 2 seconds One traced child (pid=31378) ended because it received signal 15 (SIGTERM) One traced child (pid=31382) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.12 CPU time (s): 1209.91 CPU user time (s): 1209.63 CPU system time (s): 0.278957 CPU usage (%): 99.9825 Max. virtual memory (cumulated for all children) (Kb): 15520
ERROR: no interpretation found !