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/miplib2003/normalized-mps-v2-20-10-glass4.opb
MD5SUM929651d54295ccab2bd7ed98e4ab5229
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 13303876395624
Optimality of the best value was proved NO
Number of terms in the objective function 478
Biggest coefficient in the objective function 536870912000000
Number of bits for the biggest coefficient in the objective function 49
Sum of the numbers in the objective function 1073761158741413
Number of bits of the sum of numbers in the objective function 50
Biggest number in a constraint 71583145981965762560
Number of bits of the biggest number in a constraint 66
Biggest sum of numbers in a constraint 303620978593259257856
Number of bits of the biggest sum of numbers69
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1259.64
Number of variables780
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 constraint101

Trace number 3891

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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:        906464 kB
Buffers:         32516 kB
Cached:          70104 kB
SwapCached:        944 kB
Active:          55108 kB
Inactive:        50200 kB
HighTotal:      131008 kB
HighFree:        57932 kB
LowTotal:       903652 kB
LowFree:        848532 kB
SwapTotal:     2097136 kB
SwapFree:      2095644 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5692 kB
Slab:            16992 kB
Committed_AS:    72360 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-19 03:46:55 (client local time) WITH STATUS 0 IN 401.296 SECONDS
stats: 2912 7 401.296 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 326] 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/30247/stat): 30247 (minisat+_script) R 30246 30247 6847 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1788484584 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/30247/statm): 174 3 169 147 0 27 0
[pid=30247] 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=30248
New process pid=30249
New process pid=30250
execve syscall for /bin/sed executable
One traced child (pid=30249) 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=30250) exited with status: 0
One traced child (pid=30248) exited with status: 0
New process pid=30251
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-glass4.opb
One traced child (pid=30251) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=30252
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-glass4.opb

[startup+10.0043 s]
Raw data (loadavg): 0.93 0.98 0.90 2/57 30252
Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30247/statm): 532 234 485 147 0 385 0
[pid=30247] vsize: 2128
Raw data (/proc/30252/stat): 30252 (minisat+_bignum) R 30247 30247 6847 0 -1 0 5536 0 0 0 942 22 0 0 25 0 1 0 1788484591 20459520 4902 4294967295 134512640 135167914 3221224448 3221201920 134843030 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30252/statm): 4995 4902 162 162 0 4833 0
[pid=30252] vsize: 19980
Current children cumulated CPU time (s) 9.65
Current children cumulated vsize (Kb) 22108

[startup+20.0051 s]
Raw data (loadavg): 0.94 0.98 0.91 2/57 30252
Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30247/statm): 532 234 485 147 0 385 0
[pid=30247] vsize: 2128
Raw data (/proc/30252/stat): 30252 (minisat+_bignum) R 30247 30247 6847 0 -1 0 13852 0 0 0 1884 54 0 0 25 0 1 0 1788484591 51822592 12559 4294967295 134512640 135167914 3221224448 3221200624 134625468 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30252/statm): 12652 12559 162 162 0 12490 0
[pid=30252] vsize: 50608
Current children cumulated CPU time (s) 19.39
Current children cumulated vsize (Kb) 52736

[startup+30.006 s]
Raw data (loadavg): 0.95 0.98 0.91 1/57 30252
Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30247/statm): 532 234 485 147 0 385 0
[pid=30247] vsize: 2128
Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 18799 0 0 0 2833 76 0 0 25 0 1 0 1788484591 66686976 16188 4294967295 134512640 135167914 3221224448 3221200220 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/30252/statm): 16281 16188 162 162 0 16119 0
[pid=30252] vsize: 65124
Current children cumulated CPU time (s) 29.1
Current children cumulated vsize (Kb) 67252

[startup+40.0069 s]
Raw data (loadavg): 0.95 0.98 0.91 2/57 30252
Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30247/statm): 532 234 485 147 0 385 0
[pid=30247] vsize: 2128
Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 27979 0 0 0 3777 109 0 0 25 0 1 0 1788484591 93487104 22731 4294967295 134512640 135167914 3221224448 3221200156 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/30252/statm): 22824 22731 162 162 0 22662 0
[pid=30252] vsize: 91296
Current children cumulated CPU time (s) 38.87
Current children cumulated vsize (Kb) 93424

