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-scsd1.opb
MD5SUM0d161f98f04bb13a3a82ce824c7be961
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 15200
Biggest coefficient in the objective function 262144000000000
Number of bits for the biggest coefficient in the objective function 48
Sum of the numbers in the objective function 183748611699849900
Number of bits of the sum of numbers in the objective function 58
Biggest number in a constraint 262144000000000
Number of bits of the biggest number in a constraint 48
Biggest sum of numbers in a constraint 183748611699849900
Number of bits of the biggest sum of numbers58
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables15200
Total number of constraints77
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 constraints77
Minimum length of a constraint400
Maximum length of a constraint1000

Trace number 6019

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        913268 kB
Buffers:         20552 kB
Cached:          71108 kB
SwapCached:        752 kB
Active:          26940 kB
Inactive:        67300 kB
HighTotal:      131008 kB
HighFree:        57960 kB
LowTotal:       903652 kB
LowFree:        855308 kB
SwapTotal:     2097892 kB
SwapFree:      2096628 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5728 kB
Slab:            21372 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 03:01:29 (client local time) WITH STATUS 0 IN 488.692 SECONDS
stats: 3191 7 488.692 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 764] 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/27388/stat): 27388 (minisat+_script) R 27387 27388 28974 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1855070476 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/27388/statm): 174 3 169 147 0 27 0
[pid=27388] 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=27389
New process pid=27390
New process pid=27391
execve syscall for /bin/sed executable
open syscall for file /etc/ld.so.preload
One traced child (pid=27390) exited with status: 0
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=27391) exited with status: 0
One traced child (pid=27389) exited with status: 0
New process pid=27392
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-scsd1.opb
One traced child (pid=27392) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=27393
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-scsd1.opb

[startup+10.0046 s]
Raw data (loadavg): 0.90 0.97 0.91 2/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) R 27388 27388 28974 0 -1 0 3986 0 0 0 951 18 0 0 25 0 1 0 1855070483 15155200 3592 4294967295 134512640 135167914 3221224448 3221116384 134694528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27393/statm): 3700 3592 162 162 0 3538 0
[pid=27393] vsize: 14800
Current children cumulated CPU time (s) 9.7
Current children cumulated vsize (Kb) 16928

[startup+20.0054 s]
Raw data (loadavg): 0.91 0.97 0.91 2/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) R 27388 27388 28974 0 -1 0 9839 0 0 0 1903 42 0 0 25 0 1 0 1855070483 35078144 8456 4294967295 134512640 135167914 3221224448 3221116576 134696157 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27393/statm): 8564 8456 162 162 0 8402 0
[pid=27393] vsize: 34256
Current children cumulated CPU time (s) 19.46
Current children cumulated vsize (Kb) 36384

[startup+30.0062 s]
Raw data (loadavg): 0.93 0.97 0.91 2/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) R 27388 27388 28974 0 -1 0 15855 0 0 0 2858 65 0 0 25 0 1 0 1855070483 54321152 13154 4294967295 134512640 135167914 3221224448 3221118096 134843030 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27393/statm): 13262 13154 162 162 0 13100 0
[pid=27393] vsize: 53048
Current children cumulated CPU time (s) 29.24
Current children cumulated vsize (Kb) 55176

[startup+40.007 s]
Raw data (loadavg): 0.94 0.97 0.91 1/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) T 27388 27388 28974 0 -1 0 20007 0 0 0 3816 84 0 0 25 0 1 0 1855070483 71327744 17306 4294967295 134512640 135167914 3221224448 3221117372 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/27393/statm): 17414 17306 162 162 0 17252 0
[pid=27393] vsize: 69656
Current children cumulated CPU time (s) 39.01
Current children cumulated vsize (Kb) 71784

[startup+50.0089 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) R 27388 27388 28974 0 -1 0 28738 0 0 0 4765 112 0 0 25 0 1 0 1855070483 107089920 26037 4294967295 134512640 135167914 3221224448 3221116416 134625423 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27393/statm): 26145 26037 162 162 0 25983 0
[pid=27393] vsize: 104580
Current children cumulated CPU time (s) 48.78
Current children cumulated vsize (Kb) 106708

