Name | mps-v2-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-share2b.opb |
MD5SUM | 4012b33f10ee9cb79561239f68fdcd6b |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | |
(Un)Satisfiability was proved | |
Best value of the objective function | |
Optimality of the best value was proved | |
Number of terms in the objective function | 870 |
Biggest coefficient in the objective function | 204010946560 |
Number of bits for the biggest coefficient in the objective function | 38 |
Sum of the numbers in the objective function | 4534411718529 |
Number of bits of the sum of numbers in the objective function | 43 |
Biggest number in a constraint | 552977039360 |
Number of bits of the biggest number in a constraint | 40 |
Biggest sum of numbers in a constraint | 10976862656529 |
Number of bits of the biggest sum of numbers | 44 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 2370 |
Total number of constraints | 96 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 96 |
Minimum length of a constraint | 30 |
Maximum length of a constraint | 360 |
LAUNCH ON wulflinc10 THE 2005-09-18 20:35:37 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2814 boxname=wulflinc10 idbench=470 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 4012b33f10ee9cb79561239f68fdcd6b /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-share2b.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-share2b.opb IDLAUNCH: 2814 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 450.999 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 450.999 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 917788 kB Buffers: 35204 kB Cached: 54872 kB SwapCached: 228 kB Active: 66924 kB Inactive: 26124 kB HighTotal: 131008 kB HighFree: 72352 kB LowTotal: 903652 kB LowFree: 845436 kB SwapTotal: 2097136 kB SwapFree: 2096756 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6272 kB Slab: 18172 kB Committed_AS: 64128 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-18 20:55:47 (client local time) WITH STATUS 0 IN 1207.22 SECONDS stats: 2814 7 1207.22 0
c Parsing PB file... c Converting 109 PB-constraints to clauses... c -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp c -- Detecting intervals from adjacent constraints: ############# c -- Clauses(.)/Splits(s): (none) c ---[ 108]---> Adder-cost: 860 maxlim: 24691811 bits: 26/25 c ---[ 107]---> Adder-cost: 574 maxlim: 5838564 bits: 24/23 c ---[ 106]---> Adder-cost: 632 maxlim: 6553549 bits: 24/23 c ---[ 105]---> Adder-cost: 860 maxlim: 11796389 bits: 25/24 c ---[ 104]---> Adder-cost: 1538 maxlim: 131070999 bits: 28/27 c ---[ 103]---> Adder-cost: 1520 maxlim: 131070999 bits: 28/27 c ---[ 102]---> Adder-cost: 1292 maxlim: 117963899 bits: 28/27 c ---[ 101]---> Adder-cost: 1032 maxlim: 117963899 bits: 28/27 c ---[ 100]---> BDD-cost: 160 c ---[ 98]---> Sorter-cost: 2247 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 97]---> Adder-cost: 684 maxlim: 7974098 bits: 24/23 c ---[ 96]---> Adder-cost: 482 maxlim: 2944795 bits: 23/22 c ---[ 95]---> Adder-cost: 451 maxlim: 1638349 bits: 22/21 c ---[ 94]---> Adder-cost: 669 maxlim: 2949029 bits: 23/22 c ---[ 93]---> Adder-cost: 1179 maxlim: 29162629 bits: 26/25 c ---[ 92]---> Adder-cost: 1203 maxlim: 29162629 bits: 26/25 c ---[ 91]---> Adder-cost: 857 maxlim: 26868939 bits: 26/25 c ---[ 90]---> Adder-cost: 771 maxlim: 26868939 bits: 26/25 c ---[ 89]---> BDD-cost: 140 c ---[ 87]---> Sorter-cost: 1452 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 86]---> Adder-cost: 1186 maxlim: 16204591 bits: 25/24 c ---[ 85]---> Adder-cost: 754 maxlim: 4970022 bits: 23/23 c ---[ 84]---> Adder-cost: 769 maxlim: 3276749 bits: 23/22 c ---[ 83]---> Adder-cost: 966 maxlim: 5898149 bits: 24/23 c ---[ 82]---> Adder-cost: 1745 maxlim: 65534999 bits: 27/26 c ---[ 81]---> Adder-cost: 1659 maxlim: 65534999 bits: 27/26 c ---[ 80]---> Adder-cost: 1313 maxlim: 29490749 bits: 26/25 c ---[ 79]---> Adder-cost: 1225 maxlim: 58981499 bits: 27/26 c ---[ 78]---> BDD-cost: 150 c ---[ 76]---> Adder-cost: 248 maxlim: 96246 bits: 18/17 c ---[ 75]---> Adder-cost: 970 maxlim: 9886616 bits: 24/24 c ---[ 74]---> Adder-cost: 620 maxlim: 3731054 bits: 23/22 c ---[ 73]---> Adder-cost: 758 maxlim: 1638349 bits: 22/21 c ---[ 72]---> Adder-cost: 721 maxlim: 2949029 bits: 23/22 c ---[ 71]---> Adder-cost: 1500 maxlim: 29162629 bits: 26/25 c ---[ 70]---> Adder-cost: 1390 maxlim: 29162629 bits: 26/25 c ---[ 69]---> Adder-cost: 1121 maxlim: 26868939 bits: 26/25 c ---[ 68]---> Adder-cost: 1077 maxlim: 26868939 bits: 26/25 c ---[ 67]---> BDD-cost: 140 c ---[ 65]---> Sorter-cost: 2235 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 64]---> Adder-cost: 858 maxlim: 10320981 bits: 24/24 c ---[ 63]---> Adder-cost: 444 maxlim: 3505911 bits: 23/22 c ---[ 62]---> Adder-cost: 670 maxlim: 1638349 bits: 22/21 c ---[ 61]---> Adder-cost: 922 maxlim: 2949029 bits: 23/22 c ---[ 60]---> Adder-cost: 1578 maxlim: 33094669 bits: 26/25 c ---[ 59]---> Adder-cost: 1469 maxlim: 33094669 bits: 26/25 c ---[ 58]---> Adder-cost: 1360 maxlim: 29817969 bits: 26/25 c ---[ 57]---> Adder-cost: 1282 maxlim: 29817969 bits: 26/25 c ---[ 56]---> BDD-cost: 140 c ---[ 54]---> Sorter-cost: 2609 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 53]---> Adder-cost: 886 maxlim: 14431144 bits: 25/24 c ---[ 52]---> Adder-cost: 550 maxlim: 3866247 bits: 23/22 c ---[ 51]---> Adder-cost: 575 maxlim: 3276749 bits: 23/22 c ---[ 50]---> Adder-cost: 818 maxlim: 5898149 bits: 24/23 c ---[ 49]---> Adder-cost: 1533 maxlim: 58326149 bits: 27/26 c ---[ 48]---> Adder-cost: 1549 maxlim: 58326149 bits: 27/26 c ---[ 47]---> Adder-cost: 1225 maxlim: 53738699 bits: 27/26 c ---[ 46]---> Adder-cost: 1321 maxlim: 53738699 bits: 27/26 c ---[ 45]---> BDD-cost: 150 c ---[ 43]---> Sorter-cost: 2520 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 42]---> Sorter-cost: 465 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 41]---> BDD-cost: 58 c ---[ 40]---> Sorter-cost: 1966 Base: 2 2 2 2 2 2 2 2 2 2 2 5 2 c ---[ 39]---> Sorter-cost: 543 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 38]---> BDD-cost: 53 c ---[ 37]---> Sorter-cost: 249 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 36]---> BDD-cost: 53 c ---[ 35]---> Sorter-cost: 3109 Base: 2 2 2 2 2 2 2 2 2 2 2 5 2 c ---[ 34]---> BDD-cost: 10 c ---[ 33]---> BDD-cost: 10 c ---[ 32]---> Sorter-cost: 295 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 31]---> Sorter-cost: 295 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 30]---> Sorter-cost: 295 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 29]---> Adder-cost: 366 maxlim: 964540 bits: 21/20 c ---[ 28]---> BDD-cost: 48 c ---[ 27]---> BDD-cost: 48 c ---[ 26]---> BDD-cost: 48 c ---[ 25]---> BDD-cost: 10 c ---[ 23]---> Sorter-cost: 352 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 21]---> BDD-cost: 143 c ---[ 19]---> Sorter-cost: 333 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 17]---> Sorter-cost: 323 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 15]---> BDD-cost: 133 c ---[ 13]---> BDD-cost: 128 c ---[ 12]---> BDD-cost: 48 c ---[ 11]---> Sorter-cost: 810 Base: 2 2 2 2 2 2 2 2 2 2 2 2 3 c ---[ 10]---> Adder-cost: 856 maxlim: 42535866 bits: 27/26 c ---[ 9]---> Adder-cost: 622 maxlim: 8828577 bits: 25/24 c ---[ 8]---> Adder-cost: 690 maxlim: 13107149 bits: 25/24 c ---[ 7]---> Adder-cost: 860 maxlim: 23592869 bits: 26/25 c ---[ 6]---> Adder-cost: 1596 maxlim: 235928699 bits: 29/28 c ---[ 5]---> Adder-cost: 1614 maxlim: 235928699 bits: 29/28 c ---[ 4]---> Adder-cost: 1432 maxlim: 217578689 bits: 29/28 c ---[ 3]---> Adder-cost: 1464 maxlim: 217578689 bits: 29/28 c ---[ 2]---> BDD-cost: 170 c ---[ 0]---> Sorter-cost: 2644 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 469982 1608750 | 156660 0 0 nan | 0.000 % | c | 101 | 469817 1608381 | 172326 76 305 4.0 | 3.136 % | c | 252 | 469817 1608381 | 189558 227 1774 7.8 | 3.136 % | c | 477 | 469817 1608381 | 208514 452 3745 8.3 | 3.136 % | c | 817 | 469817 1608381 | 229365 792 9533 12.0 | 3.136 % | c | 1325 | 469817 1608381 | 252302 1300 25297 19.5 | 3.136 % | c | 2084 | 469817 1608381 | 277532 2059 46649 22.7 | 3.136 % | c | 3223 | 469556 1607801 | 305286 3168 55879 17.6 | 3.223 % | c | 4931 | 469354 1607336 | 335814 4860 132236 27.2 | 3.298 % | c | 7493 | 469095 1606436 | 369396 7419 195209 26.3 | 3.311 % | c | 11337 | 469095 1606436 | 406335 11263 315276 28.0 | 3.311 % | c | 17103 | 469095 1606436 | 446969 17029 619643 36.4 | 3.311 % | c | 25752 | 469057 1606335 | 491666 25633 953628 37.2 | 3.322 % | c | 38726 | 468885 1605727 | 540832 38601 1743603 45.2 | 3.329 % | c | 58187 | 468646 1605194 | 594916 58029 2868936 49.4 | 3.407 % | c | 87380 | 468590 1605069 | 654407 87214 4525565 51.9 | 3.425 % | c | 131169 | 468122 1603675 | 719848 130978 6390243 48.8 | 3.502 % | c | 196854 | 468016 1603438 | 791833 196651 9700417 49.3 | 3.535 % | c | 295381 | 468016 1603438 | 871016 295178 15254998 51.7 | 3.535 % |
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/32026/stat): 32026 (minisat+_script) R 32025 32026 22582 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1785988435 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/32026/statm): 174 3 169 147 0 27 0 [pid=32026] 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=32027 New process pid=32028 New process pid=32029 execve syscall for /bin/sed executable One traced child (pid=32028) 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=32029) exited with status: 0 One traced child (pid=32027) exited with status: 0 New process pid=32030 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-share2b.opb [startup+10.0027 s] Raw data (loadavg): 1.06 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 633 0 0 0 989 2 0 0 25 0 1 0 1785988440 2904064 588 4294967295 134512640 135094434 3221224432 3221221808 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 709 588 145 145 0 564 0 [pid=32030] vsize: 2836 Current children cumulated CPU time (s) 9.91 Current children cumulated vsize (Kb) 4960 [startup+20.0033 s] Raw data (loadavg): 1.05 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 811 0 0 0 1989 3 0 0 25 0 1 0 1785988440 3391488 685 4294967295 134512640 135094434 3221224432 3221221808 134677313 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 828 685 145 145 0 683 0 [pid=32030] vsize: 3312 Current children cumulated CPU time (s) 19.92 Current children cumulated vsize (Kb) 5436 [startup+30.0038 s] Raw data (loadavg): 1.04 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 905 0 0 0 2988 3 0 0 25 0 1 0 1785988440 3575808 747 4294967295 134512640 135094434 3221224432 3221221104 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 873 747 145 145 0 728 0 [pid=32030] vsize: 3492 Current children cumulated CPU time (s) 29.91 Current children cumulated vsize (Kb) 5616 [startup+40.0044 s] Raw data (loadavg): 1.04 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 987 0 0 0 3988 3 0 0 25 0 1 0 1785988440 3563520 750 4294967295 134512640 135094434 3221224432 3221221632 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 870 750 145 145 0 725 0 [pid=32030] vsize: 3480 Current children cumulated CPU time (s) 39.91 Current children cumulated vsize (Kb) 5604 [startup+50.0049 s] Raw data (loadavg): 1.03 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 1093 0 0 0 4988 4 0 0 25 0 1 0 1785988440 4145152 817 4294967295 134512640 135094434 3221224432 3221221456 134600267 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 1012 817 145 145 0 867 0 [pid=32030] vsize: 4048 Current children cumulated CPU time (s) 49.92 Current children cumulated vsize (Kb) 6172 [startup+60.0055 s] Raw data (loadavg): 1.02 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 1202 0 0 0 5987 4 0 0 25 0 1 0 1785988440 4132864 826 4294967295 134512640 135094434 3221224432 3221221808 134600314 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 1009 826 145 145 0 864 0 [pid=32030] vsize: 4036 Current children cumulated CPU time (s) 59.91 Current children cumulated vsize (Kb) 6160 [startup+70.0061 s] Raw data (loadavg): 1.02 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 1556 0 0 0 6986 5 0 0 25 0 1 0 1785988440 4780032 1019 4294967295 134512640 135094434 3221224432 3221221432 134676241 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 1167 1019 145 145 0 1022 0 [pid=32030] vsize: 4668 Current children cumulated CPU time (s) 69.91 Current children cumulated vsize (Kb) 6792 [startup+80.0066 s] Raw data (loadavg): 1.02 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 1653 0 0 0 7985 6 0 0 25 0 1 0 1785988440 4722688 1005 4294967295 134512640 135094434 3221224432 3221220576 134677346 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 1153 1005 145 145 0 1008 0 [pid=32030] vsize: 4612 Current children cumulated CPU time (s) 79.91 Current children cumulated vsize (Kb) 6736 [startup+90.0072 s] Raw data (loadavg): 1.01 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 1743 0 0 0 8985 6 0 0 25 0 1 0 1785988440 4874240 1056 4294967295 134512640 135094434 3221224432 3221221632 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 1190 1056 145 145 0 1045 0 [pid=32030] vsize: 4760 Current children cumulated CPU time (s) 89.91 Current children cumulated vsize (Kb) 6884 [startup+100.008 s] Raw data (loadavg): 1.01 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 1898 0 0 0 9985 6 0 0 25 0 1 0 1785988440 5025792 1106 4294967295 134512640 135094434 3221224432 3221220752 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 1227 1106 145 145 0 1082 0 [pid=32030] vsize: 4908 Current children cumulated CPU time (s) 99.91 Current children cumulated vsize (Kb) 7032 [startup+110.008 s] Raw data (loadavg): 1.01 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 1998 0 0 0 10984 7 0 0 25 0 1 0 1785988440 5951488 1167 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 1453 1167 145 145 0 1308 0 [pid=32030] vsize: 5812 Current children cumulated CPU time (s) 109.91 Current children cumulated vsize (Kb) 7936 [startup+120.009 s] Raw data (loadavg): 1.01 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 2111 0 0 0 11984 7 0 0 25 0 1 0 1785988440 6049792 1215 4294967295 134512640 135094434 3221224432 3221220928 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 1477 1215 145 145 0 1332 0 [pid=32030] vsize: 5908 Current children cumulated CPU time (s) 119.91 Current children cumulated vsize (Kb) 8032 [startup+130.008 s] Raw data (loadavg): 1.01 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 2225 0 0 0 12983 8 0 0 25 0 1 0 1785988440 6057984 1217 4294967295 134512640 135094434 3221224432 3221221168 134677091 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 1479 1217 145 145 0 1334 0 [pid=32030] vsize: 5916 Current children cumulated CPU time (s) 129.91 Current children cumulated vsize (Kb) 8040 [startup+140.009 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 2654 0 0 0 13982 9 0 0 25 0 1 0 1785988440 6901760 1439 4294967295 134512640 135094434 3221224432 3221221104 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 1685 1439 145 145 0 1540 0 [pid=32030] vsize: 6740 Current children cumulated CPU time (s) 139.91 Current children cumulated vsize (Kb) 8864 [startup+150.01 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 2654 0 0 0 14983 9 0 0 25 0 1 0 1785988440 6901760 1439 4294967295 134512640 135094434 3221224432 3221221456 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 1685 1439 145 145 0 1540 0 [pid=32030] vsize: 6740 Current children cumulated CPU time (s) 149.92 Current children cumulated vsize (Kb) 8864 [startup+160.009 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 2774 0 0 0 15982 9 0 0 25 0 1 0 1785988440 6946816 1456 4294967295 134512640 135094434 3221224432 3221221456 134677290 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 1696 1456 145 145 0 1551 0 [pid=32030] vsize: 6784 Current children cumulated CPU time (s) 159.91 Current children cumulated vsize (Kb) 8908 [startup+170.01 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 2998 0 0 0 16981 10 0 0 25 0 1 0 1785988440 7135232 1537 4294967295 134512640 135094434 3221224432 3221220752 134600151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32030/statm): 1742 1537 145 145 0 1597 0 [pid=32030] vsize: 6968 Current children cumulated CPU time (s) 169.91 Current children cumulated vsize (Kb) 9092 [startup+180.01 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 3147 0 0 0 17980 11 0 0 25 0 1 0 1785988440 7348224 1622 4294967295 134512640 135094434 3221224432 3221220224 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 1794 1622 145 145 0 1649 0 [pid=32030] vsize: 7176 Current children cumulated CPU time (s) 179.91 Current children cumulated vsize (Kb) 9300 [startup+190.011 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 3147 0 0 0 18980 11 0 0 25 0 1 0 1785988440 7348224 1622 4294967295 134512640 135094434 3221224432 3221220752 134600175 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 1794 1622 145 145 0 1649 0 [pid=32030] vsize: 7176 Current children cumulated CPU time (s) 189.91 Current children cumulated vsize (Kb) 9300 [startup+200.011 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 3147 0 0 0 19980 11 0 0 25 0 1 0 1785988440 7348224 1622 4294967295 134512640 135094434 3221224432 3221221188 134677077 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 1794 1622 145 145 0 1649 0 [pid=32030] vsize: 7176 Current children cumulated CPU time (s) 199.91 Current children cumulated vsize (Kb) 9300 [startup+210.012 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 3147 0 0 0 20980 11 0 0 25 0 1 0 1785988440 7348224 1622 4294967295 134512640 135094434 3221224432 3221221880 134677084 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 1794 1622 145 145 0 1649 0 [pid=32030] vsize: 7176 Current children cumulated CPU time (s) 209.91 Current children cumulated vsize (Kb) 9300 [startup+220.012 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 3318 0 0 0 21979 12 0 0 25 0 1 0 1785988440 7507968 1682 4294967295 134512640 135094434 3221224432 3221222256 134677138 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 1833 1682 145 145 0 1688 0 [pid=32030] vsize: 7332 Current children cumulated CPU time (s) 219.91 Current children cumulated vsize (Kb) 9456 [startup+230.013 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 3373 0 0 0 22979 12 0 0 25 0 1 0 1785988440 7565312 1696 4294967295 134512640 135094434 3221224432 3221221280 134676586 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 1847 1696 145 145 0 1702 0 [pid=32030] vsize: 7388 Current children cumulated CPU time (s) 229.91 Current children cumulated vsize (Kb) 9512 [startup+240.014 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 10828 0 0 0 23909 45 0 0 25 0 1 0 1785988440 41287680 9135 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 10080 9135 145 145 0 9935 0 [pid=32030] vsize: 40320 Current children cumulated CPU time (s) 239.54 Current children cumulated vsize (Kb) 42444 [startup+250.014 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 11162 0 0 0 24902 49 0 0 25 0 1 0 1785988440 42672128 9469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 10418 9469 145 145 0 10273 0 [pid=32030] vsize: 41672 Current children cumulated CPU time (s) 249.51 Current children cumulated vsize (Kb) 43796 [startup+260.014 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 11647 0 0 0 25893 52 0 0 25 0 1 0 1785988440 44699648 9954 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32030/statm): 10913 9954 145 145 0 10768 0 [pid=32030] vsize: 43652 Current children cumulated CPU time (s) 259.45 Current children cumulated vsize (Kb) 45776 [startup+270.015 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 11996 0 0 0 26886 55 0 0 25 0 1 0 1785988440 46100480 10303 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 11255 10303 145 145 0 11110 0 [pid=32030] vsize: 45020 Current children cumulated CPU time (s) 269.41 Current children cumulated vsize (Kb) 47144 [startup+280.016 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 12325 0 0 0 27879 58 0 0 25 0 1 0 1785988440 47427584 10632 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 11579 10632 145 145 0 11434 0 [pid=32030] vsize: 46316 Current children cumulated CPU time (s) 279.37 Current children cumulated vsize (Kb) 48440 [startup+290.017 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 12772 0 0 0 28872 62 0 0 25 0 1 0 1785988440 49364992 11079 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 12052 11079 145 145 0 11907 0 [pid=32030] vsize: 48208 Current children cumulated CPU time (s) 289.34 Current children cumulated vsize (Kb) 50332 [startup+300.018 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 13169 0 0 0 29865 65 0 0 25 0 1 0 1785988440 50970624 11476 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 12444 11476 145 145 0 12299 0 [pid=32030] vsize: 49776 Current children cumulated CPU time (s) 299.3 Current children cumulated vsize (Kb) 51900 [startup+310.018 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 13505 0 0 0 30859 68 0 0 25 0 1 0 1785988440 52330496 11812 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 12776 11812 145 145 0 12631 0 [pid=32030] vsize: 51104 Current children cumulated CPU time (s) 309.27 Current children cumulated vsize (Kb) 53228 [startup+320.018 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 13853 0 0 0 31853 70 0 0 25 0 1 0 1785988440 53739520 12160 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 13120 12160 145 145 0 12975 0 [pid=32030] vsize: 52480 Current children cumulated CPU time (s) 319.23 Current children cumulated vsize (Kb) 54604 [startup+330.019 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 14141 0 0 0 32848 72 0 0 25 0 1 0 1785988440 54902784 12448 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 13404 12448 145 145 0 13259 0 [pid=32030] vsize: 53616 Current children cumulated CPU time (s) 329.2 Current children cumulated vsize (Kb) 55740 [startup+340.019 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 14367 0 0 0 33844 74 0 0 25 0 1 0 1785988440 55762944 12674 4294967295 134512640 135094434 3221224432 3221223056 134557612 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 13614 12674 145 145 0 13469 0 [pid=32030] vsize: 54456 Current children cumulated CPU time (s) 339.18 Current children cumulated vsize (Kb) 56580 [startup+350.02 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 14683 0 0 0 34838 77 0 0 25 0 1 0 1785988440 57032704 12990 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 13924 12990 145 145 0 13779 0 [pid=32030] vsize: 55696 Current children cumulated CPU time (s) 349.15 Current children cumulated vsize (Kb) 57820 [startup+360.02 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 14990 0 0 0 35831 80 0 0 25 0 1 0 1785988440 58535936 13297 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 14291 13297 145 145 0 14146 0 [pid=32030] vsize: 57164 Current children cumulated CPU time (s) 359.11 Current children cumulated vsize (Kb) 59288 [startup+370.021 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 15272 0 0 0 36825 83 0 0 25 0 1 0 1785988440 59670528 13579 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 14568 13579 145 145 0 14423 0 [pid=32030] vsize: 58272 Current children cumulated CPU time (s) 369.08 Current children cumulated vsize (Kb) 60396 [startup+380.021 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 15579 0 0 0 37819 86 0 0 25 0 1 0 1785988440 60911616 13886 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 14871 13886 145 145 0 14726 0 [pid=32030] vsize: 59484 Current children cumulated CPU time (s) 379.05 Current children cumulated vsize (Kb) 61608 [startup+390.023 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 15850 0 0 0 38815 88 0 0 25 0 1 0 1785988440 62013440 14157 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 15140 14157 145 145 0 14995 0 [pid=32030] vsize: 60560 Current children cumulated CPU time (s) 389.03 Current children cumulated vsize (Kb) 62684 [startup+400.024 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 16127 0 0 0 39810 90 0 0 25 0 1 0 1785988440 63139840 14434 4294967295 134512640 135094434 3221224432 3221223088 134558169 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 15415 14434 145 145 0 15270 0 [pid=32030] vsize: 61660 Current children cumulated CPU time (s) 399 Current children cumulated vsize (Kb) 63784 [startup+410.024 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 16339 0 0 0 40806 91 0 0 25 0 1 0 1785988440 64004096 14646 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32030/statm): 15626 14646 145 145 0 15481 0 [pid=32030] vsize: 62504 Current children cumulated CPU time (s) 408.97 Current children cumulated vsize (Kb) 64628 [startup+420.026 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 16554 0 0 0 41803 93 0 0 25 0 1 0 1785988440 64872448 14861 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 15838 14861 145 145 0 15693 0 [pid=32030] vsize: 63352 Current children cumulated CPU time (s) 418.96 Current children cumulated vsize (Kb) 65476 [startup+430.026 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 16883 0 0 0 42796 95 0 0 25 0 1 0 1785988440 66195456 15190 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 16161 15190 145 145 0 16016 0 [pid=32030] vsize: 64644 Current children cumulated CPU time (s) 428.91 Current children cumulated vsize (Kb) 66768 [startup+440.027 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 17194 0 0 0 43791 98 0 0 25 0 1 0 1785988440 67457024 15501 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 16469 15501 145 145 0 16324 0 [pid=32030] vsize: 65876 Current children cumulated CPU time (s) 438.89 Current children cumulated vsize (Kb) 68000 [startup+450.027 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 17443 0 0 0 44787 99 0 0 25 0 1 0 1785988440 68456448 15750 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 16713 15750 145 145 0 16568 0 [pid=32030] vsize: 66852 Current children cumulated CPU time (s) 448.86 Current children cumulated vsize (Kb) 68976 [startup+460.027 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) T 32026 32026 22582 0 -1 0 17782 0 0 0 45781 102 0 0 25 0 1 0 1785988440 69816320 16089 4294967295 134512640 135094434 3221224432 3221222780 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/32030/statm): 17045 16089 145 145 0 16900 0 [pid=32030] vsize: 68180 Current children cumulated CPU time (s) 458.83 Current children cumulated vsize (Kb) 70304 [startup+470.027 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 18072 0 0 0 46775 104 0 0 25 0 1 0 1785988440 70979584 16379 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 17329 16379 145 145 0 17184 0 [pid=32030] vsize: 69316 Current children cumulated CPU time (s) 468.79 Current children cumulated vsize (Kb) 71440 [startup+480.028 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 18550 0 0 0 47767 108 0 0 25 0 1 0 1785988440 72908800 16857 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 17800 16857 145 145 0 17655 0 [pid=32030] vsize: 71200 Current children cumulated CPU time (s) 478.75 Current children cumulated vsize (Kb) 73324 [startup+490.03 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 18868 0 0 0 48761 110 0 0 25 0 1 0 1785988440 74715136 17175 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 18241 17175 145 145 0 18096 0 [pid=32030] vsize: 72964 Current children cumulated CPU time (s) 488.71 Current children cumulated vsize (Kb) 75088 [startup+500.03 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) T 32026 32026 22582 0 -1 0 19265 0 0 0 49753 113 0 0 25 0 1 0 1785988440 76312576 17572 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/32030/statm): 18631 17572 145 145 0 18486 0 [pid=32030] vsize: 74524 Current children cumulated CPU time (s) 498.66 Current children cumulated vsize (Kb) 76648 [startup+510.031 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 19617 0 0 0 50747 116 0 0 25 0 1 0 1785988440 77729792 17924 4294967295 134512640 135094434 3221224432 3221223104 134555560 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 18977 17924 145 145 0 18832 0 [pid=32030] vsize: 75908 Current children cumulated CPU time (s) 508.63 Current children cumulated vsize (Kb) 78032 [startup+520.031 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 19923 0 0 0 51740 119 0 0 25 0 1 0 1785988440 78962688 18230 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 19278 18230 145 145 0 19133 0 [pid=32030] vsize: 77112 Current children cumulated CPU time (s) 518.59 Current children cumulated vsize (Kb) 79236 [startup+530.032 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 20200 0 0 0 52735 122 0 0 25 0 1 0 1785988440 80080896 18507 4294967295 134512640 135094434 3221224432 3221223088 134557849 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 19551 18507 145 145 0 19406 0 [pid=32030] vsize: 78204 Current children cumulated CPU time (s) 528.57 Current children cumulated vsize (Kb) 80328 [startup+540.032 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 20449 0 0 0 53731 124 0 0 25 0 1 0 1785988440 81104896 18756 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 19801 18756 145 145 0 19656 0 [pid=32030] vsize: 79204 Current children cumulated CPU time (s) 538.55 Current children cumulated vsize (Kb) 81328 [startup+550.033 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 20704 0 0 0 54725 125 0 0 25 0 1 0 1785988440 82137088 19011 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 20053 19011 145 145 0 19908 0 [pid=32030] vsize: 80212 Current children cumulated CPU time (s) 548.5 Current children cumulated vsize (Kb) 82336 [startup+560.033 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 20932 0 0 0 55721 127 0 0 25 0 1 0 1785988440 83054592 19239 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 20277 19239 145 145 0 20132 0 [pid=32030] vsize: 81108 Current children cumulated CPU time (s) 558.48 Current children cumulated vsize (Kb) 83232 [startup+570.033 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 21196 0 0 0 56716 129 0 0 25 0 1 0 1785988440 84131840 19503 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 20540 19503 145 145 0 20395 0 [pid=32030] vsize: 82160 Current children cumulated CPU time (s) 568.45 Current children cumulated vsize (Kb) 84284 [startup+580.034 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 21426 0 0 0 57712 131 0 0 25 0 1 0 1785988440 85073920 19733 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 20770 19733 145 145 0 20625 0 [pid=32030] vsize: 83080 Current children cumulated CPU time (s) 578.43 Current children cumulated vsize (Kb) 85204 [startup+590.034 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 21825 0 0 0 58704 134 0 0 25 0 1 0 1785988440 86683648 20132 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 21163 20132 145 145 0 21018 0 [pid=32030] vsize: 84652 Current children cumulated CPU time (s) 588.38 Current children cumulated vsize (Kb) 86776 [startup+600.035 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 22147 0 0 0 59699 136 0 0 25 0 1 0 1785988440 87982080 20454 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 21480 20454 145 145 0 21335 0 [pid=32030] vsize: 85920 Current children cumulated CPU time (s) 598.35 Current children cumulated vsize (Kb) 88044 [startup+610.035 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 22453 0 0 0 60693 138 0 0 25 0 1 0 1785988440 89235456 20760 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 21786 20760 145 145 0 21641 0 [pid=32030] vsize: 87144 Current children cumulated CPU time (s) 608.31 Current children cumulated vsize (Kb) 89268 [startup+620.036 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 22729 0 0 0 61690 139 0 0 25 0 1 0 1785988440 90370048 21036 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32030/statm): 22063 21036 145 145 0 21918 0 [pid=32030] vsize: 88252 Current children cumulated CPU time (s) 618.29 Current children cumulated vsize (Kb) 90376 [startup+630.037 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 23059 0 0 0 62682 143 0 0 25 0 1 0 1785988440 91688960 21366 4294967295 134512640 135094434 3221224432 3221223072 134558269 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32030/statm): 22385 21366 145 145 0 22240 0 [pid=32030] vsize: 89540 Current children cumulated CPU time (s) 628.25 Current children cumulated vsize (Kb) 91664 [startup+640.038 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 23399 0 0 0 63675 146 0 0 25 0 1 0 1785988440 93065216 21706 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32030/statm): 22721 21706 145 145 0 22576 0 [pid=32030] vsize: 90884 Current children cumulated CPU time (s) 638.21 Current children cumulated vsize (Kb) 93008 [startup+650.039 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 23689 0 0 0 64669 148 0 0 25 0 1 0 1785988440 94240768 21996 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32030/statm): 23008 21996 145 145 0 22863 0 [pid=32030] vsize: 92032 Current children cumulated CPU time (s) 648.17 Current children cumulated vsize (Kb) 94156 [startup+660.039 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 23980 0 0 0 65665 150 0 0 25 0 1 0 1785988440 95416320 22287 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32030/statm): 23295 22287 145 145 0 23150 0 [pid=32030] vsize: 93180 Current children cumulated CPU time (s) 658.15 Current children cumulated vsize (Kb) 95304 [startup+670.041 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 24222 0 0 0 66660 152 0 0 25 0 1 0 1785988440 96407552 22529 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32030/statm): 23537 22529 145 145 0 23392 0 [pid=32030] vsize: 94148 Current children cumulated CPU time (s) 668.12 Current children cumulated vsize (Kb) 96272 [startup+680.041 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 24446 0 0 0 67657 154 0 0 25 0 1 0 1785988440 97341440 22753 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32030/statm): 23765 22753 145 145 0 23620 0 [pid=32030] vsize: 95060 Current children cumulated CPU time (s) 678.11 Current children cumulated vsize (Kb) 97184 [startup+690.043 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 24658 0 0 0 68652 156 0 0 25 0 1 0 1785988440 98193408 22965 4294967295 134512640 135094434 3221224432 3221223104 134555232 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32030/statm): 23973 22965 145 145 0 23828 0 [pid=32030] vsize: 95892 Current children cumulated CPU time (s) 688.08 Current children cumulated vsize (Kb) 98016 [startup+700.043 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 24863 0 0 0 69647 158 0 0 25 0 1 0 1785988440 99020800 23170 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32030/statm): 24175 23170 145 145 0 24030 0 [pid=32030] vsize: 96700 Current children cumulated CPU time (s) 698.05 Current children cumulated vsize (Kb) 98824 [startup+710.044 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 25063 0 0 0 70643 160 0 0 25 0 1 0 1785988440 99823616 23370 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32030/statm): 24371 23370 145 145 0 24226 0 [pid=32030] vsize: 97484 Current children cumulated CPU time (s) 708.03 Current children cumulated vsize (Kb) 99608 [startup+720.046 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 25249 0 0 0 71640 162 0 0 25 0 1 0 1785988440 100585472 23556 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32030/statm): 24557 23556 145 145 0 24412 0 [pid=32030] vsize: 98228 Current children cumulated CPU time (s) 718.02 Current children cumulated vsize (Kb) 100352 [startup+730.046 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 25453 0 0 0 72636 163 0 0 25 0 1 0 1785988440 101433344 23760 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32030/statm): 24764 23760 145 145 0 24619 0 [pid=32030] vsize: 99056 Current children cumulated CPU time (s) 727.99 Current children cumulated vsize (Kb) 101180 [startup+740.048 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 25657 0 0 0 73632 165 0 0 25 0 1 0 1785988440 102248448 23964 4294967295 134512640 135094434 3221224432 3221223104 134556288 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32030/statm): 24963 23964 145 145 0 24818 0 [pid=32030] vsize: 99852 Current children cumulated CPU time (s) 737.97 Current children cumulated vsize (Kb) 101976 [startup+750.048 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 25843 0 0 0 74628 167 0 0 25 0 1 0 1785988440 102998016 24150 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32030/statm): 25146 24150 145 145 0 25001 0 [pid=32030] vsize: 100584 Current children cumulated CPU time (s) 747.95 Current children cumulated vsize (Kb) 102708 [startup+760.049 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 26020 0 0 0 75625 168 0 0 25 0 1 0 1785988440 103727104 24327 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32030/statm): 25324 24327 145 145 0 25179 0 [pid=32030] vsize: 101296 Current children cumulated CPU time (s) 757.93 Current children cumulated vsize (Kb) 103420 [startup+770.05 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 26201 0 0 0 76621 171 0 0 25 0 1 0 1785988440 104464384 24508 4294967295 134512640 135094434 3221224432 3221223096 134562037 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32030/statm): 25504 24508 145 145 0 25359 0 [pid=32030] vsize: 102016 Current children cumulated CPU time (s) 767.92 Current children cumulated vsize (Kb) 104140 [startup+780.051 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 26373 0 0 0 77618 173 0 0 25 0 1 0 1785988440 105189376 24680 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32030/statm): 25681 24680 145 145 0 25536 0 [pid=32030] vsize: 102724 Current children cumulated CPU time (s) 777.91 Current children cumulated vsize (Kb) 104848 [startup+790.052 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 26541 0 0 0 78614 175 0 0 25 0 1 0 1785988440 105877504 24848 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32030/statm): 25849 24848 145 145 0 25704 0 [pid=32030] vsize: 103396 Current children cumulated CPU time (s) 787.89 Current children cumulated vsize (Kb) 105520 [startup+800.052 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 26729 0 0 0 79611 176 0 0 25 0 1 0 1785988440 106622976 25036 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32030/statm): 26031 25036 145 145 0 25886 0 [pid=32030] vsize: 104124 Current children cumulated CPU time (s) 797.87 Current children cumulated vsize (Kb) 106248 [startup+810.053 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 26911 0 0 0 80609 177 0 0 25 0 1 0 1785988440 107425792 25218 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32030/statm): 26227 25218 145 145 0 26082 0 [pid=32030] vsize: 104908 Current children cumulated CPU time (s) 807.86 Current children cumulated vsize (Kb) 107032 [startup+820.053 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 27068 0 0 0 81606 179 0 0 25 0 1 0 1785988440 109166592 25375 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32030/statm): 26652 25375 145 145 0 26507 0 [pid=32030] vsize: 106608 Current children cumulated CPU time (s) 817.85 Current children cumulated vsize (Kb) 108732 [startup+830.054 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 27215 0 0 0 82603 180 0 0 25 0 1 0 1785988440 109731840 25522 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32030/statm): 26790 25522 145 145 0 26645 0 [pid=32030] vsize: 107160 Current children cumulated CPU time (s) 827.83 Current children cumulated vsize (Kb) 109284 [startup+840.055 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 27337 0 0 0 83600 181 0 0 25 0 1 0 1785988440 110211072 25644 4294967295 134512640 135094434 3221224432 3221223104 134556073 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32030/statm): 26907 25644 145 145 0 26762 0 [pid=32030] vsize: 107628 Current children cumulated CPU time (s) 837.81 Current children cumulated vsize (Kb) 109752 [startup+850.056 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 27462 0 0 0 84598 182 0 0 25 0 1 0 1785988440 110702592 25769 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32030/statm): 27027 25769 145 145 0 26882 0 [pid=32030] vsize: 108108 Current children cumulated CPU time (s) 847.8 Current children cumulated vsize (Kb) 110232 [startup+860.056 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 27627 0 0 0 85596 183 0 0 25 0 1 0 1785988440 111407104 25934 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32030/statm): 27199 25934 145 145 0 27054 0 [pid=32030] vsize: 108796 Current children cumulated CPU time (s) 857.79 Current children cumulated vsize (Kb) 110920 [startup+870.058 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 27752 0 0 0 86594 184 0 0 25 0 1 0 1785988440 111964160 26059 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32030/statm): 27335 26059 145 145 0 27190 0 [pid=32030] vsize: 109340 Current children cumulated CPU time (s) 867.78 Current children cumulated vsize (Kb) 111464 [startup+880.059 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 27879 0 0 0 87592 185 0 0 25 0 1 0 1785988440 112480256 26186 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 27461 26186 145 145 0 27316 0 [pid=32030] vsize: 109844 Current children cumulated CPU time (s) 877.77 Current children cumulated vsize (Kb) 111968 [startup+890.06 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 28031 0 0 0 88589 186 0 0 25 0 1 0 1785988440 113086464 26338 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 27609 26338 145 145 0 27464 0 [pid=32030] vsize: 110436 Current children cumulated CPU time (s) 887.75 Current children cumulated vsize (Kb) 112560 [startup+900.061 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 28185 0 0 0 89587 187 0 0 25 0 1 0 1785988440 113700864 26492 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 27759 26492 145 145 0 27614 0 [pid=32030] vsize: 111036 Current children cumulated CPU time (s) 897.74 Current children cumulated vsize (Kb) 113160 [startup+910.06 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 28335 0 0 0 90582 190 0 0 25 0 1 0 1785988440 114327552 26642 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 27912 26642 145 145 0 27767 0 [pid=32030] vsize: 111648 Current children cumulated CPU time (s) 907.72 Current children cumulated vsize (Kb) 113772 [startup+920.062 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 28459 0 0 0 91580 192 0 0 25 0 1 0 1785988440 114831360 26766 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 28035 26766 145 145 0 27890 0 [pid=32030] vsize: 112140 Current children cumulated CPU time (s) 917.72 Current children cumulated vsize (Kb) 114264 [startup+930.062 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 28623 0 0 0 92577 193 0 0 25 0 1 0 1785988440 115490816 26930 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 28196 26930 145 145 0 28051 0 [pid=32030] vsize: 112784 Current children cumulated CPU time (s) 927.7 Current children cumulated vsize (Kb) 114908 [startup+940.063 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 28763 0 0 0 93575 194 0 0 25 0 1 0 1785988440 116056064 27070 4294967295 134512640 135094434 3221224432 3221223088 134557849 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 28334 27070 145 145 0 28189 0 [pid=32030] vsize: 113336 Current children cumulated CPU time (s) 937.69 Current children cumulated vsize (Kb) 115460 [startup+950.063 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 28906 0 0 0 94572 196 0 0 25 0 1 0 1785988440 116629504 27213 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 28474 27213 145 145 0 28329 0 [pid=32030] vsize: 113896 Current children cumulated CPU time (s) 947.68 Current children cumulated vsize (Kb) 116020 [startup+960.064 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 29065 0 0 0 95569 197 0 0 25 0 1 0 1785988440 117280768 27372 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 28633 27372 145 145 0 28488 0 [pid=32030] vsize: 114532 Current children cumulated CPU time (s) 957.66 Current children cumulated vsize (Kb) 116656 [startup+970.065 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 29237 0 0 0 96566 199 0 0 25 0 1 0 1785988440 117981184 27544 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32030/statm): 28804 27544 145 145 0 28659 0 [pid=32030] vsize: 115216 Current children cumulated CPU time (s) 967.65 Current children cumulated vsize (Kb) 117340 [startup+980.065 s] Raw data (loadavg): 1.00 1.00 0.98 1/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) T 32026 32026 22582 0 -1 0 29381 0 0 0 97563 200 0 0 25 0 1 0 1785988440 118599680 27688 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/32030/statm): 28955 27688 145 145 0 28810 0 [pid=32030] vsize: 115820 Current children cumulated CPU time (s) 977.63 Current children cumulated vsize (Kb) 117944 [startup+990.067 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 29651 0 0 0 98559 201 0 0 25 0 1 0 1785988440 119697408 27958 4294967295 134512640 135094434 3221224432 3221222896 134780607 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 29223 27958 145 145 0 29078 0 [pid=32030] vsize: 116892 Current children cumulated CPU time (s) 987.6 Current children cumulated vsize (Kb) 119016 [startup+1000.07 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 29845 0 0 0 99556 203 0 0 25 0 1 0 1785988440 120475648 28152 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 29413 28152 145 145 0 29268 0 [pid=32030] vsize: 117652 Current children cumulated CPU time (s) 997.59 Current children cumulated vsize (Kb) 119776 [startup+1010.07 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 30048 0 0 0 100553 204 0 0 25 0 1 0 1785988440 121294848 28355 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 29613 28355 145 145 0 29468 0 [pid=32030] vsize: 118452 Current children cumulated CPU time (s) 1007.57 Current children cumulated vsize (Kb) 120576 [startup+1020.07 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 30269 0 0 0 101549 205 0 0 25 0 1 0 1785988440 122200064 28576 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 29834 28576 145 145 0 29689 0 [pid=32030] vsize: 119336 Current children cumulated CPU time (s) 1017.54 Current children cumulated vsize (Kb) 121460 [startup+1030.07 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) T 32026 32026 22582 0 -1 0 30391 0 0 0 102548 206 0 0 25 0 1 0 1785988440 122695680 28698 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/32030/statm): 29955 28698 145 145 0 29810 0 [pid=32030] vsize: 119820 Current children cumulated CPU time (s) 1027.54 Current children cumulated vsize (Kb) 121944 [startup+1040.07 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 30566 0 0 0 103545 207 0 0 25 0 1 0 1785988440 123396096 28873 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 30126 28873 145 145 0 29981 0 [pid=32030] vsize: 120504 Current children cumulated CPU time (s) 1037.52 Current children cumulated vsize (Kb) 122628 [startup+1050.07 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 30763 0 0 0 104542 209 0 0 25 0 1 0 1785988440 124190720 29070 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 30320 29070 145 145 0 30175 0 [pid=32030] vsize: 121280 Current children cumulated CPU time (s) 1047.51 Current children cumulated vsize (Kb) 123404 [startup+1060.07 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) T 32026 32026 22582 0 -1 0 30958 0 0 0 105539 210 0 0 25 0 1 0 1785988440 125005824 29265 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/32030/statm): 30519 29265 145 145 0 30374 0 [pid=32030] vsize: 122076 Current children cumulated CPU time (s) 1057.49 Current children cumulated vsize (Kb) 124200 [startup+1070.07 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 31149 0 0 0 106536 211 0 0 25 0 1 0 1785988440 125779968 29456 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 30708 29456 145 145 0 30563 0 [pid=32030] vsize: 122832 Current children cumulated CPU time (s) 1067.47 Current children cumulated vsize (Kb) 124956 [startup+1080.07 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 31549 0 0 0 107529 215 0 0 25 0 1 0 1785988440 127381504 29856 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32030/statm): 31099 29856 145 145 0 30954 0 [pid=32030] vsize: 124396 Current children cumulated CPU time (s) 1077.44 Current children cumulated vsize (Kb) 126520 [startup+1090.07 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 31740 0 0 0 108525 216 0 0 25 0 1 0 1785988440 128151552 30047 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32030/statm): 31287 30047 145 145 0 31142 0 [pid=32030] vsize: 125148 Current children cumulated CPU time (s) 1087.41 Current children cumulated vsize (Kb) 127272 [startup+1100.07 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 31868 0 0 0 109522 218 0 0 25 0 1 0 1785988440 128688128 30175 4294967295 134512640 135094434 3221224432 3221223056 134557648 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32030/statm): 31418 30175 145 145 0 31273 0 [pid=32030] vsize: 125672 Current children cumulated CPU time (s) 1097.4 Current children cumulated vsize (Kb) 127796 [startup+1110.07 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 32010 0 0 0 110520 219 0 0 25 0 1 0 1785988440 129290240 30317 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32030/statm): 31565 30317 145 145 0 31420 0 [pid=32030] vsize: 126260 Current children cumulated CPU time (s) 1107.39 Current children cumulated vsize (Kb) 128384 [startup+1120.08 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 32280 0 0 0 111516 221 0 0 25 0 1 0 1785988440 130371584 30587 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32030/statm): 31829 30587 145 145 0 31684 0 [pid=32030] vsize: 127316 Current children cumulated CPU time (s) 1117.37 Current children cumulated vsize (Kb) 129440 [startup+1130.08 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 32396 0 0 0 112514 222 0 0 25 0 1 0 1785988440 130850816 30703 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32030/statm): 31946 30703 145 145 0 31801 0 [pid=32030] vsize: 127784 Current children cumulated CPU time (s) 1127.36 Current children cumulated vsize (Kb) 129908 [startup+1140.08 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 32527 0 0 0 113511 223 0 0 25 0 1 0 1785988440 131371008 30834 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32030/statm): 32073 30834 145 145 0 31928 0 [pid=32030] vsize: 128292 Current children cumulated CPU time (s) 1137.34 Current children cumulated vsize (Kb) 130416 [startup+1150.08 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 32812 0 0 0 114506 225 0 0 25 0 1 0 1785988440 132501504 31119 4294967295 134512640 135094434 3221224432 3221223092 134553499 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32030/statm): 32349 31119 145 145 0 32204 0 [pid=32030] vsize: 129396 Current children cumulated CPU time (s) 1147.31 Current children cumulated vsize (Kb) 131520 [startup+1160.08 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 33094 0 0 0 115501 227 0 0 25 0 1 0 1785988440 133636096 31401 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32030/statm): 32626 31401 145 145 0 32481 0 [pid=32030] vsize: 130504 Current children cumulated CPU time (s) 1157.28 Current children cumulated vsize (Kb) 132628 [startup+1170.08 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 33434 0 0 0 116494 231 0 0 25 0 1 0 1785988440 135008256 31741 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32030/statm): 32961 31741 145 145 0 32816 0 [pid=32030] vsize: 131844 Current children cumulated CPU time (s) 1167.25 Current children cumulated vsize (Kb) 133968 [startup+1180.08 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 33694 0 0 0 117489 233 0 0 25 0 1 0 1785988440 136056832 32001 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32030/statm): 33217 32001 145 145 0 33072 0 [pid=32030] vsize: 132868 Current children cumulated CPU time (s) 1177.22 Current children cumulated vsize (Kb) 134992 [startup+1190.08 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 33937 0 0 0 118484 235 0 0 25 0 1 0 1785988440 137039872 32244 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 33457 32244 145 145 0 33312 0 [pid=32030] vsize: 133828 Current children cumulated CPU time (s) 1187.19 Current children cumulated vsize (Kb) 135952 [startup+1200.08 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 34162 0 0 0 119481 236 0 0 25 0 1 0 1785988440 137953280 32469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 33680 32469 145 145 0 33535 0 [pid=32030] vsize: 134720 Current children cumulated CPU time (s) 1197.17 Current children cumulated vsize (Kb) 136844 [startup+1210.08 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 34397 0 0 0 120477 238 0 0 25 0 1 0 1785988440 138891264 32704 4294967295 134512640 135094434 3221224432 3221223104 134556410 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 33909 32704 145 145 0 33764 0 [pid=32030] vsize: 135636 Current children cumulated CPU time (s) 1207.15 Current children cumulated vsize (Kb) 137760 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.08 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 32030 Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32026/statm): 531 226 485 147 0 384 0 [pid=32026] vsize: 2124 Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 34397 0 0 0 120477 238 0 0 25 0 1 0 1785988440 138891264 32704 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32030/statm): 33909 32704 145 145 0 33764 0 [pid=32030] vsize: 135636 Current children cumulated CPU time (s) 1207.15 Current children cumulated vsize (Kb) 137760 Sending SIGTERM to -32026 Sleeping 2 seconds One traced child (pid=32026) ended because it received signal 15 (SIGTERM) One traced child (pid=32030) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.15 CPU time (s): 1207.22 CPU user time (s): 1204.77 CPU system time (s): 2.44963 CPU usage (%): 99.7587 Max. virtual memory (cumulated for all children) (Kb): 137760
ERROR: no interpretation found !