Name | mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-fast0507.opb |
MD5SUM | 2854384016ebafb26c8bfb47f81aee87 |
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.18 |
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 wulflinc11 THE 2005-09-20 04:14:44 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3353 boxname=wulflinc11 idbench=1009 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 2854384016ebafb26c8bfb47f81aee87 /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-13-7-fast0507.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-13-7-fast0507.opb IDLAUNCH: 3353 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.028 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.028 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: 874688 kB Buffers: 25340 kB Cached: 107840 kB SwapCached: 916 kB Active: 37236 kB Inactive: 98536 kB HighTotal: 131008 kB HighFree: 22596 kB LowTotal: 903652 kB LowFree: 852092 kB SwapTotal: 2097136 kB SwapFree: 2095640 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5660 kB Slab: 18652 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-20 04:34:55 (client local time) WITH STATUS 10 IN 1207.2 SECONDS stats: 3353 7 1207.2 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-wulflinc11-3353-1009-3-0-32739.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/308/stat): 308 (minisat+_script) R 307 308 9854 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1797344601 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/308/statm): 174 3 169 147 0 27 0 [pid=308] 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=309 New process pid=310 New process pid=311 execve syscall for /bin/sed executable One traced child (pid=310) 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=311) exited with status: 0 One traced child (pid=309) exited with status: 0 New process pid=312 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-13-7-fast0507.opb [startup+10.0033 s] Raw data (loadavg): 0.93 0.97 0.94 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 16770 0 0 0 889 63 0 0 25 0 1 0 1797344606 55410688 12241 4294967295 134512640 135094434 3221224432 3221222128 134519913 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 13528 12241 145 145 0 13383 0 [pid=312] vsize: 54112 Current children cumulated CPU time (s) 9.53 Current children cumulated vsize (Kb) 56236 [startup+20.0051 s] Raw data (loadavg): 1.02 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) T 308 308 9854 0 -1 0 56800 0 0 0 1693 182 0 0 23 0 1 0 1797344606 187686912 42384 4294967295 134512640 135094434 3221224432 3221221292 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/312/statm): 45822 42384 145 145 0 45677 0 [pid=312] vsize: 183288 Current children cumulated CPU time (s) 18.76 Current children cumulated vsize (Kb) 185412 [startup+30.0058 s] Raw data (loadavg): 1.01 0.99 0.95 1/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) T 308 308 9854 0 -1 0 98834 0 0 0 2494 303 0 0 23 0 1 0 1797344606 335245312 73872 4294967295 134512640 135094434 3221224432 3221220508 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/312/statm): 81847 73872 145 145 0 81702 0 [pid=312] vsize: 327388 Current children cumulated CPU time (s) 27.98 Current children cumulated vsize (Kb) 329512 [startup+40.0066 s] Raw data (loadavg): 1.01 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 115785 0 0 0 3383 358 0 0 22 0 1 0 1797344606 379695104 89915 4294967295 134512640 135094434 3221224432 3221216480 134522806 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/312/statm): 92699 89915 145 145 0 92554 0 [pid=312] vsize: 370796 Current children cumulated CPU time (s) 37.42 Current children cumulated vsize (Kb) 372920 [startup+50.0084 s] Raw data (loadavg): 1.01 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 126981 0 0 0 4277 410 0 0 25 0 1 0 1797344606 428355584 101111 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 104579 101111 145 145 0 104434 0 [pid=312] vsize: 418316 Current children cumulated CPU time (s) 46.88 Current children cumulated vsize (Kb) 420440 [startup+60.0092 s] Raw data (loadavg): 1.01 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 126991 0 0 0 5278 410 0 0 25 0 1 0 1797344606 428396544 101121 4294967295 134512640 135094434 3221224432 3221223092 134553494 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 104589 101121 145 145 0 104444 0 [pid=312] vsize: 418356 Current children cumulated CPU time (s) 56.89 Current children cumulated vsize (Kb) 420480 [startup+70.01 s] Raw data (loadavg): 1.01 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 127009 0 0 0 6277 410 0 0 25 0 1 0 1797344606 428470272 101139 4294967295 134512640 135094434 3221224432 3221223108 134553436 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/312/statm): 104607 101139 145 145 0 104462 0 [pid=312] vsize: 418428 Current children cumulated CPU time (s) 66.88 Current children cumulated vsize (Kb) 420552 [startup+80.0118 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 127066 0 0 0 7275 411 0 0 25 0 1 0 1797344606 428703744 101196 4294967295 134512640 135094434 3221224432 3221223092 134553519 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 104664 101196 145 145 0 104519 0 [pid=312] vsize: 418656 Current children cumulated CPU time (s) 76.87 Current children cumulated vsize (Kb) 420780 [startup+90.0115 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 127547 0 0 0 8269 413 0 0 25 0 1 0 1797344606 430673920 101677 4294967295 134512640 135094434 3221224432 3221223092 134553494 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 105145 101677 145 145 0 105000 0 [pid=312] vsize: 420580 Current children cumulated CPU time (s) 86.83 Current children cumulated vsize (Kb) 422704 [startup+100.012 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 127744 0 0 0 9267 414 0 0 25 0 1 0 1797344606 431714304 101874 4294967295 134512640 135094434 3221224432 3221223152 134558439 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 105399 101874 145 145 0 105254 0 [pid=312] vsize: 421596 Current children cumulated CPU time (s) 96.82 Current children cumulated vsize (Kb) 423720 [startup+110.013 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 127831 0 0 0 10266 415 0 0 25 0 1 0 1797344606 431996928 101961 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 105468 101961 145 145 0 105323 0 [pid=312] vsize: 421872 Current children cumulated CPU time (s) 106.82 Current children cumulated vsize (Kb) 423996 [startup+120.015 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 127890 0 0 0 11264 416 0 0 25 0 1 0 1797344606 432238592 102020 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 105527 102020 145 145 0 105382 0 [pid=312] vsize: 422108 Current children cumulated CPU time (s) 116.81 Current children cumulated vsize (Kb) 424232 [startup+130.016 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 127936 0 0 0 12264 416 0 0 25 0 1 0 1797344606 432422912 102066 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/312/statm): 105572 102066 145 145 0 105427 0 [pid=312] vsize: 422288 Current children cumulated CPU time (s) 126.81 Current children cumulated vsize (Kb) 424412 [startup+140.016 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 127978 0 0 0 13262 417 0 0 25 0 1 0 1797344606 432529408 102108 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/312/statm): 105598 102108 145 145 0 105453 0 [pid=312] vsize: 422392 Current children cumulated CPU time (s) 136.8 Current children cumulated vsize (Kb) 424516 [startup+150.018 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128007 0 0 0 14261 418 0 0 25 0 1 0 1797344606 432631808 102137 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 105623 102137 145 145 0 105478 0 [pid=312] vsize: 422492 Current children cumulated CPU time (s) 146.8 Current children cumulated vsize (Kb) 424616 [startup+160.019 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128028 0 0 0 15261 418 0 0 25 0 1 0 1797344606 432701440 102158 4294967295 134512640 135094434 3221224432 3221223044 134563089 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 105640 102158 145 145 0 105495 0 [pid=312] vsize: 422560 Current children cumulated CPU time (s) 156.8 Current children cumulated vsize (Kb) 424684 [startup+170.021 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128043 0 0 0 16261 418 0 0 25 0 1 0 1797344606 432762880 102173 4294967295 134512640 135094434 3221224432 3221223104 134553523 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 105655 102173 145 145 0 105510 0 [pid=312] vsize: 422620 Current children cumulated CPU time (s) 166.8 Current children cumulated vsize (Kb) 424744 [startup+180.022 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128056 0 0 0 17261 418 0 0 25 0 1 0 1797344606 432812032 102186 4294967295 134512640 135094434 3221224432 3221223120 134554859 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 105667 102186 145 145 0 105522 0 [pid=312] vsize: 422668 Current children cumulated CPU time (s) 176.8 Current children cumulated vsize (Kb) 424792 [startup+190.022 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128065 0 0 0 18261 418 0 0 25 0 1 0 1797344606 432848896 102195 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 105676 102195 145 145 0 105531 0 [pid=312] vsize: 422704 Current children cumulated CPU time (s) 186.8 Current children cumulated vsize (Kb) 424828 [startup+200.023 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128081 0 0 0 19261 418 0 0 25 0 1 0 1797344606 432943104 102211 4294967295 134512640 135094434 3221224432 3221223072 134562057 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 105699 102211 145 145 0 105554 0 [pid=312] vsize: 422796 Current children cumulated CPU time (s) 196.8 Current children cumulated vsize (Kb) 424920 [startup+210.024 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128081 0 0 0 20261 418 0 0 25 0 1 0 1797344606 432943104 102211 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 105699 102211 145 145 0 105554 0 [pid=312] vsize: 422796 Current children cumulated CPU time (s) 206.8 Current children cumulated vsize (Kb) 424920 [startup+220.026 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128088 0 0 0 21261 418 0 0 25 0 1 0 1797344606 432967680 102218 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 105705 102218 145 145 0 105560 0 [pid=312] vsize: 422820 Current children cumulated CPU time (s) 216.8 Current children cumulated vsize (Kb) 424944 [startup+230.027 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128097 0 0 0 22261 418 0 0 25 0 1 0 1797344606 432988160 102227 4294967295 134512640 135094434 3221224432 3221223044 134562998 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 105710 102227 145 145 0 105565 0 [pid=312] vsize: 422840 Current children cumulated CPU time (s) 226.8 Current children cumulated vsize (Kb) 424964 [startup+240.026 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128102 0 0 0 23261 418 0 0 25 0 1 0 1797344606 433008640 102232 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 105715 102232 145 145 0 105570 0 [pid=312] vsize: 422860 Current children cumulated CPU time (s) 236.8 Current children cumulated vsize (Kb) 424984 [startup+250.027 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128110 0 0 0 24261 418 0 0 25 0 1 0 1797344606 433037312 102240 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 105722 102240 145 145 0 105577 0 [pid=312] vsize: 422888 Current children cumulated CPU time (s) 246.8 Current children cumulated vsize (Kb) 425012 [startup+260.028 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128114 0 0 0 25262 418 0 0 25 0 1 0 1797344606 433053696 102244 4294967295 134512640 135094434 3221224432 3221223044 134563059 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 105726 102244 145 145 0 105581 0 [pid=312] vsize: 422904 Current children cumulated CPU time (s) 256.81 Current children cumulated vsize (Kb) 425028 [startup+270.029 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128124 0 0 0 26262 418 0 0 25 0 1 0 1797344606 433074176 102254 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 105731 102254 145 145 0 105586 0 [pid=312] vsize: 422924 Current children cumulated CPU time (s) 266.81 Current children cumulated vsize (Kb) 425048 [startup+280.029 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128130 0 0 0 27262 418 0 0 25 0 1 0 1797344606 433098752 102260 4294967295 134512640 135094434 3221224432 3221223120 134554796 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 105737 102260 145 145 0 105592 0 [pid=312] vsize: 422948 Current children cumulated CPU time (s) 276.81 Current children cumulated vsize (Kb) 425072 [startup+290.03 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128132 0 0 0 28262 418 0 0 25 0 1 0 1797344606 433106944 102262 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 105739 102262 145 145 0 105594 0 [pid=312] vsize: 422956 Current children cumulated CPU time (s) 286.81 Current children cumulated vsize (Kb) 425080 [startup+300.031 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128134 0 0 0 29263 418 0 0 25 0 1 0 1797344606 433115136 102264 4294967295 134512640 135094434 3221224432 3221223072 134562128 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 105741 102264 145 145 0 105596 0 [pid=312] vsize: 422964 Current children cumulated CPU time (s) 296.82 Current children cumulated vsize (Kb) 425088 [startup+310.032 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128141 0 0 0 30263 418 0 0 25 0 1 0 1797344606 433135616 102271 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 105746 102271 145 145 0 105601 0 [pid=312] vsize: 422984 Current children cumulated CPU time (s) 306.82 Current children cumulated vsize (Kb) 425108 [startup+320.034 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128146 0 0 0 31263 418 0 0 25 0 1 0 1797344606 433147904 102276 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 105749 102276 145 145 0 105604 0 [pid=312] vsize: 422996 Current children cumulated CPU time (s) 316.82 Current children cumulated vsize (Kb) 425120 [startup+330.034 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128150 0 0 0 32263 418 0 0 25 0 1 0 1797344606 433164288 102280 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 105753 102280 145 145 0 105608 0 [pid=312] vsize: 423012 Current children cumulated CPU time (s) 326.82 Current children cumulated vsize (Kb) 425136 [startup+340.035 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128153 0 0 0 33263 418 0 0 25 0 1 0 1797344606 433172480 102283 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 105755 102283 145 145 0 105610 0 [pid=312] vsize: 423020 Current children cumulated CPU time (s) 336.82 Current children cumulated vsize (Kb) 425144 [startup+350.037 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128156 0 0 0 34263 418 0 0 25 0 1 0 1797344606 433184768 102286 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 105758 102286 145 145 0 105613 0 [pid=312] vsize: 423032 Current children cumulated CPU time (s) 346.82 Current children cumulated vsize (Kb) 425156 [startup+360.038 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128159 0 0 0 35264 418 0 0 25 0 1 0 1797344606 433197056 102289 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 105761 102289 145 145 0 105616 0 [pid=312] vsize: 423044 Current children cumulated CPU time (s) 356.83 Current children cumulated vsize (Kb) 425168 [startup+370.039 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128167 0 0 0 36264 418 0 0 25 0 1 0 1797344606 433225728 102297 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 105768 102297 145 145 0 105623 0 [pid=312] vsize: 423072 Current children cumulated CPU time (s) 366.83 Current children cumulated vsize (Kb) 425196 [startup+380.039 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128169 0 0 0 37264 418 0 0 25 0 1 0 1797344606 433233920 102299 4294967295 134512640 135094434 3221224432 3221223044 134563089 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 105770 102299 145 145 0 105625 0 [pid=312] vsize: 423080 Current children cumulated CPU time (s) 376.83 Current children cumulated vsize (Kb) 425204 [startup+390.04 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128173 0 0 0 38264 418 0 0 25 0 1 0 1797344606 433238016 102303 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 105771 102303 145 145 0 105626 0 [pid=312] vsize: 423084 Current children cumulated CPU time (s) 386.83 Current children cumulated vsize (Kb) 425208 [startup+400.041 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128175 0 0 0 39264 418 0 0 25 0 1 0 1797344606 433246208 102305 4294967295 134512640 135094434 3221224432 3221223044 134563059 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 105773 102305 145 145 0 105628 0 [pid=312] vsize: 423092 Current children cumulated CPU time (s) 396.83 Current children cumulated vsize (Kb) 425216 [startup+410.042 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128178 0 0 0 40264 419 0 0 25 0 1 0 1797344606 433254400 102308 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 105775 102308 145 145 0 105630 0 [pid=312] vsize: 423100 Current children cumulated CPU time (s) 406.84 Current children cumulated vsize (Kb) 425224 [startup+420.043 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128180 0 0 0 41265 419 0 0 25 0 1 0 1797344606 433262592 102310 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 105777 102310 145 145 0 105632 0 [pid=312] vsize: 423108 Current children cumulated CPU time (s) 416.85 Current children cumulated vsize (Kb) 425232 [startup+430.044 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128183 0 0 0 42265 419 0 0 25 0 1 0 1797344606 433274880 102313 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 105780 102313 145 145 0 105635 0 [pid=312] vsize: 423120 Current children cumulated CPU time (s) 426.85 Current children cumulated vsize (Kb) 425244 [startup+440.045 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128187 0 0 0 43265 419 0 0 25 0 1 0 1797344606 433291264 102317 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 105784 102317 145 145 0 105639 0 [pid=312] vsize: 423136 Current children cumulated CPU time (s) 436.85 Current children cumulated vsize (Kb) 425260 [startup+450.046 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128193 0 0 0 44265 419 0 0 25 0 1 0 1797344606 433311744 102323 4294967295 134512640 135094434 3221224432 3221223072 134562095 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 105789 102323 145 145 0 105644 0 [pid=312] vsize: 423156 Current children cumulated CPU time (s) 446.85 Current children cumulated vsize (Kb) 425280 [startup+460.047 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128215 0 0 0 45266 419 0 0 25 0 1 0 1797344606 433446912 102345 4294967295 134512640 135094434 3221224432 3221223184 134559282 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 105822 102345 145 145 0 105677 0 [pid=312] vsize: 423288 Current children cumulated CPU time (s) 456.86 Current children cumulated vsize (Kb) 425412 [startup+470.048 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128217 0 0 0 46265 419 0 0 25 0 1 0 1797344606 433451008 102347 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/312/statm): 105823 102347 145 145 0 105678 0 [pid=312] vsize: 423292 Current children cumulated CPU time (s) 466.85 Current children cumulated vsize (Kb) 425416 [startup+480.05 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128219 0 0 0 47265 419 0 0 25 0 1 0 1797344606 433459200 102349 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/312/statm): 105825 102349 145 145 0 105680 0 [pid=312] vsize: 423300 Current children cumulated CPU time (s) 476.85 Current children cumulated vsize (Kb) 425424 [startup+490.051 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128229 0 0 0 48265 420 0 0 25 0 1 0 1797344606 433496064 102359 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/312/statm): 105834 102359 145 145 0 105689 0 [pid=312] vsize: 423336 Current children cumulated CPU time (s) 486.86 Current children cumulated vsize (Kb) 425460 [startup+500.053 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128235 0 0 0 49264 420 0 0 25 0 1 0 1797344606 433520640 102365 4294967295 134512640 135094434 3221224432 3221223044 134563112 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/312/statm): 105840 102365 145 145 0 105695 0 [pid=312] vsize: 423360 Current children cumulated CPU time (s) 496.85 Current children cumulated vsize (Kb) 425484 [startup+510.055 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128247 0 0 0 50264 421 0 0 25 0 1 0 1797344606 433565696 102377 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/312/statm): 105851 102377 145 145 0 105706 0 [pid=312] vsize: 423404 Current children cumulated CPU time (s) 506.86 Current children cumulated vsize (Kb) 425528 [startup+520.055 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128254 0 0 0 51263 421 0 0 25 0 1 0 1797344606 433594368 102384 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/312/statm): 105858 102384 145 145 0 105713 0 [pid=312] vsize: 423432 Current children cumulated CPU time (s) 516.85 Current children cumulated vsize (Kb) 425556 [startup+530.057 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128263 0 0 0 52263 421 0 0 25 0 1 0 1797344606 433631232 102393 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/312/statm): 105867 102393 145 145 0 105722 0 [pid=312] vsize: 423468 Current children cumulated CPU time (s) 526.85 Current children cumulated vsize (Kb) 425592 [startup+540.058 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128322 0 0 0 53262 422 0 0 25 0 1 0 1797344606 433827840 102452 4294967295 134512640 135094434 3221224432 3221223076 134561789 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/312/statm): 105915 102452 145 145 0 105770 0 [pid=312] vsize: 423660 Current children cumulated CPU time (s) 536.85 Current children cumulated vsize (Kb) 425784 [startup+550.06 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128324 0 0 0 54261 423 0 0 25 0 1 0 1797344606 433836032 102454 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/312/statm): 105917 102454 145 145 0 105772 0 [pid=312] vsize: 423668 Current children cumulated CPU time (s) 546.85 Current children cumulated vsize (Kb) 425792 [startup+560.061 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128328 0 0 0 55261 423 0 0 25 0 1 0 1797344606 433852416 102458 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/312/statm): 105921 102458 145 145 0 105776 0 [pid=312] vsize: 423684 Current children cumulated CPU time (s) 556.85 Current children cumulated vsize (Kb) 425808 [startup+570.061 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128334 0 0 0 56261 423 0 0 25 0 1 0 1797344606 433872896 102464 4294967295 134512640 135094434 3221224432 3221223136 134554413 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/312/statm): 105926 102464 145 145 0 105781 0 [pid=312] vsize: 423704 Current children cumulated CPU time (s) 566.85 Current children cumulated vsize (Kb) 425828 [startup+580.062 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128339 0 0 0 57260 424 0 0 25 0 1 0 1797344606 433893376 102469 4294967295 134512640 135094434 3221224432 3221223184 134559282 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/312/statm): 105931 102469 145 145 0 105786 0 [pid=312] vsize: 423724 Current children cumulated CPU time (s) 576.85 Current children cumulated vsize (Kb) 425848 [startup+590.063 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128347 0 0 0 58260 424 0 0 25 0 1 0 1797344606 433926144 102477 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 105939 102477 145 145 0 105794 0 [pid=312] vsize: 423756 Current children cumulated CPU time (s) 586.85 Current children cumulated vsize (Kb) 425880 [startup+600.064 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128354 0 0 0 59260 424 0 0 25 0 1 0 1797344606 433950720 102484 4294967295 134512640 135094434 3221224432 3221223056 134557694 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 105945 102484 145 145 0 105800 0 [pid=312] vsize: 423780 Current children cumulated CPU time (s) 596.85 Current children cumulated vsize (Kb) 425904 [startup+610.064 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128382 0 0 0 60260 424 0 0 25 0 1 0 1797344606 434061312 102512 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 105972 102512 145 145 0 105827 0 [pid=312] vsize: 423888 Current children cumulated CPU time (s) 606.85 Current children cumulated vsize (Kb) 426012 [startup+620.065 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128389 0 0 0 61260 424 0 0 25 0 1 0 1797344606 434089984 102519 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 105979 102519 145 145 0 105834 0 [pid=312] vsize: 423916 Current children cumulated CPU time (s) 616.85 Current children cumulated vsize (Kb) 426040 [startup+630.066 s] Raw data (loadavg): 1.00 0.99 0.95 3/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128397 0 0 0 62260 424 0 0 25 0 1 0 1797344606 434118656 102527 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 105986 102527 145 145 0 105841 0 [pid=312] vsize: 423944 Current children cumulated CPU time (s) 626.85 Current children cumulated vsize (Kb) 426068 [startup+640.067 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128404 0 0 0 63261 424 0 0 25 0 1 0 1797344606 434147328 102534 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 105993 102534 145 145 0 105848 0 [pid=312] vsize: 423972 Current children cumulated CPU time (s) 636.86 Current children cumulated vsize (Kb) 426096 [startup+650.068 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128413 0 0 0 64261 424 0 0 25 0 1 0 1797344606 434184192 102543 4294967295 134512640 135094434 3221224432 3221223072 134562088 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106002 102543 145 145 0 105857 0 [pid=312] vsize: 424008 Current children cumulated CPU time (s) 646.86 Current children cumulated vsize (Kb) 426132 [startup+660.069 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128431 0 0 0 65261 425 0 0 25 0 1 0 1797344606 434253824 102561 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106019 102561 145 145 0 105874 0 [pid=312] vsize: 424076 Current children cumulated CPU time (s) 656.87 Current children cumulated vsize (Kb) 426200 [startup+670.07 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128465 0 0 0 66260 425 0 0 25 0 1 0 1797344606 434388992 102595 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/312/statm): 106052 102595 145 145 0 105907 0 [pid=312] vsize: 424208 Current children cumulated CPU time (s) 666.86 Current children cumulated vsize (Kb) 426332 [startup+680.071 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128505 0 0 0 67259 425 0 0 25 0 1 0 1797344606 434548736 102635 4294967295 134512640 135094434 3221224432 3221223088 134561460 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106091 102635 145 145 0 105946 0 [pid=312] vsize: 424364 Current children cumulated CPU time (s) 676.85 Current children cumulated vsize (Kb) 426488 [startup+690.072 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128512 0 0 0 68259 425 0 0 25 0 1 0 1797344606 434565120 102642 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106095 102642 145 145 0 105950 0 [pid=312] vsize: 424380 Current children cumulated CPU time (s) 686.85 Current children cumulated vsize (Kb) 426504 [startup+700.073 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128517 0 0 0 69259 425 0 0 25 0 1 0 1797344606 434585600 102647 4294967295 134512640 135094434 3221224432 3221223136 134554559 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106100 102647 145 145 0 105955 0 [pid=312] vsize: 424400 Current children cumulated CPU time (s) 696.85 Current children cumulated vsize (Kb) 426524 [startup+710.074 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128519 0 0 0 70260 425 0 0 25 0 1 0 1797344606 434593792 102649 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106102 102649 145 145 0 105957 0 [pid=312] vsize: 424408 Current children cumulated CPU time (s) 706.86 Current children cumulated vsize (Kb) 426532 [startup+720.075 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128523 0 0 0 71260 425 0 0 25 0 1 0 1797344606 434601984 102653 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106104 102653 145 145 0 105959 0 [pid=312] vsize: 424416 Current children cumulated CPU time (s) 716.86 Current children cumulated vsize (Kb) 426540 [startup+730.076 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128524 0 0 0 72260 425 0 0 25 0 1 0 1797344606 434606080 102654 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106105 102654 145 145 0 105960 0 [pid=312] vsize: 424420 Current children cumulated CPU time (s) 726.86 Current children cumulated vsize (Kb) 426544 [startup+740.077 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128533 0 0 0 73260 426 0 0 25 0 1 0 1797344606 434642944 102663 4294967295 134512640 135094434 3221224432 3221223056 134563167 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106114 102663 145 145 0 105969 0 [pid=312] vsize: 424456 Current children cumulated CPU time (s) 736.87 Current children cumulated vsize (Kb) 426580 [startup+750.078 s] Raw data (loadavg): 1.00 0.99 0.95 3/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128536 0 0 0 74260 426 0 0 25 0 1 0 1797344606 434655232 102666 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106117 102666 145 145 0 105972 0 [pid=312] vsize: 424468 Current children cumulated CPU time (s) 746.87 Current children cumulated vsize (Kb) 426592 [startup+760.08 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128538 0 0 0 75260 426 0 0 25 0 1 0 1797344606 434663424 102668 4294967295 134512640 135094434 3221224432 3221223120 134554760 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106119 102668 145 145 0 105974 0 [pid=312] vsize: 424476 Current children cumulated CPU time (s) 756.87 Current children cumulated vsize (Kb) 426600 [startup+770.081 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128541 0 0 0 76261 426 0 0 25 0 1 0 1797344606 434671616 102671 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106121 102671 145 145 0 105976 0 [pid=312] vsize: 424484 Current children cumulated CPU time (s) 766.88 Current children cumulated vsize (Kb) 426608 [startup+780.082 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128549 0 0 0 77261 426 0 0 25 0 1 0 1797344606 434704384 102679 4294967295 134512640 135094434 3221224432 3221223088 134557956 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106129 102679 145 145 0 105984 0 [pid=312] vsize: 424516 Current children cumulated CPU time (s) 776.88 Current children cumulated vsize (Kb) 426640 [startup+790.082 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128659 0 0 0 78259 426 0 0 25 0 1 0 1797344606 435146752 102789 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106237 102789 145 145 0 106092 0 [pid=312] vsize: 424948 Current children cumulated CPU time (s) 786.86 Current children cumulated vsize (Kb) 427072 [startup+800.083 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128665 0 0 0 79259 426 0 0 25 0 1 0 1797344606 435171328 102795 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106243 102795 145 145 0 106098 0 [pid=312] vsize: 424972 Current children cumulated CPU time (s) 796.86 Current children cumulated vsize (Kb) 427096 [startup+810.084 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128675 0 0 0 80259 426 0 0 25 0 1 0 1797344606 435212288 102805 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106253 102805 145 145 0 106108 0 [pid=312] vsize: 425012 Current children cumulated CPU time (s) 806.86 Current children cumulated vsize (Kb) 427136 [startup+820.085 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128717 0 0 0 81259 426 0 0 25 0 1 0 1797344606 435511296 102847 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106326 102847 145 145 0 106181 0 [pid=312] vsize: 425304 Current children cumulated CPU time (s) 816.86 Current children cumulated vsize (Kb) 427428 [startup+830.086 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128717 0 0 0 82259 426 0 0 25 0 1 0 1797344606 435511296 102847 4294967295 134512640 135094434 3221224432 3221223088 134561476 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106326 102847 145 145 0 106181 0 [pid=312] vsize: 425304 Current children cumulated CPU time (s) 826.86 Current children cumulated vsize (Kb) 427428 [startup+840.086 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128717 0 0 0 83259 426 0 0 25 0 1 0 1797344606 435511296 102847 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106326 102847 145 145 0 106181 0 [pid=312] vsize: 425304 Current children cumulated CPU time (s) 836.86 Current children cumulated vsize (Kb) 427428 [startup+850.087 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128718 0 0 0 84260 426 0 0 25 0 1 0 1797344606 435511296 102848 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106326 102848 145 145 0 106181 0 [pid=312] vsize: 425304 Current children cumulated CPU time (s) 846.87 Current children cumulated vsize (Kb) 427428 [startup+860.088 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128718 0 0 0 85260 426 0 0 25 0 1 0 1797344606 435511296 102848 4294967295 134512640 135094434 3221224432 3221223044 134563130 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106326 102848 145 145 0 106181 0 [pid=312] vsize: 425304 Current children cumulated CPU time (s) 856.87 Current children cumulated vsize (Kb) 427428 [startup+870.089 s] Raw data (loadavg): 1.08 1.00 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128719 0 0 0 86260 426 0 0 25 0 1 0 1797344606 435511296 102849 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106326 102849 145 145 0 106181 0 [pid=312] vsize: 425304 Current children cumulated CPU time (s) 866.87 Current children cumulated vsize (Kb) 427428 [startup+880.09 s] Raw data (loadavg): 1.07 1.00 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128720 0 0 0 87260 426 0 0 25 0 1 0 1797344606 435511296 102850 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106326 102850 145 145 0 106181 0 [pid=312] vsize: 425304 Current children cumulated CPU time (s) 876.87 Current children cumulated vsize (Kb) 427428 [startup+890.09 s] Raw data (loadavg): 1.06 1.00 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128721 0 0 0 88261 426 0 0 25 0 1 0 1797344606 435515392 102851 4294967295 134512640 135094434 3221224432 3221223072 134562068 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106327 102851 145 145 0 106182 0 [pid=312] vsize: 425308 Current children cumulated CPU time (s) 886.88 Current children cumulated vsize (Kb) 427432 [startup+900.091 s] Raw data (loadavg): 1.05 1.00 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128723 0 0 0 89261 426 0 0 25 0 1 0 1797344606 435523584 102853 4294967295 134512640 135094434 3221224432 3221223088 134561734 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106329 102853 145 145 0 106184 0 [pid=312] vsize: 425316 Current children cumulated CPU time (s) 896.88 Current children cumulated vsize (Kb) 427440 [startup+910.092 s] Raw data (loadavg): 1.04 1.00 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128727 0 0 0 90261 426 0 0 25 0 1 0 1797344606 435539968 102857 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106333 102857 145 145 0 106188 0 [pid=312] vsize: 425332 Current children cumulated CPU time (s) 906.88 Current children cumulated vsize (Kb) 427456 [startup+920.093 s] Raw data (loadavg): 1.03 1.00 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128742 0 0 0 91261 426 0 0 25 0 1 0 1797344606 435597312 102872 4294967295 134512640 135094434 3221224432 3221223120 134554821 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106347 102872 145 145 0 106202 0 [pid=312] vsize: 425388 Current children cumulated CPU time (s) 916.88 Current children cumulated vsize (Kb) 427512 [startup+930.093 s] Raw data (loadavg): 1.03 1.00 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128770 0 0 0 92261 426 0 0 25 0 1 0 1797344606 435712000 102900 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106375 102900 145 145 0 106230 0 [pid=312] vsize: 425500 Current children cumulated CPU time (s) 926.88 Current children cumulated vsize (Kb) 427624 [startup+940.094 s] Raw data (loadavg): 1.02 1.00 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128787 0 0 0 93261 426 0 0 25 0 1 0 1797344606 435777536 102917 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106391 102917 145 145 0 106246 0 [pid=312] vsize: 425564 Current children cumulated CPU time (s) 936.88 Current children cumulated vsize (Kb) 427688 [startup+950.096 s] Raw data (loadavg): 1.02 1.00 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128829 0 0 0 94260 427 0 0 25 0 1 0 1797344606 435945472 102959 4294967295 134512640 135094434 3221224432 3221223120 134554760 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106432 102959 145 145 0 106287 0 [pid=312] vsize: 425728 Current children cumulated CPU time (s) 946.88 Current children cumulated vsize (Kb) 427852 [startup+960.097 s] Raw data (loadavg): 1.02 1.00 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128853 0 0 0 95260 427 0 0 25 0 1 0 1797344606 436043776 102983 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106456 102983 145 145 0 106311 0 [pid=312] vsize: 425824 Current children cumulated CPU time (s) 956.88 Current children cumulated vsize (Kb) 427948 [startup+970.098 s] Raw data (loadavg): 1.01 1.00 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128871 0 0 0 96260 427 0 0 25 0 1 0 1797344606 436113408 103001 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106473 103001 145 145 0 106328 0 [pid=312] vsize: 425892 Current children cumulated CPU time (s) 966.88 Current children cumulated vsize (Kb) 428016 [startup+980.1 s] Raw data (loadavg): 1.01 1.00 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128941 0 0 0 97258 428 0 0 25 0 1 0 1797344606 436396032 103071 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/312/statm): 106542 103071 145 145 0 106397 0 [pid=312] vsize: 426168 Current children cumulated CPU time (s) 976.87 Current children cumulated vsize (Kb) 428292 [startup+990.1 s] Raw data (loadavg): 1.01 1.00 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129063 0 0 0 98256 429 0 0 25 0 1 0 1797344606 436883456 103193 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106661 103193 145 145 0 106516 0 [pid=312] vsize: 426644 Current children cumulated CPU time (s) 986.86 Current children cumulated vsize (Kb) 428768 [startup+1000.1 s] Raw data (loadavg): 1.01 1.00 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129083 0 0 0 99256 429 0 0 25 0 1 0 1797344606 436961280 103213 4294967295 134512640 135094434 3221224432 3221223088 134557804 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106680 103213 145 145 0 106535 0 [pid=312] vsize: 426720 Current children cumulated CPU time (s) 996.86 Current children cumulated vsize (Kb) 428844 [startup+1010.1 s] Raw data (loadavg): 1.00 1.00 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129088 0 0 0 100256 429 0 0 25 0 1 0 1797344606 436981760 103218 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106685 103218 145 145 0 106540 0 [pid=312] vsize: 426740 Current children cumulated CPU time (s) 1006.86 Current children cumulated vsize (Kb) 428864 [startup+1020.1 s] Raw data (loadavg): 1.00 1.00 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129105 0 0 0 101255 429 0 0 25 0 1 0 1797344606 437051392 103235 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106702 103235 145 145 0 106557 0 [pid=312] vsize: 426808 Current children cumulated CPU time (s) 1016.85 Current children cumulated vsize (Kb) 428932 [startup+1030.1 s] Raw data (loadavg): 1.00 1.00 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129115 0 0 0 102255 429 0 0 25 0 1 0 1797344606 437088256 103245 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106711 103245 145 145 0 106566 0 [pid=312] vsize: 426844 Current children cumulated CPU time (s) 1026.85 Current children cumulated vsize (Kb) 428968 [startup+1040.11 s] Raw data (loadavg): 1.00 1.00 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129130 0 0 0 103256 429 0 0 25 0 1 0 1797344606 437149696 103260 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106726 103260 145 145 0 106581 0 [pid=312] vsize: 426904 Current children cumulated CPU time (s) 1036.86 Current children cumulated vsize (Kb) 429028 [startup+1050.11 s] Raw data (loadavg): 1.00 1.00 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129168 0 0 0 104255 430 0 0 25 0 1 0 1797344606 437305344 103298 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106764 103298 145 145 0 106619 0 [pid=312] vsize: 427056 Current children cumulated CPU time (s) 1046.86 Current children cumulated vsize (Kb) 429180 [startup+1060.11 s] Raw data (loadavg): 1.00 1.00 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129195 0 0 0 105255 430 0 0 25 0 1 0 1797344606 437411840 103325 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106790 103325 145 145 0 106645 0 [pid=312] vsize: 427160 Current children cumulated CPU time (s) 1056.86 Current children cumulated vsize (Kb) 429284 [startup+1070.11 s] Raw data (loadavg): 1.00 1.00 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129220 0 0 0 106255 430 0 0 25 0 1 0 1797344606 437514240 103350 4294967295 134512640 135094434 3221224432 3221223084 134561527 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106815 103350 145 145 0 106670 0 [pid=312] vsize: 427260 Current children cumulated CPU time (s) 1066.86 Current children cumulated vsize (Kb) 429384 [startup+1080.11 s] Raw data (loadavg): 1.00 1.00 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129235 0 0 0 107255 430 0 0 25 0 1 0 1797344606 437571584 103365 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106829 103365 145 145 0 106684 0 [pid=312] vsize: 427316 Current children cumulated CPU time (s) 1076.86 Current children cumulated vsize (Kb) 429440 [startup+1090.11 s] Raw data (loadavg): 1.00 1.00 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129251 0 0 0 108255 430 0 0 25 0 1 0 1797344606 437637120 103381 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106845 103381 145 145 0 106700 0 [pid=312] vsize: 427380 Current children cumulated CPU time (s) 1086.86 Current children cumulated vsize (Kb) 429504 [startup+1100.11 s] Raw data (loadavg): 1.00 1.00 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129265 0 0 0 109255 430 0 0 25 0 1 0 1797344606 437694464 103395 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106859 103395 145 145 0 106714 0 [pid=312] vsize: 427436 Current children cumulated CPU time (s) 1096.86 Current children cumulated vsize (Kb) 429560 [startup+1110.11 s] Raw data (loadavg): 1.00 1.00 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129279 0 0 0 110255 430 0 0 25 0 1 0 1797344606 437747712 103409 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106872 103409 145 145 0 106727 0 [pid=312] vsize: 427488 Current children cumulated CPU time (s) 1106.86 Current children cumulated vsize (Kb) 429612 [startup+1120.11 s] Raw data (loadavg): 1.00 1.00 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129299 0 0 0 111255 431 0 0 25 0 1 0 1797344606 437829632 103429 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106892 103429 145 145 0 106747 0 [pid=312] vsize: 427568 Current children cumulated CPU time (s) 1116.87 Current children cumulated vsize (Kb) 429692 [startup+1130.11 s] Raw data (loadavg): 1.00 1.00 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129318 0 0 0 112254 431 0 0 25 0 1 0 1797344606 437907456 103448 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106911 103448 145 145 0 106766 0 [pid=312] vsize: 427644 Current children cumulated CPU time (s) 1126.86 Current children cumulated vsize (Kb) 429768 [startup+1140.11 s] Raw data (loadavg): 1.00 1.00 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129327 0 0 0 113254 431 0 0 25 0 1 0 1797344606 437944320 103457 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106920 103457 145 145 0 106775 0 [pid=312] vsize: 427680 Current children cumulated CPU time (s) 1136.86 Current children cumulated vsize (Kb) 429804 [startup+1150.11 s] Raw data (loadavg): 1.00 1.00 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129337 0 0 0 114254 431 0 0 25 0 1 0 1797344606 437985280 103467 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106930 103467 145 145 0 106785 0 [pid=312] vsize: 427720 Current children cumulated CPU time (s) 1146.86 Current children cumulated vsize (Kb) 429844 [startup+1160.12 s] Raw data (loadavg): 1.00 1.00 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129339 0 0 0 115255 431 0 0 25 0 1 0 1797344606 437993472 103469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106932 103469 145 145 0 106787 0 [pid=312] vsize: 427728 Current children cumulated CPU time (s) 1156.87 Current children cumulated vsize (Kb) 429852 [startup+1170.12 s] Raw data (loadavg): 1.00 1.00 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129343 0 0 0 116255 431 0 0 25 0 1 0 1797344606 438009856 103473 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106936 103473 145 145 0 106791 0 [pid=312] vsize: 427744 Current children cumulated CPU time (s) 1166.87 Current children cumulated vsize (Kb) 429868 [startup+1180.12 s] Raw data (loadavg): 1.00 1.00 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129351 0 0 0 117255 431 0 0 25 0 1 0 1797344606 438042624 103481 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106944 103481 145 145 0 106799 0 [pid=312] vsize: 427776 Current children cumulated CPU time (s) 1176.87 Current children cumulated vsize (Kb) 429900 [startup+1190.12 s] Raw data (loadavg): 1.00 1.00 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129358 0 0 0 118255 431 0 0 25 0 1 0 1797344606 438067200 103488 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106950 103488 145 145 0 106805 0 [pid=312] vsize: 427800 Current children cumulated CPU time (s) 1186.87 Current children cumulated vsize (Kb) 429924 [startup+1200.12 s] Raw data (loadavg): 1.00 1.00 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129374 0 0 0 119255 431 0 0 25 0 1 0 1797344606 438132736 103504 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106966 103504 145 145 0 106821 0 [pid=312] vsize: 427864 Current children cumulated CPU time (s) 1196.87 Current children cumulated vsize (Kb) 429988 [startup+1210.12 s] Raw data (loadavg): 1.00 1.00 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129393 0 0 0 120256 431 0 0 25 0 1 0 1797344606 438210560 103523 4294967295 134512640 135094434 3221224432 3221223100 134562168 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106985 103523 145 145 0 106840 0 [pid=312] vsize: 427940 Current children cumulated CPU time (s) 1206.88 Current children cumulated vsize (Kb) 430064 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.12 s] Raw data (loadavg): 1.00 1.00 0.95 2/57 312 Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/308/statm): 531 226 485 147 0 384 0 [pid=308] vsize: 2124 Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129393 0 0 0 120256 431 0 0 25 0 1 0 1797344606 438210560 103523 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/312/statm): 106985 103523 145 145 0 106840 0 [pid=312] vsize: 427940 Current children cumulated CPU time (s) 1206.88 Current children cumulated vsize (Kb) 430064 Sending SIGTERM to -308 Sleeping 2 seconds One traced child (pid=308) ended because it received signal 15 (SIGTERM) One traced child (pid=312) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.51 CPU time (s): 1207.2 CPU user time (s): 1202.66 CPU system time (s): 4.54231 CPU usage (%): 99.7267 Max. virtual memory (cumulated for all children) (Kb): 430064
ERROR: no interpretation found !