[startup+60.0097 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) T 27388 27388 28974 0 -1 0 32421 0 0 0 5724 129 0 0 25 0 1 0 1855070483 111374336 27083 4294967295 134512640 135167914 3221224448 3221115676 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/27393/statm): 27191 27083 162 162 0 27029 0
[pid=27393] vsize: 108764
Current children cumulated CPU time (s) 58.54
Current children cumulated vsize (Kb) 110892

[startup+70.0105 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) R 27388 27388 28974 0 -1 0 36543 0 0 0 6679 146 0 0 25 0 1 0 1855070483 128258048 31205 4294967295 134512640 135167914 3221224448 3221120540 134722229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27393/statm): 31313 31205 162 162 0 31151 0
[pid=27393] vsize: 125252
Current children cumulated CPU time (s) 68.26
Current children cumulated vsize (Kb) 127380

[startup+80.0113 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) R 27388 27388 28974 0 -1 0 40558 0 0 0 7636 164 0 0 25 0 1 0 1855070483 144703488 35220 4294967295 134512640 135167914 3221224448 3221117536 134847261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27393/statm): 35328 35220 162 162 0 35166 0
[pid=27393] vsize: 141312
Current children cumulated CPU time (s) 78.01
Current children cumulated vsize (Kb) 143440

[startup+90.0121 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) R 27388 27388 28974 0 -1 0 44623 0 0 0 8591 182 0 0 25 0 1 0 1855070483 161353728 39285 4294967295 134512640 135167914 3221224448 3221116896 134847203 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27393/statm): 39393 39285 162 162 0 39231 0
[pid=27393] vsize: 157572
Current children cumulated CPU time (s) 87.74
Current children cumulated vsize (Kb) 159700

[startup+100.012 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) R 27388 27388 28974 0 -1 0 57491 0 0 0 9541 218 0 0 25 0 1 0 1855070483 192462848 46880 4294967295 134512640 135167914 3221224448 3221115520 134847175 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27393/statm): 46988 46880 162 162 0 46826 0
[pid=27393] vsize: 187952
Current children cumulated CPU time (s) 97.6
Current children cumulated vsize (Kb) 190080

[startup+110.014 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) R 27388 27388 28974 0 -1 0 61492 0 0 0 10492 239 0 0 25 0 1 0 1855070483 208850944 50881 4294967295 134512640 135167914 3221224448 3221117728 134849061 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27393/statm): 50989 50881 162 162 0 50827 0
[pid=27393] vsize: 203956
Current children cumulated CPU time (s) 107.32
Current children cumulated vsize (Kb) 206084

[startup+120.015 s]
Raw data (loadavg): 1.16 1.02 0.93 2/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) R 27388 27388 28974 0 -1 0 65461 0 0 0 11448 257 0 0 25 0 1 0 1855070483 225107968 54850 4294967295 134512640 135167914 3221224448 3221116732 134722229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27393/statm): 54958 54850 162 162 0 54796 0
[pid=27393] vsize: 219832
Current children cumulated CPU time (s) 117.06
Current children cumulated vsize (Kb) 221960

[startup+130.014 s]
Raw data (loadavg): 1.13 1.02 0.93 2/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) R 27388 27388 28974 0 -1 0 69350 0 0 0 12408 274 0 0 25 0 1 0 1855070483 241037312 58739 4294967295 134512640 135167914 3221224448 3221117816 134845939 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27393/statm): 58847 58739 162 162 0 58685 0
[pid=27393] vsize: 235388
Current children cumulated CPU time (s) 126.83
Current children cumulated vsize (Kb) 237516

[startup+140.015 s]
Raw data (loadavg): 1.11 1.02 0.93 2/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) T 27388 27388 28974 0 -1 0 73503 0 0 0 13363 295 0 0 25 0 1 0 1855070483 258052096 62892 4294967295 134512640 135167914 3221224448 3221115708 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/27393/statm): 63001 62892 162 162 0 62839 0
[pid=27393] vsize: 252004
Current children cumulated CPU time (s) 136.59
Current children cumulated vsize (Kb) 254132

[startup+150.016 s]
Raw data (loadavg): 1.10 1.02 0.93 2/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) T 27388 27388 28974 0 -1 0 77611 0 0 0 14320 313 0 0 25 0 1 0 1855070483 274874368 67000 4294967295 134512640 135167914 3221224448 3221115836 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/27393/statm): 67108 67000 162 162 0 66946 0
[pid=27393] vsize: 268432
Current children cumulated CPU time (s) 146.34
Current children cumulated vsize (Kb) 270560

