Some explanations

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

General information on the benchmark

Namemps-v2-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-vtp.base.opb
MD5SUM62492fa5ef4f36caec6c1eec4eeb566a
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 181
Biggest coefficient in the objective function 1073741824
Number of bits for the biggest coefficient in the objective function 31
Sum of the numbers in the objective function 7516192762
Number of bits of the sum of numbers in the objective function 33
Biggest number in a constraint 198568686125056
Number of bits of the biggest number in a constraint 48
Biggest sum of numbers in a constraint 12817928787879752
Number of bits of the biggest sum of numbers54
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables4524
Total number of constraints262
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 constraints262
Minimum length of a constraint11
Maximum length of a constraint1080

Trace number 2667

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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:        911216 kB
Buffers:         35168 kB
Cached:          60376 kB
SwapCached:        744 kB
Active:          67932 kB
Inactive:        30204 kB
HighTotal:      131008 kB
HighFree:        67508 kB
LowTotal:       903652 kB
LowFree:        843708 kB
SwapTotal:     2097892 kB
SwapFree:      2096644 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5736 kB
Slab:            19612 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 20:50:46 (client local time) WITH STATUS 0 IN 729.671 SECONDS
stats: 2827 7 729.671 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 305] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...
c Parsing PB file...
c Converting 261 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ############################################
c   -- Clauses(.)/Splits(s): sssssssssssssssssssssssssss
c ---[ 286]---> BDD-cost:   18
c ---[ 285]---> BDD-cost:   16
c ---[ 284]---> BDD-cost:   16
c ---[ 283]---> BDD-cost:   16
c ---[ 282]---> BDD-cost:   18
c ---[ 281]---> BDD-cost:   16
c ---[ 280]---> BDD-cost:   16
c ---[ 279]---> BDD-cost:   16
c ---[ 278]---> BDD-cost:   18
c ---[ 277]---> BDD-cost:   16
c ---[ 276]---> BDD-cost:   16
c ---[ 275]---> BDD-cost:   16
c ---[ 274]---> BDD-cost:   18
c ---[ 273]---> BDD-cost:   16
c ---[ 272]---> BDD-cost:   16
c ---[ 271]---> BDD-cost:   16
c ---[ 270]---> BDD-cost:   18
c ---[ 269]---> BDD-cost:   16
c ---[ 268]---> BDD-cost:   16
c ---[ 267]---> BDD-cost:   16
c ---[ 266]---> BDD-cost:   18
c ---[ 265]---> BDD-cost:   16
c ---[ 264]---> BDD-cost:   16
c ---[ 263]---> BDD-cost:   16
c ---[ 262]---> BDD-cost:   18
c ---[ 261]---> BDD-cost:   16
c ---[ 260]---> BDD-cost:   16
c ---[ 259]---> BDD-cost:   16
c ---[ 258]---> BDD-cost:   18
c ---[ 257]---> BDD-cost:   16
c ---[ 256]---> BDD-cost:   16
c ---[ 255]---> BDD-cost:   16
c ---[ 221]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 219]---> Sorter-cost: 2344     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 217]---> Sorter-cost: 2370     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 215]---> Sorter-cost: 3598     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 213]---> Sorter-cost: 2363     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 211]---> Sorter-cost: 2378     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 209]---> Sorter-cost: 2440     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 207]---> Sorter-cost: 1691     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 205]---> Sorter-cost: 1041     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3
c ---[ 203]---> Adder-cost: 475   maxlim: 8105876   bits: 24/23
c ---[ 201]---> Sorter-cost: 3427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 199]---> Sorter-cost: 3442     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 197]---> Sorter-cost: 3457     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 195]---> Adder-cost: 502   maxlim: 75018132   bits: 28/27
c ---[ 193]---> Sorter-cost: 3571     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 191]---> Sorter-cost: 1997     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 189]---> Sorter-cost: 1663     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 187]---> Sorter-cost: 3364     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 185]---> Sorter-cost: 3324     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 183]---> Sorter-cost: 3339     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 181]---> Adder-cost: 410   maxlim: 74725284   bits: 28/27
c ---[ 179]---> Sorter-cost: 3447     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 177]---> Adder-cost: 420   maxlim: 275744676   bits: 30/29
c ---[ 175]---> Sorter-cost: 1977     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 173]---> Sorter-cost:  605     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 171]---> Sorter-cost: 2111     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3
c ---[ 169]---> Adder-cost: 388   maxlim: 9779094   bits: 25/24
c ---[ 167]---> Sorter-cost: 2171     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 165]---> Sorter-cost: 2186     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 163]---> Sorter-cost: 2207     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 161]---> Sorter-cost: 2252     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 159]---> Sorter-cost: 1601     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 147]---> 
c *

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/27508/stat): 27508 (minisat+_script) R 27507 27508 20728 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1844196815 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/27508/statm): 174 3 169 147 0 27 0
[pid=27508] 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=27509
New process pid=27510
New process pid=27511
execve syscall for /bin/sed executable
One traced child (pid=27510) 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=27511) exited with status: 0
One traced child (pid=27509) exited with status: 0
New process pid=27512
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-vtp.base.opb
One traced child (pid=27512) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=27513
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-vtp.base.opb

