Some explanations

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

General information on the benchmark

Namemps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-glass4.opb
MD5SUM758e74effa84acafd590b5cf55ba15ee
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 1015815551953
Optimality of the best value was proved NO
Number of terms in the objective function 351
Biggest coefficient in the objective function 524288000000
Number of bits for the biggest coefficient in the objective function 39
Sum of the numbers in the objective function 1048594922917
Number of bits of the sum of numbers in the objective function 40
Biggest number in a constraint 1075200000000000000
Number of bits of the biggest number in a constraint 60
Biggest sum of numbers in a constraint 2440670651161677657
Number of bits of the biggest sum of numbers62
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1202.77
Number of variables653
Total number of constraints707
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)338
Number of constraints which are nor clauses,nor cardinality constraints369
Minimum length of a constraint1
Maximum length of a constraint75

Trace number 6110

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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:        915668 kB
Buffers:          7432 kB
Cached:          83952 kB
SwapCached:        756 kB
Active:          20204 kB
Inactive:        73796 kB
HighTotal:      131008 kB
HighFree:        42896 kB
LowTotal:       903652 kB
LowFree:        872772 kB
SwapTotal:     2097892 kB
SwapFree:      2096608 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5716 kB
Slab:            19296 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 03:46:45 (client local time) WITH STATUS 0 IN 404.918 SECONDS
stats: 3296 7 404.918 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 647] 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/6414/stat): 6414 (minisat+_script) R 6413 6414 20728 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1855366711 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/6414/statm): 174 3 169 147 0 27 0
[pid=6414] 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=6415
New process pid=6416
New process pid=6417
execve syscall for /bin/sed executable
One traced child (pid=6416) 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=6417) exited with status: 0
One traced child (pid=6415) exited with status: 0
New process pid=6418
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-glass4.opb
One traced child (pid=6418) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=6419
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-glass4.opb

[startup+10.0035 s]
Raw data (loadavg): 0.93 0.95 0.94 2/57 6419
Raw data (/proc/6414/stat): 6414 (minisat+_script) S 6413 6414 20728 0 -1 0 314 368 0 0 0 1 1 1 21 0 1 0 1855366711 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6414/statm): 532 234 485 147 0 385 0
[pid=6414] vsize: 2128
Raw data (/proc/6419/stat): 6419 (minisat+_bignum) R 6414 6414 20728 0 -1 0 5634 0 0 0 940 25 0 0 25 0 1 0 1855366719 20889600 5000 4294967295 134512640 135167914 3221224448 3221206368 134845927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6419/statm): 5100 5000 162 162 0 4938 0
[pid=6419] vsize: 20400
Current children cumulated CPU time (s) 9.68
Current children cumulated vsize (Kb) 22528

[startup+20.0042 s]
Raw data (loadavg): 0.94 0.96 0.94 2/57 6419
Raw data (/proc/6414/stat): 6414 (minisat+_script) S 6413 6414 20728 0 -1 0 314 368 0 0 0 1 1 1 21 0 1 0 1855366711 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6414/statm): 532 234 485 147 0 385 0
[pid=6414] vsize: 2128
Raw data (/proc/6419/stat): 6419 (minisat+_bignum) R 6414 6414 20728 0 -1 0 13853 0 0 0 1885 56 0 0 25 0 1 0 1855366719 46456832 11242 4294967295 134512640 135167914 3221224448 3221206720 134843074 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6419/statm): 11342 11242 162 162 0 11180 0
[pid=6419] vsize: 45368
Current children cumulated CPU time (s) 19.44
Current children cumulated vsize (Kb) 47496

[startup+30.0079 s]
Raw data (loadavg): 0.95 0.96 0.94 2/57 6419
Raw data (/proc/6414/stat): 6414 (minisat+_script) S 6413 6414 20728 0 -1 0 314 368 0 0 0 1 1 1 21 0 1 0 1855366711 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6414/statm): 532 234 485 147 0 385 0
[pid=6414] vsize: 2128
Raw data (/proc/6419/stat): 6419 (minisat+_bignum) R 6414 6414 20728 0 -1 0 18551 0 0 0 2825 80 0 0 25 0 1 0 1855366719 65699840 15940 4294967295 134512640 135167914 3221224448 3221207776 134694383 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6419/statm): 16040 15940 162 162 0 15878 0
[pid=6419] vsize: 64160
Current children cumulated CPU time (s) 29.08
Current children cumulated vsize (Kb) 66288

