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/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-net12.opb
MD5SUM8fd050825d75dbe16d9da083f4b2fd63
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 8257573732279
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 benchmark1269.78
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 5917

Launcher Data

LAUNCH ON wulflinc25 THE 2005-09-20 02:08:12 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3108 boxname=wulflinc25 idbench=764 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  8fd050825d75dbe16d9da083f4b2fd63  /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-net12.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-net12.opb
IDLAUNCH: 3108
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.220
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.220
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        924752 kB
Buffers:          2216 kB
Cached:          79756 kB
SwapCached:        852 kB
Active:          20388 kB
Inactive:        64120 kB
HighTotal:      131008 kB
HighFree:        47908 kB
LowTotal:       903652 kB
LowFree:        876844 kB
SwapTotal:     2097892 kB
SwapFree:      2096524 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           5720 kB
Slab:            19532 kB
Committed_AS:    64132 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 02:15:05 (client local time) WITH STATUS 0 IN 400.237 SECONDS
stats: 3108 7 400.237 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/26429/stat): 26429 (minisat+_script) R 26428 26429 4419 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1854843804 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/26429/statm): 174 3 169 147 0 27 0
[pid=26429] 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=26430
New process pid=26431
New process pid=26432
execve syscall for /bin/sed executable
One traced child (pid=26431) 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=26432) exited with status: 0
One traced child (pid=26430) exited with status: 0
New process pid=26433
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-net12.opb
One traced child (pid=26433) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=26434
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-net12.opb

[startup+10.0031 s]
Raw data (loadavg): 1.06 0.99 0.94 2/57 26434
Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26429/statm): 532 234 485 147 0 385 0
[pid=26429] vsize: 2128
Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 5168 0 0 0 945 23 0 0 25 0 1 0 1854843811 19046400 4534 4294967295 134512640 135167914 3221224448 3221201516 134849056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26434/statm): 4650 4534 162 162 0 4488 0
[pid=26434] vsize: 18600
Current children cumulated CPU time (s) 9.7
Current children cumulated vsize (Kb) 20728

[startup+20.0047 s]
Raw data (loadavg): 1.05 0.99 0.94 2/57 26434
Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26429/statm): 532 234 485 147 0 385 0
[pid=26429] vsize: 2128
Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 13911 0 0 0 1878 58 0 0 25 0 1 0 1854843811 52158464 12618 4294967295 134512640 135167914 3221224448 3221200640 134625414 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26434/statm): 12734 12618 162 162 0 12572 0
[pid=26434] vsize: 50936
Current children cumulated CPU time (s) 19.38
Current children cumulated vsize (Kb) 53064

[startup+30.0053 s]
Raw data (loadavg): 1.04 0.99 0.94 1/57 26434
Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26429/statm): 532 234 485 147 0 385 0
[pid=26429] vsize: 2128
Raw data (/proc/26434/stat): 26434 (minisat+_bignum) T 26429 26429 4419 0 -1 0 18434 0 0 0 2827 79 0 0 25 0 1 0 1854843811 65286144 15823 4294967295 134512640 135167914 3221224448 3221201372 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/26434/statm): 15939 15823 162 162 0 15777 0
[pid=26434] vsize: 63756
Current children cumulated CPU time (s) 29.08
Current children cumulated vsize (Kb) 65884

[startup+40.0049 s]
Raw data (loadavg): 1.03 0.99 0.94 2/57 26434
Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26429/statm): 532 234 485 147 0 385 0
[pid=26429] vsize: 2128
Raw data (/proc/26434/stat): 26434 (minisat+_bignum) T 26429 26429 4419 0 -1 0 27650 0 0 0 3777 107 0 0 25 0 1 0 1854843811 92233728 22402 4294967295 134512640 135167914 3221224448 3221200156 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/26434/statm): 22518 22402 162 162 0 22356 0
[pid=26434] vsize: 90072
Current children cumulated CPU time (s) 38.86
Current children cumulated vsize (Kb) 92200

[startup+50.0055 s]
Raw data (loadavg): 1.03 0.99 0.94 2/57 26434
Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26429/statm): 532 234 485 147 0 385 0
[pid=26429] vsize: 2128
Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 32403 0 0 0 4723 128 0 0 25 0 1 0 1854843811 111702016 27155 4294967295 134512640 135167914 3221224448 3221202844 134722512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26434/statm): 27271 27155 162 162 0 27109 0
[pid=26434] vsize: 109084
Current children cumulated CPU time (s) 48.53
Current children cumulated vsize (Kb) 111212