[startup+160.017 s]
Raw data (loadavg): 1.08 1.02 0.93 2/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) R 27388 27388 28974 0 -1 0 81611 0 0 0 15278 331 0 0 25 0 1 0 1855070483 291258368 71000 4294967295 134512640 135167914 3221224448 3221117648 134845933 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27393/statm): 71108 71000 162 162 0 70946 0
[pid=27393] vsize: 284432
Current children cumulated CPU time (s) 156.1
Current children cumulated vsize (Kb) 286560

[startup+170.018 s]
Raw data (loadavg): 1.07 1.02 0.93 1/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) T 27388 27388 28974 0 -1 0 85620 0 0 0 16237 349 0 0 25 0 1 0 1855070483 307679232 75009 4294967295 134512640 135167914 3221224448 3221115900 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/27393/statm): 75117 75009 162 162 0 74955 0
[pid=27393] vsize: 300468
Current children cumulated CPU time (s) 165.87
Current children cumulated vsize (Kb) 302596

[startup+180.019 s]
Raw data (loadavg): 1.06 1.01 0.93 2/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) R 27388 27388 28974 0 -1 0 108072 0 0 0 17176 403 0 0 25 0 1 0 1855070483 399642624 97461 4294967295 134512640 135167914 3221224448 3221117040 134694392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27393/statm): 97569 97461 162 162 0 97407 0
[pid=27393] vsize: 390276
Current children cumulated CPU time (s) 175.8
Current children cumulated vsize (Kb) 392404

[startup+190.019 s]
Raw data (loadavg): 1.05 1.01 0.93 2/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) R 27388 27388 28974 0 -1 0 111554 0 0 0 18136 422 0 0 25 0 1 0 1855070483 370708480 90397 4294967295 134512640 135167914 3221224448 3221116544 134843404 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27393/statm): 90505 90397 162 162 0 90343 0
[pid=27393] vsize: 362020
Current children cumulated CPU time (s) 185.59
Current children cumulated vsize (Kb) 364148

[startup+200.019 s]
Raw data (loadavg): 1.04 1.01 0.93 2/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) R 27388 27388 28974 0 -1 0 115689 0 0 0 19089 441 0 0 25 0 1 0 1855070483 387645440 94532 4294967295 134512640 135167914 3221224448 3221115664 134843064 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27393/statm): 94640 94532 162 162 0 94478 0
[pid=27393] vsize: 378560
Current children cumulated CPU time (s) 195.31
Current children cumulated vsize (Kb) 380688

[startup+210.02 s]
Raw data (loadavg): 1.03 1.01 0.93 1/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) T 27388 27388 28974 0 -1 0 120028 0 0 0 20044 461 0 0 25 0 1 0 1855070483 405417984 98871 4294967295 134512640 135167914 3221224448 3221115772 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/27393/statm): 98979 98871 162 162 0 98817 0
[pid=27393] vsize: 395916
Current children cumulated CPU time (s) 205.06
Current children cumulated vsize (Kb) 398044

[startup+220.021 s]
Raw data (loadavg): 1.03 1.01 0.93 2/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) R 27388 27388 28974 0 -1 0 124334 0 0 0 20993 480 0 0 25 0 1 0 1855070483 423055360 103177 4294967295 134512640 135167914 3221224448 3221115740 134522361 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27393/statm): 103285 103177 162 162 0 103123 0
[pid=27393] vsize: 413140
Current children cumulated CPU time (s) 214.74
Current children cumulated vsize (Kb) 415268

[startup+230.021 s]
Raw data (loadavg): 1.02 1.01 0.93 2/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) R 27388 27388 28974 0 -1 0 128453 0 0 0 21948 498 0 0 25 0 1 0 1855070483 439926784 107296 4294967295 134512640 135167914 3221224448 3221117728 134849110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27393/statm): 107404 107296 162 162 0 107242 0
[pid=27393] vsize: 429616
Current children cumulated CPU time (s) 224.47
Current children cumulated vsize (Kb) 431744

[startup+240.022 s]
Raw data (loadavg): 1.02 1.01 0.93 1/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) T 27388 27388 28974 0 -1 0 132461 0 0 0 22906 514 0 0 25 0 1 0 1855070483 456343552 111304 4294967295 134512640 135167914 3221224448 3221116700 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/27393/statm): 111412 111304 162 162 0 111250 0
[pid=27393] vsize: 445648
Current children cumulated CPU time (s) 234.21
Current children cumulated vsize (Kb) 447776

