Some explanations

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

General information on the benchmark

Namemps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-blend2.opb
MD5SUM16b86ac5ad712621c8050f8776cfb803
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 88
Biggest coefficient in the objective function 24014225
Number of bits for the biggest coefficient in the objective function 25
Sum of the numbers in the objective function 235593725
Number of bits of the sum of numbers in the objective function 28
Biggest number in a constraint 8935312239624192
Number of bits of the biggest number in a constraint 53
Biggest sum of numbers in a constraint 1346963845029350184
Number of bits of the biggest sum of numbers61
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables2944
Total number of constraints531
Number of constraints which are clauses9
Number of constraints which are cardinality constraints (but not clauses)310
Number of constraints which are nor clauses,nor cardinality constraints212
Minimum length of a constraint1
Maximum length of a constraint2659

Trace number 4486

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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:        841108 kB
Buffers:         34944 kB
Cached:         129232 kB
SwapCached:        792 kB
Active:          64756 kB
Inactive:       102052 kB
HighTotal:      131008 kB
HighFree:        44912 kB
LowTotal:       903652 kB
LowFree:        796196 kB
SwapTotal:     2097892 kB
SwapFree:      2096664 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5744 kB
Slab:            21208 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-19 17:56:41 (client local time) WITH STATUS 0 IN 659.449 SECONDS
stats: 2963 7 659.449 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 702] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...

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/30214/stat): 30214 (minisat+_script) R 30213 30214 19818 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1851789152 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/30214/statm): 174 3 169 147 0 27 0
[pid=30214] 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=30215
New process pid=30216
New process pid=30217
execve syscall for /bin/sed executable
One traced child (pid=30216) 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=30217) exited with status: 0
One traced child (pid=30215) exited with status: 0
New process pid=30218
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-20-10-blend2.opb
One traced child (pid=30218) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=30219
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-20-10-blend2.opb

[startup+10.0052 s]
Raw data (loadavg): 0.99 0.97 0.70 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 4820 0 3 0 926 20 0 0 25 0 1 0 1851789180 17432576 4106 4294967295 134512640 135167914 3221224448 3220804600 134619943 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30219/statm): 4256 4106 162 162 0 4094 0
[pid=30219] vsize: 17024
Current children cumulated CPU time (s) 9.55
Current children cumulated vsize (Kb) 19152

[startup+20.006 s]
Raw data (loadavg): 0.99 0.97 0.70 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 11198 0 3 0 1866 48 0 0 25 0 1 0 1851789180 40857600 9825 4294967295 134512640 135167914 3221224448 3220805968 134620274 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30219/statm): 9975 9825 162 162 0 9813 0
[pid=30219] vsize: 39900
Current children cumulated CPU time (s) 19.23
Current children cumulated vsize (Kb) 42028

[startup+30.0068 s]
Raw data (loadavg): 0.99 0.97 0.70 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 18459 0 3 0 2808 77 0 0 25 0 1 0 1851789180 65200128 15768 4294967295 134512640 135167914 3221224448 3220807292 134842996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30219/statm): 15918 15768 162 162 0 15756 0
[pid=30219] vsize: 63672
Current children cumulated CPU time (s) 28.94
Current children cumulated vsize (Kb) 65800

[startup+40.0076 s]
Raw data (loadavg): 0.99 0.97 0.71 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 27826 0 3 0 3754 107 0 0 25 0 1 0 1851789180 103567360 25135 4294967295 134512640 135167914 3221224448 3220806896 134844647 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30219/statm): 25285 25135 162 162 0 25123 0
[pid=30219] vsize: 101140
Current children cumulated CPU time (s) 38.7
Current children cumulated vsize (Kb) 103268

[startup+50.0094 s]
Raw data (loadavg): 0.99 0.97 0.71 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 32665 0 3 0 4704 129 0 0 25 0 1 0 1851789180 112586752 27337 4294967295 134512640 135167914 3221224448 3220810528 134694386 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30219/statm): 27487 27337 162 162 0 27325 0
[pid=30219] vsize: 109948
Current children cumulated CPU time (s) 48.42
Current children cumulated vsize (Kb) 112076