[startup+50.0088 s]
Raw data (loadavg): 0.96 0.98 0.91 2/57 30252
Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30247/statm): 532 234 485 147 0 385 0
[pid=30247] vsize: 2128
Raw data (/proc/30252/stat): 30252 (minisat+_bignum) R 30247 30247 6847 0 -1 0 32628 0 0 0 4727 128 0 0 25 0 1 0 1788484591 112529408 27380 4294967295 134512640 135167914 3221224448 3221200640 134620615 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30252/statm): 27473 27380 162 162 0 27311 0
[pid=30252] vsize: 109892
Current children cumulated CPU time (s) 48.56
Current children cumulated vsize (Kb) 112020

[startup+60.0097 s]
Raw data (loadavg): 0.97 0.98 0.91 1/57 30252
Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30247/statm): 532 234 485 147 0 385 0
[pid=30247] vsize: 2128
Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 37425 0 0 0 5673 152 0 0 25 0 1 0 1788484591 132177920 32177 4294967295 134512640 135167914 3221224448 3221200348 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/30252/statm): 32270 32177 162 162 0 32108 0
[pid=30252] vsize: 129080
Current children cumulated CPU time (s) 58.26
Current children cumulated vsize (Kb) 131208

[startup+70.0106 s]
Raw data (loadavg): 0.97 0.98 0.91 1/57 30252
Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30247/statm): 532 234 485 147 0 385 0
[pid=30247] vsize: 2128
Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 42273 0 0 0 6621 175 0 0 25 0 1 0 1788484591 152035328 37025 4294967295 134512640 135167914 3221224448 3221200396 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/30252/statm): 37118 37025 162 162 0 36956 0
[pid=30252] vsize: 148472
Current children cumulated CPU time (s) 67.97
Current children cumulated vsize (Kb) 150600

[startup+80.0116 s]
Raw data (loadavg): 0.98 0.98 0.91 2/57 30252
Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30247/statm): 532 234 485 147 0 385 0
[pid=30247] vsize: 2128
Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 55749 0 0 0 7567 214 0 0 25 0 1 0 1788484591 185634816 45228 4294967295 134512640 135167914 3221224448 3221201500 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/30252/statm): 45321 45228 162 162 0 45159 0
[pid=30252] vsize: 181284
Current children cumulated CPU time (s) 77.82
Current children cumulated vsize (Kb) 183412

[startup+90.0125 s]
Raw data (loadavg): 0.98 0.98 0.91 2/57 30252
Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30247/statm): 532 234 485 147 0 385 0
[pid=30247] vsize: 2128
Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 60853 0 0 0 8511 235 0 0 25 0 1 0 1788484591 206540800 50332 4294967295 134512640 135167914 3221224448 3221200220 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/30252/statm): 50425 50332 162 162 0 50263 0
[pid=30252] vsize: 201700
Current children cumulated CPU time (s) 87.47
Current children cumulated vsize (Kb) 203828

[startup+100.013 s]
Raw data (loadavg): 0.98 0.98 0.91 2/57 30252
Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30247/statm): 532 234 485 147 0 385 0
[pid=30247] vsize: 2128
Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 65675 0 0 0 9458 258 0 0 25 0 1 0 1788484591 226291712 55154 4294967295 134512640 135167914 3221224448 3221200380 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/30252/statm): 55247 55154 162 162 0 55085 0
[pid=30252] vsize: 220988
Current children cumulated CPU time (s) 97.17
Current children cumulated vsize (Kb) 223116

[startup+110.014 s]
Raw data (loadavg): 0.98 0.98 0.91 1/57 30252
Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30247/statm): 532 234 485 147 0 385 0
[pid=30247] vsize: 2128
Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 70450 0 0 0 10411 278 0 0 25 0 1 0 1788484591 245850112 59929 4294967295 134512640 135167914 3221224448 3221201852 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/30252/statm): 60022 59929 162 162 0 59860 0
[pid=30252] vsize: 240088
Current children cumulated CPU time (s) 106.9
Current children cumulated vsize (Kb) 242216