[startup+10.004 s]
Raw data (loadavg): 0.84 0.90 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 1568 0 0 0 972 5 0 0 25 0 1 0 1844196832 6123520 1357 4294967295 134512640 135167914 3221224448 3221221440 134843420 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27513/statm): 1495 1357 162 162 0 1333 0
[pid=27513] vsize: 5980
Current children cumulated CPU time (s) 9.89
Current children cumulated vsize (Kb) 8108

[startup+20.0048 s]
Raw data (loadavg): 0.86 0.90 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 6295 0 0 0 1928 26 0 0 25 0 1 0 1844196832 23650304 5464 4294967295 134512640 135167914 3221224448 3221041212 134934490 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27513/statm): 5774 5464 162 162 0 5612 0
[pid=27513] vsize: 23096
Current children cumulated CPU time (s) 19.66
Current children cumulated vsize (Kb) 25224

[startup+30.0054 s]
Raw data (loadavg): 0.88 0.91 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 11234 0 0 0 2885 47 0 0 25 0 1 0 1844196832 41181184 9744 4294967295 134512640 135167914 3221224448 3221039808 134847261 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27513/statm): 10054 9744 162 162 0 9892 0
[pid=27513] vsize: 40216
Current children cumulated CPU time (s) 29.44
Current children cumulated vsize (Kb) 42344

[startup+40.0051 s]
Raw data (loadavg): 0.90 0.91 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 17146 0 0 0 3839 71 0 0 25 0 1 0 1844196832 59998208 14338 4294967295 134512640 135167914 3221224448 3221051144 134693650 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27513/statm): 14648 14338 162 162 0 14486 0
[pid=27513] vsize: 58592
Current children cumulated CPU time (s) 39.22
Current children cumulated vsize (Kb) 60720

[startup+50.0068 s]
Raw data (loadavg): 0.91 0.91 0.91 1/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) T 27508 27508 20728 0 -1 0 20571 0 0 0 4798 88 0 0 25 0 1 0 1844196832 74027008 17763 4294967295 134512640 135167914 3221224448 3221045372 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/27513/statm): 18073 17763 162 162 0 17911 0
[pid=27513] vsize: 72292
Current children cumulated CPU time (s) 48.98
Current children cumulated vsize (Kb) 74420

[startup+60.0075 s]
Raw data (loadavg): 0.93 0.91 0.91 1/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) T 27508 27508 20728 0 -1 0 28514 0 0 0 5754 115 0 0 25 0 1 0 1844196832 95760384 23069 4294967295 134512640 135167914 3221224448 3221060844 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/27513/statm): 23379 23069 162 162 0 23217 0
[pid=27513] vsize: 93516
Current children cumulated CPU time (s) 58.81
Current children cumulated vsize (Kb) 95644

[startup+70.0082 s]
Raw data (loadavg): 0.94 0.92 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 31801 0 0 0 6716 130 0 0 25 0 1 0 1844196832 109223936 26356 4294967295 134512640 135167914 3221224448 3221039872 134844644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27513/statm): 26666 26356 162 162 0 26504 0
[pid=27513] vsize: 106664
Current children cumulated CPU time (s) 68.58
Current children cumulated vsize (Kb) 108792

[startup+80.0089 s]
Raw data (loadavg): 0.95 0.92 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 35064 0 0 0 7680 145 0 0 25 0 1 0 1844196832 122589184 29619 4294967295 134512640 135167914 3221224448 3221039872 134722532 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27513/statm): 29929 29619 162 162 0 29767 0
[pid=27513] vsize: 119716
Current children cumulated CPU time (s) 78.37
Current children cumulated vsize (Kb) 121844

[startup+90.0086 s]
Raw data (loadavg): 0.95 0.92 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 38178 0 0 0 8645 161 0 0 25 0 1 0 1844196832 135344128 32733 4294967295 134512640 135167914 3221224448 3221076872 134846971 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27513/statm): 33043 32733 162 162 0 32881 0
[pid=27513] vsize: 132172
Current children cumulated CPU time (s) 88.18
Current children cumulated vsize (Kb) 134300

