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-gesa2_o.opb
MD5SUM1b076646de46807d226b08ba41913d63
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 7248
Biggest coefficient in the objective function 409031671808
Number of bits for the biggest coefficient in the objective function 39
Sum of the numbers in the objective function 178209334735200
Number of bits of the sum of numbers in the objective function 48
Biggest number in a constraint 409031671808
Number of bits of the biggest number in a constraint 39
Biggest sum of numbers in a constraint 178209334735200
Number of bits of the biggest sum of numbers48
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables11184
Total number of constraints1584
Number of constraints which are clauses192
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints1392
Minimum length of a constraint2
Maximum length of a constraint209

Trace number 6199

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        915456 kB
Buffers:         10168 kB
Cached:          79844 kB
SwapCached:        904 kB
Active:          21860 kB
Inactive:        70888 kB
HighTotal:      131008 kB
HighFree:        46928 kB
LowTotal:       903652 kB
LowFree:        868528 kB
SwapTotal:     2097892 kB
SwapFree:      2096536 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5732 kB
Slab:            20792 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 04:39:36 (client local time) WITH STATUS 0 IN 1206.64 SECONDS
stats: 3359 7 1206.64 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/28813/stat): 28813 (minisat+_script) R 28812 28813 2660 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1855603943 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/28813/statm): 174 3 169 147 0 27 0
[pid=28813] vsize: 696
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libtermcap.so.2
open syscall for file tls/i686/libtermcap.so.2
open syscall for file tls/mmx/libtermcap.so.2
open syscall for file tls/libtermcap.so.2
open syscall for file i686/mmx/libtermcap.so.2
open syscall for file i686/libtermcap.so.2
open syscall for file mmx/libtermcap.so.2
open syscall for file libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/libtermcap.so.2
open syscall for file /etc/ld.so.cache
open syscall for file /lib/libtermcap.so.2
open syscall for file tls/i686/mmx/libdl.so.2
open syscall for file tls/i686/libdl.so.2
open syscall for file tls/mmx/libdl.so.2
open syscall for file tls/libdl.so.2
open syscall for file i686/mmx/libdl.so.2
open syscall for file i686/libdl.so.2
open syscall for file mmx/libdl.so.2
open syscall for file libdl.so.2
open syscall for file /oldhome/oroussel/lib/libdl.so.2
open syscall for file /lib/libdl.so.2
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /lib/tls/libc.so.6
open syscall for file /dev/tty
open syscall for file /etc/mtab
open syscall for file /proc/meminfo
open syscall for file /oldhome/oroussel/solvers/minisat+_script
New process pid=28814
New process pid=28815
New process pid=28816
execve syscall for /bin/sed executable
One traced child (pid=28815) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=28816) exited with status: 0
One traced child (pid=28814) exited with status: 0
New process pid=28817
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-gesa2_o.opb

[startup+10.0037 s]
Raw data (loadavg): 0.94 0.98 0.92 1/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) T 28813 28813 2660 0 -1 0 36780 0 0 0 783 118 0 0 24 0 1 0 1855603948 107933696 26191 4294967295 134512640 135094434 3221224432 3221205788 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/28817/statm): 26351 26191 145 145 0 26206 0
[pid=28817] vsize: 105404
Current children cumulated CPU time (s) 9.02
Current children cumulated vsize (Kb) 107528

[startup+20.0044 s]
Raw data (loadavg): 1.02 1.00 0.93 1/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) T 28813 28813 2660 0 -1 0 72404 0 0 0 1582 233 0 0 24 0 1 0 1855603948 210653184 51269 4294967295 134512640 135094434 3221224432 3221205436 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/28817/statm): 51429 51269 145 145 0 51284 0
[pid=28817] vsize: 205716
Current children cumulated CPU time (s) 18.16
Current children cumulated vsize (Kb) 207840

[startup+30.0051 s]
Raw data (loadavg): 1.02 1.00 0.93 1/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) T 28813 28813 2660 0 -1 0 91648 0 0 0 2386 314 0 0 23 0 1 0 1855603948 289476608 70513 4294967295 134512640 135094434 3221224432 3221206844 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/28817/statm): 70673 70513 145 145 0 70528 0
[pid=28817] vsize: 282692
Current children cumulated CPU time (s) 27.01
Current children cumulated vsize (Kb) 284816

[startup+40.0059 s]
Raw data (loadavg): 1.01 1.00 0.93 1/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) T 28813 28813 2660 0 -1 0 141194 0 0 0 3218 441 0 0 24 0 1 0 1855603948 406048768 98968 4294967295 134512640 135094434 3221224432 3221204732 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/28817/statm): 99133 98968 145 145 0 98988 0
[pid=28817] vsize: 396532
Current children cumulated CPU time (s) 36.6
Current children cumulated vsize (Kb) 398656

