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-blend2.opb
MD5SUMa940bff1d003826845b22f555cfd27b8
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 88
Biggest coefficient in the objective function 24014225
Number of bits for the biggest coefficient in the objective function 25
Sum of the numbers in the objective function 235593725
Number of bits of the sum of numbers in the objective function 28
Biggest number in a constraint 37203426086400
Number of bits of the biggest number in a constraint 46
Biggest sum of numbers in a constraint 1353236888971560
Number of bits of the biggest sum of numbers51
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables2061
Total number of constraints531
Number of constraints which are clauses9
Number of constraints which are cardinality constraints (but not clauses)310
Number of constraints which are nor clauses,nor cardinality constraints212
Minimum length of a constraint1
Maximum length of a constraint1776

Trace number 6183

Launcher Data

LAUNCH ON wulflinc1 THE 2005-09-20 04:10:40 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3347 boxname=wulflinc1 idbench=1003 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a940bff1d003826845b22f555cfd27b8  /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-blend2.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-blend2.opb
IDLAUNCH: 3347
/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:        874572 kB
Buffers:          9352 kB
Cached:         121680 kB
SwapCached:       1160 kB
Active:          40680 kB
Inactive:        92952 kB
HighTotal:      131008 kB
HighFree:        26068 kB
LowTotal:       903652 kB
LowFree:        848504 kB
SwapTotal:     2097136 kB
SwapFree:      2095268 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5764 kB
Slab:            20800 kB
Committed_AS:    92628 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 04:30:51 (client local time) WITH STATUS 0 IN 1205.58 SECONDS
stats: 3347 7 1205.58 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/21406/stat): 21406 (minisat+_script) R 21405 21406 10120 0 -1 0 18 0 0 0 0 0 0 0 23 0 1 0 1740468110 712704 3 4294967295 134512640 135087896 3221221664 3221221664 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/21406/statm): 174 3 169 147 0 27 0
[pid=21406] 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=21407
New process pid=21408
New process pid=21409
execve syscall for /bin/sed executable
One traced child (pid=21408) 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=21409) exited with status: 0
One traced child (pid=21407) exited with status: 0
New process pid=21410
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-blend2.opb

[startup+10.0032 s]
Raw data (loadavg): 0.93 1.03 0.99 1/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) T 21406 21406 10120 0 -1 0 37590 0 0 0 776 123 0 0 24 0 1 0 1740468116 111386624 26998 4294967295 134512640 135094434 3221221600 3220938604 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/21410/statm): 27194 26998 145 145 0 27049 0
[pid=21410] vsize: 108776
Current children cumulated CPU time (s) 9
Current children cumulated vsize (Kb) 112972

[startup+20.005 s]
Raw data (loadavg): 0.94 1.03 0.99 1/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) T 21406 21406 10120 0 -1 0 72626 0 0 0 1589 231 0 0 25 0 1 0 1740468116 211701760 51488 4294967295 134512640 135094434 3221221600 3220939308 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/21410/statm): 51685 51488 145 145 0 51540 0
[pid=21410] vsize: 206740
Current children cumulated CPU time (s) 18.21
Current children cumulated vsize (Kb) 210936

[startup+30.0058 s]
Raw data (loadavg): 0.95 1.03 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) T 21406 21406 10120 0 -1 0 87995 0 0 0 2436 293 0 0 25 0 1 0 1740468116 274235392 66774 4294967295 134512640 135094434 3221221600 3220942828 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/21410/statm): 66952 66774 145 145 0 66807 0
[pid=21410] vsize: 267808
Current children cumulated CPU time (s) 27.3
Current children cumulated vsize (Kb) 272004

[startup+40.0066 s]
Raw data (loadavg): 0.96 1.03 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 139010 0 0 0 3255 423 0 0 25 0 1 0 1740468116 483160064 117789 4294967295 134512640 135094434 3221221600 3220940000 134597460 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 117959 117789 145 145 0 117814 0
[pid=21410] vsize: 471836
Current children cumulated CPU time (s) 36.79
Current children cumulated vsize (Kb) 476032