[startup+60.0061 s]
Raw data (loadavg): 1.02 0.99 0.94 1/57 26434
Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26429/statm): 532 234 485 147 0 385 0
[pid=26429] vsize: 2128
Raw data (/proc/26434/stat): 26434 (minisat+_bignum) T 26429 26429 4419 0 -1 0 37240 0 0 0 5674 147 0 0 25 0 1 0 1854843811 131514368 31992 4294967295 134512640 135167914 3221224448 3221201148 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/26434/statm): 32108 31992 162 162 0 31946 0
[pid=26434] vsize: 128432
Current children cumulated CPU time (s) 58.23
Current children cumulated vsize (Kb) 130560

[startup+70.0067 s]
Raw data (loadavg): 1.02 0.99 0.94 2/57 26434
Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26429/statm): 532 234 485 147 0 385 0
[pid=26429] vsize: 2128
Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 42090 0 0 0 6620 169 0 0 25 0 1 0 1854843811 151379968 36842 4294967295 134512640 135167914 3221224448 3221201224 134693631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26434/statm): 36958 36842 162 162 0 36796 0
[pid=26434] vsize: 147832
Current children cumulated CPU time (s) 67.91
Current children cumulated vsize (Kb) 149960

[startup+80.0073 s]
Raw data (loadavg): 1.02 0.99 0.94 2/57 26434
Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26429/statm): 532 234 485 147 0 385 0
[pid=26429] vsize: 2128
Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 55561 0 0 0 7561 208 0 0 25 0 1 0 1854843811 184958976 45040 4294967295 134512640 135167914 3221224448 3221201888 134624387 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26434/statm): 45156 45040 162 162 0 44994 0
[pid=26434] vsize: 180624
Current children cumulated CPU time (s) 77.71
Current children cumulated vsize (Kb) 182752

[startup+90.0069 s]
Raw data (loadavg): 1.01 0.99 0.94 2/57 26434
Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26429/statm): 532 234 485 147 0 385 0
[pid=26429] vsize: 2128
Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 60658 0 0 0 8503 234 0 0 25 0 1 0 1854843811 205836288 50137 4294967295 134512640 135167914 3221224448 3221200848 134849096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26434/statm): 50253 50137 162 162 0 50091 0
[pid=26434] vsize: 201012
Current children cumulated CPU time (s) 87.39
Current children cumulated vsize (Kb) 203140

[startup+100.007 s]
Raw data (loadavg): 1.01 0.99 0.94 1/57 26434
Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26429/statm): 532 234 485 147 0 385 0
[pid=26429] vsize: 2128
Raw data (/proc/26434/stat): 26434 (minisat+_bignum) T 26429 26429 4419 0 -1 0 65525 0 0 0 9451 254 0 0 24 0 1 0 1854843811 225771520 55004 4294967295 134512640 135167914 3221224448 3221200444 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/26434/statm): 55120 55004 162 162 0 54958 0
[pid=26434] vsize: 220480
Current children cumulated CPU time (s) 97.07
Current children cumulated vsize (Kb) 222608

[startup+110.008 s]
Raw data (loadavg): 1.01 0.99 0.94 2/57 26434
Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26429/statm): 532 234 485 147 0 385 0
[pid=26429] vsize: 2128
Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 70323 0 0 0 10397 278 0 0 25 0 1 0 1854843811 245424128 59802 4294967295 134512640 135167914 3221224448 3221201408 134849187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26434/statm): 59918 59802 162 162 0 59756 0
[pid=26434] vsize: 239672
Current children cumulated CPU time (s) 106.77
Current children cumulated vsize (Kb) 241800

[startup+120.01 s]
Raw data (loadavg): 1.01 0.99 0.94 2/57 26434
Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26429/statm): 532 234 485 147 0 385 0
[pid=26429] vsize: 2128
Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 75143 0 0 0 11346 301 0 0 25 0 1 0 1854843811 265166848 64622 4294967295 134512640 135167914 3221224448 3221200764 134722576 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26434/statm): 64738 64622 162 162 0 64576 0
[pid=26434] vsize: 258952
Current children cumulated CPU time (s) 116.49
Current children cumulated vsize (Kb) 261080

