Name | mps-v2-13-7/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-israel.opb |
MD5SUM | 326c72a25c8066513471046cf298330a |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | -20715832672 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 1780 |
Biggest coefficient in the objective function | 788267008000 |
Number of bits for the biggest coefficient in the objective function | 40 |
Sum of the numbers in the objective function | 9669174315900 |
Number of bits of the sum of numbers in the objective function | 44 |
Biggest number in a constraint | 788267008000 |
Number of bits of the biggest number in a constraint | 40 |
Biggest sum of numbers in a constraint | 9669174315900 |
Number of bits of the biggest sum of numbers | 44 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1195.11 |
Number of variables | 2840 |
Total number of constraints | 174 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 174 |
Minimum length of a constraint | 20 |
Maximum length of a constraint | 2360 |
LAUNCH ON wulflinc18 THE 2005-09-20 02:48:10 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3167 boxname=wulflinc18 idbench=823 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 326c72a25c8066513471046cf298330a /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-israel.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-israel.opb IDLAUNCH: 3167 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.177 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.177 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: 859592 kB Buffers: 23060 kB Cached: 118952 kB SwapCached: 856 kB Active: 33124 kB Inactive: 111524 kB HighTotal: 131008 kB HighFree: 26516 kB LowTotal: 903652 kB LowFree: 833076 kB SwapTotal: 2097892 kB SwapFree: 2096528 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5732 kB Slab: 24812 kB Committed_AS: 64184 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-20 03:08:10 (client local time) WITH STATUS 0 IN 1200.14 SECONDS stats: 3167 7 1200.14 0
c Parsing PB file... c Converting 174 PB-constraints to clauses... c -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppp c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ssssssssssssssssssss c ---[ 193]---> Adder-cost: 1210 maxlim: 14189788 bits: 24/24 c ---[ 191]---> Adder-cost: 349 maxlim: 104839835 bits: 28/27 c ---[ 190]---> Sorter-cost: 3818 Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 3 5 2 2 2 2 c ---[ 189]---> Sorter-cost: 3582 Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 3 5 2 2 2 2 c ---[ 188]---> Sorter-cost: 3582 Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 3 5 2 2 2 2 c ---[ 187]---> Sorter-cost: 3582 Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 3 5 2 2 2 2 c ---[ 186]---> Sorter-cost: 3582 Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 3 5 2 2 2 2 c ---[ 185]---> Sorter-cost: 3557 Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 3 5 2 2 2 2 2 c ---[ 184]---> Sorter-cost: 3393 Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 3 5 2 2 2 2 2 c ---[ 183]---> Sorter-cost: 3393 Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 3 5 2 2 2 2 2 c ---[ 182]---> Adder-cost: 403 maxlim: 104838683 bits: 28/27 c ---[ 180]---> Adder-cost: 313 maxlim: 104838555 bits: 28/27 c ---[ 179]---> Sorter-cost: 1779 Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 c ---[ 178]---> Sorter-cost: 1345 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 c ---[ 177]---> Sorter-cost: 1408 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 176]---> Sorter-cost: 1690 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 c ---[ 175]---> Sorter-cost: 1793 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 c ---[ 174]---> Sorter-cost: 2477 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 c ---[ 173]---> Sorter-cost: 2309 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 c ---[ 172]---> Sorter-cost: 2428 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 c ---[ 171]---> Sorter-cost: 2782 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 c ---[ 170]---> Sorter-cost: 579 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 c ---[ 169]---> Sorter-cost: 2475 Base: 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2 2 c ---[ 168]---> Sorter-cost: 2310 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 c ---[ 167]---> Sorter-cost: 2373 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 3 c ---[ 166]---> Sorter-cost: 2284 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 3 c ---[ 165]---> Sorter-cost: 2282 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 3 c ---[ 164]---> Sorter-cost: 2285 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 3 c ---[ 163]---> Sorter-cost: 2282 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 3 c ---[ 162]---> Sorter-cost: 2283 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 3 c ---[ 161]---> Sorter-cost: 2282 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 3 c ---[ 160]---> Sorter-cost: 2284 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 3 c ---[ 159]---> Sorter-cost: 4744 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 158]---> Sorter-cost: 2284 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 3 c ---[ 157]---> Sorter-cost: 2282 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 3 c ---[ 156]---> Sorter-cost: 2284 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 3 c ---[ 155]---> Adder-cost: 510 maxlim: 85195112 bits: 27/27 c ---[ 154]---> Adder-cost: 474 maxlim: 45873511 bits: 26/26 c ---[ 153]---> Adder-cost: 478 maxlim: 45873511 bits: 26/26 c ---[ 152]---> Adder-cost: 468 maxlim: 45873510 bits: 26/26 c ---[ 151]---> Adder-cost: 468 maxlim: 45873510 bits: 26/26 c ---[ 150]---> Adder-cost: 468 maxlim: 45873509 bits: 26/26 c ---[ 149]---> Adder-cost: 468 maxlim: 45873509 bits: 26/26 c ---[ 148]---> Sorter-cost: 1030 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 147]---> Adder-cost: 468 maxlim: 45873508 bits: 26/26 c ---[ 146]---> Adder-cost: 468 maxlim: 45873508 bits: 26/26 c ---[ 145]---> Adder-cost: 468 maxlim: 45873507 bits: 26/26 c ---[ 144]---> Adder-cost: 460 maxlim: 45873507 bits: 26/26 c ---[ 143]---> Adder-cost: 460 maxlim: 45873506 bits: 26/26 c ---[ 142]---> Sorter-cost: 1285 Base: 2 2
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/27608/stat): 27608 (minisat+_script) R 27607 27608 31027 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1855022392 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/27608/statm): 174 3 169 147 0 27 0 [pid=27608] 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=27609 New process pid=27610 New process pid=27611 execve syscall for /bin/sed executable One traced child (pid=27610) 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=27611) exited with status: 0 One traced child (pid=27609) exited with status: 0 New process pid=27612 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-israel.opb [startup+10.0032 s] Raw data (loadavg): 0.93 0.98 0.92 1/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) T 27608 27608 31027 0 -1 0 1986 0 0 0 980 8 0 0 25 0 1 0 1855022397 7983104 1629 4294967295 134512640 135094434 3221224432 3221218700 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/27612/statm): 1949 1629 145 145 0 1804 0 [pid=27612] vsize: 7796 Current children cumulated CPU time (s) 9.89 Current children cumulated vsize (Kb) 9920 [startup+20.0052 s] Raw data (loadavg): 0.94 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 2306 0 0 0 1977 9 0 0 25 0 1 0 1855022397 8835072 1949 4294967295 134512640 135094434 3221224432 3221221004 134676331 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27612/statm): 2157 1949 145 145 0 2012 0 [pid=27612] vsize: 8628 Current children cumulated CPU time (s) 19.87 Current children cumulated vsize (Kb) 10752 [startup+30.0061 s] Raw data (loadavg): 0.95 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 2364 0 0 0 2976 10 0 0 25 0 1 0 1855022397 8990720 2007 4294967295 134512640 135094434 3221224432 3221221000 134676334 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 2195 2007 145 145 0 2050 0 [pid=27612] vsize: 8780 Current children cumulated CPU time (s) 29.87 Current children cumulated vsize (Kb) 10904 [startup+40.007 s] Raw data (loadavg): 0.95 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 3969 15 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221218112 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 39.85 Current children cumulated vsize (Kb) 16136 [startup+50.0079 s] Raw data (loadavg): 0.96 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 4969 15 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221218284 134600233 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 49.85 Current children cumulated vsize (Kb) 16136 [startup+60.0079 s] Raw data (loadavg): 0.97 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 5969 15 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221218816 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 59.85 Current children cumulated vsize (Kb) 16136 [startup+70.0088 s] Raw data (loadavg): 0.97 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 6970 15 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221218912 134676349 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 69.86 Current children cumulated vsize (Kb) 16136 [startup+80.0097 s] Raw data (loadavg): 0.98 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 7970 15 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219872 134677239 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 79.86 Current children cumulated vsize (Kb) 16136 [startup+90.0107 s] Raw data (loadavg): 0.98 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 8970 15 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219048 134677377 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 89.86 Current children cumulated vsize (Kb) 16136 [startup+100.012 s] Raw data (loadavg): 0.98 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 9970 15 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220100 134677232 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 99.86 Current children cumulated vsize (Kb) 16136 [startup+110.013 s] Raw data (loadavg): 0.98 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 10970 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219440 134676259 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 109.87 Current children cumulated vsize (Kb) 16136 [startup+120.013 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 11970 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219572 134677232 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 119.87 Current children cumulated vsize (Kb) 16136 [startup+130.013 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 12970 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219440 134677059 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 129.87 Current children cumulated vsize (Kb) 16136 [startup+140.014 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 13971 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219408 134676341 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 139.88 Current children cumulated vsize (Kb) 16136 [startup+150.015 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 14971 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221218992 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 149.88 Current children cumulated vsize (Kb) 16136 [startup+160.015 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 15971 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219392 134677233 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 159.88 Current children cumulated vsize (Kb) 16136 [startup+170.016 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 16971 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220400 134676552 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 169.88 Current children cumulated vsize (Kb) 16136 [startup+180.017 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 17971 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219520 134676471 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 179.88 Current children cumulated vsize (Kb) 16136 [startup+190.018 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 18972 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219520 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 189.89 Current children cumulated vsize (Kb) 16136 [startup+200.019 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 19972 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221218992 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 199.89 Current children cumulated vsize (Kb) 16136 [startup+210.019 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 20972 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221218816 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 209.89 Current children cumulated vsize (Kb) 16136 [startup+220.02 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 21972 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219088 134676273 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 219.89 Current children cumulated vsize (Kb) 16136 [startup+230.021 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 22972 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219232 134677091 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 229.89 Current children cumulated vsize (Kb) 16136 [startup+240.022 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 23973 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219680 134600241 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 239.9 Current children cumulated vsize (Kb) 16136 [startup+250.022 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 24973 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219792 134677138 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 249.9 Current children cumulated vsize (Kb) 16136 [startup+260.022 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 25973 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219872 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 259.9 Current children cumulated vsize (Kb) 16136 [startup+270.023 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 26973 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220048 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 269.9 Current children cumulated vsize (Kb) 16136 [startup+280.023 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 27973 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221218448 134600162 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 279.9 Current children cumulated vsize (Kb) 16136 [startup+290.025 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 28974 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219592 134677084 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 289.91 Current children cumulated vsize (Kb) 16136 [startup+300.026 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 29974 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220672 134676311 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 299.91 Current children cumulated vsize (Kb) 16136 [startup+310.026 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 30974 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219872 134600151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 309.91 Current children cumulated vsize (Kb) 16136 [startup+320.027 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 31974 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221218992 134600228 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 319.91 Current children cumulated vsize (Kb) 16136 [startup+330.028 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 32974 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219932 134677228 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 329.91 Current children cumulated vsize (Kb) 16136 [startup+340.029 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 33975 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219968 134677059 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 339.92 Current children cumulated vsize (Kb) 16136 [startup+350.03 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 34975 17 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220048 134600291 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 349.93 Current children cumulated vsize (Kb) 16136 [startup+360.03 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 35975 17 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221218884 134677085 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 359.93 Current children cumulated vsize (Kb) 16136 [startup+370.031 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 36975 17 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219872 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 369.93 Current children cumulated vsize (Kb) 16136 [startup+380.032 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 37975 17 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219088 134676321 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 379.93 Current children cumulated vsize (Kb) 16136 [startup+390.033 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 38975 17 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219728 134783376 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 389.93 Current children cumulated vsize (Kb) 16136 [startup+400.034 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 39976 17 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219696 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 399.94 Current children cumulated vsize (Kb) 16136 [startup+410.034 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 40976 17 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220752 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 409.94 Current children cumulated vsize (Kb) 16136 [startup+420.035 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 41976 17 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219344 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 419.94 Current children cumulated vsize (Kb) 16136 [startup+430.035 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 42976 17 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219344 134600228 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 429.94 Current children cumulated vsize (Kb) 16136 [startup+440.036 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 43976 17 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219520 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 439.94 Current children cumulated vsize (Kb) 16136 [startup+450.037 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 44976 17 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220224 134676519 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 449.94 Current children cumulated vsize (Kb) 16136 [startup+460.037 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 45976 17 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219316 134676992 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 459.94 Current children cumulated vsize (Kb) 16136 [startup+470.038 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 46977 17 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219520 134676510 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 469.95 Current children cumulated vsize (Kb) 16136 [startup+480.039 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 47977 17 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219264 134677059 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 479.95 Current children cumulated vsize (Kb) 16136 [startup+490.04 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 48977 17 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221218640 134676601 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 489.95 Current children cumulated vsize (Kb) 16136 [startup+500.041 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 49977 17 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219696 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 499.95 Current children cumulated vsize (Kb) 16136 [startup+510.042 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 50977 17 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221218816 134677257 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 509.95 Current children cumulated vsize (Kb) 16136 [startup+520.043 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 51978 17 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219344 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 519.96 Current children cumulated vsize (Kb) 16136 [startup+530.043 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 52978 17 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219696 134600301 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 529.96 Current children cumulated vsize (Kb) 16136 [startup+540.044 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 53978 18 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220752 134677287 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 539.97 Current children cumulated vsize (Kb) 16136 [startup+550.045 s] Raw data (loadavg): 1.07 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 54978 18 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220752 134600904 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 549.97 Current children cumulated vsize (Kb) 16136 [startup+560.046 s] Raw data (loadavg): 1.06 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 55978 18 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219872 134600314 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 559.97 Current children cumulated vsize (Kb) 16136 [startup+570.047 s] Raw data (loadavg): 1.05 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 56978 18 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219696 134600228 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 569.97 Current children cumulated vsize (Kb) 16136 [startup+580.047 s] Raw data (loadavg): 1.04 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 57979 18 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220048 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 579.98 Current children cumulated vsize (Kb) 16136 [startup+590.049 s] Raw data (loadavg): 1.04 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 58979 18 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219872 134676589 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 589.98 Current children cumulated vsize (Kb) 16136 [startup+600.05 s] Raw data (loadavg): 1.03 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 59979 18 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220576 134600232 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 599.98 Current children cumulated vsize (Kb) 16136 [startup+610.05 s] Raw data (loadavg): 1.03 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 60979 18 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219948 134677081 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 609.98 Current children cumulated vsize (Kb) 16136 [startup+620.051 s] Raw data (loadavg): 1.02 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 61980 18 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219848 134676989 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 619.99 Current children cumulated vsize (Kb) 16136 [startup+630.052 s] Raw data (loadavg): 1.02 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 62980 18 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220048 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 629.99 Current children cumulated vsize (Kb) 16136 [startup+640.053 s] Raw data (loadavg): 1.01 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 63980 18 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219320 134676241 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 639.99 Current children cumulated vsize (Kb) 16136 [startup+650.054 s] Raw data (loadavg): 1.01 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 64980 18 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221218700 134677228 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 649.99 Current children cumulated vsize (Kb) 16136 [startup+660.054 s] Raw data (loadavg): 1.01 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 65980 18 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219872 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 659.99 Current children cumulated vsize (Kb) 16136 [startup+670.055 s] Raw data (loadavg): 1.01 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 66981 18 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220400 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 670 Current children cumulated vsize (Kb) 16136 [startup+680.056 s] Raw data (loadavg): 1.01 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 67981 18 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221218816 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 680 Current children cumulated vsize (Kb) 16136 [startup+690.058 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 68981 18 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219520 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 690 Current children cumulated vsize (Kb) 16136 [startup+700.059 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 69981 18 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219580 134677378 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 700 Current children cumulated vsize (Kb) 16136 [startup+710.059 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 70981 19 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220224 134677346 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 710.01 Current children cumulated vsize (Kb) 16136 [startup+720.06 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 71981 19 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219872 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 720.01 Current children cumulated vsize (Kb) 16136 [startup+730.061 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 72982 19 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220400 134600295 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 730.02 Current children cumulated vsize (Kb) 16136 [startup+740.062 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 73982 19 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219696 134676595 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 740.02 Current children cumulated vsize (Kb) 16136 [startup+750.063 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 74982 19 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220300 134676331 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 750.02 Current children cumulated vsize (Kb) 16136 [startup+760.063 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 75982 19 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221218816 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 760.02 Current children cumulated vsize (Kb) 16136 [startup+770.064 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 76982 19 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219696 134677310 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 770.02 Current children cumulated vsize (Kb) 16136 [startup+780.065 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 77982 19 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221218992 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 780.02 Current children cumulated vsize (Kb) 16136 [startup+790.066 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 78983 19 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221218816 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 790.03 Current children cumulated vsize (Kb) 16136 [startup+800.066 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 79983 19 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220048 134676503 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 800.03 Current children cumulated vsize (Kb) 16136 [startup+810.067 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 80983 19 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219696 134677278 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 810.03 Current children cumulated vsize (Kb) 16136 [startup+820.068 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 81983 19 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220400 134676471 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 820.03 Current children cumulated vsize (Kb) 16136 [startup+830.069 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 82983 19 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220400 134676545 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 830.03 Current children cumulated vsize (Kb) 16136 [startup+840.071 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 83984 19 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219344 134676522 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 840.04 Current children cumulated vsize (Kb) 16136 [startup+850.072 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 84984 19 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221218992 134677354 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 850.04 Current children cumulated vsize (Kb) 16136 [startup+860.073 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 85984 19 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220112 134676336 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 860.04 Current children cumulated vsize (Kb) 16136 [startup+870.075 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 86985 19 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220048 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 870.05 Current children cumulated vsize (Kb) 16136 [startup+880.076 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 87985 19 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220752 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 880.05 Current children cumulated vsize (Kb) 16136 [startup+890.077 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 88985 19 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219312 134677147 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 890.05 Current children cumulated vsize (Kb) 16136 [startup+900.078 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 89985 19 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219500 134676382 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 900.05 Current children cumulated vsize (Kb) 16136 [startup+910.079 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 90985 20 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221218640 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 910.06 Current children cumulated vsize (Kb) 16136 [startup+920.08 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 91985 20 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220048 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 920.06 Current children cumulated vsize (Kb) 16136 [startup+930.081 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 92986 20 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220104 134676609 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 930.07 Current children cumulated vsize (Kb) 16136 [startup+940.082 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 93986 20 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219684 134600238 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 940.07 Current children cumulated vsize (Kb) 16136 [startup+950.083 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 94986 20 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220576 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 950.07 Current children cumulated vsize (Kb) 16136 [startup+960.084 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 95986 20 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219328 134600241 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 960.07 Current children cumulated vsize (Kb) 16136 [startup+970.085 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 96986 20 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219872 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 970.07 Current children cumulated vsize (Kb) 16136 [startup+980.086 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 97987 20 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220400 134600151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 980.08 Current children cumulated vsize (Kb) 16136 [startup+990.088 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 98987 20 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219840 134677147 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 990.08 Current children cumulated vsize (Kb) 16136 [startup+1000.09 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 99987 20 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219168 134677354 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 1000.08 Current children cumulated vsize (Kb) 16136 [startup+1010.09 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 100987 20 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 1010.08 Current children cumulated vsize (Kb) 16136 [startup+1020.09 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 101988 20 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220496 134676999 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 1020.09 Current children cumulated vsize (Kb) 16136 [startup+1030.09 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 102988 20 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219696 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 1030.09 Current children cumulated vsize (Kb) 16136 [startup+1040.09 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 103988 20 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220048 134600314 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 1040.09 Current children cumulated vsize (Kb) 16136 [startup+1050.09 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 104988 20 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219520 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 1050.09 Current children cumulated vsize (Kb) 16136 [startup+1060.1 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 105988 20 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220372 134676244 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 1060.09 Current children cumulated vsize (Kb) 16136 [startup+1070.1 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 106989 20 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221218992 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 1070.1 Current children cumulated vsize (Kb) 16136 [startup+1080.1 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 107989 20 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219848 134676989 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 1080.1 Current children cumulated vsize (Kb) 16136 [startup+1090.1 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 108989 21 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220576 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 1090.11 Current children cumulated vsize (Kb) 16136 [startup+1100.1 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 109989 21 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219344 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 1100.11 Current children cumulated vsize (Kb) 16136 [startup+1110.1 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 110989 21 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219872 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 1110.11 Current children cumulated vsize (Kb) 16136 [startup+1120.1 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 111989 21 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220112 134677086 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 1120.11 Current children cumulated vsize (Kb) 16136 [startup+1130.1 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 112990 21 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220496 134677065 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 1130.12 Current children cumulated vsize (Kb) 16136 [startup+1140.1 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 113990 21 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220576 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 1140.12 Current children cumulated vsize (Kb) 16136 [startup+1150.1 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 114990 21 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220928 134676542 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 1150.12 Current children cumulated vsize (Kb) 16136 [startup+1160.1 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 115990 21 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221218976 134600241 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 1160.12 Current children cumulated vsize (Kb) 16136 [startup+1170.11 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 116990 21 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220576 134600310 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 1170.12 Current children cumulated vsize (Kb) 16136 [startup+1180.11 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 117990 21 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220576 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 1180.12 Current children cumulated vsize (Kb) 16136 [startup+1190.11 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 118991 21 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220048 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 1190.13 Current children cumulated vsize (Kb) 16136 [startup+1200.11 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 119991 21 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219840 134676245 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 1200.13 Current children cumulated vsize (Kb) 16136 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1200.11 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 27612 Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27608/statm): 531 226 485 147 0 384 0 [pid=27608] vsize: 2124 Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 119991 21 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219872 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0 [pid=27612] vsize: 14012 Current children cumulated CPU time (s) 1200.13 Current children cumulated vsize (Kb) 16136 Sending SIGTERM to -27608 Sleeping 2 seconds One traced child (pid=27608) ended because it received signal 15 (SIGTERM) One traced child (pid=27612) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1200.12 CPU time (s): 1200.14 CPU user time (s): 1199.91 CPU system time (s): 0.224965 CPU usage (%): 100.002 Max. virtual memory (cumulated for all children) (Kb): 16136
ERROR: no interpretation found !