Some explanations

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

General information on the benchmark

Namemps-v2-13-7/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-lotfi.opb
MD5SUM69367ad5ee917e4a74e95e8f089c09d8
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 160
Biggest coefficient in the objective function 524288
Number of bits for the biggest coefficient in the objective function 20
Sum of the numbers in the objective function 8388600
Number of bits of the sum of numbers in the objective function 23
Biggest number in a constraint 5242880000000000
Number of bits of the biggest number in a constraint 53
Biggest sum of numbers in a constraint 39992649862466400
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 variables6160
Total number of constraints153
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 constraints153
Minimum length of a constraint20
Maximum length of a constraint2660

Trace number 6030

Launcher Data

LAUNCH ON wulflinc5 THE 2005-09-20 02:50:31 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3169 boxname=wulflinc5 idbench=825 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  69367ad5ee917e4a74e95e8f089c09d8  /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-lotfi.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-lotfi.opb
IDLAUNCH: 3169
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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	: 2
cpu MHz		: 451.007
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        884848 kB
Buffers:         23516 kB
Cached:         101000 kB
SwapCached:        740 kB
Active:          31448 kB
Inactive:        95808 kB
HighTotal:      131008 kB
HighFree:        31052 kB
LowTotal:       903652 kB
LowFree:        853796 kB
SwapTotal:     2097136 kB
SwapFree:      2095892 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5804 kB
Slab:            16772 kB
Committed_AS:    64300 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 03:03:20 (client local time) WITH STATUS 0 IN 752.247 SECONDS
stats: 3169 7 752.247 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 356] 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/24681/stat): 24681 (minisat+_script) R 24680 24681 824 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1796848080 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/24681/statm): 174 3 169 147 0 27 0
[pid=24681] 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=24682
New process pid=24683
New process pid=24684
execve syscall for /bin/sed executable
One traced child (pid=24683) 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=24684) exited with status: 0
One traced child (pid=24682) exited with status: 0
New process pid=24685
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-lotfi.opb
One traced child (pid=24685) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=24686
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-lotfi.opb

[startup+10.004 s]
Raw data (loadavg): 0.87 0.94 0.96 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 1209 0 0 0 975 6 0 0 25 0 1 0 1796848093 4706304 1039 4294967295 134512640 135167914 3221224448 3221221112 134693553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24686/statm): 1149 1039 162 162 0 987 0
[pid=24686] vsize: 4596
Current children cumulated CPU time (s) 9.88
Current children cumulated vsize (Kb) 6724

[startup+20.0048 s]
Raw data (loadavg): 0.89 0.94 0.96 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 2026 0 0 0 1970 8 0 0 25 0 1 0 1796848093 8155136 1814 4294967295 134512640 135167914 3221224448 3220724448 134844715 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24686/statm): 1991 1814 162 162 0 1829 0
[pid=24686] vsize: 7964
Current children cumulated CPU time (s) 19.85
Current children cumulated vsize (Kb) 10092

[startup+30.0065 s]
Raw data (loadavg): 0.91 0.94 0.96 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 2549 0 0 0 2966 9 0 0 25 0 1 0 1796848093 9330688 2129 4294967295 134512640 135167914 3221224448 3221220032 134849148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24686/statm): 2278 2129 162 162 0 2116 0
[pid=24686] vsize: 9112
Current children cumulated CPU time (s) 29.82
Current children cumulated vsize (Kb) 11240

[startup+40.0072 s]
Raw data (loadavg): 0.92 0.94 0.96 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 2549 0 0 0 3966 10 0 0 25 0 1 0 1796848093 9330688 2129 4294967295 134512640 135167914 3221224448 3221219792 134844700 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24686/statm): 2278 2129 162 162 0 2116 0
[pid=24686] vsize: 9112
Current children cumulated CPU time (s) 39.83
Current children cumulated vsize (Kb) 11240

[startup+50.008 s]
Raw data (loadavg): 0.93 0.95 0.96 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 2549 0 0 0 4966 10 0 0 25 0 1 0 1796848093 9330688 2129 4294967295 134512640 135167914 3221224448 3221220304 134843118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24686/statm): 2278 2129 162 162 0 2116 0
[pid=24686] vsize: 9112
Current children cumulated CPU time (s) 49.83
Current children cumulated vsize (Kb) 11240