[startup+130.01 s]
Raw data (loadavg): 1.00 0.99 0.94 2/57 26434
Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26429/statm): 532 234 485 147 0 385 0
[pid=26429] vsize: 2128
Raw data (/proc/26434/stat): 26434 (minisat+_bignum) T 26429 26429 4419 0 -1 0 79948 0 0 0 12294 323 0 0 25 0 1 0 1854843811 284848128 69427 4294967295 134512640 135167914 3221224448 3221200220 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/26434/statm): 69543 69427 162 162 0 69381 0
[pid=26434] vsize: 278172
Current children cumulated CPU time (s) 126.19
Current children cumulated vsize (Kb) 280300

[startup+140.01 s]
Raw data (loadavg): 1.00 0.99 0.94 2/57 26434
Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26429/statm): 532 234 485 147 0 385 0
[pid=26429] vsize: 2128
Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 84843 0 0 0 13239 344 0 0 25 0 1 0 1854843811 304898048 74322 4294967295 134512640 135167914 3221224448 3221201440 134624226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26434/statm): 74438 74322 162 162 0 74276 0
[pid=26434] vsize: 297752
Current children cumulated CPU time (s) 135.85
Current children cumulated vsize (Kb) 299880

[startup+150.011 s]
Raw data (loadavg): 1.00 0.99 0.94 2/57 26434
Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26429/statm): 532 234 485 147 0 385 0
[pid=26429] vsize: 2128
Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 106786 0 0 0 14182 397 0 0 25 0 1 0 1854843811 351580160 85719 4294967295 134512640 135167914 3221224448 3221202112 134624153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26434/statm): 85835 85719 162 162 0 85673 0
[pid=26434] vsize: 343340
Current children cumulated CPU time (s) 145.81
Current children cumulated vsize (Kb) 345468

[startup+160.011 s]
Raw data (loadavg): 1.00 0.99 0.94 2/57 26434
Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26429/statm): 532 234 485 147 0 385 0
[pid=26429] vsize: 2128
Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 111934 0 0 0 15125 420 0 0 25 0 1 0 1854843811 372666368 90867 4294967295 134512640 135167914 3221224448 3221201520 134849082 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26434/statm): 90983 90867 162 162 0 90821 0
[pid=26434] vsize: 363932
Current children cumulated CPU time (s) 155.47
Current children cumulated vsize (Kb) 366060

[startup+170.012 s]
Raw data (loadavg): 1.00 0.99 0.94 2/57 26434
Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26429/statm): 532 234 485 147 0 385 0
[pid=26429] vsize: 2128
Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 116934 0 0 0 16071 443 0 0 25 0 1 0 1854843811 393146368 95867 4294967295 134512640 135167914 3221224448 3221200384 134843400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26434/statm): 95983 95867 162 162 0 95821 0
[pid=26434] vsize: 383932
Current children cumulated CPU time (s) 165.16
Current children cumulated vsize (Kb) 386060

[startup+180.012 s]
Raw data (loadavg): 1.00 0.99 0.94 2/57 26434
Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26429/statm): 532 234 485 147 0 385 0
[pid=26429] vsize: 2128
Raw data (/proc/26434/stat): 26434 (minisat+_bignum) T 26429 26429 4419 0 -1 0 121955 0 0 0 17018 467 0 0 25 0 1 0 1854843811 413712384 100888 4294967295 134512640 135167914 3221224448 3221200380 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/26434/statm): 101004 100888 162 162 0 100842 0
[pid=26434] vsize: 404016
Current children cumulated CPU time (s) 174.87
Current children cumulated vsize (Kb) 406144

[startup+190.013 s]
Raw data (loadavg): 1.00 0.99 0.94 2/57 26434
Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26429/statm): 532 234 485 147 0 385 0
[pid=26429] vsize: 2128
Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 126980 0 0 0 17957 491 0 0 25 0 1 0 1854843811 434294784 105913 4294967295 134512640 135167914 3221224448 3221200572 134843033 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26434/statm): 106029 105913 162 162 0 105867 0
[pid=26434] vsize: 424116
Current children cumulated CPU time (s) 184.5
Current children cumulated vsize (Kb) 426244

[startup+200.014 s]
Raw data (loadavg): 1.00 0.99 0.94 2/57 26434
Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26429/statm): 532 234 485 147 0 385 0
[pid=26429] vsize: 2128
Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 131996 0 0 0 18908 512 0 0 25 0 1 0 1854843811 454840320 110929 4294967295 134512640 135167914 3221224448 3221200928 134722539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26434/statm): 111045 110929 162 162 0 110883 0
[pid=26434] vsize: 444180
Current children cumulated CPU time (s) 194.22
Current children cumulated vsize (Kb) 446308