[startup+40.0086 s]
Raw data (loadavg): 0.95 0.96 0.94 2/57 6419
Raw data (/proc/6414/stat): 6414 (minisat+_script) S 6413 6414 20728 0 -1 0 314 368 0 0 0 1 1 1 21 0 1 0 1855366711 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6414/statm): 532 234 485 147 0 385 0
[pid=6414] vsize: 2128
Raw data (/proc/6419/stat): 6419 (minisat+_bignum) T 6414 6414 20728 0 -1 0 27524 0 0 0 3769 111 0 0 25 0 1 0 1855366719 91652096 22276 4294967295 134512640 135167914 3221224448 3221206108 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/6419/statm): 22376 22276 162 162 0 22214 0
[pid=6419] vsize: 89504
Current children cumulated CPU time (s) 38.83
Current children cumulated vsize (Kb) 91632

[startup+50.0093 s]
Raw data (loadavg): 0.96 0.96 0.94 2/57 6419
Raw data (/proc/6414/stat): 6414 (minisat+_script) S 6413 6414 20728 0 -1 0 314 368 0 0 0 1 1 1 21 0 1 0 1855366711 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6414/statm): 532 234 485 147 0 385 0
[pid=6414] vsize: 2128
Raw data (/proc/6419/stat): 6419 (minisat+_bignum) R 6414 6414 20728 0 -1 0 32405 0 0 0 4715 134 0 0 25 0 1 0 1855366719 111644672 27157 4294967295 134512640 135167914 3221224448 3221207572 134849060 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6419/statm): 27257 27157 162 162 0 27095 0
[pid=6419] vsize: 109028
Current children cumulated CPU time (s) 48.52
Current children cumulated vsize (Kb) 111156

[startup+60.009 s]
Raw data (loadavg): 0.97 0.96 0.94 2/57 6419
Raw data (/proc/6414/stat): 6414 (minisat+_script) S 6413 6414 20728 0 -1 0 314 368 0 0 0 1 1 1 21 0 1 0 1855366711 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6414/statm): 532 234 485 147 0 385 0
[pid=6414] vsize: 2128
Raw data (/proc/6419/stat): 6419 (minisat+_bignum) R 6414 6414 20728 0 -1 0 37264 0 0 0 5657 158 0 0 25 0 1 0 1855366719 131547136 32016 4294967295 134512640 135167914 3221224448 3221206460 134522320 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6419/statm): 32116 32016 162 162 0 31954 0
[pid=6419] vsize: 128464
Current children cumulated CPU time (s) 58.18
Current children cumulated vsize (Kb) 130592

[startup+70.0107 s]
Raw data (loadavg): 0.97 0.96 0.94 2/57 6419
Raw data (/proc/6414/stat): 6414 (minisat+_script) S 6413 6414 20728 0 -1 0 314 368 0 0 0 1 1 1 21 0 1 0 1855366711 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6414/statm): 532 234 485 147 0 385 0
[pid=6414] vsize: 2128
Raw data (/proc/6419/stat): 6419 (minisat+_bignum) T 6414 6414 20728 0 -1 0 42117 0 0 0 6604 180 0 0 25 0 1 0 1855366719 151425024 36869 4294967295 134512640 135167914 3221224448 3221206300 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/6419/statm): 36969 36869 162 162 0 36807 0
[pid=6419] vsize: 147876
Current children cumulated CPU time (s) 67.87
Current children cumulated vsize (Kb) 150004

[startup+80.0114 s]
Raw data (loadavg): 0.98 0.96 0.94 2/57 6419
Raw data (/proc/6414/stat): 6414 (minisat+_script) S 6413 6414 20728 0 -1 0 314 368 0 0 0 1 1 1 21 0 1 0 1855366711 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6414/statm): 532 234 485 147 0 385 0
[pid=6414] vsize: 2128
Raw data (/proc/6419/stat): 6419 (minisat+_bignum) R 6414 6414 20728 0 -1 0 55600 0 0 0 7547 217 0 0 25 0 1 0 1855366719 185053184 45079 4294967295 134512640 135167914 3221224448 3221206868 134843117 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6419/statm): 45179 45079 162 162 0 45017 0
[pid=6419] vsize: 180716
Current children cumulated CPU time (s) 77.67
Current children cumulated vsize (Kb) 182844