[startup+100.009 s]
Raw data (loadavg): 0.96 0.92 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 41217 0 0 0 9612 176 0 0 25 0 1 0 1844196832 147791872 35772 4294967295 134512640 135167914 3221224448 3221054592 134847211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27513/statm): 36082 35772 162 162 0 35920 0
[pid=27513] vsize: 144328
Current children cumulated CPU time (s) 98
Current children cumulated vsize (Kb) 146456

[startup+110.01 s]
Raw data (loadavg): 0.97 0.92 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 54527 0 0 0 10558 212 0 0 25 0 1 0 1844196832 202309632 49082 4294967295 134512640 135167914 3221224448 3221052752 134694392 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27513/statm): 49392 49082 162 162 0 49230 0
[pid=27513] vsize: 197568
Current children cumulated CPU time (s) 107.82
Current children cumulated vsize (Kb) 199696

[startup+120.011 s]
Raw data (loadavg): 0.97 0.93 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 56366 0 0 0 11536 222 0 0 25 0 1 0 1844196832 188243968 45648 4294967295 134512640 135167914 3221224448 3221041996 134844675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27513/statm): 45958 45648 162 162 0 45796 0
[pid=27513] vsize: 183832
Current children cumulated CPU time (s) 117.7
Current children cumulated vsize (Kb) 185960

[startup+130.011 s]
Raw data (loadavg): 0.98 0.93 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 59575 0 0 0 12501 236 0 0 25 0 1 0 1844196832 201388032 48857 4294967295 134512640 135167914 3221224448 3221040796 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27513/statm): 49167 48857 162 162 0 49005 0
[pid=27513] vsize: 196668
Current children cumulated CPU time (s) 127.49
Current children cumulated vsize (Kb) 198796

[startup+140.012 s]
Raw data (loadavg): 0.98 0.93 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 62407 0 0 0 13471 249 0 0 25 0 1 0 1844196832 212987904 51689 4294967295 134512640 135167914 3221224448 3221048032 134695583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27513/statm): 51999 51689 162 162 0 51837 0
[pid=27513] vsize: 207996
Current children cumulated CPU time (s) 137.32
Current children cumulated vsize (Kb) 210124

[startup+150.014 s]
Raw data (loadavg): 0.98 0.93 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 65465 0 0 0 14437 263 0 0 25 0 1 0 1844196832 225513472 54747 4294967295 134512640 135167914 3221224448 3221040224 134844676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27513/statm): 55057 54747 162 162 0 54895 0
[pid=27513] vsize: 220228
Current children cumulated CPU time (s) 147.12
Current children cumulated vsize (Kb) 222356

[startup+160.015 s]
Raw data (loadavg): 0.98 0.93 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 68243 0 0 0 15406 277 0 0 25 0 1 0 1844196832 236892160 57525 4294967295 134512640 135167914 3221224448 3221038560 134843153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27513/statm): 57835 57525 162 162 0 57673 0
[pid=27513] vsize: 231340
Current children cumulated CPU time (s) 156.95
Current children cumulated vsize (Kb) 233468

[startup+170.015 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 71147 0 0 0 16372 291 0 0 25 0 1 0 1844196832 248786944 60429 4294967295 134512640 135167914 3221224448 3221045296 134693566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27513/statm): 60739 60429 162 162 0 60577 0
[pid=27513] vsize: 242956
Current children cumulated CPU time (s) 166.75
Current children cumulated vsize (Kb) 245084

[startup+180.016 s]
Raw data (loadavg): 0.99 0.94 0.91 1/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) T 27508 27508 20728 0 -1 0 73919 0 0 0 17342 303 0 0 25 0 1 0 1844196832 260141056 63201 4294967295 134512640 135167914 3221224448 3221037996 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/27513/statm): 63511 63201 162 162 0 63349 0
[pid=27513] vsize: 254044
Current children cumulated CPU time (s) 176.57
Current children cumulated vsize (Kb) 256172

[startup+190.017 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 76614 0 0 0 18312 316 0 0 25 0 1 0 1844196832 271179776 65896 4294967295 134512640 135167914 3221224448 3221040352 134694392 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27513/statm): 66206 65896 162 162 0 66044 0
[pid=27513] vsize: 264824
Current children cumulated CPU time (s) 186.4
Current children cumulated vsize (Kb) 266952

[startup+200.017 s]
Raw data (loadavg): 0.99 0.94 0.91 1/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) T 27508 27508 20728 0 -1 0 79462 0 0 0 19284 327 0 0 25 0 1 0 1844196832 282845184 68744 4294967295 134512640 135167914 3221224448 3221036700 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/27513/statm): 69054 68744 162 162 0 68892 0
[pid=27513] vsize: 276216
Current children cumulated CPU time (s) 196.23
Current children cumulated vsize (Kb) 278344

