Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
  1. LAUNCHER DATA
    These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
    Note that some very long lines in this section may be truncated by your web browser !
  3. WATCHER DATA
    This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
    Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
    When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
  4. VERIFIER DATA
    The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.

General information on the benchmark

Namemps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-fast0507.opb
MD5SUM38504d32a17a57a658eee171614b901e
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
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 numbers17
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1189.22
Number of variables63009
Total number of constraints63516
Number of constraints which are clauses507
Number of constraints which are cardinality constraints (but not clauses)63009
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint1
Maximum length of a constraint7753

Trace number 3904

Launcher Data

LAUNCH ON wulflinc27 THE 2005-09-19 03:35:03 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2908 boxname=wulflinc27 idbench=564 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  38504d32a17a57a658eee171614b901e  /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-fast0507.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-fast0507.opb
IDLAUNCH: 2908
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        874204 kB
Buffers:         37236 kB
Cached:          90520 kB
SwapCached:        764 kB
Active:          80920 kB
Inactive:        49460 kB
HighTotal:      131008 kB
HighFree:        37856 kB
LowTotal:       903652 kB
LowFree:        836348 kB
SwapTotal:     2097892 kB
SwapFree:      2096616 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5728 kB
Slab:            24404 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-19 03:55:14 (client local time) WITH STATUS 10 IN 1207.18 SECONDS
stats: 2908 7 1207.18 10

Solver Data

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 Found solution: 343
c ---[   0]---> Adder-cost: 125984   maxlim: 122082   bits: 17/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  882303  3556733 |  294101       0        0     nan |  0.000 % |
c |       100 |  882255  3556553 |  323511      96      289     3.0 |  0.016 % |
c |       250 |  881309  3553217 |  355862     114      351     3.1 |  0.101 % |
c |       475 |  880776  3551348 |  391448     259      864     3.3 |  0.151 % |
c |       812 |  880279  3549615 |  430593     523     1870     3.6 |  0.196 % |
c |      1318 |  879889  3548279 |  473652     977     4292     4.4 |  0.232 % |
c |      2077 |  879700  3547656 |  521017    1709    10871     6.4 |  0.251 % |
c |      3216 |  879644  3547470 |  573119    2839    17243     6.1 |  0.256 % |
c |      4924 |  879509  3547011 |  630431    4532    25034     5.5 |  0.270 % |
c |      7486 |  879420  3546722 |  693474    7079    43284     6.1 |  0.279 % |
c |     11330 |  879361  3546531 |  762822   10915    68960     6.3 |  0.286 % |
c |     17096 |  879361  3546531 |  839104   16681   104664     6.3 |  0.286 % |
c |     25745 |  879361  3546531 |  923014   25330   246101     9.7 |  0.286 % |
c |     38719 |  879284  3546264 | 1015316   38293   536469    14.0 |  0.293 % |
c 
c *** TERMINATED ***
s SATISFIABLE

#### TRACE IS TOO LONG. SEE FILE pb05-wulflinc27-2908-564-3-0-15386.out.gz TO GET THE COMPLETE TRACE
#### TAIL OF TRACE ####
...c Parsing PB file...
c Converting 494 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ==
c   -- Clauses(.)/Splits(s): .......................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |     487   407371 |     162       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 343
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

Watcher Data

Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing Stack size limit: 67108864 bytes
Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb
Enforcing VSIZE limit: 994918400 bytes
Current StackSize limit: 67108864 bytes
Raw data (/proc/15423/stat): 15423 (minisat+_script) R 15422 15423 28974 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1846681004 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/15423/statm): 174 3 169 147 0 27 0
[pid=15423] vsize: 696
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libtermcap.so.2
open syscall for file tls/i686/libtermcap.so.2
open syscall for file tls/mmx/libtermcap.so.2
open syscall for file tls/libtermcap.so.2
open syscall for file i686/mmx/libtermcap.so.2
open syscall for file i686/libtermcap.so.2
open syscall for file mmx/libtermcap.so.2
open syscall for file libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/libtermcap.so.2
open syscall for file /etc/ld.so.cache
open syscall for file /lib/libtermcap.so.2
open syscall for file tls/i686/mmx/libdl.so.2
open syscall for file tls/i686/libdl.so.2
open syscall for file tls/mmx/libdl.so.2
open syscall for file tls/libdl.so.2
open syscall for file i686/mmx/libdl.so.2
open syscall for file i686/libdl.so.2
open syscall for file mmx/libdl.so.2
open syscall for file libdl.so.2
open syscall for file /oldhome/oroussel/lib/libdl.so.2
open syscall for file /lib/libdl.so.2
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /lib/tls/libc.so.6
open syscall for file /dev/tty
open syscall for file /etc/mtab
open syscall for file /proc/meminfo
open syscall for file /oldhome/oroussel/solvers/minisat+_script
New process pid=15424
New process pid=15425
New process pid=15426
execve syscall for /bin/sed executable
One traced child (pid=15425) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=15426) exited with status: 0
One traced child (pid=15424) exited with status: 0
New process pid=15427
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-fast0507.opb

[startup+10.0031 s]
Raw data (loadavg): 0.93 0.96 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 16435 0 0 0 885 65 0 0 25 0 1 0 1846681009 55410688 11906 4294967295 134512640 135094434 3221224432 3221222128 134519836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 13528 11913 145 145 0 13383 0
[pid=15427] vsize: 54112
Current children cumulated CPU time (s) 9.51
Current children cumulated vsize (Kb) 56236

[startup+20.0049 s]
Raw data (loadavg): 0.94 0.96 0.95 1/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) T 15423 15423 28974 0 -1 0 56273 0 0 0 1688 182 0 0 23 0 1 0 1846681009 186327040 41857 4294967295 134512640 135094434 3221224432 3221221964 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/15427/statm): 45490 41857 145 145 0 45345 0
[pid=15427] vsize: 181960
Current children cumulated CPU time (s) 18.71
Current children cumulated vsize (Kb) 184084