[startup+120.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 30252
Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30247/statm): 532 234 485 147 0 385 0
[pid=30247] vsize: 2128
Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 75247 0 0 0 11360 303 0 0 25 0 1 0 1788484591 265498624 64726 4294967295 134512640 135167914 3221224448 3221200252 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/30252/statm): 64819 64726 162 162 0 64657 0
[pid=30252] vsize: 259276
Current children cumulated CPU time (s) 116.64
Current children cumulated vsize (Kb) 261404

[startup+130.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 30252
Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30247/statm): 532 234 485 147 0 385 0
[pid=30247] vsize: 2128
Raw data (/proc/30252/stat): 30252 (minisat+_bignum) R 30247 30247 6847 0 -1 0 80090 0 0 0 12302 329 0 0 25 0 1 0 1788484591 285335552 69569 4294967295 134512640 135167914 3221224448 3221201664 134843010 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30252/statm): 69662 69569 162 162 0 69500 0
[pid=30252] vsize: 278648
Current children cumulated CPU time (s) 126.32
Current children cumulated vsize (Kb) 280776

[startup+140.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 30252
Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30247/statm): 532 234 485 147 0 385 0
[pid=30247] vsize: 2128
Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 84901 0 0 0 13249 349 0 0 25 0 1 0 1788484591 305041408 74380 4294967295 134512640 135167914 3221224448 3221200220 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/30252/statm): 74473 74380 162 162 0 74311 0
[pid=30252] vsize: 297892
Current children cumulated CPU time (s) 135.99
Current children cumulated vsize (Kb) 300020

[startup+150.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 30252
Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30247/statm): 532 234 485 147 0 385 0
[pid=30247] vsize: 2128
Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 106801 0 0 0 14193 401 0 0 25 0 1 0 1788484591 351547392 85734 4294967295 134512640 135167914 3221224448 3221200380 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/30252/statm): 85827 85734 162 162 0 85665 0
[pid=30252] vsize: 343308
Current children cumulated CPU time (s) 145.95
Current children cumulated vsize (Kb) 345436

[startup+160.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 30252
Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30247/statm): 532 234 485 147 0 385 0
[pid=30247] vsize: 2128
Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 111941 0 0 0 15138 424 0 0 25 0 1 0 1788484591 372600832 90874 4294967295 134512640 135167914 3221224448 3221200156 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/30252/statm): 90967 90874 162 162 0 90805 0
[pid=30252] vsize: 363868
Current children cumulated CPU time (s) 155.63
Current children cumulated vsize (Kb) 365996

[startup+170.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 30252
Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30247/statm): 532 234 485 147 0 385 0
[pid=30247] vsize: 2128
Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 116942 0 0 0 16083 447 0 0 25 0 1 0 1788484591 393084928 95875 4294967295 134512640 135167914 3221224448 3221200156 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/30252/statm): 95968 95875 162 162 0 95806 0
[pid=30252] vsize: 383872
Current children cumulated CPU time (s) 165.31
Current children cumulated vsize (Kb) 386000

[startup+180.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 30252
Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30247/statm): 532 234 485 147 0 385 0
[pid=30247] vsize: 2128
Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 121945 0 0 0 17025 472 0 0 25 0 1 0 1788484591 413577216 100878 4294967295 134512640 135167914 3221224448 3221200476 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/30252/statm): 100971 100878 162 162 0 100809 0
[pid=30252] vsize: 403884
Current children cumulated CPU time (s) 174.98
Current children cumulated vsize (Kb) 406012

[startup+190.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 30252
Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30247/statm): 532 234 485 147 0 385 0
[pid=30247] vsize: 2128
Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 126910 0 0 0 17973 495 0 0 25 0 1 0 1788484591 433913856 105843 4294967295 134512640 135167914 3221224448 3221201148 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/30252/statm): 105936 105843 162 162 0 105774 0
[pid=30252] vsize: 423744
Current children cumulated CPU time (s) 184.69
Current children cumulated vsize (Kb) 425872

[startup+200.022 s]
Raw data (loadavg): 0.99 0.98 0.91 1/57 30252
Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30247/statm): 532 234 485 147 0 385 0
[pid=30247] vsize: 2128
Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 131898 0 0 0 18922 516 0 0 24 0 1 0 1788484591 454344704 110831 4294967295 134512640 135167914 3221224448 3221200476 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/30252/statm): 110924 110831 162 162 0 110762 0
[pid=30252] vsize: 443696
Current children cumulated CPU time (s) 194.39
Current children cumulated vsize (Kb) 445824