[startup+210.018 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 82152 0 0 0 20256 339 0 0 25 0 1 0 1844196832 293863424 71434 4294967295 134512640 135167914 3221224448 3221048228 134624790 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27513/statm): 71744 71434 162 162 0 71582 0
[pid=27513] vsize: 286976
Current children cumulated CPU time (s) 206.07
Current children cumulated vsize (Kb) 289104

[startup+220.019 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 84808 0 0 0 21224 353 0 0 25 0 1 0 1844196832 304742400 74090 4294967295 134512640 135167914 3221224448 3221041312 134695622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27513/statm): 74400 74090 162 162 0 74238 0
[pid=27513] vsize: 297600
Current children cumulated CPU time (s) 215.89
Current children cumulated vsize (Kb) 299728

[startup+230.019 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 107412 0 0 0 22160 409 0 0 25 0 1 0 1844196832 397328384 96694 4294967295 134512640 135167914 3221224448 3221057056 134625423 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27513/statm): 97004 96694 162 162 0 96842 0
[pid=27513] vsize: 388016
Current children cumulated CPU time (s) 225.81
Current children cumulated vsize (Kb) 390144

[startup+240.02 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 108926 0 0 0 23141 419 0 0 25 0 1 0 1844196832 360333312 87662 4294967295 134512640 135167914 3221224448 3221056544 134845937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27513/statm): 87972 87662 162 162 0 87810 0
[pid=27513] vsize: 351888
Current children cumulated CPU time (s) 235.72
Current children cumulated vsize (Kb) 354016

[startup+250.021 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 111573 0 0 0 24110 432 0 0 25 0 1 0 1844196832 371175424 90309 4294967295 134512640 135167914 3221224448 3221043712 134694392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27513/statm): 90619 90309 162 162 0 90457 0
[pid=27513] vsize: 362476
Current children cumulated CPU time (s) 245.54
Current children cumulated vsize (Kb) 364604

[startup+260.021 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 114219 0 0 0 25082 444 0 0 25 0 1 0 1844196832 382013440 92955 4294967295 134512640 135167914 3221224448 3221055600 134516629 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27513/statm): 93265 92955 162 162 0 93103 0
[pid=27513] vsize: 373060
Current children cumulated CPU time (s) 255.38
Current children cumulated vsize (Kb) 375188

[startup+270.022 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 116792 0 0 0 26055 455 0 0 25 0 1 0 1844196832 392552448 95528 4294967295 134512640 135167914 3221224448 3221040464 134849102 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27513/statm): 95838 95528 162 162 0 95676 0
[pid=27513] vsize: 383352
Current children cumulated CPU time (s) 265.22
Current children cumulated vsize (Kb) 385480

[startup+280.023 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 119767 0 0 0 27021 469 0 0 25 0 1 0 1844196832 404738048 98503 4294967295 134512640 135167914 3221224448 3221049308 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27513/statm): 98813 98503 162 162 0 98651 0
[pid=27513] vsize: 395252
Current children cumulated CPU time (s) 275.02
Current children cumulated vsize (Kb) 397380

[startup+290.024 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 122321 0 0 0 27993 480 0 0 25 0 1 0 1844196832 415199232 101057 4294967295 134512640 135167914 3221224448 3221038704 134845913 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27513/statm): 101367 101057 162 162 0 101205 0
[pid=27513] vsize: 405468
Current children cumulated CPU time (s) 284.85
Current children cumulated vsize (Kb) 407596

[startup+300.025 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 124896 0 0 0 28966 491 0 0 25 0 1 0 1844196832 425746432 103632 4294967295 134512640 135167914 3221224448 3221042844 134694368 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27513/statm): 103942 103632 162 162 0 103780 0
[pid=27513] vsize: 415768
Current children cumulated CPU time (s) 294.69
Current children cumulated vsize (Kb) 417896

[startup+310.026 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) T 27508 27508 20728 0 -1 0 127400 0 0 0 29938 503 0 0 25 0 1 0 1844196832 436002816 106136 4294967295 134512640 135167914 3221224448 3221038268 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/27513/statm): 106446 106136 162 162 0 106284 0
[pid=27513] vsize: 425784
Current children cumulated CPU time (s) 304.53
Current children cumulated vsize (Kb) 427912