[startup+90.0121 s]
Raw data (loadavg): 0.98 0.96 0.94 2/57 6419
Raw data (/proc/6414/stat): 6414 (minisat+_script) S 6413 6414 20728 0 -1 0 314 368 0 0 0 1 1 1 21 0 1 0 1855366711 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6414/statm): 532 234 485 147 0 385 0
[pid=6414] vsize: 2128
Raw data (/proc/6419/stat): 6419 (minisat+_bignum) R 6414 6414 20728 0 -1 0 60689 0 0 0 8490 243 0 0 25 0 1 0 1855366719 205897728 50168 4294967295 134512640 135167914 3221224448 3221206416 134843118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6419/statm): 50268 50168 162 162 0 50106 0
[pid=6419] vsize: 201072
Current children cumulated CPU time (s) 87.36
Current children cumulated vsize (Kb) 203200

[startup+100.013 s]
Raw data (loadavg): 0.98 0.96 0.94 2/57 6419
Raw data (/proc/6414/stat): 6414 (minisat+_script) S 6413 6414 20728 0 -1 0 314 368 0 0 0 1 1 1 21 0 1 0 1855366711 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6414/statm): 532 234 485 147 0 385 0
[pid=6414] vsize: 2128
Raw data (/proc/6419/stat): 6419 (minisat+_bignum) R 6414 6414 20728 0 -1 0 65730 0 0 0 9433 266 0 0 25 0 1 0 1855366719 226545664 55209 4294967295 134512640 135167914 3221224448 3221206928 134620299 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6419/statm): 55309 55209 162 162 0 55147 0
[pid=6419] vsize: 221236
Current children cumulated CPU time (s) 97.02
Current children cumulated vsize (Kb) 223364

[startup+110.013 s]
Raw data (loadavg): 0.98 0.96 0.94 1/57 6419
Raw data (/proc/6414/stat): 6414 (minisat+_script) S 6413 6414 20728 0 -1 0 314 368 0 0 0 1 1 1 21 0 1 0 1855366711 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6414/statm): 532 234 485 147 0 385 0
[pid=6414] vsize: 2128
Raw data (/proc/6419/stat): 6419 (minisat+_bignum) T 6414 6414 20728 0 -1 0 70758 0 0 0 10378 291 0 0 25 0 1 0 1855366719 247140352 60237 4294967295 134512640 135167914 3221224448 3221206268 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/6419/statm): 60337 60237 162 162 0 60175 0
[pid=6419] vsize: 241348
Current children cumulated CPU time (s) 106.72
Current children cumulated vsize (Kb) 243476

[startup+120.014 s]
Raw data (loadavg): 0.99 0.97 0.94 1/57 6419
Raw data (/proc/6414/stat): 6414 (minisat+_script) S 6413 6414 20728 0 -1 0 314 368 0 0 0 1 1 1 21 0 1 0 1855366711 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6414/statm): 532 234 485 147 0 385 0
[pid=6414] vsize: 2128
Raw data (/proc/6419/stat): 6419 (minisat+_bignum) T 6414 6414 20728 0 -1 0 75792 0 0 0 11321 315 0 0 25 0 1 0 1855366719 267759616 65271 4294967295 134512640 135167914 3221224448 3221205996 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/6419/statm): 65371 65271 162 162 0 65209 0
[pid=6419] vsize: 261484
Current children cumulated CPU time (s) 116.39
Current children cumulated vsize (Kb) 263612

[startup+130.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 6419
Raw data (/proc/6414/stat): 6414 (minisat+_script) S 6413 6414 20728 0 -1 0 314 368 0 0 0 1 1 1 21 0 1 0 1855366711 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6414/statm): 532 234 485 147 0 385 0
[pid=6414] vsize: 2128
Raw data (/proc/6419/stat): 6419 (minisat+_bignum) R 6414 6414 20728 0 -1 0 80762 0 0 0 12266 342 0 0 25 0 1 0 1855366719 288116736 70241 4294967295 134512640 135167914 3221224448 3221208932 134621095 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6419/statm): 70341 70241 162 162 0 70179 0
[pid=6419] vsize: 281364
Current children cumulated CPU time (s) 126.11
Current children cumulated vsize (Kb) 283492

[startup+140.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 6419
Raw data (/proc/6414/stat): 6414 (minisat+_script) S 6413 6414 20728 0 -1 0 314 368 0 0 0 1 1 1 21 0 1 0 1855366711 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6414/statm): 532 234 485 147 0 385 0
[pid=6414] vsize: 2128
Raw data (/proc/6419/stat): 6419 (minisat+_bignum) R 6414 6414 20728 0 -1 0 106271 0 0 0 13166 413 0 0 25 0 1 0 1855366719 392601600 95750 4294967295 134512640 135167914 3221224448 3221207312 134694392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6419/statm): 95850 95750 162 162 0 95688 0
[pid=6419] vsize: 383400
Current children cumulated CPU time (s) 135.82
Current children cumulated vsize (Kb) 385528

