Name | mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-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.22 |
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 wulflinc27 THE 2005-09-19 03:35:03 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2908 boxname=wulflinc27 idbench=564 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 38504d32a17a57a658eee171614b901e /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-fast0507.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-fast0507.opb IDLAUNCH: 2908 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 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 : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 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: 874204 kB Buffers: 37236 kB Cached: 90520 kB SwapCached: 764 kB Active: 80920 kB Inactive: 49460 kB HighTotal: 131008 kB HighFree: 37856 kB LowTotal: 903652 kB LowFree: 836348 kB SwapTotal: 2097892 kB SwapFree: 2096616 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5728 kB Slab: 24404 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-19 03:55:14 (client local time) WITH STATUS 10 IN 1207.18 SECONDS stats: 2908 7 1207.18 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-wulflinc27-2908-564-3-0-15386.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/15423/stat): 15423 (minisat+_script) R 15422 15423 28974 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1846681004 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/15423/statm): 174 3 169 147 0 27 0 [pid=15423] 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=15424 New process pid=15425 New process pid=15426 execve syscall for /bin/sed executable One traced child (pid=15425) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=15426) exited with status: 0 One traced child (pid=15424) exited with status: 0 New process pid=15427 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-fast0507.opb [startup+10.0031 s] Raw data (loadavg): 0.93 0.96 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 16435 0 0 0 885 65 0 0 25 0 1 0 1846681009 55410688 11906 4294967295 134512640 135094434 3221224432 3221222128 134519836 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 13528 11913 145 145 0 13383 0 [pid=15427] vsize: 54112 Current children cumulated CPU time (s) 9.51 Current children cumulated vsize (Kb) 56236 [startup+20.0049 s] Raw data (loadavg): 0.94 0.96 0.95 1/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) T 15423 15423 28974 0 -1 0 56273 0 0 0 1688 182 0 0 23 0 1 0 1846681009 186327040 41857 4294967295 134512640 135094434 3221224432 3221221964 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/15427/statm): 45490 41857 145 145 0 45345 0 [pid=15427] vsize: 181960 Current children cumulated CPU time (s) 18.71 Current children cumulated vsize (Kb) 184084 [startup+30.0057 s] Raw data (loadavg): 0.95 0.96 0.95 1/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) T 15423 15423 28974 0 -1 0 98279 0 0 0 2489 303 0 0 24 0 1 0 1846681009 333815808 73317 4294967295 134512640 135094434 3221224432 3221220508 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/15427/statm): 81498 73317 145 145 0 81353 0 [pid=15427] vsize: 325992 Current children cumulated CPU time (s) 27.93 Current children cumulated vsize (Kb) 328116 [startup+40.0076 s] Raw data (loadavg): 0.96 0.96 0.95 1/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) T 15423 15423 28974 0 -1 0 114713 0 0 0 3380 361 0 0 24 0 1 0 1846681009 375799808 88843 4294967295 134512640 135094434 3221224432 3221216092 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/15427/statm): 91748 88843 145 145 0 91603 0 [pid=15427] vsize: 366992 Current children cumulated CPU time (s) 37.42 Current children cumulated vsize (Kb) 369116 [startup+50.0084 s] Raw data (loadavg): 0.96 0.96 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 126981 0 0 0 4264 416 0 0 25 0 1 0 1846681009 428355584 101111 4294967295 134512640 135094434 3221224432 3221223136 134559007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15427/statm): 104579 101111 145 145 0 104434 0 [pid=15427] vsize: 418316 Current children cumulated CPU time (s) 46.81 Current children cumulated vsize (Kb) 420440 [startup+60.0092 s] Raw data (loadavg): 0.97 0.96 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 126990 0 0 0 5262 417 0 0 25 0 1 0 1846681009 428392448 101120 4294967295 134512640 135094434 3221224432 3221223092 134553530 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 104588 101120 145 145 0 104443 0 [pid=15427] vsize: 418352 Current children cumulated CPU time (s) 56.8 Current children cumulated vsize (Kb) 420476 [startup+70.01 s] Raw data (loadavg): 0.97 0.96 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 127009 0 0 0 6262 417 0 0 25 0 1 0 1846681009 428470272 101139 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 104607 101139 145 145 0 104462 0 [pid=15427] vsize: 418428 Current children cumulated CPU time (s) 66.8 Current children cumulated vsize (Kb) 420552 [startup+80.0109 s] Raw data (loadavg): 0.98 0.96 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 127066 0 0 0 7262 417 0 0 25 0 1 0 1846681009 428703744 101196 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 104664 101196 145 145 0 104519 0 [pid=15427] vsize: 418656 Current children cumulated CPU time (s) 76.8 Current children cumulated vsize (Kb) 420780 [startup+90.0117 s] Raw data (loadavg): 0.98 0.96 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 127547 0 0 0 8255 420 0 0 25 0 1 0 1846681009 430673920 101677 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105145 101677 145 145 0 105000 0 [pid=15427] vsize: 420580 Current children cumulated CPU time (s) 86.76 Current children cumulated vsize (Kb) 422704 [startup+100.013 s] Raw data (loadavg): 0.98 0.96 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 127744 0 0 0 9252 422 0 0 25 0 1 0 1846681009 431714304 101874 4294967295 134512640 135094434 3221224432 3221223072 134562057 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105399 101874 145 145 0 105254 0 [pid=15427] vsize: 421596 Current children cumulated CPU time (s) 96.75 Current children cumulated vsize (Kb) 423720 [startup+110.014 s] Raw data (loadavg): 0.98 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 127831 0 0 0 10251 423 0 0 25 0 1 0 1846681009 431996928 101961 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105468 101961 145 145 0 105323 0 [pid=15427] vsize: 421872 Current children cumulated CPU time (s) 106.75 Current children cumulated vsize (Kb) 423996 [startup+120.015 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 127889 0 0 0 11251 424 0 0 25 0 1 0 1846681009 432234496 102019 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105526 102019 145 145 0 105381 0 [pid=15427] vsize: 422104 Current children cumulated CPU time (s) 116.76 Current children cumulated vsize (Kb) 424228 [startup+130.016 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 127935 0 0 0 12250 424 0 0 25 0 1 0 1846681009 432418816 102065 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105571 102065 145 145 0 105426 0 [pid=15427] vsize: 422284 Current children cumulated CPU time (s) 126.75 Current children cumulated vsize (Kb) 424408 [startup+140.018 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 127978 0 0 0 13250 424 0 0 25 0 1 0 1846681009 432529408 102108 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105598 102108 145 145 0 105453 0 [pid=15427] vsize: 422392 Current children cumulated CPU time (s) 136.75 Current children cumulated vsize (Kb) 424516 [startup+150.019 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128007 0 0 0 14250 424 0 0 25 0 1 0 1846681009 432631808 102137 4294967295 134512640 135094434 3221224432 3221223088 134557774 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105623 102137 145 145 0 105478 0 [pid=15427] vsize: 422492 Current children cumulated CPU time (s) 146.75 Current children cumulated vsize (Kb) 424616 [startup+160.018 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128029 0 0 0 15249 425 0 0 25 0 1 0 1846681009 432705536 102159 4294967295 134512640 135094434 3221224432 3221223088 134558398 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105641 102159 145 145 0 105496 0 [pid=15427] vsize: 422564 Current children cumulated CPU time (s) 156.75 Current children cumulated vsize (Kb) 424688 [startup+170.02 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128043 0 0 0 16249 425 0 0 25 0 1 0 1846681009 432762880 102173 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105655 102173 145 145 0 105510 0 [pid=15427] vsize: 422620 Current children cumulated CPU time (s) 166.75 Current children cumulated vsize (Kb) 424744 [startup+180.021 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128056 0 0 0 17249 425 0 0 25 0 1 0 1846681009 432812032 102186 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105667 102186 145 145 0 105522 0 [pid=15427] vsize: 422668 Current children cumulated CPU time (s) 176.75 Current children cumulated vsize (Kb) 424792 [startup+190.022 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128065 0 0 0 18249 425 0 0 25 0 1 0 1846681009 432848896 102195 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105676 102195 145 145 0 105531 0 [pid=15427] vsize: 422704 Current children cumulated CPU time (s) 186.75 Current children cumulated vsize (Kb) 424828 [startup+200.023 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128081 0 0 0 19249 425 0 0 25 0 1 0 1846681009 432943104 102211 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105699 102211 145 145 0 105554 0 [pid=15427] vsize: 422796 Current children cumulated CPU time (s) 196.75 Current children cumulated vsize (Kb) 424920 [startup+210.024 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128081 0 0 0 20249 425 0 0 25 0 1 0 1846681009 432943104 102211 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105699 102211 145 145 0 105554 0 [pid=15427] vsize: 422796 Current children cumulated CPU time (s) 206.75 Current children cumulated vsize (Kb) 424920 [startup+220.024 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128088 0 0 0 21249 426 0 0 25 0 1 0 1846681009 432967680 102218 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105705 102218 145 145 0 105560 0 [pid=15427] vsize: 422820 Current children cumulated CPU time (s) 216.76 Current children cumulated vsize (Kb) 424944 [startup+230.025 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128097 0 0 0 22249 426 0 0 25 0 1 0 1846681009 432988160 102227 4294967295 134512640 135094434 3221224432 3221223088 134561505 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15427/statm): 105710 102227 145 145 0 105565 0 [pid=15427] vsize: 422840 Current children cumulated CPU time (s) 226.76 Current children cumulated vsize (Kb) 424964 [startup+240.027 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128102 0 0 0 23249 426 0 0 25 0 1 0 1846681009 433008640 102232 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105715 102232 145 145 0 105570 0 [pid=15427] vsize: 422860 Current children cumulated CPU time (s) 236.76 Current children cumulated vsize (Kb) 424984 [startup+250.028 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128110 0 0 0 24249 426 0 0 25 0 1 0 1846681009 433037312 102240 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105722 102240 145 145 0 105577 0 [pid=15427] vsize: 422888 Current children cumulated CPU time (s) 246.76 Current children cumulated vsize (Kb) 425012 [startup+260.029 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128114 0 0 0 25249 426 0 0 25 0 1 0 1846681009 433053696 102244 4294967295 134512640 135094434 3221224432 3221223072 134562092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105726 102244 145 145 0 105581 0 [pid=15427] vsize: 422904 Current children cumulated CPU time (s) 256.76 Current children cumulated vsize (Kb) 425028 [startup+270.031 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128125 0 0 0 26250 426 0 0 25 0 1 0 1846681009 433078272 102255 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15427/statm): 105732 102255 145 145 0 105587 0 [pid=15427] vsize: 422928 Current children cumulated CPU time (s) 266.77 Current children cumulated vsize (Kb) 425052 [startup+280.031 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128130 0 0 0 27249 426 0 0 25 0 1 0 1846681009 433098752 102260 4294967295 134512640 135094434 3221224432 3221223044 134563124 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105737 102260 145 145 0 105592 0 [pid=15427] vsize: 422948 Current children cumulated CPU time (s) 276.76 Current children cumulated vsize (Kb) 425072 [startup+290.033 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128132 0 0 0 28249 426 0 0 25 0 1 0 1846681009 433106944 102262 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105739 102262 145 145 0 105594 0 [pid=15427] vsize: 422956 Current children cumulated CPU time (s) 286.76 Current children cumulated vsize (Kb) 425080 [startup+300.034 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128134 0 0 0 29249 426 0 0 25 0 1 0 1846681009 433115136 102264 4294967295 134512640 135094434 3221224432 3221223072 134562128 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105741 102264 145 145 0 105596 0 [pid=15427] vsize: 422964 Current children cumulated CPU time (s) 296.76 Current children cumulated vsize (Kb) 425088 [startup+310.036 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128141 0 0 0 30249 426 0 0 25 0 1 0 1846681009 433135616 102271 4294967295 134512640 135094434 3221224432 3221223152 134561655 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105746 102271 145 145 0 105601 0 [pid=15427] vsize: 422984 Current children cumulated CPU time (s) 306.76 Current children cumulated vsize (Kb) 425108 [startup+320.037 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128146 0 0 0 31249 426 0 0 25 0 1 0 1846681009 433147904 102276 4294967295 134512640 135094434 3221224432 3221223044 134563124 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105749 102276 145 145 0 105604 0 [pid=15427] vsize: 422996 Current children cumulated CPU time (s) 316.76 Current children cumulated vsize (Kb) 425120 [startup+330.038 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128150 0 0 0 32250 426 0 0 25 0 1 0 1846681009 433164288 102280 4294967295 134512640 135094434 3221224432 3221223072 134561792 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105753 102280 145 145 0 105608 0 [pid=15427] vsize: 423012 Current children cumulated CPU time (s) 326.77 Current children cumulated vsize (Kb) 425136 [startup+340.039 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128153 0 0 0 33250 426 0 0 25 0 1 0 1846681009 433172480 102283 4294967295 134512640 135094434 3221224432 3221223088 134561508 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105755 102283 145 145 0 105610 0 [pid=15427] vsize: 423020 Current children cumulated CPU time (s) 336.77 Current children cumulated vsize (Kb) 425144 [startup+350.04 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128156 0 0 0 34250 427 0 0 25 0 1 0 1846681009 433184768 102286 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105758 102286 145 145 0 105613 0 [pid=15427] vsize: 423032 Current children cumulated CPU time (s) 346.78 Current children cumulated vsize (Kb) 425156 [startup+360.041 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128159 0 0 0 35250 427 0 0 25 0 1 0 1846681009 433197056 102289 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105761 102289 145 145 0 105616 0 [pid=15427] vsize: 423044 Current children cumulated CPU time (s) 356.78 Current children cumulated vsize (Kb) 425168 [startup+370.042 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128167 0 0 0 36250 427 0 0 25 0 1 0 1846681009 433225728 102297 4294967295 134512640 135094434 3221224432 3221223088 134550399 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105768 102297 145 145 0 105623 0 [pid=15427] vsize: 423072 Current children cumulated CPU time (s) 366.78 Current children cumulated vsize (Kb) 425196 [startup+380.043 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128169 0 0 0 37250 427 0 0 25 0 1 0 1846681009 433233920 102299 4294967295 134512640 135094434 3221224432 3221223088 134557829 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105770 102299 145 145 0 105625 0 [pid=15427] vsize: 423080 Current children cumulated CPU time (s) 376.78 Current children cumulated vsize (Kb) 425204 [startup+390.043 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128173 0 0 0 38251 427 0 0 25 0 1 0 1846681009 433238016 102303 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105771 102303 145 145 0 105626 0 [pid=15427] vsize: 423084 Current children cumulated CPU time (s) 386.79 Current children cumulated vsize (Kb) 425208 [startup+400.044 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128175 0 0 0 39251 427 0 0 25 0 1 0 1846681009 433246208 102305 4294967295 134512640 135094434 3221224432 3221223044 134563069 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105773 102305 145 145 0 105628 0 [pid=15427] vsize: 423092 Current children cumulated CPU time (s) 396.79 Current children cumulated vsize (Kb) 425216 [startup+410.045 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128178 0 0 0 40251 427 0 0 25 0 1 0 1846681009 433254400 102308 4294967295 134512640 135094434 3221224432 3221223084 134561534 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105775 102308 145 145 0 105630 0 [pid=15427] vsize: 423100 Current children cumulated CPU time (s) 406.79 Current children cumulated vsize (Kb) 425224 [startup+420.046 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128180 0 0 0 41251 427 0 0 25 0 1 0 1846681009 433262592 102310 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105777 102310 145 145 0 105632 0 [pid=15427] vsize: 423108 Current children cumulated CPU time (s) 416.79 Current children cumulated vsize (Kb) 425232 [startup+430.047 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128183 0 0 0 42251 427 0 0 25 0 1 0 1846681009 433274880 102313 4294967295 134512640 135094434 3221224432 3221223136 134554553 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105780 102313 145 145 0 105635 0 [pid=15427] vsize: 423120 Current children cumulated CPU time (s) 426.79 Current children cumulated vsize (Kb) 425244 [startup+440.049 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128187 0 0 0 43252 427 0 0 25 0 1 0 1846681009 433291264 102317 4294967295 134512640 135094434 3221224432 3221223044 134563041 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105784 102317 145 145 0 105639 0 [pid=15427] vsize: 423136 Current children cumulated CPU time (s) 436.8 Current children cumulated vsize (Kb) 425260 [startup+450.049 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128193 0 0 0 44252 427 0 0 25 0 1 0 1846681009 433311744 102323 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105789 102323 145 145 0 105644 0 [pid=15427] vsize: 423156 Current children cumulated CPU time (s) 446.8 Current children cumulated vsize (Kb) 425280 [startup+460.05 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128215 0 0 0 45252 427 0 0 25 0 1 0 1846681009 433446912 102345 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105822 102345 145 145 0 105677 0 [pid=15427] vsize: 423288 Current children cumulated CPU time (s) 456.8 Current children cumulated vsize (Kb) 425412 [startup+470.052 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128217 0 0 0 46251 428 0 0 25 0 1 0 1846681009 433451008 102347 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105823 102347 145 145 0 105678 0 [pid=15427] vsize: 423292 Current children cumulated CPU time (s) 466.8 Current children cumulated vsize (Kb) 425416 [startup+480.053 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128219 0 0 0 47250 429 0 0 25 0 1 0 1846681009 433459200 102349 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105825 102349 145 145 0 105680 0 [pid=15427] vsize: 423300 Current children cumulated CPU time (s) 476.8 Current children cumulated vsize (Kb) 425424 [startup+490.055 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128229 0 0 0 48250 429 0 0 25 0 1 0 1846681009 433496064 102359 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105834 102359 145 145 0 105689 0 [pid=15427] vsize: 423336 Current children cumulated CPU time (s) 486.8 Current children cumulated vsize (Kb) 425460 [startup+500.056 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128236 0 0 0 49250 430 0 0 25 0 1 0 1846681009 433524736 102366 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105841 102366 145 145 0 105696 0 [pid=15427] vsize: 423364 Current children cumulated CPU time (s) 496.81 Current children cumulated vsize (Kb) 425488 [startup+510.056 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128247 0 0 0 50250 430 0 0 25 0 1 0 1846681009 433565696 102377 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105851 102377 145 145 0 105706 0 [pid=15427] vsize: 423404 Current children cumulated CPU time (s) 506.81 Current children cumulated vsize (Kb) 425528 [startup+520.058 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128254 0 0 0 51250 430 0 0 25 0 1 0 1846681009 433594368 102384 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105858 102384 145 145 0 105713 0 [pid=15427] vsize: 423432 Current children cumulated CPU time (s) 516.81 Current children cumulated vsize (Kb) 425556 [startup+530.059 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128264 0 0 0 52250 430 0 0 25 0 1 0 1846681009 433631232 102394 4294967295 134512640 135094434 3221224432 3221223184 134559282 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105867 102394 145 145 0 105722 0 [pid=15427] vsize: 423468 Current children cumulated CPU time (s) 526.81 Current children cumulated vsize (Kb) 425592 [startup+540.061 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128323 0 0 0 53249 431 0 0 25 0 1 0 1846681009 433831936 102453 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105916 102453 145 145 0 105771 0 [pid=15427] vsize: 423664 Current children cumulated CPU time (s) 536.81 Current children cumulated vsize (Kb) 425788 [startup+550.063 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128326 0 0 0 54249 431 0 0 25 0 1 0 1846681009 433844224 102456 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105919 102456 145 145 0 105774 0 [pid=15427] vsize: 423676 Current children cumulated CPU time (s) 546.81 Current children cumulated vsize (Kb) 425800 [startup+560.064 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128329 0 0 0 55249 431 0 0 25 0 1 0 1846681009 433856512 102459 4294967295 134512640 135094434 3221224432 3221223044 134563094 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105922 102459 145 145 0 105777 0 [pid=15427] vsize: 423688 Current children cumulated CPU time (s) 556.81 Current children cumulated vsize (Kb) 425812 [startup+570.064 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128334 0 0 0 56249 431 0 0 25 0 1 0 1846681009 433872896 102464 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105926 102464 145 145 0 105781 0 [pid=15427] vsize: 423704 Current children cumulated CPU time (s) 566.81 Current children cumulated vsize (Kb) 425828 [startup+580.065 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128341 0 0 0 57249 432 0 0 25 0 1 0 1846681009 433901568 102471 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105933 102471 145 145 0 105788 0 [pid=15427] vsize: 423732 Current children cumulated CPU time (s) 576.82 Current children cumulated vsize (Kb) 425856 [startup+590.067 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128348 0 0 0 58249 432 0 0 25 0 1 0 1846681009 433930240 102478 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105940 102478 145 145 0 105795 0 [pid=15427] vsize: 423760 Current children cumulated CPU time (s) 586.82 Current children cumulated vsize (Kb) 425884 [startup+600.068 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128357 0 0 0 59249 432 0 0 25 0 1 0 1846681009 433958912 102487 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105947 102487 145 145 0 105802 0 [pid=15427] vsize: 423788 Current children cumulated CPU time (s) 596.82 Current children cumulated vsize (Kb) 425912 [startup+610.069 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128385 0 0 0 60248 432 0 0 25 0 1 0 1846681009 434073600 102515 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105975 102515 145 145 0 105830 0 [pid=15427] vsize: 423900 Current children cumulated CPU time (s) 606.81 Current children cumulated vsize (Kb) 426024 [startup+620.071 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128390 0 0 0 61248 432 0 0 25 0 1 0 1846681009 434089984 102520 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105979 102520 145 145 0 105834 0 [pid=15427] vsize: 423916 Current children cumulated CPU time (s) 616.81 Current children cumulated vsize (Kb) 426040 [startup+630.071 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128398 0 0 0 62249 432 0 0 25 0 1 0 1846681009 434122752 102528 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105987 102528 145 145 0 105842 0 [pid=15427] vsize: 423948 Current children cumulated CPU time (s) 626.82 Current children cumulated vsize (Kb) 426072 [startup+640.073 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128409 0 0 0 63249 433 0 0 25 0 1 0 1846681009 434167808 102539 4294967295 134512640 135094434 3221224432 3221223084 134558036 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 105998 102539 145 145 0 105853 0 [pid=15427] vsize: 423992 Current children cumulated CPU time (s) 636.83 Current children cumulated vsize (Kb) 426116 [startup+650.074 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128416 0 0 0 64249 433 0 0 25 0 1 0 1846681009 434192384 102546 4294967295 134512640 135094434 3221224432 3221223072 134562131 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106004 102546 145 145 0 105859 0 [pid=15427] vsize: 424016 Current children cumulated CPU time (s) 646.83 Current children cumulated vsize (Kb) 426140 [startup+660.075 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128432 0 0 0 65249 433 0 0 25 0 1 0 1846681009 434257920 102562 4294967295 134512640 135094434 3221224432 3221223044 134563061 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106020 102562 145 145 0 105875 0 [pid=15427] vsize: 424080 Current children cumulated CPU time (s) 656.83 Current children cumulated vsize (Kb) 426204 [startup+670.076 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128498 0 0 0 66248 433 0 0 25 0 1 0 1846681009 434520064 102628 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15427/statm): 106084 102628 145 145 0 105939 0 [pid=15427] vsize: 424336 Current children cumulated CPU time (s) 666.82 Current children cumulated vsize (Kb) 426460 [startup+680.076 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128505 0 0 0 67247 434 0 0 25 0 1 0 1846681009 434548736 102635 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106091 102635 145 145 0 105946 0 [pid=15427] vsize: 424364 Current children cumulated CPU time (s) 676.82 Current children cumulated vsize (Kb) 426488 [startup+690.077 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128514 0 0 0 68247 434 0 0 25 0 1 0 1846681009 434573312 102644 4294967295 134512640 135094434 3221224432 3221223072 134562057 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106097 102644 145 145 0 105952 0 [pid=15427] vsize: 424388 Current children cumulated CPU time (s) 686.82 Current children cumulated vsize (Kb) 426512 [startup+700.078 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128517 0 0 0 69247 434 0 0 25 0 1 0 1846681009 434585600 102647 4294967295 134512640 135094434 3221224432 3221223088 134561502 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106100 102647 145 145 0 105955 0 [pid=15427] vsize: 424400 Current children cumulated CPU time (s) 696.82 Current children cumulated vsize (Kb) 426524 [startup+710.079 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128519 0 0 0 70247 434 0 0 25 0 1 0 1846681009 434593792 102649 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106102 102649 145 145 0 105957 0 [pid=15427] vsize: 424408 Current children cumulated CPU time (s) 706.82 Current children cumulated vsize (Kb) 426532 [startup+720.08 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128523 0 0 0 71248 434 0 0 25 0 1 0 1846681009 434601984 102653 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106104 102653 145 145 0 105959 0 [pid=15427] vsize: 424416 Current children cumulated CPU time (s) 716.83 Current children cumulated vsize (Kb) 426540 [startup+730.081 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128524 0 0 0 72248 434 0 0 25 0 1 0 1846681009 434606080 102654 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106105 102654 145 145 0 105960 0 [pid=15427] vsize: 424420 Current children cumulated CPU time (s) 726.83 Current children cumulated vsize (Kb) 426544 [startup+740.081 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128533 0 0 0 73248 434 0 0 25 0 1 0 1846681009 434642944 102663 4294967295 134512640 135094434 3221224432 3221223044 134563059 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106114 102663 145 145 0 105969 0 [pid=15427] vsize: 424456 Current children cumulated CPU time (s) 736.83 Current children cumulated vsize (Kb) 426580 [startup+750.082 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128536 0 0 0 74248 434 0 0 25 0 1 0 1846681009 434655232 102666 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106117 102666 145 145 0 105972 0 [pid=15427] vsize: 424468 Current children cumulated CPU time (s) 746.83 Current children cumulated vsize (Kb) 426592 [startup+760.083 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128538 0 0 0 75248 434 0 0 25 0 1 0 1846681009 434663424 102668 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106119 102668 145 145 0 105974 0 [pid=15427] vsize: 424476 Current children cumulated CPU time (s) 756.83 Current children cumulated vsize (Kb) 426600 [startup+770.085 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128544 0 0 0 76248 434 0 0 25 0 1 0 1846681009 434683904 102674 4294967295 134512640 135094434 3221224432 3221223088 134557875 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106124 102674 145 145 0 105979 0 [pid=15427] vsize: 424496 Current children cumulated CPU time (s) 766.83 Current children cumulated vsize (Kb) 426620 [startup+780.086 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128601 0 0 0 77248 435 0 0 25 0 1 0 1846681009 434913280 102731 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106180 102731 145 145 0 106035 0 [pid=15427] vsize: 424720 Current children cumulated CPU time (s) 776.84 Current children cumulated vsize (Kb) 426844 [startup+790.087 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128660 0 0 0 78247 435 0 0 25 0 1 0 1846681009 435150848 102790 4294967295 134512640 135094434 3221224432 3221223120 134554733 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106238 102790 145 145 0 106093 0 [pid=15427] vsize: 424952 Current children cumulated CPU time (s) 786.83 Current children cumulated vsize (Kb) 427076 [startup+800.088 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128667 0 0 0 79247 435 0 0 25 0 1 0 1846681009 435179520 102797 4294967295 134512640 135094434 3221224432 3221223088 134561463 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106245 102797 145 145 0 106100 0 [pid=15427] vsize: 424980 Current children cumulated CPU time (s) 796.83 Current children cumulated vsize (Kb) 427104 [startup+810.089 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128678 0 0 0 80247 436 0 0 25 0 1 0 1846681009 435224576 102808 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106256 102808 145 145 0 106111 0 [pid=15427] vsize: 425024 Current children cumulated CPU time (s) 806.84 Current children cumulated vsize (Kb) 427148 [startup+820.09 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128717 0 0 0 81247 436 0 0 25 0 1 0 1846681009 435511296 102847 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106326 102847 145 145 0 106181 0 [pid=15427] vsize: 425304 Current children cumulated CPU time (s) 816.84 Current children cumulated vsize (Kb) 427428 [startup+830.091 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128717 0 0 0 82247 436 0 0 25 0 1 0 1846681009 435511296 102847 4294967295 134512640 135094434 3221224432 3221223088 134561717 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106326 102847 145 145 0 106181 0 [pid=15427] vsize: 425304 Current children cumulated CPU time (s) 826.84 Current children cumulated vsize (Kb) 427428 [startup+840.092 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128717 0 0 0 83248 436 0 0 25 0 1 0 1846681009 435511296 102847 4294967295 134512640 135094434 3221224432 3221223088 134550375 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106326 102847 145 145 0 106181 0 [pid=15427] vsize: 425304 Current children cumulated CPU time (s) 836.85 Current children cumulated vsize (Kb) 427428 [startup+850.092 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128718 0 0 0 84248 436 0 0 25 0 1 0 1846681009 435511296 102848 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106326 102848 145 145 0 106181 0 [pid=15427] vsize: 425304 Current children cumulated CPU time (s) 846.85 Current children cumulated vsize (Kb) 427428 [startup+860.093 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128718 0 0 0 85248 436 0 0 25 0 1 0 1846681009 435511296 102848 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106326 102848 145 145 0 106181 0 [pid=15427] vsize: 425304 Current children cumulated CPU time (s) 856.85 Current children cumulated vsize (Kb) 427428 [startup+870.095 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128719 0 0 0 86248 436 0 0 25 0 1 0 1846681009 435511296 102849 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106326 102849 145 145 0 106181 0 [pid=15427] vsize: 425304 Current children cumulated CPU time (s) 866.85 Current children cumulated vsize (Kb) 427428 [startup+880.096 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128720 0 0 0 87248 436 0 0 25 0 1 0 1846681009 435511296 102850 4294967295 134512640 135094434 3221224432 3221223088 134557795 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106326 102850 145 145 0 106181 0 [pid=15427] vsize: 425304 Current children cumulated CPU time (s) 876.85 Current children cumulated vsize (Kb) 427428 [startup+890.097 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128721 0 0 0 88249 436 0 0 25 0 1 0 1846681009 435515392 102851 4294967295 134512640 135094434 3221224432 3221223044 134563104 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106327 102851 145 145 0 106182 0 [pid=15427] vsize: 425308 Current children cumulated CPU time (s) 886.86 Current children cumulated vsize (Kb) 427432 [startup+900.098 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128724 0 0 0 89249 436 0 0 25 0 1 0 1846681009 435527680 102854 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106330 102854 145 145 0 106185 0 [pid=15427] vsize: 425320 Current children cumulated CPU time (s) 896.86 Current children cumulated vsize (Kb) 427444 [startup+910.098 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128729 0 0 0 90249 436 0 0 25 0 1 0 1846681009 435548160 102859 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106335 102859 145 145 0 106190 0 [pid=15427] vsize: 425340 Current children cumulated CPU time (s) 906.86 Current children cumulated vsize (Kb) 427464 [startup+920.099 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128746 0 0 0 91249 436 0 0 25 0 1 0 1846681009 435613696 102876 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106351 102876 145 145 0 106206 0 [pid=15427] vsize: 425404 Current children cumulated CPU time (s) 916.86 Current children cumulated vsize (Kb) 427528 [startup+930.1 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128772 0 0 0 92249 437 0 0 25 0 1 0 1846681009 435720192 102902 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106377 102902 145 145 0 106232 0 [pid=15427] vsize: 425508 Current children cumulated CPU time (s) 926.87 Current children cumulated vsize (Kb) 427632 [startup+940.101 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128806 0 0 0 93248 437 0 0 25 0 1 0 1846681009 435855360 102936 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106410 102936 145 145 0 106265 0 [pid=15427] vsize: 425640 Current children cumulated CPU time (s) 936.86 Current children cumulated vsize (Kb) 427764 [startup+950.102 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128830 0 0 0 94248 437 0 0 25 0 1 0 1846681009 435949568 102960 4294967295 134512640 135094434 3221224432 3221223072 134562088 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106433 102960 145 145 0 106288 0 [pid=15427] vsize: 425732 Current children cumulated CPU time (s) 946.86 Current children cumulated vsize (Kb) 427856 [startup+960.103 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128854 0 0 0 95248 438 0 0 25 0 1 0 1846681009 436047872 102984 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106457 102984 145 145 0 106312 0 [pid=15427] vsize: 425828 Current children cumulated CPU time (s) 956.87 Current children cumulated vsize (Kb) 427952 [startup+970.104 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128873 0 0 0 96248 438 0 0 25 0 1 0 1846681009 436121600 103003 4294967295 134512640 135094434 3221224432 3221223044 134563039 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106475 103003 145 145 0 106330 0 [pid=15427] vsize: 425900 Current children cumulated CPU time (s) 966.87 Current children cumulated vsize (Kb) 428024 [startup+980.105 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128979 0 0 0 97245 439 0 0 25 0 1 0 1846681009 436547584 103109 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15427/statm): 106579 103109 145 145 0 106434 0 [pid=15427] vsize: 426316 Current children cumulated CPU time (s) 976.85 Current children cumulated vsize (Kb) 428440 [startup+990.106 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129069 0 0 0 98243 440 0 0 25 0 1 0 1846681009 436903936 103199 4294967295 134512640 135094434 3221224432 3221223088 134561463 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106666 103199 145 145 0 106521 0 [pid=15427] vsize: 426664 Current children cumulated CPU time (s) 986.84 Current children cumulated vsize (Kb) 428788 [startup+1000.11 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129084 0 0 0 99243 440 0 0 25 0 1 0 1846681009 436965376 103214 4294967295 134512640 135094434 3221224432 3221223064 134562981 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106681 103214 145 145 0 106536 0 [pid=15427] vsize: 426724 Current children cumulated CPU time (s) 996.84 Current children cumulated vsize (Kb) 428848 [startup+1010.11 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129090 0 0 0 100243 440 0 0 25 0 1 0 1846681009 436989952 103220 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106687 103220 145 145 0 106542 0 [pid=15427] vsize: 426748 Current children cumulated CPU time (s) 1006.84 Current children cumulated vsize (Kb) 428872 [startup+1020.11 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129106 0 0 0 101243 440 0 0 25 0 1 0 1846681009 437055488 103236 4294967295 134512640 135094434 3221224432 3221223088 134562165 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106703 103236 145 145 0 106558 0 [pid=15427] vsize: 426812 Current children cumulated CPU time (s) 1016.84 Current children cumulated vsize (Kb) 428936 [startup+1030.11 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129116 0 0 0 102243 440 0 0 25 0 1 0 1846681009 437092352 103246 4294967295 134512640 135094434 3221224432 3221223136 134554538 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106712 103246 145 145 0 106567 0 [pid=15427] vsize: 426848 Current children cumulated CPU time (s) 1026.84 Current children cumulated vsize (Kb) 428972 [startup+1040.11 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129137 0 0 0 103243 440 0 0 25 0 1 0 1846681009 437178368 103267 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106733 103267 145 145 0 106588 0 [pid=15427] vsize: 426932 Current children cumulated CPU time (s) 1036.84 Current children cumulated vsize (Kb) 429056 [startup+1050.11 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129174 0 0 0 104242 441 0 0 25 0 1 0 1846681009 437325824 103304 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106769 103304 145 145 0 106624 0 [pid=15427] vsize: 427076 Current children cumulated CPU time (s) 1046.84 Current children cumulated vsize (Kb) 429200 [startup+1060.11 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129202 0 0 0 105242 441 0 0 25 0 1 0 1846681009 437440512 103332 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106797 103332 145 145 0 106652 0 [pid=15427] vsize: 427188 Current children cumulated CPU time (s) 1056.84 Current children cumulated vsize (Kb) 429312 [startup+1070.11 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129221 0 0 0 106242 441 0 0 25 0 1 0 1846681009 437518336 103351 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106816 103351 145 145 0 106671 0 [pid=15427] vsize: 427264 Current children cumulated CPU time (s) 1066.84 Current children cumulated vsize (Kb) 429388 [startup+1080.11 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129238 0 0 0 107240 443 0 0 25 0 1 0 1846681009 437583872 103368 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106832 103368 145 145 0 106687 0 [pid=15427] vsize: 427328 Current children cumulated CPU time (s) 1076.84 Current children cumulated vsize (Kb) 429452 [startup+1090.11 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129253 0 0 0 108240 443 0 0 25 0 1 0 1846681009 437645312 103383 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106847 103383 145 145 0 106702 0 [pid=15427] vsize: 427388 Current children cumulated CPU time (s) 1086.84 Current children cumulated vsize (Kb) 429512 [startup+1100.11 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129265 0 0 0 109239 444 0 0 25 0 1 0 1846681009 437694464 103395 4294967295 134512640 135094434 3221224432 3221223044 134563087 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106859 103395 145 145 0 106714 0 [pid=15427] vsize: 427436 Current children cumulated CPU time (s) 1096.84 Current children cumulated vsize (Kb) 429560 [startup+1110.12 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129283 0 0 0 110239 444 0 0 25 0 1 0 1846681009 437764096 103413 4294967295 134512640 135094434 3221224432 3221223088 134557798 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106876 103413 145 145 0 106731 0 [pid=15427] vsize: 427504 Current children cumulated CPU time (s) 1106.84 Current children cumulated vsize (Kb) 429628 [startup+1120.12 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129302 0 0 0 111239 444 0 0 25 0 1 0 1846681009 437841920 103432 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106895 103432 145 145 0 106750 0 [pid=15427] vsize: 427580 Current children cumulated CPU time (s) 1116.84 Current children cumulated vsize (Kb) 429704 [startup+1130.12 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129319 0 0 0 112239 444 0 0 25 0 1 0 1846681009 437911552 103449 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106912 103449 145 145 0 106767 0 [pid=15427] vsize: 427648 Current children cumulated CPU time (s) 1126.84 Current children cumulated vsize (Kb) 429772 [startup+1140.12 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129330 0 0 0 113239 445 0 0 25 0 1 0 1846681009 437952512 103460 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106922 103460 145 145 0 106777 0 [pid=15427] vsize: 427688 Current children cumulated CPU time (s) 1136.85 Current children cumulated vsize (Kb) 429812 [startup+1150.12 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129337 0 0 0 114239 445 0 0 25 0 1 0 1846681009 437985280 103467 4294967295 134512640 135094434 3221224432 3221223084 134561527 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106930 103467 145 145 0 106785 0 [pid=15427] vsize: 427720 Current children cumulated CPU time (s) 1146.85 Current children cumulated vsize (Kb) 429844 [startup+1160.12 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129340 0 0 0 115239 445 0 0 25 0 1 0 1846681009 437997568 103470 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106933 103470 145 145 0 106788 0 [pid=15427] vsize: 427732 Current children cumulated CPU time (s) 1156.85 Current children cumulated vsize (Kb) 429856 [startup+1170.12 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129345 0 0 0 116239 445 0 0 25 0 1 0 1846681009 438018048 103475 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106938 103475 145 145 0 106793 0 [pid=15427] vsize: 427752 Current children cumulated CPU time (s) 1166.85 Current children cumulated vsize (Kb) 429876 [startup+1180.12 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129352 0 0 0 117239 445 0 0 25 0 1 0 1846681009 438046720 103482 4294967295 134512640 135094434 3221224432 3221223088 134561482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106945 103482 145 145 0 106800 0 [pid=15427] vsize: 427780 Current children cumulated CPU time (s) 1176.85 Current children cumulated vsize (Kb) 429904 [startup+1190.12 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129359 0 0 0 118239 445 0 0 25 0 1 0 1846681009 438071296 103489 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106951 103489 145 145 0 106806 0 [pid=15427] vsize: 427804 Current children cumulated CPU time (s) 1186.85 Current children cumulated vsize (Kb) 429928 [startup+1200.12 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129382 0 0 0 119238 446 0 0 25 0 1 0 1846681009 438165504 103512 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106974 103512 145 145 0 106829 0 [pid=15427] vsize: 427896 Current children cumulated CPU time (s) 1196.85 Current children cumulated vsize (Kb) 430020 [startup+1210.12 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129393 0 0 0 120238 446 0 0 25 0 1 0 1846681009 438210560 103523 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106985 103523 145 145 0 106840 0 [pid=15427] vsize: 427940 Current children cumulated CPU time (s) 1206.85 Current children cumulated vsize (Kb) 430064 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.12 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15427 Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15423/statm): 531 226 485 147 0 384 0 [pid=15423] vsize: 2124 Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129393 0 0 0 120238 446 0 0 25 0 1 0 1846681009 438210560 103523 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15427/statm): 106985 103523 145 145 0 106840 0 [pid=15427] vsize: 427940 Current children cumulated CPU time (s) 1206.85 Current children cumulated vsize (Kb) 430064 Sending SIGTERM to -15423 Sleeping 2 seconds One traced child (pid=15423) ended because it received signal 15 (SIGTERM) One traced child (pid=15427) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.51 CPU time (s): 1207.18 CPU user time (s): 1202.49 CPU system time (s): 4.69029 CPU usage (%): 99.7248 Max. virtual memory (cumulated for all children) (Kb): 430064
ERROR: no interpretation found !