[startup+210.023 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 30252
Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30247/statm): 532 234 485 147 0 385 0
[pid=30247] vsize: 2128
Raw data (/proc/30252/stat): 30252 (minisat+_bignum) R 30247 30247 6847 0 -1 0 136823 0 0 0 19866 540 0 0 25 0 1 0 1788484591 474517504 115756 4294967295 134512640 135167914 3221224448 3221200992 134843420 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30252/statm): 115849 115756 162 162 0 115687 0
[pid=30252] vsize: 463396
Current children cumulated CPU time (s) 204.07
Current children cumulated vsize (Kb) 465524

[startup+220.024 s]
Raw data (loadavg): 0.99 0.98 0.91 1/57 30252
Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30247/statm): 532 234 485 147 0 385 0
[pid=30247] vsize: 2128
Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 141715 0 0 0 20816 563 0 0 25 0 1 0 1788484591 494555136 120648 4294967295 134512640 135167914 3221224448 3221200444 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/30252/statm): 120741 120648 162 162 0 120579 0
[pid=30252] vsize: 482964
Current children cumulated CPU time (s) 213.8
Current children cumulated vsize (Kb) 485092

[startup+230.025 s]
Raw data (loadavg): 0.99 0.98 0.91 1/57 30252
Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30247/statm): 532 234 485 147 0 385 0
[pid=30247] vsize: 2128
Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 146413 0 0 0 21761 584 0 0 25 0 1 0 1788484591 513798144 125346 4294967295 134512640 135167914 3221224448 3221200380 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/30252/statm): 125439 125346 162 162 0 125277 0
[pid=30252] vsize: 501756
Current children cumulated CPU time (s) 223.46
Current children cumulated vsize (Kb) 503884

[startup+240.026 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 30252
Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30247/statm): 532 234 485 147 0 385 0
[pid=30247] vsize: 2128
Raw data (/proc/30252/stat): 30252 (minisat+_bignum) R 30247 30247 6847 0 -1 0 151365 0 0 0 22703 609 0 0 25 0 1 0 1788484591 534081536 130298 4294967295 134512640 135167914 3221224448 3221200444 134934490 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30252/statm): 130391 130298 162 162 0 130229 0
[pid=30252] vsize: 521564
Current children cumulated CPU time (s) 233.13
Current children cumulated vsize (Kb) 523692

[startup+250.027 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 30252
Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30247/statm): 532 234 485 147 0 385 0
[pid=30247] vsize: 2128
Raw data (/proc/30252/stat): 30252 (minisat+_bignum) R 30247 30247 6847 0 -1 0 156201 0 0 0 23648 631 0 0 25 0 1 0 1788484591 553889792 135134 4294967295 134512640 135167914 3221224448 3221201052 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30252/statm): 135227 135134 162 162 0 135065 0
[pid=30252] vsize: 540908
Current children cumulated CPU time (s) 242.8
Current children cumulated vsize (Kb) 543036

[startup+260.028 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 30252
Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30247/statm): 532 234 485 147 0 385 0
[pid=30247] vsize: 2128
Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 160857 0 0 0 24598 653 0 0 25 0 1 0 1788484591 572960768 139790 4294967295 134512640 135167914 3221224448 3221200444 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/30252/statm): 139883 139790 162 162 0 139721 0
[pid=30252] vsize: 559532
Current children cumulated CPU time (s) 252.52
Current children cumulated vsize (Kb) 561660

[startup+270.028 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 30252
Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30247/statm): 532 234 485 147 0 385 0
[pid=30247] vsize: 2128
Raw data (/proc/30252/stat): 30252 (minisat+_bignum) R 30247 30247 6847 0 -1 0 165591 0 0 0 25545 676 0 0 25 0 1 0 1788484591 592351232 144524 4294967295 134512640 135167914 3221224448 3221200448 134845042 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30252/statm): 144617 144524 162 162 0 144455 0
[pid=30252] vsize: 578468
Current children cumulated CPU time (s) 262.22
Current children cumulated vsize (Kb) 580596