[startup+150.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 6419
Raw data (/proc/6414/stat): 6414 (minisat+_script) S 6413 6414 20728 0 -1 0 314 368 0 0 0 1 1 1 21 0 1 0 1855366711 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6414/statm): 532 234 485 147 0 385 0
[pid=6414] vsize: 2128
Raw data (/proc/6419/stat): 6419 (minisat+_bignum) R 6414 6414 20728 0 -1 0 107735 0 0 0 14147 423 0 0 25 0 1 0 1855366719 355401728 86668 4294967295 134512640 135167914 3221224448 3221206672 134843001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6419/statm): 86768 86668 162 162 0 86606 0
[pid=6419] vsize: 347072
Current children cumulated CPU time (s) 145.73
Current children cumulated vsize (Kb) 349200

[startup+160.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 6419
Raw data (/proc/6414/stat): 6414 (minisat+_script) S 6413 6414 20728 0 -1 0 314 368 0 0 0 1 1 1 21 0 1 0 1855366711 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6414/statm): 532 234 485 147 0 385 0
[pid=6414] vsize: 2128
Raw data (/proc/6419/stat): 6419 (minisat+_bignum) T 6414 6414 20728 0 -1 0 112757 0 0 0 15094 443 0 0 25 0 1 0 1855366719 375971840 91690 4294967295 134512640 135167914 3221224448 3221206044 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/6419/statm): 91790 91690 162 162 0 91628 0
[pid=6419] vsize: 367160
Current children cumulated CPU time (s) 155.4
Current children cumulated vsize (Kb) 369288

[startup+170.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 6419
Raw data (/proc/6414/stat): 6414 (minisat+_script) S 6413 6414 20728 0 -1 0 314 368 0 0 0 1 1 1 21 0 1 0 1855366711 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6414/statm): 532 234 485 147 0 385 0
[pid=6414] vsize: 2128
Raw data (/proc/6419/stat): 6419 (minisat+_bignum) R 6414 6414 20728 0 -1 0 117580 0 0 0 16042 465 0 0 25 0 1 0 1855366719 395726848 96513 4294967295 134512640 135167914 3221224448 3221206404 134845880 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6419/statm): 96613 96513 162 162 0 96451 0
[pid=6419] vsize: 386452
Current children cumulated CPU time (s) 165.1
Current children cumulated vsize (Kb) 388580

[startup+180.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 6419
Raw data (/proc/6414/stat): 6414 (minisat+_script) S 6413 6414 20728 0 -1 0 314 368 0 0 0 1 1 1 21 0 1 0 1855366711 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6414/statm): 532 234 485 147 0 385 0
[pid=6414] vsize: 2128
Raw data (/proc/6419/stat): 6419 (minisat+_bignum) R 6414 6414 20728 0 -1 0 122494 0 0 0 16983 490 0 0 25 0 1 0 1855366719 415854592 101427 4294967295 134512640 135167914 3221224448 3221206432 134843402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6419/statm): 101527 101427 162 162 0 101365 0
[pid=6419] vsize: 406108
Current children cumulated CPU time (s) 174.76
Current children cumulated vsize (Kb) 408236

[startup+190.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 6419
Raw data (/proc/6414/stat): 6414 (minisat+_script) S 6413 6414 20728 0 -1 0 314 368 0 0 0 1 1 1 21 0 1 0 1855366711 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6414/statm): 532 234 485 147 0 385 0
[pid=6414] vsize: 2128
Raw data (/proc/6419/stat): 6419 (minisat+_bignum) R 6414 6414 20728 0 -1 0 127345 0 0 0 17932 512 0 0 25 0 1 0 1855366719 435724288 106278 4294967295 134512640 135167914 3221224448 3221207124 134849086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6419/statm): 106378 106278 162 162 0 106216 0
[pid=6419] vsize: 425512
Current children cumulated CPU time (s) 184.47
Current children cumulated vsize (Kb) 427640

[startup+200.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 6419
Raw data (/proc/6414/stat): 6414 (minisat+_script) S 6413 6414 20728 0 -1 0 314 368 0 0 0 1 1 1 21 0 1 0 1855366711 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6414/statm): 532 234 485 147 0 385 0
[pid=6414] vsize: 2128
Raw data (/proc/6419/stat): 6419 (minisat+_bignum) T 6414 6414 20728 0 -1 0 132223 0 0 0 18880 532 0 0 21 0 1 0 1855366719 455704576 111156 4294967295 134512640 135167914 3221224448 3221206780 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/6419/statm): 111256 111156 162 162 0 111094 0
[pid=6419] vsize: 445024
Current children cumulated CPU time (s) 194.15
Current children cumulated vsize (Kb) 447152

