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/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-scsd8.opb
MD5SUM63dde7c8c3b02bd89e3e065c5bd58b69
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 82500
Biggest coefficient in the objective function 221357547985043456
Number of bits for the biggest coefficient in the objective function 58
Sum of the numbers in the objective function 595796164546237562880
Number of bits of the sum of numbers in the objective function 70
Biggest number in a constraint 221357547985043456
Number of bits of the biggest number in a constraint 58
Biggest sum of numbers in a constraint 595796164546237562880
Number of bits of the biggest sum of numbers70
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables82500
Total number of constraints397
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints397
Minimum length of a constraint300
Maximum length of a constraint720

Trace number 2653

Launcher Data

LAUNCH ON wulflinc18 THE 2005-09-18 20:32:57 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2809 boxname=wulflinc18 idbench=465 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  63dde7c8c3b02bd89e3e065c5bd58b69  /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-scsd8.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-scsd8.opb
IDLAUNCH: 2809
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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.177
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:        902156 kB
Buffers:         35432 kB
Cached:          61916 kB
SwapCached:        844 kB
Active:          76880 kB
Inactive:        23072 kB
HighTotal:      131008 kB
HighFree:        66192 kB
LowTotal:       903652 kB
LowFree:        835964 kB
SwapTotal:     2097892 kB
SwapFree:      2096548 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5764 kB
Slab:            26908 kB
Committed_AS:    64184 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 20:40:40 (client local time) WITH STATUS 0 IN 449.549 SECONDS
stats: 2809 7 449.549 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 2754] 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/6330/stat): 6330 (minisat+_script) R 6329 6330 31027 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1844129878 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/6330/statm): 174 3 169 147 0 27 0
[pid=6330] 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=6331
New process pid=6332
New process pid=6333
execve syscall for /bin/sed executable
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
One traced child (pid=6332) exited with status: 0
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=6333) exited with status: 0
One traced child (pid=6331) exited with status: 0
New process pid=6334
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-scsd8.opb
One traced child (pid=6334) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=6335
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-scsd8.opb

[startup+10.0036 s]
Raw data (loadavg): 0.93 0.97 0.96 1/57 6335
Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6330/statm): 532 234 485 147 0 385 0
[pid=6330] vsize: 2128
Raw data (/proc/6335/stat): 6335 (minisat+_bignum) T 6330 6330 31027 0 -1 0 4988 0 0 0 936 27 0 0 25 0 1 0 1844129886 23150592 4687 4294967295 134512640 135167914 3221224448 3221222652 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/6335/statm): 5652 4687 162 162 0 5490 0
[pid=6335] vsize: 22608
Current children cumulated CPU time (s) 9.65
Current children cumulated vsize (Kb) 24736

[startup+20.0046 s]
Raw data (loadavg): 0.94 0.97 0.96 2/57 6335
Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6330/statm): 532 234 485 147 0 385 0
[pid=6330] vsize: 2128
Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 7202 0 0 0 1902 42 0 0 25 0 1 0 1844129886 32219136 6901 4294967295 134512640 135167914 3221224448 3221223016 134846935 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6335/statm): 7866 6901 162 162 0 7704 0
[pid=6335] vsize: 31464
Current children cumulated CPU time (s) 19.46
Current children cumulated vsize (Kb) 33592

[startup+30.0065 s]
Raw data (loadavg): 0.95 0.97 0.96 2/57 6335
Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6330/statm): 532 234 485 147 0 385 0
[pid=6330] vsize: 2128
Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 9469 0 0 0 2873 56 0 0 25 0 1 0 1844129886 41504768 9168 4294967295 134512640 135167914 3221224448 3221222724 134845880 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6335/statm): 10133 9168 162 162 0 9971 0
[pid=6335] vsize: 40532
Current children cumulated CPU time (s) 29.31
Current children cumulated vsize (Kb) 42660