[startup+50.0073 s]
Raw data (loadavg): 0.96 1.03 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) T 21406 21406 10120 0 -1 0 151089 0 0 0 4131 478 0 0 25 0 1 0 1740468116 446193664 108777 4294967295 134512640 135094434 3221221600 3220946172 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/21410/statm): 108934 108777 145 145 0 108789 0
[pid=21410] vsize: 435736
Current children cumulated CPU time (s) 46.1
Current children cumulated vsize (Kb) 439932

[startup+60.0071 s]
Raw data (loadavg): 0.97 1.03 0.99 1/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) T 21406 21406 10120 0 -1 0 163316 0 0 0 5014 523 0 0 25 0 1 0 1740468116 496214016 121004 4294967295 134512640 135094434 3221221600 3220942828 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/21410/statm): 121146 121004 145 145 0 121001 0
[pid=21410] vsize: 484584
Current children cumulated CPU time (s) 55.38
Current children cumulated vsize (Kb) 488780

[startup+70.0079 s]
Raw data (loadavg): 0.97 1.03 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 5970 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221214576 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 65.16
Current children cumulated vsize (Kb) 333752

[startup+80.0087 s]
Raw data (loadavg): 0.98 1.02 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 6970 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221214752 134676598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 75.16
Current children cumulated vsize (Kb) 333752

[startup+90.0095 s]
Raw data (loadavg): 0.98 1.02 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 7970 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221214928 134677340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 85.16
Current children cumulated vsize (Kb) 333752

[startup+100.01 s]
Raw data (loadavg): 0.98 1.02 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 8971 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221214848 134676317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 95.17
Current children cumulated vsize (Kb) 333752

[startup+110.011 s]
Raw data (loadavg): 0.98 1.02 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 9971 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221214912 134600167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 105.17
Current children cumulated vsize (Kb) 333752

[startup+120.012 s]
Raw data (loadavg): 0.99 1.02 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 10971 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215260 134676382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 115.17
Current children cumulated vsize (Kb) 333752

[startup+130.013 s]
Raw data (loadavg): 0.99 1.02 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 11972 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215356 134677081 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 125.18
Current children cumulated vsize (Kb) 333752

[startup+140.014 s]
Raw data (loadavg): 0.99 1.02 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 12972 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215200 134676376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 135.18
Current children cumulated vsize (Kb) 333752

[startup+150.015 s]
Raw data (loadavg): 0.99 1.02 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 13972 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215104 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 145.18
Current children cumulated vsize (Kb) 333752

[startup+160.015 s]
Raw data (loadavg): 0.99 1.02 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 14972 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221214752 134676519 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 155.18
Current children cumulated vsize (Kb) 333752

[startup+170.016 s]
Raw data (loadavg): 0.99 1.02 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 15973 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215280 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 165.19
Current children cumulated vsize (Kb) 333752

[startup+180.017 s]
Raw data (loadavg): 0.99 1.02 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 16973 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215104 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 175.19
Current children cumulated vsize (Kb) 333752

[startup+190.017 s]
Raw data (loadavg): 0.99 1.01 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 17973 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221214812 134676460 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 185.19
Current children cumulated vsize (Kb) 333752

[startup+200.018 s]
Raw data (loadavg): 0.99 1.01 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 18973 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215456 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 195.19
Current children cumulated vsize (Kb) 333752

[startup+210.019 s]
Raw data (loadavg): 0.99 1.01 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 19973 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215104 134600191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 205.19
Current children cumulated vsize (Kb) 333752

[startup+220.02 s]
Raw data (loadavg): 0.99 1.01 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 20974 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215280 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 215.2
Current children cumulated vsize (Kb) 333752

[startup+230.021 s]
Raw data (loadavg): 0.99 1.01 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 21974 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215104 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 225.2
Current children cumulated vsize (Kb) 333752

[startup+240.022 s]
Raw data (loadavg): 0.99 1.01 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 22974 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215200 134676301 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 235.2
Current children cumulated vsize (Kb) 333752

[startup+250.023 s]
Raw data (loadavg): 0.99 1.01 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 23974 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215704 134676334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 245.2
Current children cumulated vsize (Kb) 333752