[startup+210.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 6419
Raw data (/proc/6414/stat): 6414 (minisat+_script) S 6413 6414 20728 0 -1 0 314 368 0 0 0 1 1 1 21 0 1 0 1855366711 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6414/statm): 532 234 485 147 0 385 0
[pid=6414] vsize: 2128
Raw data (/proc/6419/stat): 6419 (minisat+_bignum) T 6414 6414 20728 0 -1 0 137057 0 0 0 19825 553 0 0 25 0 1 0 1855366719 475504640 115990 4294967295 134512640 135167914 3221224448 3221206300 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/6419/statm): 116090 115990 162 162 0 115928 0
[pid=6419] vsize: 464360
Current children cumulated CPU time (s) 203.81
Current children cumulated vsize (Kb) 466488

[startup+220.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 6419
Raw data (/proc/6414/stat): 6414 (minisat+_script) S 6413 6414 20728 0 -1 0 314 368 0 0 0 1 1 1 21 0 1 0 1855366711 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6414/statm): 532 234 485 147 0 385 0
[pid=6414] vsize: 2128
Raw data (/proc/6419/stat): 6419 (minisat+_bignum) R 6414 6414 20728 0 -1 0 141844 0 0 0 20773 574 0 0 25 0 1 0 1855366719 495112192 120777 4294967295 134512640 135167914 3221224448 3221206108 134934490 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6419/statm): 120877 120777 162 162 0 120715 0
[pid=6419] vsize: 483508
Current children cumulated CPU time (s) 213.5
Current children cumulated vsize (Kb) 485636

[startup+230.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 6419
Raw data (/proc/6414/stat): 6414 (minisat+_script) S 6413 6414 20728 0 -1 0 314 368 0 0 0 1 1 1 21 0 1 0 1855366711 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6414/statm): 532 234 485 147 0 385 0
[pid=6414] vsize: 2128
Raw data (/proc/6419/stat): 6419 (minisat+_bignum) T 6414 6414 20728 0 -1 0 146373 0 0 0 21727 595 0 0 25 0 1 0 1855366719 513662976 125306 4294967295 134512640 135167914 3221224448 3221207324 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/6419/statm): 125406 125306 162 162 0 125244 0
[pid=6419] vsize: 501624
Current children cumulated CPU time (s) 223.25
Current children cumulated vsize (Kb) 503752

[startup+240.024 s]
Raw data (loadavg): 0.99 0.97 0.94 1/57 6419
Raw data (/proc/6414/stat): 6414 (minisat+_script) S 6413 6414 20728 0 -1 0 314 368 0 0 0 1 1 1 21 0 1 0 1855366711 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6414/statm): 532 234 485 147 0 385 0
[pid=6414] vsize: 2128
Raw data (/proc/6419/stat): 6419 (minisat+_bignum) T 6414 6414 20728 0 -1 0 151292 0 0 0 22673 617 0 0 25 0 1 0 1855366719 533811200 130225 4294967295 134512640 135167914 3221224448 3221206076 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/6419/statm): 130325 130225 162 162 0 130163 0
[pid=6419] vsize: 521300
Current children cumulated CPU time (s) 232.93
Current children cumulated vsize (Kb) 523428

[startup+250.025 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 6419
Raw data (/proc/6414/stat): 6414 (minisat+_script) S 6413 6414 20728 0 -1 0 314 368 0 0 0 1 1 1 21 0 1 0 1855366711 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6414/statm): 532 234 485 147 0 385 0
[pid=6414] vsize: 2128
Raw data (/proc/6419/stat): 6419 (minisat+_bignum) R 6414 6414 20728 0 -1 0 156059 0 0 0 23620 641 0 0 21 0 1 0 1855366719 553336832 134992 4294967295 134512640 135167914 3221224448 3221206272 134843036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6419/statm): 135092 134992 162 162 0 134930 0
[pid=6419] vsize: 540368
Current children cumulated CPU time (s) 242.64
Current children cumulated vsize (Kb) 542496