[startup+40.0074 s]
Raw data (loadavg): 0.96 0.97 0.96 2/57 6335
Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6330/statm): 532 234 485 147 0 385 0
[pid=6330] vsize: 2128
Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 12873 0 0 0 3833 77 0 0 25 0 1 0 1844129886 53448704 12088 4294967295 134512640 135167914 3221224448 3221223132 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6335/statm): 13049 12088 162 162 0 12887 0
[pid=6335] vsize: 52196
Current children cumulated CPU time (s) 39.12
Current children cumulated vsize (Kb) 54324

[startup+50.0084 s]
Raw data (loadavg): 0.96 0.97 0.96 2/57 6335
Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6330/statm): 532 234 485 147 0 385 0
[pid=6330] vsize: 2128
Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 18386 0 0 0 4788 101 0 0 25 0 1 0 1844129886 74674176 17271 4294967295 134512640 135167914 3221224448 3221116640 134625423 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6335/statm): 18231 17271 162 162 0 18069 0
[pid=6335] vsize: 72924
Current children cumulated CPU time (s) 48.91
Current children cumulated vsize (Kb) 75052

[startup+60.0093 s]
Raw data (loadavg): 0.97 0.97 0.96 2/57 6335
Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6330/statm): 532 234 485 147 0 385 0
[pid=6330] vsize: 2128
Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 24999 0 0 0 5733 128 0 0 25 0 1 0 1844129886 99061760 23225 4294967295 134512640 135167914 3221224448 3221119980 134625005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6335/statm): 24185 23225 162 162 0 24023 0
[pid=6335] vsize: 96740
Current children cumulated CPU time (s) 58.63
Current children cumulated vsize (Kb) 98868

[startup+70.0102 s]
Raw data (loadavg): 0.97 0.97 0.96 2/57 6335
Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6330/statm): 532 234 485 147 0 385 0
[pid=6330] vsize: 2128
Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 29529 0 0 0 6684 149 0 0 25 0 1 0 1844129886 112218112 26437 4294967295 134512640 135167914 3221224448 3221116096 134845911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6335/statm): 27397 26437 162 162 0 27235 0
[pid=6335] vsize: 109588
Current children cumulated CPU time (s) 68.35
Current children cumulated vsize (Kb) 111716

[startup+80.0121 s]
Raw data (loadavg): 0.98 0.97 0.96 2/57 6335
Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6330/statm): 532 234 485 147 0 385 0
[pid=6330] vsize: 2128
Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 38331 0 0 0 7632 179 0 0 25 0 1 0 1844129886 137469952 32602 4294967295 134512640 135167914 3221224448 3221117772 134619926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6335/statm): 33562 32602 162 162 0 33400 0
[pid=6335] vsize: 134248
Current children cumulated CPU time (s) 78.13
Current children cumulated vsize (Kb) 136376

[startup+90.013 s]
Raw data (loadavg): 0.98 0.97 0.96 1/57 6335
Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6330/statm): 532 234 485 147 0 385 0
[pid=6330] vsize: 2128
Raw data (/proc/6335/stat): 6335 (minisat+_bignum) T 6330 6330 31027 0 -1 0 42926 0 0 0 8579 201 0 0 25 0 1 0 1844129886 156295168 37197 4294967295 134512640 135167914 3221224448 3221115996 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/6335/statm): 38158 37197 162 162 0 37996 0
[pid=6335] vsize: 152632
Current children cumulated CPU time (s) 87.82
Current children cumulated vsize (Kb) 154760

[startup+100.013 s]
Raw data (loadavg): 0.98 0.97 0.96 2/57 6335
Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6330/statm): 532 234 485 147 0 385 0
[pid=6330] vsize: 2128
Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 47486 0 0 0 9526 224 0 0 25 0 1 0 1844129886 174968832 41757 4294967295 134512640 135167914 3221224448 3221116208 134619122 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6335/statm): 42717 41757 162 162 0 42555 0
[pid=6335] vsize: 170868
Current children cumulated CPU time (s) 97.52
Current children cumulated vsize (Kb) 172996