[startup+280.029 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 30252
Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30247/statm): 532 234 485 147 0 385 0
[pid=30247] vsize: 2128
Raw data (/proc/30252/stat): 30252 (minisat+_bignum) R 30247 30247 6847 0 -1 0 187783 0 0 0 26454 739 0 0 25 0 1 0 1788484591 783175680 166716 4294967295 134512640 135167914 3221224448 3221201536 134625368 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30252/statm): 191205 166722 162 162 0 191043 0
[pid=30252] vsize: 764820
Current children cumulated CPU time (s) 271.94
Current children cumulated vsize (Kb) 766948

[startup+290.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 30252
Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30247/statm): 532 234 485 147 0 385 0
[pid=30247] vsize: 2128
Raw data (/proc/30252/stat): 30252 (minisat+_bignum) R 30247 30247 6847 0 -1 0 212179 0 0 0 27398 796 0 0 25 0 1 0 1788484591 783175680 191112 4294967295 134512640 135167914 3221224448 3221201536 134625428 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30252/statm): 191205 191112 162 162 0 191043 0
[pid=30252] vsize: 764820
Current children cumulated CPU time (s) 281.95
Current children cumulated vsize (Kb) 766948

[startup+300.031 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 30252
Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30247/statm): 532 234 485 147 0 385 0
[pid=30247] vsize: 2128
Raw data (/proc/30252/stat): 30252 (minisat+_bignum) R 30247 30247 6847 0 -1 0 214001 0 0 0 28373 808 0 0 25 0 1 0 1788484591 704249856 171843 4294967295 134512640 135167914 3221224448 3221200700 134934490 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30252/statm): 171936 171843 162 162 0 171774 0
[pid=30252] vsize: 687744
Current children cumulated CPU time (s) 291.82
Current children cumulated vsize (Kb) 689872

[startup+310.032 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 30252
Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30247/statm): 532 234 485 147 0 385 0
[pid=30247] vsize: 2128
Raw data (/proc/30252/stat): 30252 (minisat+_bignum) R 30247 30247 6847 0 -1 0 218899 0 0 0 29316 833 0 0 25 0 1 0 1788484591 724312064 176741 4294967295 134512640 135167914 3221224448 3221201296 134695738 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30252/statm): 176834 176741 162 162 0 176672 0
[pid=30252] vsize: 707336
Current children cumulated CPU time (s) 301.5
Current children cumulated vsize (Kb) 709464

[startup+320.033 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 30252
Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30247/statm): 532 234 485 147 0 385 0
[pid=30247] vsize: 2128
Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 224140 0 0 0 30256 862 0 0 25 0 1 0 1788484591 745779200 181982 4294967295 134512640 135167914 3221224448 3221200172 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/30252/statm): 182075 181982 162 162 0 181913 0
[pid=30252] vsize: 728300
Current children cumulated CPU time (s) 311.19
Current children cumulated vsize (Kb) 730428

[startup+330.035 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 30252
Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30247/statm): 532 234 485 147 0 385 0
[pid=30247] vsize: 2128
Raw data (/proc/30252/stat): 30252 (minisat+_bignum) R 30247 30247 6847 0 -1 0 229368 0 0 0 31192 888 0 0 25 0 1 0 1788484591 767193088 187210 4294967295 134512640 135167914 3221224448 3221200640 134619683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30252/statm): 187303 187210 162 162 0 187141 0
[pid=30252] vsize: 749212
Current children cumulated CPU time (s) 320.81
Current children cumulated vsize (Kb) 751340

[startup+340.036 s]
Raw data (loadavg): 0.99 0.98 0.91 1/57 30252
Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30247/statm): 532 234 485 147 0 385 0
[pid=30247] vsize: 2128
Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 234443 0 0 0 32133 910 0 0 25 0 1 0 1788484591 787980288 192285 4294967295 134512640 135167914 3221224448 3221200156 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/30252/statm): 192378 192285 162 162 0 192216 0
[pid=30252] vsize: 769512
Current children cumulated CPU time (s) 330.44
Current children cumulated vsize (Kb) 771640

[startup+350.036 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 30252
Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30247/statm): 532 234 485 147 0 385 0
[pid=30247] vsize: 2128
Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 239562 0 0 0 33076 935 0 0 25 0 1 0 1788484591 808947712 197404 4294967295 134512640 135167914 3221224448 3221200220 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/30252/statm): 197497 197404 162 162 0 197335 0
[pid=30252] vsize: 789988
Current children cumulated CPU time (s) 340.12
Current children cumulated vsize (Kb) 792116