[startup+50.0076 s]
Raw data (loadavg): 1.01 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 141964 0 0 0 4202 454 0 0 25 0 1 0 1855603948 236421120 57556 4294967295 134512640 135094434 3221224432 3221219968 134676294 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 57720 57556 145 145 0 57575 0
[pid=28817] vsize: 230880
Current children cumulated CPU time (s) 46.57
Current children cumulated vsize (Kb) 233004

[startup+60.0083 s]
Raw data (loadavg): 1.01 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 141964 0 0 0 5202 454 0 0 25 0 1 0 1855603948 236421120 57556 4294967295 134512640 135094434 3221224432 3221220576 134677284 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 57720 57556 145 145 0 57575 0
[pid=28817] vsize: 230880
Current children cumulated CPU time (s) 56.57
Current children cumulated vsize (Kb) 233004

[startup+70.01 s]
Raw data (loadavg): 1.01 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 141964 0 0 0 6201 455 0 0 25 0 1 0 1855603948 236421120 57556 4294967295 134512640 135094434 3221224432 3221220640 134676341 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 57720 57556 145 145 0 57575 0
[pid=28817] vsize: 230880
Current children cumulated CPU time (s) 66.57
Current children cumulated vsize (Kb) 233004

[startup+80.0118 s]
Raw data (loadavg): 1.01 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 141964 0 0 0 7201 455 0 0 25 0 1 0 1855603948 236421120 57556 4294967295 134512640 135094434 3221224432 3221221436 134676382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 57720 57556 145 145 0 57575 0
[pid=28817] vsize: 230880
Current children cumulated CPU time (s) 76.57
Current children cumulated vsize (Kb) 233004