[startup+320.026 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 130317 0 0 0 30906 517 0 0 25 0 1 0 1844196832 447950848 109053 4294967295 134512640 135167914 3221224448 3221047776 134624134 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27513/statm): 109363 109053 162 162 0 109201 0
[pid=27513] vsize: 437452
Current children cumulated CPU time (s) 314.35
Current children cumulated vsize (Kb) 439580

[startup+330.027 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 132800 0 0 0 31877 530 0 0 25 0 1 0 1844196832 458121216 111536 4294967295 134512640 135167914 3221224448 3221037456 134849143 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27513/statm): 111846 111536 162 162 0 111684 0
[pid=27513] vsize: 447384
Current children cumulated CPU time (s) 324.19
Current children cumulated vsize (Kb) 449512

[startup+340.028 s]
Raw data (loadavg): 0.99 0.96 0.91 1/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) T 27508 27508 20728 0 -1 0 135318 0 0 0 32852 540 0 0 25 0 1 0 1844196832 468434944 114054 4294967295 134512640 135167914 3221224448 3221046332 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/27513/statm): 114364 114054 162 162 0 114202 0
[pid=27513] vsize: 457456
Current children cumulated CPU time (s) 334.04
Current children cumulated vsize (Kb) 459584

[startup+350.029 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 137775 0 0 0 33824 551 0 0 25 0 1 0 1844196832 478498816 116511 4294967295 134512640 135167914 3221224448 3221038112 134694392 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27513/statm): 116821 116511 162 162 0 116659 0
[pid=27513] vsize: 467284
Current children cumulated CPU time (s) 343.87
Current children cumulated vsize (Kb) 469412

[startup+360.029 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 140438 0 0 0 34796 564 0 0 25 0 1 0 1844196832 489406464 119174 4294967295 134512640 135167914 3221224448 3221038332 134722225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27513/statm): 119484 119174 162 162 0 119322 0
[pid=27513] vsize: 477936
Current children cumulated CPU time (s) 353.72
Current children cumulated vsize (Kb) 480064

[startup+370.03 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 142901 0 0 0 35768 576 0 0 25 0 1 0 1844196832 499494912 121637 4294967295 134512640 135167914 3221224448 3221050812 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27513/statm): 121947 121637 162 162 0 121785 0
[pid=27513] vsize: 487788
Current children cumulated CPU time (s) 363.56
Current children cumulated vsize (Kb) 489916

[startup+380.031 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 145426 0 0 0 36742 586 0 0 25 0 1 0 1844196832 509837312 124162 4294967295 134512640 135167914 3221224448 3221042016 134694528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27513/statm): 124472 124162 162 162 0 124310 0
[pid=27513] vsize: 497888
Current children cumulated CPU time (s) 373.4
Current children cumulated vsize (Kb) 500016

[startup+390.032 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 147846 0 0 0 37715 596 0 0 25 0 1 0 1844196832 519749632 126582 4294967295 134512640 135167914 3221224448 3221068360 134846935 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27513/statm): 126892 126582 162 162 0 126730 0
[pid=27513] vsize: 507568
Current children cumulated CPU time (s) 383.23
Current children cumulated vsize (Kb) 509696

[startup+400.033 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 150464 0 0 0 38686 609 0 0 25 0 1 0 1844196832 530472960 129200 4294967295 134512640 135167914 3221224448 3221047328 134844706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27513/statm): 129510 129200 162 162 0 129348 0
[pid=27513] vsize: 518040
Current children cumulated CPU time (s) 393.07
Current children cumulated vsize (Kb) 520168

[startup+410.034 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 152896 0 0 0 39658 619 0 0 25 0 1 0 1844196832 540434432 131632 4294967295 134512640 135167914 3221224448 3221042464 134843402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27513/statm): 131942 131632 162 162 0 131780 0
[pid=27513] vsize: 527768
Current children cumulated CPU time (s) 402.89
Current children cumulated vsize (Kb) 529896

[startup+420.034 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 155363 0 0 0 40633 629 0 0 25 0 1 0 1844196832 550539264 134099 4294967295 134512640 135167914 3221224448 3221043264 134694392 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27513/statm): 134409 134099 162 162 0 134247 0
[pid=27513] vsize: 537636
Current children cumulated CPU time (s) 412.74
Current children cumulated vsize (Kb) 539764

[startup+430.034 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 157745 0 0 0 41606 639 0 0 25 0 1 0 1844196832 560295936 136481 4294967295 134512640 135167914 3221224448 3221041744 134624420 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27513/statm): 136791 136481 162 162 0 136629 0
[pid=27513] vsize: 547164
Current children cumulated CPU time (s) 422.57
Current children cumulated vsize (Kb) 549292