[startup+250.022 s]
Raw data (loadavg): 1.02 1.01 0.93 2/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) R 27388 27388 28974 0 -1 0 136554 0 0 0 23863 533 0 0 25 0 1 0 1855070483 473108480 115397 4294967295 134512640 135167914 3221224448 3221118752 134694394 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27393/statm): 115505 115397 162 162 0 115343 0
[pid=27393] vsize: 462020
Current children cumulated CPU time (s) 243.97
Current children cumulated vsize (Kb) 464148

[startup+260.023 s]
Raw data (loadavg): 1.01 1.01 0.93 2/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) R 27388 27388 28974 0 -1 0 140534 0 0 0 24819 552 0 0 25 0 1 0 1855070483 489410560 119377 4294967295 134512640 135167914 3221224448 3221116096 134624855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27393/statm): 119485 119377 162 162 0 119323 0
[pid=27393] vsize: 477940
Current children cumulated CPU time (s) 253.72
Current children cumulated vsize (Kb) 480068

[startup+270.024 s]
Raw data (loadavg): 1.01 1.01 0.93 2/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) R 27388 27388 28974 0 -1 0 144489 0 0 0 25778 567 0 0 25 0 1 0 1855070483 505618432 123332 4294967295 134512640 135167914 3221224448 3221116704 134849595 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27393/statm): 123442 123332 162 162 0 123280 0
[pid=27393] vsize: 493768
Current children cumulated CPU time (s) 263.46
Current children cumulated vsize (Kb) 495896

[startup+280.025 s]
Raw data (loadavg): 1.01 1.00 0.93 2/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) R 27388 27388 28974 0 -1 0 148474 0 0 0 26736 584 0 0 25 0 1 0 1855070483 521940992 127317 4294967295 134512640 135167914 3221224448 3221116160 134843404 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27393/statm): 127427 127317 162 162 0 127265 0
[pid=27393] vsize: 509708
Current children cumulated CPU time (s) 273.21
Current children cumulated vsize (Kb) 511836

[startup+290.026 s]
Raw data (loadavg): 1.01 1.00 0.93 2/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) T 27388 27388 28974 0 -1 0 152461 0 0 0 27692 602 0 0 25 0 1 0 1855070483 538271744 131304 4294967295 134512640 135167914 3221224448 3221115324 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/27393/statm): 131414 131304 162 162 0 131252 0
[pid=27393] vsize: 525656
Current children cumulated CPU time (s) 282.95
Current children cumulated vsize (Kb) 527784

[startup+300.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) R 27388 27388 28974 0 -1 0 156329 0 0 0 28650 618 0 0 25 0 1 0 1855070483 554115072 135172 4294967295 134512640 135167914 3221224448 3221117064 134849057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27393/statm): 135282 135172 162 162 0 135120 0
[pid=27393] vsize: 541128
Current children cumulated CPU time (s) 292.69
Current children cumulated vsize (Kb) 543256

[startup+310.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) R 27388 27388 28974 0 -1 0 160176 0 0 0 29605 636 0 0 25 0 1 0 1855070483 569872384 139019 4294967295 134512640 135167914 3221224448 3221117424 134693561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27393/statm): 139129 139019 162 162 0 138967 0
[pid=27393] vsize: 556516
Current children cumulated CPU time (s) 302.42
Current children cumulated vsize (Kb) 558644

[startup+320.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) R 27388 27388 28974 0 -1 0 163961 0 0 0 30565 652 0 0 25 0 1 0 1855070483 585375744 142804 4294967295 134512640 135167914 3221224448 3221116184 134843032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27393/statm): 142914 142804 162 162 0 142752 0
[pid=27393] vsize: 571656
Current children cumulated CPU time (s) 312.18
Current children cumulated vsize (Kb) 573784

[startup+330.028 s]
Raw data (loadavg): 1.00 1.00 0.93 1/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) T 27388 27388 28974 0 -1 0 167880 0 0 0 31524 667 0 0 25 0 1 0 1855070483 601427968 146723 4294967295 134512640 135167914 3221224448 3221116028 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/27393/statm): 146833 146723 162 162 0 146671 0
[pid=27393] vsize: 587332
Current children cumulated CPU time (s) 321.92
Current children cumulated vsize (Kb) 589460