[startup+90.0115 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 141968 0 0 0 8201 455 0 0 25 0 1 0 1855603948 236421120 57560 4294967295 134512640 135094434 3221224432 3221206068 134597140 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 57720 57560 145 145 0 57575 0
[pid=28817] vsize: 230880
Current children cumulated CPU time (s) 86.57
Current children cumulated vsize (Kb) 233004

[startup+100.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 163059 0 0 0 9153 504 0 0 25 0 1 0 1855603948 322809856 78651 4294967295 134512640 135094434 3221224432 3221205392 134596875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 78811 78651 145 145 0 78666 0
[pid=28817] vsize: 315244
Current children cumulated CPU time (s) 96.58
Current children cumulated vsize (Kb) 317368

[startup+110.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 163059 0 0 0 10152 504 0 0 25 0 1 0 1855603948 322809856 78651 4294967295 134512640 135094434 3221224432 3221223232 134596743 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 78811 78651 145 145 0 78666 0
[pid=28817] vsize: 315244
Current children cumulated CPU time (s) 106.57
Current children cumulated vsize (Kb) 317368

[startup+120.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 163059 0 0 0 11149 508 0 0 25 0 1 0 1855603948 236421120 57560 4294967295 134512640 135094434 3221224432 3221220224 134677290 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 57720 57560 145 145 0 57575 0
[pid=28817] vsize: 230880
Current children cumulated CPU time (s) 116.58
Current children cumulated vsize (Kb) 233004

[startup+130.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 163059 0 0 0 12149 508 0 0 25 0 1 0 1855603948 236421120 57560 4294967295 134512640 135094434 3221224432 3221220224 134677346 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 57720 57560 145 145 0 57575 0
[pid=28817] vsize: 230880
Current children cumulated CPU time (s) 126.58
Current children cumulated vsize (Kb) 233004

[startup+140.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 163059 0 0 0 13149 508 0 0 25 0 1 0 1855603948 236421120 57560 4294967295 134512640 135094434 3221224432 3221219968 134676294 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 57720 57560 145 145 0 57575 0
[pid=28817] vsize: 230880
Current children cumulated CPU time (s) 136.58
Current children cumulated vsize (Kb) 233004

[startup+150.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 163059 0 0 0 14149 508 0 0 25 0 1 0 1855603948 236421120 57560 4294967295 134512640 135094434 3221224432 3221221632 134600144 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 57720 57560 145 145 0 57575 0
[pid=28817] vsize: 230880
Current children cumulated CPU time (s) 146.58
Current children cumulated vsize (Kb) 233004

[startup+160.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 173605 0 0 0 15125 533 0 0 25 0 1 0 1855603948 279617536 68106 4294967295 134512640 135094434 3221224432 3221204448 134597164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 68266 68106 145 145 0 68121 0
[pid=28817] vsize: 273064
Current children cumulated CPU time (s) 156.59
Current children cumulated vsize (Kb) 275188

[startup+170.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 194696 0 0 0 16076 582 0 0 25 0 1 0 1855603948 322809856 78651 4294967295 134512640 135094434 3221224432 3221204864 134596860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 78811 78651 145 145 0 78666 0
[pid=28817] vsize: 315244
Current children cumulated CPU time (s) 166.59
Current children cumulated vsize (Kb) 317368

[startup+180.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 236878 0 0 0 16981 677 0 0 25 0 1 0 1855603948 495587328 120833 4294967295 134512640 135094434 3221224432 3221207360 134597447 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 120993 120833 145 145 0 120848 0
[pid=28817] vsize: 483972
Current children cumulated CPU time (s) 176.59
Current children cumulated vsize (Kb) 486096

[startup+190.018 s]
Raw data (loadavg): 1.07 1.02 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 242959 0 0 0 17917 708 0 0 25 0 1 0 1855603948 434106368 105823 4294967295 134512640 135094434 3221224432 3221223232 134596750 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 105983 105823 145 145 0 105838 0
[pid=28817] vsize: 423932
Current children cumulated CPU time (s) 186.26
Current children cumulated vsize (Kb) 426056

[startup+200.019 s]
Raw data (loadavg): 1.06 1.02 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 242959 0 0 0 18909 716 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221219520 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 196.26
Current children cumulated vsize (Kb) 257328

[startup+210.02 s]
Raw data (loadavg): 1.05 1.01 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 242959 0 0 0 19909 716 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221220848 134677059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 206.26
Current children cumulated vsize (Kb) 257328

[startup+220.021 s]
Raw data (loadavg): 1.04 1.01 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 242959 0 0 0 20910 716 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221220644 134676335 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 216.27
Current children cumulated vsize (Kb) 257328

[startup+230.022 s]
Raw data (loadavg): 1.04 1.01 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 242959 0 0 0 21909 716 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221204064 134597533 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 226.26
Current children cumulated vsize (Kb) 257328

[startup+240.022 s]
Raw data (loadavg): 1.03 1.01 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 258778 0 0 0 22874 752 0 0 25 0 1 0 1855603948 304525312 74187 4294967295 134512640 135094434 3221224432 3221205040 134597012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 74347 74187 145 145 0 74202 0
[pid=28817] vsize: 297388
Current children cumulated CPU time (s) 236.27
Current children cumulated vsize (Kb) 299512

[startup+250.023 s]
Raw data (loadavg): 1.02 1.01 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 279869 0 0 0 23824 802 0 0 25 0 1 0 1855603948 347717632 84732 4294967295 134512640 135094434 3221224432 3221205920 134596866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 84892 84732 145 145 0 84747 0
[pid=28817] vsize: 339568
Current children cumulated CPU time (s) 246.27
Current children cumulated vsize (Kb) 341692

[startup+260.024 s]
Raw data (loadavg): 1.02 1.01 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 322051 0 0 0 24728 898 0 0 25 0 1 0 1855603948 520495104 126914 4294967295 134512640 135094434 3221224432 3221205600 134597418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 127074 126914 145 145 0 126929 0
[pid=28817] vsize: 508296
Current children cumulated CPU time (s) 256.27
Current children cumulated vsize (Kb) 510420

[startup+270.025 s]
Raw data (loadavg): 1.02 1.01 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 322051 0 0 0 25717 910 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221220048 134600267 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 266.28
Current children cumulated vsize (Kb) 257328

[startup+280.025 s]
Raw data (loadavg): 1.01 1.01 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 322051 0 0 0 26717 910 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221220048 134676598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 276.28
Current children cumulated vsize (Kb) 257328

[startup+290.026 s]
Raw data (loadavg): 1.01 1.01 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 322051 0 0 0 27717 910 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221220544 134676993 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 286.28
Current children cumulated vsize (Kb) 257328

[startup+300.028 s]
Raw data (loadavg): 1.01 1.01 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 322051 0 0 0 28718 910 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221220576 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 296.29
Current children cumulated vsize (Kb) 257328

[startup+310.028 s]
Raw data (loadavg): 1.01 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 324688 0 0 0 29712 916 0 0 25 0 1 0 1855603948 272130048 66278 4294967295 134512640 135094434 3221224432 3221204864 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 66438 66278 145 145 0 66293 0
[pid=28817] vsize: 265752
Current children cumulated CPU time (s) 306.29
Current children cumulated vsize (Kb) 267876

[startup+320.029 s]
Raw data (loadavg): 1.01 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 357016 0 0 0 30638 990 0 0 25 0 1 0 1855603948 390914048 90696 4294967295 134512640 135094434 3221224432 3221204016 134597368 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 95438 90702 145 145 0 95293 0
[pid=28817] vsize: 381752
Current children cumulated CPU time (s) 316.29
Current children cumulated vsize (Kb) 383876

[startup+330.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 361598 0 0 0 31626 1003 0 0 25 0 1 0 1855603948 347717632 84732 4294967295 134512640 135094434 3221224432 3221205744 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 84892 84732 145 145 0 84747 0
[pid=28817] vsize: 339568
Current children cumulated CPU time (s) 326.3
Current children cumulated vsize (Kb) 341692

[startup+340.031 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 403780 0 0 0 32525 1103 0 0 25 0 1 0 1855603948 434106368 105823 4294967295 134512640 135094434 3221224432 3221207752 134597121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 105983 105823 145 145 0 105838 0
[pid=28817] vsize: 423932
Current children cumulated CPU time (s) 336.29
Current children cumulated vsize (Kb) 426056

[startup+350.031 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 403780 0 0 0 33518 1111 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221220672 134677028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 346.3
Current children cumulated vsize (Kb) 257328

[startup+360.032 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 403780 0 0 0 34518 1111 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221220224 134600274 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 356.3
Current children cumulated vsize (Kb) 257328

[startup+370.033 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 403780 0 0 0 35518 1111 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221220752 134677290 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 366.3
Current children cumulated vsize (Kb) 257328

[startup+380.034 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 403780 0 0 0 36518 1111 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221220824 134676334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 376.3
Current children cumulated vsize (Kb) 257328

[startup+390.033 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 422236 0 0 0 37477 1152 0 0 25 0 1 0 1855603948 326123520 79460 4294967295 134512640 135094434 3221224432 3221204192 134597477 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 79620 79460 145 145 0 79475 0
[pid=28817] vsize: 318480
Current children cumulated CPU time (s) 386.3
Current children cumulated vsize (Kb) 320604

[startup+400.034 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 443327 0 0 0 38427 1203 0 0 25 0 1 0 1855603948 347717632 84732 4294967295 134512640 135094434 3221224432 3221204160 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 84892 84732 145 145 0 84747 0
[pid=28817] vsize: 339568
Current children cumulated CPU time (s) 396.31
Current children cumulated vsize (Kb) 341692

[startup+410.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 470367 0 0 0 39364 1266 0 0 25 0 1 0 1855603948 520495104 111772 4294967295 134512640 135094434 3221224432 3221207184 134597368 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 127074 111778 145 145 0 126929 0
[pid=28817] vsize: 508296
Current children cumulated CPU time (s) 406.31
Current children cumulated vsize (Kb) 510420

[startup+420.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 485509 0 0 0 40325 1305 0 0 25 0 1 0 1855603948 434106368 105823 4294967295 134512640 135094434 3221224432 3221223232 134596764 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 105983 105823 145 145 0 105838 0
[pid=28817] vsize: 423932
Current children cumulated CPU time (s) 416.31
Current children cumulated vsize (Kb) 426056

[startup+430.036 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 485509 0 0 0 41318 1313 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221220224 134600144 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 426.32
Current children cumulated vsize (Kb) 257328

[startup+440.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 485509 0 0 0 42318 1313 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221219772 134676331 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 436.32
Current children cumulated vsize (Kb) 257328

[startup+450.038 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 485509 0 0 0 43318 1313 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221220736 134600162 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 446.32
Current children cumulated vsize (Kb) 257328

[startup+460.038 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 485509 0 0 0 44318 1313 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221221448 134600234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 456.32
Current children cumulated vsize (Kb) 257328

[startup+470.039 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 503965 0 0 0 45275 1356 0 0 25 0 1 0 1855603948 304525312 74187 4294967295 134512640 135094434 3221224432 3221203808 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 74347 74187 145 145 0 74202 0
[pid=28817] vsize: 297388
Current children cumulated CPU time (s) 466.32
Current children cumulated vsize (Kb) 299512

[startup+480.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 525056 0 0 0 46225 1406 0 0 25 0 1 0 1855603948 347717632 84732 4294967295 134512640 135094434 3221224432 3221209264 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 84892 84732 145 145 0 84747 0
[pid=28817] vsize: 339568
Current children cumulated CPU time (s) 476.32
Current children cumulated vsize (Kb) 341692

[startup+490.041 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 567238 0 0 0 47131 1501 0 0 25 0 1 0 1855603948 520495104 126914 4294967295 134512640 135094434 3221224432 3221205952 134597421 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 127074 126914 145 145 0 126929 0
[pid=28817] vsize: 508296
Current children cumulated CPU time (s) 486.33
Current children cumulated vsize (Kb) 510420

[startup+500.041 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 567238 0 0 0 48119 1513 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221220476 134676331 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 496.33
Current children cumulated vsize (Kb) 257328

[startup+510.042 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 567238 0 0 0 49120 1513 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221220672 134677059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 506.34
Current children cumulated vsize (Kb) 257328

[startup+520.043 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 567238 0 0 0 50120 1513 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221219872 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 516.34
Current children cumulated vsize (Kb) 257328

[startup+530.043 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 567238 0 0 0 51120 1513 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221221456 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 526.34
Current children cumulated vsize (Kb) 257328

[startup+540.044 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 575148 0 0 0 52101 1532 0 0 25 0 1 0 1855603948 282927104 68914 4294967295 134512640 135094434 3221224432 3221205216 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 69074 68914 145 145 0 68929 0
[pid=28817] vsize: 276296
Current children cumulated CPU time (s) 536.34
Current children cumulated vsize (Kb) 278420

[startup+550.046 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 606785 0 0 0 53029 1605 0 0 25 0 1 0 1855603948 390914048 95278 4294967295 134512640 135094434 3221224432 3221204896 134597418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 95438 95278 145 145 0 95293 0
[pid=28817] vsize: 381752
Current children cumulated CPU time (s) 546.35
Current children cumulated vsize (Kb) 383876

[startup+560.047 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 606785 0 0 0 54027 1607 0 0 25 0 1 0 1855603948 347717632 84732 4294967295 134512640 135094434 3221224432 3221205296 134595105 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 84892 84732 145 145 0 84747 0
[pid=28817] vsize: 339568
Current children cumulated CPU time (s) 556.35
Current children cumulated vsize (Kb) 341692

[startup+570.046 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 606785 0 0 0 55023 1610 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221219872 134601016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 566.34
Current children cumulated vsize (Kb) 257328

[startup+580.047 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 606785 0 0 0 56023 1610 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221220752 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 576.34
Current children cumulated vsize (Kb) 257328

[startup+590.048 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 606785 0 0 0 57024 1610 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221220636 134676460 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 586.35
Current children cumulated vsize (Kb) 257328

[startup+600.048 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 606785 0 0 0 58024 1610 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221221280 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 596.35
Current children cumulated vsize (Kb) 257328

[startup+610.049 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 625241 0 0 0 58980 1655 0 0 25 0 1 0 1855603948 304525312 74187 4294967295 134512640 135094434 3221224432 3221204864 134596997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 74347 74187 145 145 0 74202 0
[pid=28817] vsize: 297388
Current children cumulated CPU time (s) 606.36
Current children cumulated vsize (Kb) 299512

[startup+620.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 646332 0 0 0 59931 1703 0 0 25 0 1 0 1855603948 347717632 84732 4294967295 134512640 135094434 3221224432 3221205644 134595492 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 84892 84732 145 145 0 84747 0
[pid=28817] vsize: 339568
Current children cumulated CPU time (s) 616.35
Current children cumulated vsize (Kb) 341692

[startup+630.051 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 646332 0 0 0 60932 1703 0 0 25 0 1 0 1855603948 347717632 84732 4294967295 134512640 135094434 3221224432 3221223232 134596743 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 84892 84732 145 145 0 84747 0
[pid=28817] vsize: 339568
Current children cumulated CPU time (s) 626.36
Current children cumulated vsize (Kb) 341692

[startup+640.051 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 646332 0 0 0 61928 1707 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221221436 134676988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 636.36
Current children cumulated vsize (Kb) 257328

[startup+650.053 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 646332 0 0 0 62927 1708 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221220752 134676471 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 646.36
Current children cumulated vsize (Kb) 257328

[startup+660.054 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 646332 0 0 0 63927 1709 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221220576 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 656.37
Current children cumulated vsize (Kb) 257328

[startup+670.055 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 646332 0 0 0 64927 1709 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221207712 134597410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 666.37
Current children cumulated vsize (Kb) 257328

[startup+680.056 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 664788 0 0 0 65883 1754 0 0 25 0 1 0 1855603948 304525312 74187 4294967295 134512640 135094434 3221224432 3221207152 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 74347 74187 145 145 0 74202 0
[pid=28817] vsize: 297388
Current children cumulated CPU time (s) 676.38
Current children cumulated vsize (Kb) 299512

[startup+690.057 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 685879 0 0 0 66832 1804 0 0 25 0 1 0 1855603948 347717632 84732 4294967295 134512640 135094434 3221224432 3221205216 134596848 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 84892 84732 145 145 0 84747 0
[pid=28817] vsize: 339568
Current children cumulated CPU time (s) 686.37
Current children cumulated vsize (Kb) 341692

[startup+700.058 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 728061 0 0 0 67737 1900 0 0 25 0 1 0 1855603948 520495104 126914 4294967295 134512640 135094434 3221224432 3221205072 134597418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 127074 126914 145 145 0 126929 0
[pid=28817] vsize: 508296
Current children cumulated CPU time (s) 696.38
Current children cumulated vsize (Kb) 510420

[startup+710.058 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 728061 0 0 0 68725 1912 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221219344 134676601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 706.38
Current children cumulated vsize (Kb) 257328

[startup+720.059 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 728061 0 0 0 69725 1912 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221220224 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 716.38
Current children cumulated vsize (Kb) 257328

[startup+730.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 728061 0 0 0 70725 1913 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221220848 134677059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 726.39
Current children cumulated vsize (Kb) 257328

[startup+740.061 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 728061 0 0 0 71725 1913 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221219872 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 736.39
Current children cumulated vsize (Kb) 257328

[startup+750.061 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 735971 0 0 0 72707 1931 0 0 25 0 1 0 1855603948 282927104 68914 4294967295 134512640 135094434 3221224432 3221204956 134595088 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 69074 68914 145 145 0 68929 0
[pid=28817] vsize: 276296
Current children cumulated CPU time (s) 746.39
Current children cumulated vsize (Kb) 278420

[startup+760.062 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 767608 0 0 0 73632 2006 0 0 25 0 1 0 1855603948 347717632 84732 4294967295 134512640 135094434 3221224432 3221204556 134594756 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 84892 84732 145 145 0 84747 0
[pid=28817] vsize: 339568
Current children cumulated CPU time (s) 756.39
Current children cumulated vsize (Kb) 341692

[startup+770.062 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 767608 0 0 0 74632 2006 0 0 25 0 1 0 1855603948 347717632 84732 4294967295 134512640 135094434 3221224432 3221206192 134595021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 84892 84732 145 145 0 84747 0
[pid=28817] vsize: 339568
Current children cumulated CPU time (s) 766.39
Current children cumulated vsize (Kb) 341692

[startup+780.063 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 767608 0 0 0 75629 2010 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 776.4
Current children cumulated vsize (Kb) 257328

[startup+790.063 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 767608 0 0 0 76628 2010 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221220296 134677084 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 786.39
Current children cumulated vsize (Kb) 257328

[startup+800.064 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 767608 0 0 0 77629 2010 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221220928 134600215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 796.4
Current children cumulated vsize (Kb) 257328

[startup+810.065 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 767608 0 0 0 78629 2010 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221219696 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 806.4
Current children cumulated vsize (Kb) 257328

[startup+820.066 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 786064 0 0 0 79587 2053 0 0 25 0 1 0 1855603948 304525312 74187 4294967295 134512640 135094434 3221224432 3221206192 134594919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 74347 74187 145 145 0 74202 0
[pid=28817] vsize: 297388
Current children cumulated CPU time (s) 816.41
Current children cumulated vsize (Kb) 299512

[startup+830.066 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 807155 0 0 0 80538 2102 0 0 25 0 1 0 1855603948 347717632 84732 4294967295 134512640 135094434 3221224432 3221206344 134595322 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 84892 84732 145 145 0 84747 0
[pid=28817] vsize: 339568
Current children cumulated CPU time (s) 826.41
Current children cumulated vsize (Kb) 341692

[startup+840.067 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 807155 0 0 0 81537 2106 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221223212 134802881 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 836.44
Current children cumulated vsize (Kb) 257328

[startup+850.098 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 807155 0 0 0 82537 2106 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221220044 134600154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 846.44
Current children cumulated vsize (Kb) 257328

[startup+860.098 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 807155 0 0 0 83537 2106 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221220820 134677085 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 856.44
Current children cumulated vsize (Kb) 257328

[startup+870.098 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 807155 0 0 0 84538 2106 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221220204 134676988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 866.45
Current children cumulated vsize (Kb) 257328

[startup+880.099 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 809792 0 0 0 85531 2112 0 0 25 0 1 0 1855603948 272130048 66278 4294967295 134512640 135094434 3221224432 3221204720 134597450 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 66438 66278 145 145 0 66293 0
[pid=28817] vsize: 265752
Current children cumulated CPU time (s) 876.44
Current children cumulated vsize (Kb) 267876

[startup+890.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 825611 0 0 0 86494 2150 0 0 25 0 1 0 1855603948 304525312 74187 4294967295 134512640 135094434 3221224432 3221204944 134595105 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 74347 74187 145 145 0 74202 0
[pid=28817] vsize: 297388
Current children cumulated CPU time (s) 886.45
Current children cumulated vsize (Kb) 299512

[startup+900.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 846702 0 0 0 87445 2199 0 0 25 0 1 0 1855603948 347717632 84732 4294967295 134512640 135094434 3221224432 3221206080 134595569 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 84892 84732 145 145 0 84747 0
[pid=28817] vsize: 339568
Current children cumulated CPU time (s) 896.45
Current children cumulated vsize (Kb) 341692

[startup+910.101 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 846702 0 0 0 88441 2203 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221220200 134677149 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 906.45
Current children cumulated vsize (Kb) 257328

[startup+920.102 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 846702 0 0 0 89442 2203 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221220036 134600238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 916.46
Current children cumulated vsize (Kb) 257328

[startup+930.102 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 846702 0 0 0 90441 2203 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221221024 134676259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 926.45
Current children cumulated vsize (Kb) 257328

[startup+940.103 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 846702 0 0 0 91442 2203 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221220320 134676273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 936.46
Current children cumulated vsize (Kb) 257328

[startup+950.104 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 854612 0 0 0 92423 2222 0 0 25 0 1 0 1855603948 282927104 68914 4294967295 134512640 135094434 3221224432 3221205136 134595058 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 69074 68914 145 145 0 68929 0
[pid=28817] vsize: 276296
Current children cumulated CPU time (s) 946.46
Current children cumulated vsize (Kb) 278420

[startup+960.105 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 886249 0 0 0 93351 2294 0 0 25 0 1 0 1855603948 390914048 95278 4294967295 134512640 135094434 3221224432 3221207360 134597418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 95438 95278 145 145 0 95293 0
[pid=28817] vsize: 381752
Current children cumulated CPU time (s) 956.46
Current children cumulated vsize (Kb) 383876

[startup+970.105 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 886249 0 0 0 94350 2296 0 0 25 0 1 0 1855603948 347717632 84732 4294967295 134512640 135094434 3221224432 3221208436 134595331 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 84892 84732 145 145 0 84747 0
[pid=28817] vsize: 339568
Current children cumulated CPU time (s) 966.47
Current children cumulated vsize (Kb) 341692

[startup+980.106 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 928431 0 0 0 95250 2396 0 0 25 0 1 0 1855603948 434106368 105823 4294967295 134512640 135094434 3221224432 3221223232 134596743 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 105983 105823 145 145 0 105838 0
[pid=28817] vsize: 423932
Current children cumulated CPU time (s) 976.47
Current children cumulated vsize (Kb) 426056

[startup+990.107 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 928431 0 0 0 96242 2404 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221220388 134600238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 986.47
Current children cumulated vsize (Kb) 257328

[startup+1000.11 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 928431 0 0 0 97242 2404 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221220908 134676240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 996.47
Current children cumulated vsize (Kb) 257328

[startup+1010.11 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 928431 0 0 0 98243 2404 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221220256 134783376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 1006.48
Current children cumulated vsize (Kb) 257328

[startup+1020.11 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 928431 0 0 0 99243 2404 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221221632 134677310 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 1016.48
Current children cumulated vsize (Kb) 257328

[startup+1030.11 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 946887 0 0 0 100199 2448 0 0 25 0 1 0 1855603948 304525312 74187 4294967295 134512640 135094434 3221224432 3221206064 134597243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 74347 74187 145 145 0 74202 0
[pid=28817] vsize: 297388
Current children cumulated CPU time (s) 1026.48
Current children cumulated vsize (Kb) 299512

[startup+1040.11 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 967978 0 0 0 101149 2498 0 0 25 0 1 0 1855603948 347717632 84732 4294967295 134512640 135094434 3221224432 3221207504 134596806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 84892 84732 145 145 0 84747 0
[pid=28817] vsize: 339568
Current children cumulated CPU time (s) 1036.48
Current children cumulated vsize (Kb) 341692

[startup+1050.11 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 967978 0 0 0 102146 2502 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221219744 134677375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 1046.49
Current children cumulated vsize (Kb) 257328

[startup+1060.11 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 967978 0 0 0 103145 2502 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221220224 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 1056.48
Current children cumulated vsize (Kb) 257328

[startup+1070.11 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 967978 0 0 0 104146 2502 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221220752 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 1066.49
Current children cumulated vsize (Kb) 257328

[startup+1080.11 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 967978 0 0 0 105146 2502 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221220576 134600002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 1076.49
Current children cumulated vsize (Kb) 257328

[startup+1090.11 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 970615 0 0 0 106140 2509 0 0 25 0 1 0 1855603948 272130048 66278 4294967295 134512640 135094434 3221224432 3221205920 134596821 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 66438 66278 145 145 0 66293 0
[pid=28817] vsize: 265752
Current children cumulated CPU time (s) 1086.5
Current children cumulated vsize (Kb) 267876

[startup+1100.11 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 995928 0 0 0 107084 2565 0 0 25 0 1 0 1855603948 390914048 83681 4294967295 134512640 135094434 3221224432 3221206656 134597368 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 95438 83687 145 145 0 95293 0
[pid=28817] vsize: 381752
Current children cumulated CPU time (s) 1096.5
Current children cumulated vsize (Kb) 383876

[startup+1110.11 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 1007525 0 0 0 108055 2594 0 0 25 0 1 0 1855603948 347717632 84732 4294967295 134512640 135094434 3221224432 3221206976 134596809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 84892 84732 145 145 0 84747 0
[pid=28817] vsize: 339568
Current children cumulated CPU time (s) 1106.5
Current children cumulated vsize (Kb) 341692

[startup+1120.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 1049707 0 0 0 108958 2691 0 0 25 0 1 0 1855603948 520495104 126914 4294967295 134512640 135094434 3221224432 3221206832 134597410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 127074 126914 145 145 0 126929 0
[pid=28817] vsize: 508296
Current children cumulated CPU time (s) 1116.5
Current children cumulated vsize (Kb) 510420

[startup+1130.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 1049707 0 0 0 109947 2702 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221220272 134676465 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 1126.5
Current children cumulated vsize (Kb) 257328

[startup+1140.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 1049707 0 0 0 110947 2703 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221220048 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 1136.51
Current children cumulated vsize (Kb) 257328

[startup+1150.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 1049707 0 0 0 111947 2703 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 1146.51
Current children cumulated vsize (Kb) 257328

[startup+1160.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 1049707 0 0 0 112947 2703 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221220384 134600241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 1156.51
Current children cumulated vsize (Kb) 257328

[startup+1170.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 1060334 0 0 0 113923 2727 0 0 25 0 1 0 1855603948 326123520 71631 4294967295 134512640 135094434 3221224432 3221204368 134597368 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 79620 71638 145 145 0 79475 0
[pid=28817] vsize: 318480
Current children cumulated CPU time (s) 1166.51
Current children cumulated vsize (Kb) 320604

[startup+1180.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 1089254 0 0 0 114854 2796 0 0 25 0 1 0 1855603948 347717632 84732 4294967295 134512640 135094434 3221224432 3221205744 134596842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 84892 84732 145 145 0 84747 0
[pid=28817] vsize: 339568
Current children cumulated CPU time (s) 1176.51
Current children cumulated vsize (Kb) 341692

[startup+1190.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 1089254 0 0 0 115855 2796 0 0 25 0 1 0 1855603948 347717632 84732 4294967295 134512640 135094434 3221224432 3221205620 134595340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 84892 84732 145 145 0 84747 0
[pid=28817] vsize: 339568
Current children cumulated CPU time (s) 1186.52
Current children cumulated vsize (Kb) 341692

[startup+1200.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 1131436 0 0 0 116756 2895 0 0 25 0 1 0 1855603948 434106368 105823 4294967295 134512640 135094434 3221224432 3221223232 134596743 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 105983 105823 145 145 0 105838 0
[pid=28817] vsize: 423932
Current children cumulated CPU time (s) 1196.52
Current children cumulated vsize (Kb) 426056

[startup+1210.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 1131436 0 0 0 117748 2903 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221219696 134677300 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 1206.52
Current children cumulated vsize (Kb) 257328



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28817
Raw data (/proc/28813/stat): 28813 (minisat+_script) S 28812 28813 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855603943 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28813/statm): 531 226 485 147 0 384 0
[pid=28813] vsize: 2124
Raw data (/proc/28817/stat): 28817 (minisat+_64-bit) R 28813 28813 2660 0 -1 0 1131436 0 0 0 117748 2903 0 0 25 0 1 0 1855603948 261328896 63641 4294967295 134512640 135094434 3221224432 3221220132 134677077 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28817/statm): 63801 63641 145 145 0 63656 0
[pid=28817] vsize: 255204
Current children cumulated CPU time (s) 1206.52
Current children cumulated vsize (Kb) 257328

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

Child status: 0
Real time (s): 1210.24
CPU time (s): 1206.64
CPU user time (s): 1177.49
CPU system time (s): 29.1546
CPU usage (%): 99.7023
Max. virtual memory (cumulated for all children) (Kb): 510420



Verifier Data




ERROR: no interpretation found !