[startup+440.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 160430 0 0 0 42574 652 0 0 25 0 1 0 1844196832 571293696 139166 4294967295 134512640 135167914 3221224448 3221063472 134623813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27513/statm): 139476 139166 162 162 0 139314 0
[pid=27513] vsize: 557904
Current children cumulated CPU time (s) 432.38
Current children cumulated vsize (Kb) 560032

[startup+450.036 s]
Raw data (loadavg): 1.07 0.98 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 162947 0 0 0 43544 663 0 0 25 0 1 0 1844196832 581603328 141683 4294967295 134512640 135167914 3221224448 3221056608 134847226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27513/statm): 141993 141683 162 162 0 141831 0
[pid=27513] vsize: 567972
Current children cumulated CPU time (s) 442.19
Current children cumulated vsize (Kb) 570100

[startup+460.036 s]
Raw data (loadavg): 1.06 0.98 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 165387 0 0 0 44517 674 0 0 25 0 1 0 1844196832 591597568 144123 4294967295 134512640 135167914 3221224448 3221046880 134843113 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27513/statm): 144433 144123 162 162 0 144271 0
[pid=27513] vsize: 577732
Current children cumulated CPU time (s) 452.03
Current children cumulated vsize (Kb) 579860

[startup+470.037 s]
Raw data (loadavg): 1.05 0.98 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 167802 0 0 0 45491 685 0 0 25 0 1 0 1844196832 601489408 146538 4294967295 134512640 135167914 3221224448 3221040608 134844703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27513/statm): 146848 146538 162 162 0 146686 0
[pid=27513] vsize: 587392
Current children cumulated CPU time (s) 461.88
Current children cumulated vsize (Kb) 589520

[startup+480.038 s]
Raw data (loadavg): 1.04 0.98 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 170303 0 0 0 46464 698 0 0 25 0 1 0 1844196832 611733504 149039 4294967295 134512640 135167914 3221224448 3221046400 134694383 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27513/statm): 149349 149039 162 162 0 149187 0
[pid=27513] vsize: 597396
Current children cumulated CPU time (s) 471.74
Current children cumulated vsize (Kb) 599524

[startup+490.038 s]
Raw data (loadavg): 1.04 0.98 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 213185 0 0 0 47359 798 0 0 25 0 1 0 1844196832 787378176 191921 4294967295 134512640 135167914 3221224448 3221065472 134845881 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27513/statm): 192231 191921 162 162 0 192069 0
[pid=27513] vsize: 768924
Current children cumulated CPU time (s) 481.69
Current children cumulated vsize (Kb) 771052

[startup+500.039 s]
Raw data (loadavg): 1.03 0.98 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 213185 0 0 0 48359 798 0 0 25 0 1 0 1844196832 787378176 191921 4294967295 134512640 135167914 3221224448 3221065488 134849099 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27513/statm): 192231 191921 162 162 0 192069 0
[pid=27513] vsize: 768924
Current children cumulated CPU time (s) 491.69
Current children cumulated vsize (Kb) 771052

[startup+510.04 s]
Raw data (loadavg): 1.03 0.98 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 215502 0 0 0 49330 815 0 0 25 0 1 0 1844196832 710479872 173147 4294967295 134512640 135167914 3221224448 3221052960 134695981 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27513/statm): 173457 173147 162 162 0 173295 0
[pid=27513] vsize: 693828
Current children cumulated CPU time (s) 501.57
Current children cumulated vsize (Kb) 695956

[startup+520.04 s]
Raw data (loadavg): 1.02 0.98 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 217918 0 0 0 50301 828 0 0 25 0 1 0 1844196832 720375808 175563 4294967295 134512640 135167914 3221224448 3221040156 134842996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27513/statm): 175873 175563 162 162 0 175711 0
[pid=27513] vsize: 703492
Current children cumulated CPU time (s) 511.41
Current children cumulated vsize (Kb) 705620

[startup+530.041 s]
Raw data (loadavg): 1.02 0.98 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 220365 0 0 0 51276 838 0 0 25 0 1 0 1844196832 730398720 178010 4294967295 134512640 135167914 3221224448 3221068672 134849187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27513/statm): 178320 178010 162 162 0 178158 0
[pid=27513] vsize: 713280
Current children cumulated CPU time (s) 521.26
Current children cumulated vsize (Kb) 715408

[startup+540.042 s]
Raw data (loadavg): 1.01 0.98 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 222797 0 0 0 52250 849 0 0 25 0 1 0 1844196832 740360192 180442 4294967295 134512640 135167914 3221224448 3221054464 134694405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27513/statm): 180752 180442 162 162 0 180590 0
[pid=27513] vsize: 723008
Current children cumulated CPU time (s) 531.11
Current children cumulated vsize (Kb) 725136