[startup+360.037 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 30252
Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30247/statm): 532 234 485 147 0 385 0
[pid=30247] vsize: 2128
Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 244658 0 0 0 34013 964 0 0 25 0 1 0 1788484591 829820928 202500 4294967295 134512640 135167914 3221224448 3221200252 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/30252/statm): 202593 202500 162 162 0 202431 0
[pid=30252] vsize: 810372
Current children cumulated CPU time (s) 349.78
Current children cumulated vsize (Kb) 812500

[startup+370.037 s]
Raw data (loadavg): 0.99 0.98 0.91 1/57 30252
Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30247/statm): 532 234 485 147 0 385 0
[pid=30247] vsize: 2128
Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 249828 0 0 0 34955 989 0 0 25 0 1 0 1788484591 851001344 207670 4294967295 134512640 135167914 3221224448 3221200252 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/30252/statm): 207764 207670 162 162 0 207602 0
[pid=30252] vsize: 831056
Current children cumulated CPU time (s) 359.45
Current children cumulated vsize (Kb) 833184

[startup+380.039 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 30252
Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30247/statm): 532 234 485 147 0 385 0
[pid=30247] vsize: 2128
Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 254996 0 0 0 35897 1015 0 0 25 0 1 0 1788484591 872165376 212838 4294967295 134512640 135167914 3221224448 3221200348 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/30252/statm): 212931 212838 162 162 0 212769 0
[pid=30252] vsize: 851724
Current children cumulated CPU time (s) 369.13
Current children cumulated vsize (Kb) 853852

[startup+390.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 30252
Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30247/statm): 532 234 485 147 0 385 0
[pid=30247] vsize: 2128
Raw data (/proc/30252/stat): 30252 (minisat+_bignum) R 30247 30247 6847 0 -1 0 260138 0 0 0 36835 1042 0 0 25 0 1 0 1788484591 893227008 217980 4294967295 134512640 135167914 3221224448 3221200704 134849592 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30252/statm): 218073 217980 162 162 0 217911 0
[pid=30252] vsize: 872292
Current children cumulated CPU time (s) 378.78
Current children cumulated vsize (Kb) 874420

[startup+400.041 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 30252
Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30247/statm): 532 234 485 147 0 385 0
[pid=30247] vsize: 2128
Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 265343 0 0 0 37775 1067 0 0 25 0 1 0 1788484591 914546688 223185 4294967295 134512640 135167914 3221224448 3221201292 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/30252/statm): 223278 223185 162 162 0 223116 0
[pid=30252] vsize: 893112
Current children cumulated CPU time (s) 388.43
Current children cumulated vsize (Kb) 895240

[startup+410.042 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 30252
Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30247/statm): 532 234 485 147 0 385 0
[pid=30247] vsize: 2128
Raw data (/proc/30252/stat): 30252 (minisat+_bignum) R 30247 30247 6847 0 -1 0 270456 0 0 0 38713 1094 0 0 25 0 1 0 1788484591 935489536 227818 4294967295 134512640 135167914 3221224448 3221202336 134844668 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30252/statm): 228391 227818 162 162 0 228229 0
[pid=30252] vsize: 913564
Current children cumulated CPU time (s) 398.08
Current children cumulated vsize (Kb) 915692



Mem limit exceeded: sending SIGTERM then SIGKILL

[startup+412.946 s]
Raw data (loadavg): 0.99 0.98 0.91 1/57 30252
Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30247/statm): 532 234 485 147 0 385 0
[pid=30247] vsize: 2128
Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 271933 0 0 0 38986 1100 0 0 25 0 1 0 1788484591 941543424 228785 4294967295 134512640 135167914 3221224448 3221200380 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/30252/statm): 229869 228785 162 162 0 229707 0
[pid=30252] vsize: 919476
Current children cumulated CPU time (s) 400.87
Current children cumulated vsize (Kb) 921604

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

Child status: 0
Real time (s): 413.37
CPU time (s): 401.296
CPU user time (s): 389.869
CPU system time (s): 11.4273
CPU usage (%): 97.0791
Max. virtual memory (cumulated for all children) (Kb): 921604

Verifier Data

ERROR: no interpretation found !