[startup+60.0087 s]
Raw data (loadavg): 0.94 0.95 0.96 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 2549 0 0 0 5967 10 0 0 25 0 1 0 1796848093 9330688 2129 4294967295 134512640 135167914 3221224448 3221220384 134843406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24686/statm): 2278 2129 162 162 0 2116 0
[pid=24686] vsize: 9112
Current children cumulated CPU time (s) 59.84
Current children cumulated vsize (Kb) 11240

[startup+70.0095 s]
Raw data (loadavg): 0.95 0.95 0.96 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 2549 0 0 0 6967 10 0 0 25 0 1 0 1796848093 9330688 2129 4294967295 134512640 135167914 3221224448 3221220340 134843000 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24686/statm): 2278 2129 162 162 0 2116 0
[pid=24686] vsize: 9112
Current children cumulated CPU time (s) 69.84
Current children cumulated vsize (Kb) 11240

[startup+80.0102 s]
Raw data (loadavg): 0.96 0.95 0.96 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 2549 0 0 0 7967 10 0 0 25 0 1 0 1796848093 9330688 2129 4294967295 134512640 135167914 3221224448 3221220540 134844632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24686/statm): 2278 2129 162 162 0 2116 0
[pid=24686] vsize: 9112
Current children cumulated CPU time (s) 79.84
Current children cumulated vsize (Kb) 11240

[startup+90.0109 s]
Raw data (loadavg): 0.96 0.95 0.96 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 2549 0 0 0 8968 10 0 0 25 0 1 0 1796848093 9330688 2129 4294967295 134512640 135167914 3221224448 3221220000 134720495 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24686/statm): 2278 2129 162 162 0 2116 0
[pid=24686] vsize: 9112
Current children cumulated CPU time (s) 89.85
Current children cumulated vsize (Kb) 11240

[startup+100.013 s]
Raw data (loadavg): 0.97 0.95 0.96 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 2549 0 0 0 9968 10 0 0 25 0 1 0 1796848093 9330688 2129 4294967295 134512640 135167914 3221224448 3221221464 134842997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24686/statm): 2278 2129 162 162 0 2116 0
[pid=24686] vsize: 9112
Current children cumulated CPU time (s) 99.85
Current children cumulated vsize (Kb) 11240

[startup+110.013 s]
Raw data (loadavg): 0.97 0.95 0.96 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 2549 0 0 0 10968 10 0 0 25 0 1 0 1796848093 9330688 2129 4294967295 134512640 135167914 3221224448 3221221064 134845877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24686/statm): 2278 2129 162 162 0 2116 0
[pid=24686] vsize: 9112
Current children cumulated CPU time (s) 109.85
Current children cumulated vsize (Kb) 11240

[startup+120.014 s]
Raw data (loadavg): 0.98 0.95 0.96 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 2549 0 0 0 11968 10 0 0 25 0 1 0 1796848093 9330688 2129 4294967295 134512640 135167914 3221224448 3221221264 134849187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24686/statm): 2278 2129 162 162 0 2116 0
[pid=24686] vsize: 9112
Current children cumulated CPU time (s) 119.85
Current children cumulated vsize (Kb) 11240

[startup+130.015 s]
Raw data (loadavg): 0.98 0.95 0.96 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 2549 0 0 0 12969 10 0 0 25 0 1 0 1796848093 9330688 2129 4294967295 134512640 135167914 3221224448 3221220672 134844718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24686/statm): 2278 2129 162 162 0 2116 0
[pid=24686] vsize: 9112
Current children cumulated CPU time (s) 129.86
Current children cumulated vsize (Kb) 11240

[startup+140.016 s]
Raw data (loadavg): 0.98 0.95 0.96 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 2549 0 0 0 13969 10 0 0 25 0 1 0 1796848093 9330688 2129 4294967295 134512640 135167914 3221224448 3221221248 134522821 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24686/statm): 2278 2129 162 162 0 2116 0
[pid=24686] vsize: 9112
Current children cumulated CPU time (s) 139.86
Current children cumulated vsize (Kb) 11240

[startup+150.016 s]
Raw data (loadavg): 0.98 0.95 0.96 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 2549 0 0 0 14969 10 0 0 25 0 1 0 1796848093 9330688 2129 4294967295 134512640 135167914 3221224448 3221219568 134844644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24686/statm): 2278 2129 162 162 0 2116 0
[pid=24686] vsize: 9112
Current children cumulated CPU time (s) 149.86
Current children cumulated vsize (Kb) 11240

