Some explanations

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

General information on the benchmark

Namemps-v2-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-agg2.opb
MD5SUM0cd976844df23087580a4e793412c20f
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 6930
Biggest coefficient in the objective function 53730040872960
Number of bits for the biggest coefficient in the objective function 46
Sum of the numbers in the objective function 8516865379203027
Number of bits of the sum of numbers in the objective function 53
Biggest number in a constraint 22763326668800000
Number of bits of the biggest number in a constraint 55
Biggest sum of numbers in a constraint 46271983665442689
Number of bits of the biggest sum of numbers56
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables9060
Total number of constraints467
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints467
Minimum length of a constraint30
Maximum length of a constraint1440

Trace number 2606

Launcher Data

LAUNCH ON wulflinc26 THE 2005-09-18 20:09:20 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2750 boxname=wulflinc26 idbench=406 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  0cd976844df23087580a4e793412c20f  /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-20-10-agg2.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-20-10-agg2.opb
IDLAUNCH: 2750
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
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.061
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:        901688 kB
Buffers:         35812 kB
Cached:          69196 kB
SwapCached:        868 kB
Active:          69280 kB
Inactive:        38376 kB
HighTotal:      131008 kB
HighFree:        59080 kB
LowTotal:       903652 kB
LowFree:        842608 kB
SwapTotal:     2097892 kB
SwapFree:      2096540 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           5700 kB
Slab:            19708 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 20:29:30 (client local time) WITH STATUS 0 IN 1209.9 SECONDS
stats: 2750 7 1209.9 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 306] 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/26280/stat): 26280 (minisat+_script) R 26279 26280 16528 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1844032709 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/26280/statm): 174 3 169 147 0 27 0
[pid=26280] 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=26281
New process pid=26282
New process pid=26283
execve syscall for /bin/sed executable
One traced child (pid=26282) 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=26283) exited with status: 0
One traced child (pid=26281) exited with status: 0
New process pid=26284
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-20-10-agg2.opb
One traced child (pid=26284) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=26285
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-20-10-agg2.opb

[startup+10.0041 s]
Raw data (loadavg): 0.72 0.83 0.89 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 1966 0 3 0 947 15 0 0 25 0 1 0 1844032717 8589312 1901 4294967295 134512640 135167914 3221224448 3221221228 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2097 1901 162 162 0 1935 0
[pid=26285] vsize: 8388
Current children cumulated CPU time (s) 9.65
Current children cumulated vsize (Kb) 10516

[startup+20.0048 s]
Raw data (loadavg): 0.76 0.84 0.89 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2022 0 3 0 1946 16 0 0 25 0 1 0 1844032717 8769536 1957 4294967295 134512640 135167914 3221224448 3221219616 134845890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2141 1957 162 162 0 1979 0
[pid=26285] vsize: 8564
Current children cumulated CPU time (s) 19.65
Current children cumulated vsize (Kb) 10692

[startup+30.0055 s]
Raw data (loadavg): 0.80 0.84 0.89 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2022 0 3 0 2947 16 0 0 25 0 1 0 1844032717 8769536 1957 4294967295 134512640 135167914 3221224448 3221221744 134849099 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2141 1957 162 162 0 1979 0
[pid=26285] vsize: 8564
Current children cumulated CPU time (s) 29.66
Current children cumulated vsize (Kb) 10692

[startup+40.0062 s]
Raw data (loadavg): 0.83 0.85 0.90 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2153 0 3 0 3945 17 0 0 25 0 1 0 1844032717 9224192 2046 4294967295 134512640 135167914 3221224448 3221218560 134844715 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2252 2046 162 162 0 2090 0
[pid=26285] vsize: 9008
Current children cumulated CPU time (s) 39.65
Current children cumulated vsize (Kb) 11136

[startup+50.0068 s]
Raw data (loadavg): 0.85 0.85 0.90 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2153 0 3 0 4945 17 0 0 25 0 1 0 1844032717 9224192 2046 4294967295 134512640 135167914 3221224448 3221219696 134849122 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2252 2046 162 162 0 2090 0
[pid=26285] vsize: 9008
Current children cumulated CPU time (s) 49.65
Current children cumulated vsize (Kb) 11136

[startup+60.0065 s]
Raw data (loadavg): 0.88 0.86 0.90 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2153 0 3 0 5945 17 0 0 25 0 1 0 1844032717 9224192 2046 4294967295 134512640 135167914 3221224448 3221220336 134696653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2252 2046 162 162 0 2090 0
[pid=26285] vsize: 9008
Current children cumulated CPU time (s) 59.65
Current children cumulated vsize (Kb) 11136

[startup+70.0072 s]
Raw data (loadavg): 0.89 0.86 0.90 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2153 0 3 0 6946 17 0 0 25 0 1 0 1844032717 9224192 2046 4294967295 134512640 135167914 3221224448 3221220896 134845881 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2252 2046 162 162 0 2090 0
[pid=26285] vsize: 9008
Current children cumulated CPU time (s) 69.66
Current children cumulated vsize (Kb) 11136

[startup+80.0079 s]
Raw data (loadavg): 0.91 0.87 0.90 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2153 0 3 0 7946 17 0 0 25 0 1 0 1844032717 9224192 2046 4294967295 134512640 135167914 3221224448 3221221728 134844647 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2252 2046 162 162 0 2090 0
[pid=26285] vsize: 9008
Current children cumulated CPU time (s) 79.66
Current children cumulated vsize (Kb) 11136

