| Name | mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-lp4l.opb |
| MD5SUM | 3c39e3c2b993ee2185e2a1a3e73b9723 |
| Bench Category | optimization, small integers (OPTSMALLINT) |
| Has Objective Function | YES |
| Satisfiable | YES |
| (Un)Satisfiability was proved | YES |
| Best value of the objective function | 2967 |
| Optimality of the best value was proved | YES |
| Number of terms in the objective function | 1086 |
| Biggest coefficient in the objective function | 283 |
| Number of bits for the biggest coefficient in the objective function | 9 |
| Sum of the numbers in the objective function | 197191 |
| Number of bits of the sum of numbers in the objective function | 18 |
| Biggest number in a constraint | 283 |
| Number of bits of the biggest number in a constraint | 9 |
| Biggest sum of numbers in a constraint | 197191 |
| Number of bits of the biggest sum of numbers | 18 |
| Best result obtained on this benchmark | OPTIMUM FOUND |
| Best CPU time to get the best result obtained on this benchmark | 315.832 |
| Number of variables | 1086 |
| Total number of constraints | 1171 |
| Number of constraints which are clauses | 0 |
| Number of constraints which are cardinality constraints (but not clauses) | 1170 |
| Number of constraints which are nor clauses,nor cardinality constraints | 1 |
| Minimum length of a constraint | 1 |
| Maximum length of a constraint | 1086 |
LAUNCH ON wulflinc23 THE 2005-09-19 03:07:09 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2860 boxname=wulflinc23 idbench=516 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 3c39e3c2b993ee2185e2a1a3e73b9723 /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-lp4l.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-lp4l.opb IDLAUNCH: 2860 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.037 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.037 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: 889160 kB Buffers: 36924 kB Cached: 80060 kB SwapCached: 792 kB Active: 66824 kB Inactive: 52708 kB HighTotal: 131008 kB HighFree: 47796 kB LowTotal: 903652 kB LowFree: 841364 kB SwapTotal: 2097136 kB SwapFree: 2095868 kB Dirty: 36 kB Writeback: 0 kB Mapped: 5692 kB Slab: 20384 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-19 03:27:19 (client local time) WITH STATUS 10 IN 1206.33 SECONDS stats: 2860 7 1206.33 10
c Parsing PB file... c Converting 169 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: #################################################################################### c -- Clauses(.)/Splits(s): (none) c ---[ 168]---> Adder-cost: 592 maxlim: 2471 bits: 12/12 c ---[ 166]---> BDD-cost: 41 c ---[ 164]---> BDD-cost: 67 c ---[ 162]---> BDD-cost: 99 c ---[ 160]---> BDD-cost: 79 c ---[ 158]---> BDD-cost: 45 c ---[ 156]---> BDD-cost: 69 c ---[ 154]---> BDD-cost: 55 c ---[ 152]---> BDD-cost: 37 c ---[ 150]---> BDD-cost: 27 c ---[ 148]---> BDD-cost: 77 c ---[ 146]---> BDD-cost: 79 c ---[ 144]---> BDD-cost: 23 c ---[ 142]---> BDD-cost: 75 c ---[ 140]---> BDD-cost: 77 c ---[ 138]---> BDD-cost: 41 c ---[ 136]---> BDD-cost: 75 c ---[ 134]---> BDD-cost: 107 c ---[ 132]---> BDD-cost: 91 c ---[ 130]---> BDD-cost: 127 c ---[ 128]---> BDD-cost: 123 c ---[ 126]---> BDD-cost: 89 c ---[ 124]---> BDD-cost: 57 c ---[ 122]---> BDD-cost: 89 c ---[ 120]---> BDD-cost: 71 c ---[ 118]---> BDD-cost: 103 c ---[ 116]---> BDD-cost: 117 c ---[ 114]---> BDD-cost: 125 c ---[ 112]---> BDD-cost: 91 c ---[ 110]---> BDD-cost: 59 c ---[ 108]---> BDD-cost: 89 c ---[ 106]---> BDD-cost: 71 c ---[ 104]---> BDD-cost: 129 c ---[ 102]---> BDD-cost: 113 c ---[ 100]---> BDD-cost: 123 c ---[ 98]---> BDD-cost: 89 c ---[ 96]---> BDD-cost: 61 c ---[ 94]---> BDD-cost: 59 c ---[ 92]---> BDD-cost: 33 c ---[ 90]---> BDD-cost: 123 c ---[ 88]---> BDD-cost: 121 c ---[ 86]---> BDD-cost: 99 c ---[ 84]---> BDD-cost: 45 c ---[ 82]---> BDD-cost: 69 c ---[ 80]---> BDD-cost: 59 c ---[ 78]---> BDD-cost: 33 c ---[ 76]---> BDD-cost: 73 c ---[ 74]---> BDD-cost: 69 c ---[ 72]---> BDD-cost: 47 c ---[ 70]---> BDD-cost: 67 c ---[ 68]---> BDD-cost: 95 c ---[ 66]---> BDD-cost: 85 c ---[ 64]---> BDD-cost: 107 c ---[ 62]---> BDD-cost: 97 c ---[ 60]---> BDD-cost: 33 c ---[ 58]---> BDD-cost: 79 c ---[ 56]---> BDD-cost: 87 c ---[ 54]---> BDD-cost: 75 c ---[ 52]---> BDD-cost: 67 c ---[ 50]---> BDD-cost: 43 c ---[ 48]---> BDD-cost: 75 c ---[ 46]---> BDD-cost: 105 c ---[ 44]---> BDD-cost: 87 c ---[ 42]---> BDD-cost: 77 c ---[ 40]---> BDD-cost: 63 c ---[ 38]---> BDD-cost: 39 c ---[ 36]---> BDD-cost: 77 c ---[ 34]---> BDD-cost: 63 c ---[ 32]---> BDD-cost: 5 c ---[ 30]---> BDD-cost: 169 c ---[ 28]---> BDD-cost: 155 c ---[ 26]---> BDD-cost: 115 c ---[ 24]---> BDD-cost: 77 c ---[ 22]---> BDD-cost: 83 c ---[ 20]---> BDD-cost: 111 c ---[ 18]---> BDD-cost: 107 c ---[ 16]---> BDD-cost: 161 c ---[ 14]---> BDD-cost: 151 c ---[ 12]---> BDD-cost: 117 c ---[ 10]---> BDD-cost: 57 c ---[ 8]---> BDD-cost: 85 c ---[ 6]---> BDD-cost: 71 c ---[ 4]---> BDD-cost: 25 c ---[ 2]---> BDD-cost: 37 c ---[ 0]---> Adder-cost: 2160 maxlim: 1059 bits: 11/11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 35697 111365 | 11899 0 0 nan | 0.000 % | c | 100 | 35673 111283 | 13088 98 3550 36.2 | 1.208 % | c | 250 | 35673 111283 | 14397 248 6872 27.7 | 1.208 % | c | 475 | 35673 111283 | 15837 473 22930 48.5 | 1.208 % | c | 812 | 35582 110964 | 17421 797 32292 40.5 | 1.350 % | c | 1318 | 35228 109731 | 19163 1236 39075 31.6 | 1.930 % | c | 2077 | 35115 109352 | 21079 1978 55328 28.0 | 2.083 % | c | 3216 | 35106 109323 | 23187 3116 134443 43.1 | 2.102 % | c | 4924 | 35091 109270 | 25506 4817 501813 104.2 | 2.111 % | c ============================================================================== c [1mFound solution: 4678[0m c ---[ 0]---> Adder-cost: 8142 maxlim: 192513 bits: 18/18 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 5808 | 91968 312356 | 30656 5701 636022 111.6 | 2.111 % | c | 5908 | 91968 312356 | 33721 5801 638088 110.0 | 1.222 % | c ============================================================================== c [1mFound solution: 4381[0m c ---[ 0]---> Adder-cost: 0 maxlim: 192810 bits: 18/18 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6012 | 91987 312479 | 30662 5905 642881 108.9 | 1.222 % | c | 6113 | 91987 312479 | 33728 6006 643901 107.2 | 1.248 % | c | 6263 | 91987 312479 | 37101 6156 648018 105.3 | 1.248 % | c | 6490 | 91987 312479 | 40811 6383 655375 102.7 | 1.248 % | c | 6828 | 91987 312479 | 44892 6721 678577 101.0 | 1.248 % | c | 7334 | 91987 312479 | 49381 7227 710491 98.3 | 1.248 % | c | 8093 | 91987 312479 | 54319 7986 772776 96.8 | 1.248 % | c ============================================================================== c [1mFound solution: 4329[0m c ---[ 0]---> Adder-cost: 0 maxlim: 192862 bits: 18/18 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 8535 | 92003 312609 | 30667 8428 796805 94.5 | 1.248 % | c | 8635 | 91996 312585 | 33733 8527 798553 93.6 | 1.285 % | c | 8786 | 91996 312585 | 37107 8678 799323 92.1 | 1.285 % | c | 9015 | 91996 312585 | 40817 8907 810541 91.0 | 1.285 % | c ============================================================================== c [1mFound solution: 4303[0m c ---[ 0]---> Adder-cost: 0 maxlim: 192888 bits: 18/18 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 9343 | 92000 312645 | 30666 9235 872957 94.5 | 1.285 % | c | 9447 | 92000 312645 | 33732 9339 877086 93.9 | 1.306 % | c | 9599 | 92000 312645 | 37105 9491 896729 94.5 | 1.306 % | c | 9825 | 91979 312575 | 40816 9711 900061 92.7 | 1.322 % | c | 10164 | 91979 312575 | 44898 10050 962481 95.8 | 1.322 % | c | 10673 | 91967 312533 | 49387 10550 1020834 96.8 | 1.328 % | c | 11432 | 91967 312533 | 54326 11309 1107842 98.0 | 1.328 % | c | 12574 | 91967 312533 | 59759 12451 1288451 103.5 | 1.328 % | c | 14282 | 91951 312481 | 65735 14156 1567998 110.8 | 1.344 % | c | 16846 | 91944 312457 | 72308 16718 2021257 120.9 | 1.349 % | c | 20697 | 91944 312457 | 79539 20569 2889530 140.5 | 1.349 % | c ============================================================================== c [1mFound solution: 4269[0m c ---[ 0]---> Adder-cost: 0 maxlim: 192922 bits: 18/18 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21234 | 91954 312544 | 30651 21106 2966775 140.6 | 1.349 % | c | 21335 | 91898 312350 | 33716 21192 2969519 140.1 | 1.413 % | c | 21485 | 91898 312350 | 37087 21342 3004545 140.8 | 1.413 % | c | 21711 | 91785 311959 | 40796 21531 3013007 139.9 | 1.504 % | c | 22051 | 91785 311959 | 44876 21871 3070258 140.4 | 1.504 % | c | 22559 | 91785 311959 | 49363 22379 3176774 142.0 | 1.504 % | c | 23320 | 91756 311856 | 54300 23120 3255681 140.8 | 1.520 % | c | 24459 | 91756 311856 | 59730 24259 3473974 143.2 | 1.520 % | c | 26169 | 91756 311856 | 65703 25969 3776044 145.4 | 1.520 % | c | 28733 | 91756 311856 | 72273 28533 4179806 146.5 | 1.520 % | c | 32579 | 91676 311577 | 79500 32345 4833206 149.4 | 1.589 % | c | 38348 | 91676 311577 | 87450 38114 6308737 165.5 | 1.589 % | c | 46997 | 91601 311320 | 96195 46740 8459122 181.0 | 1.643 % | c ============================================================================== c [1mFound solution: 4262[0m c ---[ 0]---> Adder-cost: 0 maxlim: 192929 bits: 18/18 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 59475 | 91556 311180 | 30518 59211 11444311 193.3 | 1.643 % | c | 59575 | 91556 311180 | 33569 16951 2967034 175.0 | 1.685 % | c | 59727 | 91556 311180 | 36926 17103 2987056 174.7 | 1.685 % | c | 59955 | 91556 311180 | 40619 17331 3023499 174.5 | 1.685 % | c | 60296 | 91556 311180 | 44681 17672 3059606 173.1 | 1.685 % | c | 60802 | 91556 311180 | 49149 18178 3146794 173.1 | 1.685 % | c | 61561 | 91556 311180 | 54064 18937 3286300 173.5 | 1.685 % | c | 62700 | 91556 311180 | 59470 20076 3636099 181.1 | 1.685 % | c | 64412 | 91556 311180 | 65418 21788 3877981 178.0 | 1.685 % | c ============================================================================== c [1mFound solution: 4219[0m c ---[ 0]---> Adder-cost: 0 maxlim: 192972 bits: 18/18 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 66546 | 91560 311241 | 30520 23922 4366619 182.5 | 1.685 % | c | 66646 | 91560 311241 | 33572 24022 4371054 182.0 | 1.707 % | c | 66797 | 91560 311241 | 36929 24173 4384424 181.4 | 1.707 % | c | 67026 | 91560 311241 | 40622 24402 4398296 180.2 | 1.707 % | c | 67363 | 91560 311241 | 44684 24739 4461698 180.4 | 1.707 % | c | 67871 | 91560 311241 | 49152 25247 4557821 180.5 | 1.707 % | c | 68634 | 91560 311241 | 54068 26010 4671976 179.6 | 1.707 % | c | 69773 | 91560 311241 | 59474 27149 5037188 185.5 | 1.707 % | c | 71481 | 91560 311241 | 65422 28857 5394646 186.9 | 1.707 % | c | 74043 | 91535 311160 | 71964 31415 6062380 193.0 | 1.733 % | c | 77887 | 91535 311160 | 79161 35259 6921757 196.3 | 1.733 % | c | 83653 | 91535 311160 | 87077 41025 8057816 196.4 | 1.733 % | c | 92304 | 91535 311160 | 95784 49676 10781790 217.0 | 1.733 % | c ============================================================================== c [1mFound solution: 4172[0m c ---[ 0]---> Adder-cost: 0 maxlim: 193019 bits: 18/18 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 95559 | 91542 311224 | 30514 52931 11644687 220.0 | 1.733 % | c | 95659 | 91542 311224 | 33565 18941 3654438 192.9 | 1.754 % | c | 95809 | 91542 311224 | 36921 19091 3658733 191.6 | 1.754 % | c ============================================================================== c [1mFound solution: 3944[0m c ---[ 0]---> Adder-cost: 0 maxlim: 193247 bits: 18/18 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 95994 | 91551 311287 | 30517 19276 3681560 191.0 | 1.754 % | c | 96096 | 91551 311287 | 33568 19378 3703843 191.1 | 1.775 % | c | 96246 | 91551 311287 | 36925 19528 3722802 190.6 | 1.775 % | c | 96471 | 91551 311287 | 40618 19753 3810541 192.9 | 1.775 % | c | 96811 | 91551 311287 | 44679 20093 3856602 191.9 | 1.775 % | c | 97319 | 91551 311287 | 49147 20601 3980720 193.2 | 1.775 % | c | 98078 | 91551 311287 | 54062 21360 4197445 196.5 | 1.775 % | c | 99219 | 91551 311287 | 59468 22501 4443126 197.5 | 1.775 % | c | 100927 | 91551 311287 | 65415 24209 5125900 211.7 | 1.775 % | c | 103490 | 91551 311287 | 71957 26772 5785251 216.1 | 1.775 % | c | 107334 | 91551 311287 | 79153 30616 7230782 236.2 | 1.775 % | c | 113103 | 91551 311287 | 87068 36385 8775221 241.2 | 1.775 % | c | 121753 | 91551 311287 | 95775 45035 11913321 264.5 | 1.775 % | c | 134728 | 91506 311130 | 105352 58002 16013485 276.1 | 1.796 % | c | 154190 | 91497 311099 | 115888 77462 23776761 306.9 | 1.802 % | c | 183385 | 91480 311042 | 127477 106650 33287203 312.1 | 1.812 % | c c *** TERMINATED *** s SATISFIABLE v CO100001_bit0 -CO100002_bit0 -CO100003_bit0 -CO100004_bit0 -CO100005_bit0 -CO100006_bit0 -CO100007_bit0 -CO100008_bit0 -CO100009_bit0 -CO100010_bit0 -CO100011_bit0 -CO100012_bit0 -CO100013_bit0 -CO100014_bit0 -CO100015_bit0 -CO100016_bit0 -CO100017_bit0 -CO100018_bit0 -CO100019_bit0 -CO100020_bit0 -CO100021_bit0 -CO100022_bit0 -CO100023_bit0 -CO100024_bit0 -CO100025_bit0 -CO100026_bit0 CO100027_bit0 -CO100028_bit0 -CO100029_bit0 -CO100030_bit0 -CO100031_bit0 -CO100032_bit0 -CO100033_bit0 -CO100034_bit0 -CO100035_bit0 -CO100036_bit0 -CO100037_bit0 -CO100038_bit0 -CO100039_bit0 -CO100040_bit0 -CO100041_bit0 -CO100042_bit0 -CO100043_bit0 -CO100044_bit0 -CO100045_bit0 -CO100046_bit0 -CO100047_bit0 -CO100048_bit0 -CO100049_bit0 -CO100050_bit0 -CO100051_bit0 -CO100052_bit0 -CO100053_bit0 -CO100054_bit0 -CO100055_bit0 -CO100056_bit0 -CO100057_bit0 -CO100058_bit0 -CO100059_bit0 -CO100060_bit0 -CO100061_bit0 -CO100062_bit0 -CO100063_bit0 -CO100064_bit0 -CO100065_bit0 CO100066_bit0 -CO100067_bit0 -CO100068_bit0 -CO100069_bit0 -CO100070_bit0 -CO100071_bit0 -CO100072_bit0 -CO100073_bit0 -CO100074_bit0 -CO100075_bit0 -CO100076_bit0 -CO100077_bit0 -CO100078_bit0 -CO100079_bit0 -CO100080_bit0 CO100081_bit0 -CO100082_bit0 CO100083_bit0 -CO100084_bit0 -CO100085_bit0 -CO100086_bit0 -CO100087_bit0 -CO100088_bit0 -CO100089_bit0 -CO100090_bit0 -CO100091_bit0 -CO100092_bit0 -CO100093_bit0 -CO100094_bit0 -CO100095_bit0 -CO100096_bit0 -CO100097_bit0 -CO100098_bit0 -CO100099_bit0 CO100100_bit0 -CO100101_bit0 -CO100102_bit0 -CO100103_bit0 -CO100104_bit0 -CO100105_bit0 -CO100106_bit0 -CO100107_bit0 -CO100108_bit0 -CO100109_bit0 CO100110_bit0 -CO100111_bit0 -CO100112_bit0 -CO100113_bit0 -CO100114_bit0 -CO100115_bit0 -CO100116_bit0 -CO100117_bit0 -CO100118_bit0 -CO100119_bit0 -CO100120_bit0 -CO100121_bit0 -CO100122_bit0 -CO100123_bit0 -CO100124_bit0 -CO100125_bit0 -CO100126_bit0 -CO100127_bit0 -CO100128_bit0 -CO100129_bit0 -CO100130_bit0 -CO100131_bit0 -CO100132_bit0 -CO100133_bit0 -CO100134_bit0 CO100135_bit0 -CO100136_bit0 -CO100137_bit0 CO100138_bit0 -CO100139_bit0 -CO100140_bit0 -CO100141_bit0 -CO100142_bit0 -CO100143_bit0 -CO100144_bit0 -CO100145_bit0 -CO100146_bit0 -CO100147_bit0 -CO100148_bit0 -CO100149_bit0 -CO100150_bit0 -CO100151_bit0 -CO100152_bit0 -CO100153_bit0 -CO100154_bit0 -CO100155_bit0 -CO100156_bit0 -CO100157_bit0 -CO100158_bit0 -CO100159_bit0 -CO100160_bit0 -CO100161_bit0 -CO100162_bit0 -CO100163_bit0 -CO100164_bit0 -CO100165_bit0 CO100166_bit0 -CO100167_bit0 -CO100168_bit0 -CO100169_bit0 -CO100170_bit0 -CO100171_bit0 -CO100172_bit0 -CO100173_bit0 -CO100174_bit0 -CO100175_bit0 -CO100176_bit0 -CO100177_bit0 -CO100178_bit0 -CO100179_bit0 -CO100180_bit0 -CO100181_bit0 -CO100182_bit0 -CO100183_bit0 -CO100184_bit0 -CO100185_bit0 -CO100186_bit0 -CO100187_bit0 -CO100188_bit0 -CO100189_bit0 -CO100190_bit0 -CO100191_bit0 -CO100192_bit0 -CO100193_bit0 -CO100194_bit0 -CO100195_bit0 -CO100196_bit0 -CO100197_bit0 -CO100198_bit0 CO100199_bit0 -CO100200_bit0 -CO100201_bit0 -CO100202_bit0 -CO100203_bit0 -CO100204_bit0 -CO100205_bit0 -CO100206_bit0 -CO100207_bit0 -CO100208_bit0 -CO100209_bit0 -CO100210_bit0 -CO100211_bit0 -CO100212_bit0 -CO100213_bit0 -CO100214_bit0 -CO100215_bit0 -CO100216_bit0 -CO100217_bit0 -CO100218_bit0 -CO100219_bit0 -CO100220_bit0 -CO100221_bit0 -CO100222_bit0 -CO100223_bit0 -CO100224_bit0 -CO100225_bit0 -CO100226_bit0 -CO100227_bit0 -CO100228_bit0 -CO100229_bit0 CO100230_bit0 -CO100231_bit0 -CO100232_bit0 -CO100233_bit0 -CO100234_bit0 -CO100235_bit0 -CO100236_bit0 -CO100237_bit0 -CO100238_bit0 -CO100239_bit0 -CO100240_bit0 -CO100241_bit0 -CO100242_bit0 -CO100243_bit0 -CO100244_bit0 -CO100245_bit0 -CO100246_bit0 -CO100247_bit0 -CO100248_bit0 -CO100249_bit0 -CO100250_bit0 -CO100251_bit0 -CO100252_bit0 -CO100253_bit0 -CO100254_bit0 -CO100255_bit0 -CO100256_bit0 -CO100257_bit0 -CO100258_bit0 -CO100259_bit0 -CO100260_bit0 -CO100261_bit0 -CO100262_bit0 -CO100263_bit0 -CO100264_bit0 -CO100265_bit0 -CO100266_bit0 -CO100267_bit0 -CO100268_bit0 -CO100269_bit0 -CO100270_bit0 -CO100271_bit0 -CO100272_bit0 -CO100273_bit0 -CO100274_bit0 -CO100275_bit0 -CO100276_bit0 -CO100277_bit0 -CO100278_bit0 -CO100279_bit0 -CO100280_bit0 -CO100281_bit0 -CO100282_bit0 -CO100283_bit0 -CO100284_bit0 -CO100285_bit0 -CO100286_bit0 -CO100287_bit0 -CO100288_bit0 -CO100289_bit0 -CO100290_bit0 -CO100291_bit0 -CO100292_bit0 -CO100293_bit0 CO100294_bit0 -CO100295_bit0 -CO100296_bit0 -CO100297_bit0 -CO100298_bit0 -CO100299_bit0 -CO100300_bit0 -CO100301_bit0 -CO100302_bit0 -CO100303_bit0 -CO100304_bit0 -CO100305_bit0 -CO100306_bit0 -CO100307_bit0 -CO100308_bit0 -CO100309_bit0 -CO100310_bit0 -CO100311_bit0 -CO100312_bit0 -CO100313_bit0 -CO100314_bit0 -CO100315_bit0 -CO100316_bit0 -CO100317_bit0 -CO100318_bit0 -CO100319_bit0 -CO100320_bit0 -CO100321_bit0 -CO100322_bit0 -CO100323_bit0 -CO100324_bit0 -CO100325_bit0 -CO100326_bit0 -CO100327_bit0 -CO100328_bit0 -CO100329_bit0 -CO100330_bit0 -CO100331_bit0 -CO100332_bit0 -CO100333_bit0 -CO100334_bit0 -CO100335_bit0 -CO100336_bit0 -CO100337_bit0 -CO100338_bit0 -CO100339_bit0 -CO100340_bit0 -CO100341_bit0 -CO100342_bit0 -CO100343_bit0 -CO100344_bit0 -CO100345_bit0 -CO100346_bit0 -CO100347_bit0 -CO100348_bit0 -CO100349_bit0 -CO100350_bit0 -CO100351_bit0 -CO100352_bit0 -CO100353_bit0 -CO100354_bit0 -CO100355_bit0 -CO100356_bit0 -CO100357_bit0 -CO100358_bit0 -CO100359_bit0 -CO100360_bit0 -CO100361_bit0 -CO100362_bit0 -CO100363_bit0 -CO100364_bit0 -CO100365_bit0 -CO100366_bit0 -CO100367_bit0 -CO100368_bit0 -CO100369_bit0 -CO100370_bit0 -CO100371_bit0 -CO100372_bit0 -CO100373_bit0 -CO100374_bit0 -CO100375_bit0 -CO100376_bit0 -CO100377_bit0 -CO100378_bit0 -CO100379_bit0 -CO100380_bit0 -CO100381_bit0 -CO100382_bit0 -CO100383_bit0 -CO100384_bit0 -CO100385_bit0 -CO100386_bit0 -CO100387_bit0 -CO100388_bit0 -CO100389_bit0 -CO100390_bit0 -CO100391_bit0 -CO100392_bit0 -CO100393_bit0 -CO100394_bit0 -CO100395_bit0 -CO100396_bit0 -CO100397_bit0 -CO100398_bit0 -CO100399_bit0 -CO100400_bit0 -CO100401_bit0 -CO100402_bit0 -CO100403_bit0 -CO100404_bit0 -CO100405_bit0 -CO100406_bit0 CO100407_bit0 -CO100408_bit0 -CO100409_bit0 -CO100410_bit0 -CO100411_bit0 -CO100412_bit0 -CO100413_bit0 -CO100414_bit0 -CO100415_bit0 -CO100416_bit0 -CO100417_bit0 -CO100418_bit0 -CO100419_bit0 -CO100420_bit0 -CO100421_bit0 -CO100422_bit0 -CO100423_bit0 -CO100424_bit0 -CO100425_bit0 -CO100426_bit0 -CO100427_bit0 -CO100428_bit0 -CO100429_bit0 -CO100430_bit0 -CO100431_bit0 -CO100432_bit0 -CO100433_bit0 -CO100434_bit0 -CO100435_bit0 -CO100436_bit0 -CO100437_bit0 -CO100438_bit0 -CO100439_bit0 -CO100440_bit0 -CO100441_bit0 -CO100442_bit0 -CO100443_bit0 -CO100444_bit0 -CO100445_bit0 CO100446_bit0 -CO100447_bit0 -CO100448_bit0 -CO100449_bit0 -CO100450_bit0 -CO100451_bit0 -CO100452_bit0 -CO100453_bit0 -CO100454_bit0 -CO100455_bit0 -CO100456_bit0 -CO100457_bit0 -CO100458_bit0 -CO100459_bit0 -CO100460_bit0 -CO100461_bit0 -CO100462_bit0 -CO100463_bit0 -CO100464_bit0 -CO100465_bit0 -CO100466_bit0 -CO100467_bit0 -CO100468_bit0 -CO100469_bit0 -CO100470_bit0 -CO100471_bit0 -CO100472_bit0 -CO100473_bit0 -CO100474_bit0 -CO100475_bit0 -CO100476_bit0 -CO100477_bit0 -CO100478_bit0 -CO100479_bit0 -CO100480_bit0 -CO100481_bit0 -CO100482_bit0 -CO100483_bit0 -CO100484_bit0 -CO100485_bit0 -CO100486_bit0 -CO100487_bit0 -CO100488_bit0 -CO100489_bit0 -CO100490_bit0 -CO100491_bit0 -CO100492_bit0 -CO100493_bit0 -CO100494_bit0 -CO100495_bit0 -CO100496_bit0 -CO100497_bit0 -CO100498_bit0 -CO100499_bit0 -CO100500_bit0 -CO100501_bit0 -CO100502_bit0 -CO100503_bit0 -CO100504_bit0 -CO100505_bit0 -CO100506_bit0 -CO100507_bit0 -CO100508_bit0 -CO100509_bit0 CO100510_bit0 -CO100511_bit0 -CO100512_bit0 -CO100513_bit0 -CO100514_bit0 -CO100515_bit0 -CO100516_bit0 -CO100517_bit0 -CO100518_bit0 -CO100519_bit0 -CO100520_bit0 -CO100521_bit0 -CO100522_bit0 -CO100523_bit0 -CO100524_bit0 -CO100525_bit0 -CO100526_bit0 -CO100527_bit0 -CO100528_bit0 -CO100529_bit0 -CO100530_bit0 -CO100531_bit0 -CO100532_bit0 -CO100533_bit0 -CO100534_bit0 -CO100535_bit0 -CO100536_bit0 -CO100537_bit0 -CO100538_bit0 -CO100539_bit0 -CO100540_bit0 -CO100541_bit0 -CO100542_bit0 -CO100543_bit0 -CO100544_bit0 -CO100545_bit0 -CO100546_bit0 -CO100547_bit0 -CO100548_bit0 -CO100549_bit0 -CO100550_bit0 -CO100551_bit0 CO100552_bit0 -CO100553_bit0 -CO100554_bit0 -CO100555_bit0 -CO100556_bit0 -CO100557_bit0 -CO100558_bit0 -CO100559_bit0 -CO100560_bit0 -CO100561_bit0 -CO100562_bit0 -CO100563_bit0 -CO100564_bit0 -CO100565_bit0 -CO100566_bit0 -CO100567_bit0 -CO100568_bit0 -CO100569_bit0 -CO100570_bit0 -CO100571_bit0 -CO100572_bit0 CO100573_bit0 -CO100574_bit0 -CO100575_bit0 -CO100576_bit0 -CO100577_bit0 -CO100578_bit0 -CO100579_bit0 -CO100580_bit0 -CO100581_bit0 -CO100582_bit0 -CO100583_bit0 -CO100584_bit0 -CO100585_bit0 -CO100586_bit0 -CO100587_bit0 -CO100588_bit0 -CO100589_bit0 -CO100590_bit0 -CO100591_bit0 -CO100592_bit0 -CO100593_bit0 -CO100594_bit0 -CO100595_bit0 -CO100596_bit0 -CO100597_bit0 -CO100598_bit0 -CO100599_bit0 -CO100600_bit0 -CO100601_bit0 -CO100602_bit0 -CO100603_bit0 -CO100604_bit0 -CO100605_bit0 -CO100606_bit0 -CO100607_bit0 -CO100608_bit0 -CO100609_bit0 -CO100610_bit0 -CO100611_bit0 -CO100612_bit0 -CO100613_bit0 -CO100614_bit0 -CO100615_bit0 -CO100616_bit0 -CO100617_bit0 -CO100618_bit0 -CO100619_bit0 -CO100620_bit0 -CO100621_bit0 -CO100622_bit0 -CO100623_bit0 -CO100624_bit0 -CO100625_bit0 -CO100626_bit0 -CO100627_bit0 -CO100628_bit0 -CO100629_bit0 -CO100630_bit0 -CO100631_bit0 -CO100632_bit0 -CO100633_bit0 -CO100634_bit0 -CO100635_bit0 -CO100636_bit0 -CO100637_bit0 -CO100638_bit0 -CO100639_bit0 -CO100640_bit0 -CO100641_bit0 -CO100642_bit0 -CO100643_bit0 -CO100644_bit0 -CO100645_bit0 -CO100646_bit0 -CO100647_bit0 -CO100648_bit0 -CO100649_bit0 -CO100650_bit0 -CO100651_bit0 -CO100652_bit0 -CO100653_bit0 -CO100654_bit0 -CO100655_bit0 -CO100656_bit0 -CO100657_bit0 -CO100658_bit0 -CO100659_bit0 -CO100660_bit0 -CO100661_bit0 -CO100662_bit0 -CO100663_bit0 -CO100664_bit0 -CO100665_bit0 -CO100666_bit0 -CO100667_bit0 -CO100668_bit0 -CO100669_bit0 -CO100670_bit0 -CO100671_bit0 -CO100672_bit0 -CO100673_bit0 -CO100674_bit0 -CO100675_bit0 -CO100676_bit0 -CO100677_bit0 -CO100678_bit0 -CO100679_bit0 -CO100680_bit0 -CO100681_bit0 -CO100682_bit0 -CO100683_bit0 -CO100684_bit0 -CO100685_bit0 -CO100686_bit0 -CO100687_bit0 -CO100688_bit0 -CO100689_bit0 -CO100690_bit0 -CO100691_bit0 -CO100692_bit0 -CO100693_bit0 -CO100694_bit0 -CO100695_bit0 -CO100696_bit0 -CO100697_bit0 -CO100698_bit0 -CO100699_bit0 -CO100700_bit0 -CO100701_bit0 -CO100702_bit0 -CO100703_bit0 CO100704_bit0 -CO100705_bit0 -CO100706_bit0 -CO100707_bit0 -CO100708_bit0 -CO100709_bit0 -CO100710_bit0 -CO100711_bit0 -CO100712_bit0 -CO100713_bit0 -CO100714_bit0 -CO100715_bit0 -CO100716_bit0 -CO100717_bit0 -CO100718_bit0 -CO100719_bit0 -CO100720_bit0 -CO100721_bit0 -CO100722_bit0 -CO100723_bit0 -CO100724_bit0 -CO100725_bit0 -CO100726_bit0 -CO100727_bit0 -CO100728_bit0 -CO100729_bit0 -CO100730_bit0 -CO100731_bit0 -CO100732_bit0 -CO100733_bit0 -CO100734_bit0 -CO100735_bit0 -CO100736_bit0 -CO100737_bit0 -CO100738_bit0 -CO100739_bit0 -CO100740_bit0 -CO100741_bit0 -CO100742_bit0 -CO100743_bit0 -CO100744_bit0 -CO100745_bit0 -CO100746_bit0 -CO100747_bit0 -CO100748_bit0 -CO100749_bit0 -CO100750_bit0 CO100751_bit0 -CO100752_bit0 -CO100753_bit0 -CO100754_bit0 -CO100755_bit0 -CO100756_bit0 -CO100757_bit0 -CO100758_bit0 CO100759_bit0 -CO100760_bit0 -CO100761_bit0 -CO100762_bit0 -CO100763_bit0 -CO100764_bit0 -CO100765_bit0 -CO100766_bit0 -CO100767_bit0 -CO100768_bit0 -CO100769_bit0 -CO100770_bit0 -CO100771_bit0 -CO100772_bit0 -CO100773_bit0 -CO100774_bit0 -CO100775_bit0 -CO100776_bit0 -CO100777_bit0 -CO100778_bit0 -CO100779_bit0 -CO100780_bit0 -CO100781_bit0 -CO100782_bit0 -CO100783_bit0 -CO100784_bit0 -CO100785_bit0 -CO100786_bit0 -CO100787_bit0 -CO100788_bit0 -CO100789_bit0 -CO100790_bit0 -CO100791_bit0 -CO100792_bit0 -CO100793_bit0 -CO100794_bit0 -CO100795_bit0 -CO100796_bit0 -CO100797_bit0 -CO100798_bit0 -CO100799_bit0 -CO100800_bit0 -CO100801_bit0 -CO100802_bit0 -CO100803_bit0 -CO100804_bit0 -CO100805_bit0 -CO100806_bit0 -CO100807_bit0 -CO100808_bit0 -CO100809_bit0 -CO100810_bit0 -CO100811_bit0 -CO100812_bit0 -CO100813_bit0 -CO100814_bit0 -CO100815_bit0 -CO100816_bit0 -CO100817_bit0 -CO100818_bit0
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/19907/stat): 19907 (minisat+_script) R 19906 19907 5299 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1846539733 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/19907/statm): 174 3 169 147 0 27 0 [pid=19907] 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=19908 New process pid=19909 New process pid=19910 execve syscall for /bin/sed executable One traced child (pid=19909) 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=19910) exited with status: 0 One traced child (pid=19908) exited with status: 0 New process pid=19911 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-lp4l.opb [startup+10.0036 s] Raw data (loadavg): 0.93 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 2434 0 0 0 973 10 0 0 25 0 1 0 1846539738 10838016 2293 4294967295 134512640 135094434 3221224432 3221223024 134556843 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19911/statm): 2646 2293 145 145 0 2501 0 [pid=19911] vsize: 10584 Current children cumulated CPU time (s) 9.85 Current children cumulated vsize (Kb) 12708 [startup+20.0052 s] Raw data (loadavg): 0.94 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 6865 0 0 0 1941 27 0 0 25 0 1 0 1846539738 28241920 6042 4294967295 134512640 135094434 3221224432 3221223088 134558426 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19911/statm): 6895 6042 145 145 0 6750 0 [pid=19911] vsize: 27580 Current children cumulated CPU time (s) 19.7 Current children cumulated vsize (Kb) 29704 [startup+30.0059 s] Raw data (loadavg): 0.95 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 7444 0 0 0 2936 30 0 0 25 0 1 0 1846539738 29216768 6282 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19911/statm): 7133 6282 145 145 0 6988 0 [pid=19911] vsize: 28532 Current children cumulated CPU time (s) 29.68 Current children cumulated vsize (Kb) 30656 [startup+40.0075 s] Raw data (loadavg): 0.96 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 7828 0 0 0 3926 34 0 0 25 0 1 0 1846539738 30777344 6666 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19911/statm): 7514 6666 145 145 0 7369 0 [pid=19911] vsize: 30056 Current children cumulated CPU time (s) 39.62 Current children cumulated vsize (Kb) 32180 [startup+50.0091 s] Raw data (loadavg): 0.96 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 8294 0 0 0 4919 37 0 0 25 0 1 0 1846539738 32673792 7132 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19911/statm): 7977 7132 145 145 0 7832 0 [pid=19911] vsize: 31908 Current children cumulated CPU time (s) 49.58 Current children cumulated vsize (Kb) 34032 [startup+60.0098 s] Raw data (loadavg): 0.97 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 8820 0 0 0 5908 42 0 0 25 0 1 0 1846539738 34881536 7658 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19911/statm): 8516 7658 145 145 0 8371 0 [pid=19911] vsize: 34064 Current children cumulated CPU time (s) 59.52 Current children cumulated vsize (Kb) 36188 [startup+70.0114 s] Raw data (loadavg): 0.97 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 9394 0 0 0 6898 46 0 0 25 0 1 0 1846539738 37224448 8232 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19911/statm): 9088 8232 145 145 0 8943 0 [pid=19911] vsize: 36352 Current children cumulated CPU time (s) 69.46 Current children cumulated vsize (Kb) 38476 [startup+80.0131 s] Raw data (loadavg): 0.98 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 9883 0 0 0 7891 50 0 0 25 0 1 0 1846539738 38354944 8510 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19911/statm): 9364 8510 145 145 0 9219 0 [pid=19911] vsize: 37456 Current children cumulated CPU time (s) 79.43 Current children cumulated vsize (Kb) 39580 [startup+90.0137 s] Raw data (loadavg): 0.98 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 10302 0 0 0 8883 53 0 0 25 0 1 0 1846539738 40062976 8929 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19911/statm): 9781 8929 145 145 0 9636 0 [pid=19911] vsize: 39124 Current children cumulated CPU time (s) 89.38 Current children cumulated vsize (Kb) 41248 [startup+100.014 s] Raw data (loadavg): 0.98 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 10749 0 0 0 9874 58 0 0 25 0 1 0 1846539738 41881600 9376 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19911/statm): 10225 9376 145 145 0 10080 0 [pid=19911] vsize: 40900 Current children cumulated CPU time (s) 99.34 Current children cumulated vsize (Kb) 43024 [startup+110.017 s] Raw data (loadavg): 0.98 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 11311 0 0 0 10864 63 0 0 25 0 1 0 1846539738 44175360 9938 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 10785 9938 145 145 0 10640 0 [pid=19911] vsize: 43140 Current children cumulated CPU time (s) 109.29 Current children cumulated vsize (Kb) 45264 [startup+120.018 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 11617 0 0 0 11859 64 0 0 25 0 1 0 1846539738 45420544 10244 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 11089 10244 145 145 0 10944 0 [pid=19911] vsize: 44356 Current children cumulated CPU time (s) 119.25 Current children cumulated vsize (Kb) 46480 [startup+130.018 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 11938 0 0 0 12854 66 0 0 25 0 1 0 1846539738 46858240 10565 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 11440 10565 145 145 0 11295 0 [pid=19911] vsize: 45760 Current children cumulated CPU time (s) 129.22 Current children cumulated vsize (Kb) 47884 [startup+140.02 s] Raw data (loadavg): 0.99 0.98 0.99 3/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 12414 0 0 0 13843 70 0 0 25 0 1 0 1846539738 48803840 11041 4294967295 134512640 135094434 3221224432 3221222896 134790884 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19911/statm): 11915 11041 145 145 0 11770 0 [pid=19911] vsize: 47660 Current children cumulated CPU time (s) 139.15 Current children cumulated vsize (Kb) 49784 [startup+150.02 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 12929 0 0 0 14832 75 0 0 25 0 1 0 1846539738 50905088 11556 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 12428 11556 145 145 0 12283 0 [pid=19911] vsize: 49712 Current children cumulated CPU time (s) 149.09 Current children cumulated vsize (Kb) 51836 [startup+160.021 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 13333 0 0 0 15825 77 0 0 19 0 1 0 1846539738 52551680 11960 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19911/statm): 12830 11960 145 145 0 12685 0 [pid=19911] vsize: 51320 Current children cumulated CPU time (s) 159.04 Current children cumulated vsize (Kb) 53444 [startup+170.023 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 13738 0 0 0 16816 81 0 0 25 0 1 0 1846539738 54206464 12365 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 13234 12365 145 145 0 13089 0 [pid=19911] vsize: 52936 Current children cumulated CPU time (s) 168.99 Current children cumulated vsize (Kb) 55060 [startup+180.023 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 14190 0 0 0 17809 83 0 0 25 0 1 0 1846539738 56049664 12817 4294967295 134512640 135094434 3221224432 3221222960 134783013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 13684 12817 145 145 0 13539 0 [pid=19911] vsize: 54736 Current children cumulated CPU time (s) 178.94 Current children cumulated vsize (Kb) 56860 [startup+190.025 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 14688 0 0 0 18800 86 0 0 25 0 1 0 1846539738 58081280 13315 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 14180 13315 145 145 0 14035 0 [pid=19911] vsize: 56720 Current children cumulated CPU time (s) 188.88 Current children cumulated vsize (Kb) 58844 [startup+200.026 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 15148 0 0 0 19792 89 0 0 25 0 1 0 1846539738 59961344 13775 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19911/statm): 14639 13775 145 145 0 14494 0 [pid=19911] vsize: 58556 Current children cumulated CPU time (s) 198.83 Current children cumulated vsize (Kb) 60680 [startup+210.026 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 15488 0 0 0 20786 93 0 0 25 0 1 0 1846539738 61345792 14115 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19911/statm): 14977 14115 145 145 0 14832 0 [pid=19911] vsize: 59908 Current children cumulated CPU time (s) 208.81 Current children cumulated vsize (Kb) 62032 [startup+220.028 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 15924 0 0 0 21777 96 0 0 25 0 1 0 1846539738 63123456 14551 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19911/statm): 15411 14551 145 145 0 15266 0 [pid=19911] vsize: 61644 Current children cumulated CPU time (s) 218.75 Current children cumulated vsize (Kb) 63768 [startup+230.029 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 16395 0 0 0 22769 99 0 0 25 0 1 0 1846539738 65044480 15022 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19911/statm): 15880 15022 145 145 0 15735 0 [pid=19911] vsize: 63520 Current children cumulated CPU time (s) 228.7 Current children cumulated vsize (Kb) 65644 [startup+240.029 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 16827 0 0 0 23760 102 0 0 25 0 1 0 1846539738 66809856 15454 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19911/statm): 16311 15454 145 145 0 16166 0 [pid=19911] vsize: 65244 Current children cumulated CPU time (s) 238.64 Current children cumulated vsize (Kb) 67368 [startup+250.031 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 17282 0 0 0 24752 105 0 0 25 0 1 0 1846539738 68669440 15909 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 16765 15909 145 145 0 16620 0 [pid=19911] vsize: 67060 Current children cumulated CPU time (s) 248.59 Current children cumulated vsize (Kb) 69184 [startup+260.032 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 17697 0 0 0 25746 109 0 0 25 0 1 0 1846539738 70365184 16324 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 17179 16324 145 145 0 17034 0 [pid=19911] vsize: 68716 Current children cumulated CPU time (s) 258.57 Current children cumulated vsize (Kb) 70840 [startup+270.032 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 18201 0 0 0 26738 112 0 0 25 0 1 0 1846539738 72421376 16828 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19911/statm): 17681 16828 145 145 0 17536 0 [pid=19911] vsize: 70724 Current children cumulated CPU time (s) 268.52 Current children cumulated vsize (Kb) 72848 [startup+280.033 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 18694 0 0 0 27732 115 0 0 25 0 1 0 1846539738 73830400 17174 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 18025 17174 145 145 0 17880 0 [pid=19911] vsize: 72100 Current children cumulated CPU time (s) 278.49 Current children cumulated vsize (Kb) 74224 [startup+290.034 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 18694 0 0 0 28732 115 0 0 25 0 1 0 1846539738 73830400 17174 4294967295 134512640 135094434 3221224432 3221223024 134557522 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 18025 17174 145 145 0 17880 0 [pid=19911] vsize: 72100 Current children cumulated CPU time (s) 288.49 Current children cumulated vsize (Kb) 74224 [startup+300.035 s] Raw data (loadavg): 0.99 0.98 0.99 3/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 18694 0 0 0 29733 115 0 0 25 0 1 0 1846539738 73830400 17174 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 18025 17174 145 145 0 17880 0 [pid=19911] vsize: 72100 Current children cumulated CPU time (s) 298.5 Current children cumulated vsize (Kb) 74224 [startup+310.036 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 18694 0 0 0 30733 115 0 0 25 0 1 0 1846539738 73830400 17174 4294967295 134512640 135094434 3221224432 3221222160 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 18025 17174 145 145 0 17880 0 [pid=19911] vsize: 72100 Current children cumulated CPU time (s) 308.5 Current children cumulated vsize (Kb) 74224 [startup+320.037 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 18694 0 0 0 31733 115 0 0 25 0 1 0 1846539738 73830400 17174 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 18025 17174 145 145 0 17880 0 [pid=19911] vsize: 72100 Current children cumulated CPU time (s) 318.5 Current children cumulated vsize (Kb) 74224 [startup+330.038 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 18694 0 0 0 32733 115 0 0 25 0 1 0 1846539738 73830400 17174 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 18025 17174 145 145 0 17880 0 [pid=19911] vsize: 72100 Current children cumulated CPU time (s) 328.5 Current children cumulated vsize (Kb) 74224 [startup+340.039 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 18694 0 0 0 33734 115 0 0 25 0 1 0 1846539738 73830400 17174 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 18025 17174 145 145 0 17880 0 [pid=19911] vsize: 72100 Current children cumulated CPU time (s) 338.51 Current children cumulated vsize (Kb) 74224 [startup+350.039 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 18694 0 0 0 34734 115 0 0 25 0 1 0 1846539738 73830400 17174 4294967295 134512640 135094434 3221224432 3221223024 134778850 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 18025 17174 145 145 0 17880 0 [pid=19911] vsize: 72100 Current children cumulated CPU time (s) 348.51 Current children cumulated vsize (Kb) 74224 [startup+360.039 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 18694 0 0 0 35734 115 0 0 25 0 1 0 1846539738 73830400 17174 4294967295 134512640 135094434 3221224432 3221223024 134557500 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 18025 17174 145 145 0 17880 0 [pid=19911] vsize: 72100 Current children cumulated CPU time (s) 358.51 Current children cumulated vsize (Kb) 74224 [startup+370.041 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 18694 0 0 0 36734 115 0 0 25 0 1 0 1846539738 73830400 17174 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 18025 17174 145 145 0 17880 0 [pid=19911] vsize: 72100 Current children cumulated CPU time (s) 368.51 Current children cumulated vsize (Kb) 74224 [startup+380.041 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 18694 0 0 0 37734 115 0 0 25 0 1 0 1846539738 73830400 17174 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 18025 17174 145 145 0 17880 0 [pid=19911] vsize: 72100 Current children cumulated CPU time (s) 378.51 Current children cumulated vsize (Kb) 74224 [startup+390.042 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 18694 0 0 0 38735 115 0 0 25 0 1 0 1846539738 73830400 17174 4294967295 134512640 135094434 3221224432 3221223024 134557287 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 18025 17174 145 145 0 17880 0 [pid=19911] vsize: 72100 Current children cumulated CPU time (s) 388.52 Current children cumulated vsize (Kb) 74224 [startup+400.043 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 18694 0 0 0 39735 115 0 0 25 0 1 0 1846539738 73830400 17174 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 18025 17174 145 145 0 17880 0 [pid=19911] vsize: 72100 Current children cumulated CPU time (s) 398.52 Current children cumulated vsize (Kb) 74224 [startup+410.043 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 18694 0 0 0 40735 115 0 0 25 0 1 0 1846539738 73830400 17174 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 18025 17174 145 145 0 17880 0 [pid=19911] vsize: 72100 Current children cumulated CPU time (s) 408.52 Current children cumulated vsize (Kb) 74224 [startup+420.044 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 18695 0 0 0 41735 115 0 0 25 0 1 0 1846539738 73830400 17175 4294967295 134512640 135094434 3221224432 3221223024 134556853 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 18025 17175 145 145 0 17880 0 [pid=19911] vsize: 72100 Current children cumulated CPU time (s) 418.52 Current children cumulated vsize (Kb) 74224 [startup+430.044 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 18695 0 0 0 42736 115 0 0 25 0 1 0 1846539738 73830400 17175 4294967295 134512640 135094434 3221224432 3221223024 134557002 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 18025 17175 145 145 0 17880 0 [pid=19911] vsize: 72100 Current children cumulated CPU time (s) 428.53 Current children cumulated vsize (Kb) 74224 [startup+440.044 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 18695 0 0 0 43736 115 0 0 25 0 1 0 1846539738 73830400 17175 4294967295 134512640 135094434 3221224432 3221223104 134555599 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 18025 17175 145 145 0 17880 0 [pid=19911] vsize: 72100 Current children cumulated CPU time (s) 438.53 Current children cumulated vsize (Kb) 74224 [startup+450.045 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 18695 0 0 0 44736 115 0 0 25 0 1 0 1846539738 73830400 17175 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 18025 17175 145 145 0 17880 0 [pid=19911] vsize: 72100 Current children cumulated CPU time (s) 448.53 Current children cumulated vsize (Kb) 74224 [startup+460.045 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 18900 0 0 0 45734 116 0 0 25 0 1 0 1846539738 74670080 17380 4294967295 134512640 135094434 3221224432 3221223072 134558043 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 18230 17380 145 145 0 18085 0 [pid=19911] vsize: 72920 Current children cumulated CPU time (s) 458.52 Current children cumulated vsize (Kb) 75044 [startup+470.046 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 19427 0 0 0 46731 117 0 0 25 0 1 0 1846539738 75071488 17479 4294967295 134512640 135094434 3221224432 3221223044 134563130 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 18328 17479 145 145 0 18183 0 [pid=19911] vsize: 73312 Current children cumulated CPU time (s) 468.5 Current children cumulated vsize (Kb) 75436 [startup+480.047 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 19427 0 0 0 47731 117 0 0 25 0 1 0 1846539738 75071488 17479 4294967295 134512640 135094434 3221224432 3221223120 134554788 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 18328 17479 145 145 0 18183 0 [pid=19911] vsize: 73312 Current children cumulated CPU time (s) 478.5 Current children cumulated vsize (Kb) 75436 [startup+490.047 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 19427 0 0 0 48731 117 0 0 25 0 1 0 1846539738 75071488 17479 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 18328 17479 145 145 0 18183 0 [pid=19911] vsize: 73312 Current children cumulated CPU time (s) 488.5 Current children cumulated vsize (Kb) 75436 [startup+500.048 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 19427 0 0 0 49731 117 0 0 25 0 1 0 1846539738 75071488 17479 4294967295 134512640 135094434 3221224432 3221223088 134558392 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 18328 17479 145 145 0 18183 0 [pid=19911] vsize: 73312 Current children cumulated CPU time (s) 498.5 Current children cumulated vsize (Kb) 75436 [startup+510.048 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 19427 0 0 0 50731 118 0 0 25 0 1 0 1846539738 75071488 17479 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 18328 17479 145 145 0 18183 0 [pid=19911] vsize: 73312 Current children cumulated CPU time (s) 508.51 Current children cumulated vsize (Kb) 75436 [startup+520.048 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 19427 0 0 0 51732 118 0 0 25 0 1 0 1846539738 75071488 17479 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 18328 17479 145 145 0 18183 0 [pid=19911] vsize: 73312 Current children cumulated CPU time (s) 518.52 Current children cumulated vsize (Kb) 75436 [startup+530.049 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 19427 0 0 0 52732 118 0 0 25 0 1 0 1846539738 75071488 17479 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 18328 17479 145 145 0 18183 0 [pid=19911] vsize: 73312 Current children cumulated CPU time (s) 528.52 Current children cumulated vsize (Kb) 75436 [startup+540.048 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 19427 0 0 0 53732 118 0 0 25 0 1 0 1846539738 75071488 17479 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 18328 17479 145 145 0 18183 0 [pid=19911] vsize: 73312 Current children cumulated CPU time (s) 538.52 Current children cumulated vsize (Kb) 75436 [startup+550.049 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 19427 0 0 0 54732 118 0 0 25 0 1 0 1846539738 75071488 17479 4294967295 134512640 135094434 3221224432 3221223064 134557638 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 18328 17479 145 145 0 18183 0 [pid=19911] vsize: 73312 Current children cumulated CPU time (s) 548.52 Current children cumulated vsize (Kb) 75436 [startup+560.05 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 19427 0 0 0 55732 118 0 0 25 0 1 0 1846539738 75071488 17479 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 18328 17479 145 145 0 18183 0 [pid=19911] vsize: 73312 Current children cumulated CPU time (s) 558.52 Current children cumulated vsize (Kb) 75436 [startup+570.05 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 19427 0 0 0 56733 118 0 0 25 0 1 0 1846539738 75071488 17479 4294967295 134512640 135094434 3221224432 3221223104 134556543 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 18328 17479 145 145 0 18183 0 [pid=19911] vsize: 73312 Current children cumulated CPU time (s) 568.53 Current children cumulated vsize (Kb) 75436 [startup+580.051 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 19427 0 0 0 57733 118 0 0 25 0 1 0 1846539738 75071488 17479 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 18328 17479 145 145 0 18183 0 [pid=19911] vsize: 73312 Current children cumulated CPU time (s) 578.53 Current children cumulated vsize (Kb) 75436 [startup+590.052 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 19427 0 0 0 58733 118 0 0 25 0 1 0 1846539738 75071488 17479 4294967295 134512640 135094434 3221224432 3221223104 134555570 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 18328 17479 145 145 0 18183 0 [pid=19911] vsize: 73312 Current children cumulated CPU time (s) 588.53 Current children cumulated vsize (Kb) 75436 [startup+600.052 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 19427 0 0 0 59733 118 0 0 25 0 1 0 1846539738 75071488 17479 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 18328 17479 145 145 0 18183 0 [pid=19911] vsize: 73312 Current children cumulated CPU time (s) 598.53 Current children cumulated vsize (Kb) 75436 [startup+610.053 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 19466 0 0 0 60733 118 0 0 25 0 1 0 1846539738 75231232 17518 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 18367 17518 145 145 0 18222 0 [pid=19911] vsize: 73468 Current children cumulated CPU time (s) 608.53 Current children cumulated vsize (Kb) 75592 [startup+620.054 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 19981 0 0 0 61726 121 0 0 25 0 1 0 1846539738 77340672 18033 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 18882 18033 145 145 0 18737 0 [pid=19911] vsize: 75528 Current children cumulated CPU time (s) 618.49 Current children cumulated vsize (Kb) 77652 [startup+630.054 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 20533 0 0 0 62717 124 0 0 25 0 1 0 1846539738 79601664 18585 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 19434 18585 145 145 0 19289 0 [pid=19911] vsize: 77736 Current children cumulated CPU time (s) 628.43 Current children cumulated vsize (Kb) 79860 [startup+640.054 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 21040 0 0 0 63709 128 0 0 25 0 1 0 1846539738 81678336 19092 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 19941 19092 145 145 0 19796 0 [pid=19911] vsize: 79764 Current children cumulated CPU time (s) 638.39 Current children cumulated vsize (Kb) 81888 [startup+650.055 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 21598 0 0 0 64702 130 0 0 25 0 1 0 1846539738 83963904 19650 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19911/statm): 20499 19650 145 145 0 20354 0 [pid=19911] vsize: 81996 Current children cumulated CPU time (s) 648.34 Current children cumulated vsize (Kb) 84120 [startup+660.055 s] Raw data (loadavg): 0.99 0.98 0.99 3/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 22304 0 0 0 65696 133 0 0 25 0 1 0 1846539738 86855680 20356 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19911/statm): 21205 20356 145 145 0 21060 0 [pid=19911] vsize: 84820 Current children cumulated CPU time (s) 658.31 Current children cumulated vsize (Kb) 86944 [startup+670.057 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 22674 0 0 0 66689 136 0 0 25 0 1 0 1846539738 88371200 20726 4294967295 134512640 135094434 3221224432 3221223024 134556990 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19911/statm): 21575 20726 145 145 0 21430 0 [pid=19911] vsize: 86300 Current children cumulated CPU time (s) 668.27 Current children cumulated vsize (Kb) 88424 [startup+680.058 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 23147 0 0 0 67681 140 0 0 25 0 1 0 1846539738 90308608 21199 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19911/statm): 22048 21199 145 145 0 21903 0 [pid=19911] vsize: 88192 Current children cumulated CPU time (s) 678.23 Current children cumulated vsize (Kb) 90316 [startup+690.057 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 23546 0 0 0 68673 142 0 0 25 0 1 0 1846539738 91942912 21598 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19911/statm): 22447 21598 145 145 0 22302 0 [pid=19911] vsize: 89788 Current children cumulated CPU time (s) 688.17 Current children cumulated vsize (Kb) 91912 [startup+700.059 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 23958 0 0 0 69665 146 0 0 25 0 1 0 1846539738 93630464 22010 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19911/statm): 22859 22010 145 145 0 22714 0 [pid=19911] vsize: 91436 Current children cumulated CPU time (s) 698.13 Current children cumulated vsize (Kb) 93560 [startup+710.059 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 24514 0 0 0 70655 151 0 0 25 0 1 0 1846539738 95903744 22566 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19911/statm): 23414 22566 145 145 0 23269 0 [pid=19911] vsize: 93656 Current children cumulated CPU time (s) 708.08 Current children cumulated vsize (Kb) 95780 [startup+720.06 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 25131 0 0 0 71649 153 0 0 25 0 1 0 1846539738 98426880 23183 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19911/statm): 24030 23183 145 145 0 23885 0 [pid=19911] vsize: 96120 Current children cumulated CPU time (s) 718.04 Current children cumulated vsize (Kb) 98244 [startup+730.062 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 25688 0 0 0 72642 156 0 0 25 0 1 0 1846539738 100704256 23740 4294967295 134512640 135094434 3221224432 3221223024 134557236 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 24586 23740 145 145 0 24441 0 [pid=19911] vsize: 98344 Current children cumulated CPU time (s) 728 Current children cumulated vsize (Kb) 100468 [startup+740.062 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 26173 0 0 0 73636 158 0 0 25 0 1 0 1846539738 102686720 24225 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 25070 24225 145 145 0 24925 0 [pid=19911] vsize: 100280 Current children cumulated CPU time (s) 737.96 Current children cumulated vsize (Kb) 102404 [startup+750.063 s] Raw data (loadavg): 0.99 0.98 0.99 3/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 26574 0 0 0 74627 162 0 0 25 0 1 0 1846539738 104325120 24626 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 25470 24626 145 145 0 25325 0 [pid=19911] vsize: 101880 Current children cumulated CPU time (s) 747.91 Current children cumulated vsize (Kb) 104004 [startup+760.064 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 26997 0 0 0 75619 165 0 0 25 0 1 0 1846539738 106311680 25049 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 25955 25049 145 145 0 25810 0 [pid=19911] vsize: 103820 Current children cumulated CPU time (s) 757.86 Current children cumulated vsize (Kb) 105944 [startup+770.065 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 27504 0 0 0 76611 168 0 0 25 0 1 0 1846539738 108384256 25556 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 26461 25556 145 145 0 26316 0 [pid=19911] vsize: 105844 Current children cumulated CPU time (s) 767.81 Current children cumulated vsize (Kb) 107968 [startup+780.066 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 27958 0 0 0 77603 171 0 0 25 0 1 0 1846539738 110239744 26010 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 26914 26010 145 145 0 26769 0 [pid=19911] vsize: 107656 Current children cumulated CPU time (s) 777.76 Current children cumulated vsize (Kb) 109780 [startup+790.067 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 28371 0 0 0 78596 174 0 0 25 0 1 0 1846539738 111927296 26423 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 27326 26423 145 145 0 27181 0 [pid=19911] vsize: 109304 Current children cumulated CPU time (s) 787.72 Current children cumulated vsize (Kb) 111428 [startup+800.068 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 29063 0 0 0 79589 178 0 0 25 0 1 0 1846539738 114753536 27115 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 28016 27115 145 145 0 27871 0 [pid=19911] vsize: 112064 Current children cumulated CPU time (s) 797.69 Current children cumulated vsize (Kb) 114188 [startup+810.068 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 29832 0 0 0 80580 182 0 0 25 0 1 0 1846539738 117899264 27884 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 28784 27884 145 145 0 28639 0 [pid=19911] vsize: 115136 Current children cumulated CPU time (s) 807.64 Current children cumulated vsize (Kb) 117260 [startup+820.068 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 30426 0 0 0 81573 184 0 0 25 0 1 0 1846539738 120328192 28478 4294967295 134512640 135094434 3221224432 3221222896 134781535 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 29377 28478 145 145 0 29232 0 [pid=19911] vsize: 117508 Current children cumulated CPU time (s) 817.59 Current children cumulated vsize (Kb) 119632 [startup+830.069 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 30901 0 0 0 82566 187 0 0 25 0 1 0 1846539738 122265600 28953 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 29850 28953 145 145 0 29705 0 [pid=19911] vsize: 119400 Current children cumulated CPU time (s) 827.55 Current children cumulated vsize (Kb) 121524 [startup+840.069 s] Raw data (loadavg): 0.99 0.98 0.99 3/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 31346 0 0 0 83558 190 0 0 25 0 1 0 1846539738 124084224 29398 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 30294 29398 145 145 0 30149 0 [pid=19911] vsize: 121176 Current children cumulated CPU time (s) 837.5 Current children cumulated vsize (Kb) 123300 [startup+850.069 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 31729 0 0 0 84551 194 0 0 25 0 1 0 1846539738 125648896 29781 4294967295 134512640 135094434 3221224432 3221223024 134557002 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19911/statm): 30676 29781 145 145 0 30531 0 [pid=19911] vsize: 122704 Current children cumulated CPU time (s) 847.47 Current children cumulated vsize (Kb) 124828 [startup+860.07 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 32081 0 0 0 85544 197 0 0 25 0 1 0 1846539738 127082496 30133 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 31026 30133 145 145 0 30881 0 [pid=19911] vsize: 124104 Current children cumulated CPU time (s) 857.43 Current children cumulated vsize (Kb) 126228 [startup+870.071 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 32452 0 0 0 86538 199 0 0 25 0 1 0 1846539738 128602112 30504 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 31397 30504 145 145 0 31252 0 [pid=19911] vsize: 125588 Current children cumulated CPU time (s) 867.39 Current children cumulated vsize (Kb) 127712 [startup+880.071 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 32875 0 0 0 87533 201 0 0 25 0 1 0 1846539738 130326528 30927 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 31818 30927 145 145 0 31673 0 [pid=19911] vsize: 127272 Current children cumulated CPU time (s) 877.36 Current children cumulated vsize (Kb) 129396 [startup+890.071 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 33298 0 0 0 88527 204 0 0 25 0 1 0 1846539738 132055040 31350 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 32240 31350 145 145 0 32095 0 [pid=19911] vsize: 128960 Current children cumulated CPU time (s) 887.33 Current children cumulated vsize (Kb) 131084 [startup+900.072 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 33664 0 0 0 89522 205 0 0 25 0 1 0 1846539738 133550080 31716 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 32605 31716 145 145 0 32460 0 [pid=19911] vsize: 130420 Current children cumulated CPU time (s) 897.29 Current children cumulated vsize (Kb) 132544 [startup+910.072 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 34026 0 0 0 90517 208 0 0 25 0 1 0 1846539738 135028736 32078 4294967295 134512640 135094434 3221224432 3221223088 134557956 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 32966 32078 145 145 0 32821 0 [pid=19911] vsize: 131864 Current children cumulated CPU time (s) 907.27 Current children cumulated vsize (Kb) 133988 [startup+920.073 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 34414 0 0 0 91512 210 0 0 25 0 1 0 1846539738 136613888 32466 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19911/statm): 33353 32466 145 145 0 33208 0 [pid=19911] vsize: 133412 Current children cumulated CPU time (s) 917.24 Current children cumulated vsize (Kb) 135536 [startup+930.073 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 34808 0 0 0 92506 213 0 0 25 0 1 0 1846539738 138223616 32860 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 33746 32860 145 145 0 33601 0 [pid=19911] vsize: 134984 Current children cumulated CPU time (s) 927.21 Current children cumulated vsize (Kb) 137108 [startup+940.074 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 35156 0 0 0 93500 215 0 0 25 0 1 0 1846539738 139644928 33208 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 34093 33208 145 145 0 33948 0 [pid=19911] vsize: 136372 Current children cumulated CPU time (s) 937.17 Current children cumulated vsize (Kb) 138496 [startup+950.075 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 35564 0 0 0 94494 217 0 0 25 0 1 0 1846539738 141312000 33616 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 34500 33616 145 145 0 34355 0 [pid=19911] vsize: 138000 Current children cumulated CPU time (s) 947.13 Current children cumulated vsize (Kb) 140124 [startup+960.075 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 35978 0 0 0 95489 219 0 0 25 0 1 0 1846539738 143003648 34030 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 34913 34030 145 145 0 34768 0 [pid=19911] vsize: 139652 Current children cumulated CPU time (s) 957.1 Current children cumulated vsize (Kb) 141776 [startup+970.077 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) T 19907 19907 5299 0 -1 0 36295 0 0 0 96484 221 0 0 25 0 1 0 1846539738 144297984 34347 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/19911/statm): 35229 34347 145 145 0 35084 0 [pid=19911] vsize: 140916 Current children cumulated CPU time (s) 967.07 Current children cumulated vsize (Kb) 143040 [startup+980.078 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 36581 0 0 0 97479 224 0 0 25 0 1 0 1846539738 145465344 34633 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 35514 34633 145 145 0 35369 0 [pid=19911] vsize: 142056 Current children cumulated CPU time (s) 977.05 Current children cumulated vsize (Kb) 144180 [startup+990.077 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 36985 0 0 0 98474 226 0 0 25 0 1 0 1846539738 147111936 35037 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 35916 35037 145 145 0 35771 0 [pid=19911] vsize: 143664 Current children cumulated CPU time (s) 987.02 Current children cumulated vsize (Kb) 145788 [startup+1000.08 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) T 19907 19907 5299 0 -1 0 37427 0 0 0 99468 228 0 0 25 0 1 0 1846539738 148918272 35479 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/19911/statm): 36357 35479 145 145 0 36212 0 [pid=19911] vsize: 145428 Current children cumulated CPU time (s) 996.98 Current children cumulated vsize (Kb) 147552 [startup+1010.08 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 37774 0 0 0 100463 230 0 0 25 0 1 0 1846539738 150335488 35826 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 36703 35826 145 145 0 36558 0 [pid=19911] vsize: 146812 Current children cumulated CPU time (s) 1006.95 Current children cumulated vsize (Kb) 148936 [startup+1020.08 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 38095 0 0 0 101458 233 0 0 25 0 1 0 1846539738 151646208 36147 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 37023 36147 145 145 0 36878 0 [pid=19911] vsize: 148092 Current children cumulated CPU time (s) 1016.93 Current children cumulated vsize (Kb) 150216 [startup+1030.08 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 38470 0 0 0 102452 236 0 0 25 0 1 0 1846539738 153178112 36522 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 37397 36522 145 145 0 37252 0 [pid=19911] vsize: 149588 Current children cumulated CPU time (s) 1026.9 Current children cumulated vsize (Kb) 151712 [startup+1040.08 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 38764 0 0 0 103446 238 0 0 25 0 1 0 1846539738 154378240 36816 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 37690 36816 145 145 0 37545 0 [pid=19911] vsize: 150760 Current children cumulated CPU time (s) 1036.86 Current children cumulated vsize (Kb) 152884 [startup+1050.08 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 39221 0 0 0 104439 241 0 0 25 0 1 0 1846539738 156246016 37273 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 38146 37273 145 145 0 38001 0 [pid=19911] vsize: 152584 Current children cumulated CPU time (s) 1046.82 Current children cumulated vsize (Kb) 154708 [startup+1060.08 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 39704 0 0 0 105433 244 0 0 25 0 1 0 1846539738 158220288 37756 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 38628 37756 145 145 0 38483 0 [pid=19911] vsize: 154512 Current children cumulated CPU time (s) 1056.79 Current children cumulated vsize (Kb) 156636 [startup+1070.08 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 40041 0 0 0 106427 247 0 0 25 0 1 0 1846539738 159600640 38093 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 38965 38093 145 145 0 38820 0 [pid=19911] vsize: 155860 Current children cumulated CPU time (s) 1066.76 Current children cumulated vsize (Kb) 157984 [startup+1080.08 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 40401 0 0 0 107423 249 0 0 25 0 1 0 1846539738 161067008 38453 4294967295 134512640 135094434 3221224432 3221223024 134557386 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 39323 38453 145 145 0 39178 0 [pid=19911] vsize: 157292 Current children cumulated CPU time (s) 1076.74 Current children cumulated vsize (Kb) 159416 [startup+1090.08 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 40853 0 0 0 108418 251 0 0 25 0 1 0 1846539738 162918400 38905 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 39775 38905 145 145 0 39630 0 [pid=19911] vsize: 159100 Current children cumulated CPU time (s) 1086.71 Current children cumulated vsize (Kb) 161224 [startup+1100.08 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 41238 0 0 0 109413 252 0 0 25 0 1 0 1846539738 164495360 39290 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 40160 39290 145 145 0 40015 0 [pid=19911] vsize: 160640 Current children cumulated CPU time (s) 1096.67 Current children cumulated vsize (Kb) 162764 [startup+1110.09 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 41484 0 0 0 110408 254 0 0 25 0 1 0 1846539738 165507072 39536 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19911/statm): 40407 39536 145 145 0 40262 0 [pid=19911] vsize: 161628 Current children cumulated CPU time (s) 1106.64 Current children cumulated vsize (Kb) 163752 [startup+1120.09 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 41813 0 0 0 111401 257 0 0 25 0 1 0 1846539738 166842368 39865 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 40733 39865 145 145 0 40588 0 [pid=19911] vsize: 162932 Current children cumulated CPU time (s) 1116.6 Current children cumulated vsize (Kb) 165056 [startup+1130.09 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 42233 0 0 0 112395 260 0 0 25 0 1 0 1846539738 168554496 40285 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 41151 40285 145 145 0 41006 0 [pid=19911] vsize: 164604 Current children cumulated CPU time (s) 1126.57 Current children cumulated vsize (Kb) 166728 [startup+1140.09 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 42725 0 0 0 113388 263 0 0 25 0 1 0 1846539738 170569728 40777 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 41643 40777 145 145 0 41498 0 [pid=19911] vsize: 166572 Current children cumulated CPU time (s) 1136.53 Current children cumulated vsize (Kb) 168696 [startup+1150.09 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 43153 0 0 0 114381 266 0 0 25 0 1 0 1846539738 172318720 41205 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 42070 41205 145 145 0 41925 0 [pid=19911] vsize: 168280 Current children cumulated CPU time (s) 1146.49 Current children cumulated vsize (Kb) 170404 [startup+1160.09 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 43616 0 0 0 115373 269 0 0 25 0 1 0 1846539738 174211072 41668 4294967295 134512640 135094434 3221224432 3221222912 134781474 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 42532 41668 145 145 0 42387 0 [pid=19911] vsize: 170128 Current children cumulated CPU time (s) 1156.44 Current children cumulated vsize (Kb) 172252 [startup+1170.09 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) T 19907 19907 5299 0 -1 0 44072 0 0 0 116367 271 0 0 25 0 1 0 1846539738 176074752 42124 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/19911/statm): 42987 42124 145 145 0 42842 0 [pid=19911] vsize: 171948 Current children cumulated CPU time (s) 1166.4 Current children cumulated vsize (Kb) 174072 [startup+1180.09 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) T 19907 19907 5299 0 -1 0 44449 0 0 0 117360 274 0 0 25 0 1 0 1846539738 177614848 42501 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/19911/statm): 43363 42501 145 145 0 43218 0 [pid=19911] vsize: 173452 Current children cumulated CPU time (s) 1176.36 Current children cumulated vsize (Kb) 175576 [startup+1190.09 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 44819 0 0 0 118354 276 0 0 25 0 1 0 1846539738 179126272 42871 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 43732 42871 145 145 0 43587 0 [pid=19911] vsize: 174928 Current children cumulated CPU time (s) 1186.32 Current children cumulated vsize (Kb) 177052 [startup+1200.09 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 45198 0 0 0 119348 279 0 0 25 0 1 0 1846539738 180674560 43250 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 44110 43250 145 145 0 43965 0 [pid=19911] vsize: 176440 Current children cumulated CPU time (s) 1196.29 Current children cumulated vsize (Kb) 178564 [startup+1210.09 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 45586 0 0 0 120342 281 0 0 25 0 1 0 1846539738 182259712 43638 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 44497 43638 145 145 0 44352 0 [pid=19911] vsize: 177988 Current children cumulated CPU time (s) 1206.25 Current children cumulated vsize (Kb) 180112 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.09 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 19911 Raw data (/proc/19907/stat): 19907 (minisat+_script) S 19906 19907 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846539733 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19907/statm): 531 226 485 147 0 384 0 [pid=19907] vsize: 2124 Raw data (/proc/19911/stat): 19911 (minisat+_64-bit) R 19907 19907 5299 0 -1 0 45586 0 0 0 120342 281 0 0 25 0 1 0 1846539738 182259712 43638 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19911/statm): 44497 43638 145 145 0 44352 0 [pid=19911] vsize: 177988 Current children cumulated CPU time (s) 1206.25 Current children cumulated vsize (Kb) 180112 Sending SIGTERM to -19907 Sleeping 2 seconds One traced child (pid=19907) ended because it received signal 15 (SIGTERM) One traced child (pid=19911) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.18 CPU time (s): 1206.33 CPU user time (s): 1203.43 CPU system time (s): 2.89956 CPU usage (%): 99.6816 Max. virtual memory (cumulated for all children) (Kb): 180112
ERROR: no interpretation found !