[startup+110.014 s]
Raw data (loadavg): 0.98 0.97 0.96 1/57 6335
Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6330/statm): 532 234 485 147 0 385 0
[pid=6330] vsize: 2128
Raw data (/proc/6335/stat): 6335 (minisat+_bignum) T 6330 6330 31027 0 -1 0 51996 0 0 0 10476 244 0 0 25 0 1 0 1844129886 193441792 46267 4294967295 134512640 135167914 3221224448 3221116156 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/6335/statm): 47227 46267 162 162 0 47065 0
[pid=6335] vsize: 188908
Current children cumulated CPU time (s) 107.22
Current children cumulated vsize (Kb) 191036

[startup+120.015 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 6335
Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6330/statm): 532 234 485 147 0 385 0
[pid=6330] vsize: 2128
Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 65107 0 0 0 11424 280 0 0 25 0 1 0 1844129886 225546240 54105 4294967295 134512640 135167914 3221224448 3221116400 134849061 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6335/statm): 55065 54105 162 162 0 54903 0
[pid=6335] vsize: 220260
Current children cumulated CPU time (s) 117.06
Current children cumulated vsize (Kb) 222388

[startup+130.016 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 6335
Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6330/statm): 532 234 485 147 0 385 0
[pid=6330] vsize: 2128
Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 69672 0 0 0 12376 302 0 0 25 0 1 0 1844129886 244244480 58670 4294967295 134512640 135167914 3221224448 3221116564 134697266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6335/statm): 59630 58670 162 162 0 59468 0
[pid=6335] vsize: 238520
Current children cumulated CPU time (s) 126.8
Current children cumulated vsize (Kb) 240648

[startup+140.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 6335
Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6330/statm): 532 234 485 147 0 385 0
[pid=6330] vsize: 2128
Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 74204 0 0 0 13327 325 0 0 25 0 1 0 1844129886 262807552 63202 4294967295 134512640 135167914 3221224448 3221120256 134845901 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6335/statm): 64162 63202 162 162 0 64000 0
[pid=6335] vsize: 256648
Current children cumulated CPU time (s) 136.54
Current children cumulated vsize (Kb) 258776

[startup+150.018 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 6335
Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6330/statm): 532 234 485 147 0 385 0
[pid=6330] vsize: 2128
Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 78674 0 0 0 14276 346 0 0 25 0 1 0 1844129886 281116672 67672 4294967295 134512640 135167914 3221224448 3221115888 134843030 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6335/statm): 68632 67672 162 162 0 68470 0
[pid=6335] vsize: 274528
Current children cumulated CPU time (s) 146.24
Current children cumulated vsize (Kb) 276656

[startup+160.019 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 6335
Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6330/statm): 532 234 485 147 0 385 0
[pid=6330] vsize: 2128
Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 83175 0 0 0 15226 367 0 0 25 0 1 0 1844129886 299552768 72173 4294967295 134512640 135167914 3221224448 3221119296 134849096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6335/statm): 73133 72173 162 162 0 72971 0
[pid=6335] vsize: 292532
Current children cumulated CPU time (s) 155.95
Current children cumulated vsize (Kb) 294660

[startup+170.019 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 6335
Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6330/statm): 532 234 485 147 0 385 0
[pid=6330] vsize: 2128
Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 87622 0 0 0 16176 387 0 0 25 0 1 0 1844129886 317767680 76620 4294967295 134512640 135167914 3221224448 3221119924 134697371 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6335/statm): 77580 76620 162 162 0 77418 0
[pid=6335] vsize: 310320
Current children cumulated CPU time (s) 165.65
Current children cumulated vsize (Kb) 312448

[startup+180.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 6335
Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6330/statm): 532 234 485 147 0 385 0
[pid=6330] vsize: 2128
Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 92044 0 0 0 17129 408 0 0 25 0 1 0 1844129886 335880192 81042 4294967295 134512640 135167914 3221224448 3221115440 134843426 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6335/statm): 82002 81042 162 162 0 81840 0
[pid=6335] vsize: 328008
Current children cumulated CPU time (s) 175.39
Current children cumulated vsize (Kb) 330136