[startup+60.0102 s]
Raw data (loadavg): 0.99 0.97 0.71 1/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) T 30214 30214 19818 0 -1 0 37450 0 3 0 5655 151 0 0 25 0 1 0 1851789180 132186112 32122 4294967295 134512640 135167914 3221224448 3220804124 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/30219/statm): 32272 32122 162 162 0 32110 0
[pid=30219] vsize: 129088
Current children cumulated CPU time (s) 58.15
Current children cumulated vsize (Kb) 131216

[startup+70.0109 s]
Raw data (loadavg): 0.99 0.97 0.72 1/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) T 30214 30214 19818 0 -1 0 41956 0 3 0 6611 170 0 0 25 0 1 0 1851789180 150642688 36628 4294967295 134512640 135167914 3221224448 3220806684 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/30219/statm): 36778 36628 162 162 0 36616 0
[pid=30219] vsize: 147112
Current children cumulated CPU time (s) 67.9
Current children cumulated vsize (Kb) 149240

[startup+80.0118 s]
Raw data (loadavg): 0.99 0.97 0.72 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 55168 0 3 0 7553 210 0 0 25 0 1 0 1851789180 183160832 44567 4294967295 134512640 135167914 3221224448 3220814592 134843064 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30219/statm): 44717 44567 162 162 0 44555 0
[pid=30219] vsize: 178868
Current children cumulated CPU time (s) 77.72
Current children cumulated vsize (Kb) 180996

[startup+90.0125 s]
Raw data (loadavg): 0.99 0.97 0.72 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 59409 0 3 0 8504 230 0 0 25 0 1 0 1851789180 200531968 48808 4294967295 134512640 135167914 3221224448 3220804400 134621344 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30219/statm): 48958 48808 162 162 0 48796 0
[pid=30219] vsize: 195832
Current children cumulated CPU time (s) 87.43
Current children cumulated vsize (Kb) 197960

[startup+100.013 s]
Raw data (loadavg): 0.99 0.97 0.72 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 63473 0 3 0 9462 247 0 0 25 0 1 0 1851789180 217178112 52872 4294967295 134512640 135167914 3221224448 3220810448 134620938 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30219/statm): 53022 52872 162 162 0 52860 0
[pid=30219] vsize: 212088
Current children cumulated CPU time (s) 97.18
Current children cumulated vsize (Kb) 214216

[startup+110.014 s]
Raw data (loadavg): 0.99 0.97 0.73 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 67408 0 3 0 10420 264 0 0 25 0 1 0 1851789180 233295872 56807 4294967295 134512640 135167914 3221224448 3220804288 134624000 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30219/statm): 56957 56807 162 162 0 56795 0
[pid=30219] vsize: 227828
Current children cumulated CPU time (s) 106.93
Current children cumulated vsize (Kb) 229956

[startup+120.015 s]
Raw data (loadavg): 0.99 0.97 0.73 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 71242 0 3 0 11376 283 0 0 23 0 1 0 1851789180 248999936 60641 4294967295 134512640 135167914 3221224448 3220812800 134843010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30219/statm): 60791 60641 162 162 0 60629 0
[pid=30219] vsize: 243164
Current children cumulated CPU time (s) 116.68
Current children cumulated vsize (Kb) 245292

[startup+130.016 s]
Raw data (loadavg): 0.99 0.97 0.73 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 74893 0 3 0 12337 299 0 0 25 0 1 0 1851789180 263954432 64292 4294967295 134512640 135167914 3221224448 3220806400 134847156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30219/statm): 64442 64292 162 162 0 64280 0
[pid=30219] vsize: 257768
Current children cumulated CPU time (s) 126.45
Current children cumulated vsize (Kb) 259896

[startup+140.017 s]
Raw data (loadavg): 0.99 0.97 0.73 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 78608 0 3 0 13302 314 0 0 25 0 1 0 1851789180 279171072 68007 4294967295 134512640 135167914 3221224448 3220807744 134845911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30219/statm): 68157 68007 162 162 0 67995 0
[pid=30219] vsize: 272628
Current children cumulated CPU time (s) 136.25
Current children cumulated vsize (Kb) 274756

