Name | mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-khb05250.opb |
MD5SUM | 18d2c1f575fe90b4288795c634aa1a5b |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 303845819772 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 37494 |
Biggest coefficient in the objective function | 6251324899328 |
Number of bits for the biggest coefficient in the objective function | 43 |
Sum of the numbers in the objective function | 5652283493428566 |
Number of bits of the sum of numbers in the objective function | 53 |
Biggest number in a constraint | 6251324899328 |
Number of bits of the biggest number in a constraint | 43 |
Biggest sum of numbers in a constraint | 5652283493428566 |
Number of bits of the biggest sum of numbers | 53 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1205.48 |
Number of variables | 38297 |
Total number of constraints | 126 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 24 |
Number of constraints which are nor clauses,nor cardinality constraints | 102 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 1530 |
LAUNCH ON wulflinc10 THE 2005-09-19 03:06:55 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2858 boxname=wulflinc10 idbench=514 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 18d2c1f575fe90b4288795c634aa1a5b /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-khb05250.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-khb05250.opb IDLAUNCH: 2858 /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: 861492 kB Buffers: 36936 kB Cached: 108560 kB SwapCached: 228 kB Active: 71232 kB Inactive: 77180 kB HighTotal: 131008 kB HighFree: 53424 kB LowTotal: 903652 kB LowFree: 808068 kB SwapTotal: 2097136 kB SwapFree: 2096756 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6272 kB Slab: 18912 kB Committed_AS: 64164 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-19 03:27:06 (client local time) WITH STATUS 0 IN 1209.48 SECONDS stats: 2858 7 1209.48 0
c Parsing PB file... c Converting 179 PB-constraints to clauses... c -- Unit propagations: pppppp c -- Detecting intervals from adjacent constraints: ############################################################################ c -- Clauses(.)/Splits(s): (none) c ---[ 178]---> BDD-cost: 22 c ---[ 174]---> Adder-cost: 843 maxlim: 149504 bits: 19/18 c ---[ 172]---> Adder-cost: 795 maxlim: 89088 bits: 18/17 c ---[ 170]---> Adder-cost: 939 maxlim: 688128 bits: 21/20 c ---[ 168]---> Adder-cost: 987 maxlim: 1369088 bits: 22/21 c ---[ 166]---> Adder-cost: 699 maxlim: 31744 bits: 16/15 c ---[ 164]---> Adder-cost: 939 maxlim: 572416 bits: 21/20 c ---[ 162]---> Adder-cost: 1035 maxlim: 2426880 bits: 23/22 c ---[ 160]---> Adder-cost: 987 maxlim: 1115136 bits: 22/21 c ---[ 158]---> Adder-cost: 747 maxlim: 33792 bits: 17/16 c ---[ 156]---> Adder-cost: 747 maxlim: 32768 bits: 17/16 c ---[ 154]---> Adder-cost: 1083 maxlim: 5626880 bits: 24/23 c ---[ 152]---> Adder-cost: 939 maxlim: 925696 bits: 21/20 c ---[ 150]---> Adder-cost: 987 maxlim: 1501184 bits: 22/21 c ---[ 148]---> Adder-cost: 843 maxlim: 146432 bits: 19/18 c ---[ 146]---> Adder-cost: 939 maxlim: 629760 bits: 21/20 c ---[ 144]---> Adder-cost: 939 maxlim: 577536 bits: 21/20 c ---[ 142]---> Adder-cost: 843 maxlim: 231424 bits: 19/18 c ---[ 140]---> Adder-cost: 1035 maxlim: 3088384 bits: 23/22 c ---[ 138]---> Adder-cost: 843 maxlim: 259072 bits: 19/18 c ---[ 136]---> Adder-cost: 843 maxlim: 199680 bits: 19/18 c ---[ 134]---> Adder-cost: 747 maxlim: 38912 bits: 17/16 c ---[ 132]---> Adder-cost: 939 maxlim: 826368 bits: 21/20 c ---[ 130]---> Adder-cost: 939 maxlim: 564224 bits: 21/20 c ---[ 128]---> Adder-cost: 891 maxlim: 311296 bits: 20/19 c ---[ 126]---> Adder-cost: 939 maxlim: 833536 bits: 21/20 c ---[ 124]---> Adder-cost: 891 maxlim: 345088 bits: 20/19 c ---[ 122]---> Adder-cost: 1083 maxlim: 4472832 bits: 24/23 c ---[ 120]---> Adder-cost: 939 maxlim: 590848 bits: 21/20 c ---[ 118]---> Adder-cost: 891 maxlim: 493568 bits: 20/19 c ---[ 116]---> Adder-cost: 891 maxlim: 506880 bits: 20/19 c ---[ 114]---> Adder-cost: 843 maxlim: 236544 bits: 19/18 c ---[ 112]---> Adder-cost: 891 maxlim: 329728 bits: 20/19 c ---[ 110]---> Adder-cost: 939 maxlim: 701440 bits: 21/20 c ---[ 108]---> Adder-cost: 1095 maxlim: 13221888 bits: 25/24 c ---[ 106]---> Adder-cost: 891 maxlim: 332800 bits: 20/19 c ---[ 104]---> Adder-cost: 891 maxlim: 374784 bits: 20/19 c ---[ 102]---> Adder-cost: 1035 maxlim: 3759104 bits: 23/22 c ---[ 100]---> Adder-cost: 1035 maxlim: 2266112 bits: 23/22 c ---[ 98]---> Adder-cost: 939 maxlim: 721920 bits: 21/20 c ---[ 96]---> Adder-cost: 891 maxlim: 335872 bits: 20/19 c ---[ 94]---> Adder-cost: 987 maxlim: 1721344 bits: 22/21 c ---[ 92]---> Adder-cost: 987 maxlim: 1143808 bits: 22/21 c ---[ 90]---> Adder-cost: 891 maxlim: 281600 bits: 20/19 c ---[ 88]---> Adder-cost: 891 maxlim: 512000 bits: 20/19 c ---[ 86]---> Adder-cost: 1035 maxlim: 2294784 bits: 23/22 c ---[ 84]---> Adder-cost: 939 maxlim: 750592 bits: 21/20 c ---[ 82]---> Adder-cost: 843 maxlim: 227328 bits: 19/18 c ---[ 80]---> Adder-cost: 747 maxlim: 50176 bits: 17/16 c ---[ 78]---> Adder-cost: 987 maxlim: 1499136 bits: 22/21 c ---[ 76]---> Adder-cost: 843 maxlim: 227328 bits: 19/18 c ---[ 74]---> Adder-cost: 1104 maxlim: 150048743 bits: 28/28 c ---[ 73]---> BDD-cost: 33 c ---[ 72]---> BDD-cost: 33 c ---[ 71]---> BDD-cost: 33 c ---[ 70]---> BDD-cost: 33 c ---[ 69]---> BDD-cost: 33 c ---[ 68]---> BDD-cost: 33 c ---[ 67]---> BDD-cost: 33 c ---[ 66]---> BDD-cost: 33 c ---[ 65]---> BDD-cost: 33 c ---[ 64]---> BDD-cost: 33 c ---[ 63]---> BDD-cost: 33 c ---[ 62]---> BDD-cost: 33 c ---[ 61]---> BDD-cost: 33 c ---[ 60]---> BDD-cost: 33 c ---[ 59]---> BDD-cost: 33 c ---[ 58]---> BDD-cost: 33 c ---[ 57]---> BDD-cost: 33 c ---[ 56]---> BDD-cost: 33 c ---[ 55]---> BDD-cost: 33 c ---[ 54]---> BDD-cost: 33 c ---[ 53]---> BDD-cost: 33 c ---[ 52]---> BDD-cost: 33 c ---[ 51]---> BDD-cost: 33 c ---[ 50]---> BDD-cost: 33 c ---[ 48]---> Adder-cost: 1960 maxlim: 79069134 bits: 27/27 c ---[ 46]---> Adder-cost: 1960 maxlim: 79069134 bits: 27/27 c ---[ 44]---> Adder-cost: 1960 maxlim: 79069134 bits: 27/27 c ---[ 42]---> Adder-cost: 1960 maxlim: 79069134 bits: 27/27 c ---[ 40]---> Adder-cost: 1960 maxlim: 79069134 bits: 27/27 c ---[ 38]---> Adder-cost: 1960 maxlim: 79069134 bits: 27/27 c ---[ 36]---> Adder-cost: 1960 maxlim: 79069134 bits: 27/27 c ---[ 34]---> Adder-cost: 1960 maxlim: 79069134 bits: 27/27 c ---[ 32]---> Adder-cost: 1960 maxlim: 79069134 bits: 27/27 c ---[ 30]---> Adder-cost: 1960 maxlim: 79069134 bits: 27/27 c ---[ 28]---> Adder-cost: 1960 maxlim: 79069134 bits: 27/27 c ---[ 26]---> Adder-cost: 1960 maxlim: 79069134 bits: 27/27 c ---[ 24]---> Adder-cost: 1960 maxlim: 79069134 bits: 27/27 c ---[ 22]---> Adder-cost: 1960 maxlim: 79069134 bits: 27/27 c ---[ 20]---> Adder-cost: 1960 maxlim: 79069134 bits: 27/27 c ---[ 18]---> Adder-cost: 1960 maxlim: 79069134 bits: 27/27 c ---[ 16]---> Adder-cost: 1960 maxlim: 79069134 bits: 27/27 c ---[ 14]---> Adder-cost: 1960 maxlim: 79069134 bits: 27/27 c ---[ 12]---> Adder-cost: 1960 maxlim: 79069134 bits: 27/27 c ---[ 10]---> Adder-cost: 1960 maxlim: 79069134 bits: 27/27 c ---[ 8]---> Adder-cost: 1960 maxlim: 79069134 bits: 27/27 c ---[ 6]---> Adder-cost: 1960 maxlim: 79069134 bits: 27/27 c ---[ 4]---> Adder-cost: 1960 maxlim: 79069134 bits: 27/27 c ---[ 2]---> Adder-cost: 1960 maxlim: 79069134 bits: 27/27 c ---[ 0]---> Adder-cost: 1960 maxlim: 79069134 bits: 27/27 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 651899 2325349 | 217299 0 0 nan | 0.000 % | c | 100 | 651899 2325349 | 239028 100 305 3.0 | 13.317 % | c | 250 | 651867 2325243 | 262931 246 773 3.1 | 13.321 % | c | 475 | 651867 2325243 | 289224 471 1478 3.1 | 13.321 % | c | 812 | 651811 2325057 | 318147 803 2650 3.3 | 13.329 % | c | 1318 | 651787 2324977 | 349962 1307 4359 3.3 | 13.332 % | c | 2077 | 651771 2324925 | 384958 2064 7054 3.4 | 13.334 % | c | 3216 | 651682 2324628 | 423454 3191 11076 3.5 | 13.346 % | c | 4924 | 651626 2324442 | 465799 4894 17215 3.5 | 13.353 % | c | 7486 | 651498 2324018 | 512379 7443 27785 3.7 | 13.370 % | c | 11330 | 651337 2323483 | 563617 11269 41701 3.7 | 13.392 % | c | 17096 | 651199 2323027 | 619979 17014 62443 3.7 | 13.409 % | c | 25745 | 651004 2322380 | 681977 25623 97565 3.8 | 13.433 % | c | 38719 | 650862 2321906 | 750175 38559 152251 3.9 | 13.449 % | c | 58180 | 650821 2321771 | 825192 58011 252817 4.4 | 13.453 % | c | 87372 | 650778 2321626 | 907711 87181 424597 4.9 | 13.456 % |
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/2745/stat): 2745 (minisat+_script) R 2744 2745 22582 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1788336612 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/2745/statm): 174 3 169 147 0 27 0 [pid=2745] 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=2746 New process pid=2747 New process pid=2748 execve syscall for /bin/sed executable One traced child (pid=2747) 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=2748) exited with status: 0 One traced child (pid=2746) exited with status: 0 New process pid=2749 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-khb05250.opb [startup+10.0039 s] Raw data (loadavg): 1.11 1.09 1.06 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 6840 0 0 0 939 31 0 0 24 0 1 0 1788336617 31391744 6201 4294967295 134512640 135094434 3221224432 3221221984 134780516 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2749/statm): 7664 6201 145 145 0 7519 0 [pid=2749] vsize: 30656 Current children cumulated CPU time (s) 9.72 Current children cumulated vsize (Kb) 32780 [startup+20.0045 s] Raw data (loadavg): 1.09 1.09 1.06 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 13538 0 0 0 1874 63 0 0 25 0 1 0 1788336617 64696320 12833 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2749/statm): 15795 12833 145 145 0 15650 0 [pid=2749] vsize: 63180 Current children cumulated CPU time (s) 19.39 Current children cumulated vsize (Kb) 65304 [startup+30.0061 s] Raw data (loadavg): 1.08 1.09 1.06 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 13735 0 0 0 2870 65 0 0 25 0 1 0 1788336617 65499136 13030 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 15991 13030 145 145 0 15846 0 [pid=2749] vsize: 63964 Current children cumulated CPU time (s) 29.37 Current children cumulated vsize (Kb) 66088 [startup+40.0066 s] Raw data (loadavg): 1.06 1.08 1.06 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 13850 0 0 0 3869 66 0 0 25 0 1 0 1788336617 65990656 13145 4294967295 134512640 135094434 3221224432 3221223044 134563148 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16111 13145 145 145 0 15966 0 [pid=2749] vsize: 64444 Current children cumulated CPU time (s) 39.37 Current children cumulated vsize (Kb) 66568 [startup+50.0072 s] Raw data (loadavg): 1.05 1.08 1.06 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 13938 0 0 0 4868 66 0 0 25 0 1 0 1788336617 66338816 13233 4294967295 134512640 135094434 3221224432 3221223072 134562110 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16196 13233 145 145 0 16051 0 [pid=2749] vsize: 64784 Current children cumulated CPU time (s) 49.36 Current children cumulated vsize (Kb) 66908 [startup+60.0077 s] Raw data (loadavg): 1.05 1.08 1.06 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 13994 0 0 0 5867 66 0 0 25 0 1 0 1788336617 66560000 13289 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16250 13289 145 145 0 16105 0 [pid=2749] vsize: 65000 Current children cumulated CPU time (s) 59.35 Current children cumulated vsize (Kb) 67124 [startup+70.0083 s] Raw data (loadavg): 1.04 1.07 1.05 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14037 0 0 0 6866 66 0 0 25 0 1 0 1788336617 66756608 13332 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16298 13332 145 145 0 16153 0 [pid=2749] vsize: 65192 Current children cumulated CPU time (s) 69.34 Current children cumulated vsize (Kb) 67316 [startup+80.0089 s] Raw data (loadavg): 1.03 1.07 1.05 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14062 0 0 0 7866 67 0 0 25 0 1 0 1788336617 66854912 13357 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16322 13357 145 145 0 16177 0 [pid=2749] vsize: 65288 Current children cumulated CPU time (s) 79.35 Current children cumulated vsize (Kb) 67412 [startup+90.0094 s] Raw data (loadavg): 1.03 1.07 1.05 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14085 0 0 0 8865 67 0 0 25 0 1 0 1788336617 67006464 13380 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16359 13380 145 145 0 16214 0 [pid=2749] vsize: 65436 Current children cumulated CPU time (s) 89.34 Current children cumulated vsize (Kb) 67560 [startup+100.009 s] Raw data (loadavg): 1.02 1.07 1.05 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14108 0 0 0 9865 67 0 0 25 0 1 0 1788336617 67088384 13403 4294967295 134512640 135094434 3221224432 3221223044 134563092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16379 13403 145 145 0 16234 0 [pid=2749] vsize: 65516 Current children cumulated CPU time (s) 99.34 Current children cumulated vsize (Kb) 67640 [startup+110.01 s] Raw data (loadavg): 1.02 1.06 1.05 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14127 0 0 0 10865 68 0 0 25 0 1 0 1788336617 67162112 13422 4294967295 134512640 135094434 3221224432 3221223044 134563092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16397 13422 145 145 0 16252 0 [pid=2749] vsize: 65588 Current children cumulated CPU time (s) 109.35 Current children cumulated vsize (Kb) 67712 [startup+120.01 s] Raw data (loadavg): 1.02 1.06 1.05 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14142 0 0 0 11864 68 0 0 25 0 1 0 1788336617 67219456 13437 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16411 13437 145 145 0 16266 0 [pid=2749] vsize: 65644 Current children cumulated CPU time (s) 119.34 Current children cumulated vsize (Kb) 67768 [startup+130.011 s] Raw data (loadavg): 1.01 1.06 1.05 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14153 0 0 0 12865 68 0 0 25 0 1 0 1788336617 67260416 13448 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16421 13448 145 145 0 16276 0 [pid=2749] vsize: 65684 Current children cumulated CPU time (s) 129.35 Current children cumulated vsize (Kb) 67808 [startup+140.011 s] Raw data (loadavg): 1.01 1.06 1.05 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14168 0 0 0 13865 68 0 0 25 0 1 0 1788336617 67313664 13463 4294967295 134512640 135094434 3221224432 3221223072 134562082 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16434 13463 145 145 0 16289 0 [pid=2749] vsize: 65736 Current children cumulated CPU time (s) 139.35 Current children cumulated vsize (Kb) 67860 [startup+150.012 s] Raw data (loadavg): 1.01 1.05 1.05 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14179 0 0 0 14865 68 0 0 25 0 1 0 1788336617 67354624 13474 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16444 13474 145 145 0 16299 0 [pid=2749] vsize: 65776 Current children cumulated CPU time (s) 149.35 Current children cumulated vsize (Kb) 67900 [startup+160.012 s] Raw data (loadavg): 1.01 1.05 1.05 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14188 0 0 0 15865 68 0 0 25 0 1 0 1788336617 67391488 13483 4294967295 134512640 135094434 3221224432 3221223184 134559282 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16453 13483 145 145 0 16308 0 [pid=2749] vsize: 65812 Current children cumulated CPU time (s) 159.35 Current children cumulated vsize (Kb) 67936 [startup+170.013 s] Raw data (loadavg): 1.00 1.05 1.04 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14203 0 0 0 16865 68 0 0 25 0 1 0 1788336617 67444736 13498 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16466 13498 145 145 0 16321 0 [pid=2749] vsize: 65864 Current children cumulated CPU time (s) 169.35 Current children cumulated vsize (Kb) 67988 [startup+180.013 s] Raw data (loadavg): 1.00 1.05 1.04 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14214 0 0 0 17865 68 0 0 25 0 1 0 1788336617 67477504 13509 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16474 13509 145 145 0 16329 0 [pid=2749] vsize: 65896 Current children cumulated CPU time (s) 179.35 Current children cumulated vsize (Kb) 68020 [startup+190.014 s] Raw data (loadavg): 1.00 1.05 1.04 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14225 0 0 0 18865 68 0 0 25 0 1 0 1788336617 67518464 13520 4294967295 134512640 135094434 3221224432 3221223072 134562113 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16484 13520 145 145 0 16339 0 [pid=2749] vsize: 65936 Current children cumulated CPU time (s) 189.35 Current children cumulated vsize (Kb) 68060 [startup+200.014 s] Raw data (loadavg): 1.00 1.04 1.04 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14233 0 0 0 19865 68 0 0 25 0 1 0 1788336617 67547136 13528 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16491 13528 145 145 0 16346 0 [pid=2749] vsize: 65964 Current children cumulated CPU time (s) 199.35 Current children cumulated vsize (Kb) 68088 [startup+210.014 s] Raw data (loadavg): 1.00 1.04 1.04 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14243 0 0 0 20865 68 0 0 25 0 1 0 1788336617 67584000 13538 4294967295 134512640 135094434 3221224432 3221223044 134563071 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16500 13538 145 145 0 16355 0 [pid=2749] vsize: 66000 Current children cumulated CPU time (s) 209.35 Current children cumulated vsize (Kb) 68124 [startup+220.015 s] Raw data (loadavg): 1.00 1.04 1.04 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14252 0 0 0 21864 69 0 0 25 0 1 0 1788336617 67616768 13547 4294967295 134512640 135094434 3221224432 3221223088 134561688 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16508 13547 145 145 0 16363 0 [pid=2749] vsize: 66032 Current children cumulated CPU time (s) 219.35 Current children cumulated vsize (Kb) 68156 [startup+230.015 s] Raw data (loadavg): 1.00 1.04 1.04 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14258 0 0 0 22864 70 0 0 25 0 1 0 1788336617 67641344 13553 4294967295 134512640 135094434 3221224432 3221223072 134562108 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16514 13553 145 145 0 16369 0 [pid=2749] vsize: 66056 Current children cumulated CPU time (s) 229.36 Current children cumulated vsize (Kb) 68180 [startup+240.016 s] Raw data (loadavg): 1.00 1.04 1.04 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14296 0 0 0 23863 71 0 0 25 0 1 0 1788336617 67919872 13591 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16582 13591 145 145 0 16437 0 [pid=2749] vsize: 66328 Current children cumulated CPU time (s) 239.36 Current children cumulated vsize (Kb) 68452 [startup+250.015 s] Raw data (loadavg): 1.00 1.03 1.04 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14297 0 0 0 24863 71 0 0 25 0 1 0 1788336617 67919872 13592 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16582 13592 145 145 0 16437 0 [pid=2749] vsize: 66328 Current children cumulated CPU time (s) 249.36 Current children cumulated vsize (Kb) 68452 [startup+260.016 s] Raw data (loadavg): 1.00 1.03 1.04 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14298 0 0 0 25863 71 0 0 25 0 1 0 1788336617 67919872 13593 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16582 13593 145 145 0 16437 0 [pid=2749] vsize: 66328 Current children cumulated CPU time (s) 259.36 Current children cumulated vsize (Kb) 68452 [startup+270.017 s] Raw data (loadavg): 1.00 1.03 1.03 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14299 0 0 0 26863 71 0 0 25 0 1 0 1788336617 67919872 13594 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16582 13594 145 145 0 16437 0 [pid=2749] vsize: 66328 Current children cumulated CPU time (s) 269.36 Current children cumulated vsize (Kb) 68452 [startup+280.017 s] Raw data (loadavg): 1.00 1.03 1.03 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14302 0 0 0 27863 72 0 0 25 0 1 0 1788336617 67932160 13597 4294967295 134512640 135094434 3221224432 3221223044 134563130 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16585 13597 145 145 0 16440 0 [pid=2749] vsize: 66340 Current children cumulated CPU time (s) 279.37 Current children cumulated vsize (Kb) 68464 [startup+290.019 s] Raw data (loadavg): 1.00 1.03 1.03 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14310 0 0 0 28863 72 0 0 25 0 1 0 1788336617 67960832 13605 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16592 13605 145 145 0 16447 0 [pid=2749] vsize: 66368 Current children cumulated CPU time (s) 289.37 Current children cumulated vsize (Kb) 68492 [startup+300.019 s] Raw data (loadavg): 1.00 1.03 1.03 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14318 0 0 0 29863 72 0 0 25 0 1 0 1788336617 67989504 13613 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16599 13613 145 145 0 16454 0 [pid=2749] vsize: 66396 Current children cumulated CPU time (s) 299.37 Current children cumulated vsize (Kb) 68520 [startup+310.02 s] Raw data (loadavg): 1.00 1.03 1.03 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14328 0 0 0 30862 72 0 0 25 0 1 0 1788336617 68026368 13623 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2749/statm): 16608 13623 145 145 0 16463 0 [pid=2749] vsize: 66432 Current children cumulated CPU time (s) 309.36 Current children cumulated vsize (Kb) 68556 [startup+320.02 s] Raw data (loadavg): 1.00 1.02 1.03 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14333 0 0 0 31862 73 0 0 25 0 1 0 1788336617 68046848 13628 4294967295 134512640 135094434 3221224432 3221223092 134553499 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16613 13628 145 145 0 16468 0 [pid=2749] vsize: 66452 Current children cumulated CPU time (s) 319.37 Current children cumulated vsize (Kb) 68576 [startup+330.021 s] Raw data (loadavg): 1.00 1.02 1.03 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14349 0 0 0 32862 73 0 0 25 0 1 0 1788336617 68104192 13644 4294967295 134512640 135094434 3221224432 3221223044 134563043 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16627 13644 145 145 0 16482 0 [pid=2749] vsize: 66508 Current children cumulated CPU time (s) 329.37 Current children cumulated vsize (Kb) 68632 [startup+340.022 s] Raw data (loadavg): 1.00 1.02 1.03 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14359 0 0 0 33862 73 0 0 25 0 1 0 1788336617 68141056 13654 4294967295 134512640 135094434 3221224432 3221223088 134561448 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16636 13654 145 145 0 16491 0 [pid=2749] vsize: 66544 Current children cumulated CPU time (s) 339.37 Current children cumulated vsize (Kb) 68668 [startup+350.022 s] Raw data (loadavg): 1.00 1.02 1.03 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14369 0 0 0 34862 73 0 0 25 0 1 0 1788336617 68177920 13664 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16645 13664 145 145 0 16500 0 [pid=2749] vsize: 66580 Current children cumulated CPU time (s) 349.37 Current children cumulated vsize (Kb) 68704 [startup+360.023 s] Raw data (loadavg): 1.00 1.02 1.03 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14386 0 0 0 35862 73 0 0 25 0 1 0 1788336617 68243456 13681 4294967295 134512640 135094434 3221224432 3221223076 134561789 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16661 13681 145 145 0 16516 0 [pid=2749] vsize: 66644 Current children cumulated CPU time (s) 359.37 Current children cumulated vsize (Kb) 68768 [startup+370.023 s] Raw data (loadavg): 1.00 1.02 1.02 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14400 0 0 0 36862 73 0 0 25 0 1 0 1788336617 68296704 13695 4294967295 134512640 135094434 3221224432 3221223136 134554440 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16674 13695 145 145 0 16529 0 [pid=2749] vsize: 66696 Current children cumulated CPU time (s) 369.37 Current children cumulated vsize (Kb) 68820 [startup+380.024 s] Raw data (loadavg): 1.00 1.02 1.02 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14409 0 0 0 37862 74 0 0 25 0 1 0 1788336617 68329472 13704 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16682 13704 145 145 0 16537 0 [pid=2749] vsize: 66728 Current children cumulated CPU time (s) 379.38 Current children cumulated vsize (Kb) 68852 [startup+390.024 s] Raw data (loadavg): 1.00 1.02 1.02 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14414 0 0 0 38862 74 0 0 25 0 1 0 1788336617 68349952 13709 4294967295 134512640 135094434 3221224432 3221223044 134563077 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16687 13709 145 145 0 16542 0 [pid=2749] vsize: 66748 Current children cumulated CPU time (s) 389.38 Current children cumulated vsize (Kb) 68872 [startup+400.025 s] Raw data (loadavg): 1.00 1.02 1.02 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14436 0 0 0 39862 74 0 0 25 0 1 0 1788336617 68431872 13731 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16707 13731 145 145 0 16562 0 [pid=2749] vsize: 66828 Current children cumulated CPU time (s) 399.38 Current children cumulated vsize (Kb) 68952 [startup+410.025 s] Raw data (loadavg): 1.00 1.02 1.02 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14450 0 0 0 40862 74 0 0 25 0 1 0 1788336617 68485120 13745 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16720 13745 145 145 0 16575 0 [pid=2749] vsize: 66880 Current children cumulated CPU time (s) 409.38 Current children cumulated vsize (Kb) 69004 [startup+420.025 s] Raw data (loadavg): 1.00 1.02 1.02 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14460 0 0 0 41862 74 0 0 25 0 1 0 1788336617 68517888 13755 4294967295 134512640 135094434 3221224432 3221223072 134562095 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16728 13755 145 145 0 16583 0 [pid=2749] vsize: 66912 Current children cumulated CPU time (s) 419.38 Current children cumulated vsize (Kb) 69036 [startup+430.026 s] Raw data (loadavg): 1.00 1.01 1.02 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14471 0 0 0 42862 74 0 0 25 0 1 0 1788336617 68558848 13766 4294967295 134512640 135094434 3221224432 3221223104 134556257 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16738 13766 145 145 0 16593 0 [pid=2749] vsize: 66952 Current children cumulated CPU time (s) 429.38 Current children cumulated vsize (Kb) 69076 [startup+440.026 s] Raw data (loadavg): 1.00 1.01 1.02 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14484 0 0 0 43862 74 0 0 25 0 1 0 1788336617 68608000 13779 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16750 13779 145 145 0 16605 0 [pid=2749] vsize: 67000 Current children cumulated CPU time (s) 439.38 Current children cumulated vsize (Kb) 69124 [startup+450.026 s] Raw data (loadavg): 1.00 1.01 1.02 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14492 0 0 0 44862 75 0 0 25 0 1 0 1788336617 68636672 13787 4294967295 134512640 135094434 3221224432 3221223072 134562115 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16757 13787 145 145 0 16612 0 [pid=2749] vsize: 67028 Current children cumulated CPU time (s) 449.39 Current children cumulated vsize (Kb) 69152 [startup+460.026 s] Raw data (loadavg): 1.00 1.01 1.02 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14505 0 0 0 45861 75 0 0 25 0 1 0 1788336617 68685824 13800 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16769 13800 145 145 0 16624 0 [pid=2749] vsize: 67076 Current children cumulated CPU time (s) 459.38 Current children cumulated vsize (Kb) 69200 [startup+470.027 s] Raw data (loadavg): 1.00 1.01 1.02 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14517 0 0 0 46861 75 0 0 25 0 1 0 1788336617 68730880 13812 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16780 13812 145 145 0 16635 0 [pid=2749] vsize: 67120 Current children cumulated CPU time (s) 469.38 Current children cumulated vsize (Kb) 69244 [startup+480.027 s] Raw data (loadavg): 1.00 1.01 1.01 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14528 0 0 0 47861 75 0 0 25 0 1 0 1788336617 68775936 13823 4294967295 134512640 135094434 3221224432 3221223044 134563061 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16791 13823 145 145 0 16646 0 [pid=2749] vsize: 67164 Current children cumulated CPU time (s) 479.38 Current children cumulated vsize (Kb) 69288 [startup+490.028 s] Raw data (loadavg): 1.00 1.01 1.01 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14539 0 0 0 48861 75 0 0 25 0 1 0 1788336617 68816896 13834 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16801 13834 145 145 0 16656 0 [pid=2749] vsize: 67204 Current children cumulated CPU time (s) 489.38 Current children cumulated vsize (Kb) 69328 [startup+500.029 s] Raw data (loadavg): 1.00 1.01 1.01 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14554 0 0 0 49860 76 0 0 25 0 1 0 1788336617 68874240 13849 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2749/statm): 16815 13849 145 145 0 16670 0 [pid=2749] vsize: 67260 Current children cumulated CPU time (s) 499.38 Current children cumulated vsize (Kb) 69384 [startup+510.029 s] Raw data (loadavg): 1.00 1.01 1.01 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14568 0 0 0 50860 76 0 0 25 0 1 0 1788336617 68927488 13863 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16828 13863 145 145 0 16683 0 [pid=2749] vsize: 67312 Current children cumulated CPU time (s) 509.38 Current children cumulated vsize (Kb) 69436 [startup+520.03 s] Raw data (loadavg): 1.00 1.01 1.01 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14587 0 0 0 51860 77 0 0 25 0 1 0 1788336617 68997120 13882 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16845 13882 145 145 0 16700 0 [pid=2749] vsize: 67380 Current children cumulated CPU time (s) 519.39 Current children cumulated vsize (Kb) 69504 [startup+530.03 s] Raw data (loadavg): 1.00 1.00 1.01 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14595 0 0 0 52860 77 0 0 25 0 1 0 1788336617 69029888 13890 4294967295 134512640 135094434 3221224432 3221223044 134563061 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16853 13890 145 145 0 16708 0 [pid=2749] vsize: 67412 Current children cumulated CPU time (s) 529.39 Current children cumulated vsize (Kb) 69536 [startup+540.031 s] Raw data (loadavg): 1.00 1.00 1.01 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14605 0 0 0 53860 77 0 0 25 0 1 0 1788336617 69066752 13900 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16862 13900 145 145 0 16717 0 [pid=2749] vsize: 67448 Current children cumulated CPU time (s) 539.39 Current children cumulated vsize (Kb) 69572 [startup+550.03 s] Raw data (loadavg): 1.00 1.00 1.01 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14618 0 0 0 54860 77 0 0 25 0 1 0 1788336617 69115904 13913 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16874 13913 145 145 0 16729 0 [pid=2749] vsize: 67496 Current children cumulated CPU time (s) 549.39 Current children cumulated vsize (Kb) 69620 [startup+560.031 s] Raw data (loadavg): 1.00 1.00 1.01 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14629 0 0 0 55860 77 0 0 25 0 1 0 1788336617 69156864 13924 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16884 13924 145 145 0 16739 0 [pid=2749] vsize: 67536 Current children cumulated CPU time (s) 559.39 Current children cumulated vsize (Kb) 69660 [startup+570.031 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14639 0 0 0 56859 77 0 0 25 0 1 0 1788336617 69193728 13934 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16893 13934 145 145 0 16748 0 [pid=2749] vsize: 67572 Current children cumulated CPU time (s) 569.38 Current children cumulated vsize (Kb) 69696 [startup+580.032 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14650 0 0 0 57860 77 0 0 25 0 1 0 1788336617 69238784 13945 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16904 13945 145 145 0 16759 0 [pid=2749] vsize: 67616 Current children cumulated CPU time (s) 579.39 Current children cumulated vsize (Kb) 69740 [startup+590.033 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14659 0 0 0 58860 77 0 0 25 0 1 0 1788336617 69533696 13954 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16976 13954 145 145 0 16831 0 [pid=2749] vsize: 67904 Current children cumulated CPU time (s) 589.39 Current children cumulated vsize (Kb) 70028 [startup+600.033 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14675 0 0 0 59860 78 0 0 25 0 1 0 1788336617 69595136 13970 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 16991 13970 145 145 0 16846 0 [pid=2749] vsize: 67964 Current children cumulated CPU time (s) 599.4 Current children cumulated vsize (Kb) 70088 [startup+610.034 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14687 0 0 0 60860 78 0 0 25 0 1 0 1788336617 69640192 13982 4294967295 134512640 135094434 3221224432 3221223088 134557859 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17002 13982 145 145 0 16857 0 [pid=2749] vsize: 68008 Current children cumulated CPU time (s) 609.4 Current children cumulated vsize (Kb) 70132 [startup+620.034 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14697 0 0 0 61860 78 0 0 25 0 1 0 1788336617 69677056 13992 4294967295 134512640 135094434 3221224432 3221223088 134557875 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17011 13992 145 145 0 16866 0 [pid=2749] vsize: 68044 Current children cumulated CPU time (s) 619.4 Current children cumulated vsize (Kb) 70168 [startup+630.035 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14704 0 0 0 62860 78 0 0 25 0 1 0 1788336617 69705728 13999 4294967295 134512640 135094434 3221224432 3221223088 134561778 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17018 13999 145 145 0 16873 0 [pid=2749] vsize: 68072 Current children cumulated CPU time (s) 629.4 Current children cumulated vsize (Kb) 70196 [startup+640.035 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14717 0 0 0 63860 78 0 0 25 0 1 0 1788336617 69754880 14012 4294967295 134512640 135094434 3221224432 3221223044 134563110 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17030 14012 145 145 0 16885 0 [pid=2749] vsize: 68120 Current children cumulated CPU time (s) 639.4 Current children cumulated vsize (Kb) 70244 [startup+650.036 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14729 0 0 0 64860 78 0 0 25 0 1 0 1788336617 69799936 14024 4294967295 134512640 135094434 3221224432 3221223088 134557818 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17041 14024 145 145 0 16896 0 [pid=2749] vsize: 68164 Current children cumulated CPU time (s) 649.4 Current children cumulated vsize (Kb) 70288 [startup+660.036 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14748 0 0 0 65860 78 0 0 25 0 1 0 1788336617 69873664 14043 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17059 14043 145 145 0 16914 0 [pid=2749] vsize: 68236 Current children cumulated CPU time (s) 659.4 Current children cumulated vsize (Kb) 70360 [startup+670.037 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14763 0 0 0 66860 78 0 0 25 0 1 0 1788336617 69931008 14058 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17073 14058 145 145 0 16928 0 [pid=2749] vsize: 68292 Current children cumulated CPU time (s) 669.4 Current children cumulated vsize (Kb) 70416 [startup+680.038 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14779 0 0 0 67860 78 0 0 25 0 1 0 1788336617 69992448 14074 4294967295 134512640 135094434 3221224432 3221223044 134563024 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17088 14074 145 145 0 16943 0 [pid=2749] vsize: 68352 Current children cumulated CPU time (s) 679.4 Current children cumulated vsize (Kb) 70476 [startup+690.038 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14793 0 0 0 68860 78 0 0 25 0 1 0 1788336617 70045696 14088 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17101 14088 145 145 0 16956 0 [pid=2749] vsize: 68404 Current children cumulated CPU time (s) 689.4 Current children cumulated vsize (Kb) 70528 [startup+700.038 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14801 0 0 0 69860 78 0 0 25 0 1 0 1788336617 70074368 14096 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17108 14096 145 145 0 16963 0 [pid=2749] vsize: 68432 Current children cumulated CPU time (s) 699.4 Current children cumulated vsize (Kb) 70556 [startup+710.039 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14815 0 0 0 70860 79 0 0 25 0 1 0 1788336617 70127616 14110 4294967295 134512640 135094434 3221224432 3221223072 134562144 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17121 14110 145 145 0 16976 0 [pid=2749] vsize: 68484 Current children cumulated CPU time (s) 709.41 Current children cumulated vsize (Kb) 70608 [startup+720.04 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14828 0 0 0 71860 79 0 0 25 0 1 0 1788336617 70176768 14123 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17133 14123 145 145 0 16988 0 [pid=2749] vsize: 68532 Current children cumulated CPU time (s) 719.41 Current children cumulated vsize (Kb) 70656 [startup+730.04 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14842 0 0 0 72861 79 0 0 25 0 1 0 1788336617 70230016 14137 4294967295 134512640 135094434 3221224432 3221223156 134558440 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17146 14137 145 145 0 17001 0 [pid=2749] vsize: 68584 Current children cumulated CPU time (s) 729.42 Current children cumulated vsize (Kb) 70708 [startup+740.041 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14851 0 0 0 73861 79 0 0 25 0 1 0 1788336617 70266880 14146 4294967295 134512640 135094434 3221224432 3221223044 134563087 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17155 14146 145 145 0 17010 0 [pid=2749] vsize: 68620 Current children cumulated CPU time (s) 739.42 Current children cumulated vsize (Kb) 70744 [startup+750.04 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14865 0 0 0 74861 79 0 0 25 0 1 0 1788336617 70320128 14160 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17168 14160 145 145 0 17023 0 [pid=2749] vsize: 68672 Current children cumulated CPU time (s) 749.42 Current children cumulated vsize (Kb) 70796 [startup+760.041 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14876 0 0 0 75861 79 0 0 25 0 1 0 1788336617 70361088 14171 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17178 14171 145 145 0 17033 0 [pid=2749] vsize: 68712 Current children cumulated CPU time (s) 759.42 Current children cumulated vsize (Kb) 70836 [startup+770.042 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14890 0 0 0 76861 79 0 0 25 0 1 0 1788336617 70414336 14185 4294967295 134512640 135094434 3221224432 3221223072 134538541 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17191 14185 145 145 0 17046 0 [pid=2749] vsize: 68764 Current children cumulated CPU time (s) 769.42 Current children cumulated vsize (Kb) 70888 [startup+780.042 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14903 0 0 0 77861 79 0 0 25 0 1 0 1788336617 70463488 14198 4294967295 134512640 135094434 3221224432 3221223044 134563094 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17203 14198 145 145 0 17058 0 [pid=2749] vsize: 68812 Current children cumulated CPU time (s) 779.42 Current children cumulated vsize (Kb) 70936 [startup+790.043 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14915 0 0 0 78861 79 0 0 25 0 1 0 1788336617 70508544 14210 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17214 14210 145 145 0 17069 0 [pid=2749] vsize: 68856 Current children cumulated CPU time (s) 789.42 Current children cumulated vsize (Kb) 70980 [startup+800.042 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14922 0 0 0 79861 80 0 0 25 0 1 0 1788336617 70537216 14217 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17221 14217 145 145 0 17076 0 [pid=2749] vsize: 68884 Current children cumulated CPU time (s) 799.43 Current children cumulated vsize (Kb) 71008 [startup+810.043 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14934 0 0 0 80861 80 0 0 25 0 1 0 1788336617 70582272 14229 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17232 14229 145 145 0 17087 0 [pid=2749] vsize: 68928 Current children cumulated CPU time (s) 809.43 Current children cumulated vsize (Kb) 71052 [startup+820.043 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14946 0 0 0 81860 80 0 0 25 0 1 0 1788336617 70627328 14241 4294967295 134512640 135094434 3221224432 3221223044 134563074 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17243 14241 145 145 0 17098 0 [pid=2749] vsize: 68972 Current children cumulated CPU time (s) 819.42 Current children cumulated vsize (Kb) 71096 [startup+830.047 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14958 0 0 0 82859 82 0 0 25 0 1 0 1788336617 70672384 14253 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17254 14253 145 145 0 17109 0 [pid=2749] vsize: 69016 Current children cumulated CPU time (s) 829.43 Current children cumulated vsize (Kb) 71140 [startup+840.048 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14970 0 0 0 83859 82 0 0 25 0 1 0 1788336617 70717440 14265 4294967295 134512640 135094434 3221224432 3221223044 134563092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17265 14265 145 145 0 17120 0 [pid=2749] vsize: 69060 Current children cumulated CPU time (s) 839.43 Current children cumulated vsize (Kb) 71184 [startup+850.047 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14981 0 0 0 84858 82 0 0 25 0 1 0 1788336617 70758400 14276 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17275 14276 145 145 0 17130 0 [pid=2749] vsize: 69100 Current children cumulated CPU time (s) 849.42 Current children cumulated vsize (Kb) 71224 [startup+860.048 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14994 0 0 0 85858 82 0 0 25 0 1 0 1788336617 70807552 14289 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17287 14289 145 145 0 17142 0 [pid=2749] vsize: 69148 Current children cumulated CPU time (s) 859.42 Current children cumulated vsize (Kb) 71272 [startup+870.048 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15003 0 0 0 86858 83 0 0 25 0 1 0 1788336617 70844416 14298 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17296 14298 145 145 0 17151 0 [pid=2749] vsize: 69184 Current children cumulated CPU time (s) 869.43 Current children cumulated vsize (Kb) 71308 [startup+880.05 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15019 0 0 0 87858 83 0 0 25 0 1 0 1788336617 70905856 14314 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17311 14314 145 145 0 17166 0 [pid=2749] vsize: 69244 Current children cumulated CPU time (s) 879.43 Current children cumulated vsize (Kb) 71368 [startup+890.05 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15029 0 0 0 88858 83 0 0 25 0 1 0 1788336617 70942720 14324 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17320 14324 145 145 0 17175 0 [pid=2749] vsize: 69280 Current children cumulated CPU time (s) 889.43 Current children cumulated vsize (Kb) 71404 [startup+900.05 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15045 0 0 0 89857 83 0 0 25 0 1 0 1788336617 71004160 14340 4294967295 134512640 135094434 3221224432 3221223044 134563127 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17335 14340 145 145 0 17190 0 [pid=2749] vsize: 69340 Current children cumulated CPU time (s) 899.42 Current children cumulated vsize (Kb) 71464 [startup+910.051 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15061 0 0 0 90857 84 0 0 25 0 1 0 1788336617 71061504 14356 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17349 14356 145 145 0 17204 0 [pid=2749] vsize: 69396 Current children cumulated CPU time (s) 909.43 Current children cumulated vsize (Kb) 71520 [startup+920.051 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15079 0 0 0 91857 84 0 0 25 0 1 0 1788336617 71131136 14374 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17366 14374 145 145 0 17221 0 [pid=2749] vsize: 69464 Current children cumulated CPU time (s) 919.43 Current children cumulated vsize (Kb) 71588 [startup+930.052 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15094 0 0 0 92857 84 0 0 25 0 1 0 1788336617 71188480 14389 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17380 14389 145 145 0 17235 0 [pid=2749] vsize: 69520 Current children cumulated CPU time (s) 929.43 Current children cumulated vsize (Kb) 71644 [startup+940.052 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15116 0 0 0 93857 84 0 0 25 0 1 0 1788336617 71270400 14411 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17400 14411 145 145 0 17255 0 [pid=2749] vsize: 69600 Current children cumulated CPU time (s) 939.43 Current children cumulated vsize (Kb) 71724 [startup+950.053 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15126 0 0 0 94857 84 0 0 25 0 1 0 1788336617 71307264 14421 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17409 14421 145 145 0 17264 0 [pid=2749] vsize: 69636 Current children cumulated CPU time (s) 949.43 Current children cumulated vsize (Kb) 71760 [startup+960.053 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15162 0 0 0 95857 84 0 0 25 0 1 0 1788336617 71446528 14457 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17443 14457 145 145 0 17298 0 [pid=2749] vsize: 69772 Current children cumulated CPU time (s) 959.43 Current children cumulated vsize (Kb) 71896 [startup+970.054 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15174 0 0 0 96857 85 0 0 25 0 1 0 1788336617 71491584 14469 4294967295 134512640 135094434 3221224432 3221223088 134561502 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17454 14469 145 145 0 17309 0 [pid=2749] vsize: 69816 Current children cumulated CPU time (s) 969.44 Current children cumulated vsize (Kb) 71940 [startup+980.054 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15184 0 0 0 97857 85 0 0 25 0 1 0 1788336617 71528448 14479 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17463 14479 145 145 0 17318 0 [pid=2749] vsize: 69852 Current children cumulated CPU time (s) 979.44 Current children cumulated vsize (Kb) 71976 [startup+990.055 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15195 0 0 0 98857 85 0 0 25 0 1 0 1788336617 71573504 14490 4294967295 134512640 135094434 3221224432 3221223184 134559282 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17474 14490 145 145 0 17329 0 [pid=2749] vsize: 69896 Current children cumulated CPU time (s) 989.44 Current children cumulated vsize (Kb) 72020 [startup+1000.05 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15231 0 0 0 99857 85 0 0 25 0 1 0 1788336617 71712768 14526 4294967295 134512640 135094434 3221224432 3221223044 134563057 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17508 14526 145 145 0 17363 0 [pid=2749] vsize: 70032 Current children cumulated CPU time (s) 999.44 Current children cumulated vsize (Kb) 72156 [startup+1010.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15260 0 0 0 100856 85 0 0 25 0 1 0 1788336617 71819264 14555 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17534 14555 145 145 0 17389 0 [pid=2749] vsize: 70136 Current children cumulated CPU time (s) 1009.43 Current children cumulated vsize (Kb) 72260 [startup+1020.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15278 0 0 0 101856 86 0 0 25 0 1 0 1788336617 71888896 14573 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17551 14573 145 145 0 17406 0 [pid=2749] vsize: 70204 Current children cumulated CPU time (s) 1019.44 Current children cumulated vsize (Kb) 72328 [startup+1030.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15291 0 0 0 102856 86 0 0 25 0 1 0 1788336617 71938048 14586 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17563 14586 145 145 0 17418 0 [pid=2749] vsize: 70252 Current children cumulated CPU time (s) 1029.44 Current children cumulated vsize (Kb) 72376 [startup+1040.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15302 0 0 0 103856 86 0 0 25 0 1 0 1788336617 71979008 14597 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17573 14597 145 145 0 17428 0 [pid=2749] vsize: 70292 Current children cumulated CPU time (s) 1039.44 Current children cumulated vsize (Kb) 72416 [startup+1050.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15320 0 0 0 104855 87 0 0 25 0 1 0 1788336617 72048640 14615 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17590 14615 145 145 0 17445 0 [pid=2749] vsize: 70360 Current children cumulated CPU time (s) 1049.44 Current children cumulated vsize (Kb) 72484 [startup+1060.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15345 0 0 0 105856 87 0 0 25 0 1 0 1788336617 72146944 14640 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17614 14640 145 145 0 17469 0 [pid=2749] vsize: 70456 Current children cumulated CPU time (s) 1059.45 Current children cumulated vsize (Kb) 72580 [startup+1070.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15364 0 0 0 106856 87 0 0 25 0 1 0 1788336617 72216576 14659 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17631 14659 145 145 0 17486 0 [pid=2749] vsize: 70524 Current children cumulated CPU time (s) 1069.45 Current children cumulated vsize (Kb) 72648 [startup+1080.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15381 0 0 0 107855 87 0 0 25 0 1 0 1788336617 72282112 14676 4294967295 134512640 135094434 3221224432 3221223056 134557669 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17647 14676 145 145 0 17502 0 [pid=2749] vsize: 70588 Current children cumulated CPU time (s) 1079.44 Current children cumulated vsize (Kb) 72712 [startup+1090.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15394 0 0 0 108855 87 0 0 25 0 1 0 1788336617 72331264 14689 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17659 14689 145 145 0 17514 0 [pid=2749] vsize: 70636 Current children cumulated CPU time (s) 1089.44 Current children cumulated vsize (Kb) 72760 [startup+1100.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15423 0 0 0 109855 87 0 0 25 0 1 0 1788336617 72445952 14718 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17687 14718 145 145 0 17542 0 [pid=2749] vsize: 70748 Current children cumulated CPU time (s) 1099.44 Current children cumulated vsize (Kb) 72872 [startup+1110.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15435 0 0 0 110855 87 0 0 25 0 1 0 1788336617 72491008 14730 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17698 14730 145 145 0 17553 0 [pid=2749] vsize: 70792 Current children cumulated CPU time (s) 1109.44 Current children cumulated vsize (Kb) 72916 [startup+1120.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15451 0 0 0 111855 87 0 0 25 0 1 0 1788336617 72552448 14746 4294967295 134512640 135094434 3221224432 3221223088 134561476 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17713 14746 145 145 0 17568 0 [pid=2749] vsize: 70852 Current children cumulated CPU time (s) 1119.44 Current children cumulated vsize (Kb) 72976 [startup+1130.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15465 0 0 0 112855 88 0 0 25 0 1 0 1788336617 72605696 14760 4294967295 134512640 135094434 3221224432 3221223044 134563064 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17726 14760 145 145 0 17581 0 [pid=2749] vsize: 70904 Current children cumulated CPU time (s) 1129.45 Current children cumulated vsize (Kb) 73028 [startup+1140.07 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15476 0 0 0 113855 88 0 0 25 0 1 0 1788336617 72646656 14771 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17736 14771 145 145 0 17591 0 [pid=2749] vsize: 70944 Current children cumulated CPU time (s) 1139.45 Current children cumulated vsize (Kb) 73068 [startup+1150.07 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15483 0 0 0 114855 88 0 0 25 0 1 0 1788336617 72675328 14778 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17743 14778 145 145 0 17598 0 [pid=2749] vsize: 70972 Current children cumulated CPU time (s) 1149.45 Current children cumulated vsize (Kb) 73096 [startup+1160.07 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15503 0 0 0 115855 88 0 0 25 0 1 0 1788336617 72753152 14798 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17762 14798 145 145 0 17617 0 [pid=2749] vsize: 71048 Current children cumulated CPU time (s) 1159.45 Current children cumulated vsize (Kb) 73172 [startup+1170.07 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15513 0 0 0 116855 88 0 0 25 0 1 0 1788336617 72790016 14808 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17771 14808 145 145 0 17626 0 [pid=2749] vsize: 71084 Current children cumulated CPU time (s) 1169.45 Current children cumulated vsize (Kb) 73208 [startup+1180.07 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15528 0 0 0 117855 88 0 0 25 0 1 0 1788336617 72843264 14823 4294967295 134512640 135094434 3221224432 3221223044 134563089 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17784 14823 145 145 0 17639 0 [pid=2749] vsize: 71136 Current children cumulated CPU time (s) 1179.45 Current children cumulated vsize (Kb) 73260 [startup+1190.07 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15539 0 0 0 118856 88 0 0 25 0 1 0 1788336617 72888320 14834 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17795 14834 145 145 0 17650 0 [pid=2749] vsize: 71180 Current children cumulated CPU time (s) 1189.46 Current children cumulated vsize (Kb) 73304 [startup+1200.07 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15554 0 0 0 119855 89 0 0 25 0 1 0 1788336617 72945664 14849 4294967295 134512640 135094434 3221224432 3221223088 134561505 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17809 14849 145 145 0 17664 0 [pid=2749] vsize: 71236 Current children cumulated CPU time (s) 1199.46 Current children cumulated vsize (Kb) 73360 [startup+1210.07 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15583 0 0 0 120855 89 0 0 25 0 1 0 1788336617 73056256 14878 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17836 14878 145 145 0 17691 0 [pid=2749] vsize: 71344 Current children cumulated CPU time (s) 1209.46 Current children cumulated vsize (Kb) 73468 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.07 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 2749 Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/2745/statm): 531 226 485 147 0 384 0 [pid=2745] vsize: 2124 Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15583 0 0 0 120855 89 0 0 25 0 1 0 1788336617 73056256 14878 4294967295 134512640 135094434 3221224432 3221223044 134563043 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2749/statm): 17836 14878 145 145 0 17691 0 [pid=2749] vsize: 71344 Current children cumulated CPU time (s) 1209.46 Current children cumulated vsize (Kb) 73468 Sending SIGTERM to -2745 Sleeping 2 seconds One traced child (pid=2745) ended because it received signal 15 (SIGTERM) One traced child (pid=2749) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.1 CPU time (s): 1209.48 CPU user time (s): 1208.56 CPU system time (s): 0.922859 CPU usage (%): 99.9489 Max. virtual memory (cumulated for all children) (Kb): 73468
ERROR: no interpretation found !