[startup+340.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) R 27388 27388 28974 0 -1 0 180359 0 0 0 32471 700 0 0 25 0 1 0 1855070483 789721088 159202 4294967295 134512640 135167914 3221224448 3221117088 134625368 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27393/statm): 192803 159210 162 162 0 192641 0
[pid=27393] vsize: 771212
Current children cumulated CPU time (s) 331.72
Current children cumulated vsize (Kb) 773340

[startup+350.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) R 27388 27388 28974 0 -1 0 213850 0 0 0 33396 775 0 0 25 0 1 0 1855070483 789721088 192693 4294967295 134512640 135167914 3221224448 3221117040 134694392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27393/statm): 192803 192693 162 162 0 192641 0
[pid=27393] vsize: 771212
Current children cumulated CPU time (s) 341.72
Current children cumulated vsize (Kb) 773340

[startup+360.03 s]
Raw data (loadavg): 1.00 1.00 0.93 1/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) T 27388 27388 28974 0 -1 0 215196 0 0 0 34378 784 0 0 25 0 1 0 1855070483 708845568 172948 4294967295 134512640 135167914 3221224448 3221116220 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/27393/statm): 173058 172948 162 162 0 172896 0
[pid=27393] vsize: 692232
Current children cumulated CPU time (s) 351.63
Current children cumulated vsize (Kb) 694360

[startup+370.031 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) R 27388 27388 28974 0 -1 0 219317 0 0 0 35335 802 0 0 25 0 1 0 1855070483 725721088 177069 4294967295 134512640 135167914 3221224448 3221118944 134849606 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27393/statm): 177178 177069 162 162 0 177016 0
[pid=27393] vsize: 708712
Current children cumulated CPU time (s) 361.38
Current children cumulated vsize (Kb) 710840

[startup+380.032 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) R 27388 27388 28974 0 -1 0 223541 0 0 0 36290 820 0 0 25 0 1 0 1855070483 743022592 181293 4294967295 134512640 135167914 3221224448 3221116040 134845877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27393/statm): 181402 181293 162 162 0 181240 0
[pid=27393] vsize: 725608
Current children cumulated CPU time (s) 371.11
Current children cumulated vsize (Kb) 727736

[startup+390.033 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) T 27388 27388 28974 0 -1 0 227753 0 0 0 37242 842 0 0 25 0 1 0 1855070483 760274944 185505 4294967295 134512640 135167914 3221224448 3221115996 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/27393/statm): 185614 185505 162 162 0 185452 0
[pid=27393] vsize: 742456
Current children cumulated CPU time (s) 380.85
Current children cumulated vsize (Kb) 744584

[startup+400.033 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) R 27388 27388 28974 0 -1 0 231868 0 0 0 38196 862 0 0 25 0 1 0 1855070483 777129984 189620 4294967295 134512640 135167914 3221224448 3221117500 134722512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27393/statm): 189729 189620 162 162 0 189567 0
[pid=27393] vsize: 758916
Current children cumulated CPU time (s) 390.59
Current children cumulated vsize (Kb) 761044

[startup+410.033 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) R 27388 27388 28974 0 -1 0 235955 0 0 0 39149 880 0 0 25 0 1 0 1855070483 793870336 193707 4294967295 134512640 135167914 3221224448 3221116320 134623786 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27393/statm): 193816 193707 162 162 0 193654 0
[pid=27393] vsize: 775264
Current children cumulated CPU time (s) 400.3
Current children cumulated vsize (Kb) 777392

[startup+420.034 s]
Raw data (loadavg): 1.00 1.00 0.93 1/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) T 27388 27388 28974 0 -1 0 240013 0 0 0 40104 898 0 0 25 0 1 0 1855070483 810491904 197765 4294967295 134512640 135167914 3221224448 3221116252 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/27393/statm): 197874 197765 162 162 0 197712 0
[pid=27393] vsize: 791496
Current children cumulated CPU time (s) 410.03
Current children cumulated vsize (Kb) 793624

[startup+430.034 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) T 27388 27388 28974 0 -1 0 244014 0 0 0 41058 918 0 0 25 0 1 0 1855070483 826880000 201766 4294967295 134512640 135167914 3221224448 3221115836 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/27393/statm): 201875 201766 162 162 0 201713 0
[pid=27393] vsize: 807500
Current children cumulated CPU time (s) 419.77
Current children cumulated vsize (Kb) 809628

