Name | mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-fast0507.opb |
MD5SUM | 38504d32a17a57a658eee171614b901e |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 324 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 63009 |
Biggest coefficient in the objective function | 2 |
Number of bits for the biggest coefficient in the objective function | 2 |
Sum of the numbers in the objective function | 122425 |
Number of bits of the sum of numbers in the objective function | 17 |
Biggest number in a constraint | 2 |
Number of bits of the biggest number in a constraint | 2 |
Biggest sum of numbers in a constraint | 122425 |
Number of bits of the biggest sum of numbers | 17 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1189.29 |
Number of variables | 63009 |
Total number of constraints | 63516 |
Number of constraints which are clauses | 507 |
Number of constraints which are cardinality constraints (but not clauses) | 63009 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 7753 |
LAUNCH ON wulflinc4 THE 2005-09-20 03:35:46 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3292 boxname=wulflinc4 idbench=948 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 38504d32a17a57a658eee171614b901e /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-fast0507.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-fast0507.opb IDLAUNCH: 3292 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.169 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.169 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: 868044 kB Buffers: 33540 kB Cached: 106020 kB SwapCached: 860 kB Active: 49476 kB Inactive: 92684 kB HighTotal: 131008 kB HighFree: 26432 kB LowTotal: 903652 kB LowFree: 841612 kB SwapTotal: 2097136 kB SwapFree: 2095644 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5520 kB Slab: 18776 kB Committed_AS: 72360 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-20 03:55:57 (client local time) WITH STATUS 10 IN 1207.21 SECONDS stats: 3292 7 1207.21 10
c Parsing PB file... c Converting 494 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: == c -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................... c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 487 407371 | 162 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 343[0m c ---[ 0]---> Adder-cost: 125984 maxlim: 122082 bits: 17/17 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 882303 3556733 | 294101 0 0 nan | 0.000 % | c | 100 | 882255 3556553 | 323511 96 289 3.0 | 0.016 % | c | 250 | 881309 3553217 | 355862 114 351 3.1 | 0.101 % | c | 475 | 880776 3551348 | 391448 259 864 3.3 | 0.151 % | c | 812 | 880279 3549615 | 430593 523 1870 3.6 | 0.196 % | c | 1318 | 879889 3548279 | 473652 977 4292 4.4 | 0.232 % | c | 2077 | 879700 3547656 | 521017 1709 10871 6.4 | 0.251 % | c | 3216 | 879644 3547470 | 573119 2839 17243 6.1 | 0.256 % | c | 4924 | 879509 3547011 | 630431 4532 25034 5.5 | 0.270 % | c | 7486 | 879420 3546722 | 693474 7079 43284 6.1 | 0.279 % | c | 11330 | 879361 3546531 | 762822 10915 68960 6.3 | 0.286 % | c | 17096 | 879361 3546531 | 839104 16681 104664 6.3 | 0.286 % | c | 25745 | 879361 3546531 | 923014 25330 246101 9.7 | 0.286 % | c | 38719 | 879284 3546264 | 1015316 38293 536469 14.0 | 0.293 % | c c *** TERMINATED *** s SATISFIABLE #### TRACE IS TOO LONG. SEE FILE pb05-wulflinc4-3292-948-3-0-8861.out.gz TO GET THE COMPLETE TRACE #### TAIL OF TRACE #### ...c Parsing PB file... c Converting 494 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: == c -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................... c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 487 407371 | 162 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 343[0m c ---[ 0]---> Adder-cost: 125984 maxlim: 122082 bits: 17/17 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 882303 3556733 | 294101 0 0 nan | 0.000 % | c | 100 | 882255 3556553 | 323511 96 289 3.0 | 0.016 % | c | 250 | 881309 3553217 | 355862 114 351 3.1 | 0.101 % | c | 475 | 880776 3551348 | 391448 259 864 3.3 | 0.151 % | c | 812 | 880279 3549615 | 430593 523 1870 3.6 | 0.196 % | c | 1318 | 879889 3548279 | 473652 977 4292 4.4 | 0.232 % | c | 2077 | 879700 3547656 | 521017 1709 10871 6.4 | 0.251 % | c | 3216 | 879644 3547470 | 573119 2839 17243 6.1 | 0.256 % | c | 4924 | 879509 3547011 | 630431 4532 25034 5.5 | 0.270 % | c | 7486 | 879420 3546722 | 693474 7079 43284 6.1 | 0.279 % | c | 11330 | 879361 3546531 | 762822 10915 68960 6.3 | 0.286 % | c | 17096 | 879361 3546531 | 839104 16681 104664 6.3 | 0.286 % | c | 25745 | 879361 3546531 | 923014 25330 246101 9.7 | 0.286 % | c | 38719 | 879284 3546264 | 1015316 38293 536469 14.0 | 0.293 % | c c *** TERMINATED *** s SATISFIABLE
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/8898/stat): 8898 (minisat+_script) R 8897 8898 6847 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1797100190 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/8898/statm): 174 3 169 147 0 27 0 [pid=8898] 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=8899 New process pid=8900 New process pid=8901 One traced child (pid=8900) exited with status: 0 execve syscall for /bin/sed executable 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=8901) exited with status: 0 One traced child (pid=8899) exited with status: 0 New process pid=8902 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-fast0507.opb [startup+10.0045 s] Raw data (loadavg): 0.96 0.97 0.89 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 15408 0 0 0 887 63 0 0 25 0 1 0 1797100195 50012160 10879 4294967295 134512640 135094434 3221224432 3221222160 134519159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 12210 10880 145 145 0 12065 0 [pid=8902] vsize: 48840 Current children cumulated CPU time (s) 9.51 Current children cumulated vsize (Kb) 50964 [startup+20.0054 s] Raw data (loadavg): 0.96 0.97 0.89 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 55972 0 0 0 1688 185 0 0 23 0 1 0 1797100195 185556992 41556 4294967295 134512640 135094434 3221224432 3221221872 134781858 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8902/statm): 45302 41556 145 145 0 45157 0 [pid=8902] vsize: 181208 Current children cumulated CPU time (s) 18.74 Current children cumulated vsize (Kb) 183332 [startup+30.0062 s] Raw data (loadavg): 0.97 0.97 0.89 1/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) T 8898 8898 6847 0 -1 0 97910 0 0 0 2492 304 0 0 24 0 1 0 1797100195 332865536 72948 4294967295 134512640 135094434 3221224432 3221220844 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/8902/statm): 81266 72948 145 145 0 81121 0 [pid=8902] vsize: 325064 Current children cumulated CPU time (s) 27.97 Current children cumulated vsize (Kb) 327188 [startup+40.0071 s] Raw data (loadavg): 0.97 0.97 0.90 1/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) T 8898 8898 6847 0 -1 0 114257 0 0 0 3385 358 0 0 25 0 1 0 1797100195 374099968 88387 4294967295 134512640 135094434 3221224432 3221216092 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/8902/statm): 91333 88387 145 145 0 91188 0 [pid=8902] vsize: 365332 Current children cumulated CPU time (s) 37.44 Current children cumulated vsize (Kb) 367456 [startup+50.0089 s] Raw data (loadavg): 0.98 0.97 0.90 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 126981 0 0 0 4273 414 0 0 25 0 1 0 1797100195 428355584 101111 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8902/statm): 104579 101111 145 145 0 104434 0 [pid=8902] vsize: 418316 Current children cumulated CPU time (s) 46.88 Current children cumulated vsize (Kb) 420440 [startup+60.0108 s] Raw data (loadavg): 0.98 0.97 0.90 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 126990 0 0 0 5271 415 0 0 25 0 1 0 1797100195 428392448 101120 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 104588 101120 145 145 0 104443 0 [pid=8902] vsize: 418352 Current children cumulated CPU time (s) 56.87 Current children cumulated vsize (Kb) 420476 [startup+70.0116 s] Raw data (loadavg): 0.98 0.97 0.90 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 127009 0 0 0 6270 415 0 0 25 0 1 0 1797100195 428470272 101139 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8902/statm): 104607 101139 145 145 0 104462 0 [pid=8902] vsize: 418428 Current children cumulated CPU time (s) 66.86 Current children cumulated vsize (Kb) 420552 [startup+80.0125 s] Raw data (loadavg): 0.98 0.97 0.90 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 127063 0 0 0 7270 416 0 0 25 0 1 0 1797100195 428691456 101193 4294967295 134512640 135094434 3221224432 3221223044 134563052 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 104661 101193 145 145 0 104516 0 [pid=8902] vsize: 418644 Current children cumulated CPU time (s) 76.87 Current children cumulated vsize (Kb) 420768 [startup+90.0133 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 127545 0 0 0 8263 419 0 0 25 0 1 0 1797100195 430665728 101675 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105143 101675 145 145 0 104998 0 [pid=8902] vsize: 420572 Current children cumulated CPU time (s) 86.83 Current children cumulated vsize (Kb) 422696 [startup+100.014 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 127744 0 0 0 9261 420 0 0 25 0 1 0 1797100195 431714304 101874 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105399 101874 145 145 0 105254 0 [pid=8902] vsize: 421596 Current children cumulated CPU time (s) 96.82 Current children cumulated vsize (Kb) 423720 [startup+110.016 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 127831 0 0 0 10259 420 0 0 25 0 1 0 1797100195 431996928 101961 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105468 101961 145 145 0 105323 0 [pid=8902] vsize: 421872 Current children cumulated CPU time (s) 106.8 Current children cumulated vsize (Kb) 423996 [startup+120.017 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 127887 0 0 0 11259 421 0 0 25 0 1 0 1797100195 432226304 102017 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105524 102017 145 145 0 105379 0 [pid=8902] vsize: 422096 Current children cumulated CPU time (s) 116.81 Current children cumulated vsize (Kb) 424220 [startup+130.017 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 127933 0 0 0 12258 421 0 0 25 0 1 0 1797100195 432410624 102063 4294967295 134512640 135094434 3221224432 3221223104 134555583 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105569 102063 145 145 0 105424 0 [pid=8902] vsize: 422276 Current children cumulated CPU time (s) 126.8 Current children cumulated vsize (Kb) 424400 [startup+140.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 127976 0 0 0 13258 421 0 0 25 0 1 0 1797100195 432529408 102106 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105598 102106 145 145 0 105453 0 [pid=8902] vsize: 422392 Current children cumulated CPU time (s) 136.8 Current children cumulated vsize (Kb) 424516 [startup+150.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128005 0 0 0 14258 421 0 0 25 0 1 0 1797100195 432623616 102135 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105621 102135 145 145 0 105476 0 [pid=8902] vsize: 422484 Current children cumulated CPU time (s) 146.8 Current children cumulated vsize (Kb) 424608 [startup+160.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128027 0 0 0 15258 421 0 0 25 0 1 0 1797100195 432697344 102157 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105639 102157 145 145 0 105494 0 [pid=8902] vsize: 422556 Current children cumulated CPU time (s) 156.8 Current children cumulated vsize (Kb) 424680 [startup+170.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128042 0 0 0 16258 421 0 0 25 0 1 0 1797100195 432758784 102172 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105654 102172 145 145 0 105509 0 [pid=8902] vsize: 422616 Current children cumulated CPU time (s) 166.8 Current children cumulated vsize (Kb) 424740 [startup+180.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128055 0 0 0 17258 421 0 0 25 0 1 0 1797100195 432807936 102185 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105666 102185 145 145 0 105521 0 [pid=8902] vsize: 422664 Current children cumulated CPU time (s) 176.8 Current children cumulated vsize (Kb) 424788 [startup+190.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128063 0 0 0 18258 421 0 0 25 0 1 0 1797100195 432840704 102193 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105674 102193 145 145 0 105529 0 [pid=8902] vsize: 422696 Current children cumulated CPU time (s) 186.8 Current children cumulated vsize (Kb) 424820 [startup+200.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128081 0 0 0 19258 422 0 0 25 0 1 0 1797100195 432943104 102211 4294967295 134512640 135094434 3221224432 3221223088 134561502 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105699 102211 145 145 0 105554 0 [pid=8902] vsize: 422796 Current children cumulated CPU time (s) 196.81 Current children cumulated vsize (Kb) 424920 [startup+210.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128081 0 0 0 20258 422 0 0 25 0 1 0 1797100195 432943104 102211 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105699 102211 145 145 0 105554 0 [pid=8902] vsize: 422796 Current children cumulated CPU time (s) 206.81 Current children cumulated vsize (Kb) 424920 [startup+220.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128087 0 0 0 21258 422 0 0 25 0 1 0 1797100195 432963584 102217 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105704 102217 145 145 0 105559 0 [pid=8902] vsize: 422816 Current children cumulated CPU time (s) 216.81 Current children cumulated vsize (Kb) 424940 [startup+230.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128096 0 0 0 22258 422 0 0 25 0 1 0 1797100195 432984064 102226 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105709 102226 145 145 0 105564 0 [pid=8902] vsize: 422836 Current children cumulated CPU time (s) 226.81 Current children cumulated vsize (Kb) 424960 [startup+240.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128101 0 0 0 23258 422 0 0 25 0 1 0 1797100195 433004544 102231 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105714 102231 145 145 0 105569 0 [pid=8902] vsize: 422856 Current children cumulated CPU time (s) 236.81 Current children cumulated vsize (Kb) 424980 [startup+250.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128109 0 0 0 24258 422 0 0 25 0 1 0 1797100195 433033216 102239 4294967295 134512640 135094434 3221224432 3221223072 134562068 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105721 102239 145 145 0 105576 0 [pid=8902] vsize: 422884 Current children cumulated CPU time (s) 246.81 Current children cumulated vsize (Kb) 425008 [startup+260.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128113 0 0 0 25259 422 0 0 25 0 1 0 1797100195 433049600 102243 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105725 102243 145 145 0 105580 0 [pid=8902] vsize: 422900 Current children cumulated CPU time (s) 256.82 Current children cumulated vsize (Kb) 425024 [startup+270.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128121 0 0 0 26259 422 0 0 25 0 1 0 1797100195 433065984 102251 4294967295 134512640 135094434 3221224432 3221223044 134563064 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105729 102251 145 145 0 105584 0 [pid=8902] vsize: 422916 Current children cumulated CPU time (s) 266.82 Current children cumulated vsize (Kb) 425040 [startup+280.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128129 0 0 0 27259 422 0 0 25 0 1 0 1797100195 433094656 102259 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105736 102259 145 145 0 105591 0 [pid=8902] vsize: 422944 Current children cumulated CPU time (s) 276.82 Current children cumulated vsize (Kb) 425068 [startup+290.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128132 0 0 0 28259 422 0 0 25 0 1 0 1797100195 433106944 102262 4294967295 134512640 135094434 3221224432 3221223088 134561463 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105739 102262 145 145 0 105594 0 [pid=8902] vsize: 422956 Current children cumulated CPU time (s) 286.82 Current children cumulated vsize (Kb) 425080 [startup+300.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128133 0 0 0 29259 422 0 0 25 0 1 0 1797100195 433111040 102263 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105740 102263 145 145 0 105595 0 [pid=8902] vsize: 422960 Current children cumulated CPU time (s) 296.82 Current children cumulated vsize (Kb) 425084 [startup+310.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128140 0 0 0 30259 422 0 0 25 0 1 0 1797100195 433131520 102270 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105745 102270 145 145 0 105600 0 [pid=8902] vsize: 422980 Current children cumulated CPU time (s) 306.82 Current children cumulated vsize (Kb) 425104 [startup+320.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128145 0 0 0 31259 422 0 0 25 0 1 0 1797100195 433143808 102275 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105748 102275 145 145 0 105603 0 [pid=8902] vsize: 422992 Current children cumulated CPU time (s) 316.82 Current children cumulated vsize (Kb) 425116 [startup+330.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128150 0 0 0 32259 422 0 0 25 0 1 0 1797100195 433164288 102280 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105753 102280 145 145 0 105608 0 [pid=8902] vsize: 423012 Current children cumulated CPU time (s) 326.82 Current children cumulated vsize (Kb) 425136 [startup+340.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128153 0 0 0 33260 422 0 0 25 0 1 0 1797100195 433172480 102283 4294967295 134512640 135094434 3221224432 3221223044 134563077 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105755 102283 145 145 0 105610 0 [pid=8902] vsize: 423020 Current children cumulated CPU time (s) 336.83 Current children cumulated vsize (Kb) 425144 [startup+350.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128154 0 0 0 34260 422 0 0 25 0 1 0 1797100195 433176576 102284 4294967295 134512640 135094434 3221224432 3221223120 134554750 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105756 102284 145 145 0 105611 0 [pid=8902] vsize: 423024 Current children cumulated CPU time (s) 346.83 Current children cumulated vsize (Kb) 425148 [startup+360.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128157 0 0 0 35260 422 0 0 25 0 1 0 1797100195 433188864 102287 4294967295 134512640 135094434 3221224432 3221223052 134562986 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105759 102287 145 145 0 105614 0 [pid=8902] vsize: 423036 Current children cumulated CPU time (s) 356.83 Current children cumulated vsize (Kb) 425160 [startup+370.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128164 0 0 0 36260 422 0 0 25 0 1 0 1797100195 433213440 102294 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105765 102294 145 145 0 105620 0 [pid=8902] vsize: 423060 Current children cumulated CPU time (s) 366.83 Current children cumulated vsize (Kb) 425184 [startup+380.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128168 0 0 0 37260 422 0 0 25 0 1 0 1797100195 433229824 102298 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105769 102298 145 145 0 105624 0 [pid=8902] vsize: 423076 Current children cumulated CPU time (s) 376.83 Current children cumulated vsize (Kb) 425200 [startup+390.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128172 0 0 0 38261 422 0 0 25 0 1 0 1797100195 433233920 102302 4294967295 134512640 135094434 3221224432 3221223088 134561471 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105770 102302 145 145 0 105625 0 [pid=8902] vsize: 423080 Current children cumulated CPU time (s) 386.84 Current children cumulated vsize (Kb) 425204 [startup+400.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128174 0 0 0 39261 422 0 0 25 0 1 0 1797100195 433242112 102304 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105772 102304 145 145 0 105627 0 [pid=8902] vsize: 423088 Current children cumulated CPU time (s) 396.84 Current children cumulated vsize (Kb) 425212 [startup+410.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128176 0 0 0 40261 422 0 0 25 0 1 0 1797100195 433250304 102306 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105774 102306 145 145 0 105629 0 [pid=8902] vsize: 423096 Current children cumulated CPU time (s) 406.84 Current children cumulated vsize (Kb) 425220 [startup+420.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128179 0 0 0 41261 422 0 0 25 0 1 0 1797100195 433258496 102309 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105776 102309 145 145 0 105631 0 [pid=8902] vsize: 423104 Current children cumulated CPU time (s) 416.84 Current children cumulated vsize (Kb) 425228 [startup+430.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128181 0 0 0 42261 423 0 0 25 0 1 0 1797100195 433266688 102311 4294967295 134512640 135094434 3221224432 3221223088 134561514 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105778 102311 145 145 0 105633 0 [pid=8902] vsize: 423112 Current children cumulated CPU time (s) 426.85 Current children cumulated vsize (Kb) 425236 [startup+440.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128185 0 0 0 43262 423 0 0 25 0 1 0 1797100195 433283072 102315 4294967295 134512640 135094434 3221224432 3221223088 134561698 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105782 102315 145 145 0 105637 0 [pid=8902] vsize: 423128 Current children cumulated CPU time (s) 436.86 Current children cumulated vsize (Kb) 425252 [startup+450.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128190 0 0 0 44262 423 0 0 25 0 1 0 1797100195 433299456 102320 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105786 102320 145 145 0 105641 0 [pid=8902] vsize: 423144 Current children cumulated CPU time (s) 446.86 Current children cumulated vsize (Kb) 425268 [startup+460.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128211 0 0 0 45262 423 0 0 25 0 1 0 1797100195 433446912 102341 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105822 102341 145 145 0 105677 0 [pid=8902] vsize: 423288 Current children cumulated CPU time (s) 456.86 Current children cumulated vsize (Kb) 425412 [startup+470.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128216 0 0 0 46262 423 0 0 25 0 1 0 1797100195 433446912 102346 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8902/statm): 105822 102346 145 145 0 105677 0 [pid=8902] vsize: 423288 Current children cumulated CPU time (s) 466.86 Current children cumulated vsize (Kb) 425412 [startup+480.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128218 0 0 0 47262 423 0 0 25 0 1 0 1797100195 433455104 102348 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105824 102348 145 145 0 105679 0 [pid=8902] vsize: 423296 Current children cumulated CPU time (s) 476.86 Current children cumulated vsize (Kb) 425420 [startup+490.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128224 0 0 0 48262 423 0 0 25 0 1 0 1797100195 433475584 102354 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105829 102354 145 145 0 105684 0 [pid=8902] vsize: 423316 Current children cumulated CPU time (s) 486.86 Current children cumulated vsize (Kb) 425440 [startup+500.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128231 0 0 0 49262 423 0 0 25 0 1 0 1797100195 433504256 102361 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105836 102361 145 145 0 105691 0 [pid=8902] vsize: 423344 Current children cumulated CPU time (s) 496.86 Current children cumulated vsize (Kb) 425468 [startup+510.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128245 0 0 0 50262 423 0 0 25 0 1 0 1797100195 433557504 102375 4294967295 134512640 135094434 3221224432 3221223044 134563089 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105849 102375 145 145 0 105704 0 [pid=8902] vsize: 423396 Current children cumulated CPU time (s) 506.86 Current children cumulated vsize (Kb) 425520 [startup+520.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128250 0 0 0 51262 423 0 0 25 0 1 0 1797100195 433577984 102380 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105854 102380 145 145 0 105709 0 [pid=8902] vsize: 423416 Current children cumulated CPU time (s) 516.86 Current children cumulated vsize (Kb) 425540 [startup+530.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128258 0 0 0 52263 423 0 0 25 0 1 0 1797100195 433610752 102388 4294967295 134512640 135094434 3221224432 3221223072 134562057 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105862 102388 145 145 0 105717 0 [pid=8902] vsize: 423448 Current children cumulated CPU time (s) 526.87 Current children cumulated vsize (Kb) 425572 [startup+540.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128320 0 0 0 53261 424 0 0 25 0 1 0 1797100195 433819648 102450 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105913 102450 145 145 0 105768 0 [pid=8902] vsize: 423652 Current children cumulated CPU time (s) 536.86 Current children cumulated vsize (Kb) 425776 [startup+550.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128324 0 0 0 54261 424 0 0 25 0 1 0 1797100195 433836032 102454 4294967295 134512640 135094434 3221224432 3221223044 134563041 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105917 102454 145 145 0 105772 0 [pid=8902] vsize: 423668 Current children cumulated CPU time (s) 546.86 Current children cumulated vsize (Kb) 425792 [startup+560.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128327 0 0 0 55262 424 0 0 25 0 1 0 1797100195 433848320 102457 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105920 102457 145 145 0 105775 0 [pid=8902] vsize: 423680 Current children cumulated CPU time (s) 556.87 Current children cumulated vsize (Kb) 425804 [startup+570.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128330 0 0 0 56262 424 0 0 25 0 1 0 1797100195 433860608 102460 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105923 102460 145 145 0 105778 0 [pid=8902] vsize: 423692 Current children cumulated CPU time (s) 566.87 Current children cumulated vsize (Kb) 425816 [startup+580.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128335 0 0 0 57262 424 0 0 25 0 1 0 1797100195 433876992 102465 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105927 102465 145 145 0 105782 0 [pid=8902] vsize: 423708 Current children cumulated CPU time (s) 576.87 Current children cumulated vsize (Kb) 425832 [startup+590.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128343 0 0 0 58262 424 0 0 25 0 1 0 1797100195 433909760 102473 4294967295 134512640 135094434 3221224432 3221223044 134563080 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105935 102473 145 145 0 105790 0 [pid=8902] vsize: 423740 Current children cumulated CPU time (s) 586.87 Current children cumulated vsize (Kb) 425864 [startup+600.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128351 0 0 0 59262 424 0 0 25 0 1 0 1797100195 433942528 102481 4294967295 134512640 135094434 3221224432 3221223088 134561508 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105943 102481 145 145 0 105798 0 [pid=8902] vsize: 423772 Current children cumulated CPU time (s) 596.87 Current children cumulated vsize (Kb) 425896 [startup+610.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128375 0 0 0 60262 424 0 0 25 0 1 0 1797100195 434032640 102505 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105965 102505 145 145 0 105820 0 [pid=8902] vsize: 423860 Current children cumulated CPU time (s) 606.87 Current children cumulated vsize (Kb) 425984 [startup+620.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128387 0 0 0 61262 424 0 0 25 0 1 0 1797100195 434081792 102517 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105977 102517 145 145 0 105832 0 [pid=8902] vsize: 423908 Current children cumulated CPU time (s) 616.87 Current children cumulated vsize (Kb) 426032 [startup+630.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128392 0 0 0 62262 424 0 0 25 0 1 0 1797100195 434098176 102522 4294967295 134512640 135094434 3221224432 3221223044 134563069 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105981 102522 145 145 0 105836 0 [pid=8902] vsize: 423924 Current children cumulated CPU time (s) 626.87 Current children cumulated vsize (Kb) 426048 [startup+640.066 s] Raw data (loadavg): 0.99 0.97 0.91 5/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128400 0 0 0 63262 424 0 0 25 0 1 0 1797100195 434130944 102530 4294967295 134512640 135094434 3221224432 3221223072 134558048 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105989 102530 145 145 0 105844 0 [pid=8902] vsize: 423956 Current children cumulated CPU time (s) 636.87 Current children cumulated vsize (Kb) 426080 [startup+650.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128410 0 0 0 64262 424 0 0 25 0 1 0 1797100195 434171904 102540 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 105999 102540 145 145 0 105854 0 [pid=8902] vsize: 423996 Current children cumulated CPU time (s) 646.87 Current children cumulated vsize (Kb) 426120 [startup+660.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128422 0 0 0 65262 424 0 0 25 0 1 0 1797100195 434216960 102552 4294967295 134512640 135094434 3221224432 3221223072 134562090 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106010 102552 145 145 0 105865 0 [pid=8902] vsize: 424040 Current children cumulated CPU time (s) 656.87 Current children cumulated vsize (Kb) 426164 [startup+670.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128432 0 0 0 66262 425 0 0 25 0 1 0 1797100195 434257920 102562 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106020 102562 145 145 0 105875 0 [pid=8902] vsize: 424080 Current children cumulated CPU time (s) 666.88 Current children cumulated vsize (Kb) 426204 [startup+680.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128501 0 0 0 67261 425 0 0 25 0 1 0 1797100195 434532352 102631 4294967295 134512640 135094434 3221224432 3221223044 134563066 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106087 102631 145 145 0 105942 0 [pid=8902] vsize: 424348 Current children cumulated CPU time (s) 676.87 Current children cumulated vsize (Kb) 426472 [startup+690.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128506 0 0 0 68262 425 0 0 25 0 1 0 1797100195 434552832 102636 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106092 102636 145 145 0 105947 0 [pid=8902] vsize: 424368 Current children cumulated CPU time (s) 686.88 Current children cumulated vsize (Kb) 426492 [startup+700.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128514 0 0 0 69261 425 0 0 25 0 1 0 1797100195 434573312 102644 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106097 102644 145 145 0 105952 0 [pid=8902] vsize: 424388 Current children cumulated CPU time (s) 696.87 Current children cumulated vsize (Kb) 426512 [startup+710.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128518 0 0 0 70262 425 0 0 25 0 1 0 1797100195 434589696 102648 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106101 102648 145 145 0 105956 0 [pid=8902] vsize: 424404 Current children cumulated CPU time (s) 706.88 Current children cumulated vsize (Kb) 426528 [startup+720.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128519 0 0 0 71262 425 0 0 25 0 1 0 1797100195 434593792 102649 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106102 102649 145 145 0 105957 0 [pid=8902] vsize: 424408 Current children cumulated CPU time (s) 716.88 Current children cumulated vsize (Kb) 426532 [startup+730.075 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128523 0 0 0 72262 425 0 0 25 0 1 0 1797100195 434601984 102653 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106104 102653 145 145 0 105959 0 [pid=8902] vsize: 424416 Current children cumulated CPU time (s) 726.88 Current children cumulated vsize (Kb) 426540 [startup+740.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128528 0 0 0 73262 425 0 0 25 0 1 0 1797100195 434622464 102658 4294967295 134512640 135094434 3221224432 3221223088 134561737 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106109 102658 145 145 0 105964 0 [pid=8902] vsize: 424436 Current children cumulated CPU time (s) 736.88 Current children cumulated vsize (Kb) 426560 [startup+750.077 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128534 0 0 0 74262 425 0 0 25 0 1 0 1797100195 434647040 102664 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106115 102664 145 145 0 105970 0 [pid=8902] vsize: 424460 Current children cumulated CPU time (s) 746.88 Current children cumulated vsize (Kb) 426584 [startup+760.079 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128537 0 0 0 75262 425 0 0 25 0 1 0 1797100195 434659328 102667 4294967295 134512640 135094434 3221224432 3221223088 134561476 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106118 102667 145 145 0 105973 0 [pid=8902] vsize: 424472 Current children cumulated CPU time (s) 756.88 Current children cumulated vsize (Kb) 426596 [startup+770.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128540 0 0 0 76263 426 0 0 25 0 1 0 1797100195 434667520 102670 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106120 102670 145 145 0 105975 0 [pid=8902] vsize: 424480 Current children cumulated CPU time (s) 766.9 Current children cumulated vsize (Kb) 426604 [startup+780.081 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128546 0 0 0 77263 426 0 0 25 0 1 0 1797100195 434692096 102676 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106126 102676 145 145 0 105981 0 [pid=8902] vsize: 424504 Current children cumulated CPU time (s) 776.9 Current children cumulated vsize (Kb) 426628 [startup+790.082 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8902 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128647 0 0 0 78261 426 0 0 25 0 1 0 1797100195 435097600 102777 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106225 102777 145 145 0 106080 0 [pid=8902] vsize: 424900 Current children cumulated CPU time (s) 786.88 Current children cumulated vsize (Kb) 427024 [startup+800.082 s] Raw data (loadavg): 0.99 0.97 0.91 3/61 8945 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128661 0 0 0 79260 427 0 0 17 0 1 0 1797100195 435154944 102791 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106239 102791 145 145 0 106094 0 [pid=8902] vsize: 424956 Current children cumulated CPU time (s) 796.88 Current children cumulated vsize (Kb) 427080 [startup+810.085 s] Raw data (loadavg): 1.07 0.99 0.91 2/57 8953 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128669 0 0 0 80260 427 0 0 25 0 1 0 1797100195 435187712 102799 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106247 102799 145 145 0 106102 0 [pid=8902] vsize: 424988 Current children cumulated CPU time (s) 806.88 Current children cumulated vsize (Kb) 427112 [startup+820.086 s] Raw data (loadavg): 1.06 0.99 0.91 2/57 8953 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128679 0 0 0 81260 427 0 0 25 0 1 0 1797100195 435228672 102809 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106257 102809 145 145 0 106112 0 [pid=8902] vsize: 425028 Current children cumulated CPU time (s) 816.88 Current children cumulated vsize (Kb) 427152 [startup+830.087 s] Raw data (loadavg): 1.05 0.99 0.91 2/57 8953 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128717 0 0 0 82260 428 0 0 25 0 1 0 1797100195 435511296 102847 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106326 102847 145 145 0 106181 0 [pid=8902] vsize: 425304 Current children cumulated CPU time (s) 826.89 Current children cumulated vsize (Kb) 427428 [startup+840.088 s] Raw data (loadavg): 1.04 0.99 0.91 2/57 8953 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128717 0 0 0 83260 428 0 0 25 0 1 0 1797100195 435511296 102847 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106326 102847 145 145 0 106181 0 [pid=8902] vsize: 425304 Current children cumulated CPU time (s) 836.89 Current children cumulated vsize (Kb) 427428 [startup+850.089 s] Raw data (loadavg): 1.03 0.99 0.91 2/57 8953 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128717 0 0 0 84260 428 0 0 25 0 1 0 1797100195 435511296 102847 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106326 102847 145 145 0 106181 0 [pid=8902] vsize: 425304 Current children cumulated CPU time (s) 846.89 Current children cumulated vsize (Kb) 427428 [startup+860.09 s] Raw data (loadavg): 1.03 0.99 0.91 2/57 8953 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128718 0 0 0 85260 428 0 0 25 0 1 0 1797100195 435511296 102848 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106326 102848 145 145 0 106181 0 [pid=8902] vsize: 425304 Current children cumulated CPU time (s) 856.89 Current children cumulated vsize (Kb) 427428 [startup+870.092 s] Raw data (loadavg): 1.02 0.99 0.91 2/57 8955 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128718 0 0 0 86261 428 0 0 25 0 1 0 1797100195 435511296 102848 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106326 102848 145 145 0 106181 0 [pid=8902] vsize: 425304 Current children cumulated CPU time (s) 866.9 Current children cumulated vsize (Kb) 427428 [startup+880.093 s] Raw data (loadavg): 1.02 0.99 0.91 2/57 8957 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128719 0 0 0 87261 428 0 0 25 0 1 0 1797100195 435511296 102849 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106326 102849 145 145 0 106181 0 [pid=8902] vsize: 425304 Current children cumulated CPU time (s) 876.9 Current children cumulated vsize (Kb) 427428 [startup+890.094 s] Raw data (loadavg): 1.02 0.99 0.91 2/57 8957 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128720 0 0 0 88261 428 0 0 25 0 1 0 1797100195 435511296 102850 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106326 102850 145 145 0 106181 0 [pid=8902] vsize: 425304 Current children cumulated CPU time (s) 886.9 Current children cumulated vsize (Kb) 427428 [startup+900.095 s] Raw data (loadavg): 1.01 0.99 0.91 2/57 8957 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128721 0 0 0 89261 428 0 0 25 0 1 0 1797100195 435515392 102851 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106327 102851 145 145 0 106182 0 [pid=8902] vsize: 425308 Current children cumulated CPU time (s) 896.9 Current children cumulated vsize (Kb) 427432 [startup+910.096 s] Raw data (loadavg): 1.01 0.99 0.91 2/57 8957 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128724 0 0 0 90262 428 0 0 25 0 1 0 1797100195 435527680 102854 4294967295 134512640 135094434 3221224432 3221223112 134554880 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106330 102854 145 145 0 106185 0 [pid=8902] vsize: 425320 Current children cumulated CPU time (s) 906.91 Current children cumulated vsize (Kb) 427444 [startup+920.097 s] Raw data (loadavg): 1.01 0.99 0.91 2/57 8957 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128729 0 0 0 91262 428 0 0 25 0 1 0 1797100195 435548160 102859 4294967295 134512640 135094434 3221224432 3221223084 134561522 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106335 102859 145 145 0 106190 0 [pid=8902] vsize: 425340 Current children cumulated CPU time (s) 916.91 Current children cumulated vsize (Kb) 427464 [startup+930.098 s] Raw data (loadavg): 1.01 0.99 0.91 2/57 8957 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128744 0 0 0 92262 428 0 0 25 0 1 0 1797100195 435605504 102874 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106349 102874 145 145 0 106204 0 [pid=8902] vsize: 425396 Current children cumulated CPU time (s) 926.91 Current children cumulated vsize (Kb) 427520 [startup+940.099 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 8957 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128772 0 0 0 93261 428 0 0 25 0 1 0 1797100195 435720192 102902 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106377 102902 145 145 0 106232 0 [pid=8902] vsize: 425508 Current children cumulated CPU time (s) 936.9 Current children cumulated vsize (Kb) 427632 [startup+950.1 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 8957 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128806 0 0 0 94261 428 0 0 25 0 1 0 1797100195 435855360 102936 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106410 102936 145 145 0 106265 0 [pid=8902] vsize: 425640 Current children cumulated CPU time (s) 946.9 Current children cumulated vsize (Kb) 427764 [startup+960.101 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 8957 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128830 0 0 0 95261 428 0 0 25 0 1 0 1797100195 435949568 102960 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106433 102960 145 145 0 106288 0 [pid=8902] vsize: 425732 Current children cumulated CPU time (s) 956.9 Current children cumulated vsize (Kb) 427856 [startup+970.102 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 8957 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128853 0 0 0 96260 429 0 0 25 0 1 0 1797100195 436043776 102983 4294967295 134512640 135094434 3221224432 3221223044 134563024 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106456 102983 145 145 0 106311 0 [pid=8902] vsize: 425824 Current children cumulated CPU time (s) 966.9 Current children cumulated vsize (Kb) 427948 [startup+980.102 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 8957 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128872 0 0 0 97260 429 0 0 25 0 1 0 1797100195 436117504 103002 4294967295 134512640 135094434 3221224432 3221223108 134554883 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106474 103002 145 145 0 106329 0 [pid=8902] vsize: 425896 Current children cumulated CPU time (s) 976.9 Current children cumulated vsize (Kb) 428020 [startup+990.102 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 8957 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128963 0 0 0 98258 430 0 0 25 0 1 0 1797100195 436482048 103093 4294967295 134512640 135094434 3221224432 3221223024 134556815 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106563 103093 145 145 0 106418 0 [pid=8902] vsize: 426252 Current children cumulated CPU time (s) 986.89 Current children cumulated vsize (Kb) 428376 [startup+1000.1 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 8957 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 129066 0 0 0 99256 430 0 0 25 0 1 0 1797100195 436895744 103196 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106664 103196 145 145 0 106519 0 [pid=8902] vsize: 426656 Current children cumulated CPU time (s) 996.87 Current children cumulated vsize (Kb) 428780 [startup+1010.1 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 8957 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 129083 0 0 0 100256 430 0 0 25 0 1 0 1797100195 436961280 103213 4294967295 134512640 135094434 3221224432 3221223088 134561741 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106680 103213 145 145 0 106535 0 [pid=8902] vsize: 426720 Current children cumulated CPU time (s) 1006.87 Current children cumulated vsize (Kb) 428844 [startup+1020.11 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 8957 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 129088 0 0 0 101256 430 0 0 25 0 1 0 1797100195 436981760 103218 4294967295 134512640 135094434 3221224432 3221223072 134562045 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106685 103218 145 145 0 106540 0 [pid=8902] vsize: 426740 Current children cumulated CPU time (s) 1016.87 Current children cumulated vsize (Kb) 428864 [startup+1030.11 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 8957 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 129106 0 0 0 102256 431 0 0 25 0 1 0 1797100195 437055488 103236 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106703 103236 145 145 0 106558 0 [pid=8902] vsize: 426812 Current children cumulated CPU time (s) 1026.88 Current children cumulated vsize (Kb) 428936 [startup+1040.11 s] Raw data (loadavg): 1.08 1.00 0.92 2/57 8957 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 129115 0 0 0 103256 431 0 0 25 0 1 0 1797100195 437088256 103245 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106711 103245 145 145 0 106566 0 [pid=8902] vsize: 426844 Current children cumulated CPU time (s) 1036.88 Current children cumulated vsize (Kb) 428968 [startup+1050.11 s] Raw data (loadavg): 1.07 1.00 0.92 2/57 8957 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 129132 0 0 0 104256 431 0 0 25 0 1 0 1797100195 437157888 103262 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106728 103262 145 145 0 106583 0 [pid=8902] vsize: 426912 Current children cumulated CPU time (s) 1046.88 Current children cumulated vsize (Kb) 429036 [startup+1060.11 s] Raw data (loadavg): 1.06 1.00 0.92 2/57 8957 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 129169 0 0 0 105255 431 0 0 25 0 1 0 1797100195 437309440 103299 4294967295 134512640 135094434 3221224432 3221223088 134558026 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106765 103299 145 145 0 106620 0 [pid=8902] vsize: 427060 Current children cumulated CPU time (s) 1056.87 Current children cumulated vsize (Kb) 429184 [startup+1070.11 s] Raw data (loadavg): 1.05 1.00 0.92 2/57 8957 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 129196 0 0 0 106254 432 0 0 25 0 1 0 1797100195 437415936 103326 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106791 103326 145 145 0 106646 0 [pid=8902] vsize: 427164 Current children cumulated CPU time (s) 1066.87 Current children cumulated vsize (Kb) 429288 [startup+1080.11 s] Raw data (loadavg): 1.04 1.00 0.92 2/57 8957 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 129220 0 0 0 107254 432 0 0 25 0 1 0 1797100195 437514240 103350 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106815 103350 145 145 0 106670 0 [pid=8902] vsize: 427260 Current children cumulated CPU time (s) 1076.87 Current children cumulated vsize (Kb) 429384 [startup+1090.11 s] Raw data (loadavg): 1.03 1.00 0.92 2/57 8957 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 129235 0 0 0 108254 432 0 0 25 0 1 0 1797100195 437571584 103365 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106829 103365 145 145 0 106684 0 [pid=8902] vsize: 427316 Current children cumulated CPU time (s) 1086.87 Current children cumulated vsize (Kb) 429440 [startup+1100.11 s] Raw data (loadavg): 1.03 1.00 0.92 2/57 8957 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 129249 0 0 0 109254 432 0 0 25 0 1 0 1797100195 437628928 103379 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106843 103379 145 145 0 106698 0 [pid=8902] vsize: 427372 Current children cumulated CPU time (s) 1096.87 Current children cumulated vsize (Kb) 429496 [startup+1110.11 s] Raw data (loadavg): 1.02 1.00 0.92 2/57 8957 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 129265 0 0 0 110254 432 0 0 25 0 1 0 1797100195 437694464 103395 4294967295 134512640 135094434 3221224432 3221223088 134558029 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106859 103395 145 145 0 106714 0 [pid=8902] vsize: 427436 Current children cumulated CPU time (s) 1106.87 Current children cumulated vsize (Kb) 429560 [startup+1120.11 s] Raw data (loadavg): 1.02 1.00 0.92 2/57 8957 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 129279 0 0 0 111254 432 0 0 25 0 1 0 1797100195 437747712 103409 4294967295 134512640 135094434 3221224432 3221223120 134554854 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106872 103409 145 145 0 106727 0 [pid=8902] vsize: 427488 Current children cumulated CPU time (s) 1116.87 Current children cumulated vsize (Kb) 429612 [startup+1130.11 s] Raw data (loadavg): 1.02 1.00 0.92 2/57 8957 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 129299 0 0 0 112254 433 0 0 25 0 1 0 1797100195 437829632 103429 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106892 103429 145 145 0 106747 0 [pid=8902] vsize: 427568 Current children cumulated CPU time (s) 1126.88 Current children cumulated vsize (Kb) 429692 [startup+1140.12 s] Raw data (loadavg): 1.01 1.00 0.92 2/57 8957 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 129317 0 0 0 113253 433 0 0 25 0 1 0 1797100195 437903360 103447 4294967295 134512640 135094434 3221224432 3221223088 134561505 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106910 103447 145 145 0 106765 0 [pid=8902] vsize: 427640 Current children cumulated CPU time (s) 1136.87 Current children cumulated vsize (Kb) 429764 [startup+1150.12 s] Raw data (loadavg): 1.01 1.00 0.92 2/57 8957 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 129326 0 0 0 114253 433 0 0 25 0 1 0 1797100195 437940224 103456 4294967295 134512640 135094434 3221224432 3221223072 134562128 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106919 103456 145 145 0 106774 0 [pid=8902] vsize: 427676 Current children cumulated CPU time (s) 1146.87 Current children cumulated vsize (Kb) 429800 [startup+1160.12 s] Raw data (loadavg): 1.01 1.00 0.92 2/57 8957 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 129337 0 0 0 115253 433 0 0 25 0 1 0 1797100195 437985280 103467 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106930 103467 145 145 0 106785 0 [pid=8902] vsize: 427720 Current children cumulated CPU time (s) 1156.87 Current children cumulated vsize (Kb) 429844 [startup+1170.12 s] Raw data (loadavg): 1.01 1.00 0.92 2/57 8957 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 129339 0 0 0 116254 433 0 0 25 0 1 0 1797100195 437993472 103469 4294967295 134512640 135094434 3221224432 3221223044 134563089 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106932 103469 145 145 0 106787 0 [pid=8902] vsize: 427728 Current children cumulated CPU time (s) 1166.88 Current children cumulated vsize (Kb) 429852 [startup+1180.12 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 8959 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 129343 0 0 0 117254 433 0 0 25 0 1 0 1797100195 438009856 103473 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106936 103473 145 145 0 106791 0 [pid=8902] vsize: 427744 Current children cumulated CPU time (s) 1176.88 Current children cumulated vsize (Kb) 429868 [startup+1190.12 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 8959 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 129349 0 0 0 118254 433 0 0 25 0 1 0 1797100195 438034432 103479 4294967295 134512640 135094434 3221224432 3221223076 134558040 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106942 103479 145 145 0 106797 0 [pid=8902] vsize: 427768 Current children cumulated CPU time (s) 1186.88 Current children cumulated vsize (Kb) 429892 [startup+1200.12 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 8959 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 129355 0 0 0 119254 433 0 0 25 0 1 0 1797100195 438059008 103485 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106948 103485 145 145 0 106803 0 [pid=8902] vsize: 427792 Current children cumulated CPU time (s) 1196.88 Current children cumulated vsize (Kb) 429916 [startup+1210.12 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 8959 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 129370 0 0 0 120254 433 0 0 25 0 1 0 1797100195 438116352 103500 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106962 103500 145 145 0 106817 0 [pid=8902] vsize: 427848 Current children cumulated CPU time (s) 1206.88 Current children cumulated vsize (Kb) 429972 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.12 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 8959 Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8898/statm): 531 226 485 147 0 384 0 [pid=8898] vsize: 2124 Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 129370 0 0 0 120254 433 0 0 25 0 1 0 1797100195 438116352 103500 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8902/statm): 106962 103500 145 145 0 106817 0 [pid=8902] vsize: 427848 Current children cumulated CPU time (s) 1206.88 Current children cumulated vsize (Kb) 429972 Sending SIGTERM to -8898 Sleeping 2 seconds One traced child (pid=8898) ended because it received signal 15 (SIGTERM) One traced child (pid=8902) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.51 CPU time (s): 1207.21 CPU user time (s): 1202.65 CPU system time (s): 4.56531 CPU usage (%): 99.7274 Max. virtual memory (cumulated for all children) (Kb): 429972
ERROR: no interpretation found !