[startup+260.026 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 6419
Raw data (/proc/6414/stat): 6414 (minisat+_script) S 6413 6414 20728 0 -1 0 314 368 0 0 0 1 1 1 21 0 1 0 1855366711 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6414/statm): 532 234 485 147 0 385 0
[pid=6414] vsize: 2128
Raw data (/proc/6419/stat): 6419 (minisat+_bignum) R 6414 6414 20728 0 -1 0 160587 0 0 0 24570 662 0 0 25 0 1 0 1855366719 571883520 139520 4294967295 134512640 135167914 3221224448 3221206432 134849201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6419/statm): 139620 139520 162 162 0 139458 0
[pid=6419] vsize: 558480
Current children cumulated CPU time (s) 252.35
Current children cumulated vsize (Kb) 560608

[startup+270.027 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 6419
Raw data (/proc/6414/stat): 6414 (minisat+_script) S 6413 6414 20728 0 -1 0 314 368 0 0 0 1 1 1 21 0 1 0 1855366711 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6414/statm): 532 234 485 147 0 385 0
[pid=6414] vsize: 2128
Raw data (/proc/6419/stat): 6419 (minisat+_bignum) R 6414 6414 20728 0 -1 0 165054 0 0 0 25521 680 0 0 25 0 1 0 1855366719 590180352 143987 4294967295 134512640 135167914 3221224448 3221206408 134844674 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6419/statm): 144087 143987 162 162 0 143925 0
[pid=6419] vsize: 576348
Current children cumulated CPU time (s) 262.04
Current children cumulated vsize (Kb) 578476

[startup+280.027 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 6419
Raw data (/proc/6414/stat): 6414 (minisat+_script) S 6413 6414 20728 0 -1 0 314 368 0 0 0 1 1 1 21 0 1 0 1855366711 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6414/statm): 532 234 485 147 0 385 0
[pid=6414] vsize: 2128
Raw data (/proc/6419/stat): 6419 (minisat+_bignum) R 6414 6414 20728 0 -1 0 169603 0 0 0 26465 704 0 0 21 0 1 0 1855366719 608813056 148536 4294967295 134512640 135167914 3221224448 3221206528 134844668 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6419/statm): 148636 148536 162 162 0 148474 0
[pid=6419] vsize: 594544
Current children cumulated CPU time (s) 271.72
Current children cumulated vsize (Kb) 596672

[startup+290.028 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 6419
Raw data (/proc/6414/stat): 6414 (minisat+_script) S 6413 6414 20728 0 -1 0 314 368 0 0 0 1 1 1 21 0 1 0 1855366711 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6414/statm): 532 234 485 147 0 385 0
[pid=6414] vsize: 2128
Raw data (/proc/6419/stat): 6419 (minisat+_bignum) R 6414 6414 20728 0 -1 0 212046 0 0 0 27358 810 0 0 25 0 1 0 1855366719 782659584 190979 4294967295 134512640 135167914 3221224448 3221206380 134845876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6419/statm): 191079 190979 162 162 0 190917 0
[pid=6419] vsize: 764316
Current children cumulated CPU time (s) 281.71
Current children cumulated vsize (Kb) 766444

[startup+300.029 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 6419
Raw data (/proc/6414/stat): 6414 (minisat+_script) S 6413 6414 20728 0 -1 0 314 368 0 0 0 1 1 1 21 0 1 0 1855366711 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6414/statm): 532 234 485 147 0 385 0
[pid=6414] vsize: 2128
Raw data (/proc/6419/stat): 6419 (minisat+_bignum) R 6414 6414 20728 0 -1 0 213313 0 0 0 28338 821 0 0 25 0 1 0 1855366719 701460480 171155 4294967295 134512640 135167914 3221224448 3221207456 134844637 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6419/statm): 171255 171155 162 162 0 171093 0
[pid=6419] vsize: 685020
Current children cumulated CPU time (s) 291.62
Current children cumulated vsize (Kb) 687148

[startup+310.028 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 6419
Raw data (/proc/6414/stat): 6414 (minisat+_script) S 6413 6414 20728 0 -1 0 314 368 0 0 0 1 1 1 21 0 1 0 1855366711 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6414/statm): 532 234 485 147 0 385 0
[pid=6414] vsize: 2128
Raw data (/proc/6419/stat): 6419 (minisat+_bignum) R 6414 6414 20728 0 -1 0 218001 0 0 0 29286 844 0 0 25 0 1 0 1855366719 720662528 175843 4294967295 134512640 135167914 3221224448 3221206668 134722656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6419/statm): 175943 175843 162 162 0 175781 0
[pid=6419] vsize: 703772
Current children cumulated CPU time (s) 301.33
Current children cumulated vsize (Kb) 705900

