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-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-nw04.opb
MD5SUMa5c401bba5afccf02c7b40cb1c595b15
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 31302
Optimality of the best value was proved NO
Number of terms in the objective function 87482
Biggest coefficient in the objective function 5220
Number of bits for the biggest coefficient in the objective function 13
Sum of the numbers in the objective function 120189580
Number of bits of the sum of numbers in the objective function 27
Biggest number in a constraint 5220
Number of bits of the biggest number in a constraint 13
Biggest sum of numbers in a constraint 120189580
Number of bits of the biggest sum of numbers27
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1235.66
Number of variables87482
Total number of constraints87518
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)87518
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint1
Maximum length of a constraint42032

Trace number 6221

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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:        854192 kB
Buffers:         11000 kB
Cached:         139684 kB
SwapCached:       1160 kB
Active:          56860 kB
Inactive:        96452 kB
HighTotal:      131008 kB
HighFree:         7952 kB
LowTotal:       903652 kB
LowFree:        846240 kB
SwapTotal:     2097136 kB
SwapFree:      2095268 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5764 kB
Slab:            21280 kB
Committed_AS:    92628 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 04:51:15 (client local time) WITH STATUS 0 IN 1209.03 SECONDS
stats: 3378 7 1209.03 0

Solver Data



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/21519/stat): 21519 (minisat+_script) R 21518 21519 10120 0 -1 0 18 0 0 0 0 0 0 0 21 0 1 0 1740590615 712704 3 4294967295 134512640 135087896 3221221664 3221221664 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/21519/statm): 174 3 169 147 0 27 0
[pid=21519] vsize: 696
open syscall for file /etc/ld.so.preload
open syscall for file /usr/local/intel-8.0-20031016/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /usr/local/intel-8.0-20031016/lib/tls/i686/libtermcap.so.2
open syscall for file /usr/local/intel-8.0-20031016/lib/tls/mmx/libtermcap.so.2
open syscall for file /usr/local/intel-8.0-20031016/lib/tls/libtermcap.so.2
open syscall for file /usr/local/intel-8.0-20031016/lib/i686/mmx/libtermcap.so.2
open syscall for file /usr/local/intel-8.0-20031016/lib/i686/libtermcap.so.2
open syscall for file /usr/local/intel-8.0-20031016/lib/mmx/libtermcap.so.2
open syscall for file /usr/local/intel-8.0-20031016/lib/libtermcap.so.2
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/i686/libtermcap.so.2
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/mmx/libtermcap.so.2
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/libtermcap.so.2
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/i686/mmx/libtermcap.so.2
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/i686/libtermcap.so.2
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/mmx/libtermcap.so.2
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/libtermcap.so.2
open syscall for file /usr/local/globus-2.4.3/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /usr/local/globus-2.4.3/lib/tls/i686/libtermcap.so.2
open syscall for file /usr/local/globus-2.4.3/lib/tls/mmx/libtermcap.so.2
open syscall for file /usr/local/globus-2.4.3/lib/tls/libtermcap.so.2
open syscall for file /usr/local/globus-2.4.3/lib/i686/mmx/libtermcap.so.2
open syscall for file /usr/local/globus-2.4.3/lib/i686/libtermcap.so.2
open syscall for file /usr/local/globus-2.4.3/lib/mmx/libtermcap.so.2
open syscall for file /usr/local/globus-2.4.3/lib/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 /usr/local/intel-8.0-20031016/lib/libdl.so.2
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/libdl.so.2
open syscall for file /usr/local/globus-2.4.3/lib/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 /usr/local/intel-8.0-20031016/lib/libc.so.6
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/libc.so.6
open syscall for file /usr/local/globus-2.4.3/lib/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 /usr/lib/locale/locale-archive
open syscall for file /etc/mtab
open syscall for file /proc/meminfo
open syscall for file /oldhome/oroussel/solvers/minisat+_script
open syscall for file /usr/lib/gconv/gconv-modules.cache
New process pid=21520
New process pid=21521
New process pid=21522
execve syscall for /bin/sed executable
One traced child (pid=21521) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file /usr/local/intel-8.0-20031016/lib/tls/i686/mmx/libc.so.6
open syscall for file /usr/local/intel-8.0-20031016/lib/tls/i686/libc.so.6
open syscall for file /usr/local/intel-8.0-20031016/lib/tls/mmx/libc.so.6
open syscall for file /usr/local/intel-8.0-20031016/lib/tls/libc.so.6
open syscall for file /usr/local/intel-8.0-20031016/lib/i686/mmx/libc.so.6
open syscall for file /usr/local/intel-8.0-20031016/lib/i686/libc.so.6
open syscall for file /usr/local/intel-8.0-20031016/lib/mmx/libc.so.6
open syscall for file /usr/local/intel-8.0-20031016/lib/libc.so.6
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/i686/mmx/libc.so.6
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/i686/libc.so.6
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/mmx/libc.so.6
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/libc.so.6
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/i686/mmx/libc.so.6
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/i686/libc.so.6
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/mmx/libc.so.6
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/libc.so.6
open syscall for file /usr/local/globus-2.4.3/lib/tls/i686/mmx/libc.so.6
open syscall for file /usr/local/globus-2.4.3/lib/tls/i686/libc.so.6
open syscall for file /usr/local/globus-2.4.3/lib/tls/mmx/libc.so.6
open syscall for file /usr/local/globus-2.4.3/lib/tls/libc.so.6
open syscall for file /usr/local/globus-2.4.3/lib/i686/mmx/libc.so.6
open syscall for file /usr/local/globus-2.4.3/lib/i686/libc.so.6
open syscall for file /usr/local/globus-2.4.3/lib/mmx/libc.so.6
open syscall for file /usr/local/globus-2.4.3/lib/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
open syscall for file /usr/lib/locale/locale-archive
open syscall for file /usr/lib/gconv/gconv-modules.cache
One traced child (pid=21522) exited with status: 0
One traced child (pid=21520) exited with status: 0
New process pid=21523
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-nw04.opb

[startup+10.003 s]
Raw data (loadavg): 0.94 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 27405 0 0 0 817 103 0 0 25 0 1 0 1740590622 71360512 6804 4294967295 134512640 135094434 3221221600 3221216416 134591084 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21523/statm): 17422 6804 145 145 0 17277 0
[pid=21523] vsize: 69688
Current children cumulated CPU time (s) 9.21
Current children cumulated vsize (Kb) 73884

[startup+20.0048 s]
Raw data (loadavg): 0.95 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 32927 0 0 0 1783 121 0 0 25 0 1 0 1740590622 84217856 8555 4294967295 134512640 135094434 3221221600 3220323968 134596863 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21523/statm): 20561 8555 145 145 0 20416 0
[pid=21523] vsize: 82244
Current children cumulated CPU time (s) 19.05
Current children cumulated vsize (Kb) 86440