[startup+210.014 s]
Raw data (loadavg): 1.00 0.99 0.94 2/57 26434
Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26429/statm): 532 234 485 147 0 385 0
[pid=26429] vsize: 2128
Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 136904 0 0 0 19849 535 0 0 25 0 1 0 1854843811 474943488 115837 4294967295 134512640 135167914 3221224448 3221200552 134693665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26434/statm): 115953 115837 162 162 0 115791 0
[pid=26434] vsize: 463812
Current children cumulated CPU time (s) 203.86
Current children cumulated vsize (Kb) 465940

[startup+220.016 s]
Raw data (loadavg): 1.00 0.99 0.94 2/57 26434
Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26429/statm): 532 234 485 147 0 385 0
[pid=26429] vsize: 2128
Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 141787 0 0 0 20796 557 0 0 25 0 1 0 1854843811 494944256 120720 4294967295 134512640 135167914 3221224448 3221200480 134849163 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26434/statm): 120836 120720 162 162 0 120674 0
[pid=26434] vsize: 483344
Current children cumulated CPU time (s) 213.55
Current children cumulated vsize (Kb) 485472

[startup+230.016 s]
Raw data (loadavg): 1.00 0.99 0.94 2/57 26434
Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26429/statm): 532 234 485 147 0 385 0
[pid=26429] vsize: 2128
Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 146498 0 0 0 21741 579 0 0 25 0 1 0 1854843811 514240512 125431 4294967295 134512640 135167914 3221224448 3221200840 134849057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26434/statm): 125547 125431 162 162 0 125385 0
[pid=26434] vsize: 502188
Current children cumulated CPU time (s) 223.22
Current children cumulated vsize (Kb) 504316

[startup+240.017 s]
Raw data (loadavg): 1.00 0.99 0.94 2/57 26434
Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26429/statm): 532 234 485 147 0 385 0
[pid=26429] vsize: 2128
Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 151474 0 0 0 22689 602 0 0 25 0 1 0 1854843811 534622208 130407 4294967295 134512640 135167914 3221224448 3221200876 134844632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26434/statm): 130523 130407 162 162 0 130361 0
[pid=26434] vsize: 522092
Current children cumulated CPU time (s) 232.93
Current children cumulated vsize (Kb) 524220

[startup+250.018 s]
Raw data (loadavg): 1.00 0.99 0.94 2/57 26434
Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26429/statm): 532 234 485 147 0 385 0
[pid=26429] vsize: 2128
Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 156308 0 0 0 23636 626 0 0 25 0 1 0 1854843811 554422272 135241 4294967295 134512640 135167914 3221224448 3221201884 134693552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26434/statm): 135357 135241 162 162 0 135195 0
[pid=26434] vsize: 541428
Current children cumulated CPU time (s) 242.64
Current children cumulated vsize (Kb) 543556

[startup+260.018 s]
Raw data (loadavg): 1.00 0.99 0.94 2/57 26434
Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26429/statm): 532 234 485 147 0 385 0
[pid=26429] vsize: 2128
Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 161021 0 0 0 24584 647 0 0 25 0 1 0 1854843811 573726720 139954 4294967295 134512640 135167914 3221224448 3221201940 134843117 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26434/statm): 140070 139954 162 162 0 139908 0
[pid=26434] vsize: 560280
Current children cumulated CPU time (s) 252.33
Current children cumulated vsize (Kb) 562408

[startup+270.019 s]
Raw data (loadavg): 1.00 0.99 0.94 2/57 26434
Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26429/statm): 532 234 485 147 0 385 0
[pid=26429] vsize: 2128
Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 165709 0 0 0 25530 669 0 0 25 0 1 0 1854843811 592928768 144642 4294967295 134512640 135167914 3221224448 3221202224 134845901 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26434/statm): 144758 144642 162 162 0 144596 0
[pid=26434] vsize: 579032
Current children cumulated CPU time (s) 262.01
Current children cumulated vsize (Kb) 581160

[startup+280.019 s]
Raw data (loadavg): 1.00 0.99 0.94 2/57 26434
Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26429/statm): 532 234 485 147 0 385 0
[pid=26429] vsize: 2128
Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 192739 0 0 0 26429 742 0 0 25 0 1 0 1854843811 783515648 171672 4294967295 134512640 135167914 3221224448 3221201536 134625368 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26434/statm): 191288 171679 162 162 0 191126 0
[pid=26434] vsize: 765152
Current children cumulated CPU time (s) 271.73
Current children cumulated vsize (Kb) 767280