[startup+320.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 6419
Raw data (/proc/6414/stat): 6414 (minisat+_script) S 6413 6414 20728 0 -1 0 314 368 0 0 0 1 1 1 21 0 1 0 1855366711 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6414/statm): 532 234 485 147 0 385 0
[pid=6414] vsize: 2128
Raw data (/proc/6419/stat): 6419 (minisat+_bignum) R 6414 6414 20728 0 -1 0 223113 0 0 0 30225 868 0 0 25 0 1 0 1855366719 741601280 180955 4294967295 134512640 135167914 3221224448 3221206204 134934490 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6419/statm): 181055 180955 162 162 0 180893 0
[pid=6419] vsize: 724220
Current children cumulated CPU time (s) 310.96
Current children cumulated vsize (Kb) 726348

[startup+330.031 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 6419
Raw data (/proc/6414/stat): 6414 (minisat+_script) S 6413 6414 20728 0 -1 0 314 368 0 0 0 1 1 1 21 0 1 0 1855366711 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6414/statm): 532 234 485 147 0 385 0
[pid=6414] vsize: 2128
Raw data (/proc/6419/stat): 6419 (minisat+_bignum) R 6414 6414 20728 0 -1 0 228281 0 0 0 31166 894 0 0 25 0 1 0 1855366719 762773504 186123 4294967295 134512640 135167914 3221224448 3221206076 134934490 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6419/statm): 186224 186123 162 162 0 186062 0
[pid=6419] vsize: 744896
Current children cumulated CPU time (s) 320.63
Current children cumulated vsize (Kb) 747024

[startup+340.031 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 6419
Raw data (/proc/6414/stat): 6414 (minisat+_script) S 6413 6414 20728 0 -1 0 314 368 0 0 0 1 1 1 21 0 1 0 1855366711 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6414/statm): 532 234 485 147 0 385 0
[pid=6414] vsize: 2128
Raw data (/proc/6419/stat): 6419 (minisat+_bignum) R 6414 6414 20728 0 -1 0 233411 0 0 0 32107 920 0 0 25 0 1 0 1855366719 783781888 191253 4294967295 134512640 135167914 3221224448 3221207472 134845921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6419/statm): 191353 191253 162 162 0 191191 0
[pid=6419] vsize: 765412
Current children cumulated CPU time (s) 330.3
Current children cumulated vsize (Kb) 767540

[startup+350.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 6419
Raw data (/proc/6414/stat): 6414 (minisat+_script) S 6413 6414 20728 0 -1 0 314 368 0 0 0 1 1 1 21 0 1 0 1855366711 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6414/statm): 532 234 485 147 0 385 0
[pid=6414] vsize: 2128
Raw data (/proc/6419/stat): 6419 (minisat+_bignum) R 6414 6414 20728 0 -1 0 238544 0 0 0 33049 945 0 0 25 0 1 0 1855366719 804806656 196386 4294967295 134512640 135167914 3221224448 3221206464 134620365 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6419/statm): 196486 196386 162 162 0 196324 0
[pid=6419] vsize: 785944
Current children cumulated CPU time (s) 339.97
Current children cumulated vsize (Kb) 788072

[startup+360.033 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 6419
Raw data (/proc/6414/stat): 6414 (minisat+_script) S 6413 6414 20728 0 -1 0 314 368 0 0 0 1 1 1 21 0 1 0 1855366711 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6414/statm): 532 234 485 147 0 385 0
[pid=6414] vsize: 2128
Raw data (/proc/6419/stat): 6419 (minisat+_bignum) R 6414 6414 20728 0 -1 0 243628 0 0 0 33989 969 0 0 25 0 1 0 1855366719 825630720 201470 4294967295 134512640 135167914 3221224448 3221206972 134849557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6419/statm): 201570 201470 162 162 0 201408 0
[pid=6419] vsize: 806280
Current children cumulated CPU time (s) 349.61
Current children cumulated vsize (Kb) 808408

[startup+370.034 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 6419
Raw data (/proc/6414/stat): 6414 (minisat+_script) S 6413 6414 20728 0 -1 0 314 368 0 0 0 1 1 1 21 0 1 0 1855366711 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6414/statm): 532 234 485 147 0 385 0
[pid=6414] vsize: 2128
Raw data (/proc/6419/stat): 6419 (minisat+_bignum) R 6414 6414 20728 0 -1 0 248762 0 0 0 34929 995 0 0 25 0 1 0 1855366719 846659584 206604 4294967295 134512640 135167914 3221224448 3221206432 134694539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6419/statm): 206704 206604 162 162 0 206542 0
[pid=6419] vsize: 826816
Current children cumulated CPU time (s) 359.27
Current children cumulated vsize (Kb) 828944