[startup+150.018 s]
Raw data (loadavg): 0.99 0.97 0.74 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 82124 0 3 0 14262 330 0 0 23 0 1 0 1851789180 293572608 71523 4294967295 134512640 135167914 3221224448 3220818176 134844650 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30219/statm): 71673 71523 162 162 0 71511 0
[pid=30219] vsize: 286692
Current children cumulated CPU time (s) 146.01
Current children cumulated vsize (Kb) 288820

[startup+160.019 s]
Raw data (loadavg): 0.99 0.97 0.74 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 85469 0 3 0 15229 343 0 0 21 0 1 0 1851789180 307273728 74868 4294967295 134512640 135167914 3221224448 3220804720 134693563 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30219/statm): 75018 74868 162 162 0 74856 0
[pid=30219] vsize: 300072
Current children cumulated CPU time (s) 155.81
Current children cumulated vsize (Kb) 302200

[startup+170.019 s]
Raw data (loadavg): 0.99 0.97 0.74 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) T 30214 30214 19818 0 -1 0 107269 0 3 0 16171 395 0 0 25 0 1 0 1851789180 353370112 86122 4294967295 134512640 135167914 3221224448 3220803964 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/30219/statm): 86272 86122 162 162 0 86110 0
[pid=30219] vsize: 345088
Current children cumulated CPU time (s) 165.75
Current children cumulated vsize (Kb) 347216

[startup+180.02 s]
Raw data (loadavg): 0.99 0.97 0.74 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 110659 0 3 0 17133 410 0 0 25 0 1 0 1851789180 367255552 89512 4294967295 134512640 135167914 3221224448 3220806968 134849057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30219/statm): 89662 89512 162 162 0 89500 0
[pid=30219] vsize: 358648
Current children cumulated CPU time (s) 175.52
Current children cumulated vsize (Kb) 360776

[startup+190.02 s]
Raw data (loadavg): 0.99 0.97 0.74 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 113896 0 3 0 18098 425 0 0 25 0 1 0 1851789180 380514304 92749 4294967295 134512640 135167914 3221224448 3220807776 134843026 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30219/statm): 92899 92749 162 162 0 92737 0
[pid=30219] vsize: 371596
Current children cumulated CPU time (s) 185.32
Current children cumulated vsize (Kb) 373724

[startup+200.021 s]
Raw data (loadavg): 0.99 0.97 0.75 1/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) T 30214 30214 19818 0 -1 0 117050 0 3 0 19062 439 0 0 25 0 1 0 1851789180 393437184 95903 4294967295 134512640 135167914 3221224448 3220803964 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/30219/statm): 96054 95903 162 162 0 95892 0
[pid=30219] vsize: 384216
Current children cumulated CPU time (s) 195.1
Current children cumulated vsize (Kb) 386344

[startup+210.022 s]
Raw data (loadavg): 0.99 0.97 0.75 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 120260 0 3 0 20027 452 0 0 25 0 1 0 1851789180 406581248 99113 4294967295 134512640 135167914 3221224448 3220810640 134693573 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30219/statm): 99263 99113 162 162 0 99101 0
[pid=30219] vsize: 397052
Current children cumulated CPU time (s) 204.88
Current children cumulated vsize (Kb) 399180

[startup+220.023 s]
Raw data (loadavg): 0.99 0.97 0.75 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 123260 0 3 0 20995 466 0 0 25 0 1 0 1851789180 418869248 102113 4294967295 134512640 135167914 3221224448 3220804720 134693561 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30219/statm): 102263 102113 162 162 0 102101 0
[pid=30219] vsize: 409052
Current children cumulated CPU time (s) 214.7
Current children cumulated vsize (Kb) 411180

[startup+230.024 s]
Raw data (loadavg): 0.99 0.97 0.75 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 126418 0 3 0 21959 481 0 0 25 0 1 0 1851789180 431804416 105271 4294967295 134512640 135167914 3221224448 3220809880 134843032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30219/statm): 105421 105271 162 162 0 105259 0
[pid=30219] vsize: 421684
Current children cumulated CPU time (s) 224.49
Current children cumulated vsize (Kb) 423812