[startup+30.0056 s]
Raw data (loadavg): 0.95 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 32927 0 0 0 2783 121 0 0 25 0 1 0 1740590622 84217856 8555 4294967295 134512640 135094434 3221221600 3221181440 134597094 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21523/statm): 20561 8555 145 145 0 20416 0
[pid=21523] vsize: 82244
Current children cumulated CPU time (s) 29.05
Current children cumulated vsize (Kb) 86440

[startup+40.0064 s]
Raw data (loadavg): 0.96 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 33257 0 0 0 3783 122 0 0 25 0 1 0 1740590622 85569536 8885 4294967295 134512640 135094434 3221221600 3220883648 134597026 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21523/statm): 20891 8885 145 145 0 20746 0
[pid=21523] vsize: 83564
Current children cumulated CPU time (s) 39.06
Current children cumulated vsize (Kb) 87760

[startup+50.0082 s]
Raw data (loadavg): 0.97 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 33283 0 0 0 4782 122 0 0 25 0 1 0 1740590622 85676032 8911 4294967295 134512640 135094434 3221221600 3220264128 134597026 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21523/statm): 20917 8911 145 145 0 20772 0
[pid=21523] vsize: 83668
Current children cumulated CPU time (s) 49.05
Current children cumulated vsize (Kb) 87864

[startup+60.009 s]
Raw data (loadavg): 0.97 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 34017 0 0 0 5781 123 0 0 25 0 1 0 1740590622 89980928 9645 4294967295 134512640 135094434 3221221600 3219769920 134597094 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21523/statm): 21968 9645 145 145 0 21823 0
[pid=21523] vsize: 87872
Current children cumulated CPU time (s) 59.05
Current children cumulated vsize (Kb) 92068

[startup+70.0097 s]
Raw data (loadavg): 0.98 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 34041 0 0 0 6781 124 0 0 25 0 1 0 1740590622 89980928 9669 4294967295 134512640 135094434 3221221600 3219690368 134596875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21523/statm): 21968 9669 145 145 0 21823 0
[pid=21523] vsize: 87872
Current children cumulated CPU time (s) 69.06
Current children cumulated vsize (Kb) 92068

[startup+80.0105 s]
Raw data (loadavg): 0.98 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 34744 0 0 0 7780 125 0 0 25 0 1 0 1740590622 91328512 10042 4294967295 134512640 135094434 3221221600 3220612784 134597017 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 22297 10042 145 145 0 22152 0
[pid=21523] vsize: 89188
Current children cumulated CPU time (s) 79.06
Current children cumulated vsize (Kb) 93384

[startup+90.0103 s]
Raw data (loadavg): 0.98 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 34831 0 0 0 8780 125 0 0 25 0 1 0 1740590622 91328512 10129 4294967295 134512640 135094434 3221221600 3219777840 134597094 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 22297 10129 145 145 0 22152 0
[pid=21523] vsize: 89188
Current children cumulated CPU time (s) 89.06
Current children cumulated vsize (Kb) 93384

[startup+100.011 s]
Raw data (loadavg): 0.98 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 34916 0 0 0 9780 126 0 0 25 0 1 0 1740590622 91328512 10214 4294967295 134512640 135094434 3221221600 3220044304 134597023 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 22297 10214 145 145 0 22152 0
[pid=21523] vsize: 89188
Current children cumulated CPU time (s) 99.07
Current children cumulated vsize (Kb) 93384

