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/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-van.opb
MD5SUM63aca17b11625a83c7613ee93b3a2e23
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 29193312741
Optimality of the best value was proved NO
Number of terms in the objective function 192
Biggest coefficient in the objective function 2427002644
Number of bits for the biggest coefficient in the objective function 32
Sum of the numbers in the objective function 319999999936
Number of bits of the sum of numbers in the objective function 39
Biggest number in a constraint 28349428224
Number of bits of the biggest number in a constraint 35
Biggest sum of numbers in a constraint 319999999936
Number of bits of the biggest sum of numbers39
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1206.36
Number of variables98496
Total number of constraints39811
Number of constraints which are clauses128
Number of constraints which are cardinality constraints (but not clauses)195
Number of constraints which are nor clauses,nor cardinality constraints39488
Minimum length of a constraint1
Maximum length of a constraint361

Trace number 6350

Launcher Data

LAUNCH ON wulflinc15 THE 2005-09-20 05:47:34 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3507 boxname=wulflinc15 idbench=1163 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  63aca17b11625a83c7613ee93b3a2e23  /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-van.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-van.opb
IDLAUNCH: 3507
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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	: 890.88

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        765356 kB
Buffers:         13656 kB
Cached:         225844 kB
SwapCached:        744 kB
Active:         154024 kB
Inactive:        88080 kB
HighTotal:      131008 kB
HighFree:         3808 kB
LowTotal:       903652 kB
LowFree:        761548 kB
SwapTotal:     2097136 kB
SwapFree:      2095884 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           5720 kB
Slab:            21536 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 06:07:47 (client local time) WITH STATUS 0 IN 1204.6 SECONDS
stats: 3507 7 1204.6 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/31945/stat): 31945 (minisat+_script) R 31944 31945 31778 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1797895871 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/31945/statm): 174 3 169 147 0 27 0
[pid=31945] 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=31946
New process pid=31947
New process pid=31948
execve syscall for /bin/sed executable
One traced child (pid=31947) 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=31948) exited with status: 0
One traced child (pid=31946) exited with status: 0
New process pid=31949
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-van.opb

[startup+10.0036 s]
Raw data (loadavg): 0.97 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 1166 0 0 0 983 5 0 0 25 0 1 0 1797895876 5545984 1100 4294967295 134512640 135094434 3221224448 3221223316 134796002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 1354 1100 145 145 0 1209 0
[pid=31949] vsize: 5416
Current children cumulated CPU time (s) 9.88
Current children cumulated vsize (Kb) 7540

[startup+20.0054 s]
Raw data (loadavg): 0.97 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 2250 0 0 0 1972 12 0 0 25 0 1 0 1797895876 10432512 2086 4294967295 134512640 135094434 3221224448 3221223328 134588013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 2547 2086 145 145 0 2402 0
[pid=31949] vsize: 10188
Current children cumulated CPU time (s) 19.84
Current children cumulated vsize (Kb) 12312

[startup+30.0062 s]
Raw data (loadavg): 0.98 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 3004 0 0 0 2963 17 0 0 25 0 1 0 1797895876 12386304 2840 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 3024 2840 145 145 0 2879 0
[pid=31949] vsize: 12096
Current children cumulated CPU time (s) 29.8
Current children cumulated vsize (Kb) 14220

[startup+40.0071 s]
Raw data (loadavg): 0.98 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 3304 0 0 0 3960 19 0 0 25 0 1 0 1797895876 17760256 3140 4294967295 134512640 135094434 3221224448 3221223332 134796010 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 4336 3140 145 145 0 4191 0
[pid=31949] vsize: 17344
Current children cumulated CPU time (s) 39.79
Current children cumulated vsize (Kb) 19468

[startup+50.0079 s]
Raw data (loadavg): 0.98 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 3591 0 0 0 4956 21 0 0 25 0 1 0 1797895876 18464768 3427 4294967295 134512640 135094434 3221224448 3221223360 134587900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31949/statm): 4508 3427 145 145 0 4363 0
[pid=31949] vsize: 18032
Current children cumulated CPU time (s) 49.77
Current children cumulated vsize (Kb) 20156

[startup+60.0087 s]
Raw data (loadavg): 0.98 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 3941 0 0 0 5952 23 0 0 25 0 1 0 1797895876 19361792 3777 4294967295 134512640 135094434 3221224448 3221223340 134796030 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 4727 3777 145 145 0 4582 0
[pid=31949] vsize: 18908
Current children cumulated CPU time (s) 59.75
Current children cumulated vsize (Kb) 21032

