Name | mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-markshare2.opb |
MD5SUM | 3b5121187baf09367bd50bdc4d869d21 |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 5632 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 140 |
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 | 7340025 |
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 | 7340025 |
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.36 |
Number of variables | 200 |
Total number of constraints | 67 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 60 |
Number of constraints which are nor clauses,nor cardinality constraints | 7 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 80 |
LAUNCH ON wulflinc27 THE 2005-09-20 03:42:50 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3301 boxname=wulflinc27 idbench=957 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 3b5121187baf09367bd50bdc4d869d21 /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-markshare2.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-markshare2.opb IDLAUNCH: 3301 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.169 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.169 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: 921316 kB Buffers: 16344 kB Cached: 67624 kB SwapCached: 692 kB Active: 24108 kB Inactive: 62424 kB HighTotal: 131008 kB HighFree: 61096 kB LowTotal: 903652 kB LowFree: 860220 kB SwapTotal: 2097892 kB SwapFree: 2096628 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5728 kB Slab: 20996 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-20 04:03:01 (client local time) WITH STATUS 10 IN 1209.87 SECONDS stats: 3301 7 1209.87 10
c Parsing PB file... c Converting 14 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ####### c -- Clauses(.)/Splits(s): (none) c ---[ 12]---> Adder-cost: 354 maxlim: 431615 bits: 20/19 c ---[ 10]---> Adder-cost: 380 maxlim: 461183 bits: 20/19 c ---[ 8]---> Adder-cost: 350 maxlim: 445183 bits: 20/19 c ---[ 6]---> Adder-cost: 340 maxlim: 477951 bits: 20/19 c ---[ 4]---> Adder-cost: 390 maxlim: 451839 bits: 20/19 c ---[ 2]---> Adder-cost: 358 maxlim: 468735 bits: 20/19 c ---[ 0]---> Adder-cost: 374 maxlim: 444543 bits: 20/19 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 17222 61228 | 5740 0 0 nan | 0.000 % | c | 100 | 17222 61228 | 6314 100 905 9.1 | 9.969 % | c | 253 | 17214 61202 | 6945 252 2033 8.1 | 10.003 % | c | 478 | 17206 61176 | 7639 476 4722 9.9 | 10.038 % | c ============================================================================== c [1mFound solution: 866304[0m c ---[ 0]---> Sorter-cost: 1068 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 | 536 | 19853 67360 | 6617 534 5740 10.7 | 10.038 % | c ============================================================================== c [1mFound solution: 828672[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 | 632 | 19863 67400 | 6621 629 13956 22.2 | 10.038 % | c | 733 | 19863 67400 | 7283 730 20234 27.7 | 7.644 % | c | 884 | 19855 67374 | 8011 879 45616 51.9 | 7.696 % | c | 1110 | 19847 67348 | 8812 1105 70591 63.9 | 7.696 % | c | 1447 | 19839 67322 | 9693 1441 95879 66.5 | 7.723 % | c ============================================================================== c [1mFound solution: 702720[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 | 1945 | 19842 67325 | 6614 1938 159401 82.3 | 7.723 % | c | 2046 | 19842 67325 | 7275 2039 167910 82.3 | 7.761 % | c | 2197 | 19842 67325 | 8002 2190 179220 81.8 | 7.761 % | c | 2423 | 19842 67325 | 8803 2416 196028 81.1 | 7.761 % | c | 2761 | 19842 67325 | 9683 2754 236792 86.0 | 7.761 % | c | 3268 | 19842 67325 | 10651 3261 287766 88.2 | 7.761 % | c ============================================================================== c [1mFound solution: 676352[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 | 3715 | 19858 67370 | 6619 3708 318920 86.0 | 7.761 % | c | 3815 | 19858 67370 | 7280 3808 328892 86.4 | 7.766 % | c | 3965 | 19858 67370 | 8008 3958 346566 87.6 | 7.766 % | c | 4190 | 19858 67370 | 8809 4183 366380 87.6 | 7.766 % | c | 4528 | 19852 67357 | 9690 4520 400494 88.6 | 7.819 % | c | 5034 | 19844 67331 | 10659 5025 444892 88.5 | 7.845 % | c | 5794 | 19836 67305 | 11725 5784 509124 88.0 | 7.871 % | c | 6934 | 19828 67279 | 12898 6923 580155 83.8 | 7.897 % | c ============================================================================== c [1mFound solution: 674304[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 | 7359 | 19838 67302 | 6612 7348 621804 84.6 | 7.897 % | c | 7463 | 19838 67302 | 7273 3778 243653 64.5 | 7.913 % | c | 7614 | 19838 67302 | 8000 3929 255506 65.0 | 7.913 % | c ============================================================================== c [1mFound solution: 654336[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 | 7790 | 19849 67335 | 6616 4105 268736 65.5 | 7.913 % | c ============================================================================== c [1mFound solution: 645120[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 | 7856 | 19857 67359 | 6619 4171 271081 65.0 | 7.913 % | c | 7958 | 19857 67359 | 7280 4273 278513 65.2 | 7.938 % | c ============================================================================== c [1mFound solution: 465408[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 | 8075 | 19869 67387 | 6623 4390 284865 64.9 | 7.938 % | c | 8175 | 19869 67387 | 7285 4490 290752 64.8 | 7.949 % | c | 8326 | 19869 67387 | 8013 4641 302249 65.1 | 7.949 % | c | 8551 | 19869 67387 | 8815 4866 312895 64.3 | 7.949 % | c | 8888 | 19869 67387 | 9696 5203 337269 64.8 | 7.949 % | c | 9394 | 19869 67387 | 10666 5709 372234 65.2 | 7.949 % | c | 10153 | 19869 67387 | 11733 6468 427615 66.1 | 7.949 % | c | 11294 | 19869 67387 | 12906 7609 506572 66.6 | 7.949 % | c | 13003 | 19863 67369 | 14196 9317 680687 73.1 | 7.975 % | c | 15565 | 19838 67290 | 15616 11876 979173 82.4 | 8.079 % | c | 19410 | 19838 67290 | 17178 15721 1427200 90.8 | 8.079 % | c ============================================================================== c [1mFound solution: 426240[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 | 24555 | 19802 67164 | 6600 11781 991951 84.2 | 8.079 % | c | 24656 | 19802 67164 | 7260 5992 340445 56.8 | 8.251 % | c | 24806 | 19802 67164 | 7986 6142 346020 56.3 | 8.251 % | c | 25031 | 19802 67164 | 8784 6367 351779 55.3 | 8.251 % | c | 25370 | 19802 67164 | 9663 6706 376621 56.2 | 8.251 % | c | 25878 | 19802 67164 | 10629 7214 412120 57.1 | 8.251 % | c | 26639 | 19802 67164 | 11692 7975 454198 57.0 | 8.251 % | c | 27779 | 19802 67164 | 12861 9115 506655 55.6 | 8.251 % | c | 29487 | 19802 67164 | 14147 10823 597522 55.2 | 8.251 % | c | 32049 | 19802 67164 | 15562 13385 746703 55.8 | 8.251 % | c | 35893 | 19802 67164 | 17118 9134 445739 48.8 | 8.251 % | c | 41660 | 19802 67164 | 18830 14901 900002 60.4 | 8.251 % | c | 50309 | 19802 67164 | 20713 13630 900207 66.0 | 8.251 % | c | 63285 | 19802 67164 | 22784 15643 876282 56.0 | 8.251 % | c | 82746 | 19802 67164 | 25063 23100 1569191 67.9 | 8.251 % | c ============================================================================== c [1mFound solution: 420352[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 | 110809 | 19810 67183 | 6603 24998 2030699 81.2 | 8.251 % | c | 110909 | 19810 67183 | 7263 6350 368699 58.1 | 8.269 % | c | 111061 | 19810 67183 | 7989 6502 374493 57.6 | 8.269 % | c | 111288 | 19810 67183 | 8788 6729 385690 57.3 | 8.269 % | c | 111626 | 19810 67183 | 9667 7067 413477 58.5 | 8.269 % | c | 112132 | 19810 67183 | 10634 7573 438726 57.9 | 8.269 % | c | 112891 | 19810 67183 | 11697 8332 475591 57.1 | 8.269 % | c | 114031 | 19810 67183 | 12867 9472 602990 63.7 | 8.269 % | c | 115740 | 19810 67183 | 14154 11181 705503 63.1 | 8.269 % | c ============================================================================== c [1mFound solution: 411392[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 | 118101 | 19822 67210 | 6607 13542 911670 67.3 | 8.269 % | c | 118201 | 19822 67210 | 7267 6871 405686 59.0 | 8.282 % | c | 118351 | 19822 67210 | 7994 7021 414241 59.0 | 8.282 % | c | 118576 | 19822 67210 | 8793 7246 434055 59.9 | 8.282 % | c | 118913 | 19822 67210 | 9673 7583 456334 60.2 | 8.282 % | c | 119419 | 19822 67210 | 10640 8089 483898 59.8 | 8.282 % | c | 120178 | 19822 67210 | 11704 8848 528469 59.7 | 8.282 % | c | 121317 | 19822 67210 | 12875 9987 592730 59.4 | 8.282 % | c | 123025 | 19822 67210 | 14162 11695 721731 61.7 | 8.282 % | c | 125587 | 19822 67210 | 15578 14257 897308 62.9 | 8.282 % | c | 129431 | 19822 67210 | 17136 9873 539594 54.7 | 8.282 % | c | 135198 | 19814 67184 | 18850 15639 1121030 71.7 | 8.308 % | c | 143849 | 19814 67184 | 20735 14328 969560 67.7 | 8.308 % | c ============================================================================== c [1mFound solution: 404480[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 | 151309 | 19816 67186 | 6605 11073 646615 58.4 | 8.308 % | c | 151411 | 19816 67186 | 7265 5639 309058 54.8 | 8.374 % | c | 151561 | 19816 67186 | 7992 5789 311658 53.8 | 8.374 % | c | 151786 | 19816 67186 | 8791 6014 337987 56.2 | 8.374 % | c | 152124 | 19816 67186 | 9670 6352 350939 55.2 | 8.374 % | c ============================================================================== c [1mFound solution: 363264[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 | 152583 | 19829 67218 | 6609 6811 361631 53.1 | 8.374 % | c | 152685 | 19829 67218 | 7269 6913 366844 53.1 | 8.385 % | c | 152836 | 19829 67218 | 7996 7064 390436 55.3 | 8.385 % | c | 153061 | 19829 67218 | 8796 7289 402314 55.2 | 8.385 % | c | 153398 | 19829 67218 | 9676 7626 416355 54.6 | 8.385 % | c | 153907 | 19829 67218 | 10643 8135 436418 53.6 | 8.385 % | c | 154667 | 19829 67218 | 11708 8895 517597 58.2 | 8.385 % | c | 155807 | 19829 67218 | 12879 10035 580468 57.8 | 8.385 % | c | 157517 | 19829 67218 | 14166 11745 642591 54.7 | 8.385 % | c | 160079 | 19829 67218 | 15583 14307 764160 53.4 | 8.385 % | c ============================================================================== c [1mFound solution: 343936[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 | 162554 | 19860 67292 | 6620 8590 324198 37.7 | 8.385 % | c | 162655 | 19860 67292 | 7282 4396 151608 34.5 | 8.372 % | c | 162807 | 19860 67292 | 8010 4548 161742 35.6 | 8.372 % | c | 163033 | 19860 67292 | 8811 4774 168934 35.4 | 8.372 % | c | 163371 | 19860 67292 | 9692 5112 176581 34.5 | 8.372 % | c | 163877 | 19860 67292 | 10661 5618 253166 45.1 | 8.372 % | c | 164636 | 19860 67292 | 11727 6377 301500 47.3 | 8.372 % | c | 165778 | 19860 67292 | 12900 7519 356921 47.5 | 8.372 % | c | 167486 | 19860 67292 | 14190 9227 445248 48.3 | 8.372 % | c | 170048 | 19860 67292 | 15609 11789 602596 51.1 | 8.372 % | c | 173892 | 19860 67292 | 17170 15633 831926 53.2 | 8.372 % | c | 179659 | 19860 67292 | 18887 12423 597867 48.1 | 8.372 % | c | 188308 | 19848 67265 | 20776 11130 791462 71.1 | 8.449 % | c ============================================================================== c [1mFound solution: 260352[0m c ---[ 0]---> Sorter-cost: 5 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 | 188746 | 19854 67281 | 6618 11568 801463 69.3 | 8.449 % | c | 188847 | 19854 67281 | 7279 5885 256847 43.6 | 8.465 % | c | 188997 | 19854 67281 | 8007 6035 266435 44.1 | 8.465 % | c | 189223 | 19854 67281 | 8808 6261 281425 44.9 | 8.465 % | c | 189561 | 19854 67281 | 9689 6599 298712 45.3 | 8.465 % | c | 190067 | 19854 67281 | 10658 7105 319291 44.9 | 8.465 % | c | 190827 | 19854 67281 | 11724 7865 359467 45.7 | 8.465 % | c | 191968 | 19854 67281 | 12896 9006 410789 45.6 | 8.465 % | c | 193677 | 19854 67281 | 14186 10715 531399 49.6 | 8.465 % | c | 196241 | 19854 67281 | 15604 13279 685851 51.6 | 8.465 % | c | 200085 | 19854 67281 | 17165 8898 488070 54.9 | 8.465 % | c | 205852 | 19854 67281 | 18881 14665 711080 48.5 | 8.465 % | c ============================================================================== c [1mFound solution: 80128[0m c ---[ 0]---> Sorter-cost: 3 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 | 206193 | 19806 67113 | 6602 14727 700340 47.6 | 8.465 % | c | 206293 | 19806 67113 | 7262 3782 103785 27.4 | 8.666 % | c | 206444 | 19806 67113 | 7988 3933 104553 26.6 | 8.666 % | c | 206669 | 19806 67113 | 8787 4158 107432 25.8 | 8.666 % | c | 207006 | 19806 67113 | 9665 4495 116514 25.9 | 8.666 % | c | 207513 | 19806 67113 | 10632 5002 128589 25.7 | 8.666 % | c ============================================================================== c [1mFound solution: 64896[0m c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 207893 | 19615 66613 | 6538 5362 135046 25.2 | 8.666 % | c | 207995 | 19615 66613 | 7191 5464 137131 25.1 | 10.089 % | c | 208146 | 19615 66613 | 7910 5615 139840 24.9 | 10.089 % | c | 208371 | 19615 66613 | 8702 5840 147321 25.2 | 10.089 % | c | 208708 | 19615 66613 | 9572 6177 155749 25.2 | 10.089 % | c | 209215 | 19615 66613 | 10529 6684 179508 26.9 | 10.089 % | c | 209976 | 19615 66613 | 11582 7445 201615 27.1 | 10.089 % | c | 211115 | 19615 66613 | 12740 8584 243072 28.3 | 10.089 % | c | 212823 | 19615 66613 | 14014 10292 303964 29.5 | 10.089 % | c | 215385 | 19615 66613 | 15416 12854 404034 31.4 | 10.089 % | c | 219229 | 19615 66613 | 16957 8598 318726 37.1 | 10.089 % | c ============================================================================== c [1mFound solution: 63616[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 222041 | 19622 66634 | 6540 11410 477534 41.9 | 10.089 % | c | 222143 | 19622 66634 | 7194 5807 236093 40.7 | 10.102 % | c | 222293 | 19622 66634 | 7913 5957 236962 39.8 | 10.102 % | c | 222518 | 19622 66634 | 8704 6182 240201 38.9 | 10.102 % | c | 222855 | 19622 66634 | 9575 6519 253550 38.9 | 10.102 % | c | 223361 | 19622 66634 | 10532 7025 263589 37.5 | 10.102 % | c | 224121 | 19622 66634 | 11586 7785 284201 36.5 | 10.102 % | c | 225260 | 19622 66634 | 12744 8924 354542 39.7 | 10.102 % | c | 226971 | 19622 66634 | 14019 10635 414350 39.0 | 10.102 % | c | 229533 | 19622 66634 | 15420 13197 533639 40.4 | 10.102 % | c | 233377 | 19607 66589 | 16963 8676 346338 39.9 | 10.179 % | c | 239144 | 19607 66589 | 18659 14443 554456 38.4 | 10.179 % | c | 247793 | 19530 66415 | 20525 13278 517714 39.0 | 10.816 % | c | 260769 | 19429 66185 | 22577 15427 982742 63.7 | 11.633 % | c | 280230 | 19319 65931 | 24835 23197 1024138 44.1 | 12.628 % | c | 309423 | 19319 65931 | 27319 25948 1521579 58.6 | 12.628 % | c ============================================================================== c [1mFound solution: 59008[0m c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 327090 | 19320 65935 | 6440 27848 1354853 48.7 | 12.628 % | c | 327191 | 19320 65935 | 7084 6666 249277 37.4 | 12.732 % | c | 327341 | 19320 65935 | 7792 6816 250694 36.8 | 12.732 % | c | 327566 | 19320 65935 | 8571 7041 259558 36.9 | 12.732 % | c | 327904 | 19320 65935 | 9428 7379 266686 36.1 | 12.732 % | c | 328410 | 19320 65935 | 10371 7885 277400 35.2 | 12.732 % | c | 329171 | 19320 65935 | 11408 8646 299566 34.6 | 12.732 % | c | 330310 | 19320 65935 | 12549 9785 331642 33.9 | 12.732 % | c | 332018 | 19320 65935 | 13804 11493 456254 39.7 | 12.732 % | c | 334582 | 19320 65935 | 15185 14057 533507 38.0 | 12.732 % | c | 338428 | 19320 65935 | 16703 9687 452672 46.7 | 12.732 % | c | 344195 | 19320 65935 | 18374 15454 704774 45.6 | 12.732 % | c | 352844 | 19306 65902 | 20211 14334 779072 54.4 | 12.911 % | c | 365818 | 19288 65862 | 22232 16842 680144 40.4 | 13.038 % | c | 385280 | 19288 65862 | 24455 13318 512736 38.5 | 13.038 % | c | 414473 | 19288 65862 | 26901 17159 819651 47.8 | 13.038 % | c | 458262 | 19259 65797 | 29591 16835 605068 35.9 | 13.242 % | c | 523948 | 19241 65756 | 32550 15348 637855 41.6 | 13.369 % | c | 622474 | 19241 65756 | 35805 17341 946468 54.6 | 13.369 % |
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/27842/stat): 27842 (minisat+_script) R 27841 27842 28974 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1855368781 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/27842/statm): 174 3 169 147 0 27 0 [pid=27842] 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=27843 New process pid=27844 New process pid=27845 execve syscall for /bin/sed executable One traced child (pid=27844) 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=27845) exited with status: 0 One traced child (pid=27843) exited with status: 0 New process pid=27846 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-markshare2.opb [startup+10.0044 s] Raw data (loadavg): 0.93 0.95 0.90 2/57 27846 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 1115 0 0 0 979 6 0 0 25 0 1 0 1855368786 4968448 1102 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27846/statm): 1213 1102 145 145 0 1068 0 [pid=27846] vsize: 4852 Current children cumulated CPU time (s) 9.86 Current children cumulated vsize (Kb) 6976 [startup+20.0053 s] Raw data (loadavg): 0.94 0.96 0.91 2/57 27846 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 1293 0 0 0 1976 7 0 0 25 0 1 0 1855368786 5685248 1280 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 1388 1280 145 145 0 1243 0 [pid=27846] vsize: 5552 Current children cumulated CPU time (s) 19.84 Current children cumulated vsize (Kb) 7676 [startup+30.0071 s] Raw data (loadavg): 0.95 0.96 0.91 2/57 27846 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 1590 0 0 0 2970 10 0 0 25 0 1 0 1855368786 6918144 1577 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 1689 1577 145 145 0 1544 0 [pid=27846] vsize: 6756 Current children cumulated CPU time (s) 29.81 Current children cumulated vsize (Kb) 8880 [startup+40.0079 s] Raw data (loadavg): 0.95 0.96 0.91 2/57 27846 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 1952 0 0 0 3962 13 0 0 25 0 1 0 1855368786 8388608 1939 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 2048 1939 145 145 0 1903 0 [pid=27846] vsize: 8192 Current children cumulated CPU time (s) 39.76 Current children cumulated vsize (Kb) 10316 [startup+50.0087 s] Raw data (loadavg): 0.96 0.96 0.91 2/57 27846 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 2282 0 0 0 4955 16 0 0 25 0 1 0 1855368786 9736192 2269 4294967295 134512640 135094434 3221224432 3221223056 134562068 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 2377 2269 145 145 0 2232 0 [pid=27846] vsize: 9508 Current children cumulated CPU time (s) 49.72 Current children cumulated vsize (Kb) 11632 [startup+60.0095 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 27846 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 2481 0 0 0 5951 18 0 0 25 0 1 0 1855368786 10608640 2468 4294967295 134512640 135094434 3221224432 3221223220 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 2590 2468 145 145 0 2445 0 [pid=27846] vsize: 10360 Current children cumulated CPU time (s) 59.7 Current children cumulated vsize (Kb) 12484 [startup+70.0104 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 27846 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 2481 0 0 0 6951 19 0 0 25 0 1 0 1855368786 10608640 2468 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 2590 2468 145 145 0 2445 0 [pid=27846] vsize: 10360 Current children cumulated CPU time (s) 69.71 Current children cumulated vsize (Kb) 12484 [startup+80.0122 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 27846 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 2481 0 0 0 7950 19 0 0 25 0 1 0 1855368786 10608640 2468 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27846/statm): 2590 2468 145 145 0 2445 0 [pid=27846] vsize: 10360 Current children cumulated CPU time (s) 79.7 Current children cumulated vsize (Kb) 12484 [startup+90.0131 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 27846 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 2481 0 0 0 8950 19 0 0 25 0 1 0 1855368786 10608640 2468 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 2590 2468 145 145 0 2445 0 [pid=27846] vsize: 10360 Current children cumulated CPU time (s) 89.7 Current children cumulated vsize (Kb) 12484 [startup+100.014 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 27846 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 2483 0 0 0 9950 19 0 0 25 0 1 0 1855368786 10608640 2470 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 2590 2470 145 145 0 2445 0 [pid=27846] vsize: 10360 Current children cumulated CPU time (s) 99.7 Current children cumulated vsize (Kb) 12484 [startup+110.016 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 27846 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 2483 0 0 0 10950 20 0 0 25 0 1 0 1855368786 10608640 2470 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 2590 2470 145 145 0 2445 0 [pid=27846] vsize: 10360 Current children cumulated CPU time (s) 109.71 Current children cumulated vsize (Kb) 12484 [startup+120.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27846 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 2485 0 0 0 11951 20 0 0 25 0 1 0 1855368786 10608640 2472 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 2590 2472 145 145 0 2445 0 [pid=27846] vsize: 10360 Current children cumulated CPU time (s) 119.72 Current children cumulated vsize (Kb) 12484 [startup+130.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27846 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 2485 0 0 0 12951 20 0 0 25 0 1 0 1855368786 10608640 2472 4294967295 134512640 135094434 3221224432 3221223104 134555560 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 2590 2472 145 145 0 2445 0 [pid=27846] vsize: 10360 Current children cumulated CPU time (s) 129.72 Current children cumulated vsize (Kb) 12484 [startup+140.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27846 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 2485 0 0 0 13951 20 0 0 25 0 1 0 1855368786 10608640 2472 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 2590 2472 145 145 0 2445 0 [pid=27846] vsize: 10360 Current children cumulated CPU time (s) 139.72 Current children cumulated vsize (Kb) 12484 [startup+150.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27846 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 2552 0 0 0 14950 20 0 0 25 0 1 0 1855368786 10874880 2539 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 2655 2539 145 145 0 2510 0 [pid=27846] vsize: 10620 Current children cumulated CPU time (s) 149.71 Current children cumulated vsize (Kb) 12744 [startup+160.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27846 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 2558 0 0 0 15950 20 0 0 25 0 1 0 1855368786 10899456 2545 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 2661 2545 145 145 0 2516 0 [pid=27846] vsize: 10644 Current children cumulated CPU time (s) 159.71 Current children cumulated vsize (Kb) 12768 [startup+170.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27846 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 2591 0 0 0 16949 21 0 0 25 0 1 0 1855368786 11034624 2578 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 2694 2578 145 145 0 2549 0 [pid=27846] vsize: 10776 Current children cumulated CPU time (s) 169.71 Current children cumulated vsize (Kb) 12900 [startup+180.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27846 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 2908 0 0 0 17944 23 0 0 25 0 1 0 1855368786 12324864 2895 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3009 2895 145 145 0 2864 0 [pid=27846] vsize: 12036 Current children cumulated CPU time (s) 179.68 Current children cumulated vsize (Kb) 14160 [startup+190.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27846 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 2908 0 0 0 18944 23 0 0 25 0 1 0 1855368786 12324864 2895 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3009 2895 145 145 0 2864 0 [pid=27846] vsize: 12036 Current children cumulated CPU time (s) 189.68 Current children cumulated vsize (Kb) 14160 [startup+200.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27846 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 2908 0 0 0 19944 23 0 0 25 0 1 0 1855368786 12324864 2895 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3009 2895 145 145 0 2864 0 [pid=27846] vsize: 12036 Current children cumulated CPU time (s) 199.68 Current children cumulated vsize (Kb) 14160 [startup+210.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27846 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 2997 0 0 0 20943 24 0 0 25 0 1 0 1855368786 12689408 2984 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3098 2984 145 145 0 2953 0 [pid=27846] vsize: 12392 Current children cumulated CPU time (s) 209.68 Current children cumulated vsize (Kb) 14516 [startup+220.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27846 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3125 0 0 0 21940 25 0 0 25 0 1 0 1855368786 13213696 3112 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3226 3112 145 145 0 3081 0 [pid=27846] vsize: 12904 Current children cumulated CPU time (s) 219.66 Current children cumulated vsize (Kb) 15028 [startup+230.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27846 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3125 0 0 0 22940 25 0 0 25 0 1 0 1855368786 13213696 3112 4294967295 134512640 135094434 3221224432 3221223056 134562108 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3226 3112 145 145 0 3081 0 [pid=27846] vsize: 12904 Current children cumulated CPU time (s) 229.66 Current children cumulated vsize (Kb) 15028 [startup+240.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27846 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3125 0 0 0 23941 25 0 0 25 0 1 0 1855368786 13213696 3112 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3226 3112 145 145 0 3081 0 [pid=27846] vsize: 12904 Current children cumulated CPU time (s) 239.67 Current children cumulated vsize (Kb) 15028 [startup+250.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27846 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 24940 26 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 249.67 Current children cumulated vsize (Kb) 15240 [startup+260.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27846 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 25939 26 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 259.66 Current children cumulated vsize (Kb) 15240 [startup+270.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27846 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 26939 27 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 269.67 Current children cumulated vsize (Kb) 15240 [startup+280.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27846 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 27940 27 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 279.68 Current children cumulated vsize (Kb) 15240 [startup+290.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27846 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 28940 27 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 289.68 Current children cumulated vsize (Kb) 15240 [startup+300.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27846 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 29940 27 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 299.68 Current children cumulated vsize (Kb) 15240 [startup+310.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27846 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 30940 27 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134558002 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 309.68 Current children cumulated vsize (Kb) 15240 [startup+320.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27846 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 31940 27 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 319.68 Current children cumulated vsize (Kb) 15240 [startup+330.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27846 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 32940 27 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 329.68 Current children cumulated vsize (Kb) 15240 [startup+340.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27846 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 33940 27 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 339.68 Current children cumulated vsize (Kb) 15240 [startup+350.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27846 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 34940 27 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 349.68 Current children cumulated vsize (Kb) 15240 [startup+360.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27846 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 35941 27 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 359.69 Current children cumulated vsize (Kb) 15240 [startup+370.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27846 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 36941 27 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 369.69 Current children cumulated vsize (Kb) 15240 [startup+380.04 s] Raw data (loadavg): 1.07 0.99 0.91 2/57 27897 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 37940 28 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223104 134556468 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 379.69 Current children cumulated vsize (Kb) 15240 [startup+390.041 s] Raw data (loadavg): 1.06 0.99 0.91 2/57 27897 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 38940 28 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 389.69 Current children cumulated vsize (Kb) 15240 [startup+400.042 s] Raw data (loadavg): 1.05 0.99 0.91 2/57 27897 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 39940 29 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 399.7 Current children cumulated vsize (Kb) 15240 [startup+410.042 s] Raw data (loadavg): 1.04 0.99 0.91 2/57 27897 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 40940 29 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 409.7 Current children cumulated vsize (Kb) 15240 [startup+420.043 s] Raw data (loadavg): 1.04 0.99 0.91 2/57 27897 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 41940 29 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 419.7 Current children cumulated vsize (Kb) 15240 [startup+430.044 s] Raw data (loadavg): 1.03 0.99 0.91 2/57 27897 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 42940 29 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223104 134555563 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 429.7 Current children cumulated vsize (Kb) 15240 [startup+440.045 s] Raw data (loadavg): 1.03 0.99 0.91 2/57 27897 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 43941 29 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 439.71 Current children cumulated vsize (Kb) 15240 [startup+450.045 s] Raw data (loadavg): 1.02 0.99 0.91 2/57 27901 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 44941 29 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 449.71 Current children cumulated vsize (Kb) 15240 [startup+460.046 s] Raw data (loadavg): 1.02 0.99 0.91 2/57 27901 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 45941 29 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134558398 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 459.71 Current children cumulated vsize (Kb) 15240 [startup+470.046 s] Raw data (loadavg): 1.01 0.99 0.91 2/57 27901 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 46941 29 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 469.71 Current children cumulated vsize (Kb) 15240 [startup+480.047 s] Raw data (loadavg): 1.01 0.99 0.91 2/57 27901 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 47941 29 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 479.71 Current children cumulated vsize (Kb) 15240 [startup+490.048 s] Raw data (loadavg): 1.01 0.99 0.91 2/57 27901 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 48941 29 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223024 134551702 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 489.71 Current children cumulated vsize (Kb) 15240 [startup+500.049 s] Raw data (loadavg): 1.01 0.99 0.91 2/57 27901 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 49941 29 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 499.71 Current children cumulated vsize (Kb) 15240 [startup+510.05 s] Raw data (loadavg): 1.01 0.99 0.91 2/57 27901 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 50942 29 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 509.72 Current children cumulated vsize (Kb) 15240 [startup+520.05 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 27901 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 51942 29 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 519.72 Current children cumulated vsize (Kb) 15240 [startup+530.052 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 27901 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 52942 29 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223024 134557500 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 529.72 Current children cumulated vsize (Kb) 15240 [startup+540.053 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 27901 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3180 0 0 0 53943 29 0 0 25 0 1 0 1855368786 13430784 3167 4294967295 134512640 135094434 3221224432 3221223056 134557705 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3167 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 539.73 Current children cumulated vsize (Kb) 15240 [startup+550.054 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 27901 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3180 0 0 0 54943 29 0 0 25 0 1 0 1855368786 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3167 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 549.73 Current children cumulated vsize (Kb) 15240 [startup+560.056 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 27901 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3180 0 0 0 55943 30 0 0 25 0 1 0 1855368786 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3167 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 559.74 Current children cumulated vsize (Kb) 15240 [startup+570.057 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 27901 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3180 0 0 0 56943 30 0 0 25 0 1 0 1855368786 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3167 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 569.74 Current children cumulated vsize (Kb) 15240 [startup+580.057 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 27901 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3180 0 0 0 57942 30 0 0 25 0 1 0 1855368786 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3167 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 579.73 Current children cumulated vsize (Kb) 15240 [startup+590.059 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 27901 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3180 0 0 0 58942 31 0 0 25 0 1 0 1855368786 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3167 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 589.74 Current children cumulated vsize (Kb) 15240 [startup+600.059 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 27901 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3180 0 0 0 59942 32 0 0 25 0 1 0 1855368786 13430784 3167 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3167 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 599.75 Current children cumulated vsize (Kb) 15240 [startup+610.06 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 27901 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3180 0 0 0 60942 32 0 0 25 0 1 0 1855368786 13430784 3167 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3167 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 609.75 Current children cumulated vsize (Kb) 15240 [startup+620.061 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 27901 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3180 0 0 0 61942 32 0 0 25 0 1 0 1855368786 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3167 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 619.75 Current children cumulated vsize (Kb) 15240 [startup+630.062 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 27901 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3180 0 0 0 62942 32 0 0 25 0 1 0 1855368786 13430784 3167 4294967295 134512640 135094434 3221224432 3221223104 134556246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3167 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 629.75 Current children cumulated vsize (Kb) 15240 [startup+640.062 s] Raw data (loadavg): 1.08 1.00 0.92 2/57 27901 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3180 0 0 0 63942 33 0 0 25 0 1 0 1855368786 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3167 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 639.76 Current children cumulated vsize (Kb) 15240 [startup+650.063 s] Raw data (loadavg): 1.07 1.00 0.92 2/57 27901 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3180 0 0 0 64942 33 0 0 25 0 1 0 1855368786 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3167 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 649.76 Current children cumulated vsize (Kb) 15240 [startup+660.064 s] Raw data (loadavg): 1.06 1.00 0.92 2/57 27901 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3180 0 0 0 65942 33 0 0 25 0 1 0 1855368786 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3167 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 659.76 Current children cumulated vsize (Kb) 15240 [startup+670.065 s] Raw data (loadavg): 1.20 1.03 0.93 2/57 27901 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3180 0 0 0 66942 33 0 0 25 0 1 0 1855368786 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3167 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 669.76 Current children cumulated vsize (Kb) 15240 [startup+680.066 s] Raw data (loadavg): 1.17 1.03 0.93 2/57 27901 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3180 0 0 0 67942 33 0 0 25 0 1 0 1855368786 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3167 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 679.76 Current children cumulated vsize (Kb) 15240 [startup+690.066 s] Raw data (loadavg): 1.14 1.03 0.93 2/57 27901 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3180 0 0 0 68942 33 0 0 25 0 1 0 1855368786 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3167 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 689.76 Current children cumulated vsize (Kb) 15240 [startup+700.067 s] Raw data (loadavg): 1.12 1.03 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3180 0 0 0 69943 33 0 0 25 0 1 0 1855368786 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3167 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 699.77 Current children cumulated vsize (Kb) 15240 [startup+710.068 s] Raw data (loadavg): 1.10 1.03 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3180 0 0 0 70943 33 0 0 25 0 1 0 1855368786 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3167 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 709.77 Current children cumulated vsize (Kb) 15240 [startup+720.069 s] Raw data (loadavg): 1.09 1.03 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3180 0 0 0 71943 33 0 0 25 0 1 0 1855368786 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3167 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 719.77 Current children cumulated vsize (Kb) 15240 [startup+730.07 s] Raw data (loadavg): 1.07 1.03 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3180 0 0 0 72943 33 0 0 25 0 1 0 1855368786 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3167 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 729.77 Current children cumulated vsize (Kb) 15240 [startup+740.071 s] Raw data (loadavg): 1.06 1.02 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3180 0 0 0 73943 33 0 0 25 0 1 0 1855368786 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3167 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 739.77 Current children cumulated vsize (Kb) 15240 [startup+750.07 s] Raw data (loadavg): 1.05 1.02 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3183 0 0 0 74943 33 0 0 25 0 1 0 1855368786 13430784 3170 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3170 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 749.77 Current children cumulated vsize (Kb) 15240 [startup+760.072 s] Raw data (loadavg): 1.04 1.02 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3183 0 0 0 75944 33 0 0 25 0 1 0 1855368786 13430784 3170 4294967295 134512640 135094434 3221224432 3221223024 134557328 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3170 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 759.78 Current children cumulated vsize (Kb) 15240 [startup+770.073 s] Raw data (loadavg): 1.04 1.02 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3183 0 0 0 76944 34 0 0 25 0 1 0 1855368786 13430784 3170 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3279 3170 145 145 0 3134 0 [pid=27846] vsize: 13116 Current children cumulated CPU time (s) 769.79 Current children cumulated vsize (Kb) 15240 [startup+780.074 s] Raw data (loadavg): 1.03 1.02 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3345 0 0 0 77941 34 0 0 25 0 1 0 1855368786 14094336 3332 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3441 3332 145 145 0 3296 0 [pid=27846] vsize: 13764 Current children cumulated CPU time (s) 779.76 Current children cumulated vsize (Kb) 15888 [startup+790.075 s] Raw data (loadavg): 1.02 1.02 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3485 0 0 0 78939 36 0 0 25 0 1 0 1855368786 14667776 3472 4294967295 134512640 135094434 3221224432 3221223088 134557917 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3581 3472 145 145 0 3436 0 [pid=27846] vsize: 14324 Current children cumulated CPU time (s) 789.76 Current children cumulated vsize (Kb) 16448 [startup+800.076 s] Raw data (loadavg): 1.02 1.02 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3492 0 0 0 79939 36 0 0 25 0 1 0 1855368786 14700544 3479 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3589 3479 145 145 0 3444 0 [pid=27846] vsize: 14356 Current children cumulated CPU time (s) 799.76 Current children cumulated vsize (Kb) 16480 [startup+810.076 s] Raw data (loadavg): 1.02 1.02 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3505 0 0 0 80939 36 0 0 25 0 1 0 1855368786 14766080 3492 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3605 3492 145 145 0 3460 0 [pid=27846] vsize: 14420 Current children cumulated CPU time (s) 809.76 Current children cumulated vsize (Kb) 16544 [startup+820.077 s] Raw data (loadavg): 1.01 1.02 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3508 0 0 0 81939 36 0 0 25 0 1 0 1855368786 14766080 3495 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3605 3495 145 145 0 3460 0 [pid=27846] vsize: 14420 Current children cumulated CPU time (s) 819.76 Current children cumulated vsize (Kb) 16544 [startup+830.079 s] Raw data (loadavg): 1.01 1.02 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3508 0 0 0 82939 36 0 0 25 0 1 0 1855368786 14766080 3495 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3605 3495 145 145 0 3460 0 [pid=27846] vsize: 14420 Current children cumulated CPU time (s) 829.76 Current children cumulated vsize (Kb) 16544 [startup+840.08 s] Raw data (loadavg): 1.01 1.02 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3509 0 0 0 83940 36 0 0 25 0 1 0 1855368786 14766080 3496 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3605 3496 145 145 0 3460 0 [pid=27846] vsize: 14420 Current children cumulated CPU time (s) 839.77 Current children cumulated vsize (Kb) 16544 [startup+850.081 s] Raw data (loadavg): 1.01 1.01 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3509 0 0 0 84939 36 0 0 25 0 1 0 1855368786 14766080 3496 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3605 3496 145 145 0 3460 0 [pid=27846] vsize: 14420 Current children cumulated CPU time (s) 849.76 Current children cumulated vsize (Kb) 16544 [startup+860.082 s] Raw data (loadavg): 1.01 1.01 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3509 0 0 0 85940 36 0 0 25 0 1 0 1855368786 14766080 3496 4294967295 134512640 135094434 3221224432 3221223056 134557726 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3605 3496 145 145 0 3460 0 [pid=27846] vsize: 14420 Current children cumulated CPU time (s) 859.77 Current children cumulated vsize (Kb) 16544 [startup+870.083 s] Raw data (loadavg): 1.00 1.01 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3557 0 0 0 86939 36 0 0 25 0 1 0 1855368786 15093760 3544 4294967295 134512640 135094434 3221224432 3221223088 134558411 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3685 3544 145 145 0 3540 0 [pid=27846] vsize: 14740 Current children cumulated CPU time (s) 869.76 Current children cumulated vsize (Kb) 16864 [startup+880.084 s] Raw data (loadavg): 1.00 1.01 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3560 0 0 0 87940 36 0 0 25 0 1 0 1855368786 15126528 3547 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3693 3547 145 145 0 3548 0 [pid=27846] vsize: 14772 Current children cumulated CPU time (s) 879.77 Current children cumulated vsize (Kb) 16896 [startup+890.086 s] Raw data (loadavg): 1.00 1.01 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3567 0 0 0 88940 36 0 0 25 0 1 0 1855368786 15142912 3554 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3697 3554 145 145 0 3552 0 [pid=27846] vsize: 14788 Current children cumulated CPU time (s) 889.77 Current children cumulated vsize (Kb) 16912 [startup+900.086 s] Raw data (loadavg): 1.00 1.01 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3733 0 0 0 89938 37 0 0 25 0 1 0 1855368786 15843328 3720 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 3868 3720 145 145 0 3723 0 [pid=27846] vsize: 15472 Current children cumulated CPU time (s) 899.76 Current children cumulated vsize (Kb) 17596 [startup+910.087 s] Raw data (loadavg): 1.00 1.01 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3892 0 0 0 90934 39 0 0 25 0 1 0 1855368786 16490496 3879 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 4026 3879 145 145 0 3881 0 [pid=27846] vsize: 16104 Current children cumulated CPU time (s) 909.74 Current children cumulated vsize (Kb) 18228 [startup+920.087 s] Raw data (loadavg): 1.00 1.01 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3898 0 0 0 91935 39 0 0 25 0 1 0 1855368786 16523264 3885 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 4034 3885 145 145 0 3889 0 [pid=27846] vsize: 16136 Current children cumulated CPU time (s) 919.75 Current children cumulated vsize (Kb) 18260 [startup+930.089 s] Raw data (loadavg): 1.00 1.01 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3917 0 0 0 92934 39 0 0 25 0 1 0 1855368786 16621568 3904 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 4058 3904 145 145 0 3913 0 [pid=27846] vsize: 16232 Current children cumulated CPU time (s) 929.74 Current children cumulated vsize (Kb) 18356 [startup+940.09 s] Raw data (loadavg): 1.00 1.01 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3924 0 0 0 93935 39 0 0 25 0 1 0 1855368786 16654336 3911 4294967295 134512640 135094434 3221224432 3221223104 134555849 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 4066 3911 145 145 0 3921 0 [pid=27846] vsize: 16264 Current children cumulated CPU time (s) 939.75 Current children cumulated vsize (Kb) 18388 [startup+950.091 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4010 0 0 0 94934 39 0 0 25 0 1 0 1855368786 17006592 3997 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 4152 3997 145 145 0 4007 0 [pid=27846] vsize: 16608 Current children cumulated CPU time (s) 949.74 Current children cumulated vsize (Kb) 18732 [startup+960.092 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4016 0 0 0 95934 39 0 0 25 0 1 0 1855368786 17039360 4003 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 4160 4003 145 145 0 4015 0 [pid=27846] vsize: 16640 Current children cumulated CPU time (s) 959.74 Current children cumulated vsize (Kb) 18764 [startup+970.092 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4023 0 0 0 96934 39 0 0 25 0 1 0 1855368786 17072128 4010 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 4168 4010 145 145 0 4023 0 [pid=27846] vsize: 16672 Current children cumulated CPU time (s) 969.74 Current children cumulated vsize (Kb) 18796 [startup+980.093 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4036 0 0 0 97934 39 0 0 25 0 1 0 1855368786 17137664 4023 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 4184 4023 145 145 0 4039 0 [pid=27846] vsize: 16736 Current children cumulated CPU time (s) 979.74 Current children cumulated vsize (Kb) 18860 [startup+990.094 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4061 0 0 0 98934 40 0 0 25 0 1 0 1855368786 17235968 4048 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 4208 4048 145 145 0 4063 0 [pid=27846] vsize: 16832 Current children cumulated CPU time (s) 989.75 Current children cumulated vsize (Kb) 18956 [startup+1000.09 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4061 0 0 0 99934 40 0 0 25 0 1 0 1855368786 17235968 4048 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 4208 4048 145 145 0 4063 0 [pid=27846] vsize: 16832 Current children cumulated CPU time (s) 999.75 Current children cumulated vsize (Kb) 18956 [startup+1010.1 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4071 0 0 0 100934 40 0 0 25 0 1 0 1855368786 17285120 4058 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 4220 4058 145 145 0 4075 0 [pid=27846] vsize: 16880 Current children cumulated CPU time (s) 1009.75 Current children cumulated vsize (Kb) 19004 [startup+1020.1 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4073 0 0 0 101934 40 0 0 25 0 1 0 1855368786 17285120 4060 4294967295 134512640 135094434 3221224432 3221223104 134556236 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 4220 4060 145 145 0 4075 0 [pid=27846] vsize: 16880 Current children cumulated CPU time (s) 1019.75 Current children cumulated vsize (Kb) 19004 [startup+1030.1 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4152 0 0 0 102932 41 0 0 25 0 1 0 1855368786 17616896 4139 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27846/statm): 4301 4139 145 145 0 4156 0 [pid=27846] vsize: 17204 Current children cumulated CPU time (s) 1029.74 Current children cumulated vsize (Kb) 19328 [startup+1040.1 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4152 0 0 0 103931 41 0 0 25 0 1 0 1855368786 17616896 4139 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 4301 4139 145 145 0 4156 0 [pid=27846] vsize: 17204 Current children cumulated CPU time (s) 1039.73 Current children cumulated vsize (Kb) 19328 [startup+1050.1 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4155 0 0 0 104932 41 0 0 25 0 1 0 1855368786 17633280 4142 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 4305 4142 145 145 0 4160 0 [pid=27846] vsize: 17220 Current children cumulated CPU time (s) 1049.74 Current children cumulated vsize (Kb) 19344 [startup+1060.1 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4157 0 0 0 105932 41 0 0 25 0 1 0 1855368786 17633280 4144 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 4305 4144 145 145 0 4160 0 [pid=27846] vsize: 17220 Current children cumulated CPU time (s) 1059.74 Current children cumulated vsize (Kb) 19344 [startup+1070.1 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4295 0 0 0 106929 42 0 0 25 0 1 0 1855368786 18190336 4282 4294967295 134512640 135094434 3221224432 3221223104 134555787 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 4441 4282 145 145 0 4296 0 [pid=27846] vsize: 17764 Current children cumulated CPU time (s) 1069.72 Current children cumulated vsize (Kb) 19888 [startup+1080.1 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4295 0 0 0 107929 42 0 0 25 0 1 0 1855368786 18190336 4282 4294967295 134512640 135094434 3221224432 3221223104 134554886 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 4441 4282 145 145 0 4296 0 [pid=27846] vsize: 17764 Current children cumulated CPU time (s) 1079.72 Current children cumulated vsize (Kb) 19888 [startup+1090.1 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4298 0 0 0 108930 42 0 0 25 0 1 0 1855368786 18202624 4285 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 4444 4285 145 145 0 4299 0 [pid=27846] vsize: 17776 Current children cumulated CPU time (s) 1089.73 Current children cumulated vsize (Kb) 19900 [startup+1100.1 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4298 0 0 0 109930 42 0 0 25 0 1 0 1855368786 18202624 4285 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 4444 4285 145 145 0 4299 0 [pid=27846] vsize: 17776 Current children cumulated CPU time (s) 1099.73 Current children cumulated vsize (Kb) 19900 [startup+1110.1 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4301 0 0 0 110930 42 0 0 25 0 1 0 1855368786 18219008 4288 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 4448 4288 145 145 0 4303 0 [pid=27846] vsize: 17792 Current children cumulated CPU time (s) 1109.73 Current children cumulated vsize (Kb) 19916 [startup+1120.1 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4301 0 0 0 111930 42 0 0 25 0 1 0 1855368786 18219008 4288 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 4448 4288 145 145 0 4303 0 [pid=27846] vsize: 17792 Current children cumulated CPU time (s) 1119.73 Current children cumulated vsize (Kb) 19916 [startup+1130.1 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4301 0 0 0 112930 42 0 0 25 0 1 0 1855368786 18219008 4288 4294967295 134512640 135094434 3221224432 3221223056 134557636 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 4448 4288 145 145 0 4303 0 [pid=27846] vsize: 17792 Current children cumulated CPU time (s) 1129.73 Current children cumulated vsize (Kb) 19916 [startup+1140.11 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4301 0 0 0 113931 42 0 0 25 0 1 0 1855368786 18219008 4288 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 4448 4288 145 145 0 4303 0 [pid=27846] vsize: 17792 Current children cumulated CPU time (s) 1139.74 Current children cumulated vsize (Kb) 19916 [startup+1150.11 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4320 0 0 0 114931 43 0 0 25 0 1 0 1855368786 18317312 4307 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 4472 4307 145 145 0 4327 0 [pid=27846] vsize: 17888 Current children cumulated CPU time (s) 1149.75 Current children cumulated vsize (Kb) 20012 [startup+1160.11 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4321 0 0 0 115931 43 0 0 25 0 1 0 1855368786 18317312 4308 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 4472 4308 145 145 0 4327 0 [pid=27846] vsize: 17888 Current children cumulated CPU time (s) 1159.75 Current children cumulated vsize (Kb) 20012 [startup+1170.11 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4327 0 0 0 116931 43 0 0 25 0 1 0 1855368786 18350080 4314 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 4480 4314 145 145 0 4335 0 [pid=27846] vsize: 17920 Current children cumulated CPU time (s) 1169.75 Current children cumulated vsize (Kb) 20044 [startup+1180.11 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4348 0 0 0 117930 44 0 0 25 0 1 0 1855368786 18448384 4335 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 4504 4335 145 145 0 4359 0 [pid=27846] vsize: 18016 Current children cumulated CPU time (s) 1179.75 Current children cumulated vsize (Kb) 20140 [startup+1190.11 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4350 0 0 0 118930 45 0 0 25 0 1 0 1855368786 18448384 4337 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 4504 4337 145 145 0 4359 0 [pid=27846] vsize: 18016 Current children cumulated CPU time (s) 1189.76 Current children cumulated vsize (Kb) 20140 [startup+1200.11 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4350 0 0 0 119939 45 0 0 25 0 1 0 1855368786 18448384 4337 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 4504 4337 145 145 0 4359 0 [pid=27846] vsize: 18016 Current children cumulated CPU time (s) 1199.85 Current children cumulated vsize (Kb) 20140 [startup+1210.21 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4350 0 0 0 120939 45 0 0 25 0 1 0 1855368786 18448384 4337 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 4504 4337 145 145 0 4359 0 [pid=27846] vsize: 18016 Current children cumulated CPU time (s) 1209.85 Current children cumulated vsize (Kb) 20140 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.21 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 27903 Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27842/statm): 531 226 485 147 0 384 0 [pid=27842] vsize: 2124 Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4350 0 0 0 120939 45 0 0 25 0 1 0 1855368786 18448384 4337 4294967295 134512640 135094434 3221224432 3221223056 134557726 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27846/statm): 4504 4337 145 145 0 4359 0 [pid=27846] vsize: 18016 Current children cumulated CPU time (s) 1209.85 Current children cumulated vsize (Kb) 20140 Sending SIGTERM to -27842 Sleeping 2 seconds One traced child (pid=27842) ended because it received signal 15 (SIGTERM) One traced child (pid=27846) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.22 CPU time (s): 1209.87 CPU user time (s): 1209.4 CPU system time (s): 0.465929 CPU usage (%): 99.9706 Max. virtual memory (cumulated for all children) (Kb): 20140
ERROR: no interpretation found !