[startup+240.025 s]
Raw data (loadavg): 0.99 0.97 0.75 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 129295 0 3 0 22929 494 0 0 25 0 1 0 1851789180 443588608 108148 4294967295 134512640 135167914 3221224448 3220806736 134849082 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30219/statm): 108298 108148 162 162 0 108136 0
[pid=30219] vsize: 433192
Current children cumulated CPU time (s) 234.32
Current children cumulated vsize (Kb) 435320

[startup+250.025 s]
Raw data (loadavg): 0.99 0.97 0.75 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 132199 0 3 0 23897 507 0 0 25 0 1 0 1851789180 455483392 111052 4294967295 134512640 135167914 3221224448 3220808732 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30219/statm): 111202 111052 162 162 0 111040 0
[pid=30219] vsize: 444808
Current children cumulated CPU time (s) 244.13
Current children cumulated vsize (Kb) 446936

[startup+260.026 s]
Raw data (loadavg): 0.99 0.97 0.76 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 135343 0 3 0 24862 522 0 0 25 0 1 0 1851789180 468361216 114196 4294967295 134512640 135167914 3221224448 3220809072 134693563 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30219/statm): 114346 114196 162 162 0 114184 0
[pid=30219] vsize: 457384
Current children cumulated CPU time (s) 253.93
Current children cumulated vsize (Kb) 459512

[startup+270.026 s]
Raw data (loadavg): 1.07 0.99 0.76 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 137917 0 3 0 25837 533 0 0 25 0 1 0 1851789180 478904320 116770 4294967295 134512640 135167914 3221224448 3220810540 134849088 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30219/statm): 116920 116770 162 162 0 116758 0
[pid=30219] vsize: 467680
Current children cumulated CPU time (s) 263.79
Current children cumulated vsize (Kb) 469808

[startup+280.027 s]
Raw data (loadavg): 1.06 0.99 0.77 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 140811 0 3 0 26807 543 0 0 25 0 1 0 1851789180 490758144 119664 4294967295 134512640 135167914 3221224448 3220804416 134844644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30219/statm): 119814 119664 162 162 0 119652 0
[pid=30219] vsize: 479256
Current children cumulated CPU time (s) 273.59
Current children cumulated vsize (Kb) 481384

[startup+290.028 s]
Raw data (loadavg): 1.05 0.99 0.77 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 143828 0 3 0 27774 556 0 0 25 0 1 0 1851789180 503115776 122681 4294967295 134512640 135167914 3221224448 3220805648 134843139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30219/statm): 122831 122681 162 162 0 122669 0
[pid=30219] vsize: 491324
Current children cumulated CPU time (s) 283.39
Current children cumulated vsize (Kb) 493452

[startup+300.028 s]
Raw data (loadavg): 1.04 0.99 0.77 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 146335 0 3 0 28746 568 0 0 25 0 1 0 1851789180 513380352 125188 4294967295 134512640 135167914 3221224448 3220805472 134843406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30219/statm): 125337 125188 162 162 0 125175 0
[pid=30219] vsize: 501348
Current children cumulated CPU time (s) 293.23
Current children cumulated vsize (Kb) 503476

[startup+310.029 s]
Raw data (loadavg): 1.03 0.99 0.77 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 149089 0 3 0 29718 580 0 0 25 0 1 0 1851789180 524660736 127942 4294967295 134512640 135167914 3221224448 3220807024 134522492 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30219/statm): 128091 127942 162 162 0 127929 0
[pid=30219] vsize: 512364
Current children cumulated CPU time (s) 303.07
Current children cumulated vsize (Kb) 514492

[startup+320.029 s]
Raw data (loadavg): 1.03 0.99 0.77 1/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) T 30214 30214 19818 0 -1 0 152069 0 3 0 30685 593 0 0 25 0 1 0 1851789180 536858624 130922 4294967295 134512640 135167914 3221224448 3220804796 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/30219/statm): 131069 130922 162 162 0 130907 0
[pid=30219] vsize: 524276
Current children cumulated CPU time (s) 312.87
Current children cumulated vsize (Kb) 526404

[startup+330.03 s]
Raw data (loadavg): 1.02 0.99 0.78 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 154469 0 3 0 31657 604 0 0 25 0 1 0 1851789180 546684928 133322 4294967295 134512640 135167914 3221224448 3220805848 134843032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30219/statm): 133468 133322 162 162 0 133306 0
[pid=30219] vsize: 533872
Current children cumulated CPU time (s) 322.7
Current children cumulated vsize (Kb) 536000