[startup+70.0095 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 4646 0 0 0 6946 26 0 0 25 0 1 0 1797895876 20996096 4317 4294967295 134512640 135094434 3221224448 3221223360 134587866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 5126 4317 145 145 0 4981 0
[pid=31949] vsize: 20504
Current children cumulated CPU time (s) 69.72
Current children cumulated vsize (Kb) 22628

[startup+80.0104 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 4905 0 0 0 7941 29 0 0 25 0 1 0 1797895876 21635072 4576 4294967295 134512640 135094434 3221224448 3221223316 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 5282 4576 145 145 0 5137 0
[pid=31949] vsize: 21128
Current children cumulated CPU time (s) 79.7
Current children cumulated vsize (Kb) 23252

[startup+90.0102 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) T 31945 31945 31778 0 -1 0 5302 0 0 0 8932 33 0 0 25 0 1 0 1797895876 23228416 4973 4294967295 134512640 135094434 3221224448 3221223384 134801661 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/31949/statm): 5671 4973 145 145 0 5526 0
[pid=31949] vsize: 22684
Current children cumulated CPU time (s) 89.65
Current children cumulated vsize (Kb) 24808

[startup+100.011 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 5677 0 0 0 9921 38 0 0 25 0 1 0 1797895876 24764416 5348 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 6046 5348 145 145 0 5901 0
[pid=31949] vsize: 24184
Current children cumulated CPU time (s) 99.59
Current children cumulated vsize (Kb) 26308

[startup+110.012 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 6015 0 0 0 10912 44 0 0 25 0 1 0 1797895876 26148864 5686 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31949/statm): 6384 5686 145 145 0 6239 0
[pid=31949] vsize: 25536
Current children cumulated CPU time (s) 109.56
Current children cumulated vsize (Kb) 27660

[startup+120.014 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 6326 0 0 0 11903 48 0 0 25 0 1 0 1797895876 27422720 5997 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 6695 5997 145 145 0 6550 0
[pid=31949] vsize: 26780
Current children cumulated CPU time (s) 119.51
Current children cumulated vsize (Kb) 28904

[startup+130.014 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 6652 0 0 0 12895 52 0 0 25 0 1 0 1797895876 28758016 6323 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 7021 6323 145 145 0 6876 0
[pid=31949] vsize: 28084
Current children cumulated CPU time (s) 129.47
Current children cumulated vsize (Kb) 30208

[startup+140.014 s]
Raw data (loadavg): 0.99 0.98 0.95 1/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) T 31945 31945 31778 0 -1 0 6975 0 0 0 13887 56 0 0 25 0 1 0 1797895876 30081024 6646 4294967295 134512640 135094434 3221224448 3221223384 134801661 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/31949/statm): 7344 6646 145 145 0 7199 0
[pid=31949] vsize: 29376
Current children cumulated CPU time (s) 139.43
Current children cumulated vsize (Kb) 31500

[startup+150.015 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 7318 0 0 0 14878 60 0 0 25 0 1 0 1797895876 31485952 6989 4294967295 134512640 135094434 3221224448 3221223360 134587905 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 7687 6989 145 145 0 7542 0
[pid=31949] vsize: 30748
Current children cumulated CPU time (s) 149.38
Current children cumulated vsize (Kb) 32872

[startup+160.016 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 7635 0 0 0 15868 65 0 0 25 0 1 0 1797895876 32784384 7306 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 8004 7306 145 145 0 7859 0
[pid=31949] vsize: 32016
Current children cumulated CPU time (s) 159.33
Current children cumulated vsize (Kb) 34140

[startup+170.017 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 7964 0 0 0 16862 68 0 0 25 0 1 0 1797895876 34131968 7635 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31949/statm): 8333 7635 145 145 0 8188 0
[pid=31949] vsize: 33332
Current children cumulated CPU time (s) 169.3
Current children cumulated vsize (Kb) 35456

[startup+180.018 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 8284 0 0 0 17854 71 0 0 25 0 1 0 1797895876 35442688 7955 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 8653 7955 145 145 0 8508 0
[pid=31949] vsize: 34612
Current children cumulated CPU time (s) 179.25
Current children cumulated vsize (Kb) 36736

[startup+190.018 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 8644 0 0 0 18843 78 0 0 25 0 1 0 1797895876 36917248 8315 4294967295 134512640 135094434 3221224448 3221223360 134587868 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 9013 8315 145 145 0 8868 0
[pid=31949] vsize: 36052
Current children cumulated CPU time (s) 189.21
Current children cumulated vsize (Kb) 38176

[startup+200.019 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) T 31945 31945 31778 0 -1 0 8959 0 0 0 19834 82 0 0 25 0 1 0 1797895876 38207488 8630 4294967295 134512640 135094434 3221224448 3221223368 134801661 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/31949/statm): 9328 8630 145 145 0 9183 0
[pid=31949] vsize: 37312
Current children cumulated CPU time (s) 199.16
Current children cumulated vsize (Kb) 39436

[startup+210.019 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 9298 0 0 0 20826 86 0 0 25 0 1 0 1797895876 39596032 8969 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 9667 8969 145 145 0 9522 0
[pid=31949] vsize: 38668
Current children cumulated CPU time (s) 209.12
Current children cumulated vsize (Kb) 40792

[startup+220.02 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 9607 0 0 0 21817 89 0 0 25 0 1 0 1797895876 40861696 9278 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 9976 9278 145 145 0 9831 0
[pid=31949] vsize: 39904
Current children cumulated CPU time (s) 219.06
Current children cumulated vsize (Kb) 42028

[startup+230.021 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 9943 0 0 0 22808 94 0 0 25 0 1 0 1797895876 42237952 9614 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31949/statm): 10312 9614 145 145 0 10167 0
[pid=31949] vsize: 41248
Current children cumulated CPU time (s) 229.02
Current children cumulated vsize (Kb) 43372

[startup+240.021 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 10226 0 0 0 23798 99 0 0 25 0 1 0 1797895876 43397120 9897 4294967295 134512640 135094434 3221224448 3221223332 134795999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 10595 9897 145 145 0 10450 0
[pid=31949] vsize: 42380
Current children cumulated CPU time (s) 238.97
Current children cumulated vsize (Kb) 44504

[startup+250.021 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) T 31945 31945 31778 0 -1 0 10587 0 0 0 24788 104 0 0 25 0 1 0 1797895876 44875776 10258 4294967295 134512640 135094434 3221224448 3221223384 134801661 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/31949/statm): 10956 10258 145 145 0 10811 0
[pid=31949] vsize: 43824
Current children cumulated CPU time (s) 248.92
Current children cumulated vsize (Kb) 45948

[startup+260.022 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 10906 0 0 0 25780 108 0 0 25 0 1 0 1797895876 46182400 10577 4294967295 134512640 135094434 3221224448 3221223332 134796018 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 11275 10577 145 145 0 11130 0
[pid=31949] vsize: 45100
Current children cumulated CPU time (s) 258.88
Current children cumulated vsize (Kb) 47224

[startup+270.023 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 11208 0 0 0 26772 111 0 0 25 0 1 0 1797895876 47419392 10879 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31949/statm): 11577 10879 145 145 0 11432 0
[pid=31949] vsize: 46308
Current children cumulated CPU time (s) 268.83
Current children cumulated vsize (Kb) 48432

[startup+280.024 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 11498 0 0 0 27762 116 0 0 25 0 1 0 1797895876 48607232 11169 4294967295 134512640 135094434 3221224448 3221223340 134796030 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 11867 11169 145 145 0 11722 0
[pid=31949] vsize: 47468
Current children cumulated CPU time (s) 278.78
Current children cumulated vsize (Kb) 49592

[startup+290.025 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 11812 0 0 0 28753 120 0 0 25 0 1 0 1797895876 49893376 11483 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31949/statm): 12181 11483 145 145 0 12036 0
[pid=31949] vsize: 48724
Current children cumulated CPU time (s) 288.73
Current children cumulated vsize (Kb) 50848

[startup+300.026 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 12130 0 0 0 29745 124 0 0 25 0 1 0 1797895876 51195904 11801 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 12499 11801 145 145 0 12354 0
[pid=31949] vsize: 49996
Current children cumulated CPU time (s) 298.69
Current children cumulated vsize (Kb) 52120

[startup+310.026 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 12441 0 0 0 30735 129 0 0 22 0 1 0 1797895876 52469760 12112 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31949/statm): 12810 12112 145 145 0 12665 0
[pid=31949] vsize: 51240
Current children cumulated CPU time (s) 308.64
Current children cumulated vsize (Kb) 53364

[startup+320.027 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 12757 0 0 0 31726 133 0 0 25 0 1 0 1797895876 53764096 12428 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31949/statm): 13126 12428 145 145 0 12981 0
[pid=31949] vsize: 52504
Current children cumulated CPU time (s) 318.59
Current children cumulated vsize (Kb) 54628

[startup+330.028 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 13099 0 0 0 32716 137 0 0 25 0 1 0 1797895876 55164928 12770 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31949/statm): 13468 12770 145 145 0 13323 0
[pid=31949] vsize: 53872
Current children cumulated CPU time (s) 328.53
Current children cumulated vsize (Kb) 55996

[startup+340.028 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 13397 0 0 0 33710 140 0 0 25 0 1 0 1797895876 56385536 13068 4294967295 134512640 135094434 3221224448 3221223340 134795992 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 13766 13068 145 145 0 13621 0
[pid=31949] vsize: 55064
Current children cumulated CPU time (s) 338.5
Current children cumulated vsize (Kb) 57188

[startup+350.029 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 13686 0 0 0 34703 143 0 0 25 0 1 0 1797895876 57569280 13357 4294967295 134512640 135094434 3221224448 3221223360 134587866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31949/statm): 14055 13357 145 145 0 13910 0
[pid=31949] vsize: 56220
Current children cumulated CPU time (s) 348.46
Current children cumulated vsize (Kb) 58344

[startup+360.029 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 14001 0 0 0 35694 147 0 0 25 0 1 0 1797895876 58859520 13672 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 14370 13672 145 145 0 14225 0
[pid=31949] vsize: 57480
Current children cumulated CPU time (s) 358.41
Current children cumulated vsize (Kb) 59604

[startup+370.03 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 14306 0 0 0 36686 151 0 0 25 0 1 0 1797895876 60108800 13977 4294967295 134512640 135094434 3221224448 3221223332 134796004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 14675 13977 145 145 0 14530 0
[pid=31949] vsize: 58700
Current children cumulated CPU time (s) 368.37
Current children cumulated vsize (Kb) 60824

[startup+380.031 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 14596 0 0 0 37677 156 0 0 25 0 1 0 1797895876 61296640 14267 4294967295 134512640 135094434 3221224448 3221223344 134587880 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 14965 14267 145 145 0 14820 0
[pid=31949] vsize: 59860
Current children cumulated CPU time (s) 378.33
Current children cumulated vsize (Kb) 61984

[startup+390.031 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 14914 0 0 0 38668 161 0 0 25 0 1 0 1797895876 62599168 14585 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 15283 14585 145 145 0 15138 0
[pid=31949] vsize: 61132
Current children cumulated CPU time (s) 388.29
Current children cumulated vsize (Kb) 63256

[startup+400.032 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 15232 0 0 0 39660 164 0 0 25 0 1 0 1797895876 63901696 14903 4294967295 134512640 135094434 3221224448 3221223332 134796021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 15601 14903 145 145 0 15456 0
[pid=31949] vsize: 62404
Current children cumulated CPU time (s) 398.24
Current children cumulated vsize (Kb) 64528

[startup+410.033 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 15556 0 0 0 40651 168 0 0 25 0 1 0 1797895876 65228800 15227 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31949/statm): 15925 15227 145 145 0 15780 0
[pid=31949] vsize: 63700
Current children cumulated CPU time (s) 408.19
Current children cumulated vsize (Kb) 65824

[startup+420.033 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 15851 0 0 0 41642 172 0 0 25 0 1 0 1797895876 66437120 15522 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 16220 15522 145 145 0 16075 0
[pid=31949] vsize: 64880
Current children cumulated CPU time (s) 418.14
Current children cumulated vsize (Kb) 67004

[startup+430.034 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 16179 0 0 0 42633 176 0 0 25 0 1 0 1797895876 67780608 15850 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 16548 15850 145 145 0 16403 0
[pid=31949] vsize: 66192
Current children cumulated CPU time (s) 428.09
Current children cumulated vsize (Kb) 68316

[startup+440.034 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 16494 0 0 0 43625 179 0 0 25 0 1 0 1797895876 69070848 16165 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 16863 16165 145 145 0 16718 0
[pid=31949] vsize: 67452
Current children cumulated CPU time (s) 438.04
Current children cumulated vsize (Kb) 69576

[startup+450.035 s]
Raw data (loadavg): 0.99 0.98 0.95 1/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) T 31945 31945 31778 0 -1 0 16805 0 0 0 44617 183 0 0 25 0 1 0 1797895876 70344704 16476 4294967295 134512640 135094434 3221224448 3221223384 134801661 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/31949/statm): 17174 16476 145 145 0 17029 0
[pid=31949] vsize: 68696
Current children cumulated CPU time (s) 448
Current children cumulated vsize (Kb) 70820

[startup+460.036 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 17127 0 0 0 45610 187 0 0 25 0 1 0 1797895876 71663616 16798 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 17496 16798 145 145 0 17351 0
[pid=31949] vsize: 69984
Current children cumulated CPU time (s) 457.97
Current children cumulated vsize (Kb) 72108

[startup+470.037 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 17470 0 0 0 46600 191 0 0 25 0 1 0 1797895876 73068544 17141 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31949/statm): 17839 17141 145 145 0 17694 0
[pid=31949] vsize: 71356
Current children cumulated CPU time (s) 467.91
Current children cumulated vsize (Kb) 73480

[startup+480.037 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) T 31945 31945 31778 0 -1 0 17770 0 0 0 47590 195 0 0 25 0 1 0 1797895876 74297344 17441 4294967295 134512640 135094434 3221224448 3221223384 134801661 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/31949/statm): 18139 17441 145 145 0 17994 0
[pid=31949] vsize: 72556
Current children cumulated CPU time (s) 477.85
Current children cumulated vsize (Kb) 74680

[startup+490.038 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 18048 0 0 0 48583 199 0 0 25 0 1 0 1797895876 75436032 17719 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 18417 17719 145 145 0 18272 0
[pid=31949] vsize: 73668
Current children cumulated CPU time (s) 487.82
Current children cumulated vsize (Kb) 75792

[startup+500.039 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 18391 0 0 0 49572 204 0 0 25 0 1 0 1797895876 76840960 18062 4294967295 134512640 135094434 3221224448 3221223332 134796009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 18760 18062 145 145 0 18615 0
[pid=31949] vsize: 75040
Current children cumulated CPU time (s) 497.76
Current children cumulated vsize (Kb) 77164

[startup+510.04 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) T 31945 31945 31778 0 -1 0 18709 0 0 0 50563 209 0 0 25 0 1 0 1797895876 78143488 18380 4294967295 134512640 135094434 3221224448 3221223384 134801661 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/31949/statm): 19078 18380 145 145 0 18933 0
[pid=31949] vsize: 76312
Current children cumulated CPU time (s) 507.72
Current children cumulated vsize (Kb) 78436

[startup+520.041 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 19000 0 0 0 51554 214 0 0 25 0 1 0 1797895876 79335424 18671 4294967295 134512640 135094434 3221224448 3221223360 134587900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 19369 18671 145 145 0 19224 0
[pid=31949] vsize: 77476
Current children cumulated CPU time (s) 517.68
Current children cumulated vsize (Kb) 79600

[startup+530.042 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 19311 0 0 0 52546 218 0 0 25 0 1 0 1797895876 80609280 18982 4294967295 134512640 135094434 3221224448 3221223360 134587866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31949/statm): 19680 18982 145 145 0 19535 0
[pid=31949] vsize: 78720
Current children cumulated CPU time (s) 527.64
Current children cumulated vsize (Kb) 80844

[startup+540.041 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 19644 0 0 0 53536 222 0 0 25 0 1 0 1797895876 81973248 19315 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 20013 19315 145 145 0 19868 0
[pid=31949] vsize: 80052
Current children cumulated CPU time (s) 537.58
Current children cumulated vsize (Kb) 82176

[startup+550.042 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 19941 0 0 0 54528 225 0 0 25 0 1 0 1797895876 83189760 19612 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 20310 19612 145 145 0 20165 0
[pid=31949] vsize: 81240
Current children cumulated CPU time (s) 547.53
Current children cumulated vsize (Kb) 83364

[startup+560.043 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 20260 0 0 0 55519 231 0 0 25 0 1 0 1797895876 84496384 19931 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 20629 19931 145 145 0 20484 0
[pid=31949] vsize: 82516
Current children cumulated CPU time (s) 557.5
Current children cumulated vsize (Kb) 84640

[startup+570.044 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 20585 0 0 0 56510 234 0 0 25 0 1 0 1797895876 85827584 20256 4294967295 134512640 135094434 3221224448 3221223360 134587900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 20954 20256 145 145 0 20809 0
[pid=31949] vsize: 83816
Current children cumulated CPU time (s) 567.44
Current children cumulated vsize (Kb) 85940

[startup+580.045 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 20933 0 0 0 57501 239 0 0 25 0 1 0 1797895876 87314432 20604 4294967295 134512640 135094434 3221224448 3221223332 134795999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 21317 20604 145 145 0 21172 0
[pid=31949] vsize: 85268
Current children cumulated CPU time (s) 577.4
Current children cumulated vsize (Kb) 87392

[startup+590.044 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 21237 0 0 0 58492 243 0 0 25 0 1 0 1797895876 88559616 20908 4294967295 134512640 135094434 3221224448 3221223360 134587866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31949/statm): 21621 20908 145 145 0 21476 0
[pid=31949] vsize: 86484
Current children cumulated CPU time (s) 587.35
Current children cumulated vsize (Kb) 88608

[startup+600.045 s]
Raw data (loadavg): 0.99 0.98 0.95 1/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) T 31945 31945 31778 0 -1 0 21545 0 0 0 59486 247 0 0 25 0 1 0 1797895876 89821184 21216 4294967295 134512640 135094434 3221224448 3221223384 134801661 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/31949/statm): 21929 21216 145 145 0 21784 0
[pid=31949] vsize: 87716
Current children cumulated CPU time (s) 597.33
Current children cumulated vsize (Kb) 89840

[startup+610.12 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 21862 0 0 0 60477 251 0 0 25 0 1 0 1797895876 91119616 21533 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 22246 21533 145 145 0 22101 0
[pid=31949] vsize: 88984
Current children cumulated CPU time (s) 607.28
Current children cumulated vsize (Kb) 91108

[startup+620.121 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 22149 0 0 0 61468 256 0 0 25 0 1 0 1797895876 92295168 21820 4294967295 134512640 135094434 3221224448 3221223360 134587866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 22533 21820 145 145 0 22388 0
[pid=31949] vsize: 90132
Current children cumulated CPU time (s) 617.24
Current children cumulated vsize (Kb) 92256

[startup+630.122 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 22456 0 0 0 62457 260 0 0 25 0 1 0 1797895876 93548544 22127 4294967295 134512640 135094434 3221224448 3221223360 134587873 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 22839 22127 145 145 0 22694 0
[pid=31949] vsize: 91356
Current children cumulated CPU time (s) 627.17
Current children cumulated vsize (Kb) 93480

[startup+640.122 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 22779 0 0 0 63449 264 0 0 25 0 1 0 1797895876 94871552 22450 4294967295 134512640 135094434 3221224448 3221223360 134587866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 23162 22450 145 145 0 23017 0
[pid=31949] vsize: 92648
Current children cumulated CPU time (s) 637.13
Current children cumulated vsize (Kb) 94772

[startup+650.122 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 23104 0 0 0 64441 268 0 0 25 0 1 0 1797895876 96202752 22775 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31949/statm): 23487 22775 145 145 0 23342 0
[pid=31949] vsize: 93948
Current children cumulated CPU time (s) 647.09
Current children cumulated vsize (Kb) 96072

[startup+660.123 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 23374 0 0 0 65431 272 0 0 25 0 1 0 1797895876 97308672 23045 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31949/statm): 23757 23045 145 145 0 23612 0
[pid=31949] vsize: 95028
Current children cumulated CPU time (s) 657.03
Current children cumulated vsize (Kb) 97152

[startup+670.125 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 23686 0 0 0 66422 276 0 0 25 0 1 0 1797895876 98586624 23357 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 24069 23357 145 145 0 23924 0
[pid=31949] vsize: 96276
Current children cumulated CPU time (s) 666.98
Current children cumulated vsize (Kb) 98400

[startup+680.126 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 24025 0 0 0 67412 282 0 0 25 0 1 0 1797895876 99975168 23696 4294967295 134512640 135094434 3221224448 3221223332 134796012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 24408 23696 145 145 0 24263 0
[pid=31949] vsize: 97632
Current children cumulated CPU time (s) 676.94
Current children cumulated vsize (Kb) 99756

[startup+690.126 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 24336 0 0 0 68403 287 0 0 25 0 1 0 1797895876 101249024 24007 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 24719 24007 145 145 0 24574 0
[pid=31949] vsize: 98876
Current children cumulated CPU time (s) 686.9
Current children cumulated vsize (Kb) 101000

[startup+700.126 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 24641 0 0 0 69394 291 0 0 25 0 1 0 1797895876 102498304 24312 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 25024 24312 145 145 0 24879 0
[pid=31949] vsize: 100096
Current children cumulated CPU time (s) 696.85
Current children cumulated vsize (Kb) 102220

[startup+710.127 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 24981 0 0 0 70385 295 0 0 25 0 1 0 1797895876 103890944 24652 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31949/statm): 25364 24652 145 145 0 25219 0
[pid=31949] vsize: 101456
Current children cumulated CPU time (s) 706.8
Current children cumulated vsize (Kb) 103580

[startup+720.128 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 25307 0 0 0 71376 300 0 0 25 0 1 0 1797895876 105226240 24978 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 25690 24978 145 145 0 25545 0
[pid=31949] vsize: 102760
Current children cumulated CPU time (s) 716.76
Current children cumulated vsize (Kb) 104884

[startup+730.129 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 25600 0 0 0 72367 305 0 0 25 0 1 0 1797895876 106426368 25271 4294967295 134512640 135094434 3221224448 3221223360 134587903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 25983 25271 145 145 0 25838 0
[pid=31949] vsize: 103932
Current children cumulated CPU time (s) 726.72
Current children cumulated vsize (Kb) 106056

[startup+740.13 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 25894 0 0 0 73360 308 0 0 25 0 1 0 1797895876 107630592 25565 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 26277 25565 145 145 0 26132 0
[pid=31949] vsize: 105108
Current children cumulated CPU time (s) 736.68
Current children cumulated vsize (Kb) 107232

[startup+750.131 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 26209 0 0 0 74352 313 0 0 25 0 1 0 1797895876 108916736 25880 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 26591 25880 145 145 0 26446 0
[pid=31949] vsize: 106364
Current children cumulated CPU time (s) 746.65
Current children cumulated vsize (Kb) 108488

[startup+760.131 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 26499 0 0 0 75344 317 0 0 25 0 1 0 1797895876 110104576 26170 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 26881 26170 145 145 0 26736 0
[pid=31949] vsize: 107524
Current children cumulated CPU time (s) 756.61
Current children cumulated vsize (Kb) 109648

[startup+770.132 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 26801 0 0 0 76335 320 0 0 25 0 1 0 1797895876 111341568 26472 4294967295 134512640 135094434 3221224448 3221223360 134587866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31949/statm): 27183 26472 145 145 0 27038 0
[pid=31949] vsize: 108732
Current children cumulated CPU time (s) 766.55
Current children cumulated vsize (Kb) 110856

[startup+780.133 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 27102 0 0 0 77325 325 0 0 25 0 1 0 1797895876 112574464 26773 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 27484 26773 145 145 0 27339 0
[pid=31949] vsize: 109936
Current children cumulated CPU time (s) 776.5
Current children cumulated vsize (Kb) 112060

[startup+790.134 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 27395 0 0 0 78317 329 0 0 25 0 1 0 1797895876 113774592 27066 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 27777 27066 145 145 0 27632 0
[pid=31949] vsize: 111108
Current children cumulated CPU time (s) 786.46
Current children cumulated vsize (Kb) 113232

[startup+800.135 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 27690 0 0 0 79306 335 0 0 25 0 1 0 1797895876 114982912 27361 4294967295 134512640 135094434 3221224448 3221223332 134796010 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 28072 27361 145 145 0 27927 0
[pid=31949] vsize: 112288
Current children cumulated CPU time (s) 796.41
Current children cumulated vsize (Kb) 114412

[startup+810.136 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 28031 0 0 0 80297 340 0 0 25 0 1 0 1797895876 116379648 27702 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 28413 27702 145 145 0 28268 0
[pid=31949] vsize: 113652
Current children cumulated CPU time (s) 806.37
Current children cumulated vsize (Kb) 115776

[startup+820.136 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 28352 0 0 0 81290 344 0 0 25 0 1 0 1797895876 117694464 28023 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 28734 28023 145 145 0 28589 0
[pid=31949] vsize: 114936
Current children cumulated CPU time (s) 816.34
Current children cumulated vsize (Kb) 117060

[startup+830.137 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 28675 0 0 0 82282 348 0 0 25 0 1 0 1797895876 119017472 28346 4294967295 134512640 135094434 3221224448 3221223360 134587903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31949/statm): 29057 28346 145 145 0 28912 0
[pid=31949] vsize: 116228
Current children cumulated CPU time (s) 826.3
Current children cumulated vsize (Kb) 118352

[startup+840.138 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 28998 0 0 0 83274 352 0 0 25 0 1 0 1797895876 120340480 28669 4294967295 134512640 135094434 3221224448 3221223332 134796010 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 29380 28669 145 145 0 29235 0
[pid=31949] vsize: 117520
Current children cumulated CPU time (s) 836.26
Current children cumulated vsize (Kb) 119644

[startup+850.139 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 29309 0 0 0 84266 356 0 0 25 0 1 0 1797895876 121614336 28980 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 29691 28980 145 145 0 29546 0
[pid=31949] vsize: 118764
Current children cumulated CPU time (s) 846.22
Current children cumulated vsize (Kb) 120888

[startup+860.14 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 29625 0 0 0 85257 361 0 0 25 0 1 0 1797895876 122908672 29296 4294967295 134512640 135094434 3221224448 3221223332 134796021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 30007 29296 145 145 0 29862 0
[pid=31949] vsize: 120028
Current children cumulated CPU time (s) 856.18
Current children cumulated vsize (Kb) 122152

[startup+870.14 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 29960 0 0 0 86249 365 0 0 25 0 1 0 1797895876 124280832 29631 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 30342 29631 145 145 0 30197 0
[pid=31949] vsize: 121368
Current children cumulated CPU time (s) 866.14
Current children cumulated vsize (Kb) 123492

[startup+880.141 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 30290 0 0 0 87240 370 0 0 25 0 1 0 1797895876 125628416 29961 4294967295 134512640 135094434 3221224448 3221223332 134796009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 30671 29961 145 145 0 30526 0
[pid=31949] vsize: 122684
Current children cumulated CPU time (s) 876.1
Current children cumulated vsize (Kb) 124808

[startup+890.141 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 30602 0 0 0 88231 374 0 0 25 0 1 0 1797895876 126906368 30273 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31949/statm): 30983 30273 145 145 0 30838 0
[pid=31949] vsize: 123932
Current children cumulated CPU time (s) 886.05
Current children cumulated vsize (Kb) 126056

[startup+900.142 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 30925 0 0 0 89222 378 0 0 25 0 1 0 1797895876 128229376 30596 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 31306 30596 145 145 0 31161 0
[pid=31949] vsize: 125224
Current children cumulated CPU time (s) 896
Current children cumulated vsize (Kb) 127348

[startup+910.143 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 31230 0 0 0 90214 382 0 0 25 0 1 0 1797895876 129478656 30901 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31949/statm): 31611 30901 145 145 0 31466 0
[pid=31949] vsize: 126444
Current children cumulated CPU time (s) 905.96
Current children cumulated vsize (Kb) 128568

[startup+920.144 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 31565 0 0 0 91204 387 0 0 25 0 1 0 1797895876 130850816 31236 4294967295 134512640 135094434 3221224448 3221223344 134587880 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31949/statm): 31946 31236 145 145 0 31801 0
[pid=31949] vsize: 127784
Current children cumulated CPU time (s) 915.91
Current children cumulated vsize (Kb) 129908

[startup+930.144 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 31867 0 0 0 92195 390 0 0 25 0 1 0 1797895876 132087808 31538 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31949/statm): 32248 31538 145 145 0 32103 0
[pid=31949] vsize: 128992
Current children cumulated CPU time (s) 925.85
Current children cumulated vsize (Kb) 131116

[startup+940.144 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 32220 0 0 0 93185 395 0 0 25 0 1 0 1797895876 133533696 31891 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31949/statm): 32601 31891 145 145 0 32456 0
[pid=31949] vsize: 130404
Current children cumulated CPU time (s) 935.8
Current children cumulated vsize (Kb) 132528

[startup+950.146 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 32557 0 0 0 94174 400 0 0 25 0 1 0 1797895876 134914048 32228 4294967295 134512640 135094434 3221224448 3221223360 134587866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31949/statm): 32938 32228 145 145 0 32793 0
[pid=31949] vsize: 131752
Current children cumulated CPU time (s) 945.74
Current children cumulated vsize (Kb) 133876

[startup+960.147 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 32888 0 0 0 95166 403 0 0 25 0 1 0 1797895876 136269824 32559 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 33269 32559 145 145 0 33124 0
[pid=31949] vsize: 133076
Current children cumulated CPU time (s) 955.69
Current children cumulated vsize (Kb) 135200

[startup+970.149 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 33240 0 0 0 96157 407 0 0 25 0 1 0 1797895876 137711616 32911 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31949/statm): 33621 32911 145 145 0 33476 0
[pid=31949] vsize: 134484
Current children cumulated CPU time (s) 965.64
Current children cumulated vsize (Kb) 136608

[startup+980.15 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 33816 0 0 0 97147 411 0 0 25 0 1 0 1797895876 140070912 33487 4294967295 134512640 135094434 3221224448 3221223332 134796010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31949/statm): 34197 33487 145 145 0 34052 0
[pid=31949] vsize: 136788
Current children cumulated CPU time (s) 975.58
Current children cumulated vsize (Kb) 138912

[startup+990.149 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 34384 0 0 0 98136 415 0 0 25 0 1 0 1797895876 142393344 34055 4294967295 134512640 135094434 3221224448 3221223360 134587868 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 34764 34055 145 145 0 34619 0
[pid=31949] vsize: 139056
Current children cumulated CPU time (s) 985.51
Current children cumulated vsize (Kb) 141180

[startup+1000.15 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 34840 0 0 0 99127 420 0 0 25 0 1 0 1797895876 144293888 34511 4294967295 134512640 135094434 3221224448 3221223340 134795992 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 35228 34511 145 145 0 35083 0
[pid=31949] vsize: 140912
Current children cumulated CPU time (s) 995.47
Current children cumulated vsize (Kb) 143036

[startup+1010.15 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 35173 0 0 0 100117 425 0 0 25 0 1 0 1797895876 145715200 34844 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31949/statm): 35575 34844 145 145 0 35430 0
[pid=31949] vsize: 142300
Current children cumulated CPU time (s) 1005.42
Current children cumulated vsize (Kb) 144424

[startup+1020.15 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 35496 0 0 0 101108 429 0 0 25 0 1 0 1797895876 147107840 35167 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 35915 35167 145 145 0 35770 0
[pid=31949] vsize: 143660
Current children cumulated CPU time (s) 1015.37
Current children cumulated vsize (Kb) 145784

[startup+1030.15 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 35811 0 0 0 102101 432 0 0 25 0 1 0 1797895876 148422656 35482 4294967295 134512640 135094434 3221224448 3221223360 134587905 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 36236 35482 145 145 0 36091 0
[pid=31949] vsize: 144944
Current children cumulated CPU time (s) 1025.33
Current children cumulated vsize (Kb) 147068

[startup+1040.15 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) T 31945 31945 31778 0 -1 0 36136 0 0 0 103091 437 0 0 25 0 1 0 1797895876 149807104 35807 4294967295 134512640 135094434 3221224448 3221223384 134801661 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/31949/statm): 36574 35807 145 145 0 36429 0
[pid=31949] vsize: 146296
Current children cumulated CPU time (s) 1035.28
Current children cumulated vsize (Kb) 148420

[startup+1050.15 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 36468 0 0 0 104081 442 0 0 25 0 1 0 1797895876 151203840 36139 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 36915 36139 145 145 0 36770 0
[pid=31949] vsize: 147660
Current children cumulated CPU time (s) 1045.23
Current children cumulated vsize (Kb) 149784

[startup+1060.16 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 36810 0 0 0 105072 446 0 0 25 0 1 0 1797895876 152616960 36481 4294967295 134512640 135094434 3221224448 3221223360 134587919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 37260 36481 145 145 0 37115 0
[pid=31949] vsize: 149040
Current children cumulated CPU time (s) 1055.18
Current children cumulated vsize (Kb) 151164

[startup+1070.16 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 37123 0 0 0 106062 451 0 0 25 0 1 0 1797895876 153972736 36794 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31949/statm): 37591 36794 145 145 0 37446 0
[pid=31949] vsize: 150364
Current children cumulated CPU time (s) 1065.13
Current children cumulated vsize (Kb) 152488

[startup+1080.16 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 37450 0 0 0 107052 455 0 0 25 0 1 0 1797895876 155295744 37121 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 37914 37121 145 145 0 37769 0
[pid=31949] vsize: 151656
Current children cumulated CPU time (s) 1075.07
Current children cumulated vsize (Kb) 153780

[startup+1090.16 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 37760 0 0 0 108044 459 0 0 25 0 1 0 1797895876 156622848 37431 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 38238 37431 145 145 0 38093 0
[pid=31949] vsize: 152952
Current children cumulated CPU time (s) 1085.03
Current children cumulated vsize (Kb) 155076

[startup+1100.16 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 38064 0 0 0 109036 464 0 0 25 0 1 0 1797895876 157917184 37735 4294967295 134512640 135094434 3221224448 3221223332 134796004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 38554 37735 145 145 0 38409 0
[pid=31949] vsize: 154216
Current children cumulated CPU time (s) 1095
Current children cumulated vsize (Kb) 156340

[startup+1110.16 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 38381 0 0 0 110029 467 0 0 25 0 1 0 1797895876 159236096 38052 4294967295 134512640 135094434 3221224448 3221223344 134587885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 38876 38052 145 145 0 38731 0
[pid=31949] vsize: 155504
Current children cumulated CPU time (s) 1104.96
Current children cumulated vsize (Kb) 157628

[startup+1120.16 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 38706 0 0 0 111021 470 0 0 25 0 1 0 1797895876 160632832 38377 4294967295 134512640 135094434 3221224448 3221223360 134587866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 39217 38377 145 145 0 39072 0
[pid=31949] vsize: 156868
Current children cumulated CPU time (s) 1114.91
Current children cumulated vsize (Kb) 158992

[startup+1130.16 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 39011 0 0 0 112013 475 0 0 25 0 1 0 1797895876 161894400 38682 4294967295 134512640 135094434 3221224448 3221223360 134587903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31949/statm): 39525 38682 145 145 0 39380 0
[pid=31949] vsize: 158100
Current children cumulated CPU time (s) 1124.88
Current children cumulated vsize (Kb) 160224

[startup+1140.16 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 39303 0 0 0 113004 479 0 0 25 0 1 0 1797895876 163115008 38974 4294967295 134512640 135094434 3221224448 3221223360 134587903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 39823 38974 145 145 0 39678 0
[pid=31949] vsize: 159292
Current children cumulated CPU time (s) 1134.83
Current children cumulated vsize (Kb) 161416

[startup+1150.16 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 39580 0 0 0 113995 483 0 0 25 0 1 0 1797895876 164311040 39251 4294967295 134512640 135094434 3221224448 3221223348 134587879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 40115 39251 145 145 0 39970 0
[pid=31949] vsize: 160460
Current children cumulated CPU time (s) 1144.78
Current children cumulated vsize (Kb) 162584

[startup+1160.16 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 39886 0 0 0 114987 486 0 0 25 0 1 0 1797895876 165601280 39557 4294967295 134512640 135094434 3221224448 3221223360 134587866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 40430 39557 145 145 0 40285 0
[pid=31949] vsize: 161720
Current children cumulated CPU time (s) 1154.73
Current children cumulated vsize (Kb) 163844

[startup+1170.16 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 40183 0 0 0 115980 489 0 0 25 0 1 0 1797895876 166846464 39854 4294967295 134512640 135094434 3221224448 3221223360 134587866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 40734 39854 145 145 0 40589 0
[pid=31949] vsize: 162936
Current children cumulated CPU time (s) 1164.69
Current children cumulated vsize (Kb) 165060

[startup+1180.16 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 40499 0 0 0 116972 493 0 0 25 0 1 0 1797895876 168165376 40170 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 41056 40170 145 145 0 40911 0
[pid=31949] vsize: 164224
Current children cumulated CPU time (s) 1174.65
Current children cumulated vsize (Kb) 166348

[startup+1190.16 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 40808 0 0 0 117963 498 0 0 25 0 1 0 1797895876 169459712 40479 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31949/statm): 41372 40479 145 145 0 41227 0
[pid=31949] vsize: 165488
Current children cumulated CPU time (s) 1184.61
Current children cumulated vsize (Kb) 167612

[startup+1200.17 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 41121 0 0 0 118954 502 0 0 25 0 1 0 1797895876 170758144 40792 4294967295 134512640 135094434 3221224448 3221223332 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 41689 40792 145 145 0 41544 0
[pid=31949] vsize: 166756
Current children cumulated CPU time (s) 1194.56
Current children cumulated vsize (Kb) 168880

[startup+1210.17 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 41405 0 0 0 119946 506 0 0 25 0 1 0 1797895876 171941888 41076 4294967295 134512640 135094434 3221224448 3221223340 134795992 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 41978 41076 145 145 0 41833 0
[pid=31949] vsize: 167912
Current children cumulated CPU time (s) 1204.52
Current children cumulated vsize (Kb) 170036



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.17 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 31949
Raw data (/proc/31945/stat): 31945 (minisat+_script) S 31944 31945 31778 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797895871 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31945/statm): 531 226 485 147 0 384 0
[pid=31945] vsize: 2124
Raw data (/proc/31949/stat): 31949 (minisat+_64-bit) R 31945 31945 31778 0 -1 0 41405 0 0 0 119946 506 0 0 25 0 1 0 1797895876 171941888 41076 4294967295 134512640 135094434 3221224448 3221223360 134587903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31949/statm): 41978 41076 145 145 0 41833 0
[pid=31949] vsize: 167912
Current children cumulated CPU time (s) 1204.52
Current children cumulated vsize (Kb) 170036

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

Child status: 0
Real time (s): 1210.25
CPU time (s): 1204.6
CPU user time (s): 1199.46
CPU system time (s): 5.13522
CPU usage (%): 99.5332
Max. virtual memory (cumulated for all children) (Kb): 170036



Verifier Data




ERROR: no interpretation found !