[startup+550.043 s]
Raw data (loadavg): 1.01 0.98 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) T 27508 27508 20728 0 -1 0 225301 0 0 0 53222 860 0 0 25 0 1 0 1844196832 750616576 182946 4294967295 134512640 135167914 3221224448 3221036316 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/27513/statm): 183256 182946 162 162 0 183094 0
[pid=27513] vsize: 733024
Current children cumulated CPU time (s) 540.94
Current children cumulated vsize (Kb) 735152

[startup+560.043 s]
Raw data (loadavg): 1.01 0.98 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 227678 0 0 0 54195 871 0 0 25 0 1 0 1844196832 760352768 185323 4294967295 134512640 135167914 3221224448 3221040544 134844644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27513/statm): 185633 185323 162 162 0 185471 0
[pid=27513] vsize: 742532
Current children cumulated CPU time (s) 550.78
Current children cumulated vsize (Kb) 744660

[startup+570.043 s]
Raw data (loadavg): 1.01 0.98 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 230076 0 0 0 55171 880 0 0 25 0 1 0 1844196832 770174976 187721 4294967295 134512640 135167914 3221224448 3221071776 134695967 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27513/statm): 188031 187721 162 162 0 187869 0
[pid=27513] vsize: 752124
Current children cumulated CPU time (s) 560.63
Current children cumulated vsize (Kb) 754252

[startup+580.044 s]
Raw data (loadavg): 1.01 0.98 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 232503 0 0 0 56143 891 0 0 25 0 1 0 1844196832 780115968 190148 4294967295 134512640 135167914 3221224448 3221039456 134849153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27513/statm): 190458 190148 162 162 0 190296 0
[pid=27513] vsize: 761832
Current children cumulated CPU time (s) 570.46
Current children cumulated vsize (Kb) 763960

[startup+590.044 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 234939 0 0 0 57119 900 0 0 25 0 1 0 1844196832 790093824 192584 4294967295 134512640 135167914 3221224448 3221039920 134693561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27513/statm): 192894 192584 162 162 0 192732 0
[pid=27513] vsize: 771576
Current children cumulated CPU time (s) 580.31
Current children cumulated vsize (Kb) 773704

[startup+600.045 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 237324 0 0 0 58092 911 0 0 25 0 1 0 1844196832 799862784 194969 4294967295 134512640 135167914 3221224448 3221048512 134844653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27513/statm): 195279 194969 162 162 0 195117 0
[pid=27513] vsize: 781116
Current children cumulated CPU time (s) 590.15
Current children cumulated vsize (Kb) 783244

[startup+610.046 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) T 27508 27508 20728 0 -1 0 239974 0 0 0 59061 923 0 0 17 0 1 0 1844196832 810717184 197619 4294967295 134512640 135167914 3221224448 3221075180 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/27513/statm): 197929 197619 162 162 0 197767 0
[pid=27513] vsize: 791716
Current children cumulated CPU time (s) 599.96
Current children cumulated vsize (Kb) 793844

[startup+620.047 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 242484 0 0 0 60033 935 0 0 25 0 1 0 1844196832 820998144 200129 4294967295 134512640 135167914 3221224448 3221068448 134843160 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27513/statm): 200439 200129 162 162 0 200277 0
[pid=27513] vsize: 801756
Current children cumulated CPU time (s) 609.8
Current children cumulated vsize (Kb) 803884

[startup+630.047 s]
Raw data (loadavg): 1.00 0.98 0.91 1/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) T 27508 27508 20728 0 -1 0 244852 0 0 0 61008 944 0 0 25 0 1 0 1844196832 830697472 202497 4294967295 134512640 135167914 3221224448 3221060956 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/27513/statm): 202807 202497 162 162 0 202645 0
[pid=27513] vsize: 811228
Current children cumulated CPU time (s) 619.64
Current children cumulated vsize (Kb) 813356

[startup+640.048 s]
Raw data (loadavg): 1.00 0.98 0.91 1/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) T 27508 27508 20728 0 -1 0 247339 0 0 0 61982 955 0 0 25 0 1 0 1844196832 840884224 204984 4294967295 134512640 135167914 3221224448 3221040124 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/27513/statm): 205294 204984 162 162 0 205132 0
[pid=27513] vsize: 821176
Current children cumulated CPU time (s) 629.49
Current children cumulated vsize (Kb) 823304

[startup+650.05 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 249682 0 0 0 62958 965 0 0 25 0 1 0 1844196832 850481152 207327 4294967295 134512640 135167914 3221224448 3221041696 134694377 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27513/statm): 207637 207327 162 162 0 207475 0
[pid=27513] vsize: 830548
Current children cumulated CPU time (s) 639.35
Current children cumulated vsize (Kb) 832676