[startup+160.017 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 2549 0 0 0 15969 10 0 0 25 0 1 0 1796848093 9330688 2129 4294967295 134512640 135167914 3221224448 3221221664 134629451 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24686/statm): 2278 2129 162 162 0 2116 0
[pid=24686] vsize: 9112
Current children cumulated CPU time (s) 159.86
Current children cumulated vsize (Kb) 11240

[startup+170.017 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 2549 0 0 0 16969 10 0 0 25 0 1 0 1796848093 9330688 2129 4294967295 134512640 135167914 3221224448 3221221376 134844708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24686/statm): 2278 2129 162 162 0 2116 0
[pid=24686] vsize: 9112
Current children cumulated CPU time (s) 169.86
Current children cumulated vsize (Kb) 11240

[startup+180.018 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 2549 0 0 0 17970 10 0 0 25 0 1 0 1796848093 9330688 2129 4294967295 134512640 135167914 3221224448 3221222460 134693643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24686/statm): 2278 2129 162 162 0 2116 0
[pid=24686] vsize: 9112
Current children cumulated CPU time (s) 179.87
Current children cumulated vsize (Kb) 11240

[startup+190.018 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 2549 0 0 0 18970 10 0 0 25 0 1 0 1796848093 9330688 2129 4294967295 134512640 135167914 3221224448 3221220752 134849179 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24686/statm): 2278 2129 162 162 0 2116 0
[pid=24686] vsize: 9112
Current children cumulated CPU time (s) 189.87
Current children cumulated vsize (Kb) 11240

[startup+200.018 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 2549 0 0 0 19970 10 0 0 25 0 1 0 1796848093 9330688 2129 4294967295 134512640 135167914 3221224448 3221221388 134723262 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24686/statm): 2278 2129 162 162 0 2116 0
[pid=24686] vsize: 9112
Current children cumulated CPU time (s) 199.87
Current children cumulated vsize (Kb) 11240

[startup+210.019 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 2549 0 0 0 20970 10 0 0 25 0 1 0 1796848093 9330688 2129 4294967295 134512640 135167914 3221224448 3221222080 134843139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24686/statm): 2278 2129 162 162 0 2116 0
[pid=24686] vsize: 9112
Current children cumulated CPU time (s) 209.87
Current children cumulated vsize (Kb) 11240

[startup+220.02 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 2549 0 0 0 21971 10 0 0 25 0 1 0 1796848093 9330688 2129 4294967295 134512640 135167914 3221224448 3221220080 134844653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24686/statm): 2278 2129 162 162 0 2116 0
[pid=24686] vsize: 9112
Current children cumulated CPU time (s) 219.88
Current children cumulated vsize (Kb) 11240

[startup+230.02 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 2549 0 0 0 22971 10 0 0 25 0 1 0 1796848093 9330688 2129 4294967295 134512640 135167914 3221224448 3221221104 134849196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24686/statm): 2278 2129 162 162 0 2116 0
[pid=24686] vsize: 9112
Current children cumulated CPU time (s) 229.88
Current children cumulated vsize (Kb) 11240

[startup+240.021 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 2549 0 0 0 23971 10 0 0 25 0 1 0 1796848093 9330688 2129 4294967295 134512640 135167914 3221224448 3221221744 134843404 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24686/statm): 2278 2129 162 162 0 2116 0
[pid=24686] vsize: 9112
Current children cumulated CPU time (s) 239.88
Current children cumulated vsize (Kb) 11240

[startup+250.021 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 2549 0 0 0 24971 10 0 0 25 0 1 0 1796848093 9330688 2129 4294967295 134512640 135167914 3221224448 3221221712 134843123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24686/statm): 2278 2129 162 162 0 2116 0
[pid=24686] vsize: 9112
Current children cumulated CPU time (s) 249.88
Current children cumulated vsize (Kb) 11240

[startup+260.021 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 2549 0 0 0 25971 10 0 0 25 0 1 0 1796848093 9330688 2129 4294967295 134512640 135167914 3221224448 3221220448 134845911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24686/statm): 2278 2129 162 162 0 2116 0
[pid=24686] vsize: 9112
Current children cumulated CPU time (s) 259.88
Current children cumulated vsize (Kb) 11240