[startup+290.02 s]
Raw data (loadavg): 1.00 0.99 0.94 2/57 26434
Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26429/statm): 532 234 485 147 0 385 0
[pid=26429] vsize: 2128
Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 212239 0 0 0 27384 787 0 0 25 0 1 0 1854843811 783515648 191172 4294967295 134512640 135167914 3221224448 3221201488 134694435 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26434/statm): 191288 191172 162 162 0 191126 0
[pid=26434] vsize: 765152
Current children cumulated CPU time (s) 281.73
Current children cumulated vsize (Kb) 767280

[startup+300.021 s]
Raw data (loadavg): 1.00 0.99 0.94 2/57 26434
Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26429/statm): 532 234 485 147 0 385 0
[pid=26429] vsize: 2128
Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 214229 0 0 0 28358 799 0 0 25 0 1 0 1854843811 705277952 172071 4294967295 134512640 135167914 3221224448 3221200620 134722512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26434/statm): 172187 172071 162 162 0 172025 0
[pid=26434] vsize: 688748
Current children cumulated CPU time (s) 291.59
Current children cumulated vsize (Kb) 690876

[startup+310.021 s]
Raw data (loadavg): 1.00 0.99 0.94 2/57 26434
Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26429/statm): 532 234 485 147 0 385 0
[pid=26429] vsize: 2128
Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 219171 0 0 0 29304 819 0 0 25 0 1 0 1854843811 725520384 177013 4294967295 134512640 135167914 3221224448 3221201200 134624975 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26434/statm): 177129 177013 162 162 0 176967 0
[pid=26434] vsize: 708516
Current children cumulated CPU time (s) 301.25
Current children cumulated vsize (Kb) 710644

[startup+320.022 s]
Raw data (loadavg): 1.00 0.99 0.94 2/57 26434
Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26429/statm): 532 234 485 147 0 385 0
[pid=26429] vsize: 2128
Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 224344 0 0 0 30244 845 0 0 25 0 1 0 1854843811 746708992 182186 4294967295 134512640 135167914 3221224448 3221201728 134843010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26434/statm): 182302 182186 162 162 0 182140 0
[pid=26434] vsize: 729208
Current children cumulated CPU time (s) 310.91
Current children cumulated vsize (Kb) 731336

[startup+330.022 s]
Raw data (loadavg): 1.00 0.99 0.94 2/57 26434
Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26429/statm): 532 234 485 147 0 385 0
[pid=26429] vsize: 2128
Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 229559 0 0 0 31188 869 0 0 25 0 1 0 1854843811 768069632 187401 4294967295 134512640 135167914 3221224448 3221201468 134843033 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26434/statm): 187517 187401 162 162 0 187355 0
[pid=26434] vsize: 750068
Current children cumulated CPU time (s) 320.59
Current children cumulated vsize (Kb) 752196

[startup+340.022 s]
Raw data (loadavg): 1.00 0.99 0.94 2/57 26434
Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26429/statm): 532 234 485 147 0 385 0
[pid=26429] vsize: 2128
Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 234661 0 0 0 32130 895 0 0 25 0 1 0 1854843811 788967424 192503 4294967295 134512640 135167914 3221224448 3221201440 134622385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26434/statm): 192619 192503 162 162 0 192457 0
[pid=26434] vsize: 770476
Current children cumulated CPU time (s) 330.27
Current children cumulated vsize (Kb) 772604

[startup+350.023 s]
Raw data (loadavg): 1.00 0.99 0.94 1/57 26434
Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26429/statm): 532 234 485 147 0 385 0
[pid=26429] vsize: 2128
Raw data (/proc/26434/stat): 26434 (minisat+_bignum) T 26429 26429 4419 0 -1 0 239857 0 0 0 33079 914 0 0 25 0 1 0 1854843811 810250240 197699 4294967295 134512640 135167914 3221224448 3221200700 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/26434/statm): 197815 197699 162 162 0 197653 0
[pid=26434] vsize: 791260
Current children cumulated CPU time (s) 339.95
Current children cumulated vsize (Kb) 793388