[startup+30.0057 s]
Raw data (loadavg): 0.95 0.96 0.95 1/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) T 15423 15423 28974 0 -1 0 98279 0 0 0 2489 303 0 0 24 0 1 0 1846681009 333815808 73317 4294967295 134512640 135094434 3221224432 3221220508 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/15427/statm): 81498 73317 145 145 0 81353 0
[pid=15427] vsize: 325992
Current children cumulated CPU time (s) 27.93
Current children cumulated vsize (Kb) 328116

[startup+40.0076 s]
Raw data (loadavg): 0.96 0.96 0.95 1/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) T 15423 15423 28974 0 -1 0 114713 0 0 0 3380 361 0 0 24 0 1 0 1846681009 375799808 88843 4294967295 134512640 135094434 3221224432 3221216092 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/15427/statm): 91748 88843 145 145 0 91603 0
[pid=15427] vsize: 366992
Current children cumulated CPU time (s) 37.42
Current children cumulated vsize (Kb) 369116

[startup+50.0084 s]
Raw data (loadavg): 0.96 0.96 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 126981 0 0 0 4264 416 0 0 25 0 1 0 1846681009 428355584 101111 4294967295 134512640 135094434 3221224432 3221223136 134559007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15427/statm): 104579 101111 145 145 0 104434 0
[pid=15427] vsize: 418316
Current children cumulated CPU time (s) 46.81
Current children cumulated vsize (Kb) 420440

[startup+60.0092 s]
Raw data (loadavg): 0.97 0.96 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 126990 0 0 0 5262 417 0 0 25 0 1 0 1846681009 428392448 101120 4294967295 134512640 135094434 3221224432 3221223092 134553530 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 104588 101120 145 145 0 104443 0
[pid=15427] vsize: 418352
Current children cumulated CPU time (s) 56.8
Current children cumulated vsize (Kb) 420476

[startup+70.01 s]
Raw data (loadavg): 0.97 0.96 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 127009 0 0 0 6262 417 0 0 25 0 1 0 1846681009 428470272 101139 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 104607 101139 145 145 0 104462 0
[pid=15427] vsize: 418428
Current children cumulated CPU time (s) 66.8
Current children cumulated vsize (Kb) 420552

[startup+80.0109 s]
Raw data (loadavg): 0.98 0.96 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 127066 0 0 0 7262 417 0 0 25 0 1 0 1846681009 428703744 101196 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 104664 101196 145 145 0 104519 0
[pid=15427] vsize: 418656
Current children cumulated CPU time (s) 76.8
Current children cumulated vsize (Kb) 420780

[startup+90.0117 s]
Raw data (loadavg): 0.98 0.96 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 127547 0 0 0 8255 420 0 0 25 0 1 0 1846681009 430673920 101677 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105145 101677 145 145 0 105000 0
[pid=15427] vsize: 420580
Current children cumulated CPU time (s) 86.76
Current children cumulated vsize (Kb) 422704

[startup+100.013 s]
Raw data (loadavg): 0.98 0.96 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 127744 0 0 0 9252 422 0 0 25 0 1 0 1846681009 431714304 101874 4294967295 134512640 135094434 3221224432 3221223072 134562057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105399 101874 145 145 0 105254 0
[pid=15427] vsize: 421596
Current children cumulated CPU time (s) 96.75
Current children cumulated vsize (Kb) 423720

[startup+110.014 s]
Raw data (loadavg): 0.98 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 127831 0 0 0 10251 423 0 0 25 0 1 0 1846681009 431996928 101961 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105468 101961 145 145 0 105323 0
[pid=15427] vsize: 421872
Current children cumulated CPU time (s) 106.75
Current children cumulated vsize (Kb) 423996