[startup+270.021 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 2549 0 0 0 26972 10 0 0 25 0 1 0 1796848093 9330688 2129 4294967295 134512640 135167914 3221224448 3221221376 134845901 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24686/statm): 2278 2129 162 162 0 2116 0
[pid=24686] vsize: 9112
Current children cumulated CPU time (s) 269.89
Current children cumulated vsize (Kb) 11240

[startup+280.022 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 2549 0 0 0 27972 10 0 0 25 0 1 0 1796848093 9330688 2129 4294967295 134512640 135167914 3221224448 3221221472 134629069 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24686/statm): 2278 2129 162 162 0 2116 0
[pid=24686] vsize: 9112
Current children cumulated CPU time (s) 279.89
Current children cumulated vsize (Kb) 11240

[startup+290.023 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 2549 0 0 0 28972 10 0 0 25 0 1 0 1796848093 9330688 2129 4294967295 134512640 135167914 3221224448 3221222112 134722521 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24686/statm): 2278 2129 162 162 0 2116 0
[pid=24686] vsize: 9112
Current children cumulated CPU time (s) 289.89
Current children cumulated vsize (Kb) 11240

[startup+300.022 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 2549 0 0 0 29972 10 0 0 25 0 1 0 1796848093 9330688 2129 4294967295 134512640 135167914 3221224448 3221222608 134844691 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24686/statm): 2278 2129 162 162 0 2116 0
[pid=24686] vsize: 9112
Current children cumulated CPU time (s) 299.89
Current children cumulated vsize (Kb) 11240

[startup+310.023 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) T 24681 24681 824 0 -1 0 7393 0 0 0 30944 26 0 0 25 0 1 0 1796848093 25198592 5858 4294967295 134512640 135167914 3221224448 3221168220 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/24686/statm): 6152 5858 162 162 0 5990 0
[pid=24686] vsize: 24608
Current children cumulated CPU time (s) 309.77
Current children cumulated vsize (Kb) 26736

[startup+320.023 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 12784 0 0 0 31898 45 0 0 25 0 1 0 1796848093 44580864 10590 4294967295 134512640 135167914 3221224448 3221168352 134843064 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24686/statm): 10884 10590 162 162 0 10722 0
[pid=24686] vsize: 43536
Current children cumulated CPU time (s) 319.5
Current children cumulated vsize (Kb) 45664

[startup+330.024 s]
Raw data (loadavg): 0.99 0.97 0.96 1/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) T 24681 24681 824 0 -1 0 19261 0 0 0 32847 71 0 0 25 0 1 0 1796848093 65712128 15749 4294967295 134512640 135167914 3221224448 3221174940 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/24686/statm): 16043 15749 162 162 0 15881 0
[pid=24686] vsize: 64172
Current children cumulated CPU time (s) 329.25
Current children cumulated vsize (Kb) 66300

[startup+340.024 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 23397 0 0 0 33803 90 0 0 25 0 1 0 1796848093 82653184 19885 4294967295 134512640 135167914 3221224448 3221173760 134620493 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24686/statm): 20179 19885 162 162 0 20017 0
[pid=24686] vsize: 80716
Current children cumulated CPU time (s) 339
Current children cumulated vsize (Kb) 82844

[startup+350.024 s]
Raw data (loadavg): 0.99 0.97 0.96 1/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) T 24681 24681 824 0 -1 0 32076 0 0 0 34752 119 0 0 25 0 1 0 1796848093 107401216 25927 4294967295 134512640 135167914 3221224448 3221168092 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/24686/statm): 26221 25927 162 162 0 26059 0
[pid=24686] vsize: 104884
Current children cumulated CPU time (s) 348.78
Current children cumulated vsize (Kb) 107012

[startup+360.025 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 36486 0 0 0 35703 141 0 0 25 0 1 0 1796848093 125464576 30337 4294967295 134512640 135167914 3221224448 3221175552 134620627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24686/statm): 30631 30337 162 162 0 30469 0
[pid=24686] vsize: 122524
Current children cumulated CPU time (s) 358.51
Current children cumulated vsize (Kb) 124652

[startup+370.025 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 40893 0 0 0 36655 163 0 0 25 0 1 0 1796848093 143515648 34744 4294967295 134512640 135167914 3221224448 3221172320 134844668 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24686/statm): 35038 34744 162 162 0 34876 0
[pid=24686] vsize: 140152
Current children cumulated CPU time (s) 368.25
Current children cumulated vsize (Kb) 142280