[startup+190.022 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 6335
Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6330/statm): 532 234 485 147 0 385 0
[pid=6330] vsize: 2128
Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 96397 0 0 0 18078 428 0 0 25 0 1 0 1844129886 353710080 85395 4294967295 134512640 135167914 3221224448 3221117460 134697377 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6335/statm): 86355 85395 162 162 0 86193 0
[pid=6335] vsize: 345420
Current children cumulated CPU time (s) 185.08
Current children cumulated vsize (Kb) 347548

[startup+200.023 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 6335
Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6330/statm): 532 234 485 147 0 385 0
[pid=6330] vsize: 2128
Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 118050 0 0 0 19023 480 0 0 25 0 1 0 1844129886 399204352 96502 4294967295 134512640 135167914 3221224448 3221118288 134849196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6335/statm): 97462 96502 162 162 0 97300 0
[pid=6335] vsize: 389848
Current children cumulated CPU time (s) 195.05
Current children cumulated vsize (Kb) 391976

[startup+210.024 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 6335
Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6330/statm): 532 234 485 147 0 385 0
[pid=6330] vsize: 2128
Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 122674 0 0 0 19971 503 0 0 25 0 1 0 1844129886 418144256 101126 4294967295 134512640 135167914 3221224448 3221116520 134846921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6335/statm): 102086 101126 162 162 0 101924 0
[pid=6335] vsize: 408344
Current children cumulated CPU time (s) 204.76
Current children cumulated vsize (Kb) 410472

[startup+220.025 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 6335
Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6330/statm): 532 234 485 147 0 385 0
[pid=6330] vsize: 2128
Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 127302 0 0 0 20918 524 0 0 25 0 1 0 1844129886 437104640 105754 4294967295 134512640 135167914 3221224448 3221115520 134847159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6335/statm): 106715 105754 162 162 0 106553 0
[pid=6335] vsize: 426860
Current children cumulated CPU time (s) 214.44
Current children cumulated vsize (Kb) 428988

[startup+230.026 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 6335
Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6330/statm): 532 234 485 147 0 385 0
[pid=6330] vsize: 2128
Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 131867 0 0 0 21867 546 0 0 25 0 1 0 1844129886 455798784 110319 4294967295 134512640 135167914 3221224448 3221116448 134843064 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6335/statm): 111279 110319 162 162 0 111117 0
[pid=6335] vsize: 445116
Current children cumulated CPU time (s) 224.15
Current children cumulated vsize (Kb) 447244

[startup+240.027 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 6335
Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6330/statm): 532 234 485 147 0 385 0
[pid=6330] vsize: 2128
Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 136442 0 0 0 22817 566 0 0 25 0 1 0 1844129886 474537984 114894 4294967295 134512640 135167914 3221224448 3221116224 134844720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6335/statm): 115854 114894 162 162 0 115692 0
[pid=6335] vsize: 463416
Current children cumulated CPU time (s) 233.85
Current children cumulated vsize (Kb) 465544

[startup+250.028 s]
Raw data (loadavg): 0.99 0.97 0.96 1/57 6335
Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6330/statm): 532 234 485 147 0 385 0
[pid=6330] vsize: 2128
Raw data (/proc/6335/stat): 6335 (minisat+_bignum) T 6330 6330 31027 0 -1 0 140987 0 0 0 23766 588 0 0 25 0 1 0 1844129886 493158400 119439 4294967295 134512640 135167914 3221224448 3221115932 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/6335/statm): 120400 119439 162 162 0 120238 0
[pid=6335] vsize: 481600
Current children cumulated CPU time (s) 243.56
Current children cumulated vsize (Kb) 483728