[startup+660.05 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 252112 0 0 0 63929 978 0 0 25 0 1 0 1844196832 860434432 209757 4294967295 134512640 135167914 3221224448 3221040840 134693631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27513/statm): 210067 209757 162 162 0 209905 0
[pid=27513] vsize: 840268
Current children cumulated CPU time (s) 649.19
Current children cumulated vsize (Kb) 842396

[startup+670.05 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 254439 0 0 0 64906 988 0 0 25 0 1 0 1844196832 869965824 212084 4294967295 134512640 135167914 3221224448 3221040960 134844751 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27513/statm): 212394 212084 162 162 0 212232 0
[pid=27513] vsize: 849576
Current children cumulated CPU time (s) 659.06
Current children cumulated vsize (Kb) 851704

[startup+680.051 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 257324 0 0 0 65875 1002 0 0 25 0 1 0 1844196832 881782784 214969 4294967295 134512640 135167914 3221224448 3221036444 134842996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27513/statm): 215279 214969 162 162 0 215117 0
[pid=27513] vsize: 861116
Current children cumulated CPU time (s) 668.89
Current children cumulated vsize (Kb) 863244

[startup+690.051 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 259681 0 0 0 66850 1012 0 0 25 0 1 0 1844196832 891387904 217326 4294967295 134512640 135167914 3221224448 3221054304 134845881 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27513/statm): 217624 217326 162 162 0 217462 0
[pid=27513] vsize: 870496
Current children cumulated CPU time (s) 678.74
Current children cumulated vsize (Kb) 872624

[startup+700.052 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 262128 0 0 0 67822 1022 0 0 25 0 1 0 1844196832 901373952 219773 4294967295 134512640 135167914 3221224448 3221062752 134849201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27513/statm): 220062 219773 162 162 0 219900 0
[pid=27513] vsize: 880248
Current children cumulated CPU time (s) 688.56
Current children cumulated vsize (Kb) 882376

[startup+710.054 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 264479 0 0 0 68795 1033 0 0 25 0 1 0 1844196832 911003648 222124 4294967295 134512640 135167914 3221224448 3221041764 134843000 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27513/statm): 222413 222124 162 162 0 222251 0
[pid=27513] vsize: 889652
Current children cumulated CPU time (s) 698.4
Current children cumulated vsize (Kb) 891780

[startup+720.053 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 266822 0 0 0 69769 1043 0 0 25 0 1 0 1844196832 920600576 224467 4294967295 134512640 135167914 3221224448 3221046652 134693552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27513/statm): 224756 224467 162 162 0 224594 0
[pid=27513] vsize: 899024
Current children cumulated CPU time (s) 708.24
Current children cumulated vsize (Kb) 901152

[startup+730.054 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 269276 0 0 0 70742 1056 0 0 25 0 1 0 1844196832 930635776 226921 4294967295 134512640 135167914 3221224448 3221063924 134697276 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27513/statm): 227206 226921 162 162 0 227044 0
[pid=27513] vsize: 908824
Current children cumulated CPU time (s) 718.1
Current children cumulated vsize (Kb) 910952

[startup+740.055 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 271624 0 8 0 71710 1070 0 0 25 0 1 0 1844196832 940187648 229150 4294967295 134512640 135167914 3221224448 3221065568 134619209 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27513/statm): 229538 229150 162 162 0 229376 0
[pid=27513] vsize: 918152
Current children cumulated CPU time (s) 727.92
Current children cumulated vsize (Kb) 920280



Mem limit exceeded: sending SIGTERM then SIGKILL

[startup+741.561 s]
Raw data (loadavg): 1.00 0.98 0.91 1/57 27513
Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27508/statm): 532 234 485 147 0 385 0
[pid=27508] vsize: 2128
Raw data (/proc/27513/stat): 27513 (minisat+_bignum) T 27508 27508 20728 0 -1 0 271987 0 15 0 71853 1071 0 0 25 0 1 0 1844196832 941543424 229475 4294967295 134512640 135167914 3221224448 3221040444 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/27513/statm): 229869 229475 162 162 0 229707 0
[pid=27513] vsize: 919476
Current children cumulated CPU time (s) 729.36
Current children cumulated vsize (Kb) 921604

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

Child status: 0
Real time (s): 741.995
CPU time (s): 729.671
CPU user time (s): 718.532
CPU system time (s): 11.1393
CPU usage (%): 98.339
Max. virtual memory (cumulated for all children) (Kb): 921604

Verifier Data

ERROR: no interpretation found !