[startup+380.025 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 45142 0 0 0 37606 183 0 0 25 0 1 0 1796848093 160919552 38993 4294967295 134512640 135167914 3221224448 3221169616 134845921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24686/statm): 39287 38993 162 162 0 39125 0
[pid=24686] vsize: 157148
Current children cumulated CPU time (s) 377.96
Current children cumulated vsize (Kb) 159276

[startup+390.026 s]
Raw data (loadavg): 1.07 0.99 0.97 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) T 24681 24681 824 0 -1 0 58200 0 0 0 38553 220 0 0 25 0 1 0 1796848093 192806912 46778 4294967295 134512640 135167914 3221224448 3221174188 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/24686/statm): 47072 46778 162 162 0 46910 0
[pid=24686] vsize: 188288
Current children cumulated CPU time (s) 387.8
Current children cumulated vsize (Kb) 190416

[startup+400.026 s]
Raw data (loadavg): 1.06 0.99 0.97 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 62535 0 0 0 39505 241 0 0 25 0 1 0 1796848093 210563072 51113 4294967295 134512640 135167914 3221224448 3221181968 134623978 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24686/statm): 51407 51113 162 162 0 51245 0
[pid=24686] vsize: 205628
Current children cumulated CPU time (s) 397.53
Current children cumulated vsize (Kb) 207756

[startup+410.027 s]
Raw data (loadavg): 1.05 0.99 0.97 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) T 24681 24681 824 0 -1 0 66982 0 0 0 40456 262 0 0 25 0 1 0 1796848093 228777984 55560 4294967295 134512640 135167914 3221224448 3221168860 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/24686/statm): 55854 55560 162 162 0 55692 0
[pid=24686] vsize: 223416
Current children cumulated CPU time (s) 407.25
Current children cumulated vsize (Kb) 225544

[startup+420.026 s]
Raw data (loadavg): 1.04 0.99 0.97 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) T 24681 24681 824 0 -1 0 71312 0 0 0 41407 282 0 0 25 0 1 0 1796848093 246513664 59890 4294967295 134512640 135167914 3221224448 3221172732 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/24686/statm): 60184 59890 162 162 0 60022 0
[pid=24686] vsize: 240736
Current children cumulated CPU time (s) 416.96
Current children cumulated vsize (Kb) 242864

[startup+430.027 s]
Raw data (loadavg): 1.03 0.99 0.97 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 75680 0 0 0 42358 302 0 0 25 0 1 0 1796848093 264404992 64258 4294967295 134512640 135167914 3221224448 3221176832 134722539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24686/statm): 64552 64258 162 162 0 64390 0
[pid=24686] vsize: 258208
Current children cumulated CPU time (s) 426.67
Current children cumulated vsize (Kb) 260336

[startup+440.028 s]
Raw data (loadavg): 1.03 0.99 0.97 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 79917 0 0 0 43311 323 0 0 25 0 1 0 1796848093 281759744 68495 4294967295 134512640 135167914 3221224448 3221176128 134624231 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24686/statm): 68789 68495 162 162 0 68627 0
[pid=24686] vsize: 275156
Current children cumulated CPU time (s) 436.41
Current children cumulated vsize (Kb) 277284

[startup+450.027 s]
Raw data (loadavg): 1.02 0.99 0.97 1/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) T 24681 24681 824 0 -1 0 84172 0 0 0 44266 341 0 0 25 0 1 0 1796848093 299188224 72750 4294967295 134512640 135167914 3221224448 3221167468 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/24686/statm): 73044 72750 162 162 0 72882 0
[pid=24686] vsize: 292176
Current children cumulated CPU time (s) 446.14
Current children cumulated vsize (Kb) 294304

[startup+460.028 s]
Raw data (loadavg): 1.02 0.99 0.97 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 88464 0 0 0 45222 361 0 0 25 0 1 0 1796848093 316768256 77042 4294967295 134512640 135167914 3221224448 3221176384 134695554 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24686/statm): 77336 77042 162 162 0 77174 0
[pid=24686] vsize: 309344
Current children cumulated CPU time (s) 455.9
Current children cumulated vsize (Kb) 311472

[startup+470.029 s]
Raw data (loadavg): 1.02 0.99 0.97 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 110240 0 0 0 46164 414 0 0 25 0 1 0 1796848093 362766336 88272 4294967295 134512640 135167914 3221224448 3221176032 134845901 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24686/statm): 88566 88272 162 162 0 88404 0
[pid=24686] vsize: 354264
Current children cumulated CPU time (s) 465.85
Current children cumulated vsize (Kb) 356392