[startup+90.0086 s]
Raw data (loadavg): 0.92 0.87 0.90 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2153 0 3 0 8946 17 0 0 25 0 1 0 1844032717 9224192 2046 4294967295 134512640 135167914 3221224448 3221221408 134693563 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2252 2046 162 162 0 2090 0
[pid=26285] vsize: 9008
Current children cumulated CPU time (s) 89.66
Current children cumulated vsize (Kb) 11136

[startup+100.009 s]
Raw data (loadavg): 0.93 0.87 0.90 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2153 0 3 0 9946 17 0 0 25 0 1 0 1844032717 9224192 2046 4294967295 134512640 135167914 3221224448 3221221728 134845906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2252 2046 162 162 0 2090 0
[pid=26285] vsize: 9008
Current children cumulated CPU time (s) 99.66
Current children cumulated vsize (Kb) 11136

[startup+110.01 s]
Raw data (loadavg): 0.94 0.88 0.90 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2233 0 3 0 10946 17 0 0 25 0 1 0 1844032717 9478144 2126 4294967295 134512640 135167914 3221224448 3221218208 134843064 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2126 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 109.66
Current children cumulated vsize (Kb) 11384

[startup+120.011 s]
Raw data (loadavg): 0.95 0.88 0.90 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2233 0 3 0 11946 18 0 0 25 0 1 0 1844032717 9478144 2126 4294967295 134512640 135167914 3221224448 3221220400 134849108 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2126 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 119.67
Current children cumulated vsize (Kb) 11384

[startup+130.011 s]
Raw data (loadavg): 0.96 0.88 0.90 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2233 0 3 0 12946 18 0 0 25 0 1 0 1844032717 9478144 2126 4294967295 134512640 135167914 3221224448 3221221020 134718176 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2126 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 129.67
Current children cumulated vsize (Kb) 11384

[startup+140.012 s]
Raw data (loadavg): 0.97 0.89 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2233 0 3 0 13947 18 0 0 25 0 1 0 1844032717 9478144 2126 4294967295 134512640 135167914 3221224448 3221222064 134845895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2126 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 139.68
Current children cumulated vsize (Kb) 11384

[startup+150.013 s]
Raw data (loadavg): 0.97 0.89 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2233 0 3 0 14947 18 0 0 25 0 1 0 1844032717 9478144 2126 4294967295 134512640 135167914 3221224448 3221218400 134843036 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2126 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 149.68
Current children cumulated vsize (Kb) 11384

[startup+160.012 s]
Raw data (loadavg): 0.97 0.89 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2233 0 3 0 15947 18 0 0 25 0 1 0 1844032717 9478144 2126 4294967295 134512640 135167914 3221224448 3221218928 134843406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2126 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 159.68
Current children cumulated vsize (Kb) 11384

[startup+170.013 s]
Raw data (loadavg): 0.98 0.90 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2233 0 3 0 16947 18 0 0 25 0 1 0 1844032717 9478144 2126 4294967295 134512640 135167914 3221224448 3221219628 134723236 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2126 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 169.68
Current children cumulated vsize (Kb) 11384

[startup+180.013 s]
Raw data (loadavg): 0.98 0.90 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2233 0 3 0 17947 18 0 0 25 0 1 0 1844032717 9478144 2126 4294967295 134512640 135167914 3221224448 3221219824 134844637 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2126 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 179.68
Current children cumulated vsize (Kb) 11384

[startup+190.014 s]
Raw data (loadavg): 0.98 0.90 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2233 0 3 0 18948 18 0 0 25 0 1 0 1844032717 9478144 2126 4294967295 134512640 135167914 3221224448 3221219728 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2126 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 189.69
Current children cumulated vsize (Kb) 11384

[startup+200.015 s]
Raw data (loadavg): 0.98 0.90 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2233 0 3 0 19948 18 0 0 25 0 1 0 1844032717 9478144 2126 4294967295 134512640 135167914 3221224448 3221219328 134849148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2126 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 199.69
Current children cumulated vsize (Kb) 11384

[startup+210.015 s]
Raw data (loadavg): 0.99 0.91 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2233 0 3 0 20948 18 0 0 25 0 1 0 1844032717 9478144 2126 4294967295 134512640 135167914 3221224448 3221219500 134695322 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2126 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 209.69
Current children cumulated vsize (Kb) 11384

[startup+220.015 s]
Raw data (loadavg): 0.99 0.91 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2233 0 3 0 21948 18 0 0 25 0 1 0 1844032717 9478144 2126 4294967295 134512640 135167914 3221224448 3221220512 134696611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2126 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 219.69
Current children cumulated vsize (Kb) 11384

[startup+230.015 s]
Raw data (loadavg): 0.99 0.91 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2233 0 3 0 22948 18 0 0 25 0 1 0 1844032717 9478144 2126 4294967295 134512640 135167914 3221224448 3221220320 134844728 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2126 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 229.69
Current children cumulated vsize (Kb) 11384

[startup+240.016 s]
Raw data (loadavg): 0.99 0.91 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2233 0 3 0 23948 18 0 0 25 0 1 0 1844032717 9478144 2126 4294967295 134512640 135167914 3221224448 3221220032 134694489 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2126 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 239.69
Current children cumulated vsize (Kb) 11384