[startup+340.03 s]
Raw data (loadavg): 1.02 0.99 0.78 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 156996 0 3 0 32630 616 0 0 25 0 1 0 1851789180 557035520 135849 4294967295 134512640 135167914 3221224448 3220807136 134844715 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30219/statm): 135995 135849 162 162 0 135833 0
[pid=30219] vsize: 543980
Current children cumulated CPU time (s) 332.55
Current children cumulated vsize (Kb) 546108

[startup+350.031 s]
Raw data (loadavg): 1.02 0.99 0.78 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 159997 0 3 0 33598 632 0 0 25 0 1 0 1851789180 569319424 138850 4294967295 134512640 135167914 3221224448 3220814200 134845939 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30219/statm): 138994 138850 162 162 0 138832 0
[pid=30219] vsize: 555976
Current children cumulated CPU time (s) 342.39
Current children cumulated vsize (Kb) 558104

[startup+360.031 s]
Raw data (loadavg): 1.01 0.99 0.78 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 162473 0 3 0 34571 643 0 0 25 0 1 0 1851789180 579457024 141326 4294967295 134512640 135167914 3221224448 3220804960 134843010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30219/statm): 141469 141326 162 162 0 141307 0
[pid=30219] vsize: 565876
Current children cumulated CPU time (s) 352.23
Current children cumulated vsize (Kb) 568004

[startup+370.031 s]
Raw data (loadavg): 1.01 0.99 0.78 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 164787 0 3 0 35547 653 0 0 25 0 1 0 1851789180 588935168 143640 4294967295 134512640 135167914 3221224448 3220805572 134845880 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30219/statm): 143783 143640 162 162 0 143621 0
[pid=30219] vsize: 575132
Current children cumulated CPU time (s) 362.09
Current children cumulated vsize (Kb) 577260

[startup+380.032 s]
Raw data (loadavg): 1.01 0.99 0.79 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 167703 0 3 0 36516 666 0 0 25 0 1 0 1851789180 600870912 146556 4294967295 134512640 135167914 3221224448 3220806144 134844723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30219/statm): 146697 146556 162 162 0 146535 0
[pid=30219] vsize: 586788
Current children cumulated CPU time (s) 371.91
Current children cumulated vsize (Kb) 588916

[startup+390.032 s]
Raw data (loadavg): 1.01 0.99 0.79 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 170258 0 3 0 37488 676 0 0 25 0 1 0 1851789180 611332096 149111 4294967295 134512640 135167914 3221224448 3220805168 134849102 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30219/statm): 149251 149111 162 162 0 149089 0
[pid=30219] vsize: 597004
Current children cumulated CPU time (s) 381.73
Current children cumulated vsize (Kb) 599132

[startup+400.034 s]
Raw data (loadavg): 1.00 0.99 0.79 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 212960 0 3 0 38385 776 0 0 25 0 1 0 1851789180 786239488 191813 4294967295 134512640 135167914 3221224448 3220803824 134843406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30219/statm): 191953 191813 162 162 0 191791 0
[pid=30219] vsize: 767812
Current children cumulated CPU time (s) 391.7
Current children cumulated vsize (Kb) 769940

[startup+410.036 s]
Raw data (loadavg): 1.00 0.99 0.79 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 213371 0 3 0 39377 781 0 0 25 0 1 0 1851789180 701534208 171133 4294967295 134512640 135167914 3221224448 3220804032 134694392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30219/statm): 171273 171133 162 162 0 171111 0
[pid=30219] vsize: 685092
Current children cumulated CPU time (s) 401.67
Current children cumulated vsize (Kb) 687220

[startup+420.036 s]
Raw data (loadavg): 1.00 0.99 0.79 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 215603 0 3 0 40352 791 0 0 25 0 1 0 1851789180 710676480 173365 4294967295 134512640 135167914 3221224448 3220804576 134844728 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30219/statm): 173505 173365 162 162 0 173343 0
[pid=30219] vsize: 694020
Current children cumulated CPU time (s) 411.52
Current children cumulated vsize (Kb) 696148