[startup+120.015 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 127889 0 0 0 11251 424 0 0 25 0 1 0 1846681009 432234496 102019 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105526 102019 145 145 0 105381 0
[pid=15427] vsize: 422104
Current children cumulated CPU time (s) 116.76
Current children cumulated vsize (Kb) 424228

[startup+130.016 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 127935 0 0 0 12250 424 0 0 25 0 1 0 1846681009 432418816 102065 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105571 102065 145 145 0 105426 0
[pid=15427] vsize: 422284
Current children cumulated CPU time (s) 126.75
Current children cumulated vsize (Kb) 424408

[startup+140.018 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 127978 0 0 0 13250 424 0 0 25 0 1 0 1846681009 432529408 102108 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105598 102108 145 145 0 105453 0
[pid=15427] vsize: 422392
Current children cumulated CPU time (s) 136.75
Current children cumulated vsize (Kb) 424516

[startup+150.019 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128007 0 0 0 14250 424 0 0 25 0 1 0 1846681009 432631808 102137 4294967295 134512640 135094434 3221224432 3221223088 134557774 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105623 102137 145 145 0 105478 0
[pid=15427] vsize: 422492
Current children cumulated CPU time (s) 146.75
Current children cumulated vsize (Kb) 424616

[startup+160.018 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128029 0 0 0 15249 425 0 0 25 0 1 0 1846681009 432705536 102159 4294967295 134512640 135094434 3221224432 3221223088 134558398 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105641 102159 145 145 0 105496 0
[pid=15427] vsize: 422564
Current children cumulated CPU time (s) 156.75
Current children cumulated vsize (Kb) 424688

[startup+170.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128043 0 0 0 16249 425 0 0 25 0 1 0 1846681009 432762880 102173 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105655 102173 145 145 0 105510 0
[pid=15427] vsize: 422620
Current children cumulated CPU time (s) 166.75
Current children cumulated vsize (Kb) 424744

[startup+180.021 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128056 0 0 0 17249 425 0 0 25 0 1 0 1846681009 432812032 102186 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105667 102186 145 145 0 105522 0
[pid=15427] vsize: 422668
Current children cumulated CPU time (s) 176.75
Current children cumulated vsize (Kb) 424792

[startup+190.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128065 0 0 0 18249 425 0 0 25 0 1 0 1846681009 432848896 102195 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105676 102195 145 145 0 105531 0
[pid=15427] vsize: 422704
Current children cumulated CPU time (s) 186.75
Current children cumulated vsize (Kb) 424828

[startup+200.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128081 0 0 0 19249 425 0 0 25 0 1 0 1846681009 432943104 102211 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105699 102211 145 145 0 105554 0
[pid=15427] vsize: 422796
Current children cumulated CPU time (s) 196.75
Current children cumulated vsize (Kb) 424920

[startup+210.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128081 0 0 0 20249 425 0 0 25 0 1 0 1846681009 432943104 102211 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105699 102211 145 145 0 105554 0
[pid=15427] vsize: 422796
Current children cumulated CPU time (s) 206.75
Current children cumulated vsize (Kb) 424920

[startup+220.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128088 0 0 0 21249 426 0 0 25 0 1 0 1846681009 432967680 102218 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105705 102218 145 145 0 105560 0
[pid=15427] vsize: 422820
Current children cumulated CPU time (s) 216.76
Current children cumulated vsize (Kb) 424944

[startup+230.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128097 0 0 0 22249 426 0 0 25 0 1 0 1846681009 432988160 102227 4294967295 134512640 135094434 3221224432 3221223088 134561505 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15427/statm): 105710 102227 145 145 0 105565 0
[pid=15427] vsize: 422840
Current children cumulated CPU time (s) 226.76
Current children cumulated vsize (Kb) 424964

[startup+240.027 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128102 0 0 0 23249 426 0 0 25 0 1 0 1846681009 433008640 102232 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105715 102232 145 145 0 105570 0
[pid=15427] vsize: 422860
Current children cumulated CPU time (s) 236.76
Current children cumulated vsize (Kb) 424984

[startup+250.028 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128110 0 0 0 24249 426 0 0 25 0 1 0 1846681009 433037312 102240 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105722 102240 145 145 0 105577 0
[pid=15427] vsize: 422888
Current children cumulated CPU time (s) 246.76
Current children cumulated vsize (Kb) 425012

[startup+260.029 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128114 0 0 0 25249 426 0 0 25 0 1 0 1846681009 433053696 102244 4294967295 134512640 135094434 3221224432 3221223072 134562092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105726 102244 145 145 0 105581 0
[pid=15427] vsize: 422904
Current children cumulated CPU time (s) 256.76
Current children cumulated vsize (Kb) 425028

[startup+270.031 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128125 0 0 0 26250 426 0 0 25 0 1 0 1846681009 433078272 102255 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15427/statm): 105732 102255 145 145 0 105587 0
[pid=15427] vsize: 422928
Current children cumulated CPU time (s) 266.77
Current children cumulated vsize (Kb) 425052

[startup+280.031 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128130 0 0 0 27249 426 0 0 25 0 1 0 1846681009 433098752 102260 4294967295 134512640 135094434 3221224432 3221223044 134563124 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105737 102260 145 145 0 105592 0
[pid=15427] vsize: 422948
Current children cumulated CPU time (s) 276.76
Current children cumulated vsize (Kb) 425072

[startup+290.033 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128132 0 0 0 28249 426 0 0 25 0 1 0 1846681009 433106944 102262 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105739 102262 145 145 0 105594 0
[pid=15427] vsize: 422956
Current children cumulated CPU time (s) 286.76
Current children cumulated vsize (Kb) 425080

[startup+300.034 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128134 0 0 0 29249 426 0 0 25 0 1 0 1846681009 433115136 102264 4294967295 134512640 135094434 3221224432 3221223072 134562128 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105741 102264 145 145 0 105596 0
[pid=15427] vsize: 422964
Current children cumulated CPU time (s) 296.76
Current children cumulated vsize (Kb) 425088

[startup+310.036 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128141 0 0 0 30249 426 0 0 25 0 1 0 1846681009 433135616 102271 4294967295 134512640 135094434 3221224432 3221223152 134561655 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105746 102271 145 145 0 105601 0
[pid=15427] vsize: 422984
Current children cumulated CPU time (s) 306.76
Current children cumulated vsize (Kb) 425108

[startup+320.037 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128146 0 0 0 31249 426 0 0 25 0 1 0 1846681009 433147904 102276 4294967295 134512640 135094434 3221224432 3221223044 134563124 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105749 102276 145 145 0 105604 0
[pid=15427] vsize: 422996
Current children cumulated CPU time (s) 316.76
Current children cumulated vsize (Kb) 425120

[startup+330.038 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128150 0 0 0 32250 426 0 0 25 0 1 0 1846681009 433164288 102280 4294967295 134512640 135094434 3221224432 3221223072 134561792 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105753 102280 145 145 0 105608 0
[pid=15427] vsize: 423012
Current children cumulated CPU time (s) 326.77
Current children cumulated vsize (Kb) 425136

[startup+340.039 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128153 0 0 0 33250 426 0 0 25 0 1 0 1846681009 433172480 102283 4294967295 134512640 135094434 3221224432 3221223088 134561508 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105755 102283 145 145 0 105610 0
[pid=15427] vsize: 423020
Current children cumulated CPU time (s) 336.77
Current children cumulated vsize (Kb) 425144

[startup+350.04 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128156 0 0 0 34250 427 0 0 25 0 1 0 1846681009 433184768 102286 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105758 102286 145 145 0 105613 0
[pid=15427] vsize: 423032
Current children cumulated CPU time (s) 346.78
Current children cumulated vsize (Kb) 425156

[startup+360.041 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128159 0 0 0 35250 427 0 0 25 0 1 0 1846681009 433197056 102289 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105761 102289 145 145 0 105616 0
[pid=15427] vsize: 423044
Current children cumulated CPU time (s) 356.78
Current children cumulated vsize (Kb) 425168

[startup+370.042 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128167 0 0 0 36250 427 0 0 25 0 1 0 1846681009 433225728 102297 4294967295 134512640 135094434 3221224432 3221223088 134550399 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105768 102297 145 145 0 105623 0
[pid=15427] vsize: 423072
Current children cumulated CPU time (s) 366.78
Current children cumulated vsize (Kb) 425196

[startup+380.043 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128169 0 0 0 37250 427 0 0 25 0 1 0 1846681009 433233920 102299 4294967295 134512640 135094434 3221224432 3221223088 134557829 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105770 102299 145 145 0 105625 0
[pid=15427] vsize: 423080
Current children cumulated CPU time (s) 376.78
Current children cumulated vsize (Kb) 425204

[startup+390.043 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128173 0 0 0 38251 427 0 0 25 0 1 0 1846681009 433238016 102303 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105771 102303 145 145 0 105626 0
[pid=15427] vsize: 423084
Current children cumulated CPU time (s) 386.79
Current children cumulated vsize (Kb) 425208

[startup+400.044 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128175 0 0 0 39251 427 0 0 25 0 1 0 1846681009 433246208 102305 4294967295 134512640 135094434 3221224432 3221223044 134563069 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105773 102305 145 145 0 105628 0
[pid=15427] vsize: 423092
Current children cumulated CPU time (s) 396.79
Current children cumulated vsize (Kb) 425216

[startup+410.045 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128178 0 0 0 40251 427 0 0 25 0 1 0 1846681009 433254400 102308 4294967295 134512640 135094434 3221224432 3221223084 134561534 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105775 102308 145 145 0 105630 0
[pid=15427] vsize: 423100
Current children cumulated CPU time (s) 406.79
Current children cumulated vsize (Kb) 425224

[startup+420.046 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128180 0 0 0 41251 427 0 0 25 0 1 0 1846681009 433262592 102310 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105777 102310 145 145 0 105632 0
[pid=15427] vsize: 423108
Current children cumulated CPU time (s) 416.79
Current children cumulated vsize (Kb) 425232

[startup+430.047 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128183 0 0 0 42251 427 0 0 25 0 1 0 1846681009 433274880 102313 4294967295 134512640 135094434 3221224432 3221223136 134554553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105780 102313 145 145 0 105635 0
[pid=15427] vsize: 423120
Current children cumulated CPU time (s) 426.79
Current children cumulated vsize (Kb) 425244

[startup+440.049 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128187 0 0 0 43252 427 0 0 25 0 1 0 1846681009 433291264 102317 4294967295 134512640 135094434 3221224432 3221223044 134563041 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105784 102317 145 145 0 105639 0
[pid=15427] vsize: 423136
Current children cumulated CPU time (s) 436.8
Current children cumulated vsize (Kb) 425260

[startup+450.049 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128193 0 0 0 44252 427 0 0 25 0 1 0 1846681009 433311744 102323 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105789 102323 145 145 0 105644 0
[pid=15427] vsize: 423156
Current children cumulated CPU time (s) 446.8
Current children cumulated vsize (Kb) 425280

[startup+460.05 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128215 0 0 0 45252 427 0 0 25 0 1 0 1846681009 433446912 102345 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105822 102345 145 145 0 105677 0
[pid=15427] vsize: 423288
Current children cumulated CPU time (s) 456.8
Current children cumulated vsize (Kb) 425412

[startup+470.052 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128217 0 0 0 46251 428 0 0 25 0 1 0 1846681009 433451008 102347 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105823 102347 145 145 0 105678 0
[pid=15427] vsize: 423292
Current children cumulated CPU time (s) 466.8
Current children cumulated vsize (Kb) 425416

[startup+480.053 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128219 0 0 0 47250 429 0 0 25 0 1 0 1846681009 433459200 102349 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105825 102349 145 145 0 105680 0
[pid=15427] vsize: 423300
Current children cumulated CPU time (s) 476.8
Current children cumulated vsize (Kb) 425424

[startup+490.055 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128229 0 0 0 48250 429 0 0 25 0 1 0 1846681009 433496064 102359 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105834 102359 145 145 0 105689 0
[pid=15427] vsize: 423336
Current children cumulated CPU time (s) 486.8
Current children cumulated vsize (Kb) 425460

[startup+500.056 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128236 0 0 0 49250 430 0 0 25 0 1 0 1846681009 433524736 102366 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105841 102366 145 145 0 105696 0
[pid=15427] vsize: 423364
Current children cumulated CPU time (s) 496.81
Current children cumulated vsize (Kb) 425488

[startup+510.056 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128247 0 0 0 50250 430 0 0 25 0 1 0 1846681009 433565696 102377 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105851 102377 145 145 0 105706 0
[pid=15427] vsize: 423404
Current children cumulated CPU time (s) 506.81
Current children cumulated vsize (Kb) 425528

[startup+520.058 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128254 0 0 0 51250 430 0 0 25 0 1 0 1846681009 433594368 102384 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105858 102384 145 145 0 105713 0
[pid=15427] vsize: 423432
Current children cumulated CPU time (s) 516.81
Current children cumulated vsize (Kb) 425556

[startup+530.059 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128264 0 0 0 52250 430 0 0 25 0 1 0 1846681009 433631232 102394 4294967295 134512640 135094434 3221224432 3221223184 134559282 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105867 102394 145 145 0 105722 0
[pid=15427] vsize: 423468
Current children cumulated CPU time (s) 526.81
Current children cumulated vsize (Kb) 425592

[startup+540.061 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128323 0 0 0 53249 431 0 0 25 0 1 0 1846681009 433831936 102453 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105916 102453 145 145 0 105771 0
[pid=15427] vsize: 423664
Current children cumulated CPU time (s) 536.81
Current children cumulated vsize (Kb) 425788

[startup+550.063 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128326 0 0 0 54249 431 0 0 25 0 1 0 1846681009 433844224 102456 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105919 102456 145 145 0 105774 0
[pid=15427] vsize: 423676
Current children cumulated CPU time (s) 546.81
Current children cumulated vsize (Kb) 425800

[startup+560.064 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128329 0 0 0 55249 431 0 0 25 0 1 0 1846681009 433856512 102459 4294967295 134512640 135094434 3221224432 3221223044 134563094 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105922 102459 145 145 0 105777 0
[pid=15427] vsize: 423688
Current children cumulated CPU time (s) 556.81
Current children cumulated vsize (Kb) 425812

[startup+570.064 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128334 0 0 0 56249 431 0 0 25 0 1 0 1846681009 433872896 102464 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105926 102464 145 145 0 105781 0
[pid=15427] vsize: 423704
Current children cumulated CPU time (s) 566.81
Current children cumulated vsize (Kb) 425828

[startup+580.065 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128341 0 0 0 57249 432 0 0 25 0 1 0 1846681009 433901568 102471 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105933 102471 145 145 0 105788 0
[pid=15427] vsize: 423732
Current children cumulated CPU time (s) 576.82
Current children cumulated vsize (Kb) 425856

[startup+590.067 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128348 0 0 0 58249 432 0 0 25 0 1 0 1846681009 433930240 102478 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105940 102478 145 145 0 105795 0
[pid=15427] vsize: 423760
Current children cumulated CPU time (s) 586.82
Current children cumulated vsize (Kb) 425884

[startup+600.068 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128357 0 0 0 59249 432 0 0 25 0 1 0 1846681009 433958912 102487 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105947 102487 145 145 0 105802 0
[pid=15427] vsize: 423788
Current children cumulated CPU time (s) 596.82
Current children cumulated vsize (Kb) 425912

[startup+610.069 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128385 0 0 0 60248 432 0 0 25 0 1 0 1846681009 434073600 102515 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105975 102515 145 145 0 105830 0
[pid=15427] vsize: 423900
Current children cumulated CPU time (s) 606.81
Current children cumulated vsize (Kb) 426024

[startup+620.071 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128390 0 0 0 61248 432 0 0 25 0 1 0 1846681009 434089984 102520 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105979 102520 145 145 0 105834 0
[pid=15427] vsize: 423916
Current children cumulated CPU time (s) 616.81
Current children cumulated vsize (Kb) 426040

[startup+630.071 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128398 0 0 0 62249 432 0 0 25 0 1 0 1846681009 434122752 102528 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105987 102528 145 145 0 105842 0
[pid=15427] vsize: 423948
Current children cumulated CPU time (s) 626.82
Current children cumulated vsize (Kb) 426072

[startup+640.073 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128409 0 0 0 63249 433 0 0 25 0 1 0 1846681009 434167808 102539 4294967295 134512640 135094434 3221224432 3221223084 134558036 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 105998 102539 145 145 0 105853 0
[pid=15427] vsize: 423992
Current children cumulated CPU time (s) 636.83
Current children cumulated vsize (Kb) 426116

[startup+650.074 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128416 0 0 0 64249 433 0 0 25 0 1 0 1846681009 434192384 102546 4294967295 134512640 135094434 3221224432 3221223072 134562131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106004 102546 145 145 0 105859 0
[pid=15427] vsize: 424016
Current children cumulated CPU time (s) 646.83
Current children cumulated vsize (Kb) 426140

[startup+660.075 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128432 0 0 0 65249 433 0 0 25 0 1 0 1846681009 434257920 102562 4294967295 134512640 135094434 3221224432 3221223044 134563061 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106020 102562 145 145 0 105875 0
[pid=15427] vsize: 424080
Current children cumulated CPU time (s) 656.83
Current children cumulated vsize (Kb) 426204

[startup+670.076 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128498 0 0 0 66248 433 0 0 25 0 1 0 1846681009 434520064 102628 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15427/statm): 106084 102628 145 145 0 105939 0
[pid=15427] vsize: 424336
Current children cumulated CPU time (s) 666.82
Current children cumulated vsize (Kb) 426460

[startup+680.076 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128505 0 0 0 67247 434 0 0 25 0 1 0 1846681009 434548736 102635 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106091 102635 145 145 0 105946 0
[pid=15427] vsize: 424364
Current children cumulated CPU time (s) 676.82
Current children cumulated vsize (Kb) 426488

[startup+690.077 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128514 0 0 0 68247 434 0 0 25 0 1 0 1846681009 434573312 102644 4294967295 134512640 135094434 3221224432 3221223072 134562057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106097 102644 145 145 0 105952 0
[pid=15427] vsize: 424388
Current children cumulated CPU time (s) 686.82
Current children cumulated vsize (Kb) 426512

[startup+700.078 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128517 0 0 0 69247 434 0 0 25 0 1 0 1846681009 434585600 102647 4294967295 134512640 135094434 3221224432 3221223088 134561502 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106100 102647 145 145 0 105955 0
[pid=15427] vsize: 424400
Current children cumulated CPU time (s) 696.82
Current children cumulated vsize (Kb) 426524

[startup+710.079 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128519 0 0 0 70247 434 0 0 25 0 1 0 1846681009 434593792 102649 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106102 102649 145 145 0 105957 0
[pid=15427] vsize: 424408
Current children cumulated CPU time (s) 706.82
Current children cumulated vsize (Kb) 426532

[startup+720.08 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128523 0 0 0 71248 434 0 0 25 0 1 0 1846681009 434601984 102653 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106104 102653 145 145 0 105959 0
[pid=15427] vsize: 424416
Current children cumulated CPU time (s) 716.83
Current children cumulated vsize (Kb) 426540

[startup+730.081 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128524 0 0 0 72248 434 0 0 25 0 1 0 1846681009 434606080 102654 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106105 102654 145 145 0 105960 0
[pid=15427] vsize: 424420
Current children cumulated CPU time (s) 726.83
Current children cumulated vsize (Kb) 426544

[startup+740.081 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128533 0 0 0 73248 434 0 0 25 0 1 0 1846681009 434642944 102663 4294967295 134512640 135094434 3221224432 3221223044 134563059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106114 102663 145 145 0 105969 0
[pid=15427] vsize: 424456
Current children cumulated CPU time (s) 736.83
Current children cumulated vsize (Kb) 426580

[startup+750.082 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128536 0 0 0 74248 434 0 0 25 0 1 0 1846681009 434655232 102666 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106117 102666 145 145 0 105972 0
[pid=15427] vsize: 424468
Current children cumulated CPU time (s) 746.83
Current children cumulated vsize (Kb) 426592

[startup+760.083 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128538 0 0 0 75248 434 0 0 25 0 1 0 1846681009 434663424 102668 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106119 102668 145 145 0 105974 0
[pid=15427] vsize: 424476
Current children cumulated CPU time (s) 756.83
Current children cumulated vsize (Kb) 426600

[startup+770.085 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128544 0 0 0 76248 434 0 0 25 0 1 0 1846681009 434683904 102674 4294967295 134512640 135094434 3221224432 3221223088 134557875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106124 102674 145 145 0 105979 0
[pid=15427] vsize: 424496
Current children cumulated CPU time (s) 766.83
Current children cumulated vsize (Kb) 426620

[startup+780.086 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128601 0 0 0 77248 435 0 0 25 0 1 0 1846681009 434913280 102731 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106180 102731 145 145 0 106035 0
[pid=15427] vsize: 424720
Current children cumulated CPU time (s) 776.84
Current children cumulated vsize (Kb) 426844

[startup+790.087 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128660 0 0 0 78247 435 0 0 25 0 1 0 1846681009 435150848 102790 4294967295 134512640 135094434 3221224432 3221223120 134554733 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106238 102790 145 145 0 106093 0
[pid=15427] vsize: 424952
Current children cumulated CPU time (s) 786.83
Current children cumulated vsize (Kb) 427076

[startup+800.088 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128667 0 0 0 79247 435 0 0 25 0 1 0 1846681009 435179520 102797 4294967295 134512640 135094434 3221224432 3221223088 134561463 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106245 102797 145 145 0 106100 0
[pid=15427] vsize: 424980
Current children cumulated CPU time (s) 796.83
Current children cumulated vsize (Kb) 427104

[startup+810.089 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128678 0 0 0 80247 436 0 0 25 0 1 0 1846681009 435224576 102808 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106256 102808 145 145 0 106111 0
[pid=15427] vsize: 425024
Current children cumulated CPU time (s) 806.84
Current children cumulated vsize (Kb) 427148

[startup+820.09 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128717 0 0 0 81247 436 0 0 25 0 1 0 1846681009 435511296 102847 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106326 102847 145 145 0 106181 0
[pid=15427] vsize: 425304
Current children cumulated CPU time (s) 816.84
Current children cumulated vsize (Kb) 427428

[startup+830.091 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128717 0 0 0 82247 436 0 0 25 0 1 0 1846681009 435511296 102847 4294967295 134512640 135094434 3221224432 3221223088 134561717 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106326 102847 145 145 0 106181 0
[pid=15427] vsize: 425304
Current children cumulated CPU time (s) 826.84
Current children cumulated vsize (Kb) 427428

[startup+840.092 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128717 0 0 0 83248 436 0 0 25 0 1 0 1846681009 435511296 102847 4294967295 134512640 135094434 3221224432 3221223088 134550375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106326 102847 145 145 0 106181 0
[pid=15427] vsize: 425304
Current children cumulated CPU time (s) 836.85
Current children cumulated vsize (Kb) 427428

[startup+850.092 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128718 0 0 0 84248 436 0 0 25 0 1 0 1846681009 435511296 102848 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106326 102848 145 145 0 106181 0
[pid=15427] vsize: 425304
Current children cumulated CPU time (s) 846.85
Current children cumulated vsize (Kb) 427428

[startup+860.093 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128718 0 0 0 85248 436 0 0 25 0 1 0 1846681009 435511296 102848 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106326 102848 145 145 0 106181 0
[pid=15427] vsize: 425304
Current children cumulated CPU time (s) 856.85
Current children cumulated vsize (Kb) 427428

[startup+870.095 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128719 0 0 0 86248 436 0 0 25 0 1 0 1846681009 435511296 102849 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106326 102849 145 145 0 106181 0
[pid=15427] vsize: 425304
Current children cumulated CPU time (s) 866.85
Current children cumulated vsize (Kb) 427428

[startup+880.096 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128720 0 0 0 87248 436 0 0 25 0 1 0 1846681009 435511296 102850 4294967295 134512640 135094434 3221224432 3221223088 134557795 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106326 102850 145 145 0 106181 0
[pid=15427] vsize: 425304
Current children cumulated CPU time (s) 876.85
Current children cumulated vsize (Kb) 427428

[startup+890.097 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128721 0 0 0 88249 436 0 0 25 0 1 0 1846681009 435515392 102851 4294967295 134512640 135094434 3221224432 3221223044 134563104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106327 102851 145 145 0 106182 0
[pid=15427] vsize: 425308
Current children cumulated CPU time (s) 886.86
Current children cumulated vsize (Kb) 427432

[startup+900.098 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128724 0 0 0 89249 436 0 0 25 0 1 0 1846681009 435527680 102854 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106330 102854 145 145 0 106185 0
[pid=15427] vsize: 425320
Current children cumulated CPU time (s) 896.86
Current children cumulated vsize (Kb) 427444

[startup+910.098 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128729 0 0 0 90249 436 0 0 25 0 1 0 1846681009 435548160 102859 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106335 102859 145 145 0 106190 0
[pid=15427] vsize: 425340
Current children cumulated CPU time (s) 906.86
Current children cumulated vsize (Kb) 427464

[startup+920.099 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128746 0 0 0 91249 436 0 0 25 0 1 0 1846681009 435613696 102876 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106351 102876 145 145 0 106206 0
[pid=15427] vsize: 425404
Current children cumulated CPU time (s) 916.86
Current children cumulated vsize (Kb) 427528

[startup+930.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128772 0 0 0 92249 437 0 0 25 0 1 0 1846681009 435720192 102902 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106377 102902 145 145 0 106232 0
[pid=15427] vsize: 425508
Current children cumulated CPU time (s) 926.87
Current children cumulated vsize (Kb) 427632

[startup+940.101 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128806 0 0 0 93248 437 0 0 25 0 1 0 1846681009 435855360 102936 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106410 102936 145 145 0 106265 0
[pid=15427] vsize: 425640
Current children cumulated CPU time (s) 936.86
Current children cumulated vsize (Kb) 427764

[startup+950.102 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128830 0 0 0 94248 437 0 0 25 0 1 0 1846681009 435949568 102960 4294967295 134512640 135094434 3221224432 3221223072 134562088 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106433 102960 145 145 0 106288 0
[pid=15427] vsize: 425732
Current children cumulated CPU time (s) 946.86
Current children cumulated vsize (Kb) 427856

[startup+960.103 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128854 0 0 0 95248 438 0 0 25 0 1 0 1846681009 436047872 102984 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106457 102984 145 145 0 106312 0
[pid=15427] vsize: 425828
Current children cumulated CPU time (s) 956.87
Current children cumulated vsize (Kb) 427952

[startup+970.104 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128873 0 0 0 96248 438 0 0 25 0 1 0 1846681009 436121600 103003 4294967295 134512640 135094434 3221224432 3221223044 134563039 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106475 103003 145 145 0 106330 0
[pid=15427] vsize: 425900
Current children cumulated CPU time (s) 966.87
Current children cumulated vsize (Kb) 428024

[startup+980.105 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 128979 0 0 0 97245 439 0 0 25 0 1 0 1846681009 436547584 103109 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15427/statm): 106579 103109 145 145 0 106434 0
[pid=15427] vsize: 426316
Current children cumulated CPU time (s) 976.85
Current children cumulated vsize (Kb) 428440

[startup+990.106 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129069 0 0 0 98243 440 0 0 25 0 1 0 1846681009 436903936 103199 4294967295 134512640 135094434 3221224432 3221223088 134561463 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106666 103199 145 145 0 106521 0
[pid=15427] vsize: 426664
Current children cumulated CPU time (s) 986.84
Current children cumulated vsize (Kb) 428788

[startup+1000.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129084 0 0 0 99243 440 0 0 25 0 1 0 1846681009 436965376 103214 4294967295 134512640 135094434 3221224432 3221223064 134562981 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106681 103214 145 145 0 106536 0
[pid=15427] vsize: 426724
Current children cumulated CPU time (s) 996.84
Current children cumulated vsize (Kb) 428848

[startup+1010.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129090 0 0 0 100243 440 0 0 25 0 1 0 1846681009 436989952 103220 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106687 103220 145 145 0 106542 0
[pid=15427] vsize: 426748
Current children cumulated CPU time (s) 1006.84
Current children cumulated vsize (Kb) 428872

[startup+1020.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129106 0 0 0 101243 440 0 0 25 0 1 0 1846681009 437055488 103236 4294967295 134512640 135094434 3221224432 3221223088 134562165 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106703 103236 145 145 0 106558 0
[pid=15427] vsize: 426812
Current children cumulated CPU time (s) 1016.84
Current children cumulated vsize (Kb) 428936

[startup+1030.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129116 0 0 0 102243 440 0 0 25 0 1 0 1846681009 437092352 103246 4294967295 134512640 135094434 3221224432 3221223136 134554538 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106712 103246 145 145 0 106567 0
[pid=15427] vsize: 426848
Current children cumulated CPU time (s) 1026.84
Current children cumulated vsize (Kb) 428972

[startup+1040.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129137 0 0 0 103243 440 0 0 25 0 1 0 1846681009 437178368 103267 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106733 103267 145 145 0 106588 0
[pid=15427] vsize: 426932
Current children cumulated CPU time (s) 1036.84
Current children cumulated vsize (Kb) 429056

[startup+1050.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129174 0 0 0 104242 441 0 0 25 0 1 0 1846681009 437325824 103304 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106769 103304 145 145 0 106624 0
[pid=15427] vsize: 427076
Current children cumulated CPU time (s) 1046.84
Current children cumulated vsize (Kb) 429200

[startup+1060.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129202 0 0 0 105242 441 0 0 25 0 1 0 1846681009 437440512 103332 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106797 103332 145 145 0 106652 0
[pid=15427] vsize: 427188
Current children cumulated CPU time (s) 1056.84
Current children cumulated vsize (Kb) 429312

[startup+1070.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129221 0 0 0 106242 441 0 0 25 0 1 0 1846681009 437518336 103351 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106816 103351 145 145 0 106671 0
[pid=15427] vsize: 427264
Current children cumulated CPU time (s) 1066.84
Current children cumulated vsize (Kb) 429388

[startup+1080.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129238 0 0 0 107240 443 0 0 25 0 1 0 1846681009 437583872 103368 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106832 103368 145 145 0 106687 0
[pid=15427] vsize: 427328
Current children cumulated CPU time (s) 1076.84
Current children cumulated vsize (Kb) 429452

[startup+1090.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129253 0 0 0 108240 443 0 0 25 0 1 0 1846681009 437645312 103383 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106847 103383 145 145 0 106702 0
[pid=15427] vsize: 427388
Current children cumulated CPU time (s) 1086.84
Current children cumulated vsize (Kb) 429512

[startup+1100.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129265 0 0 0 109239 444 0 0 25 0 1 0 1846681009 437694464 103395 4294967295 134512640 135094434 3221224432 3221223044 134563087 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106859 103395 145 145 0 106714 0
[pid=15427] vsize: 427436
Current children cumulated CPU time (s) 1096.84
Current children cumulated vsize (Kb) 429560

[startup+1110.12 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129283 0 0 0 110239 444 0 0 25 0 1 0 1846681009 437764096 103413 4294967295 134512640 135094434 3221224432 3221223088 134557798 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106876 103413 145 145 0 106731 0
[pid=15427] vsize: 427504
Current children cumulated CPU time (s) 1106.84
Current children cumulated vsize (Kb) 429628

[startup+1120.12 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129302 0 0 0 111239 444 0 0 25 0 1 0 1846681009 437841920 103432 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106895 103432 145 145 0 106750 0
[pid=15427] vsize: 427580
Current children cumulated CPU time (s) 1116.84
Current children cumulated vsize (Kb) 429704

[startup+1130.12 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129319 0 0 0 112239 444 0 0 25 0 1 0 1846681009 437911552 103449 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106912 103449 145 145 0 106767 0
[pid=15427] vsize: 427648
Current children cumulated CPU time (s) 1126.84
Current children cumulated vsize (Kb) 429772

[startup+1140.12 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129330 0 0 0 113239 445 0 0 25 0 1 0 1846681009 437952512 103460 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106922 103460 145 145 0 106777 0
[pid=15427] vsize: 427688
Current children cumulated CPU time (s) 1136.85
Current children cumulated vsize (Kb) 429812

[startup+1150.12 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129337 0 0 0 114239 445 0 0 25 0 1 0 1846681009 437985280 103467 4294967295 134512640 135094434 3221224432 3221223084 134561527 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106930 103467 145 145 0 106785 0
[pid=15427] vsize: 427720
Current children cumulated CPU time (s) 1146.85
Current children cumulated vsize (Kb) 429844

[startup+1160.12 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129340 0 0 0 115239 445 0 0 25 0 1 0 1846681009 437997568 103470 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106933 103470 145 145 0 106788 0
[pid=15427] vsize: 427732
Current children cumulated CPU time (s) 1156.85
Current children cumulated vsize (Kb) 429856

[startup+1170.12 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129345 0 0 0 116239 445 0 0 25 0 1 0 1846681009 438018048 103475 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106938 103475 145 145 0 106793 0
[pid=15427] vsize: 427752
Current children cumulated CPU time (s) 1166.85
Current children cumulated vsize (Kb) 429876

[startup+1180.12 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129352 0 0 0 117239 445 0 0 25 0 1 0 1846681009 438046720 103482 4294967295 134512640 135094434 3221224432 3221223088 134561482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106945 103482 145 145 0 106800 0
[pid=15427] vsize: 427780
Current children cumulated CPU time (s) 1176.85
Current children cumulated vsize (Kb) 429904

[startup+1190.12 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129359 0 0 0 118239 445 0 0 25 0 1 0 1846681009 438071296 103489 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106951 103489 145 145 0 106806 0
[pid=15427] vsize: 427804
Current children cumulated CPU time (s) 1186.85
Current children cumulated vsize (Kb) 429928

[startup+1200.12 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129382 0 0 0 119238 446 0 0 25 0 1 0 1846681009 438165504 103512 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106974 103512 145 145 0 106829 0
[pid=15427] vsize: 427896
Current children cumulated CPU time (s) 1196.85
Current children cumulated vsize (Kb) 430020

[startup+1210.12 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129393 0 0 0 120238 446 0 0 25 0 1 0 1846681009 438210560 103523 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106985 103523 145 145 0 106840 0
[pid=15427] vsize: 427940
Current children cumulated CPU time (s) 1206.85
Current children cumulated vsize (Kb) 430064



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.12 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15427
Raw data (/proc/15423/stat): 15423 (minisat+_script) S 15422 15423 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846681004 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15423/statm): 531 226 485 147 0 384 0
[pid=15423] vsize: 2124
Raw data (/proc/15427/stat): 15427 (minisat+_64-bit) R 15423 15423 28974 0 -1 0 129393 0 0 0 120238 446 0 0 25 0 1 0 1846681009 438210560 103523 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15427/statm): 106985 103523 145 145 0 106840 0
[pid=15427] vsize: 427940
Current children cumulated CPU time (s) 1206.85
Current children cumulated vsize (Kb) 430064

Sending SIGTERM to -15423
Sleeping 2 seconds
One traced child (pid=15423) ended because it received signal 15 (SIGTERM)
One traced child (pid=15427) exited with status: 10
All traced children have exited ! Game is over.

Child status: 10
Real time (s): 1210.51
CPU time (s): 1207.18
CPU user time (s): 1202.49
CPU system time (s): 4.69029
CPU usage (%): 99.7248
Max. virtual memory (cumulated for all children) (Kb): 430064

Verifier Data

ERROR: no interpretation found !