[startup+250.017 s]
Raw data (loadavg): 0.99 0.92 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2233 0 3 0 24949 18 0 0 25 0 1 0 1844032717 9478144 2126 4294967295 134512640 135167914 3221224448 3221220752 134522206 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2126 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 249.7
Current children cumulated vsize (Kb) 11384

[startup+260.016 s]
Raw data (loadavg): 0.99 0.92 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2233 0 3 0 25948 19 0 0 25 0 1 0 1844032717 9478144 2126 4294967295 134512640 135167914 3221224448 3221219792 134843123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2126 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 259.7
Current children cumulated vsize (Kb) 11384

[startup+270.017 s]
Raw data (loadavg): 0.99 0.92 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2233 0 3 0 26949 19 0 0 25 0 1 0 1844032717 9478144 2126 4294967295 134512640 135167914 3221224448 3221220672 134844718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2126 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 269.71
Current children cumulated vsize (Kb) 11384

[startup+280.018 s]
Raw data (loadavg): 0.99 0.92 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2233 0 3 0 27949 19 0 0 25 0 1 0 1844032717 9478144 2126 4294967295 134512640 135167914 3221224448 3221220848 134844720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2126 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 279.71
Current children cumulated vsize (Kb) 11384

[startup+290.018 s]
Raw data (loadavg): 0.99 0.92 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2233 0 3 0 28949 19 0 0 25 0 1 0 1844032717 9478144 2126 4294967295 134512640 135167914 3221224448 3221220576 134693566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2126 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 289.71
Current children cumulated vsize (Kb) 11384

[startup+300.019 s]
Raw data (loadavg): 0.99 0.93 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2233 0 3 0 29949 19 0 0 25 0 1 0 1844032717 9478144 2126 4294967295 134512640 135167914 3221224448 3221220388 134849060 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2126 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 299.71
Current children cumulated vsize (Kb) 11384

[startup+310.019 s]
Raw data (loadavg): 0.99 0.93 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2233 0 3 0 30950 19 0 0 25 0 1 0 1844032717 9478144 2126 4294967295 134512640 135167914 3221224448 3221221024 134845895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2126 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 309.72
Current children cumulated vsize (Kb) 11384

[startup+320.019 s]
Raw data (loadavg): 0.99 0.93 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2233 0 3 0 31949 19 0 0 25 0 1 0 1844032717 9478144 2126 4294967295 134512640 135167914 3221224448 3221220856 134693609 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2126 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 319.71
Current children cumulated vsize (Kb) 11384

[startup+330.019 s]
Raw data (loadavg): 0.99 0.93 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2233 0 3 0 32950 19 0 0 25 0 1 0 1844032717 9478144 2126 4294967295 134512640 135167914 3221224448 3221220864 134843404 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2126 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 329.72
Current children cumulated vsize (Kb) 11384

[startup+340.02 s]
Raw data (loadavg): 0.99 0.93 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2233 0 3 0 33950 19 0 0 25 0 1 0 1844032717 9478144 2126 4294967295 134512640 135167914 3221224448 3221220496 134845913 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2126 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 339.72
Current children cumulated vsize (Kb) 11384