[startup+430.037 s]
Raw data (loadavg): 1.00 0.99 0.80 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 218304 0 3 0 41323 803 0 0 25 0 1 0 1851789180 721739776 176066 4294967295 134512640 135167914 3221224448 3220808104 134693624 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30219/statm): 176206 176066 162 162 0 176044 0
[pid=30219] vsize: 704824
Current children cumulated CPU time (s) 421.35
Current children cumulated vsize (Kb) 706952

[startup+440.038 s]
Raw data (loadavg): 1.00 0.99 0.80 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 221004 0 3 0 42295 814 0 0 25 0 1 0 1851789180 732786688 178766 4294967295 134512640 135167914 3221224448 3220806656 134843160 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30219/statm): 178903 178766 162 162 0 178741 0
[pid=30219] vsize: 715612
Current children cumulated CPU time (s) 431.18
Current children cumulated vsize (Kb) 717740

[startup+450.039 s]
Raw data (loadavg): 1.00 0.99 0.80 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 223121 0 3 0 43273 823 0 0 25 0 1 0 1851789180 741453824 180883 4294967295 134512640 135167914 3221224448 3220806592 134843160 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30219/statm): 181019 180883 162 162 0 180857 0
[pid=30219] vsize: 724076
Current children cumulated CPU time (s) 441.05
Current children cumulated vsize (Kb) 726204

[startup+460.039 s]
Raw data (loadavg): 1.00 0.99 0.80 1/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) T 30214 30214 19818 0 -1 0 225265 0 3 0 44251 833 0 0 25 0 1 0 1851789180 750235648 183027 4294967295 134512640 135167914 3221224448 3220803964 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/30219/statm): 183163 183027 162 162 0 183001 0
[pid=30219] vsize: 732652
Current children cumulated CPU time (s) 450.93
Current children cumulated vsize (Kb) 734780

[startup+470.04 s]
Raw data (loadavg): 1.00 0.99 0.80 1/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) T 30214 30214 19818 0 -1 0 227596 0 3 0 45227 843 0 0 25 0 1 0 1851789180 759783424 185358 4294967295 134512640 135167914 3221224448 3220804924 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/30219/statm): 185494 185358 162 162 0 185332 0
[pid=30219] vsize: 741976
Current children cumulated CPU time (s) 460.79
Current children cumulated vsize (Kb) 744104

[startup+480.041 s]
Raw data (loadavg): 1.00 0.99 0.81 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 230398 0 3 0 46196 855 0 0 25 0 1 0 1851789180 771252224 188160 4294967295 134512640 135167914 3221224448 3220808732 134722229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30219/statm): 188294 188160 162 162 0 188132 0
[pid=30219] vsize: 753176
Current children cumulated CPU time (s) 470.6
Current children cumulated vsize (Kb) 755304

[startup+490.041 s]
Raw data (loadavg): 1.00 0.99 0.81 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 232806 0 3 0 47171 866 0 0 25 0 1 0 1851789180 781107200 190568 4294967295 134512640 135167914 3221224448 3220806288 134849196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30219/statm): 190700 190568 162 162 0 190538 0
[pid=30219] vsize: 762800
Current children cumulated CPU time (s) 480.46
Current children cumulated vsize (Kb) 764928

[startup+500.042 s]
Raw data (loadavg): 1.00 0.99 0.81 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 234831 0 3 0 48152 873 0 0 25 0 1 0 1851789180 789397504 192593 4294967295 134512640 135167914 3221224448 3220806808 134845939 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30219/statm): 192724 192593 162 162 0 192562 0
[pid=30219] vsize: 770896
Current children cumulated CPU time (s) 490.34
Current children cumulated vsize (Kb) 773024

[startup+510.042 s]
Raw data (loadavg): 1.00 0.99 0.81 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 236883 0 3 0 49130 883 0 0 25 0 1 0 1851789180 797802496 194645 4294967295 134512640 135167914 3221224448 3220807168 134849143 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30219/statm): 194776 194645 162 162 0 194614 0
[pid=30219] vsize: 779104
Current children cumulated CPU time (s) 500.22
Current children cumulated vsize (Kb) 781232