[startup+480.03 s]
Raw data (loadavg): 1.01 0.99 0.97 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 114593 0 0 0 47112 436 0 0 25 0 1 0 1796848093 380596224 92625 4294967295 134512640 135167914 3221224448 3221169496 134522360 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24686/statm): 92919 92625 162 162 0 92757 0
[pid=24686] vsize: 371676
Current children cumulated CPU time (s) 475.55
Current children cumulated vsize (Kb) 373804

[startup+490.03 s]
Raw data (loadavg): 1.01 0.99 0.97 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 118970 0 0 0 48065 454 0 0 25 0 1 0 1796848093 398524416 97002 4294967295 134512640 135167914 3221224448 3221167776 134844697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24686/statm): 97296 97002 162 162 0 97134 0
[pid=24686] vsize: 389184
Current children cumulated CPU time (s) 485.26
Current children cumulated vsize (Kb) 391312

[startup+500.031 s]
Raw data (loadavg): 1.01 0.99 0.97 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) T 24681 24681 824 0 -1 0 123327 0 0 0 49016 474 0 0 25 0 1 0 1796848093 416370688 101359 4294967295 134512640 135167914 3221224448 3221171996 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/24686/statm): 101653 101359 162 162 0 101491 0
[pid=24686] vsize: 406612
Current children cumulated CPU time (s) 494.97
Current children cumulated vsize (Kb) 408740

[startup+510.032 s]
Raw data (loadavg): 1.01 0.99 0.97 1/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) T 24681 24681 824 0 -1 0 127643 0 0 0 49966 497 0 0 25 0 1 0 1796848093 434049024 105675 4294967295 134512640 135167914 3221224448 3221179772 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/24686/statm): 105969 105675 162 162 0 105807 0
[pid=24686] vsize: 423876
Current children cumulated CPU time (s) 504.7
Current children cumulated vsize (Kb) 426004

[startup+520.033 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 131918 0 0 0 50918 517 0 0 25 0 1 0 1796848093 451559424 109950 4294967295 134512640 135167914 3221224448 3221175328 134619185 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24686/statm): 110244 109950 162 162 0 110082 0
[pid=24686] vsize: 440976
Current children cumulated CPU time (s) 514.42
Current children cumulated vsize (Kb) 443104

[startup+530.033 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) T 24681 24681 824 0 -1 0 136290 0 0 0 51868 540 0 0 25 0 1 0 1796848093 469467136 114322 4294967295 134512640 135167914 3221224448 3221173724 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/24686/statm): 114616 114322 162 162 0 114454 0
[pid=24686] vsize: 458464
Current children cumulated CPU time (s) 524.15
Current children cumulated vsize (Kb) 460592

[startup+540.034 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 140536 0 0 0 52822 558 0 0 25 0 1 0 1796848093 486858752 118568 4294967295 134512640 135167914 3221224448 3221172224 134843026 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24686/statm): 118862 118568 162 162 0 118700 0
[pid=24686] vsize: 475448
Current children cumulated CPU time (s) 533.87
Current children cumulated vsize (Kb) 477576

[startup+550.034 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 144807 0 0 0 53774 577 0 0 25 0 1 0 1796848093 504352768 122839 4294967295 134512640 135167914 3221224448 3221171872 134843036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24686/statm): 123133 122839 162 162 0 122971 0
[pid=24686] vsize: 492532
Current children cumulated CPU time (s) 543.58
Current children cumulated vsize (Kb) 494660

[startup+560.035 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 149081 0 0 0 54724 599 0 0 25 0 1 0 1796848093 521859072 127113 4294967295 134512640 135167914 3221224448 3221179040 134695145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24686/statm): 127407 127113 162 162 0 127245 0
[pid=24686] vsize: 509628
Current children cumulated CPU time (s) 553.3
Current children cumulated vsize (Kb) 511756

[startup+570.035 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 153302 0 0 0 55679 619 0 0 25 0 1 0 1796848093 539148288 131334 4294967295 134512640 135167914 3221224448 3221170400 134847159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24686/statm): 131628 131334 162 162 0 131466 0
[pid=24686] vsize: 526512
Current children cumulated CPU time (s) 563.05
Current children cumulated vsize (Kb) 528640