[startup+350.02 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2233 0 3 0 34950 19 0 0 25 0 1 0 1844032717 9478144 2126 4294967295 134512640 135167914 3221224448 3221221184 134843118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2126 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 349.72
Current children cumulated vsize (Kb) 11384

[startup+360.02 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2233 0 3 0 35950 19 0 0 25 0 1 0 1844032717 9478144 2126 4294967295 134512640 135167914 3221224448 3221220608 134844647 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2126 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 359.72
Current children cumulated vsize (Kb) 11384

[startup+370.021 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2233 0 3 0 36951 19 0 0 25 0 1 0 1844032717 9478144 2126 4294967295 134512640 135167914 3221224448 3221221536 134845930 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2126 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 369.73
Current children cumulated vsize (Kb) 11384

[startup+380.021 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2233 0 3 0 37951 19 0 0 25 0 1 0 1844032717 9478144 2126 4294967295 134512640 135167914 3221224448 3221220848 134696766 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2126 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 379.73
Current children cumulated vsize (Kb) 11384

[startup+390.022 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2233 0 3 0 38951 19 0 0 25 0 1 0 1844032717 9478144 2126 4294967295 134512640 135167914 3221224448 3221220896 134722539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2126 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 389.73
Current children cumulated vsize (Kb) 11384

[startup+400.023 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2233 0 3 0 39951 19 0 0 25 0 1 0 1844032717 9478144 2126 4294967295 134512640 135167914 3221224448 3221220836 134843117 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2126 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 399.73
Current children cumulated vsize (Kb) 11384

[startup+410.023 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2233 0 3 0 40951 19 0 0 25 0 1 0 1844032717 9478144 2126 4294967295 134512640 135167914 3221224448 3221220848 134843113 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2126 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 409.73
Current children cumulated vsize (Kb) 11384

[startup+420.024 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2233 0 3 0 41952 19 0 0 25 0 1 0 1844032717 9478144 2126 4294967295 134512640 135167914 3221224448 3221221440 134843406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2126 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 419.74
Current children cumulated vsize (Kb) 11384

[startup+430.025 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2233 0 3 0 42952 19 0 0 25 0 1 0 1844032717 9478144 2126 4294967295 134512640 135167914 3221224448 3221221472 134629118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2126 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 429.74
Current children cumulated vsize (Kb) 11384

[startup+440.026 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2233 0 3 0 43952 19 0 0 25 0 1 0 1844032717 9478144 2126 4294967295 134512640 135167914 3221224448 3221221472 134629345 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2126 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 439.74
Current children cumulated vsize (Kb) 11384

[startup+450.027 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2233 0 3 0 44952 19 0 0 25 0 1 0 1844032717 9478144 2126 4294967295 134512640 135167914 3221224448 3221221036 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2126 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 449.74
Current children cumulated vsize (Kb) 11384

[startup+460.027 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2233 0 3 0 45952 19 0 0 25 0 1 0 1844032717 9478144 2126 4294967295 134512640 135167914 3221224448 3221221200 134844708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2126 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 459.74
Current children cumulated vsize (Kb) 11384

[startup+470.028 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2233 0 3 0 46952 19 0 0 25 0 1 0 1844032717 9478144 2126 4294967295 134512640 135167914 3221224448 3221221472 134630853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2126 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 469.74
Current children cumulated vsize (Kb) 11384

[startup+480.028 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2233 0 3 0 47953 19 0 0 25 0 1 0 1844032717 9478144 2126 4294967295 134512640 135167914 3221224448 3221222108 134842996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2126 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 479.75
Current children cumulated vsize (Kb) 11384

[startup+490.029 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2233 0 3 0 48953 19 0 0 25 0 1 0 1844032717 9478144 2126 4294967295 134512640 135167914 3221224448 3221221788 134722512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2126 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 489.75
Current children cumulated vsize (Kb) 11384

[startup+500.03 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2237 0 3 0 49953 19 0 0 25 0 1 0 1844032717 9478144 2130 4294967295 134512640 135167914 3221224448 3221219216 134844676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2130 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 499.75
Current children cumulated vsize (Kb) 11384

[startup+510.03 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2237 0 3 0 50953 19 0 0 25 0 1 0 1844032717 9478144 2130 4294967295 134512640 135167914 3221224448 3221219632 134696587 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2130 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 509.75
Current children cumulated vsize (Kb) 11384

[startup+520.031 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2237 0 3 0 51954 19 0 0 25 0 1 0 1844032717 9478144 2130 4294967295 134512640 135167914 3221224448 3221220496 134843010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2130 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 519.76
Current children cumulated vsize (Kb) 11384

[startup+530.031 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2237 0 3 0 52954 19 0 0 25 0 1 0 1844032717 9478144 2130 4294967295 134512640 135167914 3221224448 3221219856 134843036 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2130 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 529.76
Current children cumulated vsize (Kb) 11384

[startup+540.031 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2237 0 3 0 53954 19 0 0 25 0 1 0 1844032717 9478144 2130 4294967295 134512640 135167914 3221224448 3221220884 134845880 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2130 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 539.76
Current children cumulated vsize (Kb) 11384

[startup+550.032 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2237 0 3 0 54954 20 0 0 25 0 1 0 1844032717 9478144 2130 4294967295 134512640 135167914 3221224448 3221221024 134844718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2130 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 549.77
Current children cumulated vsize (Kb) 11384

[startup+560.033 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2237 0 3 0 55954 20 0 0 25 0 1 0 1844032717 9478144 2130 4294967295 134512640 135167914 3221224448 3221220528 134720503 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2130 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 559.77
Current children cumulated vsize (Kb) 11384

[startup+570.033 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2237 0 3 0 56955 20 0 0 25 0 1 0 1844032717 9478144 2130 4294967295 134512640 135167914 3221224448 3221221260 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2130 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 569.78
Current children cumulated vsize (Kb) 11384

[startup+580.034 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2237 0 3 0 57953 21 0 0 25 0 1 0 1844032717 9478144 2130 4294967295 134512640 135167914 3221224448 3221221488 134844720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2130 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 579.77
Current children cumulated vsize (Kb) 11384

[startup+590.035 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2237 0 3 0 58953 21 0 0 25 0 1 0 1844032717 9478144 2130 4294967295 134512640 135167914 3221224448 3221220496 134844668 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2130 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 589.77
Current children cumulated vsize (Kb) 11384

[startup+600.035 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2237 0 3 0 59953 22 0 0 25 0 1 0 1844032717 9478144 2130 4294967295 134512640 135167914 3221224448 3221221552 134696386 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2130 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 599.78
Current children cumulated vsize (Kb) 11384

[startup+610.036 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2237 0 3 0 60953 22 0 0 25 0 1 0 1844032717 9478144 2130 4294967295 134512640 135167914 3221224448 3221222316 134845940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2314 2130 162 162 0 2152 0
[pid=26285] vsize: 9256
Current children cumulated CPU time (s) 609.78
Current children cumulated vsize (Kb) 11384

[startup+620.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2336 0 3 0 61953 22 0 0 25 0 1 0 1844032717 9842688 2187 4294967295 134512640 135167914 3221224448 3221218448 134843010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2403 2187 162 162 0 2241 0
[pid=26285] vsize: 9612
Current children cumulated CPU time (s) 619.78
Current children cumulated vsize (Kb) 11740

[startup+630.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2336 0 3 0 62953 22 0 0 25 0 1 0 1844032717 9842688 2187 4294967295 134512640 135167914 3221224448 3221220400 134522227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2403 2187 162 162 0 2241 0
[pid=26285] vsize: 9612
Current children cumulated CPU time (s) 629.78
Current children cumulated vsize (Kb) 11740

[startup+640.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2336 0 3 0 63953 23 0 0 25 0 1 0 1844032717 9842688 2187 4294967295 134512640 135167914 3221224448 3221219456 134696643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2403 2187 162 162 0 2241 0
[pid=26285] vsize: 9612
Current children cumulated CPU time (s) 639.79
Current children cumulated vsize (Kb) 11740

[startup+650.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2336 0 3 0 64953 23 0 0 25 0 1 0 1844032717 9842688 2187 4294967295 134512640 135167914 3221224448 3221220672 134845921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2403 2187 162 162 0 2241 0
[pid=26285] vsize: 9612
Current children cumulated CPU time (s) 649.79
Current children cumulated vsize (Kb) 11740

[startup+660.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2336 0 3 0 65953 23 0 0 25 0 1 0 1844032717 9842688 2187 4294967295 134512640 135167914 3221224448 3221219968 134844706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2403 2187 162 162 0 2241 0
[pid=26285] vsize: 9612
Current children cumulated CPU time (s) 659.79
Current children cumulated vsize (Kb) 11740

[startup+670.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2336 0 3 0 66954 23 0 0 25 0 1 0 1844032717 9842688 2187 4294967295 134512640 135167914 3221224448 3221221200 134844731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2403 2187 162 162 0 2241 0
[pid=26285] vsize: 9612
Current children cumulated CPU time (s) 669.8
Current children cumulated vsize (Kb) 11740

[startup+680.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2336 0 3 0 67954 23 0 0 25 0 1 0 1844032717 9842688 2187 4294967295 134512640 135167914 3221224448 3221220224 134849193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2403 2187 162 162 0 2241 0
[pid=26285] vsize: 9612
Current children cumulated CPU time (s) 679.8
Current children cumulated vsize (Kb) 11740

[startup+690.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2336 0 3 0 68954 23 0 0 25 0 1 0 1844032717 9842688 2187 4294967295 134512640 135167914 3221224448 3221221024 134843402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2403 2187 162 162 0 2241 0
[pid=26285] vsize: 9612
Current children cumulated CPU time (s) 689.8
Current children cumulated vsize (Kb) 11740

[startup+700.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2336 0 3 0 69954 23 0 0 25 0 1 0 1844032717 9842688 2187 4294967295 134512640 135167914 3221224448 3221219824 134720484 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2403 2187 162 162 0 2241 0
[pid=26285] vsize: 9612
Current children cumulated CPU time (s) 699.8
Current children cumulated vsize (Kb) 11740

[startup+710.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2336 0 3 0 70954 23 0 0 25 0 1 0 1844032717 9842688 2187 4294967295 134512640 135167914 3221224448 3221221932 134845882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2403 2187 162 162 0 2241 0
[pid=26285] vsize: 9612
Current children cumulated CPU time (s) 709.8
Current children cumulated vsize (Kb) 11740

[startup+720.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2336 0 3 0 71954 24 0 0 25 0 1 0 1844032717 9842688 2187 4294967295 134512640 135167914 3221224448 3221221464 134696787 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2403 2187 162 162 0 2241 0
[pid=26285] vsize: 9612
Current children cumulated CPU time (s) 719.81
Current children cumulated vsize (Kb) 11740

[startup+730.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2336 0 3 0 72954 24 0 0 25 0 1 0 1844032717 9842688 2187 4294967295 134512640 135167914 3221224448 3221220008 134845877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2403 2187 162 162 0 2241 0
[pid=26285] vsize: 9612
Current children cumulated CPU time (s) 729.81
Current children cumulated vsize (Kb) 11740

[startup+740.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2336 0 3 0 73955 24 0 0 25 0 1 0 1844032717 9842688 2187 4294967295 134512640 135167914 3221224448 3221221616 134849110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2403 2187 162 162 0 2241 0
[pid=26285] vsize: 9612
Current children cumulated CPU time (s) 739.82
Current children cumulated vsize (Kb) 11740

[startup+750.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2368 0 3 0 74955 24 0 0 25 0 1 0 1844032717 9883648 2219 4294967295 134512640 135167914 3221224448 3221220688 134696200 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2413 2219 162 162 0 2251 0
[pid=26285] vsize: 9652
Current children cumulated CPU time (s) 749.82
Current children cumulated vsize (Kb) 11780

[startup+760.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2368 0 3 0 75955 24 0 0 25 0 1 0 1844032717 9883648 2219 4294967295 134512640 135167914 3221224448 3221221552 134843420 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2413 2219 162 162 0 2251 0
[pid=26285] vsize: 9652
Current children cumulated CPU time (s) 759.82
Current children cumulated vsize (Kb) 11780

[startup+770.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2814 0 3 0 76952 26 0 0 25 0 1 0 1844032717 11374592 2540 4294967295 134512640 135167914 3221224448 3221218944 134722532 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2777 2540 162 162 0 2615 0
[pid=26285] vsize: 11108
Current children cumulated CPU time (s) 769.81
Current children cumulated vsize (Kb) 13236

[startup+780.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2814 0 3 0 77952 26 0 0 25 0 1 0 1844032717 11374592 2540 4294967295 134512640 135167914 3221224448 3221219068 134845882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2777 2540 162 162 0 2615 0
[pid=26285] vsize: 11108
Current children cumulated CPU time (s) 779.81
Current children cumulated vsize (Kb) 13236

[startup+790.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2814 0 3 0 78953 26 0 0 25 0 1 0 1844032717 11374592 2540 4294967295 134512640 135167914 3221224448 3221219392 134845903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2777 2540 162 162 0 2615 0
[pid=26285] vsize: 11108
Current children cumulated CPU time (s) 789.82
Current children cumulated vsize (Kb) 13236

[startup+800.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2814 0 3 0 79953 26 0 0 25 0 1 0 1844032717 11374592 2540 4294967295 134512640 135167914 3221224448 3221219440 134844700 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2777 2540 162 162 0 2615 0
[pid=26285] vsize: 11108
Current children cumulated CPU time (s) 799.82
Current children cumulated vsize (Kb) 13236

[startup+810.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2814 0 3 0 80953 26 0 0 25 0 1 0 1844032717 11374592 2540 4294967295 134512640 135167914 3221224448 3221219792 134843404 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2777 2540 162 162 0 2615 0
[pid=26285] vsize: 11108
Current children cumulated CPU time (s) 809.82
Current children cumulated vsize (Kb) 13236

[startup+820.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2814 0 3 0 81953 26 0 0 25 0 1 0 1844032717 11374592 2540 4294967295 134512640 135167914 3221224448 3221219424 134845901 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2777 2540 162 162 0 2615 0
[pid=26285] vsize: 11108
Current children cumulated CPU time (s) 819.82
Current children cumulated vsize (Kb) 13236

[startup+830.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2814 0 3 0 82953 26 0 0 25 0 1 0 1844032717 11374592 2540 4294967295 134512640 135167914 3221224448 3221219504 134843400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2777 2540 162 162 0 2615 0
[pid=26285] vsize: 11108
Current children cumulated CPU time (s) 829.82
Current children cumulated vsize (Kb) 13236

[startup+840.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2814 0 3 0 83953 26 0 0 25 0 1 0 1844032717 11374592 2540 4294967295 134512640 135167914 3221224448 3221220940 134843033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2777 2540 162 162 0 2615 0
[pid=26285] vsize: 11108
Current children cumulated CPU time (s) 839.82
Current children cumulated vsize (Kb) 13236

[startup+850.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2814 0 3 0 84954 26 0 0 25 0 1 0 1844032717 11374592 2540 4294967295 134512640 135167914 3221224448 3221220056 134849087 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2777 2540 162 162 0 2615 0
[pid=26285] vsize: 11108
Current children cumulated CPU time (s) 849.83
Current children cumulated vsize (Kb) 13236

[startup+860.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2814 0 3 0 85954 26 0 0 25 0 1 0 1844032717 11374592 2540 4294967295 134512640 135167914 3221224448 3221218560 134845927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2777 2540 162 162 0 2615 0
[pid=26285] vsize: 11108
Current children cumulated CPU time (s) 859.83
Current children cumulated vsize (Kb) 13236

[startup+870.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2814 0 3 0 86954 26 0 0 25 0 1 0 1844032717 11374592 2540 4294967295 134512640 135167914 3221224448 3221220000 134845881 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2777 2540 162 162 0 2615 0
[pid=26285] vsize: 11108
Current children cumulated CPU time (s) 869.83
Current children cumulated vsize (Kb) 13236

[startup+880.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2814 0 3 0 87954 26 0 0 25 0 1 0 1844032717 11374592 2540 4294967295 134512640 135167914 3221224448 3221220912 134843113 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2777 2540 162 162 0 2615 0
[pid=26285] vsize: 11108
Current children cumulated CPU time (s) 879.83
Current children cumulated vsize (Kb) 13236

[startup+890.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2814 0 3 0 88954 26 0 0 25 0 1 0 1844032717 11374592 2540 4294967295 134512640 135167914 3221224448 3221219644 134723291 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2777 2540 162 162 0 2615 0
[pid=26285] vsize: 11108
Current children cumulated CPU time (s) 889.83
Current children cumulated vsize (Kb) 13236

[startup+900.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2814 0 3 0 89955 26 0 0 25 0 1 0 1844032717 11374592 2540 4294967295 134512640 135167914 3221224448 3221220536 134844674 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2777 2540 162 162 0 2615 0
[pid=26285] vsize: 11108
Current children cumulated CPU time (s) 899.84
Current children cumulated vsize (Kb) 13236

[startup+910.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2814 0 3 0 90955 26 0 0 25 0 1 0 1844032717 11374592 2540 4294967295 134512640 135167914 3221224448 3221218752 134696194 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2777 2540 162 162 0 2615 0
[pid=26285] vsize: 11108
Current children cumulated CPU time (s) 909.84
Current children cumulated vsize (Kb) 13236

[startup+920.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2814 0 3 0 91955 27 0 0 25 0 1 0 1844032717 11374592 2540 4294967295 134512640 135167914 3221224448 3221220384 134849187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2777 2540 162 162 0 2615 0
[pid=26285] vsize: 11108
Current children cumulated CPU time (s) 919.85
Current children cumulated vsize (Kb) 13236

[startup+930.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2814 0 3 0 92955 27 0 0 25 0 1 0 1844032717 11374592 2540 4294967295 134512640 135167914 3221224448 3221221104 134693582 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2777 2540 162 162 0 2615 0
[pid=26285] vsize: 11108
Current children cumulated CPU time (s) 929.85
Current children cumulated vsize (Kb) 13236

[startup+940.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2814 0 3 0 93955 27 0 0 25 0 1 0 1844032717 11374592 2540 4294967295 134512640 135167914 3221224448 3221219068 134718182 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2777 2540 162 162 0 2615 0
[pid=26285] vsize: 11108
Current children cumulated CPU time (s) 939.85
Current children cumulated vsize (Kb) 13236

[startup+950.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2814 0 3 0 94955 27 0 0 25 0 1 0 1844032717 11374592 2540 4294967295 134512640 135167914 3221224448 3221220432 134629322 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2777 2540 162 162 0 2615 0
[pid=26285] vsize: 11108
Current children cumulated CPU time (s) 949.85
Current children cumulated vsize (Kb) 13236

[startup+960.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2814 0 3 0 95956 27 0 0 25 0 1 0 1844032717 11374592 2540 4294967295 134512640 135167914 3221224448 3221220960 134844736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2777 2540 162 162 0 2615 0
[pid=26285] vsize: 11108
Current children cumulated CPU time (s) 959.86
Current children cumulated vsize (Kb) 13236

[startup+970.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2814 0 3 0 96956 27 0 0 25 0 1 0 1844032717 11374592 2540 4294967295 134512640 135167914 3221224448 3221219184 134630795 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2777 2540 162 162 0 2615 0
[pid=26285] vsize: 11108
Current children cumulated CPU time (s) 969.86
Current children cumulated vsize (Kb) 13236

[startup+980.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2814 0 3 0 97956 27 0 0 25 0 1 0 1844032717 11374592 2540 4294967295 134512640 135167914 3221224448 3221220732 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2777 2540 162 162 0 2615 0
[pid=26285] vsize: 11108
Current children cumulated CPU time (s) 979.86
Current children cumulated vsize (Kb) 13236

[startup+990.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2814 0 3 0 98956 27 0 0 25 0 1 0 1844032717 11374592 2540 4294967295 134512640 135167914 3221224448 3221220848 134844728 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2777 2540 162 162 0 2615 0
[pid=26285] vsize: 11108
Current children cumulated CPU time (s) 989.86
Current children cumulated vsize (Kb) 13236

[startup+1000.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2814 0 3 0 99956 27 0 0 25 0 1 0 1844032717 11374592 2540 4294967295 134512640 135167914 3221224448 3221220848 134696682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2777 2540 162 162 0 2615 0
[pid=26285] vsize: 11108
Current children cumulated CPU time (s) 999.86
Current children cumulated vsize (Kb) 13236

[startup+1010.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2814 0 3 0 100956 27 0 0 25 0 1 0 1844032717 11374592 2540 4294967295 134512640 135167914 3221224448 3221220524 134842996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2777 2540 162 162 0 2615 0
[pid=26285] vsize: 11108
Current children cumulated CPU time (s) 1009.86
Current children cumulated vsize (Kb) 13236

[startup+1020.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2814 0 3 0 101957 27 0 0 25 0 1 0 1844032717 11374592 2540 4294967295 134512640 135167914 3221224448 3221220896 134843123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2777 2540 162 162 0 2615 0
[pid=26285] vsize: 11108
Current children cumulated CPU time (s) 1019.87
Current children cumulated vsize (Kb) 13236

[startup+1030.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2814 0 3 0 102957 27 0 0 25 0 1 0 1844032717 11374592 2540 4294967295 134512640 135167914 3221224448 3221221112 134843032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2777 2540 162 162 0 2615 0
[pid=26285] vsize: 11108
Current children cumulated CPU time (s) 1029.87
Current children cumulated vsize (Kb) 13236

[startup+1040.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2814 0 3 0 103957 27 0 0 25 0 1 0 1844032717 11374592 2540 4294967295 134512640 135167914 3221224448 3221219504 134843107 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2777 2540 162 162 0 2615 0
[pid=26285] vsize: 11108
Current children cumulated CPU time (s) 1039.87
Current children cumulated vsize (Kb) 13236

[startup+1050.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2814 0 3 0 104957 27 0 0 25 0 1 0 1844032717 11374592 2540 4294967295 134512640 135167914 3221224448 3221220508 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2777 2540 162 162 0 2615 0
[pid=26285] vsize: 11108
Current children cumulated CPU time (s) 1049.87
Current children cumulated vsize (Kb) 13236

[startup+1060.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2814 0 3 0 105958 27 0 0 25 0 1 0 1844032717 11374592 2540 4294967295 134512640 135167914 3221224448 3221221280 134843030 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2777 2540 162 162 0 2615 0
[pid=26285] vsize: 11108
Current children cumulated CPU time (s) 1059.88
Current children cumulated vsize (Kb) 13236

[startup+1070.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2814 0 3 0 106958 27 0 0 25 0 1 0 1844032717 11374592 2540 4294967295 134512640 135167914 3221224448 3221221728 134844653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2777 2540 162 162 0 2615 0
[pid=26285] vsize: 11108
Current children cumulated CPU time (s) 1069.88
Current children cumulated vsize (Kb) 13236

[startup+1080.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2814 0 3 0 107958 27 0 0 25 0 1 0 1844032717 11374592 2540 4294967295 134512640 135167914 3221224448 3221220380 134845876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2777 2540 162 162 0 2615 0
[pid=26285] vsize: 11108
Current children cumulated CPU time (s) 1079.88
Current children cumulated vsize (Kb) 13236

[startup+1090.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2814 0 3 0 108958 27 0 0 25 0 1 0 1844032717 11374592 2540 4294967295 134512640 135167914 3221224448 3221220684 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2777 2540 162 162 0 2615 0
[pid=26285] vsize: 11108
Current children cumulated CPU time (s) 1089.88
Current children cumulated vsize (Kb) 13236

[startup+1100.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2814 0 3 0 109958 27 0 0 25 0 1 0 1844032717 11374592 2540 4294967295 134512640 135167914 3221224448 3221221376 134844682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2777 2540 162 162 0 2615 0
[pid=26285] vsize: 11108
Current children cumulated CPU time (s) 1099.88
Current children cumulated vsize (Kb) 13236

[startup+1110.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2814 0 3 0 110959 27 0 0 25 0 1 0 1844032717 11374592 2540 4294967295 134512640 135167914 3221224448 3221221632 134849187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2777 2540 162 162 0 2615 0
[pid=26285] vsize: 11108
Current children cumulated CPU time (s) 1109.89
Current children cumulated vsize (Kb) 13236

[startup+1120.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2814 0 3 0 111959 27 0 0 25 0 1 0 1844032717 11374592 2540 4294967295 134512640 135167914 3221224448 3221220560 134694377 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2777 2540 162 162 0 2615 0
[pid=26285] vsize: 11108
Current children cumulated CPU time (s) 1119.89
Current children cumulated vsize (Kb) 13236

[startup+1130.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2814 0 3 0 112959 27 0 0 25 0 1 0 1844032717 11374592 2540 4294967295 134512640 135167914 3221224448 3221221388 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2777 2540 162 162 0 2615 0
[pid=26285] vsize: 11108
Current children cumulated CPU time (s) 1129.89
Current children cumulated vsize (Kb) 13236

[startup+1140.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2814 0 3 0 113959 27 0 0 25 0 1 0 1844032717 11374592 2540 4294967295 134512640 135167914 3221224448 3221221728 134844731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2777 2540 162 162 0 2615 0
[pid=26285] vsize: 11108
Current children cumulated CPU time (s) 1139.89
Current children cumulated vsize (Kb) 13236

[startup+1150.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2814 0 3 0 114959 28 0 0 25 0 1 0 1844032717 11374592 2540 4294967295 134512640 135167914 3221224448 3221219264 134696380 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2777 2540 162 162 0 2615 0
[pid=26285] vsize: 11108
Current children cumulated CPU time (s) 1149.9
Current children cumulated vsize (Kb) 13236

[startup+1160.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2814 0 3 0 115959 28 0 0 25 0 1 0 1844032717 11374592 2540 4294967295 134512640 135167914 3221224448 3221221248 134722532 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2777 2540 162 162 0 2615 0
[pid=26285] vsize: 11108
Current children cumulated CPU time (s) 1159.9
Current children cumulated vsize (Kb) 13236

[startup+1170.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2814 0 3 0 116960 28 0 0 25 0 1 0 1844032717 11374592 2540 4294967295 134512640 135167914 3221224448 3221221828 134629209 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2777 2540 162 162 0 2615 0
[pid=26285] vsize: 11108
Current children cumulated CPU time (s) 1169.91
Current children cumulated vsize (Kb) 13236

[startup+1180.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2814 0 3 0 117959 29 0 0 25 0 1 0 1844032717 11374592 2540 4294967295 134512640 135167914 3221224448 3221222144 134694532 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2777 2540 162 162 0 2615 0
[pid=26285] vsize: 11108
Current children cumulated CPU time (s) 1179.91
Current children cumulated vsize (Kb) 13236

[startup+1190.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2860 0 3 0 118958 29 0 0 25 0 1 0 1844032717 11051008 2484 4294967295 134512640 135167914 3221224448 3221219116 134843033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2698 2484 162 162 0 2536 0
[pid=26285] vsize: 10792
Current children cumulated CPU time (s) 1189.9
Current children cumulated vsize (Kb) 12920

[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2887 0 3 0 119958 30 0 0 25 0 1 0 1844032717 11030528 2479 4294967295 134512640 135167914 3221224448 3221218904 134718503 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2693 2479 162 162 0 2531 0
[pid=26285] vsize: 10772
Current children cumulated CPU time (s) 1199.91
Current children cumulated vsize (Kb) 12900

[startup+1210.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2887 0 3 0 120958 30 0 0 25 0 1 0 1844032717 11030528 2479 4294967295 134512640 135167914 3221224448 3221220540 134845876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2693 2479 162 162 0 2531 0
[pid=26285] vsize: 10772
Current children cumulated CPU time (s) 1209.91
Current children cumulated vsize (Kb) 12900



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26285
Raw data (/proc/26280/stat): 26280 (minisat+_script) S 26279 26280 16528 0 -1 0 314 362 0 0 0 1 1 1 21 0 1 0 1844032709 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26280/statm): 532 234 485 147 0 385 0
[pid=26280] vsize: 2128
Raw data (/proc/26285/stat): 26285 (minisat+_bignum) R 26280 26280 16528 0 -1 0 2887 0 3 0 120958 30 0 0 25 0 1 0 1844032717 11030528 2479 4294967295 134512640 135167914 3221224448 3221220236 134849056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26285/statm): 2693 2479 162 162 0 2531 0
[pid=26285] vsize: 10772
Current children cumulated CPU time (s) 1209.91
Current children cumulated vsize (Kb) 12900

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

Child status: 0
Real time (s): 1210.08
CPU time (s): 1209.9
CPU user time (s): 1209.59
CPU system time (s): 0.312952
CPU usage (%): 99.9853
Max. virtual memory (cumulated for all children) (Kb): 13236

Verifier Data

ERROR: no interpretation found !