[startup+520.042 s]
Raw data (loadavg): 1.00 0.99 0.81 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 239349 0 3 0 50101 895 0 0 25 0 1 0 1851789180 807903232 197111 4294967295 134512640 135167914 3221224448 3220805592 134845877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30219/statm): 197242 197111 162 162 0 197080 0
[pid=30219] vsize: 788968
Current children cumulated CPU time (s) 510.05
Current children cumulated vsize (Kb) 791096

[startup+530.043 s]
Raw data (loadavg): 1.00 0.99 0.81 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 242013 0 3 0 51075 905 0 0 25 0 1 0 1851789180 818806784 199775 4294967295 134512640 135167914 3221224448 3220813376 134843026 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30219/statm): 199904 199775 162 162 0 199742 0
[pid=30219] vsize: 799616
Current children cumulated CPU time (s) 519.89
Current children cumulated vsize (Kb) 801744

[startup+540.044 s]
Raw data (loadavg): 1.00 0.99 0.82 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 244181 0 3 0 52051 914 0 0 25 0 1 0 1851789180 827682816 201943 4294967295 134512640 135167914 3221224448 3220809552 134845933 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30219/statm): 202071 201943 162 162 0 201909 0
[pid=30219] vsize: 808284
Current children cumulated CPU time (s) 529.74
Current children cumulated vsize (Kb) 810412

[startup+550.045 s]
Raw data (loadavg): 1.00 0.99 0.82 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 246127 0 3 0 53028 924 0 0 25 0 1 0 1851789180 835649536 203889 4294967295 134512640 135167914 3221224448 3220805888 134695806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30219/statm): 204016 203889 162 162 0 203854 0
[pid=30219] vsize: 816064
Current children cumulated CPU time (s) 539.61
Current children cumulated vsize (Kb) 818192

[startup+560.045 s]
Raw data (loadavg): 1.00 0.99 0.82 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) T 30214 30214 19818 0 -1 0 248152 0 3 0 54008 932 0 0 25 0 1 0 1851789180 843943936 205914 4294967295 134512640 135167914 3221224448 3220805788 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/30219/statm): 206041 205914 162 162 0 205879 0
[pid=30219] vsize: 824164
Current children cumulated CPU time (s) 549.49
Current children cumulated vsize (Kb) 826292

[startup+570.046 s]
Raw data (loadavg): 1.00 0.99 0.82 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 250849 0 3 0 54980 945 0 0 25 0 1 0 1851789180 854990848 208611 4294967295 134512640 135167914 3221224448 3220804888 134843032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30219/statm): 208738 208611 162 162 0 208576 0
[pid=30219] vsize: 834952
Current children cumulated CPU time (s) 559.34
Current children cumulated vsize (Kb) 837080

[startup+580.047 s]
Raw data (loadavg): 1.00 0.99 0.82 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 253228 0 3 0 55952 957 0 0 25 0 1 0 1851789180 864722944 210990 4294967295 134512640 135167914 3221224448 3220804192 134843139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30219/statm): 211114 210990 162 162 0 210952 0
[pid=30219] vsize: 844456
Current children cumulated CPU time (s) 569.18
Current children cumulated vsize (Kb) 846584

[startup+590.048 s]
Raw data (loadavg): 1.00 0.99 0.82 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 255219 0 3 0 56928 967 0 0 25 0 1 0 1851789180 872873984 212976 4294967295 134512640 135167914 3221224448 3220809088 134619209 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30219/statm): 213104 212976 162 162 0 212942 0
[pid=30219] vsize: 852416
Current children cumulated CPU time (s) 579.04
Current children cumulated vsize (Kb) 854544

[startup+600.049 s]
Raw data (loadavg): 1.00 0.99 0.82 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 257104 0 5 0 57902 976 0 0 25 0 1 0 1851789180 880545792 214776 4294967295 134512640 135167914 3221224448 3220812912 134845913 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30219/statm): 214977 214776 162 162 0 214815 0
[pid=30219] vsize: 859908
Current children cumulated CPU time (s) 588.87
Current children cumulated vsize (Kb) 862036