[startup+260.03 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 6335
Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6330/statm): 532 234 485 147 0 385 0
[pid=6330] vsize: 2128
Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 145525 0 0 0 24712 610 0 0 25 0 1 0 1844129886 511741952 123977 4294967295 134512640 135167914 3221224448 3221118428 134694551 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6335/statm): 124937 123977 162 162 0 124775 0
[pid=6335] vsize: 499748
Current children cumulated CPU time (s) 253.24
Current children cumulated vsize (Kb) 501876

[startup+270.031 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 6335
Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6330/statm): 532 234 485 147 0 385 0
[pid=6330] vsize: 2128
Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 150080 0 0 0 25659 633 0 0 25 0 1 0 1844129886 530399232 128532 4294967295 134512640 135167914 3221224448 3221115748 134620525 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6335/statm): 129492 128532 162 162 0 129330 0
[pid=6335] vsize: 517968
Current children cumulated CPU time (s) 262.94
Current children cumulated vsize (Kb) 520096

[startup+280.032 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 6335
Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6330/statm): 532 234 485 147 0 385 0
[pid=6330] vsize: 2128
Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 154676 0 0 0 26605 655 0 0 25 0 1 0 1844129886 549224448 133128 4294967295 134512640 135167914 3221224448 3221116512 134843068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6335/statm): 134088 133128 162 162 0 133926 0
[pid=6335] vsize: 536352
Current children cumulated CPU time (s) 272.62
Current children cumulated vsize (Kb) 538480

[startup+290.033 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 6335
Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6330/statm): 532 234 485 147 0 385 0
[pid=6330] vsize: 2128
Raw data (/proc/6335/stat): 6335 (minisat+_bignum) T 6330 6330 31027 0 -1 0 159177 0 0 0 27557 677 0 0 25 0 1 0 1844129886 567660544 137629 4294967295 134512640 135167914 3221224448 3221115484 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/6335/statm): 138589 137629 162 162 0 138427 0
[pid=6335] vsize: 554356
Current children cumulated CPU time (s) 282.36
Current children cumulated vsize (Kb) 556484

[startup+300.032 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 6335
Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6330/statm): 532 234 485 147 0 385 0
[pid=6330] vsize: 2128
Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 163683 0 0 0 28508 697 0 0 25 0 1 0 1844129886 586117120 142135 4294967295 134512640 135167914 3221224448 3221115904 134696140 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6335/statm): 143095 142135 162 162 0 142933 0
[pid=6335] vsize: 572380
Current children cumulated CPU time (s) 292.07
Current children cumulated vsize (Kb) 574508

[startup+310.033 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 6335
Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6330/statm): 532 234 485 147 0 385 0
[pid=6330] vsize: 2128
Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 168138 0 0 0 29460 715 0 0 25 0 1 0 1844129886 604364800 146590 4294967295 134512640 135167914 3221224448 3221117296 134693582 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6335/statm): 147550 146590 162 162 0 147388 0
[pid=6335] vsize: 590200
Current children cumulated CPU time (s) 301.77
Current children cumulated vsize (Kb) 592328

[startup+320.034 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 6335
Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6330/statm): 532 234 485 147 0 385 0
[pid=6330] vsize: 2128
Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 172587 0 0 0 30409 736 0 0 25 0 1 0 1844129886 622587904 151039 4294967295 134512640 135167914 3221224448 3221119516 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6335/statm): 151999 151039 162 162 0 151837 0
[pid=6335] vsize: 607996
Current children cumulated CPU time (s) 311.47
Current children cumulated vsize (Kb) 610124

[startup+330.036 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 6335
Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6330/statm): 532 234 485 147 0 385 0
[pid=6330] vsize: 2128
Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 177052 0 0 0 31359 757 0 0 25 0 1 0 1844129886 640876544 155504 4294967295 134512640 135167914 3221224448 3221115968 134722524 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6335/statm): 156464 155504 162 162 0 156302 0
[pid=6335] vsize: 625856
Current children cumulated CPU time (s) 321.18
Current children cumulated vsize (Kb) 627984