[startup+440.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) R 27388 27388 28974 0 -1 0 247997 0 0 0 42016 936 0 0 25 0 1 0 1855070483 843194368 205749 4294967295 134512640 135167914 3221224448 3221116384 134843036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27393/statm): 205858 205749 162 162 0 205696 0
[pid=27393] vsize: 823432
Current children cumulated CPU time (s) 429.53
Current children cumulated vsize (Kb) 825560

[startup+450.036 s]
Raw data (loadavg): 1.00 1.00 0.93 1/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) T 27388 27388 28974 0 -1 0 251960 0 0 0 42972 954 0 0 25 0 1 0 1855070483 859430912 209712 4294967295 134512640 135167914 3221224448 3221117116 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/27393/statm): 209822 209712 162 162 0 209660 0
[pid=27393] vsize: 839288
Current children cumulated CPU time (s) 439.27
Current children cumulated vsize (Kb) 841416

[startup+460.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) R 27388 27388 28974 0 -1 0 255890 0 0 0 43931 969 0 0 25 0 1 0 1855070483 875524096 213642 4294967295 134512640 135167914 3221224448 3221116608 134849108 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27393/statm): 213751 213642 162 162 0 213589 0
[pid=27393] vsize: 855004
Current children cumulated CPU time (s) 449.01
Current children cumulated vsize (Kb) 857132

[startup+470.037 s]
Raw data (loadavg): 1.00 1.00 0.93 1/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) T 27388 27388 28974 0 -1 0 259873 0 0 0 44889 987 0 0 25 0 1 0 1855070483 891838464 217625 4294967295 134512640 135167914 3221224448 3221115388 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/27393/statm): 217734 217625 162 162 0 217572 0
[pid=27393] vsize: 870936
Current children cumulated CPU time (s) 458.77
Current children cumulated vsize (Kb) 873064

[startup+480.038 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) R 27388 27388 28974 0 -1 0 263827 0 0 0 45846 1005 0 0 25 0 1 0 1855070483 908034048 221579 4294967295 134512640 135167914 3221224448 3221115828 134849220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27393/statm): 221688 221579 162 162 0 221526 0
[pid=27393] vsize: 886752
Current children cumulated CPU time (s) 468.52
Current children cumulated vsize (Kb) 888880

[startup+490.039 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) R 27388 27388 28974 0 -1 0 267840 0 0 0 46802 1023 0 0 25 0 1 0 1855070483 924471296 225592 4294967295 134512640 135167914 3221224448 3221118080 134694419 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27393/statm): 225701 225592 162 162 0 225539 0
[pid=27393] vsize: 902804
Current children cumulated CPU time (s) 478.26
Current children cumulated vsize (Kb) 904932

[startup+500.04 s]
Raw data (loadavg): 1.00 1.00 0.93 1/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) T 27388 27388 28974 0 -1 0 271902 0 35 0 47726 1045 0 0 23 0 1 0 1855070483 940593152 229180 4294967295 134512640 135167914 3221224448 3221115708 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/27393/statm): 229637 229180 162 162 0 229475 0
[pid=27393] vsize: 918548
Current children cumulated CPU time (s) 487.72
Current children cumulated vsize (Kb) 920676



Mem limit exceeded: sending SIGTERM then SIGKILL

[startup+500.96 s]
Raw data (loadavg): 1.00 1.00 0.93 1/57 27393
Raw data (/proc/27388/stat): 27388 (minisat+_script) S 27387 27388 28974 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1855070476 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27388/statm): 532 234 485 147 0 385 0
[pid=27388] vsize: 2128
Raw data (/proc/27393/stat): 27393 (minisat+_bignum) T 27388 27388 28974 0 -1 0 272198 0 59 0 47779 1047 0 0 20 0 1 0 1855070483 941543424 229500 4294967295 134512640 135167914 3221224448 3221116220 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/27393/statm): 229869 229500 162 162 0 229707 0
[pid=27393] vsize: 919476
Current children cumulated CPU time (s) 488.27
Current children cumulated vsize (Kb) 921604

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

Child status: 0
Real time (s): 501.385
CPU time (s): 488.692
CPU user time (s): 477.797
CPU system time (s): 10.8943
CPU usage (%): 97.4684
Max. virtual memory (cumulated for all children) (Kb): 921604

Verifier Data

ERROR: no interpretation found !