[startup+610.05 s]
Raw data (loadavg): 1.00 0.99 0.82 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 259105 0 27 0 58861 986 0 0 25 0 1 0 1851789180 888401920 216597 4294967295 134512640 135167914 3221224448 3220804004 134845880 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30219/statm): 216895 216597 162 162 0 216733 0
[pid=30219] vsize: 867580
Current children cumulated CPU time (s) 598.56
Current children cumulated vsize (Kb) 869708

[startup+620.05 s]
Raw data (loadavg): 1.00 0.99 0.83 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 261431 0 54 0 59809 996 0 0 25 0 1 0 1851789180 897343488 218830 4294967295 134512640 135167914 3221224448 3220804528 134623813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30219/statm): 219078 218830 162 162 0 218916 0
[pid=30219] vsize: 876312
Current children cumulated CPU time (s) 608.14
Current children cumulated vsize (Kb) 878440

[startup+630.051 s]
Raw data (loadavg): 1.00 0.99 0.83 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 264336 0 71 0 60763 1008 0 0 25 0 1 0 1851789180 908484608 221665 4294967295 134512640 135167914 3221224448 3220818176 134843107 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30219/statm): 221798 221665 162 162 0 221636 0
[pid=30219] vsize: 887192
Current children cumulated CPU time (s) 617.8
Current children cumulated vsize (Kb) 889320

[startup+640.052 s]
Raw data (loadavg): 1.00 0.99 0.83 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) T 30214 30214 19818 0 -1 0 266606 0 79 0 61733 1017 0 0 25 0 1 0 1851789180 917680128 223897 4294967295 134512640 135167914 3221224448 3220804812 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/30219/statm): 224043 223897 162 162 0 223881 0
[pid=30219] vsize: 896172
Current children cumulated CPU time (s) 627.59
Current children cumulated vsize (Kb) 898300

[startup+650.053 s]
Raw data (loadavg): 1.07 1.00 0.83 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 268435 0 103 0 62691 1025 0 0 25 0 1 0 1851789180 924905472 225538 4294967295 134512640 135167914 3221224448 3220813008 134845895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30219/statm): 225807 225538 162 162 0 225645 0
[pid=30219] vsize: 903228
Current children cumulated CPU time (s) 637.25
Current children cumulated vsize (Kb) 905356

[startup+660.053 s]
Raw data (loadavg): 1.06 1.00 0.83 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 270361 0 161 0 63615 1034 0 0 25 0 1 0 1851789180 931975168 227145 4294967295 134512640 135167914 3221224448 3220804724 134849060 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30219/statm): 227533 227147 162 162 0 227371 0
[pid=30219] vsize: 910132
Current children cumulated CPU time (s) 646.58
Current children cumulated vsize (Kb) 912260

[startup+670.053 s]
Raw data (loadavg): 1.05 1.00 0.84 2/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) T 30214 30214 19818 0 -1 0 272342 0 192 0 64567 1044 0 0 25 0 1 0 1851789180 939249664 229046 4294967295 134512640 135167914 3221224448 3220806012 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/30219/statm): 229309 229046 162 162 0 229147 0
[pid=30219] vsize: 917236
Current children cumulated CPU time (s) 656.2
Current children cumulated vsize (Kb) 919364



Mem limit exceeded: sending SIGTERM then SIGKILL

[startup+673.069 s]
Raw data (loadavg): 1.05 1.00 0.84 1/57 30219
Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30214/statm): 532 234 485 147 0 385 0
[pid=30214] vsize: 2128
Raw data (/proc/30219/stat): 30219 (minisat+_bignum) T 30214 30214 19818 0 -1 0 272962 0 199 0 64854 1047 0 0 25 0 1 0 1851789180 941543424 229660 4294967295 134512640 135167914 3221224448 3220805756 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/30219/statm): 229869 229660 162 162 0 229707 0
[pid=30219] vsize: 919476
Current children cumulated CPU time (s) 659.1
Current children cumulated vsize (Kb) 921604

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

Child status: 0
Real time (s): 673.501
CPU time (s): 659.449
CPU user time (s): 648.549
CPU system time (s): 10.8993
CPU usage (%): 97.9136
Max. virtual memory (cumulated for all children) (Kb): 921604

Verifier Data

ERROR: no interpretation found !