[startup+340.037 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 6335
Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6330/statm): 532 234 485 147 0 385 0
[pid=6330] vsize: 2128
Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 207059 0 0 0 32254 834 0 0 25 0 1 0 1844129886 830418944 185512 4294967295 134512640 135167914 3221224448 3221118880 134625368 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6335/statm): 202739 185512 162 162 0 202577 0
[pid=6335] vsize: 810956
Current children cumulated CPU time (s) 330.9
Current children cumulated vsize (Kb) 813084

[startup+350.038 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 6335
Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6330/statm): 532 234 485 147 0 385 0
[pid=6330] vsize: 2128
Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 223327 0 0 0 33217 871 0 0 25 0 1 0 1844129886 830418944 201779 4294967295 134512640 135167914 3221224448 3221118704 134844706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6335/statm): 202739 201779 162 162 0 202577 0
[pid=6335] vsize: 810956
Current children cumulated CPU time (s) 340.9
Current children cumulated vsize (Kb) 813084

[startup+360.039 s]
Raw data (loadavg): 0.99 0.97 0.96 1/57 6335
Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6330/statm): 532 234 485 147 0 385 0
[pid=6330] vsize: 2128
Raw data (/proc/6335/stat): 6335 (minisat+_bignum) T 6330 6330 31027 0 -1 0 224761 0 0 0 34199 881 0 0 25 0 1 0 1844129886 749907968 182122 4294967295 134512640 135167914 3221224448 3221115996 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/6335/statm): 183083 182122 162 162 0 182921 0
[pid=6335] vsize: 732332
Current children cumulated CPU time (s) 350.82
Current children cumulated vsize (Kb) 734460

[startup+370.04 s]
Raw data (loadavg): 0.99 0.97 0.96 1/57 6335
Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6330/statm): 532 234 485 147 0 385 0
[pid=6330] vsize: 2128
Raw data (/proc/6335/stat): 6335 (minisat+_bignum) T 6330 6330 31027 0 -1 0 229380 0 0 0 35146 903 0 0 25 0 1 0 1844129886 768827392 186741 4294967295 134512640 135167914 3221224448 3221115676 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/6335/statm): 187702 186741 162 162 0 187540 0
[pid=6335] vsize: 750808
Current children cumulated CPU time (s) 360.51
Current children cumulated vsize (Kb) 752936

[startup+380.042 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 6335
Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6330/statm): 532 234 485 147 0 385 0
[pid=6330] vsize: 2128
Raw data (/proc/6335/stat): 6335 (minisat+_bignum) T 6330 6330 31027 0 -1 0 234057 0 0 0 36090 925 0 0 25 0 1 0 1844129886 787980288 191418 4294967295 134512640 135167914 3221224448 3221117788 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/6335/statm): 192378 191418 162 162 0 192216 0
[pid=6335] vsize: 769512
Current children cumulated CPU time (s) 370.17
Current children cumulated vsize (Kb) 771640

[startup+390.043 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 6335
Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6330/statm): 532 234 485 147 0 385 0
[pid=6330] vsize: 2128
Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 238696 0 0 0 37039 946 0 0 25 0 1 0 1844129886 806981632 196057 4294967295 134512640 135167914 3221224448 3221116828 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6335/statm): 197017 196057 162 162 0 196855 0
[pid=6335] vsize: 788068
Current children cumulated CPU time (s) 379.87
Current children cumulated vsize (Kb) 790196

[startup+400.044 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 6335
Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6330/statm): 532 234 485 147 0 385 0
[pid=6330] vsize: 2128
Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 243328 0 0 0 37986 968 0 0 25 0 1 0 1844129886 825954304 200689 4294967295 134512640 135167914 3221224448 3221116224 134843036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6335/statm): 201649 200689 162 162 0 201487 0
[pid=6335] vsize: 806596
Current children cumulated CPU time (s) 389.56
Current children cumulated vsize (Kb) 808724