[startup+380.034 s]
Raw data (loadavg): 0.99 0.97 0.94 1/57 6419
Raw data (/proc/6414/stat): 6414 (minisat+_script) S 6413 6414 20728 0 -1 0 314 368 0 0 0 1 1 1 21 0 1 0 1855366711 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6414/statm): 532 234 485 147 0 385 0
[pid=6414] vsize: 2128
Raw data (/proc/6419/stat): 6419 (minisat+_bignum) T 6414 6414 20728 0 -1 0 253870 0 0 0 35870 1019 0 0 25 0 1 0 1855366719 867581952 211712 4294967295 134512640 135167914 3221224448 3221206396 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/6419/statm): 211812 211712 162 162 0 211650 0
[pid=6419] vsize: 847248
Current children cumulated CPU time (s) 368.92
Current children cumulated vsize (Kb) 849376

[startup+390.035 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 6419
Raw data (/proc/6414/stat): 6414 (minisat+_script) S 6413 6414 20728 0 -1 0 314 368 0 0 0 1 1 1 21 0 1 0 1855366711 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6414/statm): 532 234 485 147 0 385 0
[pid=6414] vsize: 2128
Raw data (/proc/6419/stat): 6419 (minisat+_bignum) R 6414 6414 20728 0 -1 0 258909 0 0 0 36811 1044 0 0 25 0 1 0 1855366719 888221696 216751 4294967295 134512640 135167914 3221224448 3221207328 134849110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6419/statm): 216851 216751 162 162 0 216689 0
[pid=6419] vsize: 867404
Current children cumulated CPU time (s) 378.58
Current children cumulated vsize (Kb) 869532

[startup+400.036 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 6419
Raw data (/proc/6414/stat): 6414 (minisat+_script) S 6413 6414 20728 0 -1 0 314 368 0 0 0 1 1 1 21 0 1 0 1855366711 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6414/statm): 532 234 485 147 0 385 0
[pid=6414] vsize: 2128
Raw data (/proc/6419/stat): 6419 (minisat+_bignum) T 6414 6414 20728 0 -1 0 263822 0 0 0 37751 1068 0 0 21 0 1 0 1855366719 908345344 221664 4294967295 134512640 135167914 3221224448 3221205980 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/6419/statm): 221764 221664 162 162 0 221602 0
[pid=6419] vsize: 887056
Current children cumulated CPU time (s) 388.22
Current children cumulated vsize (Kb) 889184

[startup+410.035 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 6419
Raw data (/proc/6414/stat): 6414 (minisat+_script) S 6413 6414 20728 0 -1 0 314 368 0 0 0 1 1 1 21 0 1 0 1855366711 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6414/statm): 532 234 485 147 0 385 0
[pid=6414] vsize: 2128
Raw data (/proc/6419/stat): 6419 (minisat+_bignum) R 6414 6414 20728 0 -1 0 268642 0 0 0 38698 1089 0 0 25 0 1 0 1855366719 928088064 226484 4294967295 134512640 135167914 3221224448 3221207008 134694392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6419/statm): 226584 226484 162 162 0 226422 0
[pid=6419] vsize: 906336
Current children cumulated CPU time (s) 397.9
Current children cumulated vsize (Kb) 908464



Mem limit exceeded: sending SIGTERM then SIGKILL

[startup+416.952 s]
Raw data (loadavg): 0.99 0.97 0.94 1/57 6419
Raw data (/proc/6414/stat): 6414 (minisat+_script) S 6413 6414 20728 0 -1 0 314 368 0 0 0 1 1 1 21 0 1 0 1855366711 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6414/statm): 532 234 485 147 0 385 0
[pid=6414] vsize: 2128
Raw data (/proc/6419/stat): 6419 (minisat+_bignum) T 6414 6414 20728 0 -1 0 271980 0 7 0 39342 1106 0 0 25 0 1 0 1855366719 941543424 228488 4294967295 134512640 135167914 3221224448 3221206748 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/6419/statm): 229869 228488 162 162 0 229707 0
[pid=6419] vsize: 919476
Current children cumulated CPU time (s) 404.51
Current children cumulated vsize (Kb) 921604

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

Child status: 0
Real time (s): 417.379
CPU time (s): 404.918
CPU user time (s): 393.427
CPU system time (s): 11.4913
CPU usage (%): 97.0146
Max. virtual memory (cumulated for all children) (Kb): 921604

Verifier Data

ERROR: no interpretation found !