[startup+260.024 s]
Raw data (loadavg): 0.99 1.01 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 24975 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221214928 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 255.21
Current children cumulated vsize (Kb) 333752

[startup+270.025 s]
Raw data (loadavg): 0.99 1.01 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 25975 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221214576 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 265.21
Current children cumulated vsize (Kb) 333752

[startup+280.025 s]
Raw data (loadavg): 0.99 1.01 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 26975 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221214576 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 275.21
Current children cumulated vsize (Kb) 333752

[startup+290.025 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 27975 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215456 134676532 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 285.21
Current children cumulated vsize (Kb) 333752

[startup+300.026 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 28975 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221214576 134600267 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 295.21
Current children cumulated vsize (Kb) 333752

[startup+310.026 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 29976 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215612 134676240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 305.22
Current children cumulated vsize (Kb) 333752

[startup+320.027 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 30976 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215104 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 315.22
Current children cumulated vsize (Kb) 333752

[startup+330.027 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 31976 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215024 134677049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 325.22
Current children cumulated vsize (Kb) 333752

[startup+340.027 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 32976 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215456 134600215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 335.22
Current children cumulated vsize (Kb) 333752

[startup+350.028 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 33977 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221214848 134676349 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 345.23
Current children cumulated vsize (Kb) 333752

[startup+360.029 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 34977 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215104 134676542 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 355.23
Current children cumulated vsize (Kb) 333752

[startup+370.03 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 35977 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215280 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 365.23
Current children cumulated vsize (Kb) 333752

[startup+380.03 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 36977 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215808 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 375.23
Current children cumulated vsize (Kb) 333752

[startup+390.03 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 37978 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215456 134676480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 385.24
Current children cumulated vsize (Kb) 333752

[startup+400.031 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 38978 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215104 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 395.24
Current children cumulated vsize (Kb) 333752

[startup+410.031 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 39978 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215456 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 405.24
Current children cumulated vsize (Kb) 333752

[startup+420.031 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 40978 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215332 134677232 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 415.24
Current children cumulated vsize (Kb) 333752

[startup+430.032 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 41978 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215456 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 425.24
Current children cumulated vsize (Kb) 333752

[startup+440.033 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 42979 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221214576 134677346 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 435.25
Current children cumulated vsize (Kb) 333752

[startup+450.034 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 43979 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215024 134677042 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 445.25
Current children cumulated vsize (Kb) 333752

[startup+460.035 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 44979 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221214928 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 455.25
Current children cumulated vsize (Kb) 333752

[startup+470.035 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 45979 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221214752 134677239 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 465.25
Current children cumulated vsize (Kb) 333752

[startup+480.036 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 46980 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215024 134676273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 475.26
Current children cumulated vsize (Kb) 333752

[startup+490.036 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 47980 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221214928 134677351 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 485.26
Current children cumulated vsize (Kb) 333752

[startup+500.038 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 48980 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221214400 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 495.26
Current children cumulated vsize (Kb) 333752

[startup+510.038 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 49980 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221214752 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 505.26
Current children cumulated vsize (Kb) 333752

[startup+520.038 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 50981 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215456 134677346 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 515.27
Current children cumulated vsize (Kb) 333752

[startup+530.039 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 51981 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221214928 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 525.27
Current children cumulated vsize (Kb) 333752

[startup+540.039 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 52981 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215328 134677375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 535.27
Current children cumulated vsize (Kb) 333752

[startup+550.04 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 53981 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215008 134677078 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 545.27
Current children cumulated vsize (Kb) 333752

[startup+560.04 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 54981 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215280 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 555.27
Current children cumulated vsize (Kb) 333752

[startup+570.041 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 55982 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221214928 134600175 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 565.28
Current children cumulated vsize (Kb) 333752

[startup+580.042 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 56982 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221214928 134676510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 575.28
Current children cumulated vsize (Kb) 333752

[startup+590.042 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 57982 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215024 134676311 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 585.28
Current children cumulated vsize (Kb) 333752

[startup+600.043 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 58982 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221214928 134601016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 595.28
Current children cumulated vsize (Kb) 333752

[startup+610.042 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 59982 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215348 134676335 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 605.28
Current children cumulated vsize (Kb) 333752

[startup+620.043 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 60983 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215280 134677363 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 615.29
Current children cumulated vsize (Kb) 333752

[startup+630.044 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 61983 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215440 134600246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 625.29
Current children cumulated vsize (Kb) 333752

[startup+640.045 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 62983 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215024 134677059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 635.29
Current children cumulated vsize (Kb) 333752

[startup+650.046 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 63983 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215104 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 645.29
Current children cumulated vsize (Kb) 333752

[startup+660.045 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 64984 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215280 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 655.3
Current children cumulated vsize (Kb) 333752

[startup+670.046 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 65984 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215808 134677320 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 665.3
Current children cumulated vsize (Kb) 333752

[startup+680.047 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 66984 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215456 134676489 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 675.3
Current children cumulated vsize (Kb) 333752

[startup+690.047 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 67984 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221214928 134677278 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 685.3
Current children cumulated vsize (Kb) 333752

[startup+700.048 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 68985 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215280 134600904 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 695.31
Current children cumulated vsize (Kb) 333752

[startup+710.048 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 69985 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215340 134677228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 705.31
Current children cumulated vsize (Kb) 333752

[startup+720.049 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 70985 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221216160 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 715.31
Current children cumulated vsize (Kb) 333752

[startup+730.05 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 71985 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215632 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 725.31
Current children cumulated vsize (Kb) 333752

[startup+740.051 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 72985 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215552 134677035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 735.31
Current children cumulated vsize (Kb) 333752

[startup+750.052 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 73986 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221216132 134676380 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 745.32
Current children cumulated vsize (Kb) 333752

[startup+760.051 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 74986 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215280 134677346 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 755.32
Current children cumulated vsize (Kb) 333752

[startup+770.052 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 75986 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215092 134600238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 765.32
Current children cumulated vsize (Kb) 333752

[startup+780.053 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 76986 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221214904 134676989 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 775.32
Current children cumulated vsize (Kb) 333752

[startup+790.053 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 77987 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215104 134600144 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 785.33
Current children cumulated vsize (Kb) 333752

[startup+800.054 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 78987 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215444 134600159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 795.33
Current children cumulated vsize (Kb) 333752

[startup+810.055 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 79987 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221214576 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 805.33
Current children cumulated vsize (Kb) 333752

[startup+820.056 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 80987 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221214640 134677091 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 815.33
Current children cumulated vsize (Kb) 333752

[startup+830.057 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 81988 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221214752 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 825.34
Current children cumulated vsize (Kb) 333752

[startup+840.057 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 82988 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221216160 134601161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 835.34
Current children cumulated vsize (Kb) 333752

[startup+850.057 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 83988 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215456 134676471 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 845.34
Current children cumulated vsize (Kb) 333752

[startup+860.058 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 84988 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221214928 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 855.34
Current children cumulated vsize (Kb) 333752

[startup+870.059 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 85989 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215728 134677059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 865.35
Current children cumulated vsize (Kb) 333752

[startup+880.06 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 86989 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215260 134676988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 875.35
Current children cumulated vsize (Kb) 333752

[startup+890.059 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 87989 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221214752 134600344 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 885.35
Current children cumulated vsize (Kb) 333752

[startup+900.06 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 88989 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221214752 134676519 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 895.35
Current children cumulated vsize (Kb) 333752

[startup+910.06 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 89989 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221214980 134676608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 905.35
Current children cumulated vsize (Kb) 333752

[startup+920.062 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 90990 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215280 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 915.36
Current children cumulated vsize (Kb) 333752

[startup+930.063 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 91990 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215504 134677375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 925.36
Current children cumulated vsize (Kb) 333752

[startup+940.062 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 92990 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215808 134600301 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 935.36
Current children cumulated vsize (Kb) 333752

[startup+950.063 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 93990 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215984 134676516 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 945.36
Current children cumulated vsize (Kb) 333752

[startup+960.063 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 94990 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215332 134676608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 955.36
Current children cumulated vsize (Kb) 333752

[startup+970.064 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 95991 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215456 134600314 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 965.37
Current children cumulated vsize (Kb) 333752

[startup+980.065 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 96991 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215352 134676334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 975.37
Current children cumulated vsize (Kb) 333752

[startup+990.065 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 97991 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221214928 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 985.37
Current children cumulated vsize (Kb) 333752

[startup+1000.07 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 98991 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221214928 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 995.37
Current children cumulated vsize (Kb) 333752

[startup+1010.07 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 99992 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215004 134676331 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 1005.38
Current children cumulated vsize (Kb) 333752

[startup+1020.07 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 100992 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215104 134677351 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 1015.38
Current children cumulated vsize (Kb) 333752

[startup+1030.07 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 101992 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215084 134676988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 1025.38
Current children cumulated vsize (Kb) 333752

[startup+1040.07 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 102992 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221214636 134676460 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 1035.38
Current children cumulated vsize (Kb) 333752

[startup+1050.07 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 103993 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221214808 134676461 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 1045.39
Current children cumulated vsize (Kb) 333752

[startup+1060.07 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 104993 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215200 134676317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 1055.39
Current children cumulated vsize (Kb) 333752

[startup+1070.07 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 105993 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215280 134600267 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 1065.39
Current children cumulated vsize (Kb) 333752

[startup+1080.07 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 106993 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215456 134676601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 1075.39
Current children cumulated vsize (Kb) 333752

[startup+1090.07 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 107994 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215280 134677327 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 1085.4
Current children cumulated vsize (Kb) 333752

[startup+1100.07 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 108994 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221216216 134677377 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 1095.4
Current children cumulated vsize (Kb) 333752

[startup+1110.07 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 109994 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221214928 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 1105.4
Current children cumulated vsize (Kb) 333752

[startup+1120.07 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 110994 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215904 134677059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 1115.4
Current children cumulated vsize (Kb) 333752

[startup+1130.07 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 111994 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221216160 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 1125.4
Current children cumulated vsize (Kb) 333752

[startup+1140.07 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 112995 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215024 134676259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 1135.41
Current children cumulated vsize (Kb) 333752

[startup+1150.08 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 113995 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215456 134600228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 1145.41
Current children cumulated vsize (Kb) 333752

[startup+1160.08 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 114995 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215352 134677084 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 1155.41
Current children cumulated vsize (Kb) 333752

[startup+1170.08 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 115995 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215360 134676328 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 1165.41
Current children cumulated vsize (Kb) 333752

[startup+1180.08 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 116996 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221216160 134600019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 1175.42
Current children cumulated vsize (Kb) 333752

[startup+1190.08 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 117996 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215280 134600274 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 1185.42
Current children cumulated vsize (Kb) 333752

[startup+1200.08 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 118996 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221216512 134600314 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 1195.42
Current children cumulated vsize (Kb) 333752

[startup+1210.08 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 119996 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215976 134600234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 1205.42
Current children cumulated vsize (Kb) 333752



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.08 s]
Raw data (loadavg): 0.99 1.00 0.99 2/56 21410
Raw data (/proc/21406/stat): 21406 (minisat+_script) S 21405 21406 10120 0 -1 0 322 277 0 0 0 0 0 1 21 0 1 0 1740468110 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/21406/statm): 1049 256 1003 147 0 902 0
[pid=21406] vsize: 4196
Raw data (/proc/21410/stat): 21410 (minisat+_64-bit) R 21406 21406 10120 0 -1 0 166744 0 0 0 119996 545 0 0 25 0 1 0 1740468116 337465344 82250 4294967295 134512640 135094434 3221221600 3221215456 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21410/statm): 82389 82250 145 145 0 82244 0
[pid=21410] vsize: 329556
Current children cumulated CPU time (s) 1205.42
Current children cumulated vsize (Kb) 333752

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

Child status: 0
Real time (s): 1210.23
CPU time (s): 1205.58
CPU user time (s): 1199.97
CPU system time (s): 5.60615
CPU usage (%): 99.6151
Max. virtual memory (cumulated for all children) (Kb): 488780



Verifier Data




ERROR: no interpretation found !