[startup+110.012 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 34935 0 0 0 10780 126 0 0 25 0 1 0 1740590622 91328512 10233 4294967295 134512640 135094434 3221221600 3218881648 134596852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 22297 10233 145 145 0 22152 0
[pid=21523] vsize: 89188
Current children cumulated CPU time (s) 109.07
Current children cumulated vsize (Kb) 93384

[startup+120.013 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 35057 0 0 0 11780 126 0 0 25 0 1 0 1740590622 94609408 10355 4294967295 134512640 135094434 3221221600 3220820640 134597091 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 23098 10355 145 145 0 22953 0
[pid=21523] vsize: 92392
Current children cumulated CPU time (s) 119.07
Current children cumulated vsize (Kb) 96588

[startup+130.013 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 35171 0 0 0 12779 126 0 0 25 0 1 0 1740590622 94990336 10469 4294967295 134512640 135094434 3221221600 3219231888 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 23191 10469 145 145 0 23046 0
[pid=21523] vsize: 92764
Current children cumulated CPU time (s) 129.06
Current children cumulated vsize (Kb) 96960

[startup+140.014 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 35437 0 0 0 13778 128 0 0 25 0 1 0 1740590622 95129600 10578 4294967295 134512640 135094434 3221221600 3220653792 134597094 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 23225 10578 145 145 0 23080 0
[pid=21523] vsize: 92900
Current children cumulated CPU time (s) 139.07
Current children cumulated vsize (Kb) 97096

[startup+150.015 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 35457 0 0 0 14778 128 0 0 25 0 1 0 1740590622 95174656 10598 4294967295 134512640 135094434 3221221600 3219106928 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 23236 10598 145 145 0 23091 0
[pid=21523] vsize: 92944
Current children cumulated CPU time (s) 149.07
Current children cumulated vsize (Kb) 97140

[startup+160.015 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 36358 0 0 0 15774 131 0 0 25 0 1 0 1740590622 97619968 11279 4294967295 134512640 135094434 3221221600 3218189616 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 23833 11279 145 145 0 23688 0
[pid=21523] vsize: 95332
Current children cumulated CPU time (s) 159.06
Current children cumulated vsize (Kb) 99528

[startup+170.016 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 37731 0 0 0 16770 135 0 0 25 0 1 0 1740590622 100433920 11993 4294967295 134512640 135094434 3221221600 3219790512 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 24520 11993 145 145 0 24375 0
[pid=21523] vsize: 98080
Current children cumulated CPU time (s) 169.06
Current children cumulated vsize (Kb) 102276

[startup+180.016 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 37879 0 0 0 17769 135 0 0 25 0 1 0 1740590622 100806656 12099 4294967295 134512640 135094434 3221221600 3220685120 134597084 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 24611 12099 145 145 0 24466 0
[pid=21523] vsize: 98444
Current children cumulated CPU time (s) 179.05
Current children cumulated vsize (Kb) 102640

[startup+190.016 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 37918 0 0 0 18768 136 0 0 25 0 1 0 1740590622 100929536 12138 4294967295 134512640 135094434 3221221600 3219863552 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 24641 12138 145 145 0 24496 0
[pid=21523] vsize: 98564
Current children cumulated CPU time (s) 189.05
Current children cumulated vsize (Kb) 102760

[startup+200.017 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 37918 0 0 0 19768 136 0 0 25 0 1 0 1740590622 100929536 12138 4294967295 134512640 135094434 3221221600 3219123472 134596857 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 24641 12138 145 145 0 24496 0
[pid=21523] vsize: 98564
Current children cumulated CPU time (s) 199.05
Current children cumulated vsize (Kb) 102760

[startup+210.017 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 37918 0 0 0 20769 136 0 0 25 0 1 0 1740590622 100929536 12138 4294967295 134512640 135094434 3221221600 3217729904 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 24641 12138 145 145 0 24496 0
[pid=21523] vsize: 98564
Current children cumulated CPU time (s) 209.06
Current children cumulated vsize (Kb) 102760

[startup+220.018 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 38288 0 0 0 21766 138 0 0 25 0 1 0 1740590622 101916672 12425 4294967295 134512640 135094434 3221221600 3219046032 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 24882 12425 145 145 0 24737 0
[pid=21523] vsize: 99528
Current children cumulated CPU time (s) 219.05
Current children cumulated vsize (Kb) 103724

[startup+230.018 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 38433 0 0 0 22765 139 0 0 25 0 1 0 1740590622 102375424 12570 4294967295 134512640 135094434 3221221600 3221029728 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 24994 12570 145 145 0 24849 0
[pid=21523] vsize: 99976
Current children cumulated CPU time (s) 229.05
Current children cumulated vsize (Kb) 104172

[startup+240.019 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 38628 0 0 0 23764 139 0 0 25 0 1 0 1740590622 101912576 12510 4294967295 134512640 135094434 3221221600 3219754432 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 24881 12510 145 145 0 24736 0
[pid=21523] vsize: 99524
Current children cumulated CPU time (s) 239.04
Current children cumulated vsize (Kb) 103720

[startup+250.02 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 38730 0 0 0 24764 140 0 0 25 0 1 0 1740590622 102080512 12570 4294967295 134512640 135094434 3221221600 3220870624 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 24922 12570 145 145 0 24777 0
[pid=21523] vsize: 99688
Current children cumulated CPU time (s) 249.05
Current children cumulated vsize (Kb) 103884

[startup+260.021 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 38736 0 0 0 25764 140 0 0 25 0 1 0 1740590622 102080512 12576 4294967295 134512640 135094434 3221221600 3220042896 134596860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 24922 12576 145 145 0 24777 0
[pid=21523] vsize: 99688
Current children cumulated CPU time (s) 259.05
Current children cumulated vsize (Kb) 103884

[startup+270.021 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 38736 0 0 0 26764 140 0 0 25 0 1 0 1740590622 102080512 12576 4294967295 134512640 135094434 3221221600 3218828144 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 24922 12576 145 145 0 24777 0
[pid=21523] vsize: 99688
Current children cumulated CPU time (s) 269.05
Current children cumulated vsize (Kb) 103884

[startup+280.022 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 39104 0 0 0 27762 141 0 0 25 0 1 0 1740590622 103030784 12861 4294967295 134512640 135094434 3221221600 3219998016 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 25154 12861 145 145 0 25009 0
[pid=21523] vsize: 100616
Current children cumulated CPU time (s) 279.04
Current children cumulated vsize (Kb) 104812

[startup+290.023 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 39355 0 0 0 28761 142 0 0 25 0 1 0 1740590622 102805504 12864 4294967295 134512640 135094434 3221221600 3219643376 134597046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 25099 12864 145 145 0 24954 0
[pid=21523] vsize: 100396
Current children cumulated CPU time (s) 289.04
Current children cumulated vsize (Kb) 104592

[startup+300.024 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 39379 0 0 0 29760 143 0 0 25 0 1 0 1740590622 102805504 12888 4294967295 134512640 135094434 3221221600 3221085344 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 25099 12888 145 145 0 24954 0
[pid=21523] vsize: 100396
Current children cumulated CPU time (s) 299.04
Current children cumulated vsize (Kb) 104592

[startup+310.025 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 39464 0 0 0 30760 143 0 0 25 0 1 0 1740590622 102973440 12931 4294967295 134512640 135094434 3221221600 3220053456 134596863 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 25140 12931 145 145 0 24995 0
[pid=21523] vsize: 100560
Current children cumulated CPU time (s) 309.04
Current children cumulated vsize (Kb) 104756

[startup+320.025 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 39646 0 0 0 31759 143 0 0 25 0 1 0 1740590622 103518208 13113 4294967295 134512640 135094434 3221221600 3220372720 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 25273 13113 145 145 0 25128 0
[pid=21523] vsize: 101092
Current children cumulated CPU time (s) 319.03
Current children cumulated vsize (Kb) 105288

[startup+330.026 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 40052 0 0 0 32757 144 0 0 25 0 1 0 1740590622 103546880 13179 4294967295 134512640 135094434 3221221600 3219261456 134597094 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 25280 13179 145 145 0 25135 0
[pid=21523] vsize: 101120
Current children cumulated CPU time (s) 329.02
Current children cumulated vsize (Kb) 105316

[startup+340.026 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 40163 0 0 0 33757 145 0 0 25 0 1 0 1740590622 103743488 13248 4294967295 134512640 135094434 3221221600 3220544320 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 25328 13248 145 145 0 25183 0
[pid=21523] vsize: 101312
Current children cumulated CPU time (s) 339.03
Current children cumulated vsize (Kb) 105508

[startup+350.027 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 40213 0 0 0 34758 145 0 0 25 0 1 0 1740590622 103899136 13298 4294967295 134512640 135094434 3221221600 3220210800 134596919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21523/statm): 25366 13298 145 145 0 25221 0
[pid=21523] vsize: 101464
Current children cumulated CPU time (s) 349.04
Current children cumulated vsize (Kb) 105660

[startup+360.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 40213 0 0 0 35757 145 0 0 25 0 1 0 1740590622 103899136 13298 4294967295 134512640 135094434 3221221600 3219317952 134596882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21523/statm): 25366 13298 145 145 0 25221 0
[pid=21523] vsize: 101464
Current children cumulated CPU time (s) 359.03
Current children cumulated vsize (Kb) 105660

[startup+370.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 40213 0 0 0 36757 145 0 0 25 0 1 0 1740590622 103899136 13298 4294967295 134512640 135094434 3221221600 3217227072 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 25366 13298 145 145 0 25221 0
[pid=21523] vsize: 101464
Current children cumulated CPU time (s) 369.03
Current children cumulated vsize (Kb) 105660

[startup+380.041 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 40676 0 0 0 37754 147 0 0 25 0 1 0 1740590622 111468544 13678 4294967295 134512640 135094434 3221221600 3220682128 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 27214 13678 145 145 0 27069 0
[pid=21523] vsize: 108856
Current children cumulated CPU time (s) 379.02
Current children cumulated vsize (Kb) 113052

[startup+390.042 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 40897 0 0 0 38753 148 0 0 25 0 1 0 1740590622 111087616 13640 4294967295 134512640 135094434 3221221600 3219287680 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 27121 13640 145 145 0 26976 0
[pid=21523] vsize: 108484
Current children cumulated CPU time (s) 389.02
Current children cumulated vsize (Kb) 112680

[startup+400.043 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 41001 0 0 0 39753 148 0 0 25 0 1 0 1740590622 111255552 13702 4294967295 134512640 135094434 3221221600 3220515280 134597012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 27162 13702 145 145 0 27017 0
[pid=21523] vsize: 108648
Current children cumulated CPU time (s) 399.02
Current children cumulated vsize (Kb) 112844

[startup+410.043 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 41019 0 0 0 40753 148 0 0 25 0 1 0 1740590622 111284224 13720 4294967295 134512640 135094434 3221221600 3220160992 134596919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 27169 13720 145 145 0 27024 0
[pid=21523] vsize: 108676
Current children cumulated CPU time (s) 409.02
Current children cumulated vsize (Kb) 112872

[startup+420.044 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 41019 0 0 0 41753 148 0 0 25 0 1 0 1740590622 111284224 13720 4294967295 134512640 135094434 3221221600 3219289264 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 27169 13720 145 145 0 27024 0
[pid=21523] vsize: 108676
Current children cumulated CPU time (s) 419.02
Current children cumulated vsize (Kb) 112872

[startup+430.045 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 41019 0 0 0 42753 148 0 0 25 0 1 0 1740590622 111284224 13720 4294967295 134512640 135094434 3221221600 3217196096 134596852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 27169 13720 145 145 0 27024 0
[pid=21523] vsize: 108676
Current children cumulated CPU time (s) 429.02
Current children cumulated vsize (Kb) 112872

[startup+440.045 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 41470 0 0 0 43750 150 0 0 25 0 1 0 1740590622 112521216 14088 4294967295 134512640 135094434 3221221600 3220410032 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 27471 14088 145 145 0 27326 0
[pid=21523] vsize: 109884
Current children cumulated CPU time (s) 439.01
Current children cumulated vsize (Kb) 114080

[startup+450.046 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 41705 0 0 0 44749 151 0 0 25 0 1 0 1740590622 112201728 14063 4294967295 134512640 135094434 3221221600 3218846800 134597053 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 27393 14063 145 145 0 27248 0
[pid=21523] vsize: 109572
Current children cumulated CPU time (s) 449.01
Current children cumulated vsize (Kb) 113768

[startup+460.046 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 41811 0 0 0 45749 151 0 0 25 0 1 0 1740590622 112369664 14127 4294967295 134512640 135094434 3221221600 3220237904 134597094 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 27434 14127 145 145 0 27289 0
[pid=21523] vsize: 109736
Current children cumulated CPU time (s) 459.01
Current children cumulated vsize (Kb) 113932

[startup+470.047 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 41825 0 0 0 46749 151 0 0 25 0 1 0 1740590622 112369664 14141 4294967295 134512640 135094434 3221221600 3221046624 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 27434 14141 145 145 0 27289 0
[pid=21523] vsize: 109736
Current children cumulated CPU time (s) 469.01
Current children cumulated vsize (Kb) 113932

[startup+480.048 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 41831 0 0 0 47749 151 0 0 25 0 1 0 1740590622 112381952 14147 4294967295 134512640 135094434 3221221600 3219668896 134596860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 27437 14147 145 145 0 27292 0
[pid=21523] vsize: 109748
Current children cumulated CPU time (s) 479.01
Current children cumulated vsize (Kb) 113944

[startup+490.048 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 41831 0 0 0 48749 151 0 0 25 0 1 0 1740590622 112381952 14147 4294967295 134512640 135094434 3221221600 3218660944 134596875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 27437 14147 145 145 0 27292 0
[pid=21523] vsize: 109748
Current children cumulated CPU time (s) 489.01
Current children cumulated vsize (Kb) 113944

[startup+500.049 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 41958 0 0 0 49748 152 0 0 25 0 1 0 1740590622 112783360 14274 4294967295 134512640 135094434 3221221600 3218179536 134519056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 27535 14274 145 145 0 27390 0
[pid=21523] vsize: 110140
Current children cumulated CPU time (s) 499.01
Current children cumulated vsize (Kb) 114336

[startup+510.049 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 42323 0 0 0 50746 154 0 0 25 0 1 0 1740590622 113754112 14556 4294967295 134512640 135094434 3221221600 3220942080 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 27772 14556 145 145 0 27627 0
[pid=21523] vsize: 111088
Current children cumulated CPU time (s) 509.01
Current children cumulated vsize (Kb) 115284

[startup+520.05 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 42530 0 0 0 51746 154 0 0 25 0 1 0 1740590622 113311744 14502 4294967295 134512640 135094434 3221221600 3219214464 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 27664 14502 145 145 0 27519 0
[pid=21523] vsize: 110656
Current children cumulated CPU time (s) 519.01
Current children cumulated vsize (Kb) 114852

[startup+530.051 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 42632 0 0 0 52746 154 0 0 25 0 1 0 1740590622 113479680 14562 4294967295 134512640 135094434 3221221600 3220360224 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 27705 14562 145 145 0 27560 0
[pid=21523] vsize: 110820
Current children cumulated CPU time (s) 529.01
Current children cumulated vsize (Kb) 115016

[startup+540.052 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 42646 0 0 0 53746 154 0 0 25 0 1 0 1740590622 113487872 14576 4294967295 134512640 135094434 3221221600 3221096784 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 27707 14576 145 145 0 27562 0
[pid=21523] vsize: 110828
Current children cumulated CPU time (s) 539.01
Current children cumulated vsize (Kb) 115024

[startup+550.053 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 42656 0 0 0 54746 154 0 0 25 0 1 0 1740590622 113520640 14586 4294967295 134512640 135094434 3221221600 3219497120 134596866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 27715 14586 145 145 0 27570 0
[pid=21523] vsize: 110860
Current children cumulated CPU time (s) 549.01
Current children cumulated vsize (Kb) 115056

[startup+560.053 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 42656 0 0 0 55746 154 0 0 25 0 1 0 1740590622 113520640 14586 4294967295 134512640 135094434 3221221600 3218532816 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 27715 14586 145 145 0 27570 0
[pid=21523] vsize: 110860
Current children cumulated CPU time (s) 559.01
Current children cumulated vsize (Kb) 115056

[startup+570.055 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 42759 0 0 0 56745 155 0 0 25 0 1 0 1740590622 113844224 14689 4294967295 134512640 135094434 3221221600 3217689024 134519056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 27794 14689 145 145 0 27649 0
[pid=21523] vsize: 111176
Current children cumulated CPU time (s) 569.01
Current children cumulated vsize (Kb) 115372

[startup+580.056 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 45782 0 0 0 57737 163 0 0 25 0 1 0 1740590622 120283136 16311 4294967295 134512640 135094434 3221221600 3220748480 134597017 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 29366 16311 145 145 0 29221 0
[pid=21523] vsize: 117464
Current children cumulated CPU time (s) 579.01
Current children cumulated vsize (Kb) 121660

[startup+590.056 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 46047 0 0 0 58736 163 0 0 25 0 1 0 1740590622 120041472 16313 4294967295 134512640 135094434 3221221600 3218824800 134597017 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 29307 16313 145 145 0 29162 0
[pid=21523] vsize: 117228
Current children cumulated CPU time (s) 589
Current children cumulated vsize (Kb) 121424

[startup+600.057 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 46151 0 0 0 59736 163 0 0 25 0 1 0 1740590622 120209408 16375 4294967295 134512640 135094434 3221221600 3220062080 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 29348 16375 145 145 0 29203 0
[pid=21523] vsize: 117392
Current children cumulated CPU time (s) 599
Current children cumulated vsize (Kb) 121588

[startup+610.058 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 46164 0 0 0 60736 164 0 0 25 0 1 0 1740590622 120213504 16388 4294967295 134512640 135094434 3221221600 3220819056 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 29349 16388 145 145 0 29204 0
[pid=21523] vsize: 117396
Current children cumulated CPU time (s) 609.01
Current children cumulated vsize (Kb) 121592

[startup+620.059 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 46194 0 0 0 61736 164 0 0 25 0 1 0 1740590622 120307712 16418 4294967295 134512640 135094434 3221221600 3219652704 134596919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 29372 16418 145 145 0 29227 0
[pid=21523] vsize: 117488
Current children cumulated CPU time (s) 619.01
Current children cumulated vsize (Kb) 121684

[startup+630.06 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 46194 0 0 0 62737 164 0 0 25 0 1 0 1740590622 120307712 16418 4294967295 134512640 135094434 3221221600 3218936736 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 29372 16418 145 145 0 29227 0
[pid=21523] vsize: 117488
Current children cumulated CPU time (s) 629.02
Current children cumulated vsize (Kb) 121684

[startup+640.061 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 46194 0 0 0 63736 164 0 0 25 0 1 0 1740590622 120307712 16418 4294967295 134512640 135094434 3221221600 3217919104 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 29372 16418 145 145 0 29227 0
[pid=21523] vsize: 117488
Current children cumulated CPU time (s) 639.01
Current children cumulated vsize (Kb) 121684

[startup+650.061 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 46525 0 0 0 64735 165 0 0 25 0 1 0 1740590622 121167872 16666 4294967295 134512640 135094434 3221221600 3218354176 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 29582 16666 145 145 0 29437 0
[pid=21523] vsize: 118328
Current children cumulated CPU time (s) 649.01
Current children cumulated vsize (Kb) 122524

[startup+660.062 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) T 21519 21519 10120 0 -1 0 46692 0 0 0 65734 165 0 0 25 0 1 0 1740590622 121696256 16833 4294967295 134512640 135094434 3221221600 3220655596 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/21523/statm): 29711 16833 145 145 0 29566 0
[pid=21523] vsize: 118844
Current children cumulated CPU time (s) 659
Current children cumulated vsize (Kb) 123040

[startup+670.064 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 47203 0 0 0 66733 166 0 0 25 0 1 0 1740590622 122441728 17069 4294967295 134512640 135094434 3221221600 3217617616 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 29893 17069 145 145 0 29748 0
[pid=21523] vsize: 119572
Current children cumulated CPU time (s) 669
Current children cumulated vsize (Kb) 123768

[startup+680.065 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 47307 0 0 0 67733 167 0 0 25 0 1 0 1740590622 122609664 17131 4294967295 134512640 135094434 3221221600 3218900656 134597094 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 29934 17131 145 145 0 29789 0
[pid=21523] vsize: 119736
Current children cumulated CPU time (s) 679.01
Current children cumulated vsize (Kb) 123932

[startup+690.064 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 47320 0 0 0 68733 167 0 0 25 0 1 0 1740590622 122609664 17144 4294967295 134512640 135094434 3221221600 3219685616 134597020 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 29934 17144 145 145 0 29789 0
[pid=21523] vsize: 119736
Current children cumulated CPU time (s) 689.01
Current children cumulated vsize (Kb) 123932

[startup+700.065 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 47340 0 0 0 69733 167 0 0 25 0 1 0 1740590622 122650624 17164 4294967295 134512640 135094434 3221221600 3220296512 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 29944 17164 145 145 0 29799 0
[pid=21523] vsize: 119776
Current children cumulated CPU time (s) 699.01
Current children cumulated vsize (Kb) 123972

[startup+710.066 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 47378 0 0 0 70733 167 0 0 25 0 1 0 1740590622 122769408 17202 4294967295 134512640 135094434 3221221600 3220815360 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 29973 17202 145 145 0 29828 0
[pid=21523] vsize: 119892
Current children cumulated CPU time (s) 709.01
Current children cumulated vsize (Kb) 124088

[startup+720.067 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 47408 0 0 0 71732 167 0 0 25 0 1 0 1740590622 122863616 17232 4294967295 134512640 135094434 3221221600 3219825360 134596872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 29996 17232 145 145 0 29851 0
[pid=21523] vsize: 119984
Current children cumulated CPU time (s) 719
Current children cumulated vsize (Kb) 124180

[startup+730.068 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 47408 0 0 0 72732 167 0 0 25 0 1 0 1740590622 122863616 17232 4294967295 134512640 135094434 3221221600 3218354000 134596919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 29996 17232 145 145 0 29851 0
[pid=21523] vsize: 119984
Current children cumulated CPU time (s) 729
Current children cumulated vsize (Kb) 124180

[startup+740.068 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 47408 0 0 0 73732 167 0 0 25 0 1 0 1740590622 122863616 17232 4294967295 134512640 135094434 3221221600 3217832512 134596875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 29996 17232 145 145 0 29851 0
[pid=21523] vsize: 119984
Current children cumulated CPU time (s) 739
Current children cumulated vsize (Kb) 124180

[startup+750.069 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 47408 0 0 0 74733 167 0 0 25 0 1 0 1740590622 122863616 17232 4294967295 134512640 135094434 3221221600 3217203312 134596866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 29996 17232 145 145 0 29851 0
[pid=21523] vsize: 119984
Current children cumulated CPU time (s) 749.01
Current children cumulated vsize (Kb) 124180

[startup+760.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 47408 0 0 0 75731 169 0 0 25 0 1 0 1740590622 122863616 17232 4294967295 134512640 135094434 3221221600 3215911824 134596885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 29996 17232 145 145 0 29851 0
[pid=21523] vsize: 119984
Current children cumulated CPU time (s) 759.01
Current children cumulated vsize (Kb) 124180

[startup+770.071 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 47688 0 0 0 76730 170 0 0 25 0 1 0 1740590622 123564032 17429 4294967295 134512640 135094434 3221221600 3216531520 134597046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 30167 17429 145 145 0 30022 0
[pid=21523] vsize: 120668
Current children cumulated CPU time (s) 769.01
Current children cumulated vsize (Kb) 124864

[startup+780.074 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 47899 0 0 0 77727 172 0 0 25 0 1 0 1740590622 124231680 17640 4294967295 134512640 135094434 3221221600 3219451360 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 30330 17640 145 145 0 30185 0
[pid=21523] vsize: 121320
Current children cumulated CPU time (s) 779
Current children cumulated vsize (Kb) 125516

[startup+790.074 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 47996 0 0 0 78726 172 0 0 25 0 1 0 1740590622 124538880 17737 4294967295 134512640 135094434 3221221600 3220778752 134597020 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 30405 17737 145 145 0 30260 0
[pid=21523] vsize: 121620
Current children cumulated CPU time (s) 788.99
Current children cumulated vsize (Kb) 125816

[startup+800.075 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 48285 0 0 0 79724 174 0 0 25 0 1 0 1740590622 124379136 17748 4294967295 134512640 135094434 3221221600 3217263328 134597094 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 30366 17748 145 145 0 30221 0
[pid=21523] vsize: 121464
Current children cumulated CPU time (s) 798.99
Current children cumulated vsize (Kb) 125660

[startup+810.076 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 48390 0 0 0 80724 174 0 0 25 0 1 0 1740590622 124547072 17811 4294967295 134512640 135094434 3221221600 3218602864 134597094 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 30407 17811 145 145 0 30262 0
[pid=21523] vsize: 121628
Current children cumulated CPU time (s) 808.99
Current children cumulated vsize (Kb) 125824

[startup+820.077 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 48404 0 0 0 81724 175 0 0 25 0 1 0 1740590622 124547072 17825 4294967295 134512640 135094434 3221221600 3219400672 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 30407 17825 145 145 0 30262 0
[pid=21523] vsize: 121628
Current children cumulated CPU time (s) 819
Current children cumulated vsize (Kb) 125824

[startup+830.078 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 48414 0 0 0 82724 175 0 0 25 0 1 0 1740590622 124547072 17835 4294967295 134512640 135094434 3221221600 3220016848 134597084 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 30407 17835 145 145 0 30262 0
[pid=21523] vsize: 121628
Current children cumulated CPU time (s) 829
Current children cumulated vsize (Kb) 125824

[startup+840.078 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 48423 0 0 0 83724 175 0 0 25 0 1 0 1740590622 124547072 17844 4294967295 134512640 135094434 3221221600 3220546256 134597043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 30407 17844 145 145 0 30262 0
[pid=21523] vsize: 121628
Current children cumulated CPU time (s) 839
Current children cumulated vsize (Kb) 125824

[startup+850.079 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 48433 0 0 0 84724 175 0 0 25 0 1 0 1740590622 124555264 17854 4294967295 134512640 135094434 3221221600 3221013536 134597020 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 30409 17854 145 145 0 30264 0
[pid=21523] vsize: 121636
Current children cumulated CPU time (s) 849
Current children cumulated vsize (Kb) 125832

[startup+860.08 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 48448 0 0 0 85724 175 0 0 25 0 1 0 1740590622 124604416 17869 4294967295 134512640 135094434 3221221600 3218671152 134596882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 30421 17869 145 145 0 30276 0
[pid=21523] vsize: 121684
Current children cumulated CPU time (s) 859
Current children cumulated vsize (Kb) 125880

[startup+870.081 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 48448 0 0 0 86724 175 0 0 25 0 1 0 1740590622 124604416 17869 4294967295 134512640 135094434 3221221600 3218033680 134596857 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 30421 17869 145 145 0 30276 0
[pid=21523] vsize: 121684
Current children cumulated CPU time (s) 869
Current children cumulated vsize (Kb) 125880

[startup+880.082 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 48448 0 0 0 87725 175 0 0 25 0 1 0 1740590622 124604416 17869 4294967295 134512640 135094434 3221221600 3217529440 134596875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 30421 17869 145 145 0 30276 0
[pid=21523] vsize: 121684
Current children cumulated CPU time (s) 879.01
Current children cumulated vsize (Kb) 125880

[startup+890.081 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 48448 0 0 0 88725 175 0 0 25 0 1 0 1740590622 124604416 17869 4294967295 134512640 135094434 3221221600 3216940720 134596866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 30421 17869 145 145 0 30276 0
[pid=21523] vsize: 121684
Current children cumulated CPU time (s) 889.01
Current children cumulated vsize (Kb) 125880

[startup+900.082 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 48448 0 0 0 89725 176 0 0 25 0 1 0 1740590622 124604416 17869 4294967295 134512640 135094434 3221221600 3215885600 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 30421 17869 145 145 0 30276 0
[pid=21523] vsize: 121684
Current children cumulated CPU time (s) 899.02
Current children cumulated vsize (Kb) 125880

[startup+910.083 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 48448 0 0 0 90725 176 0 0 25 0 1 0 1740590622 124604416 17869 4294967295 134512640 135094434 3221221600 3214942592 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 30421 17869 145 145 0 30276 0
[pid=21523] vsize: 121684
Current children cumulated CPU time (s) 909.02
Current children cumulated vsize (Kb) 125880

[startup+920.084 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 48909 0 0 0 91721 177 0 0 25 0 1 0 1740590622 125874176 18247 4294967295 134512640 135094434 3221221600 3218775168 134597046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21523/statm): 30731 18247 145 145 0 30586 0
[pid=21523] vsize: 122924
Current children cumulated CPU time (s) 918.99
Current children cumulated vsize (Kb) 127120

[startup+930.084 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 49020 0 0 0 92719 178 0 0 25 0 1 0 1740590622 126226432 18358 4294967295 134512640 135094434 3221221600 3220296336 134597091 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21523/statm): 30817 18358 145 145 0 30672 0
[pid=21523] vsize: 123268
Current children cumulated CPU time (s) 928.98
Current children cumulated vsize (Kb) 127464

[startup+940.084 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 49214 0 0 0 93717 179 0 0 25 0 1 0 1740590622 125927424 18317 4294967295 134512640 135094434 3221221600 3215933120 134597037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 30744 18317 145 145 0 30599 0
[pid=21523] vsize: 122976
Current children cumulated CPU time (s) 938.97
Current children cumulated vsize (Kb) 127172

[startup+950.085 s]
Raw data (loadavg): 0.99 0.98 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 49296 0 0 0 94717 179 0 0 25 0 1 0 1740590622 125931520 18358 4294967295 134512640 135094434 3221221600 3218367024 134597023 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 30745 18358 145 145 0 30600 0
[pid=21523] vsize: 122980
Current children cumulated CPU time (s) 948.97
Current children cumulated vsize (Kb) 127176

[startup+960.086 s]
Raw data (loadavg): 1.07 1.00 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 49395 0 0 0 95717 179 0 0 25 0 1 0 1740590622 126099456 18415 4294967295 134512640 135094434 3221221600 3219349104 134597094 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 30786 18415 145 145 0 30641 0
[pid=21523] vsize: 123144
Current children cumulated CPU time (s) 958.97
Current children cumulated vsize (Kb) 127340

[startup+970.087 s]
Raw data (loadavg): 1.06 1.00 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 49407 0 0 0 96717 179 0 0 25 0 1 0 1740590622 126099456 18427 4294967295 134512640 135094434 3221221600 3220036032 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 30786 18427 145 145 0 30641 0
[pid=21523] vsize: 123144
Current children cumulated CPU time (s) 968.97
Current children cumulated vsize (Kb) 127340

[startup+980.087 s]
Raw data (loadavg): 1.05 1.00 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 49416 0 0 0 97717 180 0 0 25 0 1 0 1740590622 126099456 18436 4294967295 134512640 135094434 3221221600 3220589728 134597020 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 30786 18436 145 145 0 30641 0
[pid=21523] vsize: 123144
Current children cumulated CPU time (s) 978.98
Current children cumulated vsize (Kb) 127340

[startup+990.087 s]
Raw data (loadavg): 1.04 1.00 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 49424 0 0 0 98717 180 0 0 25 0 1 0 1740590622 126099456 18444 4294967295 134512640 135094434 3221221600 3221065808 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 30786 18444 145 145 0 30641 0
[pid=21523] vsize: 123144
Current children cumulated CPU time (s) 988.98
Current children cumulated vsize (Kb) 127340

[startup+1000.09 s]
Raw data (loadavg): 1.04 1.00 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 49427 0 0 0 99717 180 0 0 25 0 1 0 1740590622 126099456 18447 4294967295 134512640 135094434 3221221600 3218588960 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 30786 18447 145 145 0 30641 0
[pid=21523] vsize: 123144
Current children cumulated CPU time (s) 998.98
Current children cumulated vsize (Kb) 127340

[startup+1010.09 s]
Raw data (loadavg): 1.03 1.00 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 49427 0 0 0 100718 180 0 0 25 0 1 0 1740590622 126099456 18447 4294967295 134512640 135094434 3221221600 3218106544 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 30786 18447 145 145 0 30641 0
[pid=21523] vsize: 123144
Current children cumulated CPU time (s) 1008.99
Current children cumulated vsize (Kb) 127340

[startup+1020.09 s]
Raw data (loadavg): 1.03 1.00 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 49427 0 0 0 101718 180 0 0 25 0 1 0 1740590622 126099456 18447 4294967295 134512640 135094434 3221221600 3217543520 134596875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 30786 18447 145 145 0 30641 0
[pid=21523] vsize: 123144
Current children cumulated CPU time (s) 1018.99
Current children cumulated vsize (Kb) 127340

[startup+1030.09 s]
Raw data (loadavg): 1.02 1.00 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 49427 0 0 0 102718 180 0 0 25 0 1 0 1740590622 126099456 18447 4294967295 134512640 135094434 3221221600 3216849024 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 30786 18447 145 145 0 30641 0
[pid=21523] vsize: 123144
Current children cumulated CPU time (s) 1028.99
Current children cumulated vsize (Kb) 127340

[startup+1040.09 s]
Raw data (loadavg): 1.02 1.00 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 49427 0 0 0 103718 180 0 0 25 0 1 0 1740590622 126099456 18447 4294967295 134512640 135094434 3221221600 3215536416 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 30786 18447 145 145 0 30641 0
[pid=21523] vsize: 123144
Current children cumulated CPU time (s) 1038.99
Current children cumulated vsize (Kb) 127340

[startup+1050.09 s]
Raw data (loadavg): 1.01 1.00 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 49819 0 0 0 104716 181 0 0 25 0 1 0 1740590622 127143936 18756 4294967295 134512640 135094434 3221221600 3218241536 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 31041 18756 145 145 0 30896 0
[pid=21523] vsize: 124164
Current children cumulated CPU time (s) 1048.98
Current children cumulated vsize (Kb) 128360

[startup+1060.09 s]
Raw data (loadavg): 1.01 1.00 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 49953 0 0 0 105715 182 0 0 25 0 1 0 1740590622 127565824 18890 4294967295 134512640 135094434 3221221600 3220075456 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 31144 18890 145 145 0 30999 0
[pid=21523] vsize: 124576
Current children cumulated CPU time (s) 1058.98
Current children cumulated vsize (Kb) 128772

[startup+1070.09 s]
Raw data (loadavg): 1.01 1.00 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 50034 0 0 0 106714 183 0 0 25 0 1 0 1740590622 127819776 18971 4294967295 134512640 135094434 3221221600 3221191648 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 31206 18971 145 145 0 31061 0
[pid=21523] vsize: 124824
Current children cumulated CPU time (s) 1068.98
Current children cumulated vsize (Kb) 129020

[startup+1080.09 s]
Raw data (loadavg): 1.01 1.00 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 50242 0 0 0 107713 183 0 0 25 0 1 0 1740590622 127324160 18903 4294967295 134512640 135094434 3221221600 3218166384 134597094 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 31085 18903 145 145 0 30940 0
[pid=21523] vsize: 124340
Current children cumulated CPU time (s) 1078.97
Current children cumulated vsize (Kb) 128536

[startup+1090.09 s]
Raw data (loadavg): 1.01 1.00 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 50342 0 0 0 108713 183 0 0 25 0 1 0 1740590622 127492096 18961 4294967295 134512640 135094434 3221221600 3219142480 134597029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 31126 18961 145 145 0 30981 0
[pid=21523] vsize: 124504
Current children cumulated CPU time (s) 1088.97
Current children cumulated vsize (Kb) 128700

[startup+1100.09 s]
Raw data (loadavg): 1.00 1.00 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 50353 0 0 0 109713 184 0 0 25 0 1 0 1740590622 127492096 18972 4294967295 134512640 135094434 3221221600 3219829584 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 31126 18972 145 145 0 30981 0
[pid=21523] vsize: 124504
Current children cumulated CPU time (s) 1098.98
Current children cumulated vsize (Kb) 128700

[startup+1110.1 s]
Raw data (loadavg): 1.00 1.00 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 50363 0 0 0 110713 184 0 0 25 0 1 0 1740590622 127492096 18982 4294967295 134512640 135094434 3221221600 3220402288 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 31126 18982 145 145 0 30981 0
[pid=21523] vsize: 124504
Current children cumulated CPU time (s) 1108.98
Current children cumulated vsize (Kb) 128700

[startup+1120.1 s]
Raw data (loadavg): 1.00 1.00 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 50371 0 0 0 111713 184 0 0 25 0 1 0 1740590622 127492096 18990 4294967295 134512640 135094434 3221221600 3220897552 134597094 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 31126 18990 145 145 0 30981 0
[pid=21523] vsize: 124504
Current children cumulated CPU time (s) 1118.98
Current children cumulated vsize (Kb) 128700

[startup+1130.1 s]
Raw data (loadavg): 1.00 1.00 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 50376 0 0 0 112714 184 0 0 25 0 1 0 1740590622 127492096 18995 4294967295 134512640 135094434 3221221600 3219208656 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 31126 18995 145 145 0 30981 0
[pid=21523] vsize: 124504
Current children cumulated CPU time (s) 1128.99
Current children cumulated vsize (Kb) 128700

[startup+1140.1 s]
Raw data (loadavg): 1.00 1.00 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 50376 0 0 0 113714 184 0 0 25 0 1 0 1740590622 127492096 18995 4294967295 134512640 135094434 3221221600 3218299968 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 31126 18995 145 145 0 30981 0
[pid=21523] vsize: 124504
Current children cumulated CPU time (s) 1138.99
Current children cumulated vsize (Kb) 128700

[startup+1150.1 s]
Raw data (loadavg): 1.00 1.00 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 50376 0 0 0 114714 184 0 0 25 0 1 0 1740590622 127492096 18995 4294967295 134512640 135094434 3221221600 3217768800 134596882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 31126 18995 145 145 0 30981 0
[pid=21523] vsize: 124504
Current children cumulated CPU time (s) 1148.99
Current children cumulated vsize (Kb) 128700

[startup+1160.1 s]
Raw data (loadavg): 1.00 1.00 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 50376 0 0 0 115714 184 0 0 25 0 1 0 1740590622 127492096 18995 4294967295 134512640 135094434 3221221600 3217111968 134596866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 31126 18995 145 145 0 30981 0
[pid=21523] vsize: 124504
Current children cumulated CPU time (s) 1158.99
Current children cumulated vsize (Kb) 128700

[startup+1170.1 s]
Raw data (loadavg): 1.00 1.00 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 50376 0 0 0 116714 184 0 0 25 0 1 0 1740590622 127492096 18995 4294967295 134512640 135094434 3221221600 3215913056 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 31126 18995 145 145 0 30981 0
[pid=21523] vsize: 124504
Current children cumulated CPU time (s) 1168.99
Current children cumulated vsize (Kb) 128700

[startup+1180.1 s]
Raw data (loadavg): 1.00 1.00 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 50440 0 0 0 117714 185 0 0 25 0 1 0 1740590622 127692800 19059 4294967295 134512640 135094434 3221221600 3215831568 134597037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 31175 19059 145 145 0 31030 0
[pid=21523] vsize: 124700
Current children cumulated CPU time (s) 1179
Current children cumulated vsize (Kb) 128896

[startup+1190.1 s]
Raw data (loadavg): 1.00 1.00 0.99 1/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) T 21519 21519 10120 0 -1 0 50869 0 0 0 118712 186 0 0 25 0 1 0 1740590622 128864256 19405 4294967295 134512640 135094434 3221221600 3219457740 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/21523/statm): 31461 19405 145 145 0 31316 0
[pid=21523] vsize: 125844
Current children cumulated CPU time (s) 1188.99
Current children cumulated vsize (Kb) 130040

[startup+1200.15 s]
Raw data (loadavg): 1.00 1.00 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 50964 0 0 0 119712 186 0 0 25 0 1 0 1740590622 129163264 19500 4294967295 134512640 135094434 3221221600 3220753232 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 31534 19500 145 145 0 31389 0
[pid=21523] vsize: 126136
Current children cumulated CPU time (s) 1198.99
Current children cumulated vsize (Kb) 130332

[startup+1210.15 s]
Raw data (loadavg): 1.00 1.00 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 51191 0 0 0 120711 187 0 0 25 0 1 0 1740590622 141348864 19451 4294967295 134512640 135094434 3221221600 3217427008 134597094 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 34509 19451 145 145 0 34364 0
[pid=21523] vsize: 138036
Current children cumulated CPU time (s) 1208.99
Current children cumulated vsize (Kb) 142232



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.15 s]
Raw data (loadavg): 1.00 1.00 0.99 2/56 21523
Raw data (/proc/21519/stat): 21519 (minisat+_script) S 21518 21519 10120 0 -1 0 322 277 0 0 0 0 0 1 20 0 1 0 1740590615 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21519/statm): 1049 256 1003 147 0 902 0
[pid=21519] vsize: 4196
Raw data (/proc/21523/stat): 21523 (minisat+_64-bit) R 21519 21519 10120 0 -1 0 51191 0 0 0 120711 187 0 0 25 0 1 0 1740590622 141348864 19451 4294967295 134512640 135094434 3221221600 3217427360 134597017 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21523/statm): 34509 19451 145 145 0 34364 0
[pid=21523] vsize: 138036
Current children cumulated CPU time (s) 1208.99
Current children cumulated vsize (Kb) 142232

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

Child status: 0
Real time (s): 1210.19
CPU time (s): 1209.03
CPU user time (s): 1207.12
CPU system time (s): 1.91571
CPU usage (%): 99.9042
Max. virtual memory (cumulated for all children) (Kb): 142232



Verifier Data




ERROR: no interpretation found !