[startup+410.045 s]
Raw data (loadavg): 0.99 0.97 0.96 1/57 6335
Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6330/statm): 532 234 485 147 0 385 0
[pid=6330] vsize: 2128
Raw data (/proc/6335/stat): 6335 (minisat+_bignum) T 6330 6330 31027 0 -1 0 247977 0 0 0 38937 990 0 0 25 0 1 0 1844129886 844996608 205338 4294967295 134512640 135167914 3221224448 3221118044 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/6335/statm): 206298 205338 162 162 0 206136 0
[pid=6335] vsize: 825192
Current children cumulated CPU time (s) 399.29
Current children cumulated vsize (Kb) 827320

[startup+420.046 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 6335
Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6330/statm): 532 234 485 147 0 385 0
[pid=6330] vsize: 2128
Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 252558 0 0 0 39885 1011 0 0 25 0 1 0 1844129886 863760384 209919 4294967295 134512640 135167914 3221224448 3221117968 134849082 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6335/statm): 210879 209919 162 162 0 210717 0
[pid=6335] vsize: 843516
Current children cumulated CPU time (s) 408.98
Current children cumulated vsize (Kb) 845644

[startup+430.048 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 6335
Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6330/statm): 532 234 485 147 0 385 0
[pid=6330] vsize: 2128
Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 257137 0 0 0 40834 1031 0 0 25 0 1 0 1844129886 882515968 214498 4294967295 134512640 135167914 3221224448 3221120896 134621017 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6335/statm): 215458 214498 162 162 0 215296 0
[pid=6335] vsize: 861832
Current children cumulated CPU time (s) 418.67
Current children cumulated vsize (Kb) 863960

[startup+440.048 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 6335
Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6330/statm): 532 234 485 147 0 385 0
[pid=6330] vsize: 2128
Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 261773 0 0 0 41786 1052 0 0 25 0 1 0 1844129886 901505024 219134 4294967295 134512640 135167914 3221224448 3221117072 134845901 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6335/statm): 220094 219134 162 162 0 219932 0
[pid=6335] vsize: 880376
Current children cumulated CPU time (s) 428.4
Current children cumulated vsize (Kb) 882504

[startup+450.048 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 6335
Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6330/statm): 532 234 485 147 0 385 0
[pid=6330] vsize: 2128
Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 266353 0 0 0 42734 1074 0 0 25 0 1 0 1844129886 920264704 223714 4294967295 134512640 135167914 3221224448 3221118416 134843030 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6335/statm): 224674 223714 162 162 0 224512 0
[pid=6335] vsize: 898696
Current children cumulated CPU time (s) 438.1
Current children cumulated vsize (Kb) 900824

[startup+460.049 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 6335
Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6330/statm): 532 234 485 147 0 385 0
[pid=6330] vsize: 2128
Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 270884 0 12 0 43667 1099 0 0 25 0 1 0 1844129886 938737664 227795 4294967295 134512640 135167914 3221224448 3221118132 134843000 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6335/statm): 229184 227795 162 162 0 229022 0
[pid=6335] vsize: 916736
Current children cumulated CPU time (s) 447.68
Current children cumulated vsize (Kb) 918864



Mem limit exceeded: sending SIGTERM then SIGKILL

[startup+461.67 s]
Raw data (loadavg): 0.99 0.97 0.96 1/57 6335
Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6330/statm): 532 234 485 147 0 385 0
[pid=6330] vsize: 2128
Raw data (/proc/6335/stat): 6335 (minisat+_bignum) T 6330 6330 31027 0 -1 0 271693 0 31 0 43808 1104 0 0 25 0 1 0 1844129886 941543424 228528 4294967295 134512640 135167914 3221224448 3221118492 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/6335/statm): 229869 228528 162 162 0 229707 0
[pid=6335] vsize: 919476
Current children cumulated CPU time (s) 449.14
Current children cumulated vsize (Kb) 921604

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

Child status: 0
Real time (s): 462.094
CPU time (s): 449.549
CPU user time (s): 438.087
CPU system time (s): 11.4613
CPU usage (%): 97.2851
Max. virtual memory (cumulated for all children) (Kb): 921604

Verifier Data

ERROR: no interpretation found !