[startup+580.036 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 157574 0 0 0 56631 640 0 0 25 0 1 0 1796848093 556646400 135606 4294967295 134512640 135167914 3221224448 3221174208 134620509 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24686/statm): 135900 135606 162 162 0 135738 0
[pid=24686] vsize: 543600
Current children cumulated CPU time (s) 572.78
Current children cumulated vsize (Kb) 545728

[startup+590.037 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 161798 0 0 0 57587 657 0 0 25 0 1 0 1796848093 573952000 139830 4294967295 134512640 135167914 3221224448 3221181212 134934490 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24686/statm): 140125 139830 162 162 0 139963 0
[pid=24686] vsize: 560500
Current children cumulated CPU time (s) 582.51
Current children cumulated vsize (Kb) 562628

[startup+600.037 s]
Raw data (loadavg): 1.00 0.99 0.97 1/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) T 24681 24681 824 0 -1 0 166044 0 0 0 58539 677 0 0 25 0 1 0 1796848093 591339520 144076 4294967295 134512640 135167914 3221224448 3221176604 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/24686/statm): 144370 144076 162 162 0 144208 0
[pid=24686] vsize: 577480
Current children cumulated CPU time (s) 592.23
Current children cumulated vsize (Kb) 579608

[startup+610.037 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 170302 0 0 0 59490 700 0 0 25 0 1 0 1796848093 608780288 148334 4294967295 134512640 135167914 3221224448 3221184720 134849092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24686/statm): 148628 148334 162 162 0 148466 0
[pid=24686] vsize: 594512
Current children cumulated CPU time (s) 601.97
Current children cumulated vsize (Kb) 596640

[startup+620.037 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 215626 0 0 0 60357 811 0 0 25 0 1 0 1796848093 794427392 193658 4294967295 134512640 135167914 3221224448 3221167936 134625515 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24686/statm): 193952 193658 162 162 0 193790 0
[pid=24686] vsize: 775808
Current children cumulated CPU time (s) 611.75
Current children cumulated vsize (Kb) 777936

[startup+630.039 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 215626 0 0 0 61358 811 0 0 25 0 1 0 1796848093 794427392 193658 4294967295 134512640 135167914 3221224448 3221167792 134845921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24686/statm): 193952 193658 162 162 0 193790 0
[pid=24686] vsize: 775808
Current children cumulated CPU time (s) 621.76
Current children cumulated vsize (Kb) 777936

[startup+640.039 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 218332 0 0 0 62324 828 0 0 25 0 1 0 1796848093 719122432 175273 4294967295 134512640 135167914 3221224448 3221171008 134695548 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24686/statm): 175567 175273 162 162 0 175405 0
[pid=24686] vsize: 702268
Current children cumulated CPU time (s) 631.59
Current children cumulated vsize (Kb) 704396

[startup+650.039 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 222670 0 0 0 63277 848 0 0 25 0 1 0 1796848093 736890880 179611 4294967295 134512640 135167914 3221224448 3221179060 134697403 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24686/statm): 179905 179611 162 162 0 179743 0
[pid=24686] vsize: 719620
Current children cumulated CPU time (s) 641.32
Current children cumulated vsize (Kb) 721748

[startup+660.04 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 227074 0 0 0 64225 869 0 0 25 0 1 0 1796848093 754929664 184015 4294967295 134512640 135167914 3221224448 3221171276 134849088 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24686/statm): 184309 184015 162 162 0 184147 0
[pid=24686] vsize: 737236
Current children cumulated CPU time (s) 651.01
Current children cumulated vsize (Kb) 739364

[startup+670.041 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) T 24681 24681 824 0 -1 0 231416 0 0 0 65176 889 0 0 25 0 1 0 1796848093 772714496 188357 4294967295 134512640 135167914 3221224448 3221180988 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/24686/statm): 188651 188357 162 162 0 188489 0
[pid=24686] vsize: 754604
Current children cumulated CPU time (s) 660.72
Current children cumulated vsize (Kb) 756732

[startup+680.042 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 235772 0 0 0 66128 909 0 0 25 0 1 0 1796848093 790556672 192713 4294967295 134512640 135167914 3221224448 3221173948 134722225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24686/statm): 193007 192713 162 162 0 192845 0
[pid=24686] vsize: 772028
Current children cumulated CPU time (s) 670.44
Current children cumulated vsize (Kb) 774156