[startup+360.023 s]
Raw data (loadavg): 1.00 0.99 0.94 2/57 26434
Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26429/statm): 532 234 485 147 0 385 0
[pid=26429] vsize: 2128
Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 245011 0 0 0 34022 939 0 0 25 0 1 0 1854843811 831361024 202853 4294967295 134512640 135167914 3221224448 3221201264 134849153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26434/statm): 202969 202853 162 162 0 202807 0
[pid=26434] vsize: 811876
Current children cumulated CPU time (s) 349.63
Current children cumulated vsize (Kb) 814004

[startup+370.024 s]
Raw data (loadavg): 1.00 0.99 0.94 2/57 26434
Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26429/statm): 532 234 485 147 0 385 0
[pid=26429] vsize: 2128
Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 250181 0 0 0 34959 966 0 0 25 0 1 0 1854843811 852537344 208023 4294967295 134512640 135167914 3221224448 3221201408 134843068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26434/statm): 208139 208023 162 162 0 207977 0
[pid=26434] vsize: 832556
Current children cumulated CPU time (s) 359.27
Current children cumulated vsize (Kb) 834684

[startup+380.024 s]
Raw data (loadavg): 1.07 1.00 0.95 2/57 26434
Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26429/statm): 532 234 485 147 0 385 0
[pid=26429] vsize: 2128
Raw data (/proc/26434/stat): 26434 (minisat+_bignum) T 26429 26429 4419 0 -1 0 255425 0 0 0 35901 989 0 0 25 0 1 0 1854843811 874016768 213267 4294967295 134512640 135167914 3221224448 3221200156 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/26434/statm): 213383 213267 162 162 0 213221 0
[pid=26434] vsize: 853532
Current children cumulated CPU time (s) 368.92
Current children cumulated vsize (Kb) 855660

[startup+390.024 s]
Raw data (loadavg): 1.06 1.00 0.95 1/57 26434
Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26429/statm): 532 234 485 147 0 385 0
[pid=26429] vsize: 2128
Raw data (/proc/26434/stat): 26434 (minisat+_bignum) T 26429 26429 4419 0 -1 0 260603 0 0 0 36841 1015 0 0 25 0 1 0 1854843811 895229952 218445 4294967295 134512640 135167914 3221224448 3221200476 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/26434/statm): 218562 218445 162 162 0 218400 0
[pid=26434] vsize: 874248
Current children cumulated CPU time (s) 378.58
Current children cumulated vsize (Kb) 876376

[startup+400.025 s]
Raw data (loadavg): 1.05 1.00 0.95 2/57 26434
Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26429/statm): 532 234 485 147 0 385 0
[pid=26429] vsize: 2128
Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 265767 0 0 0 37782 1038 0 0 25 0 1 0 1854843811 916377600 223609 4294967295 134512640 135167914 3221224448 3221200640 134621159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26434/statm): 223725 223609 162 162 0 223563 0
[pid=26434] vsize: 894900
Current children cumulated CPU time (s) 388.22
Current children cumulated vsize (Kb) 897028

[startup+410.025 s]
Raw data (loadavg): 1.04 1.00 0.95 2/57 26434
Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26429/statm): 532 234 485 147 0 385 0
[pid=26429] vsize: 2128
Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 270883 0 0 0 38721 1064 0 0 25 0 1 0 1854843811 937332736 228725 4294967295 134512640 135167914 3221224448 3221200928 134844653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26434/statm): 228841 228725 162 162 0 228679 0
[pid=26434] vsize: 915364
Current children cumulated CPU time (s) 397.87
Current children cumulated vsize (Kb) 917492



Mem limit exceeded: sending SIGTERM then SIGKILL

[startup+412.057 s]
Raw data (loadavg): 1.04 1.00 0.95 1/57 26434
Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26429/statm): 532 234 485 147 0 385 0
[pid=26429] vsize: 2128
Raw data (/proc/26434/stat): 26434 (minisat+_bignum) T 26429 26429 4419 0 -1 0 271910 0 0 0 38911 1069 0 0 25 0 1 0 1854843811 941543424 229752 4294967295 134512640 135167914 3221224448 3221201788 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/26434/statm): 229869 229752 162 162 0 229707 0
[pid=26434] vsize: 919476
Current children cumulated CPU time (s) 399.82
Current children cumulated vsize (Kb) 921604

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

Child status: 0
Real time (s): 412.487
CPU time (s): 400.237
CPU user time (s): 389.119
CPU system time (s): 11.1183
CPU usage (%): 97.0303
Max. virtual memory (cumulated for all children) (Kb): 921604

Verifier Data

ERROR: no interpretation found !