Name | mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-khb05250.opb |
MD5SUM | 5d4b655a5461d6a0782bca8bd105f9c2 |
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 | 1233.78 |
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 wulflinc2 THE 2005-09-19 18:22:36 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3018 boxname=wulflinc2 idbench=674 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 5d4b655a5461d6a0782bca8bd105f9c2 /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-20-10-khb05250.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-20-10-khb05250.opb IDLAUNCH: 3018 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.191 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.191 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: 853240 kB Buffers: 39856 kB Cached: 114552 kB SwapCached: 1040 kB Active: 67232 kB Inactive: 89880 kB HighTotal: 131008 kB HighFree: 23884 kB LowTotal: 903652 kB LowFree: 829356 kB SwapTotal: 2097136 kB SwapFree: 2095568 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5700 kB Slab: 18628 kB Committed_AS: 72360 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-19 18:42:46 (client local time) WITH STATUS 0 IN 1209.4 SECONDS stats: 3018 7 1209.4 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/28588/stat): 28588 (minisat+_script) R 28587 28588 6872 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1793807245 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/28588/statm): 174 3 169 147 0 27 0 [pid=28588] 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=28589 New process pid=28590 New process pid=28591 execve syscall for /bin/sed executable One traced child (pid=28590) 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=28591) exited with status: 0 One traced child (pid=28589) exited with status: 0 New process pid=28592 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-20-10-khb05250.opb [startup+10.0035 s] Raw data (loadavg): 0.93 0.95 0.90 1/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) T 28588 28588 6872 0 -1 0 7072 0 0 0 936 30 0 0 23 0 1 0 1793807249 32145408 6433 4294967295 134512640 135094434 3221224432 3221217340 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/28592/statm): 7848 6433 145 145 0 7703 0 [pid=28592] vsize: 31392 Current children cumulated CPU time (s) 9.68 Current children cumulated vsize (Kb) 33516 [startup+20.0043 s] Raw data (loadavg): 0.94 0.96 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 13543 0 0 0 1875 60 0 0 25 0 1 0 1793807249 64716800 12838 4294967295 134512640 135094434 3221224432 3221223104 134556375 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28592/statm): 15800 12838 145 145 0 15655 0 [pid=28592] vsize: 63200 Current children cumulated CPU time (s) 19.37 Current children cumulated vsize (Kb) 65324 [startup+30.006 s] Raw data (loadavg): 0.95 0.96 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 13738 0 0 0 2871 61 0 0 25 0 1 0 1793807249 65511424 13033 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28592/statm): 15994 13033 145 145 0 15849 0 [pid=28592] vsize: 63976 Current children cumulated CPU time (s) 29.34 Current children cumulated vsize (Kb) 66100 [startup+40.0066 s] Raw data (loadavg): 0.95 0.96 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 13852 0 0 0 3868 62 0 0 25 0 1 0 1793807249 65998848 13147 4294967295 134512640 135094434 3221224432 3221223044 134563069 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16113 13147 145 145 0 15968 0 [pid=28592] vsize: 64452 Current children cumulated CPU time (s) 39.32 Current children cumulated vsize (Kb) 66576 [startup+50.0084 s] Raw data (loadavg): 0.96 0.96 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 13941 0 0 0 4866 63 0 0 25 0 1 0 1793807249 66351104 13236 4294967295 134512640 135094434 3221224432 3221223088 134561463 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16199 13236 145 145 0 16054 0 [pid=28592] vsize: 64796 Current children cumulated CPU time (s) 49.31 Current children cumulated vsize (Kb) 66920 [startup+60.0091 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 13996 0 0 0 5865 64 0 0 25 0 1 0 1793807249 66568192 13291 4294967295 134512640 135094434 3221224432 3221223108 134554883 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16252 13291 145 145 0 16107 0 [pid=28592] vsize: 65008 Current children cumulated CPU time (s) 59.31 Current children cumulated vsize (Kb) 67132 [startup+70.0098 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14038 0 0 0 6865 64 0 0 25 0 1 0 1793807249 66760704 13333 4294967295 134512640 135094434 3221224432 3221223184 134559288 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16299 13333 145 145 0 16154 0 [pid=28592] vsize: 65196 Current children cumulated CPU time (s) 69.31 Current children cumulated vsize (Kb) 67320 [startup+80.0105 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14063 0 0 0 7865 64 0 0 25 0 1 0 1793807249 66859008 13358 4294967295 134512640 135094434 3221224432 3221223044 134563057 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16323 13358 145 145 0 16178 0 [pid=28592] vsize: 65292 Current children cumulated CPU time (s) 79.31 Current children cumulated vsize (Kb) 67416 [startup+90.0112 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14087 0 0 0 8865 64 0 0 25 0 1 0 1793807249 67014656 13382 4294967295 134512640 135094434 3221224432 3221223108 134554883 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16361 13382 145 145 0 16216 0 [pid=28592] vsize: 65444 Current children cumulated CPU time (s) 89.31 Current children cumulated vsize (Kb) 67568 [startup+100.012 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14110 0 0 0 9865 64 0 0 25 0 1 0 1793807249 67096576 13405 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16381 13405 145 145 0 16236 0 [pid=28592] vsize: 65524 Current children cumulated CPU time (s) 99.31 Current children cumulated vsize (Kb) 67648 [startup+110.013 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14128 0 0 0 10865 64 0 0 25 0 1 0 1793807249 67166208 13423 4294967295 134512640 135094434 3221224432 3221223044 134563059 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16398 13423 145 145 0 16253 0 [pid=28592] vsize: 65592 Current children cumulated CPU time (s) 109.31 Current children cumulated vsize (Kb) 67716 [startup+120.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14143 0 0 0 11864 65 0 0 25 0 1 0 1793807249 67223552 13438 4294967295 134512640 135094434 3221224432 3221223072 134562128 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16412 13438 145 145 0 16267 0 [pid=28592] vsize: 65648 Current children cumulated CPU time (s) 119.31 Current children cumulated vsize (Kb) 67772 [startup+130.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14154 0 0 0 12864 65 0 0 25 0 1 0 1793807249 67264512 13449 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16422 13449 145 145 0 16277 0 [pid=28592] vsize: 65688 Current children cumulated CPU time (s) 129.31 Current children cumulated vsize (Kb) 67812 [startup+140.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14170 0 0 0 13864 65 0 0 25 0 1 0 1793807249 67321856 13465 4294967295 134512640 135094434 3221224432 3221223044 134563130 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16436 13465 145 145 0 16291 0 [pid=28592] vsize: 65744 Current children cumulated CPU time (s) 139.31 Current children cumulated vsize (Kb) 67868 [startup+150.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14180 0 0 0 14865 65 0 0 25 0 1 0 1793807249 67358720 13475 4294967295 134512640 135094434 3221224432 3221223044 134563130 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16445 13475 145 145 0 16300 0 [pid=28592] vsize: 65780 Current children cumulated CPU time (s) 149.32 Current children cumulated vsize (Kb) 67904 [startup+160.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14193 0 0 0 15864 65 0 0 25 0 1 0 1793807249 67407872 13488 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16457 13488 145 145 0 16312 0 [pid=28592] vsize: 65828 Current children cumulated CPU time (s) 159.31 Current children cumulated vsize (Kb) 67952 [startup+170.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14205 0 0 0 16865 65 0 0 25 0 1 0 1793807249 67448832 13500 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16467 13500 145 145 0 16322 0 [pid=28592] vsize: 65868 Current children cumulated CPU time (s) 169.32 Current children cumulated vsize (Kb) 67992 [startup+180.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14215 0 0 0 17864 65 0 0 25 0 1 0 1793807249 67481600 13510 4294967295 134512640 135094434 3221224432 3221223120 134554859 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16475 13510 145 145 0 16330 0 [pid=28592] vsize: 65900 Current children cumulated CPU time (s) 179.31 Current children cumulated vsize (Kb) 68024 [startup+190.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14227 0 0 0 18864 65 0 0 25 0 1 0 1793807249 67526656 13522 4294967295 134512640 135094434 3221224432 3221223176 134559249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16486 13522 145 145 0 16341 0 [pid=28592] vsize: 65944 Current children cumulated CPU time (s) 189.31 Current children cumulated vsize (Kb) 68068 [startup+200.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14233 0 0 0 19864 65 0 0 25 0 1 0 1793807249 67547136 13528 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16491 13528 145 145 0 16346 0 [pid=28592] vsize: 65964 Current children cumulated CPU time (s) 199.31 Current children cumulated vsize (Kb) 68088 [startup+210.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14245 0 0 0 20864 65 0 0 25 0 1 0 1793807249 67592192 13540 4294967295 134512640 135094434 3221224432 3221223072 134562057 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16502 13540 145 145 0 16357 0 [pid=28592] vsize: 66008 Current children cumulated CPU time (s) 209.31 Current children cumulated vsize (Kb) 68132 [startup+220.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14253 0 0 0 21864 65 0 0 25 0 1 0 1793807249 67620864 13548 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16509 13548 145 145 0 16364 0 [pid=28592] vsize: 66036 Current children cumulated CPU time (s) 219.31 Current children cumulated vsize (Kb) 68160 [startup+230.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14259 0 0 0 22865 65 0 0 25 0 1 0 1793807249 67645440 13554 4294967295 134512640 135094434 3221224432 3221223044 134563052 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16515 13554 145 145 0 16370 0 [pid=28592] vsize: 66060 Current children cumulated CPU time (s) 229.32 Current children cumulated vsize (Kb) 68184 [startup+240.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14297 0 0 0 23865 66 0 0 25 0 1 0 1793807249 67919872 13592 4294967295 134512640 135094434 3221224432 3221223088 134561778 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16582 13592 145 145 0 16437 0 [pid=28592] vsize: 66328 Current children cumulated CPU time (s) 239.33 Current children cumulated vsize (Kb) 68452 [startup+250.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14297 0 0 0 24865 66 0 0 25 0 1 0 1793807249 67919872 13592 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16582 13592 145 145 0 16437 0 [pid=28592] vsize: 66328 Current children cumulated CPU time (s) 249.33 Current children cumulated vsize (Kb) 68452 [startup+260.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14298 0 0 0 25865 66 0 0 25 0 1 0 1793807249 67919872 13593 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16582 13593 145 145 0 16437 0 [pid=28592] vsize: 66328 Current children cumulated CPU time (s) 259.33 Current children cumulated vsize (Kb) 68452 [startup+270.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14299 0 0 0 26865 66 0 0 25 0 1 0 1793807249 67919872 13594 4294967295 134512640 135094434 3221224432 3221223072 134562108 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16582 13594 145 145 0 16437 0 [pid=28592] vsize: 66328 Current children cumulated CPU time (s) 269.33 Current children cumulated vsize (Kb) 68452 [startup+280.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14304 0 0 0 27866 66 0 0 25 0 1 0 1793807249 67936256 13599 4294967295 134512640 135094434 3221224432 3221223044 134563130 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16586 13599 145 145 0 16441 0 [pid=28592] vsize: 66344 Current children cumulated CPU time (s) 279.34 Current children cumulated vsize (Kb) 68468 [startup+290.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14312 0 0 0 28866 66 0 0 25 0 1 0 1793807249 67969024 13607 4294967295 134512640 135094434 3221224432 3221223084 134561606 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16594 13607 145 145 0 16449 0 [pid=28592] vsize: 66376 Current children cumulated CPU time (s) 289.34 Current children cumulated vsize (Kb) 68500 [startup+300.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14320 0 0 0 29866 66 0 0 25 0 1 0 1793807249 67997696 13615 4294967295 134512640 135094434 3221224432 3221223044 134563071 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16601 13615 145 145 0 16456 0 [pid=28592] vsize: 66404 Current children cumulated CPU time (s) 299.34 Current children cumulated vsize (Kb) 68528 [startup+310.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14330 0 0 0 30865 66 0 0 25 0 1 0 1793807249 68034560 13625 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16610 13625 145 145 0 16465 0 [pid=28592] vsize: 66440 Current children cumulated CPU time (s) 309.33 Current children cumulated vsize (Kb) 68564 [startup+320.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14343 0 0 0 31865 66 0 0 25 0 1 0 1793807249 68083712 13638 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16622 13638 145 145 0 16477 0 [pid=28592] vsize: 66488 Current children cumulated CPU time (s) 319.33 Current children cumulated vsize (Kb) 68612 [startup+330.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14356 0 0 0 32865 66 0 0 25 0 1 0 1793807249 68132864 13651 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16634 13651 145 145 0 16489 0 [pid=28592] vsize: 66536 Current children cumulated CPU time (s) 329.33 Current children cumulated vsize (Kb) 68660 [startup+340.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14364 0 0 0 33865 66 0 0 25 0 1 0 1793807249 68161536 13659 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16641 13659 145 145 0 16496 0 [pid=28592] vsize: 66564 Current children cumulated CPU time (s) 339.33 Current children cumulated vsize (Kb) 68688 [startup+350.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14370 0 0 0 34865 67 0 0 25 0 1 0 1793807249 68182016 13665 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16646 13665 145 145 0 16501 0 [pid=28592] vsize: 66584 Current children cumulated CPU time (s) 349.34 Current children cumulated vsize (Kb) 68708 [startup+360.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14393 0 0 0 35865 67 0 0 25 0 1 0 1793807249 68268032 13688 4294967295 134512640 135094434 3221224432 3221223044 134563012 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16667 13688 145 145 0 16522 0 [pid=28592] vsize: 66668 Current children cumulated CPU time (s) 359.34 Current children cumulated vsize (Kb) 68792 [startup+370.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14407 0 0 0 36865 67 0 0 25 0 1 0 1793807249 68321280 13702 4294967295 134512640 135094434 3221224432 3221223088 134550405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16680 13702 145 145 0 16535 0 [pid=28592] vsize: 66720 Current children cumulated CPU time (s) 369.34 Current children cumulated vsize (Kb) 68844 [startup+380.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14412 0 0 0 37865 67 0 0 25 0 1 0 1793807249 68341760 13707 4294967295 134512640 135094434 3221224432 3221223044 134563041 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16685 13707 145 145 0 16540 0 [pid=28592] vsize: 66740 Current children cumulated CPU time (s) 379.34 Current children cumulated vsize (Kb) 68864 [startup+390.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14428 0 0 0 38865 67 0 0 25 0 1 0 1793807249 68403200 13723 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16700 13723 145 145 0 16555 0 [pid=28592] vsize: 66800 Current children cumulated CPU time (s) 389.34 Current children cumulated vsize (Kb) 68924 [startup+400.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14447 0 0 0 39865 67 0 0 25 0 1 0 1793807249 68472832 13742 4294967295 134512640 135094434 3221224432 3221223120 134554742 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16717 13742 145 145 0 16572 0 [pid=28592] vsize: 66868 Current children cumulated CPU time (s) 399.34 Current children cumulated vsize (Kb) 68992 [startup+410.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14454 0 0 0 40865 67 0 0 25 0 1 0 1793807249 68497408 13749 4294967295 134512640 135094434 3221224432 3221223072 134562090 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16723 13749 145 145 0 16578 0 [pid=28592] vsize: 66892 Current children cumulated CPU time (s) 409.34 Current children cumulated vsize (Kb) 69016 [startup+420.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14469 0 0 0 41865 67 0 0 25 0 1 0 1793807249 68550656 13764 4294967295 134512640 135094434 3221224432 3221223072 134562048 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16736 13764 145 145 0 16591 0 [pid=28592] vsize: 66944 Current children cumulated CPU time (s) 419.34 Current children cumulated vsize (Kb) 69068 [startup+430.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14473 0 0 0 42865 67 0 0 25 0 1 0 1793807249 68567040 13768 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16740 13768 145 145 0 16595 0 [pid=28592] vsize: 66960 Current children cumulated CPU time (s) 429.34 Current children cumulated vsize (Kb) 69084 [startup+440.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14489 0 0 0 43865 67 0 0 25 0 1 0 1793807249 68628480 13784 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16755 13784 145 145 0 16610 0 [pid=28592] vsize: 67020 Current children cumulated CPU time (s) 439.34 Current children cumulated vsize (Kb) 69144 [startup+450.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14497 0 0 0 44865 67 0 0 25 0 1 0 1793807249 68657152 13792 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16762 13792 145 145 0 16617 0 [pid=28592] vsize: 67048 Current children cumulated CPU time (s) 449.34 Current children cumulated vsize (Kb) 69172 [startup+460.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14513 0 0 0 45865 68 0 0 25 0 1 0 1793807249 68718592 13808 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16777 13808 145 145 0 16632 0 [pid=28592] vsize: 67108 Current children cumulated CPU time (s) 459.35 Current children cumulated vsize (Kb) 69232 [startup+470.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14520 0 0 0 46865 68 0 0 25 0 1 0 1793807249 68743168 13815 4294967295 134512640 135094434 3221224432 3221223044 134563061 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16783 13815 145 145 0 16638 0 [pid=28592] vsize: 67132 Current children cumulated CPU time (s) 469.35 Current children cumulated vsize (Kb) 69256 [startup+480.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14536 0 0 0 47865 68 0 0 25 0 1 0 1793807249 68804608 13831 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16798 13831 145 145 0 16653 0 [pid=28592] vsize: 67192 Current children cumulated CPU time (s) 479.35 Current children cumulated vsize (Kb) 69316 [startup+490.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14549 0 0 0 48865 68 0 0 25 0 1 0 1793807249 68853760 13844 4294967295 134512640 135094434 3221224432 3221223088 134561734 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16810 13844 145 145 0 16665 0 [pid=28592] vsize: 67240 Current children cumulated CPU time (s) 489.35 Current children cumulated vsize (Kb) 69364 [startup+500.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14562 0 0 0 49864 68 0 0 25 0 1 0 1793807249 68902912 13857 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28592/statm): 16822 13857 145 145 0 16677 0 [pid=28592] vsize: 67288 Current children cumulated CPU time (s) 499.34 Current children cumulated vsize (Kb) 69412 [startup+510.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14578 0 0 0 50864 68 0 0 25 0 1 0 1793807249 68964352 13873 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16837 13873 145 145 0 16692 0 [pid=28592] vsize: 67348 Current children cumulated CPU time (s) 509.34 Current children cumulated vsize (Kb) 69472 [startup+520.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14593 0 0 0 51864 68 0 0 25 0 1 0 1793807249 69021696 13888 4294967295 134512640 135094434 3221224432 3221223044 134563052 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16851 13888 145 145 0 16706 0 [pid=28592] vsize: 67404 Current children cumulated CPU time (s) 519.34 Current children cumulated vsize (Kb) 69528 [startup+530.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14601 0 0 0 52864 68 0 0 25 0 1 0 1793807249 69050368 13896 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16858 13896 145 145 0 16713 0 [pid=28592] vsize: 67432 Current children cumulated CPU time (s) 529.34 Current children cumulated vsize (Kb) 69556 [startup+540.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14615 0 0 0 53864 68 0 0 25 0 1 0 1793807249 69103616 13910 4294967295 134512640 135094434 3221224432 3221223072 134558048 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16871 13910 145 145 0 16726 0 [pid=28592] vsize: 67484 Current children cumulated CPU time (s) 539.34 Current children cumulated vsize (Kb) 69608 [startup+550.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14624 0 0 0 54864 69 0 0 25 0 1 0 1793807249 69140480 13919 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16880 13919 145 145 0 16735 0 [pid=28592] vsize: 67520 Current children cumulated CPU time (s) 549.35 Current children cumulated vsize (Kb) 69644 [startup+560.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14635 0 0 0 55864 69 0 0 25 0 1 0 1793807249 69181440 13930 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16890 13930 145 145 0 16745 0 [pid=28592] vsize: 67560 Current children cumulated CPU time (s) 559.35 Current children cumulated vsize (Kb) 69684 [startup+570.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14645 0 0 0 56864 69 0 0 25 0 1 0 1793807249 69218304 13940 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16899 13940 145 145 0 16754 0 [pid=28592] vsize: 67596 Current children cumulated CPU time (s) 569.35 Current children cumulated vsize (Kb) 69720 [startup+580.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14657 0 0 0 57864 69 0 0 25 0 1 0 1793807249 69525504 13952 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16974 13952 145 145 0 16829 0 [pid=28592] vsize: 67896 Current children cumulated CPU time (s) 579.35 Current children cumulated vsize (Kb) 70020 [startup+590.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14672 0 0 0 58864 69 0 0 25 0 1 0 1793807249 69582848 13967 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 16988 13967 145 145 0 16843 0 [pid=28592] vsize: 67952 Current children cumulated CPU time (s) 589.35 Current children cumulated vsize (Kb) 70076 [startup+600.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14685 0 0 0 59864 69 0 0 25 0 1 0 1793807249 69632000 13980 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17000 13980 145 145 0 16855 0 [pid=28592] vsize: 68000 Current children cumulated CPU time (s) 599.35 Current children cumulated vsize (Kb) 70124 [startup+610.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14694 0 0 0 60864 70 0 0 25 0 1 0 1793807249 69664768 13989 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17008 13989 145 145 0 16863 0 [pid=28592] vsize: 68032 Current children cumulated CPU time (s) 609.36 Current children cumulated vsize (Kb) 70156 [startup+620.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14703 0 0 0 61864 70 0 0 25 0 1 0 1793807249 69701632 13998 4294967295 134512640 135094434 3221224432 3221223088 134561763 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17017 13998 145 145 0 16872 0 [pid=28592] vsize: 68068 Current children cumulated CPU time (s) 619.36 Current children cumulated vsize (Kb) 70192 [startup+630.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14712 0 0 0 62864 70 0 0 25 0 1 0 1793807249 69734400 14007 4294967295 134512640 135094434 3221224432 3221223056 134562985 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17025 14007 145 145 0 16880 0 [pid=28592] vsize: 68100 Current children cumulated CPU time (s) 629.36 Current children cumulated vsize (Kb) 70224 [startup+640.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14727 0 0 0 63864 70 0 0 25 0 1 0 1793807249 69791744 14022 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17039 14022 145 145 0 16894 0 [pid=28592] vsize: 68156 Current children cumulated CPU time (s) 639.36 Current children cumulated vsize (Kb) 70280 [startup+650.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14746 0 0 0 64864 70 0 0 25 0 1 0 1793807249 69865472 14041 4294967295 134512640 135094434 3221224432 3221223044 134563052 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17057 14041 145 145 0 16912 0 [pid=28592] vsize: 68228 Current children cumulated CPU time (s) 649.36 Current children cumulated vsize (Kb) 70352 [startup+660.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14760 0 0 0 65864 70 0 0 25 0 1 0 1793807249 69918720 14055 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17070 14055 145 145 0 16925 0 [pid=28592] vsize: 68280 Current children cumulated CPU time (s) 659.36 Current children cumulated vsize (Kb) 70404 [startup+670.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14777 0 0 0 66864 70 0 0 25 0 1 0 1793807249 69984256 14072 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17086 14072 145 145 0 16941 0 [pid=28592] vsize: 68344 Current children cumulated CPU time (s) 669.36 Current children cumulated vsize (Kb) 70468 [startup+680.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14791 0 0 0 67864 70 0 0 25 0 1 0 1793807249 70037504 14086 4294967295 134512640 135094434 3221224432 3221223072 134562115 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17099 14086 145 145 0 16954 0 [pid=28592] vsize: 68396 Current children cumulated CPU time (s) 679.36 Current children cumulated vsize (Kb) 70520 [startup+690.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14801 0 0 0 68864 70 0 0 25 0 1 0 1793807249 70074368 14096 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17108 14096 145 145 0 16963 0 [pid=28592] vsize: 68432 Current children cumulated CPU time (s) 689.36 Current children cumulated vsize (Kb) 70556 [startup+700.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14814 0 0 0 69864 70 0 0 25 0 1 0 1793807249 70123520 14109 4294967295 134512640 135094434 3221224432 3221223044 134563071 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17120 14109 145 145 0 16975 0 [pid=28592] vsize: 68480 Current children cumulated CPU time (s) 699.36 Current children cumulated vsize (Kb) 70604 [startup+710.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14828 0 0 0 70864 70 0 0 25 0 1 0 1793807249 70176768 14123 4294967295 134512640 135094434 3221224432 3221223088 134561660 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17133 14123 145 145 0 16988 0 [pid=28592] vsize: 68532 Current children cumulated CPU time (s) 709.36 Current children cumulated vsize (Kb) 70656 [startup+720.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14841 0 0 0 71864 70 0 0 25 0 1 0 1793807249 70225920 14136 4294967295 134512640 135094434 3221224432 3221223136 134554526 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17145 14136 145 145 0 17000 0 [pid=28592] vsize: 68580 Current children cumulated CPU time (s) 719.36 Current children cumulated vsize (Kb) 70704 [startup+730.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14850 0 0 0 72864 71 0 0 25 0 1 0 1793807249 70262784 14145 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17154 14145 145 145 0 17009 0 [pid=28592] vsize: 68616 Current children cumulated CPU time (s) 729.37 Current children cumulated vsize (Kb) 70740 [startup+740.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14865 0 0 0 73864 71 0 0 25 0 1 0 1793807249 70320128 14160 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17168 14160 145 145 0 17023 0 [pid=28592] vsize: 68672 Current children cumulated CPU time (s) 739.37 Current children cumulated vsize (Kb) 70796 [startup+750.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14875 0 0 0 74864 71 0 0 25 0 1 0 1793807249 70356992 14170 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17177 14170 145 145 0 17032 0 [pid=28592] vsize: 68708 Current children cumulated CPU time (s) 749.37 Current children cumulated vsize (Kb) 70832 [startup+760.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14889 0 0 0 75864 71 0 0 25 0 1 0 1793807249 70410240 14184 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17190 14184 145 145 0 17045 0 [pid=28592] vsize: 68760 Current children cumulated CPU time (s) 759.37 Current children cumulated vsize (Kb) 70884 [startup+770.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14903 0 0 0 76864 71 0 0 25 0 1 0 1793807249 70463488 14198 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17203 14198 145 145 0 17058 0 [pid=28592] vsize: 68812 Current children cumulated CPU time (s) 769.37 Current children cumulated vsize (Kb) 70936 [startup+780.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14915 0 0 0 77864 71 0 0 25 0 1 0 1793807249 70508544 14210 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17214 14210 145 145 0 17069 0 [pid=28592] vsize: 68856 Current children cumulated CPU time (s) 779.37 Current children cumulated vsize (Kb) 70980 [startup+790.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14922 0 0 0 78864 71 0 0 25 0 1 0 1793807249 70537216 14217 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17221 14217 145 145 0 17076 0 [pid=28592] vsize: 68884 Current children cumulated CPU time (s) 789.37 Current children cumulated vsize (Kb) 71008 [startup+800.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14934 0 0 0 79864 71 0 0 25 0 1 0 1793807249 70582272 14229 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17232 14229 145 145 0 17087 0 [pid=28592] vsize: 68928 Current children cumulated CPU time (s) 799.37 Current children cumulated vsize (Kb) 71052 [startup+810.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14946 0 0 0 80865 71 0 0 25 0 1 0 1793807249 70627328 14241 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17243 14241 145 145 0 17098 0 [pid=28592] vsize: 68972 Current children cumulated CPU time (s) 809.38 Current children cumulated vsize (Kb) 71096 [startup+820.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14958 0 0 0 81864 71 0 0 25 0 1 0 1793807249 70672384 14253 4294967295 134512640 135094434 3221224432 3221223044 134563124 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28592/statm): 17254 14253 145 145 0 17109 0 [pid=28592] vsize: 69016 Current children cumulated CPU time (s) 819.37 Current children cumulated vsize (Kb) 71140 [startup+830.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14970 0 0 0 82863 72 0 0 25 0 1 0 1793807249 70717440 14265 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28592/statm): 17265 14265 145 145 0 17120 0 [pid=28592] vsize: 69060 Current children cumulated CPU time (s) 829.37 Current children cumulated vsize (Kb) 71184 [startup+840.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14981 0 0 0 83863 72 0 0 25 0 1 0 1793807249 70758400 14276 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17275 14276 145 145 0 17130 0 [pid=28592] vsize: 69100 Current children cumulated CPU time (s) 839.37 Current children cumulated vsize (Kb) 71224 [startup+850.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14994 0 0 0 84863 72 0 0 25 0 1 0 1793807249 70807552 14289 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17287 14289 145 145 0 17142 0 [pid=28592] vsize: 69148 Current children cumulated CPU time (s) 849.37 Current children cumulated vsize (Kb) 71272 [startup+860.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15004 0 0 0 85863 72 0 0 25 0 1 0 1793807249 70848512 14299 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17297 14299 145 145 0 17152 0 [pid=28592] vsize: 69188 Current children cumulated CPU time (s) 859.37 Current children cumulated vsize (Kb) 71312 [startup+870.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15020 0 0 0 86863 72 0 0 25 0 1 0 1793807249 70909952 14315 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17312 14315 145 145 0 17167 0 [pid=28592] vsize: 69248 Current children cumulated CPU time (s) 869.37 Current children cumulated vsize (Kb) 71372 [startup+880.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15030 0 0 0 87862 73 0 0 25 0 1 0 1793807249 70946816 14325 4294967295 134512640 135094434 3221224432 3221223072 134562128 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17321 14325 145 145 0 17176 0 [pid=28592] vsize: 69284 Current children cumulated CPU time (s) 879.37 Current children cumulated vsize (Kb) 71408 [startup+890.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15046 0 0 0 88862 73 0 0 25 0 1 0 1793807249 71008256 14341 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17336 14341 145 145 0 17191 0 [pid=28592] vsize: 69344 Current children cumulated CPU time (s) 889.37 Current children cumulated vsize (Kb) 71468 [startup+900.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15063 0 0 0 89862 73 0 0 25 0 1 0 1793807249 71069696 14358 4294967295 134512640 135094434 3221224432 3221223088 134558164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17351 14358 145 145 0 17206 0 [pid=28592] vsize: 69404 Current children cumulated CPU time (s) 899.37 Current children cumulated vsize (Kb) 71528 [startup+910.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15083 0 0 0 90862 73 0 0 25 0 1 0 1793807249 71143424 14378 4294967295 134512640 135094434 3221224432 3221223044 134563059 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17369 14378 145 145 0 17224 0 [pid=28592] vsize: 69476 Current children cumulated CPU time (s) 909.37 Current children cumulated vsize (Kb) 71600 [startup+920.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15096 0 0 0 91862 73 0 0 25 0 1 0 1793807249 71192576 14391 4294967295 134512640 135094434 3221224432 3221223084 134561520 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17381 14391 145 145 0 17236 0 [pid=28592] vsize: 69524 Current children cumulated CPU time (s) 919.37 Current children cumulated vsize (Kb) 71648 [startup+930.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15117 0 0 0 92861 73 0 0 25 0 1 0 1793807249 71274496 14412 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17401 14412 145 145 0 17256 0 [pid=28592] vsize: 69604 Current children cumulated CPU time (s) 929.36 Current children cumulated vsize (Kb) 71728 [startup+940.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15128 0 0 0 93861 74 0 0 25 0 1 0 1793807249 71311360 14423 4294967295 134512640 135094434 3221224432 3221223088 134557820 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17410 14423 145 145 0 17265 0 [pid=28592] vsize: 69640 Current children cumulated CPU time (s) 939.37 Current children cumulated vsize (Kb) 71764 [startup+950.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15163 0 0 0 94861 74 0 0 25 0 1 0 1793807249 71450624 14458 4294967295 134512640 135094434 3221224432 3221223088 134557768 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17444 14458 145 145 0 17299 0 [pid=28592] vsize: 69776 Current children cumulated CPU time (s) 949.37 Current children cumulated vsize (Kb) 71900 [startup+960.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15176 0 0 0 95861 74 0 0 25 0 1 0 1793807249 71499776 14471 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17456 14471 145 145 0 17311 0 [pid=28592] vsize: 69824 Current children cumulated CPU time (s) 959.37 Current children cumulated vsize (Kb) 71948 [startup+970.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15186 0 0 0 96861 74 0 0 25 0 1 0 1793807249 71536640 14481 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17465 14481 145 145 0 17320 0 [pid=28592] vsize: 69860 Current children cumulated CPU time (s) 969.37 Current children cumulated vsize (Kb) 71984 [startup+980.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15219 0 0 0 97861 74 0 0 25 0 1 0 1793807249 71667712 14514 4294967295 134512640 135094434 3221224432 3221223044 134563137 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17497 14514 145 145 0 17352 0 [pid=28592] vsize: 69988 Current children cumulated CPU time (s) 979.37 Current children cumulated vsize (Kb) 72112 [startup+990.075 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15235 0 0 0 98861 74 0 0 25 0 1 0 1793807249 71720960 14530 4294967295 134512640 135094434 3221224432 3221223084 134561534 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17510 14530 145 145 0 17365 0 [pid=28592] vsize: 70040 Current children cumulated CPU time (s) 989.37 Current children cumulated vsize (Kb) 72164 [startup+1000.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15263 0 0 0 99861 74 0 0 25 0 1 0 1793807249 71827456 14558 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17536 14558 145 145 0 17391 0 [pid=28592] vsize: 70144 Current children cumulated CPU time (s) 999.37 Current children cumulated vsize (Kb) 72268 [startup+1010.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15283 0 0 0 100861 75 0 0 25 0 1 0 1793807249 71905280 14578 4294967295 134512640 135094434 3221224432 3221223120 134554760 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17555 14578 145 145 0 17410 0 [pid=28592] vsize: 70220 Current children cumulated CPU time (s) 1009.38 Current children cumulated vsize (Kb) 72344 [startup+1020.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15294 0 0 0 101861 75 0 0 25 0 1 0 1793807249 71950336 14589 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17566 14589 145 145 0 17421 0 [pid=28592] vsize: 70264 Current children cumulated CPU time (s) 1019.38 Current children cumulated vsize (Kb) 72388 [startup+1030.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15306 0 0 0 102861 75 0 0 25 0 1 0 1793807249 71995392 14601 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17577 14601 145 145 0 17432 0 [pid=28592] vsize: 70308 Current children cumulated CPU time (s) 1029.38 Current children cumulated vsize (Kb) 72432 [startup+1040.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15328 0 0 0 103861 75 0 0 25 0 1 0 1793807249 72081408 14623 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17598 14623 145 145 0 17453 0 [pid=28592] vsize: 70392 Current children cumulated CPU time (s) 1039.38 Current children cumulated vsize (Kb) 72516 [startup+1050.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15350 0 0 0 104860 75 0 0 25 0 1 0 1793807249 72163328 14645 4294967295 134512640 135094434 3221224432 3221223044 134563124 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17618 14645 145 145 0 17473 0 [pid=28592] vsize: 70472 Current children cumulated CPU time (s) 1049.37 Current children cumulated vsize (Kb) 72596 [startup+1060.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15370 0 0 0 105860 75 0 0 25 0 1 0 1793807249 72237056 14665 4294967295 134512640 135094434 3221224432 3221223136 134554398 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17636 14665 145 145 0 17491 0 [pid=28592] vsize: 70544 Current children cumulated CPU time (s) 1059.37 Current children cumulated vsize (Kb) 72668 [startup+1070.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15386 0 0 0 106860 75 0 0 25 0 1 0 1793807249 72298496 14681 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17651 14681 145 145 0 17506 0 [pid=28592] vsize: 70604 Current children cumulated CPU time (s) 1069.37 Current children cumulated vsize (Kb) 72728 [startup+1080.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15410 0 0 0 107860 76 0 0 25 0 1 0 1793807249 72392704 14705 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17674 14705 145 145 0 17529 0 [pid=28592] vsize: 70696 Current children cumulated CPU time (s) 1079.38 Current children cumulated vsize (Kb) 72820 [startup+1090.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15427 0 0 0 108860 76 0 0 25 0 1 0 1793807249 72458240 14722 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17690 14722 145 145 0 17545 0 [pid=28592] vsize: 70760 Current children cumulated CPU time (s) 1089.38 Current children cumulated vsize (Kb) 72884 [startup+1100.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15442 0 0 0 109859 76 0 0 25 0 1 0 1793807249 72515584 14737 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17704 14737 145 145 0 17559 0 [pid=28592] vsize: 70816 Current children cumulated CPU time (s) 1099.37 Current children cumulated vsize (Kb) 72940 [startup+1110.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15458 0 0 0 110859 76 0 0 25 0 1 0 1793807249 72577024 14753 4294967295 134512640 135094434 3221224432 3221223100 134550364 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17719 14753 145 145 0 17574 0 [pid=28592] vsize: 70876 Current children cumulated CPU time (s) 1109.37 Current children cumulated vsize (Kb) 73000 [startup+1120.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15468 0 0 0 111859 76 0 0 25 0 1 0 1793807249 72617984 14763 4294967295 134512640 135094434 3221224432 3221223056 134557705 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17729 14763 145 145 0 17584 0 [pid=28592] vsize: 70916 Current children cumulated CPU time (s) 1119.37 Current children cumulated vsize (Kb) 73040 [startup+1130.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15478 0 0 0 112860 76 0 0 25 0 1 0 1793807249 72654848 14773 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17738 14773 145 145 0 17593 0 [pid=28592] vsize: 70952 Current children cumulated CPU time (s) 1129.38 Current children cumulated vsize (Kb) 73076 [startup+1140.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15499 0 0 0 113859 76 0 0 25 0 1 0 1793807249 72736768 14794 4294967295 134512640 135094434 3221224432 3221223120 134554760 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17758 14794 145 145 0 17613 0 [pid=28592] vsize: 71032 Current children cumulated CPU time (s) 1139.37 Current children cumulated vsize (Kb) 73156 [startup+1150.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15507 0 0 0 114859 76 0 0 25 0 1 0 1793807249 72765440 14802 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17765 14802 145 145 0 17620 0 [pid=28592] vsize: 71060 Current children cumulated CPU time (s) 1149.37 Current children cumulated vsize (Kb) 73184 [startup+1160.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15516 0 0 0 115860 76 0 0 25 0 1 0 1793807249 72798208 14811 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17773 14811 145 145 0 17628 0 [pid=28592] vsize: 71092 Current children cumulated CPU time (s) 1159.38 Current children cumulated vsize (Kb) 73216 [startup+1170.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15535 0 0 0 116859 76 0 0 25 0 1 0 1793807249 72871936 14830 4294967295 134512640 135094434 3221224432 3221223072 134562108 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17791 14830 145 145 0 17646 0 [pid=28592] vsize: 71164 Current children cumulated CPU time (s) 1169.37 Current children cumulated vsize (Kb) 73288 [startup+1180.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15546 0 0 0 117859 76 0 0 25 0 1 0 1793807249 72912896 14841 4294967295 134512640 135094434 3221224432 3221223044 134563059 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17801 14841 145 145 0 17656 0 [pid=28592] vsize: 71204 Current children cumulated CPU time (s) 1179.37 Current children cumulated vsize (Kb) 73328 [startup+1190.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15562 0 0 0 118859 77 0 0 25 0 1 0 1793807249 72974336 14857 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17816 14857 145 145 0 17671 0 [pid=28592] vsize: 71264 Current children cumulated CPU time (s) 1189.38 Current children cumulated vsize (Kb) 73388 [startup+1200.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15590 0 0 0 119859 77 0 0 25 0 1 0 1793807249 73084928 14885 4294967295 134512640 135094434 3221224432 3221223044 134563094 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17843 14885 145 145 0 17698 0 [pid=28592] vsize: 71372 Current children cumulated CPU time (s) 1199.38 Current children cumulated vsize (Kb) 73496 [startup+1210.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15623 0 0 0 120859 77 0 0 25 0 1 0 1793807249 73211904 14918 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17874 14918 145 145 0 17729 0 [pid=28592] vsize: 71496 Current children cumulated CPU time (s) 1209.38 Current children cumulated vsize (Kb) 73620 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28592 Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28588/statm): 531 226 485 147 0 384 0 [pid=28588] vsize: 2124 Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15623 0 0 0 120859 77 0 0 25 0 1 0 1793807249 73211904 14918 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28592/statm): 17874 14918 145 145 0 17729 0 [pid=28592] vsize: 71496 Current children cumulated CPU time (s) 1209.38 Current children cumulated vsize (Kb) 73620 Sending SIGTERM to -28588 Sleeping 2 seconds One traced child (pid=28588) ended because it received signal 15 (SIGTERM) One traced child (pid=28592) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.12 CPU time (s): 1209.4 CPU user time (s): 1208.59 CPU system time (s): 0.806877 CPU usage (%): 99.9403 Max. virtual memory (cumulated for all children) (Kb): 73620
ERROR: no interpretation found !