[startup+690.042 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) T 24681 24681 824 0 -1 0 240213 0 0 0 67080 930 0 0 25 0 1 0 1796848093 808747008 197154 4294967295 134512640 135167914 3221224448 3221171676 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/24686/statm): 197448 197154 162 162 0 197286 0
[pid=24686] vsize: 789792
Current children cumulated CPU time (s) 680.17
Current children cumulated vsize (Kb) 791920

[startup+700.042 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 244682 0 0 0 68027 952 0 0 25 0 1 0 1796848093 827052032 201623 4294967295 134512640 135167914 3221224448 3221171648 134622326 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24686/statm): 201917 201623 162 162 0 201755 0
[pid=24686] vsize: 807668
Current children cumulated CPU time (s) 689.86
Current children cumulated vsize (Kb) 809796

[startup+710.043 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) T 24681 24681 824 0 -1 0 249152 0 0 0 68976 973 0 0 25 0 1 0 1796848093 845361152 206093 4294967295 134512640 135167914 3221224448 3221173068 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/24686/statm): 206387 206093 162 162 0 206225 0
[pid=24686] vsize: 825548
Current children cumulated CPU time (s) 699.56
Current children cumulated vsize (Kb) 827676

[startup+720.042 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 253596 0 0 0 69926 993 0 0 25 0 1 0 1796848093 863563776 210537 4294967295 134512640 135167914 3221224448 3221172344 134843032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24686/statm): 210831 210537 162 162 0 210669 0
[pid=24686] vsize: 843324
Current children cumulated CPU time (s) 709.26
Current children cumulated vsize (Kb) 845452

[startup+730.043 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 258039 0 0 0 70879 1014 0 0 25 0 1 0 1796848093 881762304 214980 4294967295 134512640 135167914 3221224448 3221170548 134697279 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24686/statm): 215274 214980 162 162 0 215112 0
[pid=24686] vsize: 861096
Current children cumulated CPU time (s) 719
Current children cumulated vsize (Kb) 863224

[startup+740.044 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) T 24681 24681 824 0 -1 0 262433 0 0 0 71830 1033 0 0 25 0 1 0 1796848093 899760128 219374 4294967295 134512640 135167914 3221224448 3221169980 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/24686/statm): 219668 219374 162 162 0 219506 0
[pid=24686] vsize: 878672
Current children cumulated CPU time (s) 728.7
Current children cumulated vsize (Kb) 880800

[startup+750.045 s]
Raw data (loadavg): 1.00 0.99 0.97 1/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) T 24681 24681 824 0 -1 0 266814 0 34 0 72736 1056 0 0 21 0 1 0 1796848093 916611072 222878 4294967295 134512640 135167914 3221224448 3221168892 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/24686/statm): 223782 222878 162 162 0 223620 0
[pid=24686] vsize: 895128
Current children cumulated CPU time (s) 737.99
Current children cumulated vsize (Kb) 897256

[startup+760.045 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) R 24681 24681 824 0 -1 0 270842 0 136 0 73573 1078 0 0 21 0 1 0 1796848093 932118528 225334 4294967295 134512640 135167914 3221224448 3221175712 134691408 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24686/statm): 227568 225334 162 162 0 227406 0
[pid=24686] vsize: 910272
Current children cumulated CPU time (s) 746.58
Current children cumulated vsize (Kb) 912400



Mem limit exceeded: sending SIGTERM then SIGKILL

[startup+768.12 s]
Raw data (loadavg): 1.00 0.99 0.97 1/57 24686
Raw data (/proc/24681/stat): 24681 (minisat+_script) S 24680 24681 824 0 -1 0 314 582 0 0 0 0 5 2 18 0 1 0 1796848080 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24681/statm): 532 234 485 147 0 385 0
[pid=24681] vsize: 2128
Raw data (/proc/24686/stat): 24686 (minisat+_bignum) T 24681 24681 824 0 -1 0 273645 0 353 0 74086 1094 0 0 20 0 1 0 1796848093 941543424 226925 4294967295 134512640 135167914 3221224448 3221177596 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/24686/statm): 229869 226925 162 162 0 229707 0
[pid=24686] vsize: 919476
Current children cumulated CPU time (s) 751.87
Current children cumulated vsize (Kb) 921604

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

Child status: 0
Real time (s): 768.553
CPU time (s): 752.247
CPU user time (s): 740.867
CPU system time (s): 11.3793
CPU usage (%): 97.8783
Max. virtual memory (cumulated for all children) (Kb): 921604

